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

Theorem dprdvalOLD 17356
 Description: The domain of definition of the internal direct product, which states that is a family of subgroups that mutually commute and have trivial intersections. (Contributed by Mario Carneiro, 25-Apr-2016.) Obsolete version of dprdval 17354 as of 11-Jul-2019. Proof adapted to use the new definition df-dprd 17346. (New usage is discouraged.) (Proof modification is discouraged.)
Hypotheses
Ref Expression
dprdvalOLD.0
dprdvalOLD.w
Assertion
Ref Expression
dprdvalOLD DProd DProd g
Distinct variable groups:   ,,,   ,,,   ,,,
Allowed substitution hints:   (,,)   (,,)

Proof of Theorem dprdvalOLD
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 simpl 455 . 2 DProd DProd
2 reldmdprd 17348 . . . . . 6 DProd
32brrelex2i 4865 . . . . 5 DProd
43adantr 463 . . . 4 DProd
52brrelexi 4864 . . . . . 6 DProd
6 breq1 4398 . . . . . . . 8 DProd DProd
7 oveq1 6285 . . . . . . . . 9 DProd DProd
8 fveq2 5849 . . . . . . . . . . . . . . . . 17
9 dprdvalOLD.0 . . . . . . . . . . . . . . . . 17
108, 9syl6eqr 2461 . . . . . . . . . . . . . . . 16
1110sneqd 3984 . . . . . . . . . . . . . . 15
1211difeq2d 3561 . . . . . . . . . . . . . 14
1312imaeq2d 5157 . . . . . . . . . . . . 13
1413eleq1d 2471 . . . . . . . . . . . 12
1514rabbidv 3051 . . . . . . . . . . 11
16 oveq1 6285 . . . . . . . . . . 11 g g
1715, 16mpteq12dv 4473 . . . . . . . . . 10 g g
1817rneqd 5051 . . . . . . . . 9 g g
197, 18eqeq12d 2424 . . . . . . . 8 DProd g DProd g
206, 19imbi12d 318 . . . . . . 7 DProd DProd g DProd DProd g
21 df-br 4396 . . . . . . . . 9 DProd DProd
22 fvex 5859 . . . . . . . . . . . . . . . . . 18
2322rgenw 2765 . . . . . . . . . . . . . . . . 17
24 ixpexg 7531 . . . . . . . . . . . . . . . . 17
2523, 24ax-mp 5 . . . . . . . . . . . . . . . 16
2625rabex 4545 . . . . . . . . . . . . . . 15
2726mptex 6124 . . . . . . . . . . . . . 14 g
2827rnex 6718 . . . . . . . . . . . . 13 g
2928rgen2w 2766 . . . . . . . . . . . 12 SubGrp Cntz mrClsSubGrp g
30 df-dprd 17346 . . . . . . . . . . . . . 14 DProd SubGrp Cntz mrClsSubGrp finSupp g
31 eqid 2402 . . . . . . . . . . . . . . 15
32 eqid 2402 . . . . . . . . . . . . . . 15 SubGrp Cntz mrClsSubGrp SubGrp Cntz mrClsSubGrp
33 ixpfn 7513 . . . . . . . . . . . . . . . . . . . . . 22
34 fnfun 5659 . . . . . . . . . . . . . . . . . . . . . 22
3533, 34syl 17 . . . . . . . . . . . . . . . . . . . . 21
36 id 22 . . . . . . . . . . . . . . . . . . . . 21
37 fvex 5859 . . . . . . . . . . . . . . . . . . . . . 22
3837a1i 11 . . . . . . . . . . . . . . . . . . . . 21
3935, 36, 383jca 1177 . . . . . . . . . . . . . . . . . . . 20
40 funisfsupp 7868 . . . . . . . . . . . . . . . . . . . 20 finSupp supp
4139, 40syl 17 . . . . . . . . . . . . . . . . . . 19 finSupp supp
4236, 38jca 530 . . . . . . . . . . . . . . . . . . . . 21
43 suppimacnv 6913 . . . . . . . . . . . . . . . . . . . . 21 supp
4442, 43syl 17 . . . . . . . . . . . . . . . . . . . 20 supp
4544eleq1d 2471 . . . . . . . . . . . . . . . . . . 19 supp
4641, 45bitrd 253 . . . . . . . . . . . . . . . . . 18 finSupp
4746rabbiia 3048 . . . . . . . . . . . . . . . . 17 finSupp
48 eqid 2402 . . . . . . . . . . . . . . . . 17 g g
4947, 48mpteq12i 4479 . . . . . . . . . . . . . . . 16 finSupp g g
5049rneqi 5050 . . . . . . . . . . . . . . 15 finSupp g g
5131, 32, 50mpt2eq123i 6341 . . . . . . . . . . . . . 14 SubGrp Cntz mrClsSubGrp finSupp g SubGrp Cntz mrClsSubGrp g
5230, 51eqtri 2431 . . . . . . . . . . . . 13 DProd SubGrp Cntz mrClsSubGrp g
5352fmpt2x 6850 . . . . . . . . . . . 12 SubGrp Cntz mrClsSubGrp g DProd SubGrp Cntz mrClsSubGrp
5429, 53mpbi 208 . . . . . . . . . . 11 DProd SubGrp Cntz mrClsSubGrp
5554fdmi 5719 . . . . . . . . . 10 DProd SubGrp Cntz mrClsSubGrp
5655eleq2i 2480 . . . . . . . . 9 DProd SubGrp Cntz mrClsSubGrp
57 opeliunxp 4875 . . . . . . . . 9 SubGrp Cntz mrClsSubGrp SubGrp Cntz mrClsSubGrp
5821, 56, 573bitri 271 . . . . . . . 8 DProd SubGrp Cntz mrClsSubGrp
5952ovmpt4g 6406 . . . . . . . . 9 SubGrp Cntz mrClsSubGrp g DProd g
6028, 59mp3an3 1315 . . . . . . . 8 SubGrp Cntz mrClsSubGrp DProd g
6158, 60sylbi 195 . . . . . . 7 DProd DProd g
6220, 61vtoclg 3117 . . . . . 6 DProd DProd g
635, 62mpcom 34 . . . . 5 DProd DProd g
6463sbcth 3292 . . . 4 DProd DProd g
654, 64syl 17 . . 3 DProd DProd DProd g
66 simpr 459 . . . . . 6 DProd
6766breq2d 4407 . . . . 5 DProd DProd DProd
6866oveq2d 6294 . . . . . 6 DProd DProd DProd
6966dmeqd 5026 . . . . . . . . . . . . 13 DProd
70 simplr 754 . . . . . . . . . . . . 13 DProd
7169, 70eqtrd 2443 . . . . . . . . . . . 12 DProd
7271ixpeq1d 7519 . . . . . . . . . . 11 DProd
7366fveq1d 5851 . . . . . . . . . . . 12 DProd
7473ixpeq2dv 7523 . . . . . . . . . . 11 DProd
7572, 74eqtrd 2443 . . . . . . . . . 10 DProd
76 biidd 237 . . . . . . . . . 10 DProd
7775, 76rabeqbidv 3054 . . . . . . . . 9 DProd
78 dprdvalOLD.w . . . . . . . . 9
7977, 78syl6eqr 2461 . . . . . . . 8 DProd
80 eqidd 2403 . . . . . . . 8 DProd g g
8179, 80mpteq12dv 4473 . . . . . . 7 DProd g g
8281rneqd 5051 . . . . . 6 DProd g g
8368, 82eqeq12d 2424 . . . . 5 DProd DProd g DProd g
8467, 83imbi12d 318 . . . 4 DProd DProd DProd g DProd DProd g
854, 84sbcied 3314 . . 3 DProd DProd DProd g DProd DProd g
8665, 85mpbid 210 . 2 DProd DProd DProd g
871, 86mpd 15 1 DProd DProd g
 Colors of variables: wff setvar class Syntax hints:   wi 4   wb 184   wa 367   w3a 974   wceq 1405   wcel 1842  cab 2387  wral 2754  crab 2758  cvv 3059  wsbc 3277   cdif 3411   cin 3413   wss 3414  csn 3972  cop 3978  cuni 4191  ciun 4271   class class class wbr 4395   cmpt 4453   cxp 4821  ccnv 4822   cdm 4823   crn 4824  cima 4826   wfun 5563   wfn 5564  wf 5565  cfv 5569  (class class class)co 6278   cmpt2 6280   supp csupp 6902  cixp 7507  cfn 7554   finSupp cfsupp 7863  c0g 15054   g cgsu 15055  mrClscmrc 15197  cgrp 16377  SubGrpcsubg 16519  Cntzccntz 16677   DProd cdprd 17344 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1639  ax-4 1652  ax-5 1725  ax-6 1771  ax-7 1814  ax-8 1844  ax-9 1846  ax-10 1861  ax-11 1866  ax-12 1878  ax-13 2026  ax-ext 2380  ax-rep 4507  ax-sep 4517  ax-nul 4525  ax-pow 4572  ax-pr 4630  ax-un 6574 This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-3an 976  df-tru 1408  df-ex 1634  df-nf 1638  df-sb 1764  df-eu 2242  df-mo 2243  df-clab 2388  df-cleq 2394  df-clel 2397  df-nfc 2552  df-ne 2600  df-ral 2759  df-rex 2760  df-reu 2761  df-rab 2763  df-v 3061  df-sbc 3278  df-csb 3374  df-dif 3417  df-un 3419  df-in 3421  df-ss 3428  df-nul 3739  df-if 3886  df-pw 3957  df-sn 3973  df-pr 3975  df-op 3979  df-uni 4192  df-iun 4273  df-br 4396  df-opab 4454  df-mpt 4455  df-id 4738  df-xp 4829  df-rel 4830  df-cnv 4831  df-co 4832  df-dm 4833  df-rn 4834  df-res 4835  df-ima 4836  df-iota 5533  df-fun 5571  df-fn 5572  df-f 5573  df-f1 5574  df-fo 5575  df-f1o 5576  df-fv 5577  df-ov 6281  df-oprab 6282  df-mpt2 6283  df-1st 6784  df-2nd 6785  df-supp 6903  df-ixp 7508  df-fsupp 7864  df-dprd 17346 This theorem is referenced by:  eldprdOLD  17357
 Copyright terms: Public domain W3C validator