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 ‘ 𝑅 ) ∧ 𝑃𝐵 ∧ ∀ 𝑥𝐵𝑦𝐵 ( ( 𝑥 · 𝑦 ) ∈ 𝑃 → ( 𝑥𝑃𝑦𝑃 ) ) ) ) )