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. } )