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