Metamath Proof Explorer

Theorem prjspvs

Description: A nonzero multiple of a vector is equivalent to the vector. (Contributed by Steven Nguyen, 6-Jun-2023)

Ref Expression
Hypotheses prjsprel.1 ⊢ ∼ ˙ = x y | x ∈ B ∧ y ∈ B ∧ ∃ l ∈ K x = l · ˙ y
prjspertr.b ⊢ B = Base V ∖ 0 V
prjspertr.s ⊢ S = Scalar ⁡ V
prjspertr.x ⊢ · ˙ = ⋅ V
prjspertr.k ⊢ K = Base S
prjspreln0.z ⊢ 0 ˙ = 0 S
Assertion prjspvs ⊢ V ∈ LVec ∧ X ∈ B ∧ N ∈ K ∖ 0 ˙ → N · ˙ X ∼ ˙ X

Proof

Step Hyp Ref Expression
1 prjsprel.1 ⊢ ∼ ˙ = x y | x ∈ B ∧ y ∈ B ∧ ∃ l ∈ K x = l · ˙ y
2 prjspertr.b ⊢ B = Base V ∖ 0 V
3 prjspertr.s ⊢ S = Scalar ⁡ V
4 prjspertr.x ⊢ · ˙ = ⋅ V
5 prjspertr.k ⊢ K = Base S
6 prjspreln0.z ⊢ 0 ˙ = 0 S
7 eqid ⊢ Base V = Base V
8 lveclmod ⊢ V ∈ LVec → V ∈ LMod
9 8 3ad2ant1 ⊢ V ∈ LVec ∧ X ∈ B ∧ N ∈ K ∖ 0 ˙ → V ∈ LMod
10 eldifi ⊢ N ∈ K ∖ 0 ˙ → N ∈ K
11 10 3ad2ant3 ⊢ V ∈ LVec ∧ X ∈ B ∧ N ∈ K ∖ 0 ˙ → N ∈ K
12 difss ⊢ Base V ∖ 0 V ⊆ Base V
13 2 12 eqsstri ⊢ B ⊆ Base V
14 13 sseli ⊢ X ∈ B → X ∈ Base V
15 14 3ad2ant2 ⊢ V ∈ LVec ∧ X ∈ B ∧ N ∈ K ∖ 0 ˙ → X ∈ Base V
16 7 3 4 5 9 11 15 lmodvscld ⊢ V ∈ LVec ∧ X ∈ B ∧ N ∈ K ∖ 0 ˙ → N · ˙ X ∈ Base V
17 eldifsni ⊢ N ∈ K ∖ 0 ˙ → N ≠ 0 ˙
18 17 3ad2ant3 ⊢ V ∈ LVec ∧ X ∈ B ∧ N ∈ K ∖ 0 ˙ → N ≠ 0 ˙
19 eldifsni ⊢ X ∈ Base V ∖ 0 V → X ≠ 0 V
20 19 2 eleq2s ⊢ X ∈ B → X ≠ 0 V
21 20 3ad2ant2 ⊢ V ∈ LVec ∧ X ∈ B ∧ N ∈ K ∖ 0 ˙ → X ≠ 0 V
22 eqid ⊢ 0 V = 0 V
23 simp1 ⊢ V ∈ LVec ∧ X ∈ B ∧ N ∈ K ∖ 0 ˙ → V ∈ LVec
24 7 4 3 5 6 22 23 11 15 lvecvsn0 ⊢ V ∈ LVec ∧ X ∈ B ∧ N ∈ K ∖ 0 ˙ → N · ˙ X ≠ 0 V ↔ N ≠ 0 ˙ ∧ X ≠ 0 V
25 18 21 24 mpbir2and ⊢ V ∈ LVec ∧ X ∈ B ∧ N ∈ K ∖ 0 ˙ → N · ˙ X ≠ 0 V
26 nelsn ⊢ N · ˙ X ≠ 0 V → ¬ N · ˙ X ∈ 0 V
27 25 26 syl ⊢ V ∈ LVec ∧ X ∈ B ∧ N ∈ K ∖ 0 ˙ → ¬ N · ˙ X ∈ 0 V
28 16 27 eldifd ⊢ V ∈ LVec ∧ X ∈ B ∧ N ∈ K ∖ 0 ˙ → N · ˙ X ∈ Base V ∖ 0 V
29 28 2 eleqtrrdi ⊢ V ∈ LVec ∧ X ∈ B ∧ N ∈ K ∖ 0 ˙ → N · ˙ X ∈ B
30 simp2 ⊢ V ∈ LVec ∧ X ∈ B ∧ N ∈ K ∖ 0 ˙ → X ∈ B
31 oveq1 ⊢ N = m → N · ˙ X = m · ˙ X
32 31 eqcoms ⊢ m = N → N · ˙ X = m · ˙ X
33 tbtru ⊢ N · ˙ X = m · ˙ X ↔ N · ˙ X = m · ˙ X ↔ ⊤
34 32 33 sylib ⊢ m = N → N · ˙ X = m · ˙ X ↔ ⊤
35 34 adantl ⊢ V ∈ LVec ∧ X ∈ B ∧ N ∈ K ∖ 0 ˙ ∧ m = N → N · ˙ X = m · ˙ X ↔ ⊤
36 trud ⊢ V ∈ LVec ∧ X ∈ B ∧ N ∈ K ∖ 0 ˙ → ⊤
37 11 35 36 rspcedvd ⊢ V ∈ LVec ∧ X ∈ B ∧ N ∈ K ∖ 0 ˙ → ∃ m ∈ K N · ˙ X = m · ˙ X
38 1 prjsprel ⊢ N · ˙ X ∼ ˙ X ↔ N · ˙ X ∈ B ∧ X ∈ B ∧ ∃ m ∈ K N · ˙ X = m · ˙ X
39 29 30 37 38 syl21anbrc ⊢ V ∈ LVec ∧ X ∈ B ∧ N ∈ K ∖ 0 ˙ → N · ˙ X ∼ ˙ X