cdleme3

Description: Part of proof of Lemma E in Crawley p. 113. F represents f(r). W is the fiducial co-atom (hyperplane) w. Here and in cdleme3fa above, we show that f(r) e. W (4th line from bottom on p. 113), meaning it is an atom and not under w, which in our notation is expressed as F e. A /\ -. F .<_ W . Their proof provides no details of our lemmas cdleme3b through cdleme3 , so there may be a simpler proof that we have overlooked. (Contributed by NM, 7-Jun-2012)

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

Proof

Step	Hyp	Ref	Expression
1		cdleme1.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
2		cdleme1.j	$⊢ \underset{˙}{\lor} = join (K)$
3		cdleme1.m	$⊢ \underset{˙}{\land} = meet (K)$
4		cdleme1.a	$⊢ A = Atoms (K)$
5		cdleme1.h	$⊢ H = LHyp (K)$
6		cdleme1.u	$⊢ U = (P \underset{˙}{\lor} Q) \underset{˙}{\land} W$
7		cdleme1.f	$⊢ F = (R \underset{˙}{\lor} U) \underset{˙}{\land} (Q \underset{˙}{\lor} ((P \underset{˙}{\lor} R) \underset{˙}{\land} W))$
8		eqid	$⊢ (P \underset{˙}{\lor} R) \underset{˙}{\land} W = (P \underset{˙}{\lor} R) \underset{˙}{\land} W$
9	1 2 3 4 5 6 7 8	cdleme3g	$⊢ ((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 (R \in A \land \neg R \underset{˙}{\leq} W)) \land (P \neq Q \land \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \to F \neq U$
10		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 (R \in A \land \neg R \underset{˙}{\leq} W)) \land (P \neq Q \land \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \to K \in HL$
11	10	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 (R \in A \land \neg R \underset{˙}{\leq} W)) \land (P \neq Q \land \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \to K \in Lat$
12		simp23l	$⊢ ((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 (R \in A \land \neg R \underset{˙}{\leq} W)) \land (P \neq Q \land \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \to R \in A$
13		eqid	$⊢ {Base}_{K} = {Base}_{K}$
14	13 4	atbase	$⊢ R \in A \to R \in {Base}_{K}$
15	12 14	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 (R \in A \land \neg R \underset{˙}{\leq} W)) \land (P \neq Q \land \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \to R \in {Base}_{K}$
16	1 2 3 4 5 6 7	cdleme3fa	$⊢ ((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 (R \in A \land \neg R \underset{˙}{\leq} W)) \land (P \neq Q \land \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \to F \in A$
17	13 4	atbase	$⊢ F \in A \to F \in {Base}_{K}$
18	16 17	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 (R \in A \land \neg R \underset{˙}{\leq} W)) \land (P \neq Q \land \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \to F \in {Base}_{K}$
19	13 1 2	latlej2	$⊢ (K \in Lat \land R \in {Base}_{K} \land F \in {Base}_{K}) \to F \underset{˙}{\leq} (R \underset{˙}{\lor} F)$
20	11 15 18 19	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 (R \in A \land \neg R \underset{˙}{\leq} W)) \land (P \neq Q \land \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \to F \underset{˙}{\leq} (R \underset{˙}{\lor} F)$
21	20	biantrurd	$⊢ ((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 (R \in A \land \neg R \underset{˙}{\leq} W)) \land (P \neq Q \land \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \to (F \underset{˙}{\leq} W \leftrightarrow (F \underset{˙}{\leq} (R \underset{˙}{\lor} F) \land F \underset{˙}{\leq} W))$
22	13 2 4	hlatjcl	$⊢ (K \in HL \land R \in A \land F \in A) \to R \underset{˙}{\lor} F \in {Base}_{K}$
23	10 12 16 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 (R \in A \land \neg R \underset{˙}{\leq} W)) \land (P \neq Q \land \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \to R \underset{˙}{\lor} F \in {Base}_{K}$
24		simp1r	$⊢ ((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 (R \in A \land \neg R \underset{˙}{\leq} W)) \land (P \neq Q \land \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \to W \in H$
25	13 5	lhpbase	$⊢ W \in H \to W \in {Base}_{K}$
26	24 25	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 (R \in A \land \neg R \underset{˙}{\leq} W)) \land (P \neq Q \land \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \to W \in {Base}_{K}$
27	13 1 3	latlem12	$⊢ (K \in Lat \land (F \in {Base}_{K} \land R \underset{˙}{\lor} F \in {Base}_{K} \land W \in {Base}_{K})) \to ((F \underset{˙}{\leq} (R \underset{˙}{\lor} F) \land F \underset{˙}{\leq} W) \leftrightarrow F \underset{˙}{\leq} ((R \underset{˙}{\lor} F) \underset{˙}{\land} W))$
28	11 18 23 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 (R \in A \land \neg R \underset{˙}{\leq} W)) \land (P \neq Q \land \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \to ((F \underset{˙}{\leq} (R \underset{˙}{\lor} F) \land F \underset{˙}{\leq} W) \leftrightarrow F \underset{˙}{\leq} ((R \underset{˙}{\lor} F) \underset{˙}{\land} W))$
29		simp1	$⊢ ((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 (R \in A \land \neg R \underset{˙}{\leq} W)) \land (P \neq Q \land \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \to (K \in HL \land W \in H)$
30		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 (R \in A \land \neg R \underset{˙}{\leq} W)) \land (P \neq Q \land \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \to P \in A$
31		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 (R \in A \land \neg R \underset{˙}{\leq} W)) \land (P \neq Q \land \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \to Q \in A$
32		simp23	$⊢ ((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 (R \in A \land \neg R \underset{˙}{\leq} W)) \land (P \neq Q \land \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \to (R \in A \land \neg R \underset{˙}{\leq} W)$
33	1 2 3 4 5 6 7	cdleme2	$⊢ ((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))) \to (R \underset{˙}{\lor} F) \underset{˙}{\land} W = U$
34	29 30 31 32 33	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 (R \in A \land \neg R \underset{˙}{\leq} W)) \land (P \neq Q \land \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \to (R \underset{˙}{\lor} F) \underset{˙}{\land} W = U$
35	34	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 (R \in A \land \neg R \underset{˙}{\leq} W)) \land (P \neq Q \land \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \to (F \underset{˙}{\leq} ((R \underset{˙}{\lor} F) \underset{˙}{\land} W) \leftrightarrow F \underset{˙}{\leq} U)$
36	28 35	bitrd	$⊢ ((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 (R \in A \land \neg R \underset{˙}{\leq} W)) \land (P \neq Q \land \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \to ((F \underset{˙}{\leq} (R \underset{˙}{\lor} F) \land F \underset{˙}{\leq} W) \leftrightarrow F \underset{˙}{\leq} U)$
37		hlatl	$⊢ K \in HL \to K \in AtLat$
38	10 37	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 (R \in A \land \neg R \underset{˙}{\leq} W)) \land (P \neq Q \land \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \to K \in AtLat$
39		simp21	$⊢ ((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 (R \in A \land \neg R \underset{˙}{\leq} W)) \land (P \neq Q \land \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \to (P \in A \land \neg P \underset{˙}{\leq} W)$
40		simp3l	$⊢ ((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 (R \in A \land \neg R \underset{˙}{\leq} W)) \land (P \neq Q \land \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \to P \neq Q$
41	1 2 3 4 5 6	lhpat2	$⊢ ((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land P \neq Q)) \to U \in A$
42	29 39 31 40 41	syl112anc	$⊢ ((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 (R \in A \land \neg R \underset{˙}{\leq} W)) \land (P \neq Q \land \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \to U \in A$
43	1 4	atcmp	$⊢ (K \in AtLat \land F \in A \land U \in A) \to (F \underset{˙}{\leq} U \leftrightarrow F = U)$
44	38 16 42 43	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 (R \in A \land \neg R \underset{˙}{\leq} W)) \land (P \neq Q \land \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \to (F \underset{˙}{\leq} U \leftrightarrow F = U)$
45	21 36 44	3bitrd	$⊢ ((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 (R \in A \land \neg R \underset{˙}{\leq} W)) \land (P \neq Q \land \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \to (F \underset{˙}{\leq} W \leftrightarrow F = U)$
46	45	necon3bbid	$⊢ ((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 (R \in A \land \neg R \underset{˙}{\leq} W)) \land (P \neq Q \land \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \to (\neg F \underset{˙}{\leq} W \leftrightarrow F \neq U)$
47	9 46	mpbird	$⊢ ((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 (R \in A \land \neg R \underset{˙}{\leq} W)) \land (P \neq Q \land \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \to \neg F \underset{˙}{\leq} W$

Metamath Proof Explorer

Theorem cdleme3

Proof