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 )