Metamath Proof Explorer

Theorem tsmssplit

Description: Split a topological group sum into two parts. (Contributed by Mario Carneiro, 19-Sep-2015) (Proof shortened by AV, 24-Jul-2019)

Ref Expression
Hypotheses tsmssplit.b ⊢ 𝐵 = ( Base ‘ 𝐺 )
tsmssplit.p ⊢ + = ( +g ‘ 𝐺 )
tsmssplit.1 ⊢ ( 𝜑 → 𝐺 ∈ CMnd )
tsmssplit.2 ⊢ ( 𝜑 → 𝐺 ∈ TopMnd )
tsmssplit.a ⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
tsmssplit.f ⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ 𝐵 )
tsmssplit.x ⊢ ( 𝜑 → 𝑋 ∈ ( 𝐺 tsums ( 𝐹 ↾ 𝐶 ) ) )
tsmssplit.y ⊢ ( 𝜑 → 𝑌 ∈ ( 𝐺 tsums ( 𝐹 ↾ 𝐷 ) ) )
tsmssplit.i ⊢ ( 𝜑 → ( 𝐶 ∩ 𝐷 ) = ∅ )
tsmssplit.u ⊢ ( 𝜑 → 𝐴 = ( 𝐶 ∪ 𝐷 ) )
Assertion tsmssplit ( 𝜑 → ( 𝑋 + 𝑌 ) ∈ ( 𝐺 tsums 𝐹 ) )

Proof

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