cdleme15

Description: Part of proof of Lemma E in Crawley p. 113, 3rd paragraph on p. 114, showing, in their notation, (s \/ t) /\ (f(s) \/ f(t)) <_ w. We use F , G for f(s), f(t) respectively. (Contributed by NM, 10-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	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$

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		eqid	$⊢ {Base}_{K} = {Base}_{K}$
10		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$
11	10	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$
12		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$
13		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$
14	9 2 4	hlatjcl	$⊢ (K \in HL \land S \in A \land T \in A) \to S \underset{˙}{\lor} T \in {Base}_{K}$
15	10 12 13 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		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$
17		simp12l	$⊢ (((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$
18		simp13l	$⊢ (((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$
19	1 2 3 4 5 6 7 9	cdleme1b	$⊢ ((K \in HL \land W \in H) \land (P \in A \land Q \in A \land S \in A)) \to F \in {Base}_{K}$
20	10 16 17 18 12 19	syl23anc	$⊢ (((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 {Base}_{K}$
21	1 2 3 4 5 6 8 9	cdleme1b	$⊢ ((K \in HL \land W \in H) \land (P \in A \land Q \in A \land T \in A)) \to G \in {Base}_{K}$
22	10 16 17 18 13 21	syl23anc	$⊢ (((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 {Base}_{K}$
23	9 2	latjcl	$⊢ (K \in Lat \land F \in {Base}_{K} \land G \in {Base}_{K}) \to F \underset{˙}{\lor} G \in {Base}_{K}$
24	11 20 22 23	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}$
25	9 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}$
26	11 15 24 25	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}$
27	9 2 4	hlatjcl	$⊢ (K \in HL \land T \in A \land P \in A) \to T \underset{˙}{\lor} P \in {Base}_{K}$
28	10 13 17 27	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 T \underset{˙}{\lor} P \in {Base}_{K}$
29	9 4	atbase	$⊢ Q \in A \to Q \in {Base}_{K}$
30	18 29	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 Q \in {Base}_{K}$
31	9 2	latjcl	$⊢ (K \in Lat \land G \in {Base}_{K} \land Q \in {Base}_{K}) \to G \underset{˙}{\lor} Q \in {Base}_{K}$
32	11 22 30 31	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 G \underset{˙}{\lor} Q \in {Base}_{K}$
33	9 3	latmcl	$⊢ (K \in Lat \land T \underset{˙}{\lor} P \in {Base}_{K} \land G \underset{˙}{\lor} Q \in {Base}_{K}) \to (T \underset{˙}{\lor} P) \underset{˙}{\land} (G \underset{˙}{\lor} Q) \in {Base}_{K}$
34	11 28 32 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 (T \underset{˙}{\lor} P) \underset{˙}{\land} (G \underset{˙}{\lor} Q) \in {Base}_{K}$
35	9 2 4	hlatjcl	$⊢ (K \in HL \land P \in A \land S \in A) \to P \underset{˙}{\lor} S \in {Base}_{K}$
36	10 17 12 35	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 P \underset{˙}{\lor} S \in {Base}_{K}$
37	9 2	latjcl	$⊢ (K \in Lat \land Q \in {Base}_{K} \land F \in {Base}_{K}) \to Q \underset{˙}{\lor} F \in {Base}_{K}$
38	11 30 20 37	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 Q \underset{˙}{\lor} F \in {Base}_{K}$
39	9 3	latmcl	$⊢ (K \in Lat \land P \underset{˙}{\lor} S \in {Base}_{K} \land Q \underset{˙}{\lor} F \in {Base}_{K}) \to (P \underset{˙}{\lor} S) \underset{˙}{\land} (Q \underset{˙}{\lor} F) \in {Base}_{K}$
40	11 36 38 39	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 (P \underset{˙}{\lor} S) \underset{˙}{\land} (Q \underset{˙}{\lor} F) \in {Base}_{K}$
41	9 2	latjcl	$⊢ (K \in Lat \land (T \underset{˙}{\lor} P) \underset{˙}{\land} (G \underset{˙}{\lor} Q) \in {Base}_{K} \land (P \underset{˙}{\lor} S) \underset{˙}{\land} (Q \underset{˙}{\lor} F) \in {Base}_{K}) \to ((T \underset{˙}{\lor} P) \underset{˙}{\land} (G \underset{˙}{\lor} Q)) \underset{˙}{\lor} ((P \underset{˙}{\lor} S) \underset{˙}{\land} (Q \underset{˙}{\lor} F)) \in {Base}_{K}$
42	11 34 40 41	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 ((T \underset{˙}{\lor} P) \underset{˙}{\land} (G \underset{˙}{\lor} Q)) \underset{˙}{\lor} ((P \underset{˙}{\lor} S) \underset{˙}{\land} (Q \underset{˙}{\lor} F)) \in {Base}_{K}$
43	9 5	lhpbase	$⊢ W \in H \to W \in {Base}_{K}$
44	16 43	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}$
45	1 2 3 4 5 6 7 8	cdleme14	$⊢ (((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} (((T \underset{˙}{\lor} P) \underset{˙}{\land} (G \underset{˙}{\lor} Q)) \underset{˙}{\lor} ((P \underset{˙}{\lor} S) \underset{˙}{\land} (Q \underset{˙}{\lor} F)))$
46		eqid	$⊢ (P \underset{˙}{\lor} S) \underset{˙}{\land} W = (P \underset{˙}{\lor} S) \underset{˙}{\land} W$
47		eqid	$⊢ (P \underset{˙}{\lor} T) \underset{˙}{\land} W = (P \underset{˙}{\lor} T) \underset{˙}{\land} W$
48	1 2 3 4 5 6 7 8 46 47	cdleme15a	$⊢ (((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 \underset{˙}{\lor} P) \underset{˙}{\land} (G \underset{˙}{\lor} Q)) \underset{˙}{\lor} ((P \underset{˙}{\lor} S) \underset{˙}{\land} (Q \underset{˙}{\lor} F)) = ((P \underset{˙}{\lor} ((P \underset{˙}{\lor} T) \underset{˙}{\land} W)) \underset{˙}{\land} (Q \underset{˙}{\lor} ((P \underset{˙}{\lor} T) \underset{˙}{\land} W))) \underset{˙}{\lor} ((P \underset{˙}{\lor} ((P \underset{˙}{\lor} S) \underset{˙}{\land} W)) \underset{˙}{\land} (Q \underset{˙}{\lor} ((P \underset{˙}{\lor} S) \underset{˙}{\land} W)))$
49	1 2 3 4 5 6 7 8 46 47	cdleme15c	$⊢ (((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 \underset{˙}{\lor} ((P \underset{˙}{\lor} T) \underset{˙}{\land} W)) \underset{˙}{\land} (Q \underset{˙}{\lor} ((P \underset{˙}{\lor} T) \underset{˙}{\land} W))) \underset{˙}{\lor} ((P \underset{˙}{\lor} ((P \underset{˙}{\lor} S) \underset{˙}{\land} W)) \underset{˙}{\land} (Q \underset{˙}{\lor} ((P \underset{˙}{\lor} S) \underset{˙}{\land} W))) = ((P \underset{˙}{\lor} T) \underset{˙}{\land} W) \underset{˙}{\lor} ((P \underset{˙}{\lor} S) \underset{˙}{\land} W)$
50	48 49	eqtrd	$⊢ (((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 \underset{˙}{\lor} P) \underset{˙}{\land} (G \underset{˙}{\lor} Q)) \underset{˙}{\lor} ((P \underset{˙}{\lor} S) \underset{˙}{\land} (Q \underset{˙}{\lor} F)) = ((P \underset{˙}{\lor} T) \underset{˙}{\land} W) \underset{˙}{\lor} ((P \underset{˙}{\lor} S) \underset{˙}{\land} W)$
51	1 2 3 4 5 6 7 8 46 47	cdleme15d	$⊢ (((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 \underset{˙}{\lor} T) \underset{˙}{\land} W) \underset{˙}{\lor} ((P \underset{˙}{\lor} S) \underset{˙}{\land} W)) \underset{˙}{\leq} W$
52	50 51	eqbrtrd	$⊢ (((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 \underset{˙}{\lor} P) \underset{˙}{\land} (G \underset{˙}{\lor} Q)) \underset{˙}{\lor} ((P \underset{˙}{\lor} S) \underset{˙}{\land} (Q \underset{˙}{\lor} F))) \underset{˙}{\leq} W$
53	9 1 11 26 42 44 45 52	lattrd	$⊢ (((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$

Metamath Proof Explorer

Theorem cdleme15

Proof