| Step | Hyp | Ref
| Expression |
| 1 | | tsmssplit.b |
. . 3
⊢ 𝐵 = (Base‘𝐺) |
| 2 | | tsmssplit.p |
. . 3
⊢ + =
(+g‘𝐺) |
| 3 | | tsmssplit.1 |
. . 3
⊢ (𝜑 → 𝐺 ∈ CMnd) |
| 4 | | tsmssplit.2 |
. . 3
⊢ (𝜑 → 𝐺 ∈ TopMnd) |
| 5 | | tsmssplit.a |
. . 3
⊢ (𝜑 → 𝐴 ∈ 𝑉) |
| 6 | | tsmssplit.f |
. . . . . 6
⊢ (𝜑 → 𝐹:𝐴⟶𝐵) |
| 7 | 6 | ffvelcdmda 7104 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → (𝐹‘𝑘) ∈ 𝐵) |
| 8 | | cmnmnd 19815 |
. . . . . . . 8
⊢ (𝐺 ∈ CMnd → 𝐺 ∈ Mnd) |
| 9 | 3, 8 | syl 17 |
. . . . . . 7
⊢ (𝜑 → 𝐺 ∈ Mnd) |
| 10 | | eqid 2737 |
. . . . . . . 8
⊢
(0g‘𝐺) = (0g‘𝐺) |
| 11 | 1, 10 | mndidcl 18762 |
. . . . . . 7
⊢ (𝐺 ∈ Mnd →
(0g‘𝐺)
∈ 𝐵) |
| 12 | 9, 11 | syl 17 |
. . . . . 6
⊢ (𝜑 → (0g‘𝐺) ∈ 𝐵) |
| 13 | 12 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → (0g‘𝐺) ∈ 𝐵) |
| 14 | 7, 13 | ifcld 4572 |
. . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → if(𝑘 ∈ 𝐶, (𝐹‘𝑘), (0g‘𝐺)) ∈ 𝐵) |
| 15 | 14 | fmpttd 7135 |
. . 3
⊢ (𝜑 → (𝑘 ∈ 𝐴 ↦ if(𝑘 ∈ 𝐶, (𝐹‘𝑘), (0g‘𝐺))):𝐴⟶𝐵) |
| 16 | 7, 13 | ifcld 4572 |
. . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → if(𝑘 ∈ 𝐷, (𝐹‘𝑘), (0g‘𝐺)) ∈ 𝐵) |
| 17 | 16 | fmpttd 7135 |
. . 3
⊢ (𝜑 → (𝑘 ∈ 𝐴 ↦ if(𝑘 ∈ 𝐷, (𝐹‘𝑘), (0g‘𝐺))):𝐴⟶𝐵) |
| 18 | | tsmssplit.x |
. . . 4
⊢ (𝜑 → 𝑋 ∈ (𝐺 tsums (𝐹 ↾ 𝐶))) |
| 19 | 6 | feqmptd 6977 |
. . . . . . . 8
⊢ (𝜑 → 𝐹 = (𝑘 ∈ 𝐴 ↦ (𝐹‘𝑘))) |
| 20 | 19 | reseq1d 5996 |
. . . . . . 7
⊢ (𝜑 → (𝐹 ↾ 𝐶) = ((𝑘 ∈ 𝐴 ↦ (𝐹‘𝑘)) ↾ 𝐶)) |
| 21 | | ssun1 4178 |
. . . . . . . . 9
⊢ 𝐶 ⊆ (𝐶 ∪ 𝐷) |
| 22 | | tsmssplit.u |
. . . . . . . . 9
⊢ (𝜑 → 𝐴 = (𝐶 ∪ 𝐷)) |
| 23 | 21, 22 | sseqtrrid 4027 |
. . . . . . . 8
⊢ (𝜑 → 𝐶 ⊆ 𝐴) |
| 24 | | iftrue 4531 |
. . . . . . . . . 10
⊢ (𝑘 ∈ 𝐶 → if(𝑘 ∈ 𝐶, (𝐹‘𝑘), (0g‘𝐺)) = (𝐹‘𝑘)) |
| 25 | 24 | mpteq2ia 5245 |
. . . . . . . . 9
⊢ (𝑘 ∈ 𝐶 ↦ if(𝑘 ∈ 𝐶, (𝐹‘𝑘), (0g‘𝐺))) = (𝑘 ∈ 𝐶 ↦ (𝐹‘𝑘)) |
| 26 | | resmpt 6055 |
. . . . . . . . 9
⊢ (𝐶 ⊆ 𝐴 → ((𝑘 ∈ 𝐴 ↦ if(𝑘 ∈ 𝐶, (𝐹‘𝑘), (0g‘𝐺))) ↾ 𝐶) = (𝑘 ∈ 𝐶 ↦ if(𝑘 ∈ 𝐶, (𝐹‘𝑘), (0g‘𝐺)))) |
| 27 | | resmpt 6055 |
. . . . . . . . 9
⊢ (𝐶 ⊆ 𝐴 → ((𝑘 ∈ 𝐴 ↦ (𝐹‘𝑘)) ↾ 𝐶) = (𝑘 ∈ 𝐶 ↦ (𝐹‘𝑘))) |
| 28 | 25, 26, 27 | 3eqtr4a 2803 |
. . . . . . . 8
⊢ (𝐶 ⊆ 𝐴 → ((𝑘 ∈ 𝐴 ↦ if(𝑘 ∈ 𝐶, (𝐹‘𝑘), (0g‘𝐺))) ↾ 𝐶) = ((𝑘 ∈ 𝐴 ↦ (𝐹‘𝑘)) ↾ 𝐶)) |
| 29 | 23, 28 | syl 17 |
. . . . . . 7
⊢ (𝜑 → ((𝑘 ∈ 𝐴 ↦ if(𝑘 ∈ 𝐶, (𝐹‘𝑘), (0g‘𝐺))) ↾ 𝐶) = ((𝑘 ∈ 𝐴 ↦ (𝐹‘𝑘)) ↾ 𝐶)) |
| 30 | 20, 29 | eqtr4d 2780 |
. . . . . 6
⊢ (𝜑 → (𝐹 ↾ 𝐶) = ((𝑘 ∈ 𝐴 ↦ if(𝑘 ∈ 𝐶, (𝐹‘𝑘), (0g‘𝐺))) ↾ 𝐶)) |
| 31 | 30 | oveq2d 7447 |
. . . . 5
⊢ (𝜑 → (𝐺 tsums (𝐹 ↾ 𝐶)) = (𝐺 tsums ((𝑘 ∈ 𝐴 ↦ if(𝑘 ∈ 𝐶, (𝐹‘𝑘), (0g‘𝐺))) ↾ 𝐶))) |
| 32 | | tmdtps 24084 |
. . . . . . 7
⊢ (𝐺 ∈ TopMnd → 𝐺 ∈ TopSp) |
| 33 | 4, 32 | syl 17 |
. . . . . 6
⊢ (𝜑 → 𝐺 ∈ TopSp) |
| 34 | | eldifn 4132 |
. . . . . . . . 9
⊢ (𝑘 ∈ (𝐴 ∖ 𝐶) → ¬ 𝑘 ∈ 𝐶) |
| 35 | 34 | adantl 481 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ (𝐴 ∖ 𝐶)) → ¬ 𝑘 ∈ 𝐶) |
| 36 | 35 | iffalsed 4536 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ (𝐴 ∖ 𝐶)) → if(𝑘 ∈ 𝐶, (𝐹‘𝑘), (0g‘𝐺)) = (0g‘𝐺)) |
| 37 | 36, 5 | suppss2 8225 |
. . . . . 6
⊢ (𝜑 → ((𝑘 ∈ 𝐴 ↦ if(𝑘 ∈ 𝐶, (𝐹‘𝑘), (0g‘𝐺))) supp (0g‘𝐺)) ⊆ 𝐶) |
| 38 | 1, 10, 3, 33, 5, 15, 37 | tsmsres 24152 |
. . . . 5
⊢ (𝜑 → (𝐺 tsums ((𝑘 ∈ 𝐴 ↦ if(𝑘 ∈ 𝐶, (𝐹‘𝑘), (0g‘𝐺))) ↾ 𝐶)) = (𝐺 tsums (𝑘 ∈ 𝐴 ↦ if(𝑘 ∈ 𝐶, (𝐹‘𝑘), (0g‘𝐺))))) |
| 39 | 31, 38 | eqtrd 2777 |
. . . 4
⊢ (𝜑 → (𝐺 tsums (𝐹 ↾ 𝐶)) = (𝐺 tsums (𝑘 ∈ 𝐴 ↦ if(𝑘 ∈ 𝐶, (𝐹‘𝑘), (0g‘𝐺))))) |
| 40 | 18, 39 | eleqtrd 2843 |
. . 3
⊢ (𝜑 → 𝑋 ∈ (𝐺 tsums (𝑘 ∈ 𝐴 ↦ if(𝑘 ∈ 𝐶, (𝐹‘𝑘), (0g‘𝐺))))) |
| 41 | | tsmssplit.y |
. . . 4
⊢ (𝜑 → 𝑌 ∈ (𝐺 tsums (𝐹 ↾ 𝐷))) |
| 42 | 19 | reseq1d 5996 |
. . . . . . 7
⊢ (𝜑 → (𝐹 ↾ 𝐷) = ((𝑘 ∈ 𝐴 ↦ (𝐹‘𝑘)) ↾ 𝐷)) |
| 43 | | ssun2 4179 |
. . . . . . . . 9
⊢ 𝐷 ⊆ (𝐶 ∪ 𝐷) |
| 44 | 43, 22 | sseqtrrid 4027 |
. . . . . . . 8
⊢ (𝜑 → 𝐷 ⊆ 𝐴) |
| 45 | | iftrue 4531 |
. . . . . . . . . 10
⊢ (𝑘 ∈ 𝐷 → if(𝑘 ∈ 𝐷, (𝐹‘𝑘), (0g‘𝐺)) = (𝐹‘𝑘)) |
| 46 | 45 | mpteq2ia 5245 |
. . . . . . . . 9
⊢ (𝑘 ∈ 𝐷 ↦ if(𝑘 ∈ 𝐷, (𝐹‘𝑘), (0g‘𝐺))) = (𝑘 ∈ 𝐷 ↦ (𝐹‘𝑘)) |
| 47 | | resmpt 6055 |
. . . . . . . . 9
⊢ (𝐷 ⊆ 𝐴 → ((𝑘 ∈ 𝐴 ↦ if(𝑘 ∈ 𝐷, (𝐹‘𝑘), (0g‘𝐺))) ↾ 𝐷) = (𝑘 ∈ 𝐷 ↦ if(𝑘 ∈ 𝐷, (𝐹‘𝑘), (0g‘𝐺)))) |
| 48 | | resmpt 6055 |
. . . . . . . . 9
⊢ (𝐷 ⊆ 𝐴 → ((𝑘 ∈ 𝐴 ↦ (𝐹‘𝑘)) ↾ 𝐷) = (𝑘 ∈ 𝐷 ↦ (𝐹‘𝑘))) |
| 49 | 46, 47, 48 | 3eqtr4a 2803 |
. . . . . . . 8
⊢ (𝐷 ⊆ 𝐴 → ((𝑘 ∈ 𝐴 ↦ if(𝑘 ∈ 𝐷, (𝐹‘𝑘), (0g‘𝐺))) ↾ 𝐷) = ((𝑘 ∈ 𝐴 ↦ (𝐹‘𝑘)) ↾ 𝐷)) |
| 50 | 44, 49 | syl 17 |
. . . . . . 7
⊢ (𝜑 → ((𝑘 ∈ 𝐴 ↦ if(𝑘 ∈ 𝐷, (𝐹‘𝑘), (0g‘𝐺))) ↾ 𝐷) = ((𝑘 ∈ 𝐴 ↦ (𝐹‘𝑘)) ↾ 𝐷)) |
| 51 | 42, 50 | eqtr4d 2780 |
. . . . . 6
⊢ (𝜑 → (𝐹 ↾ 𝐷) = ((𝑘 ∈ 𝐴 ↦ if(𝑘 ∈ 𝐷, (𝐹‘𝑘), (0g‘𝐺))) ↾ 𝐷)) |
| 52 | 51 | oveq2d 7447 |
. . . . 5
⊢ (𝜑 → (𝐺 tsums (𝐹 ↾ 𝐷)) = (𝐺 tsums ((𝑘 ∈ 𝐴 ↦ if(𝑘 ∈ 𝐷, (𝐹‘𝑘), (0g‘𝐺))) ↾ 𝐷))) |
| 53 | | eldifn 4132 |
. . . . . . . . 9
⊢ (𝑘 ∈ (𝐴 ∖ 𝐷) → ¬ 𝑘 ∈ 𝐷) |
| 54 | 53 | adantl 481 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ (𝐴 ∖ 𝐷)) → ¬ 𝑘 ∈ 𝐷) |
| 55 | 54 | iffalsed 4536 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ (𝐴 ∖ 𝐷)) → if(𝑘 ∈ 𝐷, (𝐹‘𝑘), (0g‘𝐺)) = (0g‘𝐺)) |
| 56 | 55, 5 | suppss2 8225 |
. . . . . 6
⊢ (𝜑 → ((𝑘 ∈ 𝐴 ↦ if(𝑘 ∈ 𝐷, (𝐹‘𝑘), (0g‘𝐺))) supp (0g‘𝐺)) ⊆ 𝐷) |
| 57 | 1, 10, 3, 33, 5, 17, 56 | tsmsres 24152 |
. . . . 5
⊢ (𝜑 → (𝐺 tsums ((𝑘 ∈ 𝐴 ↦ if(𝑘 ∈ 𝐷, (𝐹‘𝑘), (0g‘𝐺))) ↾ 𝐷)) = (𝐺 tsums (𝑘 ∈ 𝐴 ↦ if(𝑘 ∈ 𝐷, (𝐹‘𝑘), (0g‘𝐺))))) |
| 58 | 52, 57 | eqtrd 2777 |
. . . 4
⊢ (𝜑 → (𝐺 tsums (𝐹 ↾ 𝐷)) = (𝐺 tsums (𝑘 ∈ 𝐴 ↦ if(𝑘 ∈ 𝐷, (𝐹‘𝑘), (0g‘𝐺))))) |
| 59 | 41, 58 | eleqtrd 2843 |
. . 3
⊢ (𝜑 → 𝑌 ∈ (𝐺 tsums (𝑘 ∈ 𝐴 ↦ if(𝑘 ∈ 𝐷, (𝐹‘𝑘), (0g‘𝐺))))) |
| 60 | 1, 2, 3, 4, 5, 15,
17, 40, 59 | tsmsadd 24155 |
. 2
⊢ (𝜑 → (𝑋 + 𝑌) ∈ (𝐺 tsums ((𝑘 ∈ 𝐴 ↦ if(𝑘 ∈ 𝐶, (𝐹‘𝑘), (0g‘𝐺))) ∘f + (𝑘 ∈ 𝐴 ↦ if(𝑘 ∈ 𝐷, (𝐹‘𝑘), (0g‘𝐺)))))) |
| 61 | 24 | adantl 481 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑘 ∈ 𝐴) ∧ 𝑘 ∈ 𝐶) → if(𝑘 ∈ 𝐶, (𝐹‘𝑘), (0g‘𝐺)) = (𝐹‘𝑘)) |
| 62 | | tsmssplit.i |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝐶 ∩ 𝐷) = ∅) |
| 63 | | noel 4338 |
. . . . . . . . . . . . . . . 16
⊢ ¬
𝑘 ∈
∅ |
| 64 | | eleq2 2830 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐶 ∩ 𝐷) = ∅ → (𝑘 ∈ (𝐶 ∩ 𝐷) ↔ 𝑘 ∈ ∅)) |
| 65 | 63, 64 | mtbiri 327 |
. . . . . . . . . . . . . . 15
⊢ ((𝐶 ∩ 𝐷) = ∅ → ¬ 𝑘 ∈ (𝐶 ∩ 𝐷)) |
| 66 | 62, 65 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ¬ 𝑘 ∈ (𝐶 ∩ 𝐷)) |
| 67 | 66 | adantr 480 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → ¬ 𝑘 ∈ (𝐶 ∩ 𝐷)) |
| 68 | | elin 3967 |
. . . . . . . . . . . . 13
⊢ (𝑘 ∈ (𝐶 ∩ 𝐷) ↔ (𝑘 ∈ 𝐶 ∧ 𝑘 ∈ 𝐷)) |
| 69 | 67, 68 | sylnib 328 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → ¬ (𝑘 ∈ 𝐶 ∧ 𝑘 ∈ 𝐷)) |
| 70 | | imnan 399 |
. . . . . . . . . . . 12
⊢ ((𝑘 ∈ 𝐶 → ¬ 𝑘 ∈ 𝐷) ↔ ¬ (𝑘 ∈ 𝐶 ∧ 𝑘 ∈ 𝐷)) |
| 71 | 69, 70 | sylibr 234 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → (𝑘 ∈ 𝐶 → ¬ 𝑘 ∈ 𝐷)) |
| 72 | 71 | imp 406 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑘 ∈ 𝐴) ∧ 𝑘 ∈ 𝐶) → ¬ 𝑘 ∈ 𝐷) |
| 73 | 72 | iffalsed 4536 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑘 ∈ 𝐴) ∧ 𝑘 ∈ 𝐶) → if(𝑘 ∈ 𝐷, (𝐹‘𝑘), (0g‘𝐺)) = (0g‘𝐺)) |
| 74 | 61, 73 | oveq12d 7449 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑘 ∈ 𝐴) ∧ 𝑘 ∈ 𝐶) → (if(𝑘 ∈ 𝐶, (𝐹‘𝑘), (0g‘𝐺)) + if(𝑘 ∈ 𝐷, (𝐹‘𝑘), (0g‘𝐺))) = ((𝐹‘𝑘) + (0g‘𝐺))) |
| 75 | 1, 2, 10 | mndrid 18768 |
. . . . . . . . . 10
⊢ ((𝐺 ∈ Mnd ∧ (𝐹‘𝑘) ∈ 𝐵) → ((𝐹‘𝑘) + (0g‘𝐺)) = (𝐹‘𝑘)) |
| 76 | 9, 7, 75 | syl2an2r 685 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → ((𝐹‘𝑘) + (0g‘𝐺)) = (𝐹‘𝑘)) |
| 77 | 76 | adantr 480 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑘 ∈ 𝐴) ∧ 𝑘 ∈ 𝐶) → ((𝐹‘𝑘) + (0g‘𝐺)) = (𝐹‘𝑘)) |
| 78 | 74, 77 | eqtrd 2777 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑘 ∈ 𝐴) ∧ 𝑘 ∈ 𝐶) → (if(𝑘 ∈ 𝐶, (𝐹‘𝑘), (0g‘𝐺)) + if(𝑘 ∈ 𝐷, (𝐹‘𝑘), (0g‘𝐺))) = (𝐹‘𝑘)) |
| 79 | 71 | con2d 134 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → (𝑘 ∈ 𝐷 → ¬ 𝑘 ∈ 𝐶)) |
| 80 | 79 | imp 406 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑘 ∈ 𝐴) ∧ 𝑘 ∈ 𝐷) → ¬ 𝑘 ∈ 𝐶) |
| 81 | 80 | iffalsed 4536 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑘 ∈ 𝐴) ∧ 𝑘 ∈ 𝐷) → if(𝑘 ∈ 𝐶, (𝐹‘𝑘), (0g‘𝐺)) = (0g‘𝐺)) |
| 82 | 45 | adantl 481 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑘 ∈ 𝐴) ∧ 𝑘 ∈ 𝐷) → if(𝑘 ∈ 𝐷, (𝐹‘𝑘), (0g‘𝐺)) = (𝐹‘𝑘)) |
| 83 | 81, 82 | oveq12d 7449 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑘 ∈ 𝐴) ∧ 𝑘 ∈ 𝐷) → (if(𝑘 ∈ 𝐶, (𝐹‘𝑘), (0g‘𝐺)) + if(𝑘 ∈ 𝐷, (𝐹‘𝑘), (0g‘𝐺))) = ((0g‘𝐺) + (𝐹‘𝑘))) |
| 84 | 1, 2, 10 | mndlid 18767 |
. . . . . . . . . 10
⊢ ((𝐺 ∈ Mnd ∧ (𝐹‘𝑘) ∈ 𝐵) → ((0g‘𝐺) + (𝐹‘𝑘)) = (𝐹‘𝑘)) |
| 85 | 9, 7, 84 | syl2an2r 685 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → ((0g‘𝐺) + (𝐹‘𝑘)) = (𝐹‘𝑘)) |
| 86 | 85 | adantr 480 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑘 ∈ 𝐴) ∧ 𝑘 ∈ 𝐷) → ((0g‘𝐺) + (𝐹‘𝑘)) = (𝐹‘𝑘)) |
| 87 | 83, 86 | eqtrd 2777 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑘 ∈ 𝐴) ∧ 𝑘 ∈ 𝐷) → (if(𝑘 ∈ 𝐶, (𝐹‘𝑘), (0g‘𝐺)) + if(𝑘 ∈ 𝐷, (𝐹‘𝑘), (0g‘𝐺))) = (𝐹‘𝑘)) |
| 88 | 22 | eleq2d 2827 |
. . . . . . . . 9
⊢ (𝜑 → (𝑘 ∈ 𝐴 ↔ 𝑘 ∈ (𝐶 ∪ 𝐷))) |
| 89 | | elun 4153 |
. . . . . . . . 9
⊢ (𝑘 ∈ (𝐶 ∪ 𝐷) ↔ (𝑘 ∈ 𝐶 ∨ 𝑘 ∈ 𝐷)) |
| 90 | 88, 89 | bitrdi 287 |
. . . . . . . 8
⊢ (𝜑 → (𝑘 ∈ 𝐴 ↔ (𝑘 ∈ 𝐶 ∨ 𝑘 ∈ 𝐷))) |
| 91 | 90 | biimpa 476 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → (𝑘 ∈ 𝐶 ∨ 𝑘 ∈ 𝐷)) |
| 92 | 78, 87, 91 | mpjaodan 961 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → (if(𝑘 ∈ 𝐶, (𝐹‘𝑘), (0g‘𝐺)) + if(𝑘 ∈ 𝐷, (𝐹‘𝑘), (0g‘𝐺))) = (𝐹‘𝑘)) |
| 93 | 92 | mpteq2dva 5242 |
. . . . 5
⊢ (𝜑 → (𝑘 ∈ 𝐴 ↦ (if(𝑘 ∈ 𝐶, (𝐹‘𝑘), (0g‘𝐺)) + if(𝑘 ∈ 𝐷, (𝐹‘𝑘), (0g‘𝐺)))) = (𝑘 ∈ 𝐴 ↦ (𝐹‘𝑘))) |
| 94 | 19, 93 | eqtr4d 2780 |
. . . 4
⊢ (𝜑 → 𝐹 = (𝑘 ∈ 𝐴 ↦ (if(𝑘 ∈ 𝐶, (𝐹‘𝑘), (0g‘𝐺)) + if(𝑘 ∈ 𝐷, (𝐹‘𝑘), (0g‘𝐺))))) |
| 95 | | eqidd 2738 |
. . . . 5
⊢ (𝜑 → (𝑘 ∈ 𝐴 ↦ if(𝑘 ∈ 𝐶, (𝐹‘𝑘), (0g‘𝐺))) = (𝑘 ∈ 𝐴 ↦ if(𝑘 ∈ 𝐶, (𝐹‘𝑘), (0g‘𝐺)))) |
| 96 | | eqidd 2738 |
. . . . 5
⊢ (𝜑 → (𝑘 ∈ 𝐴 ↦ if(𝑘 ∈ 𝐷, (𝐹‘𝑘), (0g‘𝐺))) = (𝑘 ∈ 𝐴 ↦ if(𝑘 ∈ 𝐷, (𝐹‘𝑘), (0g‘𝐺)))) |
| 97 | 5, 14, 16, 95, 96 | offval2 7717 |
. . . 4
⊢ (𝜑 → ((𝑘 ∈ 𝐴 ↦ if(𝑘 ∈ 𝐶, (𝐹‘𝑘), (0g‘𝐺))) ∘f + (𝑘 ∈ 𝐴 ↦ if(𝑘 ∈ 𝐷, (𝐹‘𝑘), (0g‘𝐺)))) = (𝑘 ∈ 𝐴 ↦ (if(𝑘 ∈ 𝐶, (𝐹‘𝑘), (0g‘𝐺)) + if(𝑘 ∈ 𝐷, (𝐹‘𝑘), (0g‘𝐺))))) |
| 98 | 94, 97 | eqtr4d 2780 |
. . 3
⊢ (𝜑 → 𝐹 = ((𝑘 ∈ 𝐴 ↦ if(𝑘 ∈ 𝐶, (𝐹‘𝑘), (0g‘𝐺))) ∘f + (𝑘 ∈ 𝐴 ↦ if(𝑘 ∈ 𝐷, (𝐹‘𝑘), (0g‘𝐺))))) |
| 99 | 98 | oveq2d 7447 |
. 2
⊢ (𝜑 → (𝐺 tsums 𝐹) = (𝐺 tsums ((𝑘 ∈ 𝐴 ↦ if(𝑘 ∈ 𝐶, (𝐹‘𝑘), (0g‘𝐺))) ∘f + (𝑘 ∈ 𝐴 ↦ if(𝑘 ∈ 𝐷, (𝐹‘𝑘), (0g‘𝐺)))))) |
| 100 | 60, 99 | eleqtrrd 2844 |
1
⊢ (𝜑 → (𝑋 + 𝑌) ∈ (𝐺 tsums 𝐹)) |