dalem28

Description: Lemma for dath . Lemma dalem27 expressed differently. (Contributed by NM, 4-Aug-2012)

	Ref	Expression
Hypotheses	dalem.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))))$
	dalem.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
	dalem.j	$⊢ \underset{˙}{\lor} = join (K)$
	dalem.a	$⊢ A = Atoms (K)$
	dalem.ps	$⊢ ψ \leftrightarrow ((c \in A \land d \in A) \land \neg c \underset{˙}{\leq} Y \land (d \neq c \land \neg d \underset{˙}{\leq} Y \land C \underset{˙}{\leq} (c \underset{˙}{\lor} d)))$
	dalem23.m	$⊢ \underset{˙}{\land} = meet (K)$
	dalem23.o	$⊢ O = LPlanes (K)$
	dalem23.y	$⊢ Y = (P \underset{˙}{\lor} Q) \underset{˙}{\lor} R$
	dalem23.z	$⊢ Z = (S \underset{˙}{\lor} T) \underset{˙}{\lor} U$
	dalem23.g	$⊢ G = (c \underset{˙}{\lor} P) \underset{˙}{\land} (d \underset{˙}{\lor} S)$
Assertion	dalem28	$⊢ (φ \land Y = Z \land ψ) \to P \underset{˙}{\leq} (G \underset{˙}{\lor} c)$

Proof

Step	Hyp	Ref	Expression
1		dalem.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		dalem.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
3		dalem.j	$⊢ \underset{˙}{\lor} = join (K)$
4		dalem.a	$⊢ A = Atoms (K)$
5		dalem.ps	$⊢ ψ \leftrightarrow ((c \in A \land d \in A) \land \neg c \underset{˙}{\leq} Y \land (d \neq c \land \neg d \underset{˙}{\leq} Y \land C \underset{˙}{\leq} (c \underset{˙}{\lor} d)))$
6		dalem23.m	$⊢ \underset{˙}{\land} = meet (K)$
7		dalem23.o	$⊢ O = LPlanes (K)$
8		dalem23.y	$⊢ Y = (P \underset{˙}{\lor} Q) \underset{˙}{\lor} R$
9		dalem23.z	$⊢ Z = (S \underset{˙}{\lor} T) \underset{˙}{\lor} U$
10		dalem23.g	$⊢ G = (c \underset{˙}{\lor} P) \underset{˙}{\land} (d \underset{˙}{\lor} S)$
11	1 2 3 4 5 6 7 8 9 10	dalem27	$⊢ (φ \land Y = Z \land ψ) \to c \underset{˙}{\leq} (G \underset{˙}{\lor} P)$
12	1	dalemkehl	$⊢ φ \to K \in HL$
13	12	3ad2ant1	$⊢ (φ \land Y = Z \land ψ) \to K \in HL$
14	5	dalemccea	$⊢ ψ \to c \in A$
15	14	3ad2ant3	$⊢ (φ \land Y = Z \land ψ) \to c \in A$
16	1	dalempea	$⊢ φ \to P \in A$
17	16	3ad2ant1	$⊢ (φ \land Y = Z \land ψ) \to P \in A$
18	1 2 3 4 5 6 7 8 9 10	dalem23	$⊢ (φ \land Y = Z \land ψ) \to G \in A$
19	1 2 3 4 5 6 7 8 9 10	dalem25	$⊢ (φ \land Y = Z \land ψ) \to c \neq G$
20	2 3 4	hlatexch1	$⊢ (K \in HL \land (c \in A \land P \in A \land G \in A) \land c \neq G) \to (c \underset{˙}{\leq} (G \underset{˙}{\lor} P) \to P \underset{˙}{\leq} (G \underset{˙}{\lor} c))$
21	13 15 17 18 19 20	syl131anc	$⊢ (φ \land Y = Z \land ψ) \to (c \underset{˙}{\leq} (G \underset{˙}{\lor} P) \to P \underset{˙}{\leq} (G \underset{˙}{\lor} c))$
22	11 21	mpd	$⊢ (φ \land Y = Z \land ψ) \to P \underset{˙}{\leq} (G \underset{˙}{\lor} c)$

Metamath Proof Explorer

Theorem dalem28

Proof