# Metamath Proof Explorer

## Theorem lclkrlem2g

Description: Lemma for lclkr . Comparable hyperplanes are equal, so the kernel of the sum is closed. (Contributed by NM, 16-Jan-2015)

Ref Expression
Hypotheses lclkrlem2f.h ${⊢}{H}=\mathrm{LHyp}\left({K}\right)$
lclkrlem2f.o
lclkrlem2f.u ${⊢}{U}=\mathrm{DVecH}\left({K}\right)\left({W}\right)$
lclkrlem2f.v ${⊢}{V}={\mathrm{Base}}_{{U}}$
lclkrlem2f.s ${⊢}{S}=\mathrm{Scalar}\left({U}\right)$
lclkrlem2f.q ${⊢}{Q}={0}_{{S}}$
lclkrlem2f.z
lclkrlem2f.a
lclkrlem2f.n ${⊢}{N}=\mathrm{LSpan}\left({U}\right)$
lclkrlem2f.f ${⊢}{F}=\mathrm{LFnl}\left({U}\right)$
lclkrlem2f.j ${⊢}{J}=\mathrm{LSHyp}\left({U}\right)$
lclkrlem2f.l ${⊢}{L}=\mathrm{LKer}\left({U}\right)$
lclkrlem2f.d ${⊢}{D}=\mathrm{LDual}\left({U}\right)$
lclkrlem2f.p
lclkrlem2f.k ${⊢}{\phi }\to \left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)$
lclkrlem2f.b
lclkrlem2f.e ${⊢}{\phi }\to {E}\in {F}$
lclkrlem2f.g ${⊢}{\phi }\to {G}\in {F}$
lclkrlem2f.le
lclkrlem2f.lg
lclkrlem2f.kb
lclkrlem2f.nx
lclkrlem2f.x
lclkrlem2f.y
lclkrlem2f.ne ${⊢}{\phi }\to {L}\left({E}\right)\ne {L}\left({G}\right)$
lclkrlem2f.lp
Assertion lclkrlem2g

### Proof

Step Hyp Ref Expression
1 lclkrlem2f.h ${⊢}{H}=\mathrm{LHyp}\left({K}\right)$
2 lclkrlem2f.o
3 lclkrlem2f.u ${⊢}{U}=\mathrm{DVecH}\left({K}\right)\left({W}\right)$
4 lclkrlem2f.v ${⊢}{V}={\mathrm{Base}}_{{U}}$
5 lclkrlem2f.s ${⊢}{S}=\mathrm{Scalar}\left({U}\right)$
6 lclkrlem2f.q ${⊢}{Q}={0}_{{S}}$
7 lclkrlem2f.z
8 lclkrlem2f.a
9 lclkrlem2f.n ${⊢}{N}=\mathrm{LSpan}\left({U}\right)$
10 lclkrlem2f.f ${⊢}{F}=\mathrm{LFnl}\left({U}\right)$
11 lclkrlem2f.j ${⊢}{J}=\mathrm{LSHyp}\left({U}\right)$
12 lclkrlem2f.l ${⊢}{L}=\mathrm{LKer}\left({U}\right)$
13 lclkrlem2f.d ${⊢}{D}=\mathrm{LDual}\left({U}\right)$
14 lclkrlem2f.p
15 lclkrlem2f.k ${⊢}{\phi }\to \left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)$
16 lclkrlem2f.b
17 lclkrlem2f.e ${⊢}{\phi }\to {E}\in {F}$
18 lclkrlem2f.g ${⊢}{\phi }\to {G}\in {F}$
19 lclkrlem2f.le
20 lclkrlem2f.lg
21 lclkrlem2f.kb
22 lclkrlem2f.nx
23 lclkrlem2f.x
24 lclkrlem2f.y
25 lclkrlem2f.ne ${⊢}{\phi }\to {L}\left({E}\right)\ne {L}\left({G}\right)$
26 lclkrlem2f.lp
27 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 lclkrlem2f
28 1 3 15 dvhlvec ${⊢}{\phi }\to {U}\in \mathrm{LVec}$
29 19 20 ineq12d
30 29 oveq1d
31 eqid ${⊢}\mathrm{LSAtoms}\left({U}\right)=\mathrm{LSAtoms}\left({U}\right)$
32 25 19 20 3netr3d
33 1 2 3 4 7 8 9 31 15 16 23 24 32 22 11 lclkrlem2c
34 30 33 eqeltrd
35 11 28 34 26 lshpcmp
36 27 35 mpbid
37 eqid ${⊢}\mathrm{DIsoH}\left({K}\right)\left({W}\right)=\mathrm{DIsoH}\left({K}\right)\left({W}\right)$
38 1 2 3 4 7 8 9 31 15 16 23 24 32 22 37 lclkrlem2d
39 30 38 eqeltrd
40 36 39 eqeltrrd
41 1 3 37 4 dihrnss
42 15 40 41 syl2anc
43 1 37 3 4 2 15 42 dochoccl
44 40 43 mpbid