Theorem dvlipcn 22946

Description: A complex function with derivative bounded by M on an open ball is Lipschitz continuous with Lipschitz constant equal to M. (Contributed by Mario Carneiro, 18-Mar-2015.)

Hypotheses

Ref	Expression
dvlipcn.x	|- ( ph -> X C_ CC )
dvlipcn.f	|- ( ph -> F : X --> CC )
dvlipcn.a	|- ( ph -> A e. CC )
dvlipcn.r	|- ( ph -> R e. RR* )
dvlipcn.b	|- B = ( A ( ball ` ( abs o. - ) ) R )
dvlipcn.d	|- ( ph -> B C_ dom ( CC _D F ) )
dvlipcn.m	|- ( ph -> M e. RR )
dvlipcn.l	|- ( ( ph /\ x e. B ) -> ( abs ` ( ( CC _D F ) ` x ) ) <_ M )

Assertion

Ref	Expression
dvlipcn	|- ( ( ph /\ ( Y e. B /\ Z e. B ) ) -> ( abs ` ( ( F ` Y ) - ( F ` Z ) ) ) <_ ( M x. ( abs ` ( Y - Z ) ) ) )

Distinct variable groups:   x, B   x, F   x, M   ph, x

Allowed substitution hints:   A( x)   R( x)   X( x)   Y( x)   Z( x)

Proof of Theorem dvlipcn

Dummy variables t y z are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		1elunit 11751	. . 3 |- 1 e. ( 0 [,] 1 )
2		0elunit 11750	. . 3 |- 0 e. ( 0 [,] 1 )
3		0red 9644	. . . 4 |- ( ( ph /\ ( Y e. B /\ Z e. B ) ) -> 0 e. RR )
4		1red 9658	. . . 4 |- ( ( ph /\ ( Y e. B /\ Z e. B ) ) -> 1 e. RR )
5		dvlipcn.d	. . . . . . . . . . . . . 14 |- ( ph -> B C_ dom ( CC _D F ) )
6		ssid 3451	. . . . . . . . . . . . . . . 16 |- CC C_ CC
7	6	a1i 11	. . . . . . . . . . . . . . 15 |- ( ph -> CC C_ CC )
8		dvlipcn.f	. . . . . . . . . . . . . . 15 |- ( ph -> F : X --> CC )
9		dvlipcn.x	. . . . . . . . . . . . . . 15 |- ( ph -> X C_ CC )
10	7, 8, 9	dvbss 22856	. . . . . . . . . . . . . 14 |- ( ph -> dom ( CC _D F ) C_ X )
11	5, 10	sstrd 3442	. . . . . . . . . . . . 13 |- ( ph -> B C_ X )
12	11, 9	sstrd 3442	. . . . . . . . . . . 12 |- ( ph -> B C_ CC )
13	12	adantr 467	. . . . . . . . . . 11 |- ( ( ph /\ ( Y e. B /\ Z e. B ) ) -> B C_ CC )
14		simprl 764	. . . . . . . . . . 11 |- ( ( ph /\ ( Y e. B /\ Z e. B ) ) -> Y e. B )
15	13, 14	sseldd 3433	. . . . . . . . . 10 |- ( ( ph /\ ( Y e. B /\ Z e. B ) ) -> Y e. CC )
16	15	adantr 467	. . . . . . . . 9 |- ( ( ( ph /\ ( Y e. B /\ Z e. B ) ) /\ t e. ( 0 [,] 1 ) ) -> Y e. CC )
17		unitssre 11779	. . . . . . . . . . 11 |- ( 0 [,] 1 ) C_ RR
18		ax-resscn 9596	. . . . . . . . . . 11 |- RR C_ CC
19	17, 18	sstri 3441	. . . . . . . . . 10 |- ( 0 [,] 1 ) C_ CC
20		simpr 463	. . . . . . . . . 10 |- ( ( ( ph /\ ( Y e. B /\ Z e. B ) ) /\ t e. ( 0 [,] 1 ) ) -> t e. ( 0 [,] 1 ) )
21	19, 20	sseldi 3430	. . . . . . . . 9 |- ( ( ( ph /\ ( Y e. B /\ Z e. B ) ) /\ t e. ( 0 [,] 1 ) ) -> t e. CC )
22	16, 21	mulcomd 9664	. . . . . . . 8 |- ( ( ( ph /\ ( Y e. B /\ Z e. B ) ) /\ t e. ( 0 [,] 1 ) ) -> ( Y x. t ) = ( t x. Y ) )
23		simprr 766	. . . . . . . . . . 11 |- ( ( ph /\ ( Y e. B /\ Z e. B ) ) -> Z e. B )
24	13, 23	sseldd 3433	. . . . . . . . . 10 |- ( ( ph /\ ( Y e. B /\ Z e. B ) ) -> Z e. CC )
25	24	adantr 467	. . . . . . . . 9 |- ( ( ( ph /\ ( Y e. B /\ Z e. B ) ) /\ t e. ( 0 [,] 1 ) ) -> Z e. CC )
26		iirev 21957	. . . . . . . . . . 11 |- ( t e. ( 0 [,] 1 ) -> ( 1 - t ) e. ( 0 [,] 1 ) )
27	26	adantl 468	. . . . . . . . . 10 |- ( ( ( ph /\ ( Y e. B /\ Z e. B ) ) /\ t e. ( 0 [,] 1 ) ) -> ( 1 - t ) e. ( 0 [,] 1 ) )
28	19, 27	sseldi 3430	. . . . . . . . 9 |- ( ( ( ph /\ ( Y e. B /\ Z e. B ) ) /\ t e. ( 0 [,] 1 ) ) -> ( 1 - t ) e. CC )
29	25, 28	mulcomd 9664	. . . . . . . 8 |- ( ( ( ph /\ ( Y e. B /\ Z e. B ) ) /\ t e. ( 0 [,] 1 ) ) -> ( Z x. ( 1 - t ) ) = ( ( 1 - t ) x. Z ) )
30	22, 29	oveq12d 6308	. . . . . . 7 |- ( ( ( ph /\ ( Y e. B /\ Z e. B ) ) /\ t e. ( 0 [,] 1 ) ) -> ( ( Y x. t ) + ( Z x. ( 1 - t ) ) ) = ( ( t x. Y ) + ( ( 1 - t ) x. Z ) ) )
31		dvlipcn.a	. . . . . . . . 9 |- ( ph -> A e. CC )
32	31	ad2antrr 732	. . . . . . . 8 |- ( ( ( ph /\ ( Y e. B /\ Z e. B ) ) /\ t e. ( 0 [,] 1 ) ) -> A e. CC )
33		dvlipcn.r	. . . . . . . . 9 |- ( ph -> R e. RR* )
34	33	ad2antrr 732	. . . . . . . 8 |- ( ( ( ph /\ ( Y e. B /\ Z e. B ) ) /\ t e. ( 0 [,] 1 ) ) -> R e. RR* )
35	14	adantr 467	. . . . . . . 8 |- ( ( ( ph /\ ( Y e. B /\ Z e. B ) ) /\ t e. ( 0 [,] 1 ) ) -> Y e. B )
36	23	adantr 467	. . . . . . . 8 |- ( ( ( ph /\ ( Y e. B /\ Z e. B ) ) /\ t e. ( 0 [,] 1 ) ) -> Z e. B )
37		dvlipcn.b	. . . . . . . . 9 |- B = ( A ( ball ` ( abs o. - ) ) R )
38	37	blcvx 21816	. . . . . . . 8 |- ( ( ( A e. CC /\ R e. RR* ) /\ ( Y e. B /\ Z e. B /\ t e. ( 0 [,] 1 ) ) ) -> ( ( t x. Y ) + ( ( 1 - t ) x. Z ) ) e. B )
39	32, 34, 35, 36, 20, 38	syl23anc 1275	. . . . . . 7 |- ( ( ( ph /\ ( Y e. B /\ Z e. B ) ) /\ t e. ( 0 [,] 1 ) ) -> ( ( t x. Y ) + ( ( 1 - t ) x. Z ) ) e. B )
40	30, 39	eqeltrd 2529	. . . . . 6 |- ( ( ( ph /\ ( Y e. B /\ Z e. B ) ) /\ t e. ( 0 [,] 1 ) ) -> ( ( Y x. t ) + ( Z x. ( 1 - t ) ) ) e. B )
41		eqidd 2452	. . . . . 6 |- ( ( ph /\ ( Y e. B /\ Z e. B ) ) -> ( t e. ( 0 [,] 1 ) |-> ( ( Y x. t ) + ( Z x. ( 1 - t ) ) ) ) = ( t e. ( 0 [,] 1 ) |-> ( ( Y x. t ) + ( Z x. ( 1 - t ) ) ) ) )
42	8, 11	fssresd 5750	. . . . . . . . 9 |- ( ph -> ( F |` B ) : B --> CC )
43	42	feqmptd 5918	. . . . . . . 8 |- ( ph -> ( F |` B ) = ( z e. B |-> ( ( F |` B ) ` z ) ) )
44		fvres 5879	. . . . . . . . 9 |- ( z e. B -> ( ( F |` B ) ` z ) = ( F ` z ) )
45	44	mpteq2ia 4485	. . . . . . . 8 |- ( z e. B |-> ( ( F |` B ) ` z ) ) = ( z e. B |-> ( F ` z ) )
46	43, 45	syl6eq 2501	. . . . . . 7 |- ( ph -> ( F |` B ) = ( z e. B |-> ( F ` z ) ) )
47	46	adantr 467	. . . . . 6 |- ( ( ph /\ ( Y e. B /\ Z e. B ) ) -> ( F |` B ) = ( z e. B |-> ( F ` z ) ) )
48		fveq2 5865	. . . . . 6 |- ( z = ( ( Y x. t ) + ( Z x. ( 1 - t ) ) ) -> ( F ` z ) = ( F ` ( ( Y x. t ) + ( Z x. ( 1 - t ) ) ) ) )
49	40, 41, 47, 48	fmptco 6056	. . . . 5 |- ( ( ph /\ ( Y e. B /\ Z e. B ) ) -> ( ( F |` B ) o. ( t e. ( 0 [,] 1 ) |-> ( ( Y x. t ) + ( Z x. ( 1 - t ) ) ) ) ) = ( t e. ( 0 [,] 1 ) |-> ( F ` ( ( Y x. t ) + ( Z x. ( 1 - t ) ) ) ) ) )
50		eqid 2451	. . . . . . . 8 |- ( t e. ( 0 [,] 1 ) |-> ( ( Y x. t ) + ( Z x. ( 1 - t ) ) ) ) = ( t e. ( 0 [,] 1 ) |-> ( ( Y x. t ) + ( Z x. ( 1 - t ) ) ) )
51	40, 50	fmptd 6046	. . . . . . 7 |- ( ( ph /\ ( Y e. B /\ Z e. B ) ) -> ( t e. ( 0 [,] 1 ) |-> ( ( Y x. t ) + ( Z x. ( 1 - t ) ) ) ) : ( 0 [,] 1 ) --> B )
52		eqid 2451	. . . . . . . . 9 |- ( TopOpen ` ℂfld ) = ( TopOpen ` ℂfld )
53	52	addcn 21897	. . . . . . . . . 10 |- + e. ( ( ( TopOpen ` ℂfld ) tX ( TopOpen ` ℂfld ) ) Cn ( TopOpen ` ℂfld ) )
54	53	a1i 11	. . . . . . . . 9 |- ( ( ph /\ ( Y e. B /\ Z e. B ) ) -> + e. ( ( ( TopOpen ` ℂfld ) tX ( TopOpen ` ℂfld ) ) Cn ( TopOpen ` ℂfld ) ) )
55		cncfmptc 21943	. . . . . . . . . . . 12 |- ( ( Y e. CC /\ ( 0 [,] 1 ) C_ CC /\ CC C_ CC ) -> ( t e. ( 0 [,] 1 ) |-> Y ) e. ( ( 0 [,] 1 ) -cn-> CC ) )
56	19, 6, 55	mp3an23 1356	. . . . . . . . . . 11 |- ( Y e. CC -> ( t e. ( 0 [,] 1 ) |-> Y ) e. ( ( 0 [,] 1 ) -cn-> CC ) )
57	15, 56	syl 17	. . . . . . . . . 10 |- ( ( ph /\ ( Y e. B /\ Z e. B ) ) -> ( t e. ( 0 [,] 1 ) |-> Y ) e. ( ( 0 [,] 1 ) -cn-> CC ) )
58		cncfmptid 21944	. . . . . . . . . . . 12 |- ( ( ( 0 [,] 1 ) C_ CC /\ CC C_ CC ) -> ( t e. ( 0 [,] 1 ) |-> t ) e. ( ( 0 [,] 1 ) -cn-> CC ) )
59	19, 6, 58	mp2an 678	. . . . . . . . . . 11 |- ( t e. ( 0 [,] 1 ) |-> t ) e. ( ( 0 [,] 1 ) -cn-> CC )
60	59	a1i 11	. . . . . . . . . 10 |- ( ( ph /\ ( Y e. B /\ Z e. B ) ) -> ( t e. ( 0 [,] 1 ) |-> t ) e. ( ( 0 [,] 1 ) -cn-> CC ) )
61	57, 60	mulcncf 22398	. . . . . . . . 9 |- ( ( ph /\ ( Y e. B /\ Z e. B ) ) -> ( t e. ( 0 [,] 1 ) |-> ( Y x. t ) ) e. ( ( 0 [,] 1 ) -cn-> CC ) )
62		cncfmptc 21943	. . . . . . . . . . . 12 |- ( ( Z e. CC /\ ( 0 [,] 1 ) C_ CC /\ CC C_ CC ) -> ( t e. ( 0 [,] 1 ) |-> Z ) e. ( ( 0 [,] 1 ) -cn-> CC ) )
63	19, 6, 62	mp3an23 1356	. . . . . . . . . . 11 |- ( Z e. CC -> ( t e. ( 0 [,] 1 ) |-> Z ) e. ( ( 0 [,] 1 ) -cn-> CC ) )
64	24, 63	syl 17	. . . . . . . . . 10 |- ( ( ph /\ ( Y e. B /\ Z e. B ) ) -> ( t e. ( 0 [,] 1 ) |-> Z ) e. ( ( 0 [,] 1 ) -cn-> CC ) )
65	52	subcn 21898	. . . . . . . . . . . 12 |- - e. ( ( ( TopOpen ` ℂfld ) tX ( TopOpen ` ℂfld ) ) Cn ( TopOpen ` ℂfld ) )
66	65	a1i 11	. . . . . . . . . . 11 |- ( ( ph /\ ( Y e. B /\ Z e. B ) ) -> - e. ( ( ( TopOpen ` ℂfld ) tX ( TopOpen ` ℂfld ) ) Cn ( TopOpen ` ℂfld ) ) )
67		ax-1cn 9597	. . . . . . . . . . . . 13 |- 1 e. CC
68		cncfmptc 21943	. . . . . . . . . . . . 13 |- ( ( 1 e. CC /\ ( 0 [,] 1 ) C_ CC /\ CC C_ CC ) -> ( t e. ( 0 [,] 1 ) |-> 1 ) e. ( ( 0 [,] 1 ) -cn-> CC ) )
69	67, 19, 6, 68	mp3an 1364	. . . . . . . . . . . 12 |- ( t e. ( 0 [,] 1 ) |-> 1 ) e. ( ( 0 [,] 1 ) -cn-> CC )
70	69	a1i 11	. . . . . . . . . . 11 |- ( ( ph /\ ( Y e. B /\ Z e. B ) ) -> ( t e. ( 0 [,] 1 ) |-> 1 ) e. ( ( 0 [,] 1 ) -cn-> CC ) )
71	52, 66, 70, 60	cncfmpt2f 21946	. . . . . . . . . 10 |- ( ( ph /\ ( Y e. B /\ Z e. B ) ) -> ( t e. ( 0 [,] 1 ) |-> ( 1 - t ) ) e. ( ( 0 [,] 1 ) -cn-> CC ) )
72	64, 71	mulcncf 22398	. . . . . . . . 9 |- ( ( ph /\ ( Y e. B /\ Z e. B ) ) -> ( t e. ( 0 [,] 1 ) |-> ( Z x. ( 1 - t ) ) ) e. ( ( 0 [,] 1 ) -cn-> CC ) )
73	52, 54, 61, 72	cncfmpt2f 21946	. . . . . . . 8 |- ( ( ph /\ ( Y e. B /\ Z e. B ) ) -> ( t e. ( 0 [,] 1 ) |-> ( ( Y x. t ) + ( Z x. ( 1 - t ) ) ) ) e. ( ( 0 [,] 1 ) -cn-> CC ) )
74		cncffvrn 21930	. . . . . . . 8 |- ( ( B C_ CC /\ ( t e. ( 0 [,] 1 ) |-> ( ( Y x. t ) + ( Z x. ( 1 - t ) ) ) ) e. ( ( 0 [,] 1 ) -cn-> CC ) ) -> ( ( t e. ( 0 [,] 1 ) |-> ( ( Y x. t ) + ( Z x. ( 1 - t ) ) ) ) e. ( ( 0 [,] 1 ) -cn-> B ) <-> ( t e. ( 0 [,] 1 ) |-> ( ( Y x. t ) + ( Z x. ( 1 - t ) ) ) ) : ( 0 [,] 1 ) --> B ) )
75	13, 73, 74	syl2anc 667	. . . . . . 7 |- ( ( ph /\ ( Y e. B /\ Z e. B ) ) -> ( ( t e. ( 0 [,] 1 ) |-> ( ( Y x. t ) + ( Z x. ( 1 - t ) ) ) ) e. ( ( 0 [,] 1 ) -cn-> B ) <-> ( t e. ( 0 [,] 1 ) |-> ( ( Y x. t ) + ( Z x. ( 1 - t ) ) ) ) : ( 0 [,] 1 ) --> B ) )
76	51, 75	mpbird 236	. . . . . 6 |- ( ( ph /\ ( Y e. B /\ Z e. B ) ) -> ( t e. ( 0 [,] 1 ) |-> ( ( Y x. t ) + ( Z x. ( 1 - t ) ) ) ) e. ( ( 0 [,] 1 ) -cn-> B ) )
77	6	a1i 11	. . . . . . 7 |- ( ( ph /\ ( Y e. B /\ Z e. B ) ) -> CC C_ CC )
78	42	adantr 467	. . . . . . 7 |- ( ( ph /\ ( Y e. B /\ Z e. B ) ) -> ( F |` B ) : B --> CC )
79	52	cnfldtop 21804	. . . . . . . . . . . . . . 15 |- ( TopOpen ` ℂfld ) e. Top
80	52	cnfldtopon 21803	. . . . . . . . . . . . . . . . 17 |- ( TopOpen ` ℂfld ) e. (TopOn ` CC )
81	80	toponunii 19947	. . . . . . . . . . . . . . . 16 |- CC = U. ( TopOpen ` ℂfld )
82	81	restid 15332	. . . . . . . . . . . . . . 15 |- ( ( TopOpen ` ℂfld ) e. Top -> ( ( TopOpen ` ℂfld ) ↾t CC ) = ( TopOpen ` ℂfld ) )
83	79, 82	ax-mp 5	. . . . . . . . . . . . . 14 |- ( ( TopOpen ` ℂfld ) ↾t CC ) = ( TopOpen ` ℂfld )
84	83	eqcomi 2460	. . . . . . . . . . . . 13 |- ( TopOpen ` ℂfld ) = ( ( TopOpen ` ℂfld ) ↾t CC )
85	52, 84	dvres 22866	. . . . . . . . . . . 12 |- ( ( ( CC C_ CC /\ F : X --> CC ) /\ ( X C_ CC /\ B C_ CC ) ) -> ( CC _D ( F |` B ) ) = ( ( CC _D F ) |` ( ( int ` ( TopOpen ` ℂfld ) ) ` B ) ) )
86	7, 8, 9, 12, 85	syl22anc 1269	. . . . . . . . . . 11 |- ( ph -> ( CC _D ( F |` B ) ) = ( ( CC _D F ) |` ( ( int ` ( TopOpen ` ℂfld ) ) ` B ) ) )
87		cnxmet 21793	. . . . . . . . . . . . . . . 16 |- ( abs o. - ) e. ( *Met ` CC )
88	87	a1i 11	. . . . . . . . . . . . . . 15 |- ( ph -> ( abs o. - ) e. ( *Met ` CC ) )
89	52	cnfldtopn 21802	. . . . . . . . . . . . . . . 16 |- ( TopOpen ` ℂfld ) = ( MetOpen ` ( abs o. - ) )
90	89	blopn 21515	. . . . . . . . . . . . . . 15 |- ( ( ( abs o. - ) e. ( *Met ` CC ) /\ A e. CC /\ R e. RR* ) -> ( A ( ball ` ( abs o. - ) ) R ) e. ( TopOpen ` ℂfld ) )
91	88, 31, 33, 90	syl3anc 1268	. . . . . . . . . . . . . 14 |- ( ph -> ( A ( ball ` ( abs o. - ) ) R ) e. ( TopOpen ` ℂfld ) )
92	37, 91	syl5eqel 2533	. . . . . . . . . . . . 13 |- ( ph -> B e. ( TopOpen ` ℂfld ) )
93		isopn3i 20098	. . . . . . . . . . . . 13 |- ( ( ( TopOpen ` ℂfld ) e. Top /\ B e. ( TopOpen ` ℂfld ) ) -> ( ( int ` ( TopOpen ` ℂfld ) ) ` B ) = B )
94	79, 92, 93	sylancr 669	. . . . . . . . . . . 12 |- ( ph -> ( ( int ` ( TopOpen ` ℂfld ) ) ` B ) = B )
95	94	reseq2d 5105	. . . . . . . . . . 11 |- ( ph -> ( ( CC _D F ) |` ( ( int ` ( TopOpen ` ℂfld ) ) ` B ) ) = ( ( CC _D F ) |` B ) )
96	86, 95	eqtrd 2485	. . . . . . . . . 10 |- ( ph -> ( CC _D ( F |` B ) ) = ( ( CC _D F ) |` B ) )
97	96	dmeqd 5037	. . . . . . . . 9 |- ( ph -> dom ( CC _D ( F |` B ) ) = dom ( ( CC _D F ) |` B ) )
98		dmres 5125	. . . . . . . . . 10 |- dom ( ( CC _D F ) |` B ) = ( B i^i dom ( CC _D F ) )
99		df-ss 3418	. . . . . . . . . . 11 |- ( B C_ dom ( CC _D F ) <-> ( B i^i dom ( CC _D F ) ) = B )
100	5, 99	sylib 200	. . . . . . . . . 10 |- ( ph -> ( B i^i dom ( CC _D F ) ) = B )
101	98, 100	syl5eq 2497	. . . . . . . . 9 |- ( ph -> dom ( ( CC _D F ) |` B ) = B )
102	97, 101	eqtrd 2485	. . . . . . . 8 |- ( ph -> dom ( CC _D ( F |` B ) ) = B )
103	102	adantr 467	. . . . . . 7 |- ( ( ph /\ ( Y e. B /\ Z e. B ) ) -> dom ( CC _D ( F |` B ) ) = B )
104		dvcn 22875	. . . . . . 7 |- ( ( ( CC C_ CC /\ ( F |` B ) : B --> CC /\ B C_ CC ) /\ dom ( CC _D ( F |` B ) ) = B ) -> ( F |` B ) e. ( B -cn-> CC ) )
105	77, 78, 13, 103, 104	syl31anc 1271	. . . . . 6 |- ( ( ph /\ ( Y e. B /\ Z e. B ) ) -> ( F |` B ) e. ( B -cn-> CC ) )
106	76, 105	cncfco 21939	. . . . 5 |- ( ( ph /\ ( Y e. B /\ Z e. B ) ) -> ( ( F |` B ) o. ( t e. ( 0 [,] 1 ) |-> ( ( Y x. t ) + ( Z x. ( 1 - t ) ) ) ) ) e. ( ( 0 [,] 1 ) -cn-> CC ) )
107	49, 106	eqeltrrd 2530	. . . 4 |- ( ( ph /\ ( Y e. B /\ Z e. B ) ) -> ( t e. ( 0 [,] 1 ) |-> ( F ` ( ( Y x. t ) + ( Z x. ( 1 - t ) ) ) ) ) e. ( ( 0 [,] 1 ) -cn-> CC ) )
108	18	a1i 11	. . . . . . . 8 |- ( ( ph /\ ( Y e. B /\ Z e. B ) ) -> RR C_ CC )
109	17	a1i 11	. . . . . . . 8 |- ( ( ph /\ ( Y e. B /\ Z e. B ) ) -> ( 0 [,] 1 ) C_ RR )
110	8	ad2antrr 732	. . . . . . . . 9 |- ( ( ( ph /\ ( Y e. B /\ Z e. B ) ) /\ t e. ( 0 [,] 1 ) ) -> F : X --> CC )
111	11	ad2antrr 732	. . . . . . . . . 10 |- ( ( ( ph /\ ( Y e. B /\ Z e. B ) ) /\ t e. ( 0 [,] 1 ) ) -> B C_ X )
112	111, 40	sseldd 3433	. . . . . . . . 9 |- ( ( ( ph /\ ( Y e. B /\ Z e. B ) ) /\ t e. ( 0 [,] 1 ) ) -> ( ( Y x. t ) + ( Z x. ( 1 - t ) ) ) e. X )
113	110, 112	ffvelrnd 6023	. . . . . . . 8 |- ( ( ( ph /\ ( Y e. B /\ Z e. B ) ) /\ t e. ( 0 [,] 1 ) ) -> ( F ` ( ( Y x. t ) + ( Z x. ( 1 - t ) ) ) ) e. CC )
114	52	tgioo2 21821	. . . . . . . 8 |- ( topGen ` ran (,) ) = ( ( TopOpen ` ℂfld ) ↾t RR )
115		1re 9642	. . . . . . . . 9 |- 1 e. RR
116		iccntr 21839	. . . . . . . . 9 |- ( ( 0 e. RR /\ 1 e. RR ) -> ( ( int ` ( topGen ` ran (,) ) ) ` ( 0 [,] 1 ) ) = ( 0 (,) 1 ) )
117	3, 115, 116	sylancl 668	. . . . . . . 8 |- ( ( ph /\ ( Y e. B /\ Z e. B ) ) -> ( ( int ` ( topGen ` ran (,) ) ) ` ( 0 [,] 1 ) ) = ( 0 (,) 1 ) )
118	108, 109, 113, 114, 52, 117	dvmptntr 22925	. . . . . . 7 |- ( ( ph /\ ( Y e. B /\ Z e. B ) ) -> ( RR _D ( t e. ( 0 [,] 1 ) |-> ( F ` ( ( Y x. t ) + ( Z x. ( 1 - t ) ) ) ) ) ) = ( RR _D ( t e. ( 0 (,) 1 ) |-> ( F ` ( ( Y x. t ) + ( Z x. ( 1 - t ) ) ) ) ) ) )
119		reelprrecn 9631	. . . . . . . . 9 |- RR e. { RR , CC }
120	119	a1i 11	. . . . . . . 8 |- ( ( ph /\ ( Y e. B /\ Z e. B ) ) -> RR e. { RR , CC } )
121		cnelprrecn 9632	. . . . . . . . 9 |- CC e. { RR , CC }
122	121	a1i 11	. . . . . . . 8 |- ( ( ph /\ ( Y e. B /\ Z e. B ) ) -> CC e. { RR , CC } )
123		ioossicc 11720	. . . . . . . . . 10 |- ( 0 (,) 1 ) C_ ( 0 [,] 1 )
124	123	sseli 3428	. . . . . . . . 9 |- ( t e. ( 0 (,) 1 ) -> t e. ( 0 [,] 1 ) )
125	124, 40	sylan2 477	. . . . . . . 8 |- ( ( ( ph /\ ( Y e. B /\ Z e. B ) ) /\ t e. ( 0 (,) 1 ) ) -> ( ( Y x. t ) + ( Z x. ( 1 - t ) ) ) e. B )
126	15, 24	subcld 9986	. . . . . . . . 9 |- ( ( ph /\ ( Y e. B /\ Z e. B ) ) -> ( Y - Z ) e. CC )
127	126	adantr 467	. . . . . . . 8 |- ( ( ( ph /\ ( Y e. B /\ Z e. B ) ) /\ t e. ( 0 (,) 1 ) ) -> ( Y - Z ) e. CC )
128	11	adantr 467	. . . . . . . . . 10 |- ( ( ph /\ ( Y e. B /\ Z e. B ) ) -> B C_ X )
129	128	sselda 3432	. . . . . . . . 9 |- ( ( ( ph /\ ( Y e. B /\ Z e. B ) ) /\ z e. B ) -> z e. X )
130	8	adantr 467	. . . . . . . . . 10 |- ( ( ph /\ ( Y e. B /\ Z e. B ) ) -> F : X --> CC )
131	130	ffvelrnda 6022	. . . . . . . . 9 |- ( ( ( ph /\ ( Y e. B /\ Z e. B ) ) /\ z e. X ) -> ( F ` z ) e. CC )
132	129, 131	syldan 473	. . . . . . . 8 |- ( ( ( ph /\ ( Y e. B /\ Z e. B ) ) /\ z e. B ) -> ( F ` z ) e. CC )
133		fvex 5875	. . . . . . . . 9 |- ( ( CC _D F ) ` z ) e. _V
134	133	a1i 11	. . . . . . . 8 |- ( ( ( ph /\ ( Y e. B /\ Z e. B ) ) /\ z e. B ) -> ( ( CC _D F ) ` z ) e. _V )
135	15	adantr 467	. . . . . . . . . . 11 |- ( ( ( ph /\ ( Y e. B /\ Z e. B ) ) /\ t e. ( 0 (,) 1 ) ) -> Y e. CC )
136	124, 21	sylan2 477	. . . . . . . . . . 11 |- ( ( ( ph /\ ( Y e. B /\ Z e. B ) ) /\ t e. ( 0 (,) 1 ) ) -> t e. CC )
137	135, 136	mulcld 9663	. . . . . . . . . 10 |- ( ( ( ph /\ ( Y e. B /\ Z e. B ) ) /\ t e. ( 0 (,) 1 ) ) -> ( Y x. t ) e. CC )
138		1red 9658	. . . . . . . . . . . 12 |- ( ( ( ph /\ ( Y e. B /\ Z e. B ) ) /\ t e. ( 0 (,) 1 ) ) -> 1 e. RR )
139		simpr 463	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ ( Y e. B /\ Z e. B ) ) /\ t e. RR ) -> t e. RR )
140	139	recnd 9669	. . . . . . . . . . . . 13 |- ( ( ( ph /\ ( Y e. B /\ Z e. B ) ) /\ t e. RR ) -> t e. CC )
141		1red 9658	. . . . . . . . . . . . 13 |- ( ( ( ph /\ ( Y e. B /\ Z e. B ) ) /\ t e. RR ) -> 1 e. RR )
142	120	dvmptid 22911	. . . . . . . . . . . . 13 |- ( ( ph /\ ( Y e. B /\ Z e. B ) ) -> ( RR _D ( t e. RR |-> t ) ) = ( t e. RR |-> 1 ) )
143		ioossre 11696	. . . . . . . . . . . . . 14 |- ( 0 (,) 1 ) C_ RR
144	143	a1i 11	. . . . . . . . . . . . 13 |- ( ( ph /\ ( Y e. B /\ Z e. B ) ) -> ( 0 (,) 1 ) C_ RR )
145		iooretop 21786	. . . . . . . . . . . . . 14 |- ( 0 (,) 1 ) e. ( topGen ` ran (,) )
146	145	a1i 11	. . . . . . . . . . . . 13 |- ( ( ph /\ ( Y e. B /\ Z e. B ) ) -> ( 0 (,) 1 ) e. ( topGen ` ran (,) ) )
147	120, 140, 141, 142, 144, 114, 52, 146	dvmptres 22917	. . . . . . . . . . . 12 |- ( ( ph /\ ( Y e. B /\ Z e. B ) ) -> ( RR _D ( t e. ( 0 (,) 1 ) |-> t ) ) = ( t e. ( 0 (,) 1 ) |-> 1 ) )
148	120, 136, 138, 147, 15	dvmptcmul 22918	. . . . . . . . . . 11 |- ( ( ph /\ ( Y e. B /\ Z e. B ) ) -> ( RR _D ( t e. ( 0 (,) 1 ) |-> ( Y x. t ) ) ) = ( t e. ( 0 (,) 1 ) |-> ( Y x. 1 ) ) )
149	15	mulid1d 9660	. . . . . . . . . . . 12 |- ( ( ph /\ ( Y e. B /\ Z e. B ) ) -> ( Y x. 1 ) = Y )
150	149	mpteq2dv 4490	. . . . . . . . . . 11 |- ( ( ph /\ ( Y e. B /\ Z e. B ) ) -> ( t e. ( 0 (,) 1 ) |-> ( Y x. 1 ) ) = ( t e. ( 0 (,) 1 ) |-> Y ) )
151	148, 150	eqtrd 2485	. . . . . . . . . 10 |- ( ( ph /\ ( Y e. B /\ Z e. B ) ) -> ( RR _D ( t e. ( 0 (,) 1 ) |-> ( Y x. t ) ) ) = ( t e. ( 0 (,) 1 ) |-> Y ) )
152	24	adantr 467	. . . . . . . . . . 11 |- ( ( ( ph /\ ( Y e. B /\ Z e. B ) ) /\ t e. ( 0 (,) 1 ) ) -> Z e. CC )
153	124, 28	sylan2 477	. . . . . . . . . . 11 |- ( ( ( ph /\ ( Y e. B /\ Z e. B ) ) /\ t e. ( 0 (,) 1 ) ) -> ( 1 - t ) e. CC )
154	152, 153	mulcld 9663	. . . . . . . . . 10 |- ( ( ( ph /\ ( Y e. B /\ Z e. B ) ) /\ t e. ( 0 (,) 1 ) ) -> ( Z x. ( 1 - t ) ) e. CC )
155		negex 9873	. . . . . . . . . . 11 |- -u Z e. _V
156	155	a1i 11	. . . . . . . . . 10 |- ( ( ( ph /\ ( Y e. B /\ Z e. B ) ) /\ t e. ( 0 (,) 1 ) ) -> -u Z e. _V )
157		negex 9873	. . . . . . . . . . . . 13 |- -u 1 e. _V
158	157	a1i 11	. . . . . . . . . . . 12 |- ( ( ( ph /\ ( Y e. B /\ Z e. B ) ) /\ t e. ( 0 (,) 1 ) ) -> -u 1 e. _V )
159		1cnd 9659	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ ( Y e. B /\ Z e. B ) ) /\ t e. ( 0 (,) 1 ) ) -> 1 e. CC )
160		0red 9644	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ ( Y e. B /\ Z e. B ) ) /\ t e. ( 0 (,) 1 ) ) -> 0 e. RR )
161		1cnd 9659	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ ( Y e. B /\ Z e. B ) ) /\ t e. RR ) -> 1 e. CC )
162		0red 9644	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ ( Y e. B /\ Z e. B ) ) /\ t e. RR ) -> 0 e. RR )
163		1cnd 9659	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ ( Y e. B /\ Z e. B ) ) -> 1 e. CC )
164	120, 163	dvmptc 22912	. . . . . . . . . . . . . . 15 |- ( ( ph /\ ( Y e. B /\ Z e. B ) ) -> ( RR _D ( t e. RR |-> 1 ) ) = ( t e. RR |-> 0 ) )
165	120, 161, 162, 164, 144, 114, 52, 146	dvmptres 22917	. . . . . . . . . . . . . 14 |- ( ( ph /\ ( Y e. B /\ Z e. B ) ) -> ( RR _D ( t e. ( 0 (,) 1 ) |-> 1 ) ) = ( t e. ( 0 (,) 1 ) |-> 0 ) )
166	120, 159, 160, 165, 136, 138, 147	dvmptsub 22921	. . . . . . . . . . . . 13 |- ( ( ph /\ ( Y e. B /\ Z e. B ) ) -> ( RR _D ( t e. ( 0 (,) 1 ) |-> ( 1 - t ) ) ) = ( t e. ( 0 (,) 1 ) |-> ( 0 - 1 ) ) )
167		df-neg 9863	. . . . . . . . . . . . . 14 |- -u 1 = ( 0 - 1 )
168	167	mpteq2i 4486	. . . . . . . . . . . . 13 |- ( t e. ( 0 (,) 1 ) |-> -u 1 ) = ( t e. ( 0 (,) 1 ) |-> ( 0 - 1 ) )
169	166, 168	syl6eqr 2503	. . . . . . . . . . . 12 |- ( ( ph /\ ( Y e. B /\ Z e. B ) ) -> ( RR _D ( t e. ( 0 (,) 1 ) |-> ( 1 - t ) ) ) = ( t e. ( 0 (,) 1 ) |-> -u 1 ) )
170	120, 153, 158, 169, 24	dvmptcmul 22918	. . . . . . . . . . 11 |- ( ( ph /\ ( Y e. B /\ Z e. B ) ) -> ( RR _D ( t e. ( 0 (,) 1 ) |-> ( Z x. ( 1 - t ) ) ) ) = ( t e. ( 0 (,) 1 ) |-> ( Z x. -u 1 ) ) )
171		neg1cn 10713	. . . . . . . . . . . . . 14 |- -u 1 e. CC
172		mulcom 9625	. . . . . . . . . . . . . 14 |- ( ( Z e. CC /\ -u 1 e. CC ) -> ( Z x. -u 1 ) = ( -u 1 x. Z ) )
173	24, 171, 172	sylancl 668	. . . . . . . . . . . . 13 |- ( ( ph /\ ( Y e. B /\ Z e. B ) ) -> ( Z x. -u 1 ) = ( -u 1 x. Z ) )
174	24	mulm1d 10070	. . . . . . . . . . . . 13 |- ( ( ph /\ ( Y e. B /\ Z e. B ) ) -> ( -u 1 x. Z ) = -u Z )
175	173, 174	eqtrd 2485	. . . . . . . . . . . 12 |- ( ( ph /\ ( Y e. B /\ Z e. B ) ) -> ( Z x. -u 1 ) = -u Z )
176	175	mpteq2dv 4490	. . . . . . . . . . 11 |- ( ( ph /\ ( Y e. B /\ Z e. B ) ) -> ( t e. ( 0 (,) 1 ) |-> ( Z x. -u 1 ) ) = ( t e. ( 0 (,) 1 ) |-> -u Z ) )
177	170, 176	eqtrd 2485	. . . . . . . . . 10 |- ( ( ph /\ ( Y e. B /\ Z e. B ) ) -> ( RR _D ( t e. ( 0 (,) 1 ) |-> ( Z x. ( 1 - t ) ) ) ) = ( t e. ( 0 (,) 1 ) |-> -u Z ) )
178	120, 137, 135, 151, 154, 156, 177	dvmptadd 22914	. . . . . . . . 9 |- ( ( ph /\ ( Y e. B /\ Z e. B ) ) -> ( RR _D ( t e. ( 0 (,) 1 ) |-> ( ( Y x. t ) + ( Z x. ( 1 - t ) ) ) ) ) = ( t e. ( 0 (,) 1 ) |-> ( Y + -u Z ) ) )
179	15, 24	negsubd 9992	. . . . . . . . . 10 |- ( ( ph /\ ( Y e. B /\ Z e. B ) ) -> ( Y + -u Z ) = ( Y - Z ) )
180	179	mpteq2dv 4490	. . . . . . . . 9 |- ( ( ph /\ ( Y e. B /\ Z e. B ) ) -> ( t e. ( 0 (,) 1 ) |-> ( Y + -u Z ) ) = ( t e. ( 0 (,) 1 ) |-> ( Y - Z ) ) )
181	178, 180	eqtrd 2485	. . . . . . . 8 |- ( ( ph /\ ( Y e. B /\ Z e. B ) ) -> ( RR _D ( t e. ( 0 (,) 1 ) |-> ( ( Y x. t ) + ( Z x. ( 1 - t ) ) ) ) ) = ( t e. ( 0 (,) 1 ) |-> ( Y - Z ) ) )
182	9	adantr 467	. . . . . . . . . . 11 |- ( ( ph /\ ( Y e. B /\ Z e. B ) ) -> X C_ CC )
183	77, 130, 182, 13, 85	syl22anc 1269	. . . . . . . . . 10 |- ( ( ph /\ ( Y e. B /\ Z e. B ) ) -> ( CC _D ( F |` B ) ) = ( ( CC _D F ) |` ( ( int ` ( TopOpen ` ℂfld ) ) ` B ) ) )
184	94	adantr 467	. . . . . . . . . . 11 |- ( ( ph /\ ( Y e. B /\ Z e. B ) ) -> ( ( int ` ( TopOpen ` ℂfld ) ) ` B ) = B )
185	184	reseq2d 5105	. . . . . . . . . 10 |- ( ( ph /\ ( Y e. B /\ Z e. B ) ) -> ( ( CC _D F ) |` ( ( int ` ( TopOpen ` ℂfld ) ) ` B ) ) = ( ( CC _D F ) |` B ) )
186	183, 185	eqtrd 2485	. . . . . . . . 9 |- ( ( ph /\ ( Y e. B /\ Z e. B ) ) -> ( CC _D ( F |` B ) ) = ( ( CC _D F ) |` B ) )
187	47	oveq2d 6306	. . . . . . . . 9 |- ( ( ph /\ ( Y e. B /\ Z e. B ) ) -> ( CC _D ( F |` B ) ) = ( CC _D ( z e. B |-> ( F ` z ) ) ) )
188		dvfcn 22863	. . . . . . . . . . . . 13 |- ( CC _D ( F |` B ) ) : dom ( CC _D ( F |` B ) ) --> CC
189	103	feq2d 5715	. . . . . . . . . . . . 13 |- ( ( ph /\ ( Y e. B /\ Z e. B ) ) -> ( ( CC _D ( F |` B ) ) : dom ( CC _D ( F |` B ) ) --> CC <-> ( CC _D ( F |` B ) ) : B --> CC ) )
190	188, 189	mpbii 215	. . . . . . . . . . . 12 |- ( ( ph /\ ( Y e. B /\ Z e. B ) ) -> ( CC _D ( F |` B ) ) : B --> CC )
191	186	feq1d 5714	. . . . . . . . . . . 12 |- ( ( ph /\ ( Y e. B /\ Z e. B ) ) -> ( ( CC _D ( F |` B ) ) : B --> CC <-> ( ( CC _D F ) |` B ) : B --> CC ) )
192	190, 191	mpbid 214	. . . . . . . . . . 11 |- ( ( ph /\ ( Y e. B /\ Z e. B ) ) -> ( ( CC _D F ) |` B ) : B --> CC )
193	192	feqmptd 5918	. . . . . . . . . 10 |- ( ( ph /\ ( Y e. B /\ Z e. B ) ) -> ( ( CC _D F ) |` B ) = ( z e. B |-> ( ( ( CC _D F ) |` B ) ` z ) ) )
194		fvres 5879	. . . . . . . . . . 11 |- ( z e. B -> ( ( ( CC _D F ) |` B ) ` z ) = ( ( CC _D F ) ` z ) )
195	194	mpteq2ia 4485	. . . . . . . . . 10 |- ( z e. B |-> ( ( ( CC _D F ) |` B ) ` z ) ) = ( z e. B |-> ( ( CC _D F ) ` z ) )
196	193, 195	syl6eq 2501	. . . . . . . . 9 |- ( ( ph /\ ( Y e. B /\ Z e. B ) ) -> ( ( CC _D F ) |` B ) = ( z e. B |-> ( ( CC _D F ) ` z ) ) )
197	186, 187, 196	3eqtr3d 2493	. . . . . . . 8 |- ( ( ph /\ ( Y e. B /\ Z e. B ) ) -> ( CC _D ( z e. B |-> ( F ` z ) ) ) = ( z e. B |-> ( ( CC _D F ) ` z ) ) )
198		fveq2 5865	. . . . . . . 8 |- ( z = ( ( Y x. t ) + ( Z x. ( 1 - t ) ) ) -> ( ( CC _D F ) ` z ) = ( ( CC _D F ) ` ( ( Y x. t ) + ( Z x. ( 1 - t ) ) ) ) )
199	120, 122, 125, 127, 132, 134, 181, 197, 48, 198	dvmptco 22926	. . . . . . 7 |- ( ( ph /\ ( Y e. B /\ Z e. B ) ) -> ( RR _D ( t e. ( 0 (,) 1 ) |-> ( F ` ( ( Y x. t ) + ( Z x. ( 1 - t ) ) ) ) ) ) = ( t e. ( 0 (,) 1 ) |-> ( ( ( CC _D F ) ` ( ( Y x. t ) + ( Z x. ( 1 - t ) ) ) ) x. ( Y - Z ) ) ) )
200	118, 199	eqtrd 2485	. . . . . 6 |- ( ( ph /\ ( Y e. B /\ Z e. B ) ) -> ( RR _D ( t e. ( 0 [,] 1 ) |-> ( F ` ( ( Y x. t ) + ( Z x. ( 1 - t ) ) ) ) ) ) = ( t e. ( 0 (,) 1 ) |-> ( ( ( CC _D F ) ` ( ( Y x. t ) + ( Z x. ( 1 - t ) ) ) ) x. ( Y - Z ) ) ) )
201	200	dmeqd 5037	. . . . 5 |- ( ( ph /\ ( Y e. B /\ Z e. B ) ) -> dom ( RR _D ( t e. ( 0 [,] 1 ) |-> ( F ` ( ( Y x. t ) + ( Z x. ( 1 - t ) ) ) ) ) ) = dom ( t e. ( 0 (,) 1 ) |-> ( ( ( CC _D F ) ` ( ( Y x. t ) + ( Z x. ( 1 - t ) ) ) ) x. ( Y - Z ) ) ) )
202		ovex 6318	. . . . . . 7 |- ( ( ( CC _D F ) ` ( ( Y x. t ) + ( Z x. ( 1 - t ) ) ) ) x. ( Y - Z ) ) e. _V
203	202	rgenw 2749	. . . . . 6 |- A. t e. ( 0 (,) 1 ) ( ( ( CC _D F ) ` ( ( Y x. t ) + ( Z x. ( 1 - t ) ) ) ) x. ( Y - Z ) ) e. _V
204		dmmptg 5332	. . . . . 6 |- ( A. t e. ( 0 (,) 1 ) ( ( ( CC _D F ) ` ( ( Y x. t ) + ( Z x. ( 1 - t ) ) ) ) x. ( Y - Z ) ) e. _V -> dom ( t e. ( 0 (,) 1 ) |-> ( ( ( CC _D F ) ` ( ( Y x. t ) + ( Z x. ( 1 - t ) ) ) ) x. ( Y - Z ) ) ) = ( 0 (,) 1 ) )
205	203, 204	mp1i 13	. . . . 5 |- ( ( ph /\ ( Y e. B /\ Z e. B ) ) -> dom ( t e. ( 0 (,) 1 ) |-> ( ( ( CC _D F ) ` ( ( Y x. t ) + ( Z x. ( 1 - t ) ) ) ) x. ( Y - Z ) ) ) = ( 0 (,) 1 ) )
206	201, 205	eqtrd 2485	. . . 4 |- ( ( ph /\ ( Y e. B /\ Z e. B ) ) -> dom ( RR _D ( t e. ( 0 [,] 1 ) |-> ( F ` ( ( Y x. t ) + ( Z x. ( 1 - t ) ) ) ) ) ) = ( 0 (,) 1 ) )
207		dvlipcn.m	. . . . . 6 |- ( ph -> M e. RR )
208	207	adantr 467	. . . . 5 |- ( ( ph /\ ( Y e. B /\ Z e. B ) ) -> M e. RR )
209	126	abscld 13498	. . . . 5 |- ( ( ph /\ ( Y e. B /\ Z e. B ) ) -> ( abs ` ( Y - Z ) ) e. RR )
210	208, 209	remulcld 9671	. . . 4 |- ( ( ph /\ ( Y e. B /\ Z e. B ) ) -> ( M x. ( abs ` ( Y - Z ) ) ) e. RR )
211	200	fveq1d 5867	. . . . . . . . . . 11 |- ( ( ph /\ ( Y e. B /\ Z e. B ) ) -> ( ( RR _D ( t e. ( 0 [,] 1 ) |-> ( F ` ( ( Y x. t ) + ( Z x. ( 1 - t ) ) ) ) ) ) ` t ) = ( ( t e. ( 0 (,) 1 ) |-> ( ( ( CC _D F ) ` ( ( Y x. t ) + ( Z x. ( 1 - t ) ) ) ) x. ( Y - Z ) ) ) ` t ) )
212		eqid 2451	. . . . . . . . . . . . 13 |- ( t e. ( 0 (,) 1 ) |-> ( ( ( CC _D F ) ` ( ( Y x. t ) + ( Z x. ( 1 - t ) ) ) ) x. ( Y - Z ) ) ) = ( t e. ( 0 (,) 1 ) |-> ( ( ( CC _D F ) ` ( ( Y x. t ) + ( Z x. ( 1 - t ) ) ) ) x. ( Y - Z ) ) )
213	212	fvmpt2 5957	. . . . . . . . . . . 12 |- ( ( t e. ( 0 (,) 1 ) /\ ( ( ( CC _D F ) ` ( ( Y x. t ) + ( Z x. ( 1 - t ) ) ) ) x. ( Y - Z ) ) e. _V ) -> ( ( t e. ( 0 (,) 1 ) |-> ( ( ( CC _D F ) ` ( ( Y x. t ) + ( Z x. ( 1 - t ) ) ) ) x. ( Y - Z ) ) ) ` t ) = ( ( ( CC _D F ) ` ( ( Y x. t ) + ( Z x. ( 1 - t ) ) ) ) x. ( Y - Z ) ) )
214	202, 213	mpan2 677	. . . . . . . . . . 11 |- ( t e. ( 0 (,) 1 ) -> ( ( t e. ( 0 (,) 1 ) |-> ( ( ( CC _D F ) ` ( ( Y x. t ) + ( Z x. ( 1 - t ) ) ) ) x. ( Y - Z ) ) ) ` t ) = ( ( ( CC _D F ) ` ( ( Y x. t ) + ( Z x. ( 1 - t ) ) ) ) x. ( Y - Z ) ) )
215	211, 214	sylan9eq 2505	. . . . . . . . . 10 |- ( ( ( ph /\ ( Y e. B /\ Z e. B ) ) /\ t e. ( 0 (,) 1 ) ) -> ( ( RR _D ( t e. ( 0 [,] 1 ) |-> ( F ` ( ( Y x. t ) + ( Z x. ( 1 - t ) ) ) ) ) ) ` t ) = ( ( ( CC _D F ) ` ( ( Y x. t ) + ( Z x. ( 1 - t ) ) ) ) x. ( Y - Z ) ) )
216	215	fveq2d 5869	. . . . . . . . 9 |- ( ( ( ph /\ ( Y e. B /\ Z e. B ) ) /\ t e. ( 0 (,) 1 ) ) -> ( abs ` ( ( RR _D ( t e. ( 0 [,] 1 ) |-> ( F ` ( ( Y x. t ) + ( Z x. ( 1 - t ) ) ) ) ) ) ` t ) ) = ( abs ` ( ( ( CC _D F ) ` ( ( Y x. t ) + ( Z x. ( 1 - t ) ) ) ) x. ( Y - Z ) ) ) )
217		dvfcn 22863	. . . . . . . . . . 11 |- ( CC _D F ) : dom ( CC _D F ) --> CC
218	5	ad2antrr 732	. . . . . . . . . . . 12 |- ( ( ( ph /\ ( Y e. B /\ Z e. B ) ) /\ t e. ( 0 (,) 1 ) ) -> B C_ dom ( CC _D F ) )
219	218, 125	sseldd 3433	. . . . . . . . . . 11 |- ( ( ( ph /\ ( Y e. B /\ Z e. B ) ) /\ t e. ( 0 (,) 1 ) ) -> ( ( Y x. t ) + ( Z x. ( 1 - t ) ) ) e. dom ( CC _D F ) )
220		ffvelrn 6020	. . . . . . . . . . 11 |- ( ( ( CC _D F ) : dom ( CC _D F ) --> CC /\ ( ( Y x. t ) + ( Z x. ( 1 - t ) ) ) e. dom ( CC _D F ) ) -> ( ( CC _D F ) ` ( ( Y x. t ) + ( Z x. ( 1 - t ) ) ) ) e. CC )
221	217, 219, 220	sylancr 669	. . . . . . . . . 10 |- ( ( ( ph /\ ( Y e. B /\ Z e. B ) ) /\ t e. ( 0 (,) 1 ) ) -> ( ( CC _D F ) ` ( ( Y x. t ) + ( Z x. ( 1 - t ) ) ) ) e. CC )
222	221, 127	absmuld 13516	. . . . . . . . 9 |- ( ( ( ph /\ ( Y e. B /\ Z e. B ) ) /\ t e. ( 0 (,) 1 ) ) -> ( abs ` ( ( ( CC _D F ) ` ( ( Y x. t ) + ( Z x. ( 1 - t ) ) ) ) x. ( Y - Z ) ) ) = ( ( abs ` ( ( CC _D F ) ` ( ( Y x. t ) + ( Z x. ( 1 - t ) ) ) ) ) x. ( abs ` ( Y - Z ) ) ) )
223	216, 222	eqtrd 2485	. . . . . . . 8 |- ( ( ( ph /\ ( Y e. B /\ Z e. B ) ) /\ t e. ( 0 (,) 1 ) ) -> ( abs ` ( ( RR _D ( t e. ( 0 [,] 1 ) |-> ( F ` ( ( Y x. t ) + ( Z x. ( 1 - t ) ) ) ) ) ) ` t ) ) = ( ( abs ` ( ( CC _D F ) ` ( ( Y x. t ) + ( Z x. ( 1 - t ) ) ) ) ) x. ( abs ` ( Y - Z ) ) ) )
224	221	abscld 13498	. . . . . . . . 9 |- ( ( ( ph /\ ( Y e. B /\ Z e. B ) ) /\ t e. ( 0 (,) 1 ) ) -> ( abs ` ( ( CC _D F ) ` ( ( Y x. t ) + ( Z x. ( 1 - t ) ) ) ) ) e. RR )
225	207	ad2antrr 732	. . . . . . . . 9 |- ( ( ( ph /\ ( Y e. B /\ Z e. B ) ) /\ t e. ( 0 (,) 1 ) ) -> M e. RR )
226	127	abscld 13498	. . . . . . . . 9 |- ( ( ( ph /\ ( Y e. B /\ Z e. B ) ) /\ t e. ( 0 (,) 1 ) ) -> ( abs ` ( Y - Z ) ) e. RR )
227	127	absge0d 13506	. . . . . . . . 9 |- ( ( ( ph /\ ( Y e. B /\ Z e. B ) ) /\ t e. ( 0 (,) 1 ) ) -> 0 <_ ( abs ` ( Y - Z ) ) )
228		dvlipcn.l	. . . . . . . . . . . . 13 |- ( ( ph /\ x e. B ) -> ( abs ` ( ( CC _D F ) ` x ) ) <_ M )
229	228	ralrimiva 2802	. . . . . . . . . . . 12 |- ( ph -> A. x e. B ( abs ` ( ( CC _D F ) ` x ) ) <_ M )
230		fveq2 5865	. . . . . . . . . . . . . . 15 |- ( x = y -> ( ( CC _D F ) ` x ) = ( ( CC _D F ) ` y ) )
231	230	fveq2d 5869	. . . . . . . . . . . . . 14 |- ( x = y -> ( abs ` ( ( CC _D F ) ` x ) ) = ( abs ` ( ( CC _D F ) ` y ) ) )
232	231	breq1d 4412	. . . . . . . . . . . . 13 |- ( x = y -> ( ( abs ` ( ( CC _D F ) ` x ) ) <_ M <-> ( abs ` ( ( CC _D F ) ` y ) ) <_ M ) )
233	232	cbvralv 3019	. . . . . . . . . . . 12 |- ( A. x e. B ( abs ` ( ( CC _D F ) ` x ) ) <_ M <-> A. y e. B ( abs ` ( ( CC _D F ) ` y ) ) <_ M )
234	229, 233	sylib 200	. . . . . . . . . . 11 |- ( ph -> A. y e. B ( abs ` ( ( CC _D F ) ` y ) ) <_ M )
235	234	ad2antrr 732	. . . . . . . . . 10 |- ( ( ( ph /\ ( Y e. B /\ Z e. B ) ) /\ t e. ( 0 (,) 1 ) ) -> A. y e. B ( abs ` ( ( CC _D F ) ` y ) ) <_ M )
236		fveq2 5865	. . . . . . . . . . . . 13 |- ( y = ( ( Y x. t ) + ( Z x. ( 1 - t ) ) ) -> ( ( CC _D F ) ` y ) = ( ( CC _D F ) ` ( ( Y x. t ) + ( Z x. ( 1 - t ) ) ) ) )
237	236	fveq2d 5869	. . . . . . . . . . . 12 |- ( y = ( ( Y x. t ) + ( Z x. ( 1 - t ) ) ) -> ( abs ` ( ( CC _D F ) ` y ) ) = ( abs ` ( ( CC _D F ) ` ( ( Y x. t ) + ( Z x. ( 1 - t ) ) ) ) ) )
238	237	breq1d 4412	. . . . . . . . . . 11 |- ( y = ( ( Y x. t ) + ( Z x. ( 1 - t ) ) ) -> ( ( abs ` ( ( CC _D F ) ` y ) ) <_ M <-> ( abs ` ( ( CC _D F ) ` ( ( Y x. t ) + ( Z x. ( 1 - t ) ) ) ) ) <_ M ) )
239	238	rspcv 3146	. . . . . . . . . 10 |- ( ( ( Y x. t ) + ( Z x. ( 1 - t ) ) ) e. B -> ( A. y e. B ( abs ` ( ( CC _D F ) ` y ) ) <_ M -> ( abs ` ( ( CC _D F ) ` ( ( Y x. t ) + ( Z x. ( 1 - t ) ) ) ) ) <_ M ) )
240	125, 235, 239	sylc 62	. . . . . . . . 9 |- ( ( ( ph /\ ( Y e. B /\ Z e. B ) ) /\ t e. ( 0 (,) 1 ) ) -> ( abs ` ( ( CC _D F ) ` ( ( Y x. t ) + ( Z x. ( 1 - t ) ) ) ) ) <_ M )
241	224, 225, 226, 227, 240	lemul1ad 10546	. . . . . . . 8 |- ( ( ( ph /\ ( Y e. B /\ Z e. B ) ) /\ t e. ( 0 (,) 1 ) ) -> ( ( abs ` ( ( CC _D F ) ` ( ( Y x. t ) + ( Z x. ( 1 - t ) ) ) ) ) x. ( abs ` ( Y - Z ) ) ) <_ ( M x. ( abs ` ( Y - Z ) ) ) )
242	223, 241	eqbrtrd 4423	. . . . . . 7 |- ( ( ( ph /\ ( Y e. B /\ Z e. B ) ) /\ t e. ( 0 (,) 1 ) ) -> ( abs ` ( ( RR _D ( t e. ( 0 [,] 1 ) |-> ( F ` ( ( Y x. t ) + ( Z x. ( 1 - t ) ) ) ) ) ) ` t ) ) <_ ( M x. ( abs ` ( Y - Z ) ) ) )
243	242	ralrimiva 2802	. . . . . 6 |- ( ( ph /\ ( Y e. B /\ Z e. B ) ) -> A. t e. ( 0 (,) 1 ) ( abs ` ( ( RR _D ( t e. ( 0 [,] 1 ) |-> ( F ` ( ( Y x. t ) + ( Z x. ( 1 - t ) ) ) ) ) ) ` t ) ) <_ ( M x. ( abs ` ( Y - Z ) ) ) )
244		nfv 1761	. . . . . . 7 |- F/ z ( abs ` ( ( RR _D ( t e. ( 0 [,] 1 ) |-> ( F ` ( ( Y x. t ) + ( Z x. ( 1 - t ) ) ) ) ) ) ` t ) ) <_ ( M x. ( abs ` ( Y - Z ) ) )
245		nfcv 2592	. . . . . . . . 9 |- F/_ t abs
246		nfcv 2592	. . . . . . . . . . 11 |- F/_ t RR
247		nfcv 2592	. . . . . . . . . . 11 |- F/_ t _D
248		nfmpt1 4492	. . . . . . . . . . 11 |- F/_ t ( t e. ( 0 [,] 1 ) |-> ( F ` ( ( Y x. t ) + ( Z x. ( 1 - t ) ) ) ) )
249	246, 247, 248	nfov 6316	. . . . . . . . . 10 |- F/_ t ( RR _D ( t e. ( 0 [,] 1 ) |-> ( F ` ( ( Y x. t ) + ( Z x. ( 1 - t ) ) ) ) ) )
250		nfcv 2592	. . . . . . . . . 10 |- F/_ t z
251	249, 250	nffv 5872	. . . . . . . . 9 |- F/_ t ( ( RR _D ( t e. ( 0 [,] 1 ) |-> ( F ` ( ( Y x. t ) + ( Z x. ( 1 - t ) ) ) ) ) ) ` z )
252	245, 251	nffv 5872	. . . . . . . 8 |- F/_ t ( abs ` ( ( RR _D ( t e. ( 0 [,] 1 ) |-> ( F ` ( ( Y x. t ) + ( Z x. ( 1 - t ) ) ) ) ) ) ` z ) )
253		nfcv 2592	. . . . . . . 8 |- F/_ t <_
254		nfcv 2592	. . . . . . . 8 |- F/_ t ( M x. ( abs ` ( Y - Z ) ) )
255	252, 253, 254	nfbr 4447	. . . . . . 7 |- F/ t ( abs ` ( ( RR _D ( t e. ( 0 [,] 1 ) |-> ( F ` ( ( Y x. t ) + ( Z x. ( 1 - t ) ) ) ) ) ) ` z ) ) <_ ( M x. ( abs ` ( Y - Z ) ) )
256		fveq2 5865	. . . . . . . . 9 |- ( t = z -> ( ( RR _D ( t e. ( 0 [,] 1 ) |-> ( F ` ( ( Y x. t ) + ( Z x. ( 1 - t ) ) ) ) ) ) ` t ) = ( ( RR _D ( t e. ( 0 [,] 1 ) |-> ( F ` ( ( Y x. t ) + ( Z x. ( 1 - t ) ) ) ) ) ) ` z ) )
257	256	fveq2d 5869	. . . . . . . 8 |- ( t = z -> ( abs ` ( ( RR _D ( t e. ( 0 [,] 1 ) |-> ( F ` ( ( Y x. t ) + ( Z x. ( 1 - t ) ) ) ) ) ) ` t ) ) = ( abs ` ( ( RR _D ( t e. ( 0 [,] 1 ) |-> ( F ` ( ( Y x. t ) + ( Z x. ( 1 - t ) ) ) ) ) ) ` z ) ) )
258	257	breq1d 4412	. . . . . . 7 |- ( t = z -> ( ( abs ` ( ( RR _D ( t e. ( 0 [,] 1 ) |-> ( F ` ( ( Y x. t ) + ( Z x. ( 1 - t ) ) ) ) ) ) ` t ) ) <_ ( M x. ( abs ` ( Y - Z ) ) ) <-> ( abs ` ( ( RR _D ( t e. ( 0 [,] 1 ) |-> ( F ` ( ( Y x. t ) + ( Z x. ( 1 - t ) ) ) ) ) ) ` z ) ) <_ ( M x. ( abs ` ( Y - Z ) ) ) ) )
259	244, 255, 258	cbvral 3015	. . . . . 6 |- ( A. t e. ( 0 (,) 1 ) ( abs ` ( ( RR _D ( t e. ( 0 [,] 1 ) |-> ( F ` ( ( Y x. t ) + ( Z x. ( 1 - t ) ) ) ) ) ) ` t ) ) <_ ( M x. ( abs ` ( Y - Z ) ) ) <-> A. z e. ( 0 (,) 1 ) ( abs ` ( ( RR _D ( t e. ( 0 [,] 1 ) |-> ( F ` ( ( Y x. t ) + ( Z x. ( 1 - t ) ) ) ) ) ) ` z ) ) <_ ( M x. ( abs ` ( Y - Z ) ) ) )
260	243, 259	sylib 200	. . . . 5 |- ( ( ph /\ ( Y e. B /\ Z e. B ) ) -> A. z e. ( 0 (,) 1 ) ( abs ` ( ( RR _D ( t e. ( 0 [,] 1 ) |-> ( F ` ( ( Y x. t ) + ( Z x. ( 1 - t ) ) ) ) ) ) ` z ) ) <_ ( M x. ( abs ` ( Y - Z ) ) ) )
261	260	r19.21bi 2757	. . . 4 |- ( ( ( ph /\ ( Y e. B /\ Z e. B ) ) /\ z e. ( 0 (,) 1 ) ) -> ( abs ` ( ( RR _D ( t e. ( 0 [,] 1 ) |-> ( F ` ( ( Y x. t ) + ( Z x. ( 1 - t ) ) ) ) ) ) ` z ) ) <_ ( M x. ( abs ` ( Y - Z ) ) ) )
262	3, 4, 107, 206, 210, 261	dvlip 22945	. . 3 |- ( ( ( ph /\ ( Y e. B /\ Z e. B ) ) /\ ( 1 e. ( 0 [,] 1 ) /\ 0 e. ( 0 [,] 1 ) ) ) -> ( abs ` ( ( ( t e. ( 0 [,] 1 ) |-> ( F ` ( ( Y x. t ) + ( Z x. ( 1 - t ) ) ) ) ) ` 1 ) - ( ( t e. ( 0 [,] 1 ) |-> ( F ` ( ( Y x. t ) + ( Z x. ( 1 - t ) ) ) ) ) ` 0 ) ) ) <_ ( ( M x. ( abs ` ( Y - Z ) ) ) x. ( abs ` ( 1 - 0 ) ) ) )
263	1, 2, 262	mpanr12 691	. 2 |- ( ( ph /\ ( Y e. B /\ Z e. B ) ) -> ( abs ` ( ( ( t e. ( 0 [,] 1 ) |-> ( F ` ( ( Y x. t ) + ( Z x. ( 1 - t ) ) ) ) ) ` 1 ) - ( ( t e. ( 0 [,] 1 ) |-> ( F ` ( ( Y x. t ) + ( Z x. ( 1 - t ) ) ) ) ) ` 0 ) ) ) <_ ( ( M x. ( abs ` ( Y - Z ) ) ) x. ( abs ` ( 1 - 0 ) ) ) )
264		oveq2 6298	. . . . . . . . 9 |- ( t = 1 -> ( Y x. t ) = ( Y x. 1 ) )
265		oveq2 6298	. . . . . . . . . . 11 |- ( t = 1 -> ( 1 - t ) = ( 1 - 1 ) )
266		1m1e0 10678	. . . . . . . . . . 11 |- ( 1 - 1 ) = 0
267	265, 266	syl6eq 2501	. . . . . . . . . 10 |- ( t = 1 -> ( 1 - t ) = 0 )
268	267	oveq2d 6306	. . . . . . . . 9 |- ( t = 1 -> ( Z x. ( 1 - t ) ) = ( Z x. 0 ) )
269	264, 268	oveq12d 6308	. . . . . . . 8 |- ( t = 1 -> ( ( Y x. t ) + ( Z x. ( 1 - t ) ) ) = ( ( Y x. 1 ) + ( Z x. 0 ) ) )
270	269	fveq2d 5869	. . . . . . 7 |- ( t = 1 -> ( F ` ( ( Y x. t ) + ( Z x. ( 1 - t ) ) ) ) = ( F ` ( ( Y x. 1 ) + ( Z x. 0 ) ) ) )
271		eqid 2451	. . . . . . 7 |- ( t e. ( 0 [,] 1 ) |-> ( F ` ( ( Y x. t ) + ( Z x. ( 1 - t ) ) ) ) ) = ( t e. ( 0 [,] 1 ) |-> ( F ` ( ( Y x. t ) + ( Z x. ( 1 - t ) ) ) ) )
272		fvex 5875	. . . . . . 7 |- ( F ` ( ( Y x. 1 ) + ( Z x. 0 ) ) ) e. _V
273	270, 271, 272	fvmpt 5948	. . . . . 6 |- ( 1 e. ( 0 [,] 1 ) -> ( ( t e. ( 0 [,] 1 ) |-> ( F ` ( ( Y x. t ) + ( Z x. ( 1 - t ) ) ) ) ) ` 1 ) = ( F ` ( ( Y x. 1 ) + ( Z x. 0 ) ) ) )
274	1, 273	ax-mp 5	. . . . 5 |- ( ( t e. ( 0 [,] 1 ) |-> ( F ` ( ( Y x. t ) + ( Z x. ( 1 - t ) ) ) ) ) ` 1 ) = ( F ` ( ( Y x. 1 ) + ( Z x. 0 ) ) )
275	24	mul01d 9832	. . . . . . . 8 |- ( ( ph /\ ( Y e. B /\ Z e. B ) ) -> ( Z x. 0 ) = 0 )
276	149, 275	oveq12d 6308	. . . . . . 7 |- ( ( ph /\ ( Y e. B /\ Z e. B ) ) -> ( ( Y x. 1 ) + ( Z x. 0 ) ) = ( Y + 0 ) )
277	15	addid1d 9833	. . . . . . 7 |- ( ( ph /\ ( Y e. B /\ Z e. B ) ) -> ( Y + 0 ) = Y )
278	276, 277	eqtrd 2485	. . . . . 6 |- ( ( ph /\ ( Y e. B /\ Z e. B ) ) -> ( ( Y x. 1 ) + ( Z x. 0 ) ) = Y )
279	278	fveq2d 5869	. . . . 5 |- ( ( ph /\ ( Y e. B /\ Z e. B ) ) -> ( F ` ( ( Y x. 1 ) + ( Z x. 0 ) ) ) = ( F ` Y ) )
280	274, 279	syl5eq 2497	. . . 4 |- ( ( ph /\ ( Y e. B /\ Z e. B ) ) -> ( ( t e. ( 0 [,] 1 ) |-> ( F ` ( ( Y x. t ) + ( Z x. ( 1 - t ) ) ) ) ) ` 1 ) = ( F ` Y ) )
281		oveq2 6298	. . . . . . . . 9 |- ( t = 0 -> ( Y x. t ) = ( Y x. 0 ) )
282		oveq2 6298	. . . . . . . . . . 11 |- ( t = 0 -> ( 1 - t ) = ( 1 - 0 ) )
283		1m0e1 10720	. . . . . . . . . . 11 |- ( 1 - 0 ) = 1
284	282, 283	syl6eq 2501	. . . . . . . . . 10 |- ( t = 0 -> ( 1 - t ) = 1 )
285	284	oveq2d 6306	. . . . . . . . 9 |- ( t = 0 -> ( Z x. ( 1 - t ) ) = ( Z x. 1 ) )
286	281, 285	oveq12d 6308	. . . . . . . 8 |- ( t = 0 -> ( ( Y x. t ) + ( Z x. ( 1 - t ) ) ) = ( ( Y x. 0 ) + ( Z x. 1 ) ) )
287	286	fveq2d 5869	. . . . . . 7 |- ( t = 0 -> ( F ` ( ( Y x. t ) + ( Z x. ( 1 - t ) ) ) ) = ( F ` ( ( Y x. 0 ) + ( Z x. 1 ) ) ) )
288		fvex 5875	. . . . . . 7 |- ( F ` ( ( Y x. 0 ) + ( Z x. 1 ) ) ) e. _V
289	287, 271, 288	fvmpt 5948	. . . . . 6 |- ( 0 e. ( 0 [,] 1 ) -> ( ( t e. ( 0 [,] 1 ) |-> ( F ` ( ( Y x. t ) + ( Z x. ( 1 - t ) ) ) ) ) ` 0 ) = ( F ` ( ( Y x. 0 ) + ( Z x. 1 ) ) ) )
290	2, 289	ax-mp 5	. . . . 5 |- ( ( t e. ( 0 [,] 1 ) |-> ( F ` ( ( Y x. t ) + ( Z x. ( 1 - t ) ) ) ) ) ` 0 ) = ( F ` ( ( Y x. 0 ) + ( Z x. 1 ) ) )
291	15	mul01d 9832	. . . . . . . 8 |- ( ( ph /\ ( Y e. B /\ Z e. B ) ) -> ( Y x. 0 ) = 0 )
292	24	mulid1d 9660	. . . . . . . 8 |- ( ( ph /\ ( Y e. B /\ Z e. B ) ) -> ( Z x. 1 ) = Z )
293	291, 292	oveq12d 6308	. . . . . . 7 |- ( ( ph /\ ( Y e. B /\ Z e. B ) ) -> ( ( Y x. 0 ) + ( Z x. 1 ) ) = ( 0 + Z ) )
294	24	addid2d 9834	. . . . . . 7 |- ( ( ph /\ ( Y e. B /\ Z e. B ) ) -> ( 0 + Z ) = Z )
295	293, 294	eqtrd 2485	. . . . . 6 |- ( ( ph /\ ( Y e. B /\ Z e. B ) ) -> ( ( Y x. 0 ) + ( Z x. 1 ) ) = Z )
296	295	fveq2d 5869	. . . . 5 |- ( ( ph /\ ( Y e. B /\ Z e. B ) ) -> ( F ` ( ( Y x. 0 ) + ( Z x. 1 ) ) ) = ( F ` Z ) )
297	290, 296	syl5eq 2497	. . . 4 |- ( ( ph /\ ( Y e. B /\ Z e. B ) ) -> ( ( t e. ( 0 [,] 1 ) |-> ( F ` ( ( Y x. t ) + ( Z x. ( 1 - t ) ) ) ) ) ` 0 ) = ( F ` Z ) )
298	280, 297	oveq12d 6308	. . 3 |- ( ( ph /\ ( Y e. B /\ Z e. B ) ) -> ( ( ( t e. ( 0 [,] 1 ) |-> ( F ` ( ( Y x. t ) + ( Z x. ( 1 - t ) ) ) ) ) ` 1 ) - ( ( t e. ( 0 [,] 1 ) |-> ( F ` ( ( Y x. t ) + ( Z x. ( 1 - t ) ) ) ) ) ` 0 ) ) = ( ( F ` Y ) - ( F ` Z ) ) )
299	298	fveq2d 5869	. 2 |- ( ( ph /\ ( Y e. B /\ Z e. B ) ) -> ( abs ` ( ( ( t e. ( 0 [,] 1 ) |-> ( F ` ( ( Y x. t ) + ( Z x. ( 1 - t ) ) ) ) ) ` 1 ) - ( ( t e. ( 0 [,] 1 ) |-> ( F ` ( ( Y x. t ) + ( Z x. ( 1 - t ) ) ) ) ) ` 0 ) ) ) = ( abs ` ( ( F ` Y ) - ( F ` Z ) ) ) )
300	283	fveq2i 5868	. . . . 5 |- ( abs ` ( 1 - 0 ) ) = ( abs ` 1 )
301		abs1 13360	. . . . 5 |- ( abs ` 1 ) = 1
302	300, 301	eqtri 2473	. . . 4 |- ( abs ` ( 1 - 0 ) ) = 1
303	302	oveq2i 6301	. . 3 |- ( ( M x. ( abs ` ( Y - Z ) ) ) x. ( abs ` ( 1 - 0 ) ) ) = ( ( M x. ( abs ` ( Y - Z ) ) ) x. 1 )
304	210	recnd 9669	. . . 4 |- ( ( ph /\ ( Y e. B /\ Z e. B ) ) -> ( M x. ( abs ` ( Y - Z ) ) ) e. CC )
305	304	mulid1d 9660	. . 3 |- ( ( ph /\ ( Y e. B /\ Z e. B ) ) -> ( ( M x. ( abs ` ( Y - Z ) ) ) x. 1 ) = ( M x. ( abs ` ( Y - Z ) ) ) )
306	303, 305	syl5eq 2497	. 2 |- ( ( ph /\ ( Y e. B /\ Z e. B ) ) -> ( ( M x. ( abs ` ( Y - Z ) ) ) x. ( abs ` ( 1 - 0 ) ) ) = ( M x. ( abs ` ( Y - Z ) ) ) )
307	263, 299, 306	3brtr3d 4432	1 |- ( ( ph /\ ( Y e. B /\ Z e. B ) ) -> ( abs ` ( ( F ` Y ) - ( F ` Z ) ) ) <_ ( M x. ( abs ` ( Y - Z ) ) ) )

Syntax hints:   -> wi 4   <-> wb 188   /\ wa 371   = wceq 1444   e. wcel 1887   A.wral 2737   _Vcvv 3045   i^i cin 3403   C_ wss 3404   {cpr 3970   class class class wbr 4402   |-> cmpt 4461   dom cdm 4834   ran crn 4835   |` cres 4836   o. ccom 4838   -->wf 5578   ` cfv 5582  (class class class)co 6290   CCcc 9537   RRcr 9538   0cc0 9539   1c1 9540   + caddc 9542   x. cmul 9544   RR*cxr 9674   <_ cle 9676   - cmin 9860   -ucneg 9861   (,)cioo 11635   [,]cicc 11638   abscabs 13297   ↾_t crest 15319   TopOpenctopn 15320   topGenctg 15336   *Metcxmt 18955   ballcbl 18957  ℂ_fldccnfld 18970   Topctop 19917   intcnt 20032   Cn ccn 20240   tX ctx 20575   -cn->ccncf 21908   _D cdv 22818

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1669  ax-4 1682  ax-5 1758  ax-6 1805  ax-7 1851  ax-8 1889  ax-9 1896  ax-10 1915  ax-11 1920  ax-12 1933  ax-13 2091  ax-ext 2431  ax-rep 4515  ax-sep 4525  ax-nul 4534  ax-pow 4581  ax-pr 4639  ax-un 6583  ax-inf2 8146  ax-cnex 9595  ax-resscn 9596  ax-1cn 9597  ax-icn 9598  ax-addcl 9599  ax-addrcl 9600  ax-mulcl 9601  ax-mulrcl 9602  ax-mulcom 9603  ax-addass 9604  ax-mulass 9605  ax-distr 9606  ax-i2m1 9607  ax-1ne0 9608  ax-1rid 9609  ax-rnegex 9610  ax-rrecex 9611  ax-cnre 9612  ax-pre-lttri 9613  ax-pre-lttrn 9614  ax-pre-ltadd 9615  ax-pre-mulgt0 9616  ax-pre-sup 9617  ax-addf 9618  ax-mulf 9619

This theorem depends on definitions:  df-bi 189  df-or 372  df-an 373  df-3or 986  df-3an 987  df-tru 1447  df-ex 1664  df-nf 1668  df-sb 1798  df-eu 2303  df-mo 2304  df-clab 2438  df-cleq 2444  df-clel 2447  df-nfc 2581  df-ne 2624  df-nel 2625  df-ral 2742  df-rex 2743  df-reu 2744  df-rmo 2745  df-rab 2746  df-v 3047  df-sbc 3268  df-csb 3364  df-dif 3407  df-un 3409  df-in 3411  df-ss 3418  df-pss 3420  df-nul 3732  df-if 3882  df-pw 3953  df-sn 3969  df-pr 3971  df-tp 3973  df-op 3975  df-uni 4199  df-int 4235  df-iun 4280  df-iin 4281  df-br 4403  df-opab 4462  df-mpt 4463  df-tr 4498  df-eprel 4745  df-id 4749  df-po 4755  df-so 4756  df-fr 4793  df-se 4794  df-we 4795  df-xp 4840  df-rel 4841  df-cnv 4842  df-co 4843  df-dm 4844  df-rn 4845  df-res 4846  df-ima 4847  df-pred 5380  df-ord 5426  df-on 5427  df-lim 5428  df-suc 5429  df-iota 5546  df-fun 5584  df-fn 5585  df-f 5586  df-f1 5587  df-fo 5588  df-f1o 5589  df-fv 5590  df-isom 5591  df-riota 6252  df-ov 6293  df-oprab 6294  df-mpt2 6295  df-of 6531  df-om 6693  df-1st 6793  df-2nd 6794  df-supp 6915  df-wrecs 7028  df-recs 7090  df-rdg 7128  df-1o 7182  df-2o 7183  df-oadd 7186  df-er 7363  df-map 7474  df-pm 7475  df-ixp 7523  df-en 7570  df-dom 7571  df-sdom 7572  df-fin 7573  df-fsupp 7884  df-fi 7925  df-sup 7956  df-inf 7957  df-oi 8025  df-card 8373  df-cda 8598  df-pnf 9677  df-mnf 9678  df-xr 9679  df-ltxr 9680  df-le 9681  df-sub 9862  df-neg 9863  df-div 10270  df-nn 10610  df-2 10668  df-3 10669  df-4 10670  df-5 10671  df-6 10672  df-7 10673  df-8 10674  df-9 10675  df-10 10676  df-n0 10870  df-z 10938  df-dec 11052  df-uz 11160  df-q 11265  df-rp 11303  df-xneg 11409  df-xadd 11410  df-xmul 11411  df-ioo 11639  df-ico 11641  df-icc 11642  df-fz 11785  df-fzo 11916  df-seq 12214  df-exp 12273  df-hash 12516  df-cj 13162  df-re 13163  df-im 13164  df-sqrt 13298  df-abs 13299  df-struct 15123  df-ndx 15124  df-slot 15125  df-base 15126  df-sets 15127  df-ress 15128  df-plusg 15203  df-mulr 15204  df-starv 15205  df-sca 15206  df-vsca 15207  df-ip 15208  df-tset 15209  df-ple 15210  df-ds 15212  df-unif 15213  df-hom 15214  df-cco 15215  df-rest 15321  df-topn 15322  df-0g 15340  df-gsum 15341  df-topgen 15342  df-pt 15343  df-prds 15346  df-xrs 15400  df-qtop 15406  df-imas 15407  df-xps 15410  df-mre 15492  df-mrc 15493  df-acs 15495  df-mgm 16488  df-sgrp 16527  df-mnd 16537  df-submnd 16583  df-mulg 16676  df-cntz 16971  df-cmn 17432  df-psmet 18962  df-xmet 18963  df-met 18964  df-bl 18965  df-mopn 18966  df-fbas 18967  df-fg 18968  df-cnfld 18971  df-top 19921  df-bases 19922  df-topon 19923  df-topsp 19924  df-cld 20034  df-ntr 20035  df-cls 20036  df-nei 20114  df-lp 20152  df-perf 20153  df-cn 20243  df-cnp 20244  df-haus 20331  df-cmp 20402  df-tx 20577  df-hmeo 20770  df-fil 20861  df-fm 20953  df-flim 20954  df-flf 20955  df-xms 21335  df-ms 21336  df-tms 21337  df-cncf 21910  df-limc 22821  df-dv 22822

This theorem is referenced by:  dvlip2  22947  dv11cn  22953