lkr0f

Description: The kernel of the zero functional is the set of all vectors. (Contributed by NM, 17-Apr-2014)

	Ref	Expression
Hypotheses	lkr0f.d	$⊢ D = Scalar (W)$
	lkr0f.o	$⊢ \underset{˙}{0} = 0_{D}$
	lkr0f.v	$⊢ V = {Base}_{W}$
	lkr0f.f	$⊢ F = LFnl (W)$
	lkr0f.k	$⊢ K = LKer (W)$
Assertion	lkr0f	$⊢ (W \in LMod \land G \in F) \to (K (G) = V \leftrightarrow G = V \times \{\underset{˙}{0}\})$

Proof

Step	Hyp	Ref	Expression
1		lkr0f.d	$⊢ D = Scalar (W)$
2		lkr0f.o	$⊢ \underset{˙}{0} = 0_{D}$
3		lkr0f.v	$⊢ V = {Base}_{W}$
4		lkr0f.f	$⊢ F = LFnl (W)$
5		lkr0f.k	$⊢ K = LKer (W)$
6		eqid	$⊢ {Base}_{D} = {Base}_{D}$
7	1 6 3 4	lflf	$⊢ (W \in LMod \land G \in F) \to G : V ⟶ {Base}_{D}$
8	7	ffnd	$⊢ (W \in LMod \land G \in F) \to G Fn V$
9	8	adantr	$⊢ ((W \in LMod \land G \in F) \land K (G) = V) \to G Fn V$
10	1 2 4 5	lkrval	$⊢ (W \in LMod \land G \in F) \to K (G) = G^{-1} [\{\underset{˙}{0}\}]$
11	10	eqeq1d	$⊢ (W \in LMod \land G \in F) \to (K (G) = V \leftrightarrow G^{-1} [\{\underset{˙}{0}\}] = V)$
12	11	biimpa	$⊢ ((W \in LMod \land G \in F) \land K (G) = V) \to G^{-1} [\{\underset{˙}{0}\}] = V$
13	2	fvexi	$⊢ \underset{˙}{0} \in V$
14	13	fconst2	$⊢ G : V ⟶ \{\underset{˙}{0}\} \leftrightarrow G = V \times \{\underset{˙}{0}\}$
15		fconst4	$⊢ G : V ⟶ \{\underset{˙}{0}\} \leftrightarrow (G Fn V \land G^{-1} [\{\underset{˙}{0}\}] = V)$
16	14 15	bitr3i	$⊢ G = V \times \{\underset{˙}{0}\} \leftrightarrow (G Fn V \land G^{-1} [\{\underset{˙}{0}\}] = V)$
17	9 12 16	sylanbrc	$⊢ ((W \in LMod \land G \in F) \land K (G) = V) \to G = V \times \{\underset{˙}{0}\}$
18	17	ex	$⊢ (W \in LMod \land G \in F) \to (K (G) = V \to G = V \times \{\underset{˙}{0}\})$
19	16	bilani	$⊢ (W \in LMod \land G = V \times \{\underset{˙}{0}\}) \to (G Fn V \land G^{-1} [\{\underset{˙}{0}\}] = V)$
20		simpr	$⊢ (W \in LMod \land G = V \times \{\underset{˙}{0}\}) \to G = V \times \{\underset{˙}{0}\}$
21		eqid	$⊢ LFnl (W) = LFnl (W)$
22	1 2 3 21	lfl0f	$⊢ W \in LMod \to V \times \{\underset{˙}{0}\} \in LFnl (W)$
23	22	adantr	$⊢ (W \in LMod \land G = V \times \{\underset{˙}{0}\}) \to V \times \{\underset{˙}{0}\} \in LFnl (W)$
24	20 23	eqeltrd	$⊢ (W \in LMod \land G = V \times \{\underset{˙}{0}\}) \to G \in LFnl (W)$
25	1 2 21 5	lkrval	$⊢ (W \in LMod \land G \in LFnl (W)) \to K (G) = G^{-1} [\{\underset{˙}{0}\}]$
26	24 25	syldan	$⊢ (W \in LMod \land G = V \times \{\underset{˙}{0}\}) \to K (G) = G^{-1} [\{\underset{˙}{0}\}]$
27	26	eqeq1d	$⊢ (W \in LMod \land G = V \times \{\underset{˙}{0}\}) \to (K (G) = V \leftrightarrow G^{-1} [\{\underset{˙}{0}\}] = V)$
28		ffn	$⊢ G : V ⟶ \{\underset{˙}{0}\} \to G Fn V$
29	14 28	sylbir	$⊢ G = V \times \{\underset{˙}{0}\} \to G Fn V$
30	29	adantl	$⊢ (W \in LMod \land G = V \times \{\underset{˙}{0}\}) \to G Fn V$
31	30	biantrurd	$⊢ (W \in LMod \land G = V \times \{\underset{˙}{0}\}) \to (G^{-1} [\{\underset{˙}{0}\}] = V \leftrightarrow (G Fn V \land G^{-1} [\{\underset{˙}{0}\}] = V))$
32	27 31	bitrd	$⊢ (W \in LMod \land G = V \times \{\underset{˙}{0}\}) \to (K (G) = V \leftrightarrow (G Fn V \land G^{-1} [\{\underset{˙}{0}\}] = V))$
33	19 32	mpbird	$⊢ (W \in LMod \land G = V \times \{\underset{˙}{0}\}) \to K (G) = V$
34	33	ex	$⊢ W \in LMod \to (G = V \times \{\underset{˙}{0}\} \to K (G) = V)$
35	34	adantr	$⊢ (W \in LMod \land G \in F) \to (G = V \times \{\underset{˙}{0}\} \to K (G) = V)$
36	18 35	impbid	$⊢ (W \in LMod \land G \in F) \to (K (G) = V \leftrightarrow G = V \times \{\underset{˙}{0}\})$

Metamath Proof Explorer

Theorem lkr0f

Proof