Theorem lkr0f2

Description: The kernel of the zero functional is the set of all vectors. (Contributed by NM, 4-Feb-2015)

	Ref	Expression
Hypotheses	lkr0f2.v	⊢ 𝑉 = ( Base ‘ 𝑊 )
	lkr0f2.f	⊢ 𝐹 = ( LFnl ‘ 𝑊 )
	lkr0f2.k	⊢ 𝐾 = ( LKer ‘ 𝑊 )
	lkr0f2.d	⊢ 𝐷 = ( LDual ‘ 𝑊 )
	lkr0f2.o	⊢ 0 = ( 0g ‘ 𝐷 )
	lkr0f2.w	⊢ ( 𝜑 → 𝑊 ∈ LMod )
	lkr0f2.g	⊢ ( 𝜑 → 𝐺 ∈ 𝐹 )
Assertion	lkr0f2	⊢ ( 𝜑 → ( ( 𝐾 ‘ 𝐺 ) = 𝑉 ↔ 𝐺 = 0 ) )

Proof

Step	Hyp	Ref	Expression
1		lkr0f2.v	⊢ 𝑉 = ( Base ‘ 𝑊 )
2		lkr0f2.f	⊢ 𝐹 = ( LFnl ‘ 𝑊 )
3		lkr0f2.k	⊢ 𝐾 = ( LKer ‘ 𝑊 )
4		lkr0f2.d	⊢ 𝐷 = ( LDual ‘ 𝑊 )
5		lkr0f2.o	⊢ 0 = ( 0g ‘ 𝐷 )
6		lkr0f2.w	⊢ ( 𝜑 → 𝑊 ∈ LMod )
7		lkr0f2.g	⊢ ( 𝜑 → 𝐺 ∈ 𝐹 )
8		eqid	⊢ ( Scalar ‘ 𝑊 ) = ( Scalar ‘ 𝑊 )
9		eqid	⊢ ( 0g ‘ ( Scalar ‘ 𝑊 ) ) = ( 0g ‘ ( Scalar ‘ 𝑊 ) )
10	8 9 1 2 3	lkr0f	⊢ ( ( 𝑊 ∈ LMod ∧ 𝐺 ∈ 𝐹 ) → ( ( 𝐾 ‘ 𝐺 ) = 𝑉 ↔ 𝐺 = ( 𝑉 × { ( 0g ‘ ( Scalar ‘ 𝑊 ) ) } ) ) )
11	6 7 10	syl2anc	⊢ ( 𝜑 → ( ( 𝐾 ‘ 𝐺 ) = 𝑉 ↔ 𝐺 = ( 𝑉 × { ( 0g ‘ ( Scalar ‘ 𝑊 ) ) } ) ) )
12	1 8 9 4 5 6	ldual0v	⊢ ( 𝜑 → 0 = ( 𝑉 × { ( 0g ‘ ( Scalar ‘ 𝑊 ) ) } ) )
13	12	eqeq2d	⊢ ( 𝜑 → ( 𝐺 = 0 ↔ 𝐺 = ( 𝑉 × { ( 0g ‘ ( Scalar ‘ 𝑊 ) ) } ) ) )
14	11 13	bitr4d	⊢ ( 𝜑 → ( ( 𝐾 ‘ 𝐺 ) = 𝑉 ↔ 𝐺 = 0 ) )