Theorem lkrcl

Description: A member of the kernel of a functional is a vector. (Contributed by NM, 16-Apr-2014)

	Ref	Expression
Hypotheses	lkrcl.v	⊢ 𝑉 = ( Base ‘ 𝑊 )
	lkrcl.f	⊢ 𝐹 = ( LFnl ‘ 𝑊 )
	lkrcl.k	⊢ 𝐾 = ( LKer ‘ 𝑊 )
Assertion	lkrcl	⊢ ( ( 𝑊 ∈ 𝑌 ∧ 𝐺 ∈ 𝐹 ∧ 𝑋 ∈ ( 𝐾 ‘ 𝐺 ) ) → 𝑋 ∈ 𝑉 )

Proof

Step	Hyp	Ref	Expression
1		lkrcl.v	⊢ 𝑉 = ( Base ‘ 𝑊 )
2		lkrcl.f	⊢ 𝐹 = ( LFnl ‘ 𝑊 )
3		lkrcl.k	⊢ 𝐾 = ( LKer ‘ 𝑊 )
4		eqid	⊢ ( Scalar ‘ 𝑊 ) = ( Scalar ‘ 𝑊 )
5		eqid	⊢ ( 0g ‘ ( Scalar ‘ 𝑊 ) ) = ( 0g ‘ ( Scalar ‘ 𝑊 ) )
6	1 4 5 2 3	ellkr	⊢ ( ( 𝑊 ∈ 𝑌 ∧ 𝐺 ∈ 𝐹 ) → ( 𝑋 ∈ ( 𝐾 ‘ 𝐺 ) ↔ ( 𝑋 ∈ 𝑉 ∧ ( 𝐺 ‘ 𝑋 ) = ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ) ) )
7	6	simprbda	⊢ ( ( ( 𝑊 ∈ 𝑌 ∧ 𝐺 ∈ 𝐹 ) ∧ 𝑋 ∈ ( 𝐾 ‘ 𝐺 ) ) → 𝑋 ∈ 𝑉 )
8	7	3impa	⊢ ( ( 𝑊 ∈ 𝑌 ∧ 𝐺 ∈ 𝐹 ∧ 𝑋 ∈ ( 𝐾 ‘ 𝐺 ) ) → 𝑋 ∈ 𝑉 )