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

Metamath Proof Explorer

Theorem ldualssvsubcl

Description: Closure of vector subtraction in a dual subspace.) (Contributed by NM, 9-Mar-2015)

Ref Expression
Hypotheses ldualssvsubcl.d ⊢ 𝐷 = ( LDual ‘ 𝑊 )
ldualssvsubcl.m ⊢ − = ( -g ‘ 𝐷 )
ldualssvsubcl.s ⊢ 𝑆 = ( LSubSp ‘ 𝐷 )
ldualssvsubcl.w ⊢ ( 𝜑 → 𝑊 ∈ LMod )
ldualssvsubcl.u ⊢ ( 𝜑 → 𝑈 ∈ 𝑆 )
ldualssvsubcl.x ⊢ ( 𝜑 → 𝑋 ∈ 𝑈 )
ldualssvsubcl.y ⊢ ( 𝜑 → 𝑌 ∈ 𝑈 )
Assertion ldualssvsubcl ( 𝜑 → ( 𝑋 − 𝑌 ) ∈ 𝑈 )

Proof

Step Hyp Ref Expression
1 ldualssvsubcl.d ⊢ 𝐷 = ( LDual ‘ 𝑊 )
2 ldualssvsubcl.m ⊢ − = ( -g ‘ 𝐷 )
3 ldualssvsubcl.s ⊢ 𝑆 = ( LSubSp ‘ 𝐷 )
4 ldualssvsubcl.w ⊢ ( 𝜑 → 𝑊 ∈ LMod )
5 ldualssvsubcl.u ⊢ ( 𝜑 → 𝑈 ∈ 𝑆 )
6 ldualssvsubcl.x ⊢ ( 𝜑 → 𝑋 ∈ 𝑈 )
7 ldualssvsubcl.y ⊢ ( 𝜑 → 𝑌 ∈ 𝑈 )
8 1 4 lduallmod ⊢ ( 𝜑 → 𝐷 ∈ LMod )
9 2 3 lssvsubcl ⊢ ( ( ( 𝐷 ∈ LMod ∧ 𝑈 ∈ 𝑆 ) ∧ ( 𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑈 ) ) → ( 𝑋 − 𝑌 ) ∈ 𝑈 )
10 8 5 6 7 9 syl22anc ⊢ ( 𝜑 → ( 𝑋 − 𝑌 ) ∈ 𝑈 )