Metamath Proof Explorer

Theorem lcdvsub

Description: The value of vector subtraction in the closed kernel dual space. (Contributed by NM, 22-Mar-2015)

Ref Expression
Hypotheses lcdvsub.h 
|- H = ( LHyp ` K )
lcdvsub.u 
|- U = ( ( DVecH ` K ) ` W )
lcdvsub.s 
|- S = ( Scalar ` U )
lcdvsub.n 
|- N = ( invg ` S )
lcdvsub.e 
|- .1. = ( 1r ` S )
lcdvsub.c 
|- C = ( ( LCDual ` K ) ` W )
lcdvsub.v 
|- V = ( Base ` C )
lcdvsub.p 
|- .+ = ( +g ` C )
lcdvsub.t 
|- .x. = ( .s ` C )
lcdvsub.m 
|- .- = ( -g ` C )
lcdvsub.k 
|- ( ph -> ( K e. HL /\ W e. H ) )
lcdvsub.f 
|- ( ph -> F e. V )
lcdvsub.g 
|- ( ph -> G e. V )
Assertion lcdvsub 
|- ( ph -> ( F .- G ) = ( F .+ ( ( N ` .1. ) .x. G ) ) )

Proof

Step Hyp Ref Expression
1 lcdvsub.h 
 |-  H = ( LHyp ` K )
2 lcdvsub.u 
 |-  U = ( ( DVecH ` K ) ` W )
3 lcdvsub.s 
 |-  S = ( Scalar ` U )
4 lcdvsub.n 
 |-  N = ( invg ` S )
5 lcdvsub.e 
 |-  .1. = ( 1r ` S )
6 lcdvsub.c 
 |-  C = ( ( LCDual ` K ) ` W )
7 lcdvsub.v 
 |-  V = ( Base ` C )
8 lcdvsub.p 
 |-  .+ = ( +g ` C )
9 lcdvsub.t 
 |-  .x. = ( .s ` C )
10 lcdvsub.m 
 |-  .- = ( -g ` C )
11 lcdvsub.k 
 |-  ( ph -> ( K e. HL /\ W e. H ) )
12 lcdvsub.f 
 |-  ( ph -> F e. V )
13 lcdvsub.g 
 |-  ( ph -> G e. V )
14 1 6 11 lcdlmod 
 |-  ( ph -> C e. LMod )
15 eqid 
 |-  ( Scalar ` C ) = ( Scalar ` C )
16 eqid 
 |-  ( invg ` ( Scalar ` C ) ) = ( invg ` ( Scalar ` C ) )
17 eqid 
 |-  ( 1r ` ( Scalar ` C ) ) = ( 1r ` ( Scalar ` C ) )
18 7 8 10 15 9 16 17 lmodvsubval2 
 |-  ( ( C e. LMod /\ F e. V /\ G e. V ) -> ( F .- G ) = ( F .+ ( ( ( invg ` ( Scalar ` C ) ) ` ( 1r ` ( Scalar ` C ) ) ) .x. G ) ) )
19 14 12 13 18 syl3anc 
 |-  ( ph -> ( F .- G ) = ( F .+ ( ( ( invg ` ( Scalar ` C ) ) ` ( 1r ` ( Scalar ` C ) ) ) .x. G ) ) )
20 eqid 
 |-  ( oppR ` S ) = ( oppR ` S )
21 20 4 opprneg 
 |-  N = ( invg ` ( oppR ` S ) )
22 1 2 3 20 6 15 11 lcdsca 
 |-  ( ph -> ( Scalar ` C ) = ( oppR ` S ) )
23 22 fveq2d 
 |-  ( ph -> ( invg ` ( Scalar ` C ) ) = ( invg ` ( oppR ` S ) ) )
24 21 23 eqtr4id 
 |-  ( ph -> N = ( invg ` ( Scalar ` C ) ) )
25 20 5 oppr1 
 |-  .1. = ( 1r ` ( oppR ` S ) )
26 22 fveq2d 
 |-  ( ph -> ( 1r ` ( Scalar ` C ) ) = ( 1r ` ( oppR ` S ) ) )
27 25 26 eqtr4id 
 |-  ( ph -> .1. = ( 1r ` ( Scalar ` C ) ) )
28 24 27 fveq12d 
 |-  ( ph -> ( N ` .1. ) = ( ( invg ` ( Scalar ` C ) ) ` ( 1r ` ( Scalar ` C ) ) ) )
29 28 oveq1d 
 |-  ( ph -> ( ( N ` .1. ) .x. G ) = ( ( ( invg ` ( Scalar ` C ) ) ` ( 1r ` ( Scalar ` C ) ) ) .x. G ) )
30 29 oveq2d 
 |-  ( ph -> ( F .+ ( ( N ` .1. ) .x. G ) ) = ( F .+ ( ( ( invg ` ( Scalar ` C ) ) ` ( 1r ` ( Scalar ` C ) ) ) .x. G ) ) )
31 19 30 eqtr4d 
 |-  ( ph -> ( F .- G ) = ( F .+ ( ( N ` .1. ) .x. G ) ) )