Metamath Proof Explorer

Theorem 1arithufdlem4

Description: Lemma for 1arithufd . Nonzero ring, non-field case. Those trivial cases are handled in the final proof. (Contributed by Thierry Arnoux, 3-Jun-2025)

Ref Expression
Hypotheses 1arithufd.b ⊢ 𝐵 = ( Base ‘ 𝑅 )
1arithufd.0 ⊢ 0 = ( 0g ‘ 𝑅 )
1arithufd.u ⊢ 𝑈 = ( Unit ‘ 𝑅 )
1arithufd.p ⊢ 𝑃 = ( RPrime ‘ 𝑅 )
1arithufd.m ⊢ 𝑀 = ( mulGrp ‘ 𝑅 )
1arithufd.r ⊢ ( 𝜑 → 𝑅 ∈ UFD )
1arithufdlem.2 ⊢ ( 𝜑 → ¬ 𝑅 ∈ DivRing )
1arithufdlem.s ⊢ 𝑆 = { 𝑥 ∈ 𝐵 ∣ ∃ 𝑓 ∈ Word 𝑃 𝑥 = ( 𝑀 Σg 𝑓 ) }
1arithufdlem.3 ⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
1arithufdlem.4 ⊢ ( 𝜑 → ¬ 𝑋 ∈ 𝑈 )
1arithufdlem.5 ⊢ ( 𝜑 → 𝑋 ≠ 0 )
Assertion 1arithufdlem4 ( 𝜑 → 𝑋 ∈ 𝑆 )

Proof

Step Hyp Ref Expression
1 1arithufd.b ⊢ 𝐵 = ( Base ‘ 𝑅 )
2 1arithufd.0 ⊢ 0 = ( 0g ‘ 𝑅 )
3 1arithufd.u ⊢ 𝑈 = ( Unit ‘ 𝑅 )
4 1arithufd.p ⊢ 𝑃 = ( RPrime ‘ 𝑅 )
5 1arithufd.m ⊢ 𝑀 = ( mulGrp ‘ 𝑅 )
6 1arithufd.r ⊢ ( 𝜑 → 𝑅 ∈ UFD )
7 1arithufdlem.2 ⊢ ( 𝜑 → ¬ 𝑅 ∈ DivRing )
8 1arithufdlem.s ⊢ 𝑆 = { 𝑥 ∈ 𝐵 ∣ ∃ 𝑓 ∈ Word 𝑃 𝑥 = ( 𝑀 Σg 𝑓 ) }
9 1arithufdlem.3 ⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
10 1arithufdlem.4 ⊢ ( 𝜑 → ¬ 𝑋 ∈ 𝑈 )
11 1arithufdlem.5 ⊢ ( 𝜑 → 𝑋 ≠ 0 )
12 eqeq1 ⊢ ( 𝑥 = 𝑎 → ( 𝑥 = ( 𝑀 Σg 𝑓 ) ↔ 𝑎 = ( 𝑀 Σg 𝑓 ) ) )
13 12 rexbidv ⊢ ( 𝑥 = 𝑎 → ( ∃ 𝑓 ∈ Word 𝑃 𝑥 = ( 𝑀 Σg 𝑓 ) ↔ ∃ 𝑓 ∈ Word 𝑃 𝑎 = ( 𝑀 Σg 𝑓 ) ) )
14 eqcom ⊢ ( 𝑎 = ( 𝑀 Σg 𝑓 ) ↔ ( 𝑀 Σg 𝑓 ) = 𝑎 )
15 14 rexbii ⊢ ( ∃ 𝑓 ∈ Word 𝑃 𝑎 = ( 𝑀 Σg 𝑓 ) ↔ ∃ 𝑓 ∈ Word 𝑃 ( 𝑀 Σg 𝑓 ) = 𝑎 )
16 13 15 bitrdi ⊢ ( 𝑥 = 𝑎 → ( ∃ 𝑓 ∈ Word 𝑃 𝑥 = ( 𝑀 Σg 𝑓 ) ↔ ∃ 𝑓 ∈ Word 𝑃 ( 𝑀 Σg 𝑓 ) = 𝑎 ) )
17 6 adantr ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝑃 ) → 𝑅 ∈ UFD )
18 simpr ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝑃 ) → 𝑎 ∈ 𝑃 )
19 1 4 17 18 rprmcl ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝑃 ) → 𝑎 ∈ 𝐵 )
20 oveq2 ⊢ ( 𝑓 = ⟨“ 𝑎 ”⟩ → ( 𝑀 Σg 𝑓 ) = ( 𝑀 Σg ⟨“ 𝑎 ”⟩ ) )
21 20 eqeq1d ⊢ ( 𝑓 = ⟨“ 𝑎 ”⟩ → ( ( 𝑀 Σg 𝑓 ) = 𝑎 ↔ ( 𝑀 Σg ⟨“ 𝑎 ”⟩ ) = 𝑎 ) )
22 18 s1cld ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝑃 ) → ⟨“ 𝑎 ”⟩ ∈ Word 𝑃 )
23 5 1 mgpbas ⊢ 𝐵 = ( Base ‘ 𝑀 )
24 23 gsumws1 ⊢ ( 𝑎 ∈ 𝐵 → ( 𝑀 Σg ⟨“ 𝑎 ”⟩ ) = 𝑎 )
25 19 24 syl ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝑃 ) → ( 𝑀 Σg ⟨“ 𝑎 ”⟩ ) = 𝑎 )
26 21 22 25 rspcedvdw ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝑃 ) → ∃ 𝑓 ∈ Word 𝑃 ( 𝑀 Σg 𝑓 ) = 𝑎 )
27 16 19 26 elrabd ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝑃 ) → 𝑎 ∈ { 𝑥 ∈ 𝐵 ∣ ∃ 𝑓 ∈ Word 𝑃 𝑥 = ( 𝑀 Σg 𝑓 ) } )
28 27 8 eleqtrrdi ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝑃 ) → 𝑎 ∈ 𝑆 )
29 28 ex ⊢ ( 𝜑 → ( 𝑎 ∈ 𝑃 → 𝑎 ∈ 𝑆 ) )
30 29 ssrdv ⊢ ( 𝜑 → 𝑃 ⊆ 𝑆 )
31 30 adantr ⊢ ( ( 𝜑 ∧ ¬ 𝑋 ∈ 𝑆 ) → 𝑃 ⊆ 𝑆 )
32 anass ⊢ ( ( ( ( 𝜑 ∧ ¬ 𝑋 ∈ 𝑆 ) ∧ 𝑖 ∈ ( LIdeal ‘ 𝑅 ) ) ∧ ( ( 𝑆 ∩ 𝑖 ) = ∅ ∧ ( ( RSpan ‘ 𝑅 ) ‘ { 𝑋 } ) ⊆ 𝑖 ) ) ↔ ( ( 𝜑 ∧ ¬ 𝑋 ∈ 𝑆 ) ∧ ( 𝑖 ∈ ( LIdeal ‘ 𝑅 ) ∧ ( ( 𝑆 ∩ 𝑖 ) = ∅ ∧ ( ( RSpan ‘ 𝑅 ) ‘ { 𝑋 } ) ⊆ 𝑖 ) ) ) )
33 ineq2 ⊢ ( 𝑝 = 𝑖 → ( 𝑆 ∩ 𝑝 ) = ( 𝑆 ∩ 𝑖 ) )
34 33 eqeq1d ⊢ ( 𝑝 = 𝑖 → ( ( 𝑆 ∩ 𝑝 ) = ∅ ↔ ( 𝑆 ∩ 𝑖 ) = ∅ ) )
35 sseq2 ⊢ ( 𝑝 = 𝑖 → ( ( ( RSpan ‘ 𝑅 ) ‘ { 𝑋 } ) ⊆ 𝑝 ↔ ( ( RSpan ‘ 𝑅 ) ‘ { 𝑋 } ) ⊆ 𝑖 ) )
36 34 35 anbi12d ⊢ ( 𝑝 = 𝑖 → ( ( ( 𝑆 ∩ 𝑝 ) = ∅ ∧ ( ( RSpan ‘ 𝑅 ) ‘ { 𝑋 } ) ⊆ 𝑝 ) ↔ ( ( 𝑆 ∩ 𝑖 ) = ∅ ∧ ( ( RSpan ‘ 𝑅 ) ‘ { 𝑋 } ) ⊆ 𝑖 ) ) )
37 36 elrab ⊢ ( 𝑖 ∈ { 𝑝 ∈ ( LIdeal ‘ 𝑅 ) ∣ ( ( 𝑆 ∩ 𝑝 ) = ∅ ∧ ( ( RSpan ‘ 𝑅 ) ‘ { 𝑋 } ) ⊆ 𝑝 ) } ↔ ( 𝑖 ∈ ( LIdeal ‘ 𝑅 ) ∧ ( ( 𝑆 ∩ 𝑖 ) = ∅ ∧ ( ( RSpan ‘ 𝑅 ) ‘ { 𝑋 } ) ⊆ 𝑖 ) ) )
38 37 anbi2i ⊢ ( ( ( 𝜑 ∧ ¬ 𝑋 ∈ 𝑆 ) ∧ 𝑖 ∈ { 𝑝 ∈ ( LIdeal ‘ 𝑅 ) ∣ ( ( 𝑆 ∩ 𝑝 ) = ∅ ∧ ( ( RSpan ‘ 𝑅 ) ‘ { 𝑋 } ) ⊆ 𝑝 ) } ) ↔ ( ( 𝜑 ∧ ¬ 𝑋 ∈ 𝑆 ) ∧ ( 𝑖 ∈ ( LIdeal ‘ 𝑅 ) ∧ ( ( 𝑆 ∩ 𝑖 ) = ∅ ∧ ( ( RSpan ‘ 𝑅 ) ‘ { 𝑋 } ) ⊆ 𝑖 ) ) ) )
39 32 38 bitr4i ⊢ ( ( ( ( 𝜑 ∧ ¬ 𝑋 ∈ 𝑆 ) ∧ 𝑖 ∈ ( LIdeal ‘ 𝑅 ) ) ∧ ( ( 𝑆 ∩ 𝑖 ) = ∅ ∧ ( ( RSpan ‘ 𝑅 ) ‘ { 𝑋 } ) ⊆ 𝑖 ) ) ↔ ( ( 𝜑 ∧ ¬ 𝑋 ∈ 𝑆 ) ∧ 𝑖 ∈ { 𝑝 ∈ ( LIdeal ‘ 𝑅 ) ∣ ( ( 𝑆 ∩ 𝑝 ) = ∅ ∧ ( ( RSpan ‘ 𝑅 ) ‘ { 𝑋 } ) ⊆ 𝑝 ) } ) )
40 39 anbi1i ⊢ ( ( ( ( ( 𝜑 ∧ ¬ 𝑋 ∈ 𝑆 ) ∧ 𝑖 ∈ ( LIdeal ‘ 𝑅 ) ) ∧ ( ( 𝑆 ∩ 𝑖 ) = ∅ ∧ ( ( RSpan ‘ 𝑅 ) ‘ { 𝑋 } ) ⊆ 𝑖 ) ) ∧ 𝑖 ∈ ( PrmIdeal ‘ 𝑅 ) ) ↔ ( ( ( 𝜑 ∧ ¬ 𝑋 ∈ 𝑆 ) ∧ 𝑖 ∈ { 𝑝 ∈ ( LIdeal ‘ 𝑅 ) ∣ ( ( 𝑆 ∩ 𝑝 ) = ∅ ∧ ( ( RSpan ‘ 𝑅 ) ‘ { 𝑋 } ) ⊆ 𝑝 ) } ) ∧ 𝑖 ∈ ( PrmIdeal ‘ 𝑅 ) ) )
41 incom ⊢ ( 𝑖 ∩ 𝑆 ) = ( 𝑆 ∩ 𝑖 )
42 simpllr ⊢ ( ( ( ( ( ( 𝜑 ∧ ¬ 𝑋 ∈ 𝑆 ) ∧ 𝑖 ∈ ( LIdeal ‘ 𝑅 ) ) ∧ ( ( 𝑆 ∩ 𝑖 ) = ∅ ∧ ( ( RSpan ‘ 𝑅 ) ‘ { 𝑋 } ) ⊆ 𝑖 ) ) ∧ 𝑖 ∈ ( PrmIdeal ‘ 𝑅 ) ) ∧ ∀ 𝑗 ∈ { 𝑝 ∈ ( LIdeal ‘ 𝑅 ) ∣ ( ( 𝑆 ∩ 𝑝 ) = ∅ ∧ ( ( RSpan ‘ 𝑅 ) ‘ { 𝑋 } ) ⊆ 𝑝 ) } ¬ 𝑖 ⊊ 𝑗 ) → ( ( 𝑆 ∩ 𝑖 ) = ∅ ∧ ( ( RSpan ‘ 𝑅 ) ‘ { 𝑋 } ) ⊆ 𝑖 ) )
43 42 simpld ⊢ ( ( ( ( ( ( 𝜑 ∧ ¬ 𝑋 ∈ 𝑆 ) ∧ 𝑖 ∈ ( LIdeal ‘ 𝑅 ) ) ∧ ( ( 𝑆 ∩ 𝑖 ) = ∅ ∧ ( ( RSpan ‘ 𝑅 ) ‘ { 𝑋 } ) ⊆ 𝑖 ) ) ∧ 𝑖 ∈ ( PrmIdeal ‘ 𝑅 ) ) ∧ ∀ 𝑗 ∈ { 𝑝 ∈ ( LIdeal ‘ 𝑅 ) ∣ ( ( 𝑆 ∩ 𝑝 ) = ∅ ∧ ( ( RSpan ‘ 𝑅 ) ‘ { 𝑋 } ) ⊆ 𝑝 ) } ¬ 𝑖 ⊊ 𝑗 ) → ( 𝑆 ∩ 𝑖 ) = ∅ )
44 41 43 eqtrid ⊢ ( ( ( ( ( ( 𝜑 ∧ ¬ 𝑋 ∈ 𝑆 ) ∧ 𝑖 ∈ ( LIdeal ‘ 𝑅 ) ) ∧ ( ( 𝑆 ∩ 𝑖 ) = ∅ ∧ ( ( RSpan ‘ 𝑅 ) ‘ { 𝑋 } ) ⊆ 𝑖 ) ) ∧ 𝑖 ∈ ( PrmIdeal ‘ 𝑅 ) ) ∧ ∀ 𝑗 ∈ { 𝑝 ∈ ( LIdeal ‘ 𝑅 ) ∣ ( ( 𝑆 ∩ 𝑝 ) = ∅ ∧ ( ( RSpan ‘ 𝑅 ) ‘ { 𝑋 } ) ⊆ 𝑝 ) } ¬ 𝑖 ⊊ 𝑗 ) → ( 𝑖 ∩ 𝑆 ) = ∅ )
45 6 ad5antr ⊢ ( ( ( ( ( ( 𝜑 ∧ ¬ 𝑋 ∈ 𝑆 ) ∧ 𝑖 ∈ ( LIdeal ‘ 𝑅 ) ) ∧ ( ( 𝑆 ∩ 𝑖 ) = ∅ ∧ ( ( RSpan ‘ 𝑅 ) ‘ { 𝑋 } ) ⊆ 𝑖 ) ) ∧ 𝑖 ∈ ( PrmIdeal ‘ 𝑅 ) ) ∧ ∀ 𝑗 ∈ { 𝑝 ∈ ( LIdeal ‘ 𝑅 ) ∣ ( ( 𝑆 ∩ 𝑝 ) = ∅ ∧ ( ( RSpan ‘ 𝑅 ) ‘ { 𝑋 } ) ⊆ 𝑝 ) } ¬ 𝑖 ⊊ 𝑗 ) → 𝑅 ∈ UFD )
46 simplr ⊢ ( ( ( ( ( ( 𝜑 ∧ ¬ 𝑋 ∈ 𝑆 ) ∧ 𝑖 ∈ ( LIdeal ‘ 𝑅 ) ) ∧ ( ( 𝑆 ∩ 𝑖 ) = ∅ ∧ ( ( RSpan ‘ 𝑅 ) ‘ { 𝑋 } ) ⊆ 𝑖 ) ) ∧ 𝑖 ∈ ( PrmIdeal ‘ 𝑅 ) ) ∧ ∀ 𝑗 ∈ { 𝑝 ∈ ( LIdeal ‘ 𝑅 ) ∣ ( ( 𝑆 ∩ 𝑝 ) = ∅ ∧ ( ( RSpan ‘ 𝑅 ) ‘ { 𝑋 } ) ⊆ 𝑝 ) } ¬ 𝑖 ⊊ 𝑗 ) → 𝑖 ∈ ( PrmIdeal ‘ 𝑅 ) )
47 42 simprd ⊢ ( ( ( ( ( ( 𝜑 ∧ ¬ 𝑋 ∈ 𝑆 ) ∧ 𝑖 ∈ ( LIdeal ‘ 𝑅 ) ) ∧ ( ( 𝑆 ∩ 𝑖 ) = ∅ ∧ ( ( RSpan ‘ 𝑅 ) ‘ { 𝑋 } ) ⊆ 𝑖 ) ) ∧ 𝑖 ∈ ( PrmIdeal ‘ 𝑅 ) ) ∧ ∀ 𝑗 ∈ { 𝑝 ∈ ( LIdeal ‘ 𝑅 ) ∣ ( ( 𝑆 ∩ 𝑝 ) = ∅ ∧ ( ( RSpan ‘ 𝑅 ) ‘ { 𝑋 } ) ⊆ 𝑝 ) } ¬ 𝑖 ⊊ 𝑗 ) → ( ( RSpan ‘ 𝑅 ) ‘ { 𝑋 } ) ⊆ 𝑖 )
48 6 ufdidom ⊢ ( 𝜑 → 𝑅 ∈ IDomn )
49 48 idomringd ⊢ ( 𝜑 → 𝑅 ∈ Ring )
50 eqid ⊢ ( RSpan ‘ 𝑅 ) = ( RSpan ‘ 𝑅 )
51 1 50 rspsnid ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵 ) → 𝑋 ∈ ( ( RSpan ‘ 𝑅 ) ‘ { 𝑋 } ) )
52 49 9 51 syl2anc ⊢ ( 𝜑 → 𝑋 ∈ ( ( RSpan ‘ 𝑅 ) ‘ { 𝑋 } ) )
53 52 ad5antr ⊢ ( ( ( ( ( ( 𝜑 ∧ ¬ 𝑋 ∈ 𝑆 ) ∧ 𝑖 ∈ ( LIdeal ‘ 𝑅 ) ) ∧ ( ( 𝑆 ∩ 𝑖 ) = ∅ ∧ ( ( RSpan ‘ 𝑅 ) ‘ { 𝑋 } ) ⊆ 𝑖 ) ) ∧ 𝑖 ∈ ( PrmIdeal ‘ 𝑅 ) ) ∧ ∀ 𝑗 ∈ { 𝑝 ∈ ( LIdeal ‘ 𝑅 ) ∣ ( ( 𝑆 ∩ 𝑝 ) = ∅ ∧ ( ( RSpan ‘ 𝑅 ) ‘ { 𝑋 } ) ⊆ 𝑝 ) } ¬ 𝑖 ⊊ 𝑗 ) → 𝑋 ∈ ( ( RSpan ‘ 𝑅 ) ‘ { 𝑋 } ) )
54 47 53 sseldd ⊢ ( ( ( ( ( ( 𝜑 ∧ ¬ 𝑋 ∈ 𝑆 ) ∧ 𝑖 ∈ ( LIdeal ‘ 𝑅 ) ) ∧ ( ( 𝑆 ∩ 𝑖 ) = ∅ ∧ ( ( RSpan ‘ 𝑅 ) ‘ { 𝑋 } ) ⊆ 𝑖 ) ) ∧ 𝑖 ∈ ( PrmIdeal ‘ 𝑅 ) ) ∧ ∀ 𝑗 ∈ { 𝑝 ∈ ( LIdeal ‘ 𝑅 ) ∣ ( ( 𝑆 ∩ 𝑝 ) = ∅ ∧ ( ( RSpan ‘ 𝑅 ) ‘ { 𝑋 } ) ⊆ 𝑝 ) } ¬ 𝑖 ⊊ 𝑗 ) → 𝑋 ∈ 𝑖 )
55 nelsn ⊢ ( 𝑋 ≠ 0 → ¬ 𝑋 ∈ { 0 } )
56 11 55 syl ⊢ ( 𝜑 → ¬ 𝑋 ∈ { 0 } )
57 56 ad5antr ⊢ ( ( ( ( ( ( 𝜑 ∧ ¬ 𝑋 ∈ 𝑆 ) ∧ 𝑖 ∈ ( LIdeal ‘ 𝑅 ) ) ∧ ( ( 𝑆 ∩ 𝑖 ) = ∅ ∧ ( ( RSpan ‘ 𝑅 ) ‘ { 𝑋 } ) ⊆ 𝑖 ) ) ∧ 𝑖 ∈ ( PrmIdeal ‘ 𝑅 ) ) ∧ ∀ 𝑗 ∈ { 𝑝 ∈ ( LIdeal ‘ 𝑅 ) ∣ ( ( 𝑆 ∩ 𝑝 ) = ∅ ∧ ( ( RSpan ‘ 𝑅 ) ‘ { 𝑋 } ) ⊆ 𝑝 ) } ¬ 𝑖 ⊊ 𝑗 ) → ¬ 𝑋 ∈ { 0 } )
58 nelne1 ⊢ ( ( 𝑋 ∈ 𝑖 ∧ ¬ 𝑋 ∈ { 0 } ) → 𝑖 ≠ { 0 } )
59 54 57 58 syl2anc ⊢ ( ( ( ( ( ( 𝜑 ∧ ¬ 𝑋 ∈ 𝑆 ) ∧ 𝑖 ∈ ( LIdeal ‘ 𝑅 ) ) ∧ ( ( 𝑆 ∩ 𝑖 ) = ∅ ∧ ( ( RSpan ‘ 𝑅 ) ‘ { 𝑋 } ) ⊆ 𝑖 ) ) ∧ 𝑖 ∈ ( PrmIdeal ‘ 𝑅 ) ) ∧ ∀ 𝑗 ∈ { 𝑝 ∈ ( LIdeal ‘ 𝑅 ) ∣ ( ( 𝑆 ∩ 𝑝 ) = ∅ ∧ ( ( RSpan ‘ 𝑅 ) ‘ { 𝑋 } ) ⊆ 𝑝 ) } ¬ 𝑖 ⊊ 𝑗 ) → 𝑖 ≠ { 0 } )
60 46 59 eldifsnd ⊢ ( ( ( ( ( ( 𝜑 ∧ ¬ 𝑋 ∈ 𝑆 ) ∧ 𝑖 ∈ ( LIdeal ‘ 𝑅 ) ) ∧ ( ( 𝑆 ∩ 𝑖 ) = ∅ ∧ ( ( RSpan ‘ 𝑅 ) ‘ { 𝑋 } ) ⊆ 𝑖 ) ) ∧ 𝑖 ∈ ( PrmIdeal ‘ 𝑅 ) ) ∧ ∀ 𝑗 ∈ { 𝑝 ∈ ( LIdeal ‘ 𝑅 ) ∣ ( ( 𝑆 ∩ 𝑝 ) = ∅ ∧ ( ( RSpan ‘ 𝑅 ) ‘ { 𝑋 } ) ⊆ 𝑝 ) } ¬ 𝑖 ⊊ 𝑗 ) → 𝑖 ∈ ( ( PrmIdeal ‘ 𝑅 ) ∖ { { 0 } } ) )
61 ineq1 ⊢ ( 𝑗 = 𝑖 → ( 𝑗 ∩ 𝑃 ) = ( 𝑖 ∩ 𝑃 ) )
62 61 neeq1d ⊢ ( 𝑗 = 𝑖 → ( ( 𝑗 ∩ 𝑃 ) ≠ ∅ ↔ ( 𝑖 ∩ 𝑃 ) ≠ ∅ ) )
63 eqid ⊢ ( PrmIdeal ‘ 𝑅 ) = ( PrmIdeal ‘ 𝑅 )
64 63 4 2 isufd ⊢ ( 𝑅 ∈ UFD ↔ ( 𝑅 ∈ IDomn ∧ ∀ 𝑗 ∈ ( ( PrmIdeal ‘ 𝑅 ) ∖ { { 0 } } ) ( 𝑗 ∩ 𝑃 ) ≠ ∅ ) )
65 64 simprbi ⊢ ( 𝑅 ∈ UFD → ∀ 𝑗 ∈ ( ( PrmIdeal ‘ 𝑅 ) ∖ { { 0 } } ) ( 𝑗 ∩ 𝑃 ) ≠ ∅ )
66 65 adantr ⊢ ( ( 𝑅 ∈ UFD ∧ 𝑖 ∈ ( ( PrmIdeal ‘ 𝑅 ) ∖ { { 0 } } ) ) → ∀ 𝑗 ∈ ( ( PrmIdeal ‘ 𝑅 ) ∖ { { 0 } } ) ( 𝑗 ∩ 𝑃 ) ≠ ∅ )
67 simpr ⊢ ( ( 𝑅 ∈ UFD ∧ 𝑖 ∈ ( ( PrmIdeal ‘ 𝑅 ) ∖ { { 0 } } ) ) → 𝑖 ∈ ( ( PrmIdeal ‘ 𝑅 ) ∖ { { 0 } } ) )
68 62 66 67 rspcdva ⊢ ( ( 𝑅 ∈ UFD ∧ 𝑖 ∈ ( ( PrmIdeal ‘ 𝑅 ) ∖ { { 0 } } ) ) → ( 𝑖 ∩ 𝑃 ) ≠ ∅ )
69 45 60 68 syl2anc ⊢ ( ( ( ( ( ( 𝜑 ∧ ¬ 𝑋 ∈ 𝑆 ) ∧ 𝑖 ∈ ( LIdeal ‘ 𝑅 ) ) ∧ ( ( 𝑆 ∩ 𝑖 ) = ∅ ∧ ( ( RSpan ‘ 𝑅 ) ‘ { 𝑋 } ) ⊆ 𝑖 ) ) ∧ 𝑖 ∈ ( PrmIdeal ‘ 𝑅 ) ) ∧ ∀ 𝑗 ∈ { 𝑝 ∈ ( LIdeal ‘ 𝑅 ) ∣ ( ( 𝑆 ∩ 𝑝 ) = ∅ ∧ ( ( RSpan ‘ 𝑅 ) ‘ { 𝑋 } ) ⊆ 𝑝 ) } ¬ 𝑖 ⊊ 𝑗 ) → ( 𝑖 ∩ 𝑃 ) ≠ ∅ )
70 sseq0 ⊢ ( ( ( 𝑖 ∩ 𝑃 ) ⊆ ( 𝑖 ∩ 𝑆 ) ∧ ( 𝑖 ∩ 𝑆 ) = ∅ ) → ( 𝑖 ∩ 𝑃 ) = ∅ )
71 70 expcom ⊢ ( ( 𝑖 ∩ 𝑆 ) = ∅ → ( ( 𝑖 ∩ 𝑃 ) ⊆ ( 𝑖 ∩ 𝑆 ) → ( 𝑖 ∩ 𝑃 ) = ∅ ) )
72 71 necon3ad ⊢ ( ( 𝑖 ∩ 𝑆 ) = ∅ → ( ( 𝑖 ∩ 𝑃 ) ≠ ∅ → ¬ ( 𝑖 ∩ 𝑃 ) ⊆ ( 𝑖 ∩ 𝑆 ) ) )
73 sslin ⊢ ( 𝑃 ⊆ 𝑆 → ( 𝑖 ∩ 𝑃 ) ⊆ ( 𝑖 ∩ 𝑆 ) )
74 73 con3i ⊢ ( ¬ ( 𝑖 ∩ 𝑃 ) ⊆ ( 𝑖 ∩ 𝑆 ) → ¬ 𝑃 ⊆ 𝑆 )
75 72 74 syl6 ⊢ ( ( 𝑖 ∩ 𝑆 ) = ∅ → ( ( 𝑖 ∩ 𝑃 ) ≠ ∅ → ¬ 𝑃 ⊆ 𝑆 ) )
76 44 69 75 sylc ⊢ ( ( ( ( ( ( 𝜑 ∧ ¬ 𝑋 ∈ 𝑆 ) ∧ 𝑖 ∈ ( LIdeal ‘ 𝑅 ) ) ∧ ( ( 𝑆 ∩ 𝑖 ) = ∅ ∧ ( ( RSpan ‘ 𝑅 ) ‘ { 𝑋 } ) ⊆ 𝑖 ) ) ∧ 𝑖 ∈ ( PrmIdeal ‘ 𝑅 ) ) ∧ ∀ 𝑗 ∈ { 𝑝 ∈ ( LIdeal ‘ 𝑅 ) ∣ ( ( 𝑆 ∩ 𝑝 ) = ∅ ∧ ( ( RSpan ‘ 𝑅 ) ‘ { 𝑋 } ) ⊆ 𝑝 ) } ¬ 𝑖 ⊊ 𝑗 ) → ¬ 𝑃 ⊆ 𝑆 )
77 40 76 sylanbr ⊢ ( ( ( ( ( 𝜑 ∧ ¬ 𝑋 ∈ 𝑆 ) ∧ 𝑖 ∈ { 𝑝 ∈ ( LIdeal ‘ 𝑅 ) ∣ ( ( 𝑆 ∩ 𝑝 ) = ∅ ∧ ( ( RSpan ‘ 𝑅 ) ‘ { 𝑋 } ) ⊆ 𝑝 ) } ) ∧ 𝑖 ∈ ( PrmIdeal ‘ 𝑅 ) ) ∧ ∀ 𝑗 ∈ { 𝑝 ∈ ( LIdeal ‘ 𝑅 ) ∣ ( ( 𝑆 ∩ 𝑝 ) = ∅ ∧ ( ( RSpan ‘ 𝑅 ) ‘ { 𝑋 } ) ⊆ 𝑝 ) } ¬ 𝑖 ⊊ 𝑗 ) → ¬ 𝑃 ⊆ 𝑆 )
78 77 anasss ⊢ ( ( ( ( 𝜑 ∧ ¬ 𝑋 ∈ 𝑆 ) ∧ 𝑖 ∈ { 𝑝 ∈ ( LIdeal ‘ 𝑅 ) ∣ ( ( 𝑆 ∩ 𝑝 ) = ∅ ∧ ( ( RSpan ‘ 𝑅 ) ‘ { 𝑋 } ) ⊆ 𝑝 ) } ) ∧ ( 𝑖 ∈ ( PrmIdeal ‘ 𝑅 ) ∧ ∀ 𝑗 ∈ { 𝑝 ∈ ( LIdeal ‘ 𝑅 ) ∣ ( ( 𝑆 ∩ 𝑝 ) = ∅ ∧ ( ( RSpan ‘ 𝑅 ) ‘ { 𝑋 } ) ⊆ 𝑝 ) } ¬ 𝑖 ⊊ 𝑗 ) ) → ¬ 𝑃 ⊆ 𝑆 )
79 48 idomcringd ⊢ ( 𝜑 → 𝑅 ∈ CRing )
80 79 adantr ⊢ ( ( 𝜑 ∧ ¬ 𝑋 ∈ 𝑆 ) → 𝑅 ∈ CRing )
81 49 adantr ⊢ ( ( 𝜑 ∧ ¬ 𝑋 ∈ 𝑆 ) → 𝑅 ∈ Ring )
82 9 adantr ⊢ ( ( 𝜑 ∧ ¬ 𝑋 ∈ 𝑆 ) → 𝑋 ∈ 𝐵 )
83 82 snssd ⊢ ( ( 𝜑 ∧ ¬ 𝑋 ∈ 𝑆 ) → { 𝑋 } ⊆ 𝐵 )
84 eqid ⊢ ( LIdeal ‘ 𝑅 ) = ( LIdeal ‘ 𝑅 )
85 50 1 84 rspcl ⊢ ( ( 𝑅 ∈ Ring ∧ { 𝑋 } ⊆ 𝐵 ) → ( ( RSpan ‘ 𝑅 ) ‘ { 𝑋 } ) ∈ ( LIdeal ‘ 𝑅 ) )
86 81 83 85 syl2anc ⊢ ( ( 𝜑 ∧ ¬ 𝑋 ∈ 𝑆 ) → ( ( RSpan ‘ 𝑅 ) ‘ { 𝑋 } ) ∈ ( LIdeal ‘ 𝑅 ) )
87 5 ringmgp ⊢ ( 𝑅 ∈ Ring → 𝑀 ∈ Mnd )
88 49 87 syl ⊢ ( 𝜑 → 𝑀 ∈ Mnd )
89 8 ssrab3 ⊢ 𝑆 ⊆ 𝐵
90 89 a1i ⊢ ( 𝜑 → 𝑆 ⊆ 𝐵 )
91 eqeq1 ⊢ ( 𝑥 = ( 1r ‘ 𝑅 ) → ( 𝑥 = ( 𝑀 Σg 𝑓 ) ↔ ( 1r ‘ 𝑅 ) = ( 𝑀 Σg 𝑓 ) ) )
92 91 rexbidv ⊢ ( 𝑥 = ( 1r ‘ 𝑅 ) → ( ∃ 𝑓 ∈ Word 𝑃 𝑥 = ( 𝑀 Σg 𝑓 ) ↔ ∃ 𝑓 ∈ Word 𝑃 ( 1r ‘ 𝑅 ) = ( 𝑀 Σg 𝑓 ) ) )
93 eqcom ⊢ ( ( 1r ‘ 𝑅 ) = ( 𝑀 Σg 𝑓 ) ↔ ( 𝑀 Σg 𝑓 ) = ( 1r ‘ 𝑅 ) )
94 93 rexbii ⊢ ( ∃ 𝑓 ∈ Word 𝑃 ( 1r ‘ 𝑅 ) = ( 𝑀 Σg 𝑓 ) ↔ ∃ 𝑓 ∈ Word 𝑃 ( 𝑀 Σg 𝑓 ) = ( 1r ‘ 𝑅 ) )
95 92 94 bitrdi ⊢ ( 𝑥 = ( 1r ‘ 𝑅 ) → ( ∃ 𝑓 ∈ Word 𝑃 𝑥 = ( 𝑀 Σg 𝑓 ) ↔ ∃ 𝑓 ∈ Word 𝑃 ( 𝑀 Σg 𝑓 ) = ( 1r ‘ 𝑅 ) ) )
96 eqid ⊢ ( 1r ‘ 𝑅 ) = ( 1r ‘ 𝑅 )
97 1 96 ringidcl ⊢ ( 𝑅 ∈ Ring → ( 1r ‘ 𝑅 ) ∈ 𝐵 )
98 49 97 syl ⊢ ( 𝜑 → ( 1r ‘ 𝑅 ) ∈ 𝐵 )
99 oveq2 ⊢ ( 𝑓 = ∅ → ( 𝑀 Σg 𝑓 ) = ( 𝑀 Σg ∅ ) )
100 99 eqeq1d ⊢ ( 𝑓 = ∅ → ( ( 𝑀 Σg 𝑓 ) = ( 1r ‘ 𝑅 ) ↔ ( 𝑀 Σg ∅ ) = ( 1r ‘ 𝑅 ) ) )
101 wrd0 ⊢ ∅ ∈ Word 𝑃
102 101 a1i ⊢ ( 𝜑 → ∅ ∈ Word 𝑃 )
103 5 96 ringidval ⊢ ( 1r ‘ 𝑅 ) = ( 0g ‘ 𝑀 )
104 103 gsum0 ⊢ ( 𝑀 Σg ∅ ) = ( 1r ‘ 𝑅 )
105 104 a1i ⊢ ( 𝜑 → ( 𝑀 Σg ∅ ) = ( 1r ‘ 𝑅 ) )
106 100 102 105 rspcedvdw ⊢ ( 𝜑 → ∃ 𝑓 ∈ Word 𝑃 ( 𝑀 Σg 𝑓 ) = ( 1r ‘ 𝑅 ) )
107 95 98 106 elrabd ⊢ ( 𝜑 → ( 1r ‘ 𝑅 ) ∈ { 𝑥 ∈ 𝐵 ∣ ∃ 𝑓 ∈ Word 𝑃 𝑥 = ( 𝑀 Σg 𝑓 ) } )
108 107 8 eleqtrrdi ⊢ ( 𝜑 → ( 1r ‘ 𝑅 ) ∈ 𝑆 )
109 6 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) ∧ 𝑏 ∈ 𝑆 ) → 𝑅 ∈ UFD )
110 7 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) ∧ 𝑏 ∈ 𝑆 ) → ¬ 𝑅 ∈ DivRing )
111 eqid ⊢ ( .r ‘ 𝑅 ) = ( .r ‘ 𝑅 )
112 simplr ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) ∧ 𝑏 ∈ 𝑆 ) → 𝑎 ∈ 𝑆 )
113 simpr ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) ∧ 𝑏 ∈ 𝑆 ) → 𝑏 ∈ 𝑆 )
114 1 2 3 4 5 109 110 8 111 112 113 1arithufdlem2 ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑆 ) ∧ 𝑏 ∈ 𝑆 ) → ( 𝑎 ( .r ‘ 𝑅 ) 𝑏 ) ∈ 𝑆 )
115 114 anasss ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝑆 ∧ 𝑏 ∈ 𝑆 ) ) → ( 𝑎 ( .r ‘ 𝑅 ) 𝑏 ) ∈ 𝑆 )
116 115 ralrimivva ⊢ ( 𝜑 → ∀ 𝑎 ∈ 𝑆 ∀ 𝑏 ∈ 𝑆 ( 𝑎 ( .r ‘ 𝑅 ) 𝑏 ) ∈ 𝑆 )
117 5 111 mgpplusg ⊢ ( .r ‘ 𝑅 ) = ( +g ‘ 𝑀 )
118 23 103 117 issubm ⊢ ( 𝑀 ∈ Mnd → ( 𝑆 ∈ ( SubMnd ‘ 𝑀 ) ↔ ( 𝑆 ⊆ 𝐵 ∧ ( 1r ‘ 𝑅 ) ∈ 𝑆 ∧ ∀ 𝑎 ∈ 𝑆 ∀ 𝑏 ∈ 𝑆 ( 𝑎 ( .r ‘ 𝑅 ) 𝑏 ) ∈ 𝑆 ) ) )
119 118 biimpar ⊢ ( ( 𝑀 ∈ Mnd ∧ ( 𝑆 ⊆ 𝐵 ∧ ( 1r ‘ 𝑅 ) ∈ 𝑆 ∧ ∀ 𝑎 ∈ 𝑆 ∀ 𝑏 ∈ 𝑆 ( 𝑎 ( .r ‘ 𝑅 ) 𝑏 ) ∈ 𝑆 ) ) → 𝑆 ∈ ( SubMnd ‘ 𝑀 ) )
120 88 90 108 116 119 syl13anc ⊢ ( 𝜑 → 𝑆 ∈ ( SubMnd ‘ 𝑀 ) )
121 120 adantr ⊢ ( ( 𝜑 ∧ ¬ 𝑋 ∈ 𝑆 ) → 𝑆 ∈ ( SubMnd ‘ 𝑀 ) )
122 neq0 ⊢ ( ¬ ( 𝑆 ∩ ( ( RSpan ‘ 𝑅 ) ‘ { 𝑋 } ) ) = ∅ ↔ ∃ 𝑢 𝑢 ∈ ( 𝑆 ∩ ( ( RSpan ‘ 𝑅 ) ‘ { 𝑋 } ) ) )
123 122 biimpi ⊢ ( ¬ ( 𝑆 ∩ ( ( RSpan ‘ 𝑅 ) ‘ { 𝑋 } ) ) = ∅ → ∃ 𝑢 𝑢 ∈ ( 𝑆 ∩ ( ( RSpan ‘ 𝑅 ) ‘ { 𝑋 } ) ) )
124 123 adantl ⊢ ( ( 𝜑 ∧ ¬ ( 𝑆 ∩ ( ( RSpan ‘ 𝑅 ) ‘ { 𝑋 } ) ) = ∅ ) → ∃ 𝑢 𝑢 ∈ ( 𝑆 ∩ ( ( RSpan ‘ 𝑅 ) ‘ { 𝑋 } ) ) )
125 6 ad4antr ⊢ ( ( ( ( ( 𝜑 ∧ ¬ ( 𝑆 ∩ ( ( RSpan ‘ 𝑅 ) ‘ { 𝑋 } ) ) = ∅ ) ∧ 𝑢 ∈ ( 𝑆 ∩ ( ( RSpan ‘ 𝑅 ) ‘ { 𝑋 } ) ) ) ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑢 = ( 𝑦 ( .r ‘ 𝑅 ) 𝑋 ) ) → 𝑅 ∈ UFD )
126 7 ad4antr ⊢ ( ( ( ( ( 𝜑 ∧ ¬ ( 𝑆 ∩ ( ( RSpan ‘ 𝑅 ) ‘ { 𝑋 } ) ) = ∅ ) ∧ 𝑢 ∈ ( 𝑆 ∩ ( ( RSpan ‘ 𝑅 ) ‘ { 𝑋 } ) ) ) ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑢 = ( 𝑦 ( .r ‘ 𝑅 ) 𝑋 ) ) → ¬ 𝑅 ∈ DivRing )
127 9 ad4antr ⊢ ( ( ( ( ( 𝜑 ∧ ¬ ( 𝑆 ∩ ( ( RSpan ‘ 𝑅 ) ‘ { 𝑋 } ) ) = ∅ ) ∧ 𝑢 ∈ ( 𝑆 ∩ ( ( RSpan ‘ 𝑅 ) ‘ { 𝑋 } ) ) ) ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑢 = ( 𝑦 ( .r ‘ 𝑅 ) 𝑋 ) ) → 𝑋 ∈ 𝐵 )
128 10 ad4antr ⊢ ( ( ( ( ( 𝜑 ∧ ¬ ( 𝑆 ∩ ( ( RSpan ‘ 𝑅 ) ‘ { 𝑋 } ) ) = ∅ ) ∧ 𝑢 ∈ ( 𝑆 ∩ ( ( RSpan ‘ 𝑅 ) ‘ { 𝑋 } ) ) ) ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑢 = ( 𝑦 ( .r ‘ 𝑅 ) 𝑋 ) ) → ¬ 𝑋 ∈ 𝑈 )
129 11 ad4antr ⊢ ( ( ( ( ( 𝜑 ∧ ¬ ( 𝑆 ∩ ( ( RSpan ‘ 𝑅 ) ‘ { 𝑋 } ) ) = ∅ ) ∧ 𝑢 ∈ ( 𝑆 ∩ ( ( RSpan ‘ 𝑅 ) ‘ { 𝑋 } ) ) ) ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑢 = ( 𝑦 ( .r ‘ 𝑅 ) 𝑋 ) ) → 𝑋 ≠ 0 )
130 simplr ⊢ ( ( ( ( ( 𝜑 ∧ ¬ ( 𝑆 ∩ ( ( RSpan ‘ 𝑅 ) ‘ { 𝑋 } ) ) = ∅ ) ∧ 𝑢 ∈ ( 𝑆 ∩ ( ( RSpan ‘ 𝑅 ) ‘ { 𝑋 } ) ) ) ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑢 = ( 𝑦 ( .r ‘ 𝑅 ) 𝑋 ) ) → 𝑦 ∈ 𝐵 )
131 simpr ⊢ ( ( ( ( ( 𝜑 ∧ ¬ ( 𝑆 ∩ ( ( RSpan ‘ 𝑅 ) ‘ { 𝑋 } ) ) = ∅ ) ∧ 𝑢 ∈ ( 𝑆 ∩ ( ( RSpan ‘ 𝑅 ) ‘ { 𝑋 } ) ) ) ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑢 = ( 𝑦 ( .r ‘ 𝑅 ) 𝑋 ) ) → 𝑢 = ( 𝑦 ( .r ‘ 𝑅 ) 𝑋 ) )
132 simpllr ⊢ ( ( ( ( ( 𝜑 ∧ ¬ ( 𝑆 ∩ ( ( RSpan ‘ 𝑅 ) ‘ { 𝑋 } ) ) = ∅ ) ∧ 𝑢 ∈ ( 𝑆 ∩ ( ( RSpan ‘ 𝑅 ) ‘ { 𝑋 } ) ) ) ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑢 = ( 𝑦 ( .r ‘ 𝑅 ) 𝑋 ) ) → 𝑢 ∈ ( 𝑆 ∩ ( ( RSpan ‘ 𝑅 ) ‘ { 𝑋 } ) ) )
133 132 elin1d ⊢ ( ( ( ( ( 𝜑 ∧ ¬ ( 𝑆 ∩ ( ( RSpan ‘ 𝑅 ) ‘ { 𝑋 } ) ) = ∅ ) ∧ 𝑢 ∈ ( 𝑆 ∩ ( ( RSpan ‘ 𝑅 ) ‘ { 𝑋 } ) ) ) ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑢 = ( 𝑦 ( .r ‘ 𝑅 ) 𝑋 ) ) → 𝑢 ∈ 𝑆 )
134 131 133 eqeltrrd ⊢ ( ( ( ( ( 𝜑 ∧ ¬ ( 𝑆 ∩ ( ( RSpan ‘ 𝑅 ) ‘ { 𝑋 } ) ) = ∅ ) ∧ 𝑢 ∈ ( 𝑆 ∩ ( ( RSpan ‘ 𝑅 ) ‘ { 𝑋 } ) ) ) ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑢 = ( 𝑦 ( .r ‘ 𝑅 ) 𝑋 ) ) → ( 𝑦 ( .r ‘ 𝑅 ) 𝑋 ) ∈ 𝑆 )
135 1 2 3 4 5 125 126 8 127 128 129 111 130 134 1arithufdlem3 ⊢ ( ( ( ( ( 𝜑 ∧ ¬ ( 𝑆 ∩ ( ( RSpan ‘ 𝑅 ) ‘ { 𝑋 } ) ) = ∅ ) ∧ 𝑢 ∈ ( 𝑆 ∩ ( ( RSpan ‘ 𝑅 ) ‘ { 𝑋 } ) ) ) ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑢 = ( 𝑦 ( .r ‘ 𝑅 ) 𝑋 ) ) → 𝑋 ∈ 𝑆 )
136 49 ad2antrr ⊢ ( ( ( 𝜑 ∧ ¬ ( 𝑆 ∩ ( ( RSpan ‘ 𝑅 ) ‘ { 𝑋 } ) ) = ∅ ) ∧ 𝑢 ∈ ( 𝑆 ∩ ( ( RSpan ‘ 𝑅 ) ‘ { 𝑋 } ) ) ) → 𝑅 ∈ Ring )
137 9 ad2antrr ⊢ ( ( ( 𝜑 ∧ ¬ ( 𝑆 ∩ ( ( RSpan ‘ 𝑅 ) ‘ { 𝑋 } ) ) = ∅ ) ∧ 𝑢 ∈ ( 𝑆 ∩ ( ( RSpan ‘ 𝑅 ) ‘ { 𝑋 } ) ) ) → 𝑋 ∈ 𝐵 )
138 simpr ⊢ ( ( ( 𝜑 ∧ ¬ ( 𝑆 ∩ ( ( RSpan ‘ 𝑅 ) ‘ { 𝑋 } ) ) = ∅ ) ∧ 𝑢 ∈ ( 𝑆 ∩ ( ( RSpan ‘ 𝑅 ) ‘ { 𝑋 } ) ) ) → 𝑢 ∈ ( 𝑆 ∩ ( ( RSpan ‘ 𝑅 ) ‘ { 𝑋 } ) ) )
139 138 elin2d ⊢ ( ( ( 𝜑 ∧ ¬ ( 𝑆 ∩ ( ( RSpan ‘ 𝑅 ) ‘ { 𝑋 } ) ) = ∅ ) ∧ 𝑢 ∈ ( 𝑆 ∩ ( ( RSpan ‘ 𝑅 ) ‘ { 𝑋 } ) ) ) → 𝑢 ∈ ( ( RSpan ‘ 𝑅 ) ‘ { 𝑋 } ) )
140 1 111 50 elrspsn ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵 ) → ( 𝑢 ∈ ( ( RSpan ‘ 𝑅 ) ‘ { 𝑋 } ) ↔ ∃ 𝑦 ∈ 𝐵 𝑢 = ( 𝑦 ( .r ‘ 𝑅 ) 𝑋 ) ) )
141 140 biimpa ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵 ) ∧ 𝑢 ∈ ( ( RSpan ‘ 𝑅 ) ‘ { 𝑋 } ) ) → ∃ 𝑦 ∈ 𝐵 𝑢 = ( 𝑦 ( .r ‘ 𝑅 ) 𝑋 ) )
142 136 137 139 141 syl21anc ⊢ ( ( ( 𝜑 ∧ ¬ ( 𝑆 ∩ ( ( RSpan ‘ 𝑅 ) ‘ { 𝑋 } ) ) = ∅ ) ∧ 𝑢 ∈ ( 𝑆 ∩ ( ( RSpan ‘ 𝑅 ) ‘ { 𝑋 } ) ) ) → ∃ 𝑦 ∈ 𝐵 𝑢 = ( 𝑦 ( .r ‘ 𝑅 ) 𝑋 ) )
143 135 142 r19.29a ⊢ ( ( ( 𝜑 ∧ ¬ ( 𝑆 ∩ ( ( RSpan ‘ 𝑅 ) ‘ { 𝑋 } ) ) = ∅ ) ∧ 𝑢 ∈ ( 𝑆 ∩ ( ( RSpan ‘ 𝑅 ) ‘ { 𝑋 } ) ) ) → 𝑋 ∈ 𝑆 )
144 124 143 exlimddv ⊢ ( ( 𝜑 ∧ ¬ ( 𝑆 ∩ ( ( RSpan ‘ 𝑅 ) ‘ { 𝑋 } ) ) = ∅ ) → 𝑋 ∈ 𝑆 )
145 144 adantlr ⊢ ( ( ( 𝜑 ∧ ¬ 𝑋 ∈ 𝑆 ) ∧ ¬ ( 𝑆 ∩ ( ( RSpan ‘ 𝑅 ) ‘ { 𝑋 } ) ) = ∅ ) → 𝑋 ∈ 𝑆 )
146 simplr ⊢ ( ( ( 𝜑 ∧ ¬ 𝑋 ∈ 𝑆 ) ∧ ¬ ( 𝑆 ∩ ( ( RSpan ‘ 𝑅 ) ‘ { 𝑋 } ) ) = ∅ ) → ¬ 𝑋 ∈ 𝑆 )
147 145 146 condan ⊢ ( ( 𝜑 ∧ ¬ 𝑋 ∈ 𝑆 ) → ( 𝑆 ∩ ( ( RSpan ‘ 𝑅 ) ‘ { 𝑋 } ) ) = ∅ )
148 eqid ⊢ { 𝑝 ∈ ( LIdeal ‘ 𝑅 ) ∣ ( ( 𝑆 ∩ 𝑝 ) = ∅ ∧ ( ( RSpan ‘ 𝑅 ) ‘ { 𝑋 } ) ⊆ 𝑝 ) } = { 𝑝 ∈ ( LIdeal ‘ 𝑅 ) ∣ ( ( 𝑆 ∩ 𝑝 ) = ∅ ∧ ( ( RSpan ‘ 𝑅 ) ‘ { 𝑋 } ) ⊆ 𝑝 ) }
149 1 80 86 121 5 147 148 ssdifidlprm ⊢ ( ( 𝜑 ∧ ¬ 𝑋 ∈ 𝑆 ) → ∃ 𝑖 ∈ { 𝑝 ∈ ( LIdeal ‘ 𝑅 ) ∣ ( ( 𝑆 ∩ 𝑝 ) = ∅ ∧ ( ( RSpan ‘ 𝑅 ) ‘ { 𝑋 } ) ⊆ 𝑝 ) } ( 𝑖 ∈ ( PrmIdeal ‘ 𝑅 ) ∧ ∀ 𝑗 ∈ { 𝑝 ∈ ( LIdeal ‘ 𝑅 ) ∣ ( ( 𝑆 ∩ 𝑝 ) = ∅ ∧ ( ( RSpan ‘ 𝑅 ) ‘ { 𝑋 } ) ⊆ 𝑝 ) } ¬ 𝑖 ⊊ 𝑗 ) )
150 78 149 r19.29a ⊢ ( ( 𝜑 ∧ ¬ 𝑋 ∈ 𝑆 ) → ¬ 𝑃 ⊆ 𝑆 )
151 31 150 condan ⊢ ( 𝜑 → 𝑋 ∈ 𝑆 )