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