# 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}=\mathrm{LHyp}\left({K}\right)$
lclkrlem2e.o
lclkrlem2e.u ${⊢}{U}=\mathrm{DVecH}\left({K}\right)\left({W}\right)$
lclkrlem2e.v ${⊢}{V}={\mathrm{Base}}_{{U}}$
lclkrlem2e.z
lclkrlem2e.f ${⊢}{F}=\mathrm{LFnl}\left({U}\right)$
lclkrlem2e.l ${⊢}{L}=\mathrm{LKer}\left({U}\right)$
lclkrlem2e.d ${⊢}{D}=\mathrm{LDual}\left({U}\right)$
lclkrlem2e.p
lclkrlem2e.k ${⊢}{\phi }\to \left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)$
lclkrlem2e.x
lclkrlem2e.e ${⊢}{\phi }\to {E}\in {F}$
lclkrlem2e.g ${⊢}{\phi }\to {G}\in {F}$
lclkrlem2e.le
lclkrlem2e.ne ${⊢}{\phi }\to {L}\left({E}\right)={L}\left({G}\right)$
Assertion lclkrlem2e

### Proof

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