Theorem ldualssvscl

Description: Closure of scalar product in a dual subspace.) (Contributed by NM, 5-Feb-2015)

	Ref	Expression
Hypotheses	ldualssvscl.r	$$⊢R=\mathrm{Scalar}\left(W\right)$$
	ldualssvscl.k	$$⊢K={\mathrm{Base}}_R$$
	ldualssvscl.d	$$⊢D=\mathrm{LDual}\left(W\right)$$
	ldualssvscl.t	$$⊢\underset{\dot{}}{·}={\cdot }_D$$
	ldualssvscl.s	$$⊢S=\mathrm{LSubSp}\left(D\right)$$
	ldualssvscl.w	$$⊢\phi \to W\in \mathrm{LMod}$$
	ldualssvscl.u	$$⊢\phi \to U\in S$$
	ldualssvscl.x	$$⊢\phi \to X\in K$$
	ldualssvscl.y	$$⊢\phi \to Y\in U$$
Assertion	ldualssvscl	$$⊢\phi \to X\underset{\dot{}}{·}Y\in U$$

Proof

Step	Hyp	Ref	Expression
1		ldualssvscl.r	$$⊢R=\mathrm{Scalar}\left(W\right)$$
2		ldualssvscl.k	$$⊢K={\mathrm{Base}}_R$$
3		ldualssvscl.d	$$⊢D=\mathrm{LDual}\left(W\right)$$
4		ldualssvscl.t	$$⊢\underset{\dot{}}{·}={\cdot }_D$$
5		ldualssvscl.s	$$⊢S=\mathrm{LSubSp}\left(D\right)$$
6		ldualssvscl.w	$$⊢\phi \to W\in \mathrm{LMod}$$
7		ldualssvscl.u	$$⊢\phi \to U\in S$$
8		ldualssvscl.x	$$⊢\phi \to X\in K$$
9		ldualssvscl.y	$$⊢\phi \to Y\in U$$
10	3 6	lduallmod	$$⊢\phi \to D\in \mathrm{LMod}$$
11		eqid	$$⊢\mathrm{Scalar}\left(D\right)=\mathrm{Scalar}\left(D\right)$$
12		eqid	$$⊢{\mathrm{Base}}_{\mathrm{Scalar}\left(D\right)}={\mathrm{Base}}_{\mathrm{Scalar}\left(D\right)}$$
13	1 2 3 11 12 6	ldualsbase	$$⊢\phi \to {\mathrm{Base}}_{\mathrm{Scalar}\left(D\right)}=K$$
14	8 13	eleqtrrd	$$⊢\phi \to X\in {\mathrm{Base}}_{\mathrm{Scalar}\left(D\right)}$$
15	11 4 12 5	lssvscl	$$⊢\left(\left(D\in \mathrm{LMod}\wedge U\in S\right)\wedge \left(X\in {\mathrm{Base}}_{\mathrm{Scalar}\left(D\right)}\wedge Y\in U\right)\right)\to X\underset{\dot{}}{·}Y\in U$$
16	10 7 14 9 15	syl22anc	$$⊢\phi \to X\underset{\dot{}}{·}Y\in U$$