# Metamath Proof Explorer

## 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}$