Metamath Proof Explorer

Theorem latj12

Description: Swap 1st and 2nd members of lattice join. ( chj12 analog.) (Contributed by NM, 4-Jun-2012)

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

Proof

Step	Hyp	Ref	Expression
1		latjass.b	$⊢ B = {Base}_{K}$
2		latjass.j	$⊢ \underset{˙}{\lor} = join (K)$
3	1 2	latjcom	$⊢ (K \in Lat \land X \in B \land Y \in B) \to X \underset{˙}{\lor} Y = Y \underset{˙}{\lor} X$
4	3	3adant3r3	$⊢ (K \in Lat \land (X \in B \land Y \in B \land Z \in B)) \to X \underset{˙}{\lor} Y = Y \underset{˙}{\lor} X$
5	4	oveq1d	$⊢ (K \in Lat \land (X \in B \land Y \in B \land Z \in B)) \to (X \underset{˙}{\lor} Y) \underset{˙}{\lor} Z = (Y \underset{˙}{\lor} X) \underset{˙}{\lor} Z$
6	1 2	latjass	$⊢ (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} (Y \underset{˙}{\lor} Z)$
7		simpl	$⊢ (K \in Lat \land (X \in B \land Y \in B \land Z \in B)) \to K \in Lat$
8		simpr2	$⊢ (K \in Lat \land (X \in B \land Y \in B \land Z \in B)) \to Y \in B$
9		simpr1	$⊢ (K \in Lat \land (X \in B \land Y \in B \land Z \in B)) \to X \in B$
10		simpr3	$⊢ (K \in Lat \land (X \in B \land Y \in B \land Z \in B)) \to Z \in B$
11	1 2	latjass	$⊢ (K \in Lat \land (Y \in B \land X \in B \land Z \in B)) \to (Y \underset{˙}{\lor} X) \underset{˙}{\lor} Z = Y \underset{˙}{\lor} (X \underset{˙}{\lor} Z)$
12	7 8 9 10 11	syl13anc	$⊢ (K \in Lat \land (X \in B \land Y \in B \land Z \in B)) \to (Y \underset{˙}{\lor} X) \underset{˙}{\lor} Z = Y \underset{˙}{\lor} (X \underset{˙}{\lor} Z)$
13	5 6 12	3eqtr3d	$⊢ (K \in Lat \land (X \in B \land Y \in B \land Z \in B)) \to X \underset{˙}{\lor} (Y \underset{˙}{\lor} Z) = Y \underset{˙}{\lor} (X \underset{˙}{\lor} Z)$