cdleme0e

Description: Part of proof of Lemma E in Crawley p. 113. (Contributed by NM, 13-Jun-2012)

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

Proof

Step	Hyp	Ref	Expression
1		cdleme0.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
2		cdleme0.j	$⊢ \underset{˙}{\lor} = join (K)$
3		cdleme0.m	$⊢ \underset{˙}{\land} = meet (K)$
4		cdleme0.a	$⊢ A = Atoms (K)$
5		cdleme0.h	$⊢ H = LHyp (K)$
6		cdleme0.u	$⊢ U = (P \underset{˙}{\lor} Q) \underset{˙}{\land} W$
7		cdleme0c.3	$⊢ V = (P \underset{˙}{\lor} R) \underset{˙}{\land} W$
8	6 7	oveq12i	$⊢ U \underset{˙}{\land} V = ((P \underset{˙}{\lor} Q) \underset{˙}{\land} W) \underset{˙}{\land} ((P \underset{˙}{\lor} R) \underset{˙}{\land} W)$
9		simp1l	$⊢ ((K \in HL \land W \in H) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land Q \in A \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$
10		hlol	$⊢ K \in HL \to K \in OL$
11	9 10	syl	$⊢ ((K \in HL \land W \in H) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land Q \in A \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 OL$
12		simp21l	$⊢ ((K \in HL \land W \in H) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land Q \in A \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$
13		simp22	$⊢ ((K \in HL \land W \in H) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land Q \in A \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$
14		eqid	$⊢ {Base}_{K} = {Base}_{K}$
15	14 2 4	hlatjcl	$⊢ (K \in HL \land P \in A \land Q \in A) \to P \underset{˙}{\lor} Q \in {Base}_{K}$
16	9 12 13 15	syl3anc	$⊢ ((K \in HL \land W \in H) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land Q \in A \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 \underset{˙}{\lor} Q \in {Base}_{K}$
17		simp23l	$⊢ ((K \in HL \land W \in H) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land Q \in A \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$
18	14 2 4	hlatjcl	$⊢ (K \in HL \land P \in A \land R \in A) \to P \underset{˙}{\lor} R \in {Base}_{K}$
19	9 12 17 18	syl3anc	$⊢ ((K \in HL \land W \in H) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land Q \in A \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 \underset{˙}{\lor} R \in {Base}_{K}$
20		simp1r	$⊢ ((K \in HL \land W \in H) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land Q \in A \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$
21	14 5	lhpbase	$⊢ W \in H \to W \in {Base}_{K}$
22	20 21	syl	$⊢ ((K \in HL \land W \in H) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land Q \in A \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}$
23	14 3	latmmdir	$⊢ (K \in OL \land (P \underset{˙}{\lor} Q \in {Base}_{K} \land P \underset{˙}{\lor} R \in {Base}_{K} \land W \in {Base}_{K})) \to ((P \underset{˙}{\lor} Q) \underset{˙}{\land} (P \underset{˙}{\lor} R)) \underset{˙}{\land} W = ((P \underset{˙}{\lor} Q) \underset{˙}{\land} W) \underset{˙}{\land} ((P \underset{˙}{\lor} R) \underset{˙}{\land} W)$
24	11 16 19 22 23	syl13anc	$⊢ ((K \in HL \land W \in H) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land Q \in A \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 \underset{˙}{\lor} Q) \underset{˙}{\land} (P \underset{˙}{\lor} R)) \underset{˙}{\land} W = ((P \underset{˙}{\lor} Q) \underset{˙}{\land} W) \underset{˙}{\land} ((P \underset{˙}{\lor} R) \underset{˙}{\land} W)$
25	9	hllatd	$⊢ ((K \in HL \land W \in H) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land Q \in A \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$
26	14 4	atbase	$⊢ R \in A \to R \in {Base}_{K}$
27	17 26	syl	$⊢ ((K \in HL \land W \in H) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land Q \in A \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}$
28	14 4	atbase	$⊢ P \in A \to P \in {Base}_{K}$
29	12 28	syl	$⊢ ((K \in HL \land W \in H) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land Q \in A \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 {Base}_{K}$
30	14 4	atbase	$⊢ Q \in A \to Q \in {Base}_{K}$
31	13 30	syl	$⊢ ((K \in HL \land W \in H) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land Q \in A \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 {Base}_{K}$
32		simp3r	$⊢ ((K \in HL \land W \in H) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land Q \in A \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 R \underset{˙}{\leq} (P \underset{˙}{\lor} Q)$
33	14 1 2	latnlej1r	$⊢ (K \in Lat \land (R \in {Base}_{K} \land P \in {Base}_{K} \land Q \in {Base}_{K}) \land \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \to R \neq Q$
34	33	necomd	$⊢ (K \in Lat \land (R \in {Base}_{K} \land P \in {Base}_{K} \land Q \in {Base}_{K}) \land \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \to Q \neq R$
35	25 27 29 31 32 34	syl131anc	$⊢ ((K \in HL \land W \in H) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land Q \in A \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 \neq R$
36		simp3	$⊢ ((K \in HL \land W \in H) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land Q \in A \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 \land \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q))$
37	1 2 4	hlatcon3	$⊢ (K \in HL \land (P \in A \land Q \in A \land R \in A) \land (P \neq Q \land \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \to \neg P \underset{˙}{\leq} (Q \underset{˙}{\lor} R)$
38	9 12 13 17 36 37	syl131anc	$⊢ ((K \in HL \land W \in H) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land Q \in A \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 P \underset{˙}{\leq} (Q \underset{˙}{\lor} R)$
39	1 2 3 4	2llnma2	$⊢ (K \in HL \land (Q \in A \land R \in A \land P \in A) \land (Q \neq R \land \neg P \underset{˙}{\leq} (Q \underset{˙}{\lor} R))) \to (P \underset{˙}{\lor} Q) \underset{˙}{\land} (P \underset{˙}{\lor} R) = P$
40	9 13 17 12 35 38 39	syl132anc	$⊢ ((K \in HL \land W \in H) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land Q \in A \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 \underset{˙}{\lor} Q) \underset{˙}{\land} (P \underset{˙}{\lor} R) = P$
41	40	oveq1d	$⊢ ((K \in HL \land W \in H) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land Q \in A \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 \underset{˙}{\lor} Q) \underset{˙}{\land} (P \underset{˙}{\lor} R)) \underset{˙}{\land} W = P \underset{˙}{\land} W$
42	24 41	eqtr3d	$⊢ ((K \in HL \land W \in H) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land Q \in A \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 \underset{˙}{\lor} Q) \underset{˙}{\land} W) \underset{˙}{\land} ((P \underset{˙}{\lor} R) \underset{˙}{\land} W) = P \underset{˙}{\land} W$
43	8 42	syl5eq	$⊢ ((K \in HL \land W \in H) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land Q \in A \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 \underset{˙}{\land} V = P \underset{˙}{\land} W$
44		simp1	$⊢ ((K \in HL \land W \in H) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land Q \in A \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)$
45		simp21	$⊢ ((K \in HL \land W \in H) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land Q \in A \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)$
46		eqid	$⊢ 0. (K) = 0. (K)$
47	1 3 46 4 5	lhpmat	$⊢ ((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W)) \to P \underset{˙}{\land} W = 0. (K)$
48	44 45 47	syl2anc	$⊢ ((K \in HL \land W \in H) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land Q \in A \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 \underset{˙}{\land} W = 0. (K)$
49	43 48	eqtrd	$⊢ ((K \in HL \land W \in H) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land Q \in A \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 \underset{˙}{\land} V = 0. (K)$
50		hlatl	$⊢ K \in HL \to K \in AtLat$
51	9 50	syl	$⊢ ((K \in HL \land W \in H) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land Q \in A \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$
52		simp3l	$⊢ ((K \in HL \land W \in H) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land Q \in A \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$
53	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$
54	44 45 13 52 53	syl112anc	$⊢ ((K \in HL \land W \in H) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land Q \in A \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$
55	14 1 2	latnlej1l	$⊢ (K \in Lat \land (R \in {Base}_{K} \land P \in {Base}_{K} \land Q \in {Base}_{K}) \land \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \to R \neq P$
56	55	necomd	$⊢ (K \in Lat \land (R \in {Base}_{K} \land P \in {Base}_{K} \land Q \in {Base}_{K}) \land \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \to P \neq R$
57	25 27 29 31 32 56	syl131anc	$⊢ ((K \in HL \land W \in H) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land Q \in A \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 R$
58	1 2 3 4 5 7	lhpat2	$⊢ ((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (R \in A \land P \neq R)) \to V \in A$
59	44 45 17 57 58	syl112anc	$⊢ ((K \in HL \land W \in H) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land Q \in A \land (R \in A \land \neg R \underset{˙}{\leq} W)) \land (P \neq Q \land \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \to V \in A$
60	3 46 4	atnem0	$⊢ (K \in AtLat \land U \in A \land V \in A) \to (U \neq V \leftrightarrow U \underset{˙}{\land} V = 0. (K))$
61	51 54 59 60	syl3anc	$⊢ ((K \in HL \land W \in H) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land Q \in A \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 \neq V \leftrightarrow U \underset{˙}{\land} V = 0. (K))$
62	49 61	mpbird	$⊢ ((K \in HL \land W \in H) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land Q \in A \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 \neq V$

Metamath Proof Explorer

Theorem cdleme0e

Proof