| Step | Hyp | Ref
| Expression |
| 1 | | dprdres.1 |
. . . 4
⊢ (𝜑 → 𝐺dom DProd 𝑆) |
| 2 | | dprdgrp 20025 |
. . . 4
⊢ (𝐺dom DProd 𝑆 → 𝐺 ∈ Grp) |
| 3 | 1, 2 | syl 17 |
. . 3
⊢ (𝜑 → 𝐺 ∈ Grp) |
| 4 | | dprdres.2 |
. . . . 5
⊢ (𝜑 → dom 𝑆 = 𝐼) |
| 5 | 1, 4 | dprdf2 20027 |
. . . 4
⊢ (𝜑 → 𝑆:𝐼⟶(SubGrp‘𝐺)) |
| 6 | | dprdres.3 |
. . . 4
⊢ (𝜑 → 𝐴 ⊆ 𝐼) |
| 7 | 5, 6 | fssresd 6775 |
. . 3
⊢ (𝜑 → (𝑆 ↾ 𝐴):𝐴⟶(SubGrp‘𝐺)) |
| 8 | 1 | ad2antrr 726 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑦 ∈ (𝐴 ∖ {𝑥})) → 𝐺dom DProd 𝑆) |
| 9 | 4 | ad2antrr 726 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑦 ∈ (𝐴 ∖ {𝑥})) → dom 𝑆 = 𝐼) |
| 10 | 6 | ad2antrr 726 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑦 ∈ (𝐴 ∖ {𝑥})) → 𝐴 ⊆ 𝐼) |
| 11 | | simplr 769 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑦 ∈ (𝐴 ∖ {𝑥})) → 𝑥 ∈ 𝐴) |
| 12 | 10, 11 | sseldd 3984 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑦 ∈ (𝐴 ∖ {𝑥})) → 𝑥 ∈ 𝐼) |
| 13 | | eldifi 4131 |
. . . . . . . . . 10
⊢ (𝑦 ∈ (𝐴 ∖ {𝑥}) → 𝑦 ∈ 𝐴) |
| 14 | 13 | adantl 481 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑦 ∈ (𝐴 ∖ {𝑥})) → 𝑦 ∈ 𝐴) |
| 15 | 10, 14 | sseldd 3984 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑦 ∈ (𝐴 ∖ {𝑥})) → 𝑦 ∈ 𝐼) |
| 16 | | eldifsni 4790 |
. . . . . . . . . 10
⊢ (𝑦 ∈ (𝐴 ∖ {𝑥}) → 𝑦 ≠ 𝑥) |
| 17 | 16 | adantl 481 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑦 ∈ (𝐴 ∖ {𝑥})) → 𝑦 ≠ 𝑥) |
| 18 | 17 | necomd 2996 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑦 ∈ (𝐴 ∖ {𝑥})) → 𝑥 ≠ 𝑦) |
| 19 | | eqid 2737 |
. . . . . . . 8
⊢
(Cntz‘𝐺) =
(Cntz‘𝐺) |
| 20 | 8, 9, 12, 15, 18, 19 | dprdcntz 20028 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑦 ∈ (𝐴 ∖ {𝑥})) → (𝑆‘𝑥) ⊆ ((Cntz‘𝐺)‘(𝑆‘𝑦))) |
| 21 | 11 | fvresd 6926 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑦 ∈ (𝐴 ∖ {𝑥})) → ((𝑆 ↾ 𝐴)‘𝑥) = (𝑆‘𝑥)) |
| 22 | 14 | fvresd 6926 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑦 ∈ (𝐴 ∖ {𝑥})) → ((𝑆 ↾ 𝐴)‘𝑦) = (𝑆‘𝑦)) |
| 23 | 22 | fveq2d 6910 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑦 ∈ (𝐴 ∖ {𝑥})) → ((Cntz‘𝐺)‘((𝑆 ↾ 𝐴)‘𝑦)) = ((Cntz‘𝐺)‘(𝑆‘𝑦))) |
| 24 | 20, 21, 23 | 3sstr4d 4039 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑦 ∈ (𝐴 ∖ {𝑥})) → ((𝑆 ↾ 𝐴)‘𝑥) ⊆ ((Cntz‘𝐺)‘((𝑆 ↾ 𝐴)‘𝑦))) |
| 25 | 24 | ralrimiva 3146 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ∀𝑦 ∈ (𝐴 ∖ {𝑥})((𝑆 ↾ 𝐴)‘𝑥) ⊆ ((Cntz‘𝐺)‘((𝑆 ↾ 𝐴)‘𝑦))) |
| 26 | | fvres 6925 |
. . . . . . . 8
⊢ (𝑥 ∈ 𝐴 → ((𝑆 ↾ 𝐴)‘𝑥) = (𝑆‘𝑥)) |
| 27 | 26 | adantl 481 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ((𝑆 ↾ 𝐴)‘𝑥) = (𝑆‘𝑥)) |
| 28 | 27 | ineq1d 4219 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (((𝑆 ↾ 𝐴)‘𝑥) ∩ ((mrCls‘(SubGrp‘𝐺))‘∪ ((𝑆
↾ 𝐴) “ (𝐴 ∖ {𝑥})))) = ((𝑆‘𝑥) ∩ ((mrCls‘(SubGrp‘𝐺))‘∪ ((𝑆
↾ 𝐴) “ (𝐴 ∖ {𝑥}))))) |
| 29 | | eqid 2737 |
. . . . . . . . . . . . 13
⊢
(Base‘𝐺) =
(Base‘𝐺) |
| 30 | 29 | subgacs 19179 |
. . . . . . . . . . . 12
⊢ (𝐺 ∈ Grp →
(SubGrp‘𝐺) ∈
(ACS‘(Base‘𝐺))) |
| 31 | | acsmre 17695 |
. . . . . . . . . . . 12
⊢
((SubGrp‘𝐺)
∈ (ACS‘(Base‘𝐺)) → (SubGrp‘𝐺) ∈ (Moore‘(Base‘𝐺))) |
| 32 | 3, 30, 31 | 3syl 18 |
. . . . . . . . . . 11
⊢ (𝜑 → (SubGrp‘𝐺) ∈
(Moore‘(Base‘𝐺))) |
| 33 | 32 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (SubGrp‘𝐺) ∈ (Moore‘(Base‘𝐺))) |
| 34 | | eqid 2737 |
. . . . . . . . . 10
⊢
(mrCls‘(SubGrp‘𝐺)) = (mrCls‘(SubGrp‘𝐺)) |
| 35 | | resss 6019 |
. . . . . . . . . . . . 13
⊢ (𝑆 ↾ 𝐴) ⊆ 𝑆 |
| 36 | | imass1 6119 |
. . . . . . . . . . . . 13
⊢ ((𝑆 ↾ 𝐴) ⊆ 𝑆 → ((𝑆 ↾ 𝐴) “ (𝐴 ∖ {𝑥})) ⊆ (𝑆 “ (𝐴 ∖ {𝑥}))) |
| 37 | 35, 36 | ax-mp 5 |
. . . . . . . . . . . 12
⊢ ((𝑆 ↾ 𝐴) “ (𝐴 ∖ {𝑥})) ⊆ (𝑆 “ (𝐴 ∖ {𝑥})) |
| 38 | 6 | adantr 480 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐴 ⊆ 𝐼) |
| 39 | | ssdif 4144 |
. . . . . . . . . . . . 13
⊢ (𝐴 ⊆ 𝐼 → (𝐴 ∖ {𝑥}) ⊆ (𝐼 ∖ {𝑥})) |
| 40 | | imass2 6120 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∖ {𝑥}) ⊆ (𝐼 ∖ {𝑥}) → (𝑆 “ (𝐴 ∖ {𝑥})) ⊆ (𝑆 “ (𝐼 ∖ {𝑥}))) |
| 41 | 38, 39, 40 | 3syl 18 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝑆 “ (𝐴 ∖ {𝑥})) ⊆ (𝑆 “ (𝐼 ∖ {𝑥}))) |
| 42 | 37, 41 | sstrid 3995 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ((𝑆 ↾ 𝐴) “ (𝐴 ∖ {𝑥})) ⊆ (𝑆 “ (𝐼 ∖ {𝑥}))) |
| 43 | 42 | unissd 4917 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ∪
((𝑆 ↾ 𝐴) “ (𝐴 ∖ {𝑥})) ⊆ ∪
(𝑆 “ (𝐼 ∖ {𝑥}))) |
| 44 | | imassrn 6089 |
. . . . . . . . . . . 12
⊢ (𝑆 “ (𝐼 ∖ {𝑥})) ⊆ ran 𝑆 |
| 45 | 5 | frnd 6744 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ran 𝑆 ⊆ (SubGrp‘𝐺)) |
| 46 | 29 | subgss 19145 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 ∈ (SubGrp‘𝐺) → 𝑥 ⊆ (Base‘𝐺)) |
| 47 | | velpw 4605 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 ∈ 𝒫
(Base‘𝐺) ↔ 𝑥 ⊆ (Base‘𝐺)) |
| 48 | 46, 47 | sylibr 234 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 ∈ (SubGrp‘𝐺) → 𝑥 ∈ 𝒫 (Base‘𝐺)) |
| 49 | 48 | ssriv 3987 |
. . . . . . . . . . . . . 14
⊢
(SubGrp‘𝐺)
⊆ 𝒫 (Base‘𝐺) |
| 50 | 45, 49 | sstrdi 3996 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ran 𝑆 ⊆ 𝒫 (Base‘𝐺)) |
| 51 | 50 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ran 𝑆 ⊆ 𝒫 (Base‘𝐺)) |
| 52 | 44, 51 | sstrid 3995 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝑆 “ (𝐼 ∖ {𝑥})) ⊆ 𝒫 (Base‘𝐺)) |
| 53 | | sspwuni 5100 |
. . . . . . . . . . 11
⊢ ((𝑆 “ (𝐼 ∖ {𝑥})) ⊆ 𝒫 (Base‘𝐺) ↔ ∪ (𝑆
“ (𝐼 ∖ {𝑥})) ⊆ (Base‘𝐺)) |
| 54 | 52, 53 | sylib 218 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ∪ (𝑆 “ (𝐼 ∖ {𝑥})) ⊆ (Base‘𝐺)) |
| 55 | 33, 34, 43, 54 | mrcssd 17667 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ((mrCls‘(SubGrp‘𝐺))‘∪ ((𝑆
↾ 𝐴) “ (𝐴 ∖ {𝑥}))) ⊆
((mrCls‘(SubGrp‘𝐺))‘∪ (𝑆 “ (𝐼 ∖ {𝑥})))) |
| 56 | | sslin 4243 |
. . . . . . . . 9
⊢
(((mrCls‘(SubGrp‘𝐺))‘∪
((𝑆 ↾ 𝐴) “ (𝐴 ∖ {𝑥}))) ⊆
((mrCls‘(SubGrp‘𝐺))‘∪ (𝑆 “ (𝐼 ∖ {𝑥}))) → ((𝑆‘𝑥) ∩ ((mrCls‘(SubGrp‘𝐺))‘∪ ((𝑆
↾ 𝐴) “ (𝐴 ∖ {𝑥})))) ⊆ ((𝑆‘𝑥) ∩ ((mrCls‘(SubGrp‘𝐺))‘∪ (𝑆
“ (𝐼 ∖ {𝑥}))))) |
| 57 | 55, 56 | syl 17 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ((𝑆‘𝑥) ∩ ((mrCls‘(SubGrp‘𝐺))‘∪ ((𝑆
↾ 𝐴) “ (𝐴 ∖ {𝑥})))) ⊆ ((𝑆‘𝑥) ∩ ((mrCls‘(SubGrp‘𝐺))‘∪ (𝑆
“ (𝐼 ∖ {𝑥}))))) |
| 58 | 1 | adantr 480 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐺dom DProd 𝑆) |
| 59 | 4 | adantr 480 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → dom 𝑆 = 𝐼) |
| 60 | 6 | sselda 3983 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝑥 ∈ 𝐼) |
| 61 | | eqid 2737 |
. . . . . . . . 9
⊢
(0g‘𝐺) = (0g‘𝐺) |
| 62 | 58, 59, 60, 61, 34 | dprddisj 20029 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ((𝑆‘𝑥) ∩ ((mrCls‘(SubGrp‘𝐺))‘∪ (𝑆
“ (𝐼 ∖ {𝑥})))) =
{(0g‘𝐺)}) |
| 63 | 57, 62 | sseqtrd 4020 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ((𝑆‘𝑥) ∩ ((mrCls‘(SubGrp‘𝐺))‘∪ ((𝑆
↾ 𝐴) “ (𝐴 ∖ {𝑥})))) ⊆ {(0g‘𝐺)}) |
| 64 | 5 | ffvelcdmda 7104 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → (𝑆‘𝑥) ∈ (SubGrp‘𝐺)) |
| 65 | 60, 64 | syldan 591 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝑆‘𝑥) ∈ (SubGrp‘𝐺)) |
| 66 | 61 | subg0cl 19152 |
. . . . . . . . . 10
⊢ ((𝑆‘𝑥) ∈ (SubGrp‘𝐺) → (0g‘𝐺) ∈ (𝑆‘𝑥)) |
| 67 | 65, 66 | syl 17 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (0g‘𝐺) ∈ (𝑆‘𝑥)) |
| 68 | 43, 54 | sstrd 3994 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ∪
((𝑆 ↾ 𝐴) “ (𝐴 ∖ {𝑥})) ⊆ (Base‘𝐺)) |
| 69 | 34 | mrccl 17654 |
. . . . . . . . . . 11
⊢
(((SubGrp‘𝐺)
∈ (Moore‘(Base‘𝐺)) ∧ ∪
((𝑆 ↾ 𝐴) “ (𝐴 ∖ {𝑥})) ⊆ (Base‘𝐺)) → ((mrCls‘(SubGrp‘𝐺))‘∪ ((𝑆
↾ 𝐴) “ (𝐴 ∖ {𝑥}))) ∈ (SubGrp‘𝐺)) |
| 70 | 33, 68, 69 | syl2anc 584 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ((mrCls‘(SubGrp‘𝐺))‘∪ ((𝑆
↾ 𝐴) “ (𝐴 ∖ {𝑥}))) ∈ (SubGrp‘𝐺)) |
| 71 | 61 | subg0cl 19152 |
. . . . . . . . . 10
⊢
(((mrCls‘(SubGrp‘𝐺))‘∪
((𝑆 ↾ 𝐴) “ (𝐴 ∖ {𝑥}))) ∈ (SubGrp‘𝐺) → (0g‘𝐺) ∈
((mrCls‘(SubGrp‘𝐺))‘∪
((𝑆 ↾ 𝐴) “ (𝐴 ∖ {𝑥})))) |
| 72 | 70, 71 | syl 17 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (0g‘𝐺) ∈
((mrCls‘(SubGrp‘𝐺))‘∪
((𝑆 ↾ 𝐴) “ (𝐴 ∖ {𝑥})))) |
| 73 | 67, 72 | elind 4200 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (0g‘𝐺) ∈ ((𝑆‘𝑥) ∩ ((mrCls‘(SubGrp‘𝐺))‘∪ ((𝑆
↾ 𝐴) “ (𝐴 ∖ {𝑥}))))) |
| 74 | 73 | snssd 4809 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → {(0g‘𝐺)} ⊆ ((𝑆‘𝑥) ∩ ((mrCls‘(SubGrp‘𝐺))‘∪ ((𝑆
↾ 𝐴) “ (𝐴 ∖ {𝑥}))))) |
| 75 | 63, 74 | eqssd 4001 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ((𝑆‘𝑥) ∩ ((mrCls‘(SubGrp‘𝐺))‘∪ ((𝑆
↾ 𝐴) “ (𝐴 ∖ {𝑥})))) = {(0g‘𝐺)}) |
| 76 | 28, 75 | eqtrd 2777 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (((𝑆 ↾ 𝐴)‘𝑥) ∩ ((mrCls‘(SubGrp‘𝐺))‘∪ ((𝑆
↾ 𝐴) “ (𝐴 ∖ {𝑥})))) = {(0g‘𝐺)}) |
| 77 | 25, 76 | jca 511 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (∀𝑦 ∈ (𝐴 ∖ {𝑥})((𝑆 ↾ 𝐴)‘𝑥) ⊆ ((Cntz‘𝐺)‘((𝑆 ↾ 𝐴)‘𝑦)) ∧ (((𝑆 ↾ 𝐴)‘𝑥) ∩ ((mrCls‘(SubGrp‘𝐺))‘∪ ((𝑆
↾ 𝐴) “ (𝐴 ∖ {𝑥})))) = {(0g‘𝐺)})) |
| 78 | 77 | ralrimiva 3146 |
. . 3
⊢ (𝜑 → ∀𝑥 ∈ 𝐴 (∀𝑦 ∈ (𝐴 ∖ {𝑥})((𝑆 ↾ 𝐴)‘𝑥) ⊆ ((Cntz‘𝐺)‘((𝑆 ↾ 𝐴)‘𝑦)) ∧ (((𝑆 ↾ 𝐴)‘𝑥) ∩ ((mrCls‘(SubGrp‘𝐺))‘∪ ((𝑆
↾ 𝐴) “ (𝐴 ∖ {𝑥})))) = {(0g‘𝐺)})) |
| 79 | 1, 4 | dprddomcld 20021 |
. . . . 5
⊢ (𝜑 → 𝐼 ∈ V) |
| 80 | 79, 6 | ssexd 5324 |
. . . 4
⊢ (𝜑 → 𝐴 ∈ V) |
| 81 | 7 | fdmd 6746 |
. . . 4
⊢ (𝜑 → dom (𝑆 ↾ 𝐴) = 𝐴) |
| 82 | 19, 61, 34 | dmdprd 20018 |
. . . 4
⊢ ((𝐴 ∈ V ∧ dom (𝑆 ↾ 𝐴) = 𝐴) → (𝐺dom DProd (𝑆 ↾ 𝐴) ↔ (𝐺 ∈ Grp ∧ (𝑆 ↾ 𝐴):𝐴⟶(SubGrp‘𝐺) ∧ ∀𝑥 ∈ 𝐴 (∀𝑦 ∈ (𝐴 ∖ {𝑥})((𝑆 ↾ 𝐴)‘𝑥) ⊆ ((Cntz‘𝐺)‘((𝑆 ↾ 𝐴)‘𝑦)) ∧ (((𝑆 ↾ 𝐴)‘𝑥) ∩ ((mrCls‘(SubGrp‘𝐺))‘∪ ((𝑆
↾ 𝐴) “ (𝐴 ∖ {𝑥})))) = {(0g‘𝐺)})))) |
| 83 | 80, 81, 82 | syl2anc 584 |
. . 3
⊢ (𝜑 → (𝐺dom DProd (𝑆 ↾ 𝐴) ↔ (𝐺 ∈ Grp ∧ (𝑆 ↾ 𝐴):𝐴⟶(SubGrp‘𝐺) ∧ ∀𝑥 ∈ 𝐴 (∀𝑦 ∈ (𝐴 ∖ {𝑥})((𝑆 ↾ 𝐴)‘𝑥) ⊆ ((Cntz‘𝐺)‘((𝑆 ↾ 𝐴)‘𝑦)) ∧ (((𝑆 ↾ 𝐴)‘𝑥) ∩ ((mrCls‘(SubGrp‘𝐺))‘∪ ((𝑆
↾ 𝐴) “ (𝐴 ∖ {𝑥})))) = {(0g‘𝐺)})))) |
| 84 | 3, 7, 78, 83 | mpbir3and 1343 |
. 2
⊢ (𝜑 → 𝐺dom DProd (𝑆 ↾ 𝐴)) |
| 85 | | rnss 5950 |
. . . . . 6
⊢ ((𝑆 ↾ 𝐴) ⊆ 𝑆 → ran (𝑆 ↾ 𝐴) ⊆ ran 𝑆) |
| 86 | | uniss 4915 |
. . . . . 6
⊢ (ran
(𝑆 ↾ 𝐴) ⊆ ran 𝑆 → ∪ ran
(𝑆 ↾ 𝐴) ⊆ ∪ ran 𝑆) |
| 87 | 35, 85, 86 | mp2b 10 |
. . . . 5
⊢ ∪ ran (𝑆 ↾ 𝐴) ⊆ ∪ ran
𝑆 |
| 88 | 87 | a1i 11 |
. . . 4
⊢ (𝜑 → ∪ ran (𝑆 ↾ 𝐴) ⊆ ∪ ran
𝑆) |
| 89 | | sspwuni 5100 |
. . . . 5
⊢ (ran
𝑆 ⊆ 𝒫
(Base‘𝐺) ↔ ∪ ran 𝑆 ⊆ (Base‘𝐺)) |
| 90 | 50, 89 | sylib 218 |
. . . 4
⊢ (𝜑 → ∪ ran 𝑆 ⊆ (Base‘𝐺)) |
| 91 | 32, 34, 88, 90 | mrcssd 17667 |
. . 3
⊢ (𝜑 →
((mrCls‘(SubGrp‘𝐺))‘∪ ran
(𝑆 ↾ 𝐴)) ⊆
((mrCls‘(SubGrp‘𝐺))‘∪ ran
𝑆)) |
| 92 | 34 | dprdspan 20047 |
. . . 4
⊢ (𝐺dom DProd (𝑆 ↾ 𝐴) → (𝐺 DProd (𝑆 ↾ 𝐴)) = ((mrCls‘(SubGrp‘𝐺))‘∪ ran (𝑆 ↾ 𝐴))) |
| 93 | 84, 92 | syl 17 |
. . 3
⊢ (𝜑 → (𝐺 DProd (𝑆 ↾ 𝐴)) = ((mrCls‘(SubGrp‘𝐺))‘∪ ran (𝑆 ↾ 𝐴))) |
| 94 | 34 | dprdspan 20047 |
. . . 4
⊢ (𝐺dom DProd 𝑆 → (𝐺 DProd 𝑆) = ((mrCls‘(SubGrp‘𝐺))‘∪ ran 𝑆)) |
| 95 | 1, 94 | syl 17 |
. . 3
⊢ (𝜑 → (𝐺 DProd 𝑆) = ((mrCls‘(SubGrp‘𝐺))‘∪ ran 𝑆)) |
| 96 | 91, 93, 95 | 3sstr4d 4039 |
. 2
⊢ (𝜑 → (𝐺 DProd (𝑆 ↾ 𝐴)) ⊆ (𝐺 DProd 𝑆)) |
| 97 | 84, 96 | jca 511 |
1
⊢ (𝜑 → (𝐺dom DProd (𝑆 ↾ 𝐴) ∧ (𝐺 DProd (𝑆 ↾ 𝐴)) ⊆ (𝐺 DProd 𝑆))) |