| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | reldmdprd 20018 | . . . 4
⊢ Rel dom
DProd | 
| 2 | 1 | brrelex2i 5741 | . . 3
⊢ (𝐻dom DProd 𝑆 → 𝑆 ∈ V) | 
| 3 | 2 | a1i 11 | . 2
⊢ (𝐴 ∈ (SubGrp‘𝐺) → (𝐻dom DProd 𝑆 → 𝑆 ∈ V)) | 
| 4 | 1 | brrelex2i 5741 | . . . 4
⊢ (𝐺dom DProd 𝑆 → 𝑆 ∈ V) | 
| 5 | 4 | adantr 480 | . . 3
⊢ ((𝐺dom DProd 𝑆 ∧ ran 𝑆 ⊆ 𝒫 𝐴) → 𝑆 ∈ V) | 
| 6 | 5 | a1i 11 | . 2
⊢ (𝐴 ∈ (SubGrp‘𝐺) → ((𝐺dom DProd 𝑆 ∧ ran 𝑆 ⊆ 𝒫 𝐴) → 𝑆 ∈ V)) | 
| 7 |  | ffvelcdm 7100 | . . . . . . . . . . . . . . . 16
⊢ ((𝑆:dom 𝑆⟶(SubGrp‘𝐻) ∧ 𝑥 ∈ dom 𝑆) → (𝑆‘𝑥) ∈ (SubGrp‘𝐻)) | 
| 8 | 7 | ad2ant2lr 748 | . . . . . . . . . . . . . . 15
⊢ (((𝐴 ∈ (SubGrp‘𝐺) ∧ 𝑆:dom 𝑆⟶(SubGrp‘𝐻)) ∧ (𝑥 ∈ dom 𝑆 ∧ 𝑦 ∈ (dom 𝑆 ∖ {𝑥}))) → (𝑆‘𝑥) ∈ (SubGrp‘𝐻)) | 
| 9 |  | eqid 2736 | . . . . . . . . . . . . . . . 16
⊢
(Base‘𝐻) =
(Base‘𝐻) | 
| 10 | 9 | subgss 19146 | . . . . . . . . . . . . . . 15
⊢ ((𝑆‘𝑥) ∈ (SubGrp‘𝐻) → (𝑆‘𝑥) ⊆ (Base‘𝐻)) | 
| 11 | 8, 10 | syl 17 | . . . . . . . . . . . . . 14
⊢ (((𝐴 ∈ (SubGrp‘𝐺) ∧ 𝑆:dom 𝑆⟶(SubGrp‘𝐻)) ∧ (𝑥 ∈ dom 𝑆 ∧ 𝑦 ∈ (dom 𝑆 ∖ {𝑥}))) → (𝑆‘𝑥) ⊆ (Base‘𝐻)) | 
| 12 |  | subgdprd.1 | . . . . . . . . . . . . . . . 16
⊢ 𝐻 = (𝐺 ↾s 𝐴) | 
| 13 | 12 | subgbas 19149 | . . . . . . . . . . . . . . 15
⊢ (𝐴 ∈ (SubGrp‘𝐺) → 𝐴 = (Base‘𝐻)) | 
| 14 | 13 | ad2antrr 726 | . . . . . . . . . . . . . 14
⊢ (((𝐴 ∈ (SubGrp‘𝐺) ∧ 𝑆:dom 𝑆⟶(SubGrp‘𝐻)) ∧ (𝑥 ∈ dom 𝑆 ∧ 𝑦 ∈ (dom 𝑆 ∖ {𝑥}))) → 𝐴 = (Base‘𝐻)) | 
| 15 | 11, 14 | sseqtrrd 4020 | . . . . . . . . . . . . 13
⊢ (((𝐴 ∈ (SubGrp‘𝐺) ∧ 𝑆:dom 𝑆⟶(SubGrp‘𝐻)) ∧ (𝑥 ∈ dom 𝑆 ∧ 𝑦 ∈ (dom 𝑆 ∖ {𝑥}))) → (𝑆‘𝑥) ⊆ 𝐴) | 
| 16 | 15 | biantrud 531 | . . . . . . . . . . . 12
⊢ (((𝐴 ∈ (SubGrp‘𝐺) ∧ 𝑆:dom 𝑆⟶(SubGrp‘𝐻)) ∧ (𝑥 ∈ dom 𝑆 ∧ 𝑦 ∈ (dom 𝑆 ∖ {𝑥}))) → ((𝑆‘𝑥) ⊆ ((Cntz‘𝐺)‘(𝑆‘𝑦)) ↔ ((𝑆‘𝑥) ⊆ ((Cntz‘𝐺)‘(𝑆‘𝑦)) ∧ (𝑆‘𝑥) ⊆ 𝐴))) | 
| 17 |  | simpll 766 | . . . . . . . . . . . . . . 15
⊢ (((𝐴 ∈ (SubGrp‘𝐺) ∧ 𝑆:dom 𝑆⟶(SubGrp‘𝐻)) ∧ (𝑥 ∈ dom 𝑆 ∧ 𝑦 ∈ (dom 𝑆 ∖ {𝑥}))) → 𝐴 ∈ (SubGrp‘𝐺)) | 
| 18 |  | simplr 768 | . . . . . . . . . . . . . . . . . 18
⊢ (((𝐴 ∈ (SubGrp‘𝐺) ∧ 𝑆:dom 𝑆⟶(SubGrp‘𝐻)) ∧ (𝑥 ∈ dom 𝑆 ∧ 𝑦 ∈ (dom 𝑆 ∖ {𝑥}))) → 𝑆:dom 𝑆⟶(SubGrp‘𝐻)) | 
| 19 |  | eldifi 4130 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝑦 ∈ (dom 𝑆 ∖ {𝑥}) → 𝑦 ∈ dom 𝑆) | 
| 20 | 19 | ad2antll 729 | . . . . . . . . . . . . . . . . . 18
⊢ (((𝐴 ∈ (SubGrp‘𝐺) ∧ 𝑆:dom 𝑆⟶(SubGrp‘𝐻)) ∧ (𝑥 ∈ dom 𝑆 ∧ 𝑦 ∈ (dom 𝑆 ∖ {𝑥}))) → 𝑦 ∈ dom 𝑆) | 
| 21 | 18, 20 | ffvelcdmd 7104 | . . . . . . . . . . . . . . . . 17
⊢ (((𝐴 ∈ (SubGrp‘𝐺) ∧ 𝑆:dom 𝑆⟶(SubGrp‘𝐻)) ∧ (𝑥 ∈ dom 𝑆 ∧ 𝑦 ∈ (dom 𝑆 ∖ {𝑥}))) → (𝑆‘𝑦) ∈ (SubGrp‘𝐻)) | 
| 22 | 9 | subgss 19146 | . . . . . . . . . . . . . . . . 17
⊢ ((𝑆‘𝑦) ∈ (SubGrp‘𝐻) → (𝑆‘𝑦) ⊆ (Base‘𝐻)) | 
| 23 | 21, 22 | syl 17 | . . . . . . . . . . . . . . . 16
⊢ (((𝐴 ∈ (SubGrp‘𝐺) ∧ 𝑆:dom 𝑆⟶(SubGrp‘𝐻)) ∧ (𝑥 ∈ dom 𝑆 ∧ 𝑦 ∈ (dom 𝑆 ∖ {𝑥}))) → (𝑆‘𝑦) ⊆ (Base‘𝐻)) | 
| 24 | 23, 14 | sseqtrrd 4020 | . . . . . . . . . . . . . . 15
⊢ (((𝐴 ∈ (SubGrp‘𝐺) ∧ 𝑆:dom 𝑆⟶(SubGrp‘𝐻)) ∧ (𝑥 ∈ dom 𝑆 ∧ 𝑦 ∈ (dom 𝑆 ∖ {𝑥}))) → (𝑆‘𝑦) ⊆ 𝐴) | 
| 25 |  | eqid 2736 | . . . . . . . . . . . . . . . 16
⊢
(Cntz‘𝐺) =
(Cntz‘𝐺) | 
| 26 |  | eqid 2736 | . . . . . . . . . . . . . . . 16
⊢
(Cntz‘𝐻) =
(Cntz‘𝐻) | 
| 27 | 12, 25, 26 | resscntz 19352 | . . . . . . . . . . . . . . 15
⊢ ((𝐴 ∈ (SubGrp‘𝐺) ∧ (𝑆‘𝑦) ⊆ 𝐴) → ((Cntz‘𝐻)‘(𝑆‘𝑦)) = (((Cntz‘𝐺)‘(𝑆‘𝑦)) ∩ 𝐴)) | 
| 28 | 17, 24, 27 | syl2anc 584 | . . . . . . . . . . . . . 14
⊢ (((𝐴 ∈ (SubGrp‘𝐺) ∧ 𝑆:dom 𝑆⟶(SubGrp‘𝐻)) ∧ (𝑥 ∈ dom 𝑆 ∧ 𝑦 ∈ (dom 𝑆 ∖ {𝑥}))) → ((Cntz‘𝐻)‘(𝑆‘𝑦)) = (((Cntz‘𝐺)‘(𝑆‘𝑦)) ∩ 𝐴)) | 
| 29 | 28 | sseq2d 4015 | . . . . . . . . . . . . 13
⊢ (((𝐴 ∈ (SubGrp‘𝐺) ∧ 𝑆:dom 𝑆⟶(SubGrp‘𝐻)) ∧ (𝑥 ∈ dom 𝑆 ∧ 𝑦 ∈ (dom 𝑆 ∖ {𝑥}))) → ((𝑆‘𝑥) ⊆ ((Cntz‘𝐻)‘(𝑆‘𝑦)) ↔ (𝑆‘𝑥) ⊆ (((Cntz‘𝐺)‘(𝑆‘𝑦)) ∩ 𝐴))) | 
| 30 |  | ssin 4238 | . . . . . . . . . . . . 13
⊢ (((𝑆‘𝑥) ⊆ ((Cntz‘𝐺)‘(𝑆‘𝑦)) ∧ (𝑆‘𝑥) ⊆ 𝐴) ↔ (𝑆‘𝑥) ⊆ (((Cntz‘𝐺)‘(𝑆‘𝑦)) ∩ 𝐴)) | 
| 31 | 29, 30 | bitr4di 289 | . . . . . . . . . . . 12
⊢ (((𝐴 ∈ (SubGrp‘𝐺) ∧ 𝑆:dom 𝑆⟶(SubGrp‘𝐻)) ∧ (𝑥 ∈ dom 𝑆 ∧ 𝑦 ∈ (dom 𝑆 ∖ {𝑥}))) → ((𝑆‘𝑥) ⊆ ((Cntz‘𝐻)‘(𝑆‘𝑦)) ↔ ((𝑆‘𝑥) ⊆ ((Cntz‘𝐺)‘(𝑆‘𝑦)) ∧ (𝑆‘𝑥) ⊆ 𝐴))) | 
| 32 | 16, 31 | bitr4d 282 | . . . . . . . . . . 11
⊢ (((𝐴 ∈ (SubGrp‘𝐺) ∧ 𝑆:dom 𝑆⟶(SubGrp‘𝐻)) ∧ (𝑥 ∈ dom 𝑆 ∧ 𝑦 ∈ (dom 𝑆 ∖ {𝑥}))) → ((𝑆‘𝑥) ⊆ ((Cntz‘𝐺)‘(𝑆‘𝑦)) ↔ (𝑆‘𝑥) ⊆ ((Cntz‘𝐻)‘(𝑆‘𝑦)))) | 
| 33 | 32 | anassrs 467 | . . . . . . . . . 10
⊢ ((((𝐴 ∈ (SubGrp‘𝐺) ∧ 𝑆:dom 𝑆⟶(SubGrp‘𝐻)) ∧ 𝑥 ∈ dom 𝑆) ∧ 𝑦 ∈ (dom 𝑆 ∖ {𝑥})) → ((𝑆‘𝑥) ⊆ ((Cntz‘𝐺)‘(𝑆‘𝑦)) ↔ (𝑆‘𝑥) ⊆ ((Cntz‘𝐻)‘(𝑆‘𝑦)))) | 
| 34 | 33 | ralbidva 3175 | . . . . . . . . 9
⊢ (((𝐴 ∈ (SubGrp‘𝐺) ∧ 𝑆:dom 𝑆⟶(SubGrp‘𝐻)) ∧ 𝑥 ∈ dom 𝑆) → (∀𝑦 ∈ (dom 𝑆 ∖ {𝑥})(𝑆‘𝑥) ⊆ ((Cntz‘𝐺)‘(𝑆‘𝑦)) ↔ ∀𝑦 ∈ (dom 𝑆 ∖ {𝑥})(𝑆‘𝑥) ⊆ ((Cntz‘𝐻)‘(𝑆‘𝑦)))) | 
| 35 |  | subgrcl 19150 | . . . . . . . . . . . . . . 15
⊢ (𝐴 ∈ (SubGrp‘𝐺) → 𝐺 ∈ Grp) | 
| 36 | 35 | ad2antrr 726 | . . . . . . . . . . . . . 14
⊢ (((𝐴 ∈ (SubGrp‘𝐺) ∧ 𝑆:dom 𝑆⟶(SubGrp‘𝐻)) ∧ 𝑥 ∈ dom 𝑆) → 𝐺 ∈ Grp) | 
| 37 |  | eqid 2736 | . . . . . . . . . . . . . . 15
⊢
(Base‘𝐺) =
(Base‘𝐺) | 
| 38 | 37 | subgacs 19180 | . . . . . . . . . . . . . 14
⊢ (𝐺 ∈ Grp →
(SubGrp‘𝐺) ∈
(ACS‘(Base‘𝐺))) | 
| 39 |  | acsmre 17696 | . . . . . . . . . . . . . 14
⊢
((SubGrp‘𝐺)
∈ (ACS‘(Base‘𝐺)) → (SubGrp‘𝐺) ∈ (Moore‘(Base‘𝐺))) | 
| 40 | 36, 38, 39 | 3syl 18 | . . . . . . . . . . . . 13
⊢ (((𝐴 ∈ (SubGrp‘𝐺) ∧ 𝑆:dom 𝑆⟶(SubGrp‘𝐻)) ∧ 𝑥 ∈ dom 𝑆) → (SubGrp‘𝐺) ∈ (Moore‘(Base‘𝐺))) | 
| 41 | 12 | subggrp 19148 | . . . . . . . . . . . . . . . 16
⊢ (𝐴 ∈ (SubGrp‘𝐺) → 𝐻 ∈ Grp) | 
| 42 | 41 | ad2antrr 726 | . . . . . . . . . . . . . . 15
⊢ (((𝐴 ∈ (SubGrp‘𝐺) ∧ 𝑆:dom 𝑆⟶(SubGrp‘𝐻)) ∧ 𝑥 ∈ dom 𝑆) → 𝐻 ∈ Grp) | 
| 43 | 9 | subgacs 19180 | . . . . . . . . . . . . . . 15
⊢ (𝐻 ∈ Grp →
(SubGrp‘𝐻) ∈
(ACS‘(Base‘𝐻))) | 
| 44 |  | acsmre 17696 | . . . . . . . . . . . . . . 15
⊢
((SubGrp‘𝐻)
∈ (ACS‘(Base‘𝐻)) → (SubGrp‘𝐻) ∈ (Moore‘(Base‘𝐻))) | 
| 45 | 42, 43, 44 | 3syl 18 | . . . . . . . . . . . . . 14
⊢ (((𝐴 ∈ (SubGrp‘𝐺) ∧ 𝑆:dom 𝑆⟶(SubGrp‘𝐻)) ∧ 𝑥 ∈ dom 𝑆) → (SubGrp‘𝐻) ∈ (Moore‘(Base‘𝐻))) | 
| 46 |  | eqid 2736 | . . . . . . . . . . . . . 14
⊢
(mrCls‘(SubGrp‘𝐻)) = (mrCls‘(SubGrp‘𝐻)) | 
| 47 |  | imassrn 6088 | . . . . . . . . . . . . . . . . 17
⊢ (𝑆 “ (dom 𝑆 ∖ {𝑥})) ⊆ ran 𝑆 | 
| 48 |  | frn 6742 | . . . . . . . . . . . . . . . . . 18
⊢ (𝑆:dom 𝑆⟶(SubGrp‘𝐻) → ran 𝑆 ⊆ (SubGrp‘𝐻)) | 
| 49 | 48 | ad2antlr 727 | . . . . . . . . . . . . . . . . 17
⊢ (((𝐴 ∈ (SubGrp‘𝐺) ∧ 𝑆:dom 𝑆⟶(SubGrp‘𝐻)) ∧ 𝑥 ∈ dom 𝑆) → ran 𝑆 ⊆ (SubGrp‘𝐻)) | 
| 50 | 47, 49 | sstrid 3994 | . . . . . . . . . . . . . . . 16
⊢ (((𝐴 ∈ (SubGrp‘𝐺) ∧ 𝑆:dom 𝑆⟶(SubGrp‘𝐻)) ∧ 𝑥 ∈ dom 𝑆) → (𝑆 “ (dom 𝑆 ∖ {𝑥})) ⊆ (SubGrp‘𝐻)) | 
| 51 |  | mresspw 17636 | . . . . . . . . . . . . . . . . 17
⊢
((SubGrp‘𝐻)
∈ (Moore‘(Base‘𝐻)) → (SubGrp‘𝐻) ⊆ 𝒫 (Base‘𝐻)) | 
| 52 | 45, 51 | syl 17 | . . . . . . . . . . . . . . . 16
⊢ (((𝐴 ∈ (SubGrp‘𝐺) ∧ 𝑆:dom 𝑆⟶(SubGrp‘𝐻)) ∧ 𝑥 ∈ dom 𝑆) → (SubGrp‘𝐻) ⊆ 𝒫 (Base‘𝐻)) | 
| 53 | 50, 52 | sstrd 3993 | . . . . . . . . . . . . . . 15
⊢ (((𝐴 ∈ (SubGrp‘𝐺) ∧ 𝑆:dom 𝑆⟶(SubGrp‘𝐻)) ∧ 𝑥 ∈ dom 𝑆) → (𝑆 “ (dom 𝑆 ∖ {𝑥})) ⊆ 𝒫 (Base‘𝐻)) | 
| 54 |  | sspwuni 5099 | . . . . . . . . . . . . . . 15
⊢ ((𝑆 “ (dom 𝑆 ∖ {𝑥})) ⊆ 𝒫 (Base‘𝐻) ↔ ∪ (𝑆
“ (dom 𝑆 ∖
{𝑥})) ⊆
(Base‘𝐻)) | 
| 55 | 53, 54 | sylib 218 | . . . . . . . . . . . . . 14
⊢ (((𝐴 ∈ (SubGrp‘𝐺) ∧ 𝑆:dom 𝑆⟶(SubGrp‘𝐻)) ∧ 𝑥 ∈ dom 𝑆) → ∪ (𝑆 “ (dom 𝑆 ∖ {𝑥})) ⊆ (Base‘𝐻)) | 
| 56 | 45, 46, 55 | mrcssidd 17669 | . . . . . . . . . . . . 13
⊢ (((𝐴 ∈ (SubGrp‘𝐺) ∧ 𝑆:dom 𝑆⟶(SubGrp‘𝐻)) ∧ 𝑥 ∈ dom 𝑆) → ∪ (𝑆 “ (dom 𝑆 ∖ {𝑥})) ⊆ ((mrCls‘(SubGrp‘𝐻))‘∪ (𝑆
“ (dom 𝑆 ∖
{𝑥})))) | 
| 57 | 46 | mrccl 17655 | . . . . . . . . . . . . . . . 16
⊢
(((SubGrp‘𝐻)
∈ (Moore‘(Base‘𝐻)) ∧ ∪ (𝑆 “ (dom 𝑆 ∖ {𝑥})) ⊆ (Base‘𝐻)) → ((mrCls‘(SubGrp‘𝐻))‘∪ (𝑆
“ (dom 𝑆 ∖
{𝑥}))) ∈
(SubGrp‘𝐻)) | 
| 58 | 45, 55, 57 | syl2anc 584 | . . . . . . . . . . . . . . 15
⊢ (((𝐴 ∈ (SubGrp‘𝐺) ∧ 𝑆:dom 𝑆⟶(SubGrp‘𝐻)) ∧ 𝑥 ∈ dom 𝑆) → ((mrCls‘(SubGrp‘𝐻))‘∪ (𝑆
“ (dom 𝑆 ∖
{𝑥}))) ∈
(SubGrp‘𝐻)) | 
| 59 | 12 | subsubg 19168 | . . . . . . . . . . . . . . . 16
⊢ (𝐴 ∈ (SubGrp‘𝐺) →
(((mrCls‘(SubGrp‘𝐻))‘∪ (𝑆 “ (dom 𝑆 ∖ {𝑥}))) ∈ (SubGrp‘𝐻) ↔ (((mrCls‘(SubGrp‘𝐻))‘∪ (𝑆
“ (dom 𝑆 ∖
{𝑥}))) ∈
(SubGrp‘𝐺) ∧
((mrCls‘(SubGrp‘𝐻))‘∪ (𝑆 “ (dom 𝑆 ∖ {𝑥}))) ⊆ 𝐴))) | 
| 60 | 59 | ad2antrr 726 | . . . . . . . . . . . . . . 15
⊢ (((𝐴 ∈ (SubGrp‘𝐺) ∧ 𝑆:dom 𝑆⟶(SubGrp‘𝐻)) ∧ 𝑥 ∈ dom 𝑆) → (((mrCls‘(SubGrp‘𝐻))‘∪ (𝑆
“ (dom 𝑆 ∖
{𝑥}))) ∈
(SubGrp‘𝐻) ↔
(((mrCls‘(SubGrp‘𝐻))‘∪ (𝑆 “ (dom 𝑆 ∖ {𝑥}))) ∈ (SubGrp‘𝐺) ∧ ((mrCls‘(SubGrp‘𝐻))‘∪ (𝑆
“ (dom 𝑆 ∖
{𝑥}))) ⊆ 𝐴))) | 
| 61 | 58, 60 | mpbid 232 | . . . . . . . . . . . . . 14
⊢ (((𝐴 ∈ (SubGrp‘𝐺) ∧ 𝑆:dom 𝑆⟶(SubGrp‘𝐻)) ∧ 𝑥 ∈ dom 𝑆) → (((mrCls‘(SubGrp‘𝐻))‘∪ (𝑆
“ (dom 𝑆 ∖
{𝑥}))) ∈
(SubGrp‘𝐺) ∧
((mrCls‘(SubGrp‘𝐻))‘∪ (𝑆 “ (dom 𝑆 ∖ {𝑥}))) ⊆ 𝐴)) | 
| 62 | 61 | simpld 494 | . . . . . . . . . . . . 13
⊢ (((𝐴 ∈ (SubGrp‘𝐺) ∧ 𝑆:dom 𝑆⟶(SubGrp‘𝐻)) ∧ 𝑥 ∈ dom 𝑆) → ((mrCls‘(SubGrp‘𝐻))‘∪ (𝑆
“ (dom 𝑆 ∖
{𝑥}))) ∈
(SubGrp‘𝐺)) | 
| 63 |  | eqid 2736 | . . . . . . . . . . . . . 14
⊢
(mrCls‘(SubGrp‘𝐺)) = (mrCls‘(SubGrp‘𝐺)) | 
| 64 | 63 | mrcsscl 17664 | . . . . . . . . . . . . 13
⊢
(((SubGrp‘𝐺)
∈ (Moore‘(Base‘𝐺)) ∧ ∪ (𝑆 “ (dom 𝑆 ∖ {𝑥})) ⊆ ((mrCls‘(SubGrp‘𝐻))‘∪ (𝑆
“ (dom 𝑆 ∖
{𝑥}))) ∧
((mrCls‘(SubGrp‘𝐻))‘∪ (𝑆 “ (dom 𝑆 ∖ {𝑥}))) ∈ (SubGrp‘𝐺)) → ((mrCls‘(SubGrp‘𝐺))‘∪ (𝑆
“ (dom 𝑆 ∖
{𝑥}))) ⊆
((mrCls‘(SubGrp‘𝐻))‘∪ (𝑆 “ (dom 𝑆 ∖ {𝑥})))) | 
| 65 | 40, 56, 62, 64 | syl3anc 1372 | . . . . . . . . . . . 12
⊢ (((𝐴 ∈ (SubGrp‘𝐺) ∧ 𝑆:dom 𝑆⟶(SubGrp‘𝐻)) ∧ 𝑥 ∈ dom 𝑆) → ((mrCls‘(SubGrp‘𝐺))‘∪ (𝑆
“ (dom 𝑆 ∖
{𝑥}))) ⊆
((mrCls‘(SubGrp‘𝐻))‘∪ (𝑆 “ (dom 𝑆 ∖ {𝑥})))) | 
| 66 | 13 | ad2antrr 726 | . . . . . . . . . . . . . . . 16
⊢ (((𝐴 ∈ (SubGrp‘𝐺) ∧ 𝑆:dom 𝑆⟶(SubGrp‘𝐻)) ∧ 𝑥 ∈ dom 𝑆) → 𝐴 = (Base‘𝐻)) | 
| 67 | 55, 66 | sseqtrrd 4020 | . . . . . . . . . . . . . . 15
⊢ (((𝐴 ∈ (SubGrp‘𝐺) ∧ 𝑆:dom 𝑆⟶(SubGrp‘𝐻)) ∧ 𝑥 ∈ dom 𝑆) → ∪ (𝑆 “ (dom 𝑆 ∖ {𝑥})) ⊆ 𝐴) | 
| 68 | 37 | subgss 19146 | . . . . . . . . . . . . . . . 16
⊢ (𝐴 ∈ (SubGrp‘𝐺) → 𝐴 ⊆ (Base‘𝐺)) | 
| 69 | 68 | ad2antrr 726 | . . . . . . . . . . . . . . 15
⊢ (((𝐴 ∈ (SubGrp‘𝐺) ∧ 𝑆:dom 𝑆⟶(SubGrp‘𝐻)) ∧ 𝑥 ∈ dom 𝑆) → 𝐴 ⊆ (Base‘𝐺)) | 
| 70 | 67, 69 | sstrd 3993 | . . . . . . . . . . . . . 14
⊢ (((𝐴 ∈ (SubGrp‘𝐺) ∧ 𝑆:dom 𝑆⟶(SubGrp‘𝐻)) ∧ 𝑥 ∈ dom 𝑆) → ∪ (𝑆 “ (dom 𝑆 ∖ {𝑥})) ⊆ (Base‘𝐺)) | 
| 71 | 40, 63, 70 | mrcssidd 17669 | . . . . . . . . . . . . 13
⊢ (((𝐴 ∈ (SubGrp‘𝐺) ∧ 𝑆:dom 𝑆⟶(SubGrp‘𝐻)) ∧ 𝑥 ∈ dom 𝑆) → ∪ (𝑆 “ (dom 𝑆 ∖ {𝑥})) ⊆ ((mrCls‘(SubGrp‘𝐺))‘∪ (𝑆
“ (dom 𝑆 ∖
{𝑥})))) | 
| 72 | 63 | mrccl 17655 | . . . . . . . . . . . . . . 15
⊢
(((SubGrp‘𝐺)
∈ (Moore‘(Base‘𝐺)) ∧ ∪ (𝑆 “ (dom 𝑆 ∖ {𝑥})) ⊆ (Base‘𝐺)) → ((mrCls‘(SubGrp‘𝐺))‘∪ (𝑆
“ (dom 𝑆 ∖
{𝑥}))) ∈
(SubGrp‘𝐺)) | 
| 73 | 40, 70, 72 | syl2anc 584 | . . . . . . . . . . . . . 14
⊢ (((𝐴 ∈ (SubGrp‘𝐺) ∧ 𝑆:dom 𝑆⟶(SubGrp‘𝐻)) ∧ 𝑥 ∈ dom 𝑆) → ((mrCls‘(SubGrp‘𝐺))‘∪ (𝑆
“ (dom 𝑆 ∖
{𝑥}))) ∈
(SubGrp‘𝐺)) | 
| 74 |  | simpll 766 | . . . . . . . . . . . . . . 15
⊢ (((𝐴 ∈ (SubGrp‘𝐺) ∧ 𝑆:dom 𝑆⟶(SubGrp‘𝐻)) ∧ 𝑥 ∈ dom 𝑆) → 𝐴 ∈ (SubGrp‘𝐺)) | 
| 75 | 63 | mrcsscl 17664 | . . . . . . . . . . . . . . 15
⊢
(((SubGrp‘𝐺)
∈ (Moore‘(Base‘𝐺)) ∧ ∪ (𝑆 “ (dom 𝑆 ∖ {𝑥})) ⊆ 𝐴 ∧ 𝐴 ∈ (SubGrp‘𝐺)) → ((mrCls‘(SubGrp‘𝐺))‘∪ (𝑆
“ (dom 𝑆 ∖
{𝑥}))) ⊆ 𝐴) | 
| 76 | 40, 67, 74, 75 | syl3anc 1372 | . . . . . . . . . . . . . 14
⊢ (((𝐴 ∈ (SubGrp‘𝐺) ∧ 𝑆:dom 𝑆⟶(SubGrp‘𝐻)) ∧ 𝑥 ∈ dom 𝑆) → ((mrCls‘(SubGrp‘𝐺))‘∪ (𝑆
“ (dom 𝑆 ∖
{𝑥}))) ⊆ 𝐴) | 
| 77 | 12 | subsubg 19168 | . . . . . . . . . . . . . . 15
⊢ (𝐴 ∈ (SubGrp‘𝐺) →
(((mrCls‘(SubGrp‘𝐺))‘∪ (𝑆 “ (dom 𝑆 ∖ {𝑥}))) ∈ (SubGrp‘𝐻) ↔ (((mrCls‘(SubGrp‘𝐺))‘∪ (𝑆
“ (dom 𝑆 ∖
{𝑥}))) ∈
(SubGrp‘𝐺) ∧
((mrCls‘(SubGrp‘𝐺))‘∪ (𝑆 “ (dom 𝑆 ∖ {𝑥}))) ⊆ 𝐴))) | 
| 78 | 77 | ad2antrr 726 | . . . . . . . . . . . . . 14
⊢ (((𝐴 ∈ (SubGrp‘𝐺) ∧ 𝑆:dom 𝑆⟶(SubGrp‘𝐻)) ∧ 𝑥 ∈ dom 𝑆) → (((mrCls‘(SubGrp‘𝐺))‘∪ (𝑆
“ (dom 𝑆 ∖
{𝑥}))) ∈
(SubGrp‘𝐻) ↔
(((mrCls‘(SubGrp‘𝐺))‘∪ (𝑆 “ (dom 𝑆 ∖ {𝑥}))) ∈ (SubGrp‘𝐺) ∧ ((mrCls‘(SubGrp‘𝐺))‘∪ (𝑆
“ (dom 𝑆 ∖
{𝑥}))) ⊆ 𝐴))) | 
| 79 | 73, 76, 78 | mpbir2and 713 | . . . . . . . . . . . . 13
⊢ (((𝐴 ∈ (SubGrp‘𝐺) ∧ 𝑆:dom 𝑆⟶(SubGrp‘𝐻)) ∧ 𝑥 ∈ dom 𝑆) → ((mrCls‘(SubGrp‘𝐺))‘∪ (𝑆
“ (dom 𝑆 ∖
{𝑥}))) ∈
(SubGrp‘𝐻)) | 
| 80 | 46 | mrcsscl 17664 | . . . . . . . . . . . . 13
⊢
(((SubGrp‘𝐻)
∈ (Moore‘(Base‘𝐻)) ∧ ∪ (𝑆 “ (dom 𝑆 ∖ {𝑥})) ⊆ ((mrCls‘(SubGrp‘𝐺))‘∪ (𝑆
“ (dom 𝑆 ∖
{𝑥}))) ∧
((mrCls‘(SubGrp‘𝐺))‘∪ (𝑆 “ (dom 𝑆 ∖ {𝑥}))) ∈ (SubGrp‘𝐻)) → ((mrCls‘(SubGrp‘𝐻))‘∪ (𝑆
“ (dom 𝑆 ∖
{𝑥}))) ⊆
((mrCls‘(SubGrp‘𝐺))‘∪ (𝑆 “ (dom 𝑆 ∖ {𝑥})))) | 
| 81 | 45, 71, 79, 80 | syl3anc 1372 | . . . . . . . . . . . 12
⊢ (((𝐴 ∈ (SubGrp‘𝐺) ∧ 𝑆:dom 𝑆⟶(SubGrp‘𝐻)) ∧ 𝑥 ∈ dom 𝑆) → ((mrCls‘(SubGrp‘𝐻))‘∪ (𝑆
“ (dom 𝑆 ∖
{𝑥}))) ⊆
((mrCls‘(SubGrp‘𝐺))‘∪ (𝑆 “ (dom 𝑆 ∖ {𝑥})))) | 
| 82 | 65, 81 | eqssd 4000 | . . . . . . . . . . 11
⊢ (((𝐴 ∈ (SubGrp‘𝐺) ∧ 𝑆:dom 𝑆⟶(SubGrp‘𝐻)) ∧ 𝑥 ∈ dom 𝑆) → ((mrCls‘(SubGrp‘𝐺))‘∪ (𝑆
“ (dom 𝑆 ∖
{𝑥}))) =
((mrCls‘(SubGrp‘𝐻))‘∪ (𝑆 “ (dom 𝑆 ∖ {𝑥})))) | 
| 83 | 82 | ineq2d 4219 | . . . . . . . . . 10
⊢ (((𝐴 ∈ (SubGrp‘𝐺) ∧ 𝑆:dom 𝑆⟶(SubGrp‘𝐻)) ∧ 𝑥 ∈ dom 𝑆) → ((𝑆‘𝑥) ∩ ((mrCls‘(SubGrp‘𝐺))‘∪ (𝑆
“ (dom 𝑆 ∖
{𝑥})))) = ((𝑆‘𝑥) ∩ ((mrCls‘(SubGrp‘𝐻))‘∪ (𝑆
“ (dom 𝑆 ∖
{𝑥}))))) | 
| 84 |  | eqid 2736 | . . . . . . . . . . . . 13
⊢
(0g‘𝐺) = (0g‘𝐺) | 
| 85 | 12, 84 | subg0 19151 | . . . . . . . . . . . 12
⊢ (𝐴 ∈ (SubGrp‘𝐺) →
(0g‘𝐺) =
(0g‘𝐻)) | 
| 86 | 85 | ad2antrr 726 | . . . . . . . . . . 11
⊢ (((𝐴 ∈ (SubGrp‘𝐺) ∧ 𝑆:dom 𝑆⟶(SubGrp‘𝐻)) ∧ 𝑥 ∈ dom 𝑆) → (0g‘𝐺) = (0g‘𝐻)) | 
| 87 | 86 | sneqd 4637 | . . . . . . . . . 10
⊢ (((𝐴 ∈ (SubGrp‘𝐺) ∧ 𝑆:dom 𝑆⟶(SubGrp‘𝐻)) ∧ 𝑥 ∈ dom 𝑆) → {(0g‘𝐺)} = {(0g‘𝐻)}) | 
| 88 | 83, 87 | eqeq12d 2752 | . . . . . . . . 9
⊢ (((𝐴 ∈ (SubGrp‘𝐺) ∧ 𝑆:dom 𝑆⟶(SubGrp‘𝐻)) ∧ 𝑥 ∈ dom 𝑆) → (((𝑆‘𝑥) ∩ ((mrCls‘(SubGrp‘𝐺))‘∪ (𝑆
“ (dom 𝑆 ∖
{𝑥})))) =
{(0g‘𝐺)}
↔ ((𝑆‘𝑥) ∩
((mrCls‘(SubGrp‘𝐻))‘∪ (𝑆 “ (dom 𝑆 ∖ {𝑥})))) = {(0g‘𝐻)})) | 
| 89 | 34, 88 | anbi12d 632 | . . . . . . . 8
⊢ (((𝐴 ∈ (SubGrp‘𝐺) ∧ 𝑆:dom 𝑆⟶(SubGrp‘𝐻)) ∧ 𝑥 ∈ dom 𝑆) → ((∀𝑦 ∈ (dom 𝑆 ∖ {𝑥})(𝑆‘𝑥) ⊆ ((Cntz‘𝐺)‘(𝑆‘𝑦)) ∧ ((𝑆‘𝑥) ∩ ((mrCls‘(SubGrp‘𝐺))‘∪ (𝑆
“ (dom 𝑆 ∖
{𝑥})))) =
{(0g‘𝐺)})
↔ (∀𝑦 ∈
(dom 𝑆 ∖ {𝑥})(𝑆‘𝑥) ⊆ ((Cntz‘𝐻)‘(𝑆‘𝑦)) ∧ ((𝑆‘𝑥) ∩ ((mrCls‘(SubGrp‘𝐻))‘∪ (𝑆
“ (dom 𝑆 ∖
{𝑥})))) =
{(0g‘𝐻)}))) | 
| 90 | 89 | ralbidva 3175 | . . . . . . 7
⊢ ((𝐴 ∈ (SubGrp‘𝐺) ∧ 𝑆:dom 𝑆⟶(SubGrp‘𝐻)) → (∀𝑥 ∈ dom 𝑆(∀𝑦 ∈ (dom 𝑆 ∖ {𝑥})(𝑆‘𝑥) ⊆ ((Cntz‘𝐺)‘(𝑆‘𝑦)) ∧ ((𝑆‘𝑥) ∩ ((mrCls‘(SubGrp‘𝐺))‘∪ (𝑆
“ (dom 𝑆 ∖
{𝑥})))) =
{(0g‘𝐺)})
↔ ∀𝑥 ∈ dom
𝑆(∀𝑦 ∈ (dom 𝑆 ∖ {𝑥})(𝑆‘𝑥) ⊆ ((Cntz‘𝐻)‘(𝑆‘𝑦)) ∧ ((𝑆‘𝑥) ∩ ((mrCls‘(SubGrp‘𝐻))‘∪ (𝑆
“ (dom 𝑆 ∖
{𝑥})))) =
{(0g‘𝐻)}))) | 
| 91 | 90 | pm5.32da 579 | . . . . . 6
⊢ (𝐴 ∈ (SubGrp‘𝐺) → ((𝑆:dom 𝑆⟶(SubGrp‘𝐻) ∧ ∀𝑥 ∈ dom 𝑆(∀𝑦 ∈ (dom 𝑆 ∖ {𝑥})(𝑆‘𝑥) ⊆ ((Cntz‘𝐺)‘(𝑆‘𝑦)) ∧ ((𝑆‘𝑥) ∩ ((mrCls‘(SubGrp‘𝐺))‘∪ (𝑆
“ (dom 𝑆 ∖
{𝑥})))) =
{(0g‘𝐺)}))
↔ (𝑆:dom 𝑆⟶(SubGrp‘𝐻) ∧ ∀𝑥 ∈ dom 𝑆(∀𝑦 ∈ (dom 𝑆 ∖ {𝑥})(𝑆‘𝑥) ⊆ ((Cntz‘𝐻)‘(𝑆‘𝑦)) ∧ ((𝑆‘𝑥) ∩ ((mrCls‘(SubGrp‘𝐻))‘∪ (𝑆
“ (dom 𝑆 ∖
{𝑥})))) =
{(0g‘𝐻)})))) | 
| 92 | 12 | subsubg 19168 | . . . . . . . . . . . . 13
⊢ (𝐴 ∈ (SubGrp‘𝐺) → (𝑥 ∈ (SubGrp‘𝐻) ↔ (𝑥 ∈ (SubGrp‘𝐺) ∧ 𝑥 ⊆ 𝐴))) | 
| 93 |  | elin 3966 | . . . . . . . . . . . . . 14
⊢ (𝑥 ∈ ((SubGrp‘𝐺) ∩ 𝒫 𝐴) ↔ (𝑥 ∈ (SubGrp‘𝐺) ∧ 𝑥 ∈ 𝒫 𝐴)) | 
| 94 |  | velpw 4604 | . . . . . . . . . . . . . . 15
⊢ (𝑥 ∈ 𝒫 𝐴 ↔ 𝑥 ⊆ 𝐴) | 
| 95 | 94 | anbi2i 623 | . . . . . . . . . . . . . 14
⊢ ((𝑥 ∈ (SubGrp‘𝐺) ∧ 𝑥 ∈ 𝒫 𝐴) ↔ (𝑥 ∈ (SubGrp‘𝐺) ∧ 𝑥 ⊆ 𝐴)) | 
| 96 | 93, 95 | bitri 275 | . . . . . . . . . . . . 13
⊢ (𝑥 ∈ ((SubGrp‘𝐺) ∩ 𝒫 𝐴) ↔ (𝑥 ∈ (SubGrp‘𝐺) ∧ 𝑥 ⊆ 𝐴)) | 
| 97 | 92, 96 | bitr4di 289 | . . . . . . . . . . . 12
⊢ (𝐴 ∈ (SubGrp‘𝐺) → (𝑥 ∈ (SubGrp‘𝐻) ↔ 𝑥 ∈ ((SubGrp‘𝐺) ∩ 𝒫 𝐴))) | 
| 98 | 97 | eqrdv 2734 | . . . . . . . . . . 11
⊢ (𝐴 ∈ (SubGrp‘𝐺) → (SubGrp‘𝐻) = ((SubGrp‘𝐺) ∩ 𝒫 𝐴)) | 
| 99 | 98 | sseq2d 4015 | . . . . . . . . . 10
⊢ (𝐴 ∈ (SubGrp‘𝐺) → (ran 𝑆 ⊆ (SubGrp‘𝐻) ↔ ran 𝑆 ⊆ ((SubGrp‘𝐺) ∩ 𝒫 𝐴))) | 
| 100 |  | ssin 4238 | . . . . . . . . . 10
⊢ ((ran
𝑆 ⊆
(SubGrp‘𝐺) ∧ ran
𝑆 ⊆ 𝒫 𝐴) ↔ ran 𝑆 ⊆ ((SubGrp‘𝐺) ∩ 𝒫 𝐴)) | 
| 101 | 99, 100 | bitr4di 289 | . . . . . . . . 9
⊢ (𝐴 ∈ (SubGrp‘𝐺) → (ran 𝑆 ⊆ (SubGrp‘𝐻) ↔ (ran 𝑆 ⊆ (SubGrp‘𝐺) ∧ ran 𝑆 ⊆ 𝒫 𝐴))) | 
| 102 | 101 | anbi2d 630 | . . . . . . . 8
⊢ (𝐴 ∈ (SubGrp‘𝐺) → ((𝑆 Fn dom 𝑆 ∧ ran 𝑆 ⊆ (SubGrp‘𝐻)) ↔ (𝑆 Fn dom 𝑆 ∧ (ran 𝑆 ⊆ (SubGrp‘𝐺) ∧ ran 𝑆 ⊆ 𝒫 𝐴)))) | 
| 103 |  | df-f 6564 | . . . . . . . 8
⊢ (𝑆:dom 𝑆⟶(SubGrp‘𝐻) ↔ (𝑆 Fn dom 𝑆 ∧ ran 𝑆 ⊆ (SubGrp‘𝐻))) | 
| 104 |  | df-f 6564 | . . . . . . . . . 10
⊢ (𝑆:dom 𝑆⟶(SubGrp‘𝐺) ↔ (𝑆 Fn dom 𝑆 ∧ ran 𝑆 ⊆ (SubGrp‘𝐺))) | 
| 105 | 104 | anbi1i 624 | . . . . . . . . 9
⊢ ((𝑆:dom 𝑆⟶(SubGrp‘𝐺) ∧ ran 𝑆 ⊆ 𝒫 𝐴) ↔ ((𝑆 Fn dom 𝑆 ∧ ran 𝑆 ⊆ (SubGrp‘𝐺)) ∧ ran 𝑆 ⊆ 𝒫 𝐴)) | 
| 106 |  | anass 468 | . . . . . . . . 9
⊢ (((𝑆 Fn dom 𝑆 ∧ ran 𝑆 ⊆ (SubGrp‘𝐺)) ∧ ran 𝑆 ⊆ 𝒫 𝐴) ↔ (𝑆 Fn dom 𝑆 ∧ (ran 𝑆 ⊆ (SubGrp‘𝐺) ∧ ran 𝑆 ⊆ 𝒫 𝐴))) | 
| 107 | 105, 106 | bitri 275 | . . . . . . . 8
⊢ ((𝑆:dom 𝑆⟶(SubGrp‘𝐺) ∧ ran 𝑆 ⊆ 𝒫 𝐴) ↔ (𝑆 Fn dom 𝑆 ∧ (ran 𝑆 ⊆ (SubGrp‘𝐺) ∧ ran 𝑆 ⊆ 𝒫 𝐴))) | 
| 108 | 102, 103,
107 | 3bitr4g 314 | . . . . . . 7
⊢ (𝐴 ∈ (SubGrp‘𝐺) → (𝑆:dom 𝑆⟶(SubGrp‘𝐻) ↔ (𝑆:dom 𝑆⟶(SubGrp‘𝐺) ∧ ran 𝑆 ⊆ 𝒫 𝐴))) | 
| 109 | 108 | anbi1d 631 | . . . . . 6
⊢ (𝐴 ∈ (SubGrp‘𝐺) → ((𝑆:dom 𝑆⟶(SubGrp‘𝐻) ∧ ∀𝑥 ∈ dom 𝑆(∀𝑦 ∈ (dom 𝑆 ∖ {𝑥})(𝑆‘𝑥) ⊆ ((Cntz‘𝐺)‘(𝑆‘𝑦)) ∧ ((𝑆‘𝑥) ∩ ((mrCls‘(SubGrp‘𝐺))‘∪ (𝑆
“ (dom 𝑆 ∖
{𝑥})))) =
{(0g‘𝐺)}))
↔ ((𝑆:dom 𝑆⟶(SubGrp‘𝐺) ∧ ran 𝑆 ⊆ 𝒫 𝐴) ∧ ∀𝑥 ∈ dom 𝑆(∀𝑦 ∈ (dom 𝑆 ∖ {𝑥})(𝑆‘𝑥) ⊆ ((Cntz‘𝐺)‘(𝑆‘𝑦)) ∧ ((𝑆‘𝑥) ∩ ((mrCls‘(SubGrp‘𝐺))‘∪ (𝑆
“ (dom 𝑆 ∖
{𝑥})))) =
{(0g‘𝐺)})))) | 
| 110 | 91, 109 | bitr3d 281 | . . . . 5
⊢ (𝐴 ∈ (SubGrp‘𝐺) → ((𝑆:dom 𝑆⟶(SubGrp‘𝐻) ∧ ∀𝑥 ∈ dom 𝑆(∀𝑦 ∈ (dom 𝑆 ∖ {𝑥})(𝑆‘𝑥) ⊆ ((Cntz‘𝐻)‘(𝑆‘𝑦)) ∧ ((𝑆‘𝑥) ∩ ((mrCls‘(SubGrp‘𝐻))‘∪ (𝑆
“ (dom 𝑆 ∖
{𝑥})))) =
{(0g‘𝐻)}))
↔ ((𝑆:dom 𝑆⟶(SubGrp‘𝐺) ∧ ran 𝑆 ⊆ 𝒫 𝐴) ∧ ∀𝑥 ∈ dom 𝑆(∀𝑦 ∈ (dom 𝑆 ∖ {𝑥})(𝑆‘𝑥) ⊆ ((Cntz‘𝐺)‘(𝑆‘𝑦)) ∧ ((𝑆‘𝑥) ∩ ((mrCls‘(SubGrp‘𝐺))‘∪ (𝑆
“ (dom 𝑆 ∖
{𝑥})))) =
{(0g‘𝐺)})))) | 
| 111 | 110 | adantr 480 | . . . 4
⊢ ((𝐴 ∈ (SubGrp‘𝐺) ∧ 𝑆 ∈ V) → ((𝑆:dom 𝑆⟶(SubGrp‘𝐻) ∧ ∀𝑥 ∈ dom 𝑆(∀𝑦 ∈ (dom 𝑆 ∖ {𝑥})(𝑆‘𝑥) ⊆ ((Cntz‘𝐻)‘(𝑆‘𝑦)) ∧ ((𝑆‘𝑥) ∩ ((mrCls‘(SubGrp‘𝐻))‘∪ (𝑆
“ (dom 𝑆 ∖
{𝑥})))) =
{(0g‘𝐻)}))
↔ ((𝑆:dom 𝑆⟶(SubGrp‘𝐺) ∧ ran 𝑆 ⊆ 𝒫 𝐴) ∧ ∀𝑥 ∈ dom 𝑆(∀𝑦 ∈ (dom 𝑆 ∖ {𝑥})(𝑆‘𝑥) ⊆ ((Cntz‘𝐺)‘(𝑆‘𝑦)) ∧ ((𝑆‘𝑥) ∩ ((mrCls‘(SubGrp‘𝐺))‘∪ (𝑆
“ (dom 𝑆 ∖
{𝑥})))) =
{(0g‘𝐺)})))) | 
| 112 |  | dmexg 7924 | . . . . . 6
⊢ (𝑆 ∈ V → dom 𝑆 ∈ V) | 
| 113 | 112 | adantl 481 | . . . . 5
⊢ ((𝐴 ∈ (SubGrp‘𝐺) ∧ 𝑆 ∈ V) → dom 𝑆 ∈ V) | 
| 114 |  | eqidd 2737 | . . . . 5
⊢ ((𝐴 ∈ (SubGrp‘𝐺) ∧ 𝑆 ∈ V) → dom 𝑆 = dom 𝑆) | 
| 115 | 41 | adantr 480 | . . . . 5
⊢ ((𝐴 ∈ (SubGrp‘𝐺) ∧ 𝑆 ∈ V) → 𝐻 ∈ Grp) | 
| 116 |  | eqid 2736 | . . . . . . . 8
⊢
(0g‘𝐻) = (0g‘𝐻) | 
| 117 | 26, 116, 46 | dmdprd 20019 | . . . . . . 7
⊢ ((dom
𝑆 ∈ V ∧ dom 𝑆 = dom 𝑆) → (𝐻dom DProd 𝑆 ↔ (𝐻 ∈ Grp ∧ 𝑆:dom 𝑆⟶(SubGrp‘𝐻) ∧ ∀𝑥 ∈ dom 𝑆(∀𝑦 ∈ (dom 𝑆 ∖ {𝑥})(𝑆‘𝑥) ⊆ ((Cntz‘𝐻)‘(𝑆‘𝑦)) ∧ ((𝑆‘𝑥) ∩ ((mrCls‘(SubGrp‘𝐻))‘∪ (𝑆
“ (dom 𝑆 ∖
{𝑥})))) =
{(0g‘𝐻)})))) | 
| 118 |  | 3anass 1094 | . . . . . . 7
⊢ ((𝐻 ∈ Grp ∧ 𝑆:dom 𝑆⟶(SubGrp‘𝐻) ∧ ∀𝑥 ∈ dom 𝑆(∀𝑦 ∈ (dom 𝑆 ∖ {𝑥})(𝑆‘𝑥) ⊆ ((Cntz‘𝐻)‘(𝑆‘𝑦)) ∧ ((𝑆‘𝑥) ∩ ((mrCls‘(SubGrp‘𝐻))‘∪ (𝑆
“ (dom 𝑆 ∖
{𝑥})))) =
{(0g‘𝐻)}))
↔ (𝐻 ∈ Grp ∧
(𝑆:dom 𝑆⟶(SubGrp‘𝐻) ∧ ∀𝑥 ∈ dom 𝑆(∀𝑦 ∈ (dom 𝑆 ∖ {𝑥})(𝑆‘𝑥) ⊆ ((Cntz‘𝐻)‘(𝑆‘𝑦)) ∧ ((𝑆‘𝑥) ∩ ((mrCls‘(SubGrp‘𝐻))‘∪ (𝑆
“ (dom 𝑆 ∖
{𝑥})))) =
{(0g‘𝐻)})))) | 
| 119 | 117, 118 | bitrdi 287 | . . . . . 6
⊢ ((dom
𝑆 ∈ V ∧ dom 𝑆 = dom 𝑆) → (𝐻dom DProd 𝑆 ↔ (𝐻 ∈ Grp ∧ (𝑆:dom 𝑆⟶(SubGrp‘𝐻) ∧ ∀𝑥 ∈ dom 𝑆(∀𝑦 ∈ (dom 𝑆 ∖ {𝑥})(𝑆‘𝑥) ⊆ ((Cntz‘𝐻)‘(𝑆‘𝑦)) ∧ ((𝑆‘𝑥) ∩ ((mrCls‘(SubGrp‘𝐻))‘∪ (𝑆
“ (dom 𝑆 ∖
{𝑥})))) =
{(0g‘𝐻)}))))) | 
| 120 | 119 | baibd 539 | . . . . 5
⊢ (((dom
𝑆 ∈ V ∧ dom 𝑆 = dom 𝑆) ∧ 𝐻 ∈ Grp) → (𝐻dom DProd 𝑆 ↔ (𝑆:dom 𝑆⟶(SubGrp‘𝐻) ∧ ∀𝑥 ∈ dom 𝑆(∀𝑦 ∈ (dom 𝑆 ∖ {𝑥})(𝑆‘𝑥) ⊆ ((Cntz‘𝐻)‘(𝑆‘𝑦)) ∧ ((𝑆‘𝑥) ∩ ((mrCls‘(SubGrp‘𝐻))‘∪ (𝑆
“ (dom 𝑆 ∖
{𝑥})))) =
{(0g‘𝐻)})))) | 
| 121 | 113, 114,
115, 120 | syl21anc 837 | . . . 4
⊢ ((𝐴 ∈ (SubGrp‘𝐺) ∧ 𝑆 ∈ V) → (𝐻dom DProd 𝑆 ↔ (𝑆:dom 𝑆⟶(SubGrp‘𝐻) ∧ ∀𝑥 ∈ dom 𝑆(∀𝑦 ∈ (dom 𝑆 ∖ {𝑥})(𝑆‘𝑥) ⊆ ((Cntz‘𝐻)‘(𝑆‘𝑦)) ∧ ((𝑆‘𝑥) ∩ ((mrCls‘(SubGrp‘𝐻))‘∪ (𝑆
“ (dom 𝑆 ∖
{𝑥})))) =
{(0g‘𝐻)})))) | 
| 122 | 35 | adantr 480 | . . . . . . 7
⊢ ((𝐴 ∈ (SubGrp‘𝐺) ∧ 𝑆 ∈ V) → 𝐺 ∈ Grp) | 
| 123 | 25, 84, 63 | dmdprd 20019 | . . . . . . . . 9
⊢ ((dom
𝑆 ∈ V ∧ dom 𝑆 = dom 𝑆) → (𝐺dom DProd 𝑆 ↔ (𝐺 ∈ Grp ∧ 𝑆:dom 𝑆⟶(SubGrp‘𝐺) ∧ ∀𝑥 ∈ dom 𝑆(∀𝑦 ∈ (dom 𝑆 ∖ {𝑥})(𝑆‘𝑥) ⊆ ((Cntz‘𝐺)‘(𝑆‘𝑦)) ∧ ((𝑆‘𝑥) ∩ ((mrCls‘(SubGrp‘𝐺))‘∪ (𝑆
“ (dom 𝑆 ∖
{𝑥})))) =
{(0g‘𝐺)})))) | 
| 124 |  | 3anass 1094 | . . . . . . . . 9
⊢ ((𝐺 ∈ Grp ∧ 𝑆:dom 𝑆⟶(SubGrp‘𝐺) ∧ ∀𝑥 ∈ dom 𝑆(∀𝑦 ∈ (dom 𝑆 ∖ {𝑥})(𝑆‘𝑥) ⊆ ((Cntz‘𝐺)‘(𝑆‘𝑦)) ∧ ((𝑆‘𝑥) ∩ ((mrCls‘(SubGrp‘𝐺))‘∪ (𝑆
“ (dom 𝑆 ∖
{𝑥})))) =
{(0g‘𝐺)}))
↔ (𝐺 ∈ Grp ∧
(𝑆:dom 𝑆⟶(SubGrp‘𝐺) ∧ ∀𝑥 ∈ dom 𝑆(∀𝑦 ∈ (dom 𝑆 ∖ {𝑥})(𝑆‘𝑥) ⊆ ((Cntz‘𝐺)‘(𝑆‘𝑦)) ∧ ((𝑆‘𝑥) ∩ ((mrCls‘(SubGrp‘𝐺))‘∪ (𝑆
“ (dom 𝑆 ∖
{𝑥})))) =
{(0g‘𝐺)})))) | 
| 125 | 123, 124 | bitrdi 287 | . . . . . . . 8
⊢ ((dom
𝑆 ∈ V ∧ dom 𝑆 = dom 𝑆) → (𝐺dom DProd 𝑆 ↔ (𝐺 ∈ Grp ∧ (𝑆:dom 𝑆⟶(SubGrp‘𝐺) ∧ ∀𝑥 ∈ dom 𝑆(∀𝑦 ∈ (dom 𝑆 ∖ {𝑥})(𝑆‘𝑥) ⊆ ((Cntz‘𝐺)‘(𝑆‘𝑦)) ∧ ((𝑆‘𝑥) ∩ ((mrCls‘(SubGrp‘𝐺))‘∪ (𝑆
“ (dom 𝑆 ∖
{𝑥})))) =
{(0g‘𝐺)}))))) | 
| 126 | 125 | baibd 539 | . . . . . . 7
⊢ (((dom
𝑆 ∈ V ∧ dom 𝑆 = dom 𝑆) ∧ 𝐺 ∈ Grp) → (𝐺dom DProd 𝑆 ↔ (𝑆:dom 𝑆⟶(SubGrp‘𝐺) ∧ ∀𝑥 ∈ dom 𝑆(∀𝑦 ∈ (dom 𝑆 ∖ {𝑥})(𝑆‘𝑥) ⊆ ((Cntz‘𝐺)‘(𝑆‘𝑦)) ∧ ((𝑆‘𝑥) ∩ ((mrCls‘(SubGrp‘𝐺))‘∪ (𝑆
“ (dom 𝑆 ∖
{𝑥})))) =
{(0g‘𝐺)})))) | 
| 127 | 113, 114,
122, 126 | syl21anc 837 | . . . . . 6
⊢ ((𝐴 ∈ (SubGrp‘𝐺) ∧ 𝑆 ∈ V) → (𝐺dom DProd 𝑆 ↔ (𝑆:dom 𝑆⟶(SubGrp‘𝐺) ∧ ∀𝑥 ∈ dom 𝑆(∀𝑦 ∈ (dom 𝑆 ∖ {𝑥})(𝑆‘𝑥) ⊆ ((Cntz‘𝐺)‘(𝑆‘𝑦)) ∧ ((𝑆‘𝑥) ∩ ((mrCls‘(SubGrp‘𝐺))‘∪ (𝑆
“ (dom 𝑆 ∖
{𝑥})))) =
{(0g‘𝐺)})))) | 
| 128 | 127 | anbi1d 631 | . . . . 5
⊢ ((𝐴 ∈ (SubGrp‘𝐺) ∧ 𝑆 ∈ V) → ((𝐺dom DProd 𝑆 ∧ ran 𝑆 ⊆ 𝒫 𝐴) ↔ ((𝑆:dom 𝑆⟶(SubGrp‘𝐺) ∧ ∀𝑥 ∈ dom 𝑆(∀𝑦 ∈ (dom 𝑆 ∖ {𝑥})(𝑆‘𝑥) ⊆ ((Cntz‘𝐺)‘(𝑆‘𝑦)) ∧ ((𝑆‘𝑥) ∩ ((mrCls‘(SubGrp‘𝐺))‘∪ (𝑆
“ (dom 𝑆 ∖
{𝑥})))) =
{(0g‘𝐺)}))
∧ ran 𝑆 ⊆
𝒫 𝐴))) | 
| 129 |  | an32 646 | . . . . 5
⊢ (((𝑆:dom 𝑆⟶(SubGrp‘𝐺) ∧ ∀𝑥 ∈ dom 𝑆(∀𝑦 ∈ (dom 𝑆 ∖ {𝑥})(𝑆‘𝑥) ⊆ ((Cntz‘𝐺)‘(𝑆‘𝑦)) ∧ ((𝑆‘𝑥) ∩ ((mrCls‘(SubGrp‘𝐺))‘∪ (𝑆
“ (dom 𝑆 ∖
{𝑥})))) =
{(0g‘𝐺)}))
∧ ran 𝑆 ⊆
𝒫 𝐴) ↔ ((𝑆:dom 𝑆⟶(SubGrp‘𝐺) ∧ ran 𝑆 ⊆ 𝒫 𝐴) ∧ ∀𝑥 ∈ dom 𝑆(∀𝑦 ∈ (dom 𝑆 ∖ {𝑥})(𝑆‘𝑥) ⊆ ((Cntz‘𝐺)‘(𝑆‘𝑦)) ∧ ((𝑆‘𝑥) ∩ ((mrCls‘(SubGrp‘𝐺))‘∪ (𝑆
“ (dom 𝑆 ∖
{𝑥})))) =
{(0g‘𝐺)}))) | 
| 130 | 128, 129 | bitrdi 287 | . . . 4
⊢ ((𝐴 ∈ (SubGrp‘𝐺) ∧ 𝑆 ∈ V) → ((𝐺dom DProd 𝑆 ∧ ran 𝑆 ⊆ 𝒫 𝐴) ↔ ((𝑆:dom 𝑆⟶(SubGrp‘𝐺) ∧ ran 𝑆 ⊆ 𝒫 𝐴) ∧ ∀𝑥 ∈ dom 𝑆(∀𝑦 ∈ (dom 𝑆 ∖ {𝑥})(𝑆‘𝑥) ⊆ ((Cntz‘𝐺)‘(𝑆‘𝑦)) ∧ ((𝑆‘𝑥) ∩ ((mrCls‘(SubGrp‘𝐺))‘∪ (𝑆
“ (dom 𝑆 ∖
{𝑥})))) =
{(0g‘𝐺)})))) | 
| 131 | 111, 121,
130 | 3bitr4d 311 | . . 3
⊢ ((𝐴 ∈ (SubGrp‘𝐺) ∧ 𝑆 ∈ V) → (𝐻dom DProd 𝑆 ↔ (𝐺dom DProd 𝑆 ∧ ran 𝑆 ⊆ 𝒫 𝐴))) | 
| 132 | 131 | ex 412 | . 2
⊢ (𝐴 ∈ (SubGrp‘𝐺) → (𝑆 ∈ V → (𝐻dom DProd 𝑆 ↔ (𝐺dom DProd 𝑆 ∧ ran 𝑆 ⊆ 𝒫 𝐴)))) | 
| 133 | 3, 6, 132 | pm5.21ndd 379 | 1
⊢ (𝐴 ∈ (SubGrp‘𝐺) → (𝐻dom DProd 𝑆 ↔ (𝐺dom DProd 𝑆 ∧ ran 𝑆 ⊆ 𝒫 𝐴))) |