Metamath Proof Explorer

Theorem islshpkrN

Description: The predicate "is a hyperplane" (of a left module or left vector space). TODO: should it be U = ( Kg ) or ( Kg ) = U as in lshpkrex ? Both standards seem to be used randomly throughout set.mm; we should decide on a preferred one. (Contributed by NM, 7-Oct-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 islshpkrN 
|- ( W e. LVec -> ( U e. H <-> E. g e. F ( g =/= ( V X. { .0. } ) /\ U = ( 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 1 2 3 4 5 6 lshpset2N 
 |-  ( W e. LVec -> H = { s | E. g e. F ( g =/= ( V X. { .0. } ) /\ s = ( K ` g ) ) } )
8 7 eleq2d 
 |-  ( W e. LVec -> ( U e. H <-> U e. { s | E. g e. F ( g =/= ( V X. { .0. } ) /\ s = ( K ` g ) ) } ) )
9 elex 
 |-  ( U e. { s | E. g e. F ( g =/= ( V X. { .0. } ) /\ s = ( K ` g ) ) } -> U e. _V )
10 9 adantl 
 |-  ( ( W e. LVec /\ U e. { s | E. g e. F ( g =/= ( V X. { .0. } ) /\ s = ( K ` g ) ) } ) -> U e. _V )
11 fvex 
 |-  ( K ` g ) e. _V
12 eleq1 
 |-  ( U = ( K ` g ) -> ( U e. _V <-> ( K ` g ) e. _V ) )
13 11 12 mpbiri 
 |-  ( U = ( K ` g ) -> U e. _V )
14 13 adantl 
 |-  ( ( g =/= ( V X. { .0. } ) /\ U = ( K ` g ) ) -> U e. _V )
15 14 rexlimivw 
 |-  ( E. g e. F ( g =/= ( V X. { .0. } ) /\ U = ( K ` g ) ) -> U e. _V )
16 15 adantl 
 |-  ( ( W e. LVec /\ E. g e. F ( g =/= ( V X. { .0. } ) /\ U = ( K ` g ) ) ) -> U e. _V )
17 eqeq1 
 |-  ( s = U -> ( s = ( K ` g ) <-> U = ( K ` g ) ) )
18 17 anbi2d 
 |-  ( s = U -> ( ( g =/= ( V X. { .0. } ) /\ s = ( K ` g ) ) <-> ( g =/= ( V X. { .0. } ) /\ U = ( K ` g ) ) ) )
19 18 rexbidv 
 |-  ( s = U -> ( E. g e. F ( g =/= ( V X. { .0. } ) /\ s = ( K ` g ) ) <-> E. g e. F ( g =/= ( V X. { .0. } ) /\ U = ( K ` g ) ) ) )
20 19 elabg 
 |-  ( U e. _V -> ( U e. { s | E. g e. F ( g =/= ( V X. { .0. } ) /\ s = ( K ` g ) ) } <-> E. g e. F ( g =/= ( V X. { .0. } ) /\ U = ( K ` g ) ) ) )
21 10 16 20 pm5.21nd 
 |-  ( W e. LVec -> ( U e. { s | E. g e. F ( g =/= ( V X. { .0. } ) /\ s = ( K ` g ) ) } <-> E. g e. F ( g =/= ( V X. { .0. } ) /\ U = ( K ` g ) ) ) )
22 8 21 bitrd 
 |-  ( W e. LVec -> ( U e. H <-> E. g e. F ( g =/= ( V X. { .0. } ) /\ U = ( K ` g ) ) ) )