Metamath Proof Explorer

Theorem dochkrsm

Description: The subspace sum of a closed subspace and a kernel orthocomplement is closed. ( djhlsmcl can be used to convert sum to join.) (Contributed by NM, 29-Jan-2015)

Ref Expression
Hypotheses dochkrsm.h ⊢H=LHyp⁡K
dochkrsm.i ⊢I=DIsoH⁡K⁡W
dochkrsm.o ⊢⊥˙=ocH⁡K⁡W
dochkrsm.u ⊢U=DVecH⁡K⁡W
dochkrsm.p ⊢⊕˙=LSSum⁡U
dochkrsm.f ⊢F=LFnl⁡U
dochkrsm.l ⊢L=LKer⁡U
dochkrsm.k ⊢φ→K∈HL∧W∈H
dochkrsm.x ⊢φ→X∈ran⁡I
dochkrsm.g ⊢φ→G∈F
Assertion dochkrsm ⊢φ→X⊕˙⊥˙⁡L⁡G∈ran⁡I

Proof

Step Hyp Ref Expression
1 dochkrsm.h ⊢H=LHyp⁡K
2 dochkrsm.i ⊢I=DIsoH⁡K⁡W
3 dochkrsm.o ⊢⊥˙=ocH⁡K⁡W
4 dochkrsm.u ⊢U=DVecH⁡K⁡W
5 dochkrsm.p ⊢⊕˙=LSSum⁡U
6 dochkrsm.f ⊢F=LFnl⁡U
7 dochkrsm.l ⊢L=LKer⁡U
8 dochkrsm.k ⊢φ→K∈HL∧W∈H
9 dochkrsm.x ⊢φ→X∈ran⁡I
10 dochkrsm.g ⊢φ→G∈F
11 eqid ⊢LSAtoms⁡U=LSAtoms⁡U
12 8 adantr ⊢φ∧⊥˙⁡L⁡G∈LSAtoms⁡U→K∈HL∧W∈H
13 9 adantr ⊢φ∧⊥˙⁡L⁡G∈LSAtoms⁡U→X∈ran⁡I
14 simpr ⊢φ∧⊥˙⁡L⁡G∈LSAtoms⁡U→⊥˙⁡L⁡G∈LSAtoms⁡U
15 1 2 4 5 11 12 13 14 dihsmatrn ⊢φ∧⊥˙⁡L⁡G∈LSAtoms⁡U→X⊕˙⊥˙⁡L⁡G∈ran⁡I
16 oveq2 ⊢⊥˙⁡L⁡G=0U→X⊕˙⊥˙⁡L⁡G=X⊕˙0U
17 1 4 8 dvhlmod ⊢φ→U∈LMod
18 eqid ⊢LSubSp⁡U=LSubSp⁡U
19 1 4 2 18 dihrnlss ⊢K∈HL∧W∈H∧X∈ran⁡I→X∈LSubSp⁡U
20 8 9 19 syl2anc ⊢φ→X∈LSubSp⁡U
21 18 lsssubg ⊢U∈LMod∧X∈LSubSp⁡U→X∈SubGrp⁡U
22 17 20 21 syl2anc ⊢φ→X∈SubGrp⁡U
23 eqid ⊢0U=0U
24 23 5 lsm01 ⊢X∈SubGrp⁡U→X⊕˙0U=X
25 22 24 syl ⊢φ→X⊕˙0U=X
26 16 25 sylan9eqr ⊢φ∧⊥˙⁡L⁡G=0U→X⊕˙⊥˙⁡L⁡G=X
27 9 adantr ⊢φ∧⊥˙⁡L⁡G=0U→X∈ran⁡I
28 26 27 eqeltrd ⊢φ∧⊥˙⁡L⁡G=0U→X⊕˙⊥˙⁡L⁡G∈ran⁡I
29 1 3 4 23 11 6 7 8 10 dochsat0 ⊢φ→⊥˙⁡L⁡G∈LSAtoms⁡U∨⊥˙⁡L⁡G=0U
30 15 28 29 mpjaodan ⊢φ→X⊕˙⊥˙⁡L⁡G∈ran⁡I