Theorem lduallkr3

Description: The kernels of nonzero functionals are hyperplanes. (Contributed by NM, 22-Feb-2015)

	Ref	Expression
Hypotheses	lduallkr3.h	⊢ 𝐻 = ( LSHyp ‘ 𝑊 )
	lduallkr3.f	⊢ 𝐹 = ( LFnl ‘ 𝑊 )
	lduallkr3.k	⊢ 𝐾 = ( LKer ‘ 𝑊 )
	lduallkr3.d	⊢ 𝐷 = ( LDual ‘ 𝑊 )
	lduallkr3.o	⊢ 0 = ( 0g ‘ 𝐷 )
	lduallkr3.w	⊢ ( 𝜑 → 𝑊 ∈ LVec )
	lduallkr3.g	⊢ ( 𝜑 → 𝐺 ∈ 𝐹 )
Assertion	lduallkr3	⊢ ( 𝜑 → ( ( 𝐾 ‘ 𝐺 ) ∈ 𝐻 ↔ 𝐺 ≠ 0 ) )

Proof

Step	Hyp	Ref	Expression
1		lduallkr3.h	⊢ 𝐻 = ( LSHyp ‘ 𝑊 )
2		lduallkr3.f	⊢ 𝐹 = ( LFnl ‘ 𝑊 )
3		lduallkr3.k	⊢ 𝐾 = ( LKer ‘ 𝑊 )
4		lduallkr3.d	⊢ 𝐷 = ( LDual ‘ 𝑊 )
5		lduallkr3.o	⊢ 0 = ( 0g ‘ 𝐷 )
6		lduallkr3.w	⊢ ( 𝜑 → 𝑊 ∈ LVec )
7		lduallkr3.g	⊢ ( 𝜑 → 𝐺 ∈ 𝐹 )
8		eqid	⊢ ( Base ‘ 𝑊 ) = ( Base ‘ 𝑊 )
9		eqid	⊢ ( Scalar ‘ 𝑊 ) = ( Scalar ‘ 𝑊 )
10		eqid	⊢ ( 0g ‘ ( Scalar ‘ 𝑊 ) ) = ( 0g ‘ ( Scalar ‘ 𝑊 ) )
11	8 9 10 1 2 3 6 7	lkrshp3	⊢ ( 𝜑 → ( ( 𝐾 ‘ 𝐺 ) ∈ 𝐻 ↔ 𝐺 ≠ ( ( Base ‘ 𝑊 ) × { ( 0g ‘ ( Scalar ‘ 𝑊 ) ) } ) ) )
12		lveclmod	⊢ ( 𝑊 ∈ LVec → 𝑊 ∈ LMod )
13	6 12	syl	⊢ ( 𝜑 → 𝑊 ∈ LMod )
14	8 9 10 4 5 13	ldual0v	⊢ ( 𝜑 → 0 = ( ( Base ‘ 𝑊 ) × { ( 0g ‘ ( Scalar ‘ 𝑊 ) ) } ) )
15	14	neeq2d	⊢ ( 𝜑 → ( 𝐺 ≠ 0 ↔ 𝐺 ≠ ( ( Base ‘ 𝑊 ) × { ( 0g ‘ ( Scalar ‘ 𝑊 ) ) } ) ) )
16	11 15	bitr4d	⊢ ( 𝜑 → ( ( 𝐾 ‘ 𝐺 ) ∈ 𝐻 ↔ 𝐺 ≠ 0 ) )