let A be non degenerated commutative Ring; :: thesis: for I, J being Ideal of A holds sqrt (I /\ J) = (sqrt I) /\ (sqrt J)
let I, J be Ideal of A; :: thesis: sqrt (I /\ J) = (sqrt I) /\ (sqrt J)
A1: for o being object st o in sqrt (I /\ J) holds
o in (sqrt I) /\ (sqrt J)
proof
let o be object ; :: thesis: ( o in sqrt (I /\ J) implies o in (sqrt I) /\ (sqrt J) )
assume A2: o in sqrt (I /\ J) ; :: thesis: o in (sqrt I) /\ (sqrt J)
then reconsider o = o as Element of A ;
o in { a where a is Element of A : ex n being Element of NAT st a |^ n in I /\ J } by A2, IDEAL_1:def 24;
then consider o1 being Element of A such that
A3: o1 = o and
A4: ex n being Element of NAT st o1 |^ n in I /\ J ;
consider n1 being Element of NAT such that
A5: o1 |^ n1 in I /\ J by A4;
A6: ( o1 |^ n1 in I & o1 |^ n1 in J ) by A5, XBOOLE_0:def 4;
then o1 in { a where a is Element of A : ex n being Element of NAT st a |^ n in I } ;
then A7: o1 in sqrt I by IDEAL_1:def 24;
o1 in { a where a is Element of A : ex n being Element of NAT st a |^ n in J } by A6;
then o1 in sqrt J by IDEAL_1:def 24;
hence o in (sqrt I) /\ (sqrt J) by A3, A7, XBOOLE_0:def 4; :: thesis: verum
end;
(sqrt I) /\ (sqrt J) c= sqrt (I /\ J)
proof
let o be object ; :: according to TARSKI:def 3 :: thesis: ( not o in (sqrt I) /\ (sqrt J) or o in sqrt (I /\ J) )
assume A9: o in (sqrt I) /\ (sqrt J) ; :: thesis: o in sqrt (I /\ J)
then A10: ( o in sqrt I & o in sqrt J ) by XBOOLE_0:def 4;
reconsider o = o as Element of A by A9;
o in { a where a is Element of A : ex n being Element of NAT st a |^ n in I } by A10, IDEAL_1:def 24;
then consider o1 being Element of A such that
A11: o1 = o and
A12: ex n being Element of NAT st o1 |^ n in I ;
consider n1 being Element of NAT such that
A13: o1 |^ n1 in I by A12;
o in { a where a is Element of A : ex n being Element of NAT st a |^ n in J } by A10, IDEAL_1:def 24;
then consider o2 being Element of A such that
A14: o2 = o and
A15: ex m being Element of NAT st o2 |^ m in J ;
consider m1 being Element of NAT such that
A16: o2 |^ m1 in J by A15;
A17: (o1 |^ n1) * (o1 |^ m1) = o1 |^ (n1 + m1) by BINOM:10;
reconsider n2 = n1 + m1 as Element of NAT ;
( o1 |^ n2 in I & o1 |^ n2 in J ) by A16, A14, A11, IDEAL_1:def 2, A13, A17;
then o1 |^ n2 in I /\ J by XBOOLE_0:def 4;
then o1 in { a where a is Element of A : ex n being Element of NAT st a |^ n in I /\ J } ;
hence o in sqrt (I /\ J) by A11, IDEAL_1:def 24; :: thesis: verum
end;
hence sqrt (I /\ J) = (sqrt I) /\ (sqrt J) by A1, TARSKI:2; :: thesis: verum