Metamath Proof Explorer

Theorem dihsmatrn

Description: The subspace sum of a closed subspace and an atom is closed. TODO: see if proof at http://math.stackexchange.com/a/1233211/50776 and Mon, 13 Apr 2015 20:44:07 -0400 email could be used instead of this and dihjat2 . (Contributed by NM, 15-Jan-2015)

Ref Expression
Hypotheses dihsmatrn.h ⊢ H = LHyp ⁡ K
dihsmatrn.i ⊢ I = DIsoH ⁡ K ⁡ W
dihsmatrn.u ⊢ U = DVecH ⁡ K ⁡ W
dihsmatrn.p ⊢ ⊕ ˙ = LSSum ⁡ U
dihsmatrn.a ⊢ A = LSAtoms ⁡ U
dihsmatrn.k ⊢ φ → K ∈ HL ∧ W ∈ H
dihsmatrn.x ⊢ φ → X ∈ ran ⁡ I
dihsmatrn.q ⊢ φ → Q ∈ A
Assertion dihsmatrn ⊢ φ → X ⊕ ˙ Q ∈ ran ⁡ I

Proof

Step Hyp Ref Expression
1 dihsmatrn.h ⊢ H = LHyp ⁡ K
2 dihsmatrn.i ⊢ I = DIsoH ⁡ K ⁡ W
3 dihsmatrn.u ⊢ U = DVecH ⁡ K ⁡ W
4 dihsmatrn.p ⊢ ⊕ ˙ = LSSum ⁡ U
5 dihsmatrn.a ⊢ A = LSAtoms ⁡ U
6 dihsmatrn.k ⊢ φ → K ∈ HL ∧ W ∈ H
7 dihsmatrn.x ⊢ φ → X ∈ ran ⁡ I
8 dihsmatrn.q ⊢ φ → Q ∈ A
9 eqid ⊢ joinH ⁡ K ⁡ W = joinH ⁡ K ⁡ W
10 1 2 9 3 4 5 6 7 8 dihjat2 ⊢ φ → X joinH ⁡ K ⁡ W Q = X ⊕ ˙ Q
11 10 eqcomd ⊢ φ → X ⊕ ˙ Q = X joinH ⁡ K ⁡ W Q
12 eqid ⊢ Base U = Base U
13 eqid ⊢ LSubSp ⁡ U = LSubSp ⁡ U
14 1 3 2 13 dihrnlss ⊢ K ∈ HL ∧ W ∈ H ∧ X ∈ ran ⁡ I → X ∈ LSubSp ⁡ U
15 6 7 14 syl2anc ⊢ φ → X ∈ LSubSp ⁡ U
16 1 3 6 dvhlmod ⊢ φ → U ∈ LMod
17 13 5 16 8 lsatlssel ⊢ φ → Q ∈ LSubSp ⁡ U
18 1 3 12 13 4 2 9 6 15 17 djhlsmcl ⊢ φ → X ⊕ ˙ Q ∈ ran ⁡ I ↔ X ⊕ ˙ Q = X joinH ⁡ K ⁡ W Q
19 11 18 mpbird ⊢ φ → X ⊕ ˙ Q ∈ ran ⁡ I