| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | dprdsplit.u | . . . . . 6
⊢ (𝜑 → 𝐼 = (𝐶 ∪ 𝐷)) | 
| 2 | 1 | adantr 480 | . . . . 5
⊢ ((𝜑 ∧ 𝑋 ∈ 𝐶) → 𝐼 = (𝐶 ∪ 𝐷)) | 
| 3 | 2 | eleq2d 2826 | . . . 4
⊢ ((𝜑 ∧ 𝑋 ∈ 𝐶) → (𝑌 ∈ 𝐼 ↔ 𝑌 ∈ (𝐶 ∪ 𝐷))) | 
| 4 |  | elun 4152 | . . . 4
⊢ (𝑌 ∈ (𝐶 ∪ 𝐷) ↔ (𝑌 ∈ 𝐶 ∨ 𝑌 ∈ 𝐷)) | 
| 5 | 3, 4 | bitrdi 287 | . . 3
⊢ ((𝜑 ∧ 𝑋 ∈ 𝐶) → (𝑌 ∈ 𝐼 ↔ (𝑌 ∈ 𝐶 ∨ 𝑌 ∈ 𝐷))) | 
| 6 |  | dmdprdsplit2.1 | . . . . . . . 8
⊢ (𝜑 → 𝐺dom DProd (𝑆 ↾ 𝐶)) | 
| 7 | 6 | ad2antrr 726 | . . . . . . 7
⊢ (((𝜑 ∧ 𝑋 ∈ 𝐶) ∧ (𝑌 ∈ 𝐶 ∧ 𝑋 ≠ 𝑌)) → 𝐺dom DProd (𝑆 ↾ 𝐶)) | 
| 8 |  | dprdsplit.2 | . . . . . . . . . 10
⊢ (𝜑 → 𝑆:𝐼⟶(SubGrp‘𝐺)) | 
| 9 |  | ssun1 4177 | . . . . . . . . . . 11
⊢ 𝐶 ⊆ (𝐶 ∪ 𝐷) | 
| 10 | 9, 1 | sseqtrrid 4026 | . . . . . . . . . 10
⊢ (𝜑 → 𝐶 ⊆ 𝐼) | 
| 11 | 8, 10 | fssresd 6774 | . . . . . . . . 9
⊢ (𝜑 → (𝑆 ↾ 𝐶):𝐶⟶(SubGrp‘𝐺)) | 
| 12 | 11 | fdmd 6745 | . . . . . . . 8
⊢ (𝜑 → dom (𝑆 ↾ 𝐶) = 𝐶) | 
| 13 | 12 | ad2antrr 726 | . . . . . . 7
⊢ (((𝜑 ∧ 𝑋 ∈ 𝐶) ∧ (𝑌 ∈ 𝐶 ∧ 𝑋 ≠ 𝑌)) → dom (𝑆 ↾ 𝐶) = 𝐶) | 
| 14 |  | simplr 768 | . . . . . . 7
⊢ (((𝜑 ∧ 𝑋 ∈ 𝐶) ∧ (𝑌 ∈ 𝐶 ∧ 𝑋 ≠ 𝑌)) → 𝑋 ∈ 𝐶) | 
| 15 |  | simprl 770 | . . . . . . 7
⊢ (((𝜑 ∧ 𝑋 ∈ 𝐶) ∧ (𝑌 ∈ 𝐶 ∧ 𝑋 ≠ 𝑌)) → 𝑌 ∈ 𝐶) | 
| 16 |  | simprr 772 | . . . . . . 7
⊢ (((𝜑 ∧ 𝑋 ∈ 𝐶) ∧ (𝑌 ∈ 𝐶 ∧ 𝑋 ≠ 𝑌)) → 𝑋 ≠ 𝑌) | 
| 17 |  | dmdprdsplit.z | . . . . . . 7
⊢ 𝑍 = (Cntz‘𝐺) | 
| 18 | 7, 13, 14, 15, 16, 17 | dprdcntz 20029 | . . . . . 6
⊢ (((𝜑 ∧ 𝑋 ∈ 𝐶) ∧ (𝑌 ∈ 𝐶 ∧ 𝑋 ≠ 𝑌)) → ((𝑆 ↾ 𝐶)‘𝑋) ⊆ (𝑍‘((𝑆 ↾ 𝐶)‘𝑌))) | 
| 19 |  | fvres 6924 | . . . . . . 7
⊢ (𝑋 ∈ 𝐶 → ((𝑆 ↾ 𝐶)‘𝑋) = (𝑆‘𝑋)) | 
| 20 | 19 | ad2antlr 727 | . . . . . 6
⊢ (((𝜑 ∧ 𝑋 ∈ 𝐶) ∧ (𝑌 ∈ 𝐶 ∧ 𝑋 ≠ 𝑌)) → ((𝑆 ↾ 𝐶)‘𝑋) = (𝑆‘𝑋)) | 
| 21 |  | fvres 6924 | . . . . . . . 8
⊢ (𝑌 ∈ 𝐶 → ((𝑆 ↾ 𝐶)‘𝑌) = (𝑆‘𝑌)) | 
| 22 | 21 | ad2antrl 728 | . . . . . . 7
⊢ (((𝜑 ∧ 𝑋 ∈ 𝐶) ∧ (𝑌 ∈ 𝐶 ∧ 𝑋 ≠ 𝑌)) → ((𝑆 ↾ 𝐶)‘𝑌) = (𝑆‘𝑌)) | 
| 23 | 22 | fveq2d 6909 | . . . . . 6
⊢ (((𝜑 ∧ 𝑋 ∈ 𝐶) ∧ (𝑌 ∈ 𝐶 ∧ 𝑋 ≠ 𝑌)) → (𝑍‘((𝑆 ↾ 𝐶)‘𝑌)) = (𝑍‘(𝑆‘𝑌))) | 
| 24 | 18, 20, 23 | 3sstr3d 4037 | . . . . 5
⊢ (((𝜑 ∧ 𝑋 ∈ 𝐶) ∧ (𝑌 ∈ 𝐶 ∧ 𝑋 ≠ 𝑌)) → (𝑆‘𝑋) ⊆ (𝑍‘(𝑆‘𝑌))) | 
| 25 | 24 | exp32 420 | . . . 4
⊢ ((𝜑 ∧ 𝑋 ∈ 𝐶) → (𝑌 ∈ 𝐶 → (𝑋 ≠ 𝑌 → (𝑆‘𝑋) ⊆ (𝑍‘(𝑆‘𝑌))))) | 
| 26 | 19 | ad2antlr 727 | . . . . . . 7
⊢ (((𝜑 ∧ 𝑋 ∈ 𝐶) ∧ (𝑌 ∈ 𝐷 ∧ 𝑋 ≠ 𝑌)) → ((𝑆 ↾ 𝐶)‘𝑋) = (𝑆‘𝑋)) | 
| 27 | 6 | ad2antrr 726 | . . . . . . . 8
⊢ (((𝜑 ∧ 𝑋 ∈ 𝐶) ∧ (𝑌 ∈ 𝐷 ∧ 𝑋 ≠ 𝑌)) → 𝐺dom DProd (𝑆 ↾ 𝐶)) | 
| 28 | 12 | ad2antrr 726 | . . . . . . . 8
⊢ (((𝜑 ∧ 𝑋 ∈ 𝐶) ∧ (𝑌 ∈ 𝐷 ∧ 𝑋 ≠ 𝑌)) → dom (𝑆 ↾ 𝐶) = 𝐶) | 
| 29 |  | simplr 768 | . . . . . . . 8
⊢ (((𝜑 ∧ 𝑋 ∈ 𝐶) ∧ (𝑌 ∈ 𝐷 ∧ 𝑋 ≠ 𝑌)) → 𝑋 ∈ 𝐶) | 
| 30 | 27, 28, 29 | dprdub 20046 | . . . . . . 7
⊢ (((𝜑 ∧ 𝑋 ∈ 𝐶) ∧ (𝑌 ∈ 𝐷 ∧ 𝑋 ≠ 𝑌)) → ((𝑆 ↾ 𝐶)‘𝑋) ⊆ (𝐺 DProd (𝑆 ↾ 𝐶))) | 
| 31 | 26, 30 | eqsstrrd 4018 | . . . . . 6
⊢ (((𝜑 ∧ 𝑋 ∈ 𝐶) ∧ (𝑌 ∈ 𝐷 ∧ 𝑋 ≠ 𝑌)) → (𝑆‘𝑋) ⊆ (𝐺 DProd (𝑆 ↾ 𝐶))) | 
| 32 |  | dmdprdsplit2.3 | . . . . . . . 8
⊢ (𝜑 → (𝐺 DProd (𝑆 ↾ 𝐶)) ⊆ (𝑍‘(𝐺 DProd (𝑆 ↾ 𝐷)))) | 
| 33 | 32 | ad2antrr 726 | . . . . . . 7
⊢ (((𝜑 ∧ 𝑋 ∈ 𝐶) ∧ (𝑌 ∈ 𝐷 ∧ 𝑋 ≠ 𝑌)) → (𝐺 DProd (𝑆 ↾ 𝐶)) ⊆ (𝑍‘(𝐺 DProd (𝑆 ↾ 𝐷)))) | 
| 34 |  | eqid 2736 | . . . . . . . . 9
⊢
(Base‘𝐺) =
(Base‘𝐺) | 
| 35 | 34 | dprdssv 20037 | . . . . . . . 8
⊢ (𝐺 DProd (𝑆 ↾ 𝐷)) ⊆ (Base‘𝐺) | 
| 36 |  | fvres 6924 | . . . . . . . . . 10
⊢ (𝑌 ∈ 𝐷 → ((𝑆 ↾ 𝐷)‘𝑌) = (𝑆‘𝑌)) | 
| 37 | 36 | ad2antrl 728 | . . . . . . . . 9
⊢ (((𝜑 ∧ 𝑋 ∈ 𝐶) ∧ (𝑌 ∈ 𝐷 ∧ 𝑋 ≠ 𝑌)) → ((𝑆 ↾ 𝐷)‘𝑌) = (𝑆‘𝑌)) | 
| 38 |  | dmdprdsplit2.2 | . . . . . . . . . . 11
⊢ (𝜑 → 𝐺dom DProd (𝑆 ↾ 𝐷)) | 
| 39 | 38 | ad2antrr 726 | . . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑋 ∈ 𝐶) ∧ (𝑌 ∈ 𝐷 ∧ 𝑋 ≠ 𝑌)) → 𝐺dom DProd (𝑆 ↾ 𝐷)) | 
| 40 |  | ssun2 4178 | . . . . . . . . . . . . . 14
⊢ 𝐷 ⊆ (𝐶 ∪ 𝐷) | 
| 41 | 40, 1 | sseqtrrid 4026 | . . . . . . . . . . . . 13
⊢ (𝜑 → 𝐷 ⊆ 𝐼) | 
| 42 | 8, 41 | fssresd 6774 | . . . . . . . . . . . 12
⊢ (𝜑 → (𝑆 ↾ 𝐷):𝐷⟶(SubGrp‘𝐺)) | 
| 43 | 42 | fdmd 6745 | . . . . . . . . . . 11
⊢ (𝜑 → dom (𝑆 ↾ 𝐷) = 𝐷) | 
| 44 | 43 | ad2antrr 726 | . . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑋 ∈ 𝐶) ∧ (𝑌 ∈ 𝐷 ∧ 𝑋 ≠ 𝑌)) → dom (𝑆 ↾ 𝐷) = 𝐷) | 
| 45 |  | simprl 770 | . . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑋 ∈ 𝐶) ∧ (𝑌 ∈ 𝐷 ∧ 𝑋 ≠ 𝑌)) → 𝑌 ∈ 𝐷) | 
| 46 | 39, 44, 45 | dprdub 20046 | . . . . . . . . 9
⊢ (((𝜑 ∧ 𝑋 ∈ 𝐶) ∧ (𝑌 ∈ 𝐷 ∧ 𝑋 ≠ 𝑌)) → ((𝑆 ↾ 𝐷)‘𝑌) ⊆ (𝐺 DProd (𝑆 ↾ 𝐷))) | 
| 47 | 37, 46 | eqsstrrd 4018 | . . . . . . . 8
⊢ (((𝜑 ∧ 𝑋 ∈ 𝐶) ∧ (𝑌 ∈ 𝐷 ∧ 𝑋 ≠ 𝑌)) → (𝑆‘𝑌) ⊆ (𝐺 DProd (𝑆 ↾ 𝐷))) | 
| 48 | 34, 17 | cntz2ss 19354 | . . . . . . . 8
⊢ (((𝐺 DProd (𝑆 ↾ 𝐷)) ⊆ (Base‘𝐺) ∧ (𝑆‘𝑌) ⊆ (𝐺 DProd (𝑆 ↾ 𝐷))) → (𝑍‘(𝐺 DProd (𝑆 ↾ 𝐷))) ⊆ (𝑍‘(𝑆‘𝑌))) | 
| 49 | 35, 47, 48 | sylancr 587 | . . . . . . 7
⊢ (((𝜑 ∧ 𝑋 ∈ 𝐶) ∧ (𝑌 ∈ 𝐷 ∧ 𝑋 ≠ 𝑌)) → (𝑍‘(𝐺 DProd (𝑆 ↾ 𝐷))) ⊆ (𝑍‘(𝑆‘𝑌))) | 
| 50 | 33, 49 | sstrd 3993 | . . . . . 6
⊢ (((𝜑 ∧ 𝑋 ∈ 𝐶) ∧ (𝑌 ∈ 𝐷 ∧ 𝑋 ≠ 𝑌)) → (𝐺 DProd (𝑆 ↾ 𝐶)) ⊆ (𝑍‘(𝑆‘𝑌))) | 
| 51 | 31, 50 | sstrd 3993 | . . . . 5
⊢ (((𝜑 ∧ 𝑋 ∈ 𝐶) ∧ (𝑌 ∈ 𝐷 ∧ 𝑋 ≠ 𝑌)) → (𝑆‘𝑋) ⊆ (𝑍‘(𝑆‘𝑌))) | 
| 52 | 51 | exp32 420 | . . . 4
⊢ ((𝜑 ∧ 𝑋 ∈ 𝐶) → (𝑌 ∈ 𝐷 → (𝑋 ≠ 𝑌 → (𝑆‘𝑋) ⊆ (𝑍‘(𝑆‘𝑌))))) | 
| 53 | 25, 52 | jaod 859 | . . 3
⊢ ((𝜑 ∧ 𝑋 ∈ 𝐶) → ((𝑌 ∈ 𝐶 ∨ 𝑌 ∈ 𝐷) → (𝑋 ≠ 𝑌 → (𝑆‘𝑋) ⊆ (𝑍‘(𝑆‘𝑌))))) | 
| 54 | 5, 53 | sylbid 240 | . 2
⊢ ((𝜑 ∧ 𝑋 ∈ 𝐶) → (𝑌 ∈ 𝐼 → (𝑋 ≠ 𝑌 → (𝑆‘𝑋) ⊆ (𝑍‘(𝑆‘𝑌))))) | 
| 55 |  | dprdgrp 20026 | . . . . . . . 8
⊢ (𝐺dom DProd (𝑆 ↾ 𝐶) → 𝐺 ∈ Grp) | 
| 56 | 6, 55 | syl 17 | . . . . . . 7
⊢ (𝜑 → 𝐺 ∈ Grp) | 
| 57 | 56 | adantr 480 | . . . . . 6
⊢ ((𝜑 ∧ 𝑋 ∈ 𝐶) → 𝐺 ∈ Grp) | 
| 58 | 34 | subgacs 19180 | . . . . . 6
⊢ (𝐺 ∈ Grp →
(SubGrp‘𝐺) ∈
(ACS‘(Base‘𝐺))) | 
| 59 |  | acsmre 17696 | . . . . . 6
⊢
((SubGrp‘𝐺)
∈ (ACS‘(Base‘𝐺)) → (SubGrp‘𝐺) ∈ (Moore‘(Base‘𝐺))) | 
| 60 | 57, 58, 59 | 3syl 18 | . . . . 5
⊢ ((𝜑 ∧ 𝑋 ∈ 𝐶) → (SubGrp‘𝐺) ∈ (Moore‘(Base‘𝐺))) | 
| 61 |  | difundir 4290 | . . . . . . . . . . 11
⊢ ((𝐶 ∪ 𝐷) ∖ {𝑋}) = ((𝐶 ∖ {𝑋}) ∪ (𝐷 ∖ {𝑋})) | 
| 62 | 2 | difeq1d 4124 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑋 ∈ 𝐶) → (𝐼 ∖ {𝑋}) = ((𝐶 ∪ 𝐷) ∖ {𝑋})) | 
| 63 |  | simpr 484 | . . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑋 ∈ 𝐶) → 𝑋 ∈ 𝐶) | 
| 64 | 63 | snssd 4808 | . . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑋 ∈ 𝐶) → {𝑋} ⊆ 𝐶) | 
| 65 |  | sslin 4242 | . . . . . . . . . . . . . . 15
⊢ ({𝑋} ⊆ 𝐶 → (𝐷 ∩ {𝑋}) ⊆ (𝐷 ∩ 𝐶)) | 
| 66 | 64, 65 | syl 17 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑋 ∈ 𝐶) → (𝐷 ∩ {𝑋}) ⊆ (𝐷 ∩ 𝐶)) | 
| 67 |  | incom 4208 | . . . . . . . . . . . . . . 15
⊢ (𝐶 ∩ 𝐷) = (𝐷 ∩ 𝐶) | 
| 68 |  | dprdsplit.i | . . . . . . . . . . . . . . . 16
⊢ (𝜑 → (𝐶 ∩ 𝐷) = ∅) | 
| 69 | 68 | adantr 480 | . . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑋 ∈ 𝐶) → (𝐶 ∩ 𝐷) = ∅) | 
| 70 | 67, 69 | eqtr3id 2790 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑋 ∈ 𝐶) → (𝐷 ∩ 𝐶) = ∅) | 
| 71 |  | sseq0 4402 | . . . . . . . . . . . . . 14
⊢ (((𝐷 ∩ {𝑋}) ⊆ (𝐷 ∩ 𝐶) ∧ (𝐷 ∩ 𝐶) = ∅) → (𝐷 ∩ {𝑋}) = ∅) | 
| 72 | 66, 70, 71 | syl2anc 584 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑋 ∈ 𝐶) → (𝐷 ∩ {𝑋}) = ∅) | 
| 73 |  | disj3 4453 | . . . . . . . . . . . . 13
⊢ ((𝐷 ∩ {𝑋}) = ∅ ↔ 𝐷 = (𝐷 ∖ {𝑋})) | 
| 74 | 72, 73 | sylib 218 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑋 ∈ 𝐶) → 𝐷 = (𝐷 ∖ {𝑋})) | 
| 75 | 74 | uneq2d 4167 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑋 ∈ 𝐶) → ((𝐶 ∖ {𝑋}) ∪ 𝐷) = ((𝐶 ∖ {𝑋}) ∪ (𝐷 ∖ {𝑋}))) | 
| 76 | 61, 62, 75 | 3eqtr4a 2802 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑋 ∈ 𝐶) → (𝐼 ∖ {𝑋}) = ((𝐶 ∖ {𝑋}) ∪ 𝐷)) | 
| 77 | 76 | imaeq2d 6077 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑋 ∈ 𝐶) → (𝑆 “ (𝐼 ∖ {𝑋})) = (𝑆 “ ((𝐶 ∖ {𝑋}) ∪ 𝐷))) | 
| 78 |  | imaundi 6168 | . . . . . . . . 9
⊢ (𝑆 “ ((𝐶 ∖ {𝑋}) ∪ 𝐷)) = ((𝑆 “ (𝐶 ∖ {𝑋})) ∪ (𝑆 “ 𝐷)) | 
| 79 | 77, 78 | eqtrdi 2792 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑋 ∈ 𝐶) → (𝑆 “ (𝐼 ∖ {𝑋})) = ((𝑆 “ (𝐶 ∖ {𝑋})) ∪ (𝑆 “ 𝐷))) | 
| 80 | 79 | unieqd 4919 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑋 ∈ 𝐶) → ∪ (𝑆 “ (𝐼 ∖ {𝑋})) = ∪ ((𝑆 “ (𝐶 ∖ {𝑋})) ∪ (𝑆 “ 𝐷))) | 
| 81 |  | uniun 4929 | . . . . . . 7
⊢ ∪ ((𝑆
“ (𝐶 ∖ {𝑋})) ∪ (𝑆 “ 𝐷)) = (∪ (𝑆 “ (𝐶 ∖ {𝑋})) ∪ ∪
(𝑆 “ 𝐷)) | 
| 82 | 80, 81 | eqtrdi 2792 | . . . . . 6
⊢ ((𝜑 ∧ 𝑋 ∈ 𝐶) → ∪ (𝑆 “ (𝐼 ∖ {𝑋})) = (∪ (𝑆 “ (𝐶 ∖ {𝑋})) ∪ ∪
(𝑆 “ 𝐷))) | 
| 83 |  | dmdprdsplit2lem.k | . . . . . . . . 9
⊢ 𝐾 =
(mrCls‘(SubGrp‘𝐺)) | 
| 84 |  | difss 4135 | . . . . . . . . . . 11
⊢ (𝐶 ∖ {𝑋}) ⊆ 𝐶 | 
| 85 |  | imass2 6119 | . . . . . . . . . . 11
⊢ ((𝐶 ∖ {𝑋}) ⊆ 𝐶 → (𝑆 “ (𝐶 ∖ {𝑋})) ⊆ (𝑆 “ 𝐶)) | 
| 86 |  | uniss 4914 | . . . . . . . . . . 11
⊢ ((𝑆 “ (𝐶 ∖ {𝑋})) ⊆ (𝑆 “ 𝐶) → ∪ (𝑆 “ (𝐶 ∖ {𝑋})) ⊆ ∪
(𝑆 “ 𝐶)) | 
| 87 | 84, 85, 86 | mp2b 10 | . . . . . . . . . 10
⊢ ∪ (𝑆
“ (𝐶 ∖ {𝑋})) ⊆ ∪ (𝑆
“ 𝐶) | 
| 88 |  | imassrn 6088 | . . . . . . . . . . . 12
⊢ (𝑆 “ 𝐶) ⊆ ran 𝑆 | 
| 89 | 8 | frnd 6743 | . . . . . . . . . . . . . 14
⊢ (𝜑 → ran 𝑆 ⊆ (SubGrp‘𝐺)) | 
| 90 | 89 | adantr 480 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑋 ∈ 𝐶) → ran 𝑆 ⊆ (SubGrp‘𝐺)) | 
| 91 |  | mresspw 17636 | . . . . . . . . . . . . . 14
⊢
((SubGrp‘𝐺)
∈ (Moore‘(Base‘𝐺)) → (SubGrp‘𝐺) ⊆ 𝒫 (Base‘𝐺)) | 
| 92 | 60, 91 | syl 17 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑋 ∈ 𝐶) → (SubGrp‘𝐺) ⊆ 𝒫 (Base‘𝐺)) | 
| 93 | 90, 92 | sstrd 3993 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑋 ∈ 𝐶) → ran 𝑆 ⊆ 𝒫 (Base‘𝐺)) | 
| 94 | 88, 93 | sstrid 3994 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑋 ∈ 𝐶) → (𝑆 “ 𝐶) ⊆ 𝒫 (Base‘𝐺)) | 
| 95 |  | sspwuni 5099 | . . . . . . . . . . 11
⊢ ((𝑆 “ 𝐶) ⊆ 𝒫 (Base‘𝐺) ↔ ∪ (𝑆
“ 𝐶) ⊆
(Base‘𝐺)) | 
| 96 | 94, 95 | sylib 218 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑋 ∈ 𝐶) → ∪ (𝑆 “ 𝐶) ⊆ (Base‘𝐺)) | 
| 97 | 87, 96 | sstrid 3994 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑋 ∈ 𝐶) → ∪ (𝑆 “ (𝐶 ∖ {𝑋})) ⊆ (Base‘𝐺)) | 
| 98 | 60, 83, 97 | mrcssidd 17669 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑋 ∈ 𝐶) → ∪ (𝑆 “ (𝐶 ∖ {𝑋})) ⊆ (𝐾‘∪ (𝑆 “ (𝐶 ∖ {𝑋})))) | 
| 99 |  | imassrn 6088 | . . . . . . . . . . . 12
⊢ (𝑆 “ 𝐷) ⊆ ran 𝑆 | 
| 100 | 99, 93 | sstrid 3994 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑋 ∈ 𝐶) → (𝑆 “ 𝐷) ⊆ 𝒫 (Base‘𝐺)) | 
| 101 |  | sspwuni 5099 | . . . . . . . . . . 11
⊢ ((𝑆 “ 𝐷) ⊆ 𝒫 (Base‘𝐺) ↔ ∪ (𝑆
“ 𝐷) ⊆
(Base‘𝐺)) | 
| 102 | 100, 101 | sylib 218 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑋 ∈ 𝐶) → ∪ (𝑆 “ 𝐷) ⊆ (Base‘𝐺)) | 
| 103 | 60, 83, 102 | mrcssidd 17669 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑋 ∈ 𝐶) → ∪ (𝑆 “ 𝐷) ⊆ (𝐾‘∪ (𝑆 “ 𝐷))) | 
| 104 | 83 | dprdspan 20048 | . . . . . . . . . . . 12
⊢ (𝐺dom DProd (𝑆 ↾ 𝐷) → (𝐺 DProd (𝑆 ↾ 𝐷)) = (𝐾‘∪ ran
(𝑆 ↾ 𝐷))) | 
| 105 | 38, 104 | syl 17 | . . . . . . . . . . 11
⊢ (𝜑 → (𝐺 DProd (𝑆 ↾ 𝐷)) = (𝐾‘∪ ran
(𝑆 ↾ 𝐷))) | 
| 106 |  | df-ima 5697 | . . . . . . . . . . . . 13
⊢ (𝑆 “ 𝐷) = ran (𝑆 ↾ 𝐷) | 
| 107 | 106 | unieqi 4918 | . . . . . . . . . . . 12
⊢ ∪ (𝑆
“ 𝐷) = ∪ ran (𝑆 ↾ 𝐷) | 
| 108 | 107 | fveq2i 6908 | . . . . . . . . . . 11
⊢ (𝐾‘∪ (𝑆
“ 𝐷)) = (𝐾‘∪ ran (𝑆 ↾ 𝐷)) | 
| 109 | 105, 108 | eqtr4di 2794 | . . . . . . . . . 10
⊢ (𝜑 → (𝐺 DProd (𝑆 ↾ 𝐷)) = (𝐾‘∪ (𝑆 “ 𝐷))) | 
| 110 | 109 | adantr 480 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑋 ∈ 𝐶) → (𝐺 DProd (𝑆 ↾ 𝐷)) = (𝐾‘∪ (𝑆 “ 𝐷))) | 
| 111 | 103, 110 | sseqtrrd 4020 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑋 ∈ 𝐶) → ∪ (𝑆 “ 𝐷) ⊆ (𝐺 DProd (𝑆 ↾ 𝐷))) | 
| 112 |  | unss12 4187 | . . . . . . . 8
⊢ ((∪ (𝑆
“ (𝐶 ∖ {𝑋})) ⊆ (𝐾‘∪ (𝑆 “ (𝐶 ∖ {𝑋}))) ∧ ∪
(𝑆 “ 𝐷) ⊆ (𝐺 DProd (𝑆 ↾ 𝐷))) → (∪
(𝑆 “ (𝐶 ∖ {𝑋})) ∪ ∪
(𝑆 “ 𝐷)) ⊆ ((𝐾‘∪ (𝑆 “ (𝐶 ∖ {𝑋}))) ∪ (𝐺 DProd (𝑆 ↾ 𝐷)))) | 
| 113 | 98, 111, 112 | syl2anc 584 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑋 ∈ 𝐶) → (∪
(𝑆 “ (𝐶 ∖ {𝑋})) ∪ ∪
(𝑆 “ 𝐷)) ⊆ ((𝐾‘∪ (𝑆 “ (𝐶 ∖ {𝑋}))) ∪ (𝐺 DProd (𝑆 ↾ 𝐷)))) | 
| 114 | 83 | mrccl 17655 | . . . . . . . . 9
⊢
(((SubGrp‘𝐺)
∈ (Moore‘(Base‘𝐺)) ∧ ∪ (𝑆 “ (𝐶 ∖ {𝑋})) ⊆ (Base‘𝐺)) → (𝐾‘∪ (𝑆 “ (𝐶 ∖ {𝑋}))) ∈ (SubGrp‘𝐺)) | 
| 115 | 60, 97, 114 | syl2anc 584 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑋 ∈ 𝐶) → (𝐾‘∪ (𝑆 “ (𝐶 ∖ {𝑋}))) ∈ (SubGrp‘𝐺)) | 
| 116 |  | dprdsubg 20045 | . . . . . . . . . 10
⊢ (𝐺dom DProd (𝑆 ↾ 𝐷) → (𝐺 DProd (𝑆 ↾ 𝐷)) ∈ (SubGrp‘𝐺)) | 
| 117 | 38, 116 | syl 17 | . . . . . . . . 9
⊢ (𝜑 → (𝐺 DProd (𝑆 ↾ 𝐷)) ∈ (SubGrp‘𝐺)) | 
| 118 | 117 | adantr 480 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑋 ∈ 𝐶) → (𝐺 DProd (𝑆 ↾ 𝐷)) ∈ (SubGrp‘𝐺)) | 
| 119 |  | eqid 2736 | . . . . . . . . 9
⊢
(LSSum‘𝐺) =
(LSSum‘𝐺) | 
| 120 | 119 | lsmunss 19678 | . . . . . . . 8
⊢ (((𝐾‘∪ (𝑆
“ (𝐶 ∖ {𝑋}))) ∈ (SubGrp‘𝐺) ∧ (𝐺 DProd (𝑆 ↾ 𝐷)) ∈ (SubGrp‘𝐺)) → ((𝐾‘∪ (𝑆 “ (𝐶 ∖ {𝑋}))) ∪ (𝐺 DProd (𝑆 ↾ 𝐷))) ⊆ ((𝐾‘∪ (𝑆 “ (𝐶 ∖ {𝑋})))(LSSum‘𝐺)(𝐺 DProd (𝑆 ↾ 𝐷)))) | 
| 121 | 115, 118,
120 | syl2anc 584 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑋 ∈ 𝐶) → ((𝐾‘∪ (𝑆 “ (𝐶 ∖ {𝑋}))) ∪ (𝐺 DProd (𝑆 ↾ 𝐷))) ⊆ ((𝐾‘∪ (𝑆 “ (𝐶 ∖ {𝑋})))(LSSum‘𝐺)(𝐺 DProd (𝑆 ↾ 𝐷)))) | 
| 122 | 113, 121 | sstrd 3993 | . . . . . 6
⊢ ((𝜑 ∧ 𝑋 ∈ 𝐶) → (∪
(𝑆 “ (𝐶 ∖ {𝑋})) ∪ ∪
(𝑆 “ 𝐷)) ⊆ ((𝐾‘∪ (𝑆 “ (𝐶 ∖ {𝑋})))(LSSum‘𝐺)(𝐺 DProd (𝑆 ↾ 𝐷)))) | 
| 123 | 82, 122 | eqsstrd 4017 | . . . . 5
⊢ ((𝜑 ∧ 𝑋 ∈ 𝐶) → ∪ (𝑆 “ (𝐼 ∖ {𝑋})) ⊆ ((𝐾‘∪ (𝑆 “ (𝐶 ∖ {𝑋})))(LSSum‘𝐺)(𝐺 DProd (𝑆 ↾ 𝐷)))) | 
| 124 | 87 | a1i 11 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑋 ∈ 𝐶) → ∪ (𝑆 “ (𝐶 ∖ {𝑋})) ⊆ ∪
(𝑆 “ 𝐶)) | 
| 125 | 60, 83, 124, 96 | mrcssd 17668 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑋 ∈ 𝐶) → (𝐾‘∪ (𝑆 “ (𝐶 ∖ {𝑋}))) ⊆ (𝐾‘∪ (𝑆 “ 𝐶))) | 
| 126 | 83 | dprdspan 20048 | . . . . . . . . . . 11
⊢ (𝐺dom DProd (𝑆 ↾ 𝐶) → (𝐺 DProd (𝑆 ↾ 𝐶)) = (𝐾‘∪ ran
(𝑆 ↾ 𝐶))) | 
| 127 | 6, 126 | syl 17 | . . . . . . . . . 10
⊢ (𝜑 → (𝐺 DProd (𝑆 ↾ 𝐶)) = (𝐾‘∪ ran
(𝑆 ↾ 𝐶))) | 
| 128 |  | df-ima 5697 | . . . . . . . . . . . 12
⊢ (𝑆 “ 𝐶) = ran (𝑆 ↾ 𝐶) | 
| 129 | 128 | unieqi 4918 | . . . . . . . . . . 11
⊢ ∪ (𝑆
“ 𝐶) = ∪ ran (𝑆 ↾ 𝐶) | 
| 130 | 129 | fveq2i 6908 | . . . . . . . . . 10
⊢ (𝐾‘∪ (𝑆
“ 𝐶)) = (𝐾‘∪ ran (𝑆 ↾ 𝐶)) | 
| 131 | 127, 130 | eqtr4di 2794 | . . . . . . . . 9
⊢ (𝜑 → (𝐺 DProd (𝑆 ↾ 𝐶)) = (𝐾‘∪ (𝑆 “ 𝐶))) | 
| 132 | 131 | adantr 480 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑋 ∈ 𝐶) → (𝐺 DProd (𝑆 ↾ 𝐶)) = (𝐾‘∪ (𝑆 “ 𝐶))) | 
| 133 | 125, 132 | sseqtrrd 4020 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑋 ∈ 𝐶) → (𝐾‘∪ (𝑆 “ (𝐶 ∖ {𝑋}))) ⊆ (𝐺 DProd (𝑆 ↾ 𝐶))) | 
| 134 | 32 | adantr 480 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑋 ∈ 𝐶) → (𝐺 DProd (𝑆 ↾ 𝐶)) ⊆ (𝑍‘(𝐺 DProd (𝑆 ↾ 𝐷)))) | 
| 135 | 133, 134 | sstrd 3993 | . . . . . 6
⊢ ((𝜑 ∧ 𝑋 ∈ 𝐶) → (𝐾‘∪ (𝑆 “ (𝐶 ∖ {𝑋}))) ⊆ (𝑍‘(𝐺 DProd (𝑆 ↾ 𝐷)))) | 
| 136 | 119, 17 | lsmsubg 19673 | . . . . . 6
⊢ (((𝐾‘∪ (𝑆
“ (𝐶 ∖ {𝑋}))) ∈ (SubGrp‘𝐺) ∧ (𝐺 DProd (𝑆 ↾ 𝐷)) ∈ (SubGrp‘𝐺) ∧ (𝐾‘∪ (𝑆 “ (𝐶 ∖ {𝑋}))) ⊆ (𝑍‘(𝐺 DProd (𝑆 ↾ 𝐷)))) → ((𝐾‘∪ (𝑆 “ (𝐶 ∖ {𝑋})))(LSSum‘𝐺)(𝐺 DProd (𝑆 ↾ 𝐷))) ∈ (SubGrp‘𝐺)) | 
| 137 | 115, 118,
135, 136 | syl3anc 1372 | . . . . 5
⊢ ((𝜑 ∧ 𝑋 ∈ 𝐶) → ((𝐾‘∪ (𝑆 “ (𝐶 ∖ {𝑋})))(LSSum‘𝐺)(𝐺 DProd (𝑆 ↾ 𝐷))) ∈ (SubGrp‘𝐺)) | 
| 138 | 83 | mrcsscl 17664 | . . . . 5
⊢
(((SubGrp‘𝐺)
∈ (Moore‘(Base‘𝐺)) ∧ ∪ (𝑆 “ (𝐼 ∖ {𝑋})) ⊆ ((𝐾‘∪ (𝑆 “ (𝐶 ∖ {𝑋})))(LSSum‘𝐺)(𝐺 DProd (𝑆 ↾ 𝐷))) ∧ ((𝐾‘∪ (𝑆 “ (𝐶 ∖ {𝑋})))(LSSum‘𝐺)(𝐺 DProd (𝑆 ↾ 𝐷))) ∈ (SubGrp‘𝐺)) → (𝐾‘∪ (𝑆 “ (𝐼 ∖ {𝑋}))) ⊆ ((𝐾‘∪ (𝑆 “ (𝐶 ∖ {𝑋})))(LSSum‘𝐺)(𝐺 DProd (𝑆 ↾ 𝐷)))) | 
| 139 | 60, 123, 137, 138 | syl3anc 1372 | . . . 4
⊢ ((𝜑 ∧ 𝑋 ∈ 𝐶) → (𝐾‘∪ (𝑆 “ (𝐼 ∖ {𝑋}))) ⊆ ((𝐾‘∪ (𝑆 “ (𝐶 ∖ {𝑋})))(LSSum‘𝐺)(𝐺 DProd (𝑆 ↾ 𝐷)))) | 
| 140 |  | sslin 4242 | . . . 4
⊢ ((𝐾‘∪ (𝑆
“ (𝐼 ∖ {𝑋}))) ⊆ ((𝐾‘∪ (𝑆 “ (𝐶 ∖ {𝑋})))(LSSum‘𝐺)(𝐺 DProd (𝑆 ↾ 𝐷))) → ((𝑆‘𝑋) ∩ (𝐾‘∪ (𝑆 “ (𝐼 ∖ {𝑋})))) ⊆ ((𝑆‘𝑋) ∩ ((𝐾‘∪ (𝑆 “ (𝐶 ∖ {𝑋})))(LSSum‘𝐺)(𝐺 DProd (𝑆 ↾ 𝐷))))) | 
| 141 | 139, 140 | syl 17 | . . 3
⊢ ((𝜑 ∧ 𝑋 ∈ 𝐶) → ((𝑆‘𝑋) ∩ (𝐾‘∪ (𝑆 “ (𝐼 ∖ {𝑋})))) ⊆ ((𝑆‘𝑋) ∩ ((𝐾‘∪ (𝑆 “ (𝐶 ∖ {𝑋})))(LSSum‘𝐺)(𝐺 DProd (𝑆 ↾ 𝐷))))) | 
| 142 | 10 | sselda 3982 | . . . . 5
⊢ ((𝜑 ∧ 𝑋 ∈ 𝐶) → 𝑋 ∈ 𝐼) | 
| 143 | 8 | ffvelcdmda 7103 | . . . . 5
⊢ ((𝜑 ∧ 𝑋 ∈ 𝐼) → (𝑆‘𝑋) ∈ (SubGrp‘𝐺)) | 
| 144 | 142, 143 | syldan 591 | . . . 4
⊢ ((𝜑 ∧ 𝑋 ∈ 𝐶) → (𝑆‘𝑋) ∈ (SubGrp‘𝐺)) | 
| 145 |  | dmdprdsplit.0 | . . . 4
⊢  0 =
(0g‘𝐺) | 
| 146 | 19 | adantl 481 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑋 ∈ 𝐶) → ((𝑆 ↾ 𝐶)‘𝑋) = (𝑆‘𝑋)) | 
| 147 | 6 | adantr 480 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑋 ∈ 𝐶) → 𝐺dom DProd (𝑆 ↾ 𝐶)) | 
| 148 | 12 | adantr 480 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑋 ∈ 𝐶) → dom (𝑆 ↾ 𝐶) = 𝐶) | 
| 149 | 147, 148,
63 | dprdub 20046 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑋 ∈ 𝐶) → ((𝑆 ↾ 𝐶)‘𝑋) ⊆ (𝐺 DProd (𝑆 ↾ 𝐶))) | 
| 150 | 146, 149 | eqsstrrd 4018 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑋 ∈ 𝐶) → (𝑆‘𝑋) ⊆ (𝐺 DProd (𝑆 ↾ 𝐶))) | 
| 151 |  | dprdsubg 20045 | . . . . . . . . . . 11
⊢ (𝐺dom DProd (𝑆 ↾ 𝐶) → (𝐺 DProd (𝑆 ↾ 𝐶)) ∈ (SubGrp‘𝐺)) | 
| 152 | 6, 151 | syl 17 | . . . . . . . . . 10
⊢ (𝜑 → (𝐺 DProd (𝑆 ↾ 𝐶)) ∈ (SubGrp‘𝐺)) | 
| 153 | 152 | adantr 480 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑋 ∈ 𝐶) → (𝐺 DProd (𝑆 ↾ 𝐶)) ∈ (SubGrp‘𝐺)) | 
| 154 | 119 | lsmlub 19683 | . . . . . . . . 9
⊢ (((𝑆‘𝑋) ∈ (SubGrp‘𝐺) ∧ (𝐾‘∪ (𝑆 “ (𝐶 ∖ {𝑋}))) ∈ (SubGrp‘𝐺) ∧ (𝐺 DProd (𝑆 ↾ 𝐶)) ∈ (SubGrp‘𝐺)) → (((𝑆‘𝑋) ⊆ (𝐺 DProd (𝑆 ↾ 𝐶)) ∧ (𝐾‘∪ (𝑆 “ (𝐶 ∖ {𝑋}))) ⊆ (𝐺 DProd (𝑆 ↾ 𝐶))) ↔ ((𝑆‘𝑋)(LSSum‘𝐺)(𝐾‘∪ (𝑆 “ (𝐶 ∖ {𝑋})))) ⊆ (𝐺 DProd (𝑆 ↾ 𝐶)))) | 
| 155 | 144, 115,
153, 154 | syl3anc 1372 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑋 ∈ 𝐶) → (((𝑆‘𝑋) ⊆ (𝐺 DProd (𝑆 ↾ 𝐶)) ∧ (𝐾‘∪ (𝑆 “ (𝐶 ∖ {𝑋}))) ⊆ (𝐺 DProd (𝑆 ↾ 𝐶))) ↔ ((𝑆‘𝑋)(LSSum‘𝐺)(𝐾‘∪ (𝑆 “ (𝐶 ∖ {𝑋})))) ⊆ (𝐺 DProd (𝑆 ↾ 𝐶)))) | 
| 156 | 150, 133,
155 | mpbi2and 712 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑋 ∈ 𝐶) → ((𝑆‘𝑋)(LSSum‘𝐺)(𝐾‘∪ (𝑆 “ (𝐶 ∖ {𝑋})))) ⊆ (𝐺 DProd (𝑆 ↾ 𝐶))) | 
| 157 | 156 | ssrind 4243 | . . . . . 6
⊢ ((𝜑 ∧ 𝑋 ∈ 𝐶) → (((𝑆‘𝑋)(LSSum‘𝐺)(𝐾‘∪ (𝑆 “ (𝐶 ∖ {𝑋})))) ∩ (𝐺 DProd (𝑆 ↾ 𝐷))) ⊆ ((𝐺 DProd (𝑆 ↾ 𝐶)) ∩ (𝐺 DProd (𝑆 ↾ 𝐷)))) | 
| 158 |  | dmdprdsplit2.4 | . . . . . . 7
⊢ (𝜑 → ((𝐺 DProd (𝑆 ↾ 𝐶)) ∩ (𝐺 DProd (𝑆 ↾ 𝐷))) = { 0 }) | 
| 159 | 158 | adantr 480 | . . . . . 6
⊢ ((𝜑 ∧ 𝑋 ∈ 𝐶) → ((𝐺 DProd (𝑆 ↾ 𝐶)) ∩ (𝐺 DProd (𝑆 ↾ 𝐷))) = { 0 }) | 
| 160 | 157, 159 | sseqtrd 4019 | . . . . 5
⊢ ((𝜑 ∧ 𝑋 ∈ 𝐶) → (((𝑆‘𝑋)(LSSum‘𝐺)(𝐾‘∪ (𝑆 “ (𝐶 ∖ {𝑋})))) ∩ (𝐺 DProd (𝑆 ↾ 𝐷))) ⊆ { 0 }) | 
| 161 | 119 | lsmub1 19676 | . . . . . . . . 9
⊢ (((𝑆‘𝑋) ∈ (SubGrp‘𝐺) ∧ (𝐾‘∪ (𝑆 “ (𝐶 ∖ {𝑋}))) ∈ (SubGrp‘𝐺)) → (𝑆‘𝑋) ⊆ ((𝑆‘𝑋)(LSSum‘𝐺)(𝐾‘∪ (𝑆 “ (𝐶 ∖ {𝑋}))))) | 
| 162 | 144, 115,
161 | syl2anc 584 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑋 ∈ 𝐶) → (𝑆‘𝑋) ⊆ ((𝑆‘𝑋)(LSSum‘𝐺)(𝐾‘∪ (𝑆 “ (𝐶 ∖ {𝑋}))))) | 
| 163 | 145 | subg0cl 19153 | . . . . . . . . 9
⊢ ((𝑆‘𝑋) ∈ (SubGrp‘𝐺) → 0 ∈ (𝑆‘𝑋)) | 
| 164 | 144, 163 | syl 17 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑋 ∈ 𝐶) → 0 ∈ (𝑆‘𝑋)) | 
| 165 | 162, 164 | sseldd 3983 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑋 ∈ 𝐶) → 0 ∈ ((𝑆‘𝑋)(LSSum‘𝐺)(𝐾‘∪ (𝑆 “ (𝐶 ∖ {𝑋}))))) | 
| 166 | 145 | subg0cl 19153 | . . . . . . . 8
⊢ ((𝐺 DProd (𝑆 ↾ 𝐷)) ∈ (SubGrp‘𝐺) → 0 ∈ (𝐺 DProd (𝑆 ↾ 𝐷))) | 
| 167 | 118, 166 | syl 17 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑋 ∈ 𝐶) → 0 ∈ (𝐺 DProd (𝑆 ↾ 𝐷))) | 
| 168 | 165, 167 | elind 4199 | . . . . . 6
⊢ ((𝜑 ∧ 𝑋 ∈ 𝐶) → 0 ∈ (((𝑆‘𝑋)(LSSum‘𝐺)(𝐾‘∪ (𝑆 “ (𝐶 ∖ {𝑋})))) ∩ (𝐺 DProd (𝑆 ↾ 𝐷)))) | 
| 169 | 168 | snssd 4808 | . . . . 5
⊢ ((𝜑 ∧ 𝑋 ∈ 𝐶) → { 0 } ⊆ (((𝑆‘𝑋)(LSSum‘𝐺)(𝐾‘∪ (𝑆 “ (𝐶 ∖ {𝑋})))) ∩ (𝐺 DProd (𝑆 ↾ 𝐷)))) | 
| 170 | 160, 169 | eqssd 4000 | . . . 4
⊢ ((𝜑 ∧ 𝑋 ∈ 𝐶) → (((𝑆‘𝑋)(LSSum‘𝐺)(𝐾‘∪ (𝑆 “ (𝐶 ∖ {𝑋})))) ∩ (𝐺 DProd (𝑆 ↾ 𝐷))) = { 0 }) | 
| 171 |  | resima2 6033 | . . . . . . . . 9
⊢ ((𝐶 ∖ {𝑋}) ⊆ 𝐶 → ((𝑆 ↾ 𝐶) “ (𝐶 ∖ {𝑋})) = (𝑆 “ (𝐶 ∖ {𝑋}))) | 
| 172 | 84, 171 | mp1i 13 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑋 ∈ 𝐶) → ((𝑆 ↾ 𝐶) “ (𝐶 ∖ {𝑋})) = (𝑆 “ (𝐶 ∖ {𝑋}))) | 
| 173 | 172 | unieqd 4919 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑋 ∈ 𝐶) → ∪
((𝑆 ↾ 𝐶) “ (𝐶 ∖ {𝑋})) = ∪ (𝑆 “ (𝐶 ∖ {𝑋}))) | 
| 174 | 173 | fveq2d 6909 | . . . . . 6
⊢ ((𝜑 ∧ 𝑋 ∈ 𝐶) → (𝐾‘∪ ((𝑆 ↾ 𝐶) “ (𝐶 ∖ {𝑋}))) = (𝐾‘∪ (𝑆 “ (𝐶 ∖ {𝑋})))) | 
| 175 | 146, 174 | ineq12d 4220 | . . . . 5
⊢ ((𝜑 ∧ 𝑋 ∈ 𝐶) → (((𝑆 ↾ 𝐶)‘𝑋) ∩ (𝐾‘∪ ((𝑆 ↾ 𝐶) “ (𝐶 ∖ {𝑋})))) = ((𝑆‘𝑋) ∩ (𝐾‘∪ (𝑆 “ (𝐶 ∖ {𝑋}))))) | 
| 176 | 147, 148,
63, 145, 83 | dprddisj 20030 | . . . . 5
⊢ ((𝜑 ∧ 𝑋 ∈ 𝐶) → (((𝑆 ↾ 𝐶)‘𝑋) ∩ (𝐾‘∪ ((𝑆 ↾ 𝐶) “ (𝐶 ∖ {𝑋})))) = { 0 }) | 
| 177 | 175, 176 | eqtr3d 2778 | . . . 4
⊢ ((𝜑 ∧ 𝑋 ∈ 𝐶) → ((𝑆‘𝑋) ∩ (𝐾‘∪ (𝑆 “ (𝐶 ∖ {𝑋})))) = { 0 }) | 
| 178 | 8 | adantr 480 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑋 ∈ 𝐶) → 𝑆:𝐼⟶(SubGrp‘𝐺)) | 
| 179 |  | ffun 6738 | . . . . . . . 8
⊢ (𝑆:𝐼⟶(SubGrp‘𝐺) → Fun 𝑆) | 
| 180 |  | funiunfv 7269 | . . . . . . . 8
⊢ (Fun
𝑆 → ∪ 𝑦 ∈ (𝐶 ∖ {𝑋})(𝑆‘𝑦) = ∪ (𝑆 “ (𝐶 ∖ {𝑋}))) | 
| 181 | 178, 179,
180 | 3syl 18 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑋 ∈ 𝐶) → ∪
𝑦 ∈ (𝐶 ∖ {𝑋})(𝑆‘𝑦) = ∪ (𝑆 “ (𝐶 ∖ {𝑋}))) | 
| 182 | 6 | ad2antrr 726 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑋 ∈ 𝐶) ∧ 𝑦 ∈ (𝐶 ∖ {𝑋})) → 𝐺dom DProd (𝑆 ↾ 𝐶)) | 
| 183 | 12 | ad2antrr 726 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑋 ∈ 𝐶) ∧ 𝑦 ∈ (𝐶 ∖ {𝑋})) → dom (𝑆 ↾ 𝐶) = 𝐶) | 
| 184 |  | eldifi 4130 | . . . . . . . . . . . 12
⊢ (𝑦 ∈ (𝐶 ∖ {𝑋}) → 𝑦 ∈ 𝐶) | 
| 185 | 184 | adantl 481 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑋 ∈ 𝐶) ∧ 𝑦 ∈ (𝐶 ∖ {𝑋})) → 𝑦 ∈ 𝐶) | 
| 186 |  | simplr 768 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑋 ∈ 𝐶) ∧ 𝑦 ∈ (𝐶 ∖ {𝑋})) → 𝑋 ∈ 𝐶) | 
| 187 |  | eldifsni 4789 | . . . . . . . . . . . 12
⊢ (𝑦 ∈ (𝐶 ∖ {𝑋}) → 𝑦 ≠ 𝑋) | 
| 188 | 187 | adantl 481 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑋 ∈ 𝐶) ∧ 𝑦 ∈ (𝐶 ∖ {𝑋})) → 𝑦 ≠ 𝑋) | 
| 189 | 182, 183,
185, 186, 188, 17 | dprdcntz 20029 | . . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑋 ∈ 𝐶) ∧ 𝑦 ∈ (𝐶 ∖ {𝑋})) → ((𝑆 ↾ 𝐶)‘𝑦) ⊆ (𝑍‘((𝑆 ↾ 𝐶)‘𝑋))) | 
| 190 | 185 | fvresd 6925 | . . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑋 ∈ 𝐶) ∧ 𝑦 ∈ (𝐶 ∖ {𝑋})) → ((𝑆 ↾ 𝐶)‘𝑦) = (𝑆‘𝑦)) | 
| 191 | 19 | ad2antlr 727 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑋 ∈ 𝐶) ∧ 𝑦 ∈ (𝐶 ∖ {𝑋})) → ((𝑆 ↾ 𝐶)‘𝑋) = (𝑆‘𝑋)) | 
| 192 | 191 | fveq2d 6909 | . . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑋 ∈ 𝐶) ∧ 𝑦 ∈ (𝐶 ∖ {𝑋})) → (𝑍‘((𝑆 ↾ 𝐶)‘𝑋)) = (𝑍‘(𝑆‘𝑋))) | 
| 193 | 189, 190,
192 | 3sstr3d 4037 | . . . . . . . . 9
⊢ (((𝜑 ∧ 𝑋 ∈ 𝐶) ∧ 𝑦 ∈ (𝐶 ∖ {𝑋})) → (𝑆‘𝑦) ⊆ (𝑍‘(𝑆‘𝑋))) | 
| 194 | 193 | ralrimiva 3145 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑋 ∈ 𝐶) → ∀𝑦 ∈ (𝐶 ∖ {𝑋})(𝑆‘𝑦) ⊆ (𝑍‘(𝑆‘𝑋))) | 
| 195 |  | iunss 5044 | . . . . . . . 8
⊢ (∪ 𝑦 ∈ (𝐶 ∖ {𝑋})(𝑆‘𝑦) ⊆ (𝑍‘(𝑆‘𝑋)) ↔ ∀𝑦 ∈ (𝐶 ∖ {𝑋})(𝑆‘𝑦) ⊆ (𝑍‘(𝑆‘𝑋))) | 
| 196 | 194, 195 | sylibr 234 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑋 ∈ 𝐶) → ∪
𝑦 ∈ (𝐶 ∖ {𝑋})(𝑆‘𝑦) ⊆ (𝑍‘(𝑆‘𝑋))) | 
| 197 | 181, 196 | eqsstrrd 4018 | . . . . . 6
⊢ ((𝜑 ∧ 𝑋 ∈ 𝐶) → ∪ (𝑆 “ (𝐶 ∖ {𝑋})) ⊆ (𝑍‘(𝑆‘𝑋))) | 
| 198 | 34 | subgss 19146 | . . . . . . . 8
⊢ ((𝑆‘𝑋) ∈ (SubGrp‘𝐺) → (𝑆‘𝑋) ⊆ (Base‘𝐺)) | 
| 199 | 144, 198 | syl 17 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑋 ∈ 𝐶) → (𝑆‘𝑋) ⊆ (Base‘𝐺)) | 
| 200 | 34, 17 | cntzsubg 19358 | . . . . . . 7
⊢ ((𝐺 ∈ Grp ∧ (𝑆‘𝑋) ⊆ (Base‘𝐺)) → (𝑍‘(𝑆‘𝑋)) ∈ (SubGrp‘𝐺)) | 
| 201 | 57, 199, 200 | syl2anc 584 | . . . . . 6
⊢ ((𝜑 ∧ 𝑋 ∈ 𝐶) → (𝑍‘(𝑆‘𝑋)) ∈ (SubGrp‘𝐺)) | 
| 202 | 83 | mrcsscl 17664 | . . . . . 6
⊢
(((SubGrp‘𝐺)
∈ (Moore‘(Base‘𝐺)) ∧ ∪ (𝑆 “ (𝐶 ∖ {𝑋})) ⊆ (𝑍‘(𝑆‘𝑋)) ∧ (𝑍‘(𝑆‘𝑋)) ∈ (SubGrp‘𝐺)) → (𝐾‘∪ (𝑆 “ (𝐶 ∖ {𝑋}))) ⊆ (𝑍‘(𝑆‘𝑋))) | 
| 203 | 60, 197, 201, 202 | syl3anc 1372 | . . . . 5
⊢ ((𝜑 ∧ 𝑋 ∈ 𝐶) → (𝐾‘∪ (𝑆 “ (𝐶 ∖ {𝑋}))) ⊆ (𝑍‘(𝑆‘𝑋))) | 
| 204 | 17, 115, 144, 203 | cntzrecd 19697 | . . . 4
⊢ ((𝜑 ∧ 𝑋 ∈ 𝐶) → (𝑆‘𝑋) ⊆ (𝑍‘(𝐾‘∪ (𝑆 “ (𝐶 ∖ {𝑋}))))) | 
| 205 | 119, 144,
115, 118, 145, 170, 177, 17, 204 | lsmdisj3 19702 | . . 3
⊢ ((𝜑 ∧ 𝑋 ∈ 𝐶) → ((𝑆‘𝑋) ∩ ((𝐾‘∪ (𝑆 “ (𝐶 ∖ {𝑋})))(LSSum‘𝐺)(𝐺 DProd (𝑆 ↾ 𝐷)))) = { 0 }) | 
| 206 | 141, 205 | sseqtrd 4019 | . 2
⊢ ((𝜑 ∧ 𝑋 ∈ 𝐶) → ((𝑆‘𝑋) ∩ (𝐾‘∪ (𝑆 “ (𝐼 ∖ {𝑋})))) ⊆ { 0 }) | 
| 207 | 54, 206 | jca 511 | 1
⊢ ((𝜑 ∧ 𝑋 ∈ 𝐶) → ((𝑌 ∈ 𝐼 → (𝑋 ≠ 𝑌 → (𝑆‘𝑋) ⊆ (𝑍‘(𝑆‘𝑌)))) ∧ ((𝑆‘𝑋) ∩ (𝐾‘∪ (𝑆 “ (𝐼 ∖ {𝑋})))) ⊆ { 0 })) |