cdleme21h

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	cdleme21h	$⊢ (((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)))) \to (\exists z \in A (\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		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 \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 ((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))$
14		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 \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 ((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)))$
15		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 \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 (R \in A \land \neg R \underset{˙}{\leq} W)$
16		simp13r	$⊢ ((((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 (R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land U \underset{˙}{\leq} (S \underset{˙}{\lor} T))$
17		simp2	$⊢ ((((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 z \in A$
18		simp3l	$⊢ ((((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 \neg z \underset{˙}{\leq} W$
19		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 ((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 P \underset{˙}{\lor} z = S \underset{˙}{\lor} z$
20	17 18 19	jca31	$⊢ ((((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 ((z \in A \land \neg z \underset{˙}{\leq} W) \land P \underset{˙}{\lor} z = S \underset{˙}{\lor} z)$
21	1 2 3 4 5 6 7 8 9 10 11 12	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$
22	13 14 15 16 20 21	syl113anc	$⊢ ((((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$
23	22	rexlimdv3a	$⊢ (((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)))) \to (\exists z \in A (\neg z \underset{˙}{\leq} W \land P \underset{˙}{\lor} z = S \underset{˙}{\lor} z) \to N = O)$

Metamath Proof Explorer

Theorem cdleme21h

Proof