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 ˙ = 0 G
dprdval.w W = h i I S i | finSupp 0 ˙ h
Assertion dprdval G dom DProd S dom S = I G DProd S = ran f W G f

Proof

Step Hyp Ref Expression
1 dprdval.0 0 ˙ = 0 G
2 dprdval.w W = h i I S i | finSupp 0 ˙ h
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 V
6 5 adantr G dom DProd S dom S = I S V
7 4 brrelex1i G dom DProd s G 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 0 g = 0 G
11 10 1 eqtr4di g = G 0 g = 0 ˙
12 11 breq2d g = G finSupp 0 g h finSupp 0 ˙ h
13 12 rabbidv g = G h i dom s s i | finSupp 0 g h = h i dom s s i | finSupp 0 ˙ h
14 oveq1 g = G g f = G f
15 13 14 mpteq12dv g = G f h i dom s s i | finSupp 0 g h g f = f h i dom s s i | finSupp 0 ˙ h G f
16 15 rneqd g = G ran f h i dom s s i | finSupp 0 g h g f = ran f h i dom s s i | finSupp 0 ˙ h G f
17 9 16 eqeq12d g = G g DProd s = ran f h i dom s s i | finSupp 0 g h g f G DProd s = ran f h i dom s s i | finSupp 0 ˙ h G f
18 8 17 imbi12d g = G g dom DProd s g DProd s = ran f h i dom s s i | finSupp 0 g h g f G dom DProd s G DProd s = ran f h i dom s s i | finSupp 0 ˙ h G f
19 df-br g dom DProd s g s dom DProd
20 fvex s i V
21 20 rgenw i dom s s i V
22 ixpexg i dom s s i V i dom s s i V
23 21 22 ax-mp i dom s s i V
24 23 mptrabex f h i dom s s i | finSupp 0 g h g f V
25 24 rnex ran f h i dom s s i | finSupp 0 g h g f V
26 25 rgen2w g Grp s h | h : dom h SubGrp g i dom h y dom h i h i Cntz g h y h i mrCls SubGrp g h dom h i = 0 g ran f h i dom s s i | finSupp 0 g h g f V
27 df-dprd DProd = g Grp , s h | h : dom h SubGrp g i dom h y dom h i h i Cntz g h y h i mrCls SubGrp g h dom h i = 0 g ran f h i dom s s i | finSupp 0 g h g f
28 27 fmpox g Grp s h | h : dom h SubGrp g i dom h y dom h i h i Cntz g h y h i mrCls SubGrp g h dom h i = 0 g ran f h i dom s s i | finSupp 0 g h g f V DProd : g Grp g × h | h : dom h SubGrp g i dom h y dom h i h i Cntz g h y h i mrCls SubGrp g h dom h i = 0 g V
29 26 28 mpbi DProd : g Grp g × h | h : dom h SubGrp g i dom h y dom h i h i Cntz g h y h i mrCls SubGrp g h dom h i = 0 g V
30 29 fdmi dom DProd = g Grp g × h | h : dom h SubGrp g i dom h y dom h i h i Cntz g h y h i mrCls SubGrp g h dom h i = 0 g
31 30 eleq2i g s dom DProd g s g Grp g × h | h : dom h SubGrp g i dom h y dom h i h i Cntz g h y h i mrCls SubGrp g h dom h i = 0 g
32 opeliunxp g s g Grp g × h | h : dom h SubGrp g i dom h y dom h i h i Cntz g h y h i mrCls SubGrp g h dom h i = 0 g g Grp s h | h : dom h SubGrp g i dom h y dom h i h i Cntz g h y h i mrCls SubGrp g h dom h i = 0 g
33 19 31 32 3bitri g dom DProd s g Grp s h | h : dom h SubGrp g i dom h y dom h i h i Cntz g h y h i mrCls SubGrp g h dom h i = 0 g
34 27 ovmpt4g g Grp s h | h : dom h SubGrp g i dom h y dom h i h i Cntz g h y h i mrCls SubGrp g h dom h i = 0 g ran f h i dom s s i | finSupp 0 g h g f V g DProd s = ran f h i dom s s i | finSupp 0 g h g f
35 25 34 mp3an3 g Grp s h | h : dom h SubGrp g i dom h y dom h i h i Cntz g h y h i mrCls SubGrp g h dom h i = 0 g g DProd s = ran f h i dom s s i | finSupp 0 g h g f
36 33 35 sylbi g dom DProd s g DProd s = ran f h i dom s s i | finSupp 0 g h g f
37 18 36 vtoclg G V G dom DProd s G DProd s = ran f h i dom s s i | finSupp 0 ˙ h G f
38 7 37 mpcom G dom DProd s G DProd s = ran f h i dom s s i | finSupp 0 ˙ h G f
39 38 sbcth S V [˙S / s]˙ G dom DProd s G DProd s = ran f h i dom s s i | finSupp 0 ˙ h G f
40 6 39 syl G dom DProd S dom S = I [˙S / s]˙ G dom DProd s G DProd s = ran f h i dom s s i | finSupp 0 ˙ h G 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 i dom s s i = i 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 i I s i = i I S i
50 47 49 eqtrd G dom DProd S dom S = I s = S i dom s s i = i I S i
51 50 rabeqdv G dom DProd S dom S = I s = S h i dom s s i | finSupp 0 ˙ h = h i I S i | finSupp 0 ˙ h
52 51 2 eqtr4di G dom DProd S dom S = I s = S h i dom s s i | finSupp 0 ˙ h = W
53 eqidd G dom DProd S dom S = I s = S G f = G f
54 52 53 mpteq12dv G dom DProd S dom S = I s = S f h i dom s s i | finSupp 0 ˙ h G f = f W G f
55 54 rneqd G dom DProd S dom S = I s = S ran f h i dom s s i | finSupp 0 ˙ h G f = ran f W G f
56 43 55 eqeq12d G dom DProd S dom S = I s = S G DProd s = ran f h i dom s s i | finSupp 0 ˙ h G f G DProd S = ran f W G f
57 42 56 imbi12d G dom DProd S dom S = I s = S G dom DProd s G DProd s = ran f h i dom s s i | finSupp 0 ˙ h G f G dom DProd S G DProd S = ran f W G f
58 6 57 sbcied G dom DProd S dom S = I [˙S / s]˙ G dom DProd s G DProd s = ran f h i dom s s i | finSupp 0 ˙ h G f G dom DProd S G DProd S = ran f W G f
59 40 58 mpbid G dom DProd S dom S = I G dom DProd S G DProd S = ran f W G f
60 3 59 mpd G dom DProd S dom S = I G DProd S = ran f W G f