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

Theorem dmdprd 17708
 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.) (Proof shortened by AV, 11-Jul-2019.)
Hypotheses
Ref Expression
dmdprd.z Cntz
dmdprd.0
dmdprd.k mrClsSubGrp
Assertion
Ref Expression
dmdprd DProd SubGrp
Distinct variable groups:   ,,   ,,   ,,   ,,
Allowed substitution hints:   (,)   (,)   (,)

Proof of Theorem dmdprd
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 elex 3040 . . . . 5 SubGrp
21a1i 11 . . . 4 SubGrp
3 fex 6155 . . . . . . 7 SubGrp
43expcom 442 . . . . . 6 SubGrp
54adantr 472 . . . . 5 SubGrp
65adantrd 475 . . . 4 SubGrp
7 df-sbc 3256 . . . . . 6 SubGrp SubGrp
8 simpr 468 . . . . . . 7
9 simpr 468 . . . . . . . . . 10
109dmeqd 5042 . . . . . . . . . . 11
11 simplr 770 . . . . . . . . . . 11
1210, 11eqtrd 2505 . . . . . . . . . 10
139, 12feq12d 5727 . . . . . . . . 9 SubGrp SubGrp
1412difeq1d 3539 . . . . . . . . . . . 12
159fveq1d 5881 . . . . . . . . . . . . 13
169fveq1d 5881 . . . . . . . . . . . . . 14
1716fveq2d 5883 . . . . . . . . . . . . 13
1815, 17sseq12d 3447 . . . . . . . . . . . 12
1914, 18raleqbidv 2987 . . . . . . . . . . 11
209, 14imaeq12d 5175 . . . . . . . . . . . . . . 15
2120unieqd 4200 . . . . . . . . . . . . . 14
2221fveq2d 5883 . . . . . . . . . . . . 13
2315, 22ineq12d 3626 . . . . . . . . . . . 12
2423eqeq1d 2473 . . . . . . . . . . 11
2519, 24anbi12d 725 . . . . . . . . . 10
2612, 25raleqbidv 2987 . . . . . . . . 9
2713, 26anbi12d 725 . . . . . . . 8 SubGrp SubGrp
2827adantlr 729 . . . . . . 7 SubGrp SubGrp
298, 28sbcied 3292 . . . . . 6 SubGrp SubGrp
307, 29syl5bbr 267 . . . . 5 SubGrp SubGrp
3130ex 441 . . . 4 SubGrp SubGrp
322, 6, 31pm5.21ndd 361 . . 3 SubGrp SubGrp
3332anbi2d 718 . 2 SubGrp SubGrp
34 df-br 4396 . . 3 DProd DProd
35 fvex 5889 . . . . . . . . . . 11
3635rgenw 2768 . . . . . . . . . 10
37 ixpexg 7564 . . . . . . . . . 10
3836, 37ax-mp 5 . . . . . . . . 9
3938mptrabex 6153 . . . . . . . 8 finSupp g
4039rnex 6746 . . . . . . 7 finSupp g
4140rgen2w 2769 . . . . . 6 SubGrp Cntz mrClsSubGrp finSupp g
42 df-dprd 17705 . . . . . . 7 DProd SubGrp Cntz mrClsSubGrp finSupp g
4342fmpt2x 6878 . . . . . 6 SubGrp Cntz mrClsSubGrp finSupp g DProd SubGrp Cntz mrClsSubGrp
4441, 43mpbi 213 . . . . 5 DProd SubGrp Cntz mrClsSubGrp
4544fdmi 5746 . . . 4 DProd SubGrp Cntz mrClsSubGrp
4645eleq2i 2541 . . 3 DProd SubGrp Cntz mrClsSubGrp
47 fveq2 5879 . . . . . . 7 SubGrp SubGrp
4847feq3d 5726 . . . . . 6 SubGrp SubGrp
49 fveq2 5879 . . . . . . . . . . . 12 Cntz Cntz
50 dmdprd.z . . . . . . . . . . . 12 Cntz
5149, 50syl6eqr 2523 . . . . . . . . . . 11 Cntz
5251fveq1d 5881 . . . . . . . . . 10 Cntz
5352sseq2d 3446 . . . . . . . . 9 Cntz
5453ralbidv 2829 . . . . . . . 8 Cntz
5547fveq2d 5883 . . . . . . . . . . . 12 mrClsSubGrp mrClsSubGrp
56 dmdprd.k . . . . . . . . . . . 12 mrClsSubGrp
5755, 56syl6eqr 2523 . . . . . . . . . . 11 mrClsSubGrp
5857fveq1d 5881 . . . . . . . . . 10 mrClsSubGrp
5958ineq2d 3625 . . . . . . . . 9 mrClsSubGrp
60 fveq2 5879 . . . . . . . . . . 11
61 dmdprd.0 . . . . . . . . . . 11
6260, 61syl6eqr 2523 . . . . . . . . . 10
6362sneqd 3971 . . . . . . . . 9
6459, 63eqeq12d 2486 . . . . . . . 8 mrClsSubGrp
6554, 64anbi12d 725 . . . . . . 7 Cntz mrClsSubGrp
6665ralbidv 2829 . . . . . 6 Cntz mrClsSubGrp
6748, 66anbi12d 725 . . . . 5 SubGrp Cntz mrClsSubGrp SubGrp
6867abbidv 2589 . . . 4 SubGrp Cntz mrClsSubGrp SubGrp
6968opeliunxp2 4978 . . 3 SubGrp Cntz mrClsSubGrp SubGrp
7034, 46, 693bitri 279 . 2 DProd SubGrp
71 3anass 1011 . 2 SubGrp SubGrp
7233, 70, 713bitr4g 296 1 DProd SubGrp
 Colors of variables: wff setvar class Syntax hints:   wi 4   wb 189   wa 376   w3a 1007   wceq 1452   wcel 1904  cab 2457  wral 2756  crab 2760  cvv 3031  wsbc 3255   cdif 3387   cin 3389   wss 3390  csn 3959  cop 3965  cuni 4190  ciun 4269   class class class wbr 4395   cmpt 4454   cxp 4837   cdm 4839   crn 4840  cima 4842  wf 5585  cfv 5589  (class class class)co 6308  cixp 7540   finSupp cfsupp 7901  c0g 15416   g cgsu 15417  mrClscmrc 15567  cgrp 16747  SubGrpcsubg 16889  Cntzccntz 17047   DProd cdprd 17703 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1677  ax-4 1690  ax-5 1766  ax-6 1813  ax-7 1859  ax-8 1906  ax-9 1913  ax-10 1932  ax-11 1937  ax-12 1950  ax-13 2104  ax-ext 2451  ax-rep 4508  ax-sep 4518  ax-nul 4527  ax-pow 4579  ax-pr 4639  ax-un 6602 This theorem depends on definitions:  df-bi 190  df-or 377  df-an 378  df-3an 1009  df-tru 1455  df-ex 1672  df-nf 1676  df-sb 1806  df-eu 2323  df-mo 2324  df-clab 2458  df-cleq 2464  df-clel 2467  df-nfc 2601  df-ne 2643  df-ral 2761  df-rex 2762  df-reu 2763  df-rab 2765  df-v 3033  df-sbc 3256  df-csb 3350  df-dif 3393  df-un 3395  df-in 3397  df-ss 3404  df-nul 3723  df-if 3873  df-pw 3944  df-sn 3960  df-pr 3962  df-op 3966  df-uni 4191  df-iun 4271  df-br 4396  df-opab 4455  df-mpt 4456  df-id 4754  df-xp 4845  df-rel 4846  df-cnv 4847  df-co 4848  df-dm 4849  df-rn 4850  df-res 4851  df-ima 4852  df-iota 5553  df-fun 5591  df-fn 5592  df-f 5593  df-f1 5594  df-fo 5595  df-f1o 5596  df-fv 5597  df-oprab 6312  df-mpt2 6313  df-1st 6812  df-2nd 6813  df-ixp 7541  df-dprd 17705 This theorem is referenced by:  dmdprdd  17709  dprdgrp  17715  dprdf  17716  dprdcntz  17718  dprddisj  17719  dprdres  17739  subgdmdprd  17745
 Copyright terms: Public domain W3C validator