ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  dvcoapbr GIF version

Theorem dvcoapbr 14256
Description: The chain rule for derivatives at a point. The 𝑢 # 𝐶 → (𝐺𝑢) # (𝐺𝐶) hypothesis constrains what functions work for 𝐺. (Contributed by Mario Carneiro, 9-Aug-2014.) (Revised by Jim Kingdon, 21-Dec-2023.)
Hypotheses
Ref Expression
dvco.f (𝜑𝐹:𝑋⟶ℂ)
dvco.x (𝜑𝑋𝑆)
dvco.g (𝜑𝐺:𝑌𝑋)
dvco.y (𝜑𝑌𝑇)
dvcoap.gap (𝜑 → ∀𝑢𝑌 (𝑢 # 𝐶 → (𝐺𝑢) # (𝐺𝐶)))
dvcobr.s (𝜑𝑆 ⊆ ℂ)
dvcobr.t (𝜑𝑇 ⊆ ℂ)
dvco.bf (𝜑 → (𝐺𝐶)(𝑆 D 𝐹)𝐾)
dvco.bg (𝜑𝐶(𝑇 D 𝐺)𝐿)
dvcoap.j 𝐽 = (MetOpen‘(abs ∘ − ))
Assertion
Ref Expression
dvcoapbr (𝜑𝐶(𝑇 D (𝐹𝐺))(𝐾 · 𝐿))
Distinct variable groups:   𝑢,𝐶   𝑢,𝐺   𝑢,𝑌
Allowed substitution hints:   𝜑(𝑢)   𝑆(𝑢)   𝑇(𝑢)   𝐹(𝑢)   𝐽(𝑢)   𝐾(𝑢)   𝐿(𝑢)   𝑋(𝑢)

Proof of Theorem dvcoapbr
Dummy variables 𝑦 𝑧 𝑤 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 dvco.bg . . . 4 (𝜑𝐶(𝑇 D 𝐺)𝐿)
2 eqid 2177 . . . . 5 (𝐽t 𝑇) = (𝐽t 𝑇)
3 dvcoap.j . . . . 5 𝐽 = (MetOpen‘(abs ∘ − ))
4 eqid 2177 . . . . 5 (𝑧 ∈ {𝑤𝑌𝑤 # 𝐶} ↦ (((𝐺𝑧) − (𝐺𝐶)) / (𝑧𝐶))) = (𝑧 ∈ {𝑤𝑌𝑤 # 𝐶} ↦ (((𝐺𝑧) − (𝐺𝐶)) / (𝑧𝐶)))
5 dvcobr.t . . . . 5 (𝜑𝑇 ⊆ ℂ)
6 dvco.g . . . . . 6 (𝜑𝐺:𝑌𝑋)
7 dvco.x . . . . . . 7 (𝜑𝑋𝑆)
8 dvcobr.s . . . . . . 7 (𝜑𝑆 ⊆ ℂ)
97, 8sstrd 3167 . . . . . 6 (𝜑𝑋 ⊆ ℂ)
106, 9fssd 5380 . . . . 5 (𝜑𝐺:𝑌⟶ℂ)
11 dvco.y . . . . 5 (𝜑𝑌𝑇)
122, 3, 4, 5, 10, 11eldvap 14236 . . . 4 (𝜑 → (𝐶(𝑇 D 𝐺)𝐿 ↔ (𝐶 ∈ ((int‘(𝐽t 𝑇))‘𝑌) ∧ 𝐿 ∈ ((𝑧 ∈ {𝑤𝑌𝑤 # 𝐶} ↦ (((𝐺𝑧) − (𝐺𝐶)) / (𝑧𝐶))) lim 𝐶))))
131, 12mpbid 147 . . 3 (𝜑 → (𝐶 ∈ ((int‘(𝐽t 𝑇))‘𝑌) ∧ 𝐿 ∈ ((𝑧 ∈ {𝑤𝑌𝑤 # 𝐶} ↦ (((𝐺𝑧) − (𝐺𝐶)) / (𝑧𝐶))) lim 𝐶)))
1413simpld 112 . 2 (𝜑𝐶 ∈ ((int‘(𝐽t 𝑇))‘𝑌))
15 dvco.f . . . . . . . 8 (𝜑𝐹:𝑋⟶ℂ)
1615adantr 276 . . . . . . 7 ((𝜑𝑧 ∈ {𝑤𝑌𝑤 # 𝐶}) → 𝐹:𝑋⟶ℂ)
176adantr 276 . . . . . . . 8 ((𝜑𝑧 ∈ {𝑤𝑌𝑤 # 𝐶}) → 𝐺:𝑌𝑋)
18 elrabi 2892 . . . . . . . . 9 (𝑧 ∈ {𝑤𝑌𝑤 # 𝐶} → 𝑧𝑌)
1918adantl 277 . . . . . . . 8 ((𝜑𝑧 ∈ {𝑤𝑌𝑤 # 𝐶}) → 𝑧𝑌)
2017, 19ffvelcdmd 5654 . . . . . . 7 ((𝜑𝑧 ∈ {𝑤𝑌𝑤 # 𝐶}) → (𝐺𝑧) ∈ 𝑋)
2116, 20ffvelcdmd 5654 . . . . . 6 ((𝜑𝑧 ∈ {𝑤𝑌𝑤 # 𝐶}) → (𝐹‘(𝐺𝑧)) ∈ ℂ)
225, 10, 11dvbss 14239 . . . . . . . . . 10 (𝜑 → dom (𝑇 D 𝐺) ⊆ 𝑌)
23 cnex 7937 . . . . . . . . . . . . . 14 ℂ ∈ V
2423a1i 9 . . . . . . . . . . . . 13 (𝜑 → ℂ ∈ V)
2524, 5ssexd 4145 . . . . . . . . . . . . 13 (𝜑𝑇 ∈ V)
26 elpm2r 6668 . . . . . . . . . . . . 13 (((ℂ ∈ V ∧ 𝑇 ∈ V) ∧ (𝐺:𝑌⟶ℂ ∧ 𝑌𝑇)) → 𝐺 ∈ (ℂ ↑pm 𝑇))
2724, 25, 10, 11, 26syl22anc 1239 . . . . . . . . . . . 12 (𝜑𝐺 ∈ (ℂ ↑pm 𝑇))
28 reldvg 14233 . . . . . . . . . . . 12 ((𝑇 ⊆ ℂ ∧ 𝐺 ∈ (ℂ ↑pm 𝑇)) → Rel (𝑇 D 𝐺))
295, 27, 28syl2anc 411 . . . . . . . . . . 11 (𝜑 → Rel (𝑇 D 𝐺))
30 releldm 4864 . . . . . . . . . . 11 ((Rel (𝑇 D 𝐺) ∧ 𝐶(𝑇 D 𝐺)𝐿) → 𝐶 ∈ dom (𝑇 D 𝐺))
3129, 1, 30syl2anc 411 . . . . . . . . . 10 (𝜑𝐶 ∈ dom (𝑇 D 𝐺))
3222, 31sseldd 3158 . . . . . . . . 9 (𝜑𝐶𝑌)
3332adantr 276 . . . . . . . 8 ((𝜑𝑧 ∈ {𝑤𝑌𝑤 # 𝐶}) → 𝐶𝑌)
3417, 33ffvelcdmd 5654 . . . . . . 7 ((𝜑𝑧 ∈ {𝑤𝑌𝑤 # 𝐶}) → (𝐺𝐶) ∈ 𝑋)
3516, 34ffvelcdmd 5654 . . . . . 6 ((𝜑𝑧 ∈ {𝑤𝑌𝑤 # 𝐶}) → (𝐹‘(𝐺𝐶)) ∈ ℂ)
3621, 35subcld 8270 . . . . 5 ((𝜑𝑧 ∈ {𝑤𝑌𝑤 # 𝐶}) → ((𝐹‘(𝐺𝑧)) − (𝐹‘(𝐺𝐶))) ∈ ℂ)
3710adantr 276 . . . . . . 7 ((𝜑𝑧 ∈ {𝑤𝑌𝑤 # 𝐶}) → 𝐺:𝑌⟶ℂ)
3837, 19ffvelcdmd 5654 . . . . . 6 ((𝜑𝑧 ∈ {𝑤𝑌𝑤 # 𝐶}) → (𝐺𝑧) ∈ ℂ)
3937, 33ffvelcdmd 5654 . . . . . 6 ((𝜑𝑧 ∈ {𝑤𝑌𝑤 # 𝐶}) → (𝐺𝐶) ∈ ℂ)
4038, 39subcld 8270 . . . . 5 ((𝜑𝑧 ∈ {𝑤𝑌𝑤 # 𝐶}) → ((𝐺𝑧) − (𝐺𝐶)) ∈ ℂ)
419adantr 276 . . . . . . 7 ((𝜑𝑧 ∈ {𝑤𝑌𝑤 # 𝐶}) → 𝑋 ⊆ ℂ)
4241, 20sseldd 3158 . . . . . 6 ((𝜑𝑧 ∈ {𝑤𝑌𝑤 # 𝐶}) → (𝐺𝑧) ∈ ℂ)
4341, 34sseldd 3158 . . . . . 6 ((𝜑𝑧 ∈ {𝑤𝑌𝑤 # 𝐶}) → (𝐺𝐶) ∈ ℂ)
44 breq1 4008 . . . . . . . . . 10 (𝑤 = 𝑧 → (𝑤 # 𝐶𝑧 # 𝐶))
4544elrab 2895 . . . . . . . . 9 (𝑧 ∈ {𝑤𝑌𝑤 # 𝐶} ↔ (𝑧𝑌𝑧 # 𝐶))
4645simprbi 275 . . . . . . . 8 (𝑧 ∈ {𝑤𝑌𝑤 # 𝐶} → 𝑧 # 𝐶)
4746adantl 277 . . . . . . 7 ((𝜑𝑧 ∈ {𝑤𝑌𝑤 # 𝐶}) → 𝑧 # 𝐶)
48 breq1 4008 . . . . . . . . 9 (𝑢 = 𝑧 → (𝑢 # 𝐶𝑧 # 𝐶))
49 fveq2 5517 . . . . . . . . . 10 (𝑢 = 𝑧 → (𝐺𝑢) = (𝐺𝑧))
5049breq1d 4015 . . . . . . . . 9 (𝑢 = 𝑧 → ((𝐺𝑢) # (𝐺𝐶) ↔ (𝐺𝑧) # (𝐺𝐶)))
5148, 50imbi12d 234 . . . . . . . 8 (𝑢 = 𝑧 → ((𝑢 # 𝐶 → (𝐺𝑢) # (𝐺𝐶)) ↔ (𝑧 # 𝐶 → (𝐺𝑧) # (𝐺𝐶))))
52 dvcoap.gap . . . . . . . . 9 (𝜑 → ∀𝑢𝑌 (𝑢 # 𝐶 → (𝐺𝑢) # (𝐺𝐶)))
5352adantr 276 . . . . . . . 8 ((𝜑𝑧 ∈ {𝑤𝑌𝑤 # 𝐶}) → ∀𝑢𝑌 (𝑢 # 𝐶 → (𝐺𝑢) # (𝐺𝐶)))
5451, 53, 19rspcdva 2848 . . . . . . 7 ((𝜑𝑧 ∈ {𝑤𝑌𝑤 # 𝐶}) → (𝑧 # 𝐶 → (𝐺𝑧) # (𝐺𝐶)))
5547, 54mpd 13 . . . . . 6 ((𝜑𝑧 ∈ {𝑤𝑌𝑤 # 𝐶}) → (𝐺𝑧) # (𝐺𝐶))
5642, 43, 55subap0d 8603 . . . . 5 ((𝜑𝑧 ∈ {𝑤𝑌𝑤 # 𝐶}) → ((𝐺𝑧) − (𝐺𝐶)) # 0)
5736, 40, 56divclapd 8749 . . . 4 ((𝜑𝑧 ∈ {𝑤𝑌𝑤 # 𝐶}) → (((𝐹‘(𝐺𝑧)) − (𝐹‘(𝐺𝐶))) / ((𝐺𝑧) − (𝐺𝐶))) ∈ ℂ)
5811, 5sstrd 3167 . . . . 5 (𝜑𝑌 ⊆ ℂ)
5910, 58, 32dvlemap 14234 . . . 4 ((𝜑𝑧 ∈ {𝑤𝑌𝑤 # 𝐶}) → (((𝐺𝑧) − (𝐺𝐶)) / (𝑧𝐶)) ∈ ℂ)
60 ssidd 3178 . . . 4 (𝜑 → ℂ ⊆ ℂ)
613cntoptopon 14117 . . . . . 6 𝐽 ∈ (TopOn‘ℂ)
62 txtopon 13847 . . . . . 6 ((𝐽 ∈ (TopOn‘ℂ) ∧ 𝐽 ∈ (TopOn‘ℂ)) → (𝐽 ×t 𝐽) ∈ (TopOn‘(ℂ × ℂ)))
6361, 61, 62mp2an 426 . . . . 5 (𝐽 ×t 𝐽) ∈ (TopOn‘(ℂ × ℂ))
6463toponrestid 13606 . . . 4 (𝐽 ×t 𝐽) = ((𝐽 ×t 𝐽) ↾t (ℂ × ℂ))
65 breq1 4008 . . . . . 6 (𝑤 = (𝐺𝑧) → (𝑤 # (𝐺𝐶) ↔ (𝐺𝑧) # (𝐺𝐶)))
6665, 20, 55elrabd 2897 . . . . 5 ((𝜑𝑧 ∈ {𝑤𝑌𝑤 # 𝐶}) → (𝐺𝑧) ∈ {𝑤𝑋𝑤 # (𝐺𝐶)})
6715adantr 276 . . . . . . . 8 ((𝜑𝑦 ∈ {𝑤𝑋𝑤 # (𝐺𝐶)}) → 𝐹:𝑋⟶ℂ)
68 elrabi 2892 . . . . . . . . 9 (𝑦 ∈ {𝑤𝑋𝑤 # (𝐺𝐶)} → 𝑦𝑋)
6968adantl 277 . . . . . . . 8 ((𝜑𝑦 ∈ {𝑤𝑋𝑤 # (𝐺𝐶)}) → 𝑦𝑋)
7067, 69ffvelcdmd 5654 . . . . . . 7 ((𝜑𝑦 ∈ {𝑤𝑋𝑤 # (𝐺𝐶)}) → (𝐹𝑦) ∈ ℂ)
716adantr 276 . . . . . . . . 9 ((𝜑𝑦 ∈ {𝑤𝑋𝑤 # (𝐺𝐶)}) → 𝐺:𝑌𝑋)
7232adantr 276 . . . . . . . . 9 ((𝜑𝑦 ∈ {𝑤𝑋𝑤 # (𝐺𝐶)}) → 𝐶𝑌)
7371, 72ffvelcdmd 5654 . . . . . . . 8 ((𝜑𝑦 ∈ {𝑤𝑋𝑤 # (𝐺𝐶)}) → (𝐺𝐶) ∈ 𝑋)
7467, 73ffvelcdmd 5654 . . . . . . 7 ((𝜑𝑦 ∈ {𝑤𝑋𝑤 # (𝐺𝐶)}) → (𝐹‘(𝐺𝐶)) ∈ ℂ)
7570, 74subcld 8270 . . . . . 6 ((𝜑𝑦 ∈ {𝑤𝑋𝑤 # (𝐺𝐶)}) → ((𝐹𝑦) − (𝐹‘(𝐺𝐶))) ∈ ℂ)
769adantr 276 . . . . . . . 8 ((𝜑𝑦 ∈ {𝑤𝑋𝑤 # (𝐺𝐶)}) → 𝑋 ⊆ ℂ)
7776, 69sseldd 3158 . . . . . . 7 ((𝜑𝑦 ∈ {𝑤𝑋𝑤 # (𝐺𝐶)}) → 𝑦 ∈ ℂ)
7876, 73sseldd 3158 . . . . . . 7 ((𝜑𝑦 ∈ {𝑤𝑋𝑤 # (𝐺𝐶)}) → (𝐺𝐶) ∈ ℂ)
7977, 78subcld 8270 . . . . . 6 ((𝜑𝑦 ∈ {𝑤𝑋𝑤 # (𝐺𝐶)}) → (𝑦 − (𝐺𝐶)) ∈ ℂ)
80 breq1 4008 . . . . . . . . . 10 (𝑤 = 𝑦 → (𝑤 # (𝐺𝐶) ↔ 𝑦 # (𝐺𝐶)))
8180elrab 2895 . . . . . . . . 9 (𝑦 ∈ {𝑤𝑋𝑤 # (𝐺𝐶)} ↔ (𝑦𝑋𝑦 # (𝐺𝐶)))
8281simprbi 275 . . . . . . . 8 (𝑦 ∈ {𝑤𝑋𝑤 # (𝐺𝐶)} → 𝑦 # (𝐺𝐶))
8382adantl 277 . . . . . . 7 ((𝜑𝑦 ∈ {𝑤𝑋𝑤 # (𝐺𝐶)}) → 𝑦 # (𝐺𝐶))
8477, 78, 83subap0d 8603 . . . . . 6 ((𝜑𝑦 ∈ {𝑤𝑋𝑤 # (𝐺𝐶)}) → (𝑦 − (𝐺𝐶)) # 0)
8575, 79, 84divclapd 8749 . . . . 5 ((𝜑𝑦 ∈ {𝑤𝑋𝑤 # (𝐺𝐶)}) → (((𝐹𝑦) − (𝐹‘(𝐺𝐶))) / (𝑦 − (𝐺𝐶))) ∈ ℂ)
86 limcresi 14220 . . . . . . 7 (𝐺 lim 𝐶) ⊆ ((𝐺 ↾ {𝑤𝑌𝑤 # 𝐶}) lim 𝐶)
876feqmptd 5571 . . . . . . . . . 10 (𝜑𝐺 = (𝑧𝑌 ↦ (𝐺𝑧)))
8887reseq1d 4908 . . . . . . . . 9 (𝜑 → (𝐺 ↾ {𝑤𝑌𝑤 # 𝐶}) = ((𝑧𝑌 ↦ (𝐺𝑧)) ↾ {𝑤𝑌𝑤 # 𝐶}))
89 ssrab2 3242 . . . . . . . . . 10 {𝑤𝑌𝑤 # 𝐶} ⊆ 𝑌
90 resmpt 4957 . . . . . . . . . 10 ({𝑤𝑌𝑤 # 𝐶} ⊆ 𝑌 → ((𝑧𝑌 ↦ (𝐺𝑧)) ↾ {𝑤𝑌𝑤 # 𝐶}) = (𝑧 ∈ {𝑤𝑌𝑤 # 𝐶} ↦ (𝐺𝑧)))
9189, 90ax-mp 5 . . . . . . . . 9 ((𝑧𝑌 ↦ (𝐺𝑧)) ↾ {𝑤𝑌𝑤 # 𝐶}) = (𝑧 ∈ {𝑤𝑌𝑤 # 𝐶} ↦ (𝐺𝑧))
9288, 91eqtrdi 2226 . . . . . . . 8 (𝜑 → (𝐺 ↾ {𝑤𝑌𝑤 # 𝐶}) = (𝑧 ∈ {𝑤𝑌𝑤 # 𝐶} ↦ (𝐺𝑧)))
9392oveq1d 5892 . . . . . . 7 (𝜑 → ((𝐺 ↾ {𝑤𝑌𝑤 # 𝐶}) lim 𝐶) = ((𝑧 ∈ {𝑤𝑌𝑤 # 𝐶} ↦ (𝐺𝑧)) lim 𝐶))
9486, 93sseqtrid 3207 . . . . . 6 (𝜑 → (𝐺 lim 𝐶) ⊆ ((𝑧 ∈ {𝑤𝑌𝑤 # 𝐶} ↦ (𝐺𝑧)) lim 𝐶))
95 eqid 2177 . . . . . . . . . 10 (𝐽t 𝑌) = (𝐽t 𝑌)
9695, 3dvcnp2cntop 14248 . . . . . . . . 9 (((𝑇 ⊆ ℂ ∧ 𝐺:𝑌⟶ℂ ∧ 𝑌𝑇) ∧ 𝐶 ∈ dom (𝑇 D 𝐺)) → 𝐺 ∈ (((𝐽t 𝑌) CnP 𝐽)‘𝐶))
975, 10, 11, 31, 96syl31anc 1241 . . . . . . . 8 (𝜑𝐺 ∈ (((𝐽t 𝑌) CnP 𝐽)‘𝐶))
983, 95cnplimccntop 14224 . . . . . . . . 9 ((𝑌 ⊆ ℂ ∧ 𝐶𝑌) → (𝐺 ∈ (((𝐽t 𝑌) CnP 𝐽)‘𝐶) ↔ (𝐺:𝑌⟶ℂ ∧ (𝐺𝐶) ∈ (𝐺 lim 𝐶))))
9958, 32, 98syl2anc 411 . . . . . . . 8 (𝜑 → (𝐺 ∈ (((𝐽t 𝑌) CnP 𝐽)‘𝐶) ↔ (𝐺:𝑌⟶ℂ ∧ (𝐺𝐶) ∈ (𝐺 lim 𝐶))))
10097, 99mpbid 147 . . . . . . 7 (𝜑 → (𝐺:𝑌⟶ℂ ∧ (𝐺𝐶) ∈ (𝐺 lim 𝐶)))
101100simprd 114 . . . . . 6 (𝜑 → (𝐺𝐶) ∈ (𝐺 lim 𝐶))
10294, 101sseldd 3158 . . . . 5 (𝜑 → (𝐺𝐶) ∈ ((𝑧 ∈ {𝑤𝑌𝑤 # 𝐶} ↦ (𝐺𝑧)) lim 𝐶))
103 dvco.bf . . . . . . 7 (𝜑 → (𝐺𝐶)(𝑆 D 𝐹)𝐾)
104 eqid 2177 . . . . . . . 8 (𝐽t 𝑆) = (𝐽t 𝑆)
105 eqid 2177 . . . . . . . 8 (𝑦 ∈ {𝑤𝑋𝑤 # (𝐺𝐶)} ↦ (((𝐹𝑦) − (𝐹‘(𝐺𝐶))) / (𝑦 − (𝐺𝐶)))) = (𝑦 ∈ {𝑤𝑋𝑤 # (𝐺𝐶)} ↦ (((𝐹𝑦) − (𝐹‘(𝐺𝐶))) / (𝑦 − (𝐺𝐶))))
106104, 3, 105, 8, 15, 7eldvap 14236 . . . . . . 7 (𝜑 → ((𝐺𝐶)(𝑆 D 𝐹)𝐾 ↔ ((𝐺𝐶) ∈ ((int‘(𝐽t 𝑆))‘𝑋) ∧ 𝐾 ∈ ((𝑦 ∈ {𝑤𝑋𝑤 # (𝐺𝐶)} ↦ (((𝐹𝑦) − (𝐹‘(𝐺𝐶))) / (𝑦 − (𝐺𝐶)))) lim (𝐺𝐶)))))
107103, 106mpbid 147 . . . . . 6 (𝜑 → ((𝐺𝐶) ∈ ((int‘(𝐽t 𝑆))‘𝑋) ∧ 𝐾 ∈ ((𝑦 ∈ {𝑤𝑋𝑤 # (𝐺𝐶)} ↦ (((𝐹𝑦) − (𝐹‘(𝐺𝐶))) / (𝑦 − (𝐺𝐶)))) lim (𝐺𝐶))))
108107simprd 114 . . . . 5 (𝜑𝐾 ∈ ((𝑦 ∈ {𝑤𝑋𝑤 # (𝐺𝐶)} ↦ (((𝐹𝑦) − (𝐹‘(𝐺𝐶))) / (𝑦 − (𝐺𝐶)))) lim (𝐺𝐶)))
109 fveq2 5517 . . . . . . 7 (𝑦 = (𝐺𝑧) → (𝐹𝑦) = (𝐹‘(𝐺𝑧)))
110109oveq1d 5892 . . . . . 6 (𝑦 = (𝐺𝑧) → ((𝐹𝑦) − (𝐹‘(𝐺𝐶))) = ((𝐹‘(𝐺𝑧)) − (𝐹‘(𝐺𝐶))))
111 oveq1 5884 . . . . . 6 (𝑦 = (𝐺𝑧) → (𝑦 − (𝐺𝐶)) = ((𝐺𝑧) − (𝐺𝐶)))
112110, 111oveq12d 5895 . . . . 5 (𝑦 = (𝐺𝑧) → (((𝐹𝑦) − (𝐹‘(𝐺𝐶))) / (𝑦 − (𝐺𝐶))) = (((𝐹‘(𝐺𝑧)) − (𝐹‘(𝐺𝐶))) / ((𝐺𝑧) − (𝐺𝐶))))
11366, 85, 102, 108, 112limccoap 14232 . . . 4 (𝜑𝐾 ∈ ((𝑧 ∈ {𝑤𝑌𝑤 # 𝐶} ↦ (((𝐹‘(𝐺𝑧)) − (𝐹‘(𝐺𝐶))) / ((𝐺𝑧) − (𝐺𝐶)))) lim 𝐶))
11413simprd 114 . . . 4 (𝜑𝐿 ∈ ((𝑧 ∈ {𝑤𝑌𝑤 # 𝐶} ↦ (((𝐺𝑧) − (𝐺𝐶)) / (𝑧𝐶))) lim 𝐶))
1153mulcncntop 14139 . . . . 5 · ∈ ((𝐽 ×t 𝐽) Cn 𝐽)
1168, 15, 7dvcl 14237 . . . . . . 7 ((𝜑 ∧ (𝐺𝐶)(𝑆 D 𝐹)𝐾) → 𝐾 ∈ ℂ)
117103, 116mpdan 421 . . . . . 6 (𝜑𝐾 ∈ ℂ)
1185, 10, 11dvcl 14237 . . . . . . 7 ((𝜑𝐶(𝑇 D 𝐺)𝐿) → 𝐿 ∈ ℂ)
1191, 118mpdan 421 . . . . . 6 (𝜑𝐿 ∈ ℂ)
120117, 119opelxpd 4661 . . . . 5 (𝜑 → ⟨𝐾, 𝐿⟩ ∈ (ℂ × ℂ))
12163toponunii 13602 . . . . . 6 (ℂ × ℂ) = (𝐽 ×t 𝐽)
122121cncnpi 13813 . . . . 5 (( · ∈ ((𝐽 ×t 𝐽) Cn 𝐽) ∧ ⟨𝐾, 𝐿⟩ ∈ (ℂ × ℂ)) → · ∈ (((𝐽 ×t 𝐽) CnP 𝐽)‘⟨𝐾, 𝐿⟩))
123115, 120, 122sylancr 414 . . . 4 (𝜑 → · ∈ (((𝐽 ×t 𝐽) CnP 𝐽)‘⟨𝐾, 𝐿⟩))
12457, 59, 60, 60, 3, 64, 113, 114, 123limccnp2cntop 14231 . . 3 (𝜑 → (𝐾 · 𝐿) ∈ ((𝑧 ∈ {𝑤𝑌𝑤 # 𝐶} ↦ ((((𝐹‘(𝐺𝑧)) − (𝐹‘(𝐺𝐶))) / ((𝐺𝑧) − (𝐺𝐶))) · (((𝐺𝑧) − (𝐺𝐶)) / (𝑧𝐶)))) lim 𝐶))
12542, 43subcld 8270 . . . . . . 7 ((𝜑𝑧 ∈ {𝑤𝑌𝑤 # 𝐶}) → ((𝐺𝑧) − (𝐺𝐶)) ∈ ℂ)
12658adantr 276 . . . . . . . . 9 ((𝜑𝑧 ∈ {𝑤𝑌𝑤 # 𝐶}) → 𝑌 ⊆ ℂ)
127126, 19sseldd 3158 . . . . . . . 8 ((𝜑𝑧 ∈ {𝑤𝑌𝑤 # 𝐶}) → 𝑧 ∈ ℂ)
128126, 33sseldd 3158 . . . . . . . 8 ((𝜑𝑧 ∈ {𝑤𝑌𝑤 # 𝐶}) → 𝐶 ∈ ℂ)
129127, 128subcld 8270 . . . . . . 7 ((𝜑𝑧 ∈ {𝑤𝑌𝑤 # 𝐶}) → (𝑧𝐶) ∈ ℂ)
130127, 128, 47subap0d 8603 . . . . . . 7 ((𝜑𝑧 ∈ {𝑤𝑌𝑤 # 𝐶}) → (𝑧𝐶) # 0)
13136, 125, 129, 56, 130dmdcanap2d 8780 . . . . . 6 ((𝜑𝑧 ∈ {𝑤𝑌𝑤 # 𝐶}) → ((((𝐹‘(𝐺𝑧)) − (𝐹‘(𝐺𝐶))) / ((𝐺𝑧) − (𝐺𝐶))) · (((𝐺𝑧) − (𝐺𝐶)) / (𝑧𝐶))) = (((𝐹‘(𝐺𝑧)) − (𝐹‘(𝐺𝐶))) / (𝑧𝐶)))
132 fvco3 5589 . . . . . . . . 9 ((𝐺:𝑌𝑋𝑧𝑌) → ((𝐹𝐺)‘𝑧) = (𝐹‘(𝐺𝑧)))
13317, 19, 132syl2anc 411 . . . . . . . 8 ((𝜑𝑧 ∈ {𝑤𝑌𝑤 # 𝐶}) → ((𝐹𝐺)‘𝑧) = (𝐹‘(𝐺𝑧)))
134 fvco3 5589 . . . . . . . . 9 ((𝐺:𝑌𝑋𝐶𝑌) → ((𝐹𝐺)‘𝐶) = (𝐹‘(𝐺𝐶)))
13517, 33, 134syl2anc 411 . . . . . . . 8 ((𝜑𝑧 ∈ {𝑤𝑌𝑤 # 𝐶}) → ((𝐹𝐺)‘𝐶) = (𝐹‘(𝐺𝐶)))
136133, 135oveq12d 5895 . . . . . . 7 ((𝜑𝑧 ∈ {𝑤𝑌𝑤 # 𝐶}) → (((𝐹𝐺)‘𝑧) − ((𝐹𝐺)‘𝐶)) = ((𝐹‘(𝐺𝑧)) − (𝐹‘(𝐺𝐶))))
137136oveq1d 5892 . . . . . 6 ((𝜑𝑧 ∈ {𝑤𝑌𝑤 # 𝐶}) → ((((𝐹𝐺)‘𝑧) − ((𝐹𝐺)‘𝐶)) / (𝑧𝐶)) = (((𝐹‘(𝐺𝑧)) − (𝐹‘(𝐺𝐶))) / (𝑧𝐶)))
138131, 137eqtr4d 2213 . . . . 5 ((𝜑𝑧 ∈ {𝑤𝑌𝑤 # 𝐶}) → ((((𝐹‘(𝐺𝑧)) − (𝐹‘(𝐺𝐶))) / ((𝐺𝑧) − (𝐺𝐶))) · (((𝐺𝑧) − (𝐺𝐶)) / (𝑧𝐶))) = ((((𝐹𝐺)‘𝑧) − ((𝐹𝐺)‘𝐶)) / (𝑧𝐶)))
139138mpteq2dva 4095 . . . 4 (𝜑 → (𝑧 ∈ {𝑤𝑌𝑤 # 𝐶} ↦ ((((𝐹‘(𝐺𝑧)) − (𝐹‘(𝐺𝐶))) / ((𝐺𝑧) − (𝐺𝐶))) · (((𝐺𝑧) − (𝐺𝐶)) / (𝑧𝐶)))) = (𝑧 ∈ {𝑤𝑌𝑤 # 𝐶} ↦ ((((𝐹𝐺)‘𝑧) − ((𝐹𝐺)‘𝐶)) / (𝑧𝐶))))
140139oveq1d 5892 . . 3 (𝜑 → ((𝑧 ∈ {𝑤𝑌𝑤 # 𝐶} ↦ ((((𝐹‘(𝐺𝑧)) − (𝐹‘(𝐺𝐶))) / ((𝐺𝑧) − (𝐺𝐶))) · (((𝐺𝑧) − (𝐺𝐶)) / (𝑧𝐶)))) lim 𝐶) = ((𝑧 ∈ {𝑤𝑌𝑤 # 𝐶} ↦ ((((𝐹𝐺)‘𝑧) − ((𝐹𝐺)‘𝐶)) / (𝑧𝐶))) lim 𝐶))
141124, 140eleqtrd 2256 . 2 (𝜑 → (𝐾 · 𝐿) ∈ ((𝑧 ∈ {𝑤𝑌𝑤 # 𝐶} ↦ ((((𝐹𝐺)‘𝑧) − ((𝐹𝐺)‘𝐶)) / (𝑧𝐶))) lim 𝐶))
142 eqid 2177 . . 3 (𝑧 ∈ {𝑤𝑌𝑤 # 𝐶} ↦ ((((𝐹𝐺)‘𝑧) − ((𝐹𝐺)‘𝐶)) / (𝑧𝐶))) = (𝑧 ∈ {𝑤𝑌𝑤 # 𝐶} ↦ ((((𝐹𝐺)‘𝑧) − ((𝐹𝐺)‘𝐶)) / (𝑧𝐶)))
143 fco 5383 . . . 4 ((𝐹:𝑋⟶ℂ ∧ 𝐺:𝑌𝑋) → (𝐹𝐺):𝑌⟶ℂ)
14415, 6, 143syl2anc 411 . . 3 (𝜑 → (𝐹𝐺):𝑌⟶ℂ)
1452, 3, 142, 5, 144, 11eldvap 14236 . 2 (𝜑 → (𝐶(𝑇 D (𝐹𝐺))(𝐾 · 𝐿) ↔ (𝐶 ∈ ((int‘(𝐽t 𝑇))‘𝑌) ∧ (𝐾 · 𝐿) ∈ ((𝑧 ∈ {𝑤𝑌𝑤 # 𝐶} ↦ ((((𝐹𝐺)‘𝑧) − ((𝐹𝐺)‘𝐶)) / (𝑧𝐶))) lim 𝐶))))
14614, 141, 145mpbir2and 944 1 (𝜑𝐶(𝑇 D (𝐹𝐺))(𝐾 · 𝐿))
Colors of variables: wff set class
Syntax hints:  wi 4  wa 104  wb 105   = wceq 1353  wcel 2148  wral 2455  {crab 2459  Vcvv 2739  wss 3131  cop 3597   class class class wbr 4005  cmpt 4066   × cxp 4626  dom cdm 4628  cres 4630  ccom 4632  Rel wrel 4633  wf 5214  cfv 5218  (class class class)co 5877  pm cpm 6651  cc 7811   · cmul 7818  cmin 8130   # cap 8540   / cdiv 8631  abscabs 11008  t crest 12693  MetOpencmopn 13530  TopOnctopon 13595  intcnt 13678   Cn ccn 13770   CnP ccnp 13771   ×t ctx 13837   lim climc 14208   D cdv 14209
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in1 614  ax-in2 615  ax-io 709  ax-5 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-10 1505  ax-11 1506  ax-i12 1507  ax-bndl 1509  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-13 2150  ax-14 2151  ax-ext 2159  ax-coll 4120  ax-sep 4123  ax-nul 4131  ax-pow 4176  ax-pr 4211  ax-un 4435  ax-setind 4538  ax-iinf 4589  ax-cnex 7904  ax-resscn 7905  ax-1cn 7906  ax-1re 7907  ax-icn 7908  ax-addcl 7909  ax-addrcl 7910  ax-mulcl 7911  ax-mulrcl 7912  ax-addcom 7913  ax-mulcom 7914  ax-addass 7915  ax-mulass 7916  ax-distr 7917  ax-i2m1 7918  ax-0lt1 7919  ax-1rid 7920  ax-0id 7921  ax-rnegex 7922  ax-precex 7923  ax-cnre 7924  ax-pre-ltirr 7925  ax-pre-ltwlin 7926  ax-pre-lttrn 7927  ax-pre-apti 7928  ax-pre-ltadd 7929  ax-pre-mulgt0 7930  ax-pre-mulext 7931  ax-arch 7932  ax-caucvg 7933  ax-addf 7935  ax-mulf 7936
This theorem depends on definitions:  df-bi 117  df-stab 831  df-dc 835  df-3or 979  df-3an 980  df-tru 1356  df-fal 1359  df-nf 1461  df-sb 1763  df-eu 2029  df-mo 2030  df-clab 2164  df-cleq 2170  df-clel 2173  df-nfc 2308  df-ne 2348  df-nel 2443  df-ral 2460  df-rex 2461  df-reu 2462  df-rmo 2463  df-rab 2464  df-v 2741  df-sbc 2965  df-csb 3060  df-dif 3133  df-un 3135  df-in 3137  df-ss 3144  df-nul 3425  df-if 3537  df-pw 3579  df-sn 3600  df-pr 3601  df-op 3603  df-uni 3812  df-int 3847  df-iun 3890  df-br 4006  df-opab 4067  df-mpt 4068  df-tr 4104  df-id 4295  df-po 4298  df-iso 4299  df-iord 4368  df-on 4370  df-ilim 4371  df-suc 4373  df-iom 4592  df-xp 4634  df-rel 4635  df-cnv 4636  df-co 4637  df-dm 4638  df-rn 4639  df-res 4640  df-ima 4641  df-iota 5180  df-fun 5220  df-fn 5221  df-f 5222  df-f1 5223  df-fo 5224  df-f1o 5225  df-fv 5226  df-isom 5227  df-riota 5833  df-ov 5880  df-oprab 5881  df-mpo 5882  df-1st 6143  df-2nd 6144  df-recs 6308  df-frec 6394  df-map 6652  df-pm 6653  df-sup 6985  df-inf 6986  df-pnf 7996  df-mnf 7997  df-xr 7998  df-ltxr 7999  df-le 8000  df-sub 8132  df-neg 8133  df-reap 8534  df-ap 8541  df-div 8632  df-inn 8922  df-2 8980  df-3 8981  df-4 8982  df-n0 9179  df-z 9256  df-uz 9531  df-q 9622  df-rp 9656  df-xneg 9774  df-xadd 9775  df-seqfrec 10448  df-exp 10522  df-cj 10853  df-re 10854  df-im 10855  df-rsqrt 11009  df-abs 11010  df-rest 12695  df-topgen 12714  df-psmet 13532  df-xmet 13533  df-met 13534  df-bl 13535  df-mopn 13536  df-top 13583  df-topon 13596  df-bases 13628  df-ntr 13681  df-cn 13773  df-cnp 13774  df-tx 13838  df-cncf 14143  df-limced 14210  df-dvap 14211
This theorem is referenced by:  dvef  14273
  Copyright terms: Public domain W3C validator