cdleme43dN

Description: Part of proof of Lemma E in Crawley p. 113. TODO: FIX COMMENT p. 116 2nd line: f(r) v s = f(r) v f(g(s)). (Contributed by NM, 20-Mar-2013) (New usage is discouraged.)

	Ref	Expression
Hypotheses	cdleme43.b	$⊢ B = {Base}_{K}$
	cdleme43.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
	cdleme43.j	$⊢ \underset{˙}{\lor} = join (K)$
	cdleme43.m	$⊢ \underset{˙}{\land} = meet (K)$
	cdleme43.a	$⊢ A = Atoms (K)$
	cdleme43.h	$⊢ H = LHyp (K)$
	cdleme43.u	$⊢ U = (P \underset{˙}{\lor} Q) \underset{˙}{\land} W$
	cdleme43.x	$⊢ X = (Q \underset{˙}{\lor} P) \underset{˙}{\land} W$
	cdleme43.c	$⊢ C = (S \underset{˙}{\lor} U) \underset{˙}{\land} (Q \underset{˙}{\lor} ((P \underset{˙}{\lor} S) \underset{˙}{\land} W))$
	cdleme43.f	$⊢ Z = (P \underset{˙}{\lor} Q) \underset{˙}{\land} (C \underset{˙}{\lor} ((R \underset{˙}{\lor} S) \underset{˙}{\land} W))$
	cdleme43.d	$⊢ D = (S \underset{˙}{\lor} X) \underset{˙}{\land} (P \underset{˙}{\lor} ((Q \underset{˙}{\lor} S) \underset{˙}{\land} W))$
	cdleme43.g	$⊢ G = (Q \underset{˙}{\lor} P) \underset{˙}{\land} (D \underset{˙}{\lor} ((Z \underset{˙}{\lor} S) \underset{˙}{\land} W))$
	cdleme43.e	$⊢ E = (D \underset{˙}{\lor} U) \underset{˙}{\land} (Q \underset{˙}{\lor} ((P \underset{˙}{\lor} D) \underset{˙}{\land} W))$
	cdleme43.v	$⊢ V = (Z \underset{˙}{\lor} S) \underset{˙}{\land} W$
	cdleme43.y	$⊢ Y = (R \underset{˙}{\lor} D) \underset{˙}{\land} W$
Assertion	cdleme43dN	$⊢ (((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 (P \neq Q \land (R \in A \land \neg R \underset{˙}{\leq} W) \land (S \in A \land \neg S \underset{˙}{\leq} W)) \land (R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \to Z \underset{˙}{\lor} S = Z \underset{˙}{\lor} E$

Proof

Step	Hyp	Ref	Expression
1		cdleme43.b	$⊢ B = {Base}_{K}$
2		cdleme43.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
3		cdleme43.j	$⊢ \underset{˙}{\lor} = join (K)$
4		cdleme43.m	$⊢ \underset{˙}{\land} = meet (K)$
5		cdleme43.a	$⊢ A = Atoms (K)$
6		cdleme43.h	$⊢ H = LHyp (K)$
7		cdleme43.u	$⊢ U = (P \underset{˙}{\lor} Q) \underset{˙}{\land} W$
8		cdleme43.x	$⊢ X = (Q \underset{˙}{\lor} P) \underset{˙}{\land} W$
9		cdleme43.c	$⊢ C = (S \underset{˙}{\lor} U) \underset{˙}{\land} (Q \underset{˙}{\lor} ((P \underset{˙}{\lor} S) \underset{˙}{\land} W))$
10		cdleme43.f	$⊢ Z = (P \underset{˙}{\lor} Q) \underset{˙}{\land} (C \underset{˙}{\lor} ((R \underset{˙}{\lor} S) \underset{˙}{\land} W))$
11		cdleme43.d	$⊢ D = (S \underset{˙}{\lor} X) \underset{˙}{\land} (P \underset{˙}{\lor} ((Q \underset{˙}{\lor} S) \underset{˙}{\land} W))$
12		cdleme43.g	$⊢ G = (Q \underset{˙}{\lor} P) \underset{˙}{\land} (D \underset{˙}{\lor} ((Z \underset{˙}{\lor} S) \underset{˙}{\land} W))$
13		cdleme43.e	$⊢ E = (D \underset{˙}{\lor} U) \underset{˙}{\land} (Q \underset{˙}{\lor} ((P \underset{˙}{\lor} D) \underset{˙}{\land} W))$
14		cdleme43.v	$⊢ V = (Z \underset{˙}{\lor} S) \underset{˙}{\land} W$
15		cdleme43.y	$⊢ Y = (R \underset{˙}{\lor} D) \underset{˙}{\land} W$
16		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 (P \neq Q \land (R \in A \land \neg R \underset{˙}{\leq} W) \land (S \in A \land \neg S \underset{˙}{\leq} W)) \land (R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \to K \in HL$
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 (P \neq Q \land (R \in A \land \neg R \underset{˙}{\leq} W) \land (S \in A \land \neg S \underset{˙}{\leq} W)) \land (R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \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 (P \neq Q \land (R \in A \land \neg R \underset{˙}{\leq} W) \land (S \in A \land \neg S \underset{˙}{\leq} W)) \land (R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \to Q \in A$
19	3 5	hlatjcom	$⊢ (K \in HL \land P \in A \land Q \in A) \to P \underset{˙}{\lor} Q = Q \underset{˙}{\lor} P$
20	16 17 18 19	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 (P \neq Q \land (R \in A \land \neg R \underset{˙}{\leq} W) \land (S \in A \land \neg S \underset{˙}{\leq} W)) \land (R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \to P \underset{˙}{\lor} Q = Q \underset{˙}{\lor} P$
21	20	oveq1d	$⊢ (((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 (P \neq Q \land (R \in A \land \neg R \underset{˙}{\leq} W) \land (S \in A \land \neg S \underset{˙}{\leq} W)) \land (R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \to (P \underset{˙}{\lor} Q) \underset{˙}{\land} W = (Q \underset{˙}{\lor} P) \underset{˙}{\land} W$
22	21 7 8	3eqtr4g	$⊢ (((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 (P \neq Q \land (R \in A \land \neg R \underset{˙}{\leq} W) \land (S \in A \land \neg S \underset{˙}{\leq} W)) \land (R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \to U = X$
23	22	oveq2d	$⊢ (((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 (P \neq Q \land (R \in A \land \neg R \underset{˙}{\leq} W) \land (S \in A \land \neg S \underset{˙}{\leq} W)) \land (R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \to D \underset{˙}{\lor} U = D \underset{˙}{\lor} X$
24	23	oveq1d	$⊢ (((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 (P \neq Q \land (R \in A \land \neg R \underset{˙}{\leq} W) \land (S \in A \land \neg S \underset{˙}{\leq} W)) \land (R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \to (D \underset{˙}{\lor} U) \underset{˙}{\land} (Q \underset{˙}{\lor} ((P \underset{˙}{\lor} D) \underset{˙}{\land} W)) = (D \underset{˙}{\lor} X) \underset{˙}{\land} (Q \underset{˙}{\lor} ((P \underset{˙}{\lor} D) \underset{˙}{\land} W))$
25		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 (P \neq Q \land (R \in A \land \neg R \underset{˙}{\leq} W) \land (S \in A \land \neg S \underset{˙}{\leq} W)) \land (R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \to (K \in HL \land W \in H)$
26		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 (P \neq Q \land (R \in A \land \neg R \underset{˙}{\leq} W) \land (S \in A \land \neg S \underset{˙}{\leq} W)) \land (R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \to (Q \in A \land \neg Q \underset{˙}{\leq} W)$
27		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 (P \neq Q \land (R \in A \land \neg R \underset{˙}{\leq} W) \land (S \in A \land \neg S \underset{˙}{\leq} W)) \land (R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \to (P \in A \land \neg P \underset{˙}{\leq} W)$
28		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 (P \neq Q \land (R \in A \land \neg R \underset{˙}{\leq} W) \land (S \in A \land \neg S \underset{˙}{\leq} W)) \land (R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \to P \neq Q$
29	28	necomd	$⊢ (((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 (P \neq Q \land (R \in A \land \neg R \underset{˙}{\leq} W) \land (S \in A \land \neg S \underset{˙}{\leq} W)) \land (R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \to Q \neq P$
30		simp23	$⊢ (((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 (P \neq Q \land (R \in A \land \neg R \underset{˙}{\leq} W) \land (S \in A \land \neg S \underset{˙}{\leq} W)) \land (R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \to (S \in A \land \neg S \underset{˙}{\leq} W)$
31		simp3r	$⊢ (((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 (P \neq Q \land (R \in A \land \neg R \underset{˙}{\leq} W) \land (S \in A \land \neg S \underset{˙}{\leq} W)) \land (R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \to \neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q)$
32	20	breq2d	$⊢ (((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 (P \neq Q \land (R \in A \land \neg R \underset{˙}{\leq} W) \land (S \in A \land \neg S \underset{˙}{\leq} W)) \land (R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \to (S \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \leftrightarrow S \underset{˙}{\leq} (Q \underset{˙}{\lor} P))$
33	31 32	mtbid	$⊢ (((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 (P \neq Q \land (R \in A \land \neg R \underset{˙}{\leq} W) \land (S \in A \land \neg S \underset{˙}{\leq} W)) \land (R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \to \neg S \underset{˙}{\leq} (Q \underset{˙}{\lor} P)$
34	2 3 4 5 6 8 11	cdleme35g	$⊢ (((K \in HL \land W \in H) \land (Q \in A \land \neg Q \underset{˙}{\leq} W) \land (P \in A \land \neg P \underset{˙}{\leq} W)) \land (Q \neq P \land (S \in A \land \neg S \underset{˙}{\leq} W)) \land \neg S \underset{˙}{\leq} (Q \underset{˙}{\lor} P)) \to (D \underset{˙}{\lor} X) \underset{˙}{\land} (Q \underset{˙}{\lor} ((P \underset{˙}{\lor} D) \underset{˙}{\land} W)) = S$
35	25 26 27 29 30 33 34	syl321anc	$⊢ (((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 (P \neq Q \land (R \in A \land \neg R \underset{˙}{\leq} W) \land (S \in A \land \neg S \underset{˙}{\leq} W)) \land (R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \to (D \underset{˙}{\lor} X) \underset{˙}{\land} (Q \underset{˙}{\lor} ((P \underset{˙}{\lor} D) \underset{˙}{\land} W)) = S$
36	24 35	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 (P \neq Q \land (R \in A \land \neg R \underset{˙}{\leq} W) \land (S \in A \land \neg S \underset{˙}{\leq} W)) \land (R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \to (D \underset{˙}{\lor} U) \underset{˙}{\land} (Q \underset{˙}{\lor} ((P \underset{˙}{\lor} D) \underset{˙}{\land} W)) = S$
37	13 36	syl5eq	$⊢ (((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 (P \neq Q \land (R \in A \land \neg R \underset{˙}{\leq} W) \land (S \in A \land \neg S \underset{˙}{\leq} W)) \land (R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \to E = S$
38	37	oveq2d	$⊢ (((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 (P \neq Q \land (R \in A \land \neg R \underset{˙}{\leq} W) \land (S \in A \land \neg S \underset{˙}{\leq} W)) \land (R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \to Z \underset{˙}{\lor} E = Z \underset{˙}{\lor} S$
39	38	eqcomd	$⊢ (((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 (P \neq Q \land (R \in A \land \neg R \underset{˙}{\leq} W) \land (S \in A \land \neg S \underset{˙}{\leq} W)) \land (R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \to Z \underset{˙}{\lor} S = Z \underset{˙}{\lor} E$

Metamath Proof Explorer

Theorem cdleme43dN

Proof