Theorem ldualssvscl

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

	Ref	Expression
Hypotheses	ldualssvscl.r	⊢ 𝑅 = ( Scalar ‘ 𝑊 )
	ldualssvscl.k	⊢ 𝐾 = ( Base ‘ 𝑅 )
	ldualssvscl.d	⊢ 𝐷 = ( LDual ‘ 𝑊 )
	ldualssvscl.t	⊢ · = ( ·𝑠 ‘ 𝐷 )
	ldualssvscl.s	⊢ 𝑆 = ( LSubSp ‘ 𝐷 )
	ldualssvscl.w	⊢ ( 𝜑 → 𝑊 ∈ LMod )
	ldualssvscl.u	⊢ ( 𝜑 → 𝑈 ∈ 𝑆 )
	ldualssvscl.x	⊢ ( 𝜑 → 𝑋 ∈ 𝐾 )
	ldualssvscl.y	⊢ ( 𝜑 → 𝑌 ∈ 𝑈 )
Assertion	ldualssvscl	⊢ ( 𝜑 → ( 𝑋 · 𝑌 ) ∈ 𝑈 )

Proof

Step	Hyp	Ref	Expression
1		ldualssvscl.r	⊢ 𝑅 = ( Scalar ‘ 𝑊 )
2		ldualssvscl.k	⊢ 𝐾 = ( Base ‘ 𝑅 )
3		ldualssvscl.d	⊢ 𝐷 = ( LDual ‘ 𝑊 )
4		ldualssvscl.t	⊢ · = ( ·𝑠 ‘ 𝐷 )
5		ldualssvscl.s	⊢ 𝑆 = ( LSubSp ‘ 𝐷 )
6		ldualssvscl.w	⊢ ( 𝜑 → 𝑊 ∈ LMod )
7		ldualssvscl.u	⊢ ( 𝜑 → 𝑈 ∈ 𝑆 )
8		ldualssvscl.x	⊢ ( 𝜑 → 𝑋 ∈ 𝐾 )
9		ldualssvscl.y	⊢ ( 𝜑 → 𝑌 ∈ 𝑈 )
10	3 6	lduallmod	⊢ ( 𝜑 → 𝐷 ∈ LMod )
11		eqid	⊢ ( Scalar ‘ 𝐷 ) = ( Scalar ‘ 𝐷 )
12		eqid	⊢ ( Base ‘ ( Scalar ‘ 𝐷 ) ) = ( Base ‘ ( Scalar ‘ 𝐷 ) )
13	1 2 3 11 12 6	ldualsbase	⊢ ( 𝜑 → ( Base ‘ ( Scalar ‘ 𝐷 ) ) = 𝐾 )
14	8 13	eleqtrrd	⊢ ( 𝜑 → 𝑋 ∈ ( Base ‘ ( Scalar ‘ 𝐷 ) ) )
15	11 4 12 5	lssvscl	⊢ ( ( ( 𝐷 ∈ LMod ∧ 𝑈 ∈ 𝑆 ) ∧ ( 𝑋 ∈ ( Base ‘ ( Scalar ‘ 𝐷 ) ) ∧ 𝑌 ∈ 𝑈 ) ) → ( 𝑋 · 𝑌 ) ∈ 𝑈 )
16	10 7 14 9 15	syl22anc	⊢ ( 𝜑 → ( 𝑋 · 𝑌 ) ∈ 𝑈 )