Metamath Proof Explorer


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 ( 𝜑 → ( ( 𝐾𝐺 ) ≠ 𝑉 ↔ ( 𝐾𝐺 ) ∈ 𝐻 ) )