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 e. B /\ y e. B ) /\ E. l e. K x = ( l .x. y ) ) }
prjspertr.b
|- B = ( ( Base ` V ) \ { ( 0g ` V ) } )
prjspertr.s
|- S = ( Scalar ` V )
prjspertr.x
|- .x. = ( .s ` V )
prjspertr.k
|- K = ( Base ` S )
prjspreln0.z
|- .0. = ( 0g ` S )
Assertion prjspvs
|- ( ( V e. LVec /\ X e. B /\ N e. ( K \ { .0. } ) ) -> ( N .x. X ) .~ X )

Proof

Step Hyp Ref Expression
1 prjsprel.1
 |-  .~ = { <. x , y >. | ( ( x e. B /\ y e. B ) /\ E. l e. K x = ( l .x. y ) ) }
2 prjspertr.b
 |-  B = ( ( Base ` V ) \ { ( 0g ` V ) } )
3 prjspertr.s
 |-  S = ( Scalar ` V )
4 prjspertr.x
 |-  .x. = ( .s ` V )
5 prjspertr.k
 |-  K = ( Base ` S )
6 prjspreln0.z
 |-  .0. = ( 0g ` S )
7 eqid
 |-  ( Base ` V ) = ( Base ` V )
8 lveclmod
 |-  ( V e. LVec -> V e. LMod )
9 8 3ad2ant1
 |-  ( ( V e. LVec /\ X e. B /\ N e. ( K \ { .0. } ) ) -> V e. LMod )
10 eldifi
 |-  ( N e. ( K \ { .0. } ) -> N e. K )
11 10 3ad2ant3
 |-  ( ( V e. LVec /\ X e. B /\ N e. ( K \ { .0. } ) ) -> N e. K )
12 difss
 |-  ( ( Base ` V ) \ { ( 0g ` V ) } ) C_ ( Base ` V )
13 2 12 eqsstri
 |-  B C_ ( Base ` V )
14 13 sseli
 |-  ( X e. B -> X e. ( Base ` V ) )
15 14 3ad2ant2
 |-  ( ( V e. LVec /\ X e. B /\ N e. ( K \ { .0. } ) ) -> X e. ( Base ` V ) )
16 7 3 4 5 9 11 15 lmodvscld
 |-  ( ( V e. LVec /\ X e. B /\ N e. ( K \ { .0. } ) ) -> ( N .x. X ) e. ( Base ` V ) )
17 eldifsni
 |-  ( N e. ( K \ { .0. } ) -> N =/= .0. )
18 17 3ad2ant3
 |-  ( ( V e. LVec /\ X e. B /\ N e. ( K \ { .0. } ) ) -> N =/= .0. )
19 eldifsni
 |-  ( X e. ( ( Base ` V ) \ { ( 0g ` V ) } ) -> X =/= ( 0g ` V ) )
20 19 2 eleq2s
 |-  ( X e. B -> X =/= ( 0g ` V ) )
21 20 3ad2ant2
 |-  ( ( V e. LVec /\ X e. B /\ N e. ( K \ { .0. } ) ) -> X =/= ( 0g ` V ) )
22 eqid
 |-  ( 0g ` V ) = ( 0g ` V )
23 simp1
 |-  ( ( V e. LVec /\ X e. B /\ N e. ( K \ { .0. } ) ) -> V e. LVec )
24 7 4 3 5 6 22 23 11 15 lvecvsn0
 |-  ( ( V e. LVec /\ X e. B /\ N e. ( K \ { .0. } ) ) -> ( ( N .x. X ) =/= ( 0g ` V ) <-> ( N =/= .0. /\ X =/= ( 0g ` V ) ) ) )
25 18 21 24 mpbir2and
 |-  ( ( V e. LVec /\ X e. B /\ N e. ( K \ { .0. } ) ) -> ( N .x. X ) =/= ( 0g ` V ) )
26 nelsn
 |-  ( ( N .x. X ) =/= ( 0g ` V ) -> -. ( N .x. X ) e. { ( 0g ` V ) } )
27 25 26 syl
 |-  ( ( V e. LVec /\ X e. B /\ N e. ( K \ { .0. } ) ) -> -. ( N .x. X ) e. { ( 0g ` V ) } )
28 16 27 eldifd
 |-  ( ( V e. LVec /\ X e. B /\ N e. ( K \ { .0. } ) ) -> ( N .x. X ) e. ( ( Base ` V ) \ { ( 0g ` V ) } ) )
29 28 2 eleqtrrdi
 |-  ( ( V e. LVec /\ X e. B /\ N e. ( K \ { .0. } ) ) -> ( N .x. X ) e. B )
30 simp2
 |-  ( ( V e. LVec /\ X e. B /\ N e. ( K \ { .0. } ) ) -> X e. B )
31 oveq1
 |-  ( N = m -> ( N .x. X ) = ( m .x. X ) )
32 31 eqcoms
 |-  ( m = N -> ( N .x. X ) = ( m .x. X ) )
33 tbtru
 |-  ( ( N .x. X ) = ( m .x. X ) <-> ( ( N .x. X ) = ( m .x. X ) <-> T. ) )
34 32 33 sylib
 |-  ( m = N -> ( ( N .x. X ) = ( m .x. X ) <-> T. ) )
35 34 adantl
 |-  ( ( ( V e. LVec /\ X e. B /\ N e. ( K \ { .0. } ) ) /\ m = N ) -> ( ( N .x. X ) = ( m .x. X ) <-> T. ) )
36 trud
 |-  ( ( V e. LVec /\ X e. B /\ N e. ( K \ { .0. } ) ) -> T. )
37 11 35 36 rspcedvd
 |-  ( ( V e. LVec /\ X e. B /\ N e. ( K \ { .0. } ) ) -> E. m e. K ( N .x. X ) = ( m .x. X ) )
38 1 prjsprel
 |-  ( ( N .x. X ) .~ X <-> ( ( ( N .x. X ) e. B /\ X e. B ) /\ E. m e. K ( N .x. X ) = ( m .x. X ) ) )
39 29 30 37 38 syl21anbrc
 |-  ( ( V e. LVec /\ X e. B /\ N e. ( K \ { .0. } ) ) -> ( N .x. X ) .~ X )