cdleme27N

Description: Part of proof of Lemma E in Crawley p. 113. Eliminate the s =/= t antecedent in cdleme27a . (Contributed by NM, 3-Feb-2013) (New usage is discouraged.)

	Ref	Expression
Hypotheses	cdleme26.b	$⊢ B = {Base}_{K}$
	cdleme26.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
	cdleme26.j	$⊢ \underset{˙}{\lor} = join (K)$
	cdleme26.m	$⊢ \underset{˙}{\land} = meet (K)$
	cdleme26.a	$⊢ A = Atoms (K)$
	cdleme26.h	$⊢ H = LHyp (K)$
	cdleme27.u	$⊢ U = (P \underset{˙}{\lor} Q) \underset{˙}{\land} W$
	cdleme27.f	$⊢ F = (s \underset{˙}{\lor} U) \underset{˙}{\land} (Q \underset{˙}{\lor} ((P \underset{˙}{\lor} s) \underset{˙}{\land} W))$
	cdleme27.z	$⊢ Z = (z \underset{˙}{\lor} U) \underset{˙}{\land} (Q \underset{˙}{\lor} ((P \underset{˙}{\lor} z) \underset{˙}{\land} W))$
	cdleme27.n	$⊢ N = (P \underset{˙}{\lor} Q) \underset{˙}{\land} (Z \underset{˙}{\lor} ((s \underset{˙}{\lor} z) \underset{˙}{\land} W))$
	cdleme27.d	$⊢ D = (ι u \in B \| \forall z \in A ((\neg z \underset{˙}{\leq} W \land \neg z \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \to u = N))$
	cdleme27.c	$⊢ C = if (s \underset{˙}{\leq} (P \underset{˙}{\lor} Q), D, F)$
	cdleme27.g	$⊢ G = (t \underset{˙}{\lor} U) \underset{˙}{\land} (Q \underset{˙}{\lor} ((P \underset{˙}{\lor} t) \underset{˙}{\land} W))$
	cdleme27.o	$⊢ O = (P \underset{˙}{\lor} Q) \underset{˙}{\land} (Z \underset{˙}{\lor} ((t \underset{˙}{\lor} z) \underset{˙}{\land} W))$
	cdleme27.e	$⊢ E = (ι u \in B \| \forall z \in A ((\neg z \underset{˙}{\leq} W \land \neg z \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \to u = O))$
	cdleme27.y	$⊢ Y = if (t \underset{˙}{\leq} (P \underset{˙}{\lor} Q), E, G)$
Assertion	cdleme27N	$⊢ (((K \in HL \land W \in H) \land P \neq Q \land (s \in A \land \neg s \underset{˙}{\leq} W)) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W) \land (t \in A \land \neg t \underset{˙}{\leq} W)) \land (s \underset{˙}{\leq} (t \underset{˙}{\lor} V) \land (V \in A \land V \underset{˙}{\leq} W))) \to C \underset{˙}{\leq} (Y \underset{˙}{\lor} V)$

Proof

Step	Hyp	Ref	Expression
1		cdleme26.b	$⊢ B = {Base}_{K}$
2		cdleme26.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
3		cdleme26.j	$⊢ \underset{˙}{\lor} = join (K)$
4		cdleme26.m	$⊢ \underset{˙}{\land} = meet (K)$
5		cdleme26.a	$⊢ A = Atoms (K)$
6		cdleme26.h	$⊢ H = LHyp (K)$
7		cdleme27.u	$⊢ U = (P \underset{˙}{\lor} Q) \underset{˙}{\land} W$
8		cdleme27.f	$⊢ F = (s \underset{˙}{\lor} U) \underset{˙}{\land} (Q \underset{˙}{\lor} ((P \underset{˙}{\lor} s) \underset{˙}{\land} W))$
9		cdleme27.z	$⊢ Z = (z \underset{˙}{\lor} U) \underset{˙}{\land} (Q \underset{˙}{\lor} ((P \underset{˙}{\lor} z) \underset{˙}{\land} W))$
10		cdleme27.n	$⊢ N = (P \underset{˙}{\lor} Q) \underset{˙}{\land} (Z \underset{˙}{\lor} ((s \underset{˙}{\lor} z) \underset{˙}{\land} W))$
11		cdleme27.d	$⊢ D = (ι u \in B \| \forall z \in A ((\neg z \underset{˙}{\leq} W \land \neg z \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \to u = N))$
12		cdleme27.c	$⊢ C = if (s \underset{˙}{\leq} (P \underset{˙}{\lor} Q), D, F)$
13		cdleme27.g	$⊢ G = (t \underset{˙}{\lor} U) \underset{˙}{\land} (Q \underset{˙}{\lor} ((P \underset{˙}{\lor} t) \underset{˙}{\land} W))$
14		cdleme27.o	$⊢ O = (P \underset{˙}{\lor} Q) \underset{˙}{\land} (Z \underset{˙}{\lor} ((t \underset{˙}{\lor} z) \underset{˙}{\land} W))$
15		cdleme27.e	$⊢ E = (ι u \in B \| \forall z \in A ((\neg z \underset{˙}{\leq} W \land \neg z \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \to u = O))$
16		cdleme27.y	$⊢ Y = if (t \underset{˙}{\leq} (P \underset{˙}{\lor} Q), E, G)$
17	1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16	cdleme27b	$⊢ s = t \to C = Y$
18	17	adantl	$⊢ ((((K \in HL \land W \in H) \land P \neq Q \land (s \in A \land \neg s \underset{˙}{\leq} W)) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W) \land (t \in A \land \neg t \underset{˙}{\leq} W)) \land (s \underset{˙}{\leq} (t \underset{˙}{\lor} V) \land (V \in A \land V \underset{˙}{\leq} W))) \land s = t) \to C = Y$
19		simp11l	$⊢ (((K \in HL \land W \in H) \land P \neq Q \land (s \in A \land \neg s \underset{˙}{\leq} W)) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W) \land (t \in A \land \neg t \underset{˙}{\leq} W)) \land (s \underset{˙}{\leq} (t \underset{˙}{\lor} V) \land (V \in A \land V \underset{˙}{\leq} W))) \to K \in HL$
20	19	hllatd	$⊢ (((K \in HL \land W \in H) \land P \neq Q \land (s \in A \land \neg s \underset{˙}{\leq} W)) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W) \land (t \in A \land \neg t \underset{˙}{\leq} W)) \land (s \underset{˙}{\leq} (t \underset{˙}{\lor} V) \land (V \in A \land V \underset{˙}{\leq} W))) \to K \in Lat$
21		simp11r	$⊢ (((K \in HL \land W \in H) \land P \neq Q \land (s \in A \land \neg s \underset{˙}{\leq} W)) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W) \land (t \in A \land \neg t \underset{˙}{\leq} W)) \land (s \underset{˙}{\leq} (t \underset{˙}{\lor} V) \land (V \in A \land V \underset{˙}{\leq} W))) \to W \in H$
22		simp21	$⊢ (((K \in HL \land W \in H) \land P \neq Q \land (s \in A \land \neg s \underset{˙}{\leq} W)) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W) \land (t \in A \land \neg t \underset{˙}{\leq} W)) \land (s \underset{˙}{\leq} (t \underset{˙}{\lor} V) \land (V \in A \land V \underset{˙}{\leq} W))) \to (P \in A \land \neg P \underset{˙}{\leq} W)$
23		simp22	$⊢ (((K \in HL \land W \in H) \land P \neq Q \land (s \in A \land \neg s \underset{˙}{\leq} W)) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W) \land (t \in A \land \neg t \underset{˙}{\leq} W)) \land (s \underset{˙}{\leq} (t \underset{˙}{\lor} V) \land (V \in A \land V \underset{˙}{\leq} W))) \to (Q \in A \land \neg Q \underset{˙}{\leq} W)$
24		simp23	$⊢ (((K \in HL \land W \in H) \land P \neq Q \land (s \in A \land \neg s \underset{˙}{\leq} W)) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W) \land (t \in A \land \neg t \underset{˙}{\leq} W)) \land (s \underset{˙}{\leq} (t \underset{˙}{\lor} V) \land (V \in A \land V \underset{˙}{\leq} W))) \to (t \in A \land \neg t \underset{˙}{\leq} W)$
25		simp12	$⊢ (((K \in HL \land W \in H) \land P \neq Q \land (s \in A \land \neg s \underset{˙}{\leq} W)) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W) \land (t \in A \land \neg t \underset{˙}{\leq} W)) \land (s \underset{˙}{\leq} (t \underset{˙}{\lor} V) \land (V \in A \land V \underset{˙}{\leq} W))) \to P \neq Q$
26	1 2 3 4 5 6 7 13 9 14 15 16	cdleme27cl	$⊢ ((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 ((t \in A \land \neg t \underset{˙}{\leq} W) \land P \neq Q)) \to Y \in B$
27	19 21 22 23 24 25 26	syl222anc	$⊢ (((K \in HL \land W \in H) \land P \neq Q \land (s \in A \land \neg s \underset{˙}{\leq} W)) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W) \land (t \in A \land \neg t \underset{˙}{\leq} W)) \land (s \underset{˙}{\leq} (t \underset{˙}{\lor} V) \land (V \in A \land V \underset{˙}{\leq} W))) \to Y \in B$
28		simp3rl	$⊢ (((K \in HL \land W \in H) \land P \neq Q \land (s \in A \land \neg s \underset{˙}{\leq} W)) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W) \land (t \in A \land \neg t \underset{˙}{\leq} W)) \land (s \underset{˙}{\leq} (t \underset{˙}{\lor} V) \land (V \in A \land V \underset{˙}{\leq} W))) \to V \in A$
29	1 5	atbase	$⊢ V \in A \to V \in B$
30	28 29	syl	$⊢ (((K \in HL \land W \in H) \land P \neq Q \land (s \in A \land \neg s \underset{˙}{\leq} W)) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W) \land (t \in A \land \neg t \underset{˙}{\leq} W)) \land (s \underset{˙}{\leq} (t \underset{˙}{\lor} V) \land (V \in A \land V \underset{˙}{\leq} W))) \to V \in B$
31	1 2 3	latlej1	$⊢ (K \in Lat \land Y \in B \land V \in B) \to Y \underset{˙}{\leq} (Y \underset{˙}{\lor} V)$
32	20 27 30 31	syl3anc	$⊢ (((K \in HL \land W \in H) \land P \neq Q \land (s \in A \land \neg s \underset{˙}{\leq} W)) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W) \land (t \in A \land \neg t \underset{˙}{\leq} W)) \land (s \underset{˙}{\leq} (t \underset{˙}{\lor} V) \land (V \in A \land V \underset{˙}{\leq} W))) \to Y \underset{˙}{\leq} (Y \underset{˙}{\lor} V)$
33	32	adantr	$⊢ ((((K \in HL \land W \in H) \land P \neq Q \land (s \in A \land \neg s \underset{˙}{\leq} W)) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W) \land (t \in A \land \neg t \underset{˙}{\leq} W)) \land (s \underset{˙}{\leq} (t \underset{˙}{\lor} V) \land (V \in A \land V \underset{˙}{\leq} W))) \land s = t) \to Y \underset{˙}{\leq} (Y \underset{˙}{\lor} V)$
34	18 33	eqbrtrd	$⊢ ((((K \in HL \land W \in H) \land P \neq Q \land (s \in A \land \neg s \underset{˙}{\leq} W)) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W) \land (t \in A \land \neg t \underset{˙}{\leq} W)) \land (s \underset{˙}{\leq} (t \underset{˙}{\lor} V) \land (V \in A \land V \underset{˙}{\leq} W))) \land s = t) \to C \underset{˙}{\leq} (Y \underset{˙}{\lor} V)$
35		simpl11	$⊢ ((((K \in HL \land W \in H) \land P \neq Q \land (s \in A \land \neg s \underset{˙}{\leq} W)) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W) \land (t \in A \land \neg t \underset{˙}{\leq} W)) \land (s \underset{˙}{\leq} (t \underset{˙}{\lor} V) \land (V \in A \land V \underset{˙}{\leq} W))) \land s \neq t) \to (K \in HL \land W \in H)$
36		simpl12	$⊢ ((((K \in HL \land W \in H) \land P \neq Q \land (s \in A \land \neg s \underset{˙}{\leq} W)) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W) \land (t \in A \land \neg t \underset{˙}{\leq} W)) \land (s \underset{˙}{\leq} (t \underset{˙}{\lor} V) \land (V \in A \land V \underset{˙}{\leq} W))) \land s \neq t) \to P \neq Q$
37		simpl13	$⊢ ((((K \in HL \land W \in H) \land P \neq Q \land (s \in A \land \neg s \underset{˙}{\leq} W)) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W) \land (t \in A \land \neg t \underset{˙}{\leq} W)) \land (s \underset{˙}{\leq} (t \underset{˙}{\lor} V) \land (V \in A \land V \underset{˙}{\leq} W))) \land s \neq t) \to (s \in A \land \neg s \underset{˙}{\leq} W)$
38		simpl21	$⊢ ((((K \in HL \land W \in H) \land P \neq Q \land (s \in A \land \neg s \underset{˙}{\leq} W)) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W) \land (t \in A \land \neg t \underset{˙}{\leq} W)) \land (s \underset{˙}{\leq} (t \underset{˙}{\lor} V) \land (V \in A \land V \underset{˙}{\leq} W))) \land s \neq t) \to (P \in A \land \neg P \underset{˙}{\leq} W)$
39		simpl22	$⊢ ((((K \in HL \land W \in H) \land P \neq Q \land (s \in A \land \neg s \underset{˙}{\leq} W)) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W) \land (t \in A \land \neg t \underset{˙}{\leq} W)) \land (s \underset{˙}{\leq} (t \underset{˙}{\lor} V) \land (V \in A \land V \underset{˙}{\leq} W))) \land s \neq t) \to (Q \in A \land \neg Q \underset{˙}{\leq} W)$
40		simpl23	$⊢ ((((K \in HL \land W \in H) \land P \neq Q \land (s \in A \land \neg s \underset{˙}{\leq} W)) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W) \land (t \in A \land \neg t \underset{˙}{\leq} W)) \land (s \underset{˙}{\leq} (t \underset{˙}{\lor} V) \land (V \in A \land V \underset{˙}{\leq} W))) \land s \neq t) \to (t \in A \land \neg t \underset{˙}{\leq} W)$
41		simpr	$⊢ ((((K \in HL \land W \in H) \land P \neq Q \land (s \in A \land \neg s \underset{˙}{\leq} W)) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W) \land (t \in A \land \neg t \underset{˙}{\leq} W)) \land (s \underset{˙}{\leq} (t \underset{˙}{\lor} V) \land (V \in A \land V \underset{˙}{\leq} W))) \land s \neq t) \to s \neq t$
42		simpl3l	$⊢ ((((K \in HL \land W \in H) \land P \neq Q \land (s \in A \land \neg s \underset{˙}{\leq} W)) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W) \land (t \in A \land \neg t \underset{˙}{\leq} W)) \land (s \underset{˙}{\leq} (t \underset{˙}{\lor} V) \land (V \in A \land V \underset{˙}{\leq} W))) \land s \neq t) \to s \underset{˙}{\leq} (t \underset{˙}{\lor} V)$
43	41 42	jca	$⊢ ((((K \in HL \land W \in H) \land P \neq Q \land (s \in A \land \neg s \underset{˙}{\leq} W)) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W) \land (t \in A \land \neg t \underset{˙}{\leq} W)) \land (s \underset{˙}{\leq} (t \underset{˙}{\lor} V) \land (V \in A \land V \underset{˙}{\leq} W))) \land s \neq t) \to (s \neq t \land s \underset{˙}{\leq} (t \underset{˙}{\lor} V))$
44		simpl3r	$⊢ ((((K \in HL \land W \in H) \land P \neq Q \land (s \in A \land \neg s \underset{˙}{\leq} W)) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W) \land (t \in A \land \neg t \underset{˙}{\leq} W)) \land (s \underset{˙}{\leq} (t \underset{˙}{\lor} V) \land (V \in A \land V \underset{˙}{\leq} W))) \land s \neq t) \to (V \in A \land V \underset{˙}{\leq} W)$
45	1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16	cdleme27a	$⊢ (((K \in HL \land W \in H) \land P \neq Q \land (s \in A \land \neg s \underset{˙}{\leq} W)) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W) \land (t \in A \land \neg t \underset{˙}{\leq} W)) \land ((s \neq t \land s \underset{˙}{\leq} (t \underset{˙}{\lor} V)) \land (V \in A \land V \underset{˙}{\leq} W))) \to C \underset{˙}{\leq} (Y \underset{˙}{\lor} V)$
46	35 36 37 38 39 40 43 44 45	syl332anc	$⊢ ((((K \in HL \land W \in H) \land P \neq Q \land (s \in A \land \neg s \underset{˙}{\leq} W)) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W) \land (t \in A \land \neg t \underset{˙}{\leq} W)) \land (s \underset{˙}{\leq} (t \underset{˙}{\lor} V) \land (V \in A \land V \underset{˙}{\leq} W))) \land s \neq t) \to C \underset{˙}{\leq} (Y \underset{˙}{\lor} V)$
47	34 46	pm2.61dane	$⊢ (((K \in HL \land W \in H) \land P \neq Q \land (s \in A \land \neg s \underset{˙}{\leq} W)) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W) \land (t \in A \land \neg t \underset{˙}{\leq} W)) \land (s \underset{˙}{\leq} (t \underset{˙}{\lor} V) \land (V \in A \land V \underset{˙}{\leq} W))) \to C \underset{˙}{\leq} (Y \underset{˙}{\lor} V)$

Metamath Proof Explorer

Theorem cdleme27N

Proof