Theorem hdmapipcl

Description: The inner product (Hermitian form) ( X , Y ) will be defined as ( ( SY )X ) . Show closure. (Contributed by NM, 7-Jun-2015)

	Ref	Expression
Hypotheses	hdmapipcl.h	$$⊢H=\mathrm{LHyp}\left(K\right)$$
	hdmapipcl.u	$$⊢U=\mathrm{DVecH}\left(K\right)\left(W\right)$$
	hdmapipcl.v	$$⊢V={\mathrm{Base}}_U$$
	hdmapipcl.r	$$⊢R=\mathrm{Scalar}\left(U\right)$$
	hdmapipcl.b	$$⊢B={\mathrm{Base}}_R$$
	hdmapipcl.s	$$⊢S=\mathrm{HDMap}\left(K\right)\left(W\right)$$
	hdmapipcl.k	$$⊢\phi \to \left(K\in \mathrm{HL}\wedge W\in H\right)$$
	hdmapipcl.x	$$⊢\phi \to X\in V$$
	hdmapipcl.y	$$⊢\phi \to Y\in V$$
Assertion	hdmapipcl	$$⊢\phi \to S\left(Y\right)\left(X\right)\in B$$

Proof

Step	Hyp	Ref	Expression
1		hdmapipcl.h	$$⊢H=\mathrm{LHyp}\left(K\right)$$
2		hdmapipcl.u	$$⊢U=\mathrm{DVecH}\left(K\right)\left(W\right)$$
3		hdmapipcl.v	$$⊢V={\mathrm{Base}}_U$$
4		hdmapipcl.r	$$⊢R=\mathrm{Scalar}\left(U\right)$$
5		hdmapipcl.b	$$⊢B={\mathrm{Base}}_R$$
6		hdmapipcl.s	$$⊢S=\mathrm{HDMap}\left(K\right)\left(W\right)$$
7		hdmapipcl.k	$$⊢\phi \to \left(K\in \mathrm{HL}\wedge W\in H\right)$$
8		hdmapipcl.x	$$⊢\phi \to X\in V$$
9		hdmapipcl.y	$$⊢\phi \to Y\in V$$
10		eqid	$$⊢\mathrm{LCDual}\left(K\right)\left(W\right)=\mathrm{LCDual}\left(K\right)\left(W\right)$$
11		eqid	$$⊢{\mathrm{Base}}_{\mathrm{LCDual}\left(K\right)\left(W\right)}={\mathrm{Base}}_{\mathrm{LCDual}\left(K\right)\left(W\right)}$$
12	1 2 3 10 11 6 7 9	hdmapcl	$$⊢\phi \to S\left(Y\right)\in {\mathrm{Base}}_{\mathrm{LCDual}\left(K\right)\left(W\right)}$$
13	1 2 3 4 5 10 11 7 12 8	lcdvbasecl	$$⊢\phi \to S\left(Y\right)\left(X\right)\in B$$