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

Metamath Proof Explorer

Theorem dihsmsnrn

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 𝐼 )

Proof

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 𝐼 )