MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  cmvthOLD Structured version   Visualization version   GIF version

Theorem cmvthOLD 25868
Description: Obsolete version of cmvth 25867 as of 16-Apr-2025. (Contributed by Mario Carneiro, 29-Dec-2016.) (Proof modification is discouraged.) (New usage is discouraged.)
Hypotheses
Ref Expression
cmvthOLD.a (πœ‘ β†’ 𝐴 ∈ ℝ)
cmvthOLD.b (πœ‘ β†’ 𝐡 ∈ ℝ)
cmvthOLD.lt (πœ‘ β†’ 𝐴 < 𝐡)
cmvthOLD.f (πœ‘ β†’ 𝐹 ∈ ((𝐴[,]𝐡)–cn→ℝ))
cmvthOLD.g (πœ‘ β†’ 𝐺 ∈ ((𝐴[,]𝐡)–cn→ℝ))
cmvthOLD.df (πœ‘ β†’ dom (ℝ D 𝐹) = (𝐴(,)𝐡))
cmvthOLD.dg (πœ‘ β†’ dom (ℝ D 𝐺) = (𝐴(,)𝐡))
Assertion
Ref Expression
cmvthOLD (πœ‘ β†’ βˆƒπ‘₯ ∈ (𝐴(,)𝐡)(((πΉβ€˜π΅) βˆ’ (πΉβ€˜π΄)) Β· ((ℝ D 𝐺)β€˜π‘₯)) = (((πΊβ€˜π΅) βˆ’ (πΊβ€˜π΄)) Β· ((ℝ D 𝐹)β€˜π‘₯)))
Distinct variable groups:   π‘₯,𝐴   π‘₯,𝐡   π‘₯,𝐹   π‘₯,𝐺   πœ‘,π‘₯

Proof of Theorem cmvthOLD
Dummy variable 𝑧 is distinct from all other variables.
StepHypRef Expression
1 cmvthOLD.a . . 3 (πœ‘ β†’ 𝐴 ∈ ℝ)
2 cmvthOLD.b . . 3 (πœ‘ β†’ 𝐡 ∈ ℝ)
3 cmvthOLD.lt . . 3 (πœ‘ β†’ 𝐴 < 𝐡)
4 eqid 2724 . . . 4 (TopOpenβ€˜β„‚fld) = (TopOpenβ€˜β„‚fld)
54subcn 24726 . . . 4 βˆ’ ∈ (((TopOpenβ€˜β„‚fld) Γ—t (TopOpenβ€˜β„‚fld)) Cn (TopOpenβ€˜β„‚fld))
64mulcn 24727 . . . . 5 Β· ∈ (((TopOpenβ€˜β„‚fld) Γ—t (TopOpenβ€˜β„‚fld)) Cn (TopOpenβ€˜β„‚fld))
7 cmvthOLD.f . . . . . . . . 9 (πœ‘ β†’ 𝐹 ∈ ((𝐴[,]𝐡)–cn→ℝ))
8 cncff 24757 . . . . . . . . 9 (𝐹 ∈ ((𝐴[,]𝐡)–cn→ℝ) β†’ 𝐹:(𝐴[,]𝐡)βŸΆβ„)
97, 8syl 17 . . . . . . . 8 (πœ‘ β†’ 𝐹:(𝐴[,]𝐡)βŸΆβ„)
101rexrd 11263 . . . . . . . . 9 (πœ‘ β†’ 𝐴 ∈ ℝ*)
112rexrd 11263 . . . . . . . . 9 (πœ‘ β†’ 𝐡 ∈ ℝ*)
121, 2, 3ltled 11361 . . . . . . . . 9 (πœ‘ β†’ 𝐴 ≀ 𝐡)
13 ubicc2 13443 . . . . . . . . 9 ((𝐴 ∈ ℝ* ∧ 𝐡 ∈ ℝ* ∧ 𝐴 ≀ 𝐡) β†’ 𝐡 ∈ (𝐴[,]𝐡))
1410, 11, 12, 13syl3anc 1368 . . . . . . . 8 (πœ‘ β†’ 𝐡 ∈ (𝐴[,]𝐡))
159, 14ffvelcdmd 7078 . . . . . . 7 (πœ‘ β†’ (πΉβ€˜π΅) ∈ ℝ)
16 lbicc2 13442 . . . . . . . . 9 ((𝐴 ∈ ℝ* ∧ 𝐡 ∈ ℝ* ∧ 𝐴 ≀ 𝐡) β†’ 𝐴 ∈ (𝐴[,]𝐡))
1710, 11, 12, 16syl3anc 1368 . . . . . . . 8 (πœ‘ β†’ 𝐴 ∈ (𝐴[,]𝐡))
189, 17ffvelcdmd 7078 . . . . . . 7 (πœ‘ β†’ (πΉβ€˜π΄) ∈ ℝ)
1915, 18resubcld 11641 . . . . . 6 (πœ‘ β†’ ((πΉβ€˜π΅) βˆ’ (πΉβ€˜π΄)) ∈ ℝ)
20 iccssre 13407 . . . . . . . 8 ((𝐴 ∈ ℝ ∧ 𝐡 ∈ ℝ) β†’ (𝐴[,]𝐡) βŠ† ℝ)
211, 2, 20syl2anc 583 . . . . . . 7 (πœ‘ β†’ (𝐴[,]𝐡) βŠ† ℝ)
22 ax-resscn 11164 . . . . . . 7 ℝ βŠ† β„‚
2321, 22sstrdi 3987 . . . . . 6 (πœ‘ β†’ (𝐴[,]𝐡) βŠ† β„‚)
2422a1i 11 . . . . . 6 (πœ‘ β†’ ℝ βŠ† β„‚)
25 cncfmptc 24776 . . . . . 6 ((((πΉβ€˜π΅) βˆ’ (πΉβ€˜π΄)) ∈ ℝ ∧ (𝐴[,]𝐡) βŠ† β„‚ ∧ ℝ βŠ† β„‚) β†’ (𝑧 ∈ (𝐴[,]𝐡) ↦ ((πΉβ€˜π΅) βˆ’ (πΉβ€˜π΄))) ∈ ((𝐴[,]𝐡)–cn→ℝ))
2619, 23, 24, 25syl3anc 1368 . . . . 5 (πœ‘ β†’ (𝑧 ∈ (𝐴[,]𝐡) ↦ ((πΉβ€˜π΅) βˆ’ (πΉβ€˜π΄))) ∈ ((𝐴[,]𝐡)–cn→ℝ))
27 cmvthOLD.g . . . . . . . 8 (πœ‘ β†’ 𝐺 ∈ ((𝐴[,]𝐡)–cn→ℝ))
28 cncff 24757 . . . . . . . 8 (𝐺 ∈ ((𝐴[,]𝐡)–cn→ℝ) β†’ 𝐺:(𝐴[,]𝐡)βŸΆβ„)
2927, 28syl 17 . . . . . . 7 (πœ‘ β†’ 𝐺:(𝐴[,]𝐡)βŸΆβ„)
3029feqmptd 6951 . . . . . 6 (πœ‘ β†’ 𝐺 = (𝑧 ∈ (𝐴[,]𝐡) ↦ (πΊβ€˜π‘§)))
3130, 27eqeltrrd 2826 . . . . 5 (πœ‘ β†’ (𝑧 ∈ (𝐴[,]𝐡) ↦ (πΊβ€˜π‘§)) ∈ ((𝐴[,]𝐡)–cn→ℝ))
32 remulcl 11192 . . . . 5 ((((πΉβ€˜π΅) βˆ’ (πΉβ€˜π΄)) ∈ ℝ ∧ (πΊβ€˜π‘§) ∈ ℝ) β†’ (((πΉβ€˜π΅) βˆ’ (πΉβ€˜π΄)) Β· (πΊβ€˜π‘§)) ∈ ℝ)
334, 6, 26, 31, 22, 32cncfmpt2ss 24780 . . . 4 (πœ‘ β†’ (𝑧 ∈ (𝐴[,]𝐡) ↦ (((πΉβ€˜π΅) βˆ’ (πΉβ€˜π΄)) Β· (πΊβ€˜π‘§))) ∈ ((𝐴[,]𝐡)–cn→ℝ))
3429, 14ffvelcdmd 7078 . . . . . . 7 (πœ‘ β†’ (πΊβ€˜π΅) ∈ ℝ)
3529, 17ffvelcdmd 7078 . . . . . . 7 (πœ‘ β†’ (πΊβ€˜π΄) ∈ ℝ)
3634, 35resubcld 11641 . . . . . 6 (πœ‘ β†’ ((πΊβ€˜π΅) βˆ’ (πΊβ€˜π΄)) ∈ ℝ)
37 cncfmptc 24776 . . . . . 6 ((((πΊβ€˜π΅) βˆ’ (πΊβ€˜π΄)) ∈ ℝ ∧ (𝐴[,]𝐡) βŠ† β„‚ ∧ ℝ βŠ† β„‚) β†’ (𝑧 ∈ (𝐴[,]𝐡) ↦ ((πΊβ€˜π΅) βˆ’ (πΊβ€˜π΄))) ∈ ((𝐴[,]𝐡)–cn→ℝ))
3836, 23, 24, 37syl3anc 1368 . . . . 5 (πœ‘ β†’ (𝑧 ∈ (𝐴[,]𝐡) ↦ ((πΊβ€˜π΅) βˆ’ (πΊβ€˜π΄))) ∈ ((𝐴[,]𝐡)–cn→ℝ))
399feqmptd 6951 . . . . . 6 (πœ‘ β†’ 𝐹 = (𝑧 ∈ (𝐴[,]𝐡) ↦ (πΉβ€˜π‘§)))
4039, 7eqeltrrd 2826 . . . . 5 (πœ‘ β†’ (𝑧 ∈ (𝐴[,]𝐡) ↦ (πΉβ€˜π‘§)) ∈ ((𝐴[,]𝐡)–cn→ℝ))
41 remulcl 11192 . . . . 5 ((((πΊβ€˜π΅) βˆ’ (πΊβ€˜π΄)) ∈ ℝ ∧ (πΉβ€˜π‘§) ∈ ℝ) β†’ (((πΊβ€˜π΅) βˆ’ (πΊβ€˜π΄)) Β· (πΉβ€˜π‘§)) ∈ ℝ)
424, 6, 38, 40, 22, 41cncfmpt2ss 24780 . . . 4 (πœ‘ β†’ (𝑧 ∈ (𝐴[,]𝐡) ↦ (((πΊβ€˜π΅) βˆ’ (πΊβ€˜π΄)) Β· (πΉβ€˜π‘§))) ∈ ((𝐴[,]𝐡)–cn→ℝ))
43 resubcl 11523 . . . 4 (((((πΉβ€˜π΅) βˆ’ (πΉβ€˜π΄)) Β· (πΊβ€˜π‘§)) ∈ ℝ ∧ (((πΊβ€˜π΅) βˆ’ (πΊβ€˜π΄)) Β· (πΉβ€˜π‘§)) ∈ ℝ) β†’ ((((πΉβ€˜π΅) βˆ’ (πΉβ€˜π΄)) Β· (πΊβ€˜π‘§)) βˆ’ (((πΊβ€˜π΅) βˆ’ (πΊβ€˜π΄)) Β· (πΉβ€˜π‘§))) ∈ ℝ)
444, 5, 33, 42, 22, 43cncfmpt2ss 24780 . . 3 (πœ‘ β†’ (𝑧 ∈ (𝐴[,]𝐡) ↦ ((((πΉβ€˜π΅) βˆ’ (πΉβ€˜π΄)) Β· (πΊβ€˜π‘§)) βˆ’ (((πΊβ€˜π΅) βˆ’ (πΊβ€˜π΄)) Β· (πΉβ€˜π‘§)))) ∈ ((𝐴[,]𝐡)–cn→ℝ))
4519recnd 11241 . . . . . . . . . 10 (πœ‘ β†’ ((πΉβ€˜π΅) βˆ’ (πΉβ€˜π΄)) ∈ β„‚)
4645adantr 480 . . . . . . . . 9 ((πœ‘ ∧ 𝑧 ∈ (𝐴[,]𝐡)) β†’ ((πΉβ€˜π΅) βˆ’ (πΉβ€˜π΄)) ∈ β„‚)
4729ffvelcdmda 7077 . . . . . . . . . 10 ((πœ‘ ∧ 𝑧 ∈ (𝐴[,]𝐡)) β†’ (πΊβ€˜π‘§) ∈ ℝ)
4847recnd 11241 . . . . . . . . 9 ((πœ‘ ∧ 𝑧 ∈ (𝐴[,]𝐡)) β†’ (πΊβ€˜π‘§) ∈ β„‚)
4946, 48mulcld 11233 . . . . . . . 8 ((πœ‘ ∧ 𝑧 ∈ (𝐴[,]𝐡)) β†’ (((πΉβ€˜π΅) βˆ’ (πΉβ€˜π΄)) Β· (πΊβ€˜π‘§)) ∈ β„‚)
5036adantr 480 . . . . . . . . . 10 ((πœ‘ ∧ 𝑧 ∈ (𝐴[,]𝐡)) β†’ ((πΊβ€˜π΅) βˆ’ (πΊβ€˜π΄)) ∈ ℝ)
519ffvelcdmda 7077 . . . . . . . . . 10 ((πœ‘ ∧ 𝑧 ∈ (𝐴[,]𝐡)) β†’ (πΉβ€˜π‘§) ∈ ℝ)
5250, 51remulcld 11243 . . . . . . . . 9 ((πœ‘ ∧ 𝑧 ∈ (𝐴[,]𝐡)) β†’ (((πΊβ€˜π΅) βˆ’ (πΊβ€˜π΄)) Β· (πΉβ€˜π‘§)) ∈ ℝ)
5352recnd 11241 . . . . . . . 8 ((πœ‘ ∧ 𝑧 ∈ (𝐴[,]𝐡)) β†’ (((πΊβ€˜π΅) βˆ’ (πΊβ€˜π΄)) Β· (πΉβ€˜π‘§)) ∈ β„‚)
5449, 53subcld 11570 . . . . . . 7 ((πœ‘ ∧ 𝑧 ∈ (𝐴[,]𝐡)) β†’ ((((πΉβ€˜π΅) βˆ’ (πΉβ€˜π΄)) Β· (πΊβ€˜π‘§)) βˆ’ (((πΊβ€˜π΅) βˆ’ (πΊβ€˜π΄)) Β· (πΉβ€˜π‘§))) ∈ β„‚)
554tgioo2 24663 . . . . . . 7 (topGenβ€˜ran (,)) = ((TopOpenβ€˜β„‚fld) β†Ύt ℝ)
56 iccntr 24681 . . . . . . . 8 ((𝐴 ∈ ℝ ∧ 𝐡 ∈ ℝ) β†’ ((intβ€˜(topGenβ€˜ran (,)))β€˜(𝐴[,]𝐡)) = (𝐴(,)𝐡))
571, 2, 56syl2anc 583 . . . . . . 7 (πœ‘ β†’ ((intβ€˜(topGenβ€˜ran (,)))β€˜(𝐴[,]𝐡)) = (𝐴(,)𝐡))
5824, 21, 54, 55, 4, 57dvmptntr 25847 . . . . . 6 (πœ‘ β†’ (ℝ D (𝑧 ∈ (𝐴[,]𝐡) ↦ ((((πΉβ€˜π΅) βˆ’ (πΉβ€˜π΄)) Β· (πΊβ€˜π‘§)) βˆ’ (((πΊβ€˜π΅) βˆ’ (πΊβ€˜π΄)) Β· (πΉβ€˜π‘§))))) = (ℝ D (𝑧 ∈ (𝐴(,)𝐡) ↦ ((((πΉβ€˜π΅) βˆ’ (πΉβ€˜π΄)) Β· (πΊβ€˜π‘§)) βˆ’ (((πΊβ€˜π΅) βˆ’ (πΊβ€˜π΄)) Β· (πΉβ€˜π‘§))))))
59 reelprrecn 11199 . . . . . . . 8 ℝ ∈ {ℝ, β„‚}
6059a1i 11 . . . . . . 7 (πœ‘ β†’ ℝ ∈ {ℝ, β„‚})
61 ioossicc 13411 . . . . . . . . 9 (𝐴(,)𝐡) βŠ† (𝐴[,]𝐡)
6261sseli 3971 . . . . . . . 8 (𝑧 ∈ (𝐴(,)𝐡) β†’ 𝑧 ∈ (𝐴[,]𝐡))
6362, 49sylan2 592 . . . . . . 7 ((πœ‘ ∧ 𝑧 ∈ (𝐴(,)𝐡)) β†’ (((πΉβ€˜π΅) βˆ’ (πΉβ€˜π΄)) Β· (πΊβ€˜π‘§)) ∈ β„‚)
64 ovex 7435 . . . . . . . 8 (((πΉβ€˜π΅) βˆ’ (πΉβ€˜π΄)) Β· ((ℝ D 𝐺)β€˜π‘§)) ∈ V
6564a1i 11 . . . . . . 7 ((πœ‘ ∧ 𝑧 ∈ (𝐴(,)𝐡)) β†’ (((πΉβ€˜π΅) βˆ’ (πΉβ€˜π΄)) Β· ((ℝ D 𝐺)β€˜π‘§)) ∈ V)
6662, 48sylan2 592 . . . . . . . 8 ((πœ‘ ∧ 𝑧 ∈ (𝐴(,)𝐡)) β†’ (πΊβ€˜π‘§) ∈ β„‚)
67 fvexd 6897 . . . . . . . 8 ((πœ‘ ∧ 𝑧 ∈ (𝐴(,)𝐡)) β†’ ((ℝ D 𝐺)β€˜π‘§) ∈ V)
6830oveq2d 7418 . . . . . . . . 9 (πœ‘ β†’ (ℝ D 𝐺) = (ℝ D (𝑧 ∈ (𝐴[,]𝐡) ↦ (πΊβ€˜π‘§))))
69 dvf 25780 . . . . . . . . . . 11 (ℝ D 𝐺):dom (ℝ D 𝐺)βŸΆβ„‚
70 cmvthOLD.dg . . . . . . . . . . . 12 (πœ‘ β†’ dom (ℝ D 𝐺) = (𝐴(,)𝐡))
7170feq2d 6694 . . . . . . . . . . 11 (πœ‘ β†’ ((ℝ D 𝐺):dom (ℝ D 𝐺)βŸΆβ„‚ ↔ (ℝ D 𝐺):(𝐴(,)𝐡)βŸΆβ„‚))
7269, 71mpbii 232 . . . . . . . . . 10 (πœ‘ β†’ (ℝ D 𝐺):(𝐴(,)𝐡)βŸΆβ„‚)
7372feqmptd 6951 . . . . . . . . 9 (πœ‘ β†’ (ℝ D 𝐺) = (𝑧 ∈ (𝐴(,)𝐡) ↦ ((ℝ D 𝐺)β€˜π‘§)))
7424, 21, 48, 55, 4, 57dvmptntr 25847 . . . . . . . . 9 (πœ‘ β†’ (ℝ D (𝑧 ∈ (𝐴[,]𝐡) ↦ (πΊβ€˜π‘§))) = (ℝ D (𝑧 ∈ (𝐴(,)𝐡) ↦ (πΊβ€˜π‘§))))
7568, 73, 743eqtr3rd 2773 . . . . . . . 8 (πœ‘ β†’ (ℝ D (𝑧 ∈ (𝐴(,)𝐡) ↦ (πΊβ€˜π‘§))) = (𝑧 ∈ (𝐴(,)𝐡) ↦ ((ℝ D 𝐺)β€˜π‘§)))
7660, 66, 67, 75, 45dvmptcmul 25840 . . . . . . 7 (πœ‘ β†’ (ℝ D (𝑧 ∈ (𝐴(,)𝐡) ↦ (((πΉβ€˜π΅) βˆ’ (πΉβ€˜π΄)) Β· (πΊβ€˜π‘§)))) = (𝑧 ∈ (𝐴(,)𝐡) ↦ (((πΉβ€˜π΅) βˆ’ (πΉβ€˜π΄)) Β· ((ℝ D 𝐺)β€˜π‘§))))
7762, 53sylan2 592 . . . . . . 7 ((πœ‘ ∧ 𝑧 ∈ (𝐴(,)𝐡)) β†’ (((πΊβ€˜π΅) βˆ’ (πΊβ€˜π΄)) Β· (πΉβ€˜π‘§)) ∈ β„‚)
78 ovex 7435 . . . . . . . 8 (((πΊβ€˜π΅) βˆ’ (πΊβ€˜π΄)) Β· ((ℝ D 𝐹)β€˜π‘§)) ∈ V
7978a1i 11 . . . . . . 7 ((πœ‘ ∧ 𝑧 ∈ (𝐴(,)𝐡)) β†’ (((πΊβ€˜π΅) βˆ’ (πΊβ€˜π΄)) Β· ((ℝ D 𝐹)β€˜π‘§)) ∈ V)
8051recnd 11241 . . . . . . . . 9 ((πœ‘ ∧ 𝑧 ∈ (𝐴[,]𝐡)) β†’ (πΉβ€˜π‘§) ∈ β„‚)
8162, 80sylan2 592 . . . . . . . 8 ((πœ‘ ∧ 𝑧 ∈ (𝐴(,)𝐡)) β†’ (πΉβ€˜π‘§) ∈ β„‚)
82 fvexd 6897 . . . . . . . 8 ((πœ‘ ∧ 𝑧 ∈ (𝐴(,)𝐡)) β†’ ((ℝ D 𝐹)β€˜π‘§) ∈ V)
8339oveq2d 7418 . . . . . . . . 9 (πœ‘ β†’ (ℝ D 𝐹) = (ℝ D (𝑧 ∈ (𝐴[,]𝐡) ↦ (πΉβ€˜π‘§))))
84 dvf 25780 . . . . . . . . . . 11 (ℝ D 𝐹):dom (ℝ D 𝐹)βŸΆβ„‚
85 cmvthOLD.df . . . . . . . . . . . 12 (πœ‘ β†’ dom (ℝ D 𝐹) = (𝐴(,)𝐡))
8685feq2d 6694 . . . . . . . . . . 11 (πœ‘ β†’ ((ℝ D 𝐹):dom (ℝ D 𝐹)βŸΆβ„‚ ↔ (ℝ D 𝐹):(𝐴(,)𝐡)βŸΆβ„‚))
8784, 86mpbii 232 . . . . . . . . . 10 (πœ‘ β†’ (ℝ D 𝐹):(𝐴(,)𝐡)βŸΆβ„‚)
8887feqmptd 6951 . . . . . . . . 9 (πœ‘ β†’ (ℝ D 𝐹) = (𝑧 ∈ (𝐴(,)𝐡) ↦ ((ℝ D 𝐹)β€˜π‘§)))
8924, 21, 80, 55, 4, 57dvmptntr 25847 . . . . . . . . 9 (πœ‘ β†’ (ℝ D (𝑧 ∈ (𝐴[,]𝐡) ↦ (πΉβ€˜π‘§))) = (ℝ D (𝑧 ∈ (𝐴(,)𝐡) ↦ (πΉβ€˜π‘§))))
9083, 88, 893eqtr3rd 2773 . . . . . . . 8 (πœ‘ β†’ (ℝ D (𝑧 ∈ (𝐴(,)𝐡) ↦ (πΉβ€˜π‘§))) = (𝑧 ∈ (𝐴(,)𝐡) ↦ ((ℝ D 𝐹)β€˜π‘§)))
9136recnd 11241 . . . . . . . 8 (πœ‘ β†’ ((πΊβ€˜π΅) βˆ’ (πΊβ€˜π΄)) ∈ β„‚)
9260, 81, 82, 90, 91dvmptcmul 25840 . . . . . . 7 (πœ‘ β†’ (ℝ D (𝑧 ∈ (𝐴(,)𝐡) ↦ (((πΊβ€˜π΅) βˆ’ (πΊβ€˜π΄)) Β· (πΉβ€˜π‘§)))) = (𝑧 ∈ (𝐴(,)𝐡) ↦ (((πΊβ€˜π΅) βˆ’ (πΊβ€˜π΄)) Β· ((ℝ D 𝐹)β€˜π‘§))))
9360, 63, 65, 76, 77, 79, 92dvmptsub 25843 . . . . . 6 (πœ‘ β†’ (ℝ D (𝑧 ∈ (𝐴(,)𝐡) ↦ ((((πΉβ€˜π΅) βˆ’ (πΉβ€˜π΄)) Β· (πΊβ€˜π‘§)) βˆ’ (((πΊβ€˜π΅) βˆ’ (πΊβ€˜π΄)) Β· (πΉβ€˜π‘§))))) = (𝑧 ∈ (𝐴(,)𝐡) ↦ ((((πΉβ€˜π΅) βˆ’ (πΉβ€˜π΄)) Β· ((ℝ D 𝐺)β€˜π‘§)) βˆ’ (((πΊβ€˜π΅) βˆ’ (πΊβ€˜π΄)) Β· ((ℝ D 𝐹)β€˜π‘§)))))
9458, 93eqtrd 2764 . . . . 5 (πœ‘ β†’ (ℝ D (𝑧 ∈ (𝐴[,]𝐡) ↦ ((((πΉβ€˜π΅) βˆ’ (πΉβ€˜π΄)) Β· (πΊβ€˜π‘§)) βˆ’ (((πΊβ€˜π΅) βˆ’ (πΊβ€˜π΄)) Β· (πΉβ€˜π‘§))))) = (𝑧 ∈ (𝐴(,)𝐡) ↦ ((((πΉβ€˜π΅) βˆ’ (πΉβ€˜π΄)) Β· ((ℝ D 𝐺)β€˜π‘§)) βˆ’ (((πΊβ€˜π΅) βˆ’ (πΊβ€˜π΄)) Β· ((ℝ D 𝐹)β€˜π‘§)))))
9594dmeqd 5896 . . . 4 (πœ‘ β†’ dom (ℝ D (𝑧 ∈ (𝐴[,]𝐡) ↦ ((((πΉβ€˜π΅) βˆ’ (πΉβ€˜π΄)) Β· (πΊβ€˜π‘§)) βˆ’ (((πΊβ€˜π΅) βˆ’ (πΊβ€˜π΄)) Β· (πΉβ€˜π‘§))))) = dom (𝑧 ∈ (𝐴(,)𝐡) ↦ ((((πΉβ€˜π΅) βˆ’ (πΉβ€˜π΄)) Β· ((ℝ D 𝐺)β€˜π‘§)) βˆ’ (((πΊβ€˜π΅) βˆ’ (πΊβ€˜π΄)) Β· ((ℝ D 𝐹)β€˜π‘§)))))
96 ovex 7435 . . . . 5 ((((πΉβ€˜π΅) βˆ’ (πΉβ€˜π΄)) Β· ((ℝ D 𝐺)β€˜π‘§)) βˆ’ (((πΊβ€˜π΅) βˆ’ (πΊβ€˜π΄)) Β· ((ℝ D 𝐹)β€˜π‘§))) ∈ V
97 eqid 2724 . . . . 5 (𝑧 ∈ (𝐴(,)𝐡) ↦ ((((πΉβ€˜π΅) βˆ’ (πΉβ€˜π΄)) Β· ((ℝ D 𝐺)β€˜π‘§)) βˆ’ (((πΊβ€˜π΅) βˆ’ (πΊβ€˜π΄)) Β· ((ℝ D 𝐹)β€˜π‘§)))) = (𝑧 ∈ (𝐴(,)𝐡) ↦ ((((πΉβ€˜π΅) βˆ’ (πΉβ€˜π΄)) Β· ((ℝ D 𝐺)β€˜π‘§)) βˆ’ (((πΊβ€˜π΅) βˆ’ (πΊβ€˜π΄)) Β· ((ℝ D 𝐹)β€˜π‘§))))
9896, 97dmmpti 6685 . . . 4 dom (𝑧 ∈ (𝐴(,)𝐡) ↦ ((((πΉβ€˜π΅) βˆ’ (πΉβ€˜π΄)) Β· ((ℝ D 𝐺)β€˜π‘§)) βˆ’ (((πΊβ€˜π΅) βˆ’ (πΊβ€˜π΄)) Β· ((ℝ D 𝐹)β€˜π‘§)))) = (𝐴(,)𝐡)
9995, 98eqtrdi 2780 . . 3 (πœ‘ β†’ dom (ℝ D (𝑧 ∈ (𝐴[,]𝐡) ↦ ((((πΉβ€˜π΅) βˆ’ (πΉβ€˜π΄)) Β· (πΊβ€˜π‘§)) βˆ’ (((πΊβ€˜π΅) βˆ’ (πΊβ€˜π΄)) Β· (πΉβ€˜π‘§))))) = (𝐴(,)𝐡))
10015recnd 11241 . . . . . . . 8 (πœ‘ β†’ (πΉβ€˜π΅) ∈ β„‚)
10135recnd 11241 . . . . . . . 8 (πœ‘ β†’ (πΊβ€˜π΄) ∈ β„‚)
102100, 101mulcld 11233 . . . . . . 7 (πœ‘ β†’ ((πΉβ€˜π΅) Β· (πΊβ€˜π΄)) ∈ β„‚)
10318recnd 11241 . . . . . . . 8 (πœ‘ β†’ (πΉβ€˜π΄) ∈ β„‚)
10434recnd 11241 . . . . . . . 8 (πœ‘ β†’ (πΊβ€˜π΅) ∈ β„‚)
105103, 104mulcld 11233 . . . . . . 7 (πœ‘ β†’ ((πΉβ€˜π΄) Β· (πΊβ€˜π΅)) ∈ β„‚)
106103, 101mulcld 11233 . . . . . . 7 (πœ‘ β†’ ((πΉβ€˜π΄) Β· (πΊβ€˜π΄)) ∈ β„‚)
107102, 105, 106nnncan2d 11605 . . . . . 6 (πœ‘ β†’ ((((πΉβ€˜π΅) Β· (πΊβ€˜π΄)) βˆ’ ((πΉβ€˜π΄) Β· (πΊβ€˜π΄))) βˆ’ (((πΉβ€˜π΄) Β· (πΊβ€˜π΅)) βˆ’ ((πΉβ€˜π΄) Β· (πΊβ€˜π΄)))) = (((πΉβ€˜π΅) Β· (πΊβ€˜π΄)) βˆ’ ((πΉβ€˜π΄) Β· (πΊβ€˜π΅))))
108100, 104mulcld 11233 . . . . . . 7 (πœ‘ β†’ ((πΉβ€˜π΅) Β· (πΊβ€˜π΅)) ∈ β„‚)
109108, 105, 102nnncan1d 11604 . . . . . 6 (πœ‘ β†’ ((((πΉβ€˜π΅) Β· (πΊβ€˜π΅)) βˆ’ ((πΉβ€˜π΄) Β· (πΊβ€˜π΅))) βˆ’ (((πΉβ€˜π΅) Β· (πΊβ€˜π΅)) βˆ’ ((πΉβ€˜π΅) Β· (πΊβ€˜π΄)))) = (((πΉβ€˜π΅) Β· (πΊβ€˜π΄)) βˆ’ ((πΉβ€˜π΄) Β· (πΊβ€˜π΅))))
110107, 109eqtr4d 2767 . . . . 5 (πœ‘ β†’ ((((πΉβ€˜π΅) Β· (πΊβ€˜π΄)) βˆ’ ((πΉβ€˜π΄) Β· (πΊβ€˜π΄))) βˆ’ (((πΉβ€˜π΄) Β· (πΊβ€˜π΅)) βˆ’ ((πΉβ€˜π΄) Β· (πΊβ€˜π΄)))) = ((((πΉβ€˜π΅) Β· (πΊβ€˜π΅)) βˆ’ ((πΉβ€˜π΄) Β· (πΊβ€˜π΅))) βˆ’ (((πΉβ€˜π΅) Β· (πΊβ€˜π΅)) βˆ’ ((πΉβ€˜π΅) Β· (πΊβ€˜π΄)))))
111100, 103, 101subdird 11670 . . . . . 6 (πœ‘ β†’ (((πΉβ€˜π΅) βˆ’ (πΉβ€˜π΄)) Β· (πΊβ€˜π΄)) = (((πΉβ€˜π΅) Β· (πΊβ€˜π΄)) βˆ’ ((πΉβ€˜π΄) Β· (πΊβ€˜π΄))))
11291, 103mulcomd 11234 . . . . . . 7 (πœ‘ β†’ (((πΊβ€˜π΅) βˆ’ (πΊβ€˜π΄)) Β· (πΉβ€˜π΄)) = ((πΉβ€˜π΄) Β· ((πΊβ€˜π΅) βˆ’ (πΊβ€˜π΄))))
113103, 104, 101subdid 11669 . . . . . . 7 (πœ‘ β†’ ((πΉβ€˜π΄) Β· ((πΊβ€˜π΅) βˆ’ (πΊβ€˜π΄))) = (((πΉβ€˜π΄) Β· (πΊβ€˜π΅)) βˆ’ ((πΉβ€˜π΄) Β· (πΊβ€˜π΄))))
114112, 113eqtrd 2764 . . . . . 6 (πœ‘ β†’ (((πΊβ€˜π΅) βˆ’ (πΊβ€˜π΄)) Β· (πΉβ€˜π΄)) = (((πΉβ€˜π΄) Β· (πΊβ€˜π΅)) βˆ’ ((πΉβ€˜π΄) Β· (πΊβ€˜π΄))))
115111, 114oveq12d 7420 . . . . 5 (πœ‘ β†’ ((((πΉβ€˜π΅) βˆ’ (πΉβ€˜π΄)) Β· (πΊβ€˜π΄)) βˆ’ (((πΊβ€˜π΅) βˆ’ (πΊβ€˜π΄)) Β· (πΉβ€˜π΄))) = ((((πΉβ€˜π΅) Β· (πΊβ€˜π΄)) βˆ’ ((πΉβ€˜π΄) Β· (πΊβ€˜π΄))) βˆ’ (((πΉβ€˜π΄) Β· (πΊβ€˜π΅)) βˆ’ ((πΉβ€˜π΄) Β· (πΊβ€˜π΄)))))
116100, 103, 104subdird 11670 . . . . . 6 (πœ‘ β†’ (((πΉβ€˜π΅) βˆ’ (πΉβ€˜π΄)) Β· (πΊβ€˜π΅)) = (((πΉβ€˜π΅) Β· (πΊβ€˜π΅)) βˆ’ ((πΉβ€˜π΄) Β· (πΊβ€˜π΅))))
11791, 100mulcomd 11234 . . . . . . 7 (πœ‘ β†’ (((πΊβ€˜π΅) βˆ’ (πΊβ€˜π΄)) Β· (πΉβ€˜π΅)) = ((πΉβ€˜π΅) Β· ((πΊβ€˜π΅) βˆ’ (πΊβ€˜π΄))))
118100, 104, 101subdid 11669 . . . . . . 7 (πœ‘ β†’ ((πΉβ€˜π΅) Β· ((πΊβ€˜π΅) βˆ’ (πΊβ€˜π΄))) = (((πΉβ€˜π΅) Β· (πΊβ€˜π΅)) βˆ’ ((πΉβ€˜π΅) Β· (πΊβ€˜π΄))))
119117, 118eqtrd 2764 . . . . . 6 (πœ‘ β†’ (((πΊβ€˜π΅) βˆ’ (πΊβ€˜π΄)) Β· (πΉβ€˜π΅)) = (((πΉβ€˜π΅) Β· (πΊβ€˜π΅)) βˆ’ ((πΉβ€˜π΅) Β· (πΊβ€˜π΄))))
120116, 119oveq12d 7420 . . . . 5 (πœ‘ β†’ ((((πΉβ€˜π΅) βˆ’ (πΉβ€˜π΄)) Β· (πΊβ€˜π΅)) βˆ’ (((πΊβ€˜π΅) βˆ’ (πΊβ€˜π΄)) Β· (πΉβ€˜π΅))) = ((((πΉβ€˜π΅) Β· (πΊβ€˜π΅)) βˆ’ ((πΉβ€˜π΄) Β· (πΊβ€˜π΅))) βˆ’ (((πΉβ€˜π΅) Β· (πΊβ€˜π΅)) βˆ’ ((πΉβ€˜π΅) Β· (πΊβ€˜π΄)))))
121110, 115, 1203eqtr4d 2774 . . . 4 (πœ‘ β†’ ((((πΉβ€˜π΅) βˆ’ (πΉβ€˜π΄)) Β· (πΊβ€˜π΄)) βˆ’ (((πΊβ€˜π΅) βˆ’ (πΊβ€˜π΄)) Β· (πΉβ€˜π΄))) = ((((πΉβ€˜π΅) βˆ’ (πΉβ€˜π΄)) Β· (πΊβ€˜π΅)) βˆ’ (((πΊβ€˜π΅) βˆ’ (πΊβ€˜π΄)) Β· (πΉβ€˜π΅))))
122 fveq2 6882 . . . . . . . 8 (𝑧 = 𝐴 β†’ (πΊβ€˜π‘§) = (πΊβ€˜π΄))
123122oveq2d 7418 . . . . . . 7 (𝑧 = 𝐴 β†’ (((πΉβ€˜π΅) βˆ’ (πΉβ€˜π΄)) Β· (πΊβ€˜π‘§)) = (((πΉβ€˜π΅) βˆ’ (πΉβ€˜π΄)) Β· (πΊβ€˜π΄)))
124 fveq2 6882 . . . . . . . 8 (𝑧 = 𝐴 β†’ (πΉβ€˜π‘§) = (πΉβ€˜π΄))
125124oveq2d 7418 . . . . . . 7 (𝑧 = 𝐴 β†’ (((πΊβ€˜π΅) βˆ’ (πΊβ€˜π΄)) Β· (πΉβ€˜π‘§)) = (((πΊβ€˜π΅) βˆ’ (πΊβ€˜π΄)) Β· (πΉβ€˜π΄)))
126123, 125oveq12d 7420 . . . . . 6 (𝑧 = 𝐴 β†’ ((((πΉβ€˜π΅) βˆ’ (πΉβ€˜π΄)) Β· (πΊβ€˜π‘§)) βˆ’ (((πΊβ€˜π΅) βˆ’ (πΊβ€˜π΄)) Β· (πΉβ€˜π‘§))) = ((((πΉβ€˜π΅) βˆ’ (πΉβ€˜π΄)) Β· (πΊβ€˜π΄)) βˆ’ (((πΊβ€˜π΅) βˆ’ (πΊβ€˜π΄)) Β· (πΉβ€˜π΄))))
127 eqid 2724 . . . . . 6 (𝑧 ∈ (𝐴[,]𝐡) ↦ ((((πΉβ€˜π΅) βˆ’ (πΉβ€˜π΄)) Β· (πΊβ€˜π‘§)) βˆ’ (((πΊβ€˜π΅) βˆ’ (πΊβ€˜π΄)) Β· (πΉβ€˜π‘§)))) = (𝑧 ∈ (𝐴[,]𝐡) ↦ ((((πΉβ€˜π΅) βˆ’ (πΉβ€˜π΄)) Β· (πΊβ€˜π‘§)) βˆ’ (((πΊβ€˜π΅) βˆ’ (πΊβ€˜π΄)) Β· (πΉβ€˜π‘§))))
128 ovex 7435 . . . . . 6 ((((πΉβ€˜π΅) βˆ’ (πΉβ€˜π΄)) Β· (πΊβ€˜π‘§)) βˆ’ (((πΊβ€˜π΅) βˆ’ (πΊβ€˜π΄)) Β· (πΉβ€˜π‘§))) ∈ V
129126, 127, 128fvmpt3i 6994 . . . . 5 (𝐴 ∈ (𝐴[,]𝐡) β†’ ((𝑧 ∈ (𝐴[,]𝐡) ↦ ((((πΉβ€˜π΅) βˆ’ (πΉβ€˜π΄)) Β· (πΊβ€˜π‘§)) βˆ’ (((πΊβ€˜π΅) βˆ’ (πΊβ€˜π΄)) Β· (πΉβ€˜π‘§))))β€˜π΄) = ((((πΉβ€˜π΅) βˆ’ (πΉβ€˜π΄)) Β· (πΊβ€˜π΄)) βˆ’ (((πΊβ€˜π΅) βˆ’ (πΊβ€˜π΄)) Β· (πΉβ€˜π΄))))
13017, 129syl 17 . . . 4 (πœ‘ β†’ ((𝑧 ∈ (𝐴[,]𝐡) ↦ ((((πΉβ€˜π΅) βˆ’ (πΉβ€˜π΄)) Β· (πΊβ€˜π‘§)) βˆ’ (((πΊβ€˜π΅) βˆ’ (πΊβ€˜π΄)) Β· (πΉβ€˜π‘§))))β€˜π΄) = ((((πΉβ€˜π΅) βˆ’ (πΉβ€˜π΄)) Β· (πΊβ€˜π΄)) βˆ’ (((πΊβ€˜π΅) βˆ’ (πΊβ€˜π΄)) Β· (πΉβ€˜π΄))))
131 fveq2 6882 . . . . . . . 8 (𝑧 = 𝐡 β†’ (πΊβ€˜π‘§) = (πΊβ€˜π΅))
132131oveq2d 7418 . . . . . . 7 (𝑧 = 𝐡 β†’ (((πΉβ€˜π΅) βˆ’ (πΉβ€˜π΄)) Β· (πΊβ€˜π‘§)) = (((πΉβ€˜π΅) βˆ’ (πΉβ€˜π΄)) Β· (πΊβ€˜π΅)))
133 fveq2 6882 . . . . . . . 8 (𝑧 = 𝐡 β†’ (πΉβ€˜π‘§) = (πΉβ€˜π΅))
134133oveq2d 7418 . . . . . . 7 (𝑧 = 𝐡 β†’ (((πΊβ€˜π΅) βˆ’ (πΊβ€˜π΄)) Β· (πΉβ€˜π‘§)) = (((πΊβ€˜π΅) βˆ’ (πΊβ€˜π΄)) Β· (πΉβ€˜π΅)))
135132, 134oveq12d 7420 . . . . . 6 (𝑧 = 𝐡 β†’ ((((πΉβ€˜π΅) βˆ’ (πΉβ€˜π΄)) Β· (πΊβ€˜π‘§)) βˆ’ (((πΊβ€˜π΅) βˆ’ (πΊβ€˜π΄)) Β· (πΉβ€˜π‘§))) = ((((πΉβ€˜π΅) βˆ’ (πΉβ€˜π΄)) Β· (πΊβ€˜π΅)) βˆ’ (((πΊβ€˜π΅) βˆ’ (πΊβ€˜π΄)) Β· (πΉβ€˜π΅))))
136135, 127, 128fvmpt3i 6994 . . . . 5 (𝐡 ∈ (𝐴[,]𝐡) β†’ ((𝑧 ∈ (𝐴[,]𝐡) ↦ ((((πΉβ€˜π΅) βˆ’ (πΉβ€˜π΄)) Β· (πΊβ€˜π‘§)) βˆ’ (((πΊβ€˜π΅) βˆ’ (πΊβ€˜π΄)) Β· (πΉβ€˜π‘§))))β€˜π΅) = ((((πΉβ€˜π΅) βˆ’ (πΉβ€˜π΄)) Β· (πΊβ€˜π΅)) βˆ’ (((πΊβ€˜π΅) βˆ’ (πΊβ€˜π΄)) Β· (πΉβ€˜π΅))))
13714, 136syl 17 . . . 4 (πœ‘ β†’ ((𝑧 ∈ (𝐴[,]𝐡) ↦ ((((πΉβ€˜π΅) βˆ’ (πΉβ€˜π΄)) Β· (πΊβ€˜π‘§)) βˆ’ (((πΊβ€˜π΅) βˆ’ (πΊβ€˜π΄)) Β· (πΉβ€˜π‘§))))β€˜π΅) = ((((πΉβ€˜π΅) βˆ’ (πΉβ€˜π΄)) Β· (πΊβ€˜π΅)) βˆ’ (((πΊβ€˜π΅) βˆ’ (πΊβ€˜π΄)) Β· (πΉβ€˜π΅))))
138121, 130, 1373eqtr4d 2774 . . 3 (πœ‘ β†’ ((𝑧 ∈ (𝐴[,]𝐡) ↦ ((((πΉβ€˜π΅) βˆ’ (πΉβ€˜π΄)) Β· (πΊβ€˜π‘§)) βˆ’ (((πΊβ€˜π΅) βˆ’ (πΊβ€˜π΄)) Β· (πΉβ€˜π‘§))))β€˜π΄) = ((𝑧 ∈ (𝐴[,]𝐡) ↦ ((((πΉβ€˜π΅) βˆ’ (πΉβ€˜π΄)) Β· (πΊβ€˜π‘§)) βˆ’ (((πΊβ€˜π΅) βˆ’ (πΊβ€˜π΄)) Β· (πΉβ€˜π‘§))))β€˜π΅))
1391, 2, 3, 44, 99, 138rolle 25866 . 2 (πœ‘ β†’ βˆƒπ‘₯ ∈ (𝐴(,)𝐡)((ℝ D (𝑧 ∈ (𝐴[,]𝐡) ↦ ((((πΉβ€˜π΅) βˆ’ (πΉβ€˜π΄)) Β· (πΊβ€˜π‘§)) βˆ’ (((πΊβ€˜π΅) βˆ’ (πΊβ€˜π΄)) Β· (πΉβ€˜π‘§)))))β€˜π‘₯) = 0)
14094fveq1d 6884 . . . . . 6 (πœ‘ β†’ ((ℝ D (𝑧 ∈ (𝐴[,]𝐡) ↦ ((((πΉβ€˜π΅) βˆ’ (πΉβ€˜π΄)) Β· (πΊβ€˜π‘§)) βˆ’ (((πΊβ€˜π΅) βˆ’ (πΊβ€˜π΄)) Β· (πΉβ€˜π‘§)))))β€˜π‘₯) = ((𝑧 ∈ (𝐴(,)𝐡) ↦ ((((πΉβ€˜π΅) βˆ’ (πΉβ€˜π΄)) Β· ((ℝ D 𝐺)β€˜π‘§)) βˆ’ (((πΊβ€˜π΅) βˆ’ (πΊβ€˜π΄)) Β· ((ℝ D 𝐹)β€˜π‘§))))β€˜π‘₯))
141 fveq2 6882 . . . . . . . . 9 (𝑧 = π‘₯ β†’ ((ℝ D 𝐺)β€˜π‘§) = ((ℝ D 𝐺)β€˜π‘₯))
142141oveq2d 7418 . . . . . . . 8 (𝑧 = π‘₯ β†’ (((πΉβ€˜π΅) βˆ’ (πΉβ€˜π΄)) Β· ((ℝ D 𝐺)β€˜π‘§)) = (((πΉβ€˜π΅) βˆ’ (πΉβ€˜π΄)) Β· ((ℝ D 𝐺)β€˜π‘₯)))
143 fveq2 6882 . . . . . . . . 9 (𝑧 = π‘₯ β†’ ((ℝ D 𝐹)β€˜π‘§) = ((ℝ D 𝐹)β€˜π‘₯))
144143oveq2d 7418 . . . . . . . 8 (𝑧 = π‘₯ β†’ (((πΊβ€˜π΅) βˆ’ (πΊβ€˜π΄)) Β· ((ℝ D 𝐹)β€˜π‘§)) = (((πΊβ€˜π΅) βˆ’ (πΊβ€˜π΄)) Β· ((ℝ D 𝐹)β€˜π‘₯)))
145142, 144oveq12d 7420 . . . . . . 7 (𝑧 = π‘₯ β†’ ((((πΉβ€˜π΅) βˆ’ (πΉβ€˜π΄)) Β· ((ℝ D 𝐺)β€˜π‘§)) βˆ’ (((πΊβ€˜π΅) βˆ’ (πΊβ€˜π΄)) Β· ((ℝ D 𝐹)β€˜π‘§))) = ((((πΉβ€˜π΅) βˆ’ (πΉβ€˜π΄)) Β· ((ℝ D 𝐺)β€˜π‘₯)) βˆ’ (((πΊβ€˜π΅) βˆ’ (πΊβ€˜π΄)) Β· ((ℝ D 𝐹)β€˜π‘₯))))
146145, 97, 96fvmpt3i 6994 . . . . . 6 (π‘₯ ∈ (𝐴(,)𝐡) β†’ ((𝑧 ∈ (𝐴(,)𝐡) ↦ ((((πΉβ€˜π΅) βˆ’ (πΉβ€˜π΄)) Β· ((ℝ D 𝐺)β€˜π‘§)) βˆ’ (((πΊβ€˜π΅) βˆ’ (πΊβ€˜π΄)) Β· ((ℝ D 𝐹)β€˜π‘§))))β€˜π‘₯) = ((((πΉβ€˜π΅) βˆ’ (πΉβ€˜π΄)) Β· ((ℝ D 𝐺)β€˜π‘₯)) βˆ’ (((πΊβ€˜π΅) βˆ’ (πΊβ€˜π΄)) Β· ((ℝ D 𝐹)β€˜π‘₯))))
147140, 146sylan9eq 2784 . . . . 5 ((πœ‘ ∧ π‘₯ ∈ (𝐴(,)𝐡)) β†’ ((ℝ D (𝑧 ∈ (𝐴[,]𝐡) ↦ ((((πΉβ€˜π΅) βˆ’ (πΉβ€˜π΄)) Β· (πΊβ€˜π‘§)) βˆ’ (((πΊβ€˜π΅) βˆ’ (πΊβ€˜π΄)) Β· (πΉβ€˜π‘§)))))β€˜π‘₯) = ((((πΉβ€˜π΅) βˆ’ (πΉβ€˜π΄)) Β· ((ℝ D 𝐺)β€˜π‘₯)) βˆ’ (((πΊβ€˜π΅) βˆ’ (πΊβ€˜π΄)) Β· ((ℝ D 𝐹)β€˜π‘₯))))
148147eqeq1d 2726 . . . 4 ((πœ‘ ∧ π‘₯ ∈ (𝐴(,)𝐡)) β†’ (((ℝ D (𝑧 ∈ (𝐴[,]𝐡) ↦ ((((πΉβ€˜π΅) βˆ’ (πΉβ€˜π΄)) Β· (πΊβ€˜π‘§)) βˆ’ (((πΊβ€˜π΅) βˆ’ (πΊβ€˜π΄)) Β· (πΉβ€˜π‘§)))))β€˜π‘₯) = 0 ↔ ((((πΉβ€˜π΅) βˆ’ (πΉβ€˜π΄)) Β· ((ℝ D 𝐺)β€˜π‘₯)) βˆ’ (((πΊβ€˜π΅) βˆ’ (πΊβ€˜π΄)) Β· ((ℝ D 𝐹)β€˜π‘₯))) = 0))
14945adantr 480 . . . . . 6 ((πœ‘ ∧ π‘₯ ∈ (𝐴(,)𝐡)) β†’ ((πΉβ€˜π΅) βˆ’ (πΉβ€˜π΄)) ∈ β„‚)
15072ffvelcdmda 7077 . . . . . 6 ((πœ‘ ∧ π‘₯ ∈ (𝐴(,)𝐡)) β†’ ((ℝ D 𝐺)β€˜π‘₯) ∈ β„‚)
151149, 150mulcld 11233 . . . . 5 ((πœ‘ ∧ π‘₯ ∈ (𝐴(,)𝐡)) β†’ (((πΉβ€˜π΅) βˆ’ (πΉβ€˜π΄)) Β· ((ℝ D 𝐺)β€˜π‘₯)) ∈ β„‚)
15291adantr 480 . . . . . 6 ((πœ‘ ∧ π‘₯ ∈ (𝐴(,)𝐡)) β†’ ((πΊβ€˜π΅) βˆ’ (πΊβ€˜π΄)) ∈ β„‚)
15387ffvelcdmda 7077 . . . . . 6 ((πœ‘ ∧ π‘₯ ∈ (𝐴(,)𝐡)) β†’ ((ℝ D 𝐹)β€˜π‘₯) ∈ β„‚)
154152, 153mulcld 11233 . . . . 5 ((πœ‘ ∧ π‘₯ ∈ (𝐴(,)𝐡)) β†’ (((πΊβ€˜π΅) βˆ’ (πΊβ€˜π΄)) Β· ((ℝ D 𝐹)β€˜π‘₯)) ∈ β„‚)
155151, 154subeq0ad 11580 . . . 4 ((πœ‘ ∧ π‘₯ ∈ (𝐴(,)𝐡)) β†’ (((((πΉβ€˜π΅) βˆ’ (πΉβ€˜π΄)) Β· ((ℝ D 𝐺)β€˜π‘₯)) βˆ’ (((πΊβ€˜π΅) βˆ’ (πΊβ€˜π΄)) Β· ((ℝ D 𝐹)β€˜π‘₯))) = 0 ↔ (((πΉβ€˜π΅) βˆ’ (πΉβ€˜π΄)) Β· ((ℝ D 𝐺)β€˜π‘₯)) = (((πΊβ€˜π΅) βˆ’ (πΊβ€˜π΄)) Β· ((ℝ D 𝐹)β€˜π‘₯))))
156148, 155bitrd 279 . . 3 ((πœ‘ ∧ π‘₯ ∈ (𝐴(,)𝐡)) β†’ (((ℝ D (𝑧 ∈ (𝐴[,]𝐡) ↦ ((((πΉβ€˜π΅) βˆ’ (πΉβ€˜π΄)) Β· (πΊβ€˜π‘§)) βˆ’ (((πΊβ€˜π΅) βˆ’ (πΊβ€˜π΄)) Β· (πΉβ€˜π‘§)))))β€˜π‘₯) = 0 ↔ (((πΉβ€˜π΅) βˆ’ (πΉβ€˜π΄)) Β· ((ℝ D 𝐺)β€˜π‘₯)) = (((πΊβ€˜π΅) βˆ’ (πΊβ€˜π΄)) Β· ((ℝ D 𝐹)β€˜π‘₯))))
157156rexbidva 3168 . 2 (πœ‘ β†’ (βˆƒπ‘₯ ∈ (𝐴(,)𝐡)((ℝ D (𝑧 ∈ (𝐴[,]𝐡) ↦ ((((πΉβ€˜π΅) βˆ’ (πΉβ€˜π΄)) Β· (πΊβ€˜π‘§)) βˆ’ (((πΊβ€˜π΅) βˆ’ (πΊβ€˜π΄)) Β· (πΉβ€˜π‘§)))))β€˜π‘₯) = 0 ↔ βˆƒπ‘₯ ∈ (𝐴(,)𝐡)(((πΉβ€˜π΅) βˆ’ (πΉβ€˜π΄)) Β· ((ℝ D 𝐺)β€˜π‘₯)) = (((πΊβ€˜π΅) βˆ’ (πΊβ€˜π΄)) Β· ((ℝ D 𝐹)β€˜π‘₯))))
158139, 157mpbid 231 1 (πœ‘ β†’ βˆƒπ‘₯ ∈ (𝐴(,)𝐡)(((πΉβ€˜π΅) βˆ’ (πΉβ€˜π΄)) Β· ((ℝ D 𝐺)β€˜π‘₯)) = (((πΊβ€˜π΅) βˆ’ (πΊβ€˜π΄)) Β· ((ℝ D 𝐹)β€˜π‘₯)))
Colors of variables: wff setvar class
Syntax hints:   β†’ wi 4   ∧ wa 395   = wceq 1533   ∈ wcel 2098  βˆƒwrex 3062  Vcvv 3466   βŠ† wss 3941  {cpr 4623   class class class wbr 5139   ↦ cmpt 5222  dom cdm 5667  ran crn 5668  βŸΆwf 6530  β€˜cfv 6534  (class class class)co 7402  β„‚cc 11105  β„cr 11106  0cc0 11107   Β· cmul 11112  β„*cxr 11246   < clt 11247   ≀ cle 11248   βˆ’ cmin 11443  (,)cioo 13325  [,]cicc 13328  TopOpenctopn 17372  topGenctg 17388  β„‚fldccnfld 21234  intcnt 22865  β€“cnβ†’ccncf 24740   D cdv 25736
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-10 2129  ax-11 2146  ax-12 2163  ax-ext 2695  ax-rep 5276  ax-sep 5290  ax-nul 5297  ax-pow 5354  ax-pr 5418  ax-un 7719  ax-cnex 11163  ax-resscn 11164  ax-1cn 11165  ax-icn 11166  ax-addcl 11167  ax-addrcl 11168  ax-mulcl 11169  ax-mulrcl 11170  ax-mulcom 11171  ax-addass 11172  ax-mulass 11173  ax-distr 11174  ax-i2m1 11175  ax-1ne0 11176  ax-1rid 11177  ax-rnegex 11178  ax-rrecex 11179  ax-cnre 11180  ax-pre-lttri 11181  ax-pre-lttrn 11182  ax-pre-ltadd 11183  ax-pre-mulgt0 11184  ax-pre-sup 11185  ax-addf 11186  ax-mulf 11187
This theorem depends on definitions:  df-bi 206  df-an 396  df-or 845  df-3or 1085  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-nf 1778  df-sb 2060  df-mo 2526  df-eu 2555  df-clab 2702  df-cleq 2716  df-clel 2802  df-nfc 2877  df-ne 2933  df-nel 3039  df-ral 3054  df-rex 3063  df-rmo 3368  df-reu 3369  df-rab 3425  df-v 3468  df-sbc 3771  df-csb 3887  df-dif 3944  df-un 3946  df-in 3948  df-ss 3958  df-pss 3960  df-nul 4316  df-if 4522  df-pw 4597  df-sn 4622  df-pr 4624  df-tp 4626  df-op 4628  df-uni 4901  df-int 4942  df-iun 4990  df-iin 4991  df-br 5140  df-opab 5202  df-mpt 5223  df-tr 5257  df-id 5565  df-eprel 5571  df-po 5579  df-so 5580  df-fr 5622  df-se 5623  df-we 5624  df-xp 5673  df-rel 5674  df-cnv 5675  df-co 5676  df-dm 5677  df-rn 5678  df-res 5679  df-ima 5680  df-pred 6291  df-ord 6358  df-on 6359  df-lim 6360  df-suc 6361  df-iota 6486  df-fun 6536  df-fn 6537  df-f 6538  df-f1 6539  df-fo 6540  df-f1o 6541  df-fv 6542  df-isom 6543  df-riota 7358  df-ov 7405  df-oprab 7406  df-mpo 7407  df-of 7664  df-om 7850  df-1st 7969  df-2nd 7970  df-supp 8142  df-frecs 8262  df-wrecs 8293  df-recs 8367  df-rdg 8406  df-1o 8462  df-2o 8463  df-er 8700  df-map 8819  df-pm 8820  df-ixp 8889  df-en 8937  df-dom 8938  df-sdom 8939  df-fin 8940  df-fsupp 9359  df-fi 9403  df-sup 9434  df-inf 9435  df-oi 9502  df-card 9931  df-pnf 11249  df-mnf 11250  df-xr 11251  df-ltxr 11252  df-le 11253  df-sub 11445  df-neg 11446  df-div 11871  df-nn 12212  df-2 12274  df-3 12275  df-4 12276  df-5 12277  df-6 12278  df-7 12279  df-8 12280  df-9 12281  df-n0 12472  df-z 12558  df-dec 12677  df-uz 12822  df-q 12932  df-rp 12976  df-xneg 13093  df-xadd 13094  df-xmul 13095  df-ioo 13329  df-ico 13331  df-icc 13332  df-fz 13486  df-fzo 13629  df-seq 13968  df-exp 14029  df-hash 14292  df-cj 15048  df-re 15049  df-im 15050  df-sqrt 15184  df-abs 15185  df-struct 17085  df-sets 17102  df-slot 17120  df-ndx 17132  df-base 17150  df-ress 17179  df-plusg 17215  df-mulr 17216  df-starv 17217  df-sca 17218  df-vsca 17219  df-ip 17220  df-tset 17221  df-ple 17222  df-ds 17224  df-unif 17225  df-hom 17226  df-cco 17227  df-rest 17373  df-topn 17374  df-0g 17392  df-gsum 17393  df-topgen 17394  df-pt 17395  df-prds 17398  df-xrs 17453  df-qtop 17458  df-imas 17459  df-xps 17461  df-mre 17535  df-mrc 17536  df-acs 17538  df-mgm 18569  df-sgrp 18648  df-mnd 18664  df-submnd 18710  df-mulg 18992  df-cntz 19229  df-cmn 19698  df-psmet 21226  df-xmet 21227  df-met 21228  df-bl 21229  df-mopn 21230  df-fbas 21231  df-fg 21232  df-cnfld 21235  df-top 22740  df-topon 22757  df-topsp 22779  df-bases 22793  df-cld 22867  df-ntr 22868  df-cls 22869  df-nei 22946  df-lp 22984  df-perf 22985  df-cn 23075  df-cnp 23076  df-haus 23163  df-cmp 23235  df-tx 23410  df-hmeo 23603  df-fil 23694  df-fm 23786  df-flim 23787  df-flf 23788  df-xms 24170  df-ms 24171  df-tms 24172  df-cncf 24742  df-limc 25739  df-dv 25740
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator