Metamath Proof Explorer

Theorem axcontlem6

Description: Lemma for axcont . State the defining properties of the value of F . (Contributed by Scott Fenton, 19-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 axcontlem6 
|- ( ( ( ( N e. NN /\ Z e. ( EE ` N ) /\ U e. ( EE ` N ) ) /\ Z =/= U ) /\ P e. D ) -> ( ( F ` P ) e. ( 0 [,) +oo ) /\ A. i e. ( 1 ... N ) ( P ` i ) = ( ( ( 1 - ( F ` P ) ) x. ( Z ` i ) ) + ( ( F ` P ) 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 eqid 
 |-  ( F ` P ) = ( F ` P )
4 2 axcontlem1 
 |-  F = { <. y , s >. | ( y e. D /\ ( s e. ( 0 [,) +oo ) /\ A. j e. ( 1 ... N ) ( y ` j ) = ( ( ( 1 - s ) x. ( Z ` j ) ) + ( s x. ( U ` j ) ) ) ) ) }
5 1 4 axcontlem5 
 |-  ( ( ( ( N e. NN /\ Z e. ( EE ` N ) /\ U e. ( EE ` N ) ) /\ Z =/= U ) /\ P e. D ) -> ( ( F ` P ) = ( F ` P ) <-> ( ( F ` P ) e. ( 0 [,) +oo ) /\ A. j e. ( 1 ... N ) ( P ` j ) = ( ( ( 1 - ( F ` P ) ) x. ( Z ` j ) ) + ( ( F ` P ) x. ( U ` j ) ) ) ) ) )
6 3 5 mpbii 
 |-  ( ( ( ( N e. NN /\ Z e. ( EE ` N ) /\ U e. ( EE ` N ) ) /\ Z =/= U ) /\ P e. D ) -> ( ( F ` P ) e. ( 0 [,) +oo ) /\ A. j e. ( 1 ... N ) ( P ` j ) = ( ( ( 1 - ( F ` P ) ) x. ( Z ` j ) ) + ( ( F ` P ) x. ( U ` j ) ) ) ) )
7 fveq2 
 |-  ( j = i -> ( P ` j ) = ( P ` i ) )
8 fveq2 
 |-  ( j = i -> ( Z ` j ) = ( Z ` i ) )
9 8 oveq2d 
 |-  ( j = i -> ( ( 1 - ( F ` P ) ) x. ( Z ` j ) ) = ( ( 1 - ( F ` P ) ) x. ( Z ` i ) ) )
10 fveq2 
 |-  ( j = i -> ( U ` j ) = ( U ` i ) )
11 10 oveq2d 
 |-  ( j = i -> ( ( F ` P ) x. ( U ` j ) ) = ( ( F ` P ) x. ( U ` i ) ) )
12 9 11 oveq12d 
 |-  ( j = i -> ( ( ( 1 - ( F ` P ) ) x. ( Z ` j ) ) + ( ( F ` P ) x. ( U ` j ) ) ) = ( ( ( 1 - ( F ` P ) ) x. ( Z ` i ) ) + ( ( F ` P ) x. ( U ` i ) ) ) )
13 7 12 eqeq12d 
 |-  ( j = i -> ( ( P ` j ) = ( ( ( 1 - ( F ` P ) ) x. ( Z ` j ) ) + ( ( F ` P ) x. ( U ` j ) ) ) <-> ( P ` i ) = ( ( ( 1 - ( F ` P ) ) x. ( Z ` i ) ) + ( ( F ` P ) x. ( U ` i ) ) ) ) )
14 13 cbvralvw 
 |-  ( A. j e. ( 1 ... N ) ( P ` j ) = ( ( ( 1 - ( F ` P ) ) x. ( Z ` j ) ) + ( ( F ` P ) x. ( U ` j ) ) ) <-> A. i e. ( 1 ... N ) ( P ` i ) = ( ( ( 1 - ( F ` P ) ) x. ( Z ` i ) ) + ( ( F ` P ) x. ( U ` i ) ) ) )
15 14 anbi2i 
 |-  ( ( ( F ` P ) e. ( 0 [,) +oo ) /\ A. j e. ( 1 ... N ) ( P ` j ) = ( ( ( 1 - ( F ` P ) ) x. ( Z ` j ) ) + ( ( F ` P ) x. ( U ` j ) ) ) ) <-> ( ( F ` P ) e. ( 0 [,) +oo ) /\ A. i e. ( 1 ... N ) ( P ` i ) = ( ( ( 1 - ( F ` P ) ) x. ( Z ` i ) ) + ( ( F ` P ) x. ( U ` i ) ) ) ) )
16 6 15 sylib 
 |-  ( ( ( ( N e. NN /\ Z e. ( EE ` N ) /\ U e. ( EE ` N ) ) /\ Z =/= U ) /\ P e. D ) -> ( ( F ` P ) e. ( 0 [,) +oo ) /\ A. i e. ( 1 ... N ) ( P ` i ) = ( ( ( 1 - ( F ` P ) ) x. ( Z ` i ) ) + ( ( F ` P ) x. ( U ` i ) ) ) ) )