dprdsubg

Description: The internal direct product of a family of subgroups is a subgroup. (Contributed by Mario Carneiro, 25-Apr-2016)

		Ref	Expression
	Assertion	dprdsubg	$⊢ G dom DProd S \to G DProd S \in SubGrp (G)$

Proof

Step	Hyp	Ref	Expression
1		eqid	$⊢ {Base}_{G} = {Base}_{G}$
2	1	dprdssv	$⊢ G DProd S \subseteq {Base}_{G}$
3	2	a1i	$⊢ G dom DProd S \to G DProd S \subseteq {Base}_{G}$
4		eqid	$⊢ 0_{G} = 0_{G}$
5		eqid	$⊢ \{h \in \underset{i \in dom S}{⨉} S (i) \| {finSupp}_{0_{G}} (h)\} = \{h \in \underset{i \in dom S}{⨉} S (i) \| {finSupp}_{0_{G}} (h)\}$
6		id	$⊢ G dom DProd S \to G dom DProd S$
7		eqidd	$⊢ G dom DProd S \to dom S = dom S$
8		fvex	$⊢ 0_{G} \in V$
9		fnconstg	$⊢ 0_{G} \in V \to (dom S \times \{0_{G}\}) Fn dom S$
10	8 9	mp1i	$⊢ G dom DProd S \to (dom S \times \{0_{G}\}) Fn dom S$
11	8	fvconst2	$⊢ k \in dom S \to (dom S \times \{0_{G}\}) (k) = 0_{G}$
12	11	adantl	$⊢ (G dom DProd S \land k \in dom S) \to (dom S \times \{0_{G}\}) (k) = 0_{G}$
13		dprdf	$⊢ G dom DProd S \to S : dom S ⟶ SubGrp (G)$
14	13	ffvelcdmda	$⊢ (G dom DProd S \land k \in dom S) \to S (k) \in SubGrp (G)$
15	4	subg0cl	$⊢ S (k) \in SubGrp (G) \to 0_{G} \in S (k)$
16	14 15	syl	$⊢ (G dom DProd S \land k \in dom S) \to 0_{G} \in S (k)$
17	12 16	eqeltrd	$⊢ (G dom DProd S \land k \in dom S) \to (dom S \times \{0_{G}\}) (k) \in S (k)$
18	17	ralrimiva	$⊢ G dom DProd S \to \forall k \in dom S (dom S \times \{0_{G}\}) (k) \in S (k)$
19		df-nel	$⊢ dom S \notin V \leftrightarrow \neg dom S \in V$
20		dprddomprc	$⊢ dom S \notin V \to \neg G dom DProd S$
21	19 20	sylbir	$⊢ \neg dom S \in V \to \neg G dom DProd S$
22	21	con4i	$⊢ G dom DProd S \to dom S \in V$
23	8	a1i	$⊢ G dom DProd S \to 0_{G} \in V$
24	22 23	fczfsuppd	$⊢ G dom DProd S \to {finSupp}_{0_{G}} ((dom S \times \{0_{G}\}))$
25	5 6 7	dprdw	$⊢ G dom DProd S \to (dom S \times \{0_{G}\} \in \{h \in \underset{i \in dom S}{⨉} S (i) \| {finSupp}_{0_{G}} (h)\} \leftrightarrow ((dom S \times \{0_{G}\}) Fn dom S \land \forall k \in dom S (dom S \times \{0_{G}\}) (k) \in S (k) \land {finSupp}_{0_{G}} ((dom S \times \{0_{G}\}))))$
26	10 18 24 25	mpbir3and	$⊢ G dom DProd S \to dom S \times \{0_{G}\} \in \{h \in \underset{i \in dom S}{⨉} S (i) \| {finSupp}_{0_{G}} (h)\}$
27	4 5 6 7 26	eldprdi	$⊢ G dom DProd S \to \sum_{G} (dom S \times \{0_{G}\}) \in (G DProd S)$
28	27	ne0d	$⊢ G dom DProd S \to G DProd S \neq \emptyset$
29		eqid	$⊢ dom S = dom S$
30	4 5	eldprd	$⊢ dom S = dom S \to (x \in (G DProd S) \leftrightarrow (G dom DProd S \land \exists f \in \{h \in \underset{i \in dom S}{⨉} S (i) \| {finSupp}_{0_{G}} (h)\} x = \sum_{G} f))$
31	30	baibd	$⊢ (dom S = dom S \land G dom DProd S) \to (x \in (G DProd S) \leftrightarrow \exists f \in \{h \in \underset{i \in dom S}{⨉} S (i) \| {finSupp}_{0_{G}} (h)\} x = \sum_{G} f)$
32	4 5	eldprd	$⊢ dom S = dom S \to (y \in (G DProd S) \leftrightarrow (G dom DProd S \land \exists g \in \{h \in \underset{i \in dom S}{⨉} S (i) \| {finSupp}_{0_{G}} (h)\} y = \sum_{G} g))$
33	32	baibd	$⊢ (dom S = dom S \land G dom DProd S) \to (y \in (G DProd S) \leftrightarrow \exists g \in \{h \in \underset{i \in dom S}{⨉} S (i) \| {finSupp}_{0_{G}} (h)\} y = \sum_{G} g)$
34	31 33	anbi12d	$⊢ (dom S = dom S \land G dom DProd S) \to ((x \in (G DProd S) \land y \in (G DProd S)) \leftrightarrow (\exists f \in \{h \in \underset{i \in dom S}{⨉} S (i) \| {finSupp}_{0_{G}} (h)\} x = \sum_{G} f \land \exists g \in \{h \in \underset{i \in dom S}{⨉} S (i) \| {finSupp}_{0_{G}} (h)\} y = \sum_{G} g))$
35	29 34	mpan	$⊢ G dom DProd S \to ((x \in (G DProd S) \land y \in (G DProd S)) \leftrightarrow (\exists f \in \{h \in \underset{i \in dom S}{⨉} S (i) \| {finSupp}_{0_{G}} (h)\} x = \sum_{G} f \land \exists g \in \{h \in \underset{i \in dom S}{⨉} S (i) \| {finSupp}_{0_{G}} (h)\} y = \sum_{G} g))$
36		reeanv	$⊢ \exists f \in \{h \in \underset{i \in dom S}{⨉} S (i) \| {finSupp}_{0_{G}} (h)\} \exists g \in \{h \in \underset{i \in dom S}{⨉} S (i) \| {finSupp}_{0_{G}} (h)\} (x = \sum_{G} f \land y = \sum_{G} g) \leftrightarrow (\exists f \in \{h \in \underset{i \in dom S}{⨉} S (i) \| {finSupp}_{0_{G}} (h)\} x = \sum_{G} f \land \exists g \in \{h \in \underset{i \in dom S}{⨉} S (i) \| {finSupp}_{0_{G}} (h)\} y = \sum_{G} g)$
37		simpl	$⊢ (G dom DProd S \land (f \in \{h \in \underset{i \in dom S}{⨉} S (i) \| {finSupp}_{0_{G}} (h)\} \land g \in \{h \in \underset{i \in dom S}{⨉} S (i) \| {finSupp}_{0_{G}} (h)\})) \to G dom DProd S$
38		eqidd	$⊢ (G dom DProd S \land (f \in \{h \in \underset{i \in dom S}{⨉} S (i) \| {finSupp}_{0_{G}} (h)\} \land g \in \{h \in \underset{i \in dom S}{⨉} S (i) \| {finSupp}_{0_{G}} (h)\})) \to dom S = dom S$
39		simprl	$⊢ (G dom DProd S \land (f \in \{h \in \underset{i \in dom S}{⨉} S (i) \| {finSupp}_{0_{G}} (h)\} \land g \in \{h \in \underset{i \in dom S}{⨉} S (i) \| {finSupp}_{0_{G}} (h)\})) \to f \in \{h \in \underset{i \in dom S}{⨉} S (i) \| {finSupp}_{0_{G}} (h)\}$
40		simprr	$⊢ (G dom DProd S \land (f \in \{h \in \underset{i \in dom S}{⨉} S (i) \| {finSupp}_{0_{G}} (h)\} \land g \in \{h \in \underset{i \in dom S}{⨉} S (i) \| {finSupp}_{0_{G}} (h)\})) \to g \in \{h \in \underset{i \in dom S}{⨉} S (i) \| {finSupp}_{0_{G}} (h)\}$
41		eqid	$⊢ -_{G} = -_{G}$
42	4 5 37 38 39 40 41	dprdfsub	$⊢ (G dom DProd S \land (f \in \{h \in \underset{i \in dom S}{⨉} S (i) \| {finSupp}_{0_{G}} (h)\} \land g \in \{h \in \underset{i \in dom S}{⨉} S (i) \| {finSupp}_{0_{G}} (h)\})) \to (f {-_{G}}_{f} g \in \{h \in \underset{i \in dom S}{⨉} S (i) \| {finSupp}_{0_{G}} (h)\} \land \sum_{G} (f {-_{G}}_{f} g) = (\sum_{G}, f) -_{G} (\sum_{G}, g))$
43	42	simprd	$⊢ (G dom DProd S \land (f \in \{h \in \underset{i \in dom S}{⨉} S (i) \| {finSupp}_{0_{G}} (h)\} \land g \in \{h \in \underset{i \in dom S}{⨉} S (i) \| {finSupp}_{0_{G}} (h)\})) \to \sum_{G} (f {-_{G}}_{f} g) = (\sum_{G}, f) -_{G} (\sum_{G}, g)$
44	42	simpld	$⊢ (G dom DProd S \land (f \in \{h \in \underset{i \in dom S}{⨉} S (i) \| {finSupp}_{0_{G}} (h)\} \land g \in \{h \in \underset{i \in dom S}{⨉} S (i) \| {finSupp}_{0_{G}} (h)\})) \to f {-_{G}}_{f} g \in \{h \in \underset{i \in dom S}{⨉} S (i) \| {finSupp}_{0_{G}} (h)\}$
45	4 5 37 38 44	eldprdi	$⊢ (G dom DProd S \land (f \in \{h \in \underset{i \in dom S}{⨉} S (i) \| {finSupp}_{0_{G}} (h)\} \land g \in \{h \in \underset{i \in dom S}{⨉} S (i) \| {finSupp}_{0_{G}} (h)\})) \to \sum_{G} (f {-_{G}}_{f} g) \in (G DProd S)$
46	43 45	eqeltrrd	$⊢ (G dom DProd S \land (f \in \{h \in \underset{i \in dom S}{⨉} S (i) \| {finSupp}_{0_{G}} (h)\} \land g \in \{h \in \underset{i \in dom S}{⨉} S (i) \| {finSupp}_{0_{G}} (h)\})) \to (\sum_{G}, f) -_{G} (\sum_{G}, g) \in (G DProd S)$
47		oveq12	$⊢ (x = \sum_{G} f \land y = \sum_{G} g) \to x -_{G} y = (\sum_{G}, f) -_{G} (\sum_{G}, g)$
48	47	eleq1d	$⊢ (x = \sum_{G} f \land y = \sum_{G} g) \to (x -_{G} y \in (G DProd S) \leftrightarrow (\sum_{G}, f) -_{G} (\sum_{G}, g) \in (G DProd S))$
49	46 48	syl5ibrcom	$⊢ (G dom DProd S \land (f \in \{h \in \underset{i \in dom S}{⨉} S (i) \| {finSupp}_{0_{G}} (h)\} \land g \in \{h \in \underset{i \in dom S}{⨉} S (i) \| {finSupp}_{0_{G}} (h)\})) \to ((x = \sum_{G} f \land y = \sum_{G} g) \to x -_{G} y \in (G DProd S))$
50	49	rexlimdvva	$⊢ G dom DProd S \to (\exists f \in \{h \in \underset{i \in dom S}{⨉} S (i) \| {finSupp}_{0_{G}} (h)\} \exists g \in \{h \in \underset{i \in dom S}{⨉} S (i) \| {finSupp}_{0_{G}} (h)\} (x = \sum_{G} f \land y = \sum_{G} g) \to x -_{G} y \in (G DProd S))$
51	36 50	biimtrrid	$⊢ G dom DProd S \to ((\exists f \in \{h \in \underset{i \in dom S}{⨉} S (i) \| {finSupp}_{0_{G}} (h)\} x = \sum_{G} f \land \exists g \in \{h \in \underset{i \in dom S}{⨉} S (i) \| {finSupp}_{0_{G}} (h)\} y = \sum_{G} g) \to x -_{G} y \in (G DProd S))$
52	35 51	sylbid	$⊢ G dom DProd S \to ((x \in (G DProd S) \land y \in (G DProd S)) \to x -_{G} y \in (G DProd S))$
53	52	ralrimivv	$⊢ G dom DProd S \to \forall x \in (G DProd S) \forall y \in (G DProd S) x -_{G} y \in (G DProd S)$
54		dprdgrp	$⊢ G dom DProd S \to G \in Grp$
55	1 41	issubg4	$⊢ G \in Grp \to (G DProd S \in SubGrp (G) \leftrightarrow (G DProd S \subseteq {Base}_{G} \land G DProd S \neq \emptyset \land \forall x \in (G DProd S) \forall y \in (G DProd S) x -_{G} y \in (G DProd S)))$
56	54 55	syl	$⊢ G dom DProd S \to (G DProd S \in SubGrp (G) \leftrightarrow (G DProd S \subseteq {Base}_{G} \land G DProd S \neq \emptyset \land \forall x \in (G DProd S) \forall y \in (G DProd S) x -_{G} y \in (G DProd S)))$
57	3 28 53 56	mpbir3and	$⊢ G dom DProd S \to G DProd S \in SubGrp (G)$

Metamath Proof Explorer

Theorem dprdsubg

Proof