Metamath Proof Explorer

Theorem dvaddbr

Description: The sum rule for derivatives at a point. For the (simpler but more limited) function version, see dvadd . (Contributed by Mario Carneiro, 9-Aug-2014) (Revised by Mario Carneiro, 28-Dec-2016)

Ref Expression
Hypotheses dvadd.f ⊢ ( 𝜑 → 𝐹 : 𝑋 ⟶ ℂ )
dvadd.x ⊢ ( 𝜑 → 𝑋 ⊆ 𝑆 )
dvadd.g ⊢ ( 𝜑 → 𝐺 : 𝑌 ⟶ ℂ )
dvadd.y ⊢ ( 𝜑 → 𝑌 ⊆ 𝑆 )
dvaddbr.s ⊢ ( 𝜑 → 𝑆 ⊆ ℂ )
dvadd.k ⊢ ( 𝜑 → 𝐾 ∈ 𝑉 )
dvadd.l ⊢ ( 𝜑 → 𝐿 ∈ 𝑉 )
dvadd.bf ⊢ ( 𝜑 → 𝐶 ( 𝑆 D 𝐹 ) 𝐾 )
dvadd.bg ⊢ ( 𝜑 → 𝐶 ( 𝑆 D 𝐺 ) 𝐿 )
dvadd.j ⊢ 𝐽 = ( TopOpen ‘ ℂfld )
Assertion dvaddbr ( 𝜑 → 𝐶 ( 𝑆 D ( 𝐹 ∘f + 𝐺 ) ) ( 𝐾 + 𝐿 ) )

Proof

Step Hyp Ref Expression
1 dvadd.f ⊢ ( 𝜑 → 𝐹 : 𝑋 ⟶ ℂ )
2 dvadd.x ⊢ ( 𝜑 → 𝑋 ⊆ 𝑆 )
3 dvadd.g ⊢ ( 𝜑 → 𝐺 : 𝑌 ⟶ ℂ )
4 dvadd.y ⊢ ( 𝜑 → 𝑌 ⊆ 𝑆 )
5 dvaddbr.s ⊢ ( 𝜑 → 𝑆 ⊆ ℂ )
6 dvadd.k ⊢ ( 𝜑 → 𝐾 ∈ 𝑉 )
7 dvadd.l ⊢ ( 𝜑 → 𝐿 ∈ 𝑉 )
8 dvadd.bf ⊢ ( 𝜑 → 𝐶 ( 𝑆 D 𝐹 ) 𝐾 )
9 dvadd.bg ⊢ ( 𝜑 → 𝐶 ( 𝑆 D 𝐺 ) 𝐿 )
10 dvadd.j ⊢ 𝐽 = ( TopOpen ‘ ℂfld )
11 eqid ⊢ ( 𝐽 ↾t 𝑆 ) = ( 𝐽 ↾t 𝑆 )
12 eqid ⊢ ( 𝑧 ∈ ( 𝑋 ∖ { 𝐶 } ) ↦ ( ( ( 𝐹 ‘ 𝑧 ) − ( 𝐹 ‘ 𝐶 ) ) / ( 𝑧 − 𝐶 ) ) ) = ( 𝑧 ∈ ( 𝑋 ∖ { 𝐶 } ) ↦ ( ( ( 𝐹 ‘ 𝑧 ) − ( 𝐹 ‘ 𝐶 ) ) / ( 𝑧 − 𝐶 ) ) )
13 11 10 12 5 1 2 eldv ⊢ ( 𝜑 → ( 𝐶 ( 𝑆 D 𝐹 ) 𝐾 ↔ ( 𝐶 ∈ ( ( int ‘ ( 𝐽 ↾t 𝑆 ) ) ‘ 𝑋 ) ∧ 𝐾 ∈ ( ( 𝑧 ∈ ( 𝑋 ∖ { 𝐶 } ) ↦ ( ( ( 𝐹 ‘ 𝑧 ) − ( 𝐹 ‘ 𝐶 ) ) / ( 𝑧 − 𝐶 ) ) ) limℂ 𝐶 ) ) ) )
14 8 13 mpbid ⊢ ( 𝜑 → ( 𝐶 ∈ ( ( int ‘ ( 𝐽 ↾t 𝑆 ) ) ‘ 𝑋 ) ∧ 𝐾 ∈ ( ( 𝑧 ∈ ( 𝑋 ∖ { 𝐶 } ) ↦ ( ( ( 𝐹 ‘ 𝑧 ) − ( 𝐹 ‘ 𝐶 ) ) / ( 𝑧 − 𝐶 ) ) ) limℂ 𝐶 ) ) )
15 14 simpld ⊢ ( 𝜑 → 𝐶 ∈ ( ( int ‘ ( 𝐽 ↾t 𝑆 ) ) ‘ 𝑋 ) )
16 eqid ⊢ ( 𝑧 ∈ ( 𝑌 ∖ { 𝐶 } ) ↦ ( ( ( 𝐺 ‘ 𝑧 ) − ( 𝐺 ‘ 𝐶 ) ) / ( 𝑧 − 𝐶 ) ) ) = ( 𝑧 ∈ ( 𝑌 ∖ { 𝐶 } ) ↦ ( ( ( 𝐺 ‘ 𝑧 ) − ( 𝐺 ‘ 𝐶 ) ) / ( 𝑧 − 𝐶 ) ) )
17 11 10 16 5 3 4 eldv ⊢ ( 𝜑 → ( 𝐶 ( 𝑆 D 𝐺 ) 𝐿 ↔ ( 𝐶 ∈ ( ( int ‘ ( 𝐽 ↾t 𝑆 ) ) ‘ 𝑌 ) ∧ 𝐿 ∈ ( ( 𝑧 ∈ ( 𝑌 ∖ { 𝐶 } ) ↦ ( ( ( 𝐺 ‘ 𝑧 ) − ( 𝐺 ‘ 𝐶 ) ) / ( 𝑧 − 𝐶 ) ) ) limℂ 𝐶 ) ) ) )
18 9 17 mpbid ⊢ ( 𝜑 → ( 𝐶 ∈ ( ( int ‘ ( 𝐽 ↾t 𝑆 ) ) ‘ 𝑌 ) ∧ 𝐿 ∈ ( ( 𝑧 ∈ ( 𝑌 ∖ { 𝐶 } ) ↦ ( ( ( 𝐺 ‘ 𝑧 ) − ( 𝐺 ‘ 𝐶 ) ) / ( 𝑧 − 𝐶 ) ) ) limℂ 𝐶 ) ) )
19 18 simpld ⊢ ( 𝜑 → 𝐶 ∈ ( ( int ‘ ( 𝐽 ↾t 𝑆 ) ) ‘ 𝑌 ) )
20 15 19 elind ⊢ ( 𝜑 → 𝐶 ∈ ( ( ( int ‘ ( 𝐽 ↾t 𝑆 ) ) ‘ 𝑋 ) ∩ ( ( int ‘ ( 𝐽 ↾t 𝑆 ) ) ‘ 𝑌 ) ) )
21 10 cnfldtopon ⊢ 𝐽 ∈ ( TopOn ‘ ℂ )
22 resttopon ⊢ ( ( 𝐽 ∈ ( TopOn ‘ ℂ ) ∧ 𝑆 ⊆ ℂ ) → ( 𝐽 ↾t 𝑆 ) ∈ ( TopOn ‘ 𝑆 ) )
23 21 5 22 sylancr ⊢ ( 𝜑 → ( 𝐽 ↾t 𝑆 ) ∈ ( TopOn ‘ 𝑆 ) )
24 topontop ⊢ ( ( 𝐽 ↾t 𝑆 ) ∈ ( TopOn ‘ 𝑆 ) → ( 𝐽 ↾t 𝑆 ) ∈ Top )
25 23 24 syl ⊢ ( 𝜑 → ( 𝐽 ↾t 𝑆 ) ∈ Top )
26 toponuni ⊢ ( ( 𝐽 ↾t 𝑆 ) ∈ ( TopOn ‘ 𝑆 ) → 𝑆 = ∪ ( 𝐽 ↾t 𝑆 ) )
27 23 26 syl ⊢ ( 𝜑 → 𝑆 = ∪ ( 𝐽 ↾t 𝑆 ) )
28 2 27 sseqtrd ⊢ ( 𝜑 → 𝑋 ⊆ ∪ ( 𝐽 ↾t 𝑆 ) )
29 4 27 sseqtrd ⊢ ( 𝜑 → 𝑌 ⊆ ∪ ( 𝐽 ↾t 𝑆 ) )
30 eqid ⊢ ∪ ( 𝐽 ↾t 𝑆 ) = ∪ ( 𝐽 ↾t 𝑆 )
31 30 ntrin ⊢ ( ( ( 𝐽 ↾t 𝑆 ) ∈ Top ∧ 𝑋 ⊆ ∪ ( 𝐽 ↾t 𝑆 ) ∧ 𝑌 ⊆ ∪ ( 𝐽 ↾t 𝑆 ) ) → ( ( int ‘ ( 𝐽 ↾t 𝑆 ) ) ‘ ( 𝑋 ∩ 𝑌 ) ) = ( ( ( int ‘ ( 𝐽 ↾t 𝑆 ) ) ‘ 𝑋 ) ∩ ( ( int ‘ ( 𝐽 ↾t 𝑆 ) ) ‘ 𝑌 ) ) )
32 25 28 29 31 syl3anc ⊢ ( 𝜑 → ( ( int ‘ ( 𝐽 ↾t 𝑆 ) ) ‘ ( 𝑋 ∩ 𝑌 ) ) = ( ( ( int ‘ ( 𝐽 ↾t 𝑆 ) ) ‘ 𝑋 ) ∩ ( ( int ‘ ( 𝐽 ↾t 𝑆 ) ) ‘ 𝑌 ) ) )
33 20 32 eleqtrrd ⊢ ( 𝜑 → 𝐶 ∈ ( ( int ‘ ( 𝐽 ↾t 𝑆 ) ) ‘ ( 𝑋 ∩ 𝑌 ) ) )
34 inss1 ⊢ ( 𝑋 ∩ 𝑌 ) ⊆ 𝑋
35 ssdif ⊢ ( ( 𝑋 ∩ 𝑌 ) ⊆ 𝑋 → ( ( 𝑋 ∩ 𝑌 ) ∖ { 𝐶 } ) ⊆ ( 𝑋 ∖ { 𝐶 } ) )
36 34 35 mp1i ⊢ ( 𝜑 → ( ( 𝑋 ∩ 𝑌 ) ∖ { 𝐶 } ) ⊆ ( 𝑋 ∖ { 𝐶 } ) )
37 36 sselda ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( ( 𝑋 ∩ 𝑌 ) ∖ { 𝐶 } ) ) → 𝑧 ∈ ( 𝑋 ∖ { 𝐶 } ) )
38 2 5 sstrd ⊢ ( 𝜑 → 𝑋 ⊆ ℂ )
39 30 ntrss2 ⊢ ( ( ( 𝐽 ↾t 𝑆 ) ∈ Top ∧ 𝑋 ⊆ ∪ ( 𝐽 ↾t 𝑆 ) ) → ( ( int ‘ ( 𝐽 ↾t 𝑆 ) ) ‘ 𝑋 ) ⊆ 𝑋 )
40 25 28 39 syl2anc ⊢ ( 𝜑 → ( ( int ‘ ( 𝐽 ↾t 𝑆 ) ) ‘ 𝑋 ) ⊆ 𝑋 )
41 40 15 sseldd ⊢ ( 𝜑 → 𝐶 ∈ 𝑋 )
42 1 38 41 dvlem ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝑋 ∖ { 𝐶 } ) ) → ( ( ( 𝐹 ‘ 𝑧 ) − ( 𝐹 ‘ 𝐶 ) ) / ( 𝑧 − 𝐶 ) ) ∈ ℂ )
43 37 42 syldan ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( ( 𝑋 ∩ 𝑌 ) ∖ { 𝐶 } ) ) → ( ( ( 𝐹 ‘ 𝑧 ) − ( 𝐹 ‘ 𝐶 ) ) / ( 𝑧 − 𝐶 ) ) ∈ ℂ )
44 inss2 ⊢ ( 𝑋 ∩ 𝑌 ) ⊆ 𝑌
45 ssdif ⊢ ( ( 𝑋 ∩ 𝑌 ) ⊆ 𝑌 → ( ( 𝑋 ∩ 𝑌 ) ∖ { 𝐶 } ) ⊆ ( 𝑌 ∖ { 𝐶 } ) )
46 44 45 mp1i ⊢ ( 𝜑 → ( ( 𝑋 ∩ 𝑌 ) ∖ { 𝐶 } ) ⊆ ( 𝑌 ∖ { 𝐶 } ) )
47 46 sselda ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( ( 𝑋 ∩ 𝑌 ) ∖ { 𝐶 } ) ) → 𝑧 ∈ ( 𝑌 ∖ { 𝐶 } ) )
48 4 5 sstrd ⊢ ( 𝜑 → 𝑌 ⊆ ℂ )
49 30 ntrss2 ⊢ ( ( ( 𝐽 ↾t 𝑆 ) ∈ Top ∧ 𝑌 ⊆ ∪ ( 𝐽 ↾t 𝑆 ) ) → ( ( int ‘ ( 𝐽 ↾t 𝑆 ) ) ‘ 𝑌 ) ⊆ 𝑌 )
50 25 29 49 syl2anc ⊢ ( 𝜑 → ( ( int ‘ ( 𝐽 ↾t 𝑆 ) ) ‘ 𝑌 ) ⊆ 𝑌 )
51 50 19 sseldd ⊢ ( 𝜑 → 𝐶 ∈ 𝑌 )
52 3 48 51 dvlem ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝑌 ∖ { 𝐶 } ) ) → ( ( ( 𝐺 ‘ 𝑧 ) − ( 𝐺 ‘ 𝐶 ) ) / ( 𝑧 − 𝐶 ) ) ∈ ℂ )
53 47 52 syldan ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( ( 𝑋 ∩ 𝑌 ) ∖ { 𝐶 } ) ) → ( ( ( 𝐺 ‘ 𝑧 ) − ( 𝐺 ‘ 𝐶 ) ) / ( 𝑧 − 𝐶 ) ) ∈ ℂ )
54 ssidd ⊢ ( 𝜑 → ℂ ⊆ ℂ )
55 txtopon ⊢ ( ( 𝐽 ∈ ( TopOn ‘ ℂ ) ∧ 𝐽 ∈ ( TopOn ‘ ℂ ) ) → ( 𝐽 ×t 𝐽 ) ∈ ( TopOn ‘ ( ℂ × ℂ ) ) )
56 21 21 55 mp2an ⊢ ( 𝐽 ×t 𝐽 ) ∈ ( TopOn ‘ ( ℂ × ℂ ) )
57 56 toponrestid ⊢ ( 𝐽 ×t 𝐽 ) = ( ( 𝐽 ×t 𝐽 ) ↾t ( ℂ × ℂ ) )
58 14 simprd ⊢ ( 𝜑 → 𝐾 ∈ ( ( 𝑧 ∈ ( 𝑋 ∖ { 𝐶 } ) ↦ ( ( ( 𝐹 ‘ 𝑧 ) − ( 𝐹 ‘ 𝐶 ) ) / ( 𝑧 − 𝐶 ) ) ) limℂ 𝐶 ) )
59 42 fmpttd ⊢ ( 𝜑 → ( 𝑧 ∈ ( 𝑋 ∖ { 𝐶 } ) ↦ ( ( ( 𝐹 ‘ 𝑧 ) − ( 𝐹 ‘ 𝐶 ) ) / ( 𝑧 − 𝐶 ) ) ) : ( 𝑋 ∖ { 𝐶 } ) ⟶ ℂ )
60 38 ssdifssd ⊢ ( 𝜑 → ( 𝑋 ∖ { 𝐶 } ) ⊆ ℂ )
61 eqid ⊢ ( 𝐽 ↾t ( ( 𝑋 ∖ { 𝐶 } ) ∪ { 𝐶 } ) ) = ( 𝐽 ↾t ( ( 𝑋 ∖ { 𝐶 } ) ∪ { 𝐶 } ) )
62 34 2 sstrid ⊢ ( 𝜑 → ( 𝑋 ∩ 𝑌 ) ⊆ 𝑆 )
63 62 27 sseqtrd ⊢ ( 𝜑 → ( 𝑋 ∩ 𝑌 ) ⊆ ∪ ( 𝐽 ↾t 𝑆 ) )
64 difssd ⊢ ( 𝜑 → ( ∪ ( 𝐽 ↾t 𝑆 ) ∖ 𝑋 ) ⊆ ∪ ( 𝐽 ↾t 𝑆 ) )
65 63 64 unssd ⊢ ( 𝜑 → ( ( 𝑋 ∩ 𝑌 ) ∪ ( ∪ ( 𝐽 ↾t 𝑆 ) ∖ 𝑋 ) ) ⊆ ∪ ( 𝐽 ↾t 𝑆 ) )
66 ssun1 ⊢ ( 𝑋 ∩ 𝑌 ) ⊆ ( ( 𝑋 ∩ 𝑌 ) ∪ ( ∪ ( 𝐽 ↾t 𝑆 ) ∖ 𝑋 ) )
67 66 a1i ⊢ ( 𝜑 → ( 𝑋 ∩ 𝑌 ) ⊆ ( ( 𝑋 ∩ 𝑌 ) ∪ ( ∪ ( 𝐽 ↾t 𝑆 ) ∖ 𝑋 ) ) )
68 30 ntrss ⊢ ( ( ( 𝐽 ↾t 𝑆 ) ∈ Top ∧ ( ( 𝑋 ∩ 𝑌 ) ∪ ( ∪ ( 𝐽 ↾t 𝑆 ) ∖ 𝑋 ) ) ⊆ ∪ ( 𝐽 ↾t 𝑆 ) ∧ ( 𝑋 ∩ 𝑌 ) ⊆ ( ( 𝑋 ∩ 𝑌 ) ∪ ( ∪ ( 𝐽 ↾t 𝑆 ) ∖ 𝑋 ) ) ) → ( ( int ‘ ( 𝐽 ↾t 𝑆 ) ) ‘ ( 𝑋 ∩ 𝑌 ) ) ⊆ ( ( int ‘ ( 𝐽 ↾t 𝑆 ) ) ‘ ( ( 𝑋 ∩ 𝑌 ) ∪ ( ∪ ( 𝐽 ↾t 𝑆 ) ∖ 𝑋 ) ) ) )
69 25 65 67 68 syl3anc ⊢ ( 𝜑 → ( ( int ‘ ( 𝐽 ↾t 𝑆 ) ) ‘ ( 𝑋 ∩ 𝑌 ) ) ⊆ ( ( int ‘ ( 𝐽 ↾t 𝑆 ) ) ‘ ( ( 𝑋 ∩ 𝑌 ) ∪ ( ∪ ( 𝐽 ↾t 𝑆 ) ∖ 𝑋 ) ) ) )
70 69 33 sseldd ⊢ ( 𝜑 → 𝐶 ∈ ( ( int ‘ ( 𝐽 ↾t 𝑆 ) ) ‘ ( ( 𝑋 ∩ 𝑌 ) ∪ ( ∪ ( 𝐽 ↾t 𝑆 ) ∖ 𝑋 ) ) ) )
71 70 41 elind ⊢ ( 𝜑 → 𝐶 ∈ ( ( ( int ‘ ( 𝐽 ↾t 𝑆 ) ) ‘ ( ( 𝑋 ∩ 𝑌 ) ∪ ( ∪ ( 𝐽 ↾t 𝑆 ) ∖ 𝑋 ) ) ) ∩ 𝑋 ) )
72 34 a1i ⊢ ( 𝜑 → ( 𝑋 ∩ 𝑌 ) ⊆ 𝑋 )
73 eqid ⊢ ( ( 𝐽 ↾t 𝑆 ) ↾t 𝑋 ) = ( ( 𝐽 ↾t 𝑆 ) ↾t 𝑋 )
74 30 73 restntr ⊢ ( ( ( 𝐽 ↾t 𝑆 ) ∈ Top ∧ 𝑋 ⊆ ∪ ( 𝐽 ↾t 𝑆 ) ∧ ( 𝑋 ∩ 𝑌 ) ⊆ 𝑋 ) → ( ( int ‘ ( ( 𝐽 ↾t 𝑆 ) ↾t 𝑋 ) ) ‘ ( 𝑋 ∩ 𝑌 ) ) = ( ( ( int ‘ ( 𝐽 ↾t 𝑆 ) ) ‘ ( ( 𝑋 ∩ 𝑌 ) ∪ ( ∪ ( 𝐽 ↾t 𝑆 ) ∖ 𝑋 ) ) ) ∩ 𝑋 ) )
75 25 28 72 74 syl3anc ⊢ ( 𝜑 → ( ( int ‘ ( ( 𝐽 ↾t 𝑆 ) ↾t 𝑋 ) ) ‘ ( 𝑋 ∩ 𝑌 ) ) = ( ( ( int ‘ ( 𝐽 ↾t 𝑆 ) ) ‘ ( ( 𝑋 ∩ 𝑌 ) ∪ ( ∪ ( 𝐽 ↾t 𝑆 ) ∖ 𝑋 ) ) ) ∩ 𝑋 ) )
76 10 cnfldtop ⊢ 𝐽 ∈ Top
77 76 a1i ⊢ ( 𝜑 → 𝐽 ∈ Top )
78 cnex ⊢ ℂ ∈ V
79 ssexg ⊢ ( ( 𝑆 ⊆ ℂ ∧ ℂ ∈ V ) → 𝑆 ∈ V )
80 5 78 79 sylancl ⊢ ( 𝜑 → 𝑆 ∈ V )
81 restabs ⊢ ( ( 𝐽 ∈ Top ∧ 𝑋 ⊆ 𝑆 ∧ 𝑆 ∈ V ) → ( ( 𝐽 ↾t 𝑆 ) ↾t 𝑋 ) = ( 𝐽 ↾t 𝑋 ) )
82 77 2 80 81 syl3anc ⊢ ( 𝜑 → ( ( 𝐽 ↾t 𝑆 ) ↾t 𝑋 ) = ( 𝐽 ↾t 𝑋 ) )
83 82 fveq2d ⊢ ( 𝜑 → ( int ‘ ( ( 𝐽 ↾t 𝑆 ) ↾t 𝑋 ) ) = ( int ‘ ( 𝐽 ↾t 𝑋 ) ) )
84 83 fveq1d ⊢ ( 𝜑 → ( ( int ‘ ( ( 𝐽 ↾t 𝑆 ) ↾t 𝑋 ) ) ‘ ( 𝑋 ∩ 𝑌 ) ) = ( ( int ‘ ( 𝐽 ↾t 𝑋 ) ) ‘ ( 𝑋 ∩ 𝑌 ) ) )
85 75 84 eqtr3d ⊢ ( 𝜑 → ( ( ( int ‘ ( 𝐽 ↾t 𝑆 ) ) ‘ ( ( 𝑋 ∩ 𝑌 ) ∪ ( ∪ ( 𝐽 ↾t 𝑆 ) ∖ 𝑋 ) ) ) ∩ 𝑋 ) = ( ( int ‘ ( 𝐽 ↾t 𝑋 ) ) ‘ ( 𝑋 ∩ 𝑌 ) ) )
86 71 85 eleqtrd ⊢ ( 𝜑 → 𝐶 ∈ ( ( int ‘ ( 𝐽 ↾t 𝑋 ) ) ‘ ( 𝑋 ∩ 𝑌 ) ) )
87 undif1 ⊢ ( ( 𝑋 ∖ { 𝐶 } ) ∪ { 𝐶 } ) = ( 𝑋 ∪ { 𝐶 } )
88 41 snssd ⊢ ( 𝜑 → { 𝐶 } ⊆ 𝑋 )
89 ssequn2 ⊢ ( { 𝐶 } ⊆ 𝑋 ↔ ( 𝑋 ∪ { 𝐶 } ) = 𝑋 )
90 88 89 sylib ⊢ ( 𝜑 → ( 𝑋 ∪ { 𝐶 } ) = 𝑋 )
91 87 90 eqtrid ⊢ ( 𝜑 → ( ( 𝑋 ∖ { 𝐶 } ) ∪ { 𝐶 } ) = 𝑋 )
92 91 oveq2d ⊢ ( 𝜑 → ( 𝐽 ↾t ( ( 𝑋 ∖ { 𝐶 } ) ∪ { 𝐶 } ) ) = ( 𝐽 ↾t 𝑋 ) )
93 92 fveq2d ⊢ ( 𝜑 → ( int ‘ ( 𝐽 ↾t ( ( 𝑋 ∖ { 𝐶 } ) ∪ { 𝐶 } ) ) ) = ( int ‘ ( 𝐽 ↾t 𝑋 ) ) )
94 undif1 ⊢ ( ( ( 𝑋 ∩ 𝑌 ) ∖ { 𝐶 } ) ∪ { 𝐶 } ) = ( ( 𝑋 ∩ 𝑌 ) ∪ { 𝐶 } )
95 41 51 elind ⊢ ( 𝜑 → 𝐶 ∈ ( 𝑋 ∩ 𝑌 ) )
96 95 snssd ⊢ ( 𝜑 → { 𝐶 } ⊆ ( 𝑋 ∩ 𝑌 ) )
97 ssequn2 ⊢ ( { 𝐶 } ⊆ ( 𝑋 ∩ 𝑌 ) ↔ ( ( 𝑋 ∩ 𝑌 ) ∪ { 𝐶 } ) = ( 𝑋 ∩ 𝑌 ) )
98 96 97 sylib ⊢ ( 𝜑 → ( ( 𝑋 ∩ 𝑌 ) ∪ { 𝐶 } ) = ( 𝑋 ∩ 𝑌 ) )
99 94 98 eqtrid ⊢ ( 𝜑 → ( ( ( 𝑋 ∩ 𝑌 ) ∖ { 𝐶 } ) ∪ { 𝐶 } ) = ( 𝑋 ∩ 𝑌 ) )
100 93 99 fveq12d ⊢ ( 𝜑 → ( ( int ‘ ( 𝐽 ↾t ( ( 𝑋 ∖ { 𝐶 } ) ∪ { 𝐶 } ) ) ) ‘ ( ( ( 𝑋 ∩ 𝑌 ) ∖ { 𝐶 } ) ∪ { 𝐶 } ) ) = ( ( int ‘ ( 𝐽 ↾t 𝑋 ) ) ‘ ( 𝑋 ∩ 𝑌 ) ) )
101 86 100 eleqtrrd ⊢ ( 𝜑 → 𝐶 ∈ ( ( int ‘ ( 𝐽 ↾t ( ( 𝑋 ∖ { 𝐶 } ) ∪ { 𝐶 } ) ) ) ‘ ( ( ( 𝑋 ∩ 𝑌 ) ∖ { 𝐶 } ) ∪ { 𝐶 } ) ) )
102 59 36 60 10 61 101 limcres ⊢ ( 𝜑 → ( ( ( 𝑧 ∈ ( 𝑋 ∖ { 𝐶 } ) ↦ ( ( ( 𝐹 ‘ 𝑧 ) − ( 𝐹 ‘ 𝐶 ) ) / ( 𝑧 − 𝐶 ) ) ) ↾ ( ( 𝑋 ∩ 𝑌 ) ∖ { 𝐶 } ) ) limℂ 𝐶 ) = ( ( 𝑧 ∈ ( 𝑋 ∖ { 𝐶 } ) ↦ ( ( ( 𝐹 ‘ 𝑧 ) − ( 𝐹 ‘ 𝐶 ) ) / ( 𝑧 − 𝐶 ) ) ) limℂ 𝐶 ) )
103 36 resmptd ⊢ ( 𝜑 → ( ( 𝑧 ∈ ( 𝑋 ∖ { 𝐶 } ) ↦ ( ( ( 𝐹 ‘ 𝑧 ) − ( 𝐹 ‘ 𝐶 ) ) / ( 𝑧 − 𝐶 ) ) ) ↾ ( ( 𝑋 ∩ 𝑌 ) ∖ { 𝐶 } ) ) = ( 𝑧 ∈ ( ( 𝑋 ∩ 𝑌 ) ∖ { 𝐶 } ) ↦ ( ( ( 𝐹 ‘ 𝑧 ) − ( 𝐹 ‘ 𝐶 ) ) / ( 𝑧 − 𝐶 ) ) ) )
104 103 oveq1d ⊢ ( 𝜑 → ( ( ( 𝑧 ∈ ( 𝑋 ∖ { 𝐶 } ) ↦ ( ( ( 𝐹 ‘ 𝑧 ) − ( 𝐹 ‘ 𝐶 ) ) / ( 𝑧 − 𝐶 ) ) ) ↾ ( ( 𝑋 ∩ 𝑌 ) ∖ { 𝐶 } ) ) limℂ 𝐶 ) = ( ( 𝑧 ∈ ( ( 𝑋 ∩ 𝑌 ) ∖ { 𝐶 } ) ↦ ( ( ( 𝐹 ‘ 𝑧 ) − ( 𝐹 ‘ 𝐶 ) ) / ( 𝑧 − 𝐶 ) ) ) limℂ 𝐶 ) )
105 102 104 eqtr3d ⊢ ( 𝜑 → ( ( 𝑧 ∈ ( 𝑋 ∖ { 𝐶 } ) ↦ ( ( ( 𝐹 ‘ 𝑧 ) − ( 𝐹 ‘ 𝐶 ) ) / ( 𝑧 − 𝐶 ) ) ) limℂ 𝐶 ) = ( ( 𝑧 ∈ ( ( 𝑋 ∩ 𝑌 ) ∖ { 𝐶 } ) ↦ ( ( ( 𝐹 ‘ 𝑧 ) − ( 𝐹 ‘ 𝐶 ) ) / ( 𝑧 − 𝐶 ) ) ) limℂ 𝐶 ) )
106 58 105 eleqtrd ⊢ ( 𝜑 → 𝐾 ∈ ( ( 𝑧 ∈ ( ( 𝑋 ∩ 𝑌 ) ∖ { 𝐶 } ) ↦ ( ( ( 𝐹 ‘ 𝑧 ) − ( 𝐹 ‘ 𝐶 ) ) / ( 𝑧 − 𝐶 ) ) ) limℂ 𝐶 ) )
107 18 simprd ⊢ ( 𝜑 → 𝐿 ∈ ( ( 𝑧 ∈ ( 𝑌 ∖ { 𝐶 } ) ↦ ( ( ( 𝐺 ‘ 𝑧 ) − ( 𝐺 ‘ 𝐶 ) ) / ( 𝑧 − 𝐶 ) ) ) limℂ 𝐶 ) )
108 52 fmpttd ⊢ ( 𝜑 → ( 𝑧 ∈ ( 𝑌 ∖ { 𝐶 } ) ↦ ( ( ( 𝐺 ‘ 𝑧 ) − ( 𝐺 ‘ 𝐶 ) ) / ( 𝑧 − 𝐶 ) ) ) : ( 𝑌 ∖ { 𝐶 } ) ⟶ ℂ )
109 48 ssdifssd ⊢ ( 𝜑 → ( 𝑌 ∖ { 𝐶 } ) ⊆ ℂ )
110 eqid ⊢ ( 𝐽 ↾t ( ( 𝑌 ∖ { 𝐶 } ) ∪ { 𝐶 } ) ) = ( 𝐽 ↾t ( ( 𝑌 ∖ { 𝐶 } ) ∪ { 𝐶 } ) )
111 difssd ⊢ ( 𝜑 → ( ∪ ( 𝐽 ↾t 𝑆 ) ∖ 𝑌 ) ⊆ ∪ ( 𝐽 ↾t 𝑆 ) )
112 63 111 unssd ⊢ ( 𝜑 → ( ( 𝑋 ∩ 𝑌 ) ∪ ( ∪ ( 𝐽 ↾t 𝑆 ) ∖ 𝑌 ) ) ⊆ ∪ ( 𝐽 ↾t 𝑆 ) )
113 ssun1 ⊢ ( 𝑋 ∩ 𝑌 ) ⊆ ( ( 𝑋 ∩ 𝑌 ) ∪ ( ∪ ( 𝐽 ↾t 𝑆 ) ∖ 𝑌 ) )
114 113 a1i ⊢ ( 𝜑 → ( 𝑋 ∩ 𝑌 ) ⊆ ( ( 𝑋 ∩ 𝑌 ) ∪ ( ∪ ( 𝐽 ↾t 𝑆 ) ∖ 𝑌 ) ) )
115 30 ntrss ⊢ ( ( ( 𝐽 ↾t 𝑆 ) ∈ Top ∧ ( ( 𝑋 ∩ 𝑌 ) ∪ ( ∪ ( 𝐽 ↾t 𝑆 ) ∖ 𝑌 ) ) ⊆ ∪ ( 𝐽 ↾t 𝑆 ) ∧ ( 𝑋 ∩ 𝑌 ) ⊆ ( ( 𝑋 ∩ 𝑌 ) ∪ ( ∪ ( 𝐽 ↾t 𝑆 ) ∖ 𝑌 ) ) ) → ( ( int ‘ ( 𝐽 ↾t 𝑆 ) ) ‘ ( 𝑋 ∩ 𝑌 ) ) ⊆ ( ( int ‘ ( 𝐽 ↾t 𝑆 ) ) ‘ ( ( 𝑋 ∩ 𝑌 ) ∪ ( ∪ ( 𝐽 ↾t 𝑆 ) ∖ 𝑌 ) ) ) )
116 25 112 114 115 syl3anc ⊢ ( 𝜑 → ( ( int ‘ ( 𝐽 ↾t 𝑆 ) ) ‘ ( 𝑋 ∩ 𝑌 ) ) ⊆ ( ( int ‘ ( 𝐽 ↾t 𝑆 ) ) ‘ ( ( 𝑋 ∩ 𝑌 ) ∪ ( ∪ ( 𝐽 ↾t 𝑆 ) ∖ 𝑌 ) ) ) )
117 116 33 sseldd ⊢ ( 𝜑 → 𝐶 ∈ ( ( int ‘ ( 𝐽 ↾t 𝑆 ) ) ‘ ( ( 𝑋 ∩ 𝑌 ) ∪ ( ∪ ( 𝐽 ↾t 𝑆 ) ∖ 𝑌 ) ) ) )
118 117 51 elind ⊢ ( 𝜑 → 𝐶 ∈ ( ( ( int ‘ ( 𝐽 ↾t 𝑆 ) ) ‘ ( ( 𝑋 ∩ 𝑌 ) ∪ ( ∪ ( 𝐽 ↾t 𝑆 ) ∖ 𝑌 ) ) ) ∩ 𝑌 ) )
119 44 a1i ⊢ ( 𝜑 → ( 𝑋 ∩ 𝑌 ) ⊆ 𝑌 )
120 eqid ⊢ ( ( 𝐽 ↾t 𝑆 ) ↾t 𝑌 ) = ( ( 𝐽 ↾t 𝑆 ) ↾t 𝑌 )
121 30 120 restntr ⊢ ( ( ( 𝐽 ↾t 𝑆 ) ∈ Top ∧ 𝑌 ⊆ ∪ ( 𝐽 ↾t 𝑆 ) ∧ ( 𝑋 ∩ 𝑌 ) ⊆ 𝑌 ) → ( ( int ‘ ( ( 𝐽 ↾t 𝑆 ) ↾t 𝑌 ) ) ‘ ( 𝑋 ∩ 𝑌 ) ) = ( ( ( int ‘ ( 𝐽 ↾t 𝑆 ) ) ‘ ( ( 𝑋 ∩ 𝑌 ) ∪ ( ∪ ( 𝐽 ↾t 𝑆 ) ∖ 𝑌 ) ) ) ∩ 𝑌 ) )
122 25 29 119 121 syl3anc ⊢ ( 𝜑 → ( ( int ‘ ( ( 𝐽 ↾t 𝑆 ) ↾t 𝑌 ) ) ‘ ( 𝑋 ∩ 𝑌 ) ) = ( ( ( int ‘ ( 𝐽 ↾t 𝑆 ) ) ‘ ( ( 𝑋 ∩ 𝑌 ) ∪ ( ∪ ( 𝐽 ↾t 𝑆 ) ∖ 𝑌 ) ) ) ∩ 𝑌 ) )
123 restabs ⊢ ( ( 𝐽 ∈ Top ∧ 𝑌 ⊆ 𝑆 ∧ 𝑆 ∈ V ) → ( ( 𝐽 ↾t 𝑆 ) ↾t 𝑌 ) = ( 𝐽 ↾t 𝑌 ) )
124 77 4 80 123 syl3anc ⊢ ( 𝜑 → ( ( 𝐽 ↾t 𝑆 ) ↾t 𝑌 ) = ( 𝐽 ↾t 𝑌 ) )
125 124 fveq2d ⊢ ( 𝜑 → ( int ‘ ( ( 𝐽 ↾t 𝑆 ) ↾t 𝑌 ) ) = ( int ‘ ( 𝐽 ↾t 𝑌 ) ) )
126 125 fveq1d ⊢ ( 𝜑 → ( ( int ‘ ( ( 𝐽 ↾t 𝑆 ) ↾t 𝑌 ) ) ‘ ( 𝑋 ∩ 𝑌 ) ) = ( ( int ‘ ( 𝐽 ↾t 𝑌 ) ) ‘ ( 𝑋 ∩ 𝑌 ) ) )
127 122 126 eqtr3d ⊢ ( 𝜑 → ( ( ( int ‘ ( 𝐽 ↾t 𝑆 ) ) ‘ ( ( 𝑋 ∩ 𝑌 ) ∪ ( ∪ ( 𝐽 ↾t 𝑆 ) ∖ 𝑌 ) ) ) ∩ 𝑌 ) = ( ( int ‘ ( 𝐽 ↾t 𝑌 ) ) ‘ ( 𝑋 ∩ 𝑌 ) ) )
128 118 127 eleqtrd ⊢ ( 𝜑 → 𝐶 ∈ ( ( int ‘ ( 𝐽 ↾t 𝑌 ) ) ‘ ( 𝑋 ∩ 𝑌 ) ) )
129 undif1 ⊢ ( ( 𝑌 ∖ { 𝐶 } ) ∪ { 𝐶 } ) = ( 𝑌 ∪ { 𝐶 } )
130 51 snssd ⊢ ( 𝜑 → { 𝐶 } ⊆ 𝑌 )
131 ssequn2 ⊢ ( { 𝐶 } ⊆ 𝑌 ↔ ( 𝑌 ∪ { 𝐶 } ) = 𝑌 )
132 130 131 sylib ⊢ ( 𝜑 → ( 𝑌 ∪ { 𝐶 } ) = 𝑌 )
133 129 132 eqtrid ⊢ ( 𝜑 → ( ( 𝑌 ∖ { 𝐶 } ) ∪ { 𝐶 } ) = 𝑌 )
134 133 oveq2d ⊢ ( 𝜑 → ( 𝐽 ↾t ( ( 𝑌 ∖ { 𝐶 } ) ∪ { 𝐶 } ) ) = ( 𝐽 ↾t 𝑌 ) )
135 134 fveq2d ⊢ ( 𝜑 → ( int ‘ ( 𝐽 ↾t ( ( 𝑌 ∖ { 𝐶 } ) ∪ { 𝐶 } ) ) ) = ( int ‘ ( 𝐽 ↾t 𝑌 ) ) )
136 135 99 fveq12d ⊢ ( 𝜑 → ( ( int ‘ ( 𝐽 ↾t ( ( 𝑌 ∖ { 𝐶 } ) ∪ { 𝐶 } ) ) ) ‘ ( ( ( 𝑋 ∩ 𝑌 ) ∖ { 𝐶 } ) ∪ { 𝐶 } ) ) = ( ( int ‘ ( 𝐽 ↾t 𝑌 ) ) ‘ ( 𝑋 ∩ 𝑌 ) ) )
137 128 136 eleqtrrd ⊢ ( 𝜑 → 𝐶 ∈ ( ( int ‘ ( 𝐽 ↾t ( ( 𝑌 ∖ { 𝐶 } ) ∪ { 𝐶 } ) ) ) ‘ ( ( ( 𝑋 ∩ 𝑌 ) ∖ { 𝐶 } ) ∪ { 𝐶 } ) ) )
138 108 46 109 10 110 137 limcres ⊢ ( 𝜑 → ( ( ( 𝑧 ∈ ( 𝑌 ∖ { 𝐶 } ) ↦ ( ( ( 𝐺 ‘ 𝑧 ) − ( 𝐺 ‘ 𝐶 ) ) / ( 𝑧 − 𝐶 ) ) ) ↾ ( ( 𝑋 ∩ 𝑌 ) ∖ { 𝐶 } ) ) limℂ 𝐶 ) = ( ( 𝑧 ∈ ( 𝑌 ∖ { 𝐶 } ) ↦ ( ( ( 𝐺 ‘ 𝑧 ) − ( 𝐺 ‘ 𝐶 ) ) / ( 𝑧 − 𝐶 ) ) ) limℂ 𝐶 ) )
139 46 resmptd ⊢ ( 𝜑 → ( ( 𝑧 ∈ ( 𝑌 ∖ { 𝐶 } ) ↦ ( ( ( 𝐺 ‘ 𝑧 ) − ( 𝐺 ‘ 𝐶 ) ) / ( 𝑧 − 𝐶 ) ) ) ↾ ( ( 𝑋 ∩ 𝑌 ) ∖ { 𝐶 } ) ) = ( 𝑧 ∈ ( ( 𝑋 ∩ 𝑌 ) ∖ { 𝐶 } ) ↦ ( ( ( 𝐺 ‘ 𝑧 ) − ( 𝐺 ‘ 𝐶 ) ) / ( 𝑧 − 𝐶 ) ) ) )
140 139 oveq1d ⊢ ( 𝜑 → ( ( ( 𝑧 ∈ ( 𝑌 ∖ { 𝐶 } ) ↦ ( ( ( 𝐺 ‘ 𝑧 ) − ( 𝐺 ‘ 𝐶 ) ) / ( 𝑧 − 𝐶 ) ) ) ↾ ( ( 𝑋 ∩ 𝑌 ) ∖ { 𝐶 } ) ) limℂ 𝐶 ) = ( ( 𝑧 ∈ ( ( 𝑋 ∩ 𝑌 ) ∖ { 𝐶 } ) ↦ ( ( ( 𝐺 ‘ 𝑧 ) − ( 𝐺 ‘ 𝐶 ) ) / ( 𝑧 − 𝐶 ) ) ) limℂ 𝐶 ) )
141 138 140 eqtr3d ⊢ ( 𝜑 → ( ( 𝑧 ∈ ( 𝑌 ∖ { 𝐶 } ) ↦ ( ( ( 𝐺 ‘ 𝑧 ) − ( 𝐺 ‘ 𝐶 ) ) / ( 𝑧 − 𝐶 ) ) ) limℂ 𝐶 ) = ( ( 𝑧 ∈ ( ( 𝑋 ∩ 𝑌 ) ∖ { 𝐶 } ) ↦ ( ( ( 𝐺 ‘ 𝑧 ) − ( 𝐺 ‘ 𝐶 ) ) / ( 𝑧 − 𝐶 ) ) ) limℂ 𝐶 ) )
142 107 141 eleqtrd ⊢ ( 𝜑 → 𝐿 ∈ ( ( 𝑧 ∈ ( ( 𝑋 ∩ 𝑌 ) ∖ { 𝐶 } ) ↦ ( ( ( 𝐺 ‘ 𝑧 ) − ( 𝐺 ‘ 𝐶 ) ) / ( 𝑧 − 𝐶 ) ) ) limℂ 𝐶 ) )
143 10 addcn ⊢ + ∈ ( ( 𝐽 ×t 𝐽 ) Cn 𝐽 )
144 5 1 2 dvcl ⊢ ( ( 𝜑 ∧ 𝐶 ( 𝑆 D 𝐹 ) 𝐾 ) → 𝐾 ∈ ℂ )
145 8 144 mpdan ⊢ ( 𝜑 → 𝐾 ∈ ℂ )
146 5 3 4 dvcl ⊢ ( ( 𝜑 ∧ 𝐶 ( 𝑆 D 𝐺 ) 𝐿 ) → 𝐿 ∈ ℂ )
147 9 146 mpdan ⊢ ( 𝜑 → 𝐿 ∈ ℂ )
148 145 147 opelxpd ⊢ ( 𝜑 → ⟨ 𝐾 , 𝐿 ⟩ ∈ ( ℂ × ℂ ) )
149 56 toponunii ⊢ ( ℂ × ℂ ) = ∪ ( 𝐽 ×t 𝐽 )
150 149 cncnpi ⊢ ( ( + ∈ ( ( 𝐽 ×t 𝐽 ) Cn 𝐽 ) ∧ ⟨ 𝐾 , 𝐿 ⟩ ∈ ( ℂ × ℂ ) ) → + ∈ ( ( ( 𝐽 ×t 𝐽 ) CnP 𝐽 ) ‘ ⟨ 𝐾 , 𝐿 ⟩ ) )
151 143 148 150 sylancr ⊢ ( 𝜑 → + ∈ ( ( ( 𝐽 ×t 𝐽 ) CnP 𝐽 ) ‘ ⟨ 𝐾 , 𝐿 ⟩ ) )
152 43 53 54 54 10 57 106 142 151 limccnp2 ⊢ ( 𝜑 → ( 𝐾 + 𝐿 ) ∈ ( ( 𝑧 ∈ ( ( 𝑋 ∩ 𝑌 ) ∖ { 𝐶 } ) ↦ ( ( ( ( 𝐹 ‘ 𝑧 ) − ( 𝐹 ‘ 𝐶 ) ) / ( 𝑧 − 𝐶 ) ) + ( ( ( 𝐺 ‘ 𝑧 ) − ( 𝐺 ‘ 𝐶 ) ) / ( 𝑧 − 𝐶 ) ) ) ) limℂ 𝐶 ) )
153 eldifi ⊢ ( 𝑧 ∈ ( ( 𝑋 ∩ 𝑌 ) ∖ { 𝐶 } ) → 𝑧 ∈ ( 𝑋 ∩ 𝑌 ) )
154 153 adantl ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( ( 𝑋 ∩ 𝑌 ) ∖ { 𝐶 } ) ) → 𝑧 ∈ ( 𝑋 ∩ 𝑌 ) )
155 1 ffnd ⊢ ( 𝜑 → 𝐹 Fn 𝑋 )
156 155 adantr ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( ( 𝑋 ∩ 𝑌 ) ∖ { 𝐶 } ) ) → 𝐹 Fn 𝑋 )
157 3 ffnd ⊢ ( 𝜑 → 𝐺 Fn 𝑌 )
158 157 adantr ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( ( 𝑋 ∩ 𝑌 ) ∖ { 𝐶 } ) ) → 𝐺 Fn 𝑌 )
159 ssexg ⊢ ( ( 𝑋 ⊆ ℂ ∧ ℂ ∈ V ) → 𝑋 ∈ V )
160 38 78 159 sylancl ⊢ ( 𝜑 → 𝑋 ∈ V )
161 160 adantr ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( ( 𝑋 ∩ 𝑌 ) ∖ { 𝐶 } ) ) → 𝑋 ∈ V )
162 ssexg ⊢ ( ( 𝑌 ⊆ ℂ ∧ ℂ ∈ V ) → 𝑌 ∈ V )
163 48 78 162 sylancl ⊢ ( 𝜑 → 𝑌 ∈ V )
164 163 adantr ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( ( 𝑋 ∩ 𝑌 ) ∖ { 𝐶 } ) ) → 𝑌 ∈ V )
165 eqid ⊢ ( 𝑋 ∩ 𝑌 ) = ( 𝑋 ∩ 𝑌 )
166 eqidd ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ( ( 𝑋 ∩ 𝑌 ) ∖ { 𝐶 } ) ) ∧ 𝑧 ∈ 𝑋 ) → ( 𝐹 ‘ 𝑧 ) = ( 𝐹 ‘ 𝑧 ) )
167 eqidd ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ( ( 𝑋 ∩ 𝑌 ) ∖ { 𝐶 } ) ) ∧ 𝑧 ∈ 𝑌 ) → ( 𝐺 ‘ 𝑧 ) = ( 𝐺 ‘ 𝑧 ) )
168 156 158 161 164 165 166 167 ofval ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ( ( 𝑋 ∩ 𝑌 ) ∖ { 𝐶 } ) ) ∧ 𝑧 ∈ ( 𝑋 ∩ 𝑌 ) ) → ( ( 𝐹 ∘f + 𝐺 ) ‘ 𝑧 ) = ( ( 𝐹 ‘ 𝑧 ) + ( 𝐺 ‘ 𝑧 ) ) )
169 154 168 mpdan ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( ( 𝑋 ∩ 𝑌 ) ∖ { 𝐶 } ) ) → ( ( 𝐹 ∘f + 𝐺 ) ‘ 𝑧 ) = ( ( 𝐹 ‘ 𝑧 ) + ( 𝐺 ‘ 𝑧 ) ) )
170 eqidd ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ( ( 𝑋 ∩ 𝑌 ) ∖ { 𝐶 } ) ) ∧ 𝐶 ∈ 𝑋 ) → ( 𝐹 ‘ 𝐶 ) = ( 𝐹 ‘ 𝐶 ) )
171 eqidd ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ( ( 𝑋 ∩ 𝑌 ) ∖ { 𝐶 } ) ) ∧ 𝐶 ∈ 𝑌 ) → ( 𝐺 ‘ 𝐶 ) = ( 𝐺 ‘ 𝐶 ) )
172 156 158 161 164 165 170 171 ofval ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ( ( 𝑋 ∩ 𝑌 ) ∖ { 𝐶 } ) ) ∧ 𝐶 ∈ ( 𝑋 ∩ 𝑌 ) ) → ( ( 𝐹 ∘f + 𝐺 ) ‘ 𝐶 ) = ( ( 𝐹 ‘ 𝐶 ) + ( 𝐺 ‘ 𝐶 ) ) )
173 95 172 mpidan ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( ( 𝑋 ∩ 𝑌 ) ∖ { 𝐶 } ) ) → ( ( 𝐹 ∘f + 𝐺 ) ‘ 𝐶 ) = ( ( 𝐹 ‘ 𝐶 ) + ( 𝐺 ‘ 𝐶 ) ) )
174 169 173 oveq12d ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( ( 𝑋 ∩ 𝑌 ) ∖ { 𝐶 } ) ) → ( ( ( 𝐹 ∘f + 𝐺 ) ‘ 𝑧 ) − ( ( 𝐹 ∘f + 𝐺 ) ‘ 𝐶 ) ) = ( ( ( 𝐹 ‘ 𝑧 ) + ( 𝐺 ‘ 𝑧 ) ) − ( ( 𝐹 ‘ 𝐶 ) + ( 𝐺 ‘ 𝐶 ) ) ) )
175 difss ⊢ ( ( 𝑋 ∩ 𝑌 ) ∖ { 𝐶 } ) ⊆ ( 𝑋 ∩ 𝑌 )
176 175 34 sstri ⊢ ( ( 𝑋 ∩ 𝑌 ) ∖ { 𝐶 } ) ⊆ 𝑋
177 176 sseli ⊢ ( 𝑧 ∈ ( ( 𝑋 ∩ 𝑌 ) ∖ { 𝐶 } ) → 𝑧 ∈ 𝑋 )
178 ffvelrn ⊢ ( ( 𝐹 : 𝑋 ⟶ ℂ ∧ 𝑧 ∈ 𝑋 ) → ( 𝐹 ‘ 𝑧 ) ∈ ℂ )
179 1 177 178 syl2an ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( ( 𝑋 ∩ 𝑌 ) ∖ { 𝐶 } ) ) → ( 𝐹 ‘ 𝑧 ) ∈ ℂ )
180 175 44 sstri ⊢ ( ( 𝑋 ∩ 𝑌 ) ∖ { 𝐶 } ) ⊆ 𝑌
181 180 sseli ⊢ ( 𝑧 ∈ ( ( 𝑋 ∩ 𝑌 ) ∖ { 𝐶 } ) → 𝑧 ∈ 𝑌 )
182 ffvelrn ⊢ ( ( 𝐺 : 𝑌 ⟶ ℂ ∧ 𝑧 ∈ 𝑌 ) → ( 𝐺 ‘ 𝑧 ) ∈ ℂ )
183 3 181 182 syl2an ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( ( 𝑋 ∩ 𝑌 ) ∖ { 𝐶 } ) ) → ( 𝐺 ‘ 𝑧 ) ∈ ℂ )
184 1 41 ffvelrnd ⊢ ( 𝜑 → ( 𝐹 ‘ 𝐶 ) ∈ ℂ )
185 184 adantr ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( ( 𝑋 ∩ 𝑌 ) ∖ { 𝐶 } ) ) → ( 𝐹 ‘ 𝐶 ) ∈ ℂ )
186 3 51 ffvelrnd ⊢ ( 𝜑 → ( 𝐺 ‘ 𝐶 ) ∈ ℂ )
187 186 adantr ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( ( 𝑋 ∩ 𝑌 ) ∖ { 𝐶 } ) ) → ( 𝐺 ‘ 𝐶 ) ∈ ℂ )
188 179 183 185 187 addsub4d ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( ( 𝑋 ∩ 𝑌 ) ∖ { 𝐶 } ) ) → ( ( ( 𝐹 ‘ 𝑧 ) + ( 𝐺 ‘ 𝑧 ) ) − ( ( 𝐹 ‘ 𝐶 ) + ( 𝐺 ‘ 𝐶 ) ) ) = ( ( ( 𝐹 ‘ 𝑧 ) − ( 𝐹 ‘ 𝐶 ) ) + ( ( 𝐺 ‘ 𝑧 ) − ( 𝐺 ‘ 𝐶 ) ) ) )
189 174 188 eqtrd ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( ( 𝑋 ∩ 𝑌 ) ∖ { 𝐶 } ) ) → ( ( ( 𝐹 ∘f + 𝐺 ) ‘ 𝑧 ) − ( ( 𝐹 ∘f + 𝐺 ) ‘ 𝐶 ) ) = ( ( ( 𝐹 ‘ 𝑧 ) − ( 𝐹 ‘ 𝐶 ) ) + ( ( 𝐺 ‘ 𝑧 ) − ( 𝐺 ‘ 𝐶 ) ) ) )
190 189 oveq1d ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( ( 𝑋 ∩ 𝑌 ) ∖ { 𝐶 } ) ) → ( ( ( ( 𝐹 ∘f + 𝐺 ) ‘ 𝑧 ) − ( ( 𝐹 ∘f + 𝐺 ) ‘ 𝐶 ) ) / ( 𝑧 − 𝐶 ) ) = ( ( ( ( 𝐹 ‘ 𝑧 ) − ( 𝐹 ‘ 𝐶 ) ) + ( ( 𝐺 ‘ 𝑧 ) − ( 𝐺 ‘ 𝐶 ) ) ) / ( 𝑧 − 𝐶 ) ) )
191 179 185 subcld ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( ( 𝑋 ∩ 𝑌 ) ∖ { 𝐶 } ) ) → ( ( 𝐹 ‘ 𝑧 ) − ( 𝐹 ‘ 𝐶 ) ) ∈ ℂ )
192 183 187 subcld ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( ( 𝑋 ∩ 𝑌 ) ∖ { 𝐶 } ) ) → ( ( 𝐺 ‘ 𝑧 ) − ( 𝐺 ‘ 𝐶 ) ) ∈ ℂ )
193 176 38 sstrid ⊢ ( 𝜑 → ( ( 𝑋 ∩ 𝑌 ) ∖ { 𝐶 } ) ⊆ ℂ )
194 193 sselda ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( ( 𝑋 ∩ 𝑌 ) ∖ { 𝐶 } ) ) → 𝑧 ∈ ℂ )
195 38 41 sseldd ⊢ ( 𝜑 → 𝐶 ∈ ℂ )
196 195 adantr ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( ( 𝑋 ∩ 𝑌 ) ∖ { 𝐶 } ) ) → 𝐶 ∈ ℂ )
197 194 196 subcld ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( ( 𝑋 ∩ 𝑌 ) ∖ { 𝐶 } ) ) → ( 𝑧 − 𝐶 ) ∈ ℂ )
198 eldifsni ⊢ ( 𝑧 ∈ ( ( 𝑋 ∩ 𝑌 ) ∖ { 𝐶 } ) → 𝑧 ≠ 𝐶 )
199 198 adantl ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( ( 𝑋 ∩ 𝑌 ) ∖ { 𝐶 } ) ) → 𝑧 ≠ 𝐶 )
200 194 196 199 subne0d ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( ( 𝑋 ∩ 𝑌 ) ∖ { 𝐶 } ) ) → ( 𝑧 − 𝐶 ) ≠ 0 )
201 191 192 197 200 divdird ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( ( 𝑋 ∩ 𝑌 ) ∖ { 𝐶 } ) ) → ( ( ( ( 𝐹 ‘ 𝑧 ) − ( 𝐹 ‘ 𝐶 ) ) + ( ( 𝐺 ‘ 𝑧 ) − ( 𝐺 ‘ 𝐶 ) ) ) / ( 𝑧 − 𝐶 ) ) = ( ( ( ( 𝐹 ‘ 𝑧 ) − ( 𝐹 ‘ 𝐶 ) ) / ( 𝑧 − 𝐶 ) ) + ( ( ( 𝐺 ‘ 𝑧 ) − ( 𝐺 ‘ 𝐶 ) ) / ( 𝑧 − 𝐶 ) ) ) )
202 190 201 eqtrd ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( ( 𝑋 ∩ 𝑌 ) ∖ { 𝐶 } ) ) → ( ( ( ( 𝐹 ∘f + 𝐺 ) ‘ 𝑧 ) − ( ( 𝐹 ∘f + 𝐺 ) ‘ 𝐶 ) ) / ( 𝑧 − 𝐶 ) ) = ( ( ( ( 𝐹 ‘ 𝑧 ) − ( 𝐹 ‘ 𝐶 ) ) / ( 𝑧 − 𝐶 ) ) + ( ( ( 𝐺 ‘ 𝑧 ) − ( 𝐺 ‘ 𝐶 ) ) / ( 𝑧 − 𝐶 ) ) ) )
203 202 mpteq2dva ⊢ ( 𝜑 → ( 𝑧 ∈ ( ( 𝑋 ∩ 𝑌 ) ∖ { 𝐶 } ) ↦ ( ( ( ( 𝐹 ∘f + 𝐺 ) ‘ 𝑧 ) − ( ( 𝐹 ∘f + 𝐺 ) ‘ 𝐶 ) ) / ( 𝑧 − 𝐶 ) ) ) = ( 𝑧 ∈ ( ( 𝑋 ∩ 𝑌 ) ∖ { 𝐶 } ) ↦ ( ( ( ( 𝐹 ‘ 𝑧 ) − ( 𝐹 ‘ 𝐶 ) ) / ( 𝑧 − 𝐶 ) ) + ( ( ( 𝐺 ‘ 𝑧 ) − ( 𝐺 ‘ 𝐶 ) ) / ( 𝑧 − 𝐶 ) ) ) ) )
204 203 oveq1d ⊢ ( 𝜑 → ( ( 𝑧 ∈ ( ( 𝑋 ∩ 𝑌 ) ∖ { 𝐶 } ) ↦ ( ( ( ( 𝐹 ∘f + 𝐺 ) ‘ 𝑧 ) − ( ( 𝐹 ∘f + 𝐺 ) ‘ 𝐶 ) ) / ( 𝑧 − 𝐶 ) ) ) limℂ 𝐶 ) = ( ( 𝑧 ∈ ( ( 𝑋 ∩ 𝑌 ) ∖ { 𝐶 } ) ↦ ( ( ( ( 𝐹 ‘ 𝑧 ) − ( 𝐹 ‘ 𝐶 ) ) / ( 𝑧 − 𝐶 ) ) + ( ( ( 𝐺 ‘ 𝑧 ) − ( 𝐺 ‘ 𝐶 ) ) / ( 𝑧 − 𝐶 ) ) ) ) limℂ 𝐶 ) )
205 152 204 eleqtrrd ⊢ ( 𝜑 → ( 𝐾 + 𝐿 ) ∈ ( ( 𝑧 ∈ ( ( 𝑋 ∩ 𝑌 ) ∖ { 𝐶 } ) ↦ ( ( ( ( 𝐹 ∘f + 𝐺 ) ‘ 𝑧 ) − ( ( 𝐹 ∘f + 𝐺 ) ‘ 𝐶 ) ) / ( 𝑧 − 𝐶 ) ) ) limℂ 𝐶 ) )
206 eqid ⊢ ( 𝑧 ∈ ( ( 𝑋 ∩ 𝑌 ) ∖ { 𝐶 } ) ↦ ( ( ( ( 𝐹 ∘f + 𝐺 ) ‘ 𝑧 ) − ( ( 𝐹 ∘f + 𝐺 ) ‘ 𝐶 ) ) / ( 𝑧 − 𝐶 ) ) ) = ( 𝑧 ∈ ( ( 𝑋 ∩ 𝑌 ) ∖ { 𝐶 } ) ↦ ( ( ( ( 𝐹 ∘f + 𝐺 ) ‘ 𝑧 ) − ( ( 𝐹 ∘f + 𝐺 ) ‘ 𝐶 ) ) / ( 𝑧 − 𝐶 ) ) )
207 addcl ⊢ ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ ) → ( 𝑥 + 𝑦 ) ∈ ℂ )
208 207 adantl ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ ) ) → ( 𝑥 + 𝑦 ) ∈ ℂ )
209 208 1 3 160 163 165 off ⊢ ( 𝜑 → ( 𝐹 ∘f + 𝐺 ) : ( 𝑋 ∩ 𝑌 ) ⟶ ℂ )
210 11 10 206 5 209 62 eldv ⊢ ( 𝜑 → ( 𝐶 ( 𝑆 D ( 𝐹 ∘f + 𝐺 ) ) ( 𝐾 + 𝐿 ) ↔ ( 𝐶 ∈ ( ( int ‘ ( 𝐽 ↾t 𝑆 ) ) ‘ ( 𝑋 ∩ 𝑌 ) ) ∧ ( 𝐾 + 𝐿 ) ∈ ( ( 𝑧 ∈ ( ( 𝑋 ∩ 𝑌 ) ∖ { 𝐶 } ) ↦ ( ( ( ( 𝐹 ∘f + 𝐺 ) ‘ 𝑧 ) − ( ( 𝐹 ∘f + 𝐺 ) ‘ 𝐶 ) ) / ( 𝑧 − 𝐶 ) ) ) limℂ 𝐶 ) ) ) )
211 33 205 210 mpbir2and ⊢ ( 𝜑 → 𝐶 ( 𝑆 D ( 𝐹 ∘f + 𝐺 ) ) ( 𝐾 + 𝐿 ) )