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 | ffvelrnda 6267 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → (𝐹‘𝑘) ∈ 𝐵) |
8 | | cmnmnd 18031 |
. . . . . . . 8
⊢ (𝐺 ∈ CMnd → 𝐺 ∈ Mnd) |
9 | 3, 8 | syl 17 |
. . . . . . 7
⊢ (𝜑 → 𝐺 ∈ Mnd) |
10 | | eqid 2610 |
. . . . . . . 8
⊢
(0g‘𝐺) = (0g‘𝐺) |
11 | 1, 10 | mndidcl 17131 |
. . . . . . 7
⊢ (𝐺 ∈ Mnd →
(0g‘𝐺)
∈ 𝐵) |
12 | 9, 11 | syl 17 |
. . . . . 6
⊢ (𝜑 → (0g‘𝐺) ∈ 𝐵) |
13 | 12 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → (0g‘𝐺) ∈ 𝐵) |
14 | 7, 13 | ifcld 4081 |
. . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → if(𝑘 ∈ 𝐶, (𝐹‘𝑘), (0g‘𝐺)) ∈ 𝐵) |
15 | | eqid 2610 |
. . . 4
⊢ (𝑘 ∈ 𝐴 ↦ if(𝑘 ∈ 𝐶, (𝐹‘𝑘), (0g‘𝐺))) = (𝑘 ∈ 𝐴 ↦ if(𝑘 ∈ 𝐶, (𝐹‘𝑘), (0g‘𝐺))) |
16 | 14, 15 | fmptd 6292 |
. . 3
⊢ (𝜑 → (𝑘 ∈ 𝐴 ↦ if(𝑘 ∈ 𝐶, (𝐹‘𝑘), (0g‘𝐺))):𝐴⟶𝐵) |
17 | 7, 13 | ifcld 4081 |
. . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → if(𝑘 ∈ 𝐷, (𝐹‘𝑘), (0g‘𝐺)) ∈ 𝐵) |
18 | | eqid 2610 |
. . . 4
⊢ (𝑘 ∈ 𝐴 ↦ if(𝑘 ∈ 𝐷, (𝐹‘𝑘), (0g‘𝐺))) = (𝑘 ∈ 𝐴 ↦ if(𝑘 ∈ 𝐷, (𝐹‘𝑘), (0g‘𝐺))) |
19 | 17, 18 | fmptd 6292 |
. . 3
⊢ (𝜑 → (𝑘 ∈ 𝐴 ↦ if(𝑘 ∈ 𝐷, (𝐹‘𝑘), (0g‘𝐺))):𝐴⟶𝐵) |
20 | | tsmssplit.x |
. . . 4
⊢ (𝜑 → 𝑋 ∈ (𝐺 tsums (𝐹 ↾ 𝐶))) |
21 | 6 | feqmptd 6159 |
. . . . . . . 8
⊢ (𝜑 → 𝐹 = (𝑘 ∈ 𝐴 ↦ (𝐹‘𝑘))) |
22 | 21 | reseq1d 5316 |
. . . . . . 7
⊢ (𝜑 → (𝐹 ↾ 𝐶) = ((𝑘 ∈ 𝐴 ↦ (𝐹‘𝑘)) ↾ 𝐶)) |
23 | | ssun1 3738 |
. . . . . . . . 9
⊢ 𝐶 ⊆ (𝐶 ∪ 𝐷) |
24 | | tsmssplit.u |
. . . . . . . . 9
⊢ (𝜑 → 𝐴 = (𝐶 ∪ 𝐷)) |
25 | 23, 24 | syl5sseqr 3617 |
. . . . . . . 8
⊢ (𝜑 → 𝐶 ⊆ 𝐴) |
26 | | iftrue 4042 |
. . . . . . . . . 10
⊢ (𝑘 ∈ 𝐶 → if(𝑘 ∈ 𝐶, (𝐹‘𝑘), (0g‘𝐺)) = (𝐹‘𝑘)) |
27 | 26 | mpteq2ia 4668 |
. . . . . . . . 9
⊢ (𝑘 ∈ 𝐶 ↦ if(𝑘 ∈ 𝐶, (𝐹‘𝑘), (0g‘𝐺))) = (𝑘 ∈ 𝐶 ↦ (𝐹‘𝑘)) |
28 | | resmpt 5369 |
. . . . . . . . 9
⊢ (𝐶 ⊆ 𝐴 → ((𝑘 ∈ 𝐴 ↦ if(𝑘 ∈ 𝐶, (𝐹‘𝑘), (0g‘𝐺))) ↾ 𝐶) = (𝑘 ∈ 𝐶 ↦ if(𝑘 ∈ 𝐶, (𝐹‘𝑘), (0g‘𝐺)))) |
29 | | resmpt 5369 |
. . . . . . . . 9
⊢ (𝐶 ⊆ 𝐴 → ((𝑘 ∈ 𝐴 ↦ (𝐹‘𝑘)) ↾ 𝐶) = (𝑘 ∈ 𝐶 ↦ (𝐹‘𝑘))) |
30 | 27, 28, 29 | 3eqtr4a 2670 |
. . . . . . . 8
⊢ (𝐶 ⊆ 𝐴 → ((𝑘 ∈ 𝐴 ↦ if(𝑘 ∈ 𝐶, (𝐹‘𝑘), (0g‘𝐺))) ↾ 𝐶) = ((𝑘 ∈ 𝐴 ↦ (𝐹‘𝑘)) ↾ 𝐶)) |
31 | 25, 30 | syl 17 |
. . . . . . 7
⊢ (𝜑 → ((𝑘 ∈ 𝐴 ↦ if(𝑘 ∈ 𝐶, (𝐹‘𝑘), (0g‘𝐺))) ↾ 𝐶) = ((𝑘 ∈ 𝐴 ↦ (𝐹‘𝑘)) ↾ 𝐶)) |
32 | 22, 31 | eqtr4d 2647 |
. . . . . 6
⊢ (𝜑 → (𝐹 ↾ 𝐶) = ((𝑘 ∈ 𝐴 ↦ if(𝑘 ∈ 𝐶, (𝐹‘𝑘), (0g‘𝐺))) ↾ 𝐶)) |
33 | 32 | oveq2d 6565 |
. . . . 5
⊢ (𝜑 → (𝐺 tsums (𝐹 ↾ 𝐶)) = (𝐺 tsums ((𝑘 ∈ 𝐴 ↦ if(𝑘 ∈ 𝐶, (𝐹‘𝑘), (0g‘𝐺))) ↾ 𝐶))) |
34 | | tmdtps 21690 |
. . . . . . 7
⊢ (𝐺 ∈ TopMnd → 𝐺 ∈ TopSp) |
35 | 4, 34 | syl 17 |
. . . . . 6
⊢ (𝜑 → 𝐺 ∈ TopSp) |
36 | | eldifn 3695 |
. . . . . . . . 9
⊢ (𝑘 ∈ (𝐴 ∖ 𝐶) → ¬ 𝑘 ∈ 𝐶) |
37 | 36 | adantl 481 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ (𝐴 ∖ 𝐶)) → ¬ 𝑘 ∈ 𝐶) |
38 | 37 | iffalsed 4047 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ (𝐴 ∖ 𝐶)) → if(𝑘 ∈ 𝐶, (𝐹‘𝑘), (0g‘𝐺)) = (0g‘𝐺)) |
39 | 38, 5 | suppss2 7216 |
. . . . . 6
⊢ (𝜑 → ((𝑘 ∈ 𝐴 ↦ if(𝑘 ∈ 𝐶, (𝐹‘𝑘), (0g‘𝐺))) supp (0g‘𝐺)) ⊆ 𝐶) |
40 | 1, 10, 3, 35, 5, 16, 39 | tsmsres 21757 |
. . . . 5
⊢ (𝜑 → (𝐺 tsums ((𝑘 ∈ 𝐴 ↦ if(𝑘 ∈ 𝐶, (𝐹‘𝑘), (0g‘𝐺))) ↾ 𝐶)) = (𝐺 tsums (𝑘 ∈ 𝐴 ↦ if(𝑘 ∈ 𝐶, (𝐹‘𝑘), (0g‘𝐺))))) |
41 | 33, 40 | eqtrd 2644 |
. . . 4
⊢ (𝜑 → (𝐺 tsums (𝐹 ↾ 𝐶)) = (𝐺 tsums (𝑘 ∈ 𝐴 ↦ if(𝑘 ∈ 𝐶, (𝐹‘𝑘), (0g‘𝐺))))) |
42 | 20, 41 | eleqtrd 2690 |
. . 3
⊢ (𝜑 → 𝑋 ∈ (𝐺 tsums (𝑘 ∈ 𝐴 ↦ if(𝑘 ∈ 𝐶, (𝐹‘𝑘), (0g‘𝐺))))) |
43 | | tsmssplit.y |
. . . 4
⊢ (𝜑 → 𝑌 ∈ (𝐺 tsums (𝐹 ↾ 𝐷))) |
44 | 21 | reseq1d 5316 |
. . . . . . 7
⊢ (𝜑 → (𝐹 ↾ 𝐷) = ((𝑘 ∈ 𝐴 ↦ (𝐹‘𝑘)) ↾ 𝐷)) |
45 | | ssun2 3739 |
. . . . . . . . 9
⊢ 𝐷 ⊆ (𝐶 ∪ 𝐷) |
46 | 45, 24 | syl5sseqr 3617 |
. . . . . . . 8
⊢ (𝜑 → 𝐷 ⊆ 𝐴) |
47 | | iftrue 4042 |
. . . . . . . . . 10
⊢ (𝑘 ∈ 𝐷 → if(𝑘 ∈ 𝐷, (𝐹‘𝑘), (0g‘𝐺)) = (𝐹‘𝑘)) |
48 | 47 | mpteq2ia 4668 |
. . . . . . . . 9
⊢ (𝑘 ∈ 𝐷 ↦ if(𝑘 ∈ 𝐷, (𝐹‘𝑘), (0g‘𝐺))) = (𝑘 ∈ 𝐷 ↦ (𝐹‘𝑘)) |
49 | | resmpt 5369 |
. . . . . . . . 9
⊢ (𝐷 ⊆ 𝐴 → ((𝑘 ∈ 𝐴 ↦ if(𝑘 ∈ 𝐷, (𝐹‘𝑘), (0g‘𝐺))) ↾ 𝐷) = (𝑘 ∈ 𝐷 ↦ if(𝑘 ∈ 𝐷, (𝐹‘𝑘), (0g‘𝐺)))) |
50 | | resmpt 5369 |
. . . . . . . . 9
⊢ (𝐷 ⊆ 𝐴 → ((𝑘 ∈ 𝐴 ↦ (𝐹‘𝑘)) ↾ 𝐷) = (𝑘 ∈ 𝐷 ↦ (𝐹‘𝑘))) |
51 | 48, 49, 50 | 3eqtr4a 2670 |
. . . . . . . 8
⊢ (𝐷 ⊆ 𝐴 → ((𝑘 ∈ 𝐴 ↦ if(𝑘 ∈ 𝐷, (𝐹‘𝑘), (0g‘𝐺))) ↾ 𝐷) = ((𝑘 ∈ 𝐴 ↦ (𝐹‘𝑘)) ↾ 𝐷)) |
52 | 46, 51 | syl 17 |
. . . . . . 7
⊢ (𝜑 → ((𝑘 ∈ 𝐴 ↦ if(𝑘 ∈ 𝐷, (𝐹‘𝑘), (0g‘𝐺))) ↾ 𝐷) = ((𝑘 ∈ 𝐴 ↦ (𝐹‘𝑘)) ↾ 𝐷)) |
53 | 44, 52 | eqtr4d 2647 |
. . . . . 6
⊢ (𝜑 → (𝐹 ↾ 𝐷) = ((𝑘 ∈ 𝐴 ↦ if(𝑘 ∈ 𝐷, (𝐹‘𝑘), (0g‘𝐺))) ↾ 𝐷)) |
54 | 53 | oveq2d 6565 |
. . . . 5
⊢ (𝜑 → (𝐺 tsums (𝐹 ↾ 𝐷)) = (𝐺 tsums ((𝑘 ∈ 𝐴 ↦ if(𝑘 ∈ 𝐷, (𝐹‘𝑘), (0g‘𝐺))) ↾ 𝐷))) |
55 | | eldifn 3695 |
. . . . . . . . 9
⊢ (𝑘 ∈ (𝐴 ∖ 𝐷) → ¬ 𝑘 ∈ 𝐷) |
56 | 55 | adantl 481 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ (𝐴 ∖ 𝐷)) → ¬ 𝑘 ∈ 𝐷) |
57 | 56 | iffalsed 4047 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ (𝐴 ∖ 𝐷)) → if(𝑘 ∈ 𝐷, (𝐹‘𝑘), (0g‘𝐺)) = (0g‘𝐺)) |
58 | 57, 5 | suppss2 7216 |
. . . . . 6
⊢ (𝜑 → ((𝑘 ∈ 𝐴 ↦ if(𝑘 ∈ 𝐷, (𝐹‘𝑘), (0g‘𝐺))) supp (0g‘𝐺)) ⊆ 𝐷) |
59 | 1, 10, 3, 35, 5, 19, 58 | tsmsres 21757 |
. . . . 5
⊢ (𝜑 → (𝐺 tsums ((𝑘 ∈ 𝐴 ↦ if(𝑘 ∈ 𝐷, (𝐹‘𝑘), (0g‘𝐺))) ↾ 𝐷)) = (𝐺 tsums (𝑘 ∈ 𝐴 ↦ if(𝑘 ∈ 𝐷, (𝐹‘𝑘), (0g‘𝐺))))) |
60 | 54, 59 | eqtrd 2644 |
. . . 4
⊢ (𝜑 → (𝐺 tsums (𝐹 ↾ 𝐷)) = (𝐺 tsums (𝑘 ∈ 𝐴 ↦ if(𝑘 ∈ 𝐷, (𝐹‘𝑘), (0g‘𝐺))))) |
61 | 43, 60 | eleqtrd 2690 |
. . 3
⊢ (𝜑 → 𝑌 ∈ (𝐺 tsums (𝑘 ∈ 𝐴 ↦ if(𝑘 ∈ 𝐷, (𝐹‘𝑘), (0g‘𝐺))))) |
62 | 1, 2, 3, 4, 5, 16,
19, 42, 61 | tsmsadd 21760 |
. 2
⊢ (𝜑 → (𝑋 + 𝑌) ∈ (𝐺 tsums ((𝑘 ∈ 𝐴 ↦ if(𝑘 ∈ 𝐶, (𝐹‘𝑘), (0g‘𝐺))) ∘𝑓 + (𝑘 ∈ 𝐴 ↦ if(𝑘 ∈ 𝐷, (𝐹‘𝑘), (0g‘𝐺)))))) |
63 | 26 | adantl 481 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑘 ∈ 𝐴) ∧ 𝑘 ∈ 𝐶) → if(𝑘 ∈ 𝐶, (𝐹‘𝑘), (0g‘𝐺)) = (𝐹‘𝑘)) |
64 | | tsmssplit.i |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝐶 ∩ 𝐷) = ∅) |
65 | | noel 3878 |
. . . . . . . . . . . . . . . 16
⊢ ¬
𝑘 ∈
∅ |
66 | | eleq2 2677 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐶 ∩ 𝐷) = ∅ → (𝑘 ∈ (𝐶 ∩ 𝐷) ↔ 𝑘 ∈ ∅)) |
67 | 65, 66 | mtbiri 316 |
. . . . . . . . . . . . . . 15
⊢ ((𝐶 ∩ 𝐷) = ∅ → ¬ 𝑘 ∈ (𝐶 ∩ 𝐷)) |
68 | 64, 67 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ¬ 𝑘 ∈ (𝐶 ∩ 𝐷)) |
69 | 68 | adantr 480 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → ¬ 𝑘 ∈ (𝐶 ∩ 𝐷)) |
70 | | elin 3758 |
. . . . . . . . . . . . 13
⊢ (𝑘 ∈ (𝐶 ∩ 𝐷) ↔ (𝑘 ∈ 𝐶 ∧ 𝑘 ∈ 𝐷)) |
71 | 69, 70 | sylnib 317 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → ¬ (𝑘 ∈ 𝐶 ∧ 𝑘 ∈ 𝐷)) |
72 | | imnan 437 |
. . . . . . . . . . . 12
⊢ ((𝑘 ∈ 𝐶 → ¬ 𝑘 ∈ 𝐷) ↔ ¬ (𝑘 ∈ 𝐶 ∧ 𝑘 ∈ 𝐷)) |
73 | 71, 72 | sylibr 223 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → (𝑘 ∈ 𝐶 → ¬ 𝑘 ∈ 𝐷)) |
74 | 73 | imp 444 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑘 ∈ 𝐴) ∧ 𝑘 ∈ 𝐶) → ¬ 𝑘 ∈ 𝐷) |
75 | 74 | iffalsed 4047 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑘 ∈ 𝐴) ∧ 𝑘 ∈ 𝐶) → if(𝑘 ∈ 𝐷, (𝐹‘𝑘), (0g‘𝐺)) = (0g‘𝐺)) |
76 | 63, 75 | oveq12d 6567 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑘 ∈ 𝐴) ∧ 𝑘 ∈ 𝐶) → (if(𝑘 ∈ 𝐶, (𝐹‘𝑘), (0g‘𝐺)) + if(𝑘 ∈ 𝐷, (𝐹‘𝑘), (0g‘𝐺))) = ((𝐹‘𝑘) + (0g‘𝐺))) |
77 | 1, 2, 10 | mndrid 17135 |
. . . . . . . . . . 11
⊢ ((𝐺 ∈ Mnd ∧ (𝐹‘𝑘) ∈ 𝐵) → ((𝐹‘𝑘) + (0g‘𝐺)) = (𝐹‘𝑘)) |
78 | 9, 77 | sylan 487 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝐹‘𝑘) ∈ 𝐵) → ((𝐹‘𝑘) + (0g‘𝐺)) = (𝐹‘𝑘)) |
79 | 7, 78 | syldan 486 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → ((𝐹‘𝑘) + (0g‘𝐺)) = (𝐹‘𝑘)) |
80 | 79 | adantr 480 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑘 ∈ 𝐴) ∧ 𝑘 ∈ 𝐶) → ((𝐹‘𝑘) + (0g‘𝐺)) = (𝐹‘𝑘)) |
81 | 76, 80 | eqtrd 2644 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑘 ∈ 𝐴) ∧ 𝑘 ∈ 𝐶) → (if(𝑘 ∈ 𝐶, (𝐹‘𝑘), (0g‘𝐺)) + if(𝑘 ∈ 𝐷, (𝐹‘𝑘), (0g‘𝐺))) = (𝐹‘𝑘)) |
82 | 73 | con2d 128 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → (𝑘 ∈ 𝐷 → ¬ 𝑘 ∈ 𝐶)) |
83 | 82 | imp 444 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑘 ∈ 𝐴) ∧ 𝑘 ∈ 𝐷) → ¬ 𝑘 ∈ 𝐶) |
84 | 83 | iffalsed 4047 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑘 ∈ 𝐴) ∧ 𝑘 ∈ 𝐷) → if(𝑘 ∈ 𝐶, (𝐹‘𝑘), (0g‘𝐺)) = (0g‘𝐺)) |
85 | 47 | adantl 481 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑘 ∈ 𝐴) ∧ 𝑘 ∈ 𝐷) → if(𝑘 ∈ 𝐷, (𝐹‘𝑘), (0g‘𝐺)) = (𝐹‘𝑘)) |
86 | 84, 85 | oveq12d 6567 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑘 ∈ 𝐴) ∧ 𝑘 ∈ 𝐷) → (if(𝑘 ∈ 𝐶, (𝐹‘𝑘), (0g‘𝐺)) + if(𝑘 ∈ 𝐷, (𝐹‘𝑘), (0g‘𝐺))) = ((0g‘𝐺) + (𝐹‘𝑘))) |
87 | 1, 2, 10 | mndlid 17134 |
. . . . . . . . . . 11
⊢ ((𝐺 ∈ Mnd ∧ (𝐹‘𝑘) ∈ 𝐵) → ((0g‘𝐺) + (𝐹‘𝑘)) = (𝐹‘𝑘)) |
88 | 9, 87 | sylan 487 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝐹‘𝑘) ∈ 𝐵) → ((0g‘𝐺) + (𝐹‘𝑘)) = (𝐹‘𝑘)) |
89 | 7, 88 | syldan 486 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → ((0g‘𝐺) + (𝐹‘𝑘)) = (𝐹‘𝑘)) |
90 | 89 | adantr 480 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑘 ∈ 𝐴) ∧ 𝑘 ∈ 𝐷) → ((0g‘𝐺) + (𝐹‘𝑘)) = (𝐹‘𝑘)) |
91 | 86, 90 | eqtrd 2644 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑘 ∈ 𝐴) ∧ 𝑘 ∈ 𝐷) → (if(𝑘 ∈ 𝐶, (𝐹‘𝑘), (0g‘𝐺)) + if(𝑘 ∈ 𝐷, (𝐹‘𝑘), (0g‘𝐺))) = (𝐹‘𝑘)) |
92 | 24 | eleq2d 2673 |
. . . . . . . . 9
⊢ (𝜑 → (𝑘 ∈ 𝐴 ↔ 𝑘 ∈ (𝐶 ∪ 𝐷))) |
93 | | elun 3715 |
. . . . . . . . 9
⊢ (𝑘 ∈ (𝐶 ∪ 𝐷) ↔ (𝑘 ∈ 𝐶 ∨ 𝑘 ∈ 𝐷)) |
94 | 92, 93 | syl6bb 275 |
. . . . . . . 8
⊢ (𝜑 → (𝑘 ∈ 𝐴 ↔ (𝑘 ∈ 𝐶 ∨ 𝑘 ∈ 𝐷))) |
95 | 94 | biimpa 500 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → (𝑘 ∈ 𝐶 ∨ 𝑘 ∈ 𝐷)) |
96 | 81, 91, 95 | mpjaodan 823 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → (if(𝑘 ∈ 𝐶, (𝐹‘𝑘), (0g‘𝐺)) + if(𝑘 ∈ 𝐷, (𝐹‘𝑘), (0g‘𝐺))) = (𝐹‘𝑘)) |
97 | 96 | mpteq2dva 4672 |
. . . . 5
⊢ (𝜑 → (𝑘 ∈ 𝐴 ↦ (if(𝑘 ∈ 𝐶, (𝐹‘𝑘), (0g‘𝐺)) + if(𝑘 ∈ 𝐷, (𝐹‘𝑘), (0g‘𝐺)))) = (𝑘 ∈ 𝐴 ↦ (𝐹‘𝑘))) |
98 | 21, 97 | eqtr4d 2647 |
. . . 4
⊢ (𝜑 → 𝐹 = (𝑘 ∈ 𝐴 ↦ (if(𝑘 ∈ 𝐶, (𝐹‘𝑘), (0g‘𝐺)) + if(𝑘 ∈ 𝐷, (𝐹‘𝑘), (0g‘𝐺))))) |
99 | | eqidd 2611 |
. . . . 5
⊢ (𝜑 → (𝑘 ∈ 𝐴 ↦ if(𝑘 ∈ 𝐶, (𝐹‘𝑘), (0g‘𝐺))) = (𝑘 ∈ 𝐴 ↦ if(𝑘 ∈ 𝐶, (𝐹‘𝑘), (0g‘𝐺)))) |
100 | | eqidd 2611 |
. . . . 5
⊢ (𝜑 → (𝑘 ∈ 𝐴 ↦ if(𝑘 ∈ 𝐷, (𝐹‘𝑘), (0g‘𝐺))) = (𝑘 ∈ 𝐴 ↦ if(𝑘 ∈ 𝐷, (𝐹‘𝑘), (0g‘𝐺)))) |
101 | 5, 14, 17, 99, 100 | offval2 6812 |
. . . 4
⊢ (𝜑 → ((𝑘 ∈ 𝐴 ↦ if(𝑘 ∈ 𝐶, (𝐹‘𝑘), (0g‘𝐺))) ∘𝑓 + (𝑘 ∈ 𝐴 ↦ if(𝑘 ∈ 𝐷, (𝐹‘𝑘), (0g‘𝐺)))) = (𝑘 ∈ 𝐴 ↦ (if(𝑘 ∈ 𝐶, (𝐹‘𝑘), (0g‘𝐺)) + if(𝑘 ∈ 𝐷, (𝐹‘𝑘), (0g‘𝐺))))) |
102 | 98, 101 | eqtr4d 2647 |
. . 3
⊢ (𝜑 → 𝐹 = ((𝑘 ∈ 𝐴 ↦ if(𝑘 ∈ 𝐶, (𝐹‘𝑘), (0g‘𝐺))) ∘𝑓 + (𝑘 ∈ 𝐴 ↦ if(𝑘 ∈ 𝐷, (𝐹‘𝑘), (0g‘𝐺))))) |
103 | 102 | oveq2d 6565 |
. 2
⊢ (𝜑 → (𝐺 tsums 𝐹) = (𝐺 tsums ((𝑘 ∈ 𝐴 ↦ if(𝑘 ∈ 𝐶, (𝐹‘𝑘), (0g‘𝐺))) ∘𝑓 + (𝑘 ∈ 𝐴 ↦ if(𝑘 ∈ 𝐷, (𝐹‘𝑘), (0g‘𝐺)))))) |
104 | 62, 103 | eleqtrrd 2691 |
1
⊢ (𝜑 → (𝑋 + 𝑌) ∈ (𝐺 tsums 𝐹)) |