Metamath Proof Explorer


Theorem prjspnvs

Description: A nonzero multiple of a vector is equivalent to the vector. This converts the equivalence relation used in prjspvs (see prjspnerlem ). (Contributed by SN, 8-Aug-2024)

Ref Expression
Hypotheses prjspnvs.e ˙ = x y | x B y B l S x = l · ˙ y
prjspnvs.w W = K freeLMod 0 N
prjspnvs.b B = Base W 0 W
prjspnvs.s S = Base K
prjspnvs.x · ˙ = W
prjspnvs.0 0 ˙ = 0 K
prjspnvs.k φ K DivRing
prjspnvs.1 φ X B
prjspnvs.2 φ C S
prjspnvs.3 φ C 0 ˙
Assertion prjspnvs φ C · ˙ X ˙ X

Proof

Step Hyp Ref Expression
1 prjspnvs.e ˙ = x y | x B y B l S x = l · ˙ y
2 prjspnvs.w W = K freeLMod 0 N
3 prjspnvs.b B = Base W 0 W
4 prjspnvs.s S = Base K
5 prjspnvs.x · ˙ = W
6 prjspnvs.0 0 ˙ = 0 K
7 prjspnvs.k φ K DivRing
8 prjspnvs.1 φ X B
9 prjspnvs.2 φ C S
10 prjspnvs.3 φ C 0 ˙
11 ovexd φ 0 N V
12 2 frlmlvec K DivRing 0 N V W LVec
13 7 11 12 syl2anc φ W LVec
14 nelsn C 0 ˙ ¬ C 0 ˙
15 10 14 syl φ ¬ C 0 ˙
16 9 15 eldifd φ C S 0 ˙
17 2 frlmsca K DivRing 0 N V K = Scalar W
18 7 11 17 syl2anc φ K = Scalar W
19 18 fveq2d φ Base K = Base Scalar W
20 4 19 syl5eq φ S = Base Scalar W
21 18 fveq2d φ 0 K = 0 Scalar W
22 6 21 syl5eq φ 0 ˙ = 0 Scalar W
23 22 sneqd φ 0 ˙ = 0 Scalar W
24 20 23 difeq12d φ S 0 ˙ = Base Scalar W 0 Scalar W
25 16 24 eleqtrd φ C Base Scalar W 0 Scalar W
26 eqid x y | x B y B l Base Scalar W x = l · ˙ y = x y | x B y B l Base Scalar W x = l · ˙ y
27 eqid Scalar W = Scalar W
28 eqid Base Scalar W = Base Scalar W
29 eqid 0 Scalar W = 0 Scalar W
30 26 3 27 5 28 29 prjspvs W LVec X B C Base Scalar W 0 Scalar W C · ˙ X x y | x B y B l Base Scalar W x = l · ˙ y X
31 13 8 25 30 syl3anc φ C · ˙ X x y | x B y B l Base Scalar W x = l · ˙ y X
32 1 2 3 4 5 prjspnerlem K DivRing ˙ = x y | x B y B l Base Scalar W x = l · ˙ y
33 7 32 syl φ ˙ = x y | x B y B l Base Scalar W x = l · ˙ y
34 33 breqd φ C · ˙ X ˙ X C · ˙ X x y | x B y B l Base Scalar W x = l · ˙ y X
35 31 34 mpbird φ C · ˙ X ˙ X