cdleme36m

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. (Contributed by NM, 11-Mar-2013)

	Ref	Expression
Hypotheses	cdleme36.b	$⊢ B = {Base}_{K}$
	cdleme36.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
	cdleme36.j	$⊢ \underset{˙}{\lor} = join (K)$
	cdleme36.m	$⊢ \underset{˙}{\land} = meet (K)$
	cdleme36.a	$⊢ A = Atoms (K)$
	cdleme36.h	$⊢ H = LHyp (K)$
	cdleme36.u	$⊢ U = (P \underset{˙}{\lor} Q) \underset{˙}{\land} W$
	cdleme36.e	$⊢ E = (t \underset{˙}{\lor} U) \underset{˙}{\land} (Q \underset{˙}{\lor} ((P \underset{˙}{\lor} t) \underset{˙}{\land} W))$
	cdleme36.v	$⊢ V = (t \underset{˙}{\lor} E) \underset{˙}{\land} W$
	cdleme36.f	$⊢ F = (R \underset{˙}{\lor} V) \underset{˙}{\land} (E \underset{˙}{\lor} ((t \underset{˙}{\lor} R) \underset{˙}{\land} W))$
	cdleme36.c	$⊢ C = (S \underset{˙}{\lor} V) \underset{˙}{\land} (E \underset{˙}{\lor} ((t \underset{˙}{\lor} S) \underset{˙}{\land} W))$
Assertion	cdleme36m	$⊢ (((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 F = C) \land ((t \in A \land \neg t \underset{˙}{\leq} W) \land \neg t \underset{˙}{\leq} (P \underset{˙}{\lor} Q)))) \to R = S$

Proof

Step	Hyp	Ref	Expression
1		cdleme36.b	$⊢ B = {Base}_{K}$
2		cdleme36.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
3		cdleme36.j	$⊢ \underset{˙}{\lor} = join (K)$
4		cdleme36.m	$⊢ \underset{˙}{\land} = meet (K)$
5		cdleme36.a	$⊢ A = Atoms (K)$
6		cdleme36.h	$⊢ H = LHyp (K)$
7		cdleme36.u	$⊢ U = (P \underset{˙}{\lor} Q) \underset{˙}{\land} W$
8		cdleme36.e	$⊢ E = (t \underset{˙}{\lor} U) \underset{˙}{\land} (Q \underset{˙}{\lor} ((P \underset{˙}{\lor} t) \underset{˙}{\land} W))$
9		cdleme36.v	$⊢ V = (t \underset{˙}{\lor} E) \underset{˙}{\land} W$
10		cdleme36.f	$⊢ F = (R \underset{˙}{\lor} V) \underset{˙}{\land} (E \underset{˙}{\lor} ((t \underset{˙}{\lor} R) \underset{˙}{\land} W))$
11		cdleme36.c	$⊢ C = (S \underset{˙}{\lor} V) \underset{˙}{\land} (E \underset{˙}{\lor} ((t \underset{˙}{\lor} S) \underset{˙}{\land} W))$
12		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 F = C) \land ((t \in A \land \neg t \underset{˙}{\leq} W) \land \neg t \underset{˙}{\leq} (P \underset{˙}{\lor} Q)))) \to (K \in HL \land W \in H)$
13		simp3rl	$⊢ (((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 F = C) \land ((t \in A \land \neg t \underset{˙}{\leq} W) \land \neg t \underset{˙}{\leq} (P \underset{˙}{\lor} Q)))) \to (t \in A \land \neg t \underset{˙}{\leq} W)$
14		simp12	$⊢ (((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 F = C) \land ((t \in A \land \neg t \underset{˙}{\leq} W) \land \neg t \underset{˙}{\leq} (P \underset{˙}{\lor} Q)))) \to (P \in A \land \neg P \underset{˙}{\leq} W)$
15		simp13	$⊢ (((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 F = C) \land ((t \in A \land \neg t \underset{˙}{\leq} W) \land \neg t \underset{˙}{\leq} (P \underset{˙}{\lor} Q)))) \to (Q \in A \land \neg Q \underset{˙}{\leq} W)$
16		simp21	$⊢ (((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 F = C) \land ((t \in A \land \neg t \underset{˙}{\leq} W) \land \neg t \underset{˙}{\leq} (P \underset{˙}{\lor} Q)))) \to P \neq Q$
17		simp3rr	$⊢ (((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 F = C) \land ((t \in A \land \neg t \underset{˙}{\leq} W) \land \neg t \underset{˙}{\leq} (P \underset{˙}{\lor} Q)))) \to \neg t \underset{˙}{\leq} (P \underset{˙}{\lor} Q)$
18	2 3 4 5 6 7 8	cdleme3fa	$⊢ ((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 \land \neg t \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \to E \in A$
19	12 14 15 13 16 17 18	syl132anc	$⊢ (((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 F = C) \land ((t \in A \land \neg t \underset{˙}{\leq} W) \land \neg t \underset{˙}{\leq} (P \underset{˙}{\lor} Q)))) \to E \in A$
20	2 3 4 5 6 7 8	cdleme3	$⊢ ((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 \land \neg t \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \to \neg E \underset{˙}{\leq} W$
21	12 14 15 13 16 17 20	syl132anc	$⊢ (((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 F = C) \land ((t \in A \land \neg t \underset{˙}{\leq} W) \land \neg t \underset{˙}{\leq} (P \underset{˙}{\lor} Q)))) \to \neg E \underset{˙}{\leq} W$
22	19 21	jca	$⊢ (((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 F = C) \land ((t \in A \land \neg t \underset{˙}{\leq} W) \land \neg t \underset{˙}{\leq} (P \underset{˙}{\lor} Q)))) \to (E \in A \land \neg E \underset{˙}{\leq} W)$
23		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 F = C) \land ((t \in A \land \neg t \underset{˙}{\leq} W) \land \neg t \underset{˙}{\leq} (P \underset{˙}{\lor} Q)))) \to Q \in A$
24	23 16	jca	$⊢ (((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 F = C) \land ((t \in A \land \neg t \underset{˙}{\leq} W) \land \neg t \underset{˙}{\leq} (P \underset{˙}{\lor} Q)))) \to (Q \in A \land P \neq Q)$
25	2 3 4 5 6 7 8	cdleme3b	$⊢ ((K \in HL \land W \in H) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land P \neq Q) \land (t \in A \land \neg t \underset{˙}{\leq} W))) \to E \neq t$
26	12 14 24 13 25	syl13anc	$⊢ (((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 F = C) \land ((t \in A \land \neg t \underset{˙}{\leq} W) \land \neg t \underset{˙}{\leq} (P \underset{˙}{\lor} Q)))) \to E \neq t$
27	26	necomd	$⊢ (((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 F = C) \land ((t \in A \land \neg t \underset{˙}{\leq} W) \land \neg t \underset{˙}{\leq} (P \underset{˙}{\lor} Q)))) \to t \neq E$
28		simp22	$⊢ (((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 F = C) \land ((t \in A \land \neg t \underset{˙}{\leq} W) \land \neg t \underset{˙}{\leq} (P \underset{˙}{\lor} Q)))) \to (R \in A \land \neg R \underset{˙}{\leq} W)$
29		simp23	$⊢ (((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 F = C) \land ((t \in A \land \neg t \underset{˙}{\leq} W) \land \neg t \underset{˙}{\leq} (P \underset{˙}{\lor} Q)))) \to (S \in A \land \neg S \underset{˙}{\leq} W)$
30		simp3l1	$⊢ (((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 F = C) \land ((t \in A \land \neg t \underset{˙}{\leq} W) \land \neg t \underset{˙}{\leq} (P \underset{˙}{\lor} Q)))) \to R \underset{˙}{\leq} (P \underset{˙}{\lor} Q)$
31		simp3r	$⊢ (((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 F = C) \land ((t \in A \land \neg t \underset{˙}{\leq} W) \land \neg t \underset{˙}{\leq} (P \underset{˙}{\lor} Q)))) \to ((t \in A \land \neg t \underset{˙}{\leq} W) \land \neg t \underset{˙}{\leq} (P \underset{˙}{\lor} Q))$
32	1 2 3 4 5 6 7 8	cdleme36a	$⊢ (((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land Q \in A) \land (P \neq Q \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) \land \neg t \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \to \neg R \underset{˙}{\leq} (t \underset{˙}{\lor} E)$
33	12 14 23 16 28 30 31 32	syl331anc	$⊢ (((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 F = C) \land ((t \in A \land \neg t \underset{˙}{\leq} W) \land \neg t \underset{˙}{\leq} (P \underset{˙}{\lor} Q)))) \to \neg R \underset{˙}{\leq} (t \underset{˙}{\lor} E)$
34		simp3l2	$⊢ (((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 F = C) \land ((t \in A \land \neg t \underset{˙}{\leq} W) \land \neg t \underset{˙}{\leq} (P \underset{˙}{\lor} Q)))) \to S \underset{˙}{\leq} (P \underset{˙}{\lor} Q)$
35	1 2 3 4 5 6 7 8	cdleme36a	$⊢ (((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land Q \in A) \land (P \neq Q \land (S \in A \land \neg S \underset{˙}{\leq} W) \land S \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \land ((t \in A \land \neg t \underset{˙}{\leq} W) \land \neg t \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \to \neg S \underset{˙}{\leq} (t \underset{˙}{\lor} E)$
36	12 14 23 16 29 34 31 35	syl331anc	$⊢ (((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 F = C) \land ((t \in A \land \neg t \underset{˙}{\leq} W) \land \neg t \underset{˙}{\leq} (P \underset{˙}{\lor} Q)))) \to \neg S \underset{˙}{\leq} (t \underset{˙}{\lor} E)$
37		simp3l3	$⊢ (((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 F = C) \land ((t \in A \land \neg t \underset{˙}{\leq} W) \land \neg t \underset{˙}{\leq} (P \underset{˙}{\lor} Q)))) \to F = C$
38	2 3 4 5 6 9 10 11	cdleme35h	$⊢ (((K \in HL \land W \in H) \land (t \in A \land \neg t \underset{˙}{\leq} W) \land (E \in A \land \neg E \underset{˙}{\leq} W)) \land (t \neq E \land (R \in A \land \neg R \underset{˙}{\leq} W) \land (S \in A \land \neg S \underset{˙}{\leq} W)) \land (\neg R \underset{˙}{\leq} (t \underset{˙}{\lor} E) \land \neg S \underset{˙}{\leq} (t \underset{˙}{\lor} E) \land F = C)) \to R = S$
39	12 13 22 27 28 29 33 36 37 38	syl333anc	$⊢ (((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 F = C) \land ((t \in A \land \neg t \underset{˙}{\leq} W) \land \neg t \underset{˙}{\leq} (P \underset{˙}{\lor} Q)))) \to R = S$

Metamath Proof Explorer

Theorem cdleme36m

Proof