4atlem4a

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	4atlem4a	$⊢ ((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} ((Q \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	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$
6		simpl2	$⊢ ((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A)) \to P \in A$
7		eqid	$⊢ {Base}_{K} = {Base}_{K}$
8	7 3	atbase	$⊢ P \in A \to P \in {Base}_{K}$
9	6 8	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}$
10		simpl3	$⊢ ((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A)) \to Q \in A$
11	7 3	atbase	$⊢ Q \in A \to Q \in {Base}_{K}$
12	10 11	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}$
13		simprl	$⊢ ((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A)) \to R \in A$
14		simprr	$⊢ ((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A)) \to S \in A$
15	7 2 3	hlatjcl	$⊢ (K \in HL \land R \in A \land S \in A) \to R \underset{˙}{\lor} S \in {Base}_{K}$
16	4 13 14 15	syl3anc	$⊢ ((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A)) \to R \underset{˙}{\lor} S \in {Base}_{K}$
17	7 2	latjass	$⊢ (K \in Lat \land (P \in {Base}_{K} \land Q \in {Base}_{K} \land R \underset{˙}{\lor} S \in {Base}_{K})) \to (P \underset{˙}{\lor} Q) \underset{˙}{\lor} (R \underset{˙}{\lor} S) = P \underset{˙}{\lor} (Q \underset{˙}{\lor} (R \underset{˙}{\lor} S))$
18	5 9 12 16 17	syl13anc	$⊢ ((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} (Q \underset{˙}{\lor} (R \underset{˙}{\lor} S))$
19	2 3	hlatjass	$⊢ (K \in HL \land (Q \in A \land R \in A \land S \in A)) \to (Q \underset{˙}{\lor} R) \underset{˙}{\lor} S = Q \underset{˙}{\lor} (R \underset{˙}{\lor} S)$
20	4 10 13 14 19	syl13anc	$⊢ ((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A)) \to (Q \underset{˙}{\lor} R) \underset{˙}{\lor} S = Q \underset{˙}{\lor} (R \underset{˙}{\lor} S)$
21	20	oveq2d	$⊢ ((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} (Q \underset{˙}{\lor} (R \underset{˙}{\lor} S))$
22	18 21	eqtr4d	$⊢ ((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} ((Q \underset{˙}{\lor} R) \underset{˙}{\lor} S)$

Metamath Proof Explorer

Theorem 4atlem4a

Proof