Theorem lkrshp4

Description: A kernel is a hyperplane iff it doesn't contain all vectors. (Contributed by NM, 1-Nov-2014)

	Ref	Expression
Hypotheses	lkrshp4.v	⊢ 𝑉 = ( Base ‘ 𝑊 )
	lkrshp4.h	⊢ 𝐻 = ( LSHyp ‘ 𝑊 )
	lkrshp4.f	⊢ 𝐹 = ( LFnl ‘ 𝑊 )
	lkrshp4.k	⊢ 𝐾 = ( LKer ‘ 𝑊 )
	lkrshp4.w	⊢ ( 𝜑 → 𝑊 ∈ LVec )
	lkrshp4.g	⊢ ( 𝜑 → 𝐺 ∈ 𝐹 )
Assertion	lkrshp4	⊢ ( 𝜑 → ( ( 𝐾 ‘ 𝐺 ) ≠ 𝑉 ↔ ( 𝐾 ‘ 𝐺 ) ∈ 𝐻 ) )

Proof

Step	Hyp	Ref	Expression
1		lkrshp4.v	⊢ 𝑉 = ( Base ‘ 𝑊 )
2		lkrshp4.h	⊢ 𝐻 = ( LSHyp ‘ 𝑊 )
3		lkrshp4.f	⊢ 𝐹 = ( LFnl ‘ 𝑊 )
4		lkrshp4.k	⊢ 𝐾 = ( LKer ‘ 𝑊 )
5		lkrshp4.w	⊢ ( 𝜑 → 𝑊 ∈ LVec )
6		lkrshp4.g	⊢ ( 𝜑 → 𝐺 ∈ 𝐹 )
7	1 2 3 4 5 6	lkrshpor	⊢ ( 𝜑 → ( ( 𝐾 ‘ 𝐺 ) ∈ 𝐻 ∨ ( 𝐾 ‘ 𝐺 ) = 𝑉 ) )
8	7	orcomd	⊢ ( 𝜑 → ( ( 𝐾 ‘ 𝐺 ) = 𝑉 ∨ ( 𝐾 ‘ 𝐺 ) ∈ 𝐻 ) )
9		neor	⊢ ( ( ( 𝐾 ‘ 𝐺 ) = 𝑉 ∨ ( 𝐾 ‘ 𝐺 ) ∈ 𝐻 ) ↔ ( ( 𝐾 ‘ 𝐺 ) ≠ 𝑉 → ( 𝐾 ‘ 𝐺 ) ∈ 𝐻 ) )
10	8 9	sylib	⊢ ( 𝜑 → ( ( 𝐾 ‘ 𝐺 ) ≠ 𝑉 → ( 𝐾 ‘ 𝐺 ) ∈ 𝐻 ) )
11		lveclmod	⊢ ( 𝑊 ∈ LVec → 𝑊 ∈ LMod )
12	5 11	syl	⊢ ( 𝜑 → 𝑊 ∈ LMod )
13	12	adantr	⊢ ( ( 𝜑 ∧ ( 𝐾 ‘ 𝐺 ) ∈ 𝐻 ) → 𝑊 ∈ LMod )
14		simpr	⊢ ( ( 𝜑 ∧ ( 𝐾 ‘ 𝐺 ) ∈ 𝐻 ) → ( 𝐾 ‘ 𝐺 ) ∈ 𝐻 )
15	1 2 13 14	lshpne	⊢ ( ( 𝜑 ∧ ( 𝐾 ‘ 𝐺 ) ∈ 𝐻 ) → ( 𝐾 ‘ 𝐺 ) ≠ 𝑉 )
16	15	ex	⊢ ( 𝜑 → ( ( 𝐾 ‘ 𝐺 ) ∈ 𝐻 → ( 𝐾 ‘ 𝐺 ) ≠ 𝑉 ) )
17	10 16	impbid	⊢ ( 𝜑 → ( ( 𝐾 ‘ 𝐺 ) ≠ 𝑉 ↔ ( 𝐾 ‘ 𝐺 ) ∈ 𝐻 ) )