ldualssvscl

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

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

Metamath Proof Explorer