let A be non degenerated commutative Ring; for I, J being Ideal of A holds sqrt (I + J) = sqrt ((sqrt I) + (sqrt J))
let I, J be Ideal of A; sqrt (I + J) = sqrt ((sqrt I) + (sqrt J))
A1:
for o being object st o in sqrt (I + J) holds
o in sqrt ((sqrt I) + (sqrt J))
proof
let o be
object ;
( o in sqrt (I + J) implies o in sqrt ((sqrt I) + (sqrt J)) )
assume
o in sqrt (I + J)
;
o in sqrt ((sqrt I) + (sqrt J))
then
o in { a where a is Element of A : ex n being Element of NAT st a |^ n in I + J }
by 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 m1 being
Element of
NAT such that A5:
o1 |^ m1 in I + J
by A4;
o1 |^ m1 in { (a + b) where a, b is Element of A : ( a in I & b in J ) }
by A5, IDEAL_1:def 19;
then consider a1,
b1 being
Element of
A such that A6:
o1 |^ m1 = a1 + b1
and A7:
a1 in I
and A8:
b1 in J
;
A9:
I c= sqrt I
by TOPZARI1:20;
A10:
J c= sqrt J
by TOPZARI1:20;
A11:
a1 + b1 in { (a + b) where a, b is Element of A : ( a in sqrt I & b in sqrt J ) }
by A7, A9, A8, A10;
o1 |^ m1 in (sqrt I) + (sqrt J)
by A6, A11, IDEAL_1:def 19;
then
o1 in { a where a is Element of A : ex n being Element of NAT st a |^ n in (sqrt I) + (sqrt J) }
;
hence
o in sqrt ((sqrt I) + (sqrt J))
by A3, IDEAL_1:def 24;
verum
end;
sqrt ((sqrt I) + (sqrt J)) c= sqrt (I + J)
proof
let o be
object ;
TARSKI:def 3 ( not o in sqrt ((sqrt I) + (sqrt J)) or o in sqrt (I + J) )
assume
o in sqrt ((sqrt I) + (sqrt J))
;
o in sqrt (I + J)
then
o in { a where a is Element of A : ex n being Element of NAT st a |^ n in (sqrt I) + (sqrt J) }
by IDEAL_1:def 24;
then consider o1 being
Element of
A such that A14:
o1 = o
and A15:
ex
n being
Element of
NAT st
o1 |^ n in (sqrt I) + (sqrt J)
;
consider m1 being
Element of
NAT such that A16:
o1 |^ m1 in (sqrt I) + (sqrt J)
by A15;
o1 |^ m1 in { (a + b) where a, b is Element of A : ( a in sqrt I & b in sqrt J ) }
by A16, IDEAL_1:def 19;
then consider a1,
b1 being
Element of
A such that A17:
o1 |^ m1 = a1 + b1
and A18:
a1 in sqrt I
and A19:
b1 in sqrt J
;
a1 in { a where a is Element of A : ex n being Element of NAT st a |^ n in I }
by A18, IDEAL_1:def 24;
then consider a2 being
Element of
A such that A20:
a2 = a1
and A21:
ex
n being
Element of
NAT st
a2 |^ n in I
;
consider n2 being
Element of
NAT such that A22:
a2 |^ n2 in I
by A21;
b1 in { a where a is Element of A : ex n being Element of NAT st a |^ n in J }
by A19, IDEAL_1:def 24;
then consider b2 being
Element of
A such that A23:
b2 = b1
and A24:
ex
m being
Element of
NAT st
b2 |^ m in J
;
consider m2 being
Element of
NAT such that A25:
b2 |^ m2 in J
by A24;
set p = (
a2,
b2)
In_Power (n2 + m2);
consider f being
sequence of the
carrier of
A such that A26:
Sum ((a2,b2) In_Power (n2 + m2)) = f . (len ((a2,b2) In_Power (n2 + m2)))
and A27:
f . 0 = 0. A
and A28:
for
j being
Nat for
v being
Element of
A st
j < len ((a2,b2) In_Power (n2 + m2)) &
v = ((a2,b2) In_Power (n2 + m2)) . (j + 1) holds
f . (j + 1) = (f . j) + v
by RLVECT_1:def 12;
defpred S1[
Element of
NAT ]
means f . $1
in I + J;
A29:
for
i being
Element of
NAT st 1
<= i &
i <= len ((a2,b2) In_Power (n2 + m2)) holds
((a2,b2) In_Power (n2 + m2)) . i in I + J
proof
let i be
Element of
NAT ;
( 1 <= i & i <= len ((a2,b2) In_Power (n2 + m2)) implies ((a2,b2) In_Power (n2 + m2)) . i in I + J )
assume that A30:
1
<= i
and A31:
i <= len ((a2,b2) In_Power (n2 + m2))
;
((a2,b2) In_Power (n2 + m2)) . i in I + J
set r =
i - 1;
set l =
(n2 + m2) - (i - 1);
1
- 1
<= i - 1
by A30, XREAL_1:9;
then reconsider r =
i - 1 as
Element of
NAT by INT_1:3;
i <= (n2 + m2) + 1
by A31, BINOM:def 7;
then
r <= ((n2 + m2) + 1) - 1
by XREAL_1:9;
then
r - r <= (n2 + m2) - r
by XREAL_1:9;
then reconsider l =
(n2 + m2) - (i - 1) as
Element of
NAT by INT_1:3;
i in Seg (len ((a2,b2) In_Power (n2 + m2)))
by A30, A31;
then A32:
i in dom ((a2,b2) In_Power (n2 + m2))
by FINSEQ_1:def 3;
then A33:
((a2,b2) In_Power (n2 + m2)) . i =
((a2,b2) In_Power (n2 + m2)) /. i
by PARTFUN1:def 6
.=
(((n2 + m2) choose r) * (a2 |^ l)) * (b2 |^ r)
by A32, BINOM:def 7
;
end;
A38:
now for j being Element of NAT st 0 <= j & j < len ((a2,b2) In_Power (n2 + m2)) & S1[j] holds
S1[j + 1]let j be
Element of
NAT ;
( 0 <= j & j < len ((a2,b2) In_Power (n2 + m2)) & S1[j] implies S1[j + 1] )assume that
0 <= j
and A39:
j < len ((a2,b2) In_Power (n2 + m2))
;
( S1[j] implies S1[j + 1] )thus
(
S1[
j] implies
S1[
j + 1] )
verumproof
assume A40:
f . j in I + J
;
S1[j + 1]
A41:
j + 1
<= len ((a2,b2) In_Power (n2 + m2))
by A39, NAT_1:13;
1
<= j + 1
by NAT_1:11;
then
j + 1
in Seg (len ((a2,b2) In_Power (n2 + m2)))
by A41;
then
j + 1
in dom ((a2,b2) In_Power (n2 + m2))
by FINSEQ_1:def 3;
then A42:
((a2,b2) In_Power (n2 + m2)) /. (j + 1) = ((a2,b2) In_Power (n2 + m2)) . (j + 1)
by PARTFUN1:def 6;
then A43:
((a2,b2) In_Power (n2 + m2)) /. (j + 1) in I + J
by A29, A41, NAT_1:11;
f . (j + 1) = (f . j) + (((a2,b2) In_Power (n2 + m2)) /. (j + 1))
by A28, A39, A42;
hence
S1[
j + 1]
by A40, A43, IDEAL_1:def 1;
verum
end; end;
A44:
(a2 + b2) |^ (n2 + m2) = Sum ((a2,b2) In_Power (n2 + m2))
by BINOM:25;
A45:
S1[
0 ]
by A27, IDEAL_1:2;
A46:
for
i being
Element of
NAT st
0 <= i &
i <= len ((a2,b2) In_Power (n2 + m2)) holds
S1[
i]
from INT_1:sch 7(A45, A38);
A47:
(o1 |^ m1) |^ (n2 + m2) in I + J
by A17, A23, A20, A44, A26, A46;
reconsider n0 =
m1 * (n2 + m2) as
Element of
NAT ;
A48:
o1 |^ n0 in I + J
by A47, BINOM:11;
o1 in { a where a is Element of A : ex n being Element of NAT st a |^ n in I + J }
by A48;
hence
o in sqrt (I + J)
by A14, IDEAL_1:def 24;
verum
end;
hence
sqrt (I + J) = sqrt ((sqrt I) + (sqrt J))
by A1, TARSKI:2; verum