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