dprdsplit

Description: The direct product is the binary subgroup product ("sum") of the direct products of the partition. (Contributed by Mario Carneiro, 25-Apr-2016)

	Ref	Expression
Hypotheses	dprdsplit.2	$⊢ φ \to S : I ⟶ SubGrp (G)$
	dprdsplit.i	$⊢ φ \to C \cap D = \emptyset$
	dprdsplit.u	$⊢ φ \to I = C \cup D$
	dprdsplit.s	$⊢ \underset{˙}{\oplus} = LSSum (G)$
	dprdsplit.1	$⊢ φ \to G dom DProd S$
Assertion	dprdsplit	$⊢ φ \to G DProd S = (G DProd ({S ↾}_{C})) \underset{˙}{\oplus} (G DProd ({S ↾}_{D}))$

Proof

Step	Hyp	Ref	Expression
1		dprdsplit.2	$⊢ φ \to S : I ⟶ SubGrp (G)$
2		dprdsplit.i	$⊢ φ \to C \cap D = \emptyset$
3		dprdsplit.u	$⊢ φ \to I = C \cup D$
4		dprdsplit.s	$⊢ \underset{˙}{\oplus} = LSSum (G)$
5		dprdsplit.1	$⊢ φ \to G dom DProd S$
6	1	fdmd	$⊢ φ \to dom S = I$
7		ssun1	$⊢ C \subseteq C \cup D$
8	7 3	sseqtrrid	$⊢ φ \to C \subseteq I$
9	5 6 8	dprdres	$⊢ φ \to (G dom DProd ({S ↾}_{C}) \land G DProd ({S ↾}_{C}) \subseteq G DProd S)$
10	9	simpld	$⊢ φ \to G dom DProd ({S ↾}_{C})$
11		dprdsubg	$⊢ G dom DProd ({S ↾}_{C}) \to G DProd ({S ↾}_{C}) \in SubGrp (G)$
12	10 11	syl	$⊢ φ \to G DProd ({S ↾}_{C}) \in SubGrp (G)$
13		ssun2	$⊢ D \subseteq C \cup D$
14	13 3	sseqtrrid	$⊢ φ \to D \subseteq I$
15	5 6 14	dprdres	$⊢ φ \to (G dom DProd ({S ↾}_{D}) \land G DProd ({S ↾}_{D}) \subseteq G DProd S)$
16	15	simpld	$⊢ φ \to G dom DProd ({S ↾}_{D})$
17		dprdsubg	$⊢ G dom DProd ({S ↾}_{D}) \to G DProd ({S ↾}_{D}) \in SubGrp (G)$
18	16 17	syl	$⊢ φ \to G DProd ({S ↾}_{D}) \in SubGrp (G)$
19		eqid	$⊢ Cntz (G) = Cntz (G)$
20		eqid	$⊢ 0_{G} = 0_{G}$
21	1 2 3 19 20	dmdprdsplit	$⊢ φ \to (G dom DProd S \leftrightarrow ((G dom DProd ({S ↾}_{C}) \land G dom DProd ({S ↾}_{D})) \land G DProd ({S ↾}_{C}) \subseteq Cntz (G) (G DProd ({S ↾}_{D})) \land (G DProd ({S ↾}_{C})) \cap (G DProd ({S ↾}_{D})) = \{0_{G}\}))$
22	5 21	mpbid	$⊢ φ \to ((G dom DProd ({S ↾}_{C}) \land G dom DProd ({S ↾}_{D})) \land G DProd ({S ↾}_{C}) \subseteq Cntz (G) (G DProd ({S ↾}_{D})) \land (G DProd ({S ↾}_{C})) \cap (G DProd ({S ↾}_{D})) = \{0_{G}\})$
23	22	simp2d	$⊢ φ \to G DProd ({S ↾}_{C}) \subseteq Cntz (G) (G DProd ({S ↾}_{D}))$
24	4 19	lsmsubg	$⊢ (G DProd ({S ↾}_{C}) \in SubGrp (G) \land G DProd ({S ↾}_{D}) \in SubGrp (G) \land G DProd ({S ↾}_{C}) \subseteq Cntz (G) (G DProd ({S ↾}_{D}))) \to (G DProd ({S ↾}_{C})) \underset{˙}{\oplus} (G DProd ({S ↾}_{D})) \in SubGrp (G)$
25	12 18 23 24	syl3anc	$⊢ φ \to (G DProd ({S ↾}_{C})) \underset{˙}{\oplus} (G DProd ({S ↾}_{D})) \in SubGrp (G)$
26	3	eleq2d	$⊢ φ \to (x \in I \leftrightarrow x \in (C \cup D))$
27		elun	$⊢ x \in (C \cup D) \leftrightarrow (x \in C \lor x \in D)$
28	26 27	bitrdi	$⊢ φ \to (x \in I \leftrightarrow (x \in C \lor x \in D))$
29	28	biimpa	$⊢ (φ \land x \in I) \to (x \in C \lor x \in D)$
30		fvres	$⊢ x \in C \to ({S ↾}_{C}) (x) = S (x)$
31	30	adantl	$⊢ (φ \land x \in C) \to ({S ↾}_{C}) (x) = S (x)$
32	10	adantr	$⊢ (φ \land x \in C) \to G dom DProd ({S ↾}_{C})$
33	1 8	fssresd	$⊢ φ \to ({S ↾}_{C}) : C ⟶ SubGrp (G)$
34	33	fdmd	$⊢ φ \to dom ({S ↾}_{C}) = C$
35	34	adantr	$⊢ (φ \land x \in C) \to dom ({S ↾}_{C}) = C$
36		simpr	$⊢ (φ \land x \in C) \to x \in C$
37	32 35 36	dprdub	$⊢ (φ \land x \in C) \to ({S ↾}_{C}) (x) \subseteq G DProd ({S ↾}_{C})$
38	31 37	eqsstrrd	$⊢ (φ \land x \in C) \to S (x) \subseteq G DProd ({S ↾}_{C})$
39	4	lsmub1	$⊢ (G DProd ({S ↾}_{C}) \in SubGrp (G) \land G DProd ({S ↾}_{D}) \in SubGrp (G)) \to G DProd ({S ↾}_{C}) \subseteq (G DProd ({S ↾}_{C})) \underset{˙}{\oplus} (G DProd ({S ↾}_{D}))$
40	12 18 39	syl2anc	$⊢ φ \to G DProd ({S ↾}_{C}) \subseteq (G DProd ({S ↾}_{C})) \underset{˙}{\oplus} (G DProd ({S ↾}_{D}))$
41	40	adantr	$⊢ (φ \land x \in C) \to G DProd ({S ↾}_{C}) \subseteq (G DProd ({S ↾}_{C})) \underset{˙}{\oplus} (G DProd ({S ↾}_{D}))$
42	38 41	sstrd	$⊢ (φ \land x \in C) \to S (x) \subseteq (G DProd ({S ↾}_{C})) \underset{˙}{\oplus} (G DProd ({S ↾}_{D}))$
43		fvres	$⊢ x \in D \to ({S ↾}_{D}) (x) = S (x)$
44	43	adantl	$⊢ (φ \land x \in D) \to ({S ↾}_{D}) (x) = S (x)$
45	16	adantr	$⊢ (φ \land x \in D) \to G dom DProd ({S ↾}_{D})$
46	1 14	fssresd	$⊢ φ \to ({S ↾}_{D}) : D ⟶ SubGrp (G)$
47	46	fdmd	$⊢ φ \to dom ({S ↾}_{D}) = D$
48	47	adantr	$⊢ (φ \land x \in D) \to dom ({S ↾}_{D}) = D$
49		simpr	$⊢ (φ \land x \in D) \to x \in D$
50	45 48 49	dprdub	$⊢ (φ \land x \in D) \to ({S ↾}_{D}) (x) \subseteq G DProd ({S ↾}_{D})$
51	44 50	eqsstrrd	$⊢ (φ \land x \in D) \to S (x) \subseteq G DProd ({S ↾}_{D})$
52	4	lsmub2	$⊢ (G DProd ({S ↾}_{C}) \in SubGrp (G) \land G DProd ({S ↾}_{D}) \in SubGrp (G)) \to G DProd ({S ↾}_{D}) \subseteq (G DProd ({S ↾}_{C})) \underset{˙}{\oplus} (G DProd ({S ↾}_{D}))$
53	12 18 52	syl2anc	$⊢ φ \to G DProd ({S ↾}_{D}) \subseteq (G DProd ({S ↾}_{C})) \underset{˙}{\oplus} (G DProd ({S ↾}_{D}))$
54	53	adantr	$⊢ (φ \land x \in D) \to G DProd ({S ↾}_{D}) \subseteq (G DProd ({S ↾}_{C})) \underset{˙}{\oplus} (G DProd ({S ↾}_{D}))$
55	51 54	sstrd	$⊢ (φ \land x \in D) \to S (x) \subseteq (G DProd ({S ↾}_{C})) \underset{˙}{\oplus} (G DProd ({S ↾}_{D}))$
56	42 55	jaodan	$⊢ (φ \land (x \in C \lor x \in D)) \to S (x) \subseteq (G DProd ({S ↾}_{C})) \underset{˙}{\oplus} (G DProd ({S ↾}_{D}))$
57	29 56	syldan	$⊢ (φ \land x \in I) \to S (x) \subseteq (G DProd ({S ↾}_{C})) \underset{˙}{\oplus} (G DProd ({S ↾}_{D}))$
58	5 6 25 57	dprdlub	$⊢ φ \to G DProd S \subseteq (G DProd ({S ↾}_{C})) \underset{˙}{\oplus} (G DProd ({S ↾}_{D}))$
59	9	simprd	$⊢ φ \to G DProd ({S ↾}_{C}) \subseteq G DProd S$
60	15	simprd	$⊢ φ \to G DProd ({S ↾}_{D}) \subseteq G DProd S$
61		dprdsubg	$⊢ G dom DProd S \to G DProd S \in SubGrp (G)$
62	5 61	syl	$⊢ φ \to G DProd S \in SubGrp (G)$
63	4	lsmlub	$⊢ (G DProd ({S ↾}_{C}) \in SubGrp (G) \land G DProd ({S ↾}_{D}) \in SubGrp (G) \land G DProd S \in SubGrp (G)) \to ((G DProd ({S ↾}_{C}) \subseteq G DProd S \land G DProd ({S ↾}_{D}) \subseteq G DProd S) \leftrightarrow (G DProd ({S ↾}_{C})) \underset{˙}{\oplus} (G DProd ({S ↾}_{D})) \subseteq G DProd S)$
64	12 18 62 63	syl3anc	$⊢ φ \to ((G DProd ({S ↾}_{C}) \subseteq G DProd S \land G DProd ({S ↾}_{D}) \subseteq G DProd S) \leftrightarrow (G DProd ({S ↾}_{C})) \underset{˙}{\oplus} (G DProd ({S ↾}_{D})) \subseteq G DProd S)$
65	59 60 64	mpbi2and	$⊢ φ \to (G DProd ({S ↾}_{C})) \underset{˙}{\oplus} (G DProd ({S ↾}_{D})) \subseteq G DProd S$
66	58 65	eqssd	$⊢ φ \to G DProd S = (G DProd ({S ↾}_{C})) \underset{˙}{\oplus} (G DProd ({S ↾}_{D}))$

Metamath Proof Explorer

Theorem dprdsplit

Proof