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

Metamath Proof Explorer

Theorem cdleme19f

Description: Part of proof of Lemma E in Crawley p. 113, 5th paragraph on p. 114, line 3. D , F , N , Y , G , O represent s_2, f(s), f_s(r), t_2, f(t), f_t(r). We prove that if r <_ s \/ t, then f_t(r) = f_t(r). (Contributed by NM, 14-Nov-2012)

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

Proof

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