| Step | Hyp | Ref
| Expression |
| 1 | | gsumzsplit.b |
. . 3
⊢ 𝐵 = (Base‘𝐺) |
| 2 | | gsumzsplit.0 |
. . 3
⊢ 0 =
(0g‘𝐺) |
| 3 | | gsumzsplit.p |
. . 3
⊢ + =
(+g‘𝐺) |
| 4 | | gsumzsplit.z |
. . 3
⊢ 𝑍 = (Cntz‘𝐺) |
| 5 | | gsumzsplit.g |
. . 3
⊢ (𝜑 → 𝐺 ∈ Mnd) |
| 6 | | gsumzsplit.a |
. . 3
⊢ (𝜑 → 𝐴 ∈ 𝑉) |
| 7 | | gsumzsplit.f |
. . . 4
⊢ (𝜑 → 𝐹:𝐴⟶𝐵) |
| 8 | 2 | fvexi 6920 |
. . . . 5
⊢ 0 ∈
V |
| 9 | 8 | a1i 11 |
. . . 4
⊢ (𝜑 → 0 ∈ V) |
| 10 | | gsumzsplit.w |
. . . 4
⊢ (𝜑 → 𝐹 finSupp 0 ) |
| 11 | 7, 6, 9, 10 | fsuppmptif 9439 |
. . 3
⊢ (𝜑 → (𝑘 ∈ 𝐴 ↦ if(𝑘 ∈ 𝐶, (𝐹‘𝑘), 0 )) finSupp 0
) |
| 12 | 7, 6, 9, 10 | fsuppmptif 9439 |
. . 3
⊢ (𝜑 → (𝑘 ∈ 𝐴 ↦ if(𝑘 ∈ 𝐷, (𝐹‘𝑘), 0 )) finSupp 0
) |
| 13 | 1 | submacs 18840 |
. . . . 5
⊢ (𝐺 ∈ Mnd →
(SubMnd‘𝐺) ∈
(ACS‘𝐵)) |
| 14 | | acsmre 17695 |
. . . . 5
⊢
((SubMnd‘𝐺)
∈ (ACS‘𝐵) →
(SubMnd‘𝐺) ∈
(Moore‘𝐵)) |
| 15 | 5, 13, 14 | 3syl 18 |
. . . 4
⊢ (𝜑 → (SubMnd‘𝐺) ∈ (Moore‘𝐵)) |
| 16 | 7 | frnd 6744 |
. . . 4
⊢ (𝜑 → ran 𝐹 ⊆ 𝐵) |
| 17 | | eqid 2737 |
. . . . 5
⊢
(mrCls‘(SubMnd‘𝐺)) = (mrCls‘(SubMnd‘𝐺)) |
| 18 | 17 | mrccl 17654 |
. . . 4
⊢
(((SubMnd‘𝐺)
∈ (Moore‘𝐵)
∧ ran 𝐹 ⊆ 𝐵) →
((mrCls‘(SubMnd‘𝐺))‘ran 𝐹) ∈ (SubMnd‘𝐺)) |
| 19 | 15, 16, 18 | syl2anc 584 |
. . 3
⊢ (𝜑 →
((mrCls‘(SubMnd‘𝐺))‘ran 𝐹) ∈ (SubMnd‘𝐺)) |
| 20 | | gsumzsplit.c |
. . . . 5
⊢ (𝜑 → ran 𝐹 ⊆ (𝑍‘ran 𝐹)) |
| 21 | | eqid 2737 |
. . . . . 6
⊢ (𝐺 ↾s
((mrCls‘(SubMnd‘𝐺))‘ran 𝐹)) = (𝐺 ↾s
((mrCls‘(SubMnd‘𝐺))‘ran 𝐹)) |
| 22 | 4, 17, 21 | cntzspan 19862 |
. . . . 5
⊢ ((𝐺 ∈ Mnd ∧ ran 𝐹 ⊆ (𝑍‘ran 𝐹)) → (𝐺 ↾s
((mrCls‘(SubMnd‘𝐺))‘ran 𝐹)) ∈ CMnd) |
| 23 | 5, 20, 22 | syl2anc 584 |
. . . 4
⊢ (𝜑 → (𝐺 ↾s
((mrCls‘(SubMnd‘𝐺))‘ran 𝐹)) ∈ CMnd) |
| 24 | 21, 4 | submcmn2 19857 |
. . . . 5
⊢
(((mrCls‘(SubMnd‘𝐺))‘ran 𝐹) ∈ (SubMnd‘𝐺) → ((𝐺 ↾s
((mrCls‘(SubMnd‘𝐺))‘ran 𝐹)) ∈ CMnd ↔
((mrCls‘(SubMnd‘𝐺))‘ran 𝐹) ⊆ (𝑍‘((mrCls‘(SubMnd‘𝐺))‘ran 𝐹)))) |
| 25 | 19, 24 | syl 17 |
. . . 4
⊢ (𝜑 → ((𝐺 ↾s
((mrCls‘(SubMnd‘𝐺))‘ran 𝐹)) ∈ CMnd ↔
((mrCls‘(SubMnd‘𝐺))‘ran 𝐹) ⊆ (𝑍‘((mrCls‘(SubMnd‘𝐺))‘ran 𝐹)))) |
| 26 | 23, 25 | mpbid 232 |
. . 3
⊢ (𝜑 →
((mrCls‘(SubMnd‘𝐺))‘ran 𝐹) ⊆ (𝑍‘((mrCls‘(SubMnd‘𝐺))‘ran 𝐹))) |
| 27 | 15, 17, 16 | mrcssidd 17668 |
. . . . . . 7
⊢ (𝜑 → ran 𝐹 ⊆ ((mrCls‘(SubMnd‘𝐺))‘ran 𝐹)) |
| 28 | 27 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → ran 𝐹 ⊆ ((mrCls‘(SubMnd‘𝐺))‘ran 𝐹)) |
| 29 | 7 | ffnd 6737 |
. . . . . . 7
⊢ (𝜑 → 𝐹 Fn 𝐴) |
| 30 | | fnfvelrn 7100 |
. . . . . . 7
⊢ ((𝐹 Fn 𝐴 ∧ 𝑘 ∈ 𝐴) → (𝐹‘𝑘) ∈ ran 𝐹) |
| 31 | 29, 30 | sylan 580 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → (𝐹‘𝑘) ∈ ran 𝐹) |
| 32 | 28, 31 | sseldd 3984 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → (𝐹‘𝑘) ∈ ((mrCls‘(SubMnd‘𝐺))‘ran 𝐹)) |
| 33 | 2 | subm0cl 18824 |
. . . . . . 7
⊢
(((mrCls‘(SubMnd‘𝐺))‘ran 𝐹) ∈ (SubMnd‘𝐺) → 0 ∈
((mrCls‘(SubMnd‘𝐺))‘ran 𝐹)) |
| 34 | 19, 33 | syl 17 |
. . . . . 6
⊢ (𝜑 → 0 ∈
((mrCls‘(SubMnd‘𝐺))‘ran 𝐹)) |
| 35 | 34 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 0 ∈
((mrCls‘(SubMnd‘𝐺))‘ran 𝐹)) |
| 36 | 32, 35 | ifcld 4572 |
. . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → if(𝑘 ∈ 𝐶, (𝐹‘𝑘), 0 ) ∈
((mrCls‘(SubMnd‘𝐺))‘ran 𝐹)) |
| 37 | 36 | fmpttd 7135 |
. . 3
⊢ (𝜑 → (𝑘 ∈ 𝐴 ↦ if(𝑘 ∈ 𝐶, (𝐹‘𝑘), 0 )):𝐴⟶((mrCls‘(SubMnd‘𝐺))‘ran 𝐹)) |
| 38 | 32, 35 | ifcld 4572 |
. . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → if(𝑘 ∈ 𝐷, (𝐹‘𝑘), 0 ) ∈
((mrCls‘(SubMnd‘𝐺))‘ran 𝐹)) |
| 39 | 38 | fmpttd 7135 |
. . 3
⊢ (𝜑 → (𝑘 ∈ 𝐴 ↦ if(𝑘 ∈ 𝐷, (𝐹‘𝑘), 0 )):𝐴⟶((mrCls‘(SubMnd‘𝐺))‘ran 𝐹)) |
| 40 | 1, 2, 3, 4, 5, 6, 11, 12, 19, 26, 37, 39 | gsumzadd 19940 |
. 2
⊢ (𝜑 → (𝐺 Σg ((𝑘 ∈ 𝐴 ↦ if(𝑘 ∈ 𝐶, (𝐹‘𝑘), 0 )) ∘f
+ (𝑘 ∈ 𝐴 ↦ if(𝑘 ∈ 𝐷, (𝐹‘𝑘), 0 )))) = ((𝐺 Σg (𝑘 ∈ 𝐴 ↦ if(𝑘 ∈ 𝐶, (𝐹‘𝑘), 0 ))) + (𝐺 Σg (𝑘 ∈ 𝐴 ↦ if(𝑘 ∈ 𝐷, (𝐹‘𝑘), 0 ))))) |
| 41 | 7 | feqmptd 6977 |
. . . . 5
⊢ (𝜑 → 𝐹 = (𝑘 ∈ 𝐴 ↦ (𝐹‘𝑘))) |
| 42 | | iftrue 4531 |
. . . . . . . . . 10
⊢ (𝑘 ∈ 𝐶 → if(𝑘 ∈ 𝐶, (𝐹‘𝑘), 0 ) = (𝐹‘𝑘)) |
| 43 | 42 | adantl 481 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑘 ∈ 𝐴) ∧ 𝑘 ∈ 𝐶) → if(𝑘 ∈ 𝐶, (𝐹‘𝑘), 0 ) = (𝐹‘𝑘)) |
| 44 | | gsumzsplit.i |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝐶 ∩ 𝐷) = ∅) |
| 45 | | noel 4338 |
. . . . . . . . . . . . . . . 16
⊢ ¬
𝑘 ∈
∅ |
| 46 | | eleq2 2830 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐶 ∩ 𝐷) = ∅ → (𝑘 ∈ (𝐶 ∩ 𝐷) ↔ 𝑘 ∈ ∅)) |
| 47 | 45, 46 | mtbiri 327 |
. . . . . . . . . . . . . . 15
⊢ ((𝐶 ∩ 𝐷) = ∅ → ¬ 𝑘 ∈ (𝐶 ∩ 𝐷)) |
| 48 | 44, 47 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ¬ 𝑘 ∈ (𝐶 ∩ 𝐷)) |
| 49 | 48 | adantr 480 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → ¬ 𝑘 ∈ (𝐶 ∩ 𝐷)) |
| 50 | | elin 3967 |
. . . . . . . . . . . . 13
⊢ (𝑘 ∈ (𝐶 ∩ 𝐷) ↔ (𝑘 ∈ 𝐶 ∧ 𝑘 ∈ 𝐷)) |
| 51 | 49, 50 | sylnib 328 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → ¬ (𝑘 ∈ 𝐶 ∧ 𝑘 ∈ 𝐷)) |
| 52 | | imnan 399 |
. . . . . . . . . . . 12
⊢ ((𝑘 ∈ 𝐶 → ¬ 𝑘 ∈ 𝐷) ↔ ¬ (𝑘 ∈ 𝐶 ∧ 𝑘 ∈ 𝐷)) |
| 53 | 51, 52 | sylibr 234 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → (𝑘 ∈ 𝐶 → ¬ 𝑘 ∈ 𝐷)) |
| 54 | 53 | imp 406 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑘 ∈ 𝐴) ∧ 𝑘 ∈ 𝐶) → ¬ 𝑘 ∈ 𝐷) |
| 55 | 54 | iffalsed 4536 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑘 ∈ 𝐴) ∧ 𝑘 ∈ 𝐶) → if(𝑘 ∈ 𝐷, (𝐹‘𝑘), 0 ) = 0 ) |
| 56 | 43, 55 | oveq12d 7449 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑘 ∈ 𝐴) ∧ 𝑘 ∈ 𝐶) → (if(𝑘 ∈ 𝐶, (𝐹‘𝑘), 0 ) + if(𝑘 ∈ 𝐷, (𝐹‘𝑘), 0 )) = ((𝐹‘𝑘) + 0 )) |
| 57 | 7 | ffvelcdmda 7104 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → (𝐹‘𝑘) ∈ 𝐵) |
| 58 | 1, 3, 2 | mndrid 18768 |
. . . . . . . . . 10
⊢ ((𝐺 ∈ Mnd ∧ (𝐹‘𝑘) ∈ 𝐵) → ((𝐹‘𝑘) + 0 ) = (𝐹‘𝑘)) |
| 59 | 5, 57, 58 | syl2an2r 685 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → ((𝐹‘𝑘) + 0 ) = (𝐹‘𝑘)) |
| 60 | 59 | adantr 480 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑘 ∈ 𝐴) ∧ 𝑘 ∈ 𝐶) → ((𝐹‘𝑘) + 0 ) = (𝐹‘𝑘)) |
| 61 | 56, 60 | eqtrd 2777 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑘 ∈ 𝐴) ∧ 𝑘 ∈ 𝐶) → (if(𝑘 ∈ 𝐶, (𝐹‘𝑘), 0 ) + if(𝑘 ∈ 𝐷, (𝐹‘𝑘), 0 )) = (𝐹‘𝑘)) |
| 62 | 53 | con2d 134 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → (𝑘 ∈ 𝐷 → ¬ 𝑘 ∈ 𝐶)) |
| 63 | 62 | imp 406 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑘 ∈ 𝐴) ∧ 𝑘 ∈ 𝐷) → ¬ 𝑘 ∈ 𝐶) |
| 64 | 63 | iffalsed 4536 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑘 ∈ 𝐴) ∧ 𝑘 ∈ 𝐷) → if(𝑘 ∈ 𝐶, (𝐹‘𝑘), 0 ) = 0 ) |
| 65 | | iftrue 4531 |
. . . . . . . . . 10
⊢ (𝑘 ∈ 𝐷 → if(𝑘 ∈ 𝐷, (𝐹‘𝑘), 0 ) = (𝐹‘𝑘)) |
| 66 | 65 | adantl 481 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑘 ∈ 𝐴) ∧ 𝑘 ∈ 𝐷) → if(𝑘 ∈ 𝐷, (𝐹‘𝑘), 0 ) = (𝐹‘𝑘)) |
| 67 | 64, 66 | oveq12d 7449 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑘 ∈ 𝐴) ∧ 𝑘 ∈ 𝐷) → (if(𝑘 ∈ 𝐶, (𝐹‘𝑘), 0 ) + if(𝑘 ∈ 𝐷, (𝐹‘𝑘), 0 )) = ( 0 + (𝐹‘𝑘))) |
| 68 | 1, 3, 2 | mndlid 18767 |
. . . . . . . . . 10
⊢ ((𝐺 ∈ Mnd ∧ (𝐹‘𝑘) ∈ 𝐵) → ( 0 + (𝐹‘𝑘)) = (𝐹‘𝑘)) |
| 69 | 5, 57, 68 | syl2an2r 685 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → ( 0 + (𝐹‘𝑘)) = (𝐹‘𝑘)) |
| 70 | 69 | adantr 480 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑘 ∈ 𝐴) ∧ 𝑘 ∈ 𝐷) → ( 0 + (𝐹‘𝑘)) = (𝐹‘𝑘)) |
| 71 | 67, 70 | eqtrd 2777 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑘 ∈ 𝐴) ∧ 𝑘 ∈ 𝐷) → (if(𝑘 ∈ 𝐶, (𝐹‘𝑘), 0 ) + if(𝑘 ∈ 𝐷, (𝐹‘𝑘), 0 )) = (𝐹‘𝑘)) |
| 72 | | gsumzsplit.u |
. . . . . . . . . 10
⊢ (𝜑 → 𝐴 = (𝐶 ∪ 𝐷)) |
| 73 | 72 | eleq2d 2827 |
. . . . . . . . 9
⊢ (𝜑 → (𝑘 ∈ 𝐴 ↔ 𝑘 ∈ (𝐶 ∪ 𝐷))) |
| 74 | | elun 4153 |
. . . . . . . . 9
⊢ (𝑘 ∈ (𝐶 ∪ 𝐷) ↔ (𝑘 ∈ 𝐶 ∨ 𝑘 ∈ 𝐷)) |
| 75 | 73, 74 | bitrdi 287 |
. . . . . . . 8
⊢ (𝜑 → (𝑘 ∈ 𝐴 ↔ (𝑘 ∈ 𝐶 ∨ 𝑘 ∈ 𝐷))) |
| 76 | 75 | biimpa 476 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → (𝑘 ∈ 𝐶 ∨ 𝑘 ∈ 𝐷)) |
| 77 | 61, 71, 76 | mpjaodan 961 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → (if(𝑘 ∈ 𝐶, (𝐹‘𝑘), 0 ) + if(𝑘 ∈ 𝐷, (𝐹‘𝑘), 0 )) = (𝐹‘𝑘)) |
| 78 | 77 | mpteq2dva 5242 |
. . . . 5
⊢ (𝜑 → (𝑘 ∈ 𝐴 ↦ (if(𝑘 ∈ 𝐶, (𝐹‘𝑘), 0 ) + if(𝑘 ∈ 𝐷, (𝐹‘𝑘), 0 ))) = (𝑘 ∈ 𝐴 ↦ (𝐹‘𝑘))) |
| 79 | 41, 78 | eqtr4d 2780 |
. . . 4
⊢ (𝜑 → 𝐹 = (𝑘 ∈ 𝐴 ↦ (if(𝑘 ∈ 𝐶, (𝐹‘𝑘), 0 ) + if(𝑘 ∈ 𝐷, (𝐹‘𝑘), 0 )))) |
| 80 | 1, 2 | mndidcl 18762 |
. . . . . . . 8
⊢ (𝐺 ∈ Mnd → 0 ∈ 𝐵) |
| 81 | 5, 80 | syl 17 |
. . . . . . 7
⊢ (𝜑 → 0 ∈ 𝐵) |
| 82 | 81 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 0 ∈ 𝐵) |
| 83 | 57, 82 | ifcld 4572 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → if(𝑘 ∈ 𝐶, (𝐹‘𝑘), 0 ) ∈ 𝐵) |
| 84 | 57, 82 | ifcld 4572 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → if(𝑘 ∈ 𝐷, (𝐹‘𝑘), 0 ) ∈ 𝐵) |
| 85 | | eqidd 2738 |
. . . . 5
⊢ (𝜑 → (𝑘 ∈ 𝐴 ↦ if(𝑘 ∈ 𝐶, (𝐹‘𝑘), 0 )) = (𝑘 ∈ 𝐴 ↦ if(𝑘 ∈ 𝐶, (𝐹‘𝑘), 0 ))) |
| 86 | | eqidd 2738 |
. . . . 5
⊢ (𝜑 → (𝑘 ∈ 𝐴 ↦ if(𝑘 ∈ 𝐷, (𝐹‘𝑘), 0 )) = (𝑘 ∈ 𝐴 ↦ if(𝑘 ∈ 𝐷, (𝐹‘𝑘), 0 ))) |
| 87 | 6, 83, 84, 85, 86 | offval2 7717 |
. . . 4
⊢ (𝜑 → ((𝑘 ∈ 𝐴 ↦ if(𝑘 ∈ 𝐶, (𝐹‘𝑘), 0 )) ∘f
+ (𝑘 ∈ 𝐴 ↦ if(𝑘 ∈ 𝐷, (𝐹‘𝑘), 0 ))) = (𝑘 ∈ 𝐴 ↦ (if(𝑘 ∈ 𝐶, (𝐹‘𝑘), 0 ) + if(𝑘 ∈ 𝐷, (𝐹‘𝑘), 0 )))) |
| 88 | 79, 87 | eqtr4d 2780 |
. . 3
⊢ (𝜑 → 𝐹 = ((𝑘 ∈ 𝐴 ↦ if(𝑘 ∈ 𝐶, (𝐹‘𝑘), 0 )) ∘f
+ (𝑘 ∈ 𝐴 ↦ if(𝑘 ∈ 𝐷, (𝐹‘𝑘), 0 )))) |
| 89 | 88 | oveq2d 7447 |
. 2
⊢ (𝜑 → (𝐺 Σg 𝐹) = (𝐺 Σg ((𝑘 ∈ 𝐴 ↦ if(𝑘 ∈ 𝐶, (𝐹‘𝑘), 0 )) ∘f
+ (𝑘 ∈ 𝐴 ↦ if(𝑘 ∈ 𝐷, (𝐹‘𝑘), 0 ))))) |
| 90 | 41 | reseq1d 5996 |
. . . . . 6
⊢ (𝜑 → (𝐹 ↾ 𝐶) = ((𝑘 ∈ 𝐴 ↦ (𝐹‘𝑘)) ↾ 𝐶)) |
| 91 | | ssun1 4178 |
. . . . . . . 8
⊢ 𝐶 ⊆ (𝐶 ∪ 𝐷) |
| 92 | 91, 72 | sseqtrrid 4027 |
. . . . . . 7
⊢ (𝜑 → 𝐶 ⊆ 𝐴) |
| 93 | 42 | mpteq2ia 5245 |
. . . . . . . 8
⊢ (𝑘 ∈ 𝐶 ↦ if(𝑘 ∈ 𝐶, (𝐹‘𝑘), 0 )) = (𝑘 ∈ 𝐶 ↦ (𝐹‘𝑘)) |
| 94 | | resmpt 6055 |
. . . . . . . 8
⊢ (𝐶 ⊆ 𝐴 → ((𝑘 ∈ 𝐴 ↦ if(𝑘 ∈ 𝐶, (𝐹‘𝑘), 0 )) ↾ 𝐶) = (𝑘 ∈ 𝐶 ↦ if(𝑘 ∈ 𝐶, (𝐹‘𝑘), 0 ))) |
| 95 | | resmpt 6055 |
. . . . . . . 8
⊢ (𝐶 ⊆ 𝐴 → ((𝑘 ∈ 𝐴 ↦ (𝐹‘𝑘)) ↾ 𝐶) = (𝑘 ∈ 𝐶 ↦ (𝐹‘𝑘))) |
| 96 | 93, 94, 95 | 3eqtr4a 2803 |
. . . . . . 7
⊢ (𝐶 ⊆ 𝐴 → ((𝑘 ∈ 𝐴 ↦ if(𝑘 ∈ 𝐶, (𝐹‘𝑘), 0 )) ↾ 𝐶) = ((𝑘 ∈ 𝐴 ↦ (𝐹‘𝑘)) ↾ 𝐶)) |
| 97 | 92, 96 | syl 17 |
. . . . . 6
⊢ (𝜑 → ((𝑘 ∈ 𝐴 ↦ if(𝑘 ∈ 𝐶, (𝐹‘𝑘), 0 )) ↾ 𝐶) = ((𝑘 ∈ 𝐴 ↦ (𝐹‘𝑘)) ↾ 𝐶)) |
| 98 | 90, 97 | eqtr4d 2780 |
. . . . 5
⊢ (𝜑 → (𝐹 ↾ 𝐶) = ((𝑘 ∈ 𝐴 ↦ if(𝑘 ∈ 𝐶, (𝐹‘𝑘), 0 )) ↾ 𝐶)) |
| 99 | 98 | oveq2d 7447 |
. . . 4
⊢ (𝜑 → (𝐺 Σg (𝐹 ↾ 𝐶)) = (𝐺 Σg ((𝑘 ∈ 𝐴 ↦ if(𝑘 ∈ 𝐶, (𝐹‘𝑘), 0 )) ↾ 𝐶))) |
| 100 | 83 | fmpttd 7135 |
. . . . 5
⊢ (𝜑 → (𝑘 ∈ 𝐴 ↦ if(𝑘 ∈ 𝐶, (𝐹‘𝑘), 0 )):𝐴⟶𝐵) |
| 101 | 37 | frnd 6744 |
. . . . . 6
⊢ (𝜑 → ran (𝑘 ∈ 𝐴 ↦ if(𝑘 ∈ 𝐶, (𝐹‘𝑘), 0 )) ⊆
((mrCls‘(SubMnd‘𝐺))‘ran 𝐹)) |
| 102 | 4 | cntzidss 19358 |
. . . . . 6
⊢
((((mrCls‘(SubMnd‘𝐺))‘ran 𝐹) ⊆ (𝑍‘((mrCls‘(SubMnd‘𝐺))‘ran 𝐹)) ∧ ran (𝑘 ∈ 𝐴 ↦ if(𝑘 ∈ 𝐶, (𝐹‘𝑘), 0 )) ⊆
((mrCls‘(SubMnd‘𝐺))‘ran 𝐹)) → ran (𝑘 ∈ 𝐴 ↦ if(𝑘 ∈ 𝐶, (𝐹‘𝑘), 0 )) ⊆ (𝑍‘ran (𝑘 ∈ 𝐴 ↦ if(𝑘 ∈ 𝐶, (𝐹‘𝑘), 0 )))) |
| 103 | 26, 101, 102 | syl2anc 584 |
. . . . 5
⊢ (𝜑 → ran (𝑘 ∈ 𝐴 ↦ if(𝑘 ∈ 𝐶, (𝐹‘𝑘), 0 )) ⊆ (𝑍‘ran (𝑘 ∈ 𝐴 ↦ if(𝑘 ∈ 𝐶, (𝐹‘𝑘), 0 )))) |
| 104 | | eldifn 4132 |
. . . . . . . 8
⊢ (𝑘 ∈ (𝐴 ∖ 𝐶) → ¬ 𝑘 ∈ 𝐶) |
| 105 | 104 | adantl 481 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ (𝐴 ∖ 𝐶)) → ¬ 𝑘 ∈ 𝐶) |
| 106 | 105 | iffalsed 4536 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ (𝐴 ∖ 𝐶)) → if(𝑘 ∈ 𝐶, (𝐹‘𝑘), 0 ) = 0 ) |
| 107 | 106, 6 | suppss2 8225 |
. . . . 5
⊢ (𝜑 → ((𝑘 ∈ 𝐴 ↦ if(𝑘 ∈ 𝐶, (𝐹‘𝑘), 0 )) supp 0 ) ⊆ 𝐶) |
| 108 | 1, 2, 4, 5, 6, 100, 103, 107, 11 | gsumzres 19927 |
. . . 4
⊢ (𝜑 → (𝐺 Σg ((𝑘 ∈ 𝐴 ↦ if(𝑘 ∈ 𝐶, (𝐹‘𝑘), 0 )) ↾ 𝐶)) = (𝐺 Σg (𝑘 ∈ 𝐴 ↦ if(𝑘 ∈ 𝐶, (𝐹‘𝑘), 0 )))) |
| 109 | 99, 108 | eqtrd 2777 |
. . 3
⊢ (𝜑 → (𝐺 Σg (𝐹 ↾ 𝐶)) = (𝐺 Σg (𝑘 ∈ 𝐴 ↦ if(𝑘 ∈ 𝐶, (𝐹‘𝑘), 0 )))) |
| 110 | 41 | reseq1d 5996 |
. . . . . 6
⊢ (𝜑 → (𝐹 ↾ 𝐷) = ((𝑘 ∈ 𝐴 ↦ (𝐹‘𝑘)) ↾ 𝐷)) |
| 111 | | ssun2 4179 |
. . . . . . . 8
⊢ 𝐷 ⊆ (𝐶 ∪ 𝐷) |
| 112 | 111, 72 | sseqtrrid 4027 |
. . . . . . 7
⊢ (𝜑 → 𝐷 ⊆ 𝐴) |
| 113 | 65 | mpteq2ia 5245 |
. . . . . . . 8
⊢ (𝑘 ∈ 𝐷 ↦ if(𝑘 ∈ 𝐷, (𝐹‘𝑘), 0 )) = (𝑘 ∈ 𝐷 ↦ (𝐹‘𝑘)) |
| 114 | | resmpt 6055 |
. . . . . . . 8
⊢ (𝐷 ⊆ 𝐴 → ((𝑘 ∈ 𝐴 ↦ if(𝑘 ∈ 𝐷, (𝐹‘𝑘), 0 )) ↾ 𝐷) = (𝑘 ∈ 𝐷 ↦ if(𝑘 ∈ 𝐷, (𝐹‘𝑘), 0 ))) |
| 115 | | resmpt 6055 |
. . . . . . . 8
⊢ (𝐷 ⊆ 𝐴 → ((𝑘 ∈ 𝐴 ↦ (𝐹‘𝑘)) ↾ 𝐷) = (𝑘 ∈ 𝐷 ↦ (𝐹‘𝑘))) |
| 116 | 113, 114,
115 | 3eqtr4a 2803 |
. . . . . . 7
⊢ (𝐷 ⊆ 𝐴 → ((𝑘 ∈ 𝐴 ↦ if(𝑘 ∈ 𝐷, (𝐹‘𝑘), 0 )) ↾ 𝐷) = ((𝑘 ∈ 𝐴 ↦ (𝐹‘𝑘)) ↾ 𝐷)) |
| 117 | 112, 116 | syl 17 |
. . . . . 6
⊢ (𝜑 → ((𝑘 ∈ 𝐴 ↦ if(𝑘 ∈ 𝐷, (𝐹‘𝑘), 0 )) ↾ 𝐷) = ((𝑘 ∈ 𝐴 ↦ (𝐹‘𝑘)) ↾ 𝐷)) |
| 118 | 110, 117 | eqtr4d 2780 |
. . . . 5
⊢ (𝜑 → (𝐹 ↾ 𝐷) = ((𝑘 ∈ 𝐴 ↦ if(𝑘 ∈ 𝐷, (𝐹‘𝑘), 0 )) ↾ 𝐷)) |
| 119 | 118 | oveq2d 7447 |
. . . 4
⊢ (𝜑 → (𝐺 Σg (𝐹 ↾ 𝐷)) = (𝐺 Σg ((𝑘 ∈ 𝐴 ↦ if(𝑘 ∈ 𝐷, (𝐹‘𝑘), 0 )) ↾ 𝐷))) |
| 120 | 84 | fmpttd 7135 |
. . . . 5
⊢ (𝜑 → (𝑘 ∈ 𝐴 ↦ if(𝑘 ∈ 𝐷, (𝐹‘𝑘), 0 )):𝐴⟶𝐵) |
| 121 | 39 | frnd 6744 |
. . . . . 6
⊢ (𝜑 → ran (𝑘 ∈ 𝐴 ↦ if(𝑘 ∈ 𝐷, (𝐹‘𝑘), 0 )) ⊆
((mrCls‘(SubMnd‘𝐺))‘ran 𝐹)) |
| 122 | 4 | cntzidss 19358 |
. . . . . 6
⊢
((((mrCls‘(SubMnd‘𝐺))‘ran 𝐹) ⊆ (𝑍‘((mrCls‘(SubMnd‘𝐺))‘ran 𝐹)) ∧ ran (𝑘 ∈ 𝐴 ↦ if(𝑘 ∈ 𝐷, (𝐹‘𝑘), 0 )) ⊆
((mrCls‘(SubMnd‘𝐺))‘ran 𝐹)) → ran (𝑘 ∈ 𝐴 ↦ if(𝑘 ∈ 𝐷, (𝐹‘𝑘), 0 )) ⊆ (𝑍‘ran (𝑘 ∈ 𝐴 ↦ if(𝑘 ∈ 𝐷, (𝐹‘𝑘), 0 )))) |
| 123 | 26, 121, 122 | syl2anc 584 |
. . . . 5
⊢ (𝜑 → ran (𝑘 ∈ 𝐴 ↦ if(𝑘 ∈ 𝐷, (𝐹‘𝑘), 0 )) ⊆ (𝑍‘ran (𝑘 ∈ 𝐴 ↦ if(𝑘 ∈ 𝐷, (𝐹‘𝑘), 0 )))) |
| 124 | | eldifn 4132 |
. . . . . . . 8
⊢ (𝑘 ∈ (𝐴 ∖ 𝐷) → ¬ 𝑘 ∈ 𝐷) |
| 125 | 124 | adantl 481 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ (𝐴 ∖ 𝐷)) → ¬ 𝑘 ∈ 𝐷) |
| 126 | 125 | iffalsed 4536 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ (𝐴 ∖ 𝐷)) → if(𝑘 ∈ 𝐷, (𝐹‘𝑘), 0 ) = 0 ) |
| 127 | 126, 6 | suppss2 8225 |
. . . . 5
⊢ (𝜑 → ((𝑘 ∈ 𝐴 ↦ if(𝑘 ∈ 𝐷, (𝐹‘𝑘), 0 )) supp 0 ) ⊆ 𝐷) |
| 128 | 1, 2, 4, 5, 6, 120, 123, 127, 12 | gsumzres 19927 |
. . . 4
⊢ (𝜑 → (𝐺 Σg ((𝑘 ∈ 𝐴 ↦ if(𝑘 ∈ 𝐷, (𝐹‘𝑘), 0 )) ↾ 𝐷)) = (𝐺 Σg (𝑘 ∈ 𝐴 ↦ if(𝑘 ∈ 𝐷, (𝐹‘𝑘), 0 )))) |
| 129 | 119, 128 | eqtrd 2777 |
. . 3
⊢ (𝜑 → (𝐺 Σg (𝐹 ↾ 𝐷)) = (𝐺 Σg (𝑘 ∈ 𝐴 ↦ if(𝑘 ∈ 𝐷, (𝐹‘𝑘), 0 )))) |
| 130 | 109, 129 | oveq12d 7449 |
. 2
⊢ (𝜑 → ((𝐺 Σg (𝐹 ↾ 𝐶)) + (𝐺 Σg (𝐹 ↾ 𝐷))) = ((𝐺 Σg (𝑘 ∈ 𝐴 ↦ if(𝑘 ∈ 𝐶, (𝐹‘𝑘), 0 ))) + (𝐺 Σg (𝑘 ∈ 𝐴 ↦ if(𝑘 ∈ 𝐷, (𝐹‘𝑘), 0 ))))) |
| 131 | 40, 89, 130 | 3eqtr4d 2787 |
1
⊢ (𝜑 → (𝐺 Σg 𝐹) = ((𝐺 Σg (𝐹 ↾ 𝐶)) + (𝐺 Σg (𝐹 ↾ 𝐷)))) |