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

Metamath Proof Explorer

Theorem lkrshpor

Description: The kernel of a functional is either a hyperplane or the full vector space. (Contributed by NM, 7-Oct-2014)

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

Proof

Step Hyp Ref Expression
1 lkrshpor.v ⊢ 𝑉 = ( Base ‘ 𝑊 )
2 lkrshpor.h ⊢ 𝐻 = ( LSHyp ‘ 𝑊 )
3 lkrshpor.f ⊢ 𝐹 = ( LFnl ‘ 𝑊 )
4 lkrshpor.k ⊢ 𝐾 = ( LKer ‘ 𝑊 )
5 lkrshpor.w ⊢ ( 𝜑 → 𝑊 ∈ LVec )
6 lkrshpor.g ⊢ ( 𝜑 → 𝐺 ∈ 𝐹 )
7 lveclmod ⊢ ( 𝑊 ∈ LVec → 𝑊 ∈ LMod )
8 5 7 syl ⊢ ( 𝜑 → 𝑊 ∈ LMod )
9 eqid ⊢ ( Scalar ‘ 𝑊 ) = ( Scalar ‘ 𝑊 )
10 eqid ⊢ ( 0g ‘ ( Scalar ‘ 𝑊 ) ) = ( 0g ‘ ( Scalar ‘ 𝑊 ) )
11 9 10 1 3 4 lkr0f ⊢ ( ( 𝑊 ∈ LMod ∧ 𝐺 ∈ 𝐹 ) → ( ( 𝐾 ‘ 𝐺 ) = 𝑉 ↔ 𝐺 = ( 𝑉 × { ( 0g ‘ ( Scalar ‘ 𝑊 ) ) } ) ) )
12 8 6 11 syl2anc ⊢ ( 𝜑 → ( ( 𝐾 ‘ 𝐺 ) = 𝑉 ↔ 𝐺 = ( 𝑉 × { ( 0g ‘ ( Scalar ‘ 𝑊 ) ) } ) ) )
13 12 biimpar ⊢ ( ( 𝜑 ∧ 𝐺 = ( 𝑉 × { ( 0g ‘ ( Scalar ‘ 𝑊 ) ) } ) ) → ( 𝐾 ‘ 𝐺 ) = 𝑉 )
14 13 olcd ⊢ ( ( 𝜑 ∧ 𝐺 = ( 𝑉 × { ( 0g ‘ ( Scalar ‘ 𝑊 ) ) } ) ) → ( ( 𝐾 ‘ 𝐺 ) ∈ 𝐻 ∨ ( 𝐾 ‘ 𝐺 ) = 𝑉 ) )
15 5 adantr ⊢ ( ( 𝜑 ∧ 𝐺 ≠ ( 𝑉 × { ( 0g ‘ ( Scalar ‘ 𝑊 ) ) } ) ) → 𝑊 ∈ LVec )
16 6 adantr ⊢ ( ( 𝜑 ∧ 𝐺 ≠ ( 𝑉 × { ( 0g ‘ ( Scalar ‘ 𝑊 ) ) } ) ) → 𝐺 ∈ 𝐹 )
17 simpr ⊢ ( ( 𝜑 ∧ 𝐺 ≠ ( 𝑉 × { ( 0g ‘ ( Scalar ‘ 𝑊 ) ) } ) ) → 𝐺 ≠ ( 𝑉 × { ( 0g ‘ ( Scalar ‘ 𝑊 ) ) } ) )
18 1 9 10 2 3 4 lkrshp ⊢ ( ( 𝑊 ∈ LVec ∧ 𝐺 ∈ 𝐹 ∧ 𝐺 ≠ ( 𝑉 × { ( 0g ‘ ( Scalar ‘ 𝑊 ) ) } ) ) → ( 𝐾 ‘ 𝐺 ) ∈ 𝐻 )
19 15 16 17 18 syl3anc ⊢ ( ( 𝜑 ∧ 𝐺 ≠ ( 𝑉 × { ( 0g ‘ ( Scalar ‘ 𝑊 ) ) } ) ) → ( 𝐾 ‘ 𝐺 ) ∈ 𝐻 )
20 19 orcd ⊢ ( ( 𝜑 ∧ 𝐺 ≠ ( 𝑉 × { ( 0g ‘ ( Scalar ‘ 𝑊 ) ) } ) ) → ( ( 𝐾 ‘ 𝐺 ) ∈ 𝐻 ∨ ( 𝐾 ‘ 𝐺 ) = 𝑉 ) )
21 14 20 pm2.61dane ⊢ ( 𝜑 → ( ( 𝐾 ‘ 𝐺 ) ∈ 𝐻 ∨ ( 𝐾 ‘ 𝐺 ) = 𝑉 ) )