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 = ( LHyp ` K )
	hdmapipcl.u	|- U = ( ( DVecH ` K ) ` W )
	hdmapipcl.v	|- V = ( Base ` U )
	hdmapipcl.r	|- R = ( Scalar ` U )
	hdmapipcl.b	|- B = ( Base ` R )
	hdmapipcl.s	|- S = ( ( HDMap ` K ) ` W )
	hdmapipcl.k	|- ( ph -> ( K e. HL /\ W e. H ) )
	hdmapipcl.x	|- ( ph -> X e. V )
	hdmapipcl.y	|- ( ph -> Y e. V )
Assertion	hdmapipcl	|- ( ph -> ( ( S ` Y ) ` X ) e. B )

Proof

Step	Hyp	Ref	Expression
1		hdmapipcl.h	|- H = ( LHyp ` K )
2		hdmapipcl.u	|- U = ( ( DVecH ` K ) ` W )
3		hdmapipcl.v	|- V = ( Base ` U )
4		hdmapipcl.r	|- R = ( Scalar ` U )
5		hdmapipcl.b	|- B = ( Base ` R )
6		hdmapipcl.s	|- S = ( ( HDMap ` K ) ` W )
7		hdmapipcl.k	|- ( ph -> ( K e. HL /\ W e. H ) )
8		hdmapipcl.x	|- ( ph -> X e. V )
9		hdmapipcl.y	|- ( ph -> Y e. V )
10		eqid	|- ( ( LCDual ` K ) ` W ) = ( ( LCDual ` K ) ` W )
11		eqid	|- ( Base ` ( ( LCDual ` K ) ` W ) ) = ( Base ` ( ( LCDual ` K ) ` W ) )
12	1 2 3 10 11 6 7 9	hdmapcl	|- ( ph -> ( S ` Y ) e. ( Base ` ( ( LCDual ` K ) ` W ) ) )
13	1 2 3 4 5 10 11 7 12 8	lcdvbasecl	|- ( ph -> ( ( S ` Y ) ` X ) e. B )