let R be domRing; :: thesis: for n being non empty Ordinal
for V being non empty Algebraic_Set of n,R holds
( V is irreducible iff Ideal_ V is prime Ideal of (Polynom-Ring (n,R)) )
let n be non empty Ordinal; :: thesis: for V being non empty Algebraic_Set of n,R holds
( V is irreducible iff Ideal_ V is prime Ideal of (Polynom-Ring (n,R)) )
let V be non empty Algebraic_Set of n,R; :: thesis: ( V is irreducible iff Ideal_ V is prime Ideal of (Polynom-Ring (n,R)) )
A1: ( Ideal_ V is prime Ideal of (Polynom-Ring (n,R)) implies V is irreducible )

proof

assume A2: Ideal_ V is prime Ideal of (Polynom-Ring (n,R)) ; :: thesis: V is irreducible
assume not V is irreducible ; :: thesis: contradiction
then consider V1, V2 being Algebraic_Set of n,R such that
A4: ( V = V1 \/ V2 & V1 c< V & V2 c< V ) ;
consider o1 being object such that
A5: ( o1 in Ideal_ V1 & not o1 in Ideal_ V ) by A4, Th38, XBOOLE_0:6;
consider o2 being object such that
A6: ( o2 in Ideal_ V2 & not o2 in Ideal_ V ) by A4, Th38, XBOOLE_0:6;
reconsider f1 = o1, f2 = o2 as Element of (Polynom-Ring (n,R)) by A6, A5;
reconsider p1 = o1, p2 = o2 as Polynomial of n,R by A6, A5, POLYNOM1:def 11;
A7: Zero_ (p1 *' p2) = Zero_ {(p1 *' p2)} by Th15
.= (Zero_ {p1}) \/ (Zero_ {p2}) by Th21 ;
( Zero_ (Ideal_ V1) c= Zero_ {p1} & Zero_ (Ideal_ V2) c= Zero_ {p2} ) by A5, A6, ZFMISC_1:31, Th16;
then A8: ( V1 c= Zero_ {p1} & V2 c= Zero_ {p2} ) by Th36;
V c= Zero_ (p1 *' p2) by A7, A8, A4, XBOOLE_1:13;
then p1 *' p2 in Ideal_ V ;
then A9: f1 * f2 in Ideal_ V by POLYNOM1:def 11;
Ideal_ V is quasi-prime by A2;
hence contradiction by A9, A5, A6; :: thesis: verum

end;

( V is irreducible implies Ideal_ V is prime Ideal of (Polynom-Ring (n,R)) )

proof

assume A10: V is irreducible ; :: thesis: Ideal_ V is prime Ideal of (Polynom-Ring (n,R))
A11: Ideal_ V <> [#] (Polynom-Ring (n,R)) by Th30;
assume Ideal_ V is not prime Ideal of (Polynom-Ring (n,R)) ; :: thesis: contradiction
then ( not Ideal_ V is proper or not Ideal_ V is quasi-prime ) ;
then consider f1, f2 being Element of (Polynom-Ring (n,R)) such that
A14: ( f1 * f2 in Ideal_ V & not f1 in Ideal_ V & not f2 in Ideal_ V ) by A11;
( f1 in Polynom-Ring (n,R) & f2 in Polynom-Ring (n,R) ) by SUBSET_1:def 1;
then reconsider p1 = f1, p2 = f2 as Polynomial of n,R by POLYNOM1:def 11;
consider g being Polynomial of n,R such that
A15: ( f1 * f2 = g & V c= Zero_ g ) by A14;
A16: g = p1 *' p2 by A15, POLYNOM1:def 11;
A17: (Zero_ {p1}) \/ (Zero_ {p2}) = Zero_ {(p1 *' p2)} by Th21
.= Zero_ (p1 *' p2) by Th15 ;
A18: V c/= Zero_ {p1}

proof

assume V c= Zero_ {p1} ; :: thesis: contradiction
then A20: Ideal_ (Zero_ {p1}) c= Ideal_ V by Th29;
{p1} c= Ideal_ (Zero_ {p1}) by Th32;
hence contradiction by A14, ZFMISC_1:31, A20; :: thesis: verum

end;

A21: V c/= Zero_ {p2}

proof

assume V c= Zero_ {p2} ; :: thesis: contradiction
then A23: Ideal_ (Zero_ {p2}) c= Ideal_ V by Th29;
{p2} c= Ideal_ (Zero_ {p2}) by Th32;
hence contradiction by A14, ZFMISC_1:31, A23; :: thesis: verum

end;

A24: ( V /\ (Zero_ {p1}) c= V & V /\ (Zero_ {p2}) c= V ) by XBOOLE_1:17;
A27: ( V /\ (Zero_ {p1}) c< V & V /\ (Zero_ {p2}) c< V ) by A18, A21, XBOOLE_1:18;
V c= (V /\ (Zero_ {p1})) \/ (V /\ (Zero_ {p2}))

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in V or x in (V /\ (Zero_ {p1})) \/ (V /\ (Zero_ {p2})) )
assume A28: x in V ; :: thesis: x in (V /\ (Zero_ {p1})) \/ (V /\ (Zero_ {p2}))
assume not x in (V /\ (Zero_ {p1})) \/ (V /\ (Zero_ {p2})) ; :: thesis: contradiction
then ( not x in V /\ (Zero_ {p1}) & not x in V /\ (Zero_ {p2}) ) by XBOOLE_0:def 3;
then ( not x in Zero_ {p1} & not x in Zero_ {p2} ) by A28, XBOOLE_0:def 4;
hence contradiction by A28, A15, A16, A17, XBOOLE_0:def 3; :: thesis: verum

end;

then A30: V = (V /\ (Zero_ {f1})) \/ (V /\ (Zero_ {f2})) by A24, XBOOLE_1:8;
Zero_ {f1} <> {} by A21, A15, A16, A17, BOOLE:1;
then reconsider Z = Zero_ {f1} as non empty Subset of (Funcs (n,([#] R))) ;
Z = Zero_ ({f1} -Ideal) by Th17;
then A32: Z is algebraic_set_from_ideal ;
Zero_ {f2} <> {} by A15, A16, A17, BOOLE:1, A18;
then reconsider Z = Zero_ {f2} as non empty Subset of (Funcs (n,([#] R))) ;
Z = Zero_ ({f2} -Ideal) by Th17;
then Z is algebraic_set_from_ideal ;
then ( V /\ (Zero_ {f1}) is Algebraic_Set of n,R & V /\ (Zero_ {f2}) is Algebraic_Set of n,R ) by A32, Th19;
hence contradiction by A10, A30, A27; :: thesis: verum

end;

hence ( V is irreducible iff Ideal_ V is prime Ideal of (Polynom-Ring (n,R)) ) by A1; :: thesis: verum