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 = 0 U → X ⊕ ˙ ⊥ ˙ ⁡ L ⁡ G = X ⊕ ˙ 0 U
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 ⊢ 0 U = 0 U
24 23 5 lsm01 ⊢ X ∈ SubGrp ⁡ U → X ⊕ ˙ 0 U = X
25 22 24 syl ⊢ φ → X ⊕ ˙ 0 U = X
26 16 25 sylan9eqr ⊢ φ ∧ ⊥ ˙ ⁡ L ⁡ G = 0 U → X ⊕ ˙ ⊥ ˙ ⁡ L ⁡ G = X
27 9 adantr ⊢ φ ∧ ⊥ ˙ ⁡ L ⁡ G = 0 U → X ∈ ran ⁡ I
28 26 27 eqeltrd ⊢ φ ∧ ⊥ ˙ ⁡ L ⁡ G = 0 U → X ⊕ ˙ ⊥ ˙ ⁡ L ⁡ G ∈ ran ⁡ I
29 1 3 4 23 11 6 7 8 10 dochsat0 ⊢ φ → ⊥ ˙ ⁡ L ⁡ G ∈ LSAtoms ⁡ U ∨ ⊥ ˙ ⁡ L ⁡ G = 0 U
30 15 28 29 mpjaodan ⊢ φ → X ⊕ ˙ ⊥ ˙ ⁡ L ⁡ G ∈ ran ⁡ I