latjjdir

Description: Lattice join distributes over itself. (Contributed by NM, 2-Aug-2012)

	Ref	Expression
Hypotheses	latjass.b	$⊢ B = {Base}_{K}$
	latjass.j	$⊢ \underset{˙}{\lor} = join (K)$
Assertion	latjjdir	$⊢ (K \in Lat \land (X \in B \land Y \in B \land Z \in B)) \to (X \underset{˙}{\lor} Y) \underset{˙}{\lor} Z = (X \underset{˙}{\lor} Z) \underset{˙}{\lor} (Y \underset{˙}{\lor} Z)$

Step	Hyp	Ref	Expression
1		latjass.b	$⊢ B = {Base}_{K}$
2		latjass.j	$⊢ \underset{˙}{\lor} = join (K)$
3	1 2	latjidm	$⊢ (K \in Lat \land Z \in B) \to Z \underset{˙}{\lor} Z = Z$
4	3	3ad2antr3	$⊢ (K \in Lat \land (X \in B \land Y \in B \land Z \in B)) \to Z \underset{˙}{\lor} Z = Z$
5	4	oveq2d	$⊢ (K \in Lat \land (X \in B \land Y \in B \land Z \in B)) \to (X \underset{˙}{\lor} Y) \underset{˙}{\lor} (Z \underset{˙}{\lor} Z) = (X \underset{˙}{\lor} Y) \underset{˙}{\lor} Z$
6		simpl	$⊢ (K \in Lat \land (X \in B \land Y \in B \land Z \in B)) \to K \in Lat$
7		simpr1	$⊢ (K \in Lat \land (X \in B \land Y \in B \land Z \in B)) \to X \in B$
8		simpr2	$⊢ (K \in Lat \land (X \in B \land Y \in B \land Z \in B)) \to Y \in B$
9		simpr3	$⊢ (K \in Lat \land (X \in B \land Y \in B \land Z \in B)) \to Z \in B$
10	1 2	latj4	$⊢ (K \in Lat \land (X \in B \land Y \in B) \land (Z \in B \land Z \in B)) \to (X \underset{˙}{\lor} Y) \underset{˙}{\lor} (Z \underset{˙}{\lor} Z) = (X \underset{˙}{\lor} Z) \underset{˙}{\lor} (Y \underset{˙}{\lor} Z)$
11	6 7 8 9 9 10	syl122anc	$⊢ (K \in Lat \land (X \in B \land Y \in B \land Z \in B)) \to (X \underset{˙}{\lor} Y) \underset{˙}{\lor} (Z \underset{˙}{\lor} Z) = (X \underset{˙}{\lor} Z) \underset{˙}{\lor} (Y \underset{˙}{\lor} Z)$
12	5 11	eqtr3d	$⊢ (K \in Lat \land (X \in B \land Y \in B \land Z \in B)) \to (X \underset{˙}{\lor} Y) \underset{˙}{\lor} Z = (X \underset{˙}{\lor} Z) \underset{˙}{\lor} (Y \underset{˙}{\lor} Z)$

Metamath Proof Explorer