cdleme3c

Description: Part of proof of Lemma E in Crawley p. 113. Lemma leading to cdleme3fa and cdleme3 . (Contributed by NM, 6-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))$
	cdleme3c.z	$⊢ \underset{˙}{0} = 0. (K)$
Assertion	cdleme3c	$⊢ ((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) \land (R \in A \land \neg R \underset{˙}{\leq} W))) \to F \neq \underset{˙}{0}$

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		cdleme3c.z	$⊢ \underset{˙}{0} = 0. (K)$
9		simpll	$⊢ ((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) \land (R \in A \land \neg R \underset{˙}{\leq} W))) \to K \in HL$
10		hllat	$⊢ K \in HL \to K \in Lat$
11	10	ad2antrr	$⊢ ((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) \land (R \in A \land \neg R \underset{˙}{\leq} W))) \to K \in Lat$
12		simpr3l	$⊢ ((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) \land (R \in A \land \neg R \underset{˙}{\leq} W))) \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 P \neq Q) \land (R \in A \land \neg R \underset{˙}{\leq} W))) \to R \in {Base}_{K}$
16		hlop	$⊢ K \in HL \to K \in OP$
17	16	ad2antrr	$⊢ ((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) \land (R \in A \land \neg R \underset{˙}{\leq} W))) \to K \in OP$
18	13 8	op0cl	$⊢ K \in OP \to \underset{˙}{0} \in {Base}_{K}$
19	17 18	syl	$⊢ ((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) \land (R \in A \land \neg R \underset{˙}{\leq} W))) \to \underset{˙}{0} \in {Base}_{K}$
20	13 2	latjcl	$⊢ (K \in Lat \land R \in {Base}_{K} \land \underset{˙}{0} \in {Base}_{K}) \to R \underset{˙}{\lor} \underset{˙}{0} \in {Base}_{K}$
21	11 15 19 20	syl3anc	$⊢ ((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) \land (R \in A \land \neg R \underset{˙}{\leq} W))) \to R \underset{˙}{\lor} \underset{˙}{0} \in {Base}_{K}$
22		simpl	$⊢ ((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) \land (R \in A \land \neg R \underset{˙}{\leq} W))) \to (K \in HL \land W \in H)$
23		simpr1l	$⊢ ((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) \land (R \in A \land \neg R \underset{˙}{\leq} W))) \to P \in A$
24		simpr2l	$⊢ ((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) \land (R \in A \land \neg R \underset{˙}{\leq} W))) \to Q \in A$
25	1 2 3 4 5 6 7 13	cdleme1b	$⊢ ((K \in HL \land W \in H) \land (P \in A \land Q \in A \land R \in A)) \to F \in {Base}_{K}$
26	22 23 24 12 25	syl13anc	$⊢ ((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) \land (R \in A \land \neg R \underset{˙}{\leq} W))) \to F \in {Base}_{K}$
27	13 2	latjcl	$⊢ (K \in Lat \land R \in {Base}_{K} \land F \in {Base}_{K}) \to R \underset{˙}{\lor} F \in {Base}_{K}$
28	11 15 26 27	syl3anc	$⊢ ((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) \land (R \in A \land \neg R \underset{˙}{\leq} W))) \to R \underset{˙}{\lor} F \in {Base}_{K}$
29	13 4	atbase	$⊢ P \in A \to P \in {Base}_{K}$
30	23 29	syl	$⊢ ((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) \land (R \in A \land \neg R \underset{˙}{\leq} W))) \to P \in {Base}_{K}$
31	13 4	atbase	$⊢ Q \in A \to Q \in {Base}_{K}$
32	24 31	syl	$⊢ ((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) \land (R \in A \land \neg R \underset{˙}{\leq} W))) \to Q \in {Base}_{K}$
33	13 2	latjcl	$⊢ (K \in Lat \land P \in {Base}_{K} \land Q \in {Base}_{K}) \to P \underset{˙}{\lor} Q \in {Base}_{K}$
34	11 30 32 33	syl3anc	$⊢ ((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) \land (R \in A \land \neg R \underset{˙}{\leq} W))) \to P \underset{˙}{\lor} Q \in {Base}_{K}$
35	13 5	lhpbase	$⊢ W \in H \to W \in {Base}_{K}$
36	35	ad2antlr	$⊢ ((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) \land (R \in A \land \neg R \underset{˙}{\leq} W))) \to W \in {Base}_{K}$
37	13 1 3	latmle2	$⊢ (K \in Lat \land P \underset{˙}{\lor} Q \in {Base}_{K} \land W \in {Base}_{K}) \to ((P \underset{˙}{\lor} Q) \underset{˙}{\land} W) \underset{˙}{\leq} W$
38	11 34 36 37	syl3anc	$⊢ ((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) \land (R \in A \land \neg R \underset{˙}{\leq} W))) \to ((P \underset{˙}{\lor} Q) \underset{˙}{\land} W) \underset{˙}{\leq} W$
39	6 38	eqbrtrid	$⊢ ((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) \land (R \in A \land \neg R \underset{˙}{\leq} W))) \to U \underset{˙}{\leq} W$
40		simpr3r	$⊢ ((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) \land (R \in A \land \neg R \underset{˙}{\leq} W))) \to \neg R \underset{˙}{\leq} W$
41		nbrne2	$⊢ (U \underset{˙}{\leq} W \land \neg R \underset{˙}{\leq} W) \to U \neq R$
42	39 40 41	syl2anc	$⊢ ((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) \land (R \in A \land \neg R \underset{˙}{\leq} W))) \to U \neq R$
43	42	necomd	$⊢ ((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) \land (R \in A \land \neg R \underset{˙}{\leq} W))) \to R \neq U$
44	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$
45	44	3adant3r3	$⊢ ((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) \land (R \in A \land \neg R \underset{˙}{\leq} W))) \to U \in A$
46		eqid	$⊢ ⋖_{K} = ⋖_{K}$
47	2 46 4	atcvr1	$⊢ (K \in HL \land R \in A \land U \in A) \to (R \neq U \leftrightarrow R ⋖_{K} (R \underset{˙}{\lor} U))$
48	9 12 45 47	syl3anc	$⊢ ((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) \land (R \in A \land \neg R \underset{˙}{\leq} W))) \to (R \neq U \leftrightarrow R ⋖_{K} (R \underset{˙}{\lor} U))$
49	43 48	mpbid	$⊢ ((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) \land (R \in A \land \neg R \underset{˙}{\leq} W))) \to R ⋖_{K} (R \underset{˙}{\lor} U)$
50		hlol	$⊢ K \in HL \to K \in OL$
51	50	ad2antrr	$⊢ ((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) \land (R \in A \land \neg R \underset{˙}{\leq} W))) \to K \in OL$
52	13 2 8	olj01	$⊢ (K \in OL \land R \in {Base}_{K}) \to R \underset{˙}{\lor} \underset{˙}{0} = R$
53	51 15 52	syl2anc	$⊢ ((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) \land (R \in A \land \neg R \underset{˙}{\leq} W))) \to R \underset{˙}{\lor} \underset{˙}{0} = R$
54		simpr3	$⊢ ((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) \land (R \in A \land \neg R \underset{˙}{\leq} W))) \to (R \in A \land \neg R \underset{˙}{\leq} W)$
55	1 2 3 4 5 6 7	cdleme1	$⊢ ((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 = R \underset{˙}{\lor} U$
56	22 23 24 54 55	syl13anc	$⊢ ((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) \land (R \in A \land \neg R \underset{˙}{\leq} W))) \to R \underset{˙}{\lor} F = R \underset{˙}{\lor} U$
57	49 53 56	3brtr4d	$⊢ ((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) \land (R \in A \land \neg R \underset{˙}{\leq} W))) \to (R \underset{˙}{\lor} \underset{˙}{0}) ⋖_{K} (R \underset{˙}{\lor} F)$
58	13 46	cvrne	$⊢ ((K \in HL \land R \underset{˙}{\lor} \underset{˙}{0} \in {Base}_{K} \land R \underset{˙}{\lor} F \in {Base}_{K}) \land (R \underset{˙}{\lor} \underset{˙}{0}) ⋖_{K} (R \underset{˙}{\lor} F)) \to R \underset{˙}{\lor} \underset{˙}{0} \neq R \underset{˙}{\lor} F$
59	9 21 28 57 58	syl31anc	$⊢ ((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) \land (R \in A \land \neg R \underset{˙}{\leq} W))) \to R \underset{˙}{\lor} \underset{˙}{0} \neq R \underset{˙}{\lor} F$
60		oveq2	$⊢ \underset{˙}{0} = F \to R \underset{˙}{\lor} \underset{˙}{0} = R \underset{˙}{\lor} F$
61	60	necon3i	$⊢ R \underset{˙}{\lor} \underset{˙}{0} \neq R \underset{˙}{\lor} F \to \underset{˙}{0} \neq F$
62	59 61	syl	$⊢ ((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) \land (R \in A \land \neg R \underset{˙}{\leq} W))) \to \underset{˙}{0} \neq F$
63	62	necomd	$⊢ ((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) \land (R \in A \land \neg R \underset{˙}{\leq} W))) \to F \neq \underset{˙}{0}$

Metamath Proof Explorer

Theorem cdleme3c

Proof