Metamath Proof Explorer

Theorem axbtwnid

Description: Points are indivisible. That is, if A lies between B and B , then A = B . Axiom A6 of Schwabhauser p. 11. (Contributed by Scott Fenton, 3-Jun-2013)

Ref Expression
Assertion axbtwnid 
|- ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) -> ( A Btwn <. B , B >. -> A = B ) )

Proof

Step Hyp Ref Expression
1 simp2 
 |-  ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) -> A e. ( EE ` N ) )
2 simp3 
 |-  ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) -> B e. ( EE ` N ) )
3 brbtwn 
 |-  ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) /\ B e. ( EE ` N ) ) -> ( A Btwn <. B , B >. <-> E. t e. ( 0 [,] 1 ) A. i e. ( 1 ... N ) ( A ` i ) = ( ( ( 1 - t ) x. ( B ` i ) ) + ( t x. ( B ` i ) ) ) ) )
4 1 2 2 3 syl3anc 
 |-  ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) -> ( A Btwn <. B , B >. <-> E. t e. ( 0 [,] 1 ) A. i e. ( 1 ... N ) ( A ` i ) = ( ( ( 1 - t ) x. ( B ` i ) ) + ( t x. ( B ` i ) ) ) ) )
5 elicc01 
 |-  ( t e. ( 0 [,] 1 ) <-> ( t e. RR /\ 0 <_ t /\ t <_ 1 ) )
6 5 simp1bi 
 |-  ( t e. ( 0 [,] 1 ) -> t e. RR )
7 6 recnd 
 |-  ( t e. ( 0 [,] 1 ) -> t e. CC )
8 eqeefv 
 |-  ( ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) -> ( A = B <-> A. i e. ( 1 ... N ) ( A ` i ) = ( B ` i ) ) )
9 8 3adant1 
 |-  ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) -> ( A = B <-> A. i e. ( 1 ... N ) ( A ` i ) = ( B ` i ) ) )
10 9 adantr 
 |-  ( ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ t e. CC ) -> ( A = B <-> A. i e. ( 1 ... N ) ( A ` i ) = ( B ` i ) ) )
11 ax-1cn 
 |-  1 e. CC
12 npcan 
 |-  ( ( 1 e. CC /\ t e. CC ) -> ( ( 1 - t ) + t ) = 1 )
13 11 12 mpan 
 |-  ( t e. CC -> ( ( 1 - t ) + t ) = 1 )
14 13 ad2antlr 
 |-  ( ( ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ t e. CC ) /\ i e. ( 1 ... N ) ) -> ( ( 1 - t ) + t ) = 1 )
15 14 oveq1d 
 |-  ( ( ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ t e. CC ) /\ i e. ( 1 ... N ) ) -> ( ( ( 1 - t ) + t ) x. ( B ` i ) ) = ( 1 x. ( B ` i ) ) )
16 subcl 
 |-  ( ( 1 e. CC /\ t e. CC ) -> ( 1 - t ) e. CC )
17 11 16 mpan 
 |-  ( t e. CC -> ( 1 - t ) e. CC )
18 17 ad2antlr 
 |-  ( ( ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ t e. CC ) /\ i e. ( 1 ... N ) ) -> ( 1 - t ) e. CC )
19 simplr 
 |-  ( ( ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ t e. CC ) /\ i e. ( 1 ... N ) ) -> t e. CC )
20 simpll3 
 |-  ( ( ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ t e. CC ) /\ i e. ( 1 ... N ) ) -> B e. ( EE ` N ) )
21 fveecn 
 |-  ( ( B e. ( EE ` N ) /\ i e. ( 1 ... N ) ) -> ( B ` i ) e. CC )
22 20 21 sylancom 
 |-  ( ( ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ t e. CC ) /\ i e. ( 1 ... N ) ) -> ( B ` i ) e. CC )
23 18 19 22 adddird 
 |-  ( ( ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ t e. CC ) /\ i e. ( 1 ... N ) ) -> ( ( ( 1 - t ) + t ) x. ( B ` i ) ) = ( ( ( 1 - t ) x. ( B ` i ) ) + ( t x. ( B ` i ) ) ) )
24 22 mulid2d 
 |-  ( ( ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ t e. CC ) /\ i e. ( 1 ... N ) ) -> ( 1 x. ( B ` i ) ) = ( B ` i ) )
25 15 23 24 3eqtr3rd 
 |-  ( ( ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ t e. CC ) /\ i e. ( 1 ... N ) ) -> ( B ` i ) = ( ( ( 1 - t ) x. ( B ` i ) ) + ( t x. ( B ` i ) ) ) )
26 25 eqeq2d 
 |-  ( ( ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ t e. CC ) /\ i e. ( 1 ... N ) ) -> ( ( A ` i ) = ( B ` i ) <-> ( A ` i ) = ( ( ( 1 - t ) x. ( B ` i ) ) + ( t x. ( B ` i ) ) ) ) )
27 26 ralbidva 
 |-  ( ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ t e. CC ) -> ( A. i e. ( 1 ... N ) ( A ` i ) = ( B ` i ) <-> A. i e. ( 1 ... N ) ( A ` i ) = ( ( ( 1 - t ) x. ( B ` i ) ) + ( t x. ( B ` i ) ) ) ) )
28 10 27 bitrd 
 |-  ( ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ t e. CC ) -> ( A = B <-> A. i e. ( 1 ... N ) ( A ` i ) = ( ( ( 1 - t ) x. ( B ` i ) ) + ( t x. ( B ` i ) ) ) ) )
29 28 biimprd 
 |-  ( ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ t e. CC ) -> ( A. i e. ( 1 ... N ) ( A ` i ) = ( ( ( 1 - t ) x. ( B ` i ) ) + ( t x. ( B ` i ) ) ) -> A = B ) )
30 7 29 sylan2 
 |-  ( ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ t e. ( 0 [,] 1 ) ) -> ( A. i e. ( 1 ... N ) ( A ` i ) = ( ( ( 1 - t ) x. ( B ` i ) ) + ( t x. ( B ` i ) ) ) -> A = B ) )
31 30 rexlimdva 
 |-  ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) -> ( E. t e. ( 0 [,] 1 ) A. i e. ( 1 ... N ) ( A ` i ) = ( ( ( 1 - t ) x. ( B ` i ) ) + ( t x. ( B ` i ) ) ) -> A = B ) )
32 4 31 sylbid 
 |-  ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) -> ( A Btwn <. B , B >. -> A = B ) )