Metamath Proof Explorer

Theorem subgdprd

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

Ref Expression
Hypotheses subgdprd.1 ⊢ 𝐻 = ( 𝐺 ↾s 𝐴 )
subgdprd.2 ⊢ ( 𝜑 → 𝐴 ∈ ( SubGrp ‘ 𝐺 ) )
subgdprd.3 ⊢ ( 𝜑 → 𝐺 dom DProd 𝑆 )
subgdprd.4 ⊢ ( 𝜑 → ran 𝑆 ⊆ 𝒫 𝐴 )
Assertion subgdprd ( 𝜑 → ( 𝐻 DProd 𝑆 ) = ( 𝐺 DProd 𝑆 ) )

Proof

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