This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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