cdleme30a

Description: Part of proof of Lemma E in Crawley p. 113. (Contributed by NM, 9-Feb-2013)

	Ref	Expression
Hypotheses	cdleme30.b	$⊢ B = {Base}_{K}$
	cdleme30.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
	cdleme30.j	$⊢ \underset{˙}{\lor} = join (K)$
	cdleme30.m	$⊢ \underset{˙}{\land} = meet (K)$
	cdleme30.a	$⊢ A = Atoms (K)$
	cdleme30.h	$⊢ H = LHyp (K)$
Assertion	cdleme30a	$⊢ ((K \in HL \land W \in H) \land (s \in A \land (X \in B \land \neg X \underset{˙}{\leq} W) \land Y \in B) \land (s \underset{˙}{\lor} (X \underset{˙}{\land} W) = X \land X \underset{˙}{\leq} Y)) \to s \underset{˙}{\lor} (Y \underset{˙}{\land} W) = Y$

Proof

Step	Hyp	Ref	Expression
1		cdleme30.b	$⊢ B = {Base}_{K}$
2		cdleme30.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
3		cdleme30.j	$⊢ \underset{˙}{\lor} = join (K)$
4		cdleme30.m	$⊢ \underset{˙}{\land} = meet (K)$
5		cdleme30.a	$⊢ A = Atoms (K)$
6		cdleme30.h	$⊢ H = LHyp (K)$
7		simp1l	$⊢ ((K \in HL \land W \in H) \land (s \in A \land (X \in B \land \neg X \underset{˙}{\leq} W) \land Y \in B) \land (s \underset{˙}{\lor} (X \underset{˙}{\land} W) = X \land X \underset{˙}{\leq} Y)) \to K \in HL$
8	7	hllatd	$⊢ ((K \in HL \land W \in H) \land (s \in A \land (X \in B \land \neg X \underset{˙}{\leq} W) \land Y \in B) \land (s \underset{˙}{\lor} (X \underset{˙}{\land} W) = X \land X \underset{˙}{\leq} Y)) \to K \in Lat$
9		simp21	$⊢ ((K \in HL \land W \in H) \land (s \in A \land (X \in B \land \neg X \underset{˙}{\leq} W) \land Y \in B) \land (s \underset{˙}{\lor} (X \underset{˙}{\land} W) = X \land X \underset{˙}{\leq} Y)) \to s \in A$
10	1 5	atbase	$⊢ s \in A \to s \in B$
11	9 10	syl	$⊢ ((K \in HL \land W \in H) \land (s \in A \land (X \in B \land \neg X \underset{˙}{\leq} W) \land Y \in B) \land (s \underset{˙}{\lor} (X \underset{˙}{\land} W) = X \land X \underset{˙}{\leq} Y)) \to s \in B$
12		simp23	$⊢ ((K \in HL \land W \in H) \land (s \in A \land (X \in B \land \neg X \underset{˙}{\leq} W) \land Y \in B) \land (s \underset{˙}{\lor} (X \underset{˙}{\land} W) = X \land X \underset{˙}{\leq} Y)) \to Y \in B$
13		simp1r	$⊢ ((K \in HL \land W \in H) \land (s \in A \land (X \in B \land \neg X \underset{˙}{\leq} W) \land Y \in B) \land (s \underset{˙}{\lor} (X \underset{˙}{\land} W) = X \land X \underset{˙}{\leq} Y)) \to W \in H$
14	1 6	lhpbase	$⊢ W \in H \to W \in B$
15	13 14	syl	$⊢ ((K \in HL \land W \in H) \land (s \in A \land (X \in B \land \neg X \underset{˙}{\leq} W) \land Y \in B) \land (s \underset{˙}{\lor} (X \underset{˙}{\land} W) = X \land X \underset{˙}{\leq} Y)) \to W \in B$
16	1 4	latmcl	$⊢ (K \in Lat \land Y \in B \land W \in B) \to Y \underset{˙}{\land} W \in B$
17	8 12 15 16	syl3anc	$⊢ ((K \in HL \land W \in H) \land (s \in A \land (X \in B \land \neg X \underset{˙}{\leq} W) \land Y \in B) \land (s \underset{˙}{\lor} (X \underset{˙}{\land} W) = X \land X \underset{˙}{\leq} Y)) \to Y \underset{˙}{\land} W \in B$
18		simp22l	$⊢ ((K \in HL \land W \in H) \land (s \in A \land (X \in B \land \neg X \underset{˙}{\leq} W) \land Y \in B) \land (s \underset{˙}{\lor} (X \underset{˙}{\land} W) = X \land X \underset{˙}{\leq} Y)) \to X \in B$
19	1 3	latjass	$⊢ (K \in Lat \land (s \in B \land Y \underset{˙}{\land} W \in B \land X \in B)) \to (s \underset{˙}{\lor} (Y \underset{˙}{\land} W)) \underset{˙}{\lor} X = s \underset{˙}{\lor} ((Y \underset{˙}{\land} W) \underset{˙}{\lor} X)$
20	8 11 17 18 19	syl13anc	$⊢ ((K \in HL \land W \in H) \land (s \in A \land (X \in B \land \neg X \underset{˙}{\leq} W) \land Y \in B) \land (s \underset{˙}{\lor} (X \underset{˙}{\land} W) = X \land X \underset{˙}{\leq} Y)) \to (s \underset{˙}{\lor} (Y \underset{˙}{\land} W)) \underset{˙}{\lor} X = s \underset{˙}{\lor} ((Y \underset{˙}{\land} W) \underset{˙}{\lor} X)$
21		simp3l	$⊢ ((K \in HL \land W \in H) \land (s \in A \land (X \in B \land \neg X \underset{˙}{\leq} W) \land Y \in B) \land (s \underset{˙}{\lor} (X \underset{˙}{\land} W) = X \land X \underset{˙}{\leq} Y)) \to s \underset{˙}{\lor} (X \underset{˙}{\land} W) = X$
22		simp3r	$⊢ ((K \in HL \land W \in H) \land (s \in A \land (X \in B \land \neg X \underset{˙}{\leq} W) \land Y \in B) \land (s \underset{˙}{\lor} (X \underset{˙}{\land} W) = X \land X \underset{˙}{\leq} Y)) \to X \underset{˙}{\leq} Y$
23	1 2 4	latmlem1	$⊢ (K \in Lat \land (X \in B \land Y \in B \land W \in B)) \to (X \underset{˙}{\leq} Y \to (X \underset{˙}{\land} W) \underset{˙}{\leq} (Y \underset{˙}{\land} W))$
24	8 18 12 15 23	syl13anc	$⊢ ((K \in HL \land W \in H) \land (s \in A \land (X \in B \land \neg X \underset{˙}{\leq} W) \land Y \in B) \land (s \underset{˙}{\lor} (X \underset{˙}{\land} W) = X \land X \underset{˙}{\leq} Y)) \to (X \underset{˙}{\leq} Y \to (X \underset{˙}{\land} W) \underset{˙}{\leq} (Y \underset{˙}{\land} W))$
25	22 24	mpd	$⊢ ((K \in HL \land W \in H) \land (s \in A \land (X \in B \land \neg X \underset{˙}{\leq} W) \land Y \in B) \land (s \underset{˙}{\lor} (X \underset{˙}{\land} W) = X \land X \underset{˙}{\leq} Y)) \to (X \underset{˙}{\land} W) \underset{˙}{\leq} (Y \underset{˙}{\land} W)$
26	1 4	latmcl	$⊢ (K \in Lat \land X \in B \land W \in B) \to X \underset{˙}{\land} W \in B$
27	8 18 15 26	syl3anc	$⊢ ((K \in HL \land W \in H) \land (s \in A \land (X \in B \land \neg X \underset{˙}{\leq} W) \land Y \in B) \land (s \underset{˙}{\lor} (X \underset{˙}{\land} W) = X \land X \underset{˙}{\leq} Y)) \to X \underset{˙}{\land} W \in B$
28	1 2 3	latjlej2	$⊢ (K \in Lat \land (X \underset{˙}{\land} W \in B \land Y \underset{˙}{\land} W \in B \land s \in B)) \to ((X \underset{˙}{\land} W) \underset{˙}{\leq} (Y \underset{˙}{\land} W) \to (s \underset{˙}{\lor} (X \underset{˙}{\land} W)) \underset{˙}{\leq} (s \underset{˙}{\lor} (Y \underset{˙}{\land} W)))$
29	8 27 17 11 28	syl13anc	$⊢ ((K \in HL \land W \in H) \land (s \in A \land (X \in B \land \neg X \underset{˙}{\leq} W) \land Y \in B) \land (s \underset{˙}{\lor} (X \underset{˙}{\land} W) = X \land X \underset{˙}{\leq} Y)) \to ((X \underset{˙}{\land} W) \underset{˙}{\leq} (Y \underset{˙}{\land} W) \to (s \underset{˙}{\lor} (X \underset{˙}{\land} W)) \underset{˙}{\leq} (s \underset{˙}{\lor} (Y \underset{˙}{\land} W)))$
30	25 29	mpd	$⊢ ((K \in HL \land W \in H) \land (s \in A \land (X \in B \land \neg X \underset{˙}{\leq} W) \land Y \in B) \land (s \underset{˙}{\lor} (X \underset{˙}{\land} W) = X \land X \underset{˙}{\leq} Y)) \to (s \underset{˙}{\lor} (X \underset{˙}{\land} W)) \underset{˙}{\leq} (s \underset{˙}{\lor} (Y \underset{˙}{\land} W))$
31	21 30	eqbrtrrd	$⊢ ((K \in HL \land W \in H) \land (s \in A \land (X \in B \land \neg X \underset{˙}{\leq} W) \land Y \in B) \land (s \underset{˙}{\lor} (X \underset{˙}{\land} W) = X \land X \underset{˙}{\leq} Y)) \to X \underset{˙}{\leq} (s \underset{˙}{\lor} (Y \underset{˙}{\land} W))$
32	1 3	latjcl	$⊢ (K \in Lat \land s \in B \land Y \underset{˙}{\land} W \in B) \to s \underset{˙}{\lor} (Y \underset{˙}{\land} W) \in B$
33	8 11 17 32	syl3anc	$⊢ ((K \in HL \land W \in H) \land (s \in A \land (X \in B \land \neg X \underset{˙}{\leq} W) \land Y \in B) \land (s \underset{˙}{\lor} (X \underset{˙}{\land} W) = X \land X \underset{˙}{\leq} Y)) \to s \underset{˙}{\lor} (Y \underset{˙}{\land} W) \in B$
34	1 2 3	latleeqj2	$⊢ (K \in Lat \land X \in B \land s \underset{˙}{\lor} (Y \underset{˙}{\land} W) \in B) \to (X \underset{˙}{\leq} (s \underset{˙}{\lor} (Y \underset{˙}{\land} W)) \leftrightarrow (s \underset{˙}{\lor} (Y \underset{˙}{\land} W)) \underset{˙}{\lor} X = s \underset{˙}{\lor} (Y \underset{˙}{\land} W))$
35	8 18 33 34	syl3anc	$⊢ ((K \in HL \land W \in H) \land (s \in A \land (X \in B \land \neg X \underset{˙}{\leq} W) \land Y \in B) \land (s \underset{˙}{\lor} (X \underset{˙}{\land} W) = X \land X \underset{˙}{\leq} Y)) \to (X \underset{˙}{\leq} (s \underset{˙}{\lor} (Y \underset{˙}{\land} W)) \leftrightarrow (s \underset{˙}{\lor} (Y \underset{˙}{\land} W)) \underset{˙}{\lor} X = s \underset{˙}{\lor} (Y \underset{˙}{\land} W))$
36	31 35	mpbid	$⊢ ((K \in HL \land W \in H) \land (s \in A \land (X \in B \land \neg X \underset{˙}{\leq} W) \land Y \in B) \land (s \underset{˙}{\lor} (X \underset{˙}{\land} W) = X \land X \underset{˙}{\leq} Y)) \to (s \underset{˙}{\lor} (Y \underset{˙}{\land} W)) \underset{˙}{\lor} X = s \underset{˙}{\lor} (Y \underset{˙}{\land} W)$
37		simp1	$⊢ ((K \in HL \land W \in H) \land (s \in A \land (X \in B \land \neg X \underset{˙}{\leq} W) \land Y \in B) \land (s \underset{˙}{\lor} (X \underset{˙}{\land} W) = X \land X \underset{˙}{\leq} Y)) \to (K \in HL \land W \in H)$
38	1 2 3 4 6	lhpmod2i2	$⊢ ((K \in HL \land W \in H) \land (Y \in B \land X \in B) \land X \underset{˙}{\leq} Y) \to (Y \underset{˙}{\land} W) \underset{˙}{\lor} X = Y \underset{˙}{\land} (W \underset{˙}{\lor} X)$
39	37 12 18 22 38	syl121anc	$⊢ ((K \in HL \land W \in H) \land (s \in A \land (X \in B \land \neg X \underset{˙}{\leq} W) \land Y \in B) \land (s \underset{˙}{\lor} (X \underset{˙}{\land} W) = X \land X \underset{˙}{\leq} Y)) \to (Y \underset{˙}{\land} W) \underset{˙}{\lor} X = Y \underset{˙}{\land} (W \underset{˙}{\lor} X)$
40	39	oveq2d	$⊢ ((K \in HL \land W \in H) \land (s \in A \land (X \in B \land \neg X \underset{˙}{\leq} W) \land Y \in B) \land (s \underset{˙}{\lor} (X \underset{˙}{\land} W) = X \land X \underset{˙}{\leq} Y)) \to s \underset{˙}{\lor} ((Y \underset{˙}{\land} W) \underset{˙}{\lor} X) = s \underset{˙}{\lor} (Y \underset{˙}{\land} (W \underset{˙}{\lor} X))$
41		simp22	$⊢ ((K \in HL \land W \in H) \land (s \in A \land (X \in B \land \neg X \underset{˙}{\leq} W) \land Y \in B) \land (s \underset{˙}{\lor} (X \underset{˙}{\land} W) = X \land X \underset{˙}{\leq} Y)) \to (X \in B \land \neg X \underset{˙}{\leq} W)$
42		eqid	$⊢ 1. (K) = 1. (K)$
43	1 2 3 42 6	lhpj1	$⊢ ((K \in HL \land W \in H) \land (X \in B \land \neg X \underset{˙}{\leq} W)) \to W \underset{˙}{\lor} X = 1. (K)$
44	37 41 43	syl2anc	$⊢ ((K \in HL \land W \in H) \land (s \in A \land (X \in B \land \neg X \underset{˙}{\leq} W) \land Y \in B) \land (s \underset{˙}{\lor} (X \underset{˙}{\land} W) = X \land X \underset{˙}{\leq} Y)) \to W \underset{˙}{\lor} X = 1. (K)$
45	44	oveq2d	$⊢ ((K \in HL \land W \in H) \land (s \in A \land (X \in B \land \neg X \underset{˙}{\leq} W) \land Y \in B) \land (s \underset{˙}{\lor} (X \underset{˙}{\land} W) = X \land X \underset{˙}{\leq} Y)) \to Y \underset{˙}{\land} (W \underset{˙}{\lor} X) = Y \underset{˙}{\land} 1. (K)$
46		hlol	$⊢ K \in HL \to K \in OL$
47	7 46	syl	$⊢ ((K \in HL \land W \in H) \land (s \in A \land (X \in B \land \neg X \underset{˙}{\leq} W) \land Y \in B) \land (s \underset{˙}{\lor} (X \underset{˙}{\land} W) = X \land X \underset{˙}{\leq} Y)) \to K \in OL$
48	1 4 42	olm11	$⊢ (K \in OL \land Y \in B) \to Y \underset{˙}{\land} 1. (K) = Y$
49	47 12 48	syl2anc	$⊢ ((K \in HL \land W \in H) \land (s \in A \land (X \in B \land \neg X \underset{˙}{\leq} W) \land Y \in B) \land (s \underset{˙}{\lor} (X \underset{˙}{\land} W) = X \land X \underset{˙}{\leq} Y)) \to Y \underset{˙}{\land} 1. (K) = Y$
50	45 49	eqtrd	$⊢ ((K \in HL \land W \in H) \land (s \in A \land (X \in B \land \neg X \underset{˙}{\leq} W) \land Y \in B) \land (s \underset{˙}{\lor} (X \underset{˙}{\land} W) = X \land X \underset{˙}{\leq} Y)) \to Y \underset{˙}{\land} (W \underset{˙}{\lor} X) = Y$
51	50	oveq2d	$⊢ ((K \in HL \land W \in H) \land (s \in A \land (X \in B \land \neg X \underset{˙}{\leq} W) \land Y \in B) \land (s \underset{˙}{\lor} (X \underset{˙}{\land} W) = X \land X \underset{˙}{\leq} Y)) \to s \underset{˙}{\lor} (Y \underset{˙}{\land} (W \underset{˙}{\lor} X)) = s \underset{˙}{\lor} Y$
52	1 2 3	latlej1	$⊢ (K \in Lat \land s \in B \land X \underset{˙}{\land} W \in B) \to s \underset{˙}{\leq} (s \underset{˙}{\lor} (X \underset{˙}{\land} W))$
53	8 11 27 52	syl3anc	$⊢ ((K \in HL \land W \in H) \land (s \in A \land (X \in B \land \neg X \underset{˙}{\leq} W) \land Y \in B) \land (s \underset{˙}{\lor} (X \underset{˙}{\land} W) = X \land X \underset{˙}{\leq} Y)) \to s \underset{˙}{\leq} (s \underset{˙}{\lor} (X \underset{˙}{\land} W))$
54	53 21	breqtrd	$⊢ ((K \in HL \land W \in H) \land (s \in A \land (X \in B \land \neg X \underset{˙}{\leq} W) \land Y \in B) \land (s \underset{˙}{\lor} (X \underset{˙}{\land} W) = X \land X \underset{˙}{\leq} Y)) \to s \underset{˙}{\leq} X$
55	1 2 8 11 18 12 54 22	lattrd	$⊢ ((K \in HL \land W \in H) \land (s \in A \land (X \in B \land \neg X \underset{˙}{\leq} W) \land Y \in B) \land (s \underset{˙}{\lor} (X \underset{˙}{\land} W) = X \land X \underset{˙}{\leq} Y)) \to s \underset{˙}{\leq} Y$
56	1 2 3	latleeqj1	$⊢ (K \in Lat \land s \in B \land Y \in B) \to (s \underset{˙}{\leq} Y \leftrightarrow s \underset{˙}{\lor} Y = Y)$
57	8 11 12 56	syl3anc	$⊢ ((K \in HL \land W \in H) \land (s \in A \land (X \in B \land \neg X \underset{˙}{\leq} W) \land Y \in B) \land (s \underset{˙}{\lor} (X \underset{˙}{\land} W) = X \land X \underset{˙}{\leq} Y)) \to (s \underset{˙}{\leq} Y \leftrightarrow s \underset{˙}{\lor} Y = Y)$
58	55 57	mpbid	$⊢ ((K \in HL \land W \in H) \land (s \in A \land (X \in B \land \neg X \underset{˙}{\leq} W) \land Y \in B) \land (s \underset{˙}{\lor} (X \underset{˙}{\land} W) = X \land X \underset{˙}{\leq} Y)) \to s \underset{˙}{\lor} Y = Y$
59	40 51 58	3eqtrd	$⊢ ((K \in HL \land W \in H) \land (s \in A \land (X \in B \land \neg X \underset{˙}{\leq} W) \land Y \in B) \land (s \underset{˙}{\lor} (X \underset{˙}{\land} W) = X \land X \underset{˙}{\leq} Y)) \to s \underset{˙}{\lor} ((Y \underset{˙}{\land} W) \underset{˙}{\lor} X) = Y$
60	20 36 59	3eqtr3d	$⊢ ((K \in HL \land W \in H) \land (s \in A \land (X \in B \land \neg X \underset{˙}{\leq} W) \land Y \in B) \land (s \underset{˙}{\lor} (X \underset{˙}{\land} W) = X \land X \underset{˙}{\leq} Y)) \to s \underset{˙}{\lor} (Y \underset{˙}{\land} W) = Y$

Metamath Proof Explorer

Theorem cdleme30a

Proof