This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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