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=LFnl⁡W
lkrlss.k ⊢K=LKer⁡W
lkrlss.s ⊢S=LSubSp⁡W
Assertion lkrlss ⊢W∈LMod∧G∈F→K⁡G∈S

Proof

Step Hyp Ref Expression
1 lkrlss.f ⊢F=LFnl⁡W
2 lkrlss.k ⊢K=LKer⁡W
3 lkrlss.s ⊢S=LSubSp⁡W
4 eqid ⊢BaseW=BaseW
5 eqid ⊢Scalar⁡W=Scalar⁡W
6 eqid ⊢0Scalar⁡W=0Scalar⁡W
7 4 5 6 1 2 lkrval2 ⊢W∈LMod∧G∈F→K⁡G=x∈BaseW|G⁡x=0Scalar⁡W
8 ssrab2 ⊢x∈BaseW|G⁡x=0Scalar⁡W⊆BaseW
9 7 8 eqsstrdi ⊢W∈LMod∧G∈F→K⁡G⊆BaseW
10 eqid ⊢0W=0W
11 4 10 lmod0vcl ⊢W∈LMod→0W∈BaseW
12 11 adantr ⊢W∈LMod∧G∈F→0W∈BaseW
13 5 6 10 1 lfl0 ⊢W∈LMod∧G∈F→G⁡0W=0Scalar⁡W
14 4 5 6 1 2 ellkr ⊢W∈LMod∧G∈F→0W∈K⁡G↔0W∈BaseW∧G⁡0W=0Scalar⁡W
15 12 13 14 mpbir2and ⊢W∈LMod∧G∈F→0W∈K⁡G
16 15 ne0d ⊢W∈LMod∧G∈F→K⁡G≠∅
17 simplll ⊢W∈LMod∧G∈F∧r∈BaseScalar⁡W∧x∈K⁡G∧y∈K⁡G→W∈LMod
18 simplr ⊢W∈LMod∧G∈F∧r∈BaseScalar⁡W∧x∈K⁡G∧y∈K⁡G→r∈BaseScalar⁡W
19 simpllr ⊢W∈LMod∧G∈F∧r∈BaseScalar⁡W∧x∈K⁡G∧y∈K⁡G→G∈F
20 simprl ⊢W∈LMod∧G∈F∧r∈BaseScalar⁡W∧x∈K⁡G∧y∈K⁡G→x∈K⁡G
21 4 1 2 lkrcl ⊢W∈LMod∧G∈F∧x∈K⁡G→x∈BaseW
22 17 19 20 21 syl3anc ⊢W∈LMod∧G∈F∧r∈BaseScalar⁡W∧x∈K⁡G∧y∈K⁡G→x∈BaseW
23 eqid ⊢⋅W=⋅W
24 eqid ⊢BaseScalar⁡W=BaseScalar⁡W
25 4 5 23 24 lmodvscl ⊢W∈LMod∧r∈BaseScalar⁡W∧x∈BaseW→r⋅Wx∈BaseW
26 17 18 22 25 syl3anc ⊢W∈LMod∧G∈F∧r∈BaseScalar⁡W∧x∈K⁡G∧y∈K⁡G→r⋅Wx∈BaseW
27 simprr ⊢W∈LMod∧G∈F∧r∈BaseScalar⁡W∧x∈K⁡G∧y∈K⁡G→y∈K⁡G
28 4 1 2 lkrcl ⊢W∈LMod∧G∈F∧y∈K⁡G→y∈BaseW
29 17 19 27 28 syl3anc ⊢W∈LMod∧G∈F∧r∈BaseScalar⁡W∧x∈K⁡G∧y∈K⁡G→y∈BaseW
30 eqid ⊢+W=+W
31 4 30 lmodvacl ⊢W∈LMod∧r⋅Wx∈BaseW∧y∈BaseW→r⋅Wx+Wy∈BaseW
32 17 26 29 31 syl3anc ⊢W∈LMod∧G∈F∧r∈BaseScalar⁡W∧x∈K⁡G∧y∈K⁡G→r⋅Wx+Wy∈BaseW
33 eqid ⊢+Scalar⁡W=+Scalar⁡W
34 eqid ⊢⋅Scalar⁡W=⋅Scalar⁡W
35 4 30 5 23 24 33 34 1 lfli ⊢W∈LMod∧G∈F∧r∈BaseScalar⁡W∧x∈BaseW∧y∈BaseW→G⁡r⋅Wx+Wy=r⋅Scalar⁡WG⁡x+Scalar⁡WG⁡y
36 17 19 18 22 29 35 syl113anc ⊢W∈LMod∧G∈F∧r∈BaseScalar⁡W∧x∈K⁡G∧y∈K⁡G→G⁡r⋅Wx+Wy=r⋅Scalar⁡WG⁡x+Scalar⁡WG⁡y
37 5 6 1 2 lkrf0 ⊢W∈LMod∧G∈F∧x∈K⁡G→G⁡x=0Scalar⁡W
38 17 19 20 37 syl3anc ⊢W∈LMod∧G∈F∧r∈BaseScalar⁡W∧x∈K⁡G∧y∈K⁡G→G⁡x=0Scalar⁡W
39 38 oveq2d ⊢W∈LMod∧G∈F∧r∈BaseScalar⁡W∧x∈K⁡G∧y∈K⁡G→r⋅Scalar⁡WG⁡x=r⋅Scalar⁡W0Scalar⁡W
40 5 lmodring ⊢W∈LMod→Scalar⁡W∈Ring
41 17 40 syl ⊢W∈LMod∧G∈F∧r∈BaseScalar⁡W∧x∈K⁡G∧y∈K⁡G→Scalar⁡W∈Ring
42 24 34 6 ringrz ⊢Scalar⁡W∈Ring∧r∈BaseScalar⁡W→r⋅Scalar⁡W0Scalar⁡W=0Scalar⁡W
43 41 18 42 syl2anc ⊢W∈LMod∧G∈F∧r∈BaseScalar⁡W∧x∈K⁡G∧y∈K⁡G→r⋅Scalar⁡W0Scalar⁡W=0Scalar⁡W
44 39 43 eqtrd ⊢W∈LMod∧G∈F∧r∈BaseScalar⁡W∧x∈K⁡G∧y∈K⁡G→r⋅Scalar⁡WG⁡x=0Scalar⁡W
45 5 6 1 2 lkrf0 ⊢W∈LMod∧G∈F∧y∈K⁡G→G⁡y=0Scalar⁡W
46 17 19 27 45 syl3anc ⊢W∈LMod∧G∈F∧r∈BaseScalar⁡W∧x∈K⁡G∧y∈K⁡G→G⁡y=0Scalar⁡W
47 44 46 oveq12d ⊢W∈LMod∧G∈F∧r∈BaseScalar⁡W∧x∈K⁡G∧y∈K⁡G→r⋅Scalar⁡WG⁡x+Scalar⁡WG⁡y=0Scalar⁡W+Scalar⁡W0Scalar⁡W
48 5 lmodfgrp ⊢W∈LMod→Scalar⁡W∈Grp
49 17 48 syl ⊢W∈LMod∧G∈F∧r∈BaseScalar⁡W∧x∈K⁡G∧y∈K⁡G→Scalar⁡W∈Grp
50 24 6 grpidcl ⊢Scalar⁡W∈Grp→0Scalar⁡W∈BaseScalar⁡W
51 24 33 6 grplid ⊢Scalar⁡W∈Grp∧0Scalar⁡W∈BaseScalar⁡W→0Scalar⁡W+Scalar⁡W0Scalar⁡W=0Scalar⁡W
52 49 50 51 syl2anc2 ⊢W∈LMod∧G∈F∧r∈BaseScalar⁡W∧x∈K⁡G∧y∈K⁡G→0Scalar⁡W+Scalar⁡W0Scalar⁡W=0Scalar⁡W
53 36 47 52 3eqtrd ⊢W∈LMod∧G∈F∧r∈BaseScalar⁡W∧x∈K⁡G∧y∈K⁡G→G⁡r⋅Wx+Wy=0Scalar⁡W
54 4 5 6 1 2 ellkr ⊢W∈LMod∧G∈F→r⋅Wx+Wy∈K⁡G↔r⋅Wx+Wy∈BaseW∧G⁡r⋅Wx+Wy=0Scalar⁡W
55 54 ad2antrr ⊢W∈LMod∧G∈F∧r∈BaseScalar⁡W∧x∈K⁡G∧y∈K⁡G→r⋅Wx+Wy∈K⁡G↔r⋅Wx+Wy∈BaseW∧G⁡r⋅Wx+Wy=0Scalar⁡W
56 32 53 55 mpbir2and ⊢W∈LMod∧G∈F∧r∈BaseScalar⁡W∧x∈K⁡G∧y∈K⁡G→r⋅Wx+Wy∈K⁡G
57 56 ralrimivva ⊢W∈LMod∧G∈F∧r∈BaseScalar⁡W→∀x∈K⁡G∀y∈K⁡Gr⋅Wx+Wy∈K⁡G
58 57 ralrimiva ⊢W∈LMod∧G∈F→∀r∈BaseScalar⁡W∀x∈K⁡G∀y∈K⁡Gr⋅Wx+Wy∈K⁡G
59 5 24 4 30 23 3 islss ⊢K⁡G∈S↔K⁡G⊆BaseW∧K⁡G≠∅∧∀r∈BaseScalar⁡W∀x∈K⁡G∀y∈K⁡Gr⋅Wx+Wy∈K⁡G
60 9 16 58 59 syl3anbrc ⊢W∈LMod∧G∈F→K⁡G∈S