# Metamath Proof Explorer

## Theorem lclkrlem2f

Description: Lemma for lclkr . Construct a closed hyperplane under the kernel of the sum. (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 lclkrlem2f

### 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 3 15 dvhlmod ${⊢}{\phi }\to {U}\in \mathrm{LMod}$
28 10 12 13 14 27 17 18 lkrin
29 eqid ${⊢}\mathrm{LSubSp}\left({U}\right)=\mathrm{LSubSp}\left({U}\right)$
30 29 11 27 26 lshplss
31 10 13 14 27 17 18 ldualvaddcl
32 16 eldifad ${⊢}{\phi }\to {B}\in {V}$
33 4 5 6 10 12 27 31 32 ellkr2
34 21 33 mpbird
35 29 9 27 30 34 lspsnel5a
36 29 lsssssubg ${⊢}{U}\in \mathrm{LMod}\to \mathrm{LSubSp}\left({U}\right)\subseteq \mathrm{SubGrp}\left({U}\right)$
37 27 36 syl ${⊢}{\phi }\to \mathrm{LSubSp}\left({U}\right)\subseteq \mathrm{SubGrp}\left({U}\right)$
38 10 12 29 lkrlss ${⊢}\left({U}\in \mathrm{LMod}\wedge {E}\in {F}\right)\to {L}\left({E}\right)\in \mathrm{LSubSp}\left({U}\right)$
39 27 17 38 syl2anc ${⊢}{\phi }\to {L}\left({E}\right)\in \mathrm{LSubSp}\left({U}\right)$
40 10 12 29 lkrlss ${⊢}\left({U}\in \mathrm{LMod}\wedge {G}\in {F}\right)\to {L}\left({G}\right)\in \mathrm{LSubSp}\left({U}\right)$
41 27 18 40 syl2anc ${⊢}{\phi }\to {L}\left({G}\right)\in \mathrm{LSubSp}\left({U}\right)$
42 29 lssincl ${⊢}\left({U}\in \mathrm{LMod}\wedge {L}\left({E}\right)\in \mathrm{LSubSp}\left({U}\right)\wedge {L}\left({G}\right)\in \mathrm{LSubSp}\left({U}\right)\right)\to {L}\left({E}\right)\cap {L}\left({G}\right)\in \mathrm{LSubSp}\left({U}\right)$
43 27 39 41 42 syl3anc ${⊢}{\phi }\to {L}\left({E}\right)\cap {L}\left({G}\right)\in \mathrm{LSubSp}\left({U}\right)$
44 37 43 sseldd ${⊢}{\phi }\to {L}\left({E}\right)\cap {L}\left({G}\right)\in \mathrm{SubGrp}\left({U}\right)$
45 4 29 9 lspsncl ${⊢}\left({U}\in \mathrm{LMod}\wedge {B}\in {V}\right)\to {N}\left(\left\{{B}\right\}\right)\in \mathrm{LSubSp}\left({U}\right)$
46 27 32 45 syl2anc ${⊢}{\phi }\to {N}\left(\left\{{B}\right\}\right)\in \mathrm{LSubSp}\left({U}\right)$
47 37 46 sseldd ${⊢}{\phi }\to {N}\left(\left\{{B}\right\}\right)\in \mathrm{SubGrp}\left({U}\right)$
48 37 30 sseldd
49 8 lsmlub
50 44 47 48 49 syl3anc
51 28 35 50 mpbi2and