Metamath Proof Explorer

Theorem hlatj12

Description: Swap 1st and 2nd members of lattice join. Frequently-used special case of latj32 for atoms. (Contributed by NM, 4-Jun-2012)

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

Proof

Step	Hyp	Ref	Expression
1		hlatjcom.j	$⊢ \underset{˙}{\lor} = join (K)$
2		hlatjcom.a	$⊢ A = Atoms (K)$
3	1 2	hlatjcom	$⊢ (K \in HL \land P \in A \land Q \in A) \to P \underset{˙}{\lor} Q = Q \underset{˙}{\lor} P$
4	3	3adant3r3	$⊢ (K \in HL \land (P \in A \land Q \in A \land R \in A)) \to P \underset{˙}{\lor} Q = Q \underset{˙}{\lor} P$
5	4	oveq1d	$⊢ (K \in HL \land (P \in A \land Q \in A \land R \in A)) \to (P \underset{˙}{\lor} Q) \underset{˙}{\lor} R = (Q \underset{˙}{\lor} P) \underset{˙}{\lor} R$
6	1 2	hlatjass	$⊢ (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} (Q \underset{˙}{\lor} R)$
7		simpl	$⊢ (K \in HL \land (P \in A \land Q \in A \land R \in A)) \to K \in HL$
8		simpr2	$⊢ (K \in HL \land (P \in A \land Q \in A \land R \in A)) \to Q \in A$
9		simpr1	$⊢ (K \in HL \land (P \in A \land Q \in A \land R \in A)) \to P \in A$
10		simpr3	$⊢ (K \in HL \land (P \in A \land Q \in A \land R \in A)) \to R \in A$
11	1 2	hlatjass	$⊢ (K \in HL \land (Q \in A \land P \in A \land R \in A)) \to (Q \underset{˙}{\lor} P) \underset{˙}{\lor} R = Q \underset{˙}{\lor} (P \underset{˙}{\lor} R)$
12	7 8 9 10 11	syl13anc	$⊢ (K \in HL \land (P \in A \land Q \in A \land R \in A)) \to (Q \underset{˙}{\lor} P) \underset{˙}{\lor} R = Q \underset{˙}{\lor} (P \underset{˙}{\lor} R)$
13	5 6 12	3eqtr3d	$⊢ (K \in HL \land (P \in A \land Q \in A \land R \in A)) \to P \underset{˙}{\lor} (Q \underset{˙}{\lor} R) = Q \underset{˙}{\lor} (P \underset{˙}{\lor} R)$