dprdsn

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
	Assertion	dprdsn	$⊢ (A \in V \land S \in SubGrp (G)) \to (G dom DProd \{⟨A, S⟩\} \land G DProd \{⟨A, S⟩\} = S)$

Proof

Step	Hyp	Ref	Expression
1		eqid	$⊢ Cntz (G) = Cntz (G)$
2		eqid	$⊢ 0_{G} = 0_{G}$
3		eqid	$⊢ mrCls (SubGrp (G)) = mrCls (SubGrp (G))$
4		subgrcl	$⊢ S \in SubGrp (G) \to G \in Grp$
5	4	adantl	$⊢ (A \in V \land S \in SubGrp (G)) \to G \in Grp$
6		snex	$⊢ \{A\} \in V$
7	6	a1i	$⊢ (A \in V \land S \in SubGrp (G)) \to \{A\} \in V$
8		f1osng	$⊢ (A \in V \land S \in SubGrp (G)) \to \{⟨A, S⟩\} : \{A\} \underset{1-1 onto}{⟶} \{S\}$
9		f1of	$⊢ \{⟨A, S⟩\} : \{A\} \underset{1-1 onto}{⟶} \{S\} \to \{⟨A, S⟩\} : \{A\} ⟶ \{S\}$
10	8 9	syl	$⊢ (A \in V \land S \in SubGrp (G)) \to \{⟨A, S⟩\} : \{A\} ⟶ \{S\}$
11		simpr	$⊢ (A \in V \land S \in SubGrp (G)) \to S \in SubGrp (G)$
12	11	snssd	$⊢ (A \in V \land S \in SubGrp (G)) \to \{S\} \subseteq SubGrp (G)$
13	10 12	fssd	$⊢ (A \in V \land S \in SubGrp (G)) \to \{⟨A, S⟩\} : \{A\} ⟶ SubGrp (G)$
14		simpr1	$⊢ ((A \in V \land S \in SubGrp (G)) \land (x \in \{A\} \land y \in \{A\} \land x \neq y)) \to x \in \{A\}$
15		elsni	$⊢ x \in \{A\} \to x = A$
16	14 15	syl	$⊢ ((A \in V \land S \in SubGrp (G)) \land (x \in \{A\} \land y \in \{A\} \land x \neq y)) \to x = A$
17		simpr2	$⊢ ((A \in V \land S \in SubGrp (G)) \land (x \in \{A\} \land y \in \{A\} \land x \neq y)) \to y \in \{A\}$
18		elsni	$⊢ y \in \{A\} \to y = A$
19	17 18	syl	$⊢ ((A \in V \land S \in SubGrp (G)) \land (x \in \{A\} \land y \in \{A\} \land x \neq y)) \to y = A$
20	16 19	eqtr4d	$⊢ ((A \in V \land S \in SubGrp (G)) \land (x \in \{A\} \land y \in \{A\} \land x \neq y)) \to x = y$
21		simpr3	$⊢ ((A \in V \land S \in SubGrp (G)) \land (x \in \{A\} \land y \in \{A\} \land x \neq y)) \to x \neq y$
22	20 21	pm2.21ddne	$⊢ ((A \in V \land S \in SubGrp (G)) \land (x \in \{A\} \land y \in \{A\} \land x \neq y)) \to \{⟨A, S⟩\} (x) \subseteq Cntz (G) (\{⟨A, S⟩\} (y))$
23	5	adantr	$⊢ ((A \in V \land S \in SubGrp (G)) \land x \in \{A\}) \to G \in Grp$
24		eqid	$⊢ {Base}_{G} = {Base}_{G}$
25	24	subgacs	$⊢ G \in Grp \to SubGrp (G) \in ACS ({Base}_{G})$
26		acsmre	$⊢ SubGrp (G) \in ACS ({Base}_{G}) \to SubGrp (G) \in Moore ({Base}_{G})$
27	23 25 26	3syl	$⊢ ((A \in V \land S \in SubGrp (G)) \land x \in \{A\}) \to SubGrp (G) \in Moore ({Base}_{G})$
28	15	adantl	$⊢ ((A \in V \land S \in SubGrp (G)) \land x \in \{A\}) \to x = A$
29	28	sneqd	$⊢ ((A \in V \land S \in SubGrp (G)) \land x \in \{A\}) \to \{x\} = \{A\}$
30	29	difeq2d	$⊢ ((A \in V \land S \in SubGrp (G)) \land x \in \{A\}) \to \{A\} ∖ \{x\} = \{A\} ∖ \{A\}$
31		difid	$⊢ \{A\} ∖ \{A\} = \emptyset$
32	30 31	eqtrdi	$⊢ ((A \in V \land S \in SubGrp (G)) \land x \in \{A\}) \to \{A\} ∖ \{x\} = \emptyset$
33	32	imaeq2d	$⊢ ((A \in V \land S \in SubGrp (G)) \land x \in \{A\}) \to \{⟨A, S⟩\} [\{A\} ∖ \{x\}] = \{⟨A, S⟩\} [\emptyset]$
34		ima0	$⊢ \{⟨A, S⟩\} [\emptyset] = \emptyset$
35	33 34	eqtrdi	$⊢ ((A \in V \land S \in SubGrp (G)) \land x \in \{A\}) \to \{⟨A, S⟩\} [\{A\} ∖ \{x\}] = \emptyset$
36	35	unieqd	$⊢ ((A \in V \land S \in SubGrp (G)) \land x \in \{A\}) \to ⋃ \{⟨A, S⟩\} [\{A\} ∖ \{x\}] = ⋃ \emptyset$
37		uni0	$⊢ ⋃ \emptyset = \emptyset$
38	36 37	eqtrdi	$⊢ ((A \in V \land S \in SubGrp (G)) \land x \in \{A\}) \to ⋃ \{⟨A, S⟩\} [\{A\} ∖ \{x\}] = \emptyset$
39		0ss	$⊢ \emptyset \subseteq \{0_{G}\}$
40	39	a1i	$⊢ ((A \in V \land S \in SubGrp (G)) \land x \in \{A\}) \to \emptyset \subseteq \{0_{G}\}$
41	38 40	eqsstrd	$⊢ ((A \in V \land S \in SubGrp (G)) \land x \in \{A\}) \to ⋃ \{⟨A, S⟩\} [\{A\} ∖ \{x\}] \subseteq \{0_{G}\}$
42	2	0subg	$⊢ G \in Grp \to \{0_{G}\} \in SubGrp (G)$
43	23 42	syl	$⊢ ((A \in V \land S \in SubGrp (G)) \land x \in \{A\}) \to \{0_{G}\} \in SubGrp (G)$
44	3	mrcsscl	$⊢ (SubGrp (G) \in Moore ({Base}_{G}) \land ⋃ \{⟨A, S⟩\} [\{A\} ∖ \{x\}] \subseteq \{0_{G}\} \land \{0_{G}\} \in SubGrp (G)) \to mrCls (SubGrp (G)) (⋃ \{⟨A, S⟩\} [\{A\} ∖ \{x\}]) \subseteq \{0_{G}\}$
45	27 41 43 44	syl3anc	$⊢ ((A \in V \land S \in SubGrp (G)) \land x \in \{A\}) \to mrCls (SubGrp (G)) (⋃ \{⟨A, S⟩\} [\{A\} ∖ \{x\}]) \subseteq \{0_{G}\}$
46	2	subg0cl	$⊢ S \in SubGrp (G) \to 0_{G} \in S$
47	46	ad2antlr	$⊢ ((A \in V \land S \in SubGrp (G)) \land x \in \{A\}) \to 0_{G} \in S$
48	15	fveq2d	$⊢ x \in \{A\} \to \{⟨A, S⟩\} (x) = \{⟨A, S⟩\} (A)$
49		fvsng	$⊢ (A \in V \land S \in SubGrp (G)) \to \{⟨A, S⟩\} (A) = S$
50	48 49	sylan9eqr	$⊢ ((A \in V \land S \in SubGrp (G)) \land x \in \{A\}) \to \{⟨A, S⟩\} (x) = S$
51	47 50	eleqtrrd	$⊢ ((A \in V \land S \in SubGrp (G)) \land x \in \{A\}) \to 0_{G} \in \{⟨A, S⟩\} (x)$
52	51	snssd	$⊢ ((A \in V \land S \in SubGrp (G)) \land x \in \{A\}) \to \{0_{G}\} \subseteq \{⟨A, S⟩\} (x)$
53	45 52	sstrd	$⊢ ((A \in V \land S \in SubGrp (G)) \land x \in \{A\}) \to mrCls (SubGrp (G)) (⋃ \{⟨A, S⟩\} [\{A\} ∖ \{x\}]) \subseteq \{⟨A, S⟩\} (x)$
54		sseqin2	$⊢ mrCls (SubGrp (G)) (⋃ \{⟨A, S⟩\} [\{A\} ∖ \{x\}]) \subseteq \{⟨A, S⟩\} (x) \leftrightarrow \{⟨A, S⟩\} (x) \cap mrCls (SubGrp (G)) (⋃ \{⟨A, S⟩\} [\{A\} ∖ \{x\}]) = mrCls (SubGrp (G)) (⋃ \{⟨A, S⟩\} [\{A\} ∖ \{x\}])$
55	53 54	sylib	$⊢ ((A \in V \land S \in SubGrp (G)) \land x \in \{A\}) \to \{⟨A, S⟩\} (x) \cap mrCls (SubGrp (G)) (⋃ \{⟨A, S⟩\} [\{A\} ∖ \{x\}]) = mrCls (SubGrp (G)) (⋃ \{⟨A, S⟩\} [\{A\} ∖ \{x\}])$
56	55 45	eqsstrd	$⊢ ((A \in V \land S \in SubGrp (G)) \land x \in \{A\}) \to \{⟨A, S⟩\} (x) \cap mrCls (SubGrp (G)) (⋃ \{⟨A, S⟩\} [\{A\} ∖ \{x\}]) \subseteq \{0_{G}\}$
57	1 2 3 5 7 13 22 56	dmdprdd	$⊢ (A \in V \land S \in SubGrp (G)) \to G dom DProd \{⟨A, S⟩\}$
58	3	dprdspan	$⊢ G dom DProd \{⟨A, S⟩\} \to G DProd \{⟨A, S⟩\} = mrCls (SubGrp (G)) (⋃ ran \{⟨A, S⟩\})$
59	57 58	syl	$⊢ (A \in V \land S \in SubGrp (G)) \to G DProd \{⟨A, S⟩\} = mrCls (SubGrp (G)) (⋃ ran \{⟨A, S⟩\})$
60		rnsnopg	$⊢ A \in V \to ran \{⟨A, S⟩\} = \{S\}$
61	60	adantr	$⊢ (A \in V \land S \in SubGrp (G)) \to ran \{⟨A, S⟩\} = \{S\}$
62	61	unieqd	$⊢ (A \in V \land S \in SubGrp (G)) \to ⋃ ran \{⟨A, S⟩\} = ⋃ \{S\}$
63		unisng	$⊢ S \in SubGrp (G) \to ⋃ \{S\} = S$
64	63	adantl	$⊢ (A \in V \land S \in SubGrp (G)) \to ⋃ \{S\} = S$
65	62 64	eqtrd	$⊢ (A \in V \land S \in SubGrp (G)) \to ⋃ ran \{⟨A, S⟩\} = S$
66	65	fveq2d	$⊢ (A \in V \land S \in SubGrp (G)) \to mrCls (SubGrp (G)) (⋃ ran \{⟨A, S⟩\}) = mrCls (SubGrp (G)) (S)$
67	5 25 26	3syl	$⊢ (A \in V \land S \in SubGrp (G)) \to SubGrp (G) \in Moore ({Base}_{G})$
68	3	mrcid	$⊢ (SubGrp (G) \in Moore ({Base}_{G}) \land S \in SubGrp (G)) \to mrCls (SubGrp (G)) (S) = S$
69	67 68	sylancom	$⊢ (A \in V \land S \in SubGrp (G)) \to mrCls (SubGrp (G)) (S) = S$
70	66 69	eqtrd	$⊢ (A \in V \land S \in SubGrp (G)) \to mrCls (SubGrp (G)) (⋃ ran \{⟨A, S⟩\}) = S$
71	59 70	eqtrd	$⊢ (A \in V \land S \in SubGrp (G)) \to G DProd \{⟨A, S⟩\} = S$
72	57 71	jca	$⊢ (A \in V \land S \in SubGrp (G)) \to (G dom DProd \{⟨A, S⟩\} \land G DProd \{⟨A, S⟩\} = S)$

Metamath Proof Explorer

Theorem dprdsn

Proof