Metamath Proof Explorer

Theorem hlatj4

Description: Rearrangement of lattice join of 4 classes. Frequently-used special case of latj4 for atoms. (Contributed by NM, 9-Aug-2012)

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

Proof

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	3ad2ant1	$⊢ (K \in HL \land (P \in A \land Q \in A) \land (R \in A \land S \in A)) \to K \in Lat$
5		simp2l	$⊢ (K \in HL \land (P \in A \land Q \in A) \land (R \in A \land S \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 \land S \in A)) \to P \in {Base}_{K}$
9		simp2r	$⊢ (K \in HL \land (P \in A \land Q \in A) \land (R \in A \land S \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 \land S \in A)) \to Q \in {Base}_{K}$
12		simp3l	$⊢ (K \in HL \land (P \in A \land Q \in A) \land (R \in A \land S \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 \land S \in A)) \to R \in {Base}_{K}$
15		simp3r	$⊢ (K \in HL \land (P \in A \land Q \in A) \land (R \in A \land S \in A)) \to S \in A$
16	6 2	atbase	$⊢ S \in A \to S \in {Base}_{K}$
17	15 16	syl	$⊢ (K \in HL \land (P \in A \land Q \in A) \land (R \in A \land S \in A)) \to S \in {Base}_{K}$
18	6 1	latj4	$⊢ (K \in Lat \land (P \in {Base}_{K} \land Q \in {Base}_{K}) \land (R \in {Base}_{K} \land S \in {Base}_{K})) \to (P \underset{˙}{\lor} Q) \underset{˙}{\lor} (R \underset{˙}{\lor} S) = (P \underset{˙}{\lor} R) \underset{˙}{\lor} (Q \underset{˙}{\lor} S)$
19	4 8 11 14 17 18	syl122anc	$⊢ (K \in HL \land (P \in A \land Q \in A) \land (R \in A \land S \in A)) \to (P \underset{˙}{\lor} Q) \underset{˙}{\lor} (R \underset{˙}{\lor} S) = (P \underset{˙}{\lor} R) \underset{˙}{\lor} (Q \underset{˙}{\lor} S)$