subgdprd

Description: A direct product in a subgroup. (Contributed by Mario Carneiro, 27-Apr-2016)

	Ref	Expression
Hypotheses	subgdprd.1	$⊢ H = G ↾_{𝑠} A$
	subgdprd.2	$⊢ φ \to A \in SubGrp (G)$
	subgdprd.3	$⊢ φ \to G dom DProd S$
	subgdprd.4	$⊢ φ \to ran S \subseteq 𝒫 A$
Assertion	subgdprd	$⊢ φ \to H DProd S = G DProd S$

Proof

Step	Hyp	Ref	Expression
1		subgdprd.1	$⊢ H = G ↾_{𝑠} A$
2		subgdprd.2	$⊢ φ \to A \in SubGrp (G)$
3		subgdprd.3	$⊢ φ \to G dom DProd S$
4		subgdprd.4	$⊢ φ \to ran S \subseteq 𝒫 A$
5	1	subggrp	$⊢ A \in SubGrp (G) \to H \in Grp$
6	2 5	syl	$⊢ φ \to H \in Grp$
7		eqid	$⊢ {Base}_{H} = {Base}_{H}$
8	7	subgacs	$⊢ H \in Grp \to SubGrp (H) \in ACS ({Base}_{H})$
9		acsmre	$⊢ SubGrp (H) \in ACS ({Base}_{H}) \to SubGrp (H) \in Moore ({Base}_{H})$
10	6 8 9	3syl	$⊢ φ \to SubGrp (H) \in Moore ({Base}_{H})$
11		subgrcl	$⊢ A \in SubGrp (G) \to G \in Grp$
12	2 11	syl	$⊢ φ \to G \in Grp$
13		eqid	$⊢ {Base}_{G} = {Base}_{G}$
14	13	subgacs	$⊢ G \in Grp \to SubGrp (G) \in ACS ({Base}_{G})$
15		acsmre	$⊢ SubGrp (G) \in ACS ({Base}_{G}) \to SubGrp (G) \in Moore ({Base}_{G})$
16	12 14 15	3syl	$⊢ φ \to SubGrp (G) \in Moore ({Base}_{G})$
17		eqid	$⊢ mrCls (SubGrp (G)) = mrCls (SubGrp (G))$
18		dprdf	$⊢ G dom DProd S \to S : dom S ⟶ SubGrp (G)$
19		frn	$⊢ S : dom S ⟶ SubGrp (G) \to ran S \subseteq SubGrp (G)$
20	3 18 19	3syl	$⊢ φ \to ran S \subseteq SubGrp (G)$
21		mresspw	$⊢ SubGrp (G) \in Moore ({Base}_{G}) \to SubGrp (G) \subseteq 𝒫 {Base}_{G}$
22	16 21	syl	$⊢ φ \to SubGrp (G) \subseteq 𝒫 {Base}_{G}$
23	20 22	sstrd	$⊢ φ \to ran S \subseteq 𝒫 {Base}_{G}$
24		sspwuni	$⊢ ran S \subseteq 𝒫 {Base}_{G} \leftrightarrow ⋃ ran S \subseteq {Base}_{G}$
25	23 24	sylib	$⊢ φ \to ⋃ ran S \subseteq {Base}_{G}$
26	16 17 25	mrcssidd	$⊢ φ \to ⋃ ran S \subseteq mrCls (SubGrp (G)) (⋃ ran S)$
27	17	mrccl	$⊢ (SubGrp (G) \in Moore ({Base}_{G}) \land ⋃ ran S \subseteq {Base}_{G}) \to mrCls (SubGrp (G)) (⋃ ran S) \in SubGrp (G)$
28	16 25 27	syl2anc	$⊢ φ \to mrCls (SubGrp (G)) (⋃ ran S) \in SubGrp (G)$
29		sspwuni	$⊢ ran S \subseteq 𝒫 A \leftrightarrow ⋃ ran S \subseteq A$
30	4 29	sylib	$⊢ φ \to ⋃ ran S \subseteq A$
31	17	mrcsscl	$⊢ (SubGrp (G) \in Moore ({Base}_{G}) \land ⋃ ran S \subseteq A \land A \in SubGrp (G)) \to mrCls (SubGrp (G)) (⋃ ran S) \subseteq A$
32	16 30 2 31	syl3anc	$⊢ φ \to mrCls (SubGrp (G)) (⋃ ran S) \subseteq A$
33	1	subsubg	$⊢ A \in SubGrp (G) \to (mrCls (SubGrp (G)) (⋃ ran S) \in SubGrp (H) \leftrightarrow (mrCls (SubGrp (G)) (⋃ ran S) \in SubGrp (G) \land mrCls (SubGrp (G)) (⋃ ran S) \subseteq A))$
34	2 33	syl	$⊢ φ \to (mrCls (SubGrp (G)) (⋃ ran S) \in SubGrp (H) \leftrightarrow (mrCls (SubGrp (G)) (⋃ ran S) \in SubGrp (G) \land mrCls (SubGrp (G)) (⋃ ran S) \subseteq A))$
35	28 32 34	mpbir2and	$⊢ φ \to mrCls (SubGrp (G)) (⋃ ran S) \in SubGrp (H)$
36		eqid	$⊢ mrCls (SubGrp (H)) = mrCls (SubGrp (H))$
37	36	mrcsscl	$⊢ (SubGrp (H) \in Moore ({Base}_{H}) \land ⋃ ran S \subseteq mrCls (SubGrp (G)) (⋃ ran S) \land mrCls (SubGrp (G)) (⋃ ran S) \in SubGrp (H)) \to mrCls (SubGrp (H)) (⋃ ran S) \subseteq mrCls (SubGrp (G)) (⋃ ran S)$
38	10 26 35 37	syl3anc	$⊢ φ \to mrCls (SubGrp (H)) (⋃ ran S) \subseteq mrCls (SubGrp (G)) (⋃ ran S)$
39	1	subgdmdprd	$⊢ A \in SubGrp (G) \to (H dom DProd S \leftrightarrow (G dom DProd S \land ran S \subseteq 𝒫 A))$
40	2 39	syl	$⊢ φ \to (H dom DProd S \leftrightarrow (G dom DProd S \land ran S \subseteq 𝒫 A))$
41	3 4 40	mpbir2and	$⊢ φ \to H dom DProd S$
42		eqidd	$⊢ φ \to dom S = dom S$
43	41 42	dprdf2	$⊢ φ \to S : dom S ⟶ SubGrp (H)$
44	43	frnd	$⊢ φ \to ran S \subseteq SubGrp (H)$
45		mresspw	$⊢ SubGrp (H) \in Moore ({Base}_{H}) \to SubGrp (H) \subseteq 𝒫 {Base}_{H}$
46	10 45	syl	$⊢ φ \to SubGrp (H) \subseteq 𝒫 {Base}_{H}$
47	44 46	sstrd	$⊢ φ \to ran S \subseteq 𝒫 {Base}_{H}$
48		sspwuni	$⊢ ran S \subseteq 𝒫 {Base}_{H} \leftrightarrow ⋃ ran S \subseteq {Base}_{H}$
49	47 48	sylib	$⊢ φ \to ⋃ ran S \subseteq {Base}_{H}$
50	10 36 49	mrcssidd	$⊢ φ \to ⋃ ran S \subseteq mrCls (SubGrp (H)) (⋃ ran S)$
51	36	mrccl	$⊢ (SubGrp (H) \in Moore ({Base}_{H}) \land ⋃ ran S \subseteq {Base}_{H}) \to mrCls (SubGrp (H)) (⋃ ran S) \in SubGrp (H)$
52	10 49 51	syl2anc	$⊢ φ \to mrCls (SubGrp (H)) (⋃ ran S) \in SubGrp (H)$
53	1	subsubg	$⊢ A \in SubGrp (G) \to (mrCls (SubGrp (H)) (⋃ ran S) \in SubGrp (H) \leftrightarrow (mrCls (SubGrp (H)) (⋃ ran S) \in SubGrp (G) \land mrCls (SubGrp (H)) (⋃ ran S) \subseteq A))$
54	2 53	syl	$⊢ φ \to (mrCls (SubGrp (H)) (⋃ ran S) \in SubGrp (H) \leftrightarrow (mrCls (SubGrp (H)) (⋃ ran S) \in SubGrp (G) \land mrCls (SubGrp (H)) (⋃ ran S) \subseteq A))$
55	52 54	mpbid	$⊢ φ \to (mrCls (SubGrp (H)) (⋃ ran S) \in SubGrp (G) \land mrCls (SubGrp (H)) (⋃ ran S) \subseteq A)$
56	55	simpld	$⊢ φ \to mrCls (SubGrp (H)) (⋃ ran S) \in SubGrp (G)$
57	17	mrcsscl	$⊢ (SubGrp (G) \in Moore ({Base}_{G}) \land ⋃ ran S \subseteq mrCls (SubGrp (H)) (⋃ ran S) \land mrCls (SubGrp (H)) (⋃ ran S) \in SubGrp (G)) \to mrCls (SubGrp (G)) (⋃ ran S) \subseteq mrCls (SubGrp (H)) (⋃ ran S)$
58	16 50 56 57	syl3anc	$⊢ φ \to mrCls (SubGrp (G)) (⋃ ran S) \subseteq mrCls (SubGrp (H)) (⋃ ran S)$
59	38 58	eqssd	$⊢ φ \to mrCls (SubGrp (H)) (⋃ ran S) = mrCls (SubGrp (G)) (⋃ ran S)$
60	36	dprdspan	$⊢ H dom DProd S \to H DProd S = mrCls (SubGrp (H)) (⋃ ran S)$
61	41 60	syl	$⊢ φ \to H DProd S = mrCls (SubGrp (H)) (⋃ ran S)$
62	17	dprdspan	$⊢ G dom DProd S \to G DProd S = mrCls (SubGrp (G)) (⋃ ran S)$
63	3 62	syl	$⊢ φ \to G DProd S = mrCls (SubGrp (G)) (⋃ ran S)$
64	59 61 63	3eqtr4d	$⊢ φ \to H DProd S = G DProd S$

Metamath Proof Explorer

Theorem subgdprd

Proof