4atlem9

Description: Lemma for 4at . Substitute W for S . (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	4atlem9	$⊢ ((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A \land W \in A) \land \neg S \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} R)) \to (S \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} (R \underset{˙}{\lor} W)) \leftrightarrow (P \underset{˙}{\lor} Q) \underset{˙}{\lor} (R \underset{˙}{\lor} S) = (P \underset{˙}{\lor} Q) \underset{˙}{\lor} (R \underset{˙}{\lor} W))$

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		simp11	$⊢ ((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A \land W \in A) \land \neg S \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} R)) \to K \in HL$
5		simp22	$⊢ ((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A \land W \in A) \land \neg S \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} R)) \to S \in A$
6		simp23	$⊢ ((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A \land W \in A) \land \neg S \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} R)) \to W \in A$
7	4	hllatd	$⊢ ((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A \land W \in A) \land \neg S \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} R)) \to K \in Lat$
8		simp1	$⊢ ((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A \land W \in A) \land \neg S \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} R)) \to (K \in HL \land P \in A \land Q \in A)$
9		eqid	$⊢ {Base}_{K} = {Base}_{K}$
10	9 2 3	hlatjcl	$⊢ (K \in HL \land P \in A \land Q \in A) \to P \underset{˙}{\lor} Q \in {Base}_{K}$
11	8 10	syl	$⊢ ((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A \land W \in A) \land \neg S \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} R)) \to P \underset{˙}{\lor} Q \in {Base}_{K}$
12		simp21	$⊢ ((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A \land W \in A) \land \neg S \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} R)) \to R \in A$
13	9 3	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 \land W \in A) \land \neg S \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} R)) \to R \in {Base}_{K}$
15	9 2	latjcl	$⊢ (K \in Lat \land P \underset{˙}{\lor} Q \in {Base}_{K} \land R \in {Base}_{K}) \to (P \underset{˙}{\lor} Q) \underset{˙}{\lor} R \in {Base}_{K}$
16	7 11 14 15	syl3anc	$⊢ ((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A \land W \in A) \land \neg S \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} R)) \to (P \underset{˙}{\lor} Q) \underset{˙}{\lor} R \in {Base}_{K}$
17		simp3	$⊢ ((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A \land W \in A) \land \neg S \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} R)) \to \neg S \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} R)$
18	9 1 2 3	hlexchb2	$⊢ (K \in HL \land (S \in A \land W \in A \land (P \underset{˙}{\lor} Q) \underset{˙}{\lor} R \in {Base}_{K}) \land \neg S \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} R)) \to (S \underset{˙}{\leq} (W \underset{˙}{\lor} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} R)) \leftrightarrow S \underset{˙}{\lor} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} R) = W \underset{˙}{\lor} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} R))$
19	4 5 6 16 17 18	syl131anc	$⊢ ((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A \land W \in A) \land \neg S \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} R)) \to (S \underset{˙}{\leq} (W \underset{˙}{\lor} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} R)) \leftrightarrow S \underset{˙}{\lor} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} R) = W \underset{˙}{\lor} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} R))$
20	1 2 3	4atlem4d	$⊢ ((K \in HL \land P \in A \land Q \in A) \land (R \in A \land W \in A)) \to (P \underset{˙}{\lor} Q) \underset{˙}{\lor} (R \underset{˙}{\lor} W) = W \underset{˙}{\lor} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} R)$
21	8 12 6 20	syl12anc	$⊢ ((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A \land W \in A) \land \neg S \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} R)) \to (P \underset{˙}{\lor} Q) \underset{˙}{\lor} (R \underset{˙}{\lor} W) = W \underset{˙}{\lor} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} R)$
22	21	breq2d	$⊢ ((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A \land W \in A) \land \neg S \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} R)) \to (S \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} (R \underset{˙}{\lor} W)) \leftrightarrow S \underset{˙}{\leq} (W \underset{˙}{\lor} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} R)))$
23	1 2 3	4atlem4d	$⊢ ((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) = S \underset{˙}{\lor} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} R)$
24	8 12 5 23	syl12anc	$⊢ ((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A \land W \in A) \land \neg S \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} R)) \to (P \underset{˙}{\lor} Q) \underset{˙}{\lor} (R \underset{˙}{\lor} S) = S \underset{˙}{\lor} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} R)$
25	24 21	eqeq12d	$⊢ ((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A \land W \in A) \land \neg S \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} R)) \to ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} (R \underset{˙}{\lor} S) = (P \underset{˙}{\lor} Q) \underset{˙}{\lor} (R \underset{˙}{\lor} W) \leftrightarrow S \underset{˙}{\lor} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} R) = W \underset{˙}{\lor} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} R))$
26	19 22 25	3bitr4d	$⊢ ((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A \land W \in A) \land \neg S \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} R)) \to (S \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} (R \underset{˙}{\lor} W)) \leftrightarrow (P \underset{˙}{\lor} Q) \underset{˙}{\lor} (R \underset{˙}{\lor} S) = (P \underset{˙}{\lor} Q) \underset{˙}{\lor} (R \underset{˙}{\lor} W))$

Metamath Proof Explorer

Theorem 4atlem9

Proof