cdleme21b

Description: Part of proof of Lemma E in Crawley p. 115. (Contributed by NM, 28-Nov-2012)

	Ref	Expression
Hypotheses	cdleme21a.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
	cdleme21a.j	$⊢ \underset{˙}{\lor} = join (K)$
	cdleme21a.a	$⊢ A = Atoms (K)$
Assertion	cdleme21b	$⊢ ((K \in HL \land P \in A \land Q \in A) \land (S \in A \land P \neq Q \land \neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \land (z \in A \land P \underset{˙}{\lor} z = S \underset{˙}{\lor} z)) \to \neg z \underset{˙}{\leq} (P \underset{˙}{\lor} Q)$

Proof

Step	Hyp	Ref	Expression
1		cdleme21a.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
2		cdleme21a.j	$⊢ \underset{˙}{\lor} = join (K)$
3		cdleme21a.a	$⊢ A = Atoms (K)$
4		simp23	$⊢ ((K \in HL \land P \in A \land Q \in A) \land (S \in A \land P \neq Q \land \neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \land (z \in A \land P \underset{˙}{\lor} z = S \underset{˙}{\lor} z)) \to \neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q)$
5		simp11	$⊢ ((K \in HL \land P \in A \land Q \in A) \land (S \in A \land P \neq Q \land \neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \land (z \in A \land P \underset{˙}{\lor} z = S \underset{˙}{\lor} z)) \to K \in HL$
6		hlcvl	$⊢ K \in HL \to K \in CvLat$
7	5 6	syl	$⊢ ((K \in HL \land P \in A \land Q \in A) \land (S \in A \land P \neq Q \land \neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \land (z \in A \land P \underset{˙}{\lor} z = S \underset{˙}{\lor} z)) \to K \in CvLat$
8		simp3l	$⊢ ((K \in HL \land P \in A \land Q \in A) \land (S \in A \land P \neq Q \land \neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \land (z \in A \land P \underset{˙}{\lor} z = S \underset{˙}{\lor} z)) \to z \in A$
9		simp13	$⊢ ((K \in HL \land P \in A \land Q \in A) \land (S \in A \land P \neq Q \land \neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \land (z \in A \land P \underset{˙}{\lor} z = S \underset{˙}{\lor} z)) \to Q \in A$
10		simp12	$⊢ ((K \in HL \land P \in A \land Q \in A) \land (S \in A \land P \neq Q \land \neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \land (z \in A \land P \underset{˙}{\lor} z = S \underset{˙}{\lor} z)) \to P \in A$
11		simp21	$⊢ ((K \in HL \land P \in A \land Q \in A) \land (S \in A \land P \neq Q \land \neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \land (z \in A \land P \underset{˙}{\lor} z = S \underset{˙}{\lor} z)) \to S \in A$
12	1 2 3	atnlej1	$⊢ (K \in HL \land (S \in A \land P \in A \land Q \in A) \land \neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \to S \neq P$
13	12	necomd	$⊢ (K \in HL \land (S \in A \land P \in A \land Q \in A) \land \neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \to P \neq S$
14	5 11 10 9 4 13	syl131anc	$⊢ ((K \in HL \land P \in A \land Q \in A) \land (S \in A \land P \neq Q \land \neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \land (z \in A \land P \underset{˙}{\lor} z = S \underset{˙}{\lor} z)) \to P \neq S$
15		simp3r	$⊢ ((K \in HL \land P \in A \land Q \in A) \land (S \in A \land P \neq Q \land \neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \land (z \in A \land P \underset{˙}{\lor} z = S \underset{˙}{\lor} z)) \to P \underset{˙}{\lor} z = S \underset{˙}{\lor} z$
16	3 2	cvlsupr5	$⊢ (K \in CvLat \land (P \in A \land S \in A \land z \in A) \land (P \neq S \land P \underset{˙}{\lor} z = S \underset{˙}{\lor} z)) \to z \neq P$
17	7 10 11 8 14 15 16	syl132anc	$⊢ ((K \in HL \land P \in A \land Q \in A) \land (S \in A \land P \neq Q \land \neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \land (z \in A \land P \underset{˙}{\lor} z = S \underset{˙}{\lor} z)) \to z \neq P$
18	1 2 3	cvlatexch1	$⊢ (K \in CvLat \land (z \in A \land Q \in A \land P \in A) \land z \neq P) \to (z \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \to Q \underset{˙}{\leq} (P \underset{˙}{\lor} z))$
19	7 8 9 10 17 18	syl131anc	$⊢ ((K \in HL \land P \in A \land Q \in A) \land (S \in A \land P \neq Q \land \neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \land (z \in A \land P \underset{˙}{\lor} z = S \underset{˙}{\lor} z)) \to (z \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \to Q \underset{˙}{\leq} (P \underset{˙}{\lor} z))$
20	3 2	cvlsupr8	$⊢ (K \in CvLat \land (P \in A \land S \in A \land z \in A) \land (P \neq S \land P \underset{˙}{\lor} z = S \underset{˙}{\lor} z)) \to P \underset{˙}{\lor} S = P \underset{˙}{\lor} z$
21	7 10 11 8 14 15 20	syl132anc	$⊢ ((K \in HL \land P \in A \land Q \in A) \land (S \in A \land P \neq Q \land \neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \land (z \in A \land P \underset{˙}{\lor} z = S \underset{˙}{\lor} z)) \to P \underset{˙}{\lor} S = P \underset{˙}{\lor} z$
22	21	breq2d	$⊢ ((K \in HL \land P \in A \land Q \in A) \land (S \in A \land P \neq Q \land \neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \land (z \in A \land P \underset{˙}{\lor} z = S \underset{˙}{\lor} z)) \to (Q \underset{˙}{\leq} (P \underset{˙}{\lor} S) \leftrightarrow Q \underset{˙}{\leq} (P \underset{˙}{\lor} z))$
23	19 22	sylibrd	$⊢ ((K \in HL \land P \in A \land Q \in A) \land (S \in A \land P \neq Q \land \neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \land (z \in A \land P \underset{˙}{\lor} z = S \underset{˙}{\lor} z)) \to (z \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \to Q \underset{˙}{\leq} (P \underset{˙}{\lor} S))$
24		simp22	$⊢ ((K \in HL \land P \in A \land Q \in A) \land (S \in A \land P \neq Q \land \neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \land (z \in A \land P \underset{˙}{\lor} z = S \underset{˙}{\lor} z)) \to P \neq Q$
25	24	necomd	$⊢ ((K \in HL \land P \in A \land Q \in A) \land (S \in A \land P \neq Q \land \neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \land (z \in A \land P \underset{˙}{\lor} z = S \underset{˙}{\lor} z)) \to Q \neq P$
26	1 2 3	cvlatexch1	$⊢ (K \in CvLat \land (Q \in A \land S \in A \land P \in A) \land Q \neq P) \to (Q \underset{˙}{\leq} (P \underset{˙}{\lor} S) \to S \underset{˙}{\leq} (P \underset{˙}{\lor} Q))$
27	7 9 11 10 25 26	syl131anc	$⊢ ((K \in HL \land P \in A \land Q \in A) \land (S \in A \land P \neq Q \land \neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \land (z \in A \land P \underset{˙}{\lor} z = S \underset{˙}{\lor} z)) \to (Q \underset{˙}{\leq} (P \underset{˙}{\lor} S) \to S \underset{˙}{\leq} (P \underset{˙}{\lor} Q))$
28	23 27	syld	$⊢ ((K \in HL \land P \in A \land Q \in A) \land (S \in A \land P \neq Q \land \neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \land (z \in A \land P \underset{˙}{\lor} z = S \underset{˙}{\lor} z)) \to (z \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \to S \underset{˙}{\leq} (P \underset{˙}{\lor} Q))$
29	4 28	mtod	$⊢ ((K \in HL \land P \in A \land Q \in A) \land (S \in A \land P \neq Q \land \neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \land (z \in A \land P \underset{˙}{\lor} z = S \underset{˙}{\lor} z)) \to \neg z \underset{˙}{\leq} (P \underset{˙}{\lor} Q)$

Metamath Proof Explorer

Theorem cdleme21b

Proof