Metamath Proof Explorer

Definition df-dprd

Description: Define the internal direct product of a family of subgroups. (Contributed by Mario Carneiro, 21-Apr-2016) (Revised by AV, 11-Jul-2019)

Ref Expression
Assertion 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 finSupp ( 0g ` g ) } |-> ( g gsum f ) ) )

Detailed syntax breakdown

Step Hyp Ref Expression
0 cdprd 
 |-  DProd
1 vg 
 |-  g
2 cgrp 
 |-  Grp
3 vs 
 |-  s
4 vh 
 |-  h
5 4 cv 
 |-  h
6 5 cdm 
 |-  dom h
7 csubg 
 |-  SubGrp
8 1 cv 
 |-  g
9 8 7 cfv 
 |-  ( SubGrp ` g )
10 6 9 5 wf 
 |-  h : dom h --> ( SubGrp ` g )
11 vx 
 |-  x
12 vy 
 |-  y
13 11 cv 
 |-  x
14 13 csn 
 |-  { x }
15 6 14 cdif 
 |-  ( dom h \ { x } )
16 13 5 cfv 
 |-  ( h ` x )
17 ccntz 
 |-  Cntz
18 8 17 cfv 
 |-  ( Cntz ` g )
19 12 cv 
 |-  y
20 19 5 cfv 
 |-  ( h ` y )
21 20 18 cfv 
 |-  ( ( Cntz ` g ) ` ( h ` y ) )
22 16 21 wss 
 |-  ( h ` x ) C_ ( ( Cntz ` g ) ` ( h ` y ) )
23 22 12 15 wral 
 |-  A. y e. ( dom h \ { x } ) ( h ` x ) C_ ( ( Cntz ` g ) ` ( h ` y ) )
24 cmrc 
 |-  mrCls
25 9 24 cfv 
 |-  ( mrCls ` ( SubGrp ` g ) )
26 5 15 cima 
 |-  ( h " ( dom h \ { x } ) )
27 26 cuni 
 |-  U. ( h " ( dom h \ { x } ) )
28 27 25 cfv 
 |-  ( ( mrCls ` ( SubGrp ` g ) ) ` U. ( h " ( dom h \ { x } ) ) )
29 16 28 cin 
 |-  ( ( h ` x ) i^i ( ( mrCls ` ( SubGrp ` g ) ) ` U. ( h " ( dom h \ { x } ) ) ) )
30 c0g 
 |-  0g
31 8 30 cfv 
 |-  ( 0g ` g )
32 31 csn 
 |-  { ( 0g ` g ) }
33 29 32 wceq 
 |-  ( ( h ` x ) i^i ( ( mrCls ` ( SubGrp ` g ) ) ` U. ( h " ( dom h \ { x } ) ) ) ) = { ( 0g ` g ) }
34 23 33 wa 
 |-  ( 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 ) } )
35 34 11 6 wral 
 |-  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 ) } )
36 10 35 wa 
 |-  ( 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 ) } ) )
37 36 4 cab 
 |-  { 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 ) } ) ) }
38 vf 
 |-  f
39 3 cv 
 |-  s
40 39 cdm 
 |-  dom s
41 13 39 cfv 
 |-  ( s ` x )
42 11 40 41 cixp 
 |-  X_ x e. dom s ( s ` x )
43 cfsupp 
 |-  finSupp
44 5 31 43 wbr 
 |-  h finSupp ( 0g ` g )
45 44 4 42 crab 
 |-  { h e. X_ x e. dom s ( s ` x ) | h finSupp ( 0g ` g ) }
46 cgsu 
 |-  gsum
47 38 cv 
 |-  f
48 8 47 46 co 
 |-  ( g gsum f )
49 38 45 48 cmpt 
 |-  ( f e. { h e. X_ x e. dom s ( s ` x ) | h finSupp ( 0g ` g ) } |-> ( g gsum f ) )
50 49 crn 
 |-  ran ( f e. { h e. X_ x e. dom s ( s ` x ) | h finSupp ( 0g ` g ) } |-> ( g gsum f ) )
51 1 3 2 37 50 cmpo 
 |-  ( 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 finSupp ( 0g ` g ) } |-> ( g gsum f ) ) )
52 0 51 wceq 
 |-  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 finSupp ( 0g ` g ) } |-> ( g gsum f ) ) )