dmdprdsplit

Description: The direct product splits into the direct product of any partition of the index set. (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$
	dmdprdsplit.z	$⊢ Z = Cntz (G)$
	dmdprdsplit.0	$⊢ \underset{˙}{0} = 0_{G}$
Assertion	dmdprdsplit	$⊢ φ \to (G dom DProd S \leftrightarrow ((G dom DProd ({S ↾}_{C}) \land G dom DProd ({S ↾}_{D})) \land G DProd ({S ↾}_{C}) \subseteq Z (G DProd ({S ↾}_{D})) \land (G DProd ({S ↾}_{C})) \cap (G DProd ({S ↾}_{D})) = \{\underset{˙}{0}\}))$

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		dmdprdsplit.z	$⊢ Z = Cntz (G)$
5		dmdprdsplit.0	$⊢ \underset{˙}{0} = 0_{G}$
6		simpr	$⊢ (φ \land G dom DProd S) \to G dom DProd S$
7	1	fdmd	$⊢ φ \to dom S = I$
8	7	adantr	$⊢ (φ \land G dom DProd S) \to dom S = I$
9		ssun1	$⊢ C \subseteq C \cup D$
10	3	adantr	$⊢ (φ \land G dom DProd S) \to I = C \cup D$
11	9 10	sseqtrrid	$⊢ (φ \land G dom DProd S) \to C \subseteq I$
12	6 8 11	dprdres	$⊢ (φ \land G dom DProd S) \to (G dom DProd ({S ↾}_{C}) \land G DProd ({S ↾}_{C}) \subseteq G DProd S)$
13	12	simpld	$⊢ (φ \land G dom DProd S) \to G dom DProd ({S ↾}_{C})$
14		ssun2	$⊢ D \subseteq C \cup D$
15	14 10	sseqtrrid	$⊢ (φ \land G dom DProd S) \to D \subseteq I$
16	6 8 15	dprdres	$⊢ (φ \land G dom DProd S) \to (G dom DProd ({S ↾}_{D}) \land G DProd ({S ↾}_{D}) \subseteq G DProd S)$
17	16	simpld	$⊢ (φ \land G dom DProd S) \to G dom DProd ({S ↾}_{D})$
18	13 17	jca	$⊢ (φ \land G dom DProd S) \to (G dom DProd ({S ↾}_{C}) \land G dom DProd ({S ↾}_{D}))$
19	2	adantr	$⊢ (φ \land G dom DProd S) \to C \cap D = \emptyset$
20	6 8 11 15 19 4	dprdcntz2	$⊢ (φ \land G dom DProd S) \to G DProd ({S ↾}_{C}) \subseteq Z (G DProd ({S ↾}_{D}))$
21	6 8 11 15 19 5	dprddisj2	$⊢ (φ \land G dom DProd S) \to (G DProd ({S ↾}_{C})) \cap (G DProd ({S ↾}_{D})) = \{\underset{˙}{0}\}$
22	18 20 21	3jca	$⊢ (φ \land G dom DProd S) \to ((G dom DProd ({S ↾}_{C}) \land G dom DProd ({S ↾}_{D})) \land G DProd ({S ↾}_{C}) \subseteq Z (G DProd ({S ↾}_{D})) \land (G DProd ({S ↾}_{C})) \cap (G DProd ({S ↾}_{D})) = \{\underset{˙}{0}\})$
23	1	adantr	$⊢ (φ \land ((G dom DProd ({S ↾}_{C}) \land G dom DProd ({S ↾}_{D})) \land G DProd ({S ↾}_{C}) \subseteq Z (G DProd ({S ↾}_{D})) \land (G DProd ({S ↾}_{C})) \cap (G DProd ({S ↾}_{D})) = \{\underset{˙}{0}\})) \to S : I ⟶ SubGrp (G)$
24	2	adantr	$⊢ (φ \land ((G dom DProd ({S ↾}_{C}) \land G dom DProd ({S ↾}_{D})) \land G DProd ({S ↾}_{C}) \subseteq Z (G DProd ({S ↾}_{D})) \land (G DProd ({S ↾}_{C})) \cap (G DProd ({S ↾}_{D})) = \{\underset{˙}{0}\})) \to C \cap D = \emptyset$
25	3	adantr	$⊢ (φ \land ((G dom DProd ({S ↾}_{C}) \land G dom DProd ({S ↾}_{D})) \land G DProd ({S ↾}_{C}) \subseteq Z (G DProd ({S ↾}_{D})) \land (G DProd ({S ↾}_{C})) \cap (G DProd ({S ↾}_{D})) = \{\underset{˙}{0}\})) \to I = C \cup D$
26		simpr1l	$⊢ (φ \land ((G dom DProd ({S ↾}_{C}) \land G dom DProd ({S ↾}_{D})) \land G DProd ({S ↾}_{C}) \subseteq Z (G DProd ({S ↾}_{D})) \land (G DProd ({S ↾}_{C})) \cap (G DProd ({S ↾}_{D})) = \{\underset{˙}{0}\})) \to G dom DProd ({S ↾}_{C})$
27		simpr1r	$⊢ (φ \land ((G dom DProd ({S ↾}_{C}) \land G dom DProd ({S ↾}_{D})) \land G DProd ({S ↾}_{C}) \subseteq Z (G DProd ({S ↾}_{D})) \land (G DProd ({S ↾}_{C})) \cap (G DProd ({S ↾}_{D})) = \{\underset{˙}{0}\})) \to G dom DProd ({S ↾}_{D})$
28		simpr2	$⊢ (φ \land ((G dom DProd ({S ↾}_{C}) \land G dom DProd ({S ↾}_{D})) \land G DProd ({S ↾}_{C}) \subseteq Z (G DProd ({S ↾}_{D})) \land (G DProd ({S ↾}_{C})) \cap (G DProd ({S ↾}_{D})) = \{\underset{˙}{0}\})) \to G DProd ({S ↾}_{C}) \subseteq Z (G DProd ({S ↾}_{D}))$
29		simpr3	$⊢ (φ \land ((G dom DProd ({S ↾}_{C}) \land G dom DProd ({S ↾}_{D})) \land G DProd ({S ↾}_{C}) \subseteq Z (G DProd ({S ↾}_{D})) \land (G DProd ({S ↾}_{C})) \cap (G DProd ({S ↾}_{D})) = \{\underset{˙}{0}\})) \to (G DProd ({S ↾}_{C})) \cap (G DProd ({S ↾}_{D})) = \{\underset{˙}{0}\}$
30	23 24 25 4 5 26 27 28 29	dmdprdsplit2	$⊢ (φ \land ((G dom DProd ({S ↾}_{C}) \land G dom DProd ({S ↾}_{D})) \land G DProd ({S ↾}_{C}) \subseteq Z (G DProd ({S ↾}_{D})) \land (G DProd ({S ↾}_{C})) \cap (G DProd ({S ↾}_{D})) = \{\underset{˙}{0}\})) \to G dom DProd S$
31	22 30	impbida	$⊢ φ \to (G dom DProd S \leftrightarrow ((G dom DProd ({S ↾}_{C}) \land G dom DProd ({S ↾}_{D})) \land G DProd ({S ↾}_{C}) \subseteq Z (G DProd ({S ↾}_{D})) \land (G DProd ({S ↾}_{C})) \cap (G DProd ({S ↾}_{D})) = \{\underset{˙}{0}\}))$

Metamath Proof Explorer

Theorem dmdprdsplit

Proof