Metamath Proof Explorer

Theorem lclkrlem2e

Description: Lemma for lclkr . The kernel of the sum is closed when the kernels of the summands are equal and closed. (Contributed by NM, 17-Jan-2015)

Ref Expression
Hypotheses lclkrlem2e.h 
|- H = ( LHyp ` K )
lclkrlem2e.o 
|- ._|_ = ( ( ocH ` K ) ` W )
lclkrlem2e.u 
|- U = ( ( DVecH ` K ) ` W )
lclkrlem2e.v 
|- V = ( Base ` U )
lclkrlem2e.z 
|- .0. = ( 0g ` U )
lclkrlem2e.f 
|- F = ( LFnl ` U )
lclkrlem2e.l 
|- L = ( LKer ` U )
lclkrlem2e.d 
|- D = ( LDual ` U )
lclkrlem2e.p 
|- .+ = ( +g ` D )
lclkrlem2e.k 
|- ( ph -> ( K e. HL /\ W e. H ) )
lclkrlem2e.x 
|- ( ph -> X e. ( V \ { .0. } ) )
lclkrlem2e.e 
|- ( ph -> E e. F )
lclkrlem2e.g 
|- ( ph -> G e. F )
lclkrlem2e.le 
|- ( ph -> ( L ` E ) = ( ._|_ ` { X } ) )
lclkrlem2e.ne 
|- ( ph -> ( L ` E ) = ( L ` G ) )
Assertion lclkrlem2e 
|- ( ph -> ( ._|_ ` ( ._|_ ` ( L ` ( E .+ G ) ) ) ) = ( L ` ( E .+ G ) ) )

Proof

Step Hyp Ref Expression
1 lclkrlem2e.h 
 |-  H = ( LHyp ` K )
2 lclkrlem2e.o 
 |-  ._|_ = ( ( ocH ` K ) ` W )
3 lclkrlem2e.u 
 |-  U = ( ( DVecH ` K ) ` W )
4 lclkrlem2e.v 
 |-  V = ( Base ` U )
5 lclkrlem2e.z 
 |-  .0. = ( 0g ` U )
6 lclkrlem2e.f 
 |-  F = ( LFnl ` U )
7 lclkrlem2e.l 
 |-  L = ( LKer ` U )
8 lclkrlem2e.d 
 |-  D = ( LDual ` U )
9 lclkrlem2e.p 
 |-  .+ = ( +g ` D )
10 lclkrlem2e.k 
 |-  ( ph -> ( K e. HL /\ W e. H ) )
11 lclkrlem2e.x 
 |-  ( ph -> X e. ( V \ { .0. } ) )
12 lclkrlem2e.e 
 |-  ( ph -> E e. F )
13 lclkrlem2e.g 
 |-  ( ph -> G e. F )
14 lclkrlem2e.le 
 |-  ( ph -> ( L ` E ) = ( ._|_ ` { X } ) )
15 lclkrlem2e.ne 
 |-  ( ph -> ( L ` E ) = ( L ` G ) )
16 10 adantr 
 |-  ( ( ph /\ ( L ` ( E .+ G ) ) e. ( LSHyp ` U ) ) -> ( K e. HL /\ W e. H ) )
17 11 eldifad 
 |-  ( ph -> X e. V )
18 17 snssd 
 |-  ( ph -> { X } C_ V )
19 18 adantr 
 |-  ( ( ph /\ ( L ` ( E .+ G ) ) e. ( LSHyp ` U ) ) -> { X } C_ V )
20 eqid 
 |-  ( ( DIsoH ` K ) ` W ) = ( ( DIsoH ` K ) ` W )
21 1 20 3 4 2 dochcl 
 |-  ( ( ( K e. HL /\ W e. H ) /\ { X } C_ V ) -> ( ._|_ ` { X } ) e. ran ( ( DIsoH ` K ) ` W ) )
22 16 19 21 syl2anc 
 |-  ( ( ph /\ ( L ` ( E .+ G ) ) e. ( LSHyp ` U ) ) -> ( ._|_ ` { X } ) e. ran ( ( DIsoH ` K ) ` W ) )
23 1 20 2 dochoc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ._|_ ` { X } ) e. ran ( ( DIsoH ` K ) ` W ) ) -> ( ._|_ ` ( ._|_ ` ( ._|_ ` { X } ) ) ) = ( ._|_ ` { X } ) )
24 16 22 23 syl2anc 
 |-  ( ( ph /\ ( L ` ( E .+ G ) ) e. ( LSHyp ` U ) ) -> ( ._|_ ` ( ._|_ ` ( ._|_ ` { X } ) ) ) = ( ._|_ ` { X } ) )
25 14 adantr 
 |-  ( ( ph /\ ( L ` ( E .+ G ) ) e. ( LSHyp ` U ) ) -> ( L ` E ) = ( ._|_ ` { X } ) )
26 inidm 
 |-  ( ( L ` E ) i^i ( L ` E ) ) = ( L ` E )
27 15 ineq2d 
 |-  ( ph -> ( ( L ` E ) i^i ( L ` E ) ) = ( ( L ` E ) i^i ( L ` G ) ) )
28 26 27 syl5eqr 
 |-  ( ph -> ( L ` E ) = ( ( L ` E ) i^i ( L ` G ) ) )
29 1 3 10 dvhlmod 
 |-  ( ph -> U e. LMod )
30 6 7 8 9 29 12 13 lkrin 
 |-  ( ph -> ( ( L ` E ) i^i ( L ` G ) ) C_ ( L ` ( E .+ G ) ) )
31 28 30 eqsstrd 
 |-  ( ph -> ( L ` E ) C_ ( L ` ( E .+ G ) ) )
32 31 adantr 
 |-  ( ( ph /\ ( L ` ( E .+ G ) ) e. ( LSHyp ` U ) ) -> ( L ` E ) C_ ( L ` ( E .+ G ) ) )
33 eqid 
 |-  ( LSHyp ` U ) = ( LSHyp ` U )
34 1 3 10 dvhlvec 
 |-  ( ph -> U e. LVec )
35 34 adantr 
 |-  ( ( ph /\ ( L ` ( E .+ G ) ) e. ( LSHyp ` U ) ) -> U e. LVec )
36 eqid 
 |-  ( LSpan ` U ) = ( LSpan ` U )
37 1 3 2 4 36 10 18 dochocsp 
 |-  ( ph -> ( ._|_ ` ( ( LSpan ` U ) ` { X } ) ) = ( ._|_ ` { X } ) )
38 37 adantr 
 |-  ( ( ph /\ ( L ` ( E .+ G ) ) e. ( LSHyp ` U ) ) -> ( ._|_ ` ( ( LSpan ` U ) ` { X } ) ) = ( ._|_ ` { X } ) )
39 25 38 eqtr4d 
 |-  ( ( ph /\ ( L ` ( E .+ G ) ) e. ( LSHyp ` U ) ) -> ( L ` E ) = ( ._|_ ` ( ( LSpan ` U ) ` { X } ) ) )
40 eqid 
 |-  ( LSAtoms ` U ) = ( LSAtoms ` U )
41 4 36 5 40 29 11 lsatlspsn 
 |-  ( ph -> ( ( LSpan ` U ) ` { X } ) e. ( LSAtoms ` U ) )
42 41 adantr 
 |-  ( ( ph /\ ( L ` ( E .+ G ) ) e. ( LSHyp ` U ) ) -> ( ( LSpan ` U ) ` { X } ) e. ( LSAtoms ` U ) )
43 1 3 2 40 33 16 42 dochsatshp 
 |-  ( ( ph /\ ( L ` ( E .+ G ) ) e. ( LSHyp ` U ) ) -> ( ._|_ ` ( ( LSpan ` U ) ` { X } ) ) e. ( LSHyp ` U ) )
44 39 43 eqeltrd 
 |-  ( ( ph /\ ( L ` ( E .+ G ) ) e. ( LSHyp ` U ) ) -> ( L ` E ) e. ( LSHyp ` U ) )
45 simpr 
 |-  ( ( ph /\ ( L ` ( E .+ G ) ) e. ( LSHyp ` U ) ) -> ( L ` ( E .+ G ) ) e. ( LSHyp ` U ) )
46 33 35 44 45 lshpcmp 
 |-  ( ( ph /\ ( L ` ( E .+ G ) ) e. ( LSHyp ` U ) ) -> ( ( L ` E ) C_ ( L ` ( E .+ G ) ) <-> ( L ` E ) = ( L ` ( E .+ G ) ) ) )
47 32 46 mpbid 
 |-  ( ( ph /\ ( L ` ( E .+ G ) ) e. ( LSHyp ` U ) ) -> ( L ` E ) = ( L ` ( E .+ G ) ) )
48 25 47 eqtr3d 
 |-  ( ( ph /\ ( L ` ( E .+ G ) ) e. ( LSHyp ` U ) ) -> ( ._|_ ` { X } ) = ( L ` ( E .+ G ) ) )
49 48 fveq2d 
 |-  ( ( ph /\ ( L ` ( E .+ G ) ) e. ( LSHyp ` U ) ) -> ( ._|_ ` ( ._|_ ` { X } ) ) = ( ._|_ ` ( L ` ( E .+ G ) ) ) )
50 49 fveq2d 
 |-  ( ( ph /\ ( L ` ( E .+ G ) ) e. ( LSHyp ` U ) ) -> ( ._|_ ` ( ._|_ ` ( ._|_ ` { X } ) ) ) = ( ._|_ ` ( ._|_ ` ( L ` ( E .+ G ) ) ) ) )
51 24 50 48 3eqtr3d 
 |-  ( ( ph /\ ( L ` ( E .+ G ) ) e. ( LSHyp ` U ) ) -> ( ._|_ ` ( ._|_ ` ( L ` ( E .+ G ) ) ) ) = ( L ` ( E .+ G ) ) )
52 51 ex 
 |-  ( ph -> ( ( L ` ( E .+ G ) ) e. ( LSHyp ` U ) -> ( ._|_ ` ( ._|_ ` ( L ` ( E .+ G ) ) ) ) = ( L ` ( E .+ G ) ) ) )
53 1 3 2 4 10 dochoc1 
 |-  ( ph -> ( ._|_ ` ( ._|_ ` V ) ) = V )
54 2fveq3 
 |-  ( ( L ` ( E .+ G ) ) = V -> ( ._|_ ` ( ._|_ ` ( L ` ( E .+ G ) ) ) ) = ( ._|_ ` ( ._|_ ` V ) ) )
55 id 
 |-  ( ( L ` ( E .+ G ) ) = V -> ( L ` ( E .+ G ) ) = V )
56 54 55 eqeq12d 
 |-  ( ( L ` ( E .+ G ) ) = V -> ( ( ._|_ ` ( ._|_ ` ( L ` ( E .+ G ) ) ) ) = ( L ` ( E .+ G ) ) <-> ( ._|_ ` ( ._|_ ` V ) ) = V ) )
57 53 56 syl5ibrcom 
 |-  ( ph -> ( ( L ` ( E .+ G ) ) = V -> ( ._|_ ` ( ._|_ ` ( L ` ( E .+ G ) ) ) ) = ( L ` ( E .+ G ) ) ) )
58 6 8 9 29 12 13 ldualvaddcl 
 |-  ( ph -> ( E .+ G ) e. F )
59 4 33 6 7 34 58 lkrshpor 
 |-  ( ph -> ( ( L ` ( E .+ G ) ) e. ( LSHyp ` U ) \/ ( L ` ( E .+ G ) ) = V ) )
60 52 57 59 mpjaod 
 |-  ( ph -> ( ._|_ ` ( ._|_ ` ( L ` ( E .+ G ) ) ) ) = ( L ` ( E .+ G ) ) )