Metamath Proof Explorer

Theorem lcdvsubval

Description: The value of the value of vector addition in the closed kernel vector space dual. (Contributed by NM, 11-Jun-2015)

Ref Expression
Hypotheses lcdvsubval.h 
|- H = ( LHyp ` K )
lcdvsubval.u 
|- U = ( ( DVecH ` K ) ` W )
lcdvsubval.v 
|- V = ( Base ` U )
lcdvsubval.r 
|- R = ( Scalar ` U )
lcdvsubval.s 
|- S = ( -g ` R )
lcdvsubval.c 
|- C = ( ( LCDual ` K ) ` W )
lcdvsubval.d 
|- D = ( Base ` C )
lcdvsubval.m 
|- .- = ( -g ` C )
lcdvsubval.k 
|- ( ph -> ( K e. HL /\ W e. H ) )
lcdvsubval.f 
|- ( ph -> F e. D )
lcdvsubval.g 
|- ( ph -> G e. D )
lcdvsubval.x 
|- ( ph -> X e. V )
Assertion lcdvsubval 
|- ( ph -> ( ( F .- G ) ` X ) = ( ( F ` X ) S ( G ` X ) ) )

Proof

Step Hyp Ref Expression
1 lcdvsubval.h 
 |-  H = ( LHyp ` K )
2 lcdvsubval.u 
 |-  U = ( ( DVecH ` K ) ` W )
3 lcdvsubval.v 
 |-  V = ( Base ` U )
4 lcdvsubval.r 
 |-  R = ( Scalar ` U )
5 lcdvsubval.s 
 |-  S = ( -g ` R )
6 lcdvsubval.c 
 |-  C = ( ( LCDual ` K ) ` W )
7 lcdvsubval.d 
 |-  D = ( Base ` C )
8 lcdvsubval.m 
 |-  .- = ( -g ` C )
9 lcdvsubval.k 
 |-  ( ph -> ( K e. HL /\ W e. H ) )
10 lcdvsubval.f 
 |-  ( ph -> F e. D )
11 lcdvsubval.g 
 |-  ( ph -> G e. D )
12 lcdvsubval.x 
 |-  ( ph -> X e. V )
13 1 6 9 lcdlmod 
 |-  ( ph -> C e. LMod )
14 eqid 
 |-  ( +g ` C ) = ( +g ` C )
15 eqid 
 |-  ( Scalar ` C ) = ( Scalar ` C )
16 eqid 
 |-  ( .s ` C ) = ( .s ` C )
17 eqid 
 |-  ( invg ` ( Scalar ` C ) ) = ( invg ` ( Scalar ` C ) )
18 eqid 
 |-  ( 1r ` ( Scalar ` C ) ) = ( 1r ` ( Scalar ` C ) )
19 7 14 8 15 16 17 18 lmodvsubval2 
 |-  ( ( C e. LMod /\ F e. D /\ G e. D ) -> ( F .- G ) = ( F ( +g ` C ) ( ( ( invg ` ( Scalar ` C ) ) ` ( 1r ` ( Scalar ` C ) ) ) ( .s ` C ) G ) ) )
20 13 10 11 19 syl3anc 
 |-  ( ph -> ( F .- G ) = ( F ( +g ` C ) ( ( ( invg ` ( Scalar ` C ) ) ` ( 1r ` ( Scalar ` C ) ) ) ( .s ` C ) G ) ) )
21 20 fveq1d 
 |-  ( ph -> ( ( F .- G ) ` X ) = ( ( F ( +g ` C ) ( ( ( invg ` ( Scalar ` C ) ) ` ( 1r ` ( Scalar ` C ) ) ) ( .s ` C ) G ) ) ` X ) )
22 eqid 
 |-  ( +g ` R ) = ( +g ` R )
23 eqid 
 |-  ( Base ` R ) = ( Base ` R )
24 15 lmodfgrp 
 |-  ( C e. LMod -> ( Scalar ` C ) e. Grp )
25 13 24 syl 
 |-  ( ph -> ( Scalar ` C ) e. Grp )
26 15 lmodring 
 |-  ( C e. LMod -> ( Scalar ` C ) e. Ring )
27 13 26 syl 
 |-  ( ph -> ( Scalar ` C ) e. Ring )
28 eqid 
 |-  ( Base ` ( Scalar ` C ) ) = ( Base ` ( Scalar ` C ) )
29 28 18 ringidcl 
 |-  ( ( Scalar ` C ) e. Ring -> ( 1r ` ( Scalar ` C ) ) e. ( Base ` ( Scalar ` C ) ) )
30 27 29 syl 
 |-  ( ph -> ( 1r ` ( Scalar ` C ) ) e. ( Base ` ( Scalar ` C ) ) )
31 28 17 grpinvcl 
 |-  ( ( ( Scalar ` C ) e. Grp /\ ( 1r ` ( Scalar ` C ) ) e. ( Base ` ( Scalar ` C ) ) ) -> ( ( invg ` ( Scalar ` C ) ) ` ( 1r ` ( Scalar ` C ) ) ) e. ( Base ` ( Scalar ` C ) ) )
32 25 30 31 syl2anc 
 |-  ( ph -> ( ( invg ` ( Scalar ` C ) ) ` ( 1r ` ( Scalar ` C ) ) ) e. ( Base ` ( Scalar ` C ) ) )
33 1 2 4 23 6 15 28 9 lcdsbase 
 |-  ( ph -> ( Base ` ( Scalar ` C ) ) = ( Base ` R ) )
34 32 33 eleqtrd 
 |-  ( ph -> ( ( invg ` ( Scalar ` C ) ) ` ( 1r ` ( Scalar ` C ) ) ) e. ( Base ` R ) )
35 1 2 4 23 6 7 16 9 34 11 lcdvscl 
 |-  ( ph -> ( ( ( invg ` ( Scalar ` C ) ) ` ( 1r ` ( Scalar ` C ) ) ) ( .s ` C ) G ) e. D )
36 1 2 3 4 22 6 7 14 9 10 35 12 lcdvaddval 
 |-  ( ph -> ( ( F ( +g ` C ) ( ( ( invg ` ( Scalar ` C ) ) ` ( 1r ` ( Scalar ` C ) ) ) ( .s ` C ) G ) ) ` X ) = ( ( F ` X ) ( +g ` R ) ( ( ( ( invg ` ( Scalar ` C ) ) ` ( 1r ` ( Scalar ` C ) ) ) ( .s ` C ) G ) ` X ) ) )
37 eqid 
 |-  ( invg ` R ) = ( invg ` R )
38 1 2 4 37 6 15 17 9 lcdneg 
 |-  ( ph -> ( invg ` ( Scalar ` C ) ) = ( invg ` R ) )
39 eqid 
 |-  ( 1r ` R ) = ( 1r ` R )
40 1 2 4 39 6 15 18 9 lcd1 
 |-  ( ph -> ( 1r ` ( Scalar ` C ) ) = ( 1r ` R ) )
41 38 40 fveq12d 
 |-  ( ph -> ( ( invg ` ( Scalar ` C ) ) ` ( 1r ` ( Scalar ` C ) ) ) = ( ( invg ` R ) ` ( 1r ` R ) ) )
42 41 oveq1d 
 |-  ( ph -> ( ( ( invg ` ( Scalar ` C ) ) ` ( 1r ` ( Scalar ` C ) ) ) ( .s ` C ) G ) = ( ( ( invg ` R ) ` ( 1r ` R ) ) ( .s ` C ) G ) )
43 42 fveq1d 
 |-  ( ph -> ( ( ( ( invg ` ( Scalar ` C ) ) ` ( 1r ` ( Scalar ` C ) ) ) ( .s ` C ) G ) ` X ) = ( ( ( ( invg ` R ) ` ( 1r ` R ) ) ( .s ` C ) G ) ` X ) )
44 eqid 
 |-  ( .r ` R ) = ( .r ` R )
45 1 2 9 dvhlmod 
 |-  ( ph -> U e. LMod )
46 4 lmodring 
 |-  ( U e. LMod -> R e. Ring )
47 45 46 syl 
 |-  ( ph -> R e. Ring )
48 ringgrp 
 |-  ( R e. Ring -> R e. Grp )
49 47 48 syl 
 |-  ( ph -> R e. Grp )
50 4 23 39 lmod1cl 
 |-  ( U e. LMod -> ( 1r ` R ) e. ( Base ` R ) )
51 45 50 syl 
 |-  ( ph -> ( 1r ` R ) e. ( Base ` R ) )
52 23 37 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 1 2 3 4 23 44 6 7 16 9 53 11 12 lcdvsval 
 |-  ( ph -> ( ( ( ( invg ` R ) ` ( 1r ` R ) ) ( .s ` C ) G ) ` X ) = ( ( G ` X ) ( .r ` R ) ( ( invg ` R ) ` ( 1r ` R ) ) ) )
55 1 2 3 4 23 6 7 9 11 12 lcdvbasecl 
 |-  ( ph -> ( G ` X ) e. ( Base ` R ) )
56 23 44 39 37 47 55 ringnegr 
 |-  ( ph -> ( ( G ` X ) ( .r ` R ) ( ( invg ` R ) ` ( 1r ` R ) ) ) = ( ( invg ` R ) ` ( G ` X ) ) )
57 43 54 56 3eqtrd 
 |-  ( ph -> ( ( ( ( invg ` ( Scalar ` C ) ) ` ( 1r ` ( Scalar ` C ) ) ) ( .s ` C ) G ) ` X ) = ( ( invg ` R ) ` ( G ` X ) ) )
58 57 oveq2d 
 |-  ( ph -> ( ( F ` X ) ( +g ` R ) ( ( ( ( invg ` ( Scalar ` C ) ) ` ( 1r ` ( Scalar ` C ) ) ) ( .s ` C ) G ) ` X ) ) = ( ( F ` X ) ( +g ` R ) ( ( invg ` R ) ` ( G ` X ) ) ) )
59 1 2 3 4 23 6 7 9 10 12 lcdvbasecl 
 |-  ( ph -> ( F ` X ) e. ( Base ` R ) )
60 23 22 37 5 grpsubval 
 |-  ( ( ( F ` X ) e. ( Base ` R ) /\ ( G ` X ) e. ( Base ` R ) ) -> ( ( F ` X ) S ( G ` X ) ) = ( ( F ` X ) ( +g ` R ) ( ( invg ` R ) ` ( G ` X ) ) ) )
61 59 55 60 syl2anc 
 |-  ( ph -> ( ( F ` X ) S ( G ` X ) ) = ( ( F ` X ) ( +g ` R ) ( ( invg ` R ) ` ( G ` X ) ) ) )
62 58 61 eqtr4d 
 |-  ( ph -> ( ( F ` X ) ( +g ` R ) ( ( ( ( invg ` ( Scalar ` C ) ) ` ( 1r ` ( Scalar ` C ) ) ) ( .s ` C ) G ) ` X ) ) = ( ( F ` X ) S ( G ` X ) ) )
63 21 36 62 3eqtrd 
 |-  ( ph -> ( ( F .- G ) ` X ) = ( ( F ` X ) S ( G ` X ) ) )