Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  dprd2da Structured version   Unicode version

Theorem dprd2da 15592
 Description: The direct product of a collection of direct products. (Contributed by Mario Carneiro, 26-Apr-2016.)
Hypotheses
Ref Expression
dprd2d.1
dprd2d.2 SubGrp
dprd2d.3
dprd2d.4 DProd
dprd2d.5 DProd DProd
dprd2d.k mrClsSubGrp
Assertion
Ref Expression
dprd2da DProd
Distinct variable groups:   ,,   ,,   ,   ,   ,,   ,,
Allowed substitution hints:   ()   ()

Proof of Theorem dprd2da
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 eqid 2435 . 2 Cntz Cntz
2 eqid 2435 . 2
3 dprd2d.k . 2 mrClsSubGrp
4 dprd2d.5 . . 3 DProd DProd
5 dprdgrp 15555 . . 3 DProd DProd
64, 5syl 16 . 2
7 resiun2 5158 . . . . 5
8 iunid 4138 . . . . . 6
98reseq2i 5135 . . . . 5
107, 9eqtr3i 2457 . . . 4
11 dprd2d.1 . . . . 5
12 dprd2d.3 . . . . 5
13 relssres 5175 . . . . 5
1411, 12, 13syl2anc 643 . . . 4
1510, 14syl5eq 2479 . . 3
16 ovex 6098 . . . . . 6 DProd
17 eqid 2435 . . . . . 6 DProd DProd
1816, 17dmmpti 5566 . . . . 5 DProd
19 reldmdprd 15550 . . . . . . 7 DProd
2019brrelex2i 4911 . . . . . 6 DProd DProd DProd
21 dmexg 5122 . . . . . 6 DProd DProd
224, 20, 213syl 19 . . . . 5 DProd
2318, 22syl5eqelr 2520 . . . 4
24 ressn 5400 . . . . . 6
25 snex 4397 . . . . . . 7
26 ovex 6098 . . . . . . . . 9
27 eqid 2435 . . . . . . . . 9
2826, 27dmmpti 5566 . . . . . . . 8
29 dprd2d.4 . . . . . . . . 9 DProd
3019brrelex2i 4911 . . . . . . . . 9 DProd
31 dmexg 5122 . . . . . . . . 9
3229, 30, 313syl 19 . . . . . . . 8
3328, 32syl5eqelr 2520 . . . . . . 7
34 xpexg 4981 . . . . . . 7
3525, 33, 34sylancr 645 . . . . . 6
3624, 35syl5eqel 2519 . . . . 5
3736ralrimiva 2781 . . . 4
38 iunexg 5979 . . . 4
3923, 37, 38syl2anc 643 . . 3
4015, 39eqeltrrd 2510 . 2
41 dprd2d.2 . 2 SubGrp
4212adantr 452 . . . . . . . . 9
43 1stdm 6386 . . . . . . . . . 10
4411, 43sylan 458 . . . . . . . . 9
4542, 44sseldd 3341 . . . . . . . 8
4629ralrimiva 2781 . . . . . . . . 9 DProd
4746adantr 452 . . . . . . . 8 DProd
48 sneq 3817 . . . . . . . . . . . 12
4948imaeq2d 5195 . . . . . . . . . . 11
50 oveq1 6080 . . . . . . . . . . 11
5149, 50mpteq12dv 4279 . . . . . . . . . 10
5251breq2d 4216 . . . . . . . . 9 DProd DProd
5352rspcv 3040 . . . . . . . 8 DProd DProd
5445, 47, 53sylc 58 . . . . . . 7 DProd
55543ad2antr1 1122 . . . . . 6 DProd
5655adantr 452 . . . . 5 DProd
57 ovex 6098 . . . . . . 7
58 eqid 2435 . . . . . . 7
5957, 58dmmpti 5566 . . . . . 6
6059a1i 11 . . . . 5
61 1st2nd 6385 . . . . . . . . . . 11
6211, 61sylan 458 . . . . . . . . . 10
63 simpr 448 . . . . . . . . . 10
6462, 63eqeltrrd 2510 . . . . . . . . 9
65 df-br 4205 . . . . . . . . 9
6664, 65sylibr 204 . . . . . . . 8
6711adantr 452 . . . . . . . . 9
68 elrelimasn 5220 . . . . . . . . 9
6967, 68syl 16 . . . . . . . 8
7066, 69mpbird 224 . . . . . . 7
71703ad2antr1 1122 . . . . . 6
7271adantr 452 . . . . 5
7311adantr 452 . . . . . . . . . . 11
74 simpr2 964 . . . . . . . . . . 11
75 1st2nd 6385 . . . . . . . . . . 11
7673, 74, 75syl2anc 643 . . . . . . . . . 10
7776, 74eqeltrrd 2510 . . . . . . . . 9
78 df-br 4205 . . . . . . . . 9
7977, 78sylibr 204 . . . . . . . 8
80 elrelimasn 5220 . . . . . . . . 9
8173, 80syl 16 . . . . . . . 8
8279, 81mpbird 224 . . . . . . 7
8382adantr 452 . . . . . 6
84 simpr 448 . . . . . . . 8
8584sneqd 3819 . . . . . . 7
8685imaeq2d 5195 . . . . . 6
8783, 86eleqtrrd 2512 . . . . 5
88 simplr3 1001 . . . . . 6
89 simpr1 963 . . . . . . . . . . 11
9073, 89, 61syl2anc 643 . . . . . . . . . 10
9190, 76eqeq12d 2449 . . . . . . . . 9
92 fvex 5734 . . . . . . . . . 10
93 fvex 5734 . . . . . . . . . 10
9492, 93opth 4427 . . . . . . . . 9
9591, 94syl6bb 253 . . . . . . . 8
9695baibd 876 . . . . . . 7
9796necon3bid 2633 . . . . . 6
9888, 97mpbid 202 . . . . 5
9956, 60, 72, 87, 98, 1dprdcntz 15558 . . . 4 Cntz
100 df-ov 6076 . . . . . 6
101 oveq2 6081 . . . . . . . 8
102101, 58, 57fvmpt3i 5801 . . . . . . 7
10371, 102syl 16 . . . . . 6
10490fveq2d 5724 . . . . . 6
105100, 103, 1043eqtr4a 2493 . . . . 5
106105adantr 452 . . . 4
10784oveq1d 6088 . . . . . . . 8
10886, 107mpteq12dv 4279 . . . . . . 7
109108fveq1d 5722 . . . . . 6
110 df-ov 6076 . . . . . . . 8
111 oveq2 6081 . . . . . . . . . 10
112 eqid 2435 . . . . . . . . . 10
113 ovex 6098 . . . . . . . . . 10
114111, 112, 113fvmpt3i 5801 . . . . . . . . 9
11582, 114syl 16 . . . . . . . 8
11676fveq2d 5724 . . . . . . . 8
117110, 115, 1163eqtr4a 2493 . . . . . . 7
118117adantr 452 . . . . . 6
119109, 118eqtrd 2467 . . . . 5
120119fveq2d 5724 . . . 4 Cntz Cntz
12199, 106, 1203sstr3d 3382 . . 3 Cntz
12211, 41, 12, 29, 4, 3dprd2dlem2 15590 . . . . . . 7 DProd
12351oveq2d 6089 . . . . . . . . 9 DProd DProd
124123, 17, 16fvmpt3i 5801 . . . . . . . 8 DProd DProd
12545, 124syl 16 . . . . . . 7 DProd DProd
126122, 125sseqtr4d 3377 . . . . . 6 DProd
1271263ad2antr1 1122 . . . . 5 DProd
128127adantr 452 . . . 4 DProd
1294ad2antrr 707 . . . . . 6 DProd DProd
13018a1i 11 . . . . . 6 DProd
131453ad2antr1 1122 . . . . . . 7
132131adantr 452 . . . . . 6
13312adantr 452 . . . . . . . 8
134 1stdm 6386 . . . . . . . . 9
13573, 74, 134syl2anc 643 . . . . . . . 8
136133, 135sseldd 3341 . . . . . . 7
137136adantr 452 . . . . . 6
138 simpr 448 . . . . . 6
139129, 130, 132, 137, 138, 1dprdcntz 15558 . . . . 5 DProd Cntz DProd
140 sneq 3817 . . . . . . . . . . . . 13
141140imaeq2d 5195 . . . . . . . . . . . 12
142 oveq1 6080 . . . . . . . . . . . 12
143141, 142mpteq12dv 4279 . . . . . . . . . . 11
144143oveq2d 6089 . . . . . . . . . 10 DProd DProd
145144, 17, 16fvmpt3i 5801 . . . . . . . . 9 DProd DProd
146136, 145syl 16 . . . . . . . 8 DProd DProd
147146fveq2d 5724 . . . . . . 7 Cntz DProd Cntz DProd
148 eqid 2435 . . . . . . . . 9
149148dprdssv 15566 . . . . . . . 8 DProd
15046adantr 452 . . . . . . . . . . 11 DProd
151143breq2d 4216 . . . . . . . . . . . 12 DProd DProd
152151rspcv 3040 . . . . . . . . . . 11 DProd DProd
153136, 150, 152sylc 58 . . . . . . . . . 10 DProd
154113, 112dmmpti 5566 . . . . . . . . . . 11
155154a1i 11 . . . . . . . . . 10
156153, 155, 82dprdub 15575 . . . . . . . . 9 DProd
157117, 156eqsstr3d 3375 . . . . . . . 8 DProd
158148, 1cntz2ss 15123 . . . . . . . 8 DProd DProd Cntz DProd Cntz
159149, 157, 158sylancr 645 . . . . . . 7 Cntz DProd Cntz
160147, 159eqsstrd 3374 . . . . . 6 Cntz DProd Cntz
161160adantr 452 . . . . 5 Cntz DProd Cntz
162139, 161sstrd 3350 . . . 4 DProd Cntz
163128, 162sstrd 3350 . . 3 Cntz
164121, 163pm2.61dane 2676 . 2 Cntz
1656adantr 452 . . . . . 6
166148subgacs 14967 . . . . . 6 SubGrp ACS
167 acsmre 13869 . . . . . 6 SubGrp ACS SubGrp Moore
168165, 166, 1673syl 19 . . . . 5 SubGrp Moore
16914adantr 452 . . . . . . . . . . . . . . . 16
170 undif2 3696 . . . . . . . . . . . . . . . . . 18
17145snssd 3935 . . . . . . . . . . . . . . . . . . 19
172 ssequn1 3509 . . . . . . . . . . . . . . . . . . 19
173171, 172sylib 189 . . . . . . . . . . . . . . . . . 18
174170, 173syl5req 2480 . . . . . . . . . . . . . . . . 17
175174reseq2d 5138 . . . . . . . . . . . . . . . 16
176169, 175eqtr3d 2469 . . . . . . . . . . . . . . 15
177 resundi 5152 . . . . . . . . . . . . . . 15
178176, 177syl6eq 2483 . . . . . . . . . . . . . 14
179178difeq1d 3456 . . . . . . . . . . . . 13
180 difundir 3586 . . . . . . . . . . . . 13
181179, 180syl6eq 2483 . . . . . . . . . . . 12
182 neirr 2603 . . . . . . . . . . . . . . . . 17
18362eleq1d 2501 . . . . . . . . . . . . . . . . . 18
184 df-br 4205 . . . . . . . . . . . . . . . . . . 19
18593brres 5144 . . . . . . . . . . . . . . . . . . . . 21
186185simprbi 451 . . . . . . . . . . . . . . . . . . . 20
187 eldifsni 3920 . . . . . . . . . . . . . . . . . . . 20
188186, 187syl 16 . . . . . . . . . . . . . . . . . . 19
189184, 188sylbir 205 . . . . . . . . . . . . . . . . . 18
190183, 189syl6bi 220 . . . . . . . . . . . . . . . . 17
191182, 190mtoi 171 . . . . . . . . . . . . . . . 16
192 disjsn 3860 . . . . . . . . . . . . . . . 16
193191, 192sylibr 204 . . . . . . . . . . . . . . 15
194 disj3 3664 . . . . . . . . . . . . . . 15
195193, 194sylib 189 . . . . . . . . . . . . . 14
196195eqcomd 2440 . . . . . . . . . . . . 13
197196uneq2d 3493 . . . . . . . . . . . 12
198181, 197eqtrd 2467 . . . . . . . . . . 11
199198imaeq2d 5195 . . . . . . . . . 10
200 imaundi 5276 . . . . . . . . . 10
201199, 200syl6eq 2483 . . . . . . . . 9
202201unieqd 4018 . . . . . . . 8
203 uniun 4026 . . . . . . . 8
204202, 203syl6eq 2483 . . . . . . 7
205 imassrn 5208 . . . . . . . . . . 11
206 frn 5589 . . . . . . . . . . . . . 14 SubGrp SubGrp
20741, 206syl 16 . . . . . . . . . . . . 13 SubGrp
208207adantr 452 . . . . . . . . . . . 12 SubGrp
209 mresspw 13809 . . . . . . . . . . . . 13 SubGrp Moore SubGrp
210168, 209syl 16 . . . . . . . . . . . 12 SubGrp
211208, 210sstrd 3350 . . . . . . . . . . 11
212205, 211syl5ss 3351 . . . . . . . . . 10
213 sspwuni 4168 . . . . . . . . . 10
214212, 213sylib 189 . . . . . . . . 9
215168, 3, 214mrcssidd 13842 . . . . . . . 8
216 imassrn 5208 . . . . . . . . . . 11
217216, 211syl5ss 3351 . . . . . . . . . 10
218 sspwuni 4168 . . . . . . . . . 10
219217, 218sylib 189 . . . . . . . . 9
220168, 3, 219mrcssidd 13842 . . . . . . . 8
221 unss12 3511 . . . . . . . 8
222215, 220, 221syl2anc 643 . . . . . . 7
223204, 222eqsstrd 3374 . . . . . 6
2243mrccl 13828 . . . . . . . 8 SubGrp Moore SubGrp
225168, 214, 224syl2anc 643 . . . . . . 7 SubGrp
2263mrccl 13828 . . . . . . . 8 SubGrp Moore SubGrp
227168, 219, 226syl2anc 643 . . . . . . 7 SubGrp
228 eqid 2435 . . . . . . . 8
229228lsmunss 15284 . . . . . . 7 SubGrp SubGrp
230225, 227, 229syl2anc 643 . . . . . 6
231223, 230sstrd 3350 . . . . 5
232 difss 3466 . . . . . . . . . . . . 13
233 ressn 5400 . . . . . . . . . . . . 13
234232, 233sseqtri 3372 . . . . . . . . . . . 12
235 imass2 5232 . . . . . . . . . . . 12
236234, 235ax-mp 8 . . . . . . . . . . 11
237 ovex 6098 . . . . . . . . . . . . . . . 16
238 oveq2 6081 . . . . . . . . . . . . . . . . 17
23958, 238elrnmpt1s 5110 . . . . . . . . . . . . . . . 16
240237, 239mpan2 653 . . . . . . . . . . . . . . 15
241240rgen 2763 . . . . . . . . . . . . . 14
242241a1i 11 . . . . . . . . . . . . 13
243 oveq1 6080 . . . . . . . . . . . . . . . 16
244243eleq1d 2501 . . . . . . . . . . . . . . 15
245244ralbidv 2717 . . . . . . . . . . . . . 14
24692, 245ralsn 3841 . . . . . . . . . . . . 13
247242, 246sylibr 204 . . . . . . . . . . . 12
24841adantr 452 . . . . . . . . . . . . . 14 SubGrp
249 ffun 5585 . . . . . . . . . . . . . 14 SubGrp
250248, 249syl 16 . . . . . . . . . . . . 13
251 resss 5162 . . . . . . . . . . . . . . 15
252233, 251eqsstr3i 3371 . . . . . . . . . . . . . 14
253 fdm 5587 . . . . . . . . . . . . . . 15 SubGrp
254248, 253syl 16 . . . . . . . . . . . . . 14
255252, 254syl5sseqr 3389 . . . . . . . . . . . . 13
256 funimassov 6215 . . . . . . . . . . . . 13
257250, 255, 256syl2anc 643 . . . . . . . . . . . 12
258247, 257mpbird 224 . . . . . . . . . . 11
259236, 258syl5ss 3351 . . . . . . . . . 10
260259unissd 4031 . . . . . . . . 9
261 df-ov 6076 . . . . . . . . . . . . . 14
26241ad2antrr 707 . . . . . . . . . . . . . . 15 SubGrp
263 elrelimasn 5220 . . . . . . . . . . . . . . . . . 18
26467, 263syl 16 . . . . . . . . . . . . . . . . 17
265264biimpa 471 . . . . . . . . . . . . . . . 16
266 df-br 4205 . . . . . . . . . . . . . . . 16
267265, 266sylib 189 . . . . . . . . . . . . . . 15
268262, 267ffvelrnd 5863 . . . . . . . . . . . . . 14 SubGrp
269261, 268syl5eqel 2519 . . . . . . . . . . . . 13 SubGrp
270269, 58fmptd 5885 . . . . . . . . . . . 12 SubGrp
271 frn 5589 . . . . . . . . . . . 12 SubGrp SubGrp
272270, 271syl 16 . . . . . . . . . . 11 SubGrp
273272, 210sstrd 3350 . . . . . . . . . 10
274 sspwuni 4168 . . . . . . . . . 10
275273, 274sylib 189 . . . . . . . . 9
276168, 3, 260, 275mrcssd 13841 . . . . . . . 8
2773dprdspan 15577 . . . . . . . . 9 DProd DProd
27854, 277syl 16 . . . . . . . 8 DProd
279276, 278sseqtr4d 3377 . . . . . . 7 DProd
28016, 17fnmpti 5565 . . . . . . . . . . . . 13 DProd
281 fnressn 5910 . . . . . . . . . . . . 13 DProd DProd DProd
282280, 45, 281sylancr 645 . . . . . . . . . . . 12 DProd DProd
283125opeq2d 3983 . . . . . . . . . . . . 13 DProd DProd
284283sneqd 3819 . . . . . . . . . . . 12 DProd DProd
285282, 284eqtrd 2467 . . . . . . . . . . 11 DProd DProd
286285oveq2d 6089 . . . . . . . . . 10 DProd DProd DProd DProd
287 dprdsubg 15574 . . . . . . . . . . . . 13 DProd DProd SubGrp
28854, 287syl 16 . . . . . . . . . . . 12 DProd SubGrp
289 dprdsn 15586 . . . . . . . . . . . 12 DProd SubGrp DProd DProd DProd DProd DProd
29045, 288, 289syl2anc 643 . . . . . . . . . . 11 DProd DProd DProd DProd DProd
291290simprd 450 . . . . . . . . . 10 DProd DProd DProd
292286, 291eqtrd 2467 . . . . . . . . 9 DProd DProd DProd
2934adantr 452 . . . . . . . . . 10 DProd DProd
29418a1i 11 . . . . . . . . . 10 DProd
295 difss 3466 . . . . . . . . . . 11
296295a1i 11 . . . . . . . . . 10
297 disjdif 3692 . . . . . . . . . . 11
298297a1i 11 . . . . . . . . . 10
299293, 294, 171, 296, 298, 1dprdcntz2 15588 . . . . . . . . 9 DProd DProd Cntz DProd DProd
300292, 299eqsstr3d 3375 . . . . . . . 8 DProd Cntz DProd DProd
30129adantlr 696 . . . . . . . . . . 11 DProd
30267, 248, 42, 301, 293, 3, 296dprd2dlem1 15591 . . . . . . . . . 10 DProd DProd
303 resmpt 5183 . . . . . . . . . . . 12 DProd DProd
304295, 303ax-mp 8 . . . . . . . . . . 11 DProd DProd
305304oveq2i 6084 . . . . . . . . . 10 DProd DProd DProd DProd
306302, 305syl6eqr 2485 . . . . . . . . 9 DProd DProd
307306fveq2d 5724 . . . . . . . 8 Cntz Cntz DProd DProd
308300, 307sseqtr4d 3377 . . . . . . 7 DProd Cntz
309279, 308sstrd 3350 . . . . . 6 Cntz
310228, 1lsmsubg 15280 . . . . . 6 SubGrp SubGrp Cntz SubGrp
311225, 227, 309, 310syl3anc 1184 . . . . 5 SubGrp
3123mrcsscl 13837 . . . . 5 SubGrp Moore SubGrp
313168, 231, 311, 312syl3anc 1184 . . . 4
314 sslin 3559 . . . 4
315313, 314syl 16 . . 3
31641ffvelrnda 5862 . . . 4 SubGrp
317228lsmlub 15289 . . . . . . . . . 10 SubGrp SubGrp DProd SubGrp DProd DProd DProd
318225, 316, 288, 317syl3anc 1184 . . . . . . . . 9