Metamath Proof Explorer


Theorem dihsmsprn

Description: Subspace sum of a closed subspace and the span of a singleton. (Contributed by NM, 17-Jan-2015)

Ref Expression
Hypotheses dihsmsprn.h H = LHyp K
dihsmsprn.u U = DVecH K W
dihsmsprn.v V = Base U
dihsmsprn.p ˙ = LSSum U
dihsmsprn.n N = LSpan U
dihsmsprn.i I = DIsoH K W
dihsmsprn.k φ K HL W H
dihsmsprn.x φ X ran I
dihsmsprn.t φ T V
Assertion dihsmsprn φ X ˙ N T ran I

Proof

Step Hyp Ref Expression
1 dihsmsprn.h H = LHyp K
2 dihsmsprn.u U = DVecH K W
3 dihsmsprn.v V = Base U
4 dihsmsprn.p ˙ = LSSum U
5 dihsmsprn.n N = LSpan U
6 dihsmsprn.i I = DIsoH K W
7 dihsmsprn.k φ K HL W H
8 dihsmsprn.x φ X ran I
9 dihsmsprn.t φ T V
10 eqid joinH K W = joinH K W
11 1 2 3 4 5 6 10 7 8 9 dihjat1 φ X joinH K W N T = X ˙ N T
12 1 2 6 3 dihrnss K HL W H X ran I X V
13 7 8 12 syl2anc φ X V
14 1 2 7 dvhlmod φ U LMod
15 9 snssd φ T V
16 3 5 lspssv U LMod T V N T V
17 14 15 16 syl2anc φ N T V
18 1 6 2 3 10 djhcl K HL W H X V N T V X joinH K W N T ran I
19 7 13 17 18 syl12anc φ X joinH K W N T ran I
20 11 19 eqeltrrd φ X ˙ N T ran I