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