Metamath Proof Explorer

Theorem lvecvscan

Description: Cancellation law for scalar multiplication. ( hvmulcan analog.) (Contributed by NM, 2-Jul-2014)

Ref Expression
Hypotheses lvecmulcan.v 
|- V = ( Base ` W )
lvecmulcan.s 
|- .x. = ( .s ` W )
lvecmulcan.f 
|- F = ( Scalar ` W )
lvecmulcan.k 
|- K = ( Base ` F )
lvecmulcan.o 
|- .0. = ( 0g ` F )
lvecmulcan.w 
|- ( ph -> W e. LVec )
lvecmulcan.a 
|- ( ph -> A e. K )
lvecmulcan.x 
|- ( ph -> X e. V )
lvecmulcan.y 
|- ( ph -> Y e. V )
lvecmulcan.n 
|- ( ph -> A =/= .0. )
Assertion lvecvscan 
|- ( ph -> ( ( A .x. X ) = ( A .x. Y ) <-> X = Y ) )

Proof

Step Hyp Ref Expression
1 lvecmulcan.v 
 |-  V = ( Base ` W )
2 lvecmulcan.s 
 |-  .x. = ( .s ` W )
3 lvecmulcan.f 
 |-  F = ( Scalar ` W )
4 lvecmulcan.k 
 |-  K = ( Base ` F )
5 lvecmulcan.o 
 |-  .0. = ( 0g ` F )
6 lvecmulcan.w 
 |-  ( ph -> W e. LVec )
7 lvecmulcan.a 
 |-  ( ph -> A e. K )
8 lvecmulcan.x 
 |-  ( ph -> X e. V )
9 lvecmulcan.y 
 |-  ( ph -> Y e. V )
10 lvecmulcan.n 
 |-  ( ph -> A =/= .0. )
11 df-ne 
 |-  ( A =/= .0. <-> -. A = .0. )
12 biorf 
 |-  ( -. A = .0. -> ( ( X ( -g ` W ) Y ) = ( 0g ` W ) <-> ( A = .0. \/ ( X ( -g ` W ) Y ) = ( 0g ` W ) ) ) )
13 11 12 sylbi 
 |-  ( A =/= .0. -> ( ( X ( -g ` W ) Y ) = ( 0g ` W ) <-> ( A = .0. \/ ( X ( -g ` W ) Y ) = ( 0g ` W ) ) ) )
14 10 13 syl 
 |-  ( ph -> ( ( X ( -g ` W ) Y ) = ( 0g ` W ) <-> ( A = .0. \/ ( X ( -g ` W ) Y ) = ( 0g ` W ) ) ) )
15 lveclmod 
 |-  ( W e. LVec -> W e. LMod )
16 6 15 syl 
 |-  ( ph -> W e. LMod )
17 eqid 
 |-  ( 0g ` W ) = ( 0g ` W )
18 eqid 
 |-  ( -g ` W ) = ( -g ` W )
19 1 17 18 lmodsubeq0 
 |-  ( ( W e. LMod /\ X e. V /\ Y e. V ) -> ( ( X ( -g ` W ) Y ) = ( 0g ` W ) <-> X = Y ) )
20 16 8 9 19 syl3anc 
 |-  ( ph -> ( ( X ( -g ` W ) Y ) = ( 0g ` W ) <-> X = Y ) )
21 1 2 3 4 18 16 7 8 9 lmodsubdi 
 |-  ( ph -> ( A .x. ( X ( -g ` W ) Y ) ) = ( ( A .x. X ) ( -g ` W ) ( A .x. Y ) ) )
22 21 eqeq1d 
 |-  ( ph -> ( ( A .x. ( X ( -g ` W ) Y ) ) = ( 0g ` W ) <-> ( ( A .x. X ) ( -g ` W ) ( A .x. Y ) ) = ( 0g ` W ) ) )
23 1 18 lmodvsubcl 
 |-  ( ( W e. LMod /\ X e. V /\ Y e. V ) -> ( X ( -g ` W ) Y ) e. V )
24 16 8 9 23 syl3anc 
 |-  ( ph -> ( X ( -g ` W ) Y ) e. V )
25 1 2 3 4 5 17 6 7 24 lvecvs0or 
 |-  ( ph -> ( ( A .x. ( X ( -g ` W ) Y ) ) = ( 0g ` W ) <-> ( A = .0. \/ ( X ( -g ` W ) Y ) = ( 0g ` W ) ) ) )
26 1 3 2 4 lmodvscl 
 |-  ( ( W e. LMod /\ A e. K /\ X e. V ) -> ( A .x. X ) e. V )
27 16 7 8 26 syl3anc 
 |-  ( ph -> ( A .x. X ) e. V )
28 1 3 2 4 lmodvscl 
 |-  ( ( W e. LMod /\ A e. K /\ Y e. V ) -> ( A .x. Y ) e. V )
29 16 7 9 28 syl3anc 
 |-  ( ph -> ( A .x. Y ) e. V )
30 1 17 18 lmodsubeq0 
 |-  ( ( W e. LMod /\ ( A .x. X ) e. V /\ ( A .x. Y ) e. V ) -> ( ( ( A .x. X ) ( -g ` W ) ( A .x. Y ) ) = ( 0g ` W ) <-> ( A .x. X ) = ( A .x. Y ) ) )
31 16 27 29 30 syl3anc 
 |-  ( ph -> ( ( ( A .x. X ) ( -g ` W ) ( A .x. Y ) ) = ( 0g ` W ) <-> ( A .x. X ) = ( A .x. Y ) ) )
32 22 25 31 3bitr3d 
 |-  ( ph -> ( ( A = .0. \/ ( X ( -g ` W ) Y ) = ( 0g ` W ) ) <-> ( A .x. X ) = ( A .x. Y ) ) )
33 14 20 32 3bitr3rd 
 |-  ( ph -> ( ( A .x. X ) = ( A .x. Y ) <-> X = Y ) )