cdleme39n

Description: Part of proof of Lemma E in Crawley p. 113. Show that f(x) is one-to-one on P .\/ Q line. TODO: FIX COMMENT. E , Y , G , Z serve as f(t), f(u), f_t( R ), f_t( S ). Put hypotheses of cdleme38n in convention of cdleme32sn1awN . TODO see if this hypothesis conversion would be better if done earlier. (Contributed by NM, 15-Mar-2013)

	Ref	Expression
Hypotheses	cdleme39.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
	cdleme39.j	$⊢ \underset{˙}{\lor} = join (K)$
	cdleme39.m	$⊢ \underset{˙}{\land} = meet (K)$
	cdleme39.a	$⊢ A = Atoms (K)$
	cdleme39.h	$⊢ H = LHyp (K)$
	cdleme39.u	$⊢ U = (P \underset{˙}{\lor} Q) \underset{˙}{\land} W$
	cdleme39.e	$⊢ E = (t \underset{˙}{\lor} U) \underset{˙}{\land} (Q \underset{˙}{\lor} ((P \underset{˙}{\lor} t) \underset{˙}{\land} W))$
	cdleme39.g	$⊢ G = (P \underset{˙}{\lor} Q) \underset{˙}{\land} (E \underset{˙}{\lor} ((R \underset{˙}{\lor} t) \underset{˙}{\land} W))$
	cdleme39.y	$⊢ Y = (u \underset{˙}{\lor} U) \underset{˙}{\land} (Q \underset{˙}{\lor} ((P \underset{˙}{\lor} u) \underset{˙}{\land} W))$
	cdleme39.z	$⊢ Z = (P \underset{˙}{\lor} Q) \underset{˙}{\land} (Y \underset{˙}{\lor} ((S \underset{˙}{\lor} u) \underset{˙}{\land} W))$
Assertion	cdleme39n	$⊢ (((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 (P \neq Q \land (R \in A \land \neg R \underset{˙}{\leq} W) \land (S \in A \land \neg S \underset{˙}{\leq} W)) \land ((R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land S \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land R \neq S) \land ((t \in A \land \neg t \underset{˙}{\leq} W) \land \neg t \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \land ((u \in A \land \neg u \underset{˙}{\leq} W) \land \neg u \underset{˙}{\leq} (P \underset{˙}{\lor} Q)))) \to G \neq Z$

Proof

Step	Hyp	Ref	Expression
1		cdleme39.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
2		cdleme39.j	$⊢ \underset{˙}{\lor} = join (K)$
3		cdleme39.m	$⊢ \underset{˙}{\land} = meet (K)$
4		cdleme39.a	$⊢ A = Atoms (K)$
5		cdleme39.h	$⊢ H = LHyp (K)$
6		cdleme39.u	$⊢ U = (P \underset{˙}{\lor} Q) \underset{˙}{\land} W$
7		cdleme39.e	$⊢ E = (t \underset{˙}{\lor} U) \underset{˙}{\land} (Q \underset{˙}{\lor} ((P \underset{˙}{\lor} t) \underset{˙}{\land} W))$
8		cdleme39.g	$⊢ G = (P \underset{˙}{\lor} Q) \underset{˙}{\land} (E \underset{˙}{\lor} ((R \underset{˙}{\lor} t) \underset{˙}{\land} W))$
9		cdleme39.y	$⊢ Y = (u \underset{˙}{\lor} U) \underset{˙}{\land} (Q \underset{˙}{\lor} ((P \underset{˙}{\lor} u) \underset{˙}{\land} W))$
10		cdleme39.z	$⊢ Z = (P \underset{˙}{\lor} Q) \underset{˙}{\land} (Y \underset{˙}{\lor} ((S \underset{˙}{\lor} u) \underset{˙}{\land} W))$
11		eqid	$⊢ (t \underset{˙}{\lor} E) \underset{˙}{\land} W = (t \underset{˙}{\lor} E) \underset{˙}{\land} W$
12		eqid	$⊢ (u \underset{˙}{\lor} Y) \underset{˙}{\land} W = (u \underset{˙}{\lor} Y) \underset{˙}{\land} W$
13		eqid	$⊢ (R \underset{˙}{\lor} ((t \underset{˙}{\lor} E) \underset{˙}{\land} W)) \underset{˙}{\land} (E \underset{˙}{\lor} ((t \underset{˙}{\lor} R) \underset{˙}{\land} W)) = (R \underset{˙}{\lor} ((t \underset{˙}{\lor} E) \underset{˙}{\land} W)) \underset{˙}{\land} (E \underset{˙}{\lor} ((t \underset{˙}{\lor} R) \underset{˙}{\land} W))$
14		eqid	$⊢ (S \underset{˙}{\lor} ((u \underset{˙}{\lor} Y) \underset{˙}{\land} W)) \underset{˙}{\land} (Y \underset{˙}{\lor} ((u \underset{˙}{\lor} S) \underset{˙}{\land} W)) = (S \underset{˙}{\lor} ((u \underset{˙}{\lor} Y) \underset{˙}{\land} W)) \underset{˙}{\land} (Y \underset{˙}{\lor} ((u \underset{˙}{\lor} S) \underset{˙}{\land} W))$
15	1 2 3 4 5 6 7 9 11 12 13 14	cdleme38n	$⊢ (((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 (P \neq Q \land (R \in A \land \neg R \underset{˙}{\leq} W) \land (S \in A \land \neg S \underset{˙}{\leq} W)) \land ((R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land S \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land R \neq S) \land ((t \in A \land \neg t \underset{˙}{\leq} W) \land \neg t \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \land ((u \in A \land \neg u \underset{˙}{\leq} W) \land \neg u \underset{˙}{\leq} (P \underset{˙}{\lor} Q)))) \to (R \underset{˙}{\lor} ((t \underset{˙}{\lor} E) \underset{˙}{\land} W)) \underset{˙}{\land} (E \underset{˙}{\lor} ((t \underset{˙}{\lor} R) \underset{˙}{\land} W)) \neq (S \underset{˙}{\lor} ((u \underset{˙}{\lor} Y) \underset{˙}{\land} W)) \underset{˙}{\land} (Y \underset{˙}{\lor} ((u \underset{˙}{\lor} S) \underset{˙}{\land} W))$
16		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 (P \neq Q \land (R \in A \land \neg R \underset{˙}{\leq} W) \land (S \in A \land \neg S \underset{˙}{\leq} W)) \land ((R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land S \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land R \neq S) \land ((t \in A \land \neg t \underset{˙}{\leq} W) \land \neg t \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \land ((u \in A \land \neg u \underset{˙}{\leq} W) \land \neg u \underset{˙}{\leq} (P \underset{˙}{\lor} Q)))) \to (K \in HL \land W \in H)$
17		simp12l	$⊢ (((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 (P \neq Q \land (R \in A \land \neg R \underset{˙}{\leq} W) \land (S \in A \land \neg S \underset{˙}{\leq} W)) \land ((R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land S \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land R \neq S) \land ((t \in A \land \neg t \underset{˙}{\leq} W) \land \neg t \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \land ((u \in A \land \neg u \underset{˙}{\leq} W) \land \neg u \underset{˙}{\leq} (P \underset{˙}{\lor} Q)))) \to P \in A$
18		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 (P \neq Q \land (R \in A \land \neg R \underset{˙}{\leq} W) \land (S \in A \land \neg S \underset{˙}{\leq} W)) \land ((R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land S \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land R \neq S) \land ((t \in A \land \neg t \underset{˙}{\leq} W) \land \neg t \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \land ((u \in A \land \neg u \underset{˙}{\leq} W) \land \neg u \underset{˙}{\leq} (P \underset{˙}{\lor} Q)))) \to Q \in A$
19		simp22l	$⊢ (((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 (P \neq Q \land (R \in A \land \neg R \underset{˙}{\leq} W) \land (S \in A \land \neg S \underset{˙}{\leq} W)) \land ((R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land S \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land R \neq S) \land ((t \in A \land \neg t \underset{˙}{\leq} W) \land \neg t \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \land ((u \in A \land \neg u \underset{˙}{\leq} W) \land \neg u \underset{˙}{\leq} (P \underset{˙}{\lor} Q)))) \to R \in A$
20		simp22r	$⊢ (((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 (P \neq Q \land (R \in A \land \neg R \underset{˙}{\leq} W) \land (S \in A \land \neg S \underset{˙}{\leq} W)) \land ((R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land S \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land R \neq S) \land ((t \in A \land \neg t \underset{˙}{\leq} W) \land \neg t \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \land ((u \in A \land \neg u \underset{˙}{\leq} W) \land \neg u \underset{˙}{\leq} (P \underset{˙}{\lor} Q)))) \to \neg R \underset{˙}{\leq} W$
21		simp311	$⊢ (((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 (P \neq Q \land (R \in A \land \neg R \underset{˙}{\leq} W) \land (S \in A \land \neg S \underset{˙}{\leq} W)) \land ((R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land S \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land R \neq S) \land ((t \in A \land \neg t \underset{˙}{\leq} W) \land \neg t \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \land ((u \in A \land \neg u \underset{˙}{\leq} W) \land \neg u \underset{˙}{\leq} (P \underset{˙}{\lor} Q)))) \to R \underset{˙}{\leq} (P \underset{˙}{\lor} Q)$
22		simp32l	$⊢ (((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 (P \neq Q \land (R \in A \land \neg R \underset{˙}{\leq} W) \land (S \in A \land \neg S \underset{˙}{\leq} W)) \land ((R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land S \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land R \neq S) \land ((t \in A \land \neg t \underset{˙}{\leq} W) \land \neg t \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \land ((u \in A \land \neg u \underset{˙}{\leq} W) \land \neg u \underset{˙}{\leq} (P \underset{˙}{\lor} Q)))) \to (t \in A \land \neg t \underset{˙}{\leq} W)$
23	1 2 3 4 5 6 7 8 11	cdleme39a	$⊢ (((K \in HL \land W \in H) \land P \in A \land Q \in A) \land (R \in A \land \neg R \underset{˙}{\leq} W) \land (R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land (t \in A \land \neg t \underset{˙}{\leq} W))) \to G = (R \underset{˙}{\lor} ((t \underset{˙}{\lor} E) \underset{˙}{\land} W)) \underset{˙}{\land} (E \underset{˙}{\lor} ((t \underset{˙}{\lor} R) \underset{˙}{\land} W))$
24	16 17 18 19 20 21 22 23	syl322anc	$⊢ (((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 (P \neq Q \land (R \in A \land \neg R \underset{˙}{\leq} W) \land (S \in A \land \neg S \underset{˙}{\leq} W)) \land ((R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land S \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land R \neq S) \land ((t \in A \land \neg t \underset{˙}{\leq} W) \land \neg t \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \land ((u \in A \land \neg u \underset{˙}{\leq} W) \land \neg u \underset{˙}{\leq} (P \underset{˙}{\lor} Q)))) \to G = (R \underset{˙}{\lor} ((t \underset{˙}{\lor} E) \underset{˙}{\land} W)) \underset{˙}{\land} (E \underset{˙}{\lor} ((t \underset{˙}{\lor} R) \underset{˙}{\land} W))$
25		simp23l	$⊢ (((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 (P \neq Q \land (R \in A \land \neg R \underset{˙}{\leq} W) \land (S \in A \land \neg S \underset{˙}{\leq} W)) \land ((R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land S \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land R \neq S) \land ((t \in A \land \neg t \underset{˙}{\leq} W) \land \neg t \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \land ((u \in A \land \neg u \underset{˙}{\leq} W) \land \neg u \underset{˙}{\leq} (P \underset{˙}{\lor} Q)))) \to S \in A$
26		simp23r	$⊢ (((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 (P \neq Q \land (R \in A \land \neg R \underset{˙}{\leq} W) \land (S \in A \land \neg S \underset{˙}{\leq} W)) \land ((R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land S \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land R \neq S) \land ((t \in A \land \neg t \underset{˙}{\leq} W) \land \neg t \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \land ((u \in A \land \neg u \underset{˙}{\leq} W) \land \neg u \underset{˙}{\leq} (P \underset{˙}{\lor} Q)))) \to \neg S \underset{˙}{\leq} W$
27		simp312	$⊢ (((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 (P \neq Q \land (R \in A \land \neg R \underset{˙}{\leq} W) \land (S \in A \land \neg S \underset{˙}{\leq} W)) \land ((R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land S \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land R \neq S) \land ((t \in A \land \neg t \underset{˙}{\leq} W) \land \neg t \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \land ((u \in A \land \neg u \underset{˙}{\leq} W) \land \neg u \underset{˙}{\leq} (P \underset{˙}{\lor} Q)))) \to S \underset{˙}{\leq} (P \underset{˙}{\lor} Q)$
28		simp33l	$⊢ (((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 (P \neq Q \land (R \in A \land \neg R \underset{˙}{\leq} W) \land (S \in A \land \neg S \underset{˙}{\leq} W)) \land ((R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land S \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land R \neq S) \land ((t \in A \land \neg t \underset{˙}{\leq} W) \land \neg t \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \land ((u \in A \land \neg u \underset{˙}{\leq} W) \land \neg u \underset{˙}{\leq} (P \underset{˙}{\lor} Q)))) \to (u \in A \land \neg u \underset{˙}{\leq} W)$
29	1 2 3 4 5 6 9 10 12	cdleme39a	$⊢ (((K \in HL \land W \in H) \land P \in A \land Q \in A) \land (S \in A \land \neg S \underset{˙}{\leq} W) \land (S \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land (u \in A \land \neg u \underset{˙}{\leq} W))) \to Z = (S \underset{˙}{\lor} ((u \underset{˙}{\lor} Y) \underset{˙}{\land} W)) \underset{˙}{\land} (Y \underset{˙}{\lor} ((u \underset{˙}{\lor} S) \underset{˙}{\land} W))$
30	16 17 18 25 26 27 28 29	syl322anc	$⊢ (((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 (P \neq Q \land (R \in A \land \neg R \underset{˙}{\leq} W) \land (S \in A \land \neg S \underset{˙}{\leq} W)) \land ((R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land S \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land R \neq S) \land ((t \in A \land \neg t \underset{˙}{\leq} W) \land \neg t \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \land ((u \in A \land \neg u \underset{˙}{\leq} W) \land \neg u \underset{˙}{\leq} (P \underset{˙}{\lor} Q)))) \to Z = (S \underset{˙}{\lor} ((u \underset{˙}{\lor} Y) \underset{˙}{\land} W)) \underset{˙}{\land} (Y \underset{˙}{\lor} ((u \underset{˙}{\lor} S) \underset{˙}{\land} W))$
31	15 24 30	3netr4d	$⊢ (((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 (P \neq Q \land (R \in A \land \neg R \underset{˙}{\leq} W) \land (S \in A \land \neg S \underset{˙}{\leq} W)) \land ((R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land S \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land R \neq S) \land ((t \in A \land \neg t \underset{˙}{\leq} W) \land \neg t \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \land ((u \in A \land \neg u \underset{˙}{\leq} W) \land \neg u \underset{˙}{\leq} (P \underset{˙}{\lor} Q)))) \to G \neq Z$

Metamath Proof Explorer

Theorem cdleme39n

Proof