Metamath Proof Explorer

Theorem lkrshp

Description: The kernel of a nonzero functional is a hyperplane. (Contributed by NM, 29-Jun-2014)

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

Proof

Step Hyp Ref Expression
1 lkrshp.v ⊢ 𝑉 = ( Base ‘ 𝑊 )
2 lkrshp.d ⊢ 𝐷 = ( Scalar ‘ 𝑊 )
3 lkrshp.z ⊢ 0 = ( 0g ‘ 𝐷 )
4 lkrshp.h ⊢ 𝐻 = ( LSHyp ‘ 𝑊 )
5 lkrshp.f ⊢ 𝐹 = ( LFnl ‘ 𝑊 )
6 lkrshp.k ⊢ 𝐾 = ( LKer ‘ 𝑊 )
7 lveclmod ⊢ ( 𝑊 ∈ LVec → 𝑊 ∈ LMod )
8 7 3ad2ant1 ⊢ ( ( 𝑊 ∈ LVec ∧ 𝐺 ∈ 𝐹 ∧ 𝐺 ≠ ( 𝑉 × { 0 } ) ) → 𝑊 ∈ LMod )
9 simp2 ⊢ ( ( 𝑊 ∈ LVec ∧ 𝐺 ∈ 𝐹 ∧ 𝐺 ≠ ( 𝑉 × { 0 } ) ) → 𝐺 ∈ 𝐹 )
10 eqid ⊢ ( LSubSp ‘ 𝑊 ) = ( LSubSp ‘ 𝑊 )
11 5 6 10 lkrlss ⊢ ( ( 𝑊 ∈ LMod ∧ 𝐺 ∈ 𝐹 ) → ( 𝐾 ‘ 𝐺 ) ∈ ( LSubSp ‘ 𝑊 ) )
12 8 9 11 syl2anc ⊢ ( ( 𝑊 ∈ LVec ∧ 𝐺 ∈ 𝐹 ∧ 𝐺 ≠ ( 𝑉 × { 0 } ) ) → ( 𝐾 ‘ 𝐺 ) ∈ ( LSubSp ‘ 𝑊 ) )
13 simp3 ⊢ ( ( 𝑊 ∈ LVec ∧ 𝐺 ∈ 𝐹 ∧ 𝐺 ≠ ( 𝑉 × { 0 } ) ) → 𝐺 ≠ ( 𝑉 × { 0 } ) )
14 2 3 1 5 6 lkr0f ⊢ ( ( 𝑊 ∈ LMod ∧ 𝐺 ∈ 𝐹 ) → ( ( 𝐾 ‘ 𝐺 ) = 𝑉 ↔ 𝐺 = ( 𝑉 × { 0 } ) ) )
15 8 9 14 syl2anc ⊢ ( ( 𝑊 ∈ LVec ∧ 𝐺 ∈ 𝐹 ∧ 𝐺 ≠ ( 𝑉 × { 0 } ) ) → ( ( 𝐾 ‘ 𝐺 ) = 𝑉 ↔ 𝐺 = ( 𝑉 × { 0 } ) ) )
16 15 necon3bid ⊢ ( ( 𝑊 ∈ LVec ∧ 𝐺 ∈ 𝐹 ∧ 𝐺 ≠ ( 𝑉 × { 0 } ) ) → ( ( 𝐾 ‘ 𝐺 ) ≠ 𝑉 ↔ 𝐺 ≠ ( 𝑉 × { 0 } ) ) )
17 13 16 mpbird ⊢ ( ( 𝑊 ∈ LVec ∧ 𝐺 ∈ 𝐹 ∧ 𝐺 ≠ ( 𝑉 × { 0 } ) ) → ( 𝐾 ‘ 𝐺 ) ≠ 𝑉 )
18 eqid ⊢ ( 1r ‘ 𝐷 ) = ( 1r ‘ 𝐷 )
19 2 3 18 1 5 lfl1 ⊢ ( ( 𝑊 ∈ LVec ∧ 𝐺 ∈ 𝐹 ∧ 𝐺 ≠ ( 𝑉 × { 0 } ) ) → ∃ 𝑣 ∈ 𝑉 ( 𝐺 ‘ 𝑣 ) = ( 1r ‘ 𝐷 ) )
20 simp11 ⊢ ( ( ( 𝑊 ∈ LVec ∧ 𝐺 ∈ 𝐹 ∧ 𝐺 ≠ ( 𝑉 × { 0 } ) ) ∧ 𝑣 ∈ 𝑉 ∧ ( 𝐺 ‘ 𝑣 ) = ( 1r ‘ 𝐷 ) ) → 𝑊 ∈ LVec )
21 simp2 ⊢ ( ( ( 𝑊 ∈ LVec ∧ 𝐺 ∈ 𝐹 ∧ 𝐺 ≠ ( 𝑉 × { 0 } ) ) ∧ 𝑣 ∈ 𝑉 ∧ ( 𝐺 ‘ 𝑣 ) = ( 1r ‘ 𝐷 ) ) → 𝑣 ∈ 𝑉 )
22 simp12 ⊢ ( ( ( 𝑊 ∈ LVec ∧ 𝐺 ∈ 𝐹 ∧ 𝐺 ≠ ( 𝑉 × { 0 } ) ) ∧ 𝑣 ∈ 𝑉 ∧ ( 𝐺 ‘ 𝑣 ) = ( 1r ‘ 𝐷 ) ) → 𝐺 ∈ 𝐹 )
23 simp3 ⊢ ( ( ( 𝑊 ∈ LVec ∧ 𝐺 ∈ 𝐹 ∧ 𝐺 ≠ ( 𝑉 × { 0 } ) ) ∧ 𝑣 ∈ 𝑉 ∧ ( 𝐺 ‘ 𝑣 ) = ( 1r ‘ 𝐷 ) ) → ( 𝐺 ‘ 𝑣 ) = ( 1r ‘ 𝐷 ) )
24 2 lvecdrng ⊢ ( 𝑊 ∈ LVec → 𝐷 ∈ DivRing )
25 3 18 drngunz ⊢ ( 𝐷 ∈ DivRing → ( 1r ‘ 𝐷 ) ≠ 0 )
26 20 24 25 3syl ⊢ ( ( ( 𝑊 ∈ LVec ∧ 𝐺 ∈ 𝐹 ∧ 𝐺 ≠ ( 𝑉 × { 0 } ) ) ∧ 𝑣 ∈ 𝑉 ∧ ( 𝐺 ‘ 𝑣 ) = ( 1r ‘ 𝐷 ) ) → ( 1r ‘ 𝐷 ) ≠ 0 )
27 23 26 eqnetrd ⊢ ( ( ( 𝑊 ∈ LVec ∧ 𝐺 ∈ 𝐹 ∧ 𝐺 ≠ ( 𝑉 × { 0 } ) ) ∧ 𝑣 ∈ 𝑉 ∧ ( 𝐺 ‘ 𝑣 ) = ( 1r ‘ 𝐷 ) ) → ( 𝐺 ‘ 𝑣 ) ≠ 0 )
28 simpl11 ⊢ ( ( ( ( 𝑊 ∈ LVec ∧ 𝐺 ∈ 𝐹 ∧ 𝐺 ≠ ( 𝑉 × { 0 } ) ) ∧ 𝑣 ∈ 𝑉 ∧ ( 𝐺 ‘ 𝑣 ) = ( 1r ‘ 𝐷 ) ) ∧ 𝑣 ∈ ( 𝐾 ‘ 𝐺 ) ) → 𝑊 ∈ LVec )
29 simpl12 ⊢ ( ( ( ( 𝑊 ∈ LVec ∧ 𝐺 ∈ 𝐹 ∧ 𝐺 ≠ ( 𝑉 × { 0 } ) ) ∧ 𝑣 ∈ 𝑉 ∧ ( 𝐺 ‘ 𝑣 ) = ( 1r ‘ 𝐷 ) ) ∧ 𝑣 ∈ ( 𝐾 ‘ 𝐺 ) ) → 𝐺 ∈ 𝐹 )
30 simpr ⊢ ( ( ( ( 𝑊 ∈ LVec ∧ 𝐺 ∈ 𝐹 ∧ 𝐺 ≠ ( 𝑉 × { 0 } ) ) ∧ 𝑣 ∈ 𝑉 ∧ ( 𝐺 ‘ 𝑣 ) = ( 1r ‘ 𝐷 ) ) ∧ 𝑣 ∈ ( 𝐾 ‘ 𝐺 ) ) → 𝑣 ∈ ( 𝐾 ‘ 𝐺 ) )
31 2 3 5 6 lkrf0 ⊢ ( ( 𝑊 ∈ LVec ∧ 𝐺 ∈ 𝐹 ∧ 𝑣 ∈ ( 𝐾 ‘ 𝐺 ) ) → ( 𝐺 ‘ 𝑣 ) = 0 )
32 28 29 30 31 syl3anc ⊢ ( ( ( ( 𝑊 ∈ LVec ∧ 𝐺 ∈ 𝐹 ∧ 𝐺 ≠ ( 𝑉 × { 0 } ) ) ∧ 𝑣 ∈ 𝑉 ∧ ( 𝐺 ‘ 𝑣 ) = ( 1r ‘ 𝐷 ) ) ∧ 𝑣 ∈ ( 𝐾 ‘ 𝐺 ) ) → ( 𝐺 ‘ 𝑣 ) = 0 )
33 32 ex ⊢ ( ( ( 𝑊 ∈ LVec ∧ 𝐺 ∈ 𝐹 ∧ 𝐺 ≠ ( 𝑉 × { 0 } ) ) ∧ 𝑣 ∈ 𝑉 ∧ ( 𝐺 ‘ 𝑣 ) = ( 1r ‘ 𝐷 ) ) → ( 𝑣 ∈ ( 𝐾 ‘ 𝐺 ) → ( 𝐺 ‘ 𝑣 ) = 0 ) )
34 33 necon3ad ⊢ ( ( ( 𝑊 ∈ LVec ∧ 𝐺 ∈ 𝐹 ∧ 𝐺 ≠ ( 𝑉 × { 0 } ) ) ∧ 𝑣 ∈ 𝑉 ∧ ( 𝐺 ‘ 𝑣 ) = ( 1r ‘ 𝐷 ) ) → ( ( 𝐺 ‘ 𝑣 ) ≠ 0 → ¬ 𝑣 ∈ ( 𝐾 ‘ 𝐺 ) ) )
35 27 34 mpd ⊢ ( ( ( 𝑊 ∈ LVec ∧ 𝐺 ∈ 𝐹 ∧ 𝐺 ≠ ( 𝑉 × { 0 } ) ) ∧ 𝑣 ∈ 𝑉 ∧ ( 𝐺 ‘ 𝑣 ) = ( 1r ‘ 𝐷 ) ) → ¬ 𝑣 ∈ ( 𝐾 ‘ 𝐺 ) )
36 eqid ⊢ ( LSpan ‘ 𝑊 ) = ( LSpan ‘ 𝑊 )
37 1 36 5 6 lkrlsp3 ⊢ ( ( 𝑊 ∈ LVec ∧ ( 𝑣 ∈ 𝑉 ∧ 𝐺 ∈ 𝐹 ) ∧ ¬ 𝑣 ∈ ( 𝐾 ‘ 𝐺 ) ) → ( ( LSpan ‘ 𝑊 ) ‘ ( ( 𝐾 ‘ 𝐺 ) ∪ { 𝑣 } ) ) = 𝑉 )
38 20 21 22 35 37 syl121anc ⊢ ( ( ( 𝑊 ∈ LVec ∧ 𝐺 ∈ 𝐹 ∧ 𝐺 ≠ ( 𝑉 × { 0 } ) ) ∧ 𝑣 ∈ 𝑉 ∧ ( 𝐺 ‘ 𝑣 ) = ( 1r ‘ 𝐷 ) ) → ( ( LSpan ‘ 𝑊 ) ‘ ( ( 𝐾 ‘ 𝐺 ) ∪ { 𝑣 } ) ) = 𝑉 )
39 38 3expia ⊢ ( ( ( 𝑊 ∈ LVec ∧ 𝐺 ∈ 𝐹 ∧ 𝐺 ≠ ( 𝑉 × { 0 } ) ) ∧ 𝑣 ∈ 𝑉 ) → ( ( 𝐺 ‘ 𝑣 ) = ( 1r ‘ 𝐷 ) → ( ( LSpan ‘ 𝑊 ) ‘ ( ( 𝐾 ‘ 𝐺 ) ∪ { 𝑣 } ) ) = 𝑉 ) )
40 39 reximdva ⊢ ( ( 𝑊 ∈ LVec ∧ 𝐺 ∈ 𝐹 ∧ 𝐺 ≠ ( 𝑉 × { 0 } ) ) → ( ∃ 𝑣 ∈ 𝑉 ( 𝐺 ‘ 𝑣 ) = ( 1r ‘ 𝐷 ) → ∃ 𝑣 ∈ 𝑉 ( ( LSpan ‘ 𝑊 ) ‘ ( ( 𝐾 ‘ 𝐺 ) ∪ { 𝑣 } ) ) = 𝑉 ) )
41 19 40 mpd ⊢ ( ( 𝑊 ∈ LVec ∧ 𝐺 ∈ 𝐹 ∧ 𝐺 ≠ ( 𝑉 × { 0 } ) ) → ∃ 𝑣 ∈ 𝑉 ( ( LSpan ‘ 𝑊 ) ‘ ( ( 𝐾 ‘ 𝐺 ) ∪ { 𝑣 } ) ) = 𝑉 )
42 1 36 10 4 islshp ⊢ ( 𝑊 ∈ LVec → ( ( 𝐾 ‘ 𝐺 ) ∈ 𝐻 ↔ ( ( 𝐾 ‘ 𝐺 ) ∈ ( LSubSp ‘ 𝑊 ) ∧ ( 𝐾 ‘ 𝐺 ) ≠ 𝑉 ∧ ∃ 𝑣 ∈ 𝑉 ( ( LSpan ‘ 𝑊 ) ‘ ( ( 𝐾 ‘ 𝐺 ) ∪ { 𝑣 } ) ) = 𝑉 ) ) )
43 42 3ad2ant1 ⊢ ( ( 𝑊 ∈ LVec ∧ 𝐺 ∈ 𝐹 ∧ 𝐺 ≠ ( 𝑉 × { 0 } ) ) → ( ( 𝐾 ‘ 𝐺 ) ∈ 𝐻 ↔ ( ( 𝐾 ‘ 𝐺 ) ∈ ( LSubSp ‘ 𝑊 ) ∧ ( 𝐾 ‘ 𝐺 ) ≠ 𝑉 ∧ ∃ 𝑣 ∈ 𝑉 ( ( LSpan ‘ 𝑊 ) ‘ ( ( 𝐾 ‘ 𝐺 ) ∪ { 𝑣 } ) ) = 𝑉 ) ) )
44 12 17 41 43 mpbir3and ⊢ ( ( 𝑊 ∈ LVec ∧ 𝐺 ∈ 𝐹 ∧ 𝐺 ≠ ( 𝑉 × { 0 } ) ) → ( 𝐾 ‘ 𝐺 ) ∈ 𝐻 )