Theorem dlatjmdi

Description: In a distributive lattice, joins distribute over meets. (Contributed by Stefan O'Rear, 30-Jan-2015)

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

Proof

Step	Hyp	Ref	Expression
1		dlatjmdi.b	|- B = ( Base ` K )
2		dlatjmdi.j	|- .\/ = ( join ` K )
3		dlatjmdi.m	|- ./\ = ( meet ` K )
4		eqid	|- ( ODual ` K ) = ( ODual ` K )
5	4	odudlatb	|- ( K e. DLat -> ( K e. DLat <-> ( ODual ` K ) e. DLat ) )
6	5	ibi	|- ( K e. DLat -> ( ODual ` K ) e. DLat )
7	4 1	odubas	|- B = ( Base ` ( ODual ` K ) )
8	4 3	odujoin	|- ./\ = ( join ` ( ODual ` K ) )
9	4 2	odumeet	|- .\/ = ( meet ` ( ODual ` K ) )
10	7 8 9	dlatmjdi	|- ( ( ( ODual ` K ) e. DLat /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> ( X .\/ ( Y ./\ Z ) ) = ( ( X .\/ Y ) ./\ ( X .\/ Z ) ) )
11	6 10	sylan	|- ( ( K e. DLat /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> ( X .\/ ( Y ./\ Z ) ) = ( ( X .\/ Y ) ./\ ( X .\/ Z ) ) )