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 
|- V = ( Base ` W )
lshpset2.d 
|- D = ( Scalar ` W )
lshpset2.z 
|- .0. = ( 0g ` D )
lshpset2.h 
|- H = ( LSHyp ` W )
lshpset2.f 
|- F = ( LFnl ` W )
lshpset2.k 
|- K = ( LKer ` W )
Assertion lshpset2N 
|- ( W e. LVec -> H = { s | E. g e. F ( g =/= ( V X. { .0. } ) /\ s = ( K ` g ) ) } )

Proof

Step Hyp Ref Expression
1 lshpset2.v 
 |-  V = ( Base ` W )
2 lshpset2.d 
 |-  D = ( Scalar ` W )
3 lshpset2.z 
 |-  .0. = ( 0g ` D )
4 lshpset2.h 
 |-  H = ( LSHyp ` W )
5 lshpset2.f 
 |-  F = ( LFnl ` W )
6 lshpset2.k 
 |-  K = ( LKer ` W )
7 4 5 6 lshpkrex 
 |-  ( ( W e. LVec /\ s e. H ) -> E. g e. F ( K ` g ) = s )
8 eleq1 
 |-  ( ( K ` g ) = s -> ( ( K ` g ) e. H <-> s e. H ) )
9 8 biimparc 
 |-  ( ( s e. H /\ ( K ` g ) = s ) -> ( K ` g ) e. H )
10 9 adantll 
 |-  ( ( ( W e. LVec /\ s e. H ) /\ ( K ` g ) = s ) -> ( K ` g ) e. H )
11 10 adantlr 
 |-  ( ( ( ( W e. LVec /\ s e. H ) /\ g e. F ) /\ ( K ` g ) = s ) -> ( K ` g ) e. H )
12 simplll 
 |-  ( ( ( ( W e. LVec /\ s e. H ) /\ g e. F ) /\ ( K ` g ) = s ) -> W e. LVec )
13 simplr 
 |-  ( ( ( ( W e. LVec /\ s e. H ) /\ g e. F ) /\ ( K ` g ) = s ) -> g e. F )
14 1 2 3 4 5 6 12 13 lkrshp3 
 |-  ( ( ( ( W e. LVec /\ s e. H ) /\ g e. F ) /\ ( K ` g ) = s ) -> ( ( K ` g ) e. H <-> g =/= ( V X. { .0. } ) ) )
15 11 14 mpbid 
 |-  ( ( ( ( W e. LVec /\ s e. H ) /\ g e. F ) /\ ( K ` g ) = s ) -> g =/= ( V X. { .0. } ) )
16 15 ex 
 |-  ( ( ( W e. LVec /\ s e. H ) /\ g e. F ) -> ( ( K ` g ) = s -> g =/= ( V X. { .0. } ) ) )
17 eqimss2 
 |-  ( ( K ` g ) = s -> s C_ ( K ` g ) )
18 eqimss 
 |-  ( ( K ` g ) = s -> ( K ` g ) C_ s )
19 17 18 eqssd 
 |-  ( ( K ` g ) = s -> s = ( K ` g ) )
20 19 a1i 
 |-  ( ( ( W e. LVec /\ s e. H ) /\ g e. F ) -> ( ( K ` g ) = s -> s = ( K ` g ) ) )
21 16 20 jcad 
 |-  ( ( ( W e. LVec /\ s e. H ) /\ g e. F ) -> ( ( K ` g ) = s -> ( g =/= ( V X. { .0. } ) /\ s = ( K ` g ) ) ) )
22 21 reximdva 
 |-  ( ( W e. LVec /\ s e. H ) -> ( E. g e. F ( K ` g ) = s -> E. g e. F ( g =/= ( V X. { .0. } ) /\ s = ( K ` g ) ) ) )
23 7 22 mpd 
 |-  ( ( W e. LVec /\ s e. H ) -> E. g e. F ( g =/= ( V X. { .0. } ) /\ s = ( K ` g ) ) )
24 23 ex 
 |-  ( W e. LVec -> ( s e. H -> E. g e. F ( g =/= ( V X. { .0. } ) /\ s = ( K ` g ) ) ) )
25 1 2 3 4 5 6 lkrshp 
 |-  ( ( W e. LVec /\ g e. F /\ g =/= ( V X. { .0. } ) ) -> ( K ` g ) e. H )
26 25 3adant3r 
 |-  ( ( W e. LVec /\ g e. F /\ ( g =/= ( V X. { .0. } ) /\ s = ( K ` g ) ) ) -> ( K ` g ) e. H )
27 eqid 
 |-  ( LSpan ` W ) = ( LSpan ` W )
28 eqid 
 |-  ( LSubSp ` W ) = ( LSubSp ` W )
29 1 27 28 4 islshp 
 |-  ( W e. LVec -> ( ( K ` g ) e. H <-> ( ( K ` g ) e. ( LSubSp ` W ) /\ ( K ` g ) =/= V /\ E. v e. V ( ( LSpan ` W ) ` ( ( K ` g ) u. { v } ) ) = V ) ) )
30 29 3ad2ant1 
 |-  ( ( W e. LVec /\ g e. F /\ ( g =/= ( V X. { .0. } ) /\ s = ( K ` g ) ) ) -> ( ( K ` g ) e. H <-> ( ( K ` g ) e. ( LSubSp ` W ) /\ ( K ` g ) =/= V /\ E. v e. V ( ( LSpan ` W ) ` ( ( K ` g ) u. { v } ) ) = V ) ) )
31 26 30 mpbid 
 |-  ( ( W e. LVec /\ g e. F /\ ( g =/= ( V X. { .0. } ) /\ s = ( K ` g ) ) ) -> ( ( K ` g ) e. ( LSubSp ` W ) /\ ( K ` g ) =/= V /\ E. v e. V ( ( LSpan ` W ) ` ( ( K ` g ) u. { v } ) ) = V ) )
32 eleq1 
 |-  ( s = ( K ` g ) -> ( s e. ( LSubSp ` W ) <-> ( K ` g ) e. ( LSubSp ` W ) ) )
33 neeq1 
 |-  ( s = ( K ` g ) -> ( s =/= V <-> ( K ` g ) =/= V ) )
34 uneq1 
 |-  ( s = ( K ` g ) -> ( s u. { v } ) = ( ( K ` g ) u. { v } ) )
35 34 fveqeq2d 
 |-  ( s = ( K ` g ) -> ( ( ( LSpan ` W ) ` ( s u. { v } ) ) = V <-> ( ( LSpan ` W ) ` ( ( K ` g ) u. { v } ) ) = V ) )
36 35 rexbidv 
 |-  ( s = ( K ` g ) -> ( E. v e. V ( ( LSpan ` W ) ` ( s u. { v } ) ) = V <-> E. v e. V ( ( LSpan ` W ) ` ( ( K ` g ) u. { v } ) ) = V ) )
37 32 33 36 3anbi123d 
 |-  ( s = ( K ` g ) -> ( ( s e. ( LSubSp ` W ) /\ s =/= V /\ E. v e. V ( ( LSpan ` W ) ` ( s u. { v } ) ) = V ) <-> ( ( K ` g ) e. ( LSubSp ` W ) /\ ( K ` g ) =/= V /\ E. v e. V ( ( LSpan ` W ) ` ( ( K ` g ) u. { v } ) ) = V ) ) )
38 37 adantl 
 |-  ( ( g =/= ( V X. { .0. } ) /\ s = ( K ` g ) ) -> ( ( s e. ( LSubSp ` W ) /\ s =/= V /\ E. v e. V ( ( LSpan ` W ) ` ( s u. { v } ) ) = V ) <-> ( ( K ` g ) e. ( LSubSp ` W ) /\ ( K ` g ) =/= V /\ E. v e. V ( ( LSpan ` W ) ` ( ( K ` g ) u. { v } ) ) = V ) ) )
39 38 3ad2ant3 
 |-  ( ( W e. LVec /\ g e. F /\ ( g =/= ( V X. { .0. } ) /\ s = ( K ` g ) ) ) -> ( ( s e. ( LSubSp ` W ) /\ s =/= V /\ E. v e. V ( ( LSpan ` W ) ` ( s u. { v } ) ) = V ) <-> ( ( K ` g ) e. ( LSubSp ` W ) /\ ( K ` g ) =/= V /\ E. v e. V ( ( LSpan ` W ) ` ( ( K ` g ) u. { v } ) ) = V ) ) )
40 31 39 mpbird 
 |-  ( ( W e. LVec /\ g e. F /\ ( g =/= ( V X. { .0. } ) /\ s = ( K ` g ) ) ) -> ( s e. ( LSubSp ` W ) /\ s =/= V /\ E. v e. V ( ( LSpan ` W ) ` ( s u. { v } ) ) = V ) )
41 40 rexlimdv3a 
 |-  ( W e. LVec -> ( E. g e. F ( g =/= ( V X. { .0. } ) /\ s = ( K ` g ) ) -> ( s e. ( LSubSp ` W ) /\ s =/= V /\ E. v e. V ( ( LSpan ` W ) ` ( s u. { v } ) ) = V ) ) )
42 1 27 28 4 islshp 
 |-  ( W e. LVec -> ( s e. H <-> ( s e. ( LSubSp ` W ) /\ s =/= V /\ E. v e. V ( ( LSpan ` W ) ` ( s u. { v } ) ) = V ) ) )
43 41 42 sylibrd 
 |-  ( W e. LVec -> ( E. g e. F ( g =/= ( V X. { .0. } ) /\ s = ( K ` g ) ) -> s e. H ) )
44 24 43 impbid 
 |-  ( W e. LVec -> ( s e. H <-> E. g e. F ( g =/= ( V X. { .0. } ) /\ s = ( K ` g ) ) ) )
45 44 abbi2dv 
 |-  ( W e. LVec -> H = { s | E. g e. F ( g =/= ( V X. { .0. } ) /\ s = ( K ` g ) ) } )