Metamath Proof Explorer
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 |
⊢ ( 𝜑 → ( 𝑋 − 𝑌 ) ∈ 𝑈 ) |