Metamath Proof Explorer

Theorem cdleme21a

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	cdleme21a	$⊢ ((K \in HL \land P \in A \land Q \in A) \land (S \in A \land \neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \land (z \in A \land P \underset{˙}{\lor} z = S \underset{˙}{\lor} z)) \to S \neq z$

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		simp11	$⊢ ((K \in HL \land P \in A \land Q \in A) \land (S \in A \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$
5		hlcvl	$⊢ K \in HL \to K \in CvLat$
6	4 5	syl	$⊢ ((K \in HL \land P \in A \land Q \in A) \land (S \in A \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$
7		simp12	$⊢ ((K \in HL \land P \in A \land Q \in A) \land (S \in A \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$
8		simp2l	$⊢ ((K \in HL \land P \in A \land Q \in A) \land (S \in A \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$
9		simp3l	$⊢ ((K \in HL \land P \in A \land Q \in A) \land (S \in A \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$
10		simp13	$⊢ ((K \in HL \land P \in A \land Q \in A) \land (S \in A \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$
11		simp2r	$⊢ ((K \in HL \land P \in A \land Q \in A) \land (S \in A \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)$
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	4 8 7 10 11 13	syl131anc	$⊢ ((K \in HL \land P \in A \land Q \in A) \land (S \in A \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 \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	cvlsupr6	$⊢ (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 S$
17	16	necomd	$⊢ (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 S \neq z$
18	6 7 8 9 14 15 17	syl132anc	$⊢ ((K \in HL \land P \in A \land Q \in A) \land (S \in A \land \neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \land (z \in A \land P \underset{˙}{\lor} z = S \underset{˙}{\lor} z)) \to S \neq z$