Metamath Proof Explorer

Theorem ax5seglem4

Description: Lemma for ax5seg . Given two distinct points, the scaling constant in a betweenness statement is nonzero. (Contributed by Scott Fenton, 11-Jun-2013)

Ref Expression
Assertion ax5seglem4 
|- ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) ) /\ A. i e. ( 1 ... N ) ( B ` i ) = ( ( ( 1 - T ) x. ( A ` i ) ) + ( T x. ( C ` i ) ) ) /\ A =/= B ) -> T =/= 0 )

Proof

Step Hyp Ref Expression
1 oveq2 
 |-  ( T = 0 -> ( 1 - T ) = ( 1 - 0 ) )
2 1m0e1 
 |-  ( 1 - 0 ) = 1
3 1 2 eqtrdi 
 |-  ( T = 0 -> ( 1 - T ) = 1 )
4 3 oveq1d 
 |-  ( T = 0 -> ( ( 1 - T ) x. ( A ` i ) ) = ( 1 x. ( A ` i ) ) )
5 oveq1 
 |-  ( T = 0 -> ( T x. ( C ` i ) ) = ( 0 x. ( C ` i ) ) )
6 4 5 oveq12d 
 |-  ( T = 0 -> ( ( ( 1 - T ) x. ( A ` i ) ) + ( T x. ( C ` i ) ) ) = ( ( 1 x. ( A ` i ) ) + ( 0 x. ( C ` i ) ) ) )
7 6 eqeq2d 
 |-  ( T = 0 -> ( ( B ` i ) = ( ( ( 1 - T ) x. ( A ` i ) ) + ( T x. ( C ` i ) ) ) <-> ( B ` i ) = ( ( 1 x. ( A ` i ) ) + ( 0 x. ( C ` i ) ) ) ) )
8 7 ralbidv 
 |-  ( T = 0 -> ( A. i e. ( 1 ... N ) ( B ` i ) = ( ( ( 1 - T ) x. ( A ` i ) ) + ( T x. ( C ` i ) ) ) <-> A. i e. ( 1 ... N ) ( B ` i ) = ( ( 1 x. ( A ` i ) ) + ( 0 x. ( C ` i ) ) ) ) )
9 8 biimpac 
 |-  ( ( A. i e. ( 1 ... N ) ( B ` i ) = ( ( ( 1 - T ) x. ( A ` i ) ) + ( T x. ( C ` i ) ) ) /\ T = 0 ) -> A. i e. ( 1 ... N ) ( B ` i ) = ( ( 1 x. ( A ` i ) ) + ( 0 x. ( C ` i ) ) ) )
10 eqeefv 
 |-  ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) -> ( A = B <-> A. i e. ( 1 ... N ) ( A ` i ) = ( B ` i ) ) )
11 10 3adant1 
 |-  ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) -> ( A = B <-> A. i e. ( 1 ... N ) ( A ` i ) = ( B ` i ) ) )
12 11 3adant3r3 
 |-  ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) ) -> ( A = B <-> A. i e. ( 1 ... N ) ( A ` i ) = ( B ` i ) ) )
13 simplr1 
 |-  ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) ) /\ i e. ( 1 ... N ) ) -> A e. ( EE ` N ) )
14 fveecn 
 |-  ( ( A e. ( EE ` N ) /\ i e. ( 1 ... N ) ) -> ( A ` i ) e. CC )
15 13 14 sylancom 
 |-  ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) ) /\ i e. ( 1 ... N ) ) -> ( A ` i ) e. CC )
16 simplr3 
 |-  ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) ) /\ i e. ( 1 ... N ) ) -> C e. ( EE ` N ) )
17 fveecn 
 |-  ( ( C e. ( EE ` N ) /\ i e. ( 1 ... N ) ) -> ( C ` i ) e. CC )
18 16 17 sylancom 
 |-  ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) ) /\ i e. ( 1 ... N ) ) -> ( C ` i ) e. CC )
19 mulid2 
 |-  ( ( A ` i ) e. CC -> ( 1 x. ( A ` i ) ) = ( A ` i ) )
20 mul02 
 |-  ( ( C ` i ) e. CC -> ( 0 x. ( C ` i ) ) = 0 )
21 19 20 oveqan12d 
 |-  ( ( ( A ` i ) e. CC /\ ( C ` i ) e. CC ) -> ( ( 1 x. ( A ` i ) ) + ( 0 x. ( C ` i ) ) ) = ( ( A ` i ) + 0 ) )
22 addid1 
 |-  ( ( A ` i ) e. CC -> ( ( A ` i ) + 0 ) = ( A ` i ) )
23 22 adantr 
 |-  ( ( ( A ` i ) e. CC /\ ( C ` i ) e. CC ) -> ( ( A ` i ) + 0 ) = ( A ` i ) )
24 21 23 eqtrd 
 |-  ( ( ( A ` i ) e. CC /\ ( C ` i ) e. CC ) -> ( ( 1 x. ( A ` i ) ) + ( 0 x. ( C ` i ) ) ) = ( A ` i ) )
25 15 18 24 syl2anc 
 |-  ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) ) /\ i e. ( 1 ... N ) ) -> ( ( 1 x. ( A ` i ) ) + ( 0 x. ( C ` i ) ) ) = ( A ` i ) )
26 25 eqeq1d 
 |-  ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) ) /\ i e. ( 1 ... N ) ) -> ( ( ( 1 x. ( A ` i ) ) + ( 0 x. ( C ` i ) ) ) = ( B ` i ) <-> ( A ` i ) = ( B ` i ) ) )
27 eqcom 
 |-  ( ( ( 1 x. ( A ` i ) ) + ( 0 x. ( C ` i ) ) ) = ( B ` i ) <-> ( B ` i ) = ( ( 1 x. ( A ` i ) ) + ( 0 x. ( C ` i ) ) ) )
28 26 27 bitr3di 
 |-  ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) ) /\ i e. ( 1 ... N ) ) -> ( ( A ` i ) = ( B ` i ) <-> ( B ` i ) = ( ( 1 x. ( A ` i ) ) + ( 0 x. ( C ` i ) ) ) ) )
29 28 ralbidva 
 |-  ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) ) -> ( A. i e. ( 1 ... N ) ( A ` i ) = ( B ` i ) <-> A. i e. ( 1 ... N ) ( B ` i ) = ( ( 1 x. ( A ` i ) ) + ( 0 x. ( C ` i ) ) ) ) )
30 12 29 bitrd 
 |-  ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) ) -> ( A = B <-> A. i e. ( 1 ... N ) ( B ` i ) = ( ( 1 x. ( A ` i ) ) + ( 0 x. ( C ` i ) ) ) ) )
31 9 30 syl5ibr 
 |-  ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) ) -> ( ( A. i e. ( 1 ... N ) ( B ` i ) = ( ( ( 1 - T ) x. ( A ` i ) ) + ( T x. ( C ` i ) ) ) /\ T = 0 ) -> A = B ) )
32 31 expdimp 
 |-  ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) ) /\ A. i e. ( 1 ... N ) ( B ` i ) = ( ( ( 1 - T ) x. ( A ` i ) ) + ( T x. ( C ` i ) ) ) ) -> ( T = 0 -> A = B ) )
33 32 necon3d 
 |-  ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) ) /\ A. i e. ( 1 ... N ) ( B ` i ) = ( ( ( 1 - T ) x. ( A ` i ) ) + ( T x. ( C ` i ) ) ) ) -> ( A =/= B -> T =/= 0 ) )
34 33 3impia 
 |-  ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) ) /\ A. i e. ( 1 ... N ) ( B ` i ) = ( ( ( 1 - T ) x. ( A ` i ) ) + ( T x. ( C ` i ) ) ) /\ A =/= B ) -> T =/= 0 )