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	$⊢ \underset{˙}{\lor} = join (K)$
	dlatjmdi.m	$⊢ \underset{˙}{\land} = meet (K)$
Assertion	dlatjmdi	$⊢ (K \in DLat \land (X \in B \land Y \in B \land Z \in B)) \to X \underset{˙}{\lor} (Y \underset{˙}{\land} Z) = (X \underset{˙}{\lor} Y) \underset{˙}{\land} (X \underset{˙}{\lor} Z)$

Step	Hyp	Ref	Expression
1		dlatjmdi.b	$⊢ B = {Base}_{K}$
2		dlatjmdi.j	$⊢ \underset{˙}{\lor} = join (K)$
3		dlatjmdi.m	$⊢ \underset{˙}{\land} = meet (K)$
4		eqid	$⊢ ODual (K) = ODual (K)$
5	4	odudlatb	$⊢ K \in DLat \to (K \in DLat \leftrightarrow ODual (K) \in DLat)$
6	5	ibi	$⊢ K \in DLat \to ODual (K) \in DLat$
7	4 1	odubas	$⊢ B = {Base}_{ODual (K)}$
8	4 3	odujoin	$⊢ \underset{˙}{\land} = join (ODual (K))$
9	4 2	odumeet	$⊢ \underset{˙}{\lor} = meet (ODual (K))$
10	7 8 9	dlatmjdi	$⊢ (ODual (K) \in DLat \land (X \in B \land Y \in B \land Z \in B)) \to X \underset{˙}{\lor} (Y \underset{˙}{\land} Z) = (X \underset{˙}{\lor} Y) \underset{˙}{\land} (X \underset{˙}{\lor} Z)$
11	6 10	sylan	$⊢ (K \in DLat \land (X \in B \land Y \in B \land Z \in B)) \to X \underset{˙}{\lor} (Y \underset{˙}{\land} Z) = (X \underset{˙}{\lor} Y) \underset{˙}{\land} (X \underset{˙}{\lor} Z)$

Metamath Proof Explorer