Metamath Proof Explorer


Theorem dprd2da

Description: The direct product of a collection of direct products. (Contributed by Mario Carneiro, 26-Apr-2016)

Ref Expression
Hypotheses dprd2d.1 φ Rel A
dprd2d.2 φ S : A SubGrp G
dprd2d.3 φ dom A I
dprd2d.4 φ i I G dom DProd j A i i S j
dprd2d.5 φ G dom DProd i I G DProd j A i i S j
dprd2d.k K = mrCls SubGrp G
Assertion dprd2da φ G dom DProd S

Proof

Step Hyp Ref Expression
1 dprd2d.1 φ Rel A
2 dprd2d.2 φ S : A SubGrp G
3 dprd2d.3 φ dom A I
4 dprd2d.4 φ i I G dom DProd j A i i S j
5 dprd2d.5 φ G dom DProd i I G DProd j A i i S j
6 dprd2d.k K = mrCls SubGrp G
7 eqid Cntz G = Cntz G
8 eqid 0 G = 0 G
9 dprdgrp G dom DProd i I G DProd j A i i S j G Grp
10 5 9 syl φ G Grp
11 resiun2 A i I i = i I A i
12 iunid i I i = I
13 12 reseq2i A i I i = A I
14 11 13 eqtr3i i I A i = A I
15 relssres Rel A dom A I A I = A
16 1 3 15 syl2anc φ A I = A
17 14 16 syl5eq φ i I A i = A
18 ovex G DProd j A i i S j V
19 eqid i I G DProd j A i i S j = i I G DProd j A i i S j
20 18 19 dmmpti dom i I G DProd j A i i S j = I
21 reldmdprd Rel dom DProd
22 21 brrelex2i G dom DProd i I G DProd j A i i S j i I G DProd j A i i S j V
23 dmexg i I G DProd j A i i S j V dom i I G DProd j A i i S j V
24 5 22 23 3syl φ dom i I G DProd j A i i S j V
25 20 24 eqeltrrid φ I V
26 ressn A i = i × A i
27 snex i V
28 ovex i S j V
29 eqid j A i i S j = j A i i S j
30 28 29 dmmpti dom j A i i S j = A i
31 21 brrelex2i G dom DProd j A i i S j j A i i S j V
32 dmexg j A i i S j V dom j A i i S j V
33 4 31 32 3syl φ i I dom j A i i S j V
34 30 33 eqeltrrid φ i I A i V
35 xpexg i V A i V i × A i V
36 27 34 35 sylancr φ i I i × A i V
37 26 36 eqeltrid φ i I A i V
38 37 ralrimiva φ i I A i V
39 iunexg I V i I A i V i I A i V
40 25 38 39 syl2anc φ i I A i V
41 17 40 eqeltrrd φ A V
42 sneq i = 1 st x i = 1 st x
43 42 imaeq2d i = 1 st x A i = A 1 st x
44 oveq1 i = 1 st x i S j = 1 st x S j
45 43 44 mpteq12dv i = 1 st x j A i i S j = j A 1 st x 1 st x S j
46 45 breq2d i = 1 st x G dom DProd j A i i S j G dom DProd j A 1 st x 1 st x S j
47 4 ralrimiva φ i I G dom DProd j A i i S j
48 47 adantr φ x A i I G dom DProd j A i i S j
49 3 adantr φ x A dom A I
50 1stdm Rel A x A 1 st x dom A
51 1 50 sylan φ x A 1 st x dom A
52 49 51 sseldd φ x A 1 st x I
53 46 48 52 rspcdva φ x A G dom DProd j A 1 st x 1 st x S j
54 53 3ad2antr1 φ x A y A x y G dom DProd j A 1 st x 1 st x S j
55 54 adantr φ x A y A x y 1 st x = 1 st y G dom DProd j A 1 st x 1 st x S j
56 ovex 1 st x S j V
57 eqid j A 1 st x 1 st x S j = j A 1 st x 1 st x S j
58 56 57 dmmpti dom j A 1 st x 1 st x S j = A 1 st x
59 58 a1i φ x A y A x y 1 st x = 1 st y dom j A 1 st x 1 st x S j = A 1 st x
60 1st2nd Rel A x A x = 1 st x 2 nd x
61 1 60 sylan φ x A x = 1 st x 2 nd x
62 simpr φ x A x A
63 61 62 eqeltrrd φ x A 1 st x 2 nd x A
64 df-br 1 st x A 2 nd x 1 st x 2 nd x A
65 63 64 sylibr φ x A 1 st x A 2 nd x
66 1 adantr φ x A Rel A
67 elrelimasn Rel A 2 nd x A 1 st x 1 st x A 2 nd x
68 66 67 syl φ x A 2 nd x A 1 st x 1 st x A 2 nd x
69 65 68 mpbird φ x A 2 nd x A 1 st x
70 69 3ad2antr1 φ x A y A x y 2 nd x A 1 st x
71 70 adantr φ x A y A x y 1 st x = 1 st y 2 nd x A 1 st x
72 1 adantr φ x A y A x y Rel A
73 simpr2 φ x A y A x y y A
74 1st2nd Rel A y A y = 1 st y 2 nd y
75 72 73 74 syl2anc φ x A y A x y y = 1 st y 2 nd y
76 75 73 eqeltrrd φ x A y A x y 1 st y 2 nd y A
77 df-br 1 st y A 2 nd y 1 st y 2 nd y A
78 76 77 sylibr φ x A y A x y 1 st y A 2 nd y
79 elrelimasn Rel A 2 nd y A 1 st y 1 st y A 2 nd y
80 72 79 syl φ x A y A x y 2 nd y A 1 st y 1 st y A 2 nd y
81 78 80 mpbird φ x A y A x y 2 nd y A 1 st y
82 81 adantr φ x A y A x y 1 st x = 1 st y 2 nd y A 1 st y
83 simpr φ x A y A x y 1 st x = 1 st y 1 st x = 1 st y
84 83 sneqd φ x A y A x y 1 st x = 1 st y 1 st x = 1 st y
85 84 imaeq2d φ x A y A x y 1 st x = 1 st y A 1 st x = A 1 st y
86 82 85 eleqtrrd φ x A y A x y 1 st x = 1 st y 2 nd y A 1 st x
87 simplr3 φ x A y A x y 1 st x = 1 st y x y
88 simpr1 φ x A y A x y x A
89 72 88 60 syl2anc φ x A y A x y x = 1 st x 2 nd x
90 89 75 eqeq12d φ x A y A x y x = y 1 st x 2 nd x = 1 st y 2 nd y
91 fvex 1 st x V
92 fvex 2 nd x V
93 91 92 opth 1 st x 2 nd x = 1 st y 2 nd y 1 st x = 1 st y 2 nd x = 2 nd y
94 90 93 bitrdi φ x A y A x y x = y 1 st x = 1 st y 2 nd x = 2 nd y
95 94 baibd φ x A y A x y 1 st x = 1 st y x = y 2 nd x = 2 nd y
96 95 necon3bid φ x A y A x y 1 st x = 1 st y x y 2 nd x 2 nd y
97 87 96 mpbid φ x A y A x y 1 st x = 1 st y 2 nd x 2 nd y
98 55 59 71 86 97 7 dprdcntz φ x A y A x y 1 st x = 1 st y j A 1 st x 1 st x S j 2 nd x Cntz G j A 1 st x 1 st x S j 2 nd y
99 df-ov 1 st x S 2 nd x = S 1 st x 2 nd x
100 oveq2 j = 2 nd x 1 st x S j = 1 st x S 2 nd x
101 100 57 56 fvmpt3i 2 nd x A 1 st x j A 1 st x 1 st x S j 2 nd x = 1 st x S 2 nd x
102 70 101 syl φ x A y A x y j A 1 st x 1 st x S j 2 nd x = 1 st x S 2 nd x
103 89 fveq2d φ x A y A x y S x = S 1 st x 2 nd x
104 99 102 103 3eqtr4a φ x A y A x y j A 1 st x 1 st x S j 2 nd x = S x
105 104 adantr φ x A y A x y 1 st x = 1 st y j A 1 st x 1 st x S j 2 nd x = S x
106 83 oveq1d φ x A y A x y 1 st x = 1 st y 1 st x S j = 1 st y S j
107 85 106 mpteq12dv φ x A y A x y 1 st x = 1 st y j A 1 st x 1 st x S j = j A 1 st y 1 st y S j
108 107 fveq1d φ x A y A x y 1 st x = 1 st y j A 1 st x 1 st x S j 2 nd y = j A 1 st y 1 st y S j 2 nd y
109 df-ov 1 st y S 2 nd y = S 1 st y 2 nd y
110 oveq2 j = 2 nd y 1 st y S j = 1 st y S 2 nd y
111 eqid j A 1 st y 1 st y S j = j A 1 st y 1 st y S j
112 ovex 1 st y S j V
113 110 111 112 fvmpt3i 2 nd y A 1 st y j A 1 st y 1 st y S j 2 nd y = 1 st y S 2 nd y
114 81 113 syl φ x A y A x y j A 1 st y 1 st y S j 2 nd y = 1 st y S 2 nd y
115 75 fveq2d φ x A y A x y S y = S 1 st y 2 nd y
116 109 114 115 3eqtr4a φ x A y A x y j A 1 st y 1 st y S j 2 nd y = S y
117 116 adantr φ x A y A x y 1 st x = 1 st y j A 1 st y 1 st y S j 2 nd y = S y
118 108 117 eqtrd φ x A y A x y 1 st x = 1 st y j A 1 st x 1 st x S j 2 nd y = S y
119 118 fveq2d φ x A y A x y 1 st x = 1 st y Cntz G j A 1 st x 1 st x S j 2 nd y = Cntz G S y
120 98 105 119 3sstr3d φ x A y A x y 1 st x = 1 st y S x Cntz G S y
121 1 2 3 4 5 6 dprd2dlem2 φ x A S x G DProd j A 1 st x 1 st x S j
122 45 oveq2d i = 1 st x G DProd j A i i S j = G DProd j A 1 st x 1 st x S j
123 122 19 18 fvmpt3i 1 st x I i I G DProd j A i i S j 1 st x = G DProd j A 1 st x 1 st x S j
124 52 123 syl φ x A i I G DProd j A i i S j 1 st x = G DProd j A 1 st x 1 st x S j
125 121 124 sseqtrrd φ x A S x i I G DProd j A i i S j 1 st x
126 125 3ad2antr1 φ x A y A x y S x i I G DProd j A i i S j 1 st x
127 126 adantr φ x A y A x y 1 st x 1 st y S x i I G DProd j A i i S j 1 st x
128 5 ad2antrr φ x A y A x y 1 st x 1 st y G dom DProd i I G DProd j A i i S j
129 20 a1i φ x A y A x y 1 st x 1 st y dom i I G DProd j A i i S j = I
130 52 3ad2antr1 φ x A y A x y 1 st x I
131 130 adantr φ x A y A x y 1 st x 1 st y 1 st x I
132 3 adantr φ x A y A x y dom A I
133 1stdm Rel A y A 1 st y dom A
134 72 73 133 syl2anc φ x A y A x y 1 st y dom A
135 132 134 sseldd φ x A y A x y 1 st y I
136 135 adantr φ x A y A x y 1 st x 1 st y 1 st y I
137 simpr φ x A y A x y 1 st x 1 st y 1 st x 1 st y
138 128 129 131 136 137 7 dprdcntz φ x A y A x y 1 st x 1 st y i I G DProd j A i i S j 1 st x Cntz G i I G DProd j A i i S j 1 st y
139 sneq i = 1 st y i = 1 st y
140 139 imaeq2d i = 1 st y A i = A 1 st y
141 oveq1 i = 1 st y i S j = 1 st y S j
142 140 141 mpteq12dv i = 1 st y j A i i S j = j A 1 st y 1 st y S j
143 142 oveq2d i = 1 st y G DProd j A i i S j = G DProd j A 1 st y 1 st y S j
144 143 19 18 fvmpt3i 1 st y I i I G DProd j A i i S j 1 st y = G DProd j A 1 st y 1 st y S j
145 135 144 syl φ x A y A x y i I G DProd j A i i S j 1 st y = G DProd j A 1 st y 1 st y S j
146 145 fveq2d φ x A y A x y Cntz G i I G DProd j A i i S j 1 st y = Cntz G G DProd j A 1 st y 1 st y S j
147 eqid Base G = Base G
148 147 dprdssv G DProd j A 1 st y 1 st y S j Base G
149 142 breq2d i = 1 st y G dom DProd j A i i S j G dom DProd j A 1 st y 1 st y S j
150 47 adantr φ x A y A x y i I G dom DProd j A i i S j
151 149 150 135 rspcdva φ x A y A x y G dom DProd j A 1 st y 1 st y S j
152 112 111 dmmpti dom j A 1 st y 1 st y S j = A 1 st y
153 152 a1i φ x A y A x y dom j A 1 st y 1 st y S j = A 1 st y
154 151 153 81 dprdub φ x A y A x y j A 1 st y 1 st y S j 2 nd y G DProd j A 1 st y 1 st y S j
155 116 154 eqsstrrd φ x A y A x y S y G DProd j A 1 st y 1 st y S j
156 147 7 cntz2ss G DProd j A 1 st y 1 st y S j Base G S y G DProd j A 1 st y 1 st y S j Cntz G G DProd j A 1 st y 1 st y S j Cntz G S y
157 148 155 156 sylancr φ x A y A x y Cntz G G DProd j A 1 st y 1 st y S j Cntz G S y
158 146 157 eqsstrd φ x A y A x y Cntz G i I G DProd j A i i S j 1 st y Cntz G S y
159 158 adantr φ x A y A x y 1 st x 1 st y Cntz G i I G DProd j A i i S j 1 st y Cntz G S y
160 138 159 sstrd φ x A y A x y 1 st x 1 st y i I G DProd j A i i S j 1 st x Cntz G S y
161 127 160 sstrd φ x A y A x y 1 st x 1 st y S x Cntz G S y
162 120 161 pm2.61dane φ x A y A x y S x Cntz G S y
163 10 adantr φ x A G Grp
164 147 subgacs G Grp SubGrp G ACS Base G
165 acsmre SubGrp G ACS Base G SubGrp G Moore Base G
166 163 164 165 3syl φ x A SubGrp G Moore Base G
167 16 adantr φ x A A I = A
168 undif2 1 st x I 1 st x = 1 st x I
169 52 snssd φ x A 1 st x I
170 ssequn1 1 st x I 1 st x I = I
171 169 170 sylib φ x A 1 st x I = I
172 168 171 eqtr2id φ x A I = 1 st x I 1 st x
173 172 reseq2d φ x A A I = A 1 st x I 1 st x
174 167 173 eqtr3d φ x A A = A 1 st x I 1 st x
175 resundi A 1 st x I 1 st x = A 1 st x A I 1 st x
176 174 175 eqtrdi φ x A A = A 1 st x A I 1 st x
177 176 difeq1d φ x A A x = A 1 st x A I 1 st x x
178 difundir A 1 st x A I 1 st x x = A 1 st x x A I 1 st x x
179 177 178 eqtrdi φ x A A x = A 1 st x x A I 1 st x x
180 neirr ¬ 1 st x 1 st x
181 61 eleq1d φ x A x A I 1 st x 1 st x 2 nd x A I 1 st x
182 df-br 1 st x A I 1 st x 2 nd x 1 st x 2 nd x A I 1 st x
183 92 brresi 1 st x A I 1 st x 2 nd x 1 st x I 1 st x 1 st x A 2 nd x
184 183 simplbi 1 st x A I 1 st x 2 nd x 1 st x I 1 st x
185 eldifsni 1 st x I 1 st x 1 st x 1 st x
186 184 185 syl 1 st x A I 1 st x 2 nd x 1 st x 1 st x
187 182 186 sylbir 1 st x 2 nd x A I 1 st x 1 st x 1 st x
188 181 187 syl6bi φ x A x A I 1 st x 1 st x 1 st x
189 180 188 mtoi φ x A ¬ x A I 1 st x
190 disjsn A I 1 st x x = ¬ x A I 1 st x
191 189 190 sylibr φ x A A I 1 st x x =
192 disj3 A I 1 st x x = A I 1 st x = A I 1 st x x
193 191 192 sylib φ x A A I 1 st x = A I 1 st x x
194 193 eqcomd φ x A A I 1 st x x = A I 1 st x
195 194 uneq2d φ x A A 1 st x x A I 1 st x x = A 1 st x x A I 1 st x
196 179 195 eqtrd φ x A A x = A 1 st x x A I 1 st x
197 196 imaeq2d φ x A S A x = S A 1 st x x A I 1 st x
198 imaundi S A 1 st x x A I 1 st x = S A 1 st x x S A I 1 st x
199 197 198 eqtrdi φ x A S A x = S A 1 st x x S A I 1 st x
200 199 unieqd φ x A S A x = S A 1 st x x S A I 1 st x
201 uniun S A 1 st x x S A I 1 st x = S A 1 st x x S A I 1 st x
202 200 201 eqtrdi φ x A S A x = S A 1 st x x S A I 1 st x
203 imassrn S A 1 st x x ran S
204 2 frnd φ ran S SubGrp G
205 204 adantr φ x A ran S SubGrp G
206 mresspw SubGrp G Moore Base G SubGrp G 𝒫 Base G
207 166 206 syl φ x A SubGrp G 𝒫 Base G
208 205 207 sstrd φ x A ran S 𝒫 Base G
209 203 208 sstrid φ x A S A 1 st x x 𝒫 Base G
210 sspwuni S A 1 st x x 𝒫 Base G S A 1 st x x Base G
211 209 210 sylib φ x A S A 1 st x x Base G
212 166 6 211 mrcssidd φ x A S A 1 st x x K S A 1 st x x
213 imassrn S A I 1 st x ran S
214 213 208 sstrid φ x A S A I 1 st x 𝒫 Base G
215 sspwuni S A I 1 st x 𝒫 Base G S A I 1 st x Base G
216 214 215 sylib φ x A S A I 1 st x Base G
217 166 6 216 mrcssidd φ x A S A I 1 st x K S A I 1 st x
218 unss12 S A 1 st x x K S A 1 st x x S A I 1 st x K S A I 1 st x S A 1 st x x S A I 1 st x K S A 1 st x x K S A I 1 st x
219 212 217 218 syl2anc φ x A S A 1 st x x S A I 1 st x K S A 1 st x x K S A I 1 st x
220 202 219 eqsstrd φ x A S A x K S A 1 st x x K S A I 1 st x
221 6 mrccl SubGrp G Moore Base G S A 1 st x x Base G K S A 1 st x x SubGrp G
222 166 211 221 syl2anc φ x A K S A 1 st x x SubGrp G
223 6 mrccl SubGrp G Moore Base G S A I 1 st x Base G K S A I 1 st x SubGrp G
224 166 216 223 syl2anc φ x A K S A I 1 st x SubGrp G
225 eqid LSSum G = LSSum G
226 225 lsmunss K S A 1 st x x SubGrp G K S A I 1 st x SubGrp G K S A 1 st x x K S A I 1 st x K S A 1 st x x LSSum G K S A I 1 st x
227 222 224 226 syl2anc φ x A K S A 1 st x x K S A I 1 st x K S A 1 st x x LSSum G K S A I 1 st x
228 220 227 sstrd φ x A S A x K S A 1 st x x LSSum G K S A I 1 st x
229 difss A 1 st x x A 1 st x
230 ressn A 1 st x = 1 st x × A 1 st x
231 229 230 sseqtri A 1 st x x 1 st x × A 1 st x
232 imass2 A 1 st x x 1 st x × A 1 st x S A 1 st x x S 1 st x × A 1 st x
233 231 232 ax-mp S A 1 st x x S 1 st x × A 1 st x
234 ovex 1 st x S i V
235 oveq2 j = i 1 st x S j = 1 st x S i
236 57 235 elrnmpt1s i A 1 st x 1 st x S i V 1 st x S i ran j A 1 st x 1 st x S j
237 234 236 mpan2 i A 1 st x 1 st x S i ran j A 1 st x 1 st x S j
238 237 rgen i A 1 st x 1 st x S i ran j A 1 st x 1 st x S j
239 238 a1i φ x A i A 1 st x 1 st x S i ran j A 1 st x 1 st x S j
240 oveq1 y = 1 st x y S i = 1 st x S i
241 240 eleq1d y = 1 st x y S i ran j A 1 st x 1 st x S j 1 st x S i ran j A 1 st x 1 st x S j
242 241 ralbidv y = 1 st x i A 1 st x y S i ran j A 1 st x 1 st x S j i A 1 st x 1 st x S i ran j A 1 st x 1 st x S j
243 91 242 ralsn y 1 st x i A 1 st x y S i ran j A 1 st x 1 st x S j i A 1 st x 1 st x S i ran j A 1 st x 1 st x S j
244 239 243 sylibr φ x A y 1 st x i A 1 st x y S i ran j A 1 st x 1 st x S j
245 2 adantr φ x A S : A SubGrp G
246 245 ffund φ x A Fun S
247 resss A 1 st x A
248 230 247 eqsstrri 1 st x × A 1 st x A
249 245 fdmd φ x A dom S = A
250 248 249 sseqtrrid φ x A 1 st x × A 1 st x dom S
251 funimassov Fun S 1 st x × A 1 st x dom S S 1 st x × A 1 st x ran j A 1 st x 1 st x S j y 1 st x i A 1 st x y S i ran j A 1 st x 1 st x S j
252 246 250 251 syl2anc φ x A S 1 st x × A 1 st x ran j A 1 st x 1 st x S j y 1 st x i A 1 st x y S i ran j A 1 st x 1 st x S j
253 244 252 mpbird φ x A S 1 st x × A 1 st x ran j A 1 st x 1 st x S j
254 233 253 sstrid φ x A S A 1 st x x ran j A 1 st x 1 st x S j
255 254 unissd φ x A S A 1 st x x ran j A 1 st x 1 st x S j
256 df-ov 1 st x S j = S 1 st x j
257 2 ad2antrr φ x A j A 1 st x S : A SubGrp G
258 elrelimasn Rel A j A 1 st x 1 st x A j
259 66 258 syl φ x A j A 1 st x 1 st x A j
260 259 biimpa φ x A j A 1 st x 1 st x A j
261 df-br 1 st x A j 1 st x j A
262 260 261 sylib φ x A j A 1 st x 1 st x j A
263 257 262 ffvelrnd φ x A j A 1 st x S 1 st x j SubGrp G
264 256 263 eqeltrid φ x A j A 1 st x 1 st x S j SubGrp G
265 264 fmpttd φ x A j A 1 st x 1 st x S j : A 1 st x SubGrp G
266 265 frnd φ x A ran j A 1 st x 1 st x S j SubGrp G
267 266 207 sstrd φ x A ran j A 1 st x 1 st x S j 𝒫 Base G
268 sspwuni ran j A 1 st x 1 st x S j 𝒫 Base G ran j A 1 st x 1 st x S j Base G
269 267 268 sylib φ x A ran j A 1 st x 1 st x S j Base G
270 166 6 255 269 mrcssd φ x A K S A 1 st x x K ran j A 1 st x 1 st x S j
271 6 dprdspan G dom DProd j A 1 st x 1 st x S j G DProd j A 1 st x 1 st x S j = K ran j A 1 st x 1 st x S j
272 53 271 syl φ x A G DProd j A 1 st x 1 st x S j = K ran j A 1 st x 1 st x S j
273 270 272 sseqtrrd φ x A K S A 1 st x x G DProd j A 1 st x 1 st x S j
274 18 19 fnmpti i I G DProd j A i i S j Fn I
275 fnressn i I G DProd j A i i S j Fn I 1 st x I i I G DProd j A i i S j 1 st x = 1 st x i I G DProd j A i i S j 1 st x
276 274 52 275 sylancr φ x A i I G DProd j A i i S j 1 st x = 1 st x i I G DProd j A i i S j 1 st x
277 124 opeq2d φ x A 1 st x i I G DProd j A i i S j 1 st x = 1 st x G DProd j A 1 st x 1 st x S j
278 277 sneqd φ x A 1 st x i I G DProd j A i i S j 1 st x = 1 st x G DProd j A 1 st x 1 st x S j
279 276 278 eqtrd φ x A i I G DProd j A i i S j 1 st x = 1 st x G DProd j A 1 st x 1 st x S j
280 279 oveq2d φ x A G DProd i I G DProd j A i i S j 1 st x = G DProd 1 st x G DProd j A 1 st x 1 st x S j
281 dprdsubg G dom DProd j A 1 st x 1 st x S j G DProd j A 1 st x 1 st x S j SubGrp G
282 53 281 syl φ x A G DProd j A 1 st x 1 st x S j SubGrp G
283 dprdsn 1 st x I G DProd j A 1 st x 1 st x S j SubGrp G G dom DProd 1 st x G DProd j A 1 st x 1 st x S j G DProd 1 st x G DProd j A 1 st x 1 st x S j = G DProd j A 1 st x 1 st x S j
284 52 282 283 syl2anc φ x A G dom DProd 1 st x G DProd j A 1 st x 1 st x S j G DProd 1 st x G DProd j A 1 st x 1 st x S j = G DProd j A 1 st x 1 st x S j
285 284 simprd φ x A G DProd 1 st x G DProd j A 1 st x 1 st x S j = G DProd j A 1 st x 1 st x S j
286 280 285 eqtrd φ x A G DProd i I G DProd j A i i S j 1 st x = G DProd j A 1 st x 1 st x S j
287 5 adantr φ x A G dom DProd i I G DProd j A i i S j
288 20 a1i φ x A dom i I G DProd j A i i S j = I
289 difss I 1 st x I
290 289 a1i φ x A I 1 st x I
291 disjdif 1 st x I 1 st x =
292 291 a1i φ x A 1 st x I 1 st x =
293 287 288 169 290 292 7 dprdcntz2 φ x A G DProd i I G DProd j A i i S j 1 st x Cntz G G DProd i I G DProd j A i i S j I 1 st x
294 286 293 eqsstrrd φ x A G DProd j A 1 st x 1 st x S j Cntz G G DProd i I G DProd j A i i S j I 1 st x
295 4 adantlr φ x A i I G dom DProd j A i i S j
296 66 245 49 295 287 6 290 dprd2dlem1 φ x A K S A I 1 st x = G DProd i I 1 st x G DProd j A i i S j
297 resmpt I 1 st x I i I G DProd j A i i S j I 1 st x = i I 1 st x G DProd j A i i S j
298 289 297 ax-mp i I G DProd j A i i S j I 1 st x = i I 1 st x G DProd j A i i S j
299 298 oveq2i G DProd i I G DProd j A i i S j I 1 st x = G DProd i I 1 st x G DProd j A i i S j
300 296 299 eqtr4di φ x A K S A I 1 st x = G DProd i I G DProd j A i i S j I 1 st x
301 300 fveq2d φ x A Cntz G K S A I 1 st x = Cntz G G DProd i I G DProd j A i i S j I 1 st x
302 294 301 sseqtrrd φ x A G DProd j A 1 st x 1 st x S j Cntz G K S A I 1 st x
303 273 302 sstrd φ x A K S A 1 st x x Cntz G K S A I 1 st x
304 225 7 lsmsubg K S A 1 st x x SubGrp G K S A I 1 st x SubGrp G K S A 1 st x x Cntz G K S A I 1 st x K S A 1 st x x LSSum G K S A I 1 st x SubGrp G
305 222 224 303 304 syl3anc φ x A K S A 1 st x x LSSum G K S A I 1 st x SubGrp G
306 6 mrcsscl SubGrp G Moore Base G S A x K S A 1 st x x LSSum G K S A I 1 st x K S A 1 st x x LSSum G K S A I 1 st x SubGrp G K S A x K S A 1 st x x LSSum G K S A I 1 st x
307 166 228 305 306 syl3anc φ x A K S A x K S A 1 st x x LSSum G K S A I 1 st x
308 sslin K S A x K S A 1 st x x LSSum G K S A I 1 st x S x K S A x S x K S A 1 st x x LSSum G K S A I 1 st x
309 307 308 syl φ x A S x K S A x S x K S A 1 st x x LSSum G K S A I 1 st x
310 2 ffvelrnda φ x A S x SubGrp G
311 225 lsmlub K S A 1 st x x SubGrp G S x SubGrp G G DProd j A 1 st x 1 st x S j SubGrp G K S A 1 st x x G DProd j A 1 st x 1 st x S j S x G DProd j A 1 st x 1 st x S j K S A 1 st x x LSSum G S x G DProd j A 1 st x 1 st x S j
312 222 310 282 311 syl3anc φ x A K S A 1 st x x G DProd j A 1 st x 1 st x S j S x G DProd j A 1 st x 1 st x S j K S A 1 st x x LSSum G S x G DProd j A 1 st x 1 st x S j
313 273 121 312 mpbi2and φ x A K S A 1 st x x LSSum G S x G DProd j A 1 st x 1 st x S j
314 313 124 sseqtrrd φ x A K S A 1 st x x LSSum G S x i I G DProd j A i i S j 1 st x
315 287 288 290 dprdres φ x A G dom DProd i I G DProd j A i i S j I 1 st x G DProd i I G DProd j A i i S j I 1 st x G DProd i I G DProd j A i i S j
316 315 simpld φ x A G dom DProd i I G DProd j A i i S j I 1 st x
317 6 dprdspan G dom DProd i I G DProd j A i i S j I 1 st x G DProd i I G DProd j A i i S j I 1 st x = K ran i I G DProd j A i i S j I 1 st x
318 316 317 syl φ x A G DProd i I G DProd j A i i S j I 1 st x = K ran i I G DProd j A i i S j I 1 st x
319 df-ima i I G DProd j A i i S j I 1 st x = ran i I G DProd j A i i S j I 1 st x
320 319 unieqi i I G DProd j A i i S j I 1 st x = ran i I G DProd j A i i S j I 1 st x
321 320 fveq2i K i I G DProd j A i i S j I 1 st x = K ran i I G DProd j A i i S j I 1 st x
322 318 321 eqtr4di φ x A G DProd i I G DProd j A i i S j I 1 st x = K i I G DProd j A i i S j I 1 st x
323 300 322 eqtrd φ x A K S A I 1 st x = K i I G DProd j A i i S j I 1 st x
324 eqimss K S A I 1 st x = K i I G DProd j A i i S j I 1 st x K S A I 1 st x K i I G DProd j A i i S j I 1 st x
325 323 324 syl φ x A K S A I 1 st x K i I G DProd j A i i S j I 1 st x
326 ss2in K S A 1 st x x LSSum G S x i I G DProd j A i i S j 1 st x K S A I 1 st x K i I G DProd j A i i S j I 1 st x K S A 1 st x x LSSum G S x K S A I 1 st x i I G DProd j A i i S j 1 st x K i I G DProd j A i i S j I 1 st x
327 314 325 326 syl2anc φ x A K S A 1 st x x LSSum G S x K S A I 1 st x i I G DProd j A i i S j 1 st x K i I G DProd j A i i S j I 1 st x
328 287 288 52 8 6 dprddisj φ x A i I G DProd j A i i S j 1 st x K i I G DProd j A i i S j I 1 st x = 0 G
329 327 328 sseqtrd φ x A K S A 1 st x x LSSum G S x K S A I 1 st x 0 G
330 225 lsmub2 K S A 1 st x x SubGrp G S x SubGrp G S x K S A 1 st x x LSSum G S x
331 222 310 330 syl2anc φ x A S x K S A 1 st x x LSSum G S x
332 8 subg0cl S x SubGrp G 0 G S x
333 310 332 syl φ x A 0 G S x
334 331 333 sseldd φ x A 0 G K S A 1 st x x LSSum G S x
335 8 subg0cl K S A I 1 st x SubGrp G 0 G K S A I 1 st x
336 224 335 syl φ x A 0 G K S A I 1 st x
337 334 336 elind φ x A 0 G K S A 1 st x x LSSum G S x K S A I 1 st x
338 337 snssd φ x A 0 G K S A 1 st x x LSSum G S x K S A I 1 st x
339 329 338 eqssd φ x A K S A 1 st x x LSSum G S x K S A I 1 st x = 0 G
340 incom K S A 1 st x x S x = S x K S A 1 st x x
341 69 101 syl φ x A j A 1 st x 1 st x S j 2 nd x = 1 st x S 2 nd x
342 61 fveq2d φ x A S x = S 1 st x 2 nd x
343 99 341 342 3eqtr4a φ x A j A 1 st x 1 st x S j 2 nd x = S x
344 eqimss2 j A 1 st x 1 st x S j 2 nd x = S x S x j A 1 st x 1 st x S j 2 nd x
345 343 344 syl φ x A S x j A 1 st x 1 st x S j 2 nd x
346 eldifsn y A 1 st x x y A 1 st x y x
347 1 ad2antrr φ x A y A 1 st x y x Rel A
348 simprl φ x A y A 1 st x y x y A 1 st x
349 247 348 sseldi φ x A y A 1 st x y x y A
350 347 349 74 syl2anc φ x A y A 1 st x y x y = 1 st y 2 nd y
351 350 fveq2d φ x A y A 1 st x y x S y = S 1 st y 2 nd y
352 351 109 eqtr4di φ x A y A 1 st x y x S y = 1 st y S 2 nd y
353 350 348 eqeltrrd φ x A y A 1 st x y x 1 st y 2 nd y A 1 st x
354 fvex 2 nd y V
355 354 opelresi 1 st y 2 nd y A 1 st x 1 st y 1 st x 1 st y 2 nd y A
356 355 simplbi 1 st y 2 nd y A 1 st x 1 st y 1 st x
357 353 356 syl φ x A y A 1 st x y x 1 st y 1 st x
358 elsni 1 st y 1 st x 1 st y = 1 st x
359 357 358 syl φ x A y A 1 st x y x 1 st y = 1 st x
360 359 oveq1d φ x A y A 1 st x y x 1 st y S 2 nd y = 1 st x S 2 nd y
361 352 360 eqtrd φ x A y A 1 st x y x S y = 1 st x S 2 nd y
362 348 230 eleqtrdi φ x A y A 1 st x y x y 1 st x × A 1 st x
363 xp2nd y 1 st x × A 1 st x 2 nd y A 1 st x
364 362 363 syl φ x A y A 1 st x y x 2 nd y A 1 st x
365 simprr φ x A y A 1 st x y x y x
366 61 adantr φ x A y A 1 st x y x x = 1 st x 2 nd x
367 350 366 eqeq12d φ x A y A 1 st x y x y = x 1 st y 2 nd y = 1 st x 2 nd x
368 fvex 1 st y V
369 368 354 opth 1 st y 2 nd y = 1 st x 2 nd x 1 st y = 1 st x 2 nd y = 2 nd x
370 369 baib 1 st y = 1 st x 1 st y 2 nd y = 1 st x 2 nd x 2 nd y = 2 nd x
371 359 370 syl φ x A y A 1 st x y x 1 st y 2 nd y = 1 st x 2 nd x 2 nd y = 2 nd x
372 367 371 bitrd φ x A y A 1 st x y x y = x 2 nd y = 2 nd x
373 372 necon3bid φ x A y A 1 st x y x y x 2 nd y 2 nd x
374 365 373 mpbid φ x A y A 1 st x y x 2 nd y 2 nd x
375 eldifsn 2 nd y A 1 st x 2 nd x 2 nd y A 1 st x 2 nd y 2 nd x
376 364 374 375 sylanbrc φ x A y A 1 st x y x 2 nd y A 1 st x 2 nd x
377 ovex 1 st x S 2 nd y V
378 difss A 1 st x 2 nd x A 1 st x
379 resmpt A 1 st x 2 nd x A 1 st x j A 1 st x 1 st x S j A 1 st x 2 nd x = j A 1 st x 2 nd x 1 st x S j
380 378 379 ax-mp j A 1 st x 1 st x S j A 1 st x 2 nd x = j A 1 st x 2 nd x 1 st x S j
381 oveq2 j = 2 nd y 1 st x S j = 1 st x S 2 nd y
382 380 381 elrnmpt1s 2 nd y A 1 st x 2 nd x 1 st x S 2 nd y V 1 st x S 2 nd y ran j A 1 st x 1 st x S j A 1 st x 2 nd x
383 376 377 382 sylancl φ x A y A 1 st x y x 1 st x S 2 nd y ran j A 1 st x 1 st x S j A 1 st x 2 nd x
384 361 383 eqeltrd φ x A y A 1 st x y x S y ran j A 1 st x 1 st x S j A 1 st x 2 nd x
385 df-ima j A 1 st x 1 st x S j A 1 st x 2 nd x = ran j A 1 st x 1 st x S j A 1 st x 2 nd x
386 384 385 eleqtrrdi φ x A y A 1 st x y x S y j A 1 st x 1 st x S j A 1 st x 2 nd x
387 386 ex φ x A y A 1 st x y x S y j A 1 st x 1 st x S j A 1 st x 2 nd x
388 346 387 syl5bi φ x A y A 1 st x x S y j A 1 st x 1 st x S j A 1 st x 2 nd x
389 388 ralrimiv φ x A y A 1 st x x S y j A 1 st x 1 st x S j A 1 st x 2 nd x
390 231 250 sstrid φ x A A 1 st x x dom S
391 funimass4 Fun S A 1 st x x dom S S A 1 st x x j A 1 st x 1 st x S j A 1 st x 2 nd x y A 1 st x x S y j A 1 st x 1 st x S j A 1 st x 2 nd x
392 246 390 391 syl2anc φ x A S A 1 st x x j A 1 st x 1 st x S j A 1 st x 2 nd x y A 1 st x x S y j A 1 st x 1 st x S j A 1 st x 2 nd x
393 389 392 mpbird φ x A S A 1 st x x j A 1 st x 1 st x S j A 1 st x 2 nd x
394 393 unissd φ x A S A 1 st x x j A 1 st x 1 st x S j A 1 st x 2 nd x
395 imassrn j A 1 st x 1 st x S j A 1 st x 2 nd x ran j A 1 st x 1 st x S j
396 395 267 sstrid φ x A j A 1 st x 1 st x S j A 1 st x 2 nd x 𝒫 Base G
397 sspwuni j A 1 st x 1 st x S j A 1 st x 2 nd x 𝒫 Base G j A 1 st x 1 st x S j A 1 st x 2 nd x Base G
398 396 397 sylib φ x A j A 1 st x 1 st x S j A 1 st x 2 nd x Base G
399 166 6 394 398 mrcssd φ x A K S A 1 st x x K j A 1 st x 1 st x S j A 1 st x 2 nd x
400 ss2in S x j A 1 st x 1 st x S j 2 nd x K S A 1 st x x K j A 1 st x 1 st x S j A 1 st x 2 nd x S x K S A 1 st x x j A 1 st x 1 st x S j 2 nd x K j A 1 st x 1 st x S j A 1 st x 2 nd x
401 345 399 400 syl2anc φ x A S x K S A 1 st x x j A 1 st x 1 st x S j 2 nd x K j A 1 st x 1 st x S j A 1 st x 2 nd x
402 58 a1i φ x A dom j A 1 st x 1 st x S j = A 1 st x
403 53 402 69 8 6 dprddisj φ x A j A 1 st x 1 st x S j 2 nd x K j A 1 st x 1 st x S j A 1 st x 2 nd x = 0 G
404 401 403 sseqtrd φ x A S x K S A 1 st x x 0 G
405 8 subg0cl K S A 1 st x x SubGrp G 0 G K S A 1 st x x
406 222 405 syl φ x A 0 G K S A 1 st x x
407 333 406 elind φ x A 0 G S x K S A 1 st x x
408 407 snssd φ x A 0 G S x K S A 1 st x x
409 404 408 eqssd φ x A S x K S A 1 st x x = 0 G
410 340 409 syl5eq φ x A K S A 1 st x x S x = 0 G
411 225 222 310 224 8 339 410 lsmdisj2 φ x A S x K S A 1 st x x LSSum G K S A I 1 st x = 0 G
412 309 411 sseqtrd φ x A S x K S A x 0 G
413 7 8 6 10 41 2 162 412 dmdprdd φ G dom DProd S