Metamath Proof Explorer

Theorem ax5seglem5

Description: Lemma for ax5seg . If B is between A and C , and A is distinct from B , then A is distinct from C . (Contributed by Scott Fenton, 11-Jun-2013)

Ref Expression
Assertion ax5seglem5 
|- ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) ) /\ ( A =/= B /\ T e. ( 0 [,] 1 ) /\ A. i e. ( 1 ... N ) ( B ` i ) = ( ( ( 1 - T ) x. ( A ` i ) ) + ( T x. ( C ` i ) ) ) ) ) -> sum_ j e. ( 1 ... N ) ( ( ( A ` j ) - ( C ` j ) ) ^ 2 ) =/= 0 )

Proof

Step Hyp Ref Expression
1 fveq1 
 |-  ( A = C -> ( A ` i ) = ( C ` i ) )
2 1 oveq2d 
 |-  ( A = C -> ( T x. ( A ` i ) ) = ( T x. ( C ` i ) ) )
3 2 oveq2d 
 |-  ( A = C -> ( ( ( 1 - T ) x. ( A ` i ) ) + ( T x. ( A ` i ) ) ) = ( ( ( 1 - T ) x. ( A ` i ) ) + ( T x. ( C ` i ) ) ) )
4 3 eqeq2d 
 |-  ( A = C -> ( ( B ` i ) = ( ( ( 1 - T ) x. ( A ` i ) ) + ( T x. ( A ` i ) ) ) <-> ( B ` i ) = ( ( ( 1 - T ) x. ( A ` i ) ) + ( T x. ( C ` i ) ) ) ) )
5 4 ralbidv 
 |-  ( A = C -> ( A. i e. ( 1 ... N ) ( B ` i ) = ( ( ( 1 - T ) x. ( A ` i ) ) + ( T x. ( A ` i ) ) ) <-> A. i e. ( 1 ... N ) ( B ` i ) = ( ( ( 1 - T ) x. ( A ` i ) ) + ( T x. ( C ` i ) ) ) ) )
6 5 biimparc 
 |-  ( ( A. i e. ( 1 ... N ) ( B ` i ) = ( ( ( 1 - T ) x. ( A ` i ) ) + ( T x. ( C ` i ) ) ) /\ A = C ) -> A. i e. ( 1 ... N ) ( B ` i ) = ( ( ( 1 - T ) x. ( A ` i ) ) + ( T x. ( A ` i ) ) ) )
7 simplr1 
 |-  ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) ) /\ T e. ( 0 [,] 1 ) ) -> A e. ( EE ` N ) )
8 simplr2 
 |-  ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) ) /\ T e. ( 0 [,] 1 ) ) -> B e. ( EE ` N ) )
9 eqeefv 
 |-  ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) -> ( A = B <-> A. i e. ( 1 ... N ) ( A ` i ) = ( B ` i ) ) )
10 7 8 9 syl2anc 
 |-  ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) ) /\ T e. ( 0 [,] 1 ) ) -> ( A = B <-> A. i e. ( 1 ... N ) ( A ` i ) = ( B ` i ) ) )
11 fveecn 
 |-  ( ( A e. ( EE ` N ) /\ i e. ( 1 ... N ) ) -> ( A ` i ) e. CC )
12 7 11 sylan 
 |-  ( ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) ) /\ T e. ( 0 [,] 1 ) ) /\ i e. ( 1 ... N ) ) -> ( A ` i ) e. CC )
13 elicc01 
 |-  ( T e. ( 0 [,] 1 ) <-> ( T e. RR /\ 0 <_ T /\ T <_ 1 ) )
14 13 simp1bi 
 |-  ( T e. ( 0 [,] 1 ) -> T e. RR )
15 14 recnd 
 |-  ( T e. ( 0 [,] 1 ) -> T e. CC )
16 15 ad2antlr 
 |-  ( ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) ) /\ T e. ( 0 [,] 1 ) ) /\ i e. ( 1 ... N ) ) -> T e. CC )
17 ax-1cn 
 |-  1 e. CC
18 npcan 
 |-  ( ( 1 e. CC /\ T e. CC ) -> ( ( 1 - T ) + T ) = 1 )
19 17 18 mpan 
 |-  ( T e. CC -> ( ( 1 - T ) + T ) = 1 )
20 19 oveq1d 
 |-  ( T e. CC -> ( ( ( 1 - T ) + T ) x. ( A ` i ) ) = ( 1 x. ( A ` i ) ) )
21 mulid2 
 |-  ( ( A ` i ) e. CC -> ( 1 x. ( A ` i ) ) = ( A ` i ) )
22 20 21 sylan9eqr 
 |-  ( ( ( A ` i ) e. CC /\ T e. CC ) -> ( ( ( 1 - T ) + T ) x. ( A ` i ) ) = ( A ` i ) )
23 subcl 
 |-  ( ( 1 e. CC /\ T e. CC ) -> ( 1 - T ) e. CC )
24 17 23 mpan 
 |-  ( T e. CC -> ( 1 - T ) e. CC )
25 24 adantl 
 |-  ( ( ( A ` i ) e. CC /\ T e. CC ) -> ( 1 - T ) e. CC )
26 simpr 
 |-  ( ( ( A ` i ) e. CC /\ T e. CC ) -> T e. CC )
27 simpl 
 |-  ( ( ( A ` i ) e. CC /\ T e. CC ) -> ( A ` i ) e. CC )
28 25 26 27 adddird 
 |-  ( ( ( A ` i ) e. CC /\ T e. CC ) -> ( ( ( 1 - T ) + T ) x. ( A ` i ) ) = ( ( ( 1 - T ) x. ( A ` i ) ) + ( T x. ( A ` i ) ) ) )
29 22 28 eqtr3d 
 |-  ( ( ( A ` i ) e. CC /\ T e. CC ) -> ( A ` i ) = ( ( ( 1 - T ) x. ( A ` i ) ) + ( T x. ( A ` i ) ) ) )
30 29 eqeq1d 
 |-  ( ( ( A ` i ) e. CC /\ T e. CC ) -> ( ( A ` i ) = ( B ` i ) <-> ( ( ( 1 - T ) x. ( A ` i ) ) + ( T x. ( A ` i ) ) ) = ( B ` i ) ) )
31 12 16 30 syl2anc 
 |-  ( ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) ) /\ T e. ( 0 [,] 1 ) ) /\ i e. ( 1 ... N ) ) -> ( ( A ` i ) = ( B ` i ) <-> ( ( ( 1 - T ) x. ( A ` i ) ) + ( T x. ( A ` i ) ) ) = ( B ` i ) ) )
32 eqcom 
 |-  ( ( ( ( 1 - T ) x. ( A ` i ) ) + ( T x. ( A ` i ) ) ) = ( B ` i ) <-> ( B ` i ) = ( ( ( 1 - T ) x. ( A ` i ) ) + ( T x. ( A ` i ) ) ) )
33 31 32 bitrdi 
 |-  ( ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) ) /\ T e. ( 0 [,] 1 ) ) /\ i e. ( 1 ... N ) ) -> ( ( A ` i ) = ( B ` i ) <-> ( B ` i ) = ( ( ( 1 - T ) x. ( A ` i ) ) + ( T x. ( A ` i ) ) ) ) )
34 33 ralbidva 
 |-  ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) ) /\ T e. ( 0 [,] 1 ) ) -> ( A. i e. ( 1 ... N ) ( A ` i ) = ( B ` i ) <-> A. i e. ( 1 ... N ) ( B ` i ) = ( ( ( 1 - T ) x. ( A ` i ) ) + ( T x. ( A ` i ) ) ) ) )
35 10 34 bitrd 
 |-  ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) ) /\ T e. ( 0 [,] 1 ) ) -> ( A = B <-> A. i e. ( 1 ... N ) ( B ` i ) = ( ( ( 1 - T ) x. ( A ` i ) ) + ( T x. ( A ` i ) ) ) ) )
36 6 35 syl5ibr 
 |-  ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) ) /\ T e. ( 0 [,] 1 ) ) -> ( ( A. i e. ( 1 ... N ) ( B ` i ) = ( ( ( 1 - T ) x. ( A ` i ) ) + ( T x. ( C ` i ) ) ) /\ A = C ) -> A = B ) )
37 36 expd 
 |-  ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) ) /\ T e. ( 0 [,] 1 ) ) -> ( A. i e. ( 1 ... N ) ( B ` i ) = ( ( ( 1 - T ) x. ( A ` i ) ) + ( T x. ( C ` i ) ) ) -> ( A = C -> A = B ) ) )
38 37 impr 
 |-  ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) ) /\ ( T e. ( 0 [,] 1 ) /\ A. i e. ( 1 ... N ) ( B ` i ) = ( ( ( 1 - T ) x. ( A ` i ) ) + ( T x. ( C ` i ) ) ) ) ) -> ( A = C -> A = B ) )
39 38 necon3d 
 |-  ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) ) /\ ( T e. ( 0 [,] 1 ) /\ A. i e. ( 1 ... N ) ( B ` i ) = ( ( ( 1 - T ) x. ( A ` i ) ) + ( T x. ( C ` i ) ) ) ) ) -> ( A =/= B -> A =/= C ) )
40 39 ex 
 |-  ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) ) -> ( ( T e. ( 0 [,] 1 ) /\ A. i e. ( 1 ... N ) ( B ` i ) = ( ( ( 1 - T ) x. ( A ` i ) ) + ( T x. ( C ` i ) ) ) ) -> ( A =/= B -> A =/= C ) ) )
41 40 com23 
 |-  ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) ) -> ( A =/= B -> ( ( T e. ( 0 [,] 1 ) /\ A. i e. ( 1 ... N ) ( B ` i ) = ( ( ( 1 - T ) x. ( A ` i ) ) + ( T x. ( C ` i ) ) ) ) -> A =/= C ) ) )
42 41 exp4a 
 |-  ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) ) -> ( A =/= B -> ( T e. ( 0 [,] 1 ) -> ( A. i e. ( 1 ... N ) ( B ` i ) = ( ( ( 1 - T ) x. ( A ` i ) ) + ( T x. ( C ` i ) ) ) -> A =/= C ) ) ) )
43 42 3imp2 
 |-  ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) ) /\ ( A =/= B /\ T e. ( 0 [,] 1 ) /\ A. i e. ( 1 ... N ) ( B ` i ) = ( ( ( 1 - T ) x. ( A ` i ) ) + ( T x. ( C ` i ) ) ) ) ) -> A =/= C )
44 simplr1 
 |-  ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) ) /\ ( A =/= B /\ T e. ( 0 [,] 1 ) /\ A. i e. ( 1 ... N ) ( B ` i ) = ( ( ( 1 - T ) x. ( A ` i ) ) + ( T x. ( C ` i ) ) ) ) ) -> A e. ( EE ` N ) )
45 simplr3 
 |-  ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) ) /\ ( A =/= B /\ T e. ( 0 [,] 1 ) /\ A. i e. ( 1 ... N ) ( B ` i ) = ( ( ( 1 - T ) x. ( A ` i ) ) + ( T x. ( C ` i ) ) ) ) ) -> C e. ( EE ` N ) )
46 eqeelen 
 |-  ( ( A e. ( EE ` N ) /\ C e. ( EE ` N ) ) -> ( A = C <-> sum_ j e. ( 1 ... N ) ( ( ( A ` j ) - ( C ` j ) ) ^ 2 ) = 0 ) )
47 44 45 46 syl2anc 
 |-  ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) ) /\ ( A =/= B /\ T e. ( 0 [,] 1 ) /\ A. i e. ( 1 ... N ) ( B ` i ) = ( ( ( 1 - T ) x. ( A ` i ) ) + ( T x. ( C ` i ) ) ) ) ) -> ( A = C <-> sum_ j e. ( 1 ... N ) ( ( ( A ` j ) - ( C ` j ) ) ^ 2 ) = 0 ) )
48 47 necon3bid 
 |-  ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) ) /\ ( A =/= B /\ T e. ( 0 [,] 1 ) /\ A. i e. ( 1 ... N ) ( B ` i ) = ( ( ( 1 - T ) x. ( A ` i ) ) + ( T x. ( C ` i ) ) ) ) ) -> ( A =/= C <-> sum_ j e. ( 1 ... N ) ( ( ( A ` j ) - ( C ` j ) ) ^ 2 ) =/= 0 ) )
49 43 48 mpbid 
 |-  ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ C e. ( EE ` N ) ) ) /\ ( A =/= B /\ T e. ( 0 [,] 1 ) /\ A. i e. ( 1 ... N ) ( B ` i ) = ( ( ( 1 - T ) x. ( A ` i ) ) + ( T x. ( C ` i ) ) ) ) ) -> sum_ j e. ( 1 ... N ) ( ( ( A ` j ) - ( C ` j ) ) ^ 2 ) =/= 0 )