hlatjrot

Description: Rotate lattice join of 3 classes. Frequently-used special case of latjrot for atoms. (Contributed by NM, 2-Aug-2012)

	Ref	Expression
Hypotheses	hlatjcom.j	$⊢ \underset{˙}{\lor} = join (K)$
	hlatjcom.a	$⊢ A = Atoms (K)$
Assertion	hlatjrot	$⊢ (K \in HL \land (P \in A \land Q \in A \land R \in A)) \to (P \underset{˙}{\lor} Q) \underset{˙}{\lor} R = (R \underset{˙}{\lor} P) \underset{˙}{\lor} Q$

Step	Hyp	Ref	Expression
1		hlatjcom.j	$⊢ \underset{˙}{\lor} = join (K)$
2		hlatjcom.a	$⊢ A = Atoms (K)$
3	1 2	hlatj32	$⊢ (K \in HL \land (P \in A \land Q \in A \land R \in A)) \to (P \underset{˙}{\lor} Q) \underset{˙}{\lor} R = (P \underset{˙}{\lor} R) \underset{˙}{\lor} Q$
4	1 2	hlatjcom	$⊢ (K \in HL \land P \in A \land R \in A) \to P \underset{˙}{\lor} R = R \underset{˙}{\lor} P$
5	4	3adant3r2	$⊢ (K \in HL \land (P \in A \land Q \in A \land R \in A)) \to P \underset{˙}{\lor} R = R \underset{˙}{\lor} P$
6	5	oveq1d	$⊢ (K \in HL \land (P \in A \land Q \in A \land R \in A)) \to (P \underset{˙}{\lor} R) \underset{˙}{\lor} Q = (R \underset{˙}{\lor} P) \underset{˙}{\lor} Q$
7	3 6	eqtrd	$⊢ (K \in HL \land (P \in A \land Q \in A \land R \in A)) \to (P \underset{˙}{\lor} Q) \underset{˙}{\lor} R = (R \underset{˙}{\lor} P) \underset{˙}{\lor} Q$

Metamath Proof Explorer