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

Theorem dprdval 15337
 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.)
Hypotheses
Ref Expression
dprdval.0
dprdval.w
Assertion
Ref Expression
dprdval DProd DProd g
Distinct variable groups:   ,,,   ,,,   ,,,
Allowed substitution hints:   (,,)   (,,)

Proof of Theorem dprdval
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 simpl 443 . 2 DProd DProd
2 reldmdprd 15334 . . . . . 6 DProd
32brrelex2i 4812 . . . . 5 DProd
43adantr 451 . . . 4 DProd
52brrelexi 4811 . . . . . 6 DProd
6 breq1 4107 . . . . . . . 8 DProd DProd
7 oveq1 5952 . . . . . . . . 9 DProd DProd
8 fveq2 5608 . . . . . . . . . . . . . . . . 17
9 dprdval.0 . . . . . . . . . . . . . . . . 17
108, 9syl6eqr 2408 . . . . . . . . . . . . . . . 16
1110sneqd 3729 . . . . . . . . . . . . . . 15
1211difeq2d 3370 . . . . . . . . . . . . . 14
1312imaeq2d 5094 . . . . . . . . . . . . 13
1413eleq1d 2424 . . . . . . . . . . . 12
1514rabbidv 2856 . . . . . . . . . . 11
16 oveq1 5952 . . . . . . . . . . 11 g g
1715, 16mpteq12dv 4179 . . . . . . . . . 10 g g
1817rneqd 4988 . . . . . . . . 9 g g
197, 18eqeq12d 2372 . . . . . . . 8 DProd g DProd g
206, 19imbi12d 311 . . . . . . 7 DProd DProd g DProd DProd g
21 df-br 4105 . . . . . . . . 9 DProd DProd
22 fvex 5622 . . . . . . . . . . . . . . . . . 18
2322rgenw 2686 . . . . . . . . . . . . . . . . 17
24 ixpexg 6928 . . . . . . . . . . . . . . . . 17
2523, 24ax-mp 8 . . . . . . . . . . . . . . . 16
2625rabex 4246 . . . . . . . . . . . . . . 15
2726mptex 5832 . . . . . . . . . . . . . 14 g
2827rnex 5024 . . . . . . . . . . . . 13 g
2928rgen2w 2687 . . . . . . . . . . . 12 SubGrp Cntz mrClsSubGrp g
30 df-dprd 15332 . . . . . . . . . . . . 13 DProd SubGrp Cntz mrClsSubGrp g
3130fmpt2x 6277 . . . . . . . . . . . 12 SubGrp Cntz mrClsSubGrp g DProd SubGrp Cntz mrClsSubGrp
3229, 31mpbi 199 . . . . . . . . . . 11 DProd SubGrp Cntz mrClsSubGrp
3332fdmi 5477 . . . . . . . . . 10 DProd SubGrp Cntz mrClsSubGrp
3433eleq2i 2422 . . . . . . . . 9 DProd SubGrp Cntz mrClsSubGrp
35 opeliunxp 4822 . . . . . . . . 9 SubGrp Cntz mrClsSubGrp SubGrp Cntz mrClsSubGrp
3621, 34, 353bitri 262 . . . . . . . 8 DProd SubGrp Cntz mrClsSubGrp
3730ovmpt4g 6057 . . . . . . . . 9 SubGrp Cntz mrClsSubGrp g DProd g
3828, 37mp3an3 1266 . . . . . . . 8 SubGrp Cntz mrClsSubGrp DProd g
3936, 38sylbi 187 . . . . . . 7 DProd DProd g
4020, 39vtoclg 2919 . . . . . 6 DProd DProd g
415, 40mpcom 32 . . . . 5 DProd DProd g
4241sbcth 3081 . . . 4 DProd DProd g
434, 42syl 15 . . 3 DProd DProd DProd g
44 simpr 447 . . . . . 6 DProd
4544breq2d 4116 . . . . 5 DProd DProd DProd
4644oveq2d 5961 . . . . . 6 DProd DProd DProd
4744dmeqd 4963 . . . . . . . . . . . . 13 DProd
48 simplr 731 . . . . . . . . . . . . 13 DProd
4947, 48eqtrd 2390 . . . . . . . . . . . 12 DProd
50 ixpeq1 6915 . . . . . . . . . . . 12
5149, 50syl 15 . . . . . . . . . . 11 DProd
5244fveq1d 5610 . . . . . . . . . . . . 13 DProd
5352ralrimivw 2703 . . . . . . . . . . . 12 DProd
54 ixpeq2 6918 . . . . . . . . . . . 12
5553, 54syl 15 . . . . . . . . . . 11 DProd
5651, 55eqtrd 2390 . . . . . . . . . 10 DProd
57 biidd 228 . . . . . . . . . 10 DProd
5856, 57rabeqbidv 2859 . . . . . . . . 9 DProd
59 dprdval.w . . . . . . . . 9
6058, 59syl6eqr 2408 . . . . . . . 8 DProd
61 eqidd 2359 . . . . . . . 8 DProd g g
6260, 61mpteq12dv 4179 . . . . . . 7 DProd g g
6362rneqd 4988 . . . . . 6 DProd g g
6446, 63eqeq12d 2372 . . . . 5 DProd DProd g DProd g
6545, 64imbi12d 311 . . . 4 DProd DProd DProd g DProd DProd g
664, 65sbcied 3103 . . 3 DProd DProd DProd g DProd DProd g
6743, 66mpbid 201 . 2 DProd DProd DProd g
681, 67mpd 14 1 DProd DProd g
 Colors of variables: wff set class Syntax hints:   wi 4   wa 358   wceq 1642   wcel 1710  cab 2344  wral 2619  crab 2623  cvv 2864  wsbc 3067   cdif 3225   cin 3227   wss 3228  csn 3716  cop 3719  cuni 3908  ciun 3986   class class class wbr 4104   cmpt 4158   cxp 4769  ccnv 4770   cdm 4771   crn 4772  cima 4774  wf 5333  cfv 5337  (class class class)co 5945  cixp 6905  cfn 6951  c0g 13499   g cgsu 13500  mrClscmrc 13584  cgrp 14461  SubGrpcsubg 14714  Cntzccntz 14890   DProd cdprd 15330 This theorem is referenced by:  eldprd  15338  dprdlub  15360 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1546  ax-5 1557  ax-17 1616  ax-9 1654  ax-8 1675  ax-13 1712  ax-14 1714  ax-6 1729  ax-7 1734  ax-11 1746  ax-12 1930  ax-ext 2339  ax-rep 4212  ax-sep 4222  ax-nul 4230  ax-pow 4269  ax-pr 4295  ax-un 4594 This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-tru 1319  df-ex 1542  df-nf 1545  df-sb 1649  df-eu 2213  df-mo 2214  df-clab 2345  df-cleq 2351  df-clel 2354  df-nfc 2483  df-ne 2523  df-ral 2624  df-rex 2625  df-reu 2626  df-rab 2628  df-v 2866  df-sbc 3068  df-csb 3158  df-dif 3231  df-un 3233  df-in 3235  df-ss 3242  df-nul 3532  df-if 3642  df-pw 3703  df-sn 3722  df-pr 3723  df-op 3725  df-uni 3909  df-iun 3988  df-br 4105  df-opab 4159  df-mpt 4160  df-id 4391  df-xp 4777  df-rel 4778  df-cnv 4779  df-co 4780  df-dm 4781  df-rn 4782  df-res 4783  df-ima 4784  df-iota 5301  df-fun 5339  df-fn 5340  df-f 5341  df-f1 5342  df-fo 5343  df-f1o 5344  df-fv 5345  df-ov 5948  df-oprab 5949  df-mpt2 5950  df-1st 6209  df-2nd 6210  df-ixp 6906  df-dprd 15332
 Copyright terms: Public domain W3C validator