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	biimpi	$⊢ G = V \times \{\underset{˙}{0}\} \to (G Fn V \land G^{-1} [\{\underset{˙}{0}\}] = V)$
20	19	adantl	$⊢ (W \in LMod \land G = V \times \{\underset{˙}{0}\}) \to (G Fn V \land G^{-1} [\{\underset{˙}{0}\}] = V)$
21		simpr	$⊢ (W \in LMod \land G = V \times \{\underset{˙}{0}\}) \to G = V \times \{\underset{˙}{0}\}$
22		eqid	$⊢ LFnl (W) = LFnl (W)$
23	1 2 3 22	lfl0f	$⊢ W \in LMod \to V \times \{\underset{˙}{0}\} \in LFnl (W)$
24	23	adantr	$⊢ (W \in LMod \land G = V \times \{\underset{˙}{0}\}) \to V \times \{\underset{˙}{0}\} \in LFnl (W)$
25	21 24	eqeltrd	$⊢ (W \in LMod \land G = V \times \{\underset{˙}{0}\}) \to G \in LFnl (W)$
26	1 2 22 5	lkrval	$⊢ (W \in LMod \land G \in LFnl (W)) \to K (G) = G^{-1} [\{\underset{˙}{0}\}]$
27	25 26	syldan	$⊢ (W \in LMod \land G = V \times \{\underset{˙}{0}\}) \to K (G) = G^{-1} [\{\underset{˙}{0}\}]$
28	27	eqeq1d	$⊢ (W \in LMod \land G = V \times \{\underset{˙}{0}\}) \to (K (G) = V \leftrightarrow G^{-1} [\{\underset{˙}{0}\}] = V)$
29		ffn	$⊢ G : V ⟶ \{\underset{˙}{0}\} \to G Fn V$
30	14 29	sylbir	$⊢ G = V \times \{\underset{˙}{0}\} \to G Fn V$
31	30	adantl	$⊢ (W \in LMod \land G = V \times \{\underset{˙}{0}\}) \to G Fn V$
32	31	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))$
33	28 32	bitrd	$⊢ (W \in LMod \land G = V \times \{\underset{˙}{0}\}) \to (K (G) = V \leftrightarrow (G Fn V \land G^{-1} [\{\underset{˙}{0}\}] = V))$
34	20 33	mpbird	$⊢ (W \in LMod \land G = V \times \{\underset{˙}{0}\}) \to K (G) = V$
35	34	ex	$⊢ W \in LMod \to (G = V \times \{\underset{˙}{0}\} \to K (G) = V)$
36	35	adantr	$⊢ (W \in LMod \land G \in F) \to (G = V \times \{\underset{˙}{0}\} \to K (G) = V)$
37	18 36	impbid	$⊢ (W \in LMod \land G \in F) \to (K (G) = V \leftrightarrow G = V \times \{\underset{˙}{0}\})$

Metamath Proof Explorer

Theorem lkr0f

Proof