Metamath Proof Explorer

Theorem lkrshp3

Description: The kernels of nonzero functionals are hyperplanes. (Contributed by NM, 17-Jul-2014)

Ref Expression
Hypotheses lkrshp3.v ⊢ 𝑉 = ( Base ‘ 𝑊 )
lkrshp3.d ⊢ 𝐷 = ( Scalar ‘ 𝑊 )
lkrshp3.o ⊢ 0 = ( 0g ‘ 𝐷 )
lkrshp3.h ⊢ 𝐻 = ( LSHyp ‘ 𝑊 )
lkrshp3.f ⊢ 𝐹 = ( LFnl ‘ 𝑊 )
lkrshp3.k ⊢ 𝐾 = ( LKer ‘ 𝑊 )
lkrshp3.w ⊢ ( 𝜑 → 𝑊 ∈ LVec )
lkrshp3.g ⊢ ( 𝜑 → 𝐺 ∈ 𝐹 )
Assertion lkrshp3 ( 𝜑 → ( ( 𝐾 ‘ 𝐺 ) ∈ 𝐻 ↔ 𝐺 ≠ ( 𝑉 × { 0 } ) ) )

Proof

Step Hyp Ref Expression
1 lkrshp3.v ⊢ 𝑉 = ( Base ‘ 𝑊 )
2 lkrshp3.d ⊢ 𝐷 = ( Scalar ‘ 𝑊 )
3 lkrshp3.o ⊢ 0 = ( 0g ‘ 𝐷 )
4 lkrshp3.h ⊢ 𝐻 = ( LSHyp ‘ 𝑊 )
5 lkrshp3.f ⊢ 𝐹 = ( LFnl ‘ 𝑊 )
6 lkrshp3.k ⊢ 𝐾 = ( LKer ‘ 𝑊 )
7 lkrshp3.w ⊢ ( 𝜑 → 𝑊 ∈ LVec )
8 lkrshp3.g ⊢ ( 𝜑 → 𝐺 ∈ 𝐹 )
9 lveclmod ⊢ ( 𝑊 ∈ LVec → 𝑊 ∈ LMod )
10 7 9 syl ⊢ ( 𝜑 → 𝑊 ∈ LMod )
11 10 adantr ⊢ ( ( 𝜑 ∧ ( 𝐾 ‘ 𝐺 ) ∈ 𝐻 ) → 𝑊 ∈ LMod )
12 simpr ⊢ ( ( 𝜑 ∧ ( 𝐾 ‘ 𝐺 ) ∈ 𝐻 ) → ( 𝐾 ‘ 𝐺 ) ∈ 𝐻 )
13 1 4 11 12 lshpne ⊢ ( ( 𝜑 ∧ ( 𝐾 ‘ 𝐺 ) ∈ 𝐻 ) → ( 𝐾 ‘ 𝐺 ) ≠ 𝑉 )
14 2 3 1 5 6 lkr0f ⊢ ( ( 𝑊 ∈ LMod ∧ 𝐺 ∈ 𝐹 ) → ( ( 𝐾 ‘ 𝐺 ) = 𝑉 ↔ 𝐺 = ( 𝑉 × { 0 } ) ) )
15 10 8 14 syl2anc ⊢ ( 𝜑 → ( ( 𝐾 ‘ 𝐺 ) = 𝑉 ↔ 𝐺 = ( 𝑉 × { 0 } ) ) )
16 15 adantr ⊢ ( ( 𝜑 ∧ ( 𝐾 ‘ 𝐺 ) ∈ 𝐻 ) → ( ( 𝐾 ‘ 𝐺 ) = 𝑉 ↔ 𝐺 = ( 𝑉 × { 0 } ) ) )
17 16 necon3bid ⊢ ( ( 𝜑 ∧ ( 𝐾 ‘ 𝐺 ) ∈ 𝐻 ) → ( ( 𝐾 ‘ 𝐺 ) ≠ 𝑉 ↔ 𝐺 ≠ ( 𝑉 × { 0 } ) ) )
18 13 17 mpbid ⊢ ( ( 𝜑 ∧ ( 𝐾 ‘ 𝐺 ) ∈ 𝐻 ) → 𝐺 ≠ ( 𝑉 × { 0 } ) )
19 7 adantr ⊢ ( ( 𝜑 ∧ 𝐺 ≠ ( 𝑉 × { 0 } ) ) → 𝑊 ∈ LVec )
20 8 adantr ⊢ ( ( 𝜑 ∧ 𝐺 ≠ ( 𝑉 × { 0 } ) ) → 𝐺 ∈ 𝐹 )
21 simpr ⊢ ( ( 𝜑 ∧ 𝐺 ≠ ( 𝑉 × { 0 } ) ) → 𝐺 ≠ ( 𝑉 × { 0 } ) )
22 1 2 3 4 5 6 lkrshp ⊢ ( ( 𝑊 ∈ LVec ∧ 𝐺 ∈ 𝐹 ∧ 𝐺 ≠ ( 𝑉 × { 0 } ) ) → ( 𝐾 ‘ 𝐺 ) ∈ 𝐻 )
23 19 20 21 22 syl3anc ⊢ ( ( 𝜑 ∧ 𝐺 ≠ ( 𝑉 × { 0 } ) ) → ( 𝐾 ‘ 𝐺 ) ∈ 𝐻 )
24 18 23 impbida ⊢ ( 𝜑 → ( ( 𝐾 ‘ 𝐺 ) ∈ 𝐻 ↔ 𝐺 ≠ ( 𝑉 × { 0 } ) ) )