Theorem lcdlssvscl

Description: Closure of scalar product in a closed kernel dual vector space. (Contributed by NM, 20-Mar-2015)

	Ref	Expression
Hypotheses	lcdlssvscl.h	$$⊢H=\mathrm{LHyp}\left(K\right)$$
	lcdlssvscl.u	$$⊢U=\mathrm{DVecH}\left(K\right)\left(W\right)$$
	lcdlssvscl.f	$$⊢F=\mathrm{Scalar}\left(U\right)$$
	lcdlssvscl.r	$$⊢R={\mathrm{Base}}_F$$
	lcdlssvscl.c	$$⊢C=\mathrm{LCDual}\left(K\right)\left(W\right)$$
	lcdlssvscl.v	$$⊢V={\mathrm{Base}}_C$$
	lcdlssvscl.t	$$⊢\underset{\dot{}}{·}={\cdot }_C$$
	lcdlssvscl.s	$$⊢S=\mathrm{LSubSp}\left(C\right)$$
	lcdlssvscl.k	$$⊢\phi \to \left(K\in \mathrm{HL}\wedge W\in H\right)$$
	lcdlssvscl.l	$$⊢\phi \to L\in S$$
	lcdlssvscl.x	$$⊢\phi \to X\in R$$
	lcdlssvscl.y	$$⊢\phi \to Y\in L$$
Assertion	lcdlssvscl	$$⊢\phi \to X\underset{\dot{}}{·}Y\in L$$

Proof

Step	Hyp	Ref	Expression
1		lcdlssvscl.h	$$⊢H=\mathrm{LHyp}\left(K\right)$$
2		lcdlssvscl.u	$$⊢U=\mathrm{DVecH}\left(K\right)\left(W\right)$$
3		lcdlssvscl.f	$$⊢F=\mathrm{Scalar}\left(U\right)$$
4		lcdlssvscl.r	$$⊢R={\mathrm{Base}}_F$$
5		lcdlssvscl.c	$$⊢C=\mathrm{LCDual}\left(K\right)\left(W\right)$$
6		lcdlssvscl.v	$$⊢V={\mathrm{Base}}_C$$
7		lcdlssvscl.t	$$⊢\underset{\dot{}}{·}={\cdot }_C$$
8		lcdlssvscl.s	$$⊢S=\mathrm{LSubSp}\left(C\right)$$
9		lcdlssvscl.k	$$⊢\phi \to \left(K\in \mathrm{HL}\wedge W\in H\right)$$
10		lcdlssvscl.l	$$⊢\phi \to L\in S$$
11		lcdlssvscl.x	$$⊢\phi \to X\in R$$
12		lcdlssvscl.y	$$⊢\phi \to Y\in L$$
13	1 5 9	lcdlmod	$$⊢\phi \to C\in \mathrm{LMod}$$
14		eqid	$$⊢\mathrm{Scalar}\left(C\right)=\mathrm{Scalar}\left(C\right)$$
15		eqid	$$⊢{\mathrm{Base}}_{\mathrm{Scalar}\left(C\right)}={\mathrm{Base}}_{\mathrm{Scalar}\left(C\right)}$$
16	1 2 3 4 5 14 15 9	lcdsbase	$$⊢\phi \to {\mathrm{Base}}_{\mathrm{Scalar}\left(C\right)}=R$$
17	11 16	eleqtrrd	$$⊢\phi \to X\in {\mathrm{Base}}_{\mathrm{Scalar}\left(C\right)}$$
18	14 7 15 8	lssvscl	$$⊢\left(\left(C\in \mathrm{LMod}\wedge L\in S\right)\wedge \left(X\in {\mathrm{Base}}_{\mathrm{Scalar}\left(C\right)}\wedge Y\in L\right)\right)\to X\underset{\dot{}}{·}Y\in L$$
19	13 10 17 12 18	syl22anc	$$⊢\phi \to X\underset{\dot{}}{·}Y\in L$$