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 ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ ∀ i ∈ 1 … N B ⁡ i = 1 − T ⁢ A ⁡ i + T ⁢ 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 ⁢ A ⁡ i = 1 ⁢ A ⁡ i
5 oveq1 ⊢ T = 0 → T ⁢ C ⁡ i = 0 ⋅ C ⁡ i
6 4 5 oveq12d ⊢ T = 0 → 1 − T ⁢ A ⁡ i + T ⁢ C ⁡ i = 1 ⁢ A ⁡ i + 0 ⋅ C ⁡ i
7 6 eqeq2d ⊢ T = 0 → B ⁡ i = 1 − T ⁢ A ⁡ i + T ⁢ C ⁡ i ↔ B ⁡ i = 1 ⁢ A ⁡ i + 0 ⋅ C ⁡ i
8 7 ralbidv ⊢ T = 0 → ∀ i ∈ 1 … N B ⁡ i = 1 − T ⁢ A ⁡ i + T ⁢ C ⁡ i ↔ ∀ i ∈ 1 … N B ⁡ i = 1 ⁢ A ⁡ i + 0 ⋅ C ⁡ i
9 8 biimpac ⊢ ∀ i ∈ 1 … N B ⁡ i = 1 − T ⁢ A ⁡ i + T ⁢ C ⁡ i ∧ T = 0 → ∀ i ∈ 1 … N B ⁡ i = 1 ⁢ A ⁡ i + 0 ⋅ C ⁡ i
10 eqeefv ⊢ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N → A = B ↔ ∀ i ∈ 1 … N A ⁡ i = B ⁡ i
11 10 3adant1 ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N → A = B ↔ ∀ i ∈ 1 … N A ⁡ i = B ⁡ i
12 11 3adant3r3 ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N → A = B ↔ ∀ i ∈ 1 … N A ⁡ i = B ⁡ i
13 simplr1 ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ i ∈ 1 … N → A ∈ 𝔼 ⁡ N
14 fveecn ⊢ A ∈ 𝔼 ⁡ N ∧ i ∈ 1 … N → A ⁡ i ∈ ℂ
15 13 14 sylancom ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ i ∈ 1 … N → A ⁡ i ∈ ℂ
16 simplr3 ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ i ∈ 1 … N → C ∈ 𝔼 ⁡ N
17 fveecn ⊢ C ∈ 𝔼 ⁡ N ∧ i ∈ 1 … N → C ⁡ i ∈ ℂ
18 16 17 sylancom ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ i ∈ 1 … N → C ⁡ i ∈ ℂ
19 mulid2 ⊢ A ⁡ i ∈ ℂ → 1 ⁢ A ⁡ i = A ⁡ i
20 mul02 ⊢ C ⁡ i ∈ ℂ → 0 ⋅ C ⁡ i = 0
21 19 20 oveqan12d ⊢ A ⁡ i ∈ ℂ ∧ C ⁡ i ∈ ℂ → 1 ⁢ A ⁡ i + 0 ⋅ C ⁡ i = A ⁡ i + 0
22 addid1 ⊢ A ⁡ i ∈ ℂ → A ⁡ i + 0 = A ⁡ i
23 22 adantr ⊢ A ⁡ i ∈ ℂ ∧ C ⁡ i ∈ ℂ → A ⁡ i + 0 = A ⁡ i
24 21 23 eqtrd ⊢ A ⁡ i ∈ ℂ ∧ C ⁡ i ∈ ℂ → 1 ⁢ A ⁡ i + 0 ⋅ C ⁡ i = A ⁡ i
25 15 18 24 syl2anc ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ i ∈ 1 … N → 1 ⁢ A ⁡ i + 0 ⋅ C ⁡ i = A ⁡ i
26 25 eqeq1d ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ i ∈ 1 … N → 1 ⁢ A ⁡ i + 0 ⋅ C ⁡ i = B ⁡ i ↔ A ⁡ i = B ⁡ i
27 eqcom ⊢ 1 ⁢ A ⁡ i + 0 ⋅ C ⁡ i = B ⁡ i ↔ B ⁡ i = 1 ⁢ A ⁡ i + 0 ⋅ C ⁡ i
28 26 27 bitr3di ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ i ∈ 1 … N → A ⁡ i = B ⁡ i ↔ B ⁡ i = 1 ⁢ A ⁡ i + 0 ⋅ C ⁡ i
29 28 ralbidva ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N → ∀ i ∈ 1 … N A ⁡ i = B ⁡ i ↔ ∀ i ∈ 1 … N B ⁡ i = 1 ⁢ A ⁡ i + 0 ⋅ C ⁡ i
30 12 29 bitrd ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N → A = B ↔ ∀ i ∈ 1 … N B ⁡ i = 1 ⁢ A ⁡ i + 0 ⋅ C ⁡ i
31 9 30 syl5ibr ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N → ∀ i ∈ 1 … N B ⁡ i = 1 − T ⁢ A ⁡ i + T ⁢ C ⁡ i ∧ T = 0 → A = B
32 31 expdimp ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ ∀ i ∈ 1 … N B ⁡ i = 1 − T ⁢ A ⁡ i + T ⁢ C ⁡ i → T = 0 → A = B
33 32 necon3d ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ ∀ i ∈ 1 … N B ⁡ i = 1 − T ⁢ A ⁡ i + T ⁢ C ⁡ i → A ≠ B → T ≠ 0
34 33 3impia ⊢ N ∈ ℕ ∧ A ∈ 𝔼 ⁡ N ∧ B ∈ 𝔼 ⁡ N ∧ C ∈ 𝔼 ⁡ N ∧ ∀ i ∈ 1 … N B ⁡ i = 1 − T ⁢ A ⁡ i + T ⁢ C ⁡ i ∧ A ≠ B → T ≠ 0