Mathbox for Norm Megill < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  dochkrsm Structured version   Unicode version

Theorem dochkrsm 32318
 Description: The subspace sum of a closed subspace and a kernel orthocomplement is closed. (djhlsmcl 32274 can be used to convert sum to join.) (Contributed by NM, 29-Jan-2015.)
Hypotheses
Ref Expression
dochkrsm.h
dochkrsm.i
dochkrsm.o
dochkrsm.u
dochkrsm.p
dochkrsm.f LFnl
dochkrsm.l LKer
dochkrsm.k
dochkrsm.x
dochkrsm.g
Assertion
Ref Expression
dochkrsm

Proof of Theorem dochkrsm
StepHypRef Expression
1 dochkrsm.h . . 3
2 dochkrsm.i . . 3
3 dochkrsm.u . . 3
4 dochkrsm.p . . 3
5 eqid 2438 . . 3 LSAtoms LSAtoms
6 dochkrsm.k . . . 4
76adantr 453 . . 3 LSAtoms
8 dochkrsm.x . . . 4
98adantr 453 . . 3 LSAtoms
10 simpr 449 . . 3 LSAtoms LSAtoms
111, 2, 3, 4, 5, 7, 9, 10dihsmatrn 32296 . 2 LSAtoms
12 oveq2 6091 . . . 4
131, 3, 6dvhlmod 31970 . . . . . 6
14 eqid 2438 . . . . . . . 8
151, 3, 2, 14dihrnlss 32137 . . . . . . 7
166, 8, 15syl2anc 644 . . . . . 6
1714lsssubg 16035 . . . . . 6 SubGrp
1813, 16, 17syl2anc 644 . . . . 5 SubGrp
19 eqid 2438 . . . . . 6
2019, 4lsm01 15305 . . . . 5 SubGrp
2118, 20syl 16 . . . 4
2212, 21sylan9eqr 2492 . . 3