dprdpr

Description: A singleton family is an internal direct product, the product of which is the given subgroup. (Contributed by Mario Carneiro, 26-Apr-2016)

	Ref	Expression
Hypotheses	dmdprdpr.z	$⊢ Z = Cntz (G)$
	dmdprdpr.0	$⊢ \underset{˙}{0} = 0_{G}$
	dmdprdpr.s	$⊢ φ \to S \in SubGrp (G)$
	dmdprdpr.t	$⊢ φ \to T \in SubGrp (G)$
	dprdpr.s	$⊢ \underset{˙}{\oplus} = LSSum (G)$
	dprdpr.1	$⊢ φ \to S \subseteq Z (T)$
	dprdpr.2	$⊢ φ \to S \cap T = \{\underset{˙}{0}\}$
Assertion	dprdpr	$⊢ φ \to G DProd \{⟨\emptyset, S⟩, ⟨1_{𝑜}, T⟩\} = S \underset{˙}{\oplus} T$

Proof

Step	Hyp	Ref	Expression
1		dmdprdpr.z	$⊢ Z = Cntz (G)$
2		dmdprdpr.0	$⊢ \underset{˙}{0} = 0_{G}$
3		dmdprdpr.s	$⊢ φ \to S \in SubGrp (G)$
4		dmdprdpr.t	$⊢ φ \to T \in SubGrp (G)$
5		dprdpr.s	$⊢ \underset{˙}{\oplus} = LSSum (G)$
6		dprdpr.1	$⊢ φ \to S \subseteq Z (T)$
7		dprdpr.2	$⊢ φ \to S \cap T = \{\underset{˙}{0}\}$
8		xpscf	$⊢ \{⟨\emptyset, S⟩, ⟨1_{𝑜}, T⟩\} : 2_{𝑜} ⟶ SubGrp (G) \leftrightarrow (S \in SubGrp (G) \land T \in SubGrp (G))$
9	3 4 8	sylanbrc	$⊢ φ \to \{⟨\emptyset, S⟩, ⟨1_{𝑜}, T⟩\} : 2_{𝑜} ⟶ SubGrp (G)$
10		1n0	$⊢ 1_{𝑜} \neq \emptyset$
11	10	necomi	$⊢ \emptyset \neq 1_{𝑜}$
12		disjsn2	$⊢ \emptyset \neq 1_{𝑜} \to \{\emptyset\} \cap \{1_{𝑜}\} = \emptyset$
13	11 12	mp1i	$⊢ φ \to \{\emptyset\} \cap \{1_{𝑜}\} = \emptyset$
14		df2o3	$⊢ 2_{𝑜} = \{\emptyset, 1_{𝑜}\}$
15		df-pr	$⊢ \{\emptyset, 1_{𝑜}\} = \{\emptyset\} \cup \{1_{𝑜}\}$
16	14 15	eqtri	$⊢ 2_{𝑜} = \{\emptyset\} \cup \{1_{𝑜}\}$
17	16	a1i	$⊢ φ \to 2_{𝑜} = \{\emptyset\} \cup \{1_{𝑜}\}$
18	1 2 3 4	dmdprdpr	$⊢ φ \to (G dom DProd \{⟨\emptyset, S⟩, ⟨1_{𝑜}, T⟩\} \leftrightarrow (S \subseteq Z (T) \land S \cap T = \{\underset{˙}{0}\}))$
19	6 7 18	mpbir2and	$⊢ φ \to G dom DProd \{⟨\emptyset, S⟩, ⟨1_{𝑜}, T⟩\}$
20	9 13 17 5 19	dprdsplit	$⊢ φ \to G DProd \{⟨\emptyset, S⟩, ⟨1_{𝑜}, T⟩\} = (G DProd ({\{⟨\emptyset, S⟩, ⟨1_{𝑜}, T⟩\} ↾}_{\{\emptyset\}})) \underset{˙}{\oplus} (G DProd ({\{⟨\emptyset, S⟩, ⟨1_{𝑜}, T⟩\} ↾}_{\{1_{𝑜}\}}))$
21	9	ffnd	$⊢ φ \to \{⟨\emptyset, S⟩, ⟨1_{𝑜}, T⟩\} Fn 2_{𝑜}$
22		0ex	$⊢ \emptyset \in V$
23	22	prid1	$⊢ \emptyset \in \{\emptyset, 1_{𝑜}\}$
24	23 14	eleqtrri	$⊢ \emptyset \in 2_{𝑜}$
25		fnressn	$⊢ (\{⟨\emptyset, S⟩, ⟨1_{𝑜}, T⟩\} Fn 2_{𝑜} \land \emptyset \in 2_{𝑜}) \to {\{⟨\emptyset, S⟩, ⟨1_{𝑜}, T⟩\} ↾}_{\{\emptyset\}} = \{⟨\emptyset, \{⟨\emptyset, S⟩, ⟨1_{𝑜}, T⟩\} (\emptyset)⟩\}$
26	21 24 25	sylancl	$⊢ φ \to {\{⟨\emptyset, S⟩, ⟨1_{𝑜}, T⟩\} ↾}_{\{\emptyset\}} = \{⟨\emptyset, \{⟨\emptyset, S⟩, ⟨1_{𝑜}, T⟩\} (\emptyset)⟩\}$
27		fvpr0o	$⊢ S \in SubGrp (G) \to \{⟨\emptyset, S⟩, ⟨1_{𝑜}, T⟩\} (\emptyset) = S$
28	3 27	syl	$⊢ φ \to \{⟨\emptyset, S⟩, ⟨1_{𝑜}, T⟩\} (\emptyset) = S$
29	28	opeq2d	$⊢ φ \to ⟨\emptyset, \{⟨\emptyset, S⟩, ⟨1_{𝑜}, T⟩\} (\emptyset)⟩ = ⟨\emptyset, S⟩$
30	29	sneqd	$⊢ φ \to \{⟨\emptyset, \{⟨\emptyset, S⟩, ⟨1_{𝑜}, T⟩\} (\emptyset)⟩\} = \{⟨\emptyset, S⟩\}$
31	26 30	eqtrd	$⊢ φ \to {\{⟨\emptyset, S⟩, ⟨1_{𝑜}, T⟩\} ↾}_{\{\emptyset\}} = \{⟨\emptyset, S⟩\}$
32	31	oveq2d	$⊢ φ \to G DProd ({\{⟨\emptyset, S⟩, ⟨1_{𝑜}, T⟩\} ↾}_{\{\emptyset\}}) = G DProd \{⟨\emptyset, S⟩\}$
33		dprdsn	$⊢ (\emptyset \in V \land S \in SubGrp (G)) \to (G dom DProd \{⟨\emptyset, S⟩\} \land G DProd \{⟨\emptyset, S⟩\} = S)$
34	22 3 33	sylancr	$⊢ φ \to (G dom DProd \{⟨\emptyset, S⟩\} \land G DProd \{⟨\emptyset, S⟩\} = S)$
35	34	simprd	$⊢ φ \to G DProd \{⟨\emptyset, S⟩\} = S$
36	32 35	eqtrd	$⊢ φ \to G DProd ({\{⟨\emptyset, S⟩, ⟨1_{𝑜}, T⟩\} ↾}_{\{\emptyset\}}) = S$
37		1oex	$⊢ 1_{𝑜} \in V$
38	37	prid2	$⊢ 1_{𝑜} \in \{\emptyset, 1_{𝑜}\}$
39	38 14	eleqtrri	$⊢ 1_{𝑜} \in 2_{𝑜}$
40		fnressn	$⊢ (\{⟨\emptyset, S⟩, ⟨1_{𝑜}, T⟩\} Fn 2_{𝑜} \land 1_{𝑜} \in 2_{𝑜}) \to {\{⟨\emptyset, S⟩, ⟨1_{𝑜}, T⟩\} ↾}_{\{1_{𝑜}\}} = \{⟨1_{𝑜}, \{⟨\emptyset, S⟩, ⟨1_{𝑜}, T⟩\} (1_{𝑜})⟩\}$
41	21 39 40	sylancl	$⊢ φ \to {\{⟨\emptyset, S⟩, ⟨1_{𝑜}, T⟩\} ↾}_{\{1_{𝑜}\}} = \{⟨1_{𝑜}, \{⟨\emptyset, S⟩, ⟨1_{𝑜}, T⟩\} (1_{𝑜})⟩\}$
42		fvpr1o	$⊢ T \in SubGrp (G) \to \{⟨\emptyset, S⟩, ⟨1_{𝑜}, T⟩\} (1_{𝑜}) = T$
43	4 42	syl	$⊢ φ \to \{⟨\emptyset, S⟩, ⟨1_{𝑜}, T⟩\} (1_{𝑜}) = T$
44	43	opeq2d	$⊢ φ \to ⟨1_{𝑜}, \{⟨\emptyset, S⟩, ⟨1_{𝑜}, T⟩\} (1_{𝑜})⟩ = ⟨1_{𝑜}, T⟩$
45	44	sneqd	$⊢ φ \to \{⟨1_{𝑜}, \{⟨\emptyset, S⟩, ⟨1_{𝑜}, T⟩\} (1_{𝑜})⟩\} = \{⟨1_{𝑜}, T⟩\}$
46	41 45	eqtrd	$⊢ φ \to {\{⟨\emptyset, S⟩, ⟨1_{𝑜}, T⟩\} ↾}_{\{1_{𝑜}\}} = \{⟨1_{𝑜}, T⟩\}$
47	46	oveq2d	$⊢ φ \to G DProd ({\{⟨\emptyset, S⟩, ⟨1_{𝑜}, T⟩\} ↾}_{\{1_{𝑜}\}}) = G DProd \{⟨1_{𝑜}, T⟩\}$
48		1on	$⊢ 1_{𝑜} \in On$
49		dprdsn	$⊢ (1_{𝑜} \in On \land T \in SubGrp (G)) \to (G dom DProd \{⟨1_{𝑜}, T⟩\} \land G DProd \{⟨1_{𝑜}, T⟩\} = T)$
50	48 4 49	sylancr	$⊢ φ \to (G dom DProd \{⟨1_{𝑜}, T⟩\} \land G DProd \{⟨1_{𝑜}, T⟩\} = T)$
51	50	simprd	$⊢ φ \to G DProd \{⟨1_{𝑜}, T⟩\} = T$
52	47 51	eqtrd	$⊢ φ \to G DProd ({\{⟨\emptyset, S⟩, ⟨1_{𝑜}, T⟩\} ↾}_{\{1_{𝑜}\}}) = T$
53	36 52	oveq12d	$⊢ φ \to (G DProd ({\{⟨\emptyset, S⟩, ⟨1_{𝑜}, T⟩\} ↾}_{\{\emptyset\}})) \underset{˙}{\oplus} (G DProd ({\{⟨\emptyset, S⟩, ⟨1_{𝑜}, T⟩\} ↾}_{\{1_{𝑜}\}})) = S \underset{˙}{\oplus} T$
54	20 53	eqtrd	$⊢ φ \to G DProd \{⟨\emptyset, S⟩, ⟨1_{𝑜}, T⟩\} = S \underset{˙}{\oplus} T$

Metamath Proof Explorer

Theorem dprdpr

Proof