Theorem latmass

Description: Lattice meet is associative. (Contributed by Stefan O'Rear, 30-Jan-2015)

	Ref	Expression
Hypotheses	latmass.b	|- B = ( Base ` K )
	latmass.m	|- ./\ = ( meet ` K )
Assertion	latmass	|- ( ( K e. Lat /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> ( ( X ./\ Y ) ./\ Z ) = ( X ./\ ( Y ./\ Z ) ) )

Proof

Step	Hyp	Ref	Expression
1		latmass.b	|- B = ( Base ` K )
2		latmass.m	|- ./\ = ( meet ` K )
3		eqid	|- ( ODual ` K ) = ( ODual ` K )
4	3	odulat	|- ( K e. Lat -> ( ODual ` K ) e. Lat )
5	3 1	odubas	|- B = ( Base ` ( ODual ` K ) )
6	3 2	odujoin	|- ./\ = ( join ` ( ODual ` K ) )
7	5 6	latjass	|- ( ( ( ODual ` K ) e. Lat /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> ( ( X ./\ Y ) ./\ Z ) = ( X ./\ ( Y ./\ Z ) ) )
8	4 7	sylan	|- ( ( K e. Lat /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> ( ( X ./\ Y ) ./\ Z ) = ( X ./\ ( Y ./\ Z ) ) )