Description: The subspace sum of two singleton spans is closed. (Contributed by NM, 27-Feb-2015)
Ref | Expression | ||
---|---|---|---|
Hypotheses | dihsmsnrn.h | ⊢ 𝐻 = ( LHyp ‘ 𝐾 ) | |
dihsmsnrn.u | ⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 ) | ||
dihsmsnrn.v | ⊢ 𝑉 = ( Base ‘ 𝑈 ) | ||
dihsmsnrn.p | ⊢ ⊕ = ( LSSum ‘ 𝑈 ) | ||
dihsmsnrn.n | ⊢ 𝑁 = ( LSpan ‘ 𝑈 ) | ||
dihsmsnrn.i | ⊢ 𝐼 = ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) | ||
dihsmsnrn.k | ⊢ ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ) | ||
dihsmsnrn.x | ⊢ ( 𝜑 → 𝑋 ∈ 𝑉 ) | ||
dihsmsnrn.y | ⊢ ( 𝜑 → 𝑌 ∈ 𝑉 ) | ||
Assertion | dihsmsnrn | ⊢ ( 𝜑 → ( ( 𝑁 ‘ { 𝑋 } ) ⊕ ( 𝑁 ‘ { 𝑌 } ) ) ∈ ran 𝐼 ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | dihsmsnrn.h | ⊢ 𝐻 = ( LHyp ‘ 𝐾 ) | |
2 | dihsmsnrn.u | ⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 ) | |
3 | dihsmsnrn.v | ⊢ 𝑉 = ( Base ‘ 𝑈 ) | |
4 | dihsmsnrn.p | ⊢ ⊕ = ( LSSum ‘ 𝑈 ) | |
5 | dihsmsnrn.n | ⊢ 𝑁 = ( LSpan ‘ 𝑈 ) | |
6 | dihsmsnrn.i | ⊢ 𝐼 = ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) | |
7 | dihsmsnrn.k | ⊢ ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ) | |
8 | dihsmsnrn.x | ⊢ ( 𝜑 → 𝑋 ∈ 𝑉 ) | |
9 | dihsmsnrn.y | ⊢ ( 𝜑 → 𝑌 ∈ 𝑉 ) | |
10 | 1 2 3 5 6 | dihlsprn | ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑋 ∈ 𝑉 ) → ( 𝑁 ‘ { 𝑋 } ) ∈ ran 𝐼 ) |
11 | 7 8 10 | syl2anc | ⊢ ( 𝜑 → ( 𝑁 ‘ { 𝑋 } ) ∈ ran 𝐼 ) |
12 | 1 2 3 4 5 6 7 11 9 | dihsmsprn | ⊢ ( 𝜑 → ( ( 𝑁 ‘ { 𝑋 } ) ⊕ ( 𝑁 ‘ { 𝑌 } ) ) ∈ ran 𝐼 ) |