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	⊢ 𝐻 = ( LHyp ‘ 𝐾 )
	hdmapipcl.u	⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
	hdmapipcl.v	⊢ 𝑉 = ( Base ‘ 𝑈 )
	hdmapipcl.r	⊢ 𝑅 = ( Scalar ‘ 𝑈 )
	hdmapipcl.b	⊢ 𝐵 = ( Base ‘ 𝑅 )
	hdmapipcl.s	⊢ 𝑆 = ( ( HDMap ‘ 𝐾 ) ‘ 𝑊 )
	hdmapipcl.k	⊢ ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
	hdmapipcl.x	⊢ ( 𝜑 → 𝑋 ∈ 𝑉 )
	hdmapipcl.y	⊢ ( 𝜑 → 𝑌 ∈ 𝑉 )
Assertion	hdmapipcl	⊢ ( 𝜑 → ( ( 𝑆 ‘ 𝑌 ) ‘ 𝑋 ) ∈ 𝐵 )

Proof

Step	Hyp	Ref	Expression
1		hdmapipcl.h	⊢ 𝐻 = ( LHyp ‘ 𝐾 )
2		hdmapipcl.u	⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
3		hdmapipcl.v	⊢ 𝑉 = ( Base ‘ 𝑈 )
4		hdmapipcl.r	⊢ 𝑅 = ( Scalar ‘ 𝑈 )
5		hdmapipcl.b	⊢ 𝐵 = ( Base ‘ 𝑅 )
6		hdmapipcl.s	⊢ 𝑆 = ( ( HDMap ‘ 𝐾 ) ‘ 𝑊 )
7		hdmapipcl.k	⊢ ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
8		hdmapipcl.x	⊢ ( 𝜑 → 𝑋 ∈ 𝑉 )
9		hdmapipcl.y	⊢ ( 𝜑 → 𝑌 ∈ 𝑉 )
10		eqid	⊢ ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 ) = ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 )
11		eqid	⊢ ( Base ‘ ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 ) ) = ( Base ‘ ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 ) )
12	1 2 3 10 11 6 7 9	hdmapcl	⊢ ( 𝜑 → ( 𝑆 ‘ 𝑌 ) ∈ ( Base ‘ ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 ) ) )
13	1 2 3 4 5 10 11 7 12 8	lcdvbasecl	⊢ ( 𝜑 → ( ( 𝑆 ‘ 𝑌 ) ‘ 𝑋 ) ∈ 𝐵 )