Definition df-dprd 18394

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

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 finSupp ( 0g ` g ) } |-> ( g gsumg f ) ) )

Distinct variable group:   g, h, f, s, x, y

Detailed syntax breakdown of Definition df-dprd

Step	Hyp	Ref	Expression
1		cdprd 18392	. 2 class DProd
2		vg	. . 3 setvar g
3		vs	. . 3 setvar s
4		cgrp 17422	. . 3 class Grp
5		vh	. . . . . . . 8 setvar h
6	5	cv 1482	. . . . . . 7 class h
7	6	cdm 5114	. . . . . 6 class dom h
8	2	cv 1482	. . . . . . 7 class g
9		csubg 17588	. . . . . . 7 class SubGrp
10	8, 9	cfv 5888	. . . . . 6 class (SubGrp ` g )
11	7, 10, 6	wf 5884	. . . . 5 wff h : dom h --> (SubGrp ` g )
12		vx	. . . . . . . . . . 11 setvar x
13	12	cv 1482	. . . . . . . . . 10 class x
14	13, 6	cfv 5888	. . . . . . . . 9 class ( h ` x )
15		vy	. . . . . . . . . . . 12 setvar y
16	15	cv 1482	. . . . . . . . . . 11 class y
17	16, 6	cfv 5888	. . . . . . . . . 10 class ( h ` y )
18		ccntz 17748	. . . . . . . . . . 11 class Cntz
19	8, 18	cfv 5888	. . . . . . . . . 10 class (Cntz ` g )
20	17, 19	cfv 5888	. . . . . . . . 9 class ( (Cntz ` g ) ` ( h ` y ) )
21	14, 20	wss 3574	. . . . . . . 8 wff ( h ` x ) C_ ( (Cntz ` g ) ` ( h ` y ) )
22	13	csn 4177	. . . . . . . . 9 class { x }
23	7, 22	cdif 3571	. . . . . . . 8 class ( dom h \ { x } )
24	21, 15, 23	wral 2912	. . . . . . 7 wff A. y e. ( dom h \ { x } ) ( h ` x ) C_ ( (Cntz ` g ) ` ( h ` y ) )
25	6, 23	cima 5117	. . . . . . . . . . 11 class ( h " ( dom h \ { x } ) )
26	25	cuni 4436	. . . . . . . . . 10 class U. ( h " ( dom h \ { x } ) )
27		cmrc 16243	. . . . . . . . . . 11 class mrCls
28	10, 27	cfv 5888	. . . . . . . . . 10 class (mrCls ` (SubGrp ` g ) )
29	26, 28	cfv 5888	. . . . . . . . 9 class ( (mrCls ` (SubGrp ` g ) ) ` U. ( h " ( dom h \ { x } ) ) )
30	14, 29	cin 3573	. . . . . . . 8 class ( ( h ` x ) i^i ( (mrCls ` (SubGrp ` g ) ) ` U. ( h " ( dom h \ { x } ) ) ) )
31		c0g 16100	. . . . . . . . . 10 class 0g
32	8, 31	cfv 5888	. . . . . . . . 9 class ( 0g ` g )
33	32	csn 4177	. . . . . . . 8 class { ( 0g ` g ) }
34	30, 33	wceq 1483	. . . . . . 7 wff ( ( h ` x ) i^i ( (mrCls ` (SubGrp ` g ) ) ` U. ( h " ( dom h \ { x } ) ) ) ) = { ( 0g ` g ) }
35	24, 34	wa 384	. . . . . 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 ) } )
36	35, 12, 7	wral 2912	. . . . 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 ) } )
37	11, 36	wa 384	. . . 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 ) } ) )
38	37, 5	cab 2608	. . 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 setvar f
40		cfsupp 8275	. . . . . . 7 class finSupp
41	6, 32, 40	wbr 4653	. . . . . 6 wff h finSupp ( 0g ` g )
42	3	cv 1482	. . . . . . . 8 class s
43	42	cdm 5114	. . . . . . 7 class dom s
44	13, 42	cfv 5888	. . . . . . 7 class ( s ` x )
45	12, 43, 44	cixp 7908	. . . . . 6 class X_ x e. dom s ( s ` x )
46	41, 5, 45	crab 2916	. . . . 5 class { h e. X_ x e. dom s ( s ` x ) | h finSupp ( 0g ` g ) }
47	39	cv 1482	. . . . . 6 class f
48		cgsu 16101	. . . . . 6 class gsumg
49	8, 47, 48	co 6650	. . . . 5 class ( g gsumg f )
50	39, 46, 49	cmpt 4729	. . . 4 class ( f e. { h e. X_ x e. dom s ( s ` x ) | h finSupp ( 0g ` g ) } |-> ( g gsumg f ) )
51	50	crn 5115	. . 3 class ran ( f e. { h e. X_ x e. dom s ( s ` x ) | h finSupp ( 0g ` g ) } |-> ( g gsumg f ) )
52	2, 3, 4, 38, 51	cmpt2 6652	. 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 finSupp ( 0g ` g ) } |-> ( g gsumg f ) ) )
53	1, 52	wceq 1483	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 finSupp ( 0g ` g ) } |-> ( g gsumg f ) ) )

This definition is referenced by:  reldmdprd  18396  dmdprd  18397  dprdval  18402