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

Definition df-dprd 15233
Description: Define the internal direct product of a family of subgroups. (Contributed by Mario Carneiro, 21-Apr-2016.)
Assertion
Ref Expression
df-dprd  |- DProd  =  ( g  e.  Grp , 
s  e.  { h  |  ( h : dom  h --> (SubGrp `  g )  /\  A. x  e.  dom  h ( A. y  e.  ( dom  h  \  {
x } ) ( h `  x ) 
C_  ( (Cntz `  g ) `  (
h `  y )
)  /\  ( (
h `  x )  i^i  ( (mrCls `  (SubGrp `  g ) ) `  U. ( h " ( dom  h  \  { x } ) ) ) )  =  { ( 0g `  g ) } ) ) } 
|->  ran  ( f  e. 
{ h  e.  X_ x  e.  dom  s ( s `  x )  |  ( `' h " ( _V  \  {
( 0g `  g
) } ) )  e.  Fin }  |->  ( g  gsumg  f ) ) )
Distinct variable group:    g, h, f, s, x, y

Detailed syntax breakdown of Definition df-dprd
StepHypRef Expression
1 cdprd 15231 . 2  class DProd
2 vg . . 3  set  g
3 vs . . 3  set  s
4 cgrp 14362 . . 3  class  Grp
5 vh . . . . . . . 8  set  h
65cv 1622 . . . . . . 7  class  h
76cdm 4689 . . . . . 6  class  dom  h
82cv 1622 . . . . . . 7  class  g
9 csubg 14615 . . . . . . 7  class SubGrp
108, 9cfv 5255 . . . . . 6  class  (SubGrp `  g )
117, 10, 6wf 5251 . . . . 5  wff  h : dom  h --> (SubGrp `  g )
12 vx . . . . . . . . . . 11  set  x
1312cv 1622 . . . . . . . . . 10  class  x
1413, 6cfv 5255 . . . . . . . . 9  class  ( h `
 x )
15 vy . . . . . . . . . . . 12  set  y
1615cv 1622 . . . . . . . . . . 11  class  y
1716, 6cfv 5255 . . . . . . . . . 10  class  ( h `
 y )
18 ccntz 14791 . . . . . . . . . . 11  class Cntz
198, 18cfv 5255 . . . . . . . . . 10  class  (Cntz `  g )
2017, 19cfv 5255 . . . . . . . . 9  class  ( (Cntz `  g ) `  (
h `  y )
)
2114, 20wss 3152 . . . . . . . 8  wff  ( h `
 x )  C_  ( (Cntz `  g ) `  ( h `  y
) )
2213csn 3640 . . . . . . . . 9  class  { x }
237, 22cdif 3149 . . . . . . . 8  class  ( dom  h  \  { x } )
2421, 15, 23wral 2543 . . . . . . 7  wff  A. y  e.  ( dom  h  \  { x } ) ( h `  x
)  C_  ( (Cntz `  g ) `  (
h `  y )
)
256, 23cima 4692 . . . . . . . . . . 11  class  ( h
" ( dom  h  \  { x } ) )
2625cuni 3827 . . . . . . . . . 10  class  U. (
h " ( dom  h  \  { x } ) )
27 cmrc 13485 . . . . . . . . . . 11  class mrCls
2810, 27cfv 5255 . . . . . . . . . 10  class  (mrCls `  (SubGrp `  g ) )
2926, 28cfv 5255 . . . . . . . . 9  class  ( (mrCls `  (SubGrp `  g )
) `  U. ( h
" ( dom  h  \  { x } ) ) )
3014, 29cin 3151 . . . . . . . 8  class  ( ( h `  x )  i^i  ( (mrCls `  (SubGrp `  g ) ) `
 U. ( h
" ( dom  h  \  { x } ) ) ) )
31 c0g 13400 . . . . . . . . . 10  class  0g
328, 31cfv 5255 . . . . . . . . 9  class  ( 0g
`  g )
3332csn 3640 . . . . . . . 8  class  { ( 0g `  g ) }
3430, 33wceq 1623 . . . . . . 7  wff  ( ( h `  x )  i^i  ( (mrCls `  (SubGrp `  g ) ) `
 U. ( h
" ( dom  h  \  { x } ) ) ) )  =  { ( 0g `  g ) }
3524, 34wa 358 . . . . . 6  wff  ( A. y  e.  ( dom  h  \  { x }
) ( h `  x )  C_  (
(Cntz `  g ) `  ( h `  y
) )  /\  (
( h `  x
)  i^i  ( (mrCls `  (SubGrp `  g )
) `  U. ( h
" ( dom  h  \  { x } ) ) ) )  =  { ( 0g `  g ) } )
3635, 12, 7wral 2543 . . . . 5  wff  A. x  e.  dom  h ( A. y  e.  ( dom  h  \  { x }
) ( h `  x )  C_  (
(Cntz `  g ) `  ( h `  y
) )  /\  (
( h `  x
)  i^i  ( (mrCls `  (SubGrp `  g )
) `  U. ( h
" ( dom  h  \  { x } ) ) ) )  =  { ( 0g `  g ) } )
3711, 36wa 358 . . . 4  wff  ( h : dom  h --> (SubGrp `  g )  /\  A. x  e.  dom  h ( A. y  e.  ( dom  h  \  {
x } ) ( h `  x ) 
C_  ( (Cntz `  g ) `  (
h `  y )
)  /\  ( (
h `  x )  i^i  ( (mrCls `  (SubGrp `  g ) ) `  U. ( h " ( dom  h  \  { x } ) ) ) )  =  { ( 0g `  g ) } ) )
3837, 5cab 2269 . . 3  class  { h  |  ( h : dom  h --> (SubGrp `  g )  /\  A. x  e.  dom  h ( A. y  e.  ( dom  h  \  {
x } ) ( h `  x ) 
C_  ( (Cntz `  g ) `  (
h `  y )
)  /\  ( (
h `  x )  i^i  ( (mrCls `  (SubGrp `  g ) ) `  U. ( h " ( dom  h  \  { x } ) ) ) )  =  { ( 0g `  g ) } ) ) }
39 vf . . . . 5  set  f
406ccnv 4688 . . . . . . . 8  class  `' h
41 cvv 2788 . . . . . . . . 9  class  _V
4241, 33cdif 3149 . . . . . . . 8  class  ( _V 
\  { ( 0g
`  g ) } )
4340, 42cima 4692 . . . . . . 7  class  ( `' h " ( _V 
\  { ( 0g
`  g ) } ) )
44 cfn 6863 . . . . . . 7  class  Fin
4543, 44wcel 1684 . . . . . 6  wff  ( `' h " ( _V 
\  { ( 0g
`  g ) } ) )  e.  Fin
463cv 1622 . . . . . . . 8  class  s
4746cdm 4689 . . . . . . 7  class  dom  s
4813, 46cfv 5255 . . . . . . 7  class  ( s `
 x )
4912, 47, 48cixp 6817 . . . . . 6  class  X_ x  e.  dom  s ( s `
 x )
5045, 5, 49crab 2547 . . . . 5  class  { h  e.  X_ x  e.  dom  s ( s `  x )  |  ( `' h " ( _V 
\  { ( 0g
`  g ) } ) )  e.  Fin }
5139cv 1622 . . . . . 6  class  f
52 cgsu 13401 . . . . . 6  class  gsumg
538, 51, 52co 5858 . . . . 5  class  ( g 
gsumg  f )
5439, 50, 53cmpt 4077 . . . 4  class  ( f  e.  { h  e.  X_ x  e.  dom  s ( s `  x )  |  ( `' h " ( _V 
\  { ( 0g
`  g ) } ) )  e.  Fin } 
|->  ( g  gsumg  f ) )
5554crn 4690 . . 3  class  ran  (
f  e.  { h  e.  X_ x  e.  dom  s ( s `  x )  |  ( `' h " ( _V 
\  { ( 0g
`  g ) } ) )  e.  Fin } 
|->  ( g  gsumg  f ) )
562, 3, 4, 38, 55cmpt2 5860 . 2  class  ( g  e.  Grp ,  s  e.  { h  |  ( h : dom  h
--> (SubGrp `  g )  /\  A. x  e.  dom  h ( A. y  e.  ( dom  h  \  { x } ) ( h `  x
)  C_  ( (Cntz `  g ) `  (
h `  y )
)  /\  ( (
h `  x )  i^i  ( (mrCls `  (SubGrp `  g ) ) `  U. ( h " ( dom  h  \  { x } ) ) ) )  =  { ( 0g `  g ) } ) ) } 
|->  ran  ( f  e. 
{ h  e.  X_ x  e.  dom  s ( s `  x )  |  ( `' h " ( _V  \  {
( 0g `  g
) } ) )  e.  Fin }  |->  ( g  gsumg  f ) ) )
571, 56wceq 1623 1  wff DProd  =  ( g  e.  Grp , 
s  e.  { h  |  ( h : dom  h --> (SubGrp `  g )  /\  A. x  e.  dom  h ( A. y  e.  ( dom  h  \  {
x } ) ( h `  x ) 
C_  ( (Cntz `  g ) `  (
h `  y )
)  /\  ( (
h `  x )  i^i  ( (mrCls `  (SubGrp `  g ) ) `  U. ( h " ( dom  h  \  { x } ) ) ) )  =  { ( 0g `  g ) } ) ) } 
|->  ran  ( f  e. 
{ h  e.  X_ x  e.  dom  s ( s `  x )  |  ( `' h " ( _V  \  {
( 0g `  g
) } ) )  e.  Fin }  |->  ( g  gsumg  f ) ) )
Colors of variables: wff set class
This definition is referenced by:  reldmdprd  15235  dmdprd  15236  dprdval  15238
  Copyright terms: Public domain W3C validator