Theorem 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	⊢ 𝐷 = ( Scalar ‘ 𝑊 )
	lkr0f.o	⊢ 0 = ( 0g ‘ 𝐷 )
	lkr0f.v	⊢ 𝑉 = ( Base ‘ 𝑊 )
	lkr0f.f	⊢ 𝐹 = ( LFnl ‘ 𝑊 )
	lkr0f.k	⊢ 𝐾 = ( LKer ‘ 𝑊 )
Assertion	lkr0f	⊢ ( ( 𝑊 ∈ LMod ∧ 𝐺 ∈ 𝐹 ) → ( ( 𝐾 ‘ 𝐺 ) = 𝑉 ↔ 𝐺 = ( 𝑉 × { 0 } ) ) )

Proof

Step	Hyp	Ref	Expression
1		lkr0f.d	⊢ 𝐷 = ( Scalar ‘ 𝑊 )
2		lkr0f.o	⊢ 0 = ( 0g ‘ 𝐷 )
3		lkr0f.v	⊢ 𝑉 = ( Base ‘ 𝑊 )
4		lkr0f.f	⊢ 𝐹 = ( LFnl ‘ 𝑊 )
5		lkr0f.k	⊢ 𝐾 = ( LKer ‘ 𝑊 )
6		eqid	⊢ ( Base ‘ 𝐷 ) = ( Base ‘ 𝐷 )
7	1 6 3 4	lflf	⊢ ( ( 𝑊 ∈ LMod ∧ 𝐺 ∈ 𝐹 ) → 𝐺 : 𝑉 ⟶ ( Base ‘ 𝐷 ) )
8	7	ffnd	⊢ ( ( 𝑊 ∈ LMod ∧ 𝐺 ∈ 𝐹 ) → 𝐺 Fn 𝑉 )
9	8	adantr	⊢ ( ( ( 𝑊 ∈ LMod ∧ 𝐺 ∈ 𝐹 ) ∧ ( 𝐾 ‘ 𝐺 ) = 𝑉 ) → 𝐺 Fn 𝑉 )
10	1 2 4 5	lkrval	⊢ ( ( 𝑊 ∈ LMod ∧ 𝐺 ∈ 𝐹 ) → ( 𝐾 ‘ 𝐺 ) = ( ◡ 𝐺 “ { 0 } ) )
11	10	eqeq1d	⊢ ( ( 𝑊 ∈ LMod ∧ 𝐺 ∈ 𝐹 ) → ( ( 𝐾 ‘ 𝐺 ) = 𝑉 ↔ ( ◡ 𝐺 “ { 0 } ) = 𝑉 ) )
12	11	biimpa	⊢ ( ( ( 𝑊 ∈ LMod ∧ 𝐺 ∈ 𝐹 ) ∧ ( 𝐾 ‘ 𝐺 ) = 𝑉 ) → ( ◡ 𝐺 “ { 0 } ) = 𝑉 )
13	2	fvexi	⊢ 0 ∈ V
14	13	fconst2	⊢ ( 𝐺 : 𝑉 ⟶ { 0 } ↔ 𝐺 = ( 𝑉 × { 0 } ) )
15		fconst4	⊢ ( 𝐺 : 𝑉 ⟶ { 0 } ↔ ( 𝐺 Fn 𝑉 ∧ ( ◡ 𝐺 “ { 0 } ) = 𝑉 ) )
16	14 15	bitr3i	⊢ ( 𝐺 = ( 𝑉 × { 0 } ) ↔ ( 𝐺 Fn 𝑉 ∧ ( ◡ 𝐺 “ { 0 } ) = 𝑉 ) )
17	9 12 16	sylanbrc	⊢ ( ( ( 𝑊 ∈ LMod ∧ 𝐺 ∈ 𝐹 ) ∧ ( 𝐾 ‘ 𝐺 ) = 𝑉 ) → 𝐺 = ( 𝑉 × { 0 } ) )
18	17	ex	⊢ ( ( 𝑊 ∈ LMod ∧ 𝐺 ∈ 𝐹 ) → ( ( 𝐾 ‘ 𝐺 ) = 𝑉 → 𝐺 = ( 𝑉 × { 0 } ) ) )
19	16	biimpi	⊢ ( 𝐺 = ( 𝑉 × { 0 } ) → ( 𝐺 Fn 𝑉 ∧ ( ◡ 𝐺 “ { 0 } ) = 𝑉 ) )
20	19	adantl	⊢ ( ( 𝑊 ∈ LMod ∧ 𝐺 = ( 𝑉 × { 0 } ) ) → ( 𝐺 Fn 𝑉 ∧ ( ◡ 𝐺 “ { 0 } ) = 𝑉 ) )
21		simpr	⊢ ( ( 𝑊 ∈ LMod ∧ 𝐺 = ( 𝑉 × { 0 } ) ) → 𝐺 = ( 𝑉 × { 0 } ) )
22		eqid	⊢ ( LFnl ‘ 𝑊 ) = ( LFnl ‘ 𝑊 )
23	1 2 3 22	lfl0f	⊢ ( 𝑊 ∈ LMod → ( 𝑉 × { 0 } ) ∈ ( LFnl ‘ 𝑊 ) )
24	23	adantr	⊢ ( ( 𝑊 ∈ LMod ∧ 𝐺 = ( 𝑉 × { 0 } ) ) → ( 𝑉 × { 0 } ) ∈ ( LFnl ‘ 𝑊 ) )
25	21 24	eqeltrd	⊢ ( ( 𝑊 ∈ LMod ∧ 𝐺 = ( 𝑉 × { 0 } ) ) → 𝐺 ∈ ( LFnl ‘ 𝑊 ) )
26	1 2 22 5	lkrval	⊢ ( ( 𝑊 ∈ LMod ∧ 𝐺 ∈ ( LFnl ‘ 𝑊 ) ) → ( 𝐾 ‘ 𝐺 ) = ( ◡ 𝐺 “ { 0 } ) )
27	25 26	syldan	⊢ ( ( 𝑊 ∈ LMod ∧ 𝐺 = ( 𝑉 × { 0 } ) ) → ( 𝐾 ‘ 𝐺 ) = ( ◡ 𝐺 “ { 0 } ) )
28	27	eqeq1d	⊢ ( ( 𝑊 ∈ LMod ∧ 𝐺 = ( 𝑉 × { 0 } ) ) → ( ( 𝐾 ‘ 𝐺 ) = 𝑉 ↔ ( ◡ 𝐺 “ { 0 } ) = 𝑉 ) )
29		ffn	⊢ ( 𝐺 : 𝑉 ⟶ { 0 } → 𝐺 Fn 𝑉 )
30	14 29	sylbir	⊢ ( 𝐺 = ( 𝑉 × { 0 } ) → 𝐺 Fn 𝑉 )
31	30	adantl	⊢ ( ( 𝑊 ∈ LMod ∧ 𝐺 = ( 𝑉 × { 0 } ) ) → 𝐺 Fn 𝑉 )
32	31	biantrurd	⊢ ( ( 𝑊 ∈ LMod ∧ 𝐺 = ( 𝑉 × { 0 } ) ) → ( ( ◡ 𝐺 “ { 0 } ) = 𝑉 ↔ ( 𝐺 Fn 𝑉 ∧ ( ◡ 𝐺 “ { 0 } ) = 𝑉 ) ) )
33	28 32	bitrd	⊢ ( ( 𝑊 ∈ LMod ∧ 𝐺 = ( 𝑉 × { 0 } ) ) → ( ( 𝐾 ‘ 𝐺 ) = 𝑉 ↔ ( 𝐺 Fn 𝑉 ∧ ( ◡ 𝐺 “ { 0 } ) = 𝑉 ) ) )
34	20 33	mpbird	⊢ ( ( 𝑊 ∈ LMod ∧ 𝐺 = ( 𝑉 × { 0 } ) ) → ( 𝐾 ‘ 𝐺 ) = 𝑉 )
35	34	ex	⊢ ( 𝑊 ∈ LMod → ( 𝐺 = ( 𝑉 × { 0 } ) → ( 𝐾 ‘ 𝐺 ) = 𝑉 ) )
36	35	adantr	⊢ ( ( 𝑊 ∈ LMod ∧ 𝐺 ∈ 𝐹 ) → ( 𝐺 = ( 𝑉 × { 0 } ) → ( 𝐾 ‘ 𝐺 ) = 𝑉 ) )
37	18 36	impbid	⊢ ( ( 𝑊 ∈ LMod ∧ 𝐺 ∈ 𝐹 ) → ( ( 𝐾 ‘ 𝐺 ) = 𝑉 ↔ 𝐺 = ( 𝑉 × { 0 } ) ) )