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	$⊢ \underset{˙}{0} = 0_{G}$
	dprdval.w	$⊢ W = \{h \in \underset{i \in I}{⨉} S (i) \| {finSupp}_{\underset{˙}{0}} (h)\}$
Assertion	dprdval	$⊢ (G dom DProd S \land dom S = I) \to G DProd S = ran (f \in W ⟼ \sum_{G} f)$

Proof

Step	Hyp	Ref	Expression
1		dprdval.0	$⊢ \underset{˙}{0} = 0_{G}$
2		dprdval.w	$⊢ W = \{h \in \underset{i \in I}{⨉} S (i) \| {finSupp}_{\underset{˙}{0}} (h)\}$
3		simpl	$⊢ (G dom DProd S \land dom S = I) \to G dom DProd S$
4		reldmdprd	$⊢ Rel dom DProd$
5	4	brrelex2i	$⊢ G dom DProd S \to S \in V$
6	5	adantr	$⊢ (G dom DProd S \land dom S = I) \to S \in V$
7	4	brrelex1i	$⊢ G dom DProd s \to G \in V$
8		breq1	$⊢ g = G \to (g dom DProd s \leftrightarrow G dom DProd s)$
9		oveq1	$⊢ g = G \to g DProd s = G DProd s$
10		fveq2	$⊢ g = G \to 0_{g} = 0_{G}$
11	10 1	syl6eqr	$⊢ g = G \to 0_{g} = \underset{˙}{0}$
12	11	breq2d	$⊢ g = G \to ({finSupp}_{0_{g}} (h) \leftrightarrow {finSupp}_{\underset{˙}{0}} (h))$
13	12	rabbidv	$⊢ g = G \to \{h \in \underset{i \in dom s}{⨉} s (i) \| {finSupp}_{0_{g}} (h)\} = \{h \in \underset{i \in dom s}{⨉} s (i) \| {finSupp}_{\underset{˙}{0}} (h)\}$
14		oveq1	$⊢ g = G \to \sum_{g} f = \sum_{G} f$
15	13 14	mpteq12dv	$⊢ g = G \to (f \in \{h \in \underset{i \in dom s}{⨉} s (i) \| {finSupp}_{0_{g}} (h)\} ⟼ \sum_{g} f) = (f \in \{h \in \underset{i \in dom s}{⨉} s (i) \| {finSupp}_{\underset{˙}{0}} (h)\} ⟼ \sum_{G} f)$
16	15	rneqd	$⊢ g = G \to ran (f \in \{h \in \underset{i \in dom s}{⨉} s (i) \| {finSupp}_{0_{g}} (h)\} ⟼ \sum_{g} f) = ran (f \in \{h \in \underset{i \in dom s}{⨉} s (i) \| {finSupp}_{\underset{˙}{0}} (h)\} ⟼ \sum_{G} f)$
17	9 16	eqeq12d	$⊢ g = G \to (g DProd s = ran (f \in \{h \in \underset{i \in dom s}{⨉} s (i) \| {finSupp}_{0_{g}} (h)\} ⟼ \sum_{g} f) \leftrightarrow G DProd s = ran (f \in \{h \in \underset{i \in dom s}{⨉} s (i) \| {finSupp}_{\underset{˙}{0}} (h)\} ⟼ \sum_{G} f))$
18	8 17	imbi12d	$⊢ g = G \to ((g dom DProd s \to g DProd s = ran (f \in \{h \in \underset{i \in dom s}{⨉} s (i) \| {finSupp}_{0_{g}} (h)\} ⟼ \sum_{g} f)) \leftrightarrow (G dom DProd s \to G DProd s = ran (f \in \{h \in \underset{i \in dom s}{⨉} s (i) \| {finSupp}_{\underset{˙}{0}} (h)\} ⟼ \sum_{G} f)))$
19		df-br	$⊢ g dom DProd s \leftrightarrow ⟨g, s⟩ \in dom DProd$
20		fvex	$⊢ s (i) \in V$
21	20	rgenw	$⊢ \forall i \in dom s s (i) \in V$
22		ixpexg	$⊢ \forall i \in dom s s (i) \in V \to \underset{i \in dom s}{⨉} s (i) \in V$
23	21 22	ax-mp	$⊢ \underset{i \in dom s}{⨉} s (i) \in V$
24	23	mptrabex	$⊢ (f \in \{h \in \underset{i \in dom s}{⨉} s (i) \| {finSupp}_{0_{g}} (h)\} ⟼ \sum_{g} f) \in V$
25	24	rnex	$⊢ ran (f \in \{h \in \underset{i \in dom s}{⨉} s (i) \| {finSupp}_{0_{g}} (h)\} ⟼ \sum_{g} f) \in V$
26	25	rgen2w	$⊢ \forall g \in Grp \forall s \in \{h \| (h : dom h ⟶ SubGrp (g) \land \forall i \in dom h (\forall y \in (dom h ∖ \{i\}) h (i) \subseteq Cntz (g) (h (y)) \land h (i) \cap mrCls (SubGrp (g)) (⋃ h [dom h ∖ \{i\}]) = \{0_{g}\}))\} ran (f \in \{h \in \underset{i \in dom s}{⨉} s (i) \| {finSupp}_{0_{g}} (h)\} ⟼ \sum_{g} f) \in V$
27		df-dprd	$⊢ DProd = (g \in Grp, s \in \{h \| (h : dom h ⟶ SubGrp (g) \land \forall i \in dom h (\forall y \in (dom h ∖ \{i\}) h (i) \subseteq Cntz (g) (h (y)) \land h (i) \cap mrCls (SubGrp (g)) (⋃ h [dom h ∖ \{i\}]) = \{0_{g}\}))\} ⟼ ran (f \in \{h \in \underset{i \in dom s}{⨉} s (i) \| {finSupp}_{0_{g}} (h)\} ⟼ \sum_{g} f))$
28	27	fmpox	$⊢ \forall g \in Grp \forall s \in \{h \| (h : dom h ⟶ SubGrp (g) \land \forall i \in dom h (\forall y \in (dom h ∖ \{i\}) h (i) \subseteq Cntz (g) (h (y)) \land h (i) \cap mrCls (SubGrp (g)) (⋃ h [dom h ∖ \{i\}]) = \{0_{g}\}))\} ran (f \in \{h \in \underset{i \in dom s}{⨉} s (i) \| {finSupp}_{0_{g}} (h)\} ⟼ \sum_{g} f) \in V \leftrightarrow DProd : ⋃_{g \in Grp} (\{g\} \times \{h \| (h : dom h ⟶ SubGrp (g) \land \forall i \in dom h (\forall y \in (dom h ∖ \{i\}) h (i) \subseteq Cntz (g) (h (y)) \land h (i) \cap mrCls (SubGrp (g)) (⋃ h [dom h ∖ \{i\}]) = \{0_{g}\}))\}) ⟶ V$
29	26 28	mpbi	$⊢ DProd : ⋃_{g \in Grp} (\{g\} \times \{h \| (h : dom h ⟶ SubGrp (g) \land \forall i \in dom h (\forall y \in (dom h ∖ \{i\}) h (i) \subseteq Cntz (g) (h (y)) \land h (i) \cap mrCls (SubGrp (g)) (⋃ h [dom h ∖ \{i\}]) = \{0_{g}\}))\}) ⟶ V$
30	29	fdmi	$⊢ dom DProd = ⋃_{g \in Grp} (\{g\} \times \{h \| (h : dom h ⟶ SubGrp (g) \land \forall i \in dom h (\forall y \in (dom h ∖ \{i\}) h (i) \subseteq Cntz (g) (h (y)) \land h (i) \cap mrCls (SubGrp (g)) (⋃ h [dom h ∖ \{i\}]) = \{0_{g}\}))\})$
31	30	eleq2i	$⊢ ⟨g, s⟩ \in dom DProd \leftrightarrow ⟨g, s⟩ \in ⋃_{g \in Grp} (\{g\} \times \{h \| (h : dom h ⟶ SubGrp (g) \land \forall i \in dom h (\forall y \in (dom h ∖ \{i\}) h (i) \subseteq Cntz (g) (h (y)) \land h (i) \cap mrCls (SubGrp (g)) (⋃ h [dom h ∖ \{i\}]) = \{0_{g}\}))\})$
32		opeliunxp	$⊢ ⟨g, s⟩ \in ⋃_{g \in Grp} (\{g\} \times \{h \| (h : dom h ⟶ SubGrp (g) \land \forall i \in dom h (\forall y \in (dom h ∖ \{i\}) h (i) \subseteq Cntz (g) (h (y)) \land h (i) \cap mrCls (SubGrp (g)) (⋃ h [dom h ∖ \{i\}]) = \{0_{g}\}))\}) \leftrightarrow (g \in Grp \land s \in \{h \| (h : dom h ⟶ SubGrp (g) \land \forall i \in dom h (\forall y \in (dom h ∖ \{i\}) h (i) \subseteq Cntz (g) (h (y)) \land h (i) \cap mrCls (SubGrp (g)) (⋃ h [dom h ∖ \{i\}]) = \{0_{g}\}))\})$
33	19 31 32	3bitri	$⊢ g dom DProd s \leftrightarrow (g \in Grp \land s \in \{h \| (h : dom h ⟶ SubGrp (g) \land \forall i \in dom h (\forall y \in (dom h ∖ \{i\}) h (i) \subseteq Cntz (g) (h (y)) \land h (i) \cap mrCls (SubGrp (g)) (⋃ h [dom h ∖ \{i\}]) = \{0_{g}\}))\})$
34	27	ovmpt4g	$⊢ (g \in Grp \land s \in \{h \| (h : dom h ⟶ SubGrp (g) \land \forall i \in dom h (\forall y \in (dom h ∖ \{i\}) h (i) \subseteq Cntz (g) (h (y)) \land h (i) \cap mrCls (SubGrp (g)) (⋃ h [dom h ∖ \{i\}]) = \{0_{g}\}))\} \land ran (f \in \{h \in \underset{i \in dom s}{⨉} s (i) \| {finSupp}_{0_{g}} (h)\} ⟼ \sum_{g} f) \in V) \to g DProd s = ran (f \in \{h \in \underset{i \in dom s}{⨉} s (i) \| {finSupp}_{0_{g}} (h)\} ⟼ \sum_{g} f)$
35	25 34	mp3an3	$⊢ (g \in Grp \land s \in \{h \| (h : dom h ⟶ SubGrp (g) \land \forall i \in dom h (\forall y \in (dom h ∖ \{i\}) h (i) \subseteq Cntz (g) (h (y)) \land h (i) \cap mrCls (SubGrp (g)) (⋃ h [dom h ∖ \{i\}]) = \{0_{g}\}))\}) \to g DProd s = ran (f \in \{h \in \underset{i \in dom s}{⨉} s (i) \| {finSupp}_{0_{g}} (h)\} ⟼ \sum_{g} f)$
36	33 35	sylbi	$⊢ g dom DProd s \to g DProd s = ran (f \in \{h \in \underset{i \in dom s}{⨉} s (i) \| {finSupp}_{0_{g}} (h)\} ⟼ \sum_{g} f)$
37	18 36	vtoclg	$⊢ G \in V \to (G dom DProd s \to G DProd s = ran (f \in \{h \in \underset{i \in dom s}{⨉} s (i) \| {finSupp}_{\underset{˙}{0}} (h)\} ⟼ \sum_{G} f))$
38	7 37	mpcom	$⊢ G dom DProd s \to G DProd s = ran (f \in \{h \in \underset{i \in dom s}{⨉} s (i) \| {finSupp}_{\underset{˙}{0}} (h)\} ⟼ \sum_{G} f)$
39	38	sbcth	$⊢ S \in V \to \underset{˙}{[} S / s \underset{˙}{]} (G dom DProd s \to G DProd s = ran (f \in \{h \in \underset{i \in dom s}{⨉} s (i) \| {finSupp}_{\underset{˙}{0}} (h)\} ⟼ \sum_{G} f))$
40	6 39	syl	$⊢ (G dom DProd S \land dom S = I) \to \underset{˙}{[} S / s \underset{˙}{]} (G dom DProd s \to G DProd s = ran (f \in \{h \in \underset{i \in dom s}{⨉} s (i) \| {finSupp}_{\underset{˙}{0}} (h)\} ⟼ \sum_{G} f))$
41		simpr	$⊢ ((G dom DProd S \land dom S = I) \land s = S) \to s = S$
42	41	breq2d	$⊢ ((G dom DProd S \land dom S = I) \land s = S) \to (G dom DProd s \leftrightarrow G dom DProd S)$
43	41	oveq2d	$⊢ ((G dom DProd S \land dom S = I) \land s = S) \to G DProd s = G DProd S$
44	41	dmeqd	$⊢ ((G dom DProd S \land dom S = I) \land s = S) \to dom s = dom S$
45		simplr	$⊢ ((G dom DProd S \land dom S = I) \land s = S) \to dom S = I$
46	44 45	eqtrd	$⊢ ((G dom DProd S \land dom S = I) \land s = S) \to dom s = I$
47	46	ixpeq1d	$⊢ ((G dom DProd S \land dom S = I) \land s = S) \to \underset{i \in dom s}{⨉} s (i) = \underset{i \in I}{⨉} s (i)$
48	41	fveq1d	$⊢ ((G dom DProd S \land dom S = I) \land s = S) \to s (i) = S (i)$
49	48	ixpeq2dv	$⊢ ((G dom DProd S \land dom S = I) \land s = S) \to \underset{i \in I}{⨉} s (i) = \underset{i \in I}{⨉} S (i)$
50	47 49	eqtrd	$⊢ ((G dom DProd S \land dom S = I) \land s = S) \to \underset{i \in dom s}{⨉} s (i) = \underset{i \in I}{⨉} S (i)$
51	50	rabeqdv	$⊢ ((G dom DProd S \land dom S = I) \land s = S) \to \{h \in \underset{i \in dom s}{⨉} s (i) \| {finSupp}_{\underset{˙}{0}} (h)\} = \{h \in \underset{i \in I}{⨉} S (i) \| {finSupp}_{\underset{˙}{0}} (h)\}$
52	51 2	syl6eqr	$⊢ ((G dom DProd S \land dom S = I) \land s = S) \to \{h \in \underset{i \in dom s}{⨉} s (i) \| {finSupp}_{\underset{˙}{0}} (h)\} = W$
53		eqidd	$⊢ ((G dom DProd S \land dom S = I) \land s = S) \to \sum_{G} f = \sum_{G} f$
54	52 53	mpteq12dv	$⊢ ((G dom DProd S \land dom S = I) \land s = S) \to (f \in \{h \in \underset{i \in dom s}{⨉} s (i) \| {finSupp}_{\underset{˙}{0}} (h)\} ⟼ \sum_{G} f) = (f \in W ⟼ \sum_{G} f)$
55	54	rneqd	$⊢ ((G dom DProd S \land dom S = I) \land s = S) \to ran (f \in \{h \in \underset{i \in dom s}{⨉} s (i) \| {finSupp}_{\underset{˙}{0}} (h)\} ⟼ \sum_{G} f) = ran (f \in W ⟼ \sum_{G} f)$
56	43 55	eqeq12d	$⊢ ((G dom DProd S \land dom S = I) \land s = S) \to (G DProd s = ran (f \in \{h \in \underset{i \in dom s}{⨉} s (i) \| {finSupp}_{\underset{˙}{0}} (h)\} ⟼ \sum_{G} f) \leftrightarrow G DProd S = ran (f \in W ⟼ \sum_{G} f))$
57	42 56	imbi12d	$⊢ ((G dom DProd S \land dom S = I) \land s = S) \to ((G dom DProd s \to G DProd s = ran (f \in \{h \in \underset{i \in dom s}{⨉} s (i) \| {finSupp}_{\underset{˙}{0}} (h)\} ⟼ \sum_{G} f)) \leftrightarrow (G dom DProd S \to G DProd S = ran (f \in W ⟼ \sum_{G} f)))$
58	6 57	sbcied	$⊢ (G dom DProd S \land dom S = I) \to (\underset{˙}{[} S / s \underset{˙}{]} (G dom DProd s \to G DProd s = ran (f \in \{h \in \underset{i \in dom s}{⨉} s (i) \| {finSupp}_{\underset{˙}{0}} (h)\} ⟼ \sum_{G} f)) \leftrightarrow (G dom DProd S \to G DProd S = ran (f \in W ⟼ \sum_{G} f)))$
59	40 58	mpbid	$⊢ (G dom DProd S \land dom S = I) \to (G dom DProd S \to G DProd S = ran (f \in W ⟼ \sum_{G} f))$
60	3 59	mpd	$⊢ (G dom DProd S \land dom S = I) \to G DProd S = ran (f \in W ⟼ \sum_{G} f)$

Metamath Proof Explorer

Theorem dprdval

Proof