let A be non degenerated commutative Ring; :: thesis: for p being prime Ideal of A
for q1, q2 being Ideal of A st q1 in PRIMARY (A,p) & q2 in PRIMARY (A,p) holds
q1 /\ q2 in PRIMARY (A,p)
let p be prime Ideal of A; :: thesis: for q1, q2 being Ideal of A st q1 in PRIMARY (A,p) & q2 in PRIMARY (A,p) holds
q1 /\ q2 in PRIMARY (A,p)
let q1, q2 be Ideal of A; :: thesis: ( q1 in PRIMARY (A,p) & q2 in PRIMARY (A,p) implies q1 /\ q2 in PRIMARY (A,p) )
set M = { I where I is primary Ideal of A : I is p -primary } ;
assume A1: ( q1 in PRIMARY (A,p) & q2 in PRIMARY (A,p) ) ; :: thesis: q1 /\ q2 in PRIMARY (A,p)
then consider Q1 being primary Ideal of A such that
A2: Q1 = q1 and
A3: Q1 is p -primary ;
A4: Q1 <> [#] A ;
consider Q2 being primary Ideal of A such that
A5: Q2 = q2 and
A6: Q2 is p -primary by A1;
set Q3 = Q1 /\ Q2;
A7: sqrt (Q1 /\ Q2) = (sqrt Q1) /\ (sqrt Q2) by Th12;
A8: Q1 /\ Q2 <> [#] A by A4, XBOOLE_1:17;
A9: for x, y being Element of A st x * y in Q1 /\ Q2 & not x in Q1 /\ Q2 holds
y in sqrt (Q1 /\ Q2)
proof
let x, y be Element of A; :: thesis: ( x * y in Q1 /\ Q2 & not x in Q1 /\ Q2 implies y in sqrt (Q1 /\ Q2) )
assume A10: ( x * y in Q1 /\ Q2 & not x in Q1 /\ Q2 ) ; :: thesis: y in sqrt (Q1 /\ Q2)
assume not y in sqrt (Q1 /\ Q2) ; :: thesis: contradiction
then A12: not y in (sqrt Q1) /\ (sqrt Q2) by Th12;
per cases ( ( x * y in Q1 /\ Q2 & not x in Q1 ) or ( x * y in Q1 /\ Q2 & not x in Q2 ) ) by A10, XBOOLE_0:def 4;
suppose ( x * y in Q1 /\ Q2 & not x in Q1 ) ; :: thesis: contradiction
then ( x * y in Q1 & not x in Q1 ) by XBOOLE_0:def 4;
hence contradiction by A3, A6, A12, Def4; :: thesis: verum
end;
suppose ( x * y in Q1 /\ Q2 & not x in Q2 ) ; :: thesis: contradiction
then ( x * y in Q2 & not x in Q2 ) by XBOOLE_0:def 4;
hence contradiction by A3, A6, A12, Def4; :: thesis: verum
end;
end;
end;
reconsider Q3 = Q1 /\ Q2 as primary Ideal of A by A9, A8, Th33;
Q3 is p -primary by A3, A6, A7;
hence q1 /\ q2 in PRIMARY (A,p) by A2, A5; :: thesis: verum