cdleme16e

Description: Part of proof of Lemma E in Crawley p. 113, 3rd paragraph on p. 114, 3rd part of 3rd sentence. F and G represent f(s) and f(t) respectively. We show, in their notation, (s \/ t) /\ (f(s) \/ f(t))=(s \/ t) /\ w. (Contributed by NM, 11-Oct-2012)

	Ref	Expression
Hypotheses	cdleme12.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
	cdleme12.j	$⊢ \underset{˙}{\lor} = join (K)$
	cdleme12.m	$⊢ \underset{˙}{\land} = meet (K)$
	cdleme12.a	$⊢ A = Atoms (K)$
	cdleme12.h	$⊢ H = LHyp (K)$
	cdleme12.u	$⊢ U = (P \underset{˙}{\lor} Q) \underset{˙}{\land} W$
	cdleme12.f	$⊢ F = (S \underset{˙}{\lor} U) \underset{˙}{\land} (Q \underset{˙}{\lor} ((P \underset{˙}{\lor} S) \underset{˙}{\land} W))$
	cdleme12.g	$⊢ G = (T \underset{˙}{\lor} U) \underset{˙}{\land} (Q \underset{˙}{\lor} ((P \underset{˙}{\lor} T) \underset{˙}{\land} W))$
Assertion	cdleme16e	$⊢ (((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land ((S \in A \land \neg S \underset{˙}{\leq} W) \land (T \in A \land \neg T \underset{˙}{\leq} W) \land (P \neq Q \land S \neq T)) \land (\neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg T \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg U \underset{˙}{\leq} (S \underset{˙}{\lor} T))) \to (S \underset{˙}{\lor} T) \underset{˙}{\land} (F \underset{˙}{\lor} G) = (S \underset{˙}{\lor} T) \underset{˙}{\land} W$

Proof

Step	Hyp	Ref	Expression
1		cdleme12.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
2		cdleme12.j	$⊢ \underset{˙}{\lor} = join (K)$
3		cdleme12.m	$⊢ \underset{˙}{\land} = meet (K)$
4		cdleme12.a	$⊢ A = Atoms (K)$
5		cdleme12.h	$⊢ H = LHyp (K)$
6		cdleme12.u	$⊢ U = (P \underset{˙}{\lor} Q) \underset{˙}{\land} W$
7		cdleme12.f	$⊢ F = (S \underset{˙}{\lor} U) \underset{˙}{\land} (Q \underset{˙}{\lor} ((P \underset{˙}{\lor} S) \underset{˙}{\land} W))$
8		cdleme12.g	$⊢ G = (T \underset{˙}{\lor} U) \underset{˙}{\land} (Q \underset{˙}{\lor} ((P \underset{˙}{\lor} T) \underset{˙}{\land} W))$
9		simp11l	$⊢ (((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land ((S \in A \land \neg S \underset{˙}{\leq} W) \land (T \in A \land \neg T \underset{˙}{\leq} W) \land (P \neq Q \land S \neq T)) \land (\neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg T \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg U \underset{˙}{\leq} (S \underset{˙}{\lor} T))) \to K \in HL$
10	9	hllatd	$⊢ (((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land ((S \in A \land \neg S \underset{˙}{\leq} W) \land (T \in A \land \neg T \underset{˙}{\leq} W) \land (P \neq Q \land S \neq T)) \land (\neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg T \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg U \underset{˙}{\leq} (S \underset{˙}{\lor} T))) \to K \in Lat$
11		simp21l	$⊢ (((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land ((S \in A \land \neg S \underset{˙}{\leq} W) \land (T \in A \land \neg T \underset{˙}{\leq} W) \land (P \neq Q \land S \neq T)) \land (\neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg T \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg U \underset{˙}{\leq} (S \underset{˙}{\lor} T))) \to S \in A$
12		simp22l	$⊢ (((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land ((S \in A \land \neg S \underset{˙}{\leq} W) \land (T \in A \land \neg T \underset{˙}{\leq} W) \land (P \neq Q \land S \neq T)) \land (\neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg T \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg U \underset{˙}{\leq} (S \underset{˙}{\lor} T))) \to T \in A$
13		eqid	$⊢ {Base}_{K} = {Base}_{K}$
14	13 2 4	hlatjcl	$⊢ (K \in HL \land S \in A \land T \in A) \to S \underset{˙}{\lor} T \in {Base}_{K}$
15	9 11 12 14	syl3anc	$⊢ (((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land ((S \in A \land \neg S \underset{˙}{\leq} W) \land (T \in A \land \neg T \underset{˙}{\leq} W) \land (P \neq Q \land S \neq T)) \land (\neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg T \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg U \underset{˙}{\leq} (S \underset{˙}{\lor} T))) \to S \underset{˙}{\lor} T \in {Base}_{K}$
16		simp11	$⊢ (((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land ((S \in A \land \neg S \underset{˙}{\leq} W) \land (T \in A \land \neg T \underset{˙}{\leq} W) \land (P \neq Q \land S \neq T)) \land (\neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg T \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg U \underset{˙}{\leq} (S \underset{˙}{\lor} T))) \to (K \in HL \land W \in H)$
17		simp12	$⊢ (((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land ((S \in A \land \neg S \underset{˙}{\leq} W) \land (T \in A \land \neg T \underset{˙}{\leq} W) \land (P \neq Q \land S \neq T)) \land (\neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg T \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg U \underset{˙}{\leq} (S \underset{˙}{\lor} T))) \to (P \in A \land \neg P \underset{˙}{\leq} W)$
18		simp13	$⊢ (((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land ((S \in A \land \neg S \underset{˙}{\leq} W) \land (T \in A \land \neg T \underset{˙}{\leq} W) \land (P \neq Q \land S \neq T)) \land (\neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg T \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg U \underset{˙}{\leq} (S \underset{˙}{\lor} T))) \to (Q \in A \land \neg Q \underset{˙}{\leq} W)$
19		simp21	$⊢ (((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land ((S \in A \land \neg S \underset{˙}{\leq} W) \land (T \in A \land \neg T \underset{˙}{\leq} W) \land (P \neq Q \land S \neq T)) \land (\neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg T \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg U \underset{˙}{\leq} (S \underset{˙}{\lor} T))) \to (S \in A \land \neg S \underset{˙}{\leq} W)$
20		simp23l	$⊢ (((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land ((S \in A \land \neg S \underset{˙}{\leq} W) \land (T \in A \land \neg T \underset{˙}{\leq} W) \land (P \neq Q \land S \neq T)) \land (\neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg T \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg U \underset{˙}{\leq} (S \underset{˙}{\lor} T))) \to P \neq Q$
21		simp31	$⊢ (((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land ((S \in A \land \neg S \underset{˙}{\leq} W) \land (T \in A \land \neg T \underset{˙}{\leq} W) \land (P \neq Q \land S \neq T)) \land (\neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg T \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg U \underset{˙}{\leq} (S \underset{˙}{\lor} T))) \to \neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q)$
22	1 2 3 4 5 6 7	cdleme3fa	$⊢ ((K \in HL \land W \in H) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W) \land (S \in A \land \neg S \underset{˙}{\leq} W)) \land (P \neq Q \land \neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \to F \in A$
23	16 17 18 19 20 21 22	syl132anc	$⊢ (((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land ((S \in A \land \neg S \underset{˙}{\leq} W) \land (T \in A \land \neg T \underset{˙}{\leq} W) \land (P \neq Q \land S \neq T)) \land (\neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg T \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg U \underset{˙}{\leq} (S \underset{˙}{\lor} T))) \to F \in A$
24		simp22	$⊢ (((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land ((S \in A \land \neg S \underset{˙}{\leq} W) \land (T \in A \land \neg T \underset{˙}{\leq} W) \land (P \neq Q \land S \neq T)) \land (\neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg T \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg U \underset{˙}{\leq} (S \underset{˙}{\lor} T))) \to (T \in A \land \neg T \underset{˙}{\leq} W)$
25		simp32	$⊢ (((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land ((S \in A \land \neg S \underset{˙}{\leq} W) \land (T \in A \land \neg T \underset{˙}{\leq} W) \land (P \neq Q \land S \neq T)) \land (\neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg T \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg U \underset{˙}{\leq} (S \underset{˙}{\lor} T))) \to \neg T \underset{˙}{\leq} (P \underset{˙}{\lor} Q)$
26	1 2 3 4 5 6 8	cdleme3fa	$⊢ ((K \in HL \land W \in H) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W) \land (T \in A \land \neg T \underset{˙}{\leq} W)) \land (P \neq Q \land \neg T \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \to G \in A$
27	16 17 18 24 20 25 26	syl132anc	$⊢ (((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land ((S \in A \land \neg S \underset{˙}{\leq} W) \land (T \in A \land \neg T \underset{˙}{\leq} W) \land (P \neq Q \land S \neq T)) \land (\neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg T \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg U \underset{˙}{\leq} (S \underset{˙}{\lor} T))) \to G \in A$
28	13 2 4	hlatjcl	$⊢ (K \in HL \land F \in A \land G \in A) \to F \underset{˙}{\lor} G \in {Base}_{K}$
29	9 23 27 28	syl3anc	$⊢ (((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land ((S \in A \land \neg S \underset{˙}{\leq} W) \land (T \in A \land \neg T \underset{˙}{\leq} W) \land (P \neq Q \land S \neq T)) \land (\neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg T \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg U \underset{˙}{\leq} (S \underset{˙}{\lor} T))) \to F \underset{˙}{\lor} G \in {Base}_{K}$
30	13 1 3	latmle1	$⊢ (K \in Lat \land S \underset{˙}{\lor} T \in {Base}_{K} \land F \underset{˙}{\lor} G \in {Base}_{K}) \to ((S \underset{˙}{\lor} T) \underset{˙}{\land} (F \underset{˙}{\lor} G)) \underset{˙}{\leq} (S \underset{˙}{\lor} T)$
31	10 15 29 30	syl3anc	$⊢ (((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land ((S \in A \land \neg S \underset{˙}{\leq} W) \land (T \in A \land \neg T \underset{˙}{\leq} W) \land (P \neq Q \land S \neq T)) \land (\neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg T \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg U \underset{˙}{\leq} (S \underset{˙}{\lor} T))) \to ((S \underset{˙}{\lor} T) \underset{˙}{\land} (F \underset{˙}{\lor} G)) \underset{˙}{\leq} (S \underset{˙}{\lor} T)$
32	1 2 3 4 5 6 7 8	cdleme15	$⊢ (((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land ((S \in A \land \neg S \underset{˙}{\leq} W) \land (T \in A \land \neg T \underset{˙}{\leq} W) \land (P \neq Q \land S \neq T)) \land (\neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg T \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg U \underset{˙}{\leq} (S \underset{˙}{\lor} T))) \to ((S \underset{˙}{\lor} T) \underset{˙}{\land} (F \underset{˙}{\lor} G)) \underset{˙}{\leq} W$
33	13 3	latmcl	$⊢ (K \in Lat \land S \underset{˙}{\lor} T \in {Base}_{K} \land F \underset{˙}{\lor} G \in {Base}_{K}) \to (S \underset{˙}{\lor} T) \underset{˙}{\land} (F \underset{˙}{\lor} G) \in {Base}_{K}$
34	10 15 29 33	syl3anc	$⊢ (((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land ((S \in A \land \neg S \underset{˙}{\leq} W) \land (T \in A \land \neg T \underset{˙}{\leq} W) \land (P \neq Q \land S \neq T)) \land (\neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg T \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg U \underset{˙}{\leq} (S \underset{˙}{\lor} T))) \to (S \underset{˙}{\lor} T) \underset{˙}{\land} (F \underset{˙}{\lor} G) \in {Base}_{K}$
35		simp11r	$⊢ (((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land ((S \in A \land \neg S \underset{˙}{\leq} W) \land (T \in A \land \neg T \underset{˙}{\leq} W) \land (P \neq Q \land S \neq T)) \land (\neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg T \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg U \underset{˙}{\leq} (S \underset{˙}{\lor} T))) \to W \in H$
36	13 5	lhpbase	$⊢ W \in H \to W \in {Base}_{K}$
37	35 36	syl	$⊢ (((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land ((S \in A \land \neg S \underset{˙}{\leq} W) \land (T \in A \land \neg T \underset{˙}{\leq} W) \land (P \neq Q \land S \neq T)) \land (\neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg T \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg U \underset{˙}{\leq} (S \underset{˙}{\lor} T))) \to W \in {Base}_{K}$
38	13 1 3	latlem12	$⊢ (K \in Lat \land ((S \underset{˙}{\lor} T) \underset{˙}{\land} (F \underset{˙}{\lor} G) \in {Base}_{K} \land S \underset{˙}{\lor} T \in {Base}_{K} \land W \in {Base}_{K})) \to ((((S \underset{˙}{\lor} T) \underset{˙}{\land} (F \underset{˙}{\lor} G)) \underset{˙}{\leq} (S \underset{˙}{\lor} T) \land ((S \underset{˙}{\lor} T) \underset{˙}{\land} (F \underset{˙}{\lor} G)) \underset{˙}{\leq} W) \leftrightarrow ((S \underset{˙}{\lor} T) \underset{˙}{\land} (F \underset{˙}{\lor} G)) \underset{˙}{\leq} ((S \underset{˙}{\lor} T) \underset{˙}{\land} W))$
39	10 34 15 37 38	syl13anc	$⊢ (((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land ((S \in A \land \neg S \underset{˙}{\leq} W) \land (T \in A \land \neg T \underset{˙}{\leq} W) \land (P \neq Q \land S \neq T)) \land (\neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg T \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg U \underset{˙}{\leq} (S \underset{˙}{\lor} T))) \to ((((S \underset{˙}{\lor} T) \underset{˙}{\land} (F \underset{˙}{\lor} G)) \underset{˙}{\leq} (S \underset{˙}{\lor} T) \land ((S \underset{˙}{\lor} T) \underset{˙}{\land} (F \underset{˙}{\lor} G)) \underset{˙}{\leq} W) \leftrightarrow ((S \underset{˙}{\lor} T) \underset{˙}{\land} (F \underset{˙}{\lor} G)) \underset{˙}{\leq} ((S \underset{˙}{\lor} T) \underset{˙}{\land} W))$
40	31 32 39	mpbi2and	$⊢ (((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land ((S \in A \land \neg S \underset{˙}{\leq} W) \land (T \in A \land \neg T \underset{˙}{\leq} W) \land (P \neq Q \land S \neq T)) \land (\neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg T \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg U \underset{˙}{\leq} (S \underset{˙}{\lor} T))) \to ((S \underset{˙}{\lor} T) \underset{˙}{\land} (F \underset{˙}{\lor} G)) \underset{˙}{\leq} ((S \underset{˙}{\lor} T) \underset{˙}{\land} W)$
41		hlatl	$⊢ K \in HL \to K \in AtLat$
42	9 41	syl	$⊢ (((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land ((S \in A \land \neg S \underset{˙}{\leq} W) \land (T \in A \land \neg T \underset{˙}{\leq} W) \land (P \neq Q \land S \neq T)) \land (\neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg T \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg U \underset{˙}{\leq} (S \underset{˙}{\lor} T))) \to K \in AtLat$
43	1 2 3 4 5 6 7 8	cdleme16d	$⊢ (((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land ((S \in A \land \neg S \underset{˙}{\leq} W) \land (T \in A \land \neg T \underset{˙}{\leq} W) \land (P \neq Q \land S \neq T)) \land (\neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg T \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg U \underset{˙}{\leq} (S \underset{˙}{\lor} T))) \to (S \underset{˙}{\lor} T) \underset{˙}{\land} (F \underset{˙}{\lor} G) \in A$
44		simp21r	$⊢ (((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land ((S \in A \land \neg S \underset{˙}{\leq} W) \land (T \in A \land \neg T \underset{˙}{\leq} W) \land (P \neq Q \land S \neq T)) \land (\neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg T \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg U \underset{˙}{\leq} (S \underset{˙}{\lor} T))) \to \neg S \underset{˙}{\leq} W$
45		simp23r	$⊢ (((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land ((S \in A \land \neg S \underset{˙}{\leq} W) \land (T \in A \land \neg T \underset{˙}{\leq} W) \land (P \neq Q \land S \neq T)) \land (\neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg T \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg U \underset{˙}{\leq} (S \underset{˙}{\lor} T))) \to S \neq T$
46	1 2 3 4 5	lhpat	$⊢ ((K \in HL \land W \in H) \land (S \in A \land \neg S \underset{˙}{\leq} W) \land (T \in A \land S \neq T)) \to (S \underset{˙}{\lor} T) \underset{˙}{\land} W \in A$
47	9 35 11 44 12 45 46	syl222anc	$⊢ (((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land ((S \in A \land \neg S \underset{˙}{\leq} W) \land (T \in A \land \neg T \underset{˙}{\leq} W) \land (P \neq Q \land S \neq T)) \land (\neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg T \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg U \underset{˙}{\leq} (S \underset{˙}{\lor} T))) \to (S \underset{˙}{\lor} T) \underset{˙}{\land} W \in A$
48	1 4	atcmp	$⊢ (K \in AtLat \land (S \underset{˙}{\lor} T) \underset{˙}{\land} (F \underset{˙}{\lor} G) \in A \land (S \underset{˙}{\lor} T) \underset{˙}{\land} W \in A) \to (((S \underset{˙}{\lor} T) \underset{˙}{\land} (F \underset{˙}{\lor} G)) \underset{˙}{\leq} ((S \underset{˙}{\lor} T) \underset{˙}{\land} W) \leftrightarrow (S \underset{˙}{\lor} T) \underset{˙}{\land} (F \underset{˙}{\lor} G) = (S \underset{˙}{\lor} T) \underset{˙}{\land} W)$
49	42 43 47 48	syl3anc	$⊢ (((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land ((S \in A \land \neg S \underset{˙}{\leq} W) \land (T \in A \land \neg T \underset{˙}{\leq} W) \land (P \neq Q \land S \neq T)) \land (\neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg T \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg U \underset{˙}{\leq} (S \underset{˙}{\lor} T))) \to (((S \underset{˙}{\lor} T) \underset{˙}{\land} (F \underset{˙}{\lor} G)) \underset{˙}{\leq} ((S \underset{˙}{\lor} T) \underset{˙}{\land} W) \leftrightarrow (S \underset{˙}{\lor} T) \underset{˙}{\land} (F \underset{˙}{\lor} G) = (S \underset{˙}{\lor} T) \underset{˙}{\land} W)$
50	40 49	mpbid	$⊢ (((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land ((S \in A \land \neg S \underset{˙}{\leq} W) \land (T \in A \land \neg T \underset{˙}{\leq} W) \land (P \neq Q \land S \neq T)) \land (\neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg T \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg U \underset{˙}{\leq} (S \underset{˙}{\lor} T))) \to (S \underset{˙}{\lor} T) \underset{˙}{\land} (F \underset{˙}{\lor} G) = (S \underset{˙}{\lor} T) \underset{˙}{\land} W$

Metamath Proof Explorer

Theorem cdleme16e

Proof