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

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 
|- B = ( Base ` R )
ssdifidlprm.2 
|- ( ph -> R e. CRing )
ssdifidlprm.3 
|- ( ph -> I e. ( LIdeal ` R ) )
ssdifidlprm.4 
|- ( ph -> S e. ( SubMnd ` M ) )
ssdifidlprm.5 
|- M = ( mulGrp ` R )
ssdifidlprm.6 
|- ( ph -> ( S i^i I ) = (/) )
ssdifidlprm.7 
|- P = { p e. ( LIdeal ` R ) | ( ( S i^i p ) = (/) /\ I C_ p ) }
Assertion ssdifidlprm 
|- ( ph -> E. i e. P ( i e. ( PrmIdeal ` R ) /\ A. j e. P -. i C. j ) )

Proof

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