This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ⊢ ( 𝜑 → ( 𝑋 · 𝑌 ) ∈ 𝑈 )