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