Metamath Proof Explorer


Theorem hdmapgln2

Description: g-linear property that will be used for inner product. (Contributed by NM, 14-Jun-2015)

Ref Expression
Hypotheses hdmapgln2.h H = LHyp K
hdmapgln2.u U = DVecH K W
hdmapgln2.v V = Base U
hdmapgln2.p + ˙ = + U
hdmapgln2.t · ˙ = U
hdmapgln2.r R = Scalar U
hdmapgln2.b B = Base R
hdmapgln2.q ˙ = + R
hdmapgln2.m × ˙ = R
hdmapgln2.s S = HDMap K W
hdmapgln2.g G = HGMap K W
hdmapgln2.k φ K HL W H
hdmapgln2.x φ X V
hdmapgln2.y φ Y V
hdmapgln2.z φ Z V
hdmapgln2.a φ A B
Assertion hdmapgln2 φ S A · ˙ Y + ˙ Z X = S Y X × ˙ G A ˙ S Z X

Proof

Step Hyp Ref Expression
1 hdmapgln2.h H = LHyp K
2 hdmapgln2.u U = DVecH K W
3 hdmapgln2.v V = Base U
4 hdmapgln2.p + ˙ = + U
5 hdmapgln2.t · ˙ = U
6 hdmapgln2.r R = Scalar U
7 hdmapgln2.b B = Base R
8 hdmapgln2.q ˙ = + R
9 hdmapgln2.m × ˙ = R
10 hdmapgln2.s S = HDMap K W
11 hdmapgln2.g G = HGMap K W
12 hdmapgln2.k φ K HL W H
13 hdmapgln2.x φ X V
14 hdmapgln2.y φ Y V
15 hdmapgln2.z φ Z V
16 hdmapgln2.a φ A B
17 1 2 12 dvhlmod φ U LMod
18 3 6 5 7 lmodvscl U LMod A B Y V A · ˙ Y V
19 17 16 14 18 syl3anc φ A · ˙ Y V
20 1 2 3 4 6 8 10 12 13 19 15 hdmaplna2 φ S A · ˙ Y + ˙ Z X = S A · ˙ Y X ˙ S Z X
21 1 2 3 5 6 7 9 10 11 12 13 14 16 hdmapglnm2 φ S A · ˙ Y X = S Y X × ˙ G A
22 21 oveq1d φ S A · ˙ Y X ˙ S Z X = S Y X × ˙ G A ˙ S Z X
23 20 22 eqtrd φ S A · ˙ Y + ˙ Z X = S Y X × ˙ G A ˙ S Z X