cdlemd3

Description: Part of proof of Lemma D in Crawley p. 113. The R =/= P requirement is not mentioned in their proof. (Contributed by NM, 29-May-2012)

	Ref	Expression
Hypotheses	cdlemd3.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
	cdlemd3.j	$⊢ \underset{˙}{\lor} = join (K)$
	cdlemd3.a	$⊢ A = Atoms (K)$
	cdlemd3.h	$⊢ H = LHyp (K)$
Assertion	cdlemd3	$⊢ ((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 \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land R \neq P)) \land (R \in A \land S \in A \land \neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \to \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} S)$

Proof

Step	Hyp	Ref	Expression
1		cdlemd3.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
2		cdlemd3.j	$⊢ \underset{˙}{\lor} = join (K)$
3		cdlemd3.a	$⊢ A = Atoms (K)$
4		cdlemd3.h	$⊢ H = LHyp (K)$
5		simp33	$⊢ ((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 \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land R \neq P)) \land (R \in A \land S \in A \land \neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \to \neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q)$
6		simp1l	$⊢ ((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 \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land R \neq P)) \land (R \in A \land S \in A \land \neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \to K \in HL$
7		simp31	$⊢ ((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 \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land R \neq P)) \land (R \in A \land S \in A \land \neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \to R \in A$
8		simp32	$⊢ ((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 \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land R \neq P)) \land (R \in A \land S \in A \land \neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \to S \in A$
9		simp21l	$⊢ ((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 \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land R \neq P)) \land (R \in A \land S \in A \land \neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \to P \in A$
10		simp233	$⊢ ((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 \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land R \neq P)) \land (R \in A \land S \in A \land \neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \to R \neq P$
11	1 2 3	hlatexch1	$⊢ (K \in HL \land (R \in A \land S \in A \land P \in A) \land R \neq P) \to (R \underset{˙}{\leq} (P \underset{˙}{\lor} S) \to S \underset{˙}{\leq} (P \underset{˙}{\lor} R))$
12	6 7 8 9 10 11	syl131anc	$⊢ ((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 \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land R \neq P)) \land (R \in A \land S \in A \land \neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \to (R \underset{˙}{\leq} (P \underset{˙}{\lor} S) \to S \underset{˙}{\leq} (P \underset{˙}{\lor} R))$
13		simp22l	$⊢ ((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 \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land R \neq P)) \land (R \in A \land S \in A \land \neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \to Q \in A$
14	1 2 3	hlatlej1	$⊢ (K \in HL \land P \in A \land Q \in A) \to P \underset{˙}{\leq} (P \underset{˙}{\lor} Q)$
15	6 9 13 14	syl3anc	$⊢ ((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 \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land R \neq P)) \land (R \in A \land S \in A \land \neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \to P \underset{˙}{\leq} (P \underset{˙}{\lor} Q)$
16		simp232	$⊢ ((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 \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land R \neq P)) \land (R \in A \land S \in A \land \neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \to R \underset{˙}{\leq} (P \underset{˙}{\lor} Q)$
17	6	hllatd	$⊢ ((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 \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land R \neq P)) \land (R \in A \land S \in A \land \neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \to K \in Lat$
18		eqid	$⊢ {Base}_{K} = {Base}_{K}$
19	18 3	atbase	$⊢ P \in A \to P \in {Base}_{K}$
20	9 19	syl	$⊢ ((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 \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land R \neq P)) \land (R \in A \land S \in A \land \neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \to P \in {Base}_{K}$
21	18 3	atbase	$⊢ R \in A \to R \in {Base}_{K}$
22	7 21	syl	$⊢ ((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 \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land R \neq P)) \land (R \in A \land S \in A \land \neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \to R \in {Base}_{K}$
23	18 3	atbase	$⊢ Q \in A \to Q \in {Base}_{K}$
24	13 23	syl	$⊢ ((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 \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land R \neq P)) \land (R \in A \land S \in A \land \neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \to Q \in {Base}_{K}$
25	18 2	latjcl	$⊢ (K \in Lat \land P \in {Base}_{K} \land Q \in {Base}_{K}) \to P \underset{˙}{\lor} Q \in {Base}_{K}$
26	17 20 24 25	syl3anc	$⊢ ((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 \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land R \neq P)) \land (R \in A \land S \in A \land \neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \to P \underset{˙}{\lor} Q \in {Base}_{K}$
27	18 1 2	latjle12	$⊢ (K \in Lat \land (P \in {Base}_{K} \land R \in {Base}_{K} \land P \underset{˙}{\lor} Q \in {Base}_{K})) \to ((P \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land R \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \leftrightarrow (P \underset{˙}{\lor} R) \underset{˙}{\leq} (P \underset{˙}{\lor} Q))$
28	17 20 22 26 27	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 \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land R \neq P)) \land (R \in A \land S \in A \land \neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \to ((P \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land R \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \leftrightarrow (P \underset{˙}{\lor} R) \underset{˙}{\leq} (P \underset{˙}{\lor} Q))$
29	15 16 28	mpbi2and	$⊢ ((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 \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land R \neq P)) \land (R \in A \land S \in A \land \neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \to (P \underset{˙}{\lor} R) \underset{˙}{\leq} (P \underset{˙}{\lor} Q)$
30	18 3	atbase	$⊢ S \in A \to S \in {Base}_{K}$
31	8 30	syl	$⊢ ((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 \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land R \neq P)) \land (R \in A \land S \in A \land \neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \to S \in {Base}_{K}$
32	18 2	latjcl	$⊢ (K \in Lat \land P \in {Base}_{K} \land R \in {Base}_{K}) \to P \underset{˙}{\lor} R \in {Base}_{K}$
33	17 20 22 32	syl3anc	$⊢ ((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 \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land R \neq P)) \land (R \in A \land S \in A \land \neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \to P \underset{˙}{\lor} R \in {Base}_{K}$
34	18 1	lattr	$⊢ (K \in Lat \land (S \in {Base}_{K} \land P \underset{˙}{\lor} R \in {Base}_{K} \land P \underset{˙}{\lor} Q \in {Base}_{K})) \to ((S \underset{˙}{\leq} (P \underset{˙}{\lor} R) \land (P \underset{˙}{\lor} R) \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \to S \underset{˙}{\leq} (P \underset{˙}{\lor} Q))$
35	17 31 33 26 34	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 \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land R \neq P)) \land (R \in A \land S \in A \land \neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \to ((S \underset{˙}{\leq} (P \underset{˙}{\lor} R) \land (P \underset{˙}{\lor} R) \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \to S \underset{˙}{\leq} (P \underset{˙}{\lor} Q))$
36	29 35	mpan2d	$⊢ ((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 \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land R \neq P)) \land (R \in A \land S \in A \land \neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \to (S \underset{˙}{\leq} (P \underset{˙}{\lor} R) \to S \underset{˙}{\leq} (P \underset{˙}{\lor} Q))$
37	12 36	syld	$⊢ ((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 \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land R \neq P)) \land (R \in A \land S \in A \land \neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \to (R \underset{˙}{\leq} (P \underset{˙}{\lor} S) \to S \underset{˙}{\leq} (P \underset{˙}{\lor} Q))$
38	5 37	mtod	$⊢ ((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 \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land R \neq P)) \land (R \in A \land S \in A \land \neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \to \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} S)$

Metamath Proof Explorer

Theorem cdlemd3

Proof