Metamath Proof Explorer

Theorem ssdifidlprm

Description: If the set S of ssdifidl is multiplicatively closed, then the ideal i is prime. (Contributed by Thierry Arnoux, 3-Jun-2025)

Ref Expression
Hypotheses ssdifidlprm.1 ⊢ 𝐵 = ( Base ‘ 𝑅 )
ssdifidlprm.2 ⊢ ( 𝜑 → 𝑅 ∈ CRing )
ssdifidlprm.3 ⊢ ( 𝜑 → 𝐼 ∈ ( LIdeal ‘ 𝑅 ) )
ssdifidlprm.4 ⊢ ( 𝜑 → 𝑆 ∈ ( SubMnd ‘ 𝑀 ) )
ssdifidlprm.5 ⊢ 𝑀 = ( mulGrp ‘ 𝑅 )
ssdifidlprm.6 ⊢ ( 𝜑 → ( 𝑆 ∩ 𝐼 ) = ∅ )
ssdifidlprm.7 ⊢ 𝑃 = { 𝑝 ∈ ( LIdeal ‘ 𝑅 ) ∣ ( ( 𝑆 ∩ 𝑝 ) = ∅ ∧ 𝐼 ⊆ 𝑝 ) }
Assertion ssdifidlprm ( 𝜑 → ∃ 𝑖 ∈ 𝑃 ( 𝑖 ∈ ( PrmIdeal ‘ 𝑅 ) ∧ ∀ 𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗 ) )

Proof

Step Hyp Ref Expression
1 ssdifidlprm.1 ⊢ 𝐵 = ( Base ‘ 𝑅 )
2 ssdifidlprm.2 ⊢ ( 𝜑 → 𝑅 ∈ CRing )
3 ssdifidlprm.3 ⊢ ( 𝜑 → 𝐼 ∈ ( LIdeal ‘ 𝑅 ) )
4 ssdifidlprm.4 ⊢ ( 𝜑 → 𝑆 ∈ ( SubMnd ‘ 𝑀 ) )
5 ssdifidlprm.5 ⊢ 𝑀 = ( mulGrp ‘ 𝑅 )
6 ssdifidlprm.6 ⊢ ( 𝜑 → ( 𝑆 ∩ 𝐼 ) = ∅ )
7 ssdifidlprm.7 ⊢ 𝑃 = { 𝑝 ∈ ( LIdeal ‘ 𝑅 ) ∣ ( ( 𝑆 ∩ 𝑝 ) = ∅ ∧ 𝐼 ⊆ 𝑝 ) }
8 2 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑃 ) ∧ ∀ 𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗 ) → 𝑅 ∈ CRing )
9 7 ssrab3 ⊢ 𝑃 ⊆ ( LIdeal ‘ 𝑅 )
10 simpr ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝑃 ) → 𝑖 ∈ 𝑃 )
11 9 10 sselid ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝑃 ) → 𝑖 ∈ ( LIdeal ‘ 𝑅 ) )
12 11 adantr ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑃 ) ∧ ∀ 𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗 ) → 𝑖 ∈ ( LIdeal ‘ 𝑅 ) )
13 2 crngringd ⊢ ( 𝜑 → 𝑅 ∈ Ring )
14 eqid ⊢ ( 1r ‘ 𝑅 ) = ( 1r ‘ 𝑅 )
15 1 14 ringidcl ⊢ ( 𝑅 ∈ Ring → ( 1r ‘ 𝑅 ) ∈ 𝐵 )
16 13 15 syl ⊢ ( 𝜑 → ( 1r ‘ 𝑅 ) ∈ 𝐵 )
17 16 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑃 ) ∧ ∀ 𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗 ) → ( 1r ‘ 𝑅 ) ∈ 𝐵 )
18 eqid ⊢ ( LIdeal ‘ 𝑅 ) = ( LIdeal ‘ 𝑅 )
19 1 18 lidlss ⊢ ( 𝑖 ∈ ( LIdeal ‘ 𝑅 ) → 𝑖 ⊆ 𝐵 )
20 11 19 syl ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝑃 ) → 𝑖 ⊆ 𝐵 )
21 20 adantr ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑃 ) ∧ ∀ 𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗 ) → 𝑖 ⊆ 𝐵 )
22 incom ⊢ ( 𝑆 ∩ 𝑝 ) = ( 𝑝 ∩ 𝑆 )
23 22 eqeq1i ⊢ ( ( 𝑆 ∩ 𝑝 ) = ∅ ↔ ( 𝑝 ∩ 𝑆 ) = ∅ )
24 ineq1 ⊢ ( 𝑝 = 𝑖 → ( 𝑝 ∩ 𝑆 ) = ( 𝑖 ∩ 𝑆 ) )
25 24 eqeq1d ⊢ ( 𝑝 = 𝑖 → ( ( 𝑝 ∩ 𝑆 ) = ∅ ↔ ( 𝑖 ∩ 𝑆 ) = ∅ ) )
26 23 25 bitrid ⊢ ( 𝑝 = 𝑖 → ( ( 𝑆 ∩ 𝑝 ) = ∅ ↔ ( 𝑖 ∩ 𝑆 ) = ∅ ) )
27 sseq2 ⊢ ( 𝑝 = 𝑖 → ( 𝐼 ⊆ 𝑝 ↔ 𝐼 ⊆ 𝑖 ) )
28 26 27 anbi12d ⊢ ( 𝑝 = 𝑖 → ( ( ( 𝑆 ∩ 𝑝 ) = ∅ ∧ 𝐼 ⊆ 𝑝 ) ↔ ( ( 𝑖 ∩ 𝑆 ) = ∅ ∧ 𝐼 ⊆ 𝑖 ) ) )
29 28 7 elrab2 ⊢ ( 𝑖 ∈ 𝑃 ↔ ( 𝑖 ∈ ( LIdeal ‘ 𝑅 ) ∧ ( ( 𝑖 ∩ 𝑆 ) = ∅ ∧ 𝐼 ⊆ 𝑖 ) ) )
30 29 biimpi ⊢ ( 𝑖 ∈ 𝑃 → ( 𝑖 ∈ ( LIdeal ‘ 𝑅 ) ∧ ( ( 𝑖 ∩ 𝑆 ) = ∅ ∧ 𝐼 ⊆ 𝑖 ) ) )
31 30 simprd ⊢ ( 𝑖 ∈ 𝑃 → ( ( 𝑖 ∩ 𝑆 ) = ∅ ∧ 𝐼 ⊆ 𝑖 ) )
32 31 simpld ⊢ ( 𝑖 ∈ 𝑃 → ( 𝑖 ∩ 𝑆 ) = ∅ )
33 32 ad2antlr ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑃 ) ∧ ∀ 𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗 ) → ( 𝑖 ∩ 𝑆 ) = ∅ )
34 reldisj ⊢ ( 𝑖 ⊆ 𝐵 → ( ( 𝑖 ∩ 𝑆 ) = ∅ ↔ 𝑖 ⊆ ( 𝐵 ∖ 𝑆 ) ) )
35 34 biimpa ⊢ ( ( 𝑖 ⊆ 𝐵 ∧ ( 𝑖 ∩ 𝑆 ) = ∅ ) → 𝑖 ⊆ ( 𝐵 ∖ 𝑆 ) )
36 21 33 35 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑃 ) ∧ ∀ 𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗 ) → 𝑖 ⊆ ( 𝐵 ∖ 𝑆 ) )
37 5 14 ringidval ⊢ ( 1r ‘ 𝑅 ) = ( 0g ‘ 𝑀 )
38 37 subm0cl ⊢ ( 𝑆 ∈ ( SubMnd ‘ 𝑀 ) → ( 1r ‘ 𝑅 ) ∈ 𝑆 )
39 4 38 syl ⊢ ( 𝜑 → ( 1r ‘ 𝑅 ) ∈ 𝑆 )
40 39 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑃 ) ∧ ∀ 𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗 ) → ( 1r ‘ 𝑅 ) ∈ 𝑆 )
41 elndif ⊢ ( ( 1r ‘ 𝑅 ) ∈ 𝑆 → ¬ ( 1r ‘ 𝑅 ) ∈ ( 𝐵 ∖ 𝑆 ) )
42 40 41 syl ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑃 ) ∧ ∀ 𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗 ) → ¬ ( 1r ‘ 𝑅 ) ∈ ( 𝐵 ∖ 𝑆 ) )
43 36 42 ssneldd ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑃 ) ∧ ∀ 𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗 ) → ¬ ( 1r ‘ 𝑅 ) ∈ 𝑖 )
44 nelne1 ⊢ ( ( ( 1r ‘ 𝑅 ) ∈ 𝐵 ∧ ¬ ( 1r ‘ 𝑅 ) ∈ 𝑖 ) → 𝐵 ≠ 𝑖 )
45 17 43 44 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑃 ) ∧ ∀ 𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗 ) → 𝐵 ≠ 𝑖 )
46 45 necomd ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑃 ) ∧ ∀ 𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗 ) → 𝑖 ≠ 𝐵 )
47 33 ad4antr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑃 ) ∧ ∀ 𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗 ) ∧ 𝑎 ∈ 𝐵 ) ∧ 𝑏 ∈ 𝐵 ) ∧ ( 𝑎 ( .r ‘ 𝑅 ) 𝑏 ) ∈ 𝑖 ) ∧ ¬ ( 𝑎 ∈ 𝑖 ∨ 𝑏 ∈ 𝑖 ) ) → ( 𝑖 ∩ 𝑆 ) = ∅ )
48 ioran ⊢ ( ¬ ( 𝑎 ∈ 𝑖 ∨ 𝑏 ∈ 𝑖 ) ↔ ( ¬ 𝑎 ∈ 𝑖 ∧ ¬ 𝑏 ∈ 𝑖 ) )
49 18 lidlsubg ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑖 ∈ ( LIdeal ‘ 𝑅 ) ) → 𝑖 ∈ ( SubGrp ‘ 𝑅 ) )
50 13 11 49 syl2an2r ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝑃 ) → 𝑖 ∈ ( SubGrp ‘ 𝑅 ) )
51 50 ad6antr ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑃 ) ∧ ∀ 𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗 ) ∧ 𝑎 ∈ 𝐵 ) ∧ 𝑏 ∈ 𝐵 ) ∧ ( 𝑎 ( .r ‘ 𝑅 ) 𝑏 ) ∈ 𝑖 ) ∧ ¬ 𝑎 ∈ 𝑖 ) ∧ ¬ 𝑏 ∈ 𝑖 ) → 𝑖 ∈ ( SubGrp ‘ 𝑅 ) )
52 13 ad7antr ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑃 ) ∧ ∀ 𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗 ) ∧ 𝑎 ∈ 𝐵 ) ∧ 𝑏 ∈ 𝐵 ) ∧ ( 𝑎 ( .r ‘ 𝑅 ) 𝑏 ) ∈ 𝑖 ) ∧ ¬ 𝑎 ∈ 𝑖 ) ∧ ¬ 𝑏 ∈ 𝑖 ) → 𝑅 ∈ Ring )
53 simp-5r ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑃 ) ∧ ∀ 𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗 ) ∧ 𝑎 ∈ 𝐵 ) ∧ 𝑏 ∈ 𝐵 ) ∧ ( 𝑎 ( .r ‘ 𝑅 ) 𝑏 ) ∈ 𝑖 ) ∧ ¬ 𝑎 ∈ 𝑖 ) ∧ ¬ 𝑏 ∈ 𝑖 ) → 𝑎 ∈ 𝐵 )
54 53 snssd ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑃 ) ∧ ∀ 𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗 ) ∧ 𝑎 ∈ 𝐵 ) ∧ 𝑏 ∈ 𝐵 ) ∧ ( 𝑎 ( .r ‘ 𝑅 ) 𝑏 ) ∈ 𝑖 ) ∧ ¬ 𝑎 ∈ 𝑖 ) ∧ ¬ 𝑏 ∈ 𝑖 ) → { 𝑎 } ⊆ 𝐵 )
55 eqid ⊢ ( RSpan ‘ 𝑅 ) = ( RSpan ‘ 𝑅 )
56 55 1 18 rspcl ⊢ ( ( 𝑅 ∈ Ring ∧ { 𝑎 } ⊆ 𝐵 ) → ( ( RSpan ‘ 𝑅 ) ‘ { 𝑎 } ) ∈ ( LIdeal ‘ 𝑅 ) )
57 52 54 56 syl2anc ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑃 ) ∧ ∀ 𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗 ) ∧ 𝑎 ∈ 𝐵 ) ∧ 𝑏 ∈ 𝐵 ) ∧ ( 𝑎 ( .r ‘ 𝑅 ) 𝑏 ) ∈ 𝑖 ) ∧ ¬ 𝑎 ∈ 𝑖 ) ∧ ¬ 𝑏 ∈ 𝑖 ) → ( ( RSpan ‘ 𝑅 ) ‘ { 𝑎 } ) ∈ ( LIdeal ‘ 𝑅 ) )
58 18 lidlsubg ⊢ ( ( 𝑅 ∈ Ring ∧ ( ( RSpan ‘ 𝑅 ) ‘ { 𝑎 } ) ∈ ( LIdeal ‘ 𝑅 ) ) → ( ( RSpan ‘ 𝑅 ) ‘ { 𝑎 } ) ∈ ( SubGrp ‘ 𝑅 ) )
59 52 57 58 syl2anc ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑃 ) ∧ ∀ 𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗 ) ∧ 𝑎 ∈ 𝐵 ) ∧ 𝑏 ∈ 𝐵 ) ∧ ( 𝑎 ( .r ‘ 𝑅 ) 𝑏 ) ∈ 𝑖 ) ∧ ¬ 𝑎 ∈ 𝑖 ) ∧ ¬ 𝑏 ∈ 𝑖 ) → ( ( RSpan ‘ 𝑅 ) ‘ { 𝑎 } ) ∈ ( SubGrp ‘ 𝑅 ) )
60 eqid ⊢ ( LSSum ‘ 𝑅 ) = ( LSSum ‘ 𝑅 )
61 60 lsmub1 ⊢ ( ( 𝑖 ∈ ( SubGrp ‘ 𝑅 ) ∧ ( ( RSpan ‘ 𝑅 ) ‘ { 𝑎 } ) ∈ ( SubGrp ‘ 𝑅 ) ) → 𝑖 ⊆ ( 𝑖 ( LSSum ‘ 𝑅 ) ( ( RSpan ‘ 𝑅 ) ‘ { 𝑎 } ) ) )
62 51 59 61 syl2anc ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑃 ) ∧ ∀ 𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗 ) ∧ 𝑎 ∈ 𝐵 ) ∧ 𝑏 ∈ 𝐵 ) ∧ ( 𝑎 ( .r ‘ 𝑅 ) 𝑏 ) ∈ 𝑖 ) ∧ ¬ 𝑎 ∈ 𝑖 ) ∧ ¬ 𝑏 ∈ 𝑖 ) → 𝑖 ⊆ ( 𝑖 ( LSSum ‘ 𝑅 ) ( ( RSpan ‘ 𝑅 ) ‘ { 𝑎 } ) ) )
63 60 lsmub2 ⊢ ( ( 𝑖 ∈ ( SubGrp ‘ 𝑅 ) ∧ ( ( RSpan ‘ 𝑅 ) ‘ { 𝑎 } ) ∈ ( SubGrp ‘ 𝑅 ) ) → ( ( RSpan ‘ 𝑅 ) ‘ { 𝑎 } ) ⊆ ( 𝑖 ( LSSum ‘ 𝑅 ) ( ( RSpan ‘ 𝑅 ) ‘ { 𝑎 } ) ) )
64 51 59 63 syl2anc ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑃 ) ∧ ∀ 𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗 ) ∧ 𝑎 ∈ 𝐵 ) ∧ 𝑏 ∈ 𝐵 ) ∧ ( 𝑎 ( .r ‘ 𝑅 ) 𝑏 ) ∈ 𝑖 ) ∧ ¬ 𝑎 ∈ 𝑖 ) ∧ ¬ 𝑏 ∈ 𝑖 ) → ( ( RSpan ‘ 𝑅 ) ‘ { 𝑎 } ) ⊆ ( 𝑖 ( LSSum ‘ 𝑅 ) ( ( RSpan ‘ 𝑅 ) ‘ { 𝑎 } ) ) )
65 1 55 rspsnid ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑎 ∈ 𝐵 ) → 𝑎 ∈ ( ( RSpan ‘ 𝑅 ) ‘ { 𝑎 } ) )
66 52 53 65 syl2anc ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑃 ) ∧ ∀ 𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗 ) ∧ 𝑎 ∈ 𝐵 ) ∧ 𝑏 ∈ 𝐵 ) ∧ ( 𝑎 ( .r ‘ 𝑅 ) 𝑏 ) ∈ 𝑖 ) ∧ ¬ 𝑎 ∈ 𝑖 ) ∧ ¬ 𝑏 ∈ 𝑖 ) → 𝑎 ∈ ( ( RSpan ‘ 𝑅 ) ‘ { 𝑎 } ) )
67 64 66 sseldd ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑃 ) ∧ ∀ 𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗 ) ∧ 𝑎 ∈ 𝐵 ) ∧ 𝑏 ∈ 𝐵 ) ∧ ( 𝑎 ( .r ‘ 𝑅 ) 𝑏 ) ∈ 𝑖 ) ∧ ¬ 𝑎 ∈ 𝑖 ) ∧ ¬ 𝑏 ∈ 𝑖 ) → 𝑎 ∈ ( 𝑖 ( LSSum ‘ 𝑅 ) ( ( RSpan ‘ 𝑅 ) ‘ { 𝑎 } ) ) )
68 simplr ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑃 ) ∧ ∀ 𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗 ) ∧ 𝑎 ∈ 𝐵 ) ∧ 𝑏 ∈ 𝐵 ) ∧ ( 𝑎 ( .r ‘ 𝑅 ) 𝑏 ) ∈ 𝑖 ) ∧ ¬ 𝑎 ∈ 𝑖 ) ∧ ¬ 𝑏 ∈ 𝑖 ) → ¬ 𝑎 ∈ 𝑖 )
69 62 67 68 ssnelpssd ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑃 ) ∧ ∀ 𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗 ) ∧ 𝑎 ∈ 𝐵 ) ∧ 𝑏 ∈ 𝐵 ) ∧ ( 𝑎 ( .r ‘ 𝑅 ) 𝑏 ) ∈ 𝑖 ) ∧ ¬ 𝑎 ∈ 𝑖 ) ∧ ¬ 𝑏 ∈ 𝑖 ) → 𝑖 ⊊ ( 𝑖 ( LSSum ‘ 𝑅 ) ( ( RSpan ‘ 𝑅 ) ‘ { 𝑎 } ) ) )
70 12 ad5antr ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑃 ) ∧ ∀ 𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗 ) ∧ 𝑎 ∈ 𝐵 ) ∧ 𝑏 ∈ 𝐵 ) ∧ ( 𝑎 ( .r ‘ 𝑅 ) 𝑏 ) ∈ 𝑖 ) ∧ ¬ 𝑎 ∈ 𝑖 ) ∧ ¬ 𝑏 ∈ 𝑖 ) → 𝑖 ∈ ( LIdeal ‘ 𝑅 ) )
71 1 60 55 52 70 57 lsmidl ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑃 ) ∧ ∀ 𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗 ) ∧ 𝑎 ∈ 𝐵 ) ∧ 𝑏 ∈ 𝐵 ) ∧ ( 𝑎 ( .r ‘ 𝑅 ) 𝑏 ) ∈ 𝑖 ) ∧ ¬ 𝑎 ∈ 𝑖 ) ∧ ¬ 𝑏 ∈ 𝑖 ) → ( 𝑖 ( LSSum ‘ 𝑅 ) ( ( RSpan ‘ 𝑅 ) ‘ { 𝑎 } ) ) ∈ ( LIdeal ‘ 𝑅 ) )
72 31 simprd ⊢ ( 𝑖 ∈ 𝑃 → 𝐼 ⊆ 𝑖 )
73 72 adantl ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝑃 ) → 𝐼 ⊆ 𝑖 )
74 73 ad6antr ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑃 ) ∧ ∀ 𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗 ) ∧ 𝑎 ∈ 𝐵 ) ∧ 𝑏 ∈ 𝐵 ) ∧ ( 𝑎 ( .r ‘ 𝑅 ) 𝑏 ) ∈ 𝑖 ) ∧ ¬ 𝑎 ∈ 𝑖 ) ∧ ¬ 𝑏 ∈ 𝑖 ) → 𝐼 ⊆ 𝑖 )
75 74 62 sstrd ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑃 ) ∧ ∀ 𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗 ) ∧ 𝑎 ∈ 𝐵 ) ∧ 𝑏 ∈ 𝐵 ) ∧ ( 𝑎 ( .r ‘ 𝑅 ) 𝑏 ) ∈ 𝑖 ) ∧ ¬ 𝑎 ∈ 𝑖 ) ∧ ¬ 𝑏 ∈ 𝑖 ) → 𝐼 ⊆ ( 𝑖 ( LSSum ‘ 𝑅 ) ( ( RSpan ‘ 𝑅 ) ‘ { 𝑎 } ) ) )
76 71 75 jca ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑃 ) ∧ ∀ 𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗 ) ∧ 𝑎 ∈ 𝐵 ) ∧ 𝑏 ∈ 𝐵 ) ∧ ( 𝑎 ( .r ‘ 𝑅 ) 𝑏 ) ∈ 𝑖 ) ∧ ¬ 𝑎 ∈ 𝑖 ) ∧ ¬ 𝑏 ∈ 𝑖 ) → ( ( 𝑖 ( LSSum ‘ 𝑅 ) ( ( RSpan ‘ 𝑅 ) ‘ { 𝑎 } ) ) ∈ ( LIdeal ‘ 𝑅 ) ∧ 𝐼 ⊆ ( 𝑖 ( LSSum ‘ 𝑅 ) ( ( RSpan ‘ 𝑅 ) ‘ { 𝑎 } ) ) ) )
77 simp-6r ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑃 ) ∧ ∀ 𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗 ) ∧ 𝑎 ∈ 𝐵 ) ∧ 𝑏 ∈ 𝐵 ) ∧ ( 𝑎 ( .r ‘ 𝑅 ) 𝑏 ) ∈ 𝑖 ) ∧ ¬ 𝑎 ∈ 𝑖 ) ∧ ¬ 𝑏 ∈ 𝑖 ) → ∀ 𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗 )
78 df-ral ⊢ ( ∀ 𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗 ↔ ∀ 𝑗 ( 𝑗 ∈ 𝑃 → ¬ 𝑖 ⊊ 𝑗 ) )
79 con2b ⊢ ( ( 𝑗 ∈ 𝑃 → ¬ 𝑖 ⊊ 𝑗 ) ↔ ( 𝑖 ⊊ 𝑗 → ¬ 𝑗 ∈ 𝑃 ) )
80 79 albii ⊢ ( ∀ 𝑗 ( 𝑗 ∈ 𝑃 → ¬ 𝑖 ⊊ 𝑗 ) ↔ ∀ 𝑗 ( 𝑖 ⊊ 𝑗 → ¬ 𝑗 ∈ 𝑃 ) )
81 78 80 bitri ⊢ ( ∀ 𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗 ↔ ∀ 𝑗 ( 𝑖 ⊊ 𝑗 → ¬ 𝑗 ∈ 𝑃 ) )
82 77 81 sylib ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑃 ) ∧ ∀ 𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗 ) ∧ 𝑎 ∈ 𝐵 ) ∧ 𝑏 ∈ 𝐵 ) ∧ ( 𝑎 ( .r ‘ 𝑅 ) 𝑏 ) ∈ 𝑖 ) ∧ ¬ 𝑎 ∈ 𝑖 ) ∧ ¬ 𝑏 ∈ 𝑖 ) → ∀ 𝑗 ( 𝑖 ⊊ 𝑗 → ¬ 𝑗 ∈ 𝑃 ) )
83 ineq2 ⊢ ( 𝑝 = 𝑗 → ( 𝑆 ∩ 𝑝 ) = ( 𝑆 ∩ 𝑗 ) )
84 83 eqeq1d ⊢ ( 𝑝 = 𝑗 → ( ( 𝑆 ∩ 𝑝 ) = ∅ ↔ ( 𝑆 ∩ 𝑗 ) = ∅ ) )
85 sseq2 ⊢ ( 𝑝 = 𝑗 → ( 𝐼 ⊆ 𝑝 ↔ 𝐼 ⊆ 𝑗 ) )
86 84 85 anbi12d ⊢ ( 𝑝 = 𝑗 → ( ( ( 𝑆 ∩ 𝑝 ) = ∅ ∧ 𝐼 ⊆ 𝑝 ) ↔ ( ( 𝑆 ∩ 𝑗 ) = ∅ ∧ 𝐼 ⊆ 𝑗 ) ) )
87 86 7 elrab2 ⊢ ( 𝑗 ∈ 𝑃 ↔ ( 𝑗 ∈ ( LIdeal ‘ 𝑅 ) ∧ ( ( 𝑆 ∩ 𝑗 ) = ∅ ∧ 𝐼 ⊆ 𝑗 ) ) )
88 87 baib ⊢ ( 𝑗 ∈ ( LIdeal ‘ 𝑅 ) → ( 𝑗 ∈ 𝑃 ↔ ( ( 𝑆 ∩ 𝑗 ) = ∅ ∧ 𝐼 ⊆ 𝑗 ) ) )
89 88 rbaibd ⊢ ( ( 𝑗 ∈ ( LIdeal ‘ 𝑅 ) ∧ 𝐼 ⊆ 𝑗 ) → ( 𝑗 ∈ 𝑃 ↔ ( 𝑆 ∩ 𝑗 ) = ∅ ) )
90 89 notbid ⊢ ( ( 𝑗 ∈ ( LIdeal ‘ 𝑅 ) ∧ 𝐼 ⊆ 𝑗 ) → ( ¬ 𝑗 ∈ 𝑃 ↔ ¬ ( 𝑆 ∩ 𝑗 ) = ∅ ) )
91 90 biimpcd ⊢ ( ¬ 𝑗 ∈ 𝑃 → ( ( 𝑗 ∈ ( LIdeal ‘ 𝑅 ) ∧ 𝐼 ⊆ 𝑗 ) → ¬ ( 𝑆 ∩ 𝑗 ) = ∅ ) )
92 91 imim2i ⊢ ( ( 𝑖 ⊊ 𝑗 → ¬ 𝑗 ∈ 𝑃 ) → ( 𝑖 ⊊ 𝑗 → ( ( 𝑗 ∈ ( LIdeal ‘ 𝑅 ) ∧ 𝐼 ⊆ 𝑗 ) → ¬ ( 𝑆 ∩ 𝑗 ) = ∅ ) ) )
93 92 impd ⊢ ( ( 𝑖 ⊊ 𝑗 → ¬ 𝑗 ∈ 𝑃 ) → ( ( 𝑖 ⊊ 𝑗 ∧ ( 𝑗 ∈ ( LIdeal ‘ 𝑅 ) ∧ 𝐼 ⊆ 𝑗 ) ) → ¬ ( 𝑆 ∩ 𝑗 ) = ∅ ) )
94 93 alimi ⊢ ( ∀ 𝑗 ( 𝑖 ⊊ 𝑗 → ¬ 𝑗 ∈ 𝑃 ) → ∀ 𝑗 ( ( 𝑖 ⊊ 𝑗 ∧ ( 𝑗 ∈ ( LIdeal ‘ 𝑅 ) ∧ 𝐼 ⊆ 𝑗 ) ) → ¬ ( 𝑆 ∩ 𝑗 ) = ∅ ) )
95 ovex ⊢ ( 𝑖 ( LSSum ‘ 𝑅 ) ( ( RSpan ‘ 𝑅 ) ‘ { 𝑎 } ) ) ∈ V
96 psseq2 ⊢ ( 𝑗 = ( 𝑖 ( LSSum ‘ 𝑅 ) ( ( RSpan ‘ 𝑅 ) ‘ { 𝑎 } ) ) → ( 𝑖 ⊊ 𝑗 ↔ 𝑖 ⊊ ( 𝑖 ( LSSum ‘ 𝑅 ) ( ( RSpan ‘ 𝑅 ) ‘ { 𝑎 } ) ) ) )
97 eleq1 ⊢ ( 𝑗 = ( 𝑖 ( LSSum ‘ 𝑅 ) ( ( RSpan ‘ 𝑅 ) ‘ { 𝑎 } ) ) → ( 𝑗 ∈ ( LIdeal ‘ 𝑅 ) ↔ ( 𝑖 ( LSSum ‘ 𝑅 ) ( ( RSpan ‘ 𝑅 ) ‘ { 𝑎 } ) ) ∈ ( LIdeal ‘ 𝑅 ) ) )
98 sseq2 ⊢ ( 𝑗 = ( 𝑖 ( LSSum ‘ 𝑅 ) ( ( RSpan ‘ 𝑅 ) ‘ { 𝑎 } ) ) → ( 𝐼 ⊆ 𝑗 ↔ 𝐼 ⊆ ( 𝑖 ( LSSum ‘ 𝑅 ) ( ( RSpan ‘ 𝑅 ) ‘ { 𝑎 } ) ) ) )
99 97 98 anbi12d ⊢ ( 𝑗 = ( 𝑖 ( LSSum ‘ 𝑅 ) ( ( RSpan ‘ 𝑅 ) ‘ { 𝑎 } ) ) → ( ( 𝑗 ∈ ( LIdeal ‘ 𝑅 ) ∧ 𝐼 ⊆ 𝑗 ) ↔ ( ( 𝑖 ( LSSum ‘ 𝑅 ) ( ( RSpan ‘ 𝑅 ) ‘ { 𝑎 } ) ) ∈ ( LIdeal ‘ 𝑅 ) ∧ 𝐼 ⊆ ( 𝑖 ( LSSum ‘ 𝑅 ) ( ( RSpan ‘ 𝑅 ) ‘ { 𝑎 } ) ) ) ) )
100 96 99 anbi12d ⊢ ( 𝑗 = ( 𝑖 ( LSSum ‘ 𝑅 ) ( ( RSpan ‘ 𝑅 ) ‘ { 𝑎 } ) ) → ( ( 𝑖 ⊊ 𝑗 ∧ ( 𝑗 ∈ ( LIdeal ‘ 𝑅 ) ∧ 𝐼 ⊆ 𝑗 ) ) ↔ ( 𝑖 ⊊ ( 𝑖 ( LSSum ‘ 𝑅 ) ( ( RSpan ‘ 𝑅 ) ‘ { 𝑎 } ) ) ∧ ( ( 𝑖 ( LSSum ‘ 𝑅 ) ( ( RSpan ‘ 𝑅 ) ‘ { 𝑎 } ) ) ∈ ( LIdeal ‘ 𝑅 ) ∧ 𝐼 ⊆ ( 𝑖 ( LSSum ‘ 𝑅 ) ( ( RSpan ‘ 𝑅 ) ‘ { 𝑎 } ) ) ) ) ) )
101 ineq2 ⊢ ( 𝑗 = ( 𝑖 ( LSSum ‘ 𝑅 ) ( ( RSpan ‘ 𝑅 ) ‘ { 𝑎 } ) ) → ( 𝑆 ∩ 𝑗 ) = ( 𝑆 ∩ ( 𝑖 ( LSSum ‘ 𝑅 ) ( ( RSpan ‘ 𝑅 ) ‘ { 𝑎 } ) ) ) )
102 101 eqeq1d ⊢ ( 𝑗 = ( 𝑖 ( LSSum ‘ 𝑅 ) ( ( RSpan ‘ 𝑅 ) ‘ { 𝑎 } ) ) → ( ( 𝑆 ∩ 𝑗 ) = ∅ ↔ ( 𝑆 ∩ ( 𝑖 ( LSSum ‘ 𝑅 ) ( ( RSpan ‘ 𝑅 ) ‘ { 𝑎 } ) ) ) = ∅ ) )
103 102 notbid ⊢ ( 𝑗 = ( 𝑖 ( LSSum ‘ 𝑅 ) ( ( RSpan ‘ 𝑅 ) ‘ { 𝑎 } ) ) → ( ¬ ( 𝑆 ∩ 𝑗 ) = ∅ ↔ ¬ ( 𝑆 ∩ ( 𝑖 ( LSSum ‘ 𝑅 ) ( ( RSpan ‘ 𝑅 ) ‘ { 𝑎 } ) ) ) = ∅ ) )
104 100 103 imbi12d ⊢ ( 𝑗 = ( 𝑖 ( LSSum ‘ 𝑅 ) ( ( RSpan ‘ 𝑅 ) ‘ { 𝑎 } ) ) → ( ( ( 𝑖 ⊊ 𝑗 ∧ ( 𝑗 ∈ ( LIdeal ‘ 𝑅 ) ∧ 𝐼 ⊆ 𝑗 ) ) → ¬ ( 𝑆 ∩ 𝑗 ) = ∅ ) ↔ ( ( 𝑖 ⊊ ( 𝑖 ( LSSum ‘ 𝑅 ) ( ( RSpan ‘ 𝑅 ) ‘ { 𝑎 } ) ) ∧ ( ( 𝑖 ( LSSum ‘ 𝑅 ) ( ( RSpan ‘ 𝑅 ) ‘ { 𝑎 } ) ) ∈ ( LIdeal ‘ 𝑅 ) ∧ 𝐼 ⊆ ( 𝑖 ( LSSum ‘ 𝑅 ) ( ( RSpan ‘ 𝑅 ) ‘ { 𝑎 } ) ) ) ) → ¬ ( 𝑆 ∩ ( 𝑖 ( LSSum ‘ 𝑅 ) ( ( RSpan ‘ 𝑅 ) ‘ { 𝑎 } ) ) ) = ∅ ) ) )
105 95 104 spcv ⊢ ( ∀ 𝑗 ( ( 𝑖 ⊊ 𝑗 ∧ ( 𝑗 ∈ ( LIdeal ‘ 𝑅 ) ∧ 𝐼 ⊆ 𝑗 ) ) → ¬ ( 𝑆 ∩ 𝑗 ) = ∅ ) → ( ( 𝑖 ⊊ ( 𝑖 ( LSSum ‘ 𝑅 ) ( ( RSpan ‘ 𝑅 ) ‘ { 𝑎 } ) ) ∧ ( ( 𝑖 ( LSSum ‘ 𝑅 ) ( ( RSpan ‘ 𝑅 ) ‘ { 𝑎 } ) ) ∈ ( LIdeal ‘ 𝑅 ) ∧ 𝐼 ⊆ ( 𝑖 ( LSSum ‘ 𝑅 ) ( ( RSpan ‘ 𝑅 ) ‘ { 𝑎 } ) ) ) ) → ¬ ( 𝑆 ∩ ( 𝑖 ( LSSum ‘ 𝑅 ) ( ( RSpan ‘ 𝑅 ) ‘ { 𝑎 } ) ) ) = ∅ ) )
106 82 94 105 3syl ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑃 ) ∧ ∀ 𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗 ) ∧ 𝑎 ∈ 𝐵 ) ∧ 𝑏 ∈ 𝐵 ) ∧ ( 𝑎 ( .r ‘ 𝑅 ) 𝑏 ) ∈ 𝑖 ) ∧ ¬ 𝑎 ∈ 𝑖 ) ∧ ¬ 𝑏 ∈ 𝑖 ) → ( ( 𝑖 ⊊ ( 𝑖 ( LSSum ‘ 𝑅 ) ( ( RSpan ‘ 𝑅 ) ‘ { 𝑎 } ) ) ∧ ( ( 𝑖 ( LSSum ‘ 𝑅 ) ( ( RSpan ‘ 𝑅 ) ‘ { 𝑎 } ) ) ∈ ( LIdeal ‘ 𝑅 ) ∧ 𝐼 ⊆ ( 𝑖 ( LSSum ‘ 𝑅 ) ( ( RSpan ‘ 𝑅 ) ‘ { 𝑎 } ) ) ) ) → ¬ ( 𝑆 ∩ ( 𝑖 ( LSSum ‘ 𝑅 ) ( ( RSpan ‘ 𝑅 ) ‘ { 𝑎 } ) ) ) = ∅ ) )
107 69 76 106 mp2and ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑃 ) ∧ ∀ 𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗 ) ∧ 𝑎 ∈ 𝐵 ) ∧ 𝑏 ∈ 𝐵 ) ∧ ( 𝑎 ( .r ‘ 𝑅 ) 𝑏 ) ∈ 𝑖 ) ∧ ¬ 𝑎 ∈ 𝑖 ) ∧ ¬ 𝑏 ∈ 𝑖 ) → ¬ ( 𝑆 ∩ ( 𝑖 ( LSSum ‘ 𝑅 ) ( ( RSpan ‘ 𝑅 ) ‘ { 𝑎 } ) ) ) = ∅ )
108 neq0 ⊢ ( ¬ ( 𝑆 ∩ ( 𝑖 ( LSSum ‘ 𝑅 ) ( ( RSpan ‘ 𝑅 ) ‘ { 𝑎 } ) ) ) = ∅ ↔ ∃ 𝑒 𝑒 ∈ ( 𝑆 ∩ ( 𝑖 ( LSSum ‘ 𝑅 ) ( ( RSpan ‘ 𝑅 ) ‘ { 𝑎 } ) ) ) )
109 107 108 sylib ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑃 ) ∧ ∀ 𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗 ) ∧ 𝑎 ∈ 𝐵 ) ∧ 𝑏 ∈ 𝐵 ) ∧ ( 𝑎 ( .r ‘ 𝑅 ) 𝑏 ) ∈ 𝑖 ) ∧ ¬ 𝑎 ∈ 𝑖 ) ∧ ¬ 𝑏 ∈ 𝑖 ) → ∃ 𝑒 𝑒 ∈ ( 𝑆 ∩ ( 𝑖 ( LSSum ‘ 𝑅 ) ( ( RSpan ‘ 𝑅 ) ‘ { 𝑎 } ) ) ) )
110 simp-4r ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑃 ) ∧ ∀ 𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗 ) ∧ 𝑎 ∈ 𝐵 ) ∧ 𝑏 ∈ 𝐵 ) ∧ ( 𝑎 ( .r ‘ 𝑅 ) 𝑏 ) ∈ 𝑖 ) ∧ ¬ 𝑎 ∈ 𝑖 ) ∧ ¬ 𝑏 ∈ 𝑖 ) → 𝑏 ∈ 𝐵 )
111 110 snssd ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑃 ) ∧ ∀ 𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗 ) ∧ 𝑎 ∈ 𝐵 ) ∧ 𝑏 ∈ 𝐵 ) ∧ ( 𝑎 ( .r ‘ 𝑅 ) 𝑏 ) ∈ 𝑖 ) ∧ ¬ 𝑎 ∈ 𝑖 ) ∧ ¬ 𝑏 ∈ 𝑖 ) → { 𝑏 } ⊆ 𝐵 )
112 55 1 18 rspcl ⊢ ( ( 𝑅 ∈ Ring ∧ { 𝑏 } ⊆ 𝐵 ) → ( ( RSpan ‘ 𝑅 ) ‘ { 𝑏 } ) ∈ ( LIdeal ‘ 𝑅 ) )
113 52 111 112 syl2anc ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑃 ) ∧ ∀ 𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗 ) ∧ 𝑎 ∈ 𝐵 ) ∧ 𝑏 ∈ 𝐵 ) ∧ ( 𝑎 ( .r ‘ 𝑅 ) 𝑏 ) ∈ 𝑖 ) ∧ ¬ 𝑎 ∈ 𝑖 ) ∧ ¬ 𝑏 ∈ 𝑖 ) → ( ( RSpan ‘ 𝑅 ) ‘ { 𝑏 } ) ∈ ( LIdeal ‘ 𝑅 ) )
114 18 lidlsubg ⊢ ( ( 𝑅 ∈ Ring ∧ ( ( RSpan ‘ 𝑅 ) ‘ { 𝑏 } ) ∈ ( LIdeal ‘ 𝑅 ) ) → ( ( RSpan ‘ 𝑅 ) ‘ { 𝑏 } ) ∈ ( SubGrp ‘ 𝑅 ) )
115 52 113 114 syl2anc ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑃 ) ∧ ∀ 𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗 ) ∧ 𝑎 ∈ 𝐵 ) ∧ 𝑏 ∈ 𝐵 ) ∧ ( 𝑎 ( .r ‘ 𝑅 ) 𝑏 ) ∈ 𝑖 ) ∧ ¬ 𝑎 ∈ 𝑖 ) ∧ ¬ 𝑏 ∈ 𝑖 ) → ( ( RSpan ‘ 𝑅 ) ‘ { 𝑏 } ) ∈ ( SubGrp ‘ 𝑅 ) )
116 60 lsmub1 ⊢ ( ( 𝑖 ∈ ( SubGrp ‘ 𝑅 ) ∧ ( ( RSpan ‘ 𝑅 ) ‘ { 𝑏 } ) ∈ ( SubGrp ‘ 𝑅 ) ) → 𝑖 ⊆ ( 𝑖 ( LSSum ‘ 𝑅 ) ( ( RSpan ‘ 𝑅 ) ‘ { 𝑏 } ) ) )
117 51 115 116 syl2anc ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑃 ) ∧ ∀ 𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗 ) ∧ 𝑎 ∈ 𝐵 ) ∧ 𝑏 ∈ 𝐵 ) ∧ ( 𝑎 ( .r ‘ 𝑅 ) 𝑏 ) ∈ 𝑖 ) ∧ ¬ 𝑎 ∈ 𝑖 ) ∧ ¬ 𝑏 ∈ 𝑖 ) → 𝑖 ⊆ ( 𝑖 ( LSSum ‘ 𝑅 ) ( ( RSpan ‘ 𝑅 ) ‘ { 𝑏 } ) ) )
118 60 lsmub2 ⊢ ( ( 𝑖 ∈ ( SubGrp ‘ 𝑅 ) ∧ ( ( RSpan ‘ 𝑅 ) ‘ { 𝑏 } ) ∈ ( SubGrp ‘ 𝑅 ) ) → ( ( RSpan ‘ 𝑅 ) ‘ { 𝑏 } ) ⊆ ( 𝑖 ( LSSum ‘ 𝑅 ) ( ( RSpan ‘ 𝑅 ) ‘ { 𝑏 } ) ) )
119 51 115 118 syl2anc ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑃 ) ∧ ∀ 𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗 ) ∧ 𝑎 ∈ 𝐵 ) ∧ 𝑏 ∈ 𝐵 ) ∧ ( 𝑎 ( .r ‘ 𝑅 ) 𝑏 ) ∈ 𝑖 ) ∧ ¬ 𝑎 ∈ 𝑖 ) ∧ ¬ 𝑏 ∈ 𝑖 ) → ( ( RSpan ‘ 𝑅 ) ‘ { 𝑏 } ) ⊆ ( 𝑖 ( LSSum ‘ 𝑅 ) ( ( RSpan ‘ 𝑅 ) ‘ { 𝑏 } ) ) )
120 1 55 rspsnid ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑏 ∈ 𝐵 ) → 𝑏 ∈ ( ( RSpan ‘ 𝑅 ) ‘ { 𝑏 } ) )
121 52 110 120 syl2anc ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑃 ) ∧ ∀ 𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗 ) ∧ 𝑎 ∈ 𝐵 ) ∧ 𝑏 ∈ 𝐵 ) ∧ ( 𝑎 ( .r ‘ 𝑅 ) 𝑏 ) ∈ 𝑖 ) ∧ ¬ 𝑎 ∈ 𝑖 ) ∧ ¬ 𝑏 ∈ 𝑖 ) → 𝑏 ∈ ( ( RSpan ‘ 𝑅 ) ‘ { 𝑏 } ) )
122 119 121 sseldd ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑃 ) ∧ ∀ 𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗 ) ∧ 𝑎 ∈ 𝐵 ) ∧ 𝑏 ∈ 𝐵 ) ∧ ( 𝑎 ( .r ‘ 𝑅 ) 𝑏 ) ∈ 𝑖 ) ∧ ¬ 𝑎 ∈ 𝑖 ) ∧ ¬ 𝑏 ∈ 𝑖 ) → 𝑏 ∈ ( 𝑖 ( LSSum ‘ 𝑅 ) ( ( RSpan ‘ 𝑅 ) ‘ { 𝑏 } ) ) )
123 simpr ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑃 ) ∧ ∀ 𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗 ) ∧ 𝑎 ∈ 𝐵 ) ∧ 𝑏 ∈ 𝐵 ) ∧ ( 𝑎 ( .r ‘ 𝑅 ) 𝑏 ) ∈ 𝑖 ) ∧ ¬ 𝑎 ∈ 𝑖 ) ∧ ¬ 𝑏 ∈ 𝑖 ) → ¬ 𝑏 ∈ 𝑖 )
124 117 122 123 ssnelpssd ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑃 ) ∧ ∀ 𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗 ) ∧ 𝑎 ∈ 𝐵 ) ∧ 𝑏 ∈ 𝐵 ) ∧ ( 𝑎 ( .r ‘ 𝑅 ) 𝑏 ) ∈ 𝑖 ) ∧ ¬ 𝑎 ∈ 𝑖 ) ∧ ¬ 𝑏 ∈ 𝑖 ) → 𝑖 ⊊ ( 𝑖 ( LSSum ‘ 𝑅 ) ( ( RSpan ‘ 𝑅 ) ‘ { 𝑏 } ) ) )
125 1 60 55 52 70 113 lsmidl ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑃 ) ∧ ∀ 𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗 ) ∧ 𝑎 ∈ 𝐵 ) ∧ 𝑏 ∈ 𝐵 ) ∧ ( 𝑎 ( .r ‘ 𝑅 ) 𝑏 ) ∈ 𝑖 ) ∧ ¬ 𝑎 ∈ 𝑖 ) ∧ ¬ 𝑏 ∈ 𝑖 ) → ( 𝑖 ( LSSum ‘ 𝑅 ) ( ( RSpan ‘ 𝑅 ) ‘ { 𝑏 } ) ) ∈ ( LIdeal ‘ 𝑅 ) )
126 74 117 sstrd ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑃 ) ∧ ∀ 𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗 ) ∧ 𝑎 ∈ 𝐵 ) ∧ 𝑏 ∈ 𝐵 ) ∧ ( 𝑎 ( .r ‘ 𝑅 ) 𝑏 ) ∈ 𝑖 ) ∧ ¬ 𝑎 ∈ 𝑖 ) ∧ ¬ 𝑏 ∈ 𝑖 ) → 𝐼 ⊆ ( 𝑖 ( LSSum ‘ 𝑅 ) ( ( RSpan ‘ 𝑅 ) ‘ { 𝑏 } ) ) )
127 125 126 jca ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑃 ) ∧ ∀ 𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗 ) ∧ 𝑎 ∈ 𝐵 ) ∧ 𝑏 ∈ 𝐵 ) ∧ ( 𝑎 ( .r ‘ 𝑅 ) 𝑏 ) ∈ 𝑖 ) ∧ ¬ 𝑎 ∈ 𝑖 ) ∧ ¬ 𝑏 ∈ 𝑖 ) → ( ( 𝑖 ( LSSum ‘ 𝑅 ) ( ( RSpan ‘ 𝑅 ) ‘ { 𝑏 } ) ) ∈ ( LIdeal ‘ 𝑅 ) ∧ 𝐼 ⊆ ( 𝑖 ( LSSum ‘ 𝑅 ) ( ( RSpan ‘ 𝑅 ) ‘ { 𝑏 } ) ) ) )
128 ovex ⊢ ( 𝑖 ( LSSum ‘ 𝑅 ) ( ( RSpan ‘ 𝑅 ) ‘ { 𝑏 } ) ) ∈ V
129 psseq2 ⊢ ( 𝑗 = ( 𝑖 ( LSSum ‘ 𝑅 ) ( ( RSpan ‘ 𝑅 ) ‘ { 𝑏 } ) ) → ( 𝑖 ⊊ 𝑗 ↔ 𝑖 ⊊ ( 𝑖 ( LSSum ‘ 𝑅 ) ( ( RSpan ‘ 𝑅 ) ‘ { 𝑏 } ) ) ) )
130 eleq1 ⊢ ( 𝑗 = ( 𝑖 ( LSSum ‘ 𝑅 ) ( ( RSpan ‘ 𝑅 ) ‘ { 𝑏 } ) ) → ( 𝑗 ∈ ( LIdeal ‘ 𝑅 ) ↔ ( 𝑖 ( LSSum ‘ 𝑅 ) ( ( RSpan ‘ 𝑅 ) ‘ { 𝑏 } ) ) ∈ ( LIdeal ‘ 𝑅 ) ) )
131 sseq2 ⊢ ( 𝑗 = ( 𝑖 ( LSSum ‘ 𝑅 ) ( ( RSpan ‘ 𝑅 ) ‘ { 𝑏 } ) ) → ( 𝐼 ⊆ 𝑗 ↔ 𝐼 ⊆ ( 𝑖 ( LSSum ‘ 𝑅 ) ( ( RSpan ‘ 𝑅 ) ‘ { 𝑏 } ) ) ) )
132 130 131 anbi12d ⊢ ( 𝑗 = ( 𝑖 ( LSSum ‘ 𝑅 ) ( ( RSpan ‘ 𝑅 ) ‘ { 𝑏 } ) ) → ( ( 𝑗 ∈ ( LIdeal ‘ 𝑅 ) ∧ 𝐼 ⊆ 𝑗 ) ↔ ( ( 𝑖 ( LSSum ‘ 𝑅 ) ( ( RSpan ‘ 𝑅 ) ‘ { 𝑏 } ) ) ∈ ( LIdeal ‘ 𝑅 ) ∧ 𝐼 ⊆ ( 𝑖 ( LSSum ‘ 𝑅 ) ( ( RSpan ‘ 𝑅 ) ‘ { 𝑏 } ) ) ) ) )
133 129 132 anbi12d ⊢ ( 𝑗 = ( 𝑖 ( LSSum ‘ 𝑅 ) ( ( RSpan ‘ 𝑅 ) ‘ { 𝑏 } ) ) → ( ( 𝑖 ⊊ 𝑗 ∧ ( 𝑗 ∈ ( LIdeal ‘ 𝑅 ) ∧ 𝐼 ⊆ 𝑗 ) ) ↔ ( 𝑖 ⊊ ( 𝑖 ( LSSum ‘ 𝑅 ) ( ( RSpan ‘ 𝑅 ) ‘ { 𝑏 } ) ) ∧ ( ( 𝑖 ( LSSum ‘ 𝑅 ) ( ( RSpan ‘ 𝑅 ) ‘ { 𝑏 } ) ) ∈ ( LIdeal ‘ 𝑅 ) ∧ 𝐼 ⊆ ( 𝑖 ( LSSum ‘ 𝑅 ) ( ( RSpan ‘ 𝑅 ) ‘ { 𝑏 } ) ) ) ) ) )
134 ineq2 ⊢ ( 𝑗 = ( 𝑖 ( LSSum ‘ 𝑅 ) ( ( RSpan ‘ 𝑅 ) ‘ { 𝑏 } ) ) → ( 𝑆 ∩ 𝑗 ) = ( 𝑆 ∩ ( 𝑖 ( LSSum ‘ 𝑅 ) ( ( RSpan ‘ 𝑅 ) ‘ { 𝑏 } ) ) ) )
135 134 eqeq1d ⊢ ( 𝑗 = ( 𝑖 ( LSSum ‘ 𝑅 ) ( ( RSpan ‘ 𝑅 ) ‘ { 𝑏 } ) ) → ( ( 𝑆 ∩ 𝑗 ) = ∅ ↔ ( 𝑆 ∩ ( 𝑖 ( LSSum ‘ 𝑅 ) ( ( RSpan ‘ 𝑅 ) ‘ { 𝑏 } ) ) ) = ∅ ) )
136 135 notbid ⊢ ( 𝑗 = ( 𝑖 ( LSSum ‘ 𝑅 ) ( ( RSpan ‘ 𝑅 ) ‘ { 𝑏 } ) ) → ( ¬ ( 𝑆 ∩ 𝑗 ) = ∅ ↔ ¬ ( 𝑆 ∩ ( 𝑖 ( LSSum ‘ 𝑅 ) ( ( RSpan ‘ 𝑅 ) ‘ { 𝑏 } ) ) ) = ∅ ) )
137 133 136 imbi12d ⊢ ( 𝑗 = ( 𝑖 ( LSSum ‘ 𝑅 ) ( ( RSpan ‘ 𝑅 ) ‘ { 𝑏 } ) ) → ( ( ( 𝑖 ⊊ 𝑗 ∧ ( 𝑗 ∈ ( LIdeal ‘ 𝑅 ) ∧ 𝐼 ⊆ 𝑗 ) ) → ¬ ( 𝑆 ∩ 𝑗 ) = ∅ ) ↔ ( ( 𝑖 ⊊ ( 𝑖 ( LSSum ‘ 𝑅 ) ( ( RSpan ‘ 𝑅 ) ‘ { 𝑏 } ) ) ∧ ( ( 𝑖 ( LSSum ‘ 𝑅 ) ( ( RSpan ‘ 𝑅 ) ‘ { 𝑏 } ) ) ∈ ( LIdeal ‘ 𝑅 ) ∧ 𝐼 ⊆ ( 𝑖 ( LSSum ‘ 𝑅 ) ( ( RSpan ‘ 𝑅 ) ‘ { 𝑏 } ) ) ) ) → ¬ ( 𝑆 ∩ ( 𝑖 ( LSSum ‘ 𝑅 ) ( ( RSpan ‘ 𝑅 ) ‘ { 𝑏 } ) ) ) = ∅ ) ) )
138 128 137 spcv ⊢ ( ∀ 𝑗 ( ( 𝑖 ⊊ 𝑗 ∧ ( 𝑗 ∈ ( LIdeal ‘ 𝑅 ) ∧ 𝐼 ⊆ 𝑗 ) ) → ¬ ( 𝑆 ∩ 𝑗 ) = ∅ ) → ( ( 𝑖 ⊊ ( 𝑖 ( LSSum ‘ 𝑅 ) ( ( RSpan ‘ 𝑅 ) ‘ { 𝑏 } ) ) ∧ ( ( 𝑖 ( LSSum ‘ 𝑅 ) ( ( RSpan ‘ 𝑅 ) ‘ { 𝑏 } ) ) ∈ ( LIdeal ‘ 𝑅 ) ∧ 𝐼 ⊆ ( 𝑖 ( LSSum ‘ 𝑅 ) ( ( RSpan ‘ 𝑅 ) ‘ { 𝑏 } ) ) ) ) → ¬ ( 𝑆 ∩ ( 𝑖 ( LSSum ‘ 𝑅 ) ( ( RSpan ‘ 𝑅 ) ‘ { 𝑏 } ) ) ) = ∅ ) )
139 82 94 138 3syl ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑃 ) ∧ ∀ 𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗 ) ∧ 𝑎 ∈ 𝐵 ) ∧ 𝑏 ∈ 𝐵 ) ∧ ( 𝑎 ( .r ‘ 𝑅 ) 𝑏 ) ∈ 𝑖 ) ∧ ¬ 𝑎 ∈ 𝑖 ) ∧ ¬ 𝑏 ∈ 𝑖 ) → ( ( 𝑖 ⊊ ( 𝑖 ( LSSum ‘ 𝑅 ) ( ( RSpan ‘ 𝑅 ) ‘ { 𝑏 } ) ) ∧ ( ( 𝑖 ( LSSum ‘ 𝑅 ) ( ( RSpan ‘ 𝑅 ) ‘ { 𝑏 } ) ) ∈ ( LIdeal ‘ 𝑅 ) ∧ 𝐼 ⊆ ( 𝑖 ( LSSum ‘ 𝑅 ) ( ( RSpan ‘ 𝑅 ) ‘ { 𝑏 } ) ) ) ) → ¬ ( 𝑆 ∩ ( 𝑖 ( LSSum ‘ 𝑅 ) ( ( RSpan ‘ 𝑅 ) ‘ { 𝑏 } ) ) ) = ∅ ) )
140 124 127 139 mp2and ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑃 ) ∧ ∀ 𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗 ) ∧ 𝑎 ∈ 𝐵 ) ∧ 𝑏 ∈ 𝐵 ) ∧ ( 𝑎 ( .r ‘ 𝑅 ) 𝑏 ) ∈ 𝑖 ) ∧ ¬ 𝑎 ∈ 𝑖 ) ∧ ¬ 𝑏 ∈ 𝑖 ) → ¬ ( 𝑆 ∩ ( 𝑖 ( LSSum ‘ 𝑅 ) ( ( RSpan ‘ 𝑅 ) ‘ { 𝑏 } ) ) ) = ∅ )
141 neq0 ⊢ ( ¬ ( 𝑆 ∩ ( 𝑖 ( LSSum ‘ 𝑅 ) ( ( RSpan ‘ 𝑅 ) ‘ { 𝑏 } ) ) ) = ∅ ↔ ∃ 𝑓 𝑓 ∈ ( 𝑆 ∩ ( 𝑖 ( LSSum ‘ 𝑅 ) ( ( RSpan ‘ 𝑅 ) ‘ { 𝑏 } ) ) ) )
142 140 141 sylib ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑃 ) ∧ ∀ 𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗 ) ∧ 𝑎 ∈ 𝐵 ) ∧ 𝑏 ∈ 𝐵 ) ∧ ( 𝑎 ( .r ‘ 𝑅 ) 𝑏 ) ∈ 𝑖 ) ∧ ¬ 𝑎 ∈ 𝑖 ) ∧ ¬ 𝑏 ∈ 𝑖 ) → ∃ 𝑓 𝑓 ∈ ( 𝑆 ∩ ( 𝑖 ( LSSum ‘ 𝑅 ) ( ( RSpan ‘ 𝑅 ) ‘ { 𝑏 } ) ) ) )
143 142 adantr ⊢ ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑃 ) ∧ ∀ 𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗 ) ∧ 𝑎 ∈ 𝐵 ) ∧ 𝑏 ∈ 𝐵 ) ∧ ( 𝑎 ( .r ‘ 𝑅 ) 𝑏 ) ∈ 𝑖 ) ∧ ¬ 𝑎 ∈ 𝑖 ) ∧ ¬ 𝑏 ∈ 𝑖 ) ∧ 𝑒 ∈ ( 𝑆 ∩ ( 𝑖 ( LSSum ‘ 𝑅 ) ( ( RSpan ‘ 𝑅 ) ‘ { 𝑎 } ) ) ) ) → ∃ 𝑓 𝑓 ∈ ( 𝑆 ∩ ( 𝑖 ( LSSum ‘ 𝑅 ) ( ( RSpan ‘ 𝑅 ) ‘ { 𝑏 } ) ) ) )
144 52 ad2antrr ⊢ ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑃 ) ∧ ∀ 𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗 ) ∧ 𝑎 ∈ 𝐵 ) ∧ 𝑏 ∈ 𝐵 ) ∧ ( 𝑎 ( .r ‘ 𝑅 ) 𝑏 ) ∈ 𝑖 ) ∧ ¬ 𝑎 ∈ 𝑖 ) ∧ ¬ 𝑏 ∈ 𝑖 ) ∧ 𝑒 ∈ ( 𝑆 ∩ ( 𝑖 ( LSSum ‘ 𝑅 ) ( ( RSpan ‘ 𝑅 ) ‘ { 𝑎 } ) ) ) ) ∧ 𝑓 ∈ ( 𝑆 ∩ ( 𝑖 ( LSSum ‘ 𝑅 ) ( ( RSpan ‘ 𝑅 ) ‘ { 𝑏 } ) ) ) ) → 𝑅 ∈ Ring )
145 144 ad2antrr ⊢ ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑃 ) ∧ ∀ 𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗 ) ∧ 𝑎 ∈ 𝐵 ) ∧ 𝑏 ∈ 𝐵 ) ∧ ( 𝑎 ( .r ‘ 𝑅 ) 𝑏 ) ∈ 𝑖 ) ∧ ¬ 𝑎 ∈ 𝑖 ) ∧ ¬ 𝑏 ∈ 𝑖 ) ∧ 𝑒 ∈ ( 𝑆 ∩ ( 𝑖 ( LSSum ‘ 𝑅 ) ( ( RSpan ‘ 𝑅 ) ‘ { 𝑎 } ) ) ) ) ∧ 𝑓 ∈ ( 𝑆 ∩ ( 𝑖 ( LSSum ‘ 𝑅 ) ( ( RSpan ‘ 𝑅 ) ‘ { 𝑏 } ) ) ) ) ∧ 𝑥 ∈ 𝑖 ) ∧ 𝑒 = ( 𝑥 ( +g ‘ 𝑅 ) 𝑚 ) ) → 𝑅 ∈ Ring )
146 53 ad2antrr ⊢ ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑃 ) ∧ ∀ 𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗 ) ∧ 𝑎 ∈ 𝐵 ) ∧ 𝑏 ∈ 𝐵 ) ∧ ( 𝑎 ( .r ‘ 𝑅 ) 𝑏 ) ∈ 𝑖 ) ∧ ¬ 𝑎 ∈ 𝑖 ) ∧ ¬ 𝑏 ∈ 𝑖 ) ∧ 𝑒 ∈ ( 𝑆 ∩ ( 𝑖 ( LSSum ‘ 𝑅 ) ( ( RSpan ‘ 𝑅 ) ‘ { 𝑎 } ) ) ) ) ∧ 𝑓 ∈ ( 𝑆 ∩ ( 𝑖 ( LSSum ‘ 𝑅 ) ( ( RSpan ‘ 𝑅 ) ‘ { 𝑏 } ) ) ) ) → 𝑎 ∈ 𝐵 )
147 146 ad2antrr ⊢ ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑃 ) ∧ ∀ 𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗 ) ∧ 𝑎 ∈ 𝐵 ) ∧ 𝑏 ∈ 𝐵 ) ∧ ( 𝑎 ( .r ‘ 𝑅 ) 𝑏 ) ∈ 𝑖 ) ∧ ¬ 𝑎 ∈ 𝑖 ) ∧ ¬ 𝑏 ∈ 𝑖 ) ∧ 𝑒 ∈ ( 𝑆 ∩ ( 𝑖 ( LSSum ‘ 𝑅 ) ( ( RSpan ‘ 𝑅 ) ‘ { 𝑎 } ) ) ) ) ∧ 𝑓 ∈ ( 𝑆 ∩ ( 𝑖 ( LSSum ‘ 𝑅 ) ( ( RSpan ‘ 𝑅 ) ‘ { 𝑏 } ) ) ) ) ∧ 𝑥 ∈ 𝑖 ) ∧ 𝑒 = ( 𝑥 ( +g ‘ 𝑅 ) 𝑚 ) ) → 𝑎 ∈ 𝐵 )
148 eqid ⊢ ( .r ‘ 𝑅 ) = ( .r ‘ 𝑅 )
149 1 148 55 elrspsn ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑎 ∈ 𝐵 ) → ( 𝑚 ∈ ( ( RSpan ‘ 𝑅 ) ‘ { 𝑎 } ) ↔ ∃ 𝑜 ∈ 𝐵 𝑚 = ( 𝑜 ( .r ‘ 𝑅 ) 𝑎 ) ) )
150 145 147 149 syl2anc ⊢ ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑃 ) ∧ ∀ 𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗 ) ∧ 𝑎 ∈ 𝐵 ) ∧ 𝑏 ∈ 𝐵 ) ∧ ( 𝑎 ( .r ‘ 𝑅 ) 𝑏 ) ∈ 𝑖 ) ∧ ¬ 𝑎 ∈ 𝑖 ) ∧ ¬ 𝑏 ∈ 𝑖 ) ∧ 𝑒 ∈ ( 𝑆 ∩ ( 𝑖 ( LSSum ‘ 𝑅 ) ( ( RSpan ‘ 𝑅 ) ‘ { 𝑎 } ) ) ) ) ∧ 𝑓 ∈ ( 𝑆 ∩ ( 𝑖 ( LSSum ‘ 𝑅 ) ( ( RSpan ‘ 𝑅 ) ‘ { 𝑏 } ) ) ) ) ∧ 𝑥 ∈ 𝑖 ) ∧ 𝑒 = ( 𝑥 ( +g ‘ 𝑅 ) 𝑚 ) ) → ( 𝑚 ∈ ( ( RSpan ‘ 𝑅 ) ‘ { 𝑎 } ) ↔ ∃ 𝑜 ∈ 𝐵 𝑚 = ( 𝑜 ( .r ‘ 𝑅 ) 𝑎 ) ) )
151 144 ad6antr ⊢ ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑃 ) ∧ ∀ 𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗 ) ∧ 𝑎 ∈ 𝐵 ) ∧ 𝑏 ∈ 𝐵 ) ∧ ( 𝑎 ( .r ‘ 𝑅 ) 𝑏 ) ∈ 𝑖 ) ∧ ¬ 𝑎 ∈ 𝑖 ) ∧ ¬ 𝑏 ∈ 𝑖 ) ∧ 𝑒 ∈ ( 𝑆 ∩ ( 𝑖 ( LSSum ‘ 𝑅 ) ( ( RSpan ‘ 𝑅 ) ‘ { 𝑎 } ) ) ) ) ∧ 𝑓 ∈ ( 𝑆 ∩ ( 𝑖 ( LSSum ‘ 𝑅 ) ( ( RSpan ‘ 𝑅 ) ‘ { 𝑏 } ) ) ) ) ∧ 𝑥 ∈ 𝑖 ) ∧ 𝑒 = ( 𝑥 ( +g ‘ 𝑅 ) 𝑚 ) ) ∧ 𝑜 ∈ 𝐵 ) ∧ 𝑚 = ( 𝑜 ( .r ‘ 𝑅 ) 𝑎 ) ) ∧ 𝑦 ∈ 𝑖 ) ∧ 𝑓 = ( 𝑦 ( +g ‘ 𝑅 ) 𝑛 ) ) → 𝑅 ∈ Ring )
152 110 ad2antrr ⊢ ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑃 ) ∧ ∀ 𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗 ) ∧ 𝑎 ∈ 𝐵 ) ∧ 𝑏 ∈ 𝐵 ) ∧ ( 𝑎 ( .r ‘ 𝑅 ) 𝑏 ) ∈ 𝑖 ) ∧ ¬ 𝑎 ∈ 𝑖 ) ∧ ¬ 𝑏 ∈ 𝑖 ) ∧ 𝑒 ∈ ( 𝑆 ∩ ( 𝑖 ( LSSum ‘ 𝑅 ) ( ( RSpan ‘ 𝑅 ) ‘ { 𝑎 } ) ) ) ) ∧ 𝑓 ∈ ( 𝑆 ∩ ( 𝑖 ( LSSum ‘ 𝑅 ) ( ( RSpan ‘ 𝑅 ) ‘ { 𝑏 } ) ) ) ) → 𝑏 ∈ 𝐵 )
153 152 ad6antr ⊢ ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑃 ) ∧ ∀ 𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗 ) ∧ 𝑎 ∈ 𝐵 ) ∧ 𝑏 ∈ 𝐵 ) ∧ ( 𝑎 ( .r ‘ 𝑅 ) 𝑏 ) ∈ 𝑖 ) ∧ ¬ 𝑎 ∈ 𝑖 ) ∧ ¬ 𝑏 ∈ 𝑖 ) ∧ 𝑒 ∈ ( 𝑆 ∩ ( 𝑖 ( LSSum ‘ 𝑅 ) ( ( RSpan ‘ 𝑅 ) ‘ { 𝑎 } ) ) ) ) ∧ 𝑓 ∈ ( 𝑆 ∩ ( 𝑖 ( LSSum ‘ 𝑅 ) ( ( RSpan ‘ 𝑅 ) ‘ { 𝑏 } ) ) ) ) ∧ 𝑥 ∈ 𝑖 ) ∧ 𝑒 = ( 𝑥 ( +g ‘ 𝑅 ) 𝑚 ) ) ∧ 𝑜 ∈ 𝐵 ) ∧ 𝑚 = ( 𝑜 ( .r ‘ 𝑅 ) 𝑎 ) ) ∧ 𝑦 ∈ 𝑖 ) ∧ 𝑓 = ( 𝑦 ( +g ‘ 𝑅 ) 𝑛 ) ) → 𝑏 ∈ 𝐵 )
154 1 148 55 elrspsn ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑏 ∈ 𝐵 ) → ( 𝑛 ∈ ( ( RSpan ‘ 𝑅 ) ‘ { 𝑏 } ) ↔ ∃ 𝑞 ∈ 𝐵 𝑛 = ( 𝑞 ( .r ‘ 𝑅 ) 𝑏 ) ) )
155 151 153 154 syl2anc ⊢ ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑃 ) ∧ ∀ 𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗 ) ∧ 𝑎 ∈ 𝐵 ) ∧ 𝑏 ∈ 𝐵 ) ∧ ( 𝑎 ( .r ‘ 𝑅 ) 𝑏 ) ∈ 𝑖 ) ∧ ¬ 𝑎 ∈ 𝑖 ) ∧ ¬ 𝑏 ∈ 𝑖 ) ∧ 𝑒 ∈ ( 𝑆 ∩ ( 𝑖 ( LSSum ‘ 𝑅 ) ( ( RSpan ‘ 𝑅 ) ‘ { 𝑎 } ) ) ) ) ∧ 𝑓 ∈ ( 𝑆 ∩ ( 𝑖 ( LSSum ‘ 𝑅 ) ( ( RSpan ‘ 𝑅 ) ‘ { 𝑏 } ) ) ) ) ∧ 𝑥 ∈ 𝑖 ) ∧ 𝑒 = ( 𝑥 ( +g ‘ 𝑅 ) 𝑚 ) ) ∧ 𝑜 ∈ 𝐵 ) ∧ 𝑚 = ( 𝑜 ( .r ‘ 𝑅 ) 𝑎 ) ) ∧ 𝑦 ∈ 𝑖 ) ∧ 𝑓 = ( 𝑦 ( +g ‘ 𝑅 ) 𝑛 ) ) → ( 𝑛 ∈ ( ( RSpan ‘ 𝑅 ) ‘ { 𝑏 } ) ↔ ∃ 𝑞 ∈ 𝐵 𝑛 = ( 𝑞 ( .r ‘ 𝑅 ) 𝑏 ) ) )
156 simp-7r ⊢ ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑃 ) ∧ ∀ 𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗 ) ∧ 𝑎 ∈ 𝐵 ) ∧ 𝑏 ∈ 𝐵 ) ∧ ( 𝑎 ( .r ‘ 𝑅 ) 𝑏 ) ∈ 𝑖 ) ∧ ¬ 𝑎 ∈ 𝑖 ) ∧ ¬ 𝑏 ∈ 𝑖 ) ∧ 𝑒 ∈ ( 𝑆 ∩ ( 𝑖 ( LSSum ‘ 𝑅 ) ( ( RSpan ‘ 𝑅 ) ‘ { 𝑎 } ) ) ) ) ∧ 𝑓 ∈ ( 𝑆 ∩ ( 𝑖 ( LSSum ‘ 𝑅 ) ( ( RSpan ‘ 𝑅 ) ‘ { 𝑏 } ) ) ) ) ∧ 𝑥 ∈ 𝑖 ) ∧ 𝑒 = ( 𝑥 ( +g ‘ 𝑅 ) 𝑚 ) ) ∧ 𝑜 ∈ 𝐵 ) ∧ 𝑚 = ( 𝑜 ( .r ‘ 𝑅 ) 𝑎 ) ) ∧ 𝑦 ∈ 𝑖 ) ∧ 𝑓 = ( 𝑦 ( +g ‘ 𝑅 ) 𝑛 ) ) ∧ 𝑞 ∈ 𝐵 ) ∧ 𝑛 = ( 𝑞 ( .r ‘ 𝑅 ) 𝑏 ) ) → 𝑒 = ( 𝑥 ( +g ‘ 𝑅 ) 𝑚 ) )
157 simpllr ⊢ ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑃 ) ∧ ∀ 𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗 ) ∧ 𝑎 ∈ 𝐵 ) ∧ 𝑏 ∈ 𝐵 ) ∧ ( 𝑎 ( .r ‘ 𝑅 ) 𝑏 ) ∈ 𝑖 ) ∧ ¬ 𝑎 ∈ 𝑖 ) ∧ ¬ 𝑏 ∈ 𝑖 ) ∧ 𝑒 ∈ ( 𝑆 ∩ ( 𝑖 ( LSSum ‘ 𝑅 ) ( ( RSpan ‘ 𝑅 ) ‘ { 𝑎 } ) ) ) ) ∧ 𝑓 ∈ ( 𝑆 ∩ ( 𝑖 ( LSSum ‘ 𝑅 ) ( ( RSpan ‘ 𝑅 ) ‘ { 𝑏 } ) ) ) ) ∧ 𝑥 ∈ 𝑖 ) ∧ 𝑒 = ( 𝑥 ( +g ‘ 𝑅 ) 𝑚 ) ) ∧ 𝑜 ∈ 𝐵 ) ∧ 𝑚 = ( 𝑜 ( .r ‘ 𝑅 ) 𝑎 ) ) ∧ 𝑦 ∈ 𝑖 ) ∧ 𝑓 = ( 𝑦 ( +g ‘ 𝑅 ) 𝑛 ) ) ∧ 𝑞 ∈ 𝐵 ) ∧ 𝑛 = ( 𝑞 ( .r ‘ 𝑅 ) 𝑏 ) ) → 𝑓 = ( 𝑦 ( +g ‘ 𝑅 ) 𝑛 ) )
158 156 157 oveq12d ⊢ ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑃 ) ∧ ∀ 𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗 ) ∧ 𝑎 ∈ 𝐵 ) ∧ 𝑏 ∈ 𝐵 ) ∧ ( 𝑎 ( .r ‘ 𝑅 ) 𝑏 ) ∈ 𝑖 ) ∧ ¬ 𝑎 ∈ 𝑖 ) ∧ ¬ 𝑏 ∈ 𝑖 ) ∧ 𝑒 ∈ ( 𝑆 ∩ ( 𝑖 ( LSSum ‘ 𝑅 ) ( ( RSpan ‘ 𝑅 ) ‘ { 𝑎 } ) ) ) ) ∧ 𝑓 ∈ ( 𝑆 ∩ ( 𝑖 ( LSSum ‘ 𝑅 ) ( ( RSpan ‘ 𝑅 ) ‘ { 𝑏 } ) ) ) ) ∧ 𝑥 ∈ 𝑖 ) ∧ 𝑒 = ( 𝑥 ( +g ‘ 𝑅 ) 𝑚 ) ) ∧ 𝑜 ∈ 𝐵 ) ∧ 𝑚 = ( 𝑜 ( .r ‘ 𝑅 ) 𝑎 ) ) ∧ 𝑦 ∈ 𝑖 ) ∧ 𝑓 = ( 𝑦 ( +g ‘ 𝑅 ) 𝑛 ) ) ∧ 𝑞 ∈ 𝐵 ) ∧ 𝑛 = ( 𝑞 ( .r ‘ 𝑅 ) 𝑏 ) ) → ( 𝑒 ( .r ‘ 𝑅 ) 𝑓 ) = ( ( 𝑥 ( +g ‘ 𝑅 ) 𝑚 ) ( .r ‘ 𝑅 ) ( 𝑦 ( +g ‘ 𝑅 ) 𝑛 ) ) )
159 simp-5r ⊢ ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑃 ) ∧ ∀ 𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗 ) ∧ 𝑎 ∈ 𝐵 ) ∧ 𝑏 ∈ 𝐵 ) ∧ ( 𝑎 ( .r ‘ 𝑅 ) 𝑏 ) ∈ 𝑖 ) ∧ ¬ 𝑎 ∈ 𝑖 ) ∧ ¬ 𝑏 ∈ 𝑖 ) ∧ 𝑒 ∈ ( 𝑆 ∩ ( 𝑖 ( LSSum ‘ 𝑅 ) ( ( RSpan ‘ 𝑅 ) ‘ { 𝑎 } ) ) ) ) ∧ 𝑓 ∈ ( 𝑆 ∩ ( 𝑖 ( LSSum ‘ 𝑅 ) ( ( RSpan ‘ 𝑅 ) ‘ { 𝑏 } ) ) ) ) ∧ 𝑥 ∈ 𝑖 ) ∧ 𝑒 = ( 𝑥 ( +g ‘ 𝑅 ) 𝑚 ) ) ∧ 𝑜 ∈ 𝐵 ) ∧ 𝑚 = ( 𝑜 ( .r ‘ 𝑅 ) 𝑎 ) ) ∧ 𝑦 ∈ 𝑖 ) ∧ 𝑓 = ( 𝑦 ( +g ‘ 𝑅 ) 𝑛 ) ) ∧ 𝑞 ∈ 𝐵 ) ∧ 𝑛 = ( 𝑞 ( .r ‘ 𝑅 ) 𝑏 ) ) → 𝑚 = ( 𝑜 ( .r ‘ 𝑅 ) 𝑎 ) )
160 159 oveq2d ⊢ ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑃 ) ∧ ∀ 𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗 ) ∧ 𝑎 ∈ 𝐵 ) ∧ 𝑏 ∈ 𝐵 ) ∧ ( 𝑎 ( .r ‘ 𝑅 ) 𝑏 ) ∈ 𝑖 ) ∧ ¬ 𝑎 ∈ 𝑖 ) ∧ ¬ 𝑏 ∈ 𝑖 ) ∧ 𝑒 ∈ ( 𝑆 ∩ ( 𝑖 ( LSSum ‘ 𝑅 ) ( ( RSpan ‘ 𝑅 ) ‘ { 𝑎 } ) ) ) ) ∧ 𝑓 ∈ ( 𝑆 ∩ ( 𝑖 ( LSSum ‘ 𝑅 ) ( ( RSpan ‘ 𝑅 ) ‘ { 𝑏 } ) ) ) ) ∧ 𝑥 ∈ 𝑖 ) ∧ 𝑒 = ( 𝑥 ( +g ‘ 𝑅 ) 𝑚 ) ) ∧ 𝑜 ∈ 𝐵 ) ∧ 𝑚 = ( 𝑜 ( .r ‘ 𝑅 ) 𝑎 ) ) ∧ 𝑦 ∈ 𝑖 ) ∧ 𝑓 = ( 𝑦 ( +g ‘ 𝑅 ) 𝑛 ) ) ∧ 𝑞 ∈ 𝐵 ) ∧ 𝑛 = ( 𝑞 ( .r ‘ 𝑅 ) 𝑏 ) ) → ( 𝑥 ( +g ‘ 𝑅 ) 𝑚 ) = ( 𝑥 ( +g ‘ 𝑅 ) ( 𝑜 ( .r ‘ 𝑅 ) 𝑎 ) ) )
161 simpr ⊢ ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑃 ) ∧ ∀ 𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗 ) ∧ 𝑎 ∈ 𝐵 ) ∧ 𝑏 ∈ 𝐵 ) ∧ ( 𝑎 ( .r ‘ 𝑅 ) 𝑏 ) ∈ 𝑖 ) ∧ ¬ 𝑎 ∈ 𝑖 ) ∧ ¬ 𝑏 ∈ 𝑖 ) ∧ 𝑒 ∈ ( 𝑆 ∩ ( 𝑖 ( LSSum ‘ 𝑅 ) ( ( RSpan ‘ 𝑅 ) ‘ { 𝑎 } ) ) ) ) ∧ 𝑓 ∈ ( 𝑆 ∩ ( 𝑖 ( LSSum ‘ 𝑅 ) ( ( RSpan ‘ 𝑅 ) ‘ { 𝑏 } ) ) ) ) ∧ 𝑥 ∈ 𝑖 ) ∧ 𝑒 = ( 𝑥 ( +g ‘ 𝑅 ) 𝑚 ) ) ∧ 𝑜 ∈ 𝐵 ) ∧ 𝑚 = ( 𝑜 ( .r ‘ 𝑅 ) 𝑎 ) ) ∧ 𝑦 ∈ 𝑖 ) ∧ 𝑓 = ( 𝑦 ( +g ‘ 𝑅 ) 𝑛 ) ) ∧ 𝑞 ∈ 𝐵 ) ∧ 𝑛 = ( 𝑞 ( .r ‘ 𝑅 ) 𝑏 ) ) → 𝑛 = ( 𝑞 ( .r ‘ 𝑅 ) 𝑏 ) )
162 161 oveq2d ⊢ ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑃 ) ∧ ∀ 𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗 ) ∧ 𝑎 ∈ 𝐵 ) ∧ 𝑏 ∈ 𝐵 ) ∧ ( 𝑎 ( .r ‘ 𝑅 ) 𝑏 ) ∈ 𝑖 ) ∧ ¬ 𝑎 ∈ 𝑖 ) ∧ ¬ 𝑏 ∈ 𝑖 ) ∧ 𝑒 ∈ ( 𝑆 ∩ ( 𝑖 ( LSSum ‘ 𝑅 ) ( ( RSpan ‘ 𝑅 ) ‘ { 𝑎 } ) ) ) ) ∧ 𝑓 ∈ ( 𝑆 ∩ ( 𝑖 ( LSSum ‘ 𝑅 ) ( ( RSpan ‘ 𝑅 ) ‘ { 𝑏 } ) ) ) ) ∧ 𝑥 ∈ 𝑖 ) ∧ 𝑒 = ( 𝑥 ( +g ‘ 𝑅 ) 𝑚 ) ) ∧ 𝑜 ∈ 𝐵 ) ∧ 𝑚 = ( 𝑜 ( .r ‘ 𝑅 ) 𝑎 ) ) ∧ 𝑦 ∈ 𝑖 ) ∧ 𝑓 = ( 𝑦 ( +g ‘ 𝑅 ) 𝑛 ) ) ∧ 𝑞 ∈ 𝐵 ) ∧ 𝑛 = ( 𝑞 ( .r ‘ 𝑅 ) 𝑏 ) ) → ( 𝑦 ( +g ‘ 𝑅 ) 𝑛 ) = ( 𝑦 ( +g ‘ 𝑅 ) ( 𝑞 ( .r ‘ 𝑅 ) 𝑏 ) ) )
163 160 162 oveq12d ⊢ ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑃 ) ∧ ∀ 𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗 ) ∧ 𝑎 ∈ 𝐵 ) ∧ 𝑏 ∈ 𝐵 ) ∧ ( 𝑎 ( .r ‘ 𝑅 ) 𝑏 ) ∈ 𝑖 ) ∧ ¬ 𝑎 ∈ 𝑖 ) ∧ ¬ 𝑏 ∈ 𝑖 ) ∧ 𝑒 ∈ ( 𝑆 ∩ ( 𝑖 ( LSSum ‘ 𝑅 ) ( ( RSpan ‘ 𝑅 ) ‘ { 𝑎 } ) ) ) ) ∧ 𝑓 ∈ ( 𝑆 ∩ ( 𝑖 ( LSSum ‘ 𝑅 ) ( ( RSpan ‘ 𝑅 ) ‘ { 𝑏 } ) ) ) ) ∧ 𝑥 ∈ 𝑖 ) ∧ 𝑒 = ( 𝑥 ( +g ‘ 𝑅 ) 𝑚 ) ) ∧ 𝑜 ∈ 𝐵 ) ∧ 𝑚 = ( 𝑜 ( .r ‘ 𝑅 ) 𝑎 ) ) ∧ 𝑦 ∈ 𝑖 ) ∧ 𝑓 = ( 𝑦 ( +g ‘ 𝑅 ) 𝑛 ) ) ∧ 𝑞 ∈ 𝐵 ) ∧ 𝑛 = ( 𝑞 ( .r ‘ 𝑅 ) 𝑏 ) ) → ( ( 𝑥 ( +g ‘ 𝑅 ) 𝑚 ) ( .r ‘ 𝑅 ) ( 𝑦 ( +g ‘ 𝑅 ) 𝑛 ) ) = ( ( 𝑥 ( +g ‘ 𝑅 ) ( 𝑜 ( .r ‘ 𝑅 ) 𝑎 ) ) ( .r ‘ 𝑅 ) ( 𝑦 ( +g ‘ 𝑅 ) ( 𝑞 ( .r ‘ 𝑅 ) 𝑏 ) ) ) )
164 eqid ⊢ ( +g ‘ 𝑅 ) = ( +g ‘ 𝑅 )
165 151 ad2antrr ⊢ ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑃 ) ∧ ∀ 𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗 ) ∧ 𝑎 ∈ 𝐵 ) ∧ 𝑏 ∈ 𝐵 ) ∧ ( 𝑎 ( .r ‘ 𝑅 ) 𝑏 ) ∈ 𝑖 ) ∧ ¬ 𝑎 ∈ 𝑖 ) ∧ ¬ 𝑏 ∈ 𝑖 ) ∧ 𝑒 ∈ ( 𝑆 ∩ ( 𝑖 ( LSSum ‘ 𝑅 ) ( ( RSpan ‘ 𝑅 ) ‘ { 𝑎 } ) ) ) ) ∧ 𝑓 ∈ ( 𝑆 ∩ ( 𝑖 ( LSSum ‘ 𝑅 ) ( ( RSpan ‘ 𝑅 ) ‘ { 𝑏 } ) ) ) ) ∧ 𝑥 ∈ 𝑖 ) ∧ 𝑒 = ( 𝑥 ( +g ‘ 𝑅 ) 𝑚 ) ) ∧ 𝑜 ∈ 𝐵 ) ∧ 𝑚 = ( 𝑜 ( .r ‘ 𝑅 ) 𝑎 ) ) ∧ 𝑦 ∈ 𝑖 ) ∧ 𝑓 = ( 𝑦 ( +g ‘ 𝑅 ) 𝑛 ) ) ∧ 𝑞 ∈ 𝐵 ) ∧ 𝑛 = ( 𝑞 ( .r ‘ 𝑅 ) 𝑏 ) ) → 𝑅 ∈ Ring )
166 21 ad7antr ⊢ ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑃 ) ∧ ∀ 𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗 ) ∧ 𝑎 ∈ 𝐵 ) ∧ 𝑏 ∈ 𝐵 ) ∧ ( 𝑎 ( .r ‘ 𝑅 ) 𝑏 ) ∈ 𝑖 ) ∧ ¬ 𝑎 ∈ 𝑖 ) ∧ ¬ 𝑏 ∈ 𝑖 ) ∧ 𝑒 ∈ ( 𝑆 ∩ ( 𝑖 ( LSSum ‘ 𝑅 ) ( ( RSpan ‘ 𝑅 ) ‘ { 𝑎 } ) ) ) ) ∧ 𝑓 ∈ ( 𝑆 ∩ ( 𝑖 ( LSSum ‘ 𝑅 ) ( ( RSpan ‘ 𝑅 ) ‘ { 𝑏 } ) ) ) ) → 𝑖 ⊆ 𝐵 )
167 166 ad4antr ⊢ ( ( ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑃 ) ∧ ∀ 𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗 ) ∧ 𝑎 ∈ 𝐵 ) ∧ 𝑏 ∈ 𝐵 ) ∧ ( 𝑎 ( .r ‘ 𝑅 ) 𝑏 ) ∈ 𝑖 ) ∧ ¬ 𝑎 ∈ 𝑖 ) ∧ ¬ 𝑏 ∈ 𝑖 ) ∧ 𝑒 ∈ ( 𝑆 ∩ ( 𝑖 ( LSSum ‘ 𝑅 ) ( ( RSpan ‘ 𝑅 ) ‘ { 𝑎 } ) ) ) ) ∧ 𝑓 ∈ ( 𝑆 ∩ ( 𝑖 ( LSSum ‘ 𝑅 ) ( ( RSpan ‘ 𝑅 ) ‘ { 𝑏 } ) ) ) ) ∧ 𝑥 ∈ 𝑖 ) ∧ 𝑒 = ( 𝑥 ( +g ‘ 𝑅 ) 𝑚 ) ) ∧ 𝑜 ∈ 𝐵 ) ∧ 𝑚 = ( 𝑜 ( .r ‘ 𝑅 ) 𝑎 ) ) → 𝑖 ⊆ 𝐵 )
168 167 ad4antr ⊢ ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑃 ) ∧ ∀ 𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗 ) ∧ 𝑎 ∈ 𝐵 ) ∧ 𝑏 ∈ 𝐵 ) ∧ ( 𝑎 ( .r ‘ 𝑅 ) 𝑏 ) ∈ 𝑖 ) ∧ ¬ 𝑎 ∈ 𝑖 ) ∧ ¬ 𝑏 ∈ 𝑖 ) ∧ 𝑒 ∈ ( 𝑆 ∩ ( 𝑖 ( LSSum ‘ 𝑅 ) ( ( RSpan ‘ 𝑅 ) ‘ { 𝑎 } ) ) ) ) ∧ 𝑓 ∈ ( 𝑆 ∩ ( 𝑖 ( LSSum ‘ 𝑅 ) ( ( RSpan ‘ 𝑅 ) ‘ { 𝑏 } ) ) ) ) ∧ 𝑥 ∈ 𝑖 ) ∧ 𝑒 = ( 𝑥 ( +g ‘ 𝑅 ) 𝑚 ) ) ∧ 𝑜 ∈ 𝐵 ) ∧ 𝑚 = ( 𝑜 ( .r ‘ 𝑅 ) 𝑎 ) ) ∧ 𝑦 ∈ 𝑖 ) ∧ 𝑓 = ( 𝑦 ( +g ‘ 𝑅 ) 𝑛 ) ) ∧ 𝑞 ∈ 𝐵 ) ∧ 𝑛 = ( 𝑞 ( .r ‘ 𝑅 ) 𝑏 ) ) → 𝑖 ⊆ 𝐵 )
169 simp-8r ⊢ ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑃 ) ∧ ∀ 𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗 ) ∧ 𝑎 ∈ 𝐵 ) ∧ 𝑏 ∈ 𝐵 ) ∧ ( 𝑎 ( .r ‘ 𝑅 ) 𝑏 ) ∈ 𝑖 ) ∧ ¬ 𝑎 ∈ 𝑖 ) ∧ ¬ 𝑏 ∈ 𝑖 ) ∧ 𝑒 ∈ ( 𝑆 ∩ ( 𝑖 ( LSSum ‘ 𝑅 ) ( ( RSpan ‘ 𝑅 ) ‘ { 𝑎 } ) ) ) ) ∧ 𝑓 ∈ ( 𝑆 ∩ ( 𝑖 ( LSSum ‘ 𝑅 ) ( ( RSpan ‘ 𝑅 ) ‘ { 𝑏 } ) ) ) ) ∧ 𝑥 ∈ 𝑖 ) ∧ 𝑒 = ( 𝑥 ( +g ‘ 𝑅 ) 𝑚 ) ) ∧ 𝑜 ∈ 𝐵 ) ∧ 𝑚 = ( 𝑜 ( .r ‘ 𝑅 ) 𝑎 ) ) ∧ 𝑦 ∈ 𝑖 ) ∧ 𝑓 = ( 𝑦 ( +g ‘ 𝑅 ) 𝑛 ) ) ∧ 𝑞 ∈ 𝐵 ) ∧ 𝑛 = ( 𝑞 ( .r ‘ 𝑅 ) 𝑏 ) ) → 𝑥 ∈ 𝑖 )
170 168 169 sseldd ⊢ ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑃 ) ∧ ∀ 𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗 ) ∧ 𝑎 ∈ 𝐵 ) ∧ 𝑏 ∈ 𝐵 ) ∧ ( 𝑎 ( .r ‘ 𝑅 ) 𝑏 ) ∈ 𝑖 ) ∧ ¬ 𝑎 ∈ 𝑖 ) ∧ ¬ 𝑏 ∈ 𝑖 ) ∧ 𝑒 ∈ ( 𝑆 ∩ ( 𝑖 ( LSSum ‘ 𝑅 ) ( ( RSpan ‘ 𝑅 ) ‘ { 𝑎 } ) ) ) ) ∧ 𝑓 ∈ ( 𝑆 ∩ ( 𝑖 ( LSSum ‘ 𝑅 ) ( ( RSpan ‘ 𝑅 ) ‘ { 𝑏 } ) ) ) ) ∧ 𝑥 ∈ 𝑖 ) ∧ 𝑒 = ( 𝑥 ( +g ‘ 𝑅 ) 𝑚 ) ) ∧ 𝑜 ∈ 𝐵 ) ∧ 𝑚 = ( 𝑜 ( .r ‘ 𝑅 ) 𝑎 ) ) ∧ 𝑦 ∈ 𝑖 ) ∧ 𝑓 = ( 𝑦 ( +g ‘ 𝑅 ) 𝑛 ) ) ∧ 𝑞 ∈ 𝐵 ) ∧ 𝑛 = ( 𝑞 ( .r ‘ 𝑅 ) 𝑏 ) ) → 𝑥 ∈ 𝐵 )
171 simp-6r ⊢ ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑃 ) ∧ ∀ 𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗 ) ∧ 𝑎 ∈ 𝐵 ) ∧ 𝑏 ∈ 𝐵 ) ∧ ( 𝑎 ( .r ‘ 𝑅 ) 𝑏 ) ∈ 𝑖 ) ∧ ¬ 𝑎 ∈ 𝑖 ) ∧ ¬ 𝑏 ∈ 𝑖 ) ∧ 𝑒 ∈ ( 𝑆 ∩ ( 𝑖 ( LSSum ‘ 𝑅 ) ( ( RSpan ‘ 𝑅 ) ‘ { 𝑎 } ) ) ) ) ∧ 𝑓 ∈ ( 𝑆 ∩ ( 𝑖 ( LSSum ‘ 𝑅 ) ( ( RSpan ‘ 𝑅 ) ‘ { 𝑏 } ) ) ) ) ∧ 𝑥 ∈ 𝑖 ) ∧ 𝑒 = ( 𝑥 ( +g ‘ 𝑅 ) 𝑚 ) ) ∧ 𝑜 ∈ 𝐵 ) ∧ 𝑚 = ( 𝑜 ( .r ‘ 𝑅 ) 𝑎 ) ) ∧ 𝑦 ∈ 𝑖 ) ∧ 𝑓 = ( 𝑦 ( +g ‘ 𝑅 ) 𝑛 ) ) ∧ 𝑞 ∈ 𝐵 ) ∧ 𝑛 = ( 𝑞 ( .r ‘ 𝑅 ) 𝑏 ) ) → 𝑜 ∈ 𝐵 )
172 146 ad8antr ⊢ ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑃 ) ∧ ∀ 𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗 ) ∧ 𝑎 ∈ 𝐵 ) ∧ 𝑏 ∈ 𝐵 ) ∧ ( 𝑎 ( .r ‘ 𝑅 ) 𝑏 ) ∈ 𝑖 ) ∧ ¬ 𝑎 ∈ 𝑖 ) ∧ ¬ 𝑏 ∈ 𝑖 ) ∧ 𝑒 ∈ ( 𝑆 ∩ ( 𝑖 ( LSSum ‘ 𝑅 ) ( ( RSpan ‘ 𝑅 ) ‘ { 𝑎 } ) ) ) ) ∧ 𝑓 ∈ ( 𝑆 ∩ ( 𝑖 ( LSSum ‘ 𝑅 ) ( ( RSpan ‘ 𝑅 ) ‘ { 𝑏 } ) ) ) ) ∧ 𝑥 ∈ 𝑖 ) ∧ 𝑒 = ( 𝑥 ( +g ‘ 𝑅 ) 𝑚 ) ) ∧ 𝑜 ∈ 𝐵 ) ∧ 𝑚 = ( 𝑜 ( .r ‘ 𝑅 ) 𝑎 ) ) ∧ 𝑦 ∈ 𝑖 ) ∧ 𝑓 = ( 𝑦 ( +g ‘ 𝑅 ) 𝑛 ) ) ∧ 𝑞 ∈ 𝐵 ) ∧ 𝑛 = ( 𝑞 ( .r ‘ 𝑅 ) 𝑏 ) ) → 𝑎 ∈ 𝐵 )
173 1 148 165 171 172 ringcld ⊢ ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑃 ) ∧ ∀ 𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗 ) ∧ 𝑎 ∈ 𝐵 ) ∧ 𝑏 ∈ 𝐵 ) ∧ ( 𝑎 ( .r ‘ 𝑅 ) 𝑏 ) ∈ 𝑖 ) ∧ ¬ 𝑎 ∈ 𝑖 ) ∧ ¬ 𝑏 ∈ 𝑖 ) ∧ 𝑒 ∈ ( 𝑆 ∩ ( 𝑖 ( LSSum ‘ 𝑅 ) ( ( RSpan ‘ 𝑅 ) ‘ { 𝑎 } ) ) ) ) ∧ 𝑓 ∈ ( 𝑆 ∩ ( 𝑖 ( LSSum ‘ 𝑅 ) ( ( RSpan ‘ 𝑅 ) ‘ { 𝑏 } ) ) ) ) ∧ 𝑥 ∈ 𝑖 ) ∧ 𝑒 = ( 𝑥 ( +g ‘ 𝑅 ) 𝑚 ) ) ∧ 𝑜 ∈ 𝐵 ) ∧ 𝑚 = ( 𝑜 ( .r ‘ 𝑅 ) 𝑎 ) ) ∧ 𝑦 ∈ 𝑖 ) ∧ 𝑓 = ( 𝑦 ( +g ‘ 𝑅 ) 𝑛 ) ) ∧ 𝑞 ∈ 𝐵 ) ∧ 𝑛 = ( 𝑞 ( .r ‘ 𝑅 ) 𝑏 ) ) → ( 𝑜 ( .r ‘ 𝑅 ) 𝑎 ) ∈ 𝐵 )
174 simp-4r ⊢ ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑃 ) ∧ ∀ 𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗 ) ∧ 𝑎 ∈ 𝐵 ) ∧ 𝑏 ∈ 𝐵 ) ∧ ( 𝑎 ( .r ‘ 𝑅 ) 𝑏 ) ∈ 𝑖 ) ∧ ¬ 𝑎 ∈ 𝑖 ) ∧ ¬ 𝑏 ∈ 𝑖 ) ∧ 𝑒 ∈ ( 𝑆 ∩ ( 𝑖 ( LSSum ‘ 𝑅 ) ( ( RSpan ‘ 𝑅 ) ‘ { 𝑎 } ) ) ) ) ∧ 𝑓 ∈ ( 𝑆 ∩ ( 𝑖 ( LSSum ‘ 𝑅 ) ( ( RSpan ‘ 𝑅 ) ‘ { 𝑏 } ) ) ) ) ∧ 𝑥 ∈ 𝑖 ) ∧ 𝑒 = ( 𝑥 ( +g ‘ 𝑅 ) 𝑚 ) ) ∧ 𝑜 ∈ 𝐵 ) ∧ 𝑚 = ( 𝑜 ( .r ‘ 𝑅 ) 𝑎 ) ) ∧ 𝑦 ∈ 𝑖 ) ∧ 𝑓 = ( 𝑦 ( +g ‘ 𝑅 ) 𝑛 ) ) ∧ 𝑞 ∈ 𝐵 ) ∧ 𝑛 = ( 𝑞 ( .r ‘ 𝑅 ) 𝑏 ) ) → 𝑦 ∈ 𝑖 )
175 168 174 sseldd ⊢ ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑃 ) ∧ ∀ 𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗 ) ∧ 𝑎 ∈ 𝐵 ) ∧ 𝑏 ∈ 𝐵 ) ∧ ( 𝑎 ( .r ‘ 𝑅 ) 𝑏 ) ∈ 𝑖 ) ∧ ¬ 𝑎 ∈ 𝑖 ) ∧ ¬ 𝑏 ∈ 𝑖 ) ∧ 𝑒 ∈ ( 𝑆 ∩ ( 𝑖 ( LSSum ‘ 𝑅 ) ( ( RSpan ‘ 𝑅 ) ‘ { 𝑎 } ) ) ) ) ∧ 𝑓 ∈ ( 𝑆 ∩ ( 𝑖 ( LSSum ‘ 𝑅 ) ( ( RSpan ‘ 𝑅 ) ‘ { 𝑏 } ) ) ) ) ∧ 𝑥 ∈ 𝑖 ) ∧ 𝑒 = ( 𝑥 ( +g ‘ 𝑅 ) 𝑚 ) ) ∧ 𝑜 ∈ 𝐵 ) ∧ 𝑚 = ( 𝑜 ( .r ‘ 𝑅 ) 𝑎 ) ) ∧ 𝑦 ∈ 𝑖 ) ∧ 𝑓 = ( 𝑦 ( +g ‘ 𝑅 ) 𝑛 ) ) ∧ 𝑞 ∈ 𝐵 ) ∧ 𝑛 = ( 𝑞 ( .r ‘ 𝑅 ) 𝑏 ) ) → 𝑦 ∈ 𝐵 )
176 simplr ⊢ ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑃 ) ∧ ∀ 𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗 ) ∧ 𝑎 ∈ 𝐵 ) ∧ 𝑏 ∈ 𝐵 ) ∧ ( 𝑎 ( .r ‘ 𝑅 ) 𝑏 ) ∈ 𝑖 ) ∧ ¬ 𝑎 ∈ 𝑖 ) ∧ ¬ 𝑏 ∈ 𝑖 ) ∧ 𝑒 ∈ ( 𝑆 ∩ ( 𝑖 ( LSSum ‘ 𝑅 ) ( ( RSpan ‘ 𝑅 ) ‘ { 𝑎 } ) ) ) ) ∧ 𝑓 ∈ ( 𝑆 ∩ ( 𝑖 ( LSSum ‘ 𝑅 ) ( ( RSpan ‘ 𝑅 ) ‘ { 𝑏 } ) ) ) ) ∧ 𝑥 ∈ 𝑖 ) ∧ 𝑒 = ( 𝑥 ( +g ‘ 𝑅 ) 𝑚 ) ) ∧ 𝑜 ∈ 𝐵 ) ∧ 𝑚 = ( 𝑜 ( .r ‘ 𝑅 ) 𝑎 ) ) ∧ 𝑦 ∈ 𝑖 ) ∧ 𝑓 = ( 𝑦 ( +g ‘ 𝑅 ) 𝑛 ) ) ∧ 𝑞 ∈ 𝐵 ) ∧ 𝑛 = ( 𝑞 ( .r ‘ 𝑅 ) 𝑏 ) ) → 𝑞 ∈ 𝐵 )
177 153 ad2antrr ⊢ ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑃 ) ∧ ∀ 𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗 ) ∧ 𝑎 ∈ 𝐵 ) ∧ 𝑏 ∈ 𝐵 ) ∧ ( 𝑎 ( .r ‘ 𝑅 ) 𝑏 ) ∈ 𝑖 ) ∧ ¬ 𝑎 ∈ 𝑖 ) ∧ ¬ 𝑏 ∈ 𝑖 ) ∧ 𝑒 ∈ ( 𝑆 ∩ ( 𝑖 ( LSSum ‘ 𝑅 ) ( ( RSpan ‘ 𝑅 ) ‘ { 𝑎 } ) ) ) ) ∧ 𝑓 ∈ ( 𝑆 ∩ ( 𝑖 ( LSSum ‘ 𝑅 ) ( ( RSpan ‘ 𝑅 ) ‘ { 𝑏 } ) ) ) ) ∧ 𝑥 ∈ 𝑖 ) ∧ 𝑒 = ( 𝑥 ( +g ‘ 𝑅 ) 𝑚 ) ) ∧ 𝑜 ∈ 𝐵 ) ∧ 𝑚 = ( 𝑜 ( .r ‘ 𝑅 ) 𝑎 ) ) ∧ 𝑦 ∈ 𝑖 ) ∧ 𝑓 = ( 𝑦 ( +g ‘ 𝑅 ) 𝑛 ) ) ∧ 𝑞 ∈ 𝐵 ) ∧ 𝑛 = ( 𝑞 ( .r ‘ 𝑅 ) 𝑏 ) ) → 𝑏 ∈ 𝐵 )
178 1 148 165 176 177 ringcld ⊢ ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑃 ) ∧ ∀ 𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗 ) ∧ 𝑎 ∈ 𝐵 ) ∧ 𝑏 ∈ 𝐵 ) ∧ ( 𝑎 ( .r ‘ 𝑅 ) 𝑏 ) ∈ 𝑖 ) ∧ ¬ 𝑎 ∈ 𝑖 ) ∧ ¬ 𝑏 ∈ 𝑖 ) ∧ 𝑒 ∈ ( 𝑆 ∩ ( 𝑖 ( LSSum ‘ 𝑅 ) ( ( RSpan ‘ 𝑅 ) ‘ { 𝑎 } ) ) ) ) ∧ 𝑓 ∈ ( 𝑆 ∩ ( 𝑖 ( LSSum ‘ 𝑅 ) ( ( RSpan ‘ 𝑅 ) ‘ { 𝑏 } ) ) ) ) ∧ 𝑥 ∈ 𝑖 ) ∧ 𝑒 = ( 𝑥 ( +g ‘ 𝑅 ) 𝑚 ) ) ∧ 𝑜 ∈ 𝐵 ) ∧ 𝑚 = ( 𝑜 ( .r ‘ 𝑅 ) 𝑎 ) ) ∧ 𝑦 ∈ 𝑖 ) ∧ 𝑓 = ( 𝑦 ( +g ‘ 𝑅 ) 𝑛 ) ) ∧ 𝑞 ∈ 𝐵 ) ∧ 𝑛 = ( 𝑞 ( .r ‘ 𝑅 ) 𝑏 ) ) → ( 𝑞 ( .r ‘ 𝑅 ) 𝑏 ) ∈ 𝐵 )
179 1 164 148 165 170 173 175 178 ringdi22 ⊢ ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑃 ) ∧ ∀ 𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗 ) ∧ 𝑎 ∈ 𝐵 ) ∧ 𝑏 ∈ 𝐵 ) ∧ ( 𝑎 ( .r ‘ 𝑅 ) 𝑏 ) ∈ 𝑖 ) ∧ ¬ 𝑎 ∈ 𝑖 ) ∧ ¬ 𝑏 ∈ 𝑖 ) ∧ 𝑒 ∈ ( 𝑆 ∩ ( 𝑖 ( LSSum ‘ 𝑅 ) ( ( RSpan ‘ 𝑅 ) ‘ { 𝑎 } ) ) ) ) ∧ 𝑓 ∈ ( 𝑆 ∩ ( 𝑖 ( LSSum ‘ 𝑅 ) ( ( RSpan ‘ 𝑅 ) ‘ { 𝑏 } ) ) ) ) ∧ 𝑥 ∈ 𝑖 ) ∧ 𝑒 = ( 𝑥 ( +g ‘ 𝑅 ) 𝑚 ) ) ∧ 𝑜 ∈ 𝐵 ) ∧ 𝑚 = ( 𝑜 ( .r ‘ 𝑅 ) 𝑎 ) ) ∧ 𝑦 ∈ 𝑖 ) ∧ 𝑓 = ( 𝑦 ( +g ‘ 𝑅 ) 𝑛 ) ) ∧ 𝑞 ∈ 𝐵 ) ∧ 𝑛 = ( 𝑞 ( .r ‘ 𝑅 ) 𝑏 ) ) → ( ( 𝑥 ( +g ‘ 𝑅 ) ( 𝑜 ( .r ‘ 𝑅 ) 𝑎 ) ) ( .r ‘ 𝑅 ) ( 𝑦 ( +g ‘ 𝑅 ) ( 𝑞 ( .r ‘ 𝑅 ) 𝑏 ) ) ) = ( ( ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) ( +g ‘ 𝑅 ) ( ( 𝑜 ( .r ‘ 𝑅 ) 𝑎 ) ( .r ‘ 𝑅 ) 𝑦 ) ) ( +g ‘ 𝑅 ) ( ( 𝑥 ( .r ‘ 𝑅 ) ( 𝑞 ( .r ‘ 𝑅 ) 𝑏 ) ) ( +g ‘ 𝑅 ) ( ( 𝑜 ( .r ‘ 𝑅 ) 𝑎 ) ( .r ‘ 𝑅 ) ( 𝑞 ( .r ‘ 𝑅 ) 𝑏 ) ) ) ) )
180 158 163 179 3eqtrd ⊢ ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑃 ) ∧ ∀ 𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗 ) ∧ 𝑎 ∈ 𝐵 ) ∧ 𝑏 ∈ 𝐵 ) ∧ ( 𝑎 ( .r ‘ 𝑅 ) 𝑏 ) ∈ 𝑖 ) ∧ ¬ 𝑎 ∈ 𝑖 ) ∧ ¬ 𝑏 ∈ 𝑖 ) ∧ 𝑒 ∈ ( 𝑆 ∩ ( 𝑖 ( LSSum ‘ 𝑅 ) ( ( RSpan ‘ 𝑅 ) ‘ { 𝑎 } ) ) ) ) ∧ 𝑓 ∈ ( 𝑆 ∩ ( 𝑖 ( LSSum ‘ 𝑅 ) ( ( RSpan ‘ 𝑅 ) ‘ { 𝑏 } ) ) ) ) ∧ 𝑥 ∈ 𝑖 ) ∧ 𝑒 = ( 𝑥 ( +g ‘ 𝑅 ) 𝑚 ) ) ∧ 𝑜 ∈ 𝐵 ) ∧ 𝑚 = ( 𝑜 ( .r ‘ 𝑅 ) 𝑎 ) ) ∧ 𝑦 ∈ 𝑖 ) ∧ 𝑓 = ( 𝑦 ( +g ‘ 𝑅 ) 𝑛 ) ) ∧ 𝑞 ∈ 𝐵 ) ∧ 𝑛 = ( 𝑞 ( .r ‘ 𝑅 ) 𝑏 ) ) → ( 𝑒 ( .r ‘ 𝑅 ) 𝑓 ) = ( ( ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) ( +g ‘ 𝑅 ) ( ( 𝑜 ( .r ‘ 𝑅 ) 𝑎 ) ( .r ‘ 𝑅 ) 𝑦 ) ) ( +g ‘ 𝑅 ) ( ( 𝑥 ( .r ‘ 𝑅 ) ( 𝑞 ( .r ‘ 𝑅 ) 𝑏 ) ) ( +g ‘ 𝑅 ) ( ( 𝑜 ( .r ‘ 𝑅 ) 𝑎 ) ( .r ‘ 𝑅 ) ( 𝑞 ( .r ‘ 𝑅 ) 𝑏 ) ) ) ) )
181 70 ad2antrr ⊢ ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑃 ) ∧ ∀ 𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗 ) ∧ 𝑎 ∈ 𝐵 ) ∧ 𝑏 ∈ 𝐵 ) ∧ ( 𝑎 ( .r ‘ 𝑅 ) 𝑏 ) ∈ 𝑖 ) ∧ ¬ 𝑎 ∈ 𝑖 ) ∧ ¬ 𝑏 ∈ 𝑖 ) ∧ 𝑒 ∈ ( 𝑆 ∩ ( 𝑖 ( LSSum ‘ 𝑅 ) ( ( RSpan ‘ 𝑅 ) ‘ { 𝑎 } ) ) ) ) ∧ 𝑓 ∈ ( 𝑆 ∩ ( 𝑖 ( LSSum ‘ 𝑅 ) ( ( RSpan ‘ 𝑅 ) ‘ { 𝑏 } ) ) ) ) → 𝑖 ∈ ( LIdeal ‘ 𝑅 ) )
182 181 ad8antr ⊢ ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑃 ) ∧ ∀ 𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗 ) ∧ 𝑎 ∈ 𝐵 ) ∧ 𝑏 ∈ 𝐵 ) ∧ ( 𝑎 ( .r ‘ 𝑅 ) 𝑏 ) ∈ 𝑖 ) ∧ ¬ 𝑎 ∈ 𝑖 ) ∧ ¬ 𝑏 ∈ 𝑖 ) ∧ 𝑒 ∈ ( 𝑆 ∩ ( 𝑖 ( LSSum ‘ 𝑅 ) ( ( RSpan ‘ 𝑅 ) ‘ { 𝑎 } ) ) ) ) ∧ 𝑓 ∈ ( 𝑆 ∩ ( 𝑖 ( LSSum ‘ 𝑅 ) ( ( RSpan ‘ 𝑅 ) ‘ { 𝑏 } ) ) ) ) ∧ 𝑥 ∈ 𝑖 ) ∧ 𝑒 = ( 𝑥 ( +g ‘ 𝑅 ) 𝑚 ) ) ∧ 𝑜 ∈ 𝐵 ) ∧ 𝑚 = ( 𝑜 ( .r ‘ 𝑅 ) 𝑎 ) ) ∧ 𝑦 ∈ 𝑖 ) ∧ 𝑓 = ( 𝑦 ( +g ‘ 𝑅 ) 𝑛 ) ) ∧ 𝑞 ∈ 𝐵 ) ∧ 𝑛 = ( 𝑞 ( .r ‘ 𝑅 ) 𝑏 ) ) → 𝑖 ∈ ( LIdeal ‘ 𝑅 ) )
183 165 182 49 syl2anc ⊢ ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑃 ) ∧ ∀ 𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗 ) ∧ 𝑎 ∈ 𝐵 ) ∧ 𝑏 ∈ 𝐵 ) ∧ ( 𝑎 ( .r ‘ 𝑅 ) 𝑏 ) ∈ 𝑖 ) ∧ ¬ 𝑎 ∈ 𝑖 ) ∧ ¬ 𝑏 ∈ 𝑖 ) ∧ 𝑒 ∈ ( 𝑆 ∩ ( 𝑖 ( LSSum ‘ 𝑅 ) ( ( RSpan ‘ 𝑅 ) ‘ { 𝑎 } ) ) ) ) ∧ 𝑓 ∈ ( 𝑆 ∩ ( 𝑖 ( LSSum ‘ 𝑅 ) ( ( RSpan ‘ 𝑅 ) ‘ { 𝑏 } ) ) ) ) ∧ 𝑥 ∈ 𝑖 ) ∧ 𝑒 = ( 𝑥 ( +g ‘ 𝑅 ) 𝑚 ) ) ∧ 𝑜 ∈ 𝐵 ) ∧ 𝑚 = ( 𝑜 ( .r ‘ 𝑅 ) 𝑎 ) ) ∧ 𝑦 ∈ 𝑖 ) ∧ 𝑓 = ( 𝑦 ( +g ‘ 𝑅 ) 𝑛 ) ) ∧ 𝑞 ∈ 𝐵 ) ∧ 𝑛 = ( 𝑞 ( .r ‘ 𝑅 ) 𝑏 ) ) → 𝑖 ∈ ( SubGrp ‘ 𝑅 ) )
184 18 1 148 165 182 170 174 lidlmcld ⊢ ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑃 ) ∧ ∀ 𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗 ) ∧ 𝑎 ∈ 𝐵 ) ∧ 𝑏 ∈ 𝐵 ) ∧ ( 𝑎 ( .r ‘ 𝑅 ) 𝑏 ) ∈ 𝑖 ) ∧ ¬ 𝑎 ∈ 𝑖 ) ∧ ¬ 𝑏 ∈ 𝑖 ) ∧ 𝑒 ∈ ( 𝑆 ∩ ( 𝑖 ( LSSum ‘ 𝑅 ) ( ( RSpan ‘ 𝑅 ) ‘ { 𝑎 } ) ) ) ) ∧ 𝑓 ∈ ( 𝑆 ∩ ( 𝑖 ( LSSum ‘ 𝑅 ) ( ( RSpan ‘ 𝑅 ) ‘ { 𝑏 } ) ) ) ) ∧ 𝑥 ∈ 𝑖 ) ∧ 𝑒 = ( 𝑥 ( +g ‘ 𝑅 ) 𝑚 ) ) ∧ 𝑜 ∈ 𝐵 ) ∧ 𝑚 = ( 𝑜 ( .r ‘ 𝑅 ) 𝑎 ) ) ∧ 𝑦 ∈ 𝑖 ) ∧ 𝑓 = ( 𝑦 ( +g ‘ 𝑅 ) 𝑛 ) ) ∧ 𝑞 ∈ 𝐵 ) ∧ 𝑛 = ( 𝑞 ( .r ‘ 𝑅 ) 𝑏 ) ) → ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) ∈ 𝑖 )
185 18 1 148 165 182 173 174 lidlmcld ⊢ ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑃 ) ∧ ∀ 𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗 ) ∧ 𝑎 ∈ 𝐵 ) ∧ 𝑏 ∈ 𝐵 ) ∧ ( 𝑎 ( .r ‘ 𝑅 ) 𝑏 ) ∈ 𝑖 ) ∧ ¬ 𝑎 ∈ 𝑖 ) ∧ ¬ 𝑏 ∈ 𝑖 ) ∧ 𝑒 ∈ ( 𝑆 ∩ ( 𝑖 ( LSSum ‘ 𝑅 ) ( ( RSpan ‘ 𝑅 ) ‘ { 𝑎 } ) ) ) ) ∧ 𝑓 ∈ ( 𝑆 ∩ ( 𝑖 ( LSSum ‘ 𝑅 ) ( ( RSpan ‘ 𝑅 ) ‘ { 𝑏 } ) ) ) ) ∧ 𝑥 ∈ 𝑖 ) ∧ 𝑒 = ( 𝑥 ( +g ‘ 𝑅 ) 𝑚 ) ) ∧ 𝑜 ∈ 𝐵 ) ∧ 𝑚 = ( 𝑜 ( .r ‘ 𝑅 ) 𝑎 ) ) ∧ 𝑦 ∈ 𝑖 ) ∧ 𝑓 = ( 𝑦 ( +g ‘ 𝑅 ) 𝑛 ) ) ∧ 𝑞 ∈ 𝐵 ) ∧ 𝑛 = ( 𝑞 ( .r ‘ 𝑅 ) 𝑏 ) ) → ( ( 𝑜 ( .r ‘ 𝑅 ) 𝑎 ) ( .r ‘ 𝑅 ) 𝑦 ) ∈ 𝑖 )
186 164 183 184 185 subgcld ⊢ ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑃 ) ∧ ∀ 𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗 ) ∧ 𝑎 ∈ 𝐵 ) ∧ 𝑏 ∈ 𝐵 ) ∧ ( 𝑎 ( .r ‘ 𝑅 ) 𝑏 ) ∈ 𝑖 ) ∧ ¬ 𝑎 ∈ 𝑖 ) ∧ ¬ 𝑏 ∈ 𝑖 ) ∧ 𝑒 ∈ ( 𝑆 ∩ ( 𝑖 ( LSSum ‘ 𝑅 ) ( ( RSpan ‘ 𝑅 ) ‘ { 𝑎 } ) ) ) ) ∧ 𝑓 ∈ ( 𝑆 ∩ ( 𝑖 ( LSSum ‘ 𝑅 ) ( ( RSpan ‘ 𝑅 ) ‘ { 𝑏 } ) ) ) ) ∧ 𝑥 ∈ 𝑖 ) ∧ 𝑒 = ( 𝑥 ( +g ‘ 𝑅 ) 𝑚 ) ) ∧ 𝑜 ∈ 𝐵 ) ∧ 𝑚 = ( 𝑜 ( .r ‘ 𝑅 ) 𝑎 ) ) ∧ 𝑦 ∈ 𝑖 ) ∧ 𝑓 = ( 𝑦 ( +g ‘ 𝑅 ) 𝑛 ) ) ∧ 𝑞 ∈ 𝐵 ) ∧ 𝑛 = ( 𝑞 ( .r ‘ 𝑅 ) 𝑏 ) ) → ( ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) ( +g ‘ 𝑅 ) ( ( 𝑜 ( .r ‘ 𝑅 ) 𝑎 ) ( .r ‘ 𝑅 ) 𝑦 ) ) ∈ 𝑖 )
187 8 ad7antr ⊢ ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑃 ) ∧ ∀ 𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗 ) ∧ 𝑎 ∈ 𝐵 ) ∧ 𝑏 ∈ 𝐵 ) ∧ ( 𝑎 ( .r ‘ 𝑅 ) 𝑏 ) ∈ 𝑖 ) ∧ ¬ 𝑎 ∈ 𝑖 ) ∧ ¬ 𝑏 ∈ 𝑖 ) ∧ 𝑒 ∈ ( 𝑆 ∩ ( 𝑖 ( LSSum ‘ 𝑅 ) ( ( RSpan ‘ 𝑅 ) ‘ { 𝑎 } ) ) ) ) ∧ 𝑓 ∈ ( 𝑆 ∩ ( 𝑖 ( LSSum ‘ 𝑅 ) ( ( RSpan ‘ 𝑅 ) ‘ { 𝑏 } ) ) ) ) → 𝑅 ∈ CRing )
188 187 ad4antr ⊢ ( ( ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑃 ) ∧ ∀ 𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗 ) ∧ 𝑎 ∈ 𝐵 ) ∧ 𝑏 ∈ 𝐵 ) ∧ ( 𝑎 ( .r ‘ 𝑅 ) 𝑏 ) ∈ 𝑖 ) ∧ ¬ 𝑎 ∈ 𝑖 ) ∧ ¬ 𝑏 ∈ 𝑖 ) ∧ 𝑒 ∈ ( 𝑆 ∩ ( 𝑖 ( LSSum ‘ 𝑅 ) ( ( RSpan ‘ 𝑅 ) ‘ { 𝑎 } ) ) ) ) ∧ 𝑓 ∈ ( 𝑆 ∩ ( 𝑖 ( LSSum ‘ 𝑅 ) ( ( RSpan ‘ 𝑅 ) ‘ { 𝑏 } ) ) ) ) ∧ 𝑥 ∈ 𝑖 ) ∧ 𝑒 = ( 𝑥 ( +g ‘ 𝑅 ) 𝑚 ) ) ∧ 𝑜 ∈ 𝐵 ) ∧ 𝑚 = ( 𝑜 ( .r ‘ 𝑅 ) 𝑎 ) ) → 𝑅 ∈ CRing )
189 188 ad4antr ⊢ ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑃 ) ∧ ∀ 𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗 ) ∧ 𝑎 ∈ 𝐵 ) ∧ 𝑏 ∈ 𝐵 ) ∧ ( 𝑎 ( .r ‘ 𝑅 ) 𝑏 ) ∈ 𝑖 ) ∧ ¬ 𝑎 ∈ 𝑖 ) ∧ ¬ 𝑏 ∈ 𝑖 ) ∧ 𝑒 ∈ ( 𝑆 ∩ ( 𝑖 ( LSSum ‘ 𝑅 ) ( ( RSpan ‘ 𝑅 ) ‘ { 𝑎 } ) ) ) ) ∧ 𝑓 ∈ ( 𝑆 ∩ ( 𝑖 ( LSSum ‘ 𝑅 ) ( ( RSpan ‘ 𝑅 ) ‘ { 𝑏 } ) ) ) ) ∧ 𝑥 ∈ 𝑖 ) ∧ 𝑒 = ( 𝑥 ( +g ‘ 𝑅 ) 𝑚 ) ) ∧ 𝑜 ∈ 𝐵 ) ∧ 𝑚 = ( 𝑜 ( .r ‘ 𝑅 ) 𝑎 ) ) ∧ 𝑦 ∈ 𝑖 ) ∧ 𝑓 = ( 𝑦 ( +g ‘ 𝑅 ) 𝑛 ) ) ∧ 𝑞 ∈ 𝐵 ) ∧ 𝑛 = ( 𝑞 ( .r ‘ 𝑅 ) 𝑏 ) ) → 𝑅 ∈ CRing )
190 1 148 189 170 178 crngcomd ⊢ ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑃 ) ∧ ∀ 𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗 ) ∧ 𝑎 ∈ 𝐵 ) ∧ 𝑏 ∈ 𝐵 ) ∧ ( 𝑎 ( .r ‘ 𝑅 ) 𝑏 ) ∈ 𝑖 ) ∧ ¬ 𝑎 ∈ 𝑖 ) ∧ ¬ 𝑏 ∈ 𝑖 ) ∧ 𝑒 ∈ ( 𝑆 ∩ ( 𝑖 ( LSSum ‘ 𝑅 ) ( ( RSpan ‘ 𝑅 ) ‘ { 𝑎 } ) ) ) ) ∧ 𝑓 ∈ ( 𝑆 ∩ ( 𝑖 ( LSSum ‘ 𝑅 ) ( ( RSpan ‘ 𝑅 ) ‘ { 𝑏 } ) ) ) ) ∧ 𝑥 ∈ 𝑖 ) ∧ 𝑒 = ( 𝑥 ( +g ‘ 𝑅 ) 𝑚 ) ) ∧ 𝑜 ∈ 𝐵 ) ∧ 𝑚 = ( 𝑜 ( .r ‘ 𝑅 ) 𝑎 ) ) ∧ 𝑦 ∈ 𝑖 ) ∧ 𝑓 = ( 𝑦 ( +g ‘ 𝑅 ) 𝑛 ) ) ∧ 𝑞 ∈ 𝐵 ) ∧ 𝑛 = ( 𝑞 ( .r ‘ 𝑅 ) 𝑏 ) ) → ( 𝑥 ( .r ‘ 𝑅 ) ( 𝑞 ( .r ‘ 𝑅 ) 𝑏 ) ) = ( ( 𝑞 ( .r ‘ 𝑅 ) 𝑏 ) ( .r ‘ 𝑅 ) 𝑥 ) )
191 18 1 148 165 182 178 169 lidlmcld ⊢ ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑃 ) ∧ ∀ 𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗 ) ∧ 𝑎 ∈ 𝐵 ) ∧ 𝑏 ∈ 𝐵 ) ∧ ( 𝑎 ( .r ‘ 𝑅 ) 𝑏 ) ∈ 𝑖 ) ∧ ¬ 𝑎 ∈ 𝑖 ) ∧ ¬ 𝑏 ∈ 𝑖 ) ∧ 𝑒 ∈ ( 𝑆 ∩ ( 𝑖 ( LSSum ‘ 𝑅 ) ( ( RSpan ‘ 𝑅 ) ‘ { 𝑎 } ) ) ) ) ∧ 𝑓 ∈ ( 𝑆 ∩ ( 𝑖 ( LSSum ‘ 𝑅 ) ( ( RSpan ‘ 𝑅 ) ‘ { 𝑏 } ) ) ) ) ∧ 𝑥 ∈ 𝑖 ) ∧ 𝑒 = ( 𝑥 ( +g ‘ 𝑅 ) 𝑚 ) ) ∧ 𝑜 ∈ 𝐵 ) ∧ 𝑚 = ( 𝑜 ( .r ‘ 𝑅 ) 𝑎 ) ) ∧ 𝑦 ∈ 𝑖 ) ∧ 𝑓 = ( 𝑦 ( +g ‘ 𝑅 ) 𝑛 ) ) ∧ 𝑞 ∈ 𝐵 ) ∧ 𝑛 = ( 𝑞 ( .r ‘ 𝑅 ) 𝑏 ) ) → ( ( 𝑞 ( .r ‘ 𝑅 ) 𝑏 ) ( .r ‘ 𝑅 ) 𝑥 ) ∈ 𝑖 )
192 190 191 eqeltrd ⊢ ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑃 ) ∧ ∀ 𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗 ) ∧ 𝑎 ∈ 𝐵 ) ∧ 𝑏 ∈ 𝐵 ) ∧ ( 𝑎 ( .r ‘ 𝑅 ) 𝑏 ) ∈ 𝑖 ) ∧ ¬ 𝑎 ∈ 𝑖 ) ∧ ¬ 𝑏 ∈ 𝑖 ) ∧ 𝑒 ∈ ( 𝑆 ∩ ( 𝑖 ( LSSum ‘ 𝑅 ) ( ( RSpan ‘ 𝑅 ) ‘ { 𝑎 } ) ) ) ) ∧ 𝑓 ∈ ( 𝑆 ∩ ( 𝑖 ( LSSum ‘ 𝑅 ) ( ( RSpan ‘ 𝑅 ) ‘ { 𝑏 } ) ) ) ) ∧ 𝑥 ∈ 𝑖 ) ∧ 𝑒 = ( 𝑥 ( +g ‘ 𝑅 ) 𝑚 ) ) ∧ 𝑜 ∈ 𝐵 ) ∧ 𝑚 = ( 𝑜 ( .r ‘ 𝑅 ) 𝑎 ) ) ∧ 𝑦 ∈ 𝑖 ) ∧ 𝑓 = ( 𝑦 ( +g ‘ 𝑅 ) 𝑛 ) ) ∧ 𝑞 ∈ 𝐵 ) ∧ 𝑛 = ( 𝑞 ( .r ‘ 𝑅 ) 𝑏 ) ) → ( 𝑥 ( .r ‘ 𝑅 ) ( 𝑞 ( .r ‘ 𝑅 ) 𝑏 ) ) ∈ 𝑖 )
193 1 148 cringm4 ⊢ ( ( 𝑅 ∈ CRing ∧ ( 𝑜 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵 ) ∧ ( 𝑞 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ) ) → ( ( 𝑜 ( .r ‘ 𝑅 ) 𝑎 ) ( .r ‘ 𝑅 ) ( 𝑞 ( .r ‘ 𝑅 ) 𝑏 ) ) = ( ( 𝑜 ( .r ‘ 𝑅 ) 𝑞 ) ( .r ‘ 𝑅 ) ( 𝑎 ( .r ‘ 𝑅 ) 𝑏 ) ) )
194 189 171 172 176 177 193 syl122anc ⊢ ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑃 ) ∧ ∀ 𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗 ) ∧ 𝑎 ∈ 𝐵 ) ∧ 𝑏 ∈ 𝐵 ) ∧ ( 𝑎 ( .r ‘ 𝑅 ) 𝑏 ) ∈ 𝑖 ) ∧ ¬ 𝑎 ∈ 𝑖 ) ∧ ¬ 𝑏 ∈ 𝑖 ) ∧ 𝑒 ∈ ( 𝑆 ∩ ( 𝑖 ( LSSum ‘ 𝑅 ) ( ( RSpan ‘ 𝑅 ) ‘ { 𝑎 } ) ) ) ) ∧ 𝑓 ∈ ( 𝑆 ∩ ( 𝑖 ( LSSum ‘ 𝑅 ) ( ( RSpan ‘ 𝑅 ) ‘ { 𝑏 } ) ) ) ) ∧ 𝑥 ∈ 𝑖 ) ∧ 𝑒 = ( 𝑥 ( +g ‘ 𝑅 ) 𝑚 ) ) ∧ 𝑜 ∈ 𝐵 ) ∧ 𝑚 = ( 𝑜 ( .r ‘ 𝑅 ) 𝑎 ) ) ∧ 𝑦 ∈ 𝑖 ) ∧ 𝑓 = ( 𝑦 ( +g ‘ 𝑅 ) 𝑛 ) ) ∧ 𝑞 ∈ 𝐵 ) ∧ 𝑛 = ( 𝑞 ( .r ‘ 𝑅 ) 𝑏 ) ) → ( ( 𝑜 ( .r ‘ 𝑅 ) 𝑎 ) ( .r ‘ 𝑅 ) ( 𝑞 ( .r ‘ 𝑅 ) 𝑏 ) ) = ( ( 𝑜 ( .r ‘ 𝑅 ) 𝑞 ) ( .r ‘ 𝑅 ) ( 𝑎 ( .r ‘ 𝑅 ) 𝑏 ) ) )
195 1 148 165 171 176 ringcld ⊢ ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑃 ) ∧ ∀ 𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗 ) ∧ 𝑎 ∈ 𝐵 ) ∧ 𝑏 ∈ 𝐵 ) ∧ ( 𝑎 ( .r ‘ 𝑅 ) 𝑏 ) ∈ 𝑖 ) ∧ ¬ 𝑎 ∈ 𝑖 ) ∧ ¬ 𝑏 ∈ 𝑖 ) ∧ 𝑒 ∈ ( 𝑆 ∩ ( 𝑖 ( LSSum ‘ 𝑅 ) ( ( RSpan ‘ 𝑅 ) ‘ { 𝑎 } ) ) ) ) ∧ 𝑓 ∈ ( 𝑆 ∩ ( 𝑖 ( LSSum ‘ 𝑅 ) ( ( RSpan ‘ 𝑅 ) ‘ { 𝑏 } ) ) ) ) ∧ 𝑥 ∈ 𝑖 ) ∧ 𝑒 = ( 𝑥 ( +g ‘ 𝑅 ) 𝑚 ) ) ∧ 𝑜 ∈ 𝐵 ) ∧ 𝑚 = ( 𝑜 ( .r ‘ 𝑅 ) 𝑎 ) ) ∧ 𝑦 ∈ 𝑖 ) ∧ 𝑓 = ( 𝑦 ( +g ‘ 𝑅 ) 𝑛 ) ) ∧ 𝑞 ∈ 𝐵 ) ∧ 𝑛 = ( 𝑞 ( .r ‘ 𝑅 ) 𝑏 ) ) → ( 𝑜 ( .r ‘ 𝑅 ) 𝑞 ) ∈ 𝐵 )
196 simp-5r ⊢ ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑃 ) ∧ ∀ 𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗 ) ∧ 𝑎 ∈ 𝐵 ) ∧ 𝑏 ∈ 𝐵 ) ∧ ( 𝑎 ( .r ‘ 𝑅 ) 𝑏 ) ∈ 𝑖 ) ∧ ¬ 𝑎 ∈ 𝑖 ) ∧ ¬ 𝑏 ∈ 𝑖 ) ∧ 𝑒 ∈ ( 𝑆 ∩ ( 𝑖 ( LSSum ‘ 𝑅 ) ( ( RSpan ‘ 𝑅 ) ‘ { 𝑎 } ) ) ) ) ∧ 𝑓 ∈ ( 𝑆 ∩ ( 𝑖 ( LSSum ‘ 𝑅 ) ( ( RSpan ‘ 𝑅 ) ‘ { 𝑏 } ) ) ) ) → ( 𝑎 ( .r ‘ 𝑅 ) 𝑏 ) ∈ 𝑖 )
197 196 ad8antr ⊢ ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑃 ) ∧ ∀ 𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗 ) ∧ 𝑎 ∈ 𝐵 ) ∧ 𝑏 ∈ 𝐵 ) ∧ ( 𝑎 ( .r ‘ 𝑅 ) 𝑏 ) ∈ 𝑖 ) ∧ ¬ 𝑎 ∈ 𝑖 ) ∧ ¬ 𝑏 ∈ 𝑖 ) ∧ 𝑒 ∈ ( 𝑆 ∩ ( 𝑖 ( LSSum ‘ 𝑅 ) ( ( RSpan ‘ 𝑅 ) ‘ { 𝑎 } ) ) ) ) ∧ 𝑓 ∈ ( 𝑆 ∩ ( 𝑖 ( LSSum ‘ 𝑅 ) ( ( RSpan ‘ 𝑅 ) ‘ { 𝑏 } ) ) ) ) ∧ 𝑥 ∈ 𝑖 ) ∧ 𝑒 = ( 𝑥 ( +g ‘ 𝑅 ) 𝑚 ) ) ∧ 𝑜 ∈ 𝐵 ) ∧ 𝑚 = ( 𝑜 ( .r ‘ 𝑅 ) 𝑎 ) ) ∧ 𝑦 ∈ 𝑖 ) ∧ 𝑓 = ( 𝑦 ( +g ‘ 𝑅 ) 𝑛 ) ) ∧ 𝑞 ∈ 𝐵 ) ∧ 𝑛 = ( 𝑞 ( .r ‘ 𝑅 ) 𝑏 ) ) → ( 𝑎 ( .r ‘ 𝑅 ) 𝑏 ) ∈ 𝑖 )
198 18 1 148 165 182 195 197 lidlmcld ⊢ ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑃 ) ∧ ∀ 𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗 ) ∧ 𝑎 ∈ 𝐵 ) ∧ 𝑏 ∈ 𝐵 ) ∧ ( 𝑎 ( .r ‘ 𝑅 ) 𝑏 ) ∈ 𝑖 ) ∧ ¬ 𝑎 ∈ 𝑖 ) ∧ ¬ 𝑏 ∈ 𝑖 ) ∧ 𝑒 ∈ ( 𝑆 ∩ ( 𝑖 ( LSSum ‘ 𝑅 ) ( ( RSpan ‘ 𝑅 ) ‘ { 𝑎 } ) ) ) ) ∧ 𝑓 ∈ ( 𝑆 ∩ ( 𝑖 ( LSSum ‘ 𝑅 ) ( ( RSpan ‘ 𝑅 ) ‘ { 𝑏 } ) ) ) ) ∧ 𝑥 ∈ 𝑖 ) ∧ 𝑒 = ( 𝑥 ( +g ‘ 𝑅 ) 𝑚 ) ) ∧ 𝑜 ∈ 𝐵 ) ∧ 𝑚 = ( 𝑜 ( .r ‘ 𝑅 ) 𝑎 ) ) ∧ 𝑦 ∈ 𝑖 ) ∧ 𝑓 = ( 𝑦 ( +g ‘ 𝑅 ) 𝑛 ) ) ∧ 𝑞 ∈ 𝐵 ) ∧ 𝑛 = ( 𝑞 ( .r ‘ 𝑅 ) 𝑏 ) ) → ( ( 𝑜 ( .r ‘ 𝑅 ) 𝑞 ) ( .r ‘ 𝑅 ) ( 𝑎 ( .r ‘ 𝑅 ) 𝑏 ) ) ∈ 𝑖 )
199 194 198 eqeltrd ⊢ ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑃 ) ∧ ∀ 𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗 ) ∧ 𝑎 ∈ 𝐵 ) ∧ 𝑏 ∈ 𝐵 ) ∧ ( 𝑎 ( .r ‘ 𝑅 ) 𝑏 ) ∈ 𝑖 ) ∧ ¬ 𝑎 ∈ 𝑖 ) ∧ ¬ 𝑏 ∈ 𝑖 ) ∧ 𝑒 ∈ ( 𝑆 ∩ ( 𝑖 ( LSSum ‘ 𝑅 ) ( ( RSpan ‘ 𝑅 ) ‘ { 𝑎 } ) ) ) ) ∧ 𝑓 ∈ ( 𝑆 ∩ ( 𝑖 ( LSSum ‘ 𝑅 ) ( ( RSpan ‘ 𝑅 ) ‘ { 𝑏 } ) ) ) ) ∧ 𝑥 ∈ 𝑖 ) ∧ 𝑒 = ( 𝑥 ( +g ‘ 𝑅 ) 𝑚 ) ) ∧ 𝑜 ∈ 𝐵 ) ∧ 𝑚 = ( 𝑜 ( .r ‘ 𝑅 ) 𝑎 ) ) ∧ 𝑦 ∈ 𝑖 ) ∧ 𝑓 = ( 𝑦 ( +g ‘ 𝑅 ) 𝑛 ) ) ∧ 𝑞 ∈ 𝐵 ) ∧ 𝑛 = ( 𝑞 ( .r ‘ 𝑅 ) 𝑏 ) ) → ( ( 𝑜 ( .r ‘ 𝑅 ) 𝑎 ) ( .r ‘ 𝑅 ) ( 𝑞 ( .r ‘ 𝑅 ) 𝑏 ) ) ∈ 𝑖 )
200 164 183 192 199 subgcld ⊢ ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑃 ) ∧ ∀ 𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗 ) ∧ 𝑎 ∈ 𝐵 ) ∧ 𝑏 ∈ 𝐵 ) ∧ ( 𝑎 ( .r ‘ 𝑅 ) 𝑏 ) ∈ 𝑖 ) ∧ ¬ 𝑎 ∈ 𝑖 ) ∧ ¬ 𝑏 ∈ 𝑖 ) ∧ 𝑒 ∈ ( 𝑆 ∩ ( 𝑖 ( LSSum ‘ 𝑅 ) ( ( RSpan ‘ 𝑅 ) ‘ { 𝑎 } ) ) ) ) ∧ 𝑓 ∈ ( 𝑆 ∩ ( 𝑖 ( LSSum ‘ 𝑅 ) ( ( RSpan ‘ 𝑅 ) ‘ { 𝑏 } ) ) ) ) ∧ 𝑥 ∈ 𝑖 ) ∧ 𝑒 = ( 𝑥 ( +g ‘ 𝑅 ) 𝑚 ) ) ∧ 𝑜 ∈ 𝐵 ) ∧ 𝑚 = ( 𝑜 ( .r ‘ 𝑅 ) 𝑎 ) ) ∧ 𝑦 ∈ 𝑖 ) ∧ 𝑓 = ( 𝑦 ( +g ‘ 𝑅 ) 𝑛 ) ) ∧ 𝑞 ∈ 𝐵 ) ∧ 𝑛 = ( 𝑞 ( .r ‘ 𝑅 ) 𝑏 ) ) → ( ( 𝑥 ( .r ‘ 𝑅 ) ( 𝑞 ( .r ‘ 𝑅 ) 𝑏 ) ) ( +g ‘ 𝑅 ) ( ( 𝑜 ( .r ‘ 𝑅 ) 𝑎 ) ( .r ‘ 𝑅 ) ( 𝑞 ( .r ‘ 𝑅 ) 𝑏 ) ) ) ∈ 𝑖 )
201 164 183 186 200 subgcld ⊢ ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑃 ) ∧ ∀ 𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗 ) ∧ 𝑎 ∈ 𝐵 ) ∧ 𝑏 ∈ 𝐵 ) ∧ ( 𝑎 ( .r ‘ 𝑅 ) 𝑏 ) ∈ 𝑖 ) ∧ ¬ 𝑎 ∈ 𝑖 ) ∧ ¬ 𝑏 ∈ 𝑖 ) ∧ 𝑒 ∈ ( 𝑆 ∩ ( 𝑖 ( LSSum ‘ 𝑅 ) ( ( RSpan ‘ 𝑅 ) ‘ { 𝑎 } ) ) ) ) ∧ 𝑓 ∈ ( 𝑆 ∩ ( 𝑖 ( LSSum ‘ 𝑅 ) ( ( RSpan ‘ 𝑅 ) ‘ { 𝑏 } ) ) ) ) ∧ 𝑥 ∈ 𝑖 ) ∧ 𝑒 = ( 𝑥 ( +g ‘ 𝑅 ) 𝑚 ) ) ∧ 𝑜 ∈ 𝐵 ) ∧ 𝑚 = ( 𝑜 ( .r ‘ 𝑅 ) 𝑎 ) ) ∧ 𝑦 ∈ 𝑖 ) ∧ 𝑓 = ( 𝑦 ( +g ‘ 𝑅 ) 𝑛 ) ) ∧ 𝑞 ∈ 𝐵 ) ∧ 𝑛 = ( 𝑞 ( .r ‘ 𝑅 ) 𝑏 ) ) → ( ( ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) ( +g ‘ 𝑅 ) ( ( 𝑜 ( .r ‘ 𝑅 ) 𝑎 ) ( .r ‘ 𝑅 ) 𝑦 ) ) ( +g ‘ 𝑅 ) ( ( 𝑥 ( .r ‘ 𝑅 ) ( 𝑞 ( .r ‘ 𝑅 ) 𝑏 ) ) ( +g ‘ 𝑅 ) ( ( 𝑜 ( .r ‘ 𝑅 ) 𝑎 ) ( .r ‘ 𝑅 ) ( 𝑞 ( .r ‘ 𝑅 ) 𝑏 ) ) ) ) ∈ 𝑖 )
202 180 201 eqeltrd ⊢ ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑃 ) ∧ ∀ 𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗 ) ∧ 𝑎 ∈ 𝐵 ) ∧ 𝑏 ∈ 𝐵 ) ∧ ( 𝑎 ( .r ‘ 𝑅 ) 𝑏 ) ∈ 𝑖 ) ∧ ¬ 𝑎 ∈ 𝑖 ) ∧ ¬ 𝑏 ∈ 𝑖 ) ∧ 𝑒 ∈ ( 𝑆 ∩ ( 𝑖 ( LSSum ‘ 𝑅 ) ( ( RSpan ‘ 𝑅 ) ‘ { 𝑎 } ) ) ) ) ∧ 𝑓 ∈ ( 𝑆 ∩ ( 𝑖 ( LSSum ‘ 𝑅 ) ( ( RSpan ‘ 𝑅 ) ‘ { 𝑏 } ) ) ) ) ∧ 𝑥 ∈ 𝑖 ) ∧ 𝑒 = ( 𝑥 ( +g ‘ 𝑅 ) 𝑚 ) ) ∧ 𝑜 ∈ 𝐵 ) ∧ 𝑚 = ( 𝑜 ( .r ‘ 𝑅 ) 𝑎 ) ) ∧ 𝑦 ∈ 𝑖 ) ∧ 𝑓 = ( 𝑦 ( +g ‘ 𝑅 ) 𝑛 ) ) ∧ 𝑞 ∈ 𝐵 ) ∧ 𝑛 = ( 𝑞 ( .r ‘ 𝑅 ) 𝑏 ) ) → ( 𝑒 ( .r ‘ 𝑅 ) 𝑓 ) ∈ 𝑖 )
203 202 r19.29an ⊢ ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑃 ) ∧ ∀ 𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗 ) ∧ 𝑎 ∈ 𝐵 ) ∧ 𝑏 ∈ 𝐵 ) ∧ ( 𝑎 ( .r ‘ 𝑅 ) 𝑏 ) ∈ 𝑖 ) ∧ ¬ 𝑎 ∈ 𝑖 ) ∧ ¬ 𝑏 ∈ 𝑖 ) ∧ 𝑒 ∈ ( 𝑆 ∩ ( 𝑖 ( LSSum ‘ 𝑅 ) ( ( RSpan ‘ 𝑅 ) ‘ { 𝑎 } ) ) ) ) ∧ 𝑓 ∈ ( 𝑆 ∩ ( 𝑖 ( LSSum ‘ 𝑅 ) ( ( RSpan ‘ 𝑅 ) ‘ { 𝑏 } ) ) ) ) ∧ 𝑥 ∈ 𝑖 ) ∧ 𝑒 = ( 𝑥 ( +g ‘ 𝑅 ) 𝑚 ) ) ∧ 𝑜 ∈ 𝐵 ) ∧ 𝑚 = ( 𝑜 ( .r ‘ 𝑅 ) 𝑎 ) ) ∧ 𝑦 ∈ 𝑖 ) ∧ 𝑓 = ( 𝑦 ( +g ‘ 𝑅 ) 𝑛 ) ) ∧ ∃ 𝑞 ∈ 𝐵 𝑛 = ( 𝑞 ( .r ‘ 𝑅 ) 𝑏 ) ) → ( 𝑒 ( .r ‘ 𝑅 ) 𝑓 ) ∈ 𝑖 )
204 155 203 sylbida ⊢ ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑃 ) ∧ ∀ 𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗 ) ∧ 𝑎 ∈ 𝐵 ) ∧ 𝑏 ∈ 𝐵 ) ∧ ( 𝑎 ( .r ‘ 𝑅 ) 𝑏 ) ∈ 𝑖 ) ∧ ¬ 𝑎 ∈ 𝑖 ) ∧ ¬ 𝑏 ∈ 𝑖 ) ∧ 𝑒 ∈ ( 𝑆 ∩ ( 𝑖 ( LSSum ‘ 𝑅 ) ( ( RSpan ‘ 𝑅 ) ‘ { 𝑎 } ) ) ) ) ∧ 𝑓 ∈ ( 𝑆 ∩ ( 𝑖 ( LSSum ‘ 𝑅 ) ( ( RSpan ‘ 𝑅 ) ‘ { 𝑏 } ) ) ) ) ∧ 𝑥 ∈ 𝑖 ) ∧ 𝑒 = ( 𝑥 ( +g ‘ 𝑅 ) 𝑚 ) ) ∧ 𝑜 ∈ 𝐵 ) ∧ 𝑚 = ( 𝑜 ( .r ‘ 𝑅 ) 𝑎 ) ) ∧ 𝑦 ∈ 𝑖 ) ∧ 𝑓 = ( 𝑦 ( +g ‘ 𝑅 ) 𝑛 ) ) ∧ 𝑛 ∈ ( ( RSpan ‘ 𝑅 ) ‘ { 𝑏 } ) ) → ( 𝑒 ( .r ‘ 𝑅 ) 𝑓 ) ∈ 𝑖 )
205 204 an32s ⊢ ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑃 ) ∧ ∀ 𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗 ) ∧ 𝑎 ∈ 𝐵 ) ∧ 𝑏 ∈ 𝐵 ) ∧ ( 𝑎 ( .r ‘ 𝑅 ) 𝑏 ) ∈ 𝑖 ) ∧ ¬ 𝑎 ∈ 𝑖 ) ∧ ¬ 𝑏 ∈ 𝑖 ) ∧ 𝑒 ∈ ( 𝑆 ∩ ( 𝑖 ( LSSum ‘ 𝑅 ) ( ( RSpan ‘ 𝑅 ) ‘ { 𝑎 } ) ) ) ) ∧ 𝑓 ∈ ( 𝑆 ∩ ( 𝑖 ( LSSum ‘ 𝑅 ) ( ( RSpan ‘ 𝑅 ) ‘ { 𝑏 } ) ) ) ) ∧ 𝑥 ∈ 𝑖 ) ∧ 𝑒 = ( 𝑥 ( +g ‘ 𝑅 ) 𝑚 ) ) ∧ 𝑜 ∈ 𝐵 ) ∧ 𝑚 = ( 𝑜 ( .r ‘ 𝑅 ) 𝑎 ) ) ∧ 𝑦 ∈ 𝑖 ) ∧ 𝑛 ∈ ( ( RSpan ‘ 𝑅 ) ‘ { 𝑏 } ) ) ∧ 𝑓 = ( 𝑦 ( +g ‘ 𝑅 ) 𝑛 ) ) → ( 𝑒 ( .r ‘ 𝑅 ) 𝑓 ) ∈ 𝑖 )
206 205 r19.29an ⊢ ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑃 ) ∧ ∀ 𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗 ) ∧ 𝑎 ∈ 𝐵 ) ∧ 𝑏 ∈ 𝐵 ) ∧ ( 𝑎 ( .r ‘ 𝑅 ) 𝑏 ) ∈ 𝑖 ) ∧ ¬ 𝑎 ∈ 𝑖 ) ∧ ¬ 𝑏 ∈ 𝑖 ) ∧ 𝑒 ∈ ( 𝑆 ∩ ( 𝑖 ( LSSum ‘ 𝑅 ) ( ( RSpan ‘ 𝑅 ) ‘ { 𝑎 } ) ) ) ) ∧ 𝑓 ∈ ( 𝑆 ∩ ( 𝑖 ( LSSum ‘ 𝑅 ) ( ( RSpan ‘ 𝑅 ) ‘ { 𝑏 } ) ) ) ) ∧ 𝑥 ∈ 𝑖 ) ∧ 𝑒 = ( 𝑥 ( +g ‘ 𝑅 ) 𝑚 ) ) ∧ 𝑜 ∈ 𝐵 ) ∧ 𝑚 = ( 𝑜 ( .r ‘ 𝑅 ) 𝑎 ) ) ∧ 𝑦 ∈ 𝑖 ) ∧ ∃ 𝑛 ∈ ( ( RSpan ‘ 𝑅 ) ‘ { 𝑏 } ) 𝑓 = ( 𝑦 ( +g ‘ 𝑅 ) 𝑛 ) ) → ( 𝑒 ( .r ‘ 𝑅 ) 𝑓 ) ∈ 𝑖 )
207 113 ad2antrr ⊢ ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑃 ) ∧ ∀ 𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗 ) ∧ 𝑎 ∈ 𝐵 ) ∧ 𝑏 ∈ 𝐵 ) ∧ ( 𝑎 ( .r ‘ 𝑅 ) 𝑏 ) ∈ 𝑖 ) ∧ ¬ 𝑎 ∈ 𝑖 ) ∧ ¬ 𝑏 ∈ 𝑖 ) ∧ 𝑒 ∈ ( 𝑆 ∩ ( 𝑖 ( LSSum ‘ 𝑅 ) ( ( RSpan ‘ 𝑅 ) ‘ { 𝑎 } ) ) ) ) ∧ 𝑓 ∈ ( 𝑆 ∩ ( 𝑖 ( LSSum ‘ 𝑅 ) ( ( RSpan ‘ 𝑅 ) ‘ { 𝑏 } ) ) ) ) → ( ( RSpan ‘ 𝑅 ) ‘ { 𝑏 } ) ∈ ( LIdeal ‘ 𝑅 ) )
208 1 18 lidlss ⊢ ( ( ( RSpan ‘ 𝑅 ) ‘ { 𝑏 } ) ∈ ( LIdeal ‘ 𝑅 ) → ( ( RSpan ‘ 𝑅 ) ‘ { 𝑏 } ) ⊆ 𝐵 )
209 207 208 syl ⊢ ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑃 ) ∧ ∀ 𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗 ) ∧ 𝑎 ∈ 𝐵 ) ∧ 𝑏 ∈ 𝐵 ) ∧ ( 𝑎 ( .r ‘ 𝑅 ) 𝑏 ) ∈ 𝑖 ) ∧ ¬ 𝑎 ∈ 𝑖 ) ∧ ¬ 𝑏 ∈ 𝑖 ) ∧ 𝑒 ∈ ( 𝑆 ∩ ( 𝑖 ( LSSum ‘ 𝑅 ) ( ( RSpan ‘ 𝑅 ) ‘ { 𝑎 } ) ) ) ) ∧ 𝑓 ∈ ( 𝑆 ∩ ( 𝑖 ( LSSum ‘ 𝑅 ) ( ( RSpan ‘ 𝑅 ) ‘ { 𝑏 } ) ) ) ) → ( ( RSpan ‘ 𝑅 ) ‘ { 𝑏 } ) ⊆ 𝐵 )
210 209 ad4antr ⊢ ( ( ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑃 ) ∧ ∀ 𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗 ) ∧ 𝑎 ∈ 𝐵 ) ∧ 𝑏 ∈ 𝐵 ) ∧ ( 𝑎 ( .r ‘ 𝑅 ) 𝑏 ) ∈ 𝑖 ) ∧ ¬ 𝑎 ∈ 𝑖 ) ∧ ¬ 𝑏 ∈ 𝑖 ) ∧ 𝑒 ∈ ( 𝑆 ∩ ( 𝑖 ( LSSum ‘ 𝑅 ) ( ( RSpan ‘ 𝑅 ) ‘ { 𝑎 } ) ) ) ) ∧ 𝑓 ∈ ( 𝑆 ∩ ( 𝑖 ( LSSum ‘ 𝑅 ) ( ( RSpan ‘ 𝑅 ) ‘ { 𝑏 } ) ) ) ) ∧ 𝑥 ∈ 𝑖 ) ∧ 𝑒 = ( 𝑥 ( +g ‘ 𝑅 ) 𝑚 ) ) ∧ 𝑜 ∈ 𝐵 ) ∧ 𝑚 = ( 𝑜 ( .r ‘ 𝑅 ) 𝑎 ) ) → ( ( RSpan ‘ 𝑅 ) ‘ { 𝑏 } ) ⊆ 𝐵 )
211 simpr ⊢ ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑃 ) ∧ ∀ 𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗 ) ∧ 𝑎 ∈ 𝐵 ) ∧ 𝑏 ∈ 𝐵 ) ∧ ( 𝑎 ( .r ‘ 𝑅 ) 𝑏 ) ∈ 𝑖 ) ∧ ¬ 𝑎 ∈ 𝑖 ) ∧ ¬ 𝑏 ∈ 𝑖 ) ∧ 𝑒 ∈ ( 𝑆 ∩ ( 𝑖 ( LSSum ‘ 𝑅 ) ( ( RSpan ‘ 𝑅 ) ‘ { 𝑎 } ) ) ) ) ∧ 𝑓 ∈ ( 𝑆 ∩ ( 𝑖 ( LSSum ‘ 𝑅 ) ( ( RSpan ‘ 𝑅 ) ‘ { 𝑏 } ) ) ) ) → 𝑓 ∈ ( 𝑆 ∩ ( 𝑖 ( LSSum ‘ 𝑅 ) ( ( RSpan ‘ 𝑅 ) ‘ { 𝑏 } ) ) ) )
212 211 elin2d ⊢ ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑃 ) ∧ ∀ 𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗 ) ∧ 𝑎 ∈ 𝐵 ) ∧ 𝑏 ∈ 𝐵 ) ∧ ( 𝑎 ( .r ‘ 𝑅 ) 𝑏 ) ∈ 𝑖 ) ∧ ¬ 𝑎 ∈ 𝑖 ) ∧ ¬ 𝑏 ∈ 𝑖 ) ∧ 𝑒 ∈ ( 𝑆 ∩ ( 𝑖 ( LSSum ‘ 𝑅 ) ( ( RSpan ‘ 𝑅 ) ‘ { 𝑎 } ) ) ) ) ∧ 𝑓 ∈ ( 𝑆 ∩ ( 𝑖 ( LSSum ‘ 𝑅 ) ( ( RSpan ‘ 𝑅 ) ‘ { 𝑏 } ) ) ) ) → 𝑓 ∈ ( 𝑖 ( LSSum ‘ 𝑅 ) ( ( RSpan ‘ 𝑅 ) ‘ { 𝑏 } ) ) )
213 212 ad4antr ⊢ ( ( ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑃 ) ∧ ∀ 𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗 ) ∧ 𝑎 ∈ 𝐵 ) ∧ 𝑏 ∈ 𝐵 ) ∧ ( 𝑎 ( .r ‘ 𝑅 ) 𝑏 ) ∈ 𝑖 ) ∧ ¬ 𝑎 ∈ 𝑖 ) ∧ ¬ 𝑏 ∈ 𝑖 ) ∧ 𝑒 ∈ ( 𝑆 ∩ ( 𝑖 ( LSSum ‘ 𝑅 ) ( ( RSpan ‘ 𝑅 ) ‘ { 𝑎 } ) ) ) ) ∧ 𝑓 ∈ ( 𝑆 ∩ ( 𝑖 ( LSSum ‘ 𝑅 ) ( ( RSpan ‘ 𝑅 ) ‘ { 𝑏 } ) ) ) ) ∧ 𝑥 ∈ 𝑖 ) ∧ 𝑒 = ( 𝑥 ( +g ‘ 𝑅 ) 𝑚 ) ) ∧ 𝑜 ∈ 𝐵 ) ∧ 𝑚 = ( 𝑜 ( .r ‘ 𝑅 ) 𝑎 ) ) → 𝑓 ∈ ( 𝑖 ( LSSum ‘ 𝑅 ) ( ( RSpan ‘ 𝑅 ) ‘ { 𝑏 } ) ) )
214 1 164 60 lsmelvalx ⊢ ( ( 𝑅 ∈ CRing ∧ 𝑖 ⊆ 𝐵 ∧ ( ( RSpan ‘ 𝑅 ) ‘ { 𝑏 } ) ⊆ 𝐵 ) → ( 𝑓 ∈ ( 𝑖 ( LSSum ‘ 𝑅 ) ( ( RSpan ‘ 𝑅 ) ‘ { 𝑏 } ) ) ↔ ∃ 𝑦 ∈ 𝑖 ∃ 𝑛 ∈ ( ( RSpan ‘ 𝑅 ) ‘ { 𝑏 } ) 𝑓 = ( 𝑦 ( +g ‘ 𝑅 ) 𝑛 ) ) )
215 214 biimpa ⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝑖 ⊆ 𝐵 ∧ ( ( RSpan ‘ 𝑅 ) ‘ { 𝑏 } ) ⊆ 𝐵 ) ∧ 𝑓 ∈ ( 𝑖 ( LSSum ‘ 𝑅 ) ( ( RSpan ‘ 𝑅 ) ‘ { 𝑏 } ) ) ) → ∃ 𝑦 ∈ 𝑖 ∃ 𝑛 ∈ ( ( RSpan ‘ 𝑅 ) ‘ { 𝑏 } ) 𝑓 = ( 𝑦 ( +g ‘ 𝑅 ) 𝑛 ) )
216 188 167 210 213 215 syl31anc ⊢ ( ( ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑃 ) ∧ ∀ 𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗 ) ∧ 𝑎 ∈ 𝐵 ) ∧ 𝑏 ∈ 𝐵 ) ∧ ( 𝑎 ( .r ‘ 𝑅 ) 𝑏 ) ∈ 𝑖 ) ∧ ¬ 𝑎 ∈ 𝑖 ) ∧ ¬ 𝑏 ∈ 𝑖 ) ∧ 𝑒 ∈ ( 𝑆 ∩ ( 𝑖 ( LSSum ‘ 𝑅 ) ( ( RSpan ‘ 𝑅 ) ‘ { 𝑎 } ) ) ) ) ∧ 𝑓 ∈ ( 𝑆 ∩ ( 𝑖 ( LSSum ‘ 𝑅 ) ( ( RSpan ‘ 𝑅 ) ‘ { 𝑏 } ) ) ) ) ∧ 𝑥 ∈ 𝑖 ) ∧ 𝑒 = ( 𝑥 ( +g ‘ 𝑅 ) 𝑚 ) ) ∧ 𝑜 ∈ 𝐵 ) ∧ 𝑚 = ( 𝑜 ( .r ‘ 𝑅 ) 𝑎 ) ) → ∃ 𝑦 ∈ 𝑖 ∃ 𝑛 ∈ ( ( RSpan ‘ 𝑅 ) ‘ { 𝑏 } ) 𝑓 = ( 𝑦 ( +g ‘ 𝑅 ) 𝑛 ) )
217 206 216 r19.29a ⊢ ( ( ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑃 ) ∧ ∀ 𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗 ) ∧ 𝑎 ∈ 𝐵 ) ∧ 𝑏 ∈ 𝐵 ) ∧ ( 𝑎 ( .r ‘ 𝑅 ) 𝑏 ) ∈ 𝑖 ) ∧ ¬ 𝑎 ∈ 𝑖 ) ∧ ¬ 𝑏 ∈ 𝑖 ) ∧ 𝑒 ∈ ( 𝑆 ∩ ( 𝑖 ( LSSum ‘ 𝑅 ) ( ( RSpan ‘ 𝑅 ) ‘ { 𝑎 } ) ) ) ) ∧ 𝑓 ∈ ( 𝑆 ∩ ( 𝑖 ( LSSum ‘ 𝑅 ) ( ( RSpan ‘ 𝑅 ) ‘ { 𝑏 } ) ) ) ) ∧ 𝑥 ∈ 𝑖 ) ∧ 𝑒 = ( 𝑥 ( +g ‘ 𝑅 ) 𝑚 ) ) ∧ 𝑜 ∈ 𝐵 ) ∧ 𝑚 = ( 𝑜 ( .r ‘ 𝑅 ) 𝑎 ) ) → ( 𝑒 ( .r ‘ 𝑅 ) 𝑓 ) ∈ 𝑖 )
218 217 r19.29an ⊢ ( ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑃 ) ∧ ∀ 𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗 ) ∧ 𝑎 ∈ 𝐵 ) ∧ 𝑏 ∈ 𝐵 ) ∧ ( 𝑎 ( .r ‘ 𝑅 ) 𝑏 ) ∈ 𝑖 ) ∧ ¬ 𝑎 ∈ 𝑖 ) ∧ ¬ 𝑏 ∈ 𝑖 ) ∧ 𝑒 ∈ ( 𝑆 ∩ ( 𝑖 ( LSSum ‘ 𝑅 ) ( ( RSpan ‘ 𝑅 ) ‘ { 𝑎 } ) ) ) ) ∧ 𝑓 ∈ ( 𝑆 ∩ ( 𝑖 ( LSSum ‘ 𝑅 ) ( ( RSpan ‘ 𝑅 ) ‘ { 𝑏 } ) ) ) ) ∧ 𝑥 ∈ 𝑖 ) ∧ 𝑒 = ( 𝑥 ( +g ‘ 𝑅 ) 𝑚 ) ) ∧ ∃ 𝑜 ∈ 𝐵 𝑚 = ( 𝑜 ( .r ‘ 𝑅 ) 𝑎 ) ) → ( 𝑒 ( .r ‘ 𝑅 ) 𝑓 ) ∈ 𝑖 )
219 150 218 sylbida ⊢ ( ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑃 ) ∧ ∀ 𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗 ) ∧ 𝑎 ∈ 𝐵 ) ∧ 𝑏 ∈ 𝐵 ) ∧ ( 𝑎 ( .r ‘ 𝑅 ) 𝑏 ) ∈ 𝑖 ) ∧ ¬ 𝑎 ∈ 𝑖 ) ∧ ¬ 𝑏 ∈ 𝑖 ) ∧ 𝑒 ∈ ( 𝑆 ∩ ( 𝑖 ( LSSum ‘ 𝑅 ) ( ( RSpan ‘ 𝑅 ) ‘ { 𝑎 } ) ) ) ) ∧ 𝑓 ∈ ( 𝑆 ∩ ( 𝑖 ( LSSum ‘ 𝑅 ) ( ( RSpan ‘ 𝑅 ) ‘ { 𝑏 } ) ) ) ) ∧ 𝑥 ∈ 𝑖 ) ∧ 𝑒 = ( 𝑥 ( +g ‘ 𝑅 ) 𝑚 ) ) ∧ 𝑚 ∈ ( ( RSpan ‘ 𝑅 ) ‘ { 𝑎 } ) ) → ( 𝑒 ( .r ‘ 𝑅 ) 𝑓 ) ∈ 𝑖 )
220 219 an32s ⊢ ( ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑃 ) ∧ ∀ 𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗 ) ∧ 𝑎 ∈ 𝐵 ) ∧ 𝑏 ∈ 𝐵 ) ∧ ( 𝑎 ( .r ‘ 𝑅 ) 𝑏 ) ∈ 𝑖 ) ∧ ¬ 𝑎 ∈ 𝑖 ) ∧ ¬ 𝑏 ∈ 𝑖 ) ∧ 𝑒 ∈ ( 𝑆 ∩ ( 𝑖 ( LSSum ‘ 𝑅 ) ( ( RSpan ‘ 𝑅 ) ‘ { 𝑎 } ) ) ) ) ∧ 𝑓 ∈ ( 𝑆 ∩ ( 𝑖 ( LSSum ‘ 𝑅 ) ( ( RSpan ‘ 𝑅 ) ‘ { 𝑏 } ) ) ) ) ∧ 𝑥 ∈ 𝑖 ) ∧ 𝑚 ∈ ( ( RSpan ‘ 𝑅 ) ‘ { 𝑎 } ) ) ∧ 𝑒 = ( 𝑥 ( +g ‘ 𝑅 ) 𝑚 ) ) → ( 𝑒 ( .r ‘ 𝑅 ) 𝑓 ) ∈ 𝑖 )
221 220 r19.29an ⊢ ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑃 ) ∧ ∀ 𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗 ) ∧ 𝑎 ∈ 𝐵 ) ∧ 𝑏 ∈ 𝐵 ) ∧ ( 𝑎 ( .r ‘ 𝑅 ) 𝑏 ) ∈ 𝑖 ) ∧ ¬ 𝑎 ∈ 𝑖 ) ∧ ¬ 𝑏 ∈ 𝑖 ) ∧ 𝑒 ∈ ( 𝑆 ∩ ( 𝑖 ( LSSum ‘ 𝑅 ) ( ( RSpan ‘ 𝑅 ) ‘ { 𝑎 } ) ) ) ) ∧ 𝑓 ∈ ( 𝑆 ∩ ( 𝑖 ( LSSum ‘ 𝑅 ) ( ( RSpan ‘ 𝑅 ) ‘ { 𝑏 } ) ) ) ) ∧ 𝑥 ∈ 𝑖 ) ∧ ∃ 𝑚 ∈ ( ( RSpan ‘ 𝑅 ) ‘ { 𝑎 } ) 𝑒 = ( 𝑥 ( +g ‘ 𝑅 ) 𝑚 ) ) → ( 𝑒 ( .r ‘ 𝑅 ) 𝑓 ) ∈ 𝑖 )
222 57 ad2antrr ⊢ ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑃 ) ∧ ∀ 𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗 ) ∧ 𝑎 ∈ 𝐵 ) ∧ 𝑏 ∈ 𝐵 ) ∧ ( 𝑎 ( .r ‘ 𝑅 ) 𝑏 ) ∈ 𝑖 ) ∧ ¬ 𝑎 ∈ 𝑖 ) ∧ ¬ 𝑏 ∈ 𝑖 ) ∧ 𝑒 ∈ ( 𝑆 ∩ ( 𝑖 ( LSSum ‘ 𝑅 ) ( ( RSpan ‘ 𝑅 ) ‘ { 𝑎 } ) ) ) ) ∧ 𝑓 ∈ ( 𝑆 ∩ ( 𝑖 ( LSSum ‘ 𝑅 ) ( ( RSpan ‘ 𝑅 ) ‘ { 𝑏 } ) ) ) ) → ( ( RSpan ‘ 𝑅 ) ‘ { 𝑎 } ) ∈ ( LIdeal ‘ 𝑅 ) )
223 1 18 lidlss ⊢ ( ( ( RSpan ‘ 𝑅 ) ‘ { 𝑎 } ) ∈ ( LIdeal ‘ 𝑅 ) → ( ( RSpan ‘ 𝑅 ) ‘ { 𝑎 } ) ⊆ 𝐵 )
224 222 223 syl ⊢ ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑃 ) ∧ ∀ 𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗 ) ∧ 𝑎 ∈ 𝐵 ) ∧ 𝑏 ∈ 𝐵 ) ∧ ( 𝑎 ( .r ‘ 𝑅 ) 𝑏 ) ∈ 𝑖 ) ∧ ¬ 𝑎 ∈ 𝑖 ) ∧ ¬ 𝑏 ∈ 𝑖 ) ∧ 𝑒 ∈ ( 𝑆 ∩ ( 𝑖 ( LSSum ‘ 𝑅 ) ( ( RSpan ‘ 𝑅 ) ‘ { 𝑎 } ) ) ) ) ∧ 𝑓 ∈ ( 𝑆 ∩ ( 𝑖 ( LSSum ‘ 𝑅 ) ( ( RSpan ‘ 𝑅 ) ‘ { 𝑏 } ) ) ) ) → ( ( RSpan ‘ 𝑅 ) ‘ { 𝑎 } ) ⊆ 𝐵 )
225 simplr ⊢ ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑃 ) ∧ ∀ 𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗 ) ∧ 𝑎 ∈ 𝐵 ) ∧ 𝑏 ∈ 𝐵 ) ∧ ( 𝑎 ( .r ‘ 𝑅 ) 𝑏 ) ∈ 𝑖 ) ∧ ¬ 𝑎 ∈ 𝑖 ) ∧ ¬ 𝑏 ∈ 𝑖 ) ∧ 𝑒 ∈ ( 𝑆 ∩ ( 𝑖 ( LSSum ‘ 𝑅 ) ( ( RSpan ‘ 𝑅 ) ‘ { 𝑎 } ) ) ) ) ∧ 𝑓 ∈ ( 𝑆 ∩ ( 𝑖 ( LSSum ‘ 𝑅 ) ( ( RSpan ‘ 𝑅 ) ‘ { 𝑏 } ) ) ) ) → 𝑒 ∈ ( 𝑆 ∩ ( 𝑖 ( LSSum ‘ 𝑅 ) ( ( RSpan ‘ 𝑅 ) ‘ { 𝑎 } ) ) ) )
226 225 elin2d ⊢ ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑃 ) ∧ ∀ 𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗 ) ∧ 𝑎 ∈ 𝐵 ) ∧ 𝑏 ∈ 𝐵 ) ∧ ( 𝑎 ( .r ‘ 𝑅 ) 𝑏 ) ∈ 𝑖 ) ∧ ¬ 𝑎 ∈ 𝑖 ) ∧ ¬ 𝑏 ∈ 𝑖 ) ∧ 𝑒 ∈ ( 𝑆 ∩ ( 𝑖 ( LSSum ‘ 𝑅 ) ( ( RSpan ‘ 𝑅 ) ‘ { 𝑎 } ) ) ) ) ∧ 𝑓 ∈ ( 𝑆 ∩ ( 𝑖 ( LSSum ‘ 𝑅 ) ( ( RSpan ‘ 𝑅 ) ‘ { 𝑏 } ) ) ) ) → 𝑒 ∈ ( 𝑖 ( LSSum ‘ 𝑅 ) ( ( RSpan ‘ 𝑅 ) ‘ { 𝑎 } ) ) )
227 1 164 60 lsmelvalx ⊢ ( ( 𝑅 ∈ CRing ∧ 𝑖 ⊆ 𝐵 ∧ ( ( RSpan ‘ 𝑅 ) ‘ { 𝑎 } ) ⊆ 𝐵 ) → ( 𝑒 ∈ ( 𝑖 ( LSSum ‘ 𝑅 ) ( ( RSpan ‘ 𝑅 ) ‘ { 𝑎 } ) ) ↔ ∃ 𝑥 ∈ 𝑖 ∃ 𝑚 ∈ ( ( RSpan ‘ 𝑅 ) ‘ { 𝑎 } ) 𝑒 = ( 𝑥 ( +g ‘ 𝑅 ) 𝑚 ) ) )
228 227 biimpa ⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝑖 ⊆ 𝐵 ∧ ( ( RSpan ‘ 𝑅 ) ‘ { 𝑎 } ) ⊆ 𝐵 ) ∧ 𝑒 ∈ ( 𝑖 ( LSSum ‘ 𝑅 ) ( ( RSpan ‘ 𝑅 ) ‘ { 𝑎 } ) ) ) → ∃ 𝑥 ∈ 𝑖 ∃ 𝑚 ∈ ( ( RSpan ‘ 𝑅 ) ‘ { 𝑎 } ) 𝑒 = ( 𝑥 ( +g ‘ 𝑅 ) 𝑚 ) )
229 187 166 224 226 228 syl31anc ⊢ ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑃 ) ∧ ∀ 𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗 ) ∧ 𝑎 ∈ 𝐵 ) ∧ 𝑏 ∈ 𝐵 ) ∧ ( 𝑎 ( .r ‘ 𝑅 ) 𝑏 ) ∈ 𝑖 ) ∧ ¬ 𝑎 ∈ 𝑖 ) ∧ ¬ 𝑏 ∈ 𝑖 ) ∧ 𝑒 ∈ ( 𝑆 ∩ ( 𝑖 ( LSSum ‘ 𝑅 ) ( ( RSpan ‘ 𝑅 ) ‘ { 𝑎 } ) ) ) ) ∧ 𝑓 ∈ ( 𝑆 ∩ ( 𝑖 ( LSSum ‘ 𝑅 ) ( ( RSpan ‘ 𝑅 ) ‘ { 𝑏 } ) ) ) ) → ∃ 𝑥 ∈ 𝑖 ∃ 𝑚 ∈ ( ( RSpan ‘ 𝑅 ) ‘ { 𝑎 } ) 𝑒 = ( 𝑥 ( +g ‘ 𝑅 ) 𝑚 ) )
230 221 229 r19.29a ⊢ ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑃 ) ∧ ∀ 𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗 ) ∧ 𝑎 ∈ 𝐵 ) ∧ 𝑏 ∈ 𝐵 ) ∧ ( 𝑎 ( .r ‘ 𝑅 ) 𝑏 ) ∈ 𝑖 ) ∧ ¬ 𝑎 ∈ 𝑖 ) ∧ ¬ 𝑏 ∈ 𝑖 ) ∧ 𝑒 ∈ ( 𝑆 ∩ ( 𝑖 ( LSSum ‘ 𝑅 ) ( ( RSpan ‘ 𝑅 ) ‘ { 𝑎 } ) ) ) ) ∧ 𝑓 ∈ ( 𝑆 ∩ ( 𝑖 ( LSSum ‘ 𝑅 ) ( ( RSpan ‘ 𝑅 ) ‘ { 𝑏 } ) ) ) ) → ( 𝑒 ( .r ‘ 𝑅 ) 𝑓 ) ∈ 𝑖 )
231 5 148 mgpplusg ⊢ ( .r ‘ 𝑅 ) = ( +g ‘ 𝑀 )
232 4 ad9antr ⊢ ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑃 ) ∧ ∀ 𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗 ) ∧ 𝑎 ∈ 𝐵 ) ∧ 𝑏 ∈ 𝐵 ) ∧ ( 𝑎 ( .r ‘ 𝑅 ) 𝑏 ) ∈ 𝑖 ) ∧ ¬ 𝑎 ∈ 𝑖 ) ∧ ¬ 𝑏 ∈ 𝑖 ) ∧ 𝑒 ∈ ( 𝑆 ∩ ( 𝑖 ( LSSum ‘ 𝑅 ) ( ( RSpan ‘ 𝑅 ) ‘ { 𝑎 } ) ) ) ) ∧ 𝑓 ∈ ( 𝑆 ∩ ( 𝑖 ( LSSum ‘ 𝑅 ) ( ( RSpan ‘ 𝑅 ) ‘ { 𝑏 } ) ) ) ) → 𝑆 ∈ ( SubMnd ‘ 𝑀 ) )
233 225 elin1d ⊢ ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑃 ) ∧ ∀ 𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗 ) ∧ 𝑎 ∈ 𝐵 ) ∧ 𝑏 ∈ 𝐵 ) ∧ ( 𝑎 ( .r ‘ 𝑅 ) 𝑏 ) ∈ 𝑖 ) ∧ ¬ 𝑎 ∈ 𝑖 ) ∧ ¬ 𝑏 ∈ 𝑖 ) ∧ 𝑒 ∈ ( 𝑆 ∩ ( 𝑖 ( LSSum ‘ 𝑅 ) ( ( RSpan ‘ 𝑅 ) ‘ { 𝑎 } ) ) ) ) ∧ 𝑓 ∈ ( 𝑆 ∩ ( 𝑖 ( LSSum ‘ 𝑅 ) ( ( RSpan ‘ 𝑅 ) ‘ { 𝑏 } ) ) ) ) → 𝑒 ∈ 𝑆 )
234 211 elin1d ⊢ ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑃 ) ∧ ∀ 𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗 ) ∧ 𝑎 ∈ 𝐵 ) ∧ 𝑏 ∈ 𝐵 ) ∧ ( 𝑎 ( .r ‘ 𝑅 ) 𝑏 ) ∈ 𝑖 ) ∧ ¬ 𝑎 ∈ 𝑖 ) ∧ ¬ 𝑏 ∈ 𝑖 ) ∧ 𝑒 ∈ ( 𝑆 ∩ ( 𝑖 ( LSSum ‘ 𝑅 ) ( ( RSpan ‘ 𝑅 ) ‘ { 𝑎 } ) ) ) ) ∧ 𝑓 ∈ ( 𝑆 ∩ ( 𝑖 ( LSSum ‘ 𝑅 ) ( ( RSpan ‘ 𝑅 ) ‘ { 𝑏 } ) ) ) ) → 𝑓 ∈ 𝑆 )
235 231 232 233 234 submcld ⊢ ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑃 ) ∧ ∀ 𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗 ) ∧ 𝑎 ∈ 𝐵 ) ∧ 𝑏 ∈ 𝐵 ) ∧ ( 𝑎 ( .r ‘ 𝑅 ) 𝑏 ) ∈ 𝑖 ) ∧ ¬ 𝑎 ∈ 𝑖 ) ∧ ¬ 𝑏 ∈ 𝑖 ) ∧ 𝑒 ∈ ( 𝑆 ∩ ( 𝑖 ( LSSum ‘ 𝑅 ) ( ( RSpan ‘ 𝑅 ) ‘ { 𝑎 } ) ) ) ) ∧ 𝑓 ∈ ( 𝑆 ∩ ( 𝑖 ( LSSum ‘ 𝑅 ) ( ( RSpan ‘ 𝑅 ) ‘ { 𝑏 } ) ) ) ) → ( 𝑒 ( .r ‘ 𝑅 ) 𝑓 ) ∈ 𝑆 )
236 230 235 elind ⊢ ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑃 ) ∧ ∀ 𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗 ) ∧ 𝑎 ∈ 𝐵 ) ∧ 𝑏 ∈ 𝐵 ) ∧ ( 𝑎 ( .r ‘ 𝑅 ) 𝑏 ) ∈ 𝑖 ) ∧ ¬ 𝑎 ∈ 𝑖 ) ∧ ¬ 𝑏 ∈ 𝑖 ) ∧ 𝑒 ∈ ( 𝑆 ∩ ( 𝑖 ( LSSum ‘ 𝑅 ) ( ( RSpan ‘ 𝑅 ) ‘ { 𝑎 } ) ) ) ) ∧ 𝑓 ∈ ( 𝑆 ∩ ( 𝑖 ( LSSum ‘ 𝑅 ) ( ( RSpan ‘ 𝑅 ) ‘ { 𝑏 } ) ) ) ) → ( 𝑒 ( .r ‘ 𝑅 ) 𝑓 ) ∈ ( 𝑖 ∩ 𝑆 ) )
237 236 ne0d ⊢ ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑃 ) ∧ ∀ 𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗 ) ∧ 𝑎 ∈ 𝐵 ) ∧ 𝑏 ∈ 𝐵 ) ∧ ( 𝑎 ( .r ‘ 𝑅 ) 𝑏 ) ∈ 𝑖 ) ∧ ¬ 𝑎 ∈ 𝑖 ) ∧ ¬ 𝑏 ∈ 𝑖 ) ∧ 𝑒 ∈ ( 𝑆 ∩ ( 𝑖 ( LSSum ‘ 𝑅 ) ( ( RSpan ‘ 𝑅 ) ‘ { 𝑎 } ) ) ) ) ∧ 𝑓 ∈ ( 𝑆 ∩ ( 𝑖 ( LSSum ‘ 𝑅 ) ( ( RSpan ‘ 𝑅 ) ‘ { 𝑏 } ) ) ) ) → ( 𝑖 ∩ 𝑆 ) ≠ ∅ )
238 143 237 exlimddv ⊢ ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑃 ) ∧ ∀ 𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗 ) ∧ 𝑎 ∈ 𝐵 ) ∧ 𝑏 ∈ 𝐵 ) ∧ ( 𝑎 ( .r ‘ 𝑅 ) 𝑏 ) ∈ 𝑖 ) ∧ ¬ 𝑎 ∈ 𝑖 ) ∧ ¬ 𝑏 ∈ 𝑖 ) ∧ 𝑒 ∈ ( 𝑆 ∩ ( 𝑖 ( LSSum ‘ 𝑅 ) ( ( RSpan ‘ 𝑅 ) ‘ { 𝑎 } ) ) ) ) → ( 𝑖 ∩ 𝑆 ) ≠ ∅ )
239 109 238 exlimddv ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑃 ) ∧ ∀ 𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗 ) ∧ 𝑎 ∈ 𝐵 ) ∧ 𝑏 ∈ 𝐵 ) ∧ ( 𝑎 ( .r ‘ 𝑅 ) 𝑏 ) ∈ 𝑖 ) ∧ ¬ 𝑎 ∈ 𝑖 ) ∧ ¬ 𝑏 ∈ 𝑖 ) → ( 𝑖 ∩ 𝑆 ) ≠ ∅ )
240 239 anasss ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑃 ) ∧ ∀ 𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗 ) ∧ 𝑎 ∈ 𝐵 ) ∧ 𝑏 ∈ 𝐵 ) ∧ ( 𝑎 ( .r ‘ 𝑅 ) 𝑏 ) ∈ 𝑖 ) ∧ ( ¬ 𝑎 ∈ 𝑖 ∧ ¬ 𝑏 ∈ 𝑖 ) ) → ( 𝑖 ∩ 𝑆 ) ≠ ∅ )
241 48 240 sylan2b ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑃 ) ∧ ∀ 𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗 ) ∧ 𝑎 ∈ 𝐵 ) ∧ 𝑏 ∈ 𝐵 ) ∧ ( 𝑎 ( .r ‘ 𝑅 ) 𝑏 ) ∈ 𝑖 ) ∧ ¬ ( 𝑎 ∈ 𝑖 ∨ 𝑏 ∈ 𝑖 ) ) → ( 𝑖 ∩ 𝑆 ) ≠ ∅ )
242 241 neneqd ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑃 ) ∧ ∀ 𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗 ) ∧ 𝑎 ∈ 𝐵 ) ∧ 𝑏 ∈ 𝐵 ) ∧ ( 𝑎 ( .r ‘ 𝑅 ) 𝑏 ) ∈ 𝑖 ) ∧ ¬ ( 𝑎 ∈ 𝑖 ∨ 𝑏 ∈ 𝑖 ) ) → ¬ ( 𝑖 ∩ 𝑆 ) = ∅ )
243 47 242 condan ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑃 ) ∧ ∀ 𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗 ) ∧ 𝑎 ∈ 𝐵 ) ∧ 𝑏 ∈ 𝐵 ) ∧ ( 𝑎 ( .r ‘ 𝑅 ) 𝑏 ) ∈ 𝑖 ) → ( 𝑎 ∈ 𝑖 ∨ 𝑏 ∈ 𝑖 ) )
244 243 ex ⊢ ( ( ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑃 ) ∧ ∀ 𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗 ) ∧ 𝑎 ∈ 𝐵 ) ∧ 𝑏 ∈ 𝐵 ) → ( ( 𝑎 ( .r ‘ 𝑅 ) 𝑏 ) ∈ 𝑖 → ( 𝑎 ∈ 𝑖 ∨ 𝑏 ∈ 𝑖 ) ) )
245 244 anasss ⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑃 ) ∧ ∀ 𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗 ) ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ) ) → ( ( 𝑎 ( .r ‘ 𝑅 ) 𝑏 ) ∈ 𝑖 → ( 𝑎 ∈ 𝑖 ∨ 𝑏 ∈ 𝑖 ) ) )
246 245 ralrimivva ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑃 ) ∧ ∀ 𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗 ) → ∀ 𝑎 ∈ 𝐵 ∀ 𝑏 ∈ 𝐵 ( ( 𝑎 ( .r ‘ 𝑅 ) 𝑏 ) ∈ 𝑖 → ( 𝑎 ∈ 𝑖 ∨ 𝑏 ∈ 𝑖 ) ) )
247 1 148 isprmidlc ⊢ ( 𝑅 ∈ CRing → ( 𝑖 ∈ ( PrmIdeal ‘ 𝑅 ) ↔ ( 𝑖 ∈ ( LIdeal ‘ 𝑅 ) ∧ 𝑖 ≠ 𝐵 ∧ ∀ 𝑎 ∈ 𝐵 ∀ 𝑏 ∈ 𝐵 ( ( 𝑎 ( .r ‘ 𝑅 ) 𝑏 ) ∈ 𝑖 → ( 𝑎 ∈ 𝑖 ∨ 𝑏 ∈ 𝑖 ) ) ) ) )
248 247 biimpar ⊢ ( ( 𝑅 ∈ CRing ∧ ( 𝑖 ∈ ( LIdeal ‘ 𝑅 ) ∧ 𝑖 ≠ 𝐵 ∧ ∀ 𝑎 ∈ 𝐵 ∀ 𝑏 ∈ 𝐵 ( ( 𝑎 ( .r ‘ 𝑅 ) 𝑏 ) ∈ 𝑖 → ( 𝑎 ∈ 𝑖 ∨ 𝑏 ∈ 𝑖 ) ) ) ) → 𝑖 ∈ ( PrmIdeal ‘ 𝑅 ) )
249 8 12 46 246 248 syl13anc ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑃 ) ∧ ∀ 𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗 ) → 𝑖 ∈ ( PrmIdeal ‘ 𝑅 ) )
250 249 anasss ⊢ ( ( 𝜑 ∧ ( 𝑖 ∈ 𝑃 ∧ ∀ 𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗 ) ) → 𝑖 ∈ ( PrmIdeal ‘ 𝑅 ) )
251 simprr ⊢ ( ( 𝜑 ∧ ( 𝑖 ∈ 𝑃 ∧ ∀ 𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗 ) ) → ∀ 𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗 )
252 250 251 jca ⊢ ( ( 𝜑 ∧ ( 𝑖 ∈ 𝑃 ∧ ∀ 𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗 ) ) → ( 𝑖 ∈ ( PrmIdeal ‘ 𝑅 ) ∧ ∀ 𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗 ) )
253 5 1 mgpbas ⊢ 𝐵 = ( Base ‘ 𝑀 )
254 253 submss ⊢ ( 𝑆 ∈ ( SubMnd ‘ 𝑀 ) → 𝑆 ⊆ 𝐵 )
255 4 254 syl ⊢ ( 𝜑 → 𝑆 ⊆ 𝐵 )
256 1 13 3 255 6 7 ssdifidl ⊢ ( 𝜑 → ∃ 𝑖 ∈ 𝑃 ∀ 𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗 )
257 252 256 reximddv ⊢ ( 𝜑 → ∃ 𝑖 ∈ 𝑃 ( 𝑖 ∈ ( PrmIdeal ‘ 𝑅 ) ∧ ∀ 𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗 ) )