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 ringnegr ⊢ φ → 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