Metamath Proof Explorer

Theorem axcontlem1

Description: Lemma for axcont . Change bound variables for later use. (Contributed by Scott Fenton, 20-Jun-2013)

Ref Expression
Hypothesis axcontlem1.1 
|- 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 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 ) ) ) ) ) }

Proof

Step Hyp Ref Expression
1 axcontlem1.1 
 |-  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 ) ) ) ) ) }
2 eleq1w 
 |-  ( x = y -> ( x e. D <-> y e. D ) )
3 2 adantr 
 |-  ( ( x = y /\ t = s ) -> ( x e. D <-> y e. D ) )
4 eleq1w 
 |-  ( t = s -> ( t e. ( 0 [,) +oo ) <-> s e. ( 0 [,) +oo ) ) )
5 4 adantl 
 |-  ( ( x = y /\ t = s ) -> ( t e. ( 0 [,) +oo ) <-> s e. ( 0 [,) +oo ) ) )
6 fveq1 
 |-  ( x = y -> ( x ` i ) = ( y ` i ) )
7 oveq2 
 |-  ( t = s -> ( 1 - t ) = ( 1 - s ) )
8 7 oveq1d 
 |-  ( t = s -> ( ( 1 - t ) x. ( Z ` i ) ) = ( ( 1 - s ) x. ( Z ` i ) ) )
9 oveq1 
 |-  ( t = s -> ( t x. ( U ` i ) ) = ( s x. ( U ` i ) ) )
10 8 9 oveq12d 
 |-  ( t = s -> ( ( ( 1 - t ) x. ( Z ` i ) ) + ( t x. ( U ` i ) ) ) = ( ( ( 1 - s ) x. ( Z ` i ) ) + ( s x. ( U ` i ) ) ) )
11 6 10 eqeqan12d 
 |-  ( ( x = y /\ t = s ) -> ( ( x ` i ) = ( ( ( 1 - t ) x. ( Z ` i ) ) + ( t x. ( U ` i ) ) ) <-> ( y ` i ) = ( ( ( 1 - s ) x. ( Z ` i ) ) + ( s x. ( U ` i ) ) ) ) )
12 11 ralbidv 
 |-  ( ( x = y /\ t = s ) -> ( A. i e. ( 1 ... N ) ( x ` i ) = ( ( ( 1 - t ) x. ( Z ` i ) ) + ( t x. ( U ` i ) ) ) <-> A. i e. ( 1 ... N ) ( y ` i ) = ( ( ( 1 - s ) x. ( Z ` i ) ) + ( s x. ( U ` i ) ) ) ) )
13 fveq2 
 |-  ( i = j -> ( y ` i ) = ( y ` j ) )
14 fveq2 
 |-  ( i = j -> ( Z ` i ) = ( Z ` j ) )
15 14 oveq2d 
 |-  ( i = j -> ( ( 1 - s ) x. ( Z ` i ) ) = ( ( 1 - s ) x. ( Z ` j ) ) )
16 fveq2 
 |-  ( i = j -> ( U ` i ) = ( U ` j ) )
17 16 oveq2d 
 |-  ( i = j -> ( s x. ( U ` i ) ) = ( s x. ( U ` j ) ) )
18 15 17 oveq12d 
 |-  ( i = j -> ( ( ( 1 - s ) x. ( Z ` i ) ) + ( s x. ( U ` i ) ) ) = ( ( ( 1 - s ) x. ( Z ` j ) ) + ( s x. ( U ` j ) ) ) )
19 13 18 eqeq12d 
 |-  ( i = j -> ( ( y ` i ) = ( ( ( 1 - s ) x. ( Z ` i ) ) + ( s x. ( U ` i ) ) ) <-> ( y ` j ) = ( ( ( 1 - s ) x. ( Z ` j ) ) + ( s x. ( U ` j ) ) ) ) )
20 19 cbvralvw 
 |-  ( A. i e. ( 1 ... N ) ( y ` i ) = ( ( ( 1 - s ) x. ( Z ` i ) ) + ( s x. ( U ` i ) ) ) <-> A. j e. ( 1 ... N ) ( y ` j ) = ( ( ( 1 - s ) x. ( Z ` j ) ) + ( s x. ( U ` j ) ) ) )
21 12 20 bitrdi 
 |-  ( ( x = y /\ t = s ) -> ( A. i e. ( 1 ... N ) ( x ` i ) = ( ( ( 1 - t ) x. ( Z ` i ) ) + ( t x. ( U ` i ) ) ) <-> A. j e. ( 1 ... N ) ( y ` j ) = ( ( ( 1 - s ) x. ( Z ` j ) ) + ( s x. ( U ` j ) ) ) ) )
22 5 21 anbi12d 
 |-  ( ( x = y /\ t = s ) -> ( ( t e. ( 0 [,) +oo ) /\ A. i e. ( 1 ... N ) ( x ` i ) = ( ( ( 1 - t ) x. ( Z ` i ) ) + ( t x. ( U ` i ) ) ) ) <-> ( s e. ( 0 [,) +oo ) /\ A. j e. ( 1 ... N ) ( y ` j ) = ( ( ( 1 - s ) x. ( Z ` j ) ) + ( s x. ( U ` j ) ) ) ) ) )
23 3 22 anbi12d 
 |-  ( ( x = y /\ t = s ) -> ( ( x e. D /\ ( t e. ( 0 [,) +oo ) /\ A. i e. ( 1 ... N ) ( x ` i ) = ( ( ( 1 - t ) x. ( Z ` i ) ) + ( t x. ( U ` i ) ) ) ) ) <-> ( y e. D /\ ( s e. ( 0 [,) +oo ) /\ A. j e. ( 1 ... N ) ( y ` j ) = ( ( ( 1 - s ) x. ( Z ` j ) ) + ( s x. ( U ` j ) ) ) ) ) ) )
24 23 cbvopabv 
 |-  { <. 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 ) ) ) ) ) } = { <. 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 ) ) ) ) ) }
25 1 24 eqtri 
 |-  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 ) ) ) ) ) }