# Metamath Proof Explorer

## Theorem lkrlss

Description: The kernel of a linear functional is a subspace. ( nlelshi analog.) (Contributed by NM, 16-Apr-2014)

Ref Expression
Hypotheses lkrlss.f ${⊢}{F}=\mathrm{LFnl}\left({W}\right)$
lkrlss.k ${⊢}{K}=\mathrm{LKer}\left({W}\right)$
lkrlss.s ${⊢}{S}=\mathrm{LSubSp}\left({W}\right)$
Assertion lkrlss ${⊢}\left({W}\in \mathrm{LMod}\wedge {G}\in {F}\right)\to {K}\left({G}\right)\in {S}$

### Proof

Step Hyp Ref Expression
1 lkrlss.f ${⊢}{F}=\mathrm{LFnl}\left({W}\right)$
2 lkrlss.k ${⊢}{K}=\mathrm{LKer}\left({W}\right)$
3 lkrlss.s ${⊢}{S}=\mathrm{LSubSp}\left({W}\right)$
4 eqid ${⊢}{\mathrm{Base}}_{{W}}={\mathrm{Base}}_{{W}}$
5 eqid ${⊢}\mathrm{Scalar}\left({W}\right)=\mathrm{Scalar}\left({W}\right)$
6 eqid ${⊢}{0}_{\mathrm{Scalar}\left({W}\right)}={0}_{\mathrm{Scalar}\left({W}\right)}$
7 4 5 6 1 2 lkrval2 ${⊢}\left({W}\in \mathrm{LMod}\wedge {G}\in {F}\right)\to {K}\left({G}\right)=\left\{{x}\in {\mathrm{Base}}_{{W}}|{G}\left({x}\right)={0}_{\mathrm{Scalar}\left({W}\right)}\right\}$
8 ssrab2 ${⊢}\left\{{x}\in {\mathrm{Base}}_{{W}}|{G}\left({x}\right)={0}_{\mathrm{Scalar}\left({W}\right)}\right\}\subseteq {\mathrm{Base}}_{{W}}$
9 7 8 eqsstrdi ${⊢}\left({W}\in \mathrm{LMod}\wedge {G}\in {F}\right)\to {K}\left({G}\right)\subseteq {\mathrm{Base}}_{{W}}$
10 eqid ${⊢}{0}_{{W}}={0}_{{W}}$
11 4 10 lmod0vcl ${⊢}{W}\in \mathrm{LMod}\to {0}_{{W}}\in {\mathrm{Base}}_{{W}}$
12 11 adantr ${⊢}\left({W}\in \mathrm{LMod}\wedge {G}\in {F}\right)\to {0}_{{W}}\in {\mathrm{Base}}_{{W}}$
13 5 6 10 1 lfl0 ${⊢}\left({W}\in \mathrm{LMod}\wedge {G}\in {F}\right)\to {G}\left({0}_{{W}}\right)={0}_{\mathrm{Scalar}\left({W}\right)}$
14 4 5 6 1 2 ellkr ${⊢}\left({W}\in \mathrm{LMod}\wedge {G}\in {F}\right)\to \left({0}_{{W}}\in {K}\left({G}\right)↔\left({0}_{{W}}\in {\mathrm{Base}}_{{W}}\wedge {G}\left({0}_{{W}}\right)={0}_{\mathrm{Scalar}\left({W}\right)}\right)\right)$
15 12 13 14 mpbir2and ${⊢}\left({W}\in \mathrm{LMod}\wedge {G}\in {F}\right)\to {0}_{{W}}\in {K}\left({G}\right)$
16 15 ne0d ${⊢}\left({W}\in \mathrm{LMod}\wedge {G}\in {F}\right)\to {K}\left({G}\right)\ne \varnothing$
17 simplll ${⊢}\left(\left(\left({W}\in \mathrm{LMod}\wedge {G}\in {F}\right)\wedge {r}\in {\mathrm{Base}}_{\mathrm{Scalar}\left({W}\right)}\right)\wedge \left({x}\in {K}\left({G}\right)\wedge {y}\in {K}\left({G}\right)\right)\right)\to {W}\in \mathrm{LMod}$
18 simplr ${⊢}\left(\left(\left({W}\in \mathrm{LMod}\wedge {G}\in {F}\right)\wedge {r}\in {\mathrm{Base}}_{\mathrm{Scalar}\left({W}\right)}\right)\wedge \left({x}\in {K}\left({G}\right)\wedge {y}\in {K}\left({G}\right)\right)\right)\to {r}\in {\mathrm{Base}}_{\mathrm{Scalar}\left({W}\right)}$
19 simpllr ${⊢}\left(\left(\left({W}\in \mathrm{LMod}\wedge {G}\in {F}\right)\wedge {r}\in {\mathrm{Base}}_{\mathrm{Scalar}\left({W}\right)}\right)\wedge \left({x}\in {K}\left({G}\right)\wedge {y}\in {K}\left({G}\right)\right)\right)\to {G}\in {F}$
20 simprl ${⊢}\left(\left(\left({W}\in \mathrm{LMod}\wedge {G}\in {F}\right)\wedge {r}\in {\mathrm{Base}}_{\mathrm{Scalar}\left({W}\right)}\right)\wedge \left({x}\in {K}\left({G}\right)\wedge {y}\in {K}\left({G}\right)\right)\right)\to {x}\in {K}\left({G}\right)$
21 4 1 2 lkrcl ${⊢}\left({W}\in \mathrm{LMod}\wedge {G}\in {F}\wedge {x}\in {K}\left({G}\right)\right)\to {x}\in {\mathrm{Base}}_{{W}}$
22 17 19 20 21 syl3anc ${⊢}\left(\left(\left({W}\in \mathrm{LMod}\wedge {G}\in {F}\right)\wedge {r}\in {\mathrm{Base}}_{\mathrm{Scalar}\left({W}\right)}\right)\wedge \left({x}\in {K}\left({G}\right)\wedge {y}\in {K}\left({G}\right)\right)\right)\to {x}\in {\mathrm{Base}}_{{W}}$
23 eqid ${⊢}{\cdot }_{{W}}={\cdot }_{{W}}$
24 eqid ${⊢}{\mathrm{Base}}_{\mathrm{Scalar}\left({W}\right)}={\mathrm{Base}}_{\mathrm{Scalar}\left({W}\right)}$
25 4 5 23 24 lmodvscl ${⊢}\left({W}\in \mathrm{LMod}\wedge {r}\in {\mathrm{Base}}_{\mathrm{Scalar}\left({W}\right)}\wedge {x}\in {\mathrm{Base}}_{{W}}\right)\to {r}{\cdot }_{{W}}{x}\in {\mathrm{Base}}_{{W}}$
26 17 18 22 25 syl3anc ${⊢}\left(\left(\left({W}\in \mathrm{LMod}\wedge {G}\in {F}\right)\wedge {r}\in {\mathrm{Base}}_{\mathrm{Scalar}\left({W}\right)}\right)\wedge \left({x}\in {K}\left({G}\right)\wedge {y}\in {K}\left({G}\right)\right)\right)\to {r}{\cdot }_{{W}}{x}\in {\mathrm{Base}}_{{W}}$
27 simprr ${⊢}\left(\left(\left({W}\in \mathrm{LMod}\wedge {G}\in {F}\right)\wedge {r}\in {\mathrm{Base}}_{\mathrm{Scalar}\left({W}\right)}\right)\wedge \left({x}\in {K}\left({G}\right)\wedge {y}\in {K}\left({G}\right)\right)\right)\to {y}\in {K}\left({G}\right)$
28 4 1 2 lkrcl ${⊢}\left({W}\in \mathrm{LMod}\wedge {G}\in {F}\wedge {y}\in {K}\left({G}\right)\right)\to {y}\in {\mathrm{Base}}_{{W}}$
29 17 19 27 28 syl3anc ${⊢}\left(\left(\left({W}\in \mathrm{LMod}\wedge {G}\in {F}\right)\wedge {r}\in {\mathrm{Base}}_{\mathrm{Scalar}\left({W}\right)}\right)\wedge \left({x}\in {K}\left({G}\right)\wedge {y}\in {K}\left({G}\right)\right)\right)\to {y}\in {\mathrm{Base}}_{{W}}$
30 eqid ${⊢}{+}_{{W}}={+}_{{W}}$
31 4 30 lmodvacl ${⊢}\left({W}\in \mathrm{LMod}\wedge {r}{\cdot }_{{W}}{x}\in {\mathrm{Base}}_{{W}}\wedge {y}\in {\mathrm{Base}}_{{W}}\right)\to \left({r}{\cdot }_{{W}}{x}\right){+}_{{W}}{y}\in {\mathrm{Base}}_{{W}}$
32 17 26 29 31 syl3anc ${⊢}\left(\left(\left({W}\in \mathrm{LMod}\wedge {G}\in {F}\right)\wedge {r}\in {\mathrm{Base}}_{\mathrm{Scalar}\left({W}\right)}\right)\wedge \left({x}\in {K}\left({G}\right)\wedge {y}\in {K}\left({G}\right)\right)\right)\to \left({r}{\cdot }_{{W}}{x}\right){+}_{{W}}{y}\in {\mathrm{Base}}_{{W}}$
33 eqid ${⊢}{+}_{\mathrm{Scalar}\left({W}\right)}={+}_{\mathrm{Scalar}\left({W}\right)}$
34 eqid ${⊢}{\cdot }_{\mathrm{Scalar}\left({W}\right)}={\cdot }_{\mathrm{Scalar}\left({W}\right)}$
35 4 30 5 23 24 33 34 1 lfli ${⊢}\left({W}\in \mathrm{LMod}\wedge {G}\in {F}\wedge \left({r}\in {\mathrm{Base}}_{\mathrm{Scalar}\left({W}\right)}\wedge {x}\in {\mathrm{Base}}_{{W}}\wedge {y}\in {\mathrm{Base}}_{{W}}\right)\right)\to {G}\left(\left({r}{\cdot }_{{W}}{x}\right){+}_{{W}}{y}\right)=\left({r}{\cdot }_{\mathrm{Scalar}\left({W}\right)}{G}\left({x}\right)\right){+}_{\mathrm{Scalar}\left({W}\right)}{G}\left({y}\right)$
36 17 19 18 22 29 35 syl113anc ${⊢}\left(\left(\left({W}\in \mathrm{LMod}\wedge {G}\in {F}\right)\wedge {r}\in {\mathrm{Base}}_{\mathrm{Scalar}\left({W}\right)}\right)\wedge \left({x}\in {K}\left({G}\right)\wedge {y}\in {K}\left({G}\right)\right)\right)\to {G}\left(\left({r}{\cdot }_{{W}}{x}\right){+}_{{W}}{y}\right)=\left({r}{\cdot }_{\mathrm{Scalar}\left({W}\right)}{G}\left({x}\right)\right){+}_{\mathrm{Scalar}\left({W}\right)}{G}\left({y}\right)$
37 5 6 1 2 lkrf0 ${⊢}\left({W}\in \mathrm{LMod}\wedge {G}\in {F}\wedge {x}\in {K}\left({G}\right)\right)\to {G}\left({x}\right)={0}_{\mathrm{Scalar}\left({W}\right)}$
38 17 19 20 37 syl3anc ${⊢}\left(\left(\left({W}\in \mathrm{LMod}\wedge {G}\in {F}\right)\wedge {r}\in {\mathrm{Base}}_{\mathrm{Scalar}\left({W}\right)}\right)\wedge \left({x}\in {K}\left({G}\right)\wedge {y}\in {K}\left({G}\right)\right)\right)\to {G}\left({x}\right)={0}_{\mathrm{Scalar}\left({W}\right)}$
39 38 oveq2d ${⊢}\left(\left(\left({W}\in \mathrm{LMod}\wedge {G}\in {F}\right)\wedge {r}\in {\mathrm{Base}}_{\mathrm{Scalar}\left({W}\right)}\right)\wedge \left({x}\in {K}\left({G}\right)\wedge {y}\in {K}\left({G}\right)\right)\right)\to {r}{\cdot }_{\mathrm{Scalar}\left({W}\right)}{G}\left({x}\right)={r}{\cdot }_{\mathrm{Scalar}\left({W}\right)}{0}_{\mathrm{Scalar}\left({W}\right)}$
40 5 lmodring ${⊢}{W}\in \mathrm{LMod}\to \mathrm{Scalar}\left({W}\right)\in \mathrm{Ring}$
41 17 40 syl ${⊢}\left(\left(\left({W}\in \mathrm{LMod}\wedge {G}\in {F}\right)\wedge {r}\in {\mathrm{Base}}_{\mathrm{Scalar}\left({W}\right)}\right)\wedge \left({x}\in {K}\left({G}\right)\wedge {y}\in {K}\left({G}\right)\right)\right)\to \mathrm{Scalar}\left({W}\right)\in \mathrm{Ring}$
42 24 34 6 ringrz ${⊢}\left(\mathrm{Scalar}\left({W}\right)\in \mathrm{Ring}\wedge {r}\in {\mathrm{Base}}_{\mathrm{Scalar}\left({W}\right)}\right)\to {r}{\cdot }_{\mathrm{Scalar}\left({W}\right)}{0}_{\mathrm{Scalar}\left({W}\right)}={0}_{\mathrm{Scalar}\left({W}\right)}$
43 41 18 42 syl2anc ${⊢}\left(\left(\left({W}\in \mathrm{LMod}\wedge {G}\in {F}\right)\wedge {r}\in {\mathrm{Base}}_{\mathrm{Scalar}\left({W}\right)}\right)\wedge \left({x}\in {K}\left({G}\right)\wedge {y}\in {K}\left({G}\right)\right)\right)\to {r}{\cdot }_{\mathrm{Scalar}\left({W}\right)}{0}_{\mathrm{Scalar}\left({W}\right)}={0}_{\mathrm{Scalar}\left({W}\right)}$
44 39 43 eqtrd ${⊢}\left(\left(\left({W}\in \mathrm{LMod}\wedge {G}\in {F}\right)\wedge {r}\in {\mathrm{Base}}_{\mathrm{Scalar}\left({W}\right)}\right)\wedge \left({x}\in {K}\left({G}\right)\wedge {y}\in {K}\left({G}\right)\right)\right)\to {r}{\cdot }_{\mathrm{Scalar}\left({W}\right)}{G}\left({x}\right)={0}_{\mathrm{Scalar}\left({W}\right)}$
45 5 6 1 2 lkrf0 ${⊢}\left({W}\in \mathrm{LMod}\wedge {G}\in {F}\wedge {y}\in {K}\left({G}\right)\right)\to {G}\left({y}\right)={0}_{\mathrm{Scalar}\left({W}\right)}$
46 17 19 27 45 syl3anc ${⊢}\left(\left(\left({W}\in \mathrm{LMod}\wedge {G}\in {F}\right)\wedge {r}\in {\mathrm{Base}}_{\mathrm{Scalar}\left({W}\right)}\right)\wedge \left({x}\in {K}\left({G}\right)\wedge {y}\in {K}\left({G}\right)\right)\right)\to {G}\left({y}\right)={0}_{\mathrm{Scalar}\left({W}\right)}$
47 44 46 oveq12d ${⊢}\left(\left(\left({W}\in \mathrm{LMod}\wedge {G}\in {F}\right)\wedge {r}\in {\mathrm{Base}}_{\mathrm{Scalar}\left({W}\right)}\right)\wedge \left({x}\in {K}\left({G}\right)\wedge {y}\in {K}\left({G}\right)\right)\right)\to \left({r}{\cdot }_{\mathrm{Scalar}\left({W}\right)}{G}\left({x}\right)\right){+}_{\mathrm{Scalar}\left({W}\right)}{G}\left({y}\right)={0}_{\mathrm{Scalar}\left({W}\right)}{+}_{\mathrm{Scalar}\left({W}\right)}{0}_{\mathrm{Scalar}\left({W}\right)}$
48 5 lmodfgrp ${⊢}{W}\in \mathrm{LMod}\to \mathrm{Scalar}\left({W}\right)\in \mathrm{Grp}$
49 17 48 syl ${⊢}\left(\left(\left({W}\in \mathrm{LMod}\wedge {G}\in {F}\right)\wedge {r}\in {\mathrm{Base}}_{\mathrm{Scalar}\left({W}\right)}\right)\wedge \left({x}\in {K}\left({G}\right)\wedge {y}\in {K}\left({G}\right)\right)\right)\to \mathrm{Scalar}\left({W}\right)\in \mathrm{Grp}$
50 24 6 grpidcl ${⊢}\mathrm{Scalar}\left({W}\right)\in \mathrm{Grp}\to {0}_{\mathrm{Scalar}\left({W}\right)}\in {\mathrm{Base}}_{\mathrm{Scalar}\left({W}\right)}$
51 24 33 6 grplid ${⊢}\left(\mathrm{Scalar}\left({W}\right)\in \mathrm{Grp}\wedge {0}_{\mathrm{Scalar}\left({W}\right)}\in {\mathrm{Base}}_{\mathrm{Scalar}\left({W}\right)}\right)\to {0}_{\mathrm{Scalar}\left({W}\right)}{+}_{\mathrm{Scalar}\left({W}\right)}{0}_{\mathrm{Scalar}\left({W}\right)}={0}_{\mathrm{Scalar}\left({W}\right)}$
52 49 50 51 syl2anc2 ${⊢}\left(\left(\left({W}\in \mathrm{LMod}\wedge {G}\in {F}\right)\wedge {r}\in {\mathrm{Base}}_{\mathrm{Scalar}\left({W}\right)}\right)\wedge \left({x}\in {K}\left({G}\right)\wedge {y}\in {K}\left({G}\right)\right)\right)\to {0}_{\mathrm{Scalar}\left({W}\right)}{+}_{\mathrm{Scalar}\left({W}\right)}{0}_{\mathrm{Scalar}\left({W}\right)}={0}_{\mathrm{Scalar}\left({W}\right)}$
53 36 47 52 3eqtrd ${⊢}\left(\left(\left({W}\in \mathrm{LMod}\wedge {G}\in {F}\right)\wedge {r}\in {\mathrm{Base}}_{\mathrm{Scalar}\left({W}\right)}\right)\wedge \left({x}\in {K}\left({G}\right)\wedge {y}\in {K}\left({G}\right)\right)\right)\to {G}\left(\left({r}{\cdot }_{{W}}{x}\right){+}_{{W}}{y}\right)={0}_{\mathrm{Scalar}\left({W}\right)}$
54 4 5 6 1 2 ellkr ${⊢}\left({W}\in \mathrm{LMod}\wedge {G}\in {F}\right)\to \left(\left({r}{\cdot }_{{W}}{x}\right){+}_{{W}}{y}\in {K}\left({G}\right)↔\left(\left({r}{\cdot }_{{W}}{x}\right){+}_{{W}}{y}\in {\mathrm{Base}}_{{W}}\wedge {G}\left(\left({r}{\cdot }_{{W}}{x}\right){+}_{{W}}{y}\right)={0}_{\mathrm{Scalar}\left({W}\right)}\right)\right)$
55 54 ad2antrr ${⊢}\left(\left(\left({W}\in \mathrm{LMod}\wedge {G}\in {F}\right)\wedge {r}\in {\mathrm{Base}}_{\mathrm{Scalar}\left({W}\right)}\right)\wedge \left({x}\in {K}\left({G}\right)\wedge {y}\in {K}\left({G}\right)\right)\right)\to \left(\left({r}{\cdot }_{{W}}{x}\right){+}_{{W}}{y}\in {K}\left({G}\right)↔\left(\left({r}{\cdot }_{{W}}{x}\right){+}_{{W}}{y}\in {\mathrm{Base}}_{{W}}\wedge {G}\left(\left({r}{\cdot }_{{W}}{x}\right){+}_{{W}}{y}\right)={0}_{\mathrm{Scalar}\left({W}\right)}\right)\right)$
56 32 53 55 mpbir2and ${⊢}\left(\left(\left({W}\in \mathrm{LMod}\wedge {G}\in {F}\right)\wedge {r}\in {\mathrm{Base}}_{\mathrm{Scalar}\left({W}\right)}\right)\wedge \left({x}\in {K}\left({G}\right)\wedge {y}\in {K}\left({G}\right)\right)\right)\to \left({r}{\cdot }_{{W}}{x}\right){+}_{{W}}{y}\in {K}\left({G}\right)$
57 56 ralrimivva ${⊢}\left(\left({W}\in \mathrm{LMod}\wedge {G}\in {F}\right)\wedge {r}\in {\mathrm{Base}}_{\mathrm{Scalar}\left({W}\right)}\right)\to \forall {x}\in {K}\left({G}\right)\phantom{\rule{.4em}{0ex}}\forall {y}\in {K}\left({G}\right)\phantom{\rule{.4em}{0ex}}\left({r}{\cdot }_{{W}}{x}\right){+}_{{W}}{y}\in {K}\left({G}\right)$
58 57 ralrimiva ${⊢}\left({W}\in \mathrm{LMod}\wedge {G}\in {F}\right)\to \forall {r}\in {\mathrm{Base}}_{\mathrm{Scalar}\left({W}\right)}\phantom{\rule{.4em}{0ex}}\forall {x}\in {K}\left({G}\right)\phantom{\rule{.4em}{0ex}}\forall {y}\in {K}\left({G}\right)\phantom{\rule{.4em}{0ex}}\left({r}{\cdot }_{{W}}{x}\right){+}_{{W}}{y}\in {K}\left({G}\right)$
59 5 24 4 30 23 3 islss ${⊢}{K}\left({G}\right)\in {S}↔\left({K}\left({G}\right)\subseteq {\mathrm{Base}}_{{W}}\wedge {K}\left({G}\right)\ne \varnothing \wedge \forall {r}\in {\mathrm{Base}}_{\mathrm{Scalar}\left({W}\right)}\phantom{\rule{.4em}{0ex}}\forall {x}\in {K}\left({G}\right)\phantom{\rule{.4em}{0ex}}\forall {y}\in {K}\left({G}\right)\phantom{\rule{.4em}{0ex}}\left({r}{\cdot }_{{W}}{x}\right){+}_{{W}}{y}\in {K}\left({G}\right)\right)$
60 9 16 58 59 syl3anbrc ${⊢}\left({W}\in \mathrm{LMod}\wedge {G}\in {F}\right)\to {K}\left({G}\right)\in {S}$