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 ⊢ H = LHyp ⁡ K
dihsmsnrn.u ⊢ U = DVecH ⁡ K ⁡ W
dihsmsnrn.v ⊢ V = Base U
dihsmsnrn.p ⊢ ⊕ ˙ = LSSum ⁡ U
dihsmsnrn.n ⊢ N = LSpan ⁡ U
dihsmsnrn.i ⊢ I = DIsoH ⁡ K ⁡ W
dihsmsnrn.k ⊢ φ → K ∈ HL ∧ W ∈ H
dihsmsnrn.x ⊢ φ → X ∈ V
dihsmsnrn.y ⊢ φ → Y ∈ V
Assertion dihsmsnrn ⊢ φ → N ⁡ X ⊕ ˙ N ⁡ Y ∈ ran ⁡ I

Proof

Step Hyp Ref Expression
1 dihsmsnrn.h ⊢ H = LHyp ⁡ K
2 dihsmsnrn.u ⊢ U = DVecH ⁡ K ⁡ W
3 dihsmsnrn.v ⊢ V = Base U
4 dihsmsnrn.p ⊢ ⊕ ˙ = LSSum ⁡ U
5 dihsmsnrn.n ⊢ N = LSpan ⁡ U
6 dihsmsnrn.i ⊢ I = DIsoH ⁡ K ⁡ W
7 dihsmsnrn.k ⊢ φ → K ∈ HL ∧ W ∈ H
8 dihsmsnrn.x ⊢ φ → X ∈ V
9 dihsmsnrn.y ⊢ φ → Y ∈ V
10 1 2 3 5 6 dihlsprn ⊢ K ∈ HL ∧ W ∈ H ∧ X ∈ V → N ⁡ X ∈ ran ⁡ I
11 7 8 10 syl2anc ⊢ φ → N ⁡ X ∈ ran ⁡ I
12 1 2 3 4 5 6 7 11 9 dihsmsprn ⊢ φ → N ⁡ X ⊕ ˙ N ⁡ Y ∈ ran ⁡ I