Metamath Proof Explorer

Theorem prjspreln0

Description: Two nonzero vectors are equivalent by a nonzero scalar. (Contributed by Steven Nguyen, 31-May-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 prjspreln0 
|- ( V e. LVec -> ( X .~ Y <-> ( ( X e. B /\ Y e. B ) /\ E. m e. ( K \ { .0. } ) X = ( m .x. Y ) ) ) )

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 1 prjsprel 
 |-  ( X .~ Y <-> ( ( X e. B /\ Y e. B ) /\ E. m e. K X = ( m .x. Y ) ) )
8 simprl 
 |-  ( ( ( V e. LVec /\ ( X e. B /\ Y e. B ) ) /\ ( m e. K /\ X = ( m .x. Y ) ) ) -> m e. K )
9 simplrl 
 |-  ( ( ( V e. LVec /\ ( X e. B /\ Y e. B ) ) /\ ( m e. K /\ X = ( m .x. Y ) ) ) -> X e. B )
10 eldifsni 
 |-  ( X e. ( ( Base ` V ) \ { ( 0g ` V ) } ) -> X =/= ( 0g ` V ) )
11 10 2 eleq2s 
 |-  ( X e. B -> X =/= ( 0g ` V ) )
12 9 11 syl 
 |-  ( ( ( V e. LVec /\ ( X e. B /\ Y e. B ) ) /\ ( m e. K /\ X = ( m .x. Y ) ) ) -> X =/= ( 0g ` V ) )
13 simplrr 
 |-  ( ( ( ( V e. LVec /\ ( X e. B /\ Y e. B ) ) /\ ( m e. K /\ X = ( m .x. Y ) ) ) /\ m = .0. ) -> X = ( m .x. Y ) )
14 simpr 
 |-  ( ( ( ( V e. LVec /\ ( X e. B /\ Y e. B ) ) /\ ( m e. K /\ X = ( m .x. Y ) ) ) /\ m = .0. ) -> m = .0. )
15 14 oveq1d 
 |-  ( ( ( ( V e. LVec /\ ( X e. B /\ Y e. B ) ) /\ ( m e. K /\ X = ( m .x. Y ) ) ) /\ m = .0. ) -> ( m .x. Y ) = ( .0. .x. Y ) )
16 lveclmod 
 |-  ( V e. LVec -> V e. LMod )
17 16 ad3antrrr 
 |-  ( ( ( ( V e. LVec /\ ( X e. B /\ Y e. B ) ) /\ ( m e. K /\ X = ( m .x. Y ) ) ) /\ m = .0. ) -> V e. LMod )
18 difss 
 |-  ( ( Base ` V ) \ { ( 0g ` V ) } ) C_ ( Base ` V )
19 2 18 eqsstri 
 |-  B C_ ( Base ` V )
20 simplrr 
 |-  ( ( ( V e. LVec /\ ( X e. B /\ Y e. B ) ) /\ ( ( m e. K /\ X = ( m .x. Y ) ) /\ m = .0. ) ) -> Y e. B )
21 20 anassrs 
 |-  ( ( ( ( V e. LVec /\ ( X e. B /\ Y e. B ) ) /\ ( m e. K /\ X = ( m .x. Y ) ) ) /\ m = .0. ) -> Y e. B )
22 19 21 sselid 
 |-  ( ( ( ( V e. LVec /\ ( X e. B /\ Y e. B ) ) /\ ( m e. K /\ X = ( m .x. Y ) ) ) /\ m = .0. ) -> Y e. ( Base ` V ) )
23 eqid 
 |-  ( Base ` V ) = ( Base ` V )
24 eqid 
 |-  ( 0g ` V ) = ( 0g ` V )
25 23 3 4 6 24 lmod0vs 
 |-  ( ( V e. LMod /\ Y e. ( Base ` V ) ) -> ( .0. .x. Y ) = ( 0g ` V ) )
26 17 22 25 syl2anc 
 |-  ( ( ( ( V e. LVec /\ ( X e. B /\ Y e. B ) ) /\ ( m e. K /\ X = ( m .x. Y ) ) ) /\ m = .0. ) -> ( .0. .x. Y ) = ( 0g ` V ) )
27 13 15 26 3eqtrd 
 |-  ( ( ( ( V e. LVec /\ ( X e. B /\ Y e. B ) ) /\ ( m e. K /\ X = ( m .x. Y ) ) ) /\ m = .0. ) -> X = ( 0g ` V ) )
28 12 27 mteqand 
 |-  ( ( ( V e. LVec /\ ( X e. B /\ Y e. B ) ) /\ ( m e. K /\ X = ( m .x. Y ) ) ) -> m =/= .0. )
29 nelsn 
 |-  ( m =/= .0. -> -. m e. { .0. } )
30 28 29 syl 
 |-  ( ( ( V e. LVec /\ ( X e. B /\ Y e. B ) ) /\ ( m e. K /\ X = ( m .x. Y ) ) ) -> -. m e. { .0. } )
31 8 30 eldifd 
 |-  ( ( ( V e. LVec /\ ( X e. B /\ Y e. B ) ) /\ ( m e. K /\ X = ( m .x. Y ) ) ) -> m e. ( K \ { .0. } ) )
32 31 ex 
 |-  ( ( V e. LVec /\ ( X e. B /\ Y e. B ) ) -> ( ( m e. K /\ X = ( m .x. Y ) ) -> m e. ( K \ { .0. } ) ) )
33 simpr 
 |-  ( ( m e. K /\ X = ( m .x. Y ) ) -> X = ( m .x. Y ) )
34 32 33 jca2 
 |-  ( ( V e. LVec /\ ( X e. B /\ Y e. B ) ) -> ( ( m e. K /\ X = ( m .x. Y ) ) -> ( m e. ( K \ { .0. } ) /\ X = ( m .x. Y ) ) ) )
35 34 reximdv2 
 |-  ( ( V e. LVec /\ ( X e. B /\ Y e. B ) ) -> ( E. m e. K X = ( m .x. Y ) -> E. m e. ( K \ { .0. } ) X = ( m .x. Y ) ) )
36 difss 
 |-  ( K \ { .0. } ) C_ K
37 ssrexv 
 |-  ( ( K \ { .0. } ) C_ K -> ( E. m e. ( K \ { .0. } ) X = ( m .x. Y ) -> E. m e. K X = ( m .x. Y ) ) )
38 36 37 mp1i 
 |-  ( ( V e. LVec /\ ( X e. B /\ Y e. B ) ) -> ( E. m e. ( K \ { .0. } ) X = ( m .x. Y ) -> E. m e. K X = ( m .x. Y ) ) )
39 35 38 impbid 
 |-  ( ( V e. LVec /\ ( X e. B /\ Y e. B ) ) -> ( E. m e. K X = ( m .x. Y ) <-> E. m e. ( K \ { .0. } ) X = ( m .x. Y ) ) )
40 39 pm5.32da 
 |-  ( V e. LVec -> ( ( ( X e. B /\ Y e. B ) /\ E. m e. K X = ( m .x. Y ) ) <-> ( ( X e. B /\ Y e. B ) /\ E. m e. ( K \ { .0. } ) X = ( m .x. Y ) ) ) )
41 7 40 bitrid 
 |-  ( V e. LVec -> ( X .~ Y <-> ( ( X e. B /\ Y e. B ) /\ E. m e. ( K \ { .0. } ) X = ( m .x. Y ) ) ) )