Metamath Proof Explorer


Theorem lcdvsub

Description: The value of vector subtraction in the closed kernel dual space. (Contributed by NM, 22-Mar-2015)

Ref Expression
Hypotheses lcdvsub.h H = LHyp K
lcdvsub.u U = DVecH K W
lcdvsub.s S = Scalar U
lcdvsub.n N = inv g S
lcdvsub.e 1 ˙ = 1 S
lcdvsub.c C = LCDual K W
lcdvsub.v V = Base C
lcdvsub.p + ˙ = + C
lcdvsub.t · ˙ = C
lcdvsub.m - ˙ = - C
lcdvsub.k φ K HL W H
lcdvsub.f φ F V
lcdvsub.g φ G V
Assertion lcdvsub φ F - ˙ G = F + ˙ N 1 ˙ · ˙ G

Proof

Step Hyp Ref Expression
1 lcdvsub.h H = LHyp K
2 lcdvsub.u U = DVecH K W
3 lcdvsub.s S = Scalar U
4 lcdvsub.n N = inv g S
5 lcdvsub.e 1 ˙ = 1 S
6 lcdvsub.c C = LCDual K W
7 lcdvsub.v V = Base C
8 lcdvsub.p + ˙ = + C
9 lcdvsub.t · ˙ = C
10 lcdvsub.m - ˙ = - C
11 lcdvsub.k φ K HL W H
12 lcdvsub.f φ F V
13 lcdvsub.g φ G V
14 1 6 11 lcdlmod φ C LMod
15 eqid Scalar C = Scalar C
16 eqid inv g Scalar C = inv g Scalar C
17 eqid 1 Scalar C = 1 Scalar C
18 7 8 10 15 9 16 17 lmodvsubval2 C LMod F V G V F - ˙ G = F + ˙ inv g Scalar C 1 Scalar C · ˙ G
19 14 12 13 18 syl3anc φ F - ˙ G = F + ˙ inv g Scalar C 1 Scalar C · ˙ G
20 eqid opp r S = opp r S
21 20 4 opprneg N = inv g opp r S
22 1 2 3 20 6 15 11 lcdsca φ Scalar C = opp r S
23 22 fveq2d φ inv g Scalar C = inv g opp r S
24 21 23 eqtr4id φ N = inv g Scalar C
25 20 5 oppr1 1 ˙ = 1 opp r S
26 22 fveq2d φ 1 Scalar C = 1 opp r S
27 25 26 eqtr4id φ 1 ˙ = 1 Scalar C
28 24 27 fveq12d φ N 1 ˙ = inv g Scalar C 1 Scalar C
29 28 oveq1d φ N 1 ˙ · ˙ G = inv g Scalar C 1 Scalar C · ˙ G
30 29 oveq2d φ F + ˙ N 1 ˙ · ˙ G = F + ˙ inv g Scalar C 1 Scalar C · ˙ G
31 19 30 eqtr4d φ F - ˙ G = F + ˙ N 1 ˙ · ˙ G