This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ) ) )