cdlemb3

Description: Given two atoms not under the fiducial co-atom W , there is a third. Lemma B in Crawley p. 112. TODO: Is there a simpler more direct proof, that could be placed earlier e.g. near lhpexle ? Then replace cdlemb2 with it. This is a more general version of cdlemb2 without P =/= Q condition. (Contributed by NM, 27-Apr-2013)

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

Proof

Step	Hyp	Ref	Expression
1		cdlemg5.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
2		cdlemg5.j	$⊢ \underset{˙}{\lor} = join (K)$
3		cdlemg5.a	$⊢ A = Atoms (K)$
4		cdlemg5.h	$⊢ H = LHyp (K)$
5		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 = Q) \to (K \in HL \land W \in H)$
6		simpl2	$⊢ (((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 = Q) \to (P \in A \land \neg P \underset{˙}{\leq} W)$
7	1 2 3 4	cdlemg5	$⊢ ((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W)) \to \exists r \in A (P \neq r \land \neg r \underset{˙}{\leq} W)$
8	5 6 7	syl2anc	$⊢ (((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 = Q) \to \exists r \in A (P \neq r \land \neg r \underset{˙}{\leq} W)$
9		ancom	$⊢ (P \neq r \land \neg r \underset{˙}{\leq} W) \leftrightarrow (\neg r \underset{˙}{\leq} W \land P \neq r)$
10		eqcom	$⊢ P = r \leftrightarrow r = P$
11		simp2	$⊢ (((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 = Q \land r \in A) \to P = Q$
12	11	oveq2d	$⊢ (((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 = Q \land r \in A) \to P \underset{˙}{\lor} P = P \underset{˙}{\lor} Q$
13		simp11l	$⊢ (((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 = Q \land r \in A) \to K \in HL$
14		simp12l	$⊢ (((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 = Q \land r \in A) \to P \in A$
15	2 3	hlatjidm	$⊢ (K \in HL \land P \in A) \to P \underset{˙}{\lor} P = P$
16	13 14 15	syl2anc	$⊢ (((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 = Q \land r \in A) \to P \underset{˙}{\lor} P = P$
17	12 16	eqtr3d	$⊢ (((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 = Q \land r \in A) \to P \underset{˙}{\lor} Q = P$
18	17	breq2d	$⊢ (((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 = Q \land r \in A) \to (r \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \leftrightarrow r \underset{˙}{\leq} P)$
19		hlatl	$⊢ K \in HL \to K \in AtLat$
20	13 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 = Q \land r \in A) \to K \in AtLat$
21		simp3	$⊢ (((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 = Q \land r \in A) \to r \in A$
22	1 3	atcmp	$⊢ (K \in AtLat \land r \in A \land P \in A) \to (r \underset{˙}{\leq} P \leftrightarrow r = P)$
23	20 21 14 22	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 = Q \land r \in A) \to (r \underset{˙}{\leq} P \leftrightarrow r = P)$
24	18 23	bitr2d	$⊢ (((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 = Q \land r \in A) \to (r = P \leftrightarrow r \underset{˙}{\leq} (P \underset{˙}{\lor} Q))$
25	10 24	syl5bb	$⊢ (((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 = Q \land r \in A) \to (P = r \leftrightarrow r \underset{˙}{\leq} (P \underset{˙}{\lor} Q))$
26	25	necon3abid	$⊢ (((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 = Q \land r \in A) \to (P \neq r \leftrightarrow \neg r \underset{˙}{\leq} (P \underset{˙}{\lor} Q))$
27	26	anbi2d	$⊢ (((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 = Q \land r \in A) \to ((\neg r \underset{˙}{\leq} W \land P \neq r) \leftrightarrow (\neg r \underset{˙}{\leq} W \land \neg r \underset{˙}{\leq} (P \underset{˙}{\lor} Q)))$
28	9 27	syl5bb	$⊢ (((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 = Q \land r \in A) \to ((P \neq r \land \neg r \underset{˙}{\leq} W) \leftrightarrow (\neg r \underset{˙}{\leq} W \land \neg r \underset{˙}{\leq} (P \underset{˙}{\lor} Q)))$
29	28	3expa	$⊢ ((((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 = Q) \land r \in A) \to ((P \neq r \land \neg r \underset{˙}{\leq} W) \leftrightarrow (\neg r \underset{˙}{\leq} W \land \neg r \underset{˙}{\leq} (P \underset{˙}{\lor} Q)))$
30	29	rexbidva	$⊢ (((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 = Q) \to (\exists r \in A (P \neq r \land \neg r \underset{˙}{\leq} W) \leftrightarrow \exists r \in A (\neg r \underset{˙}{\leq} W \land \neg r \underset{˙}{\leq} (P \underset{˙}{\lor} Q)))$
31	8 30	mpbid	$⊢ (((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 = Q) \to \exists r \in A (\neg r \underset{˙}{\leq} W \land \neg r \underset{˙}{\leq} (P \underset{˙}{\lor} Q))$
32		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) \to (K \in HL \land W \in H)$
33		simpl2	$⊢ (((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) \to (P \in A \land \neg P \underset{˙}{\leq} W)$
34		simpl3	$⊢ (((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) \to (Q \in A \land \neg Q \underset{˙}{\leq} W)$
35		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) \to P \neq Q$
36	1 2 3 4	cdlemb2	$⊢ ((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) \to \exists r \in A (\neg r \underset{˙}{\leq} W \land \neg r \underset{˙}{\leq} (P \underset{˙}{\lor} Q))$
37	32 33 34 35 36	syl121anc	$⊢ (((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) \to \exists r \in A (\neg r \underset{˙}{\leq} W \land \neg r \underset{˙}{\leq} (P \underset{˙}{\lor} Q))$
38	31 37	pm2.61dane	$⊢ ((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)) \to \exists r \in A (\neg r \underset{˙}{\leq} W \land \neg r \underset{˙}{\leq} (P \underset{˙}{\lor} Q))$

Metamath Proof Explorer

Theorem cdlemb3

Proof