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=\mathrm{LHyp}\left(K\right)$$
	hdmapg.u	$$⊢U=\mathrm{DVecH}\left(K\right)\left(W\right)$$
	hdmapg.v	$$⊢V={\mathrm{Base}}_U$$
	hdmapg.s	$$⊢S=\mathrm{HDMap}\left(K\right)\left(W\right)$$
	hdmapg.g	$$⊢G=\mathrm{HGMap}\left(K\right)\left(W\right)$$
	hdmapg.k	$$⊢\phi \to \left(K\in \mathrm{HL}\wedge W\in H\right)$$
	hdmapg.x	$$⊢\phi \to X\in V$$
	hdmapg.y	$$⊢\phi \to Y\in V$$
Assertion	hdmapg	$$⊢\phi \to G\left(S\left(Y\right)\left(X\right)\right)=S\left(X\right)\left(Y\right)$$

Proof

Step	Hyp	Ref	Expression
1		hdmapg.h	$$⊢H=\mathrm{LHyp}\left(K\right)$$
2		hdmapg.u	$$⊢U=\mathrm{DVecH}\left(K\right)\left(W\right)$$
3		hdmapg.v	$$⊢V={\mathrm{Base}}_U$$
4		hdmapg.s	$$⊢S=\mathrm{HDMap}\left(K\right)\left(W\right)$$
5		hdmapg.g	$$⊢G=\mathrm{HGMap}\left(K\right)\left(W\right)$$
6		hdmapg.k	$$⊢\phi \to \left(K\in \mathrm{HL}\wedge W\in H\right)$$
7		hdmapg.x	$$⊢\phi \to X\in V$$
8		hdmapg.y	$$⊢\phi \to Y\in V$$
9		eqid	$$⊢⟨{\mathrm{I}\upharpoonright }_{{\mathrm{Base}}_K},{\mathrm{I}\upharpoonright }_{\mathrm{LTrn}\left(K\right)\left(W\right)}⟩=⟨{\mathrm{I}\upharpoonright }_{{\mathrm{Base}}_K},{\mathrm{I}\upharpoonright }_{\mathrm{LTrn}\left(K\right)\left(W\right)}⟩$$
10		eqid	$$⊢\mathrm{ocH}\left(K\right)\left(W\right)=\mathrm{ocH}\left(K\right)\left(W\right)$$
11		eqid	$$⊢{+}_U={+}_U$$
12		eqid	$$⊢{\cdot }_U={\cdot }_U$$
13		eqid	$$⊢\mathrm{Scalar}\left(U\right)=\mathrm{Scalar}\left(U\right)$$
14		eqid	$$⊢{\mathrm{Base}}_{\mathrm{Scalar}\left(U\right)}={\mathrm{Base}}_{\mathrm{Scalar}\left(U\right)}$$
15		eqid	$$⊢\mathrm{LSSum}\left(U\right)=\mathrm{LSSum}\left(U\right)$$
16		eqid	$$⊢\mathrm{LSpan}\left(U\right)=\mathrm{LSpan}\left(U\right)$$
17		eqid	$$⊢{\cdot }_{\mathrm{Scalar}\left(U\right)}={\cdot }_{\mathrm{Scalar}\left(U\right)}$$
18		eqid	$$⊢0_{\mathrm{Scalar}\left(U\right)}=0_{\mathrm{Scalar}\left(U\right)}$$
19		eqid	$$⊢{+}_{\mathrm{Scalar}\left(U\right)}={+}_{\mathrm{Scalar}\left(U\right)}$$
20	1 9 10 2 3 11 12 13 14 15 16 6 7 17 18 19 4 5 8	hdmapglem7	$$⊢\phi \to G\left(S\left(Y\right)\left(X\right)\right)=S\left(X\right)\left(Y\right)$$