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

Metamath Proof Explorer

Theorem lhpset

Description: The set of co-atoms (lattice hyperplanes). (Contributed by NM, 11-May-2012)

Ref Expression
Hypotheses lhpset.b 
|- B = ( Base ` K )
lhpset.u 
|- .1. = ( 1. ` K )
lhpset.c 
|- C = (
lhpset.h 
|- H = ( LHyp ` K )
Assertion lhpset 
|- ( K e. A -> H = { w e. B | w C .1. } )

Proof

Step Hyp Ref Expression
1 lhpset.b 
 |-  B = ( Base ` K )
2 lhpset.u 
 |-  .1. = ( 1. ` K )
3 lhpset.c 
 |-  C = (
4 lhpset.h 
 |-  H = ( LHyp ` K )
5 elex 
 |-  ( K e. A -> K e. _V )
6 fveq2 
 |-  ( k = K -> ( Base ` k ) = ( Base ` K ) )
7 6 1 eqtr4di 
 |-  ( k = K -> ( Base ` k ) = B )
8 eqidd 
 |-  ( k = K -> w = w )
9 fveq2 
 |-  ( k = K -> (
10 9 3 eqtr4di 
 |-  ( k = K -> (
11 fveq2 
 |-  ( k = K -> ( 1. ` k ) = ( 1. ` K ) )
12 11 2 eqtr4di 
 |-  ( k = K -> ( 1. ` k ) = .1. )
13 8 10 12 breq123d 
 |-  ( k = K -> ( w (  w C .1. ) )
14 7 13 rabeqbidv 
 |-  ( k = K -> { w e. ( Base ` k ) | w (
15 df-lhyp 
 |-  LHyp = ( k e. _V |-> { w e. ( Base ` k ) | w (
16 1 fvexi 
 |-  B e. _V
17 16 rabex 
 |-  { w e. B | w C .1. } e. _V
18 14 15 17 fvmpt 
 |-  ( K e. _V -> ( LHyp ` K ) = { w e. B | w C .1. } )
19 4 18 eqtrid 
 |-  ( K e. _V -> H = { w e. B | w C .1. } )
20 5 19 syl 
 |-  ( K e. A -> H = { w e. B | w C .1. } )