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 ( ( ( ๐‘ โˆˆ โ„• โˆง ( ๐ด โˆˆ ( ๐”ผ โ€˜ ๐‘ ) โˆง ๐ต โˆˆ ( ๐”ผ โ€˜ ๐‘ ) โˆง ๐ถ โˆˆ ( ๐”ผ โ€˜ ๐‘ ) ) ) โˆง โˆ€ ๐‘– โˆˆ ( 1 ... ๐‘ ) ( ๐ต โ€˜ ๐‘– ) = ( ( ( 1 โˆ’ ๐‘‡ ) ยท ( ๐ด โ€˜ ๐‘– ) ) + ( ๐‘‡ ยท ( ๐ถ โ€˜ ๐‘– ) ) ) โˆง ๐ด โ‰  ๐ต ) โ†’ ๐‘‡ โ‰  0 )

Proof

Step Hyp Ref Expression
1 oveq2 โŠข ( ๐‘‡ = 0 โ†’ ( 1 โˆ’ ๐‘‡ ) = ( 1 โˆ’ 0 ) )
2 1m0e1 โŠข ( 1 โˆ’ 0 ) = 1
3 1 2 eqtrdi โŠข ( ๐‘‡ = 0 โ†’ ( 1 โˆ’ ๐‘‡ ) = 1 )
4 3 oveq1d โŠข ( ๐‘‡ = 0 โ†’ ( ( 1 โˆ’ ๐‘‡ ) ยท ( ๐ด โ€˜ ๐‘– ) ) = ( 1 ยท ( ๐ด โ€˜ ๐‘– ) ) )
5 oveq1 โŠข ( ๐‘‡ = 0 โ†’ ( ๐‘‡ ยท ( ๐ถ โ€˜ ๐‘– ) ) = ( 0 ยท ( ๐ถ โ€˜ ๐‘– ) ) )
6 4 5 oveq12d โŠข ( ๐‘‡ = 0 โ†’ ( ( ( 1 โˆ’ ๐‘‡ ) ยท ( ๐ด โ€˜ ๐‘– ) ) + ( ๐‘‡ ยท ( ๐ถ โ€˜ ๐‘– ) ) ) = ( ( 1 ยท ( ๐ด โ€˜ ๐‘– ) ) + ( 0 ยท ( ๐ถ โ€˜ ๐‘– ) ) ) )
7 6 eqeq2d โŠข ( ๐‘‡ = 0 โ†’ ( ( ๐ต โ€˜ ๐‘– ) = ( ( ( 1 โˆ’ ๐‘‡ ) ยท ( ๐ด โ€˜ ๐‘– ) ) + ( ๐‘‡ ยท ( ๐ถ โ€˜ ๐‘– ) ) ) โ†” ( ๐ต โ€˜ ๐‘– ) = ( ( 1 ยท ( ๐ด โ€˜ ๐‘– ) ) + ( 0 ยท ( ๐ถ โ€˜ ๐‘– ) ) ) ) )
8 7 ralbidv โŠข ( ๐‘‡ = 0 โ†’ ( โˆ€ ๐‘– โˆˆ ( 1 ... ๐‘ ) ( ๐ต โ€˜ ๐‘– ) = ( ( ( 1 โˆ’ ๐‘‡ ) ยท ( ๐ด โ€˜ ๐‘– ) ) + ( ๐‘‡ ยท ( ๐ถ โ€˜ ๐‘– ) ) ) โ†” โˆ€ ๐‘– โˆˆ ( 1 ... ๐‘ ) ( ๐ต โ€˜ ๐‘– ) = ( ( 1 ยท ( ๐ด โ€˜ ๐‘– ) ) + ( 0 ยท ( ๐ถ โ€˜ ๐‘– ) ) ) ) )
9 8 biimpac โŠข ( ( โˆ€ ๐‘– โˆˆ ( 1 ... ๐‘ ) ( ๐ต โ€˜ ๐‘– ) = ( ( ( 1 โˆ’ ๐‘‡ ) ยท ( ๐ด โ€˜ ๐‘– ) ) + ( ๐‘‡ ยท ( ๐ถ โ€˜ ๐‘– ) ) ) โˆง ๐‘‡ = 0 ) โ†’ โˆ€ ๐‘– โˆˆ ( 1 ... ๐‘ ) ( ๐ต โ€˜ ๐‘– ) = ( ( 1 ยท ( ๐ด โ€˜ ๐‘– ) ) + ( 0 ยท ( ๐ถ โ€˜ ๐‘– ) ) ) )
10 eqeefv โŠข ( ( ๐ด โˆˆ ( ๐”ผ โ€˜ ๐‘ ) โˆง ๐ต โˆˆ ( ๐”ผ โ€˜ ๐‘ ) ) โ†’ ( ๐ด = ๐ต โ†” โˆ€ ๐‘– โˆˆ ( 1 ... ๐‘ ) ( ๐ด โ€˜ ๐‘– ) = ( ๐ต โ€˜ ๐‘– ) ) )
11 10 3adant1 โŠข ( ( ๐‘ โˆˆ โ„• โˆง ๐ด โˆˆ ( ๐”ผ โ€˜ ๐‘ ) โˆง ๐ต โˆˆ ( ๐”ผ โ€˜ ๐‘ ) ) โ†’ ( ๐ด = ๐ต โ†” โˆ€ ๐‘– โˆˆ ( 1 ... ๐‘ ) ( ๐ด โ€˜ ๐‘– ) = ( ๐ต โ€˜ ๐‘– ) ) )
12 11 3adant3r3 โŠข ( ( ๐‘ โˆˆ โ„• โˆง ( ๐ด โˆˆ ( ๐”ผ โ€˜ ๐‘ ) โˆง ๐ต โˆˆ ( ๐”ผ โ€˜ ๐‘ ) โˆง ๐ถ โˆˆ ( ๐”ผ โ€˜ ๐‘ ) ) ) โ†’ ( ๐ด = ๐ต โ†” โˆ€ ๐‘– โˆˆ ( 1 ... ๐‘ ) ( ๐ด โ€˜ ๐‘– ) = ( ๐ต โ€˜ ๐‘– ) ) )
13 simplr1 โŠข ( ( ( ๐‘ โˆˆ โ„• โˆง ( ๐ด โˆˆ ( ๐”ผ โ€˜ ๐‘ ) โˆง ๐ต โˆˆ ( ๐”ผ โ€˜ ๐‘ ) โˆง ๐ถ โˆˆ ( ๐”ผ โ€˜ ๐‘ ) ) ) โˆง ๐‘– โˆˆ ( 1 ... ๐‘ ) ) โ†’ ๐ด โˆˆ ( ๐”ผ โ€˜ ๐‘ ) )
14 fveecn โŠข ( ( ๐ด โˆˆ ( ๐”ผ โ€˜ ๐‘ ) โˆง ๐‘– โˆˆ ( 1 ... ๐‘ ) ) โ†’ ( ๐ด โ€˜ ๐‘– ) โˆˆ โ„‚ )
15 13 14 sylancom โŠข ( ( ( ๐‘ โˆˆ โ„• โˆง ( ๐ด โˆˆ ( ๐”ผ โ€˜ ๐‘ ) โˆง ๐ต โˆˆ ( ๐”ผ โ€˜ ๐‘ ) โˆง ๐ถ โˆˆ ( ๐”ผ โ€˜ ๐‘ ) ) ) โˆง ๐‘– โˆˆ ( 1 ... ๐‘ ) ) โ†’ ( ๐ด โ€˜ ๐‘– ) โˆˆ โ„‚ )
16 simplr3 โŠข ( ( ( ๐‘ โˆˆ โ„• โˆง ( ๐ด โˆˆ ( ๐”ผ โ€˜ ๐‘ ) โˆง ๐ต โˆˆ ( ๐”ผ โ€˜ ๐‘ ) โˆง ๐ถ โˆˆ ( ๐”ผ โ€˜ ๐‘ ) ) ) โˆง ๐‘– โˆˆ ( 1 ... ๐‘ ) ) โ†’ ๐ถ โˆˆ ( ๐”ผ โ€˜ ๐‘ ) )
17 fveecn โŠข ( ( ๐ถ โˆˆ ( ๐”ผ โ€˜ ๐‘ ) โˆง ๐‘– โˆˆ ( 1 ... ๐‘ ) ) โ†’ ( ๐ถ โ€˜ ๐‘– ) โˆˆ โ„‚ )
18 16 17 sylancom โŠข ( ( ( ๐‘ โˆˆ โ„• โˆง ( ๐ด โˆˆ ( ๐”ผ โ€˜ ๐‘ ) โˆง ๐ต โˆˆ ( ๐”ผ โ€˜ ๐‘ ) โˆง ๐ถ โˆˆ ( ๐”ผ โ€˜ ๐‘ ) ) ) โˆง ๐‘– โˆˆ ( 1 ... ๐‘ ) ) โ†’ ( ๐ถ โ€˜ ๐‘– ) โˆˆ โ„‚ )
19 mullid โŠข ( ( ๐ด โ€˜ ๐‘– ) โˆˆ โ„‚ โ†’ ( 1 ยท ( ๐ด โ€˜ ๐‘– ) ) = ( ๐ด โ€˜ ๐‘– ) )
20 mul02 โŠข ( ( ๐ถ โ€˜ ๐‘– ) โˆˆ โ„‚ โ†’ ( 0 ยท ( ๐ถ โ€˜ ๐‘– ) ) = 0 )
21 19 20 oveqan12d โŠข ( ( ( ๐ด โ€˜ ๐‘– ) โˆˆ โ„‚ โˆง ( ๐ถ โ€˜ ๐‘– ) โˆˆ โ„‚ ) โ†’ ( ( 1 ยท ( ๐ด โ€˜ ๐‘– ) ) + ( 0 ยท ( ๐ถ โ€˜ ๐‘– ) ) ) = ( ( ๐ด โ€˜ ๐‘– ) + 0 ) )
22 addrid โŠข ( ( ๐ด โ€˜ ๐‘– ) โˆˆ โ„‚ โ†’ ( ( ๐ด โ€˜ ๐‘– ) + 0 ) = ( ๐ด โ€˜ ๐‘– ) )
23 22 adantr โŠข ( ( ( ๐ด โ€˜ ๐‘– ) โˆˆ โ„‚ โˆง ( ๐ถ โ€˜ ๐‘– ) โˆˆ โ„‚ ) โ†’ ( ( ๐ด โ€˜ ๐‘– ) + 0 ) = ( ๐ด โ€˜ ๐‘– ) )
24 21 23 eqtrd โŠข ( ( ( ๐ด โ€˜ ๐‘– ) โˆˆ โ„‚ โˆง ( ๐ถ โ€˜ ๐‘– ) โˆˆ โ„‚ ) โ†’ ( ( 1 ยท ( ๐ด โ€˜ ๐‘– ) ) + ( 0 ยท ( ๐ถ โ€˜ ๐‘– ) ) ) = ( ๐ด โ€˜ ๐‘– ) )
25 15 18 24 syl2anc โŠข ( ( ( ๐‘ โˆˆ โ„• โˆง ( ๐ด โˆˆ ( ๐”ผ โ€˜ ๐‘ ) โˆง ๐ต โˆˆ ( ๐”ผ โ€˜ ๐‘ ) โˆง ๐ถ โˆˆ ( ๐”ผ โ€˜ ๐‘ ) ) ) โˆง ๐‘– โˆˆ ( 1 ... ๐‘ ) ) โ†’ ( ( 1 ยท ( ๐ด โ€˜ ๐‘– ) ) + ( 0 ยท ( ๐ถ โ€˜ ๐‘– ) ) ) = ( ๐ด โ€˜ ๐‘– ) )
26 25 eqeq1d โŠข ( ( ( ๐‘ โˆˆ โ„• โˆง ( ๐ด โˆˆ ( ๐”ผ โ€˜ ๐‘ ) โˆง ๐ต โˆˆ ( ๐”ผ โ€˜ ๐‘ ) โˆง ๐ถ โˆˆ ( ๐”ผ โ€˜ ๐‘ ) ) ) โˆง ๐‘– โˆˆ ( 1 ... ๐‘ ) ) โ†’ ( ( ( 1 ยท ( ๐ด โ€˜ ๐‘– ) ) + ( 0 ยท ( ๐ถ โ€˜ ๐‘– ) ) ) = ( ๐ต โ€˜ ๐‘– ) โ†” ( ๐ด โ€˜ ๐‘– ) = ( ๐ต โ€˜ ๐‘– ) ) )
27 eqcom โŠข ( ( ( 1 ยท ( ๐ด โ€˜ ๐‘– ) ) + ( 0 ยท ( ๐ถ โ€˜ ๐‘– ) ) ) = ( ๐ต โ€˜ ๐‘– ) โ†” ( ๐ต โ€˜ ๐‘– ) = ( ( 1 ยท ( ๐ด โ€˜ ๐‘– ) ) + ( 0 ยท ( ๐ถ โ€˜ ๐‘– ) ) ) )
28 26 27 bitr3di โŠข ( ( ( ๐‘ โˆˆ โ„• โˆง ( ๐ด โˆˆ ( ๐”ผ โ€˜ ๐‘ ) โˆง ๐ต โˆˆ ( ๐”ผ โ€˜ ๐‘ ) โˆง ๐ถ โˆˆ ( ๐”ผ โ€˜ ๐‘ ) ) ) โˆง ๐‘– โˆˆ ( 1 ... ๐‘ ) ) โ†’ ( ( ๐ด โ€˜ ๐‘– ) = ( ๐ต โ€˜ ๐‘– ) โ†” ( ๐ต โ€˜ ๐‘– ) = ( ( 1 ยท ( ๐ด โ€˜ ๐‘– ) ) + ( 0 ยท ( ๐ถ โ€˜ ๐‘– ) ) ) ) )
29 28 ralbidva โŠข ( ( ๐‘ โˆˆ โ„• โˆง ( ๐ด โˆˆ ( ๐”ผ โ€˜ ๐‘ ) โˆง ๐ต โˆˆ ( ๐”ผ โ€˜ ๐‘ ) โˆง ๐ถ โˆˆ ( ๐”ผ โ€˜ ๐‘ ) ) ) โ†’ ( โˆ€ ๐‘– โˆˆ ( 1 ... ๐‘ ) ( ๐ด โ€˜ ๐‘– ) = ( ๐ต โ€˜ ๐‘– ) โ†” โˆ€ ๐‘– โˆˆ ( 1 ... ๐‘ ) ( ๐ต โ€˜ ๐‘– ) = ( ( 1 ยท ( ๐ด โ€˜ ๐‘– ) ) + ( 0 ยท ( ๐ถ โ€˜ ๐‘– ) ) ) ) )
30 12 29 bitrd โŠข ( ( ๐‘ โˆˆ โ„• โˆง ( ๐ด โˆˆ ( ๐”ผ โ€˜ ๐‘ ) โˆง ๐ต โˆˆ ( ๐”ผ โ€˜ ๐‘ ) โˆง ๐ถ โˆˆ ( ๐”ผ โ€˜ ๐‘ ) ) ) โ†’ ( ๐ด = ๐ต โ†” โˆ€ ๐‘– โˆˆ ( 1 ... ๐‘ ) ( ๐ต โ€˜ ๐‘– ) = ( ( 1 ยท ( ๐ด โ€˜ ๐‘– ) ) + ( 0 ยท ( ๐ถ โ€˜ ๐‘– ) ) ) ) )
31 9 30 imbitrrid โŠข ( ( ๐‘ โˆˆ โ„• โˆง ( ๐ด โˆˆ ( ๐”ผ โ€˜ ๐‘ ) โˆง ๐ต โˆˆ ( ๐”ผ โ€˜ ๐‘ ) โˆง ๐ถ โˆˆ ( ๐”ผ โ€˜ ๐‘ ) ) ) โ†’ ( ( โˆ€ ๐‘– โˆˆ ( 1 ... ๐‘ ) ( ๐ต โ€˜ ๐‘– ) = ( ( ( 1 โˆ’ ๐‘‡ ) ยท ( ๐ด โ€˜ ๐‘– ) ) + ( ๐‘‡ ยท ( ๐ถ โ€˜ ๐‘– ) ) ) โˆง ๐‘‡ = 0 ) โ†’ ๐ด = ๐ต ) )
32 31 expdimp โŠข ( ( ( ๐‘ โˆˆ โ„• โˆง ( ๐ด โˆˆ ( ๐”ผ โ€˜ ๐‘ ) โˆง ๐ต โˆˆ ( ๐”ผ โ€˜ ๐‘ ) โˆง ๐ถ โˆˆ ( ๐”ผ โ€˜ ๐‘ ) ) ) โˆง โˆ€ ๐‘– โˆˆ ( 1 ... ๐‘ ) ( ๐ต โ€˜ ๐‘– ) = ( ( ( 1 โˆ’ ๐‘‡ ) ยท ( ๐ด โ€˜ ๐‘– ) ) + ( ๐‘‡ ยท ( ๐ถ โ€˜ ๐‘– ) ) ) ) โ†’ ( ๐‘‡ = 0 โ†’ ๐ด = ๐ต ) )
33 32 necon3d โŠข ( ( ( ๐‘ โˆˆ โ„• โˆง ( ๐ด โˆˆ ( ๐”ผ โ€˜ ๐‘ ) โˆง ๐ต โˆˆ ( ๐”ผ โ€˜ ๐‘ ) โˆง ๐ถ โˆˆ ( ๐”ผ โ€˜ ๐‘ ) ) ) โˆง โˆ€ ๐‘– โˆˆ ( 1 ... ๐‘ ) ( ๐ต โ€˜ ๐‘– ) = ( ( ( 1 โˆ’ ๐‘‡ ) ยท ( ๐ด โ€˜ ๐‘– ) ) + ( ๐‘‡ ยท ( ๐ถ โ€˜ ๐‘– ) ) ) ) โ†’ ( ๐ด โ‰  ๐ต โ†’ ๐‘‡ โ‰  0 ) )
34 33 3impia โŠข ( ( ( ๐‘ โˆˆ โ„• โˆง ( ๐ด โˆˆ ( ๐”ผ โ€˜ ๐‘ ) โˆง ๐ต โˆˆ ( ๐”ผ โ€˜ ๐‘ ) โˆง ๐ถ โˆˆ ( ๐”ผ โ€˜ ๐‘ ) ) ) โˆง โˆ€ ๐‘– โˆˆ ( 1 ... ๐‘ ) ( ๐ต โ€˜ ๐‘– ) = ( ( ( 1 โˆ’ ๐‘‡ ) ยท ( ๐ด โ€˜ ๐‘– ) ) + ( ๐‘‡ ยท ( ๐ถ โ€˜ ๐‘– ) ) ) โˆง ๐ด โ‰  ๐ต ) โ†’ ๐‘‡ โ‰  0 )