Metamath Proof Explorer

Theorem 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 ⊢ φ → A ∈ SubGrp ⁡ G
subgdprd.3 ⊢ φ → G dom ⁡ DProd S
subgdprd.4 ⊢ φ → ran ⁡ S ⊆ 𝒫 A
Assertion subgdprd ⊢ φ → H DProd S = G DProd S

Proof

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