This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem lshpset

Description: The set of all hyperplanes of a left module or left vector space. The vector v is called a generating vector for the hyperplane. (Contributed by NM, 29-Jun-2014)

Ref Expression
Hypotheses lshpset.v 
|- V = ( Base ` W )
lshpset.n 
|- N = ( LSpan ` W )
lshpset.s 
|- S = ( LSubSp ` W )
lshpset.h 
|- H = ( LSHyp ` W )
Assertion lshpset 
|- ( W e. X -> H = { s e. S | ( s =/= V /\ E. v e. V ( N ` ( s u. { v } ) ) = V ) } )

Proof

Step Hyp Ref Expression
1 lshpset.v 
 |-  V = ( Base ` W )
2 lshpset.n 
 |-  N = ( LSpan ` W )
3 lshpset.s 
 |-  S = ( LSubSp ` W )
4 lshpset.h 
 |-  H = ( LSHyp ` W )
5 elex 
 |-  ( W e. X -> W e. _V )
6 fveq2 
 |-  ( w = W -> ( LSubSp ` w ) = ( LSubSp ` W ) )
7 6 3 eqtr4di 
 |-  ( w = W -> ( LSubSp ` w ) = S )
8 fveq2 
 |-  ( w = W -> ( Base ` w ) = ( Base ` W ) )
9 8 1 eqtr4di 
 |-  ( w = W -> ( Base ` w ) = V )
10 9 neeq2d 
 |-  ( w = W -> ( s =/= ( Base ` w ) <-> s =/= V ) )
11 fveq2 
 |-  ( w = W -> ( LSpan ` w ) = ( LSpan ` W ) )
12 11 2 eqtr4di 
 |-  ( w = W -> ( LSpan ` w ) = N )
13 12 fveq1d 
 |-  ( w = W -> ( ( LSpan ` w ) ` ( s u. { v } ) ) = ( N ` ( s u. { v } ) ) )
14 13 9 eqeq12d 
 |-  ( w = W -> ( ( ( LSpan ` w ) ` ( s u. { v } ) ) = ( Base ` w ) <-> ( N ` ( s u. { v } ) ) = V ) )
15 9 14 rexeqbidv 
 |-  ( w = W -> ( E. v e. ( Base ` w ) ( ( LSpan ` w ) ` ( s u. { v } ) ) = ( Base ` w ) <-> E. v e. V ( N ` ( s u. { v } ) ) = V ) )
16 10 15 anbi12d 
 |-  ( w = W -> ( ( s =/= ( Base ` w ) /\ E. v e. ( Base ` w ) ( ( LSpan ` w ) ` ( s u. { v } ) ) = ( Base ` w ) ) <-> ( s =/= V /\ E. v e. V ( N ` ( s u. { v } ) ) = V ) ) )
17 7 16 rabeqbidv 
 |-  ( w = W -> { s e. ( LSubSp ` w ) | ( s =/= ( Base ` w ) /\ E. v e. ( Base ` w ) ( ( LSpan ` w ) ` ( s u. { v } ) ) = ( Base ` w ) ) } = { s e. S | ( s =/= V /\ E. v e. V ( N ` ( s u. { v } ) ) = V ) } )
18 df-lshyp 
 |-  LSHyp = ( w e. _V |-> { s e. ( LSubSp ` w ) | ( s =/= ( Base ` w ) /\ E. v e. ( Base ` w ) ( ( LSpan ` w ) ` ( s u. { v } ) ) = ( Base ` w ) ) } )
19 3 fvexi 
 |-  S e. _V
20 19 rabex 
 |-  { s e. S | ( s =/= V /\ E. v e. V ( N ` ( s u. { v } ) ) = V ) } e. _V
21 17 18 20 fvmpt 
 |-  ( W e. _V -> ( LSHyp ` W ) = { s e. S | ( s =/= V /\ E. v e. V ( N ` ( s u. { v } ) ) = V ) } )
22 5 21 syl 
 |-  ( W e. X -> ( LSHyp ` W ) = { s e. S | ( s =/= V /\ E. v e. V ( N ` ( s u. { v } ) ) = V ) } )
23 4 22 eqtrid 
 |-  ( W e. X -> H = { s e. S | ( s =/= V /\ E. v e. V ( N ` ( s u. { v } ) ) = V ) } )