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 
|- ( ph -> ( K e. HL /\ W e. H ) )
dochkrsm.x 
|- ( ph -> X e. ran I )
dochkrsm.g 
|- ( ph -> G e. F )
Assertion dochkrsm 
|- ( ph -> ( X .(+) ( ._|_ ` ( L ` G ) ) ) e. 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 
 |-  ( ph -> ( K e. HL /\ W e. H ) )
9 dochkrsm.x 
 |-  ( ph -> X e. ran I )
10 dochkrsm.g 
 |-  ( ph -> G e. F )
11 eqid 
 |-  ( LSAtoms ` U ) = ( LSAtoms ` U )
12 8 adantr 
 |-  ( ( ph /\ ( ._|_ ` ( L ` G ) ) e. ( LSAtoms ` U ) ) -> ( K e. HL /\ W e. H ) )
13 9 adantr 
 |-  ( ( ph /\ ( ._|_ ` ( L ` G ) ) e. ( LSAtoms ` U ) ) -> X e. ran I )
14 simpr 
 |-  ( ( ph /\ ( ._|_ ` ( L ` G ) ) e. ( LSAtoms ` U ) ) -> ( ._|_ ` ( L ` G ) ) e. ( LSAtoms ` U ) )
15 1 2 4 5 11 12 13 14 dihsmatrn 
 |-  ( ( ph /\ ( ._|_ ` ( L ` G ) ) e. ( LSAtoms ` U ) ) -> ( X .(+) ( ._|_ ` ( L ` G ) ) ) e. ran I )
16 oveq2 
 |-  ( ( ._|_ ` ( L ` G ) ) = { ( 0g ` U ) } -> ( X .(+) ( ._|_ ` ( L ` G ) ) ) = ( X .(+) { ( 0g ` U ) } ) )
17 1 4 8 dvhlmod 
 |-  ( ph -> U e. LMod )
18 eqid 
 |-  ( LSubSp ` U ) = ( LSubSp ` U )
19 1 4 2 18 dihrnlss 
 |-  ( ( ( K e. HL /\ W e. H ) /\ X e. ran I ) -> X e. ( LSubSp ` U ) )
20 8 9 19 syl2anc 
 |-  ( ph -> X e. ( LSubSp ` U ) )
21 18 lsssubg 
 |-  ( ( U e. LMod /\ X e. ( LSubSp ` U ) ) -> X e. ( SubGrp ` U ) )
22 17 20 21 syl2anc 
 |-  ( ph -> X e. ( SubGrp ` U ) )
23 eqid 
 |-  ( 0g ` U ) = ( 0g ` U )
24 23 5 lsm01 
 |-  ( X e. ( SubGrp ` U ) -> ( X .(+) { ( 0g ` U ) } ) = X )
25 22 24 syl 
 |-  ( ph -> ( X .(+) { ( 0g ` U ) } ) = X )
26 16 25 sylan9eqr 
 |-  ( ( ph /\ ( ._|_ ` ( L ` G ) ) = { ( 0g ` U ) } ) -> ( X .(+) ( ._|_ ` ( L ` G ) ) ) = X )
27 9 adantr 
 |-  ( ( ph /\ ( ._|_ ` ( L ` G ) ) = { ( 0g ` U ) } ) -> X e. ran I )
28 26 27 eqeltrd 
 |-  ( ( ph /\ ( ._|_ ` ( L ` G ) ) = { ( 0g ` U ) } ) -> ( X .(+) ( ._|_ ` ( L ` G ) ) ) e. ran I )
29 1 3 4 23 11 6 7 8 10 dochsat0 
 |-  ( ph -> ( ( ._|_ ` ( L ` G ) ) e. ( LSAtoms ` U ) \/ ( ._|_ ` ( L ` G ) ) = { ( 0g ` U ) } ) )
30 15 28 29 mpjaodan 
 |-  ( ph -> ( X .(+) ( ._|_ ` ( L ` G ) ) ) e. ran I )