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

Theorem dprdz 17213
Description: A family consisting entirely of trivial groups is an internal direct product, the product of which is the trivial subgroup. (Contributed by Mario Carneiro, 25-Apr-2016.)
Hypothesis
Ref Expression
dprd0.0  |-  .0.  =  ( 0g `  G )
Assertion
Ref Expression
dprdz  |-  ( ( G  e.  Grp  /\  I  e.  V )  ->  ( G dom DProd  ( x  e.  I  |->  {  .0.  } )  /\  ( G DProd 
( x  e.  I  |->  {  .0.  } ) )  =  {  .0.  } ) )
Distinct variable groups:    x,  .0.    x, G    x, I    x, V

Proof of Theorem dprdz
Dummy variables  y 
z are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 eqid 2396 . . 3  |-  (Cntz `  G )  =  (Cntz `  G )
2 dprd0.0 . . 3  |-  .0.  =  ( 0g `  G )
3 eqid 2396 . . 3  |-  (mrCls `  (SubGrp `  G ) )  =  (mrCls `  (SubGrp `  G ) )
4 simpl 455 . . 3  |-  ( ( G  e.  Grp  /\  I  e.  V )  ->  G  e.  Grp )
5 simpr 459 . . 3  |-  ( ( G  e.  Grp  /\  I  e.  V )  ->  I  e.  V )
620subg 16366 . . . . 5  |-  ( G  e.  Grp  ->  {  .0.  }  e.  (SubGrp `  G
) )
76ad2antrr 723 . . . 4  |-  ( ( ( G  e.  Grp  /\  I  e.  V )  /\  x  e.  I
)  ->  {  .0.  }  e.  (SubGrp `  G
) )
8 eqid 2396 . . . 4  |-  ( x  e.  I  |->  {  .0.  } )  =  ( x  e.  I  |->  {  .0.  } )
97, 8fmptd 5974 . . 3  |-  ( ( G  e.  Grp  /\  I  e.  V )  ->  ( x  e.  I  |->  {  .0.  } ) : I --> (SubGrp `  G ) )
10 eqid 2396 . . . . . . . . . . 11  |-  ( Base `  G )  =  (
Base `  G )
1110, 2grpidcl 16218 . . . . . . . . . 10  |-  ( G  e.  Grp  ->  .0.  e.  ( Base `  G
) )
1211adantr 463 . . . . . . . . 9  |-  ( ( G  e.  Grp  /\  I  e.  V )  ->  .0.  e.  ( Base `  G ) )
1312snssd 4106 . . . . . . . 8  |-  ( ( G  e.  Grp  /\  I  e.  V )  ->  {  .0.  }  C_  ( Base `  G )
)
1410, 1cntzsubg 16514 . . . . . . . 8  |-  ( ( G  e.  Grp  /\  {  .0.  }  C_  ( Base `  G ) )  ->  ( (Cntz `  G ) `  {  .0.  } )  e.  (SubGrp `  G ) )
1513, 14syldan 468 . . . . . . 7  |-  ( ( G  e.  Grp  /\  I  e.  V )  ->  ( (Cntz `  G
) `  {  .0.  }
)  e.  (SubGrp `  G ) )
162subg0cl 16349 . . . . . . 7  |-  ( ( (Cntz `  G ) `  {  .0.  } )  e.  (SubGrp `  G
)  ->  .0.  e.  ( (Cntz `  G ) `  {  .0.  } ) )
1715, 16syl 16 . . . . . 6  |-  ( ( G  e.  Grp  /\  I  e.  V )  ->  .0.  e.  ( (Cntz `  G ) `  {  .0.  } ) )
1817snssd 4106 . . . . 5  |-  ( ( G  e.  Grp  /\  I  e.  V )  ->  {  .0.  }  C_  ( (Cntz `  G ) `  {  .0.  } ) )
1918adantr 463 . . . 4  |-  ( ( ( G  e.  Grp  /\  I  e.  V )  /\  ( y  e.  I  /\  z  e.  I  /\  y  =/=  z ) )  ->  {  .0.  }  C_  (
(Cntz `  G ) `  {  .0.  } ) )
20 simpr1 1000 . . . . 5  |-  ( ( ( G  e.  Grp  /\  I  e.  V )  /\  ( y  e.  I  /\  z  e.  I  /\  y  =/=  z ) )  -> 
y  e.  I )
21 eqidd 2397 . . . . . 6  |-  ( x  =  y  ->  {  .0.  }  =  {  .0.  }
)
22 snex 4620 . . . . . 6  |-  {  .0.  }  e.  _V
2321, 8, 22fvmpt3i 5878 . . . . 5  |-  ( y  e.  I  ->  (
( x  e.  I  |->  {  .0.  } ) `
 y )  =  {  .0.  } )
2420, 23syl 16 . . . 4  |-  ( ( ( G  e.  Grp  /\  I  e.  V )  /\  ( y  e.  I  /\  z  e.  I  /\  y  =/=  z ) )  -> 
( ( x  e.  I  |->  {  .0.  } ) `
 y )  =  {  .0.  } )
25 simpr2 1001 . . . . . 6  |-  ( ( ( G  e.  Grp  /\  I  e.  V )  /\  ( y  e.  I  /\  z  e.  I  /\  y  =/=  z ) )  -> 
z  e.  I )
26 eqidd 2397 . . . . . . 7  |-  ( x  =  z  ->  {  .0.  }  =  {  .0.  }
)
2726, 8, 22fvmpt3i 5878 . . . . . 6  |-  ( z  e.  I  ->  (
( x  e.  I  |->  {  .0.  } ) `
 z )  =  {  .0.  } )
2825, 27syl 16 . . . . 5  |-  ( ( ( G  e.  Grp  /\  I  e.  V )  /\  ( y  e.  I  /\  z  e.  I  /\  y  =/=  z ) )  -> 
( ( x  e.  I  |->  {  .0.  } ) `
 z )  =  {  .0.  } )
2928fveq2d 5795 . . . 4  |-  ( ( ( G  e.  Grp  /\  I  e.  V )  /\  ( y  e.  I  /\  z  e.  I  /\  y  =/=  z ) )  -> 
( (Cntz `  G
) `  ( (
x  e.  I  |->  {  .0.  } ) `  z ) )  =  ( (Cntz `  G
) `  {  .0.  }
) )
3019, 24, 293sstr4d 3477 . . 3  |-  ( ( ( G  e.  Grp  /\  I  e.  V )  /\  ( y  e.  I  /\  z  e.  I  /\  y  =/=  z ) )  -> 
( ( x  e.  I  |->  {  .0.  } ) `
 y )  C_  ( (Cntz `  G ) `  ( ( x  e.  I  |->  {  .0.  } ) `
 z ) ) )
3123adantl 464 . . . . . 6  |-  ( ( ( G  e.  Grp  /\  I  e.  V )  /\  y  e.  I
)  ->  ( (
x  e.  I  |->  {  .0.  } ) `  y )  =  {  .0.  } )
3231ineq1d 3630 . . . . 5  |-  ( ( ( G  e.  Grp  /\  I  e.  V )  /\  y  e.  I
)  ->  ( (
( x  e.  I  |->  {  .0.  } ) `
 y )  i^i  ( (mrCls `  (SubGrp `  G ) ) `  U. ( ( x  e.  I  |->  {  .0.  } )
" ( I  \  { y } ) ) ) )  =  ( {  .0.  }  i^i  ( (mrCls `  (SubGrp `  G ) ) `  U. ( ( x  e.  I  |->  {  .0.  } )
" ( I  \  { y } ) ) ) ) )
3310subgacs 16376 . . . . . . . . . . 11  |-  ( G  e.  Grp  ->  (SubGrp `  G )  e.  (ACS
`  ( Base `  G
) ) )
3433ad2antrr 723 . . . . . . . . . 10  |-  ( ( ( G  e.  Grp  /\  I  e.  V )  /\  y  e.  I
)  ->  (SubGrp `  G
)  e.  (ACS `  ( Base `  G )
) )
3534acsmred 15086 . . . . . . . . 9  |-  ( ( ( G  e.  Grp  /\  I  e.  V )  /\  y  e.  I
)  ->  (SubGrp `  G
)  e.  (Moore `  ( Base `  G )
) )
36 imassrn 5277 . . . . . . . . . . 11  |-  ( ( x  e.  I  |->  {  .0.  } ) "
( I  \  {
y } ) ) 
C_  ran  ( x  e.  I  |->  {  .0.  } )
379adantr 463 . . . . . . . . . . . . 13  |-  ( ( ( G  e.  Grp  /\  I  e.  V )  /\  y  e.  I
)  ->  ( x  e.  I  |->  {  .0.  } ) : I --> (SubGrp `  G ) )
38 frn 5662 . . . . . . . . . . . . 13  |-  ( ( x  e.  I  |->  {  .0.  } ) : I --> (SubGrp `  G )  ->  ran  ( x  e.  I  |->  {  .0.  } ) 
C_  (SubGrp `  G )
)
3937, 38syl 16 . . . . . . . . . . . 12  |-  ( ( ( G  e.  Grp  /\  I  e.  V )  /\  y  e.  I
)  ->  ran  ( x  e.  I  |->  {  .0.  } )  C_  (SubGrp `  G
) )
40 mresspw 15022 . . . . . . . . . . . . 13  |-  ( (SubGrp `  G )  e.  (Moore `  ( Base `  G
) )  ->  (SubGrp `  G )  C_  ~P ( Base `  G )
)
4135, 40syl 16 . . . . . . . . . . . 12  |-  ( ( ( G  e.  Grp  /\  I  e.  V )  /\  y  e.  I
)  ->  (SubGrp `  G
)  C_  ~P ( Base `  G ) )
4239, 41sstrd 3444 . . . . . . . . . . 11  |-  ( ( ( G  e.  Grp  /\  I  e.  V )  /\  y  e.  I
)  ->  ran  ( x  e.  I  |->  {  .0.  } )  C_  ~P ( Base `  G ) )
4336, 42syl5ss 3445 . . . . . . . . . 10  |-  ( ( ( G  e.  Grp  /\  I  e.  V )  /\  y  e.  I
)  ->  ( (
x  e.  I  |->  {  .0.  } ) "
( I  \  {
y } ) ) 
C_  ~P ( Base `  G
) )
44 sspwuni 4349 . . . . . . . . . 10  |-  ( ( ( x  e.  I  |->  {  .0.  } )
" ( I  \  { y } ) )  C_  ~P ( Base `  G )  <->  U. (
( x  e.  I  |->  {  .0.  } )
" ( I  \  { y } ) )  C_  ( Base `  G ) )
4543, 44sylib 196 . . . . . . . . 9  |-  ( ( ( G  e.  Grp  /\  I  e.  V )  /\  y  e.  I
)  ->  U. (
( x  e.  I  |->  {  .0.  } )
" ( I  \  { y } ) )  C_  ( Base `  G ) )
463mrccl 15041 . . . . . . . . 9  |-  ( ( (SubGrp `  G )  e.  (Moore `  ( Base `  G ) )  /\  U. ( ( x  e.  I  |->  {  .0.  } )
" ( I  \  { y } ) )  C_  ( Base `  G ) )  -> 
( (mrCls `  (SubGrp `  G ) ) `  U. ( ( x  e.  I  |->  {  .0.  } )
" ( I  \  { y } ) ) )  e.  (SubGrp `  G ) )
4735, 45, 46syl2anc 659 . . . . . . . 8  |-  ( ( ( G  e.  Grp  /\  I  e.  V )  /\  y  e.  I
)  ->  ( (mrCls `  (SubGrp `  G )
) `  U. ( ( x  e.  I  |->  {  .0.  } ) "
( I  \  {
y } ) ) )  e.  (SubGrp `  G ) )
482subg0cl 16349 . . . . . . . 8  |-  ( ( (mrCls `  (SubGrp `  G
) ) `  U. ( ( x  e.  I  |->  {  .0.  } )
" ( I  \  { y } ) ) )  e.  (SubGrp `  G )  ->  .0.  e.  ( (mrCls `  (SubGrp `  G ) ) `  U. ( ( x  e.  I  |->  {  .0.  } )
" ( I  \  { y } ) ) ) )
4947, 48syl 16 . . . . . . 7  |-  ( ( ( G  e.  Grp  /\  I  e.  V )  /\  y  e.  I
)  ->  .0.  e.  ( (mrCls `  (SubGrp `  G
) ) `  U. ( ( x  e.  I  |->  {  .0.  } )
" ( I  \  { y } ) ) ) )
5049snssd 4106 . . . . . 6  |-  ( ( ( G  e.  Grp  /\  I  e.  V )  /\  y  e.  I
)  ->  {  .0.  } 
C_  ( (mrCls `  (SubGrp `  G ) ) `
 U. ( ( x  e.  I  |->  {  .0.  } ) "
( I  \  {
y } ) ) ) )
51 df-ss 3420 . . . . . 6  |-  ( {  .0.  }  C_  (
(mrCls `  (SubGrp `  G
) ) `  U. ( ( x  e.  I  |->  {  .0.  } )
" ( I  \  { y } ) ) )  <->  ( {  .0.  }  i^i  ( (mrCls `  (SubGrp `  G )
) `  U. ( ( x  e.  I  |->  {  .0.  } ) "
( I  \  {
y } ) ) ) )  =  {  .0.  } )
5250, 51sylib 196 . . . . 5  |-  ( ( ( G  e.  Grp  /\  I  e.  V )  /\  y  e.  I
)  ->  ( {  .0.  }  i^i  ( (mrCls `  (SubGrp `  G )
) `  U. ( ( x  e.  I  |->  {  .0.  } ) "
( I  \  {
y } ) ) ) )  =  {  .0.  } )
5332, 52eqtrd 2437 . . . 4  |-  ( ( ( G  e.  Grp  /\  I  e.  V )  /\  y  e.  I
)  ->  ( (
( x  e.  I  |->  {  .0.  } ) `
 y )  i^i  ( (mrCls `  (SubGrp `  G ) ) `  U. ( ( x  e.  I  |->  {  .0.  } )
" ( I  \  { y } ) ) ) )  =  {  .0.  } )
54 eqimss 3486 . . . 4  |-  ( ( ( ( x  e.  I  |->  {  .0.  } ) `
 y )  i^i  ( (mrCls `  (SubGrp `  G ) ) `  U. ( ( x  e.  I  |->  {  .0.  } )
" ( I  \  { y } ) ) ) )  =  {  .0.  }  ->  ( ( ( x  e.  I  |->  {  .0.  } ) `
 y )  i^i  ( (mrCls `  (SubGrp `  G ) ) `  U. ( ( x  e.  I  |->  {  .0.  } )
" ( I  \  { y } ) ) ) )  C_  {  .0.  } )
5553, 54syl 16 . . 3  |-  ( ( ( G  e.  Grp  /\  I  e.  V )  /\  y  e.  I
)  ->  ( (
( x  e.  I  |->  {  .0.  } ) `
 y )  i^i  ( (mrCls `  (SubGrp `  G ) ) `  U. ( ( x  e.  I  |->  {  .0.  } )
" ( I  \  { y } ) ) ) )  C_  {  .0.  } )
561, 2, 3, 4, 5, 9, 30, 55dmdprdd 17166 . 2  |-  ( ( G  e.  Grp  /\  I  e.  V )  ->  G dom DProd  ( x  e.  I  |->  {  .0.  } ) )
578, 7dmmptd 5636 . . . 4  |-  ( ( G  e.  Grp  /\  I  e.  V )  ->  dom  ( x  e.  I  |->  {  .0.  } )  =  I )
586adantr 463 . . . 4  |-  ( ( G  e.  Grp  /\  I  e.  V )  ->  {  .0.  }  e.  (SubGrp `  G ) )
59 eqimss 3486 . . . . 5  |-  ( ( ( x  e.  I  |->  {  .0.  } ) `
 y )  =  {  .0.  }  ->  ( ( x  e.  I  |->  {  .0.  } ) `
 y )  C_  {  .0.  } )
6031, 59syl 16 . . . 4  |-  ( ( ( G  e.  Grp  /\  I  e.  V )  /\  y  e.  I
)  ->  ( (
x  e.  I  |->  {  .0.  } ) `  y )  C_  {  .0.  } )
6156, 57, 58, 60dprdlub 17209 . . 3  |-  ( ( G  e.  Grp  /\  I  e.  V )  ->  ( G DProd  ( x  e.  I  |->  {  .0.  } ) )  C_  {  .0.  } )
62 dprdsubg 17207 . . . . 5  |-  ( G dom DProd  ( x  e.  I  |->  {  .0.  } )  ->  ( G DProd  (
x  e.  I  |->  {  .0.  } ) )  e.  (SubGrp `  G
) )
632subg0cl 16349 . . . . 5  |-  ( ( G DProd  ( x  e.  I  |->  {  .0.  } ) )  e.  (SubGrp `  G )  ->  .0.  e.  ( G DProd  ( x  e.  I  |->  {  .0.  } ) ) )
6456, 62, 633syl 20 . . . 4  |-  ( ( G  e.  Grp  /\  I  e.  V )  ->  .0.  e.  ( G DProd 
( x  e.  I  |->  {  .0.  } ) ) )
6564snssd 4106 . . 3  |-  ( ( G  e.  Grp  /\  I  e.  V )  ->  {  .0.  }  C_  ( G DProd  ( x  e.  I  |->  {  .0.  } ) ) )
6661, 65eqssd 3451 . 2  |-  ( ( G  e.  Grp  /\  I  e.  V )  ->  ( G DProd  ( x  e.  I  |->  {  .0.  } ) )  =  {  .0.  } )
6756, 66jca 530 1  |-  ( ( G  e.  Grp  /\  I  e.  V )  ->  ( G dom DProd  ( x  e.  I  |->  {  .0.  } )  /\  ( G DProd 
( x  e.  I  |->  {  .0.  } ) )  =  {  .0.  } ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 367    /\ w3a 971    = wceq 1399    e. wcel 1836    =/= wne 2591    \ cdif 3403    i^i cin 3405    C_ wss 3406   ~Pcpw 3944   {csn 3961   U.cuni 4180   class class class wbr 4384    |-> cmpt 4442   dom cdm 4930   ran crn 4931   "cima 4933   -->wf 5509   ` cfv 5513  (class class class)co 6218   Basecbs 14657   0gc0g 14870  Moorecmre 15012  mrClscmrc 15013  ACScacs 15015   Grpcgrp 16193  SubGrpcsubg 16335  Cntzccntz 16493   DProd cdprd 17160
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1633  ax-4 1646  ax-5 1719  ax-6 1765  ax-7 1808  ax-8 1838  ax-9 1840  ax-10 1855  ax-11 1860  ax-12 1872  ax-13 2020  ax-ext 2374  ax-rep 4495  ax-sep 4505  ax-nul 4513  ax-pow 4560  ax-pr 4618  ax-un 6513  ax-cnex 9481  ax-resscn 9482  ax-1cn 9483  ax-icn 9484  ax-addcl 9485  ax-addrcl 9486  ax-mulcl 9487  ax-mulrcl 9488  ax-mulcom 9489  ax-addass 9490  ax-mulass 9491  ax-distr 9492  ax-i2m1 9493  ax-1ne0 9494  ax-1rid 9495  ax-rnegex 9496  ax-rrecex 9497  ax-cnre 9498  ax-pre-lttri 9499  ax-pre-lttrn 9500  ax-pre-ltadd 9501  ax-pre-mulgt0 9502
This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-3or 972  df-3an 973  df-tru 1402  df-ex 1628  df-nf 1632  df-sb 1758  df-eu 2236  df-mo 2237  df-clab 2382  df-cleq 2388  df-clel 2391  df-nfc 2546  df-ne 2593  df-nel 2594  df-ral 2751  df-rex 2752  df-reu 2753  df-rmo 2754  df-rab 2755  df-v 3053  df-sbc 3270  df-csb 3366  df-dif 3409  df-un 3411  df-in 3413  df-ss 3420  df-pss 3422  df-nul 3729  df-if 3875  df-pw 3946  df-sn 3962  df-pr 3964  df-tp 3966  df-op 3968  df-uni 4181  df-int 4217  df-iun 4262  df-iin 4263  df-br 4385  df-opab 4443  df-mpt 4444  df-tr 4478  df-eprel 4722  df-id 4726  df-po 4731  df-so 4732  df-fr 4769  df-se 4770  df-we 4771  df-ord 4812  df-on 4813  df-lim 4814  df-suc 4815  df-xp 4936  df-rel 4937  df-cnv 4938  df-co 4939  df-dm 4940  df-rn 4941  df-res 4942  df-ima 4943  df-iota 5477  df-fun 5515  df-fn 5516  df-f 5517  df-f1 5518  df-fo 5519  df-f1o 5520  df-fv 5521  df-isom 5522  df-riota 6180  df-ov 6221  df-oprab 6222  df-mpt2 6223  df-of 6461  df-om 6622  df-1st 6721  df-2nd 6722  df-supp 6840  df-tpos 6895  df-recs 6982  df-rdg 7016  df-1o 7070  df-oadd 7074  df-er 7251  df-map 7362  df-ixp 7411  df-en 7458  df-dom 7459  df-sdom 7460  df-fin 7461  df-fsupp 7767  df-oi 7872  df-card 8255  df-pnf 9563  df-mnf 9564  df-xr 9565  df-ltxr 9566  df-le 9567  df-sub 9742  df-neg 9743  df-nn 10475  df-2 10533  df-n0 10735  df-z 10804  df-uz 11024  df-fz 11616  df-fzo 11740  df-seq 12034  df-hash 12331  df-ndx 14660  df-slot 14661  df-base 14662  df-sets 14663  df-ress 14664  df-plusg 14738  df-0g 14872  df-gsum 14873  df-mre 15016  df-mrc 15017  df-acs 15019  df-mgm 16012  df-sgrp 16051  df-mnd 16061  df-mhm 16106  df-submnd 16107  df-grp 16197  df-minusg 16198  df-sbg 16199  df-subg 16338  df-ghm 16405  df-gim 16447  df-cntz 16495  df-oppg 16521  df-cmn 16940  df-dprd 17162
This theorem is referenced by:  dprd0  17214
  Copyright terms: Public domain W3C validator