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