4atlem4b

Description: Lemma for 4at . Frequently used associative law. (Contributed by NM, 9-Jul-2012)

	Ref	Expression
Hypotheses	4at.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
	4at.j	$⊢ \underset{˙}{\lor} = join (K)$
	4at.a	$⊢ A = Atoms (K)$
Assertion	4atlem4b	$⊢ ((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) = Q \underset{˙}{\lor} ((P \underset{˙}{\lor} R) \underset{˙}{\lor} S)$

Proof

Step	Hyp	Ref	Expression
1		4at.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
2		4at.j	$⊢ \underset{˙}{\lor} = join (K)$
3		4at.a	$⊢ A = Atoms (K)$
4		simpl1	$⊢ ((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A)) \to K \in HL$
5		simpl2	$⊢ ((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A)) \to P \in A$
6		simpl3	$⊢ ((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A)) \to Q \in A$
7		simprl	$⊢ ((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A)) \to R \in A$
8		simprr	$⊢ ((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A)) \to S \in A$
9	2 3	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)$
10	4 5 6 7 8 9	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)$
11	4	hllatd	$⊢ ((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A)) \to K \in Lat$
12		eqid	$⊢ {Base}_{K} = {Base}_{K}$
13	12 2 3	hlatjcl	$⊢ (K \in HL \land P \in A \land R \in A) \to P \underset{˙}{\lor} R \in {Base}_{K}$
14	4 5 7 13	syl3anc	$⊢ ((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A)) \to P \underset{˙}{\lor} R \in {Base}_{K}$
15	12 3	atbase	$⊢ Q \in A \to Q \in {Base}_{K}$
16	6 15	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}$
17	12 3	atbase	$⊢ S \in A \to S \in {Base}_{K}$
18	17	ad2antll	$⊢ ((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A)) \to S \in {Base}_{K}$
19	12 2	latj12	$⊢ (K \in Lat \land (P \underset{˙}{\lor} R \in {Base}_{K} \land Q \in {Base}_{K} \land S \in {Base}_{K})) \to (P \underset{˙}{\lor} R) \underset{˙}{\lor} (Q \underset{˙}{\lor} S) = Q \underset{˙}{\lor} ((P \underset{˙}{\lor} R) \underset{˙}{\lor} S)$
20	11 14 16 18 19	syl13anc	$⊢ ((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A)) \to (P \underset{˙}{\lor} R) \underset{˙}{\lor} (Q \underset{˙}{\lor} S) = Q \underset{˙}{\lor} ((P \underset{˙}{\lor} R) \underset{˙}{\lor} S)$
21	10 20	eqtrd	$⊢ ((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) = Q \underset{˙}{\lor} ((P \underset{˙}{\lor} R) \underset{˙}{\lor} S)$

Metamath Proof Explorer

Theorem 4atlem4b

Proof