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 ⊢φ→XjoinH⁡K⁡WQ=X⊕˙Q
11 10 eqcomd ⊢φ→X⊕˙Q=XjoinH⁡K⁡WQ
12 eqid ⊢BaseU=BaseU
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=XjoinH⁡K⁡WQ
19 11 18 mpbird ⊢φ→X⊕˙Q∈ran⁡I