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

Metamath Proof Explorer

Theorem islshp

Description: The predicate "is a hyperplane" (of a left module or left vector space). (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 islshp 
|- ( W e. X -> ( U e. H <-> ( U e. S /\ U =/= V /\ E. v e. V ( N ` ( U 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 1 2 3 4 lshpset 
 |-  ( W e. X -> H = { s e. S | ( s =/= V /\ E. v e. V ( N ` ( s u. { v } ) ) = V ) } )
6 5 eleq2d 
 |-  ( W e. X -> ( U e. H <-> U e. { s e. S | ( s =/= V /\ E. v e. V ( N ` ( s u. { v } ) ) = V ) } ) )
7 neeq1 
 |-  ( s = U -> ( s =/= V <-> U =/= V ) )
8 uneq1 
 |-  ( s = U -> ( s u. { v } ) = ( U u. { v } ) )
9 8 fveqeq2d 
 |-  ( s = U -> ( ( N ` ( s u. { v } ) ) = V <-> ( N ` ( U u. { v } ) ) = V ) )
10 9 rexbidv 
 |-  ( s = U -> ( E. v e. V ( N ` ( s u. { v } ) ) = V <-> E. v e. V ( N ` ( U u. { v } ) ) = V ) )
11 7 10 anbi12d 
 |-  ( s = U -> ( ( s =/= V /\ E. v e. V ( N ` ( s u. { v } ) ) = V ) <-> ( U =/= V /\ E. v e. V ( N ` ( U u. { v } ) ) = V ) ) )
12 11 elrab 
 |-  ( U e. { s e. S | ( s =/= V /\ E. v e. V ( N ` ( s u. { v } ) ) = V ) } <-> ( U e. S /\ ( U =/= V /\ E. v e. V ( N ` ( U u. { v } ) ) = V ) ) )
13 3anass 
 |-  ( ( U e. S /\ U =/= V /\ E. v e. V ( N ` ( U u. { v } ) ) = V ) <-> ( U e. S /\ ( U =/= V /\ E. v e. V ( N ` ( U u. { v } ) ) = V ) ) )
14 12 13 bitr4i 
 |-  ( U e. { s e. S | ( s =/= V /\ E. v e. V ( N ` ( s u. { v } ) ) = V ) } <-> ( U e. S /\ U =/= V /\ E. v e. V ( N ` ( U u. { v } ) ) = V ) )
15 6 14 bitrdi 
 |-  ( W e. X -> ( U e. H <-> ( U e. S /\ U =/= V /\ E. v e. V ( N ` ( U u. { v } ) ) = V ) ) )