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 ⊢ 𝑇 ∈ LinFn
Assertion nlelshi ( null ‘ 𝑇 ) ∈ Sℋ

Proof

Step Hyp Ref Expression
1 nlelsh.1 ⊢ 𝑇 ∈ LinFn
2 ax-hv0cl ⊢ 0ℎ ∈ ℋ
3 1 lnfn0i ⊢ ( 𝑇 ‘ 0ℎ ) = 0
4 1 lnfnfi ⊢ 𝑇 : ℋ ⟶ ℂ
5 elnlfn ⊢ ( 𝑇 : ℋ ⟶ ℂ → ( 0ℎ ∈ ( null ‘ 𝑇 ) ↔ ( 0ℎ ∈ ℋ ∧ ( 𝑇 ‘ 0ℎ ) = 0 ) ) )
6 4 5 ax-mp ⊢ ( 0ℎ ∈ ( null ‘ 𝑇 ) ↔ ( 0ℎ ∈ ℋ ∧ ( 𝑇 ‘ 0ℎ ) = 0 ) )
7 2 3 6 mpbir2an ⊢ 0ℎ ∈ ( null ‘ 𝑇 )
8 nlfnval ⊢ ( 𝑇 : ℋ ⟶ ℂ → ( null ‘ 𝑇 ) = ( ◡ 𝑇 “ { 0 } ) )
9 4 8 ax-mp ⊢ ( null ‘ 𝑇 ) = ( ◡ 𝑇 “ { 0 } )
10 cnvimass ⊢ ( ◡ 𝑇 “ { 0 } ) ⊆ dom 𝑇
11 9 10 eqsstri ⊢ ( null ‘ 𝑇 ) ⊆ dom 𝑇
12 4 fdmi ⊢ dom 𝑇 = ℋ
13 11 12 sseqtri ⊢ ( null ‘ 𝑇 ) ⊆ ℋ
14 13 sseli ⊢ ( 𝑥 ∈ ( null ‘ 𝑇 ) → 𝑥 ∈ ℋ )
15 13 sseli ⊢ ( 𝑦 ∈ ( null ‘ 𝑇 ) → 𝑦 ∈ ℋ )
16 hvaddcl ⊢ ( ( 𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ ) → ( 𝑥 +ℎ 𝑦 ) ∈ ℋ )
17 14 15 16 syl2an ⊢ ( ( 𝑥 ∈ ( null ‘ 𝑇 ) ∧ 𝑦 ∈ ( null ‘ 𝑇 ) ) → ( 𝑥 +ℎ 𝑦 ) ∈ ℋ )
18 1 lnfnaddi ⊢ ( ( 𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ ) → ( 𝑇 ‘ ( 𝑥 +ℎ 𝑦 ) ) = ( ( 𝑇 ‘ 𝑥 ) + ( 𝑇 ‘ 𝑦 ) ) )
19 14 15 18 syl2an ⊢ ( ( 𝑥 ∈ ( null ‘ 𝑇 ) ∧ 𝑦 ∈ ( null ‘ 𝑇 ) ) → ( 𝑇 ‘ ( 𝑥 +ℎ 𝑦 ) ) = ( ( 𝑇 ‘ 𝑥 ) + ( 𝑇 ‘ 𝑦 ) ) )
20 elnlfn ⊢ ( 𝑇 : ℋ ⟶ ℂ → ( 𝑥 ∈ ( null ‘ 𝑇 ) ↔ ( 𝑥 ∈ ℋ ∧ ( 𝑇 ‘ 𝑥 ) = 0 ) ) )
21 4 20 ax-mp ⊢ ( 𝑥 ∈ ( null ‘ 𝑇 ) ↔ ( 𝑥 ∈ ℋ ∧ ( 𝑇 ‘ 𝑥 ) = 0 ) )
22 21 simprbi ⊢ ( 𝑥 ∈ ( null ‘ 𝑇 ) → ( 𝑇 ‘ 𝑥 ) = 0 )
23 elnlfn ⊢ ( 𝑇 : ℋ ⟶ ℂ → ( 𝑦 ∈ ( null ‘ 𝑇 ) ↔ ( 𝑦 ∈ ℋ ∧ ( 𝑇 ‘ 𝑦 ) = 0 ) ) )
24 4 23 ax-mp ⊢ ( 𝑦 ∈ ( null ‘ 𝑇 ) ↔ ( 𝑦 ∈ ℋ ∧ ( 𝑇 ‘ 𝑦 ) = 0 ) )
25 24 simprbi ⊢ ( 𝑦 ∈ ( null ‘ 𝑇 ) → ( 𝑇 ‘ 𝑦 ) = 0 )
26 22 25 oveqan12d ⊢ ( ( 𝑥 ∈ ( null ‘ 𝑇 ) ∧ 𝑦 ∈ ( null ‘ 𝑇 ) ) → ( ( 𝑇 ‘ 𝑥 ) + ( 𝑇 ‘ 𝑦 ) ) = ( 0 + 0 ) )
27 19 26 eqtrd ⊢ ( ( 𝑥 ∈ ( null ‘ 𝑇 ) ∧ 𝑦 ∈ ( null ‘ 𝑇 ) ) → ( 𝑇 ‘ ( 𝑥 +ℎ 𝑦 ) ) = ( 0 + 0 ) )
28 00id ⊢ ( 0 + 0 ) = 0
29 27 28 eqtrdi ⊢ ( ( 𝑥 ∈ ( null ‘ 𝑇 ) ∧ 𝑦 ∈ ( null ‘ 𝑇 ) ) → ( 𝑇 ‘ ( 𝑥 +ℎ 𝑦 ) ) = 0 )
30 elnlfn ⊢ ( 𝑇 : ℋ ⟶ ℂ → ( ( 𝑥 +ℎ 𝑦 ) ∈ ( null ‘ 𝑇 ) ↔ ( ( 𝑥 +ℎ 𝑦 ) ∈ ℋ ∧ ( 𝑇 ‘ ( 𝑥 +ℎ 𝑦 ) ) = 0 ) ) )
31 4 30 ax-mp ⊢ ( ( 𝑥 +ℎ 𝑦 ) ∈ ( null ‘ 𝑇 ) ↔ ( ( 𝑥 +ℎ 𝑦 ) ∈ ℋ ∧ ( 𝑇 ‘ ( 𝑥 +ℎ 𝑦 ) ) = 0 ) )
32 17 29 31 sylanbrc ⊢ ( ( 𝑥 ∈ ( null ‘ 𝑇 ) ∧ 𝑦 ∈ ( null ‘ 𝑇 ) ) → ( 𝑥 +ℎ 𝑦 ) ∈ ( null ‘ 𝑇 ) )
33 32 rgen2 ⊢ ∀ 𝑥 ∈ ( null ‘ 𝑇 ) ∀ 𝑦 ∈ ( null ‘ 𝑇 ) ( 𝑥 +ℎ 𝑦 ) ∈ ( null ‘ 𝑇 )
34 hvmulcl ⊢ ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℋ ) → ( 𝑥 ·ℎ 𝑦 ) ∈ ℋ )
35 15 34 sylan2 ⊢ ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ( null ‘ 𝑇 ) ) → ( 𝑥 ·ℎ 𝑦 ) ∈ ℋ )
36 1 lnfnmuli ⊢ ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℋ ) → ( 𝑇 ‘ ( 𝑥 ·ℎ 𝑦 ) ) = ( 𝑥 · ( 𝑇 ‘ 𝑦 ) ) )
37 15 36 sylan2 ⊢ ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ( null ‘ 𝑇 ) ) → ( 𝑇 ‘ ( 𝑥 ·ℎ 𝑦 ) ) = ( 𝑥 · ( 𝑇 ‘ 𝑦 ) ) )
38 25 oveq2d ⊢ ( 𝑦 ∈ ( null ‘ 𝑇 ) → ( 𝑥 · ( 𝑇 ‘ 𝑦 ) ) = ( 𝑥 · 0 ) )
39 mul01 ⊢ ( 𝑥 ∈ ℂ → ( 𝑥 · 0 ) = 0 )
40 38 39 sylan9eqr ⊢ ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ( null ‘ 𝑇 ) ) → ( 𝑥 · ( 𝑇 ‘ 𝑦 ) ) = 0 )
41 37 40 eqtrd ⊢ ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ( null ‘ 𝑇 ) ) → ( 𝑇 ‘ ( 𝑥 ·ℎ 𝑦 ) ) = 0 )
42 elnlfn ⊢ ( 𝑇 : ℋ ⟶ ℂ → ( ( 𝑥 ·ℎ 𝑦 ) ∈ ( null ‘ 𝑇 ) ↔ ( ( 𝑥 ·ℎ 𝑦 ) ∈ ℋ ∧ ( 𝑇 ‘ ( 𝑥 ·ℎ 𝑦 ) ) = 0 ) ) )
43 4 42 ax-mp ⊢ ( ( 𝑥 ·ℎ 𝑦 ) ∈ ( null ‘ 𝑇 ) ↔ ( ( 𝑥 ·ℎ 𝑦 ) ∈ ℋ ∧ ( 𝑇 ‘ ( 𝑥 ·ℎ 𝑦 ) ) = 0 ) )
44 35 41 43 sylanbrc ⊢ ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ( null ‘ 𝑇 ) ) → ( 𝑥 ·ℎ 𝑦 ) ∈ ( null ‘ 𝑇 ) )
45 44 rgen2 ⊢ ∀ 𝑥 ∈ ℂ ∀ 𝑦 ∈ ( null ‘ 𝑇 ) ( 𝑥 ·ℎ 𝑦 ) ∈ ( null ‘ 𝑇 )
46 33 45 pm3.2i ⊢ ( ∀ 𝑥 ∈ ( null ‘ 𝑇 ) ∀ 𝑦 ∈ ( null ‘ 𝑇 ) ( 𝑥 +ℎ 𝑦 ) ∈ ( null ‘ 𝑇 ) ∧ ∀ 𝑥 ∈ ℂ ∀ 𝑦 ∈ ( null ‘ 𝑇 ) ( 𝑥 ·ℎ 𝑦 ) ∈ ( null ‘ 𝑇 ) )
47 issh3 ⊢ ( ( null ‘ 𝑇 ) ⊆ ℋ → ( ( null ‘ 𝑇 ) ∈ Sℋ ↔ ( 0ℎ ∈ ( null ‘ 𝑇 ) ∧ ( ∀ 𝑥 ∈ ( null ‘ 𝑇 ) ∀ 𝑦 ∈ ( null ‘ 𝑇 ) ( 𝑥 +ℎ 𝑦 ) ∈ ( null ‘ 𝑇 ) ∧ ∀ 𝑥 ∈ ℂ ∀ 𝑦 ∈ ( null ‘ 𝑇 ) ( 𝑥 ·ℎ 𝑦 ) ∈ ( null ‘ 𝑇 ) ) ) ) )
48 13 47 ax-mp ⊢ ( ( null ‘ 𝑇 ) ∈ Sℋ ↔ ( 0ℎ ∈ ( null ‘ 𝑇 ) ∧ ( ∀ 𝑥 ∈ ( null ‘ 𝑇 ) ∀ 𝑦 ∈ ( null ‘ 𝑇 ) ( 𝑥 +ℎ 𝑦 ) ∈ ( null ‘ 𝑇 ) ∧ ∀ 𝑥 ∈ ℂ ∀ 𝑦 ∈ ( null ‘ 𝑇 ) ( 𝑥 ·ℎ 𝑦 ) ∈ ( null ‘ 𝑇 ) ) ) )
49 7 46 48 mpbir2an ⊢ ( null ‘ 𝑇 ) ∈ Sℋ