Theorem dprdval

Description: The value of the internal direct product operation, which is a function mapping the (infinite, but finitely supported) cartesian product of subgroups (which mutually commute and have trivial intersections) to its (group) sum . (Contributed by Mario Carneiro, 25-Apr-2016) (Revised by AV, 11-Jul-2019)

	Ref	Expression
Hypotheses	dprdval.0	|- .0. = ( 0g ` G )
	dprdval.w	|- W = { h e. X_ i e. I ( S ` i ) | h finSupp .0. }
Assertion	dprdval	|- ( ( G dom DProd S /\ dom S = I ) -> ( G DProd S ) = ran ( f e. W |-> ( G gsum f ) ) )

Proof

Step	Hyp	Ref	Expression
1		dprdval.0	|- .0. = ( 0g ` G )
2		dprdval.w	|- W = { h e. X_ i e. I ( S ` i ) | h finSupp .0. }
3		simpl	|- ( ( G dom DProd S /\ dom S = I ) -> G dom DProd S )
4		reldmdprd	|- Rel dom DProd
5	4	brrelex2i	|- ( G dom DProd S -> S e. _V )
6	5	adantr	|- ( ( G dom DProd S /\ dom S = I ) -> S e. _V )
7	4	brrelex1i	|- ( G dom DProd s -> G e. _V )
8		breq1	|- ( g = G -> ( g dom DProd s <-> G dom DProd s ) )
9		oveq1	|- ( g = G -> ( g DProd s ) = ( G DProd s ) )
10		fveq2	|- ( g = G -> ( 0g ` g ) = ( 0g ` G ) )
11	10 1	eqtr4di	|- ( g = G -> ( 0g ` g ) = .0. )
12	11	breq2d	|- ( g = G -> ( h finSupp ( 0g ` g ) <-> h finSupp .0. ) )
13	12	rabbidv	|- ( g = G -> { h e. X_ i e. dom s ( s ` i ) | h finSupp ( 0g ` g ) } = { h e. X_ i e. dom s ( s ` i ) | h finSupp .0. } )
14		oveq1	|- ( g = G -> ( g gsum f ) = ( G gsum f ) )
15	13 14	mpteq12dv	|- ( g = G -> ( f e. { h e. X_ i e. dom s ( s ` i ) | h finSupp ( 0g ` g ) } |-> ( g gsum f ) ) = ( f e. { h e. X_ i e. dom s ( s ` i ) | h finSupp .0. } |-> ( G gsum f ) ) )
16	15	rneqd	|- ( g = G -> ran ( f e. { h e. X_ i e. dom s ( s ` i ) | h finSupp ( 0g ` g ) } |-> ( g gsum f ) ) = ran ( f e. { h e. X_ i e. dom s ( s ` i ) | h finSupp .0. } |-> ( G gsum f ) ) )
17	9 16	eqeq12d	|- ( g = G -> ( ( g DProd s ) = ran ( f e. { h e. X_ i e. dom s ( s ` i ) | h finSupp ( 0g ` g ) } |-> ( g gsum f ) ) <-> ( G DProd s ) = ran ( f e. { h e. X_ i e. dom s ( s ` i ) | h finSupp .0. } |-> ( G gsum f ) ) ) )
18	8 17	imbi12d	|- ( g = G -> ( ( g dom DProd s -> ( g DProd s ) = ran ( f e. { h e. X_ i e. dom s ( s ` i ) | h finSupp ( 0g ` g ) } |-> ( g gsum f ) ) ) <-> ( G dom DProd s -> ( G DProd s ) = ran ( f e. { h e. X_ i e. dom s ( s ` i ) | h finSupp .0. } |-> ( G gsum f ) ) ) ) )
19		df-br	|- ( g dom DProd s <-> <. g , s >. e. dom DProd )
20		fvex	|- ( s ` i ) e. _V
21	20	rgenw	|- A. i e. dom s ( s ` i ) e. _V
22		ixpexg	|- ( A. i e. dom s ( s ` i ) e. _V -> X_ i e. dom s ( s ` i ) e. _V )
23	21 22	ax-mp	|- X_ i e. dom s ( s ` i ) e. _V
24	23	mptrabex	|- ( f e. { h e. X_ i e. dom s ( s ` i ) | h finSupp ( 0g ` g ) } |-> ( g gsum f ) ) e. _V
25	24	rnex	|- ran ( f e. { h e. X_ i e. dom s ( s ` i ) | h finSupp ( 0g ` g ) } |-> ( g gsum f ) ) e. _V
26	25	rgen2w	|- A. g e. Grp A. s e. { h | ( h : dom h --> ( SubGrp ` g ) /\ A. i e. dom h ( A. y e. ( dom h \ { i } ) ( h ` i ) C_ ( ( Cntz ` g ) ` ( h ` y ) ) /\ ( ( h ` i ) i^i ( ( mrCls ` ( SubGrp ` g ) ) ` U. ( h " ( dom h \ { i } ) ) ) ) = { ( 0g ` g ) } ) ) } ran ( f e. { h e. X_ i e. dom s ( s ` i ) | h finSupp ( 0g ` g ) } |-> ( g gsum f ) ) e. _V
27		df-dprd	|- DProd = ( g e. Grp , s e. { h | ( h : dom h --> ( SubGrp ` g ) /\ A. i e. dom h ( A. y e. ( dom h \ { i } ) ( h ` i ) C_ ( ( Cntz ` g ) ` ( h ` y ) ) /\ ( ( h ` i ) i^i ( ( mrCls ` ( SubGrp ` g ) ) ` U. ( h " ( dom h \ { i } ) ) ) ) = { ( 0g ` g ) } ) ) } |-> ran ( f e. { h e. X_ i e. dom s ( s ` i ) | h finSupp ( 0g ` g ) } |-> ( g gsum f ) ) )
28	27	fmpox	|- ( A. g e. Grp A. s e. { h | ( h : dom h --> ( SubGrp ` g ) /\ A. i e. dom h ( A. y e. ( dom h \ { i } ) ( h ` i ) C_ ( ( Cntz ` g ) ` ( h ` y ) ) /\ ( ( h ` i ) i^i ( ( mrCls ` ( SubGrp ` g ) ) ` U. ( h " ( dom h \ { i } ) ) ) ) = { ( 0g ` g ) } ) ) } ran ( f e. { h e. X_ i e. dom s ( s ` i ) | h finSupp ( 0g ` g ) } |-> ( g gsum f ) ) e. _V <-> DProd : U_ g e. Grp ( { g } X. { h | ( h : dom h --> ( SubGrp ` g ) /\ A. i e. dom h ( A. y e. ( dom h \ { i } ) ( h ` i ) C_ ( ( Cntz ` g ) ` ( h ` y ) ) /\ ( ( h ` i ) i^i ( ( mrCls ` ( SubGrp ` g ) ) ` U. ( h " ( dom h \ { i } ) ) ) ) = { ( 0g ` g ) } ) ) } ) --> _V )
29	26 28	mpbi	|- DProd : U_ g e. Grp ( { g } X. { h | ( h : dom h --> ( SubGrp ` g ) /\ A. i e. dom h ( A. y e. ( dom h \ { i } ) ( h ` i ) C_ ( ( Cntz ` g ) ` ( h ` y ) ) /\ ( ( h ` i ) i^i ( ( mrCls ` ( SubGrp ` g ) ) ` U. ( h " ( dom h \ { i } ) ) ) ) = { ( 0g ` g ) } ) ) } ) --> _V
30	29	fdmi	|- dom DProd = U_ g e. Grp ( { g } X. { h | ( h : dom h --> ( SubGrp ` g ) /\ A. i e. dom h ( A. y e. ( dom h \ { i } ) ( h ` i ) C_ ( ( Cntz ` g ) ` ( h ` y ) ) /\ ( ( h ` i ) i^i ( ( mrCls ` ( SubGrp ` g ) ) ` U. ( h " ( dom h \ { i } ) ) ) ) = { ( 0g ` g ) } ) ) } )
31	30	eleq2i	|- ( <. g , s >. e. dom DProd <-> <. g , s >. e. U_ g e. Grp ( { g } X. { h | ( h : dom h --> ( SubGrp ` g ) /\ A. i e. dom h ( A. y e. ( dom h \ { i } ) ( h ` i ) C_ ( ( Cntz ` g ) ` ( h ` y ) ) /\ ( ( h ` i ) i^i ( ( mrCls ` ( SubGrp ` g ) ) ` U. ( h " ( dom h \ { i } ) ) ) ) = { ( 0g ` g ) } ) ) } ) )
32		opeliunxp	|- ( <. g , s >. e. U_ g e. Grp ( { g } X. { h | ( h : dom h --> ( SubGrp ` g ) /\ A. i e. dom h ( A. y e. ( dom h \ { i } ) ( h ` i ) C_ ( ( Cntz ` g ) ` ( h ` y ) ) /\ ( ( h ` i ) i^i ( ( mrCls ` ( SubGrp ` g ) ) ` U. ( h " ( dom h \ { i } ) ) ) ) = { ( 0g ` g ) } ) ) } ) <-> ( g e. Grp /\ s e. { h | ( h : dom h --> ( SubGrp ` g ) /\ A. i e. dom h ( A. y e. ( dom h \ { i } ) ( h ` i ) C_ ( ( Cntz ` g ) ` ( h ` y ) ) /\ ( ( h ` i ) i^i ( ( mrCls ` ( SubGrp ` g ) ) ` U. ( h " ( dom h \ { i } ) ) ) ) = { ( 0g ` g ) } ) ) } ) )
33	19 31 32	3bitri	|- ( g dom DProd s <-> ( g e. Grp /\ s e. { h | ( h : dom h --> ( SubGrp ` g ) /\ A. i e. dom h ( A. y e. ( dom h \ { i } ) ( h ` i ) C_ ( ( Cntz ` g ) ` ( h ` y ) ) /\ ( ( h ` i ) i^i ( ( mrCls ` ( SubGrp ` g ) ) ` U. ( h " ( dom h \ { i } ) ) ) ) = { ( 0g ` g ) } ) ) } ) )
34	27	ovmpt4g	|- ( ( g e. Grp /\ s e. { h | ( h : dom h --> ( SubGrp ` g ) /\ A. i e. dom h ( A. y e. ( dom h \ { i } ) ( h ` i ) C_ ( ( Cntz ` g ) ` ( h ` y ) ) /\ ( ( h ` i ) i^i ( ( mrCls ` ( SubGrp ` g ) ) ` U. ( h " ( dom h \ { i } ) ) ) ) = { ( 0g ` g ) } ) ) } /\ ran ( f e. { h e. X_ i e. dom s ( s ` i ) | h finSupp ( 0g ` g ) } |-> ( g gsum f ) ) e. _V ) -> ( g DProd s ) = ran ( f e. { h e. X_ i e. dom s ( s ` i ) | h finSupp ( 0g ` g ) } |-> ( g gsum f ) ) )
35	25 34	mp3an3	|- ( ( g e. Grp /\ s e. { h | ( h : dom h --> ( SubGrp ` g ) /\ A. i e. dom h ( A. y e. ( dom h \ { i } ) ( h ` i ) C_ ( ( Cntz ` g ) ` ( h ` y ) ) /\ ( ( h ` i ) i^i ( ( mrCls ` ( SubGrp ` g ) ) ` U. ( h " ( dom h \ { i } ) ) ) ) = { ( 0g ` g ) } ) ) } ) -> ( g DProd s ) = ran ( f e. { h e. X_ i e. dom s ( s ` i ) | h finSupp ( 0g ` g ) } |-> ( g gsum f ) ) )
36	33 35	sylbi	|- ( g dom DProd s -> ( g DProd s ) = ran ( f e. { h e. X_ i e. dom s ( s ` i ) | h finSupp ( 0g ` g ) } |-> ( g gsum f ) ) )
37	18 36	vtoclg	|- ( G e. _V -> ( G dom DProd s -> ( G DProd s ) = ran ( f e. { h e. X_ i e. dom s ( s ` i ) | h finSupp .0. } |-> ( G gsum f ) ) ) )
38	7 37	mpcom	|- ( G dom DProd s -> ( G DProd s ) = ran ( f e. { h e. X_ i e. dom s ( s ` i ) | h finSupp .0. } |-> ( G gsum f ) ) )
39	38	sbcth	|- ( S e. _V -> [. S / s ]. ( G dom DProd s -> ( G DProd s ) = ran ( f e. { h e. X_ i e. dom s ( s ` i ) | h finSupp .0. } |-> ( G gsum f ) ) ) )
40	6 39	syl	|- ( ( G dom DProd S /\ dom S = I ) -> [. S / s ]. ( G dom DProd s -> ( G DProd s ) = ran ( f e. { h e. X_ i e. dom s ( s ` i ) | h finSupp .0. } |-> ( G gsum f ) ) ) )
41		simpr	|- ( ( ( G dom DProd S /\ dom S = I ) /\ s = S ) -> s = S )
42	41	breq2d	|- ( ( ( G dom DProd S /\ dom S = I ) /\ s = S ) -> ( G dom DProd s <-> G dom DProd S ) )
43	41	oveq2d	|- ( ( ( G dom DProd S /\ dom S = I ) /\ s = S ) -> ( G DProd s ) = ( G DProd S ) )
44	41	dmeqd	|- ( ( ( G dom DProd S /\ dom S = I ) /\ s = S ) -> dom s = dom S )
45		simplr	|- ( ( ( G dom DProd S /\ dom S = I ) /\ s = S ) -> dom S = I )
46	44 45	eqtrd	|- ( ( ( G dom DProd S /\ dom S = I ) /\ s = S ) -> dom s = I )
47	46	ixpeq1d	|- ( ( ( G dom DProd S /\ dom S = I ) /\ s = S ) -> X_ i e. dom s ( s ` i ) = X_ i e. I ( s ` i ) )
48	41	fveq1d	|- ( ( ( G dom DProd S /\ dom S = I ) /\ s = S ) -> ( s ` i ) = ( S ` i ) )
49	48	ixpeq2dv	|- ( ( ( G dom DProd S /\ dom S = I ) /\ s = S ) -> X_ i e. I ( s ` i ) = X_ i e. I ( S ` i ) )
50	47 49	eqtrd	|- ( ( ( G dom DProd S /\ dom S = I ) /\ s = S ) -> X_ i e. dom s ( s ` i ) = X_ i e. I ( S ` i ) )
51	50	rabeqdv	|- ( ( ( G dom DProd S /\ dom S = I ) /\ s = S ) -> { h e. X_ i e. dom s ( s ` i ) | h finSupp .0. } = { h e. X_ i e. I ( S ` i ) | h finSupp .0. } )
52	51 2	eqtr4di	|- ( ( ( G dom DProd S /\ dom S = I ) /\ s = S ) -> { h e. X_ i e. dom s ( s ` i ) | h finSupp .0. } = W )
53		eqidd	|- ( ( ( G dom DProd S /\ dom S = I ) /\ s = S ) -> ( G gsum f ) = ( G gsum f ) )
54	52 53	mpteq12dv	|- ( ( ( G dom DProd S /\ dom S = I ) /\ s = S ) -> ( f e. { h e. X_ i e. dom s ( s ` i ) | h finSupp .0. } |-> ( G gsum f ) ) = ( f e. W |-> ( G gsum f ) ) )
55	54	rneqd	|- ( ( ( G dom DProd S /\ dom S = I ) /\ s = S ) -> ran ( f e. { h e. X_ i e. dom s ( s ` i ) | h finSupp .0. } |-> ( G gsum f ) ) = ran ( f e. W |-> ( G gsum f ) ) )
56	43 55	eqeq12d	|- ( ( ( G dom DProd S /\ dom S = I ) /\ s = S ) -> ( ( G DProd s ) = ran ( f e. { h e. X_ i e. dom s ( s ` i ) | h finSupp .0. } |-> ( G gsum f ) ) <-> ( G DProd S ) = ran ( f e. W |-> ( G gsum f ) ) ) )
57	42 56	imbi12d	|- ( ( ( G dom DProd S /\ dom S = I ) /\ s = S ) -> ( ( G dom DProd s -> ( G DProd s ) = ran ( f e. { h e. X_ i e. dom s ( s ` i ) | h finSupp .0. } |-> ( G gsum f ) ) ) <-> ( G dom DProd S -> ( G DProd S ) = ran ( f e. W |-> ( G gsum f ) ) ) ) )
58	6 57	sbcied	|- ( ( G dom DProd S /\ dom S = I ) -> ( [. S / s ]. ( G dom DProd s -> ( G DProd s ) = ran ( f e. { h e. X_ i e. dom s ( s ` i ) | h finSupp .0. } |-> ( G gsum f ) ) ) <-> ( G dom DProd S -> ( G DProd S ) = ran ( f e. W |-> ( G gsum f ) ) ) ) )
59	40 58	mpbid	|- ( ( G dom DProd S /\ dom S = I ) -> ( G dom DProd S -> ( G DProd S ) = ran ( f e. W |-> ( G gsum f ) ) ) )
60	3 59	mpd	|- ( ( G dom DProd S /\ dom S = I ) -> ( G DProd S ) = ran ( f e. W |-> ( G gsum f ) ) )