Metamath Proof Explorer

Theorem lshpset2N

Description: The set of all hyperplanes of a left module or left vector space equals the set of all kernels of nonzero functionals. (Contributed by NM, 17-Jul-2014) (New usage is discouraged.)

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

Proof

Step Hyp Ref Expression
1 lshpset2.v ⊢ 𝑉 = ( Base ‘ 𝑊 )
2 lshpset2.d ⊢ 𝐷 = ( Scalar ‘ 𝑊 )
3 lshpset2.z ⊢ 0 = ( 0g ‘ 𝐷 )
4 lshpset2.h ⊢ 𝐻 = ( LSHyp ‘ 𝑊 )
5 lshpset2.f ⊢ 𝐹 = ( LFnl ‘ 𝑊 )
6 lshpset2.k ⊢ 𝐾 = ( LKer ‘ 𝑊 )
7 4 5 6 lshpkrex ⊢ ( ( 𝑊 ∈ LVec ∧ 𝑠 ∈ 𝐻 ) → ∃ 𝑔 ∈ 𝐹 ( 𝐾 ‘ 𝑔 ) = 𝑠 )
8 eleq1 ⊢ ( ( 𝐾 ‘ 𝑔 ) = 𝑠 → ( ( 𝐾 ‘ 𝑔 ) ∈ 𝐻 ↔ 𝑠 ∈ 𝐻 ) )
9 8 biimparc ⊢ ( ( 𝑠 ∈ 𝐻 ∧ ( 𝐾 ‘ 𝑔 ) = 𝑠 ) → ( 𝐾 ‘ 𝑔 ) ∈ 𝐻 )
10 9 adantll ⊢ ( ( ( 𝑊 ∈ LVec ∧ 𝑠 ∈ 𝐻 ) ∧ ( 𝐾 ‘ 𝑔 ) = 𝑠 ) → ( 𝐾 ‘ 𝑔 ) ∈ 𝐻 )
11 10 adantlr ⊢ ( ( ( ( 𝑊 ∈ LVec ∧ 𝑠 ∈ 𝐻 ) ∧ 𝑔 ∈ 𝐹 ) ∧ ( 𝐾 ‘ 𝑔 ) = 𝑠 ) → ( 𝐾 ‘ 𝑔 ) ∈ 𝐻 )
12 simplll ⊢ ( ( ( ( 𝑊 ∈ LVec ∧ 𝑠 ∈ 𝐻 ) ∧ 𝑔 ∈ 𝐹 ) ∧ ( 𝐾 ‘ 𝑔 ) = 𝑠 ) → 𝑊 ∈ LVec )
13 simplr ⊢ ( ( ( ( 𝑊 ∈ LVec ∧ 𝑠 ∈ 𝐻 ) ∧ 𝑔 ∈ 𝐹 ) ∧ ( 𝐾 ‘ 𝑔 ) = 𝑠 ) → 𝑔 ∈ 𝐹 )
14 1 2 3 4 5 6 12 13 lkrshp3 ⊢ ( ( ( ( 𝑊 ∈ LVec ∧ 𝑠 ∈ 𝐻 ) ∧ 𝑔 ∈ 𝐹 ) ∧ ( 𝐾 ‘ 𝑔 ) = 𝑠 ) → ( ( 𝐾 ‘ 𝑔 ) ∈ 𝐻 ↔ 𝑔 ≠ ( 𝑉 × { 0 } ) ) )
15 11 14 mpbid ⊢ ( ( ( ( 𝑊 ∈ LVec ∧ 𝑠 ∈ 𝐻 ) ∧ 𝑔 ∈ 𝐹 ) ∧ ( 𝐾 ‘ 𝑔 ) = 𝑠 ) → 𝑔 ≠ ( 𝑉 × { 0 } ) )
16 15 ex ⊢ ( ( ( 𝑊 ∈ LVec ∧ 𝑠 ∈ 𝐻 ) ∧ 𝑔 ∈ 𝐹 ) → ( ( 𝐾 ‘ 𝑔 ) = 𝑠 → 𝑔 ≠ ( 𝑉 × { 0 } ) ) )
17 eqimss2 ⊢ ( ( 𝐾 ‘ 𝑔 ) = 𝑠 → 𝑠 ⊆ ( 𝐾 ‘ 𝑔 ) )
18 eqimss ⊢ ( ( 𝐾 ‘ 𝑔 ) = 𝑠 → ( 𝐾 ‘ 𝑔 ) ⊆ 𝑠 )
19 17 18 eqssd ⊢ ( ( 𝐾 ‘ 𝑔 ) = 𝑠 → 𝑠 = ( 𝐾 ‘ 𝑔 ) )
20 19 a1i ⊢ ( ( ( 𝑊 ∈ LVec ∧ 𝑠 ∈ 𝐻 ) ∧ 𝑔 ∈ 𝐹 ) → ( ( 𝐾 ‘ 𝑔 ) = 𝑠 → 𝑠 = ( 𝐾 ‘ 𝑔 ) ) )
21 16 20 jcad ⊢ ( ( ( 𝑊 ∈ LVec ∧ 𝑠 ∈ 𝐻 ) ∧ 𝑔 ∈ 𝐹 ) → ( ( 𝐾 ‘ 𝑔 ) = 𝑠 → ( 𝑔 ≠ ( 𝑉 × { 0 } ) ∧ 𝑠 = ( 𝐾 ‘ 𝑔 ) ) ) )
22 21 reximdva ⊢ ( ( 𝑊 ∈ LVec ∧ 𝑠 ∈ 𝐻 ) → ( ∃ 𝑔 ∈ 𝐹 ( 𝐾 ‘ 𝑔 ) = 𝑠 → ∃ 𝑔 ∈ 𝐹 ( 𝑔 ≠ ( 𝑉 × { 0 } ) ∧ 𝑠 = ( 𝐾 ‘ 𝑔 ) ) ) )
23 7 22 mpd ⊢ ( ( 𝑊 ∈ LVec ∧ 𝑠 ∈ 𝐻 ) → ∃ 𝑔 ∈ 𝐹 ( 𝑔 ≠ ( 𝑉 × { 0 } ) ∧ 𝑠 = ( 𝐾 ‘ 𝑔 ) ) )
24 23 ex ⊢ ( 𝑊 ∈ LVec → ( 𝑠 ∈ 𝐻 → ∃ 𝑔 ∈ 𝐹 ( 𝑔 ≠ ( 𝑉 × { 0 } ) ∧ 𝑠 = ( 𝐾 ‘ 𝑔 ) ) ) )
25 1 2 3 4 5 6 lkrshp ⊢ ( ( 𝑊 ∈ LVec ∧ 𝑔 ∈ 𝐹 ∧ 𝑔 ≠ ( 𝑉 × { 0 } ) ) → ( 𝐾 ‘ 𝑔 ) ∈ 𝐻 )
26 25 3adant3r ⊢ ( ( 𝑊 ∈ LVec ∧ 𝑔 ∈ 𝐹 ∧ ( 𝑔 ≠ ( 𝑉 × { 0 } ) ∧ 𝑠 = ( 𝐾 ‘ 𝑔 ) ) ) → ( 𝐾 ‘ 𝑔 ) ∈ 𝐻 )
27 eqid ⊢ ( LSpan ‘ 𝑊 ) = ( LSpan ‘ 𝑊 )
28 eqid ⊢ ( LSubSp ‘ 𝑊 ) = ( LSubSp ‘ 𝑊 )
29 1 27 28 4 islshp ⊢ ( 𝑊 ∈ LVec → ( ( 𝐾 ‘ 𝑔 ) ∈ 𝐻 ↔ ( ( 𝐾 ‘ 𝑔 ) ∈ ( LSubSp ‘ 𝑊 ) ∧ ( 𝐾 ‘ 𝑔 ) ≠ 𝑉 ∧ ∃ 𝑣 ∈ 𝑉 ( ( LSpan ‘ 𝑊 ) ‘ ( ( 𝐾 ‘ 𝑔 ) ∪ { 𝑣 } ) ) = 𝑉 ) ) )
30 29 3ad2ant1 ⊢ ( ( 𝑊 ∈ LVec ∧ 𝑔 ∈ 𝐹 ∧ ( 𝑔 ≠ ( 𝑉 × { 0 } ) ∧ 𝑠 = ( 𝐾 ‘ 𝑔 ) ) ) → ( ( 𝐾 ‘ 𝑔 ) ∈ 𝐻 ↔ ( ( 𝐾 ‘ 𝑔 ) ∈ ( LSubSp ‘ 𝑊 ) ∧ ( 𝐾 ‘ 𝑔 ) ≠ 𝑉 ∧ ∃ 𝑣 ∈ 𝑉 ( ( LSpan ‘ 𝑊 ) ‘ ( ( 𝐾 ‘ 𝑔 ) ∪ { 𝑣 } ) ) = 𝑉 ) ) )
31 26 30 mpbid ⊢ ( ( 𝑊 ∈ LVec ∧ 𝑔 ∈ 𝐹 ∧ ( 𝑔 ≠ ( 𝑉 × { 0 } ) ∧ 𝑠 = ( 𝐾 ‘ 𝑔 ) ) ) → ( ( 𝐾 ‘ 𝑔 ) ∈ ( LSubSp ‘ 𝑊 ) ∧ ( 𝐾 ‘ 𝑔 ) ≠ 𝑉 ∧ ∃ 𝑣 ∈ 𝑉 ( ( LSpan ‘ 𝑊 ) ‘ ( ( 𝐾 ‘ 𝑔 ) ∪ { 𝑣 } ) ) = 𝑉 ) )
32 eleq1 ⊢ ( 𝑠 = ( 𝐾 ‘ 𝑔 ) → ( 𝑠 ∈ ( LSubSp ‘ 𝑊 ) ↔ ( 𝐾 ‘ 𝑔 ) ∈ ( LSubSp ‘ 𝑊 ) ) )
33 neeq1 ⊢ ( 𝑠 = ( 𝐾 ‘ 𝑔 ) → ( 𝑠 ≠ 𝑉 ↔ ( 𝐾 ‘ 𝑔 ) ≠ 𝑉 ) )
34 uneq1 ⊢ ( 𝑠 = ( 𝐾 ‘ 𝑔 ) → ( 𝑠 ∪ { 𝑣 } ) = ( ( 𝐾 ‘ 𝑔 ) ∪ { 𝑣 } ) )
35 34 fveqeq2d ⊢ ( 𝑠 = ( 𝐾 ‘ 𝑔 ) → ( ( ( LSpan ‘ 𝑊 ) ‘ ( 𝑠 ∪ { 𝑣 } ) ) = 𝑉 ↔ ( ( LSpan ‘ 𝑊 ) ‘ ( ( 𝐾 ‘ 𝑔 ) ∪ { 𝑣 } ) ) = 𝑉 ) )
36 35 rexbidv ⊢ ( 𝑠 = ( 𝐾 ‘ 𝑔 ) → ( ∃ 𝑣 ∈ 𝑉 ( ( LSpan ‘ 𝑊 ) ‘ ( 𝑠 ∪ { 𝑣 } ) ) = 𝑉 ↔ ∃ 𝑣 ∈ 𝑉 ( ( LSpan ‘ 𝑊 ) ‘ ( ( 𝐾 ‘ 𝑔 ) ∪ { 𝑣 } ) ) = 𝑉 ) )
37 32 33 36 3anbi123d ⊢ ( 𝑠 = ( 𝐾 ‘ 𝑔 ) → ( ( 𝑠 ∈ ( LSubSp ‘ 𝑊 ) ∧ 𝑠 ≠ 𝑉 ∧ ∃ 𝑣 ∈ 𝑉 ( ( LSpan ‘ 𝑊 ) ‘ ( 𝑠 ∪ { 𝑣 } ) ) = 𝑉 ) ↔ ( ( 𝐾 ‘ 𝑔 ) ∈ ( LSubSp ‘ 𝑊 ) ∧ ( 𝐾 ‘ 𝑔 ) ≠ 𝑉 ∧ ∃ 𝑣 ∈ 𝑉 ( ( LSpan ‘ 𝑊 ) ‘ ( ( 𝐾 ‘ 𝑔 ) ∪ { 𝑣 } ) ) = 𝑉 ) ) )
38 37 adantl ⊢ ( ( 𝑔 ≠ ( 𝑉 × { 0 } ) ∧ 𝑠 = ( 𝐾 ‘ 𝑔 ) ) → ( ( 𝑠 ∈ ( LSubSp ‘ 𝑊 ) ∧ 𝑠 ≠ 𝑉 ∧ ∃ 𝑣 ∈ 𝑉 ( ( LSpan ‘ 𝑊 ) ‘ ( 𝑠 ∪ { 𝑣 } ) ) = 𝑉 ) ↔ ( ( 𝐾 ‘ 𝑔 ) ∈ ( LSubSp ‘ 𝑊 ) ∧ ( 𝐾 ‘ 𝑔 ) ≠ 𝑉 ∧ ∃ 𝑣 ∈ 𝑉 ( ( LSpan ‘ 𝑊 ) ‘ ( ( 𝐾 ‘ 𝑔 ) ∪ { 𝑣 } ) ) = 𝑉 ) ) )
39 38 3ad2ant3 ⊢ ( ( 𝑊 ∈ LVec ∧ 𝑔 ∈ 𝐹 ∧ ( 𝑔 ≠ ( 𝑉 × { 0 } ) ∧ 𝑠 = ( 𝐾 ‘ 𝑔 ) ) ) → ( ( 𝑠 ∈ ( LSubSp ‘ 𝑊 ) ∧ 𝑠 ≠ 𝑉 ∧ ∃ 𝑣 ∈ 𝑉 ( ( LSpan ‘ 𝑊 ) ‘ ( 𝑠 ∪ { 𝑣 } ) ) = 𝑉 ) ↔ ( ( 𝐾 ‘ 𝑔 ) ∈ ( LSubSp ‘ 𝑊 ) ∧ ( 𝐾 ‘ 𝑔 ) ≠ 𝑉 ∧ ∃ 𝑣 ∈ 𝑉 ( ( LSpan ‘ 𝑊 ) ‘ ( ( 𝐾 ‘ 𝑔 ) ∪ { 𝑣 } ) ) = 𝑉 ) ) )
40 31 39 mpbird ⊢ ( ( 𝑊 ∈ LVec ∧ 𝑔 ∈ 𝐹 ∧ ( 𝑔 ≠ ( 𝑉 × { 0 } ) ∧ 𝑠 = ( 𝐾 ‘ 𝑔 ) ) ) → ( 𝑠 ∈ ( LSubSp ‘ 𝑊 ) ∧ 𝑠 ≠ 𝑉 ∧ ∃ 𝑣 ∈ 𝑉 ( ( LSpan ‘ 𝑊 ) ‘ ( 𝑠 ∪ { 𝑣 } ) ) = 𝑉 ) )
41 40 rexlimdv3a ⊢ ( 𝑊 ∈ LVec → ( ∃ 𝑔 ∈ 𝐹 ( 𝑔 ≠ ( 𝑉 × { 0 } ) ∧ 𝑠 = ( 𝐾 ‘ 𝑔 ) ) → ( 𝑠 ∈ ( LSubSp ‘ 𝑊 ) ∧ 𝑠 ≠ 𝑉 ∧ ∃ 𝑣 ∈ 𝑉 ( ( LSpan ‘ 𝑊 ) ‘ ( 𝑠 ∪ { 𝑣 } ) ) = 𝑉 ) ) )
42 1 27 28 4 islshp ⊢ ( 𝑊 ∈ LVec → ( 𝑠 ∈ 𝐻 ↔ ( 𝑠 ∈ ( LSubSp ‘ 𝑊 ) ∧ 𝑠 ≠ 𝑉 ∧ ∃ 𝑣 ∈ 𝑉 ( ( LSpan ‘ 𝑊 ) ‘ ( 𝑠 ∪ { 𝑣 } ) ) = 𝑉 ) ) )
43 41 42 sylibrd ⊢ ( 𝑊 ∈ LVec → ( ∃ 𝑔 ∈ 𝐹 ( 𝑔 ≠ ( 𝑉 × { 0 } ) ∧ 𝑠 = ( 𝐾 ‘ 𝑔 ) ) → 𝑠 ∈ 𝐻 ) )
44 24 43 impbid ⊢ ( 𝑊 ∈ LVec → ( 𝑠 ∈ 𝐻 ↔ ∃ 𝑔 ∈ 𝐹 ( 𝑔 ≠ ( 𝑉 × { 0 } ) ∧ 𝑠 = ( 𝐾 ‘ 𝑔 ) ) ) )
45 44 abbi2dv ⊢ ( 𝑊 ∈ LVec → 𝐻 = { 𝑠 ∣ ∃ 𝑔 ∈ 𝐹 ( 𝑔 ≠ ( 𝑉 × { 0 } ) ∧ 𝑠 = ( 𝐾 ‘ 𝑔 ) ) } )