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 eqtr3id
 |-  ( 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 ) ) )