This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem cdleme21g

Description: Part of proof of Lemma E in Crawley p. 115. (Contributed by NM, 29-Nov-2012)

		Ref	Expression
	Hypotheses	cdleme21.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
		cdleme21.j	$⊢ \underset{˙}{\lor} = join (K)$
		cdleme21.m	$⊢ \underset{˙}{\land} = meet (K)$
		cdleme21.a	$⊢ A = Atoms (K)$
		cdleme21.h	$⊢ H = LHyp (K)$
		cdleme21.u	$⊢ U = (P \underset{˙}{\lor} Q) \underset{˙}{\land} W$
		cdleme21.f	$⊢ F = (S \underset{˙}{\lor} U) \underset{˙}{\land} (Q \underset{˙}{\lor} ((P \underset{˙}{\lor} S) \underset{˙}{\land} W))$
		cdleme21g.g	$⊢ G = (T \underset{˙}{\lor} U) \underset{˙}{\land} (Q \underset{˙}{\lor} ((P \underset{˙}{\lor} T) \underset{˙}{\land} W))$
		cdleme21g.d	$⊢ D = (R \underset{˙}{\lor} S) \underset{˙}{\land} W$
		cdleme21g.y	$⊢ Y = (R \underset{˙}{\lor} T) \underset{˙}{\land} W$
		cdleme21g.n	$⊢ N = (P \underset{˙}{\lor} Q) \underset{˙}{\land} (F \underset{˙}{\lor} D)$
		cdleme21g.o	$⊢ O = (P \underset{˙}{\lor} Q) \underset{˙}{\land} (G \underset{˙}{\lor} Y)$
	Assertion	cdleme21g	$⊢ (((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 \neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg T \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \land ((R \in A \land \neg R \underset{˙}{\leq} W) \land (R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land U \underset{˙}{\leq} (S \underset{˙}{\lor} T)) \land ((z \in A \land \neg z \underset{˙}{\leq} W) \land P \underset{˙}{\lor} z = S \underset{˙}{\lor} z))) \to N = O$

Proof

Step	Hyp	Ref	Expression
1		cdleme21.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
2		cdleme21.j	$⊢ \underset{˙}{\lor} = join (K)$
3		cdleme21.m	$⊢ \underset{˙}{\land} = meet (K)$
4		cdleme21.a	$⊢ A = Atoms (K)$
5		cdleme21.h	$⊢ H = LHyp (K)$
6		cdleme21.u	$⊢ U = (P \underset{˙}{\lor} Q) \underset{˙}{\land} W$
7		cdleme21.f	$⊢ F = (S \underset{˙}{\lor} U) \underset{˙}{\land} (Q \underset{˙}{\lor} ((P \underset{˙}{\lor} S) \underset{˙}{\land} W))$
8		cdleme21g.g	$⊢ G = (T \underset{˙}{\lor} U) \underset{˙}{\land} (Q \underset{˙}{\lor} ((P \underset{˙}{\lor} T) \underset{˙}{\land} W))$
9		cdleme21g.d	$⊢ D = (R \underset{˙}{\lor} S) \underset{˙}{\land} W$
10		cdleme21g.y	$⊢ Y = (R \underset{˙}{\lor} T) \underset{˙}{\land} W$
11		cdleme21g.n	$⊢ N = (P \underset{˙}{\lor} Q) \underset{˙}{\land} (F \underset{˙}{\lor} D)$
12		cdleme21g.o	$⊢ O = (P \underset{˙}{\lor} Q) \underset{˙}{\land} (G \underset{˙}{\lor} Y)$
13		eqid	$⊢ (z \underset{˙}{\lor} U) \underset{˙}{\land} (Q \underset{˙}{\lor} ((P \underset{˙}{\lor} z) \underset{˙}{\land} W)) = (z \underset{˙}{\lor} U) \underset{˙}{\land} (Q \underset{˙}{\lor} ((P \underset{˙}{\lor} z) \underset{˙}{\land} W))$
14		eqid	$⊢ (R \underset{˙}{\lor} z) \underset{˙}{\land} W = (R \underset{˙}{\lor} z) \underset{˙}{\land} W$
15		eqid	$⊢ (P \underset{˙}{\lor} Q) \underset{˙}{\land} (((z \underset{˙}{\lor} U) \underset{˙}{\land} (Q \underset{˙}{\lor} ((P \underset{˙}{\lor} z) \underset{˙}{\land} W))) \underset{˙}{\lor} ((R \underset{˙}{\lor} z) \underset{˙}{\land} W)) = (P \underset{˙}{\lor} Q) \underset{˙}{\land} (((z \underset{˙}{\lor} U) \underset{˙}{\land} (Q \underset{˙}{\lor} ((P \underset{˙}{\lor} z) \underset{˙}{\land} W))) \underset{˙}{\lor} ((R \underset{˙}{\lor} z) \underset{˙}{\land} W))$
16	1 2 3 4 5 6 7 13 9 14 11 15 8 10 12	cdleme21f	$⊢ (((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 \neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg T \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \land ((R \in A \land \neg R \underset{˙}{\leq} W) \land (R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land U \underset{˙}{\leq} (S \underset{˙}{\lor} T)) \land ((z \in A \land \neg z \underset{˙}{\leq} W) \land P \underset{˙}{\lor} z = S \underset{˙}{\lor} z))) \to N = O$