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 syl5eq
 |-  ( K e. _V -> H = { w e. B | w C .1. } )
20 5 19 syl
 |-  ( K e. A -> H = { w e. B | w C .1. } )