Metamath Proof Explorer


Theorem hdmapg

Description: Apply the scalar sigma function (involution) G to an inner product reverses the arguments. The inner product of X and Y is represented by ( ( SY )X ) . Line 15 in Baer p. 111, f(x,y) alpha = f(y,x). (Contributed by NM, 14-Jun-2015)

Ref Expression
Hypotheses hdmapg.h H = LHyp K
hdmapg.u U = DVecH K W
hdmapg.v V = Base U
hdmapg.s S = HDMap K W
hdmapg.g G = HGMap K W
hdmapg.k φ K HL W H
hdmapg.x φ X V
hdmapg.y φ Y V
Assertion hdmapg φ G S Y X = S X Y

Proof

Step Hyp Ref Expression
1 hdmapg.h H = LHyp K
2 hdmapg.u U = DVecH K W
3 hdmapg.v V = Base U
4 hdmapg.s S = HDMap K W
5 hdmapg.g G = HGMap K W
6 hdmapg.k φ K HL W H
7 hdmapg.x φ X V
8 hdmapg.y φ Y V
9 eqid I Base K I LTrn K W = I Base K I LTrn K W
10 eqid ocH K W = ocH K W
11 eqid + U = + U
12 eqid U = U
13 eqid Scalar U = Scalar U
14 eqid Base Scalar U = Base Scalar U
15 eqid LSSum U = LSSum U
16 eqid LSpan U = LSpan U
17 eqid Scalar U = Scalar U
18 eqid 0 Scalar U = 0 Scalar U
19 eqid + Scalar U = + Scalar U
20 1 9 10 2 3 11 12 13 14 15 16 6 7 17 18 19 4 5 8 hdmapglem7 φ G S Y X = S X Y