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