cdleme38n

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. TODO shorter if proved directly from cdleme36m and cdleme37m ? (Contributed by NM, 14-Mar-2013)

	Ref	Expression
Hypotheses	cdleme38.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
	cdleme38.j	$⊢ \underset{˙}{\lor} = join (K)$
	cdleme38.m	$⊢ \underset{˙}{\land} = meet (K)$
	cdleme38.a	$⊢ A = Atoms (K)$
	cdleme38.h	$⊢ H = LHyp (K)$
	cdleme38.u	$⊢ U = (P \underset{˙}{\lor} Q) \underset{˙}{\land} W$
	cdleme38.e	$⊢ E = (t \underset{˙}{\lor} U) \underset{˙}{\land} (Q \underset{˙}{\lor} ((P \underset{˙}{\lor} t) \underset{˙}{\land} W))$
	cdleme38.d	$⊢ D = (u \underset{˙}{\lor} U) \underset{˙}{\land} (Q \underset{˙}{\lor} ((P \underset{˙}{\lor} u) \underset{˙}{\land} W))$
	cdleme38.v	$⊢ V = (t \underset{˙}{\lor} E) \underset{˙}{\land} W$
	cdleme38.x	$⊢ X = (u \underset{˙}{\lor} D) \underset{˙}{\land} W$
	cdleme38.f	$⊢ F = (R \underset{˙}{\lor} V) \underset{˙}{\land} (E \underset{˙}{\lor} ((t \underset{˙}{\lor} R) \underset{˙}{\land} W))$
	cdleme38.g	$⊢ G = (S \underset{˙}{\lor} X) \underset{˙}{\land} (D \underset{˙}{\lor} ((u \underset{˙}{\lor} S) \underset{˙}{\land} W))$
Assertion	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 F \neq G$

Proof

Step	Hyp	Ref	Expression
1		cdleme38.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
2		cdleme38.j	$⊢ \underset{˙}{\lor} = join (K)$
3		cdleme38.m	$⊢ \underset{˙}{\land} = meet (K)$
4		cdleme38.a	$⊢ A = Atoms (K)$
5		cdleme38.h	$⊢ H = LHyp (K)$
6		cdleme38.u	$⊢ U = (P \underset{˙}{\lor} Q) \underset{˙}{\land} W$
7		cdleme38.e	$⊢ E = (t \underset{˙}{\lor} U) \underset{˙}{\land} (Q \underset{˙}{\lor} ((P \underset{˙}{\lor} t) \underset{˙}{\land} W))$
8		cdleme38.d	$⊢ D = (u \underset{˙}{\lor} U) \underset{˙}{\land} (Q \underset{˙}{\lor} ((P \underset{˙}{\lor} u) \underset{˙}{\land} W))$
9		cdleme38.v	$⊢ V = (t \underset{˙}{\lor} E) \underset{˙}{\land} W$
10		cdleme38.x	$⊢ X = (u \underset{˙}{\lor} D) \underset{˙}{\land} W$
11		cdleme38.f	$⊢ F = (R \underset{˙}{\lor} V) \underset{˙}{\land} (E \underset{˙}{\lor} ((t \underset{˙}{\lor} R) \underset{˙}{\land} W))$
12		cdleme38.g	$⊢ G = (S \underset{˙}{\lor} X) \underset{˙}{\land} (D \underset{˙}{\lor} ((u \underset{˙}{\lor} S) \underset{˙}{\land} W))$
13		simp313	$⊢ (((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 \neq S$
14		simpl1	$⊢ ((((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)))) \land F = G) \to ((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))$
15		simpl21	$⊢ ((((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)))) \land F = G) \to P \neq Q$
16		simpl22	$⊢ ((((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)))) \land F = G) \to (R \in A \land \neg R \underset{˙}{\leq} W)$
17		simpl23	$⊢ ((((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)))) \land F = G) \to (S \in A \land \neg S \underset{˙}{\leq} W)$
18		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)$
19	18	adantr	$⊢ ((((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)))) \land F = G) \to R \underset{˙}{\leq} (P \underset{˙}{\lor} Q)$
20		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)$
21	20	adantr	$⊢ ((((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)))) \land F = G) \to S \underset{˙}{\leq} (P \underset{˙}{\lor} Q)$
22		simpr	$⊢ ((((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)))) \land F = G) \to F = G$
23	19 21 22	3jca	$⊢ ((((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)))) \land F = G) \to (R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land S \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land F = G)$
24		simpl32	$⊢ ((((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)))) \land F = G) \to ((t \in A \land \neg t \underset{˙}{\leq} W) \land \neg t \underset{˙}{\leq} (P \underset{˙}{\lor} Q))$
25		simpl33	$⊢ ((((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)))) \land F = G) \to ((u \in A \land \neg u \underset{˙}{\leq} W) \land \neg u \underset{˙}{\leq} (P \underset{˙}{\lor} Q))$
26	1 2 3 4 5 6 7 8 9 10 11 12	cdleme38m	$⊢ (((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 = G) \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 = S$
27	14 15 16 17 23 24 25 26	syl133anc	$⊢ ((((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)))) \land F = G) \to R = S$
28	27	ex	$⊢ (((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 (F = G \to R = S)$
29	28	necon3d	$⊢ (((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 \neq S \to F \neq G)$
30	13 29	mpd	$⊢ (((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 F \neq G$

Metamath Proof Explorer

Theorem cdleme38n

Proof