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