dalem19

Description: Lemma for dath . Show that a second dummy atom d exists outside of the Y and Z planes (when those planes are equal). (Contributed by NM, 15-Aug-2012)

	Ref	Expression
Hypotheses	dalema.ph	$⊢ φ \leftrightarrow (((K \in HL \land C \in {Base}_{K}) \land (P \in A \land Q \in A \land R \in A) \land (S \in A \land T \in A \land U \in A)) \land (Y \in O \land Z \in O) \land ((\neg C \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg C \underset{˙}{\leq} (Q \underset{˙}{\lor} R) \land \neg C \underset{˙}{\leq} (R \underset{˙}{\lor} P)) \land (\neg C \underset{˙}{\leq} (S \underset{˙}{\lor} T) \land \neg C \underset{˙}{\leq} (T \underset{˙}{\lor} U) \land \neg C \underset{˙}{\leq} (U \underset{˙}{\lor} S)) \land (C \underset{˙}{\leq} (P \underset{˙}{\lor} S) \land C \underset{˙}{\leq} (Q \underset{˙}{\lor} T) \land C \underset{˙}{\leq} (R \underset{˙}{\lor} U))))$
	dalemc.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
	dalemc.j	$⊢ \underset{˙}{\lor} = join (K)$
	dalemc.a	$⊢ A = Atoms (K)$
	dalem19.o	$⊢ O = LPlanes (K)$
	dalem19.y	$⊢ Y = (P \underset{˙}{\lor} Q) \underset{˙}{\lor} R$
	dalem19.z	$⊢ Z = (S \underset{˙}{\lor} T) \underset{˙}{\lor} U$
Assertion	dalem19	$⊢ (((φ \land Y = Z) \land c \in A) \land \neg c \underset{˙}{\leq} Y) \to \exists d \in A (d \neq c \land \neg d \underset{˙}{\leq} Y \land C \underset{˙}{\leq} (c \underset{˙}{\lor} d))$

Proof

Step	Hyp	Ref	Expression
1		dalema.ph	$⊢ φ \leftrightarrow (((K \in HL \land C \in {Base}_{K}) \land (P \in A \land Q \in A \land R \in A) \land (S \in A \land T \in A \land U \in A)) \land (Y \in O \land Z \in O) \land ((\neg C \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg C \underset{˙}{\leq} (Q \underset{˙}{\lor} R) \land \neg C \underset{˙}{\leq} (R \underset{˙}{\lor} P)) \land (\neg C \underset{˙}{\leq} (S \underset{˙}{\lor} T) \land \neg C \underset{˙}{\leq} (T \underset{˙}{\lor} U) \land \neg C \underset{˙}{\leq} (U \underset{˙}{\lor} S)) \land (C \underset{˙}{\leq} (P \underset{˙}{\lor} S) \land C \underset{˙}{\leq} (Q \underset{˙}{\lor} T) \land C \underset{˙}{\leq} (R \underset{˙}{\lor} U))))$
2		dalemc.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
3		dalemc.j	$⊢ \underset{˙}{\lor} = join (K)$
4		dalemc.a	$⊢ A = Atoms (K)$
5		dalem19.o	$⊢ O = LPlanes (K)$
6		dalem19.y	$⊢ Y = (P \underset{˙}{\lor} Q) \underset{˙}{\lor} R$
7		dalem19.z	$⊢ Z = (S \underset{˙}{\lor} T) \underset{˙}{\lor} U$
8	1	dalemkehl	$⊢ φ \to K \in HL$
9	8	ad3antrrr	$⊢ (((φ \land Y = Z) \land c \in A) \land \neg c \underset{˙}{\leq} Y) \to K \in HL$
10	1 2 3 4 5 6	dalemcea	$⊢ φ \to C \in A$
11	10	ad3antrrr	$⊢ (((φ \land Y = Z) \land c \in A) \land \neg c \underset{˙}{\leq} Y) \to C \in A$
12		simplr	$⊢ (((φ \land Y = Z) \land c \in A) \land \neg c \underset{˙}{\leq} Y) \to c \in A$
13	1 5	dalemyeb	$⊢ φ \to Y \in {Base}_{K}$
14	13	ad3antrrr	$⊢ (((φ \land Y = Z) \land c \in A) \land \neg c \underset{˙}{\leq} Y) \to Y \in {Base}_{K}$
15	1 2 3 4 5 6 7	dalem17	$⊢ (φ \land Y = Z) \to C \underset{˙}{\leq} Y$
16	15	ad2antrr	$⊢ (((φ \land Y = Z) \land c \in A) \land \neg c \underset{˙}{\leq} Y) \to C \underset{˙}{\leq} Y$
17		simpr	$⊢ (((φ \land Y = Z) \land c \in A) \land \neg c \underset{˙}{\leq} Y) \to \neg c \underset{˙}{\leq} Y$
18		eqid	$⊢ {Base}_{K} = {Base}_{K}$
19	18 2 3 4	atbtwnex	$⊢ ((K \in HL \land C \in A \land c \in A) \land (Y \in {Base}_{K} \land C \underset{˙}{\leq} Y \land \neg c \underset{˙}{\leq} Y)) \to \exists d \in A (d \neq c \land \neg d \underset{˙}{\leq} Y \land C \underset{˙}{\leq} (c \underset{˙}{\lor} d))$
20	9 11 12 14 16 17 19	syl33anc	$⊢ (((φ \land Y = Z) \land c \in A) \land \neg c \underset{˙}{\leq} Y) \to \exists d \in A (d \neq c \land \neg d \underset{˙}{\leq} Y \land C \underset{˙}{\leq} (c \underset{˙}{\lor} d))$

Metamath Proof Explorer

Theorem dalem19

Proof