Metamath Proof Explorer

Theorem axcontlem5

Description: Lemma for axcont . Compute the value of F . (Contributed by Scott Fenton, 18-Jun-2013)

Ref Expression
Hypotheses axcontlem5.1 
|- D = { p e. ( EE ` N ) | ( U Btwn <. Z , p >. \/ p Btwn <. Z , U >. ) }
axcontlem5.2 
|- F = { <. x , t >. | ( x e. D /\ ( t e. ( 0 [,) +oo ) /\ A. i e. ( 1 ... N ) ( x ` i ) = ( ( ( 1 - t ) x. ( Z ` i ) ) + ( t x. ( U ` i ) ) ) ) ) }
Assertion axcontlem5 
|- ( ( ( ( N e. NN /\ Z e. ( EE ` N ) /\ U e. ( EE ` N ) ) /\ Z =/= U ) /\ P e. D ) -> ( ( F ` P ) = T <-> ( T e. ( 0 [,) +oo ) /\ A. i e. ( 1 ... N ) ( P ` i ) = ( ( ( 1 - T ) x. ( Z ` i ) ) + ( T x. ( U ` i ) ) ) ) ) )

Proof

Step Hyp Ref Expression
1 axcontlem5.1 
 |-  D = { p e. ( EE ` N ) | ( U Btwn <. Z , p >. \/ p Btwn <. Z , U >. ) }
2 axcontlem5.2 
 |-  F = { <. x , t >. | ( x e. D /\ ( t e. ( 0 [,) +oo ) /\ A. i e. ( 1 ... N ) ( x ` i ) = ( ( ( 1 - t ) x. ( Z ` i ) ) + ( t x. ( U ` i ) ) ) ) ) }
3 1 2 axcontlem2 
 |-  ( ( ( N e. NN /\ Z e. ( EE ` N ) /\ U e. ( EE ` N ) ) /\ Z =/= U ) -> F : D -1-1-onto-> ( 0 [,) +oo ) )
4 f1of 
 |-  ( F : D -1-1-onto-> ( 0 [,) +oo ) -> F : D --> ( 0 [,) +oo ) )
5 3 4 syl 
 |-  ( ( ( N e. NN /\ Z e. ( EE ` N ) /\ U e. ( EE ` N ) ) /\ Z =/= U ) -> F : D --> ( 0 [,) +oo ) )
6 5 ffvelcdmda 
 |-  ( ( ( ( N e. NN /\ Z e. ( EE ` N ) /\ U e. ( EE ` N ) ) /\ Z =/= U ) /\ P e. D ) -> ( F ` P ) e. ( 0 [,) +oo ) )
7 eleq1 
 |-  ( ( F ` P ) = T -> ( ( F ` P ) e. ( 0 [,) +oo ) <-> T e. ( 0 [,) +oo ) ) )
8 6 7 syl5ibcom 
 |-  ( ( ( ( N e. NN /\ Z e. ( EE ` N ) /\ U e. ( EE ` N ) ) /\ Z =/= U ) /\ P e. D ) -> ( ( F ` P ) = T -> T e. ( 0 [,) +oo ) ) )
9 simpl 
 |-  ( ( T e. ( 0 [,) +oo ) /\ A. i e. ( 1 ... N ) ( P ` i ) = ( ( ( 1 - T ) x. ( Z ` i ) ) + ( T x. ( U ` i ) ) ) ) -> T e. ( 0 [,) +oo ) )
10 9 a1i 
 |-  ( ( ( ( N e. NN /\ Z e. ( EE ` N ) /\ U e. ( EE ` N ) ) /\ Z =/= U ) /\ P e. D ) -> ( ( T e. ( 0 [,) +oo ) /\ A. i e. ( 1 ... N ) ( P ` i ) = ( ( ( 1 - T ) x. ( Z ` i ) ) + ( T x. ( U ` i ) ) ) ) -> T e. ( 0 [,) +oo ) ) )
11 f1ofn 
 |-  ( F : D -1-1-onto-> ( 0 [,) +oo ) -> F Fn D )
12 3 11 syl 
 |-  ( ( ( N e. NN /\ Z e. ( EE ` N ) /\ U e. ( EE ` N ) ) /\ Z =/= U ) -> F Fn D )
13 fnbrfvb 
 |-  ( ( F Fn D /\ P e. D ) -> ( ( F ` P ) = T <-> P F T ) )
14 12 13 sylan 
 |-  ( ( ( ( N e. NN /\ Z e. ( EE ` N ) /\ U e. ( EE ` N ) ) /\ Z =/= U ) /\ P e. D ) -> ( ( F ` P ) = T <-> P F T ) )
15 14 3adant3 
 |-  ( ( ( ( N e. NN /\ Z e. ( EE ` N ) /\ U e. ( EE ` N ) ) /\ Z =/= U ) /\ P e. D /\ T e. ( 0 [,) +oo ) ) -> ( ( F ` P ) = T <-> P F T ) )
16 eleq1 
 |-  ( x = P -> ( x e. D <-> P e. D ) )
17 fveq1 
 |-  ( x = P -> ( x ` i ) = ( P ` i ) )
18 17 eqeq1d 
 |-  ( x = P -> ( ( x ` i ) = ( ( ( 1 - t ) x. ( Z ` i ) ) + ( t x. ( U ` i ) ) ) <-> ( P ` i ) = ( ( ( 1 - t ) x. ( Z ` i ) ) + ( t x. ( U ` i ) ) ) ) )
19 18 ralbidv 
 |-  ( x = P -> ( A. i e. ( 1 ... N ) ( x ` i ) = ( ( ( 1 - t ) x. ( Z ` i ) ) + ( t x. ( U ` i ) ) ) <-> A. i e. ( 1 ... N ) ( P ` i ) = ( ( ( 1 - t ) x. ( Z ` i ) ) + ( t x. ( U ` i ) ) ) ) )
20 19 anbi2d 
 |-  ( x = P -> ( ( t e. ( 0 [,) +oo ) /\ A. i e. ( 1 ... N ) ( x ` i ) = ( ( ( 1 - t ) x. ( Z ` i ) ) + ( t x. ( U ` i ) ) ) ) <-> ( t e. ( 0 [,) +oo ) /\ A. i e. ( 1 ... N ) ( P ` i ) = ( ( ( 1 - t ) x. ( Z ` i ) ) + ( t x. ( U ` i ) ) ) ) ) )
21 16 20 anbi12d 
 |-  ( x = P -> ( ( x e. D /\ ( t e. ( 0 [,) +oo ) /\ A. i e. ( 1 ... N ) ( x ` i ) = ( ( ( 1 - t ) x. ( Z ` i ) ) + ( t x. ( U ` i ) ) ) ) ) <-> ( P e. D /\ ( t e. ( 0 [,) +oo ) /\ A. i e. ( 1 ... N ) ( P ` i ) = ( ( ( 1 - t ) x. ( Z ` i ) ) + ( t x. ( U ` i ) ) ) ) ) ) )
22 eleq1 
 |-  ( t = T -> ( t e. ( 0 [,) +oo ) <-> T e. ( 0 [,) +oo ) ) )
23 oveq2 
 |-  ( t = T -> ( 1 - t ) = ( 1 - T ) )
24 23 oveq1d 
 |-  ( t = T -> ( ( 1 - t ) x. ( Z ` i ) ) = ( ( 1 - T ) x. ( Z ` i ) ) )
25 oveq1 
 |-  ( t = T -> ( t x. ( U ` i ) ) = ( T x. ( U ` i ) ) )
26 24 25 oveq12d 
 |-  ( t = T -> ( ( ( 1 - t ) x. ( Z ` i ) ) + ( t x. ( U ` i ) ) ) = ( ( ( 1 - T ) x. ( Z ` i ) ) + ( T x. ( U ` i ) ) ) )
27 26 eqeq2d 
 |-  ( t = T -> ( ( P ` i ) = ( ( ( 1 - t ) x. ( Z ` i ) ) + ( t x. ( U ` i ) ) ) <-> ( P ` i ) = ( ( ( 1 - T ) x. ( Z ` i ) ) + ( T x. ( U ` i ) ) ) ) )
28 27 ralbidv 
 |-  ( t = T -> ( A. i e. ( 1 ... N ) ( P ` i ) = ( ( ( 1 - t ) x. ( Z ` i ) ) + ( t x. ( U ` i ) ) ) <-> A. i e. ( 1 ... N ) ( P ` i ) = ( ( ( 1 - T ) x. ( Z ` i ) ) + ( T x. ( U ` i ) ) ) ) )
29 22 28 anbi12d 
 |-  ( t = T -> ( ( t e. ( 0 [,) +oo ) /\ A. i e. ( 1 ... N ) ( P ` i ) = ( ( ( 1 - t ) x. ( Z ` i ) ) + ( t x. ( U ` i ) ) ) ) <-> ( T e. ( 0 [,) +oo ) /\ A. i e. ( 1 ... N ) ( P ` i ) = ( ( ( 1 - T ) x. ( Z ` i ) ) + ( T x. ( U ` i ) ) ) ) ) )
30 29 anbi2d 
 |-  ( t = T -> ( ( P e. D /\ ( t e. ( 0 [,) +oo ) /\ A. i e. ( 1 ... N ) ( P ` i ) = ( ( ( 1 - t ) x. ( Z ` i ) ) + ( t x. ( U ` i ) ) ) ) ) <-> ( P e. D /\ ( T e. ( 0 [,) +oo ) /\ A. i e. ( 1 ... N ) ( P ` i ) = ( ( ( 1 - T ) x. ( Z ` i ) ) + ( T x. ( U ` i ) ) ) ) ) ) )
31 anass 
 |-  ( ( ( P e. D /\ T e. ( 0 [,) +oo ) ) /\ T e. ( 0 [,) +oo ) ) <-> ( P e. D /\ ( T e. ( 0 [,) +oo ) /\ T e. ( 0 [,) +oo ) ) ) )
32 anidm 
 |-  ( ( T e. ( 0 [,) +oo ) /\ T e. ( 0 [,) +oo ) ) <-> T e. ( 0 [,) +oo ) )
33 32 anbi2i 
 |-  ( ( P e. D /\ ( T e. ( 0 [,) +oo ) /\ T e. ( 0 [,) +oo ) ) ) <-> ( P e. D /\ T e. ( 0 [,) +oo ) ) )
34 31 33 bitr2i 
 |-  ( ( P e. D /\ T e. ( 0 [,) +oo ) ) <-> ( ( P e. D /\ T e. ( 0 [,) +oo ) ) /\ T e. ( 0 [,) +oo ) ) )
35 34 anbi1i 
 |-  ( ( ( P e. D /\ T e. ( 0 [,) +oo ) ) /\ A. i e. ( 1 ... N ) ( P ` i ) = ( ( ( 1 - T ) x. ( Z ` i ) ) + ( T x. ( U ` i ) ) ) ) <-> ( ( ( P e. D /\ T e. ( 0 [,) +oo ) ) /\ T e. ( 0 [,) +oo ) ) /\ A. i e. ( 1 ... N ) ( P ` i ) = ( ( ( 1 - T ) x. ( Z ` i ) ) + ( T x. ( U ` i ) ) ) ) )
36 anass 
 |-  ( ( ( P e. D /\ T e. ( 0 [,) +oo ) ) /\ A. i e. ( 1 ... N ) ( P ` i ) = ( ( ( 1 - T ) x. ( Z ` i ) ) + ( T x. ( U ` i ) ) ) ) <-> ( P e. D /\ ( T e. ( 0 [,) +oo ) /\ A. i e. ( 1 ... N ) ( P ` i ) = ( ( ( 1 - T ) x. ( Z ` i ) ) + ( T x. ( U ` i ) ) ) ) ) )
37 anass 
 |-  ( ( ( ( P e. D /\ T e. ( 0 [,) +oo ) ) /\ T e. ( 0 [,) +oo ) ) /\ A. i e. ( 1 ... N ) ( P ` i ) = ( ( ( 1 - T ) x. ( Z ` i ) ) + ( T x. ( U ` i ) ) ) ) <-> ( ( P e. D /\ T e. ( 0 [,) +oo ) ) /\ ( T e. ( 0 [,) +oo ) /\ A. i e. ( 1 ... N ) ( P ` i ) = ( ( ( 1 - T ) x. ( Z ` i ) ) + ( T x. ( U ` i ) ) ) ) ) )
38 35 36 37 3bitr3i 
 |-  ( ( P e. D /\ ( T e. ( 0 [,) +oo ) /\ A. i e. ( 1 ... N ) ( P ` i ) = ( ( ( 1 - T ) x. ( Z ` i ) ) + ( T x. ( U ` i ) ) ) ) ) <-> ( ( P e. D /\ T e. ( 0 [,) +oo ) ) /\ ( T e. ( 0 [,) +oo ) /\ A. i e. ( 1 ... N ) ( P ` i ) = ( ( ( 1 - T ) x. ( Z ` i ) ) + ( T x. ( U ` i ) ) ) ) ) )
39 30 38 bitrdi 
 |-  ( t = T -> ( ( P e. D /\ ( t e. ( 0 [,) +oo ) /\ A. i e. ( 1 ... N ) ( P ` i ) = ( ( ( 1 - t ) x. ( Z ` i ) ) + ( t x. ( U ` i ) ) ) ) ) <-> ( ( P e. D /\ T e. ( 0 [,) +oo ) ) /\ ( T e. ( 0 [,) +oo ) /\ A. i e. ( 1 ... N ) ( P ` i ) = ( ( ( 1 - T ) x. ( Z ` i ) ) + ( T x. ( U ` i ) ) ) ) ) ) )
40 21 39 2 brabg 
 |-  ( ( P e. D /\ T e. ( 0 [,) +oo ) ) -> ( P F T <-> ( ( P e. D /\ T e. ( 0 [,) +oo ) ) /\ ( T e. ( 0 [,) +oo ) /\ A. i e. ( 1 ... N ) ( P ` i ) = ( ( ( 1 - T ) x. ( Z ` i ) ) + ( T x. ( U ` i ) ) ) ) ) ) )
41 40 bianabs 
 |-  ( ( P e. D /\ T e. ( 0 [,) +oo ) ) -> ( P F T <-> ( T e. ( 0 [,) +oo ) /\ A. i e. ( 1 ... N ) ( P ` i ) = ( ( ( 1 - T ) x. ( Z ` i ) ) + ( T x. ( U ` i ) ) ) ) ) )
42 41 3adant1 
 |-  ( ( ( ( N e. NN /\ Z e. ( EE ` N ) /\ U e. ( EE ` N ) ) /\ Z =/= U ) /\ P e. D /\ T e. ( 0 [,) +oo ) ) -> ( P F T <-> ( T e. ( 0 [,) +oo ) /\ A. i e. ( 1 ... N ) ( P ` i ) = ( ( ( 1 - T ) x. ( Z ` i ) ) + ( T x. ( U ` i ) ) ) ) ) )
43 15 42 bitrd 
 |-  ( ( ( ( N e. NN /\ Z e. ( EE ` N ) /\ U e. ( EE ` N ) ) /\ Z =/= U ) /\ P e. D /\ T e. ( 0 [,) +oo ) ) -> ( ( F ` P ) = T <-> ( T e. ( 0 [,) +oo ) /\ A. i e. ( 1 ... N ) ( P ` i ) = ( ( ( 1 - T ) x. ( Z ` i ) ) + ( T x. ( U ` i ) ) ) ) ) )
44 43 3expia 
 |-  ( ( ( ( N e. NN /\ Z e. ( EE ` N ) /\ U e. ( EE ` N ) ) /\ Z =/= U ) /\ P e. D ) -> ( T e. ( 0 [,) +oo ) -> ( ( F ` P ) = T <-> ( T e. ( 0 [,) +oo ) /\ A. i e. ( 1 ... N ) ( P ` i ) = ( ( ( 1 - T ) x. ( Z ` i ) ) + ( T x. ( U ` i ) ) ) ) ) ) )
45 8 10 44 pm5.21ndd 
 |-  ( ( ( ( N e. NN /\ Z e. ( EE ` N ) /\ U e. ( EE ` N ) ) /\ Z =/= U ) /\ P e. D ) -> ( ( F ` P ) = T <-> ( T e. ( 0 [,) +oo ) /\ A. i e. ( 1 ... N ) ( P ` i ) = ( ( ( 1 - T ) x. ( Z ` i ) ) + ( T x. ( U ` i ) ) ) ) ) )