Metamath Proof Explorer

Theorem nlelshi

Description: The null space of a linear functional is a subspace. (Contributed by NM, 11-Feb-2006) (Revised by Mario Carneiro, 17-Nov-2013) (New usage is discouraged.)

Ref Expression
Hypothesis nlelsh.1 
|- T e. LinFn
Assertion nlelshi 
|- ( null ` T ) e. SH

Proof

Step Hyp Ref Expression
1 nlelsh.1 
 |-  T e. LinFn
2 ax-hv0cl 
 |-  0h e. ~H
3 1 lnfn0i 
 |-  ( T ` 0h ) = 0
4 1 lnfnfi 
 |-  T : ~H --> CC
5 elnlfn 
 |-  ( T : ~H --> CC -> ( 0h e. ( null ` T ) <-> ( 0h e. ~H /\ ( T ` 0h ) = 0 ) ) )
6 4 5 ax-mp 
 |-  ( 0h e. ( null ` T ) <-> ( 0h e. ~H /\ ( T ` 0h ) = 0 ) )
7 2 3 6 mpbir2an 
 |-  0h e. ( null ` T )
8 nlfnval 
 |-  ( T : ~H --> CC -> ( null ` T ) = ( `' T " { 0 } ) )
9 4 8 ax-mp 
 |-  ( null ` T ) = ( `' T " { 0 } )
10 cnvimass 
 |-  ( `' T " { 0 } ) C_ dom T
11 9 10 eqsstri 
 |-  ( null ` T ) C_ dom T
12 4 fdmi 
 |-  dom T = ~H
13 11 12 sseqtri 
 |-  ( null ` T ) C_ ~H
14 13 sseli 
 |-  ( x e. ( null ` T ) -> x e. ~H )
15 13 sseli 
 |-  ( y e. ( null ` T ) -> y e. ~H )
16 hvaddcl 
 |-  ( ( x e. ~H /\ y e. ~H ) -> ( x +h y ) e. ~H )
17 14 15 16 syl2an 
 |-  ( ( x e. ( null ` T ) /\ y e. ( null ` T ) ) -> ( x +h y ) e. ~H )
18 1 lnfnaddi 
 |-  ( ( x e. ~H /\ y e. ~H ) -> ( T ` ( x +h y ) ) = ( ( T ` x ) + ( T ` y ) ) )
19 14 15 18 syl2an 
 |-  ( ( x e. ( null ` T ) /\ y e. ( null ` T ) ) -> ( T ` ( x +h y ) ) = ( ( T ` x ) + ( T ` y ) ) )
20 elnlfn 
 |-  ( T : ~H --> CC -> ( x e. ( null ` T ) <-> ( x e. ~H /\ ( T ` x ) = 0 ) ) )
21 4 20 ax-mp 
 |-  ( x e. ( null ` T ) <-> ( x e. ~H /\ ( T ` x ) = 0 ) )
22 21 simprbi 
 |-  ( x e. ( null ` T ) -> ( T ` x ) = 0 )
23 elnlfn 
 |-  ( T : ~H --> CC -> ( y e. ( null ` T ) <-> ( y e. ~H /\ ( T ` y ) = 0 ) ) )
24 4 23 ax-mp 
 |-  ( y e. ( null ` T ) <-> ( y e. ~H /\ ( T ` y ) = 0 ) )
25 24 simprbi 
 |-  ( y e. ( null ` T ) -> ( T ` y ) = 0 )
26 22 25 oveqan12d 
 |-  ( ( x e. ( null ` T ) /\ y e. ( null ` T ) ) -> ( ( T ` x ) + ( T ` y ) ) = ( 0 + 0 ) )
27 19 26 eqtrd 
 |-  ( ( x e. ( null ` T ) /\ y e. ( null ` T ) ) -> ( T ` ( x +h y ) ) = ( 0 + 0 ) )
28 00id 
 |-  ( 0 + 0 ) = 0
29 27 28 eqtrdi 
 |-  ( ( x e. ( null ` T ) /\ y e. ( null ` T ) ) -> ( T ` ( x +h y ) ) = 0 )
30 elnlfn 
 |-  ( T : ~H --> CC -> ( ( x +h y ) e. ( null ` T ) <-> ( ( x +h y ) e. ~H /\ ( T ` ( x +h y ) ) = 0 ) ) )
31 4 30 ax-mp 
 |-  ( ( x +h y ) e. ( null ` T ) <-> ( ( x +h y ) e. ~H /\ ( T ` ( x +h y ) ) = 0 ) )
32 17 29 31 sylanbrc 
 |-  ( ( x e. ( null ` T ) /\ y e. ( null ` T ) ) -> ( x +h y ) e. ( null ` T ) )
33 32 rgen2 
 |-  A. x e. ( null ` T ) A. y e. ( null ` T ) ( x +h y ) e. ( null ` T )
34 hvmulcl 
 |-  ( ( x e. CC /\ y e. ~H ) -> ( x .h y ) e. ~H )
35 15 34 sylan2 
 |-  ( ( x e. CC /\ y e. ( null ` T ) ) -> ( x .h y ) e. ~H )
36 1 lnfnmuli 
 |-  ( ( x e. CC /\ y e. ~H ) -> ( T ` ( x .h y ) ) = ( x x. ( T ` y ) ) )
37 15 36 sylan2 
 |-  ( ( x e. CC /\ y e. ( null ` T ) ) -> ( T ` ( x .h y ) ) = ( x x. ( T ` y ) ) )
38 25 oveq2d 
 |-  ( y e. ( null ` T ) -> ( x x. ( T ` y ) ) = ( x x. 0 ) )
39 mul01 
 |-  ( x e. CC -> ( x x. 0 ) = 0 )
40 38 39 sylan9eqr 
 |-  ( ( x e. CC /\ y e. ( null ` T ) ) -> ( x x. ( T ` y ) ) = 0 )
41 37 40 eqtrd 
 |-  ( ( x e. CC /\ y e. ( null ` T ) ) -> ( T ` ( x .h y ) ) = 0 )
42 elnlfn 
 |-  ( T : ~H --> CC -> ( ( x .h y ) e. ( null ` T ) <-> ( ( x .h y ) e. ~H /\ ( T ` ( x .h y ) ) = 0 ) ) )
43 4 42 ax-mp 
 |-  ( ( x .h y ) e. ( null ` T ) <-> ( ( x .h y ) e. ~H /\ ( T ` ( x .h y ) ) = 0 ) )
44 35 41 43 sylanbrc 
 |-  ( ( x e. CC /\ y e. ( null ` T ) ) -> ( x .h y ) e. ( null ` T ) )
45 44 rgen2 
 |-  A. x e. CC A. y e. ( null ` T ) ( x .h y ) e. ( null ` T )
46 33 45 pm3.2i 
 |-  ( A. x e. ( null ` T ) A. y e. ( null ` T ) ( x +h y ) e. ( null ` T ) /\ A. x e. CC A. y e. ( null ` T ) ( x .h y ) e. ( null ` T ) )
47 issh3 
 |-  ( ( null ` T ) C_ ~H -> ( ( null ` T ) e. SH <-> ( 0h e. ( null ` T ) /\ ( A. x e. ( null ` T ) A. y e. ( null ` T ) ( x +h y ) e. ( null ` T ) /\ A. x e. CC A. y e. ( null ` T ) ( x .h y ) e. ( null ` T ) ) ) ) )
48 13 47 ax-mp 
 |-  ( ( null ` T ) e. SH <-> ( 0h e. ( null ` T ) /\ ( A. x e. ( null ` T ) A. y e. ( null ` T ) ( x +h y ) e. ( null ` T ) /\ A. x e. CC A. y e. ( null ` T ) ( x .h y ) e. ( null ` T ) ) ) )
49 7 46 48 mpbir2an 
 |-  ( null ` T ) e. SH