Metamath Proof Explorer

Theorem lvecvscan2

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

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

Proof

Step Hyp Ref Expression
1 lvecmulcan2.v 
 |-  V = ( Base ` W )
2 lvecmulcan2.s 
 |-  .x. = ( .s ` W )
3 lvecmulcan2.f 
 |-  F = ( Scalar ` W )
4 lvecmulcan2.k 
 |-  K = ( Base ` F )
5 lvecmulcan2.o 
 |-  .0. = ( 0g ` W )
6 lvecmulcan2.w 
 |-  ( ph -> W e. LVec )
7 lvecmulcan2.a 
 |-  ( ph -> A e. K )
8 lvecmulcan2.b 
 |-  ( ph -> B e. K )
9 lvecmulcan2.x 
 |-  ( ph -> X e. V )
10 lvecmulcan2.n 
 |-  ( ph -> X =/= .0. )
11 10 neneqd 
 |-  ( ph -> -. X = .0. )
12 biorf 
 |-  ( -. X = .0. -> ( ( A ( -g ` F ) B ) = ( 0g ` F ) <-> ( X = .0. \/ ( A ( -g ` F ) B ) = ( 0g ` F ) ) ) )
13 orcom 
 |-  ( ( X = .0. \/ ( A ( -g ` F ) B ) = ( 0g ` F ) ) <-> ( ( A ( -g ` F ) B ) = ( 0g ` F ) \/ X = .0. ) )
14 12 13 bitrdi 
 |-  ( -. X = .0. -> ( ( A ( -g ` F ) B ) = ( 0g ` F ) <-> ( ( A ( -g ` F ) B ) = ( 0g ` F ) \/ X = .0. ) ) )
15 11 14 syl 
 |-  ( ph -> ( ( A ( -g ` F ) B ) = ( 0g ` F ) <-> ( ( A ( -g ` F ) B ) = ( 0g ` F ) \/ X = .0. ) ) )
16 eqid 
 |-  ( 0g ` F ) = ( 0g ` F )
17 lveclmod 
 |-  ( W e. LVec -> W e. LMod )
18 6 17 syl 
 |-  ( ph -> W e. LMod )
19 3 lmodfgrp 
 |-  ( W e. LMod -> F e. Grp )
20 18 19 syl 
 |-  ( ph -> F e. Grp )
21 eqid 
 |-  ( -g ` F ) = ( -g ` F )
22 4 21 grpsubcl 
 |-  ( ( F e. Grp /\ A e. K /\ B e. K ) -> ( A ( -g ` F ) B ) e. K )
23 20 7 8 22 syl3anc 
 |-  ( ph -> ( A ( -g ` F ) B ) e. K )
24 1 2 3 4 16 5 6 23 9 lvecvs0or 
 |-  ( ph -> ( ( ( A ( -g ` F ) B ) .x. X ) = .0. <-> ( ( A ( -g ` F ) B ) = ( 0g ` F ) \/ X = .0. ) ) )
25 eqid 
 |-  ( -g ` W ) = ( -g ` W )
26 1 2 3 4 25 21 18 7 8 9 lmodsubdir 
 |-  ( ph -> ( ( A ( -g ` F ) B ) .x. X ) = ( ( A .x. X ) ( -g ` W ) ( B .x. X ) ) )
27 26 eqeq1d 
 |-  ( ph -> ( ( ( A ( -g ` F ) B ) .x. X ) = .0. <-> ( ( A .x. X ) ( -g ` W ) ( B .x. X ) ) = .0. ) )
28 15 24 27 3bitr2rd 
 |-  ( ph -> ( ( ( A .x. X ) ( -g ` W ) ( B .x. X ) ) = .0. <-> ( A ( -g ` F ) B ) = ( 0g ` F ) ) )
29 1 3 2 4 lmodvscl 
 |-  ( ( W e. LMod /\ A e. K /\ X e. V ) -> ( A .x. X ) e. V )
30 18 7 9 29 syl3anc 
 |-  ( ph -> ( A .x. X ) e. V )
31 1 3 2 4 lmodvscl 
 |-  ( ( W e. LMod /\ B e. K /\ X e. V ) -> ( B .x. X ) e. V )
32 18 8 9 31 syl3anc 
 |-  ( ph -> ( B .x. X ) e. V )
33 1 5 25 lmodsubeq0 
 |-  ( ( W e. LMod /\ ( A .x. X ) e. V /\ ( B .x. X ) e. V ) -> ( ( ( A .x. X ) ( -g ` W ) ( B .x. X ) ) = .0. <-> ( A .x. X ) = ( B .x. X ) ) )
34 18 30 32 33 syl3anc 
 |-  ( ph -> ( ( ( A .x. X ) ( -g ` W ) ( B .x. X ) ) = .0. <-> ( A .x. X ) = ( B .x. X ) ) )
35 4 16 21 grpsubeq0 
 |-  ( ( F e. Grp /\ A e. K /\ B e. K ) -> ( ( A ( -g ` F ) B ) = ( 0g ` F ) <-> A = B ) )
36 20 7 8 35 syl3anc 
 |-  ( ph -> ( ( A ( -g ` F ) B ) = ( 0g ` F ) <-> A = B ) )
37 28 34 36 3bitr3d 
 |-  ( ph -> ( ( A .x. X ) = ( B .x. X ) <-> A = B ) )