cdleme11k

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

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

Proof

Step	Hyp	Ref	Expression
1		cdleme11.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
2		cdleme11.j	$⊢ \underset{˙}{\lor} = join (K)$
3		cdleme11.m	$⊢ \underset{˙}{\land} = meet (K)$
4		cdleme11.a	$⊢ A = Atoms (K)$
5		cdleme11.h	$⊢ H = LHyp (K)$
6		cdleme11.u	$⊢ U = (P \underset{˙}{\lor} Q) \underset{˙}{\land} W$
7		cdleme11.c	$⊢ C = (P \underset{˙}{\lor} S) \underset{˙}{\land} W$
8		cdleme11.d	$⊢ D = (P \underset{˙}{\lor} T) \underset{˙}{\land} W$
9		cdleme11.f	$⊢ F = (S \underset{˙}{\lor} U) \underset{˙}{\land} (Q \underset{˙}{\lor} ((P \underset{˙}{\lor} S) \underset{˙}{\land} W))$
10	1 2 3 4 5 6 7 6 9	cdleme11j	$⊢ ((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 (S \in A \land \neg S \underset{˙}{\leq} W)) \land (P \neq Q \land \neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \to C \underset{˙}{\leq} (Q \underset{˙}{\lor} F)$
11		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 (S \in A \land \neg S \underset{˙}{\leq} W)) \land (P \neq Q \land \neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \to K \in HL$
12	11	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 (S \in A \land \neg S \underset{˙}{\leq} W)) \land (P \neq Q \land \neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \to K \in Lat$
13		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 (S \in A \land \neg S \underset{˙}{\leq} W)) \land (P \neq Q \land \neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \to P \in A$
14		eqid	$⊢ {Base}_{K} = {Base}_{K}$
15	14 4	atbase	$⊢ P \in A \to P \in {Base}_{K}$
16	13 15	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 (S \in A \land \neg S \underset{˙}{\leq} W)) \land (P \neq Q \land \neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \to P \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 \neg Q \underset{˙}{\leq} W) \land (S \in A \land \neg S \underset{˙}{\leq} W)) \land (P \neq Q \land \neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \to S \in A$
18	14 4	atbase	$⊢ S \in A \to S \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 \neg Q \underset{˙}{\leq} W) \land (S \in A \land \neg S \underset{˙}{\leq} W)) \land (P \neq Q \land \neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \to S \in {Base}_{K}$
20	14 2	latjcl	$⊢ (K \in Lat \land P \in {Base}_{K} \land S \in {Base}_{K}) \to P \underset{˙}{\lor} S \in {Base}_{K}$
21	12 16 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 \neg Q \underset{˙}{\leq} W) \land (S \in A \land \neg S \underset{˙}{\leq} W)) \land (P \neq Q \land \neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \to P \underset{˙}{\lor} S \in {Base}_{K}$
22		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 (S \in A \land \neg S \underset{˙}{\leq} W)) \land (P \neq Q \land \neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \to W \in H$
23	14 5	lhpbase	$⊢ W \in H \to W \in {Base}_{K}$
24	22 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 (S \in A \land \neg S \underset{˙}{\leq} W)) \land (P \neq Q \land \neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \to W \in {Base}_{K}$
25	14 1 3	latmle2	$⊢ (K \in Lat \land P \underset{˙}{\lor} S \in {Base}_{K} \land W \in {Base}_{K}) \to ((P \underset{˙}{\lor} S) \underset{˙}{\land} W) \underset{˙}{\leq} W$
26	12 21 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 (S \in A \land \neg S \underset{˙}{\leq} W)) \land (P \neq Q \land \neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \to ((P \underset{˙}{\lor} S) \underset{˙}{\land} W) \underset{˙}{\leq} W$
27	7 26	eqbrtrid	$⊢ ((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 (S \in A \land \neg S \underset{˙}{\leq} W)) \land (P \neq Q \land \neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \to C \underset{˙}{\leq} W$
28		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 (S \in A \land \neg S \underset{˙}{\leq} W)) \land (P \neq Q \land \neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \to (K \in HL \land W \in H)$
29		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 (S \in A \land \neg S \underset{˙}{\leq} W)) \land (P \neq Q \land \neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \to (P \in A \land \neg P \underset{˙}{\leq} W)$
30		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 (S \in A \land \neg S \underset{˙}{\leq} W)) \land (P \neq Q \land \neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \to Q \in A$
31		simp3r	$⊢ ((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 (S \in A \land \neg S \underset{˙}{\leq} W)) \land (P \neq Q \land \neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \to \neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q)$
32	1 2 3 4	cdleme00a	$⊢ (K \in HL \land (P \in A \land Q \in A \land S \in A) \land \neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \to S \neq P$
33	11 13 30 17 31 32	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 (S \in A \land \neg S \underset{˙}{\leq} W)) \land (P \neq Q \land \neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \to S \neq P$
34	33	necomd	$⊢ ((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 (S \in A \land \neg S \underset{˙}{\leq} W)) \land (P \neq Q \land \neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \to P \neq S$
35	1 2 3 4 5 7	cdleme9a	$⊢ ((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (S \in A \land P \neq S)) \to C \in A$
36	28 29 17 34 35	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 (S \in A \land \neg S \underset{˙}{\leq} W)) \land (P \neq Q \land \neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \to C \in A$
37	14 4	atbase	$⊢ C \in A \to C \in {Base}_{K}$
38	36 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 (S \in A \land \neg S \underset{˙}{\leq} W)) \land (P \neq Q \land \neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \to C \in {Base}_{K}$
39	14 4	atbase	$⊢ Q \in A \to Q \in {Base}_{K}$
40	30 39	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 (S \in A \land \neg S \underset{˙}{\leq} W)) \land (P \neq Q \land \neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \to Q \in {Base}_{K}$
41	1 2 3 4 5 6 9	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 (S \in A \land \neg S \underset{˙}{\leq} W)) \land (P \neq Q \land \neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \to F \in A$
42	14 4	atbase	$⊢ F \in A \to F \in {Base}_{K}$
43	41 42	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 (S \in A \land \neg S \underset{˙}{\leq} W)) \land (P \neq Q \land \neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \to F \in {Base}_{K}$
44	14 2	latjcl	$⊢ (K \in Lat \land Q \in {Base}_{K} \land F \in {Base}_{K}) \to Q \underset{˙}{\lor} F \in {Base}_{K}$
45	12 40 43 44	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 (S \in A \land \neg S \underset{˙}{\leq} W)) \land (P \neq Q \land \neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \to Q \underset{˙}{\lor} F \in {Base}_{K}$
46	14 1 3	latlem12	$⊢ (K \in Lat \land (C \in {Base}_{K} \land Q \underset{˙}{\lor} F \in {Base}_{K} \land W \in {Base}_{K})) \to ((C \underset{˙}{\leq} (Q \underset{˙}{\lor} F) \land C \underset{˙}{\leq} W) \leftrightarrow C \underset{˙}{\leq} ((Q \underset{˙}{\lor} F) \underset{˙}{\land} W))$
47	12 38 45 24 46	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 (S \in A \land \neg S \underset{˙}{\leq} W)) \land (P \neq Q \land \neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \to ((C \underset{˙}{\leq} (Q \underset{˙}{\lor} F) \land C \underset{˙}{\leq} W) \leftrightarrow C \underset{˙}{\leq} ((Q \underset{˙}{\lor} F) \underset{˙}{\land} W))$
48	10 27 47	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 (S \in A \land \neg S \underset{˙}{\leq} W)) \land (P \neq Q \land \neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \to C \underset{˙}{\leq} ((Q \underset{˙}{\lor} F) \underset{˙}{\land} W)$
49		hlatl	$⊢ K \in HL \to K \in AtLat$
50	11 49	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 (S \in A \land \neg S \underset{˙}{\leq} W)) \land (P \neq Q \land \neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \to K \in AtLat$
51		simp22	$⊢ ((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 (S \in A \land \neg S \underset{˙}{\leq} W)) \land (P \neq Q \land \neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \to (Q \in A \land \neg Q \underset{˙}{\leq} W)$
52		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 (S \in A \land \neg S \underset{˙}{\leq} W)) \land (P \neq Q \land \neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \to (P \neq Q \land \neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q))$
53	1 2 3 4 5 6 7 6 9	cdleme11h	$⊢ ((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 S \in A) \land (P \neq Q \land \neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \to F \neq Q$
54	28 29 51 17 52 53	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 (S \in A \land \neg S \underset{˙}{\leq} W)) \land (P \neq Q \land \neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \to F \neq Q$
55	54	necomd	$⊢ ((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 (S \in A \land \neg S \underset{˙}{\leq} W)) \land (P \neq Q \land \neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \to Q \neq F$
56	1 2 3 4 5	lhpat	$⊢ ((K \in HL \land W \in H) \land (Q \in A \land \neg Q \underset{˙}{\leq} W) \land (F \in A \land Q \neq F)) \to (Q \underset{˙}{\lor} F) \underset{˙}{\land} W \in A$
57	28 51 41 55 56	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 (S \in A \land \neg S \underset{˙}{\leq} W)) \land (P \neq Q \land \neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \to (Q \underset{˙}{\lor} F) \underset{˙}{\land} W \in A$
58	1 4	atcmp	$⊢ (K \in AtLat \land C \in A \land (Q \underset{˙}{\lor} F) \underset{˙}{\land} W \in A) \to (C \underset{˙}{\leq} ((Q \underset{˙}{\lor} F) \underset{˙}{\land} W) \leftrightarrow C = (Q \underset{˙}{\lor} F) \underset{˙}{\land} W)$
59	50 36 57 58	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 (S \in A \land \neg S \underset{˙}{\leq} W)) \land (P \neq Q \land \neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \to (C \underset{˙}{\leq} ((Q \underset{˙}{\lor} F) \underset{˙}{\land} W) \leftrightarrow C = (Q \underset{˙}{\lor} F) \underset{˙}{\land} W)$
60	48 59	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 (S \in A \land \neg S \underset{˙}{\leq} W)) \land (P \neq Q \land \neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \to C = (Q \underset{˙}{\lor} F) \underset{˙}{\land} W$

Metamath Proof Explorer

Theorem cdleme11k

Proof