Theorem hlatle

Description: The ordering of two Hilbert lattice elements is determined by the atoms under them. ( chrelat3 analog.) (Contributed by NM, 4-Nov-2011)

	Ref	Expression
Hypotheses	hlatle.b	|- B = ( Base ` K )
	hlatle.l	|- .<_ = ( le ` K )
	hlatle.a	|- A = ( Atoms ` K )
Assertion	hlatle	|- ( ( K e. HL /\ X e. B /\ Y e. B ) -> ( X .<_ Y <-> A. p e. A ( p .<_ X -> p .<_ Y ) ) )

Proof

Step	Hyp	Ref	Expression
1		hlatle.b	|- B = ( Base ` K )
2		hlatle.l	|- .<_ = ( le ` K )
3		hlatle.a	|- A = ( Atoms ` K )
4		hlomcmat	|- ( K e. HL -> ( K e. OML /\ K e. CLat /\ K e. AtLat ) )
5	1 2 3	atlatle	|- ( ( ( K e. OML /\ K e. CLat /\ K e. AtLat ) /\ X e. B /\ Y e. B ) -> ( X .<_ Y <-> A. p e. A ( p .<_ X -> p .<_ Y ) ) )
6	4 5	syl3an1	|- ( ( K e. HL /\ X e. B /\ Y e. B ) -> ( X .<_ Y <-> A. p e. A ( p .<_ X -> p .<_ Y ) ) )