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 \in LinFn$
	Assertion	nlelshi	$⊢ null (T) \in S_{ℋ}$

Proof

Step	Hyp	Ref	Expression
1		nlelsh.1	$⊢ T \in LinFn$
2		ax-hv0cl	$⊢ 0_{ℎ} \in ℋ$
3	1	lnfn0i	$⊢ T (0_{ℎ}) = 0$
4	1	lnfnfi	$⊢ T : ℋ ⟶ ℂ$
5		elnlfn	$⊢ T : ℋ ⟶ ℂ \to (0_{ℎ} \in null (T) \leftrightarrow (0_{ℎ} \in ℋ \land T (0_{ℎ}) = 0))$
6	4 5	ax-mp	$⊢ 0_{ℎ} \in null (T) \leftrightarrow (0_{ℎ} \in ℋ \land T (0_{ℎ}) = 0)$
7	2 3 6	mpbir2an	$⊢ 0_{ℎ} \in null (T)$
8		nlfnval	$⊢ T : ℋ ⟶ ℂ \to null (T) = T^{-1} [\{0\}]$
9	4 8	ax-mp	$⊢ null (T) = T^{-1} [\{0\}]$
10		cnvimass	$⊢ T^{-1} [\{0\}] \subseteq dom T$
11	9 10	eqsstri	$⊢ null (T) \subseteq dom T$
12	4	fdmi	$⊢ dom T = ℋ$
13	11 12	sseqtri	$⊢ null (T) \subseteq ℋ$
14	13	sseli	$⊢ x \in null (T) \to x \in ℋ$
15	13	sseli	$⊢ y \in null (T) \to y \in ℋ$
16		hvaddcl	$⊢ (x \in ℋ \land y \in ℋ) \to x +_{ℎ} y \in ℋ$
17	14 15 16	syl2an	$⊢ (x \in null (T) \land y \in null (T)) \to x +_{ℎ} y \in ℋ$
18	1	lnfnaddi	$⊢ (x \in ℋ \land y \in ℋ) \to T (x +_{ℎ} y) = T (x) + T (y)$
19	14 15 18	syl2an	$⊢ (x \in null (T) \land y \in null (T)) \to T (x +_{ℎ} y) = T (x) + T (y)$
20		elnlfn	$⊢ T : ℋ ⟶ ℂ \to (x \in null (T) \leftrightarrow (x \in ℋ \land T (x) = 0))$
21	4 20	ax-mp	$⊢ x \in null (T) \leftrightarrow (x \in ℋ \land T (x) = 0)$
22	21	simprbi	$⊢ x \in null (T) \to T (x) = 0$
23		elnlfn	$⊢ T : ℋ ⟶ ℂ \to (y \in null (T) \leftrightarrow (y \in ℋ \land T (y) = 0))$
24	4 23	ax-mp	$⊢ y \in null (T) \leftrightarrow (y \in ℋ \land T (y) = 0)$
25	24	simprbi	$⊢ y \in null (T) \to T (y) = 0$
26	22 25	oveqan12d	$⊢ (x \in null (T) \land y \in null (T)) \to T (x) + T (y) = 0 + 0$
27	19 26	eqtrd	$⊢ (x \in null (T) \land y \in null (T)) \to T (x +_{ℎ} y) = 0 + 0$
28		00id	$⊢ 0 + 0 = 0$
29	27 28	eqtrdi	$⊢ (x \in null (T) \land y \in null (T)) \to T (x +_{ℎ} y) = 0$
30		elnlfn	$⊢ T : ℋ ⟶ ℂ \to (x +_{ℎ} y \in null (T) \leftrightarrow (x +_{ℎ} y \in ℋ \land T (x +_{ℎ} y) = 0))$
31	4 30	ax-mp	$⊢ x +_{ℎ} y \in null (T) \leftrightarrow (x +_{ℎ} y \in ℋ \land T (x +_{ℎ} y) = 0)$
32	17 29 31	sylanbrc	$⊢ (x \in null (T) \land y \in null (T)) \to x +_{ℎ} y \in null (T)$
33	32	rgen2	$⊢ \forall x \in null (T) \forall y \in null (T) x +_{ℎ} y \in null (T)$
34		hvmulcl	$⊢ (x \in ℂ \land y \in ℋ) \to x \cdot_{ℎ} y \in ℋ$
35	15 34	sylan2	$⊢ (x \in ℂ \land y \in null (T)) \to x \cdot_{ℎ} y \in ℋ$
36	1	lnfnmuli	$⊢ (x \in ℂ \land y \in ℋ) \to T (x \cdot_{ℎ} y) = x T (y)$
37	15 36	sylan2	$⊢ (x \in ℂ \land y \in null (T)) \to T (x \cdot_{ℎ} y) = x T (y)$
38	25	oveq2d	$⊢ y \in null (T) \to x T (y) = x \cdot 0$
39		mul01	$⊢ x \in ℂ \to x \cdot 0 = 0$
40	38 39	sylan9eqr	$⊢ (x \in ℂ \land y \in null (T)) \to x T (y) = 0$
41	37 40	eqtrd	$⊢ (x \in ℂ \land y \in null (T)) \to T (x \cdot_{ℎ} y) = 0$
42		elnlfn	$⊢ T : ℋ ⟶ ℂ \to (x \cdot_{ℎ} y \in null (T) \leftrightarrow (x \cdot_{ℎ} y \in ℋ \land T (x \cdot_{ℎ} y) = 0))$
43	4 42	ax-mp	$⊢ x \cdot_{ℎ} y \in null (T) \leftrightarrow (x \cdot_{ℎ} y \in ℋ \land T (x \cdot_{ℎ} y) = 0)$
44	35 41 43	sylanbrc	$⊢ (x \in ℂ \land y \in null (T)) \to x \cdot_{ℎ} y \in null (T)$
45	44	rgen2	$⊢ \forall x \in ℂ \forall y \in null (T) x \cdot_{ℎ} y \in null (T)$
46	33 45	pm3.2i	$⊢ (\forall x \in null (T) \forall y \in null (T) x +_{ℎ} y \in null (T) \land \forall x \in ℂ \forall y \in null (T) x \cdot_{ℎ} y \in null (T))$
47		issh3	$⊢ null (T) \subseteq ℋ \to (null (T) \in S_{ℋ} \leftrightarrow (0_{ℎ} \in null (T) \land (\forall x \in null (T) \forall y \in null (T) x +_{ℎ} y \in null (T) \land \forall x \in ℂ \forall y \in null (T) x \cdot_{ℎ} y \in null (T))))$
48	13 47	ax-mp	$⊢ null (T) \in S_{ℋ} \leftrightarrow (0_{ℎ} \in null (T) \land (\forall x \in null (T) \forall y \in null (T) x +_{ℎ} y \in null (T) \land \forall x \in ℂ \forall y \in null (T) x \cdot_{ℎ} y \in null (T)))$
49	7 46 48	mpbir2an	$⊢ null (T) \in S_{ℋ}$

Metamath Proof Explorer

Theorem nlelshi

Proof