dmdprdpr

Description: A singleton family is an internal direct product, the product of which is the given subgroup. (Contributed by Mario Carneiro, 25-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)$
Assertion	dmdprdpr	$⊢ φ \to (G dom DProd \{⟨\emptyset, S⟩, ⟨1_{𝑜}, T⟩\} \leftrightarrow (S \subseteq Z (T) \land S \cap T = \{\underset{˙}{0}\}))$

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		0ex	$⊢ \emptyset \in V$
6		dprdsn	$⊢ (\emptyset \in V \land S \in SubGrp (G)) \to (G dom DProd \{⟨\emptyset, S⟩\} \land G DProd \{⟨\emptyset, S⟩\} = S)$
7	5 3 6	sylancr	$⊢ φ \to (G dom DProd \{⟨\emptyset, S⟩\} \land G DProd \{⟨\emptyset, S⟩\} = S)$
8	7	simpld	$⊢ φ \to G dom DProd \{⟨\emptyset, S⟩\}$
9		xpscf	$⊢ \{⟨\emptyset, S⟩, ⟨1_{𝑜}, T⟩\} : 2_{𝑜} ⟶ SubGrp (G) \leftrightarrow (S \in SubGrp (G) \land T \in SubGrp (G))$
10	3 4 9	sylanbrc	$⊢ φ \to \{⟨\emptyset, S⟩, ⟨1_{𝑜}, T⟩\} : 2_{𝑜} ⟶ SubGrp (G)$
11	10	ffnd	$⊢ φ \to \{⟨\emptyset, S⟩, ⟨1_{𝑜}, T⟩\} Fn 2_{𝑜}$
12	5	prid1	$⊢ \emptyset \in \{\emptyset, 1_{𝑜}\}$
13		df2o3	$⊢ 2_{𝑜} = \{\emptyset, 1_{𝑜}\}$
14	12 13	eleqtrri	$⊢ \emptyset \in 2_{𝑜}$
15		fnressn	$⊢ (\{⟨\emptyset, S⟩, ⟨1_{𝑜}, T⟩\} Fn 2_{𝑜} \land \emptyset \in 2_{𝑜}) \to {\{⟨\emptyset, S⟩, ⟨1_{𝑜}, T⟩\} ↾}_{\{\emptyset\}} = \{⟨\emptyset, \{⟨\emptyset, S⟩, ⟨1_{𝑜}, T⟩\} (\emptyset)⟩\}$
16	11 14 15	sylancl	$⊢ φ \to {\{⟨\emptyset, S⟩, ⟨1_{𝑜}, T⟩\} ↾}_{\{\emptyset\}} = \{⟨\emptyset, \{⟨\emptyset, S⟩, ⟨1_{𝑜}, T⟩\} (\emptyset)⟩\}$
17		fvpr0o	$⊢ S \in SubGrp (G) \to \{⟨\emptyset, S⟩, ⟨1_{𝑜}, T⟩\} (\emptyset) = S$
18	3 17	syl	$⊢ φ \to \{⟨\emptyset, S⟩, ⟨1_{𝑜}, T⟩\} (\emptyset) = S$
19	18	opeq2d	$⊢ φ \to ⟨\emptyset, \{⟨\emptyset, S⟩, ⟨1_{𝑜}, T⟩\} (\emptyset)⟩ = ⟨\emptyset, S⟩$
20	19	sneqd	$⊢ φ \to \{⟨\emptyset, \{⟨\emptyset, S⟩, ⟨1_{𝑜}, T⟩\} (\emptyset)⟩\} = \{⟨\emptyset, S⟩\}$
21	16 20	eqtrd	$⊢ φ \to {\{⟨\emptyset, S⟩, ⟨1_{𝑜}, T⟩\} ↾}_{\{\emptyset\}} = \{⟨\emptyset, S⟩\}$
22	8 21	breqtrrd	$⊢ φ \to G dom DProd ({\{⟨\emptyset, S⟩, ⟨1_{𝑜}, T⟩\} ↾}_{\{\emptyset\}})$
23		1on	$⊢ 1_{𝑜} \in On$
24		dprdsn	$⊢ (1_{𝑜} \in On \land T \in SubGrp (G)) \to (G dom DProd \{⟨1_{𝑜}, T⟩\} \land G DProd \{⟨1_{𝑜}, T⟩\} = T)$
25	23 4 24	sylancr	$⊢ φ \to (G dom DProd \{⟨1_{𝑜}, T⟩\} \land G DProd \{⟨1_{𝑜}, T⟩\} = T)$
26	25	simpld	$⊢ φ \to G dom DProd \{⟨1_{𝑜}, T⟩\}$
27		1oex	$⊢ 1_{𝑜} \in V$
28	27	prid2	$⊢ 1_{𝑜} \in \{\emptyset, 1_{𝑜}\}$
29	28 13	eleqtrri	$⊢ 1_{𝑜} \in 2_{𝑜}$
30		fnressn	$⊢ (\{⟨\emptyset, S⟩, ⟨1_{𝑜}, T⟩\} Fn 2_{𝑜} \land 1_{𝑜} \in 2_{𝑜}) \to {\{⟨\emptyset, S⟩, ⟨1_{𝑜}, T⟩\} ↾}_{\{1_{𝑜}\}} = \{⟨1_{𝑜}, \{⟨\emptyset, S⟩, ⟨1_{𝑜}, T⟩\} (1_{𝑜})⟩\}$
31	11 29 30	sylancl	$⊢ φ \to {\{⟨\emptyset, S⟩, ⟨1_{𝑜}, T⟩\} ↾}_{\{1_{𝑜}\}} = \{⟨1_{𝑜}, \{⟨\emptyset, S⟩, ⟨1_{𝑜}, T⟩\} (1_{𝑜})⟩\}$
32		fvpr1o	$⊢ T \in SubGrp (G) \to \{⟨\emptyset, S⟩, ⟨1_{𝑜}, T⟩\} (1_{𝑜}) = T$
33	4 32	syl	$⊢ φ \to \{⟨\emptyset, S⟩, ⟨1_{𝑜}, T⟩\} (1_{𝑜}) = T$
34	33	opeq2d	$⊢ φ \to ⟨1_{𝑜}, \{⟨\emptyset, S⟩, ⟨1_{𝑜}, T⟩\} (1_{𝑜})⟩ = ⟨1_{𝑜}, T⟩$
35	34	sneqd	$⊢ φ \to \{⟨1_{𝑜}, \{⟨\emptyset, S⟩, ⟨1_{𝑜}, T⟩\} (1_{𝑜})⟩\} = \{⟨1_{𝑜}, T⟩\}$
36	31 35	eqtrd	$⊢ φ \to {\{⟨\emptyset, S⟩, ⟨1_{𝑜}, T⟩\} ↾}_{\{1_{𝑜}\}} = \{⟨1_{𝑜}, T⟩\}$
37	26 36	breqtrrd	$⊢ φ \to G dom DProd ({\{⟨\emptyset, S⟩, ⟨1_{𝑜}, T⟩\} ↾}_{\{1_{𝑜}\}})$
38		1n0	$⊢ 1_{𝑜} \neq \emptyset$
39	38	necomi	$⊢ \emptyset \neq 1_{𝑜}$
40		disjsn2	$⊢ \emptyset \neq 1_{𝑜} \to \{\emptyset\} \cap \{1_{𝑜}\} = \emptyset$
41	39 40	mp1i	$⊢ φ \to \{\emptyset\} \cap \{1_{𝑜}\} = \emptyset$
42		df-pr	$⊢ \{\emptyset, 1_{𝑜}\} = \{\emptyset\} \cup \{1_{𝑜}\}$
43	13 42	eqtri	$⊢ 2_{𝑜} = \{\emptyset\} \cup \{1_{𝑜}\}$
44	43	a1i	$⊢ φ \to 2_{𝑜} = \{\emptyset\} \cup \{1_{𝑜}\}$
45	10 41 44 1 2	dmdprdsplit	$⊢ φ \to (G dom DProd \{⟨\emptyset, S⟩, ⟨1_{𝑜}, T⟩\} \leftrightarrow ((G dom DProd ({\{⟨\emptyset, S⟩, ⟨1_{𝑜}, T⟩\} ↾}_{\{\emptyset\}}) \land G dom DProd ({\{⟨\emptyset, S⟩, ⟨1_{𝑜}, T⟩\} ↾}_{\{1_{𝑜}\}})) \land G DProd ({\{⟨\emptyset, S⟩, ⟨1_{𝑜}, T⟩\} ↾}_{\{\emptyset\}}) \subseteq Z (G DProd ({\{⟨\emptyset, S⟩, ⟨1_{𝑜}, T⟩\} ↾}_{\{1_{𝑜}\}})) \land (G DProd ({\{⟨\emptyset, S⟩, ⟨1_{𝑜}, T⟩\} ↾}_{\{\emptyset\}})) \cap (G DProd ({\{⟨\emptyset, S⟩, ⟨1_{𝑜}, T⟩\} ↾}_{\{1_{𝑜}\}})) = \{\underset{˙}{0}\}))$
46		3anass	$⊢ ((G dom DProd ({\{⟨\emptyset, S⟩, ⟨1_{𝑜}, T⟩\} ↾}_{\{\emptyset\}}) \land G dom DProd ({\{⟨\emptyset, S⟩, ⟨1_{𝑜}, T⟩\} ↾}_{\{1_{𝑜}\}})) \land G DProd ({\{⟨\emptyset, S⟩, ⟨1_{𝑜}, T⟩\} ↾}_{\{\emptyset\}}) \subseteq Z (G DProd ({\{⟨\emptyset, S⟩, ⟨1_{𝑜}, T⟩\} ↾}_{\{1_{𝑜}\}})) \land (G DProd ({\{⟨\emptyset, S⟩, ⟨1_{𝑜}, T⟩\} ↾}_{\{\emptyset\}})) \cap (G DProd ({\{⟨\emptyset, S⟩, ⟨1_{𝑜}, T⟩\} ↾}_{\{1_{𝑜}\}})) = \{\underset{˙}{0}\}) \leftrightarrow ((G dom DProd ({\{⟨\emptyset, S⟩, ⟨1_{𝑜}, T⟩\} ↾}_{\{\emptyset\}}) \land G dom DProd ({\{⟨\emptyset, S⟩, ⟨1_{𝑜}, T⟩\} ↾}_{\{1_{𝑜}\}})) \land (G DProd ({\{⟨\emptyset, S⟩, ⟨1_{𝑜}, T⟩\} ↾}_{\{\emptyset\}}) \subseteq Z (G DProd ({\{⟨\emptyset, S⟩, ⟨1_{𝑜}, T⟩\} ↾}_{\{1_{𝑜}\}})) \land (G DProd ({\{⟨\emptyset, S⟩, ⟨1_{𝑜}, T⟩\} ↾}_{\{\emptyset\}})) \cap (G DProd ({\{⟨\emptyset, S⟩, ⟨1_{𝑜}, T⟩\} ↾}_{\{1_{𝑜}\}})) = \{\underset{˙}{0}\}))$
47	45 46	bitrdi	$⊢ φ \to (G dom DProd \{⟨\emptyset, S⟩, ⟨1_{𝑜}, T⟩\} \leftrightarrow ((G dom DProd ({\{⟨\emptyset, S⟩, ⟨1_{𝑜}, T⟩\} ↾}_{\{\emptyset\}}) \land G dom DProd ({\{⟨\emptyset, S⟩, ⟨1_{𝑜}, T⟩\} ↾}_{\{1_{𝑜}\}})) \land (G DProd ({\{⟨\emptyset, S⟩, ⟨1_{𝑜}, T⟩\} ↾}_{\{\emptyset\}}) \subseteq Z (G DProd ({\{⟨\emptyset, S⟩, ⟨1_{𝑜}, T⟩\} ↾}_{\{1_{𝑜}\}})) \land (G DProd ({\{⟨\emptyset, S⟩, ⟨1_{𝑜}, T⟩\} ↾}_{\{\emptyset\}})) \cap (G DProd ({\{⟨\emptyset, S⟩, ⟨1_{𝑜}, T⟩\} ↾}_{\{1_{𝑜}\}})) = \{\underset{˙}{0}\})))$
48	47	baibd	$⊢ (φ \land (G dom DProd ({\{⟨\emptyset, S⟩, ⟨1_{𝑜}, T⟩\} ↾}_{\{\emptyset\}}) \land G dom DProd ({\{⟨\emptyset, S⟩, ⟨1_{𝑜}, T⟩\} ↾}_{\{1_{𝑜}\}}))) \to (G dom DProd \{⟨\emptyset, S⟩, ⟨1_{𝑜}, T⟩\} \leftrightarrow (G DProd ({\{⟨\emptyset, S⟩, ⟨1_{𝑜}, T⟩\} ↾}_{\{\emptyset\}}) \subseteq Z (G DProd ({\{⟨\emptyset, S⟩, ⟨1_{𝑜}, T⟩\} ↾}_{\{1_{𝑜}\}})) \land (G DProd ({\{⟨\emptyset, S⟩, ⟨1_{𝑜}, T⟩\} ↾}_{\{\emptyset\}})) \cap (G DProd ({\{⟨\emptyset, S⟩, ⟨1_{𝑜}, T⟩\} ↾}_{\{1_{𝑜}\}})) = \{\underset{˙}{0}\}))$
49	48	ex	$⊢ φ \to ((G dom DProd ({\{⟨\emptyset, S⟩, ⟨1_{𝑜}, T⟩\} ↾}_{\{\emptyset\}}) \land G dom DProd ({\{⟨\emptyset, S⟩, ⟨1_{𝑜}, T⟩\} ↾}_{\{1_{𝑜}\}})) \to (G dom DProd \{⟨\emptyset, S⟩, ⟨1_{𝑜}, T⟩\} \leftrightarrow (G DProd ({\{⟨\emptyset, S⟩, ⟨1_{𝑜}, T⟩\} ↾}_{\{\emptyset\}}) \subseteq Z (G DProd ({\{⟨\emptyset, S⟩, ⟨1_{𝑜}, T⟩\} ↾}_{\{1_{𝑜}\}})) \land (G DProd ({\{⟨\emptyset, S⟩, ⟨1_{𝑜}, T⟩\} ↾}_{\{\emptyset\}})) \cap (G DProd ({\{⟨\emptyset, S⟩, ⟨1_{𝑜}, T⟩\} ↾}_{\{1_{𝑜}\}})) = \{\underset{˙}{0}\})))$
50	22 37 49	mp2and	$⊢ φ \to (G dom DProd \{⟨\emptyset, S⟩, ⟨1_{𝑜}, T⟩\} \leftrightarrow (G DProd ({\{⟨\emptyset, S⟩, ⟨1_{𝑜}, T⟩\} ↾}_{\{\emptyset\}}) \subseteq Z (G DProd ({\{⟨\emptyset, S⟩, ⟨1_{𝑜}, T⟩\} ↾}_{\{1_{𝑜}\}})) \land (G DProd ({\{⟨\emptyset, S⟩, ⟨1_{𝑜}, T⟩\} ↾}_{\{\emptyset\}})) \cap (G DProd ({\{⟨\emptyset, S⟩, ⟨1_{𝑜}, T⟩\} ↾}_{\{1_{𝑜}\}})) = \{\underset{˙}{0}\}))$
51	21	oveq2d	$⊢ φ \to G DProd ({\{⟨\emptyset, S⟩, ⟨1_{𝑜}, T⟩\} ↾}_{\{\emptyset\}}) = G DProd \{⟨\emptyset, S⟩\}$
52	7	simprd	$⊢ φ \to G DProd \{⟨\emptyset, S⟩\} = S$
53	51 52	eqtrd	$⊢ φ \to G DProd ({\{⟨\emptyset, S⟩, ⟨1_{𝑜}, T⟩\} ↾}_{\{\emptyset\}}) = S$
54	36	oveq2d	$⊢ φ \to G DProd ({\{⟨\emptyset, S⟩, ⟨1_{𝑜}, T⟩\} ↾}_{\{1_{𝑜}\}}) = G DProd \{⟨1_{𝑜}, T⟩\}$
55	25	simprd	$⊢ φ \to G DProd \{⟨1_{𝑜}, T⟩\} = T$
56	54 55	eqtrd	$⊢ φ \to G DProd ({\{⟨\emptyset, S⟩, ⟨1_{𝑜}, T⟩\} ↾}_{\{1_{𝑜}\}}) = T$
57	56	fveq2d	$⊢ φ \to Z (G DProd ({\{⟨\emptyset, S⟩, ⟨1_{𝑜}, T⟩\} ↾}_{\{1_{𝑜}\}})) = Z (T)$
58	53 57	sseq12d	$⊢ φ \to (G DProd ({\{⟨\emptyset, S⟩, ⟨1_{𝑜}, T⟩\} ↾}_{\{\emptyset\}}) \subseteq Z (G DProd ({\{⟨\emptyset, S⟩, ⟨1_{𝑜}, T⟩\} ↾}_{\{1_{𝑜}\}})) \leftrightarrow S \subseteq Z (T))$
59	53 56	ineq12d	$⊢ φ \to (G DProd ({\{⟨\emptyset, S⟩, ⟨1_{𝑜}, T⟩\} ↾}_{\{\emptyset\}})) \cap (G DProd ({\{⟨\emptyset, S⟩, ⟨1_{𝑜}, T⟩\} ↾}_{\{1_{𝑜}\}})) = S \cap T$
60	59	eqeq1d	$⊢ φ \to ((G DProd ({\{⟨\emptyset, S⟩, ⟨1_{𝑜}, T⟩\} ↾}_{\{\emptyset\}})) \cap (G DProd ({\{⟨\emptyset, S⟩, ⟨1_{𝑜}, T⟩\} ↾}_{\{1_{𝑜}\}})) = \{\underset{˙}{0}\} \leftrightarrow S \cap T = \{\underset{˙}{0}\})$
61	58 60	anbi12d	$⊢ φ \to ((G DProd ({\{⟨\emptyset, S⟩, ⟨1_{𝑜}, T⟩\} ↾}_{\{\emptyset\}}) \subseteq Z (G DProd ({\{⟨\emptyset, S⟩, ⟨1_{𝑜}, T⟩\} ↾}_{\{1_{𝑜}\}})) \land (G DProd ({\{⟨\emptyset, S⟩, ⟨1_{𝑜}, T⟩\} ↾}_{\{\emptyset\}})) \cap (G DProd ({\{⟨\emptyset, S⟩, ⟨1_{𝑜}, T⟩\} ↾}_{\{1_{𝑜}\}})) = \{\underset{˙}{0}\}) \leftrightarrow (S \subseteq Z (T) \land S \cap T = \{\underset{˙}{0}\}))$
62	50 61	bitrd	$⊢ φ \to (G dom DProd \{⟨\emptyset, S⟩, ⟨1_{𝑜}, T⟩\} \leftrightarrow (S \subseteq Z (T) \land S \cap T = \{\underset{˙}{0}\}))$

Metamath Proof Explorer

Theorem dmdprdpr

Proof