Metamath Proof Explorer

Theorem ldualvsubval

Description: The value of the value of vector subtraction in the dual of a vector space. TODO: shorten with ldualvsub ? (Requires D to oppR conversion.) (Contributed by NM, 26-Feb-2015)

Ref Expression
Hypotheses ldualvsubval.v 
|- V = ( Base ` W )
ldualvsubval.r 
|- R = ( Scalar ` W )
ldualvsubval.s 
|- S = ( -g ` R )
ldualvsubval.f 
|- F = ( LFnl ` W )
ldualvsubval.d 
|- D = ( LDual ` W )
ldualvsubval.m 
|- .- = ( -g ` D )
ldualvsubval.w 
|- ( ph -> W e. LMod )
ldualvsubval.g 
|- ( ph -> G e. F )
ldualvsubval.h 
|- ( ph -> H e. F )
ldualvsubval.x 
|- ( ph -> X e. V )
Assertion ldualvsubval 
|- ( ph -> ( ( G .- H ) ` X ) = ( ( G ` X ) S ( H ` X ) ) )

Proof

Step Hyp Ref Expression
1 ldualvsubval.v 
 |-  V = ( Base ` W )
2 ldualvsubval.r 
 |-  R = ( Scalar ` W )
3 ldualvsubval.s 
 |-  S = ( -g ` R )
4 ldualvsubval.f 
 |-  F = ( LFnl ` W )
5 ldualvsubval.d 
 |-  D = ( LDual ` W )
6 ldualvsubval.m 
 |-  .- = ( -g ` D )
7 ldualvsubval.w 
 |-  ( ph -> W e. LMod )
8 ldualvsubval.g 
 |-  ( ph -> G e. F )
9 ldualvsubval.h 
 |-  ( ph -> H e. F )
10 ldualvsubval.x 
 |-  ( ph -> X e. V )
11 5 7 lduallmod 
 |-  ( ph -> D e. LMod )
12 eqid 
 |-  ( Base ` D ) = ( Base ` D )
13 4 5 12 7 8 ldualelvbase 
 |-  ( ph -> G e. ( Base ` D ) )
14 4 5 12 7 9 ldualelvbase 
 |-  ( ph -> H e. ( Base ` D ) )
15 eqid 
 |-  ( +g ` D ) = ( +g ` D )
16 eqid 
 |-  ( Scalar ` D ) = ( Scalar ` D )
17 eqid 
 |-  ( .s ` D ) = ( .s ` D )
18 eqid 
 |-  ( invg ` ( Scalar ` D ) ) = ( invg ` ( Scalar ` D ) )
19 eqid 
 |-  ( 1r ` ( Scalar ` D ) ) = ( 1r ` ( Scalar ` D ) )
20 12 15 6 16 17 18 19 lmodvsubval2 
 |-  ( ( D e. LMod /\ G e. ( Base ` D ) /\ H e. ( Base ` D ) ) -> ( G .- H ) = ( G ( +g ` D ) ( ( ( invg ` ( Scalar ` D ) ) ` ( 1r ` ( Scalar ` D ) ) ) ( .s ` D ) H ) ) )
21 11 13 14 20 syl3anc 
 |-  ( ph -> ( G .- H ) = ( G ( +g ` D ) ( ( ( invg ` ( Scalar ` D ) ) ` ( 1r ` ( Scalar ` D ) ) ) ( .s ` D ) H ) ) )
22 21 fveq1d 
 |-  ( ph -> ( ( G .- H ) ` X ) = ( ( G ( +g ` D ) ( ( ( invg ` ( Scalar ` D ) ) ` ( 1r ` ( Scalar ` D ) ) ) ( .s ` D ) H ) ) ` X ) )
23 eqid 
 |-  ( +g ` R ) = ( +g ` R )
24 eqid 
 |-  ( Base ` R ) = ( Base ` R )
25 16 lmodfgrp 
 |-  ( D e. LMod -> ( Scalar ` D ) e. Grp )
26 11 25 syl 
 |-  ( ph -> ( Scalar ` D ) e. Grp )
27 16 lmodring 
 |-  ( D e. LMod -> ( Scalar ` D ) e. Ring )
28 11 27 syl 
 |-  ( ph -> ( Scalar ` D ) e. Ring )
29 eqid 
 |-  ( Base ` ( Scalar ` D ) ) = ( Base ` ( Scalar ` D ) )
30 29 19 ringidcl 
 |-  ( ( Scalar ` D ) e. Ring -> ( 1r ` ( Scalar ` D ) ) e. ( Base ` ( Scalar ` D ) ) )
31 28 30 syl 
 |-  ( ph -> ( 1r ` ( Scalar ` D ) ) e. ( Base ` ( Scalar ` D ) ) )
32 29 18 grpinvcl 
 |-  ( ( ( Scalar ` D ) e. Grp /\ ( 1r ` ( Scalar ` D ) ) e. ( Base ` ( Scalar ` D ) ) ) -> ( ( invg ` ( Scalar ` D ) ) ` ( 1r ` ( Scalar ` D ) ) ) e. ( Base ` ( Scalar ` D ) ) )
33 26 31 32 syl2anc 
 |-  ( ph -> ( ( invg ` ( Scalar ` D ) ) ` ( 1r ` ( Scalar ` D ) ) ) e. ( Base ` ( Scalar ` D ) ) )
34 2 24 5 16 29 7 ldualsbase 
 |-  ( ph -> ( Base ` ( Scalar ` D ) ) = ( Base ` R ) )
35 33 34 eleqtrd 
 |-  ( ph -> ( ( invg ` ( Scalar ` D ) ) ` ( 1r ` ( Scalar ` D ) ) ) e. ( Base ` R ) )
36 4 2 24 5 17 7 35 9 ldualvscl 
 |-  ( ph -> ( ( ( invg ` ( Scalar ` D ) ) ` ( 1r ` ( Scalar ` D ) ) ) ( .s ` D ) H ) e. F )
37 1 2 23 4 5 15 7 8 36 10 ldualvaddval 
 |-  ( ph -> ( ( G ( +g ` D ) ( ( ( invg ` ( Scalar ` D ) ) ` ( 1r ` ( Scalar ` D ) ) ) ( .s ` D ) H ) ) ` X ) = ( ( G ` X ) ( +g ` R ) ( ( ( ( invg ` ( Scalar ` D ) ) ` ( 1r ` ( Scalar ` D ) ) ) ( .s ` D ) H ) ` X ) ) )
38 eqid 
 |-  ( invg ` R ) = ( invg ` R )
39 2 38 5 16 18 7 ldualneg 
 |-  ( ph -> ( invg ` ( Scalar ` D ) ) = ( invg ` R ) )
40 eqid 
 |-  ( 1r ` R ) = ( 1r ` R )
41 2 40 5 16 19 7 ldual1 
 |-  ( ph -> ( 1r ` ( Scalar ` D ) ) = ( 1r ` R ) )
42 39 41 fveq12d 
 |-  ( ph -> ( ( invg ` ( Scalar ` D ) ) ` ( 1r ` ( Scalar ` D ) ) ) = ( ( invg ` R ) ` ( 1r ` R ) ) )
43 42 oveq1d 
 |-  ( ph -> ( ( ( invg ` ( Scalar ` D ) ) ` ( 1r ` ( Scalar ` D ) ) ) ( .s ` D ) H ) = ( ( ( invg ` R ) ` ( 1r ` R ) ) ( .s ` D ) H ) )
44 43 fveq1d 
 |-  ( ph -> ( ( ( ( invg ` ( Scalar ` D ) ) ` ( 1r ` ( Scalar ` D ) ) ) ( .s ` D ) H ) ` X ) = ( ( ( ( invg ` R ) ` ( 1r ` R ) ) ( .s ` D ) H ) ` X ) )
45 eqid 
 |-  ( .r ` R ) = ( .r ` R )
46 2 lmodring 
 |-  ( W e. LMod -> R e. Ring )
47 7 46 syl 
 |-  ( ph -> R e. Ring )
48 ringgrp 
 |-  ( R e. Ring -> R e. Grp )
49 47 48 syl 
 |-  ( ph -> R e. Grp )
50 2 24 40 lmod1cl 
 |-  ( W e. LMod -> ( 1r ` R ) e. ( Base ` R ) )
51 7 50 syl 
 |-  ( ph -> ( 1r ` R ) e. ( Base ` R ) )
52 24 38 grpinvcl 
 |-  ( ( R e. Grp /\ ( 1r ` R ) e. ( Base ` R ) ) -> ( ( invg ` R ) ` ( 1r ` R ) ) e. ( Base ` R ) )
53 49 51 52 syl2anc 
 |-  ( ph -> ( ( invg ` R ) ` ( 1r ` R ) ) e. ( Base ` R ) )
54 4 1 2 24 45 5 17 7 53 9 10 ldualvsval 
 |-  ( ph -> ( ( ( ( invg ` R ) ` ( 1r ` R ) ) ( .s ` D ) H ) ` X ) = ( ( H ` X ) ( .r ` R ) ( ( invg ` R ) ` ( 1r ` R ) ) ) )
55 2 24 1 4 lflcl 
 |-  ( ( W e. LMod /\ H e. F /\ X e. V ) -> ( H ` X ) e. ( Base ` R ) )
56 7 9 10 55 syl3anc 
 |-  ( ph -> ( H ` X ) e. ( Base ` R ) )
57 24 45 40 38 47 56 ringnegr 
 |-  ( ph -> ( ( H ` X ) ( .r ` R ) ( ( invg ` R ) ` ( 1r ` R ) ) ) = ( ( invg ` R ) ` ( H ` X ) ) )
58 44 54 57 3eqtrd 
 |-  ( ph -> ( ( ( ( invg ` ( Scalar ` D ) ) ` ( 1r ` ( Scalar ` D ) ) ) ( .s ` D ) H ) ` X ) = ( ( invg ` R ) ` ( H ` X ) ) )
59 58 oveq2d 
 |-  ( ph -> ( ( G ` X ) ( +g ` R ) ( ( ( ( invg ` ( Scalar ` D ) ) ` ( 1r ` ( Scalar ` D ) ) ) ( .s ` D ) H ) ` X ) ) = ( ( G ` X ) ( +g ` R ) ( ( invg ` R ) ` ( H ` X ) ) ) )
60 2 24 1 4 lflcl 
 |-  ( ( W e. LMod /\ G e. F /\ X e. V ) -> ( G ` X ) e. ( Base ` R ) )
61 7 8 10 60 syl3anc 
 |-  ( ph -> ( G ` X ) e. ( Base ` R ) )
62 24 23 38 3 grpsubval 
 |-  ( ( ( G ` X ) e. ( Base ` R ) /\ ( H ` X ) e. ( Base ` R ) ) -> ( ( G ` X ) S ( H ` X ) ) = ( ( G ` X ) ( +g ` R ) ( ( invg ` R ) ` ( H ` X ) ) ) )
63 61 56 62 syl2anc 
 |-  ( ph -> ( ( G ` X ) S ( H ` X ) ) = ( ( G ` X ) ( +g ` R ) ( ( invg ` R ) ` ( H ` X ) ) ) )
64 59 63 eqtr4d 
 |-  ( ph -> ( ( G ` X ) ( +g ` R ) ( ( ( ( invg ` ( Scalar ` D ) ) ` ( 1r ` ( Scalar ` D ) ) ) ( .s ` D ) H ) ` X ) ) = ( ( G ` X ) S ( H ` X ) ) )
65 22 37 64 3eqtrd 
 |-  ( ph -> ( ( G .- H ) ` X ) = ( ( G ` X ) S ( H ` X ) ) )