Metamath Proof Explorer


Theorem hdmaplnm1

Description: Multiplicative property of first (inner product) argument. (Contributed by NM, 11-Jun-2015)

Ref Expression
Hypotheses hdmaplnm1.h H = LHyp K
hdmaplnm1.u U = DVecH K W
hdmaplnm1.v V = Base U
hdmaplnm1.t · ˙ = U
hdmaplnm1.r R = Scalar U
hdmaplnm1.b B = Base R
hdmaplnm1.m × ˙ = R
hdmaplnm1.s S = HDMap K W
hdmaplnm1.k φ K HL W H
hdmaplnm1.x φ X V
hdmaplnm1.y φ Y V
hdmaplnm1.a φ A B
Assertion hdmaplnm1 φ S Y A · ˙ X = A × ˙ S Y X

Proof

Step Hyp Ref Expression
1 hdmaplnm1.h H = LHyp K
2 hdmaplnm1.u U = DVecH K W
3 hdmaplnm1.v V = Base U
4 hdmaplnm1.t · ˙ = U
5 hdmaplnm1.r R = Scalar U
6 hdmaplnm1.b B = Base R
7 hdmaplnm1.m × ˙ = R
8 hdmaplnm1.s S = HDMap K W
9 hdmaplnm1.k φ K HL W H
10 hdmaplnm1.x φ X V
11 hdmaplnm1.y φ Y V
12 hdmaplnm1.a φ A B
13 1 2 9 dvhlmod φ U LMod
14 eqid LCDual K W = LCDual K W
15 eqid Base LCDual K W = Base LCDual K W
16 eqid LFnl U = LFnl U
17 1 2 3 14 15 8 9 11 hdmapcl φ S Y Base LCDual K W
18 1 14 15 2 16 9 17 lcdvbaselfl φ S Y LFnl U
19 5 6 7 3 4 16 lflmul U LMod S Y LFnl U A B X V S Y A · ˙ X = A × ˙ S Y X
20 13 18 12 10 19 syl112anc φ S Y A · ˙ X = A × ˙ S Y X