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