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 lveclmod ⊢ V ∈ LVec → V ∈ LMod
8 7 3ad2ant1 ⊢ V ∈ LVec ∧ X ∈ B ∧ N ∈ K ∖ 0 ˙ → V ∈ LMod
9 eldifi ⊢ N ∈ K ∖ 0 ˙ → N ∈ K
10 9 3ad2ant3 ⊢ V ∈ LVec ∧ X ∈ B ∧ N ∈ K ∖ 0 ˙ → N ∈ K
11 difss ⊢ Base V ∖ 0 V ⊆ Base V
12 2 11 eqsstri ⊢ B ⊆ Base V
13 12 sseli ⊢ X ∈ B → X ∈ Base V
14 13 3ad2ant2 ⊢ V ∈ LVec ∧ X ∈ B ∧ N ∈ K ∖ 0 ˙ → X ∈ Base V
15 eqid ⊢ Base V = Base V
16 15 3 4 5 lmodvscl ⊢ V ∈ LMod ∧ N ∈ K ∧ X ∈ Base V → N · ˙ X ∈ Base V
17 8 10 14 16 syl3anc ⊢ V ∈ LVec ∧ X ∈ B ∧ N ∈ K ∖ 0 ˙ → N · ˙ X ∈ Base V
18 eldifsni ⊢ N ∈ K ∖ 0 ˙ → N ≠ 0 ˙
19 18 3ad2ant3 ⊢ V ∈ LVec ∧ X ∈ B ∧ N ∈ K ∖ 0 ˙ → N ≠ 0 ˙
20 eldifsni ⊢ X ∈ Base V ∖ 0 V → X ≠ 0 V
21 20 2 eleq2s ⊢ X ∈ B → X ≠ 0 V
22 21 3ad2ant2 ⊢ V ∈ LVec ∧ X ∈ B ∧ N ∈ K ∖ 0 ˙ → X ≠ 0 V
23 eqid ⊢ 0 V = 0 V
24 simp1 ⊢ V ∈ LVec ∧ X ∈ B ∧ N ∈ K ∖ 0 ˙ → V ∈ LVec
25 15 4 3 5 6 23 24 10 14 lvecvsn0 ⊢ V ∈ LVec ∧ X ∈ B ∧ N ∈ K ∖ 0 ˙ → N · ˙ X ≠ 0 V ↔ N ≠ 0 ˙ ∧ X ≠ 0 V
26 19 22 25 mpbir2and ⊢ V ∈ LVec ∧ X ∈ B ∧ N ∈ K ∖ 0 ˙ → N · ˙ X ≠ 0 V
27 nelsn ⊢ N · ˙ X ≠ 0 V → ¬ N · ˙ X ∈ 0 V
28 26 27 syl ⊢ V ∈ LVec ∧ X ∈ B ∧ N ∈ K ∖ 0 ˙ → ¬ N · ˙ X ∈ 0 V
29 17 28 eldifd ⊢ V ∈ LVec ∧ X ∈ B ∧ N ∈ K ∖ 0 ˙ → N · ˙ X ∈ Base V ∖ 0 V
30 29 2 eleqtrrdi ⊢ V ∈ LVec ∧ X ∈ B ∧ N ∈ K ∖ 0 ˙ → N · ˙ X ∈ B
31 simp2 ⊢ V ∈ LVec ∧ X ∈ B ∧ N ∈ K ∖ 0 ˙ → X ∈ B
32 oveq1 ⊢ N = m → N · ˙ X = m · ˙ X
33 32 eqcoms ⊢ m = N → N · ˙ X = m · ˙ X
34 tbtru ⊢ N · ˙ X = m · ˙ X ↔ N · ˙ X = m · ˙ X ↔ ⊤
35 33 34 sylib ⊢ m = N → N · ˙ X = m · ˙ X ↔ ⊤
36 35 adantl ⊢ V ∈ LVec ∧ X ∈ B ∧ N ∈ K ∖ 0 ˙ ∧ m = N → N · ˙ X = m · ˙ X ↔ ⊤
37 trud ⊢ V ∈ LVec ∧ X ∈ B ∧ N ∈ K ∖ 0 ˙ → ⊤
38 10 36 37 rspcedvd ⊢ V ∈ LVec ∧ X ∈ B ∧ N ∈ K ∖ 0 ˙ → ∃ m ∈ K N · ˙ X = m · ˙ X
39 1 prjsprel ⊢ N · ˙ X ∼ ˙ X ↔ N · ˙ X ∈ B ∧ X ∈ B ∧ ∃ m ∈ K N · ˙ X = m · ˙ X
40 30 31 38 39 syl21anbrc ⊢ V ∈ LVec ∧ X ∈ B ∧ N ∈ K ∖ 0 ˙ → N · ˙ X ∼ ˙ X