hlatjass

Description: Lattice join is associative. Frequently-used special case of latjass for atoms. (Contributed by NM, 27-Jul-2012)

	Ref	Expression
Hypotheses	hlatjcom.j	$⊢ \underset{˙}{\lor} = join (K)$
	hlatjcom.a	$⊢ A = Atoms (K)$
Assertion	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)$

Step	Hyp	Ref	Expression
1		hlatjcom.j	$⊢ \underset{˙}{\lor} = join (K)$
2		hlatjcom.a	$⊢ A = Atoms (K)$
3		hllat	$⊢ K \in HL \to K \in Lat$
4	3	adantr	$⊢ (K \in HL \land (P \in A \land Q \in A \land R \in A)) \to K \in Lat$
5		simpr1	$⊢ (K \in HL \land (P \in A \land Q \in A \land R \in A)) \to P \in A$
6		eqid	$⊢ {Base}_{K} = {Base}_{K}$
7	6 2	atbase	$⊢ P \in A \to P \in {Base}_{K}$
8	5 7	syl	$⊢ (K \in HL \land (P \in A \land Q \in A \land R \in A)) \to P \in {Base}_{K}$
9		simpr2	$⊢ (K \in HL \land (P \in A \land Q \in A \land R \in A)) \to Q \in A$
10	6 2	atbase	$⊢ Q \in A \to Q \in {Base}_{K}$
11	9 10	syl	$⊢ (K \in HL \land (P \in A \land Q \in A \land R \in A)) \to Q \in {Base}_{K}$
12		simpr3	$⊢ (K \in HL \land (P \in A \land Q \in A \land R \in A)) \to R \in A$
13	6 2	atbase	$⊢ R \in A \to R \in {Base}_{K}$
14	12 13	syl	$⊢ (K \in HL \land (P \in A \land Q \in A \land R \in A)) \to R \in {Base}_{K}$
15	6 1	latjass	$⊢ (K \in Lat \land (P \in {Base}_{K} \land Q \in {Base}_{K} \land R \in {Base}_{K})) \to (P \underset{˙}{\lor} Q) \underset{˙}{\lor} R = P \underset{˙}{\lor} (Q \underset{˙}{\lor} R)$
16	4 8 11 14 15	syl13anc	$⊢ (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)$

Metamath Proof Explorer