Metamath Proof Explorer

Theorem ldualvsub

Description: The value of vector subtraction in the dual of a vector space. (Contributed by NM, 27-Feb-2015)

Ref Expression
Hypotheses ldualvsub.r 
|- R = ( Scalar ` W )
ldualvsub.n 
|- N = ( invg ` R )
ldualvsub.u 
|- .1. = ( 1r ` R )
ldualvsub.f 
|- F = ( LFnl ` W )
ldualvsub.d 
|- D = ( LDual ` W )
ldualvsub.p 
|- .+ = ( +g ` D )
ldualvsub.t 
|- .x. = ( .s ` D )
ldualvsub.m 
|- .- = ( -g ` D )
ldualvsub.w 
|- ( ph -> W e. LMod )
ldualvsub.g 
|- ( ph -> G e. F )
ldualvsub.h 
|- ( ph -> H e. F )
Assertion ldualvsub 
|- ( ph -> ( G .- H ) = ( G .+ ( ( N ` .1. ) .x. H ) ) )

Proof

Step Hyp Ref Expression
1 ldualvsub.r 
 |-  R = ( Scalar ` W )
2 ldualvsub.n 
 |-  N = ( invg ` R )
3 ldualvsub.u 
 |-  .1. = ( 1r ` R )
4 ldualvsub.f 
 |-  F = ( LFnl ` W )
5 ldualvsub.d 
 |-  D = ( LDual ` W )
6 ldualvsub.p 
 |-  .+ = ( +g ` D )
7 ldualvsub.t 
 |-  .x. = ( .s ` D )
8 ldualvsub.m 
 |-  .- = ( -g ` D )
9 ldualvsub.w 
 |-  ( ph -> W e. LMod )
10 ldualvsub.g 
 |-  ( ph -> G e. F )
11 ldualvsub.h 
 |-  ( ph -> H e. F )
12 5 9 lduallmod 
 |-  ( ph -> D e. LMod )
13 eqid 
 |-  ( Base ` D ) = ( Base ` D )
14 4 5 13 9 10 ldualelvbase 
 |-  ( ph -> G e. ( Base ` D ) )
15 4 5 13 9 11 ldualelvbase 
 |-  ( ph -> H e. ( Base ` D ) )
16 eqid 
 |-  ( Scalar ` D ) = ( Scalar ` D )
17 eqid 
 |-  ( invg ` ( Scalar ` D ) ) = ( invg ` ( Scalar ` D ) )
18 eqid 
 |-  ( 1r ` ( Scalar ` D ) ) = ( 1r ` ( Scalar ` D ) )
19 13 6 8 16 7 17 18 lmodvsubval2 
 |-  ( ( D e. LMod /\ G e. ( Base ` D ) /\ H e. ( Base ` D ) ) -> ( G .- H ) = ( G .+ ( ( ( invg ` ( Scalar ` D ) ) ` ( 1r ` ( Scalar ` D ) ) ) .x. H ) ) )
20 12 14 15 19 syl3anc 
 |-  ( ph -> ( G .- H ) = ( G .+ ( ( ( invg ` ( Scalar ` D ) ) ` ( 1r ` ( Scalar ` D ) ) ) .x. H ) ) )
21 eqid 
 |-  ( oppR ` R ) = ( oppR ` R )
22 21 2 opprneg 
 |-  N = ( invg ` ( oppR ` R ) )
23 1 21 5 16 9 ldualsca 
 |-  ( ph -> ( Scalar ` D ) = ( oppR ` R ) )
24 23 fveq2d 
 |-  ( ph -> ( invg ` ( Scalar ` D ) ) = ( invg ` ( oppR ` R ) ) )
25 22 24 eqtr4id 
 |-  ( ph -> N = ( invg ` ( Scalar ` D ) ) )
26 21 3 oppr1 
 |-  .1. = ( 1r ` ( oppR ` R ) )
27 23 fveq2d 
 |-  ( ph -> ( 1r ` ( Scalar ` D ) ) = ( 1r ` ( oppR ` R ) ) )
28 26 27 eqtr4id 
 |-  ( ph -> .1. = ( 1r ` ( Scalar ` D ) ) )
29 25 28 fveq12d 
 |-  ( ph -> ( N ` .1. ) = ( ( invg ` ( Scalar ` D ) ) ` ( 1r ` ( Scalar ` D ) ) ) )
30 29 oveq1d 
 |-  ( ph -> ( ( N ` .1. ) .x. H ) = ( ( ( invg ` ( Scalar ` D ) ) ` ( 1r ` ( Scalar ` D ) ) ) .x. H ) )
31 30 oveq2d 
 |-  ( ph -> ( G .+ ( ( N ` .1. ) .x. H ) ) = ( G .+ ( ( ( invg ` ( Scalar ` D ) ) ` ( 1r ` ( Scalar ` D ) ) ) .x. H ) ) )
32 20 31 eqtr4d 
 |-  ( ph -> ( G .- H ) = ( G .+ ( ( N ` .1. ) .x. H ) ) )