Metamath Proof Explorer

Theorem isprmidlc

Description: The predicate "is prime ideal" for commutative rings. Alternate definition for commutative rings. See definition in Lang p. 92. (Contributed by Jeff Madsen, 19-Jun-2010) (Revised by Thierry Arnoux, 12-Jan-2024)

Ref Expression
Hypotheses isprmidlc.1 โŠข ๐ต = ( Base โ€˜ ๐‘… )
isprmidlc.2 โŠข ยท = ( .r โ€˜ ๐‘… )
Assertion isprmidlc ( ๐‘… โˆˆ CRing โ†’ ( ๐‘ƒ โˆˆ ( PrmIdeal โ€˜ ๐‘… ) โ†” ( ๐‘ƒ โˆˆ ( LIdeal โ€˜ ๐‘… ) โˆง ๐‘ƒ โ‰  ๐ต โˆง โˆ€ ๐‘ฅ โˆˆ ๐ต โˆ€ ๐‘ฆ โˆˆ ๐ต ( ( ๐‘ฅ ยท ๐‘ฆ ) โˆˆ ๐‘ƒ โ†’ ( ๐‘ฅ โˆˆ ๐‘ƒ โˆจ ๐‘ฆ โˆˆ ๐‘ƒ ) ) ) ) )

Proof

Step Hyp Ref Expression
1 isprmidlc.1 โŠข ๐ต = ( Base โ€˜ ๐‘… )
2 isprmidlc.2 โŠข ยท = ( .r โ€˜ ๐‘… )
3 crngring โŠข ( ๐‘… โˆˆ CRing โ†’ ๐‘… โˆˆ Ring )
4 prmidlidl โŠข ( ( ๐‘… โˆˆ Ring โˆง ๐‘ƒ โˆˆ ( PrmIdeal โ€˜ ๐‘… ) ) โ†’ ๐‘ƒ โˆˆ ( LIdeal โ€˜ ๐‘… ) )
5 3 4 sylan โŠข ( ( ๐‘… โˆˆ CRing โˆง ๐‘ƒ โˆˆ ( PrmIdeal โ€˜ ๐‘… ) ) โ†’ ๐‘ƒ โˆˆ ( LIdeal โ€˜ ๐‘… ) )
6 1 2 prmidlnr โŠข ( ( ๐‘… โˆˆ Ring โˆง ๐‘ƒ โˆˆ ( PrmIdeal โ€˜ ๐‘… ) ) โ†’ ๐‘ƒ โ‰  ๐ต )
7 3 6 sylan โŠข ( ( ๐‘… โˆˆ CRing โˆง ๐‘ƒ โˆˆ ( PrmIdeal โ€˜ ๐‘… ) ) โ†’ ๐‘ƒ โ‰  ๐ต )
8 3 ad4antr โŠข ( ( ( ( ( ๐‘… โˆˆ CRing โˆง ๐‘ƒ โˆˆ ( PrmIdeal โ€˜ ๐‘… ) ) โˆง ๐‘ฅ โˆˆ ๐ต ) โˆง ๐‘ฆ โˆˆ ๐ต ) โˆง ( ๐‘ฅ ยท ๐‘ฆ ) โˆˆ ๐‘ƒ ) โ†’ ๐‘… โˆˆ Ring )
9 simp-4r โŠข ( ( ( ( ( ๐‘… โˆˆ CRing โˆง ๐‘ƒ โˆˆ ( PrmIdeal โ€˜ ๐‘… ) ) โˆง ๐‘ฅ โˆˆ ๐ต ) โˆง ๐‘ฆ โˆˆ ๐ต ) โˆง ( ๐‘ฅ ยท ๐‘ฆ ) โˆˆ ๐‘ƒ ) โ†’ ๐‘ƒ โˆˆ ( PrmIdeal โ€˜ ๐‘… ) )
10 simpllr โŠข ( ( ( ( ( ๐‘… โˆˆ CRing โˆง ๐‘ƒ โˆˆ ( PrmIdeal โ€˜ ๐‘… ) ) โˆง ๐‘ฅ โˆˆ ๐ต ) โˆง ๐‘ฆ โˆˆ ๐ต ) โˆง ( ๐‘ฅ ยท ๐‘ฆ ) โˆˆ ๐‘ƒ ) โ†’ ๐‘ฅ โˆˆ ๐ต )
11 10 snssd โŠข ( ( ( ( ( ๐‘… โˆˆ CRing โˆง ๐‘ƒ โˆˆ ( PrmIdeal โ€˜ ๐‘… ) ) โˆง ๐‘ฅ โˆˆ ๐ต ) โˆง ๐‘ฆ โˆˆ ๐ต ) โˆง ( ๐‘ฅ ยท ๐‘ฆ ) โˆˆ ๐‘ƒ ) โ†’ { ๐‘ฅ } โŠ† ๐ต )
12 eqid โŠข ( RSpan โ€˜ ๐‘… ) = ( RSpan โ€˜ ๐‘… )
13 eqid โŠข ( LIdeal โ€˜ ๐‘… ) = ( LIdeal โ€˜ ๐‘… )
14 12 1 13 rspcl โŠข ( ( ๐‘… โˆˆ Ring โˆง { ๐‘ฅ } โŠ† ๐ต ) โ†’ ( ( RSpan โ€˜ ๐‘… ) โ€˜ { ๐‘ฅ } ) โˆˆ ( LIdeal โ€˜ ๐‘… ) )
15 8 11 14 syl2anc โŠข ( ( ( ( ( ๐‘… โˆˆ CRing โˆง ๐‘ƒ โˆˆ ( PrmIdeal โ€˜ ๐‘… ) ) โˆง ๐‘ฅ โˆˆ ๐ต ) โˆง ๐‘ฆ โˆˆ ๐ต ) โˆง ( ๐‘ฅ ยท ๐‘ฆ ) โˆˆ ๐‘ƒ ) โ†’ ( ( RSpan โ€˜ ๐‘… ) โ€˜ { ๐‘ฅ } ) โˆˆ ( LIdeal โ€˜ ๐‘… ) )
16 simplr โŠข ( ( ( ( ( ๐‘… โˆˆ CRing โˆง ๐‘ƒ โˆˆ ( PrmIdeal โ€˜ ๐‘… ) ) โˆง ๐‘ฅ โˆˆ ๐ต ) โˆง ๐‘ฆ โˆˆ ๐ต ) โˆง ( ๐‘ฅ ยท ๐‘ฆ ) โˆˆ ๐‘ƒ ) โ†’ ๐‘ฆ โˆˆ ๐ต )
17 16 snssd โŠข ( ( ( ( ( ๐‘… โˆˆ CRing โˆง ๐‘ƒ โˆˆ ( PrmIdeal โ€˜ ๐‘… ) ) โˆง ๐‘ฅ โˆˆ ๐ต ) โˆง ๐‘ฆ โˆˆ ๐ต ) โˆง ( ๐‘ฅ ยท ๐‘ฆ ) โˆˆ ๐‘ƒ ) โ†’ { ๐‘ฆ } โŠ† ๐ต )
18 12 1 13 rspcl โŠข ( ( ๐‘… โˆˆ Ring โˆง { ๐‘ฆ } โŠ† ๐ต ) โ†’ ( ( RSpan โ€˜ ๐‘… ) โ€˜ { ๐‘ฆ } ) โˆˆ ( LIdeal โ€˜ ๐‘… ) )
19 8 17 18 syl2anc โŠข ( ( ( ( ( ๐‘… โˆˆ CRing โˆง ๐‘ƒ โˆˆ ( PrmIdeal โ€˜ ๐‘… ) ) โˆง ๐‘ฅ โˆˆ ๐ต ) โˆง ๐‘ฆ โˆˆ ๐ต ) โˆง ( ๐‘ฅ ยท ๐‘ฆ ) โˆˆ ๐‘ƒ ) โ†’ ( ( RSpan โ€˜ ๐‘… ) โ€˜ { ๐‘ฆ } ) โˆˆ ( LIdeal โ€˜ ๐‘… ) )
20 15 19 jca โŠข ( ( ( ( ( ๐‘… โˆˆ CRing โˆง ๐‘ƒ โˆˆ ( PrmIdeal โ€˜ ๐‘… ) ) โˆง ๐‘ฅ โˆˆ ๐ต ) โˆง ๐‘ฆ โˆˆ ๐ต ) โˆง ( ๐‘ฅ ยท ๐‘ฆ ) โˆˆ ๐‘ƒ ) โ†’ ( ( ( RSpan โ€˜ ๐‘… ) โ€˜ { ๐‘ฅ } ) โˆˆ ( LIdeal โ€˜ ๐‘… ) โˆง ( ( RSpan โ€˜ ๐‘… ) โ€˜ { ๐‘ฆ } ) โˆˆ ( LIdeal โ€˜ ๐‘… ) ) )
21 simpllr โŠข ( ( ( ( ( ( ( ( ( ( ( ๐‘… โˆˆ CRing โˆง ๐‘ƒ โˆˆ ( PrmIdeal โ€˜ ๐‘… ) ) โˆง ๐‘ฅ โˆˆ ๐ต ) โˆง ๐‘ฆ โˆˆ ๐ต ) โˆง ( ๐‘ฅ ยท ๐‘ฆ ) โˆˆ ๐‘ƒ ) โˆง ๐‘Ÿ โˆˆ ( ( RSpan โ€˜ ๐‘… ) โ€˜ { ๐‘ฅ } ) ) โˆง ๐‘  โˆˆ ( ( RSpan โ€˜ ๐‘… ) โ€˜ { ๐‘ฆ } ) ) โˆง ๐‘š โˆˆ ๐ต ) โˆง ๐‘Ÿ = ( ๐‘š ยท ๐‘ฅ ) ) โˆง ๐‘› โˆˆ ๐ต ) โˆง ๐‘  = ( ๐‘› ยท ๐‘ฆ ) ) โ†’ ๐‘Ÿ = ( ๐‘š ยท ๐‘ฅ ) )
22 simpr โŠข ( ( ( ( ( ( ( ( ( ( ( ๐‘… โˆˆ CRing โˆง ๐‘ƒ โˆˆ ( PrmIdeal โ€˜ ๐‘… ) ) โˆง ๐‘ฅ โˆˆ ๐ต ) โˆง ๐‘ฆ โˆˆ ๐ต ) โˆง ( ๐‘ฅ ยท ๐‘ฆ ) โˆˆ ๐‘ƒ ) โˆง ๐‘Ÿ โˆˆ ( ( RSpan โ€˜ ๐‘… ) โ€˜ { ๐‘ฅ } ) ) โˆง ๐‘  โˆˆ ( ( RSpan โ€˜ ๐‘… ) โ€˜ { ๐‘ฆ } ) ) โˆง ๐‘š โˆˆ ๐ต ) โˆง ๐‘Ÿ = ( ๐‘š ยท ๐‘ฅ ) ) โˆง ๐‘› โˆˆ ๐ต ) โˆง ๐‘  = ( ๐‘› ยท ๐‘ฆ ) ) โ†’ ๐‘  = ( ๐‘› ยท ๐‘ฆ ) )
23 21 22 oveq12d โŠข ( ( ( ( ( ( ( ( ( ( ( ๐‘… โˆˆ CRing โˆง ๐‘ƒ โˆˆ ( PrmIdeal โ€˜ ๐‘… ) ) โˆง ๐‘ฅ โˆˆ ๐ต ) โˆง ๐‘ฆ โˆˆ ๐ต ) โˆง ( ๐‘ฅ ยท ๐‘ฆ ) โˆˆ ๐‘ƒ ) โˆง ๐‘Ÿ โˆˆ ( ( RSpan โ€˜ ๐‘… ) โ€˜ { ๐‘ฅ } ) ) โˆง ๐‘  โˆˆ ( ( RSpan โ€˜ ๐‘… ) โ€˜ { ๐‘ฆ } ) ) โˆง ๐‘š โˆˆ ๐ต ) โˆง ๐‘Ÿ = ( ๐‘š ยท ๐‘ฅ ) ) โˆง ๐‘› โˆˆ ๐ต ) โˆง ๐‘  = ( ๐‘› ยท ๐‘ฆ ) ) โ†’ ( ๐‘Ÿ ยท ๐‘  ) = ( ( ๐‘š ยท ๐‘ฅ ) ยท ( ๐‘› ยท ๐‘ฆ ) ) )
24 simp-10l โŠข ( ( ( ( ( ( ( ( ( ( ( ๐‘… โˆˆ CRing โˆง ๐‘ƒ โˆˆ ( PrmIdeal โ€˜ ๐‘… ) ) โˆง ๐‘ฅ โˆˆ ๐ต ) โˆง ๐‘ฆ โˆˆ ๐ต ) โˆง ( ๐‘ฅ ยท ๐‘ฆ ) โˆˆ ๐‘ƒ ) โˆง ๐‘Ÿ โˆˆ ( ( RSpan โ€˜ ๐‘… ) โ€˜ { ๐‘ฅ } ) ) โˆง ๐‘  โˆˆ ( ( RSpan โ€˜ ๐‘… ) โ€˜ { ๐‘ฆ } ) ) โˆง ๐‘š โˆˆ ๐ต ) โˆง ๐‘Ÿ = ( ๐‘š ยท ๐‘ฅ ) ) โˆง ๐‘› โˆˆ ๐ต ) โˆง ๐‘  = ( ๐‘› ยท ๐‘ฆ ) ) โ†’ ๐‘… โˆˆ CRing )
25 simp-4r โŠข ( ( ( ( ( ( ( ( ( ( ( ๐‘… โˆˆ CRing โˆง ๐‘ƒ โˆˆ ( PrmIdeal โ€˜ ๐‘… ) ) โˆง ๐‘ฅ โˆˆ ๐ต ) โˆง ๐‘ฆ โˆˆ ๐ต ) โˆง ( ๐‘ฅ ยท ๐‘ฆ ) โˆˆ ๐‘ƒ ) โˆง ๐‘Ÿ โˆˆ ( ( RSpan โ€˜ ๐‘… ) โ€˜ { ๐‘ฅ } ) ) โˆง ๐‘  โˆˆ ( ( RSpan โ€˜ ๐‘… ) โ€˜ { ๐‘ฆ } ) ) โˆง ๐‘š โˆˆ ๐ต ) โˆง ๐‘Ÿ = ( ๐‘š ยท ๐‘ฅ ) ) โˆง ๐‘› โˆˆ ๐ต ) โˆง ๐‘  = ( ๐‘› ยท ๐‘ฆ ) ) โ†’ ๐‘š โˆˆ ๐ต )
26 10 ad2antrr โŠข ( ( ( ( ( ( ( ๐‘… โˆˆ CRing โˆง ๐‘ƒ โˆˆ ( PrmIdeal โ€˜ ๐‘… ) ) โˆง ๐‘ฅ โˆˆ ๐ต ) โˆง ๐‘ฆ โˆˆ ๐ต ) โˆง ( ๐‘ฅ ยท ๐‘ฆ ) โˆˆ ๐‘ƒ ) โˆง ๐‘Ÿ โˆˆ ( ( RSpan โ€˜ ๐‘… ) โ€˜ { ๐‘ฅ } ) ) โˆง ๐‘  โˆˆ ( ( RSpan โ€˜ ๐‘… ) โ€˜ { ๐‘ฆ } ) ) โ†’ ๐‘ฅ โˆˆ ๐ต )
27 26 ad4antr โŠข ( ( ( ( ( ( ( ( ( ( ( ๐‘… โˆˆ CRing โˆง ๐‘ƒ โˆˆ ( PrmIdeal โ€˜ ๐‘… ) ) โˆง ๐‘ฅ โˆˆ ๐ต ) โˆง ๐‘ฆ โˆˆ ๐ต ) โˆง ( ๐‘ฅ ยท ๐‘ฆ ) โˆˆ ๐‘ƒ ) โˆง ๐‘Ÿ โˆˆ ( ( RSpan โ€˜ ๐‘… ) โ€˜ { ๐‘ฅ } ) ) โˆง ๐‘  โˆˆ ( ( RSpan โ€˜ ๐‘… ) โ€˜ { ๐‘ฆ } ) ) โˆง ๐‘š โˆˆ ๐ต ) โˆง ๐‘Ÿ = ( ๐‘š ยท ๐‘ฅ ) ) โˆง ๐‘› โˆˆ ๐ต ) โˆง ๐‘  = ( ๐‘› ยท ๐‘ฆ ) ) โ†’ ๐‘ฅ โˆˆ ๐ต )
28 simplr โŠข ( ( ( ( ( ( ( ( ( ( ( ๐‘… โˆˆ CRing โˆง ๐‘ƒ โˆˆ ( PrmIdeal โ€˜ ๐‘… ) ) โˆง ๐‘ฅ โˆˆ ๐ต ) โˆง ๐‘ฆ โˆˆ ๐ต ) โˆง ( ๐‘ฅ ยท ๐‘ฆ ) โˆˆ ๐‘ƒ ) โˆง ๐‘Ÿ โˆˆ ( ( RSpan โ€˜ ๐‘… ) โ€˜ { ๐‘ฅ } ) ) โˆง ๐‘  โˆˆ ( ( RSpan โ€˜ ๐‘… ) โ€˜ { ๐‘ฆ } ) ) โˆง ๐‘š โˆˆ ๐ต ) โˆง ๐‘Ÿ = ( ๐‘š ยท ๐‘ฅ ) ) โˆง ๐‘› โˆˆ ๐ต ) โˆง ๐‘  = ( ๐‘› ยท ๐‘ฆ ) ) โ†’ ๐‘› โˆˆ ๐ต )
29 16 ad4antr โŠข ( ( ( ( ( ( ( ( ( ๐‘… โˆˆ CRing โˆง ๐‘ƒ โˆˆ ( PrmIdeal โ€˜ ๐‘… ) ) โˆง ๐‘ฅ โˆˆ ๐ต ) โˆง ๐‘ฆ โˆˆ ๐ต ) โˆง ( ๐‘ฅ ยท ๐‘ฆ ) โˆˆ ๐‘ƒ ) โˆง ๐‘Ÿ โˆˆ ( ( RSpan โ€˜ ๐‘… ) โ€˜ { ๐‘ฅ } ) ) โˆง ๐‘  โˆˆ ( ( RSpan โ€˜ ๐‘… ) โ€˜ { ๐‘ฆ } ) ) โˆง ๐‘š โˆˆ ๐ต ) โˆง ๐‘Ÿ = ( ๐‘š ยท ๐‘ฅ ) ) โ†’ ๐‘ฆ โˆˆ ๐ต )
30 29 ad2antrr โŠข ( ( ( ( ( ( ( ( ( ( ( ๐‘… โˆˆ CRing โˆง ๐‘ƒ โˆˆ ( PrmIdeal โ€˜ ๐‘… ) ) โˆง ๐‘ฅ โˆˆ ๐ต ) โˆง ๐‘ฆ โˆˆ ๐ต ) โˆง ( ๐‘ฅ ยท ๐‘ฆ ) โˆˆ ๐‘ƒ ) โˆง ๐‘Ÿ โˆˆ ( ( RSpan โ€˜ ๐‘… ) โ€˜ { ๐‘ฅ } ) ) โˆง ๐‘  โˆˆ ( ( RSpan โ€˜ ๐‘… ) โ€˜ { ๐‘ฆ } ) ) โˆง ๐‘š โˆˆ ๐ต ) โˆง ๐‘Ÿ = ( ๐‘š ยท ๐‘ฅ ) ) โˆง ๐‘› โˆˆ ๐ต ) โˆง ๐‘  = ( ๐‘› ยท ๐‘ฆ ) ) โ†’ ๐‘ฆ โˆˆ ๐ต )
31 1 2 cringm4 โŠข ( ( ๐‘… โˆˆ CRing โˆง ( ๐‘š โˆˆ ๐ต โˆง ๐‘ฅ โˆˆ ๐ต ) โˆง ( ๐‘› โˆˆ ๐ต โˆง ๐‘ฆ โˆˆ ๐ต ) ) โ†’ ( ( ๐‘š ยท ๐‘ฅ ) ยท ( ๐‘› ยท ๐‘ฆ ) ) = ( ( ๐‘š ยท ๐‘› ) ยท ( ๐‘ฅ ยท ๐‘ฆ ) ) )
32 24 25 27 28 30 31 syl122anc โŠข ( ( ( ( ( ( ( ( ( ( ( ๐‘… โˆˆ CRing โˆง ๐‘ƒ โˆˆ ( PrmIdeal โ€˜ ๐‘… ) ) โˆง ๐‘ฅ โˆˆ ๐ต ) โˆง ๐‘ฆ โˆˆ ๐ต ) โˆง ( ๐‘ฅ ยท ๐‘ฆ ) โˆˆ ๐‘ƒ ) โˆง ๐‘Ÿ โˆˆ ( ( RSpan โ€˜ ๐‘… ) โ€˜ { ๐‘ฅ } ) ) โˆง ๐‘  โˆˆ ( ( RSpan โ€˜ ๐‘… ) โ€˜ { ๐‘ฆ } ) ) โˆง ๐‘š โˆˆ ๐ต ) โˆง ๐‘Ÿ = ( ๐‘š ยท ๐‘ฅ ) ) โˆง ๐‘› โˆˆ ๐ต ) โˆง ๐‘  = ( ๐‘› ยท ๐‘ฆ ) ) โ†’ ( ( ๐‘š ยท ๐‘ฅ ) ยท ( ๐‘› ยท ๐‘ฆ ) ) = ( ( ๐‘š ยท ๐‘› ) ยท ( ๐‘ฅ ยท ๐‘ฆ ) ) )
33 24 3 syl โŠข ( ( ( ( ( ( ( ( ( ( ( ๐‘… โˆˆ CRing โˆง ๐‘ƒ โˆˆ ( PrmIdeal โ€˜ ๐‘… ) ) โˆง ๐‘ฅ โˆˆ ๐ต ) โˆง ๐‘ฆ โˆˆ ๐ต ) โˆง ( ๐‘ฅ ยท ๐‘ฆ ) โˆˆ ๐‘ƒ ) โˆง ๐‘Ÿ โˆˆ ( ( RSpan โ€˜ ๐‘… ) โ€˜ { ๐‘ฅ } ) ) โˆง ๐‘  โˆˆ ( ( RSpan โ€˜ ๐‘… ) โ€˜ { ๐‘ฆ } ) ) โˆง ๐‘š โˆˆ ๐ต ) โˆง ๐‘Ÿ = ( ๐‘š ยท ๐‘ฅ ) ) โˆง ๐‘› โˆˆ ๐ต ) โˆง ๐‘  = ( ๐‘› ยท ๐‘ฆ ) ) โ†’ ๐‘… โˆˆ Ring )
34 5 ad9antr โŠข ( ( ( ( ( ( ( ( ( ( ( ๐‘… โˆˆ CRing โˆง ๐‘ƒ โˆˆ ( PrmIdeal โ€˜ ๐‘… ) ) โˆง ๐‘ฅ โˆˆ ๐ต ) โˆง ๐‘ฆ โˆˆ ๐ต ) โˆง ( ๐‘ฅ ยท ๐‘ฆ ) โˆˆ ๐‘ƒ ) โˆง ๐‘Ÿ โˆˆ ( ( RSpan โ€˜ ๐‘… ) โ€˜ { ๐‘ฅ } ) ) โˆง ๐‘  โˆˆ ( ( RSpan โ€˜ ๐‘… ) โ€˜ { ๐‘ฆ } ) ) โˆง ๐‘š โˆˆ ๐ต ) โˆง ๐‘Ÿ = ( ๐‘š ยท ๐‘ฅ ) ) โˆง ๐‘› โˆˆ ๐ต ) โˆง ๐‘  = ( ๐‘› ยท ๐‘ฆ ) ) โ†’ ๐‘ƒ โˆˆ ( LIdeal โ€˜ ๐‘… ) )
35 1 2 ringcl โŠข ( ( ๐‘… โˆˆ Ring โˆง ๐‘š โˆˆ ๐ต โˆง ๐‘› โˆˆ ๐ต ) โ†’ ( ๐‘š ยท ๐‘› ) โˆˆ ๐ต )
36 33 25 28 35 syl3anc โŠข ( ( ( ( ( ( ( ( ( ( ( ๐‘… โˆˆ CRing โˆง ๐‘ƒ โˆˆ ( PrmIdeal โ€˜ ๐‘… ) ) โˆง ๐‘ฅ โˆˆ ๐ต ) โˆง ๐‘ฆ โˆˆ ๐ต ) โˆง ( ๐‘ฅ ยท ๐‘ฆ ) โˆˆ ๐‘ƒ ) โˆง ๐‘Ÿ โˆˆ ( ( RSpan โ€˜ ๐‘… ) โ€˜ { ๐‘ฅ } ) ) โˆง ๐‘  โˆˆ ( ( RSpan โ€˜ ๐‘… ) โ€˜ { ๐‘ฆ } ) ) โˆง ๐‘š โˆˆ ๐ต ) โˆง ๐‘Ÿ = ( ๐‘š ยท ๐‘ฅ ) ) โˆง ๐‘› โˆˆ ๐ต ) โˆง ๐‘  = ( ๐‘› ยท ๐‘ฆ ) ) โ†’ ( ๐‘š ยท ๐‘› ) โˆˆ ๐ต )
37 simp-7r โŠข ( ( ( ( ( ( ( ( ( ( ( ๐‘… โˆˆ CRing โˆง ๐‘ƒ โˆˆ ( PrmIdeal โ€˜ ๐‘… ) ) โˆง ๐‘ฅ โˆˆ ๐ต ) โˆง ๐‘ฆ โˆˆ ๐ต ) โˆง ( ๐‘ฅ ยท ๐‘ฆ ) โˆˆ ๐‘ƒ ) โˆง ๐‘Ÿ โˆˆ ( ( RSpan โ€˜ ๐‘… ) โ€˜ { ๐‘ฅ } ) ) โˆง ๐‘  โˆˆ ( ( RSpan โ€˜ ๐‘… ) โ€˜ { ๐‘ฆ } ) ) โˆง ๐‘š โˆˆ ๐ต ) โˆง ๐‘Ÿ = ( ๐‘š ยท ๐‘ฅ ) ) โˆง ๐‘› โˆˆ ๐ต ) โˆง ๐‘  = ( ๐‘› ยท ๐‘ฆ ) ) โ†’ ( ๐‘ฅ ยท ๐‘ฆ ) โˆˆ ๐‘ƒ )
38 13 1 2 lidlmcl โŠข ( ( ( ๐‘… โˆˆ Ring โˆง ๐‘ƒ โˆˆ ( LIdeal โ€˜ ๐‘… ) ) โˆง ( ( ๐‘š ยท ๐‘› ) โˆˆ ๐ต โˆง ( ๐‘ฅ ยท ๐‘ฆ ) โˆˆ ๐‘ƒ ) ) โ†’ ( ( ๐‘š ยท ๐‘› ) ยท ( ๐‘ฅ ยท ๐‘ฆ ) ) โˆˆ ๐‘ƒ )
39 33 34 36 37 38 syl22anc โŠข ( ( ( ( ( ( ( ( ( ( ( ๐‘… โˆˆ CRing โˆง ๐‘ƒ โˆˆ ( PrmIdeal โ€˜ ๐‘… ) ) โˆง ๐‘ฅ โˆˆ ๐ต ) โˆง ๐‘ฆ โˆˆ ๐ต ) โˆง ( ๐‘ฅ ยท ๐‘ฆ ) โˆˆ ๐‘ƒ ) โˆง ๐‘Ÿ โˆˆ ( ( RSpan โ€˜ ๐‘… ) โ€˜ { ๐‘ฅ } ) ) โˆง ๐‘  โˆˆ ( ( RSpan โ€˜ ๐‘… ) โ€˜ { ๐‘ฆ } ) ) โˆง ๐‘š โˆˆ ๐ต ) โˆง ๐‘Ÿ = ( ๐‘š ยท ๐‘ฅ ) ) โˆง ๐‘› โˆˆ ๐ต ) โˆง ๐‘  = ( ๐‘› ยท ๐‘ฆ ) ) โ†’ ( ( ๐‘š ยท ๐‘› ) ยท ( ๐‘ฅ ยท ๐‘ฆ ) ) โˆˆ ๐‘ƒ )
40 32 39 eqeltrd โŠข ( ( ( ( ( ( ( ( ( ( ( ๐‘… โˆˆ CRing โˆง ๐‘ƒ โˆˆ ( PrmIdeal โ€˜ ๐‘… ) ) โˆง ๐‘ฅ โˆˆ ๐ต ) โˆง ๐‘ฆ โˆˆ ๐ต ) โˆง ( ๐‘ฅ ยท ๐‘ฆ ) โˆˆ ๐‘ƒ ) โˆง ๐‘Ÿ โˆˆ ( ( RSpan โ€˜ ๐‘… ) โ€˜ { ๐‘ฅ } ) ) โˆง ๐‘  โˆˆ ( ( RSpan โ€˜ ๐‘… ) โ€˜ { ๐‘ฆ } ) ) โˆง ๐‘š โˆˆ ๐ต ) โˆง ๐‘Ÿ = ( ๐‘š ยท ๐‘ฅ ) ) โˆง ๐‘› โˆˆ ๐ต ) โˆง ๐‘  = ( ๐‘› ยท ๐‘ฆ ) ) โ†’ ( ( ๐‘š ยท ๐‘ฅ ) ยท ( ๐‘› ยท ๐‘ฆ ) ) โˆˆ ๐‘ƒ )
41 23 40 eqeltrd โŠข ( ( ( ( ( ( ( ( ( ( ( ๐‘… โˆˆ CRing โˆง ๐‘ƒ โˆˆ ( PrmIdeal โ€˜ ๐‘… ) ) โˆง ๐‘ฅ โˆˆ ๐ต ) โˆง ๐‘ฆ โˆˆ ๐ต ) โˆง ( ๐‘ฅ ยท ๐‘ฆ ) โˆˆ ๐‘ƒ ) โˆง ๐‘Ÿ โˆˆ ( ( RSpan โ€˜ ๐‘… ) โ€˜ { ๐‘ฅ } ) ) โˆง ๐‘  โˆˆ ( ( RSpan โ€˜ ๐‘… ) โ€˜ { ๐‘ฆ } ) ) โˆง ๐‘š โˆˆ ๐ต ) โˆง ๐‘Ÿ = ( ๐‘š ยท ๐‘ฅ ) ) โˆง ๐‘› โˆˆ ๐ต ) โˆง ๐‘  = ( ๐‘› ยท ๐‘ฆ ) ) โ†’ ( ๐‘Ÿ ยท ๐‘  ) โˆˆ ๐‘ƒ )
42 8 ad2antrr โŠข ( ( ( ( ( ( ( ๐‘… โˆˆ CRing โˆง ๐‘ƒ โˆˆ ( PrmIdeal โ€˜ ๐‘… ) ) โˆง ๐‘ฅ โˆˆ ๐ต ) โˆง ๐‘ฆ โˆˆ ๐ต ) โˆง ( ๐‘ฅ ยท ๐‘ฆ ) โˆˆ ๐‘ƒ ) โˆง ๐‘Ÿ โˆˆ ( ( RSpan โ€˜ ๐‘… ) โ€˜ { ๐‘ฅ } ) ) โˆง ๐‘  โˆˆ ( ( RSpan โ€˜ ๐‘… ) โ€˜ { ๐‘ฆ } ) ) โ†’ ๐‘… โˆˆ Ring )
43 42 ad2antrr โŠข ( ( ( ( ( ( ( ( ( ๐‘… โˆˆ CRing โˆง ๐‘ƒ โˆˆ ( PrmIdeal โ€˜ ๐‘… ) ) โˆง ๐‘ฅ โˆˆ ๐ต ) โˆง ๐‘ฆ โˆˆ ๐ต ) โˆง ( ๐‘ฅ ยท ๐‘ฆ ) โˆˆ ๐‘ƒ ) โˆง ๐‘Ÿ โˆˆ ( ( RSpan โ€˜ ๐‘… ) โ€˜ { ๐‘ฅ } ) ) โˆง ๐‘  โˆˆ ( ( RSpan โ€˜ ๐‘… ) โ€˜ { ๐‘ฆ } ) ) โˆง ๐‘š โˆˆ ๐ต ) โˆง ๐‘Ÿ = ( ๐‘š ยท ๐‘ฅ ) ) โ†’ ๐‘… โˆˆ Ring )
44 simpllr โŠข ( ( ( ( ( ( ( ( ( ๐‘… โˆˆ CRing โˆง ๐‘ƒ โˆˆ ( PrmIdeal โ€˜ ๐‘… ) ) โˆง ๐‘ฅ โˆˆ ๐ต ) โˆง ๐‘ฆ โˆˆ ๐ต ) โˆง ( ๐‘ฅ ยท ๐‘ฆ ) โˆˆ ๐‘ƒ ) โˆง ๐‘Ÿ โˆˆ ( ( RSpan โ€˜ ๐‘… ) โ€˜ { ๐‘ฅ } ) ) โˆง ๐‘  โˆˆ ( ( RSpan โ€˜ ๐‘… ) โ€˜ { ๐‘ฆ } ) ) โˆง ๐‘š โˆˆ ๐ต ) โˆง ๐‘Ÿ = ( ๐‘š ยท ๐‘ฅ ) ) โ†’ ๐‘  โˆˆ ( ( RSpan โ€˜ ๐‘… ) โ€˜ { ๐‘ฆ } ) )
45 1 2 12 rspsnel โŠข ( ( ๐‘… โˆˆ Ring โˆง ๐‘ฆ โˆˆ ๐ต ) โ†’ ( ๐‘  โˆˆ ( ( RSpan โ€˜ ๐‘… ) โ€˜ { ๐‘ฆ } ) โ†” โˆƒ ๐‘› โˆˆ ๐ต ๐‘  = ( ๐‘› ยท ๐‘ฆ ) ) )
46 45 biimpa โŠข ( ( ( ๐‘… โˆˆ Ring โˆง ๐‘ฆ โˆˆ ๐ต ) โˆง ๐‘  โˆˆ ( ( RSpan โ€˜ ๐‘… ) โ€˜ { ๐‘ฆ } ) ) โ†’ โˆƒ ๐‘› โˆˆ ๐ต ๐‘  = ( ๐‘› ยท ๐‘ฆ ) )
47 43 29 44 46 syl21anc โŠข ( ( ( ( ( ( ( ( ( ๐‘… โˆˆ CRing โˆง ๐‘ƒ โˆˆ ( PrmIdeal โ€˜ ๐‘… ) ) โˆง ๐‘ฅ โˆˆ ๐ต ) โˆง ๐‘ฆ โˆˆ ๐ต ) โˆง ( ๐‘ฅ ยท ๐‘ฆ ) โˆˆ ๐‘ƒ ) โˆง ๐‘Ÿ โˆˆ ( ( RSpan โ€˜ ๐‘… ) โ€˜ { ๐‘ฅ } ) ) โˆง ๐‘  โˆˆ ( ( RSpan โ€˜ ๐‘… ) โ€˜ { ๐‘ฆ } ) ) โˆง ๐‘š โˆˆ ๐ต ) โˆง ๐‘Ÿ = ( ๐‘š ยท ๐‘ฅ ) ) โ†’ โˆƒ ๐‘› โˆˆ ๐ต ๐‘  = ( ๐‘› ยท ๐‘ฆ ) )
48 41 47 r19.29a โŠข ( ( ( ( ( ( ( ( ( ๐‘… โˆˆ CRing โˆง ๐‘ƒ โˆˆ ( PrmIdeal โ€˜ ๐‘… ) ) โˆง ๐‘ฅ โˆˆ ๐ต ) โˆง ๐‘ฆ โˆˆ ๐ต ) โˆง ( ๐‘ฅ ยท ๐‘ฆ ) โˆˆ ๐‘ƒ ) โˆง ๐‘Ÿ โˆˆ ( ( RSpan โ€˜ ๐‘… ) โ€˜ { ๐‘ฅ } ) ) โˆง ๐‘  โˆˆ ( ( RSpan โ€˜ ๐‘… ) โ€˜ { ๐‘ฆ } ) ) โˆง ๐‘š โˆˆ ๐ต ) โˆง ๐‘Ÿ = ( ๐‘š ยท ๐‘ฅ ) ) โ†’ ( ๐‘Ÿ ยท ๐‘  ) โˆˆ ๐‘ƒ )
49 simplr โŠข ( ( ( ( ( ( ( ๐‘… โˆˆ CRing โˆง ๐‘ƒ โˆˆ ( PrmIdeal โ€˜ ๐‘… ) ) โˆง ๐‘ฅ โˆˆ ๐ต ) โˆง ๐‘ฆ โˆˆ ๐ต ) โˆง ( ๐‘ฅ ยท ๐‘ฆ ) โˆˆ ๐‘ƒ ) โˆง ๐‘Ÿ โˆˆ ( ( RSpan โ€˜ ๐‘… ) โ€˜ { ๐‘ฅ } ) ) โˆง ๐‘  โˆˆ ( ( RSpan โ€˜ ๐‘… ) โ€˜ { ๐‘ฆ } ) ) โ†’ ๐‘Ÿ โˆˆ ( ( RSpan โ€˜ ๐‘… ) โ€˜ { ๐‘ฅ } ) )
50 1 2 12 rspsnel โŠข ( ( ๐‘… โˆˆ Ring โˆง ๐‘ฅ โˆˆ ๐ต ) โ†’ ( ๐‘Ÿ โˆˆ ( ( RSpan โ€˜ ๐‘… ) โ€˜ { ๐‘ฅ } ) โ†” โˆƒ ๐‘š โˆˆ ๐ต ๐‘Ÿ = ( ๐‘š ยท ๐‘ฅ ) ) )
51 50 biimpa โŠข ( ( ( ๐‘… โˆˆ Ring โˆง ๐‘ฅ โˆˆ ๐ต ) โˆง ๐‘Ÿ โˆˆ ( ( RSpan โ€˜ ๐‘… ) โ€˜ { ๐‘ฅ } ) ) โ†’ โˆƒ ๐‘š โˆˆ ๐ต ๐‘Ÿ = ( ๐‘š ยท ๐‘ฅ ) )
52 42 26 49 51 syl21anc โŠข ( ( ( ( ( ( ( ๐‘… โˆˆ CRing โˆง ๐‘ƒ โˆˆ ( PrmIdeal โ€˜ ๐‘… ) ) โˆง ๐‘ฅ โˆˆ ๐ต ) โˆง ๐‘ฆ โˆˆ ๐ต ) โˆง ( ๐‘ฅ ยท ๐‘ฆ ) โˆˆ ๐‘ƒ ) โˆง ๐‘Ÿ โˆˆ ( ( RSpan โ€˜ ๐‘… ) โ€˜ { ๐‘ฅ } ) ) โˆง ๐‘  โˆˆ ( ( RSpan โ€˜ ๐‘… ) โ€˜ { ๐‘ฆ } ) ) โ†’ โˆƒ ๐‘š โˆˆ ๐ต ๐‘Ÿ = ( ๐‘š ยท ๐‘ฅ ) )
53 48 52 r19.29a โŠข ( ( ( ( ( ( ( ๐‘… โˆˆ CRing โˆง ๐‘ƒ โˆˆ ( PrmIdeal โ€˜ ๐‘… ) ) โˆง ๐‘ฅ โˆˆ ๐ต ) โˆง ๐‘ฆ โˆˆ ๐ต ) โˆง ( ๐‘ฅ ยท ๐‘ฆ ) โˆˆ ๐‘ƒ ) โˆง ๐‘Ÿ โˆˆ ( ( RSpan โ€˜ ๐‘… ) โ€˜ { ๐‘ฅ } ) ) โˆง ๐‘  โˆˆ ( ( RSpan โ€˜ ๐‘… ) โ€˜ { ๐‘ฆ } ) ) โ†’ ( ๐‘Ÿ ยท ๐‘  ) โˆˆ ๐‘ƒ )
54 53 anasss โŠข ( ( ( ( ( ( ๐‘… โˆˆ CRing โˆง ๐‘ƒ โˆˆ ( PrmIdeal โ€˜ ๐‘… ) ) โˆง ๐‘ฅ โˆˆ ๐ต ) โˆง ๐‘ฆ โˆˆ ๐ต ) โˆง ( ๐‘ฅ ยท ๐‘ฆ ) โˆˆ ๐‘ƒ ) โˆง ( ๐‘Ÿ โˆˆ ( ( RSpan โ€˜ ๐‘… ) โ€˜ { ๐‘ฅ } ) โˆง ๐‘  โˆˆ ( ( RSpan โ€˜ ๐‘… ) โ€˜ { ๐‘ฆ } ) ) ) โ†’ ( ๐‘Ÿ ยท ๐‘  ) โˆˆ ๐‘ƒ )
55 54 ralrimivva โŠข ( ( ( ( ( ๐‘… โˆˆ CRing โˆง ๐‘ƒ โˆˆ ( PrmIdeal โ€˜ ๐‘… ) ) โˆง ๐‘ฅ โˆˆ ๐ต ) โˆง ๐‘ฆ โˆˆ ๐ต ) โˆง ( ๐‘ฅ ยท ๐‘ฆ ) โˆˆ ๐‘ƒ ) โ†’ โˆ€ ๐‘Ÿ โˆˆ ( ( RSpan โ€˜ ๐‘… ) โ€˜ { ๐‘ฅ } ) โˆ€ ๐‘  โˆˆ ( ( RSpan โ€˜ ๐‘… ) โ€˜ { ๐‘ฆ } ) ( ๐‘Ÿ ยท ๐‘  ) โˆˆ ๐‘ƒ )
56 1 2 prmidl โŠข ( ( ( ( ๐‘… โˆˆ Ring โˆง ๐‘ƒ โˆˆ ( PrmIdeal โ€˜ ๐‘… ) ) โˆง ( ( ( RSpan โ€˜ ๐‘… ) โ€˜ { ๐‘ฅ } ) โˆˆ ( LIdeal โ€˜ ๐‘… ) โˆง ( ( RSpan โ€˜ ๐‘… ) โ€˜ { ๐‘ฆ } ) โˆˆ ( LIdeal โ€˜ ๐‘… ) ) ) โˆง โˆ€ ๐‘Ÿ โˆˆ ( ( RSpan โ€˜ ๐‘… ) โ€˜ { ๐‘ฅ } ) โˆ€ ๐‘  โˆˆ ( ( RSpan โ€˜ ๐‘… ) โ€˜ { ๐‘ฆ } ) ( ๐‘Ÿ ยท ๐‘  ) โˆˆ ๐‘ƒ ) โ†’ ( ( ( RSpan โ€˜ ๐‘… ) โ€˜ { ๐‘ฅ } ) โŠ† ๐‘ƒ โˆจ ( ( RSpan โ€˜ ๐‘… ) โ€˜ { ๐‘ฆ } ) โŠ† ๐‘ƒ ) )
57 8 9 20 55 56 syl1111anc โŠข ( ( ( ( ( ๐‘… โˆˆ CRing โˆง ๐‘ƒ โˆˆ ( PrmIdeal โ€˜ ๐‘… ) ) โˆง ๐‘ฅ โˆˆ ๐ต ) โˆง ๐‘ฆ โˆˆ ๐ต ) โˆง ( ๐‘ฅ ยท ๐‘ฆ ) โˆˆ ๐‘ƒ ) โ†’ ( ( ( RSpan โ€˜ ๐‘… ) โ€˜ { ๐‘ฅ } ) โŠ† ๐‘ƒ โˆจ ( ( RSpan โ€˜ ๐‘… ) โ€˜ { ๐‘ฆ } ) โŠ† ๐‘ƒ ) )
58 1 12 rspsnid โŠข ( ( ๐‘… โˆˆ Ring โˆง ๐‘ฅ โˆˆ ๐ต ) โ†’ ๐‘ฅ โˆˆ ( ( RSpan โ€˜ ๐‘… ) โ€˜ { ๐‘ฅ } ) )
59 3 58 sylan โŠข ( ( ๐‘… โˆˆ CRing โˆง ๐‘ฅ โˆˆ ๐ต ) โ†’ ๐‘ฅ โˆˆ ( ( RSpan โ€˜ ๐‘… ) โ€˜ { ๐‘ฅ } ) )
60 59 adantr โŠข ( ( ( ๐‘… โˆˆ CRing โˆง ๐‘ฅ โˆˆ ๐ต ) โˆง ๐‘ฆ โˆˆ ๐ต ) โ†’ ๐‘ฅ โˆˆ ( ( RSpan โ€˜ ๐‘… ) โ€˜ { ๐‘ฅ } ) )
61 ssel โŠข ( ( ( RSpan โ€˜ ๐‘… ) โ€˜ { ๐‘ฅ } ) โŠ† ๐‘ƒ โ†’ ( ๐‘ฅ โˆˆ ( ( RSpan โ€˜ ๐‘… ) โ€˜ { ๐‘ฅ } ) โ†’ ๐‘ฅ โˆˆ ๐‘ƒ ) )
62 60 61 syl5com โŠข ( ( ( ๐‘… โˆˆ CRing โˆง ๐‘ฅ โˆˆ ๐ต ) โˆง ๐‘ฆ โˆˆ ๐ต ) โ†’ ( ( ( RSpan โ€˜ ๐‘… ) โ€˜ { ๐‘ฅ } ) โŠ† ๐‘ƒ โ†’ ๐‘ฅ โˆˆ ๐‘ƒ ) )
63 1 12 rspsnid โŠข ( ( ๐‘… โˆˆ Ring โˆง ๐‘ฆ โˆˆ ๐ต ) โ†’ ๐‘ฆ โˆˆ ( ( RSpan โ€˜ ๐‘… ) โ€˜ { ๐‘ฆ } ) )
64 3 63 sylan โŠข ( ( ๐‘… โˆˆ CRing โˆง ๐‘ฆ โˆˆ ๐ต ) โ†’ ๐‘ฆ โˆˆ ( ( RSpan โ€˜ ๐‘… ) โ€˜ { ๐‘ฆ } ) )
65 64 adantlr โŠข ( ( ( ๐‘… โˆˆ CRing โˆง ๐‘ฅ โˆˆ ๐ต ) โˆง ๐‘ฆ โˆˆ ๐ต ) โ†’ ๐‘ฆ โˆˆ ( ( RSpan โ€˜ ๐‘… ) โ€˜ { ๐‘ฆ } ) )
66 ssel โŠข ( ( ( RSpan โ€˜ ๐‘… ) โ€˜ { ๐‘ฆ } ) โŠ† ๐‘ƒ โ†’ ( ๐‘ฆ โˆˆ ( ( RSpan โ€˜ ๐‘… ) โ€˜ { ๐‘ฆ } ) โ†’ ๐‘ฆ โˆˆ ๐‘ƒ ) )
67 65 66 syl5com โŠข ( ( ( ๐‘… โˆˆ CRing โˆง ๐‘ฅ โˆˆ ๐ต ) โˆง ๐‘ฆ โˆˆ ๐ต ) โ†’ ( ( ( RSpan โ€˜ ๐‘… ) โ€˜ { ๐‘ฆ } ) โŠ† ๐‘ƒ โ†’ ๐‘ฆ โˆˆ ๐‘ƒ ) )
68 62 67 orim12d โŠข ( ( ( ๐‘… โˆˆ CRing โˆง ๐‘ฅ โˆˆ ๐ต ) โˆง ๐‘ฆ โˆˆ ๐ต ) โ†’ ( ( ( ( RSpan โ€˜ ๐‘… ) โ€˜ { ๐‘ฅ } ) โŠ† ๐‘ƒ โˆจ ( ( RSpan โ€˜ ๐‘… ) โ€˜ { ๐‘ฆ } ) โŠ† ๐‘ƒ ) โ†’ ( ๐‘ฅ โˆˆ ๐‘ƒ โˆจ ๐‘ฆ โˆˆ ๐‘ƒ ) ) )
69 68 adantllr โŠข ( ( ( ( ๐‘… โˆˆ CRing โˆง ๐‘ƒ โˆˆ ( PrmIdeal โ€˜ ๐‘… ) ) โˆง ๐‘ฅ โˆˆ ๐ต ) โˆง ๐‘ฆ โˆˆ ๐ต ) โ†’ ( ( ( ( RSpan โ€˜ ๐‘… ) โ€˜ { ๐‘ฅ } ) โŠ† ๐‘ƒ โˆจ ( ( RSpan โ€˜ ๐‘… ) โ€˜ { ๐‘ฆ } ) โŠ† ๐‘ƒ ) โ†’ ( ๐‘ฅ โˆˆ ๐‘ƒ โˆจ ๐‘ฆ โˆˆ ๐‘ƒ ) ) )
70 69 adantr โŠข ( ( ( ( ( ๐‘… โˆˆ CRing โˆง ๐‘ƒ โˆˆ ( PrmIdeal โ€˜ ๐‘… ) ) โˆง ๐‘ฅ โˆˆ ๐ต ) โˆง ๐‘ฆ โˆˆ ๐ต ) โˆง ( ๐‘ฅ ยท ๐‘ฆ ) โˆˆ ๐‘ƒ ) โ†’ ( ( ( ( RSpan โ€˜ ๐‘… ) โ€˜ { ๐‘ฅ } ) โŠ† ๐‘ƒ โˆจ ( ( RSpan โ€˜ ๐‘… ) โ€˜ { ๐‘ฆ } ) โŠ† ๐‘ƒ ) โ†’ ( ๐‘ฅ โˆˆ ๐‘ƒ โˆจ ๐‘ฆ โˆˆ ๐‘ƒ ) ) )
71 57 70 mpd โŠข ( ( ( ( ( ๐‘… โˆˆ CRing โˆง ๐‘ƒ โˆˆ ( PrmIdeal โ€˜ ๐‘… ) ) โˆง ๐‘ฅ โˆˆ ๐ต ) โˆง ๐‘ฆ โˆˆ ๐ต ) โˆง ( ๐‘ฅ ยท ๐‘ฆ ) โˆˆ ๐‘ƒ ) โ†’ ( ๐‘ฅ โˆˆ ๐‘ƒ โˆจ ๐‘ฆ โˆˆ ๐‘ƒ ) )
72 71 ex โŠข ( ( ( ( ๐‘… โˆˆ CRing โˆง ๐‘ƒ โˆˆ ( PrmIdeal โ€˜ ๐‘… ) ) โˆง ๐‘ฅ โˆˆ ๐ต ) โˆง ๐‘ฆ โˆˆ ๐ต ) โ†’ ( ( ๐‘ฅ ยท ๐‘ฆ ) โˆˆ ๐‘ƒ โ†’ ( ๐‘ฅ โˆˆ ๐‘ƒ โˆจ ๐‘ฆ โˆˆ ๐‘ƒ ) ) )
73 72 anasss โŠข ( ( ( ๐‘… โˆˆ CRing โˆง ๐‘ƒ โˆˆ ( PrmIdeal โ€˜ ๐‘… ) ) โˆง ( ๐‘ฅ โˆˆ ๐ต โˆง ๐‘ฆ โˆˆ ๐ต ) ) โ†’ ( ( ๐‘ฅ ยท ๐‘ฆ ) โˆˆ ๐‘ƒ โ†’ ( ๐‘ฅ โˆˆ ๐‘ƒ โˆจ ๐‘ฆ โˆˆ ๐‘ƒ ) ) )
74 73 ralrimivva โŠข ( ( ๐‘… โˆˆ CRing โˆง ๐‘ƒ โˆˆ ( PrmIdeal โ€˜ ๐‘… ) ) โ†’ โˆ€ ๐‘ฅ โˆˆ ๐ต โˆ€ ๐‘ฆ โˆˆ ๐ต ( ( ๐‘ฅ ยท ๐‘ฆ ) โˆˆ ๐‘ƒ โ†’ ( ๐‘ฅ โˆˆ ๐‘ƒ โˆจ ๐‘ฆ โˆˆ ๐‘ƒ ) ) )
75 5 7 74 3jca โŠข ( ( ๐‘… โˆˆ CRing โˆง ๐‘ƒ โˆˆ ( PrmIdeal โ€˜ ๐‘… ) ) โ†’ ( ๐‘ƒ โˆˆ ( LIdeal โ€˜ ๐‘… ) โˆง ๐‘ƒ โ‰  ๐ต โˆง โˆ€ ๐‘ฅ โˆˆ ๐ต โˆ€ ๐‘ฆ โˆˆ ๐ต ( ( ๐‘ฅ ยท ๐‘ฆ ) โˆˆ ๐‘ƒ โ†’ ( ๐‘ฅ โˆˆ ๐‘ƒ โˆจ ๐‘ฆ โˆˆ ๐‘ƒ ) ) ) )
76 3anass โŠข ( ( ๐‘ƒ โˆˆ ( LIdeal โ€˜ ๐‘… ) โˆง ๐‘ƒ โ‰  ๐ต โˆง โˆ€ ๐‘ฅ โˆˆ ๐ต โˆ€ ๐‘ฆ โˆˆ ๐ต ( ( ๐‘ฅ ยท ๐‘ฆ ) โˆˆ ๐‘ƒ โ†’ ( ๐‘ฅ โˆˆ ๐‘ƒ โˆจ ๐‘ฆ โˆˆ ๐‘ƒ ) ) ) โ†” ( ๐‘ƒ โˆˆ ( LIdeal โ€˜ ๐‘… ) โˆง ( ๐‘ƒ โ‰  ๐ต โˆง โˆ€ ๐‘ฅ โˆˆ ๐ต โˆ€ ๐‘ฆ โˆˆ ๐ต ( ( ๐‘ฅ ยท ๐‘ฆ ) โˆˆ ๐‘ƒ โ†’ ( ๐‘ฅ โˆˆ ๐‘ƒ โˆจ ๐‘ฆ โˆˆ ๐‘ƒ ) ) ) ) )
77 1 2 prmidl2 โŠข ( ( ( ๐‘… โˆˆ Ring โˆง ๐‘ƒ โˆˆ ( LIdeal โ€˜ ๐‘… ) ) โˆง ( ๐‘ƒ โ‰  ๐ต โˆง โˆ€ ๐‘ฅ โˆˆ ๐ต โˆ€ ๐‘ฆ โˆˆ ๐ต ( ( ๐‘ฅ ยท ๐‘ฆ ) โˆˆ ๐‘ƒ โ†’ ( ๐‘ฅ โˆˆ ๐‘ƒ โˆจ ๐‘ฆ โˆˆ ๐‘ƒ ) ) ) ) โ†’ ๐‘ƒ โˆˆ ( PrmIdeal โ€˜ ๐‘… ) )
78 77 anasss โŠข ( ( ๐‘… โˆˆ Ring โˆง ( ๐‘ƒ โˆˆ ( LIdeal โ€˜ ๐‘… ) โˆง ( ๐‘ƒ โ‰  ๐ต โˆง โˆ€ ๐‘ฅ โˆˆ ๐ต โˆ€ ๐‘ฆ โˆˆ ๐ต ( ( ๐‘ฅ ยท ๐‘ฆ ) โˆˆ ๐‘ƒ โ†’ ( ๐‘ฅ โˆˆ ๐‘ƒ โˆจ ๐‘ฆ โˆˆ ๐‘ƒ ) ) ) ) ) โ†’ ๐‘ƒ โˆˆ ( PrmIdeal โ€˜ ๐‘… ) )
79 76 78 sylan2b โŠข ( ( ๐‘… โˆˆ Ring โˆง ( ๐‘ƒ โˆˆ ( LIdeal โ€˜ ๐‘… ) โˆง ๐‘ƒ โ‰  ๐ต โˆง โˆ€ ๐‘ฅ โˆˆ ๐ต โˆ€ ๐‘ฆ โˆˆ ๐ต ( ( ๐‘ฅ ยท ๐‘ฆ ) โˆˆ ๐‘ƒ โ†’ ( ๐‘ฅ โˆˆ ๐‘ƒ โˆจ ๐‘ฆ โˆˆ ๐‘ƒ ) ) ) ) โ†’ ๐‘ƒ โˆˆ ( PrmIdeal โ€˜ ๐‘… ) )
80 3 79 sylan โŠข ( ( ๐‘… โˆˆ CRing โˆง ( ๐‘ƒ โˆˆ ( LIdeal โ€˜ ๐‘… ) โˆง ๐‘ƒ โ‰  ๐ต โˆง โˆ€ ๐‘ฅ โˆˆ ๐ต โˆ€ ๐‘ฆ โˆˆ ๐ต ( ( ๐‘ฅ ยท ๐‘ฆ ) โˆˆ ๐‘ƒ โ†’ ( ๐‘ฅ โˆˆ ๐‘ƒ โˆจ ๐‘ฆ โˆˆ ๐‘ƒ ) ) ) ) โ†’ ๐‘ƒ โˆˆ ( PrmIdeal โ€˜ ๐‘… ) )
81 75 80 impbida โŠข ( ๐‘… โˆˆ CRing โ†’ ( ๐‘ƒ โˆˆ ( PrmIdeal โ€˜ ๐‘… ) โ†” ( ๐‘ƒ โˆˆ ( LIdeal โ€˜ ๐‘… ) โˆง ๐‘ƒ โ‰  ๐ต โˆง โˆ€ ๐‘ฅ โˆˆ ๐ต โˆ€ ๐‘ฆ โˆˆ ๐ต ( ( ๐‘ฅ ยท ๐‘ฆ ) โˆˆ ๐‘ƒ โ†’ ( ๐‘ฅ โˆˆ ๐‘ƒ โˆจ ๐‘ฆ โˆˆ ๐‘ƒ ) ) ) ) )