cdleme39a

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))$
	cdleme39a.v	$⊢ V = (t \underset{˙}{\lor} E) \underset{˙}{\land} W$
Assertion	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} V) \underset{˙}{\land} (E \underset{˙}{\lor} ((t \underset{˙}{\lor} R) \underset{˙}{\land} W))$

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		cdleme39a.v	$⊢ V = (t \underset{˙}{\lor} E) \underset{˙}{\land} W$
10		simp11	$⊢ (((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 (K \in HL \land W \in H)$
11		simp12	$⊢ (((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 P \in A$
12		simp13	$⊢ (((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 Q \in A$
13		simp2	$⊢ (((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 (R \in A \land \neg R \underset{˙}{\leq} W)$
14		simp3l	$⊢ (((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 R \underset{˙}{\leq} (P \underset{˙}{\lor} Q)$
15	1 2 3 4 5 6	cdleme4	$⊢ ((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)) \to P \underset{˙}{\lor} Q = R \underset{˙}{\lor} U$
16	10 11 12 13 14 15	syl131anc	$⊢ (((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 P \underset{˙}{\lor} Q = R \underset{˙}{\lor} U$
17		simp3r	$⊢ (((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 (t \in A \land \neg t \underset{˙}{\leq} W)$
18	1 2 3 4 5 6 7	cdleme2	$⊢ ((K \in HL \land W \in H) \land (P \in A \land Q \in A \land (t \in A \land \neg t \underset{˙}{\leq} W))) \to (t \underset{˙}{\lor} E) \underset{˙}{\land} W = U$
19	10 11 12 17 18	syl13anc	$⊢ (((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 (t \underset{˙}{\lor} E) \underset{˙}{\land} W = U$
20	9 19	syl5eq	$⊢ (((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 V = U$
21	20	oveq2d	$⊢ (((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 R \underset{˙}{\lor} V = R \underset{˙}{\lor} U$
22	16 21	eqtr4d	$⊢ (((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 P \underset{˙}{\lor} Q = R \underset{˙}{\lor} V$
23		simp11l	$⊢ (((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 K \in HL$
24		simp2l	$⊢ (((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 R \in A$
25		simp3rl	$⊢ (((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 t \in A$
26	2 4	hlatjcom	$⊢ (K \in HL \land R \in A \land t \in A) \to R \underset{˙}{\lor} t = t \underset{˙}{\lor} R$
27	23 24 25 26	syl3anc	$⊢ (((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 R \underset{˙}{\lor} t = t \underset{˙}{\lor} R$
28	27	oveq1d	$⊢ (((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 (R \underset{˙}{\lor} t) \underset{˙}{\land} W = (t \underset{˙}{\lor} R) \underset{˙}{\land} W$
29	28	oveq2d	$⊢ (((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 E \underset{˙}{\lor} ((R \underset{˙}{\lor} t) \underset{˙}{\land} W) = E \underset{˙}{\lor} ((t \underset{˙}{\lor} R) \underset{˙}{\land} W)$
30	22 29	oveq12d	$⊢ (((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 (P \underset{˙}{\lor} Q) \underset{˙}{\land} (E \underset{˙}{\lor} ((R \underset{˙}{\lor} t) \underset{˙}{\land} W)) = (R \underset{˙}{\lor} V) \underset{˙}{\land} (E \underset{˙}{\lor} ((t \underset{˙}{\lor} R) \underset{˙}{\land} W))$
31	8 30	syl5eq	$⊢ (((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} V) \underset{˙}{\land} (E \underset{˙}{\lor} ((t \underset{˙}{\lor} R) \underset{˙}{\land} W))$

Metamath Proof Explorer

Theorem cdleme39a

Proof