cdlemn10

Description: Part of proof of Lemma N of Crawley p. 121 line 36. (Contributed by NM, 27-Feb-2014)

	Ref	Expression
Hypotheses	cdlemn10.b	$⊢ B = {Base}_{K}$
	cdlemn10.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
	cdlemn10.j	$⊢ \underset{˙}{\lor} = join (K)$
	cdlemn10.a	$⊢ A = Atoms (K)$
	cdlemn10.h	$⊢ H = LHyp (K)$
	cdlemn10.t	$⊢ T = LTrn (K) (W)$
	cdlemn10.r	$⊢ R = trL (K) (W)$
Assertion	cdlemn10	$⊢ ((K \in HL \land W \in H) \land ((Q \in A \land \neg Q \underset{˙}{\leq} W) \land (S \in A \land \neg S \underset{˙}{\leq} W) \land (X \in B \land X \underset{˙}{\leq} W)) \land (g \in T \land g (Q) = S \land R (g) \underset{˙}{\leq} X)) \to S \underset{˙}{\leq} (Q \underset{˙}{\lor} X)$

Proof

Step	Hyp	Ref	Expression
1		cdlemn10.b	$⊢ B = {Base}_{K}$
2		cdlemn10.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
3		cdlemn10.j	$⊢ \underset{˙}{\lor} = join (K)$
4		cdlemn10.a	$⊢ A = Atoms (K)$
5		cdlemn10.h	$⊢ H = LHyp (K)$
6		cdlemn10.t	$⊢ T = LTrn (K) (W)$
7		cdlemn10.r	$⊢ R = trL (K) (W)$
8		simp1l	$⊢ ((K \in HL \land W \in H) \land ((Q \in A \land \neg Q \underset{˙}{\leq} W) \land (S \in A \land \neg S \underset{˙}{\leq} W) \land (X \in B \land X \underset{˙}{\leq} W)) \land (g \in T \land g (Q) = S \land R (g) \underset{˙}{\leq} X)) \to K \in HL$
9	8	hllatd	$⊢ ((K \in HL \land W \in H) \land ((Q \in A \land \neg Q \underset{˙}{\leq} W) \land (S \in A \land \neg S \underset{˙}{\leq} W) \land (X \in B \land X \underset{˙}{\leq} W)) \land (g \in T \land g (Q) = S \land R (g) \underset{˙}{\leq} X)) \to K \in Lat$
10		simp22l	$⊢ ((K \in HL \land W \in H) \land ((Q \in A \land \neg Q \underset{˙}{\leq} W) \land (S \in A \land \neg S \underset{˙}{\leq} W) \land (X \in B \land X \underset{˙}{\leq} W)) \land (g \in T \land g (Q) = S \land R (g) \underset{˙}{\leq} X)) \to S \in A$
11	1 4	atbase	$⊢ S \in A \to S \in B$
12	10 11	syl	$⊢ ((K \in HL \land W \in H) \land ((Q \in A \land \neg Q \underset{˙}{\leq} W) \land (S \in A \land \neg S \underset{˙}{\leq} W) \land (X \in B \land X \underset{˙}{\leq} W)) \land (g \in T \land g (Q) = S \land R (g) \underset{˙}{\leq} X)) \to S \in B$
13		simp21l	$⊢ ((K \in HL \land W \in H) \land ((Q \in A \land \neg Q \underset{˙}{\leq} W) \land (S \in A \land \neg S \underset{˙}{\leq} W) \land (X \in B \land X \underset{˙}{\leq} W)) \land (g \in T \land g (Q) = S \land R (g) \underset{˙}{\leq} X)) \to Q \in A$
14	1 3 4	hlatjcl	$⊢ (K \in HL \land Q \in A \land S \in A) \to Q \underset{˙}{\lor} S \in B$
15	8 13 10 14	syl3anc	$⊢ ((K \in HL \land W \in H) \land ((Q \in A \land \neg Q \underset{˙}{\leq} W) \land (S \in A \land \neg S \underset{˙}{\leq} W) \land (X \in B \land X \underset{˙}{\leq} W)) \land (g \in T \land g (Q) = S \land R (g) \underset{˙}{\leq} X)) \to Q \underset{˙}{\lor} S \in B$
16	1 4	atbase	$⊢ Q \in A \to Q \in B$
17	13 16	syl	$⊢ ((K \in HL \land W \in H) \land ((Q \in A \land \neg Q \underset{˙}{\leq} W) \land (S \in A \land \neg S \underset{˙}{\leq} W) \land (X \in B \land X \underset{˙}{\leq} W)) \land (g \in T \land g (Q) = S \land R (g) \underset{˙}{\leq} X)) \to Q \in B$
18		simp23l	$⊢ ((K \in HL \land W \in H) \land ((Q \in A \land \neg Q \underset{˙}{\leq} W) \land (S \in A \land \neg S \underset{˙}{\leq} W) \land (X \in B \land X \underset{˙}{\leq} W)) \land (g \in T \land g (Q) = S \land R (g) \underset{˙}{\leq} X)) \to X \in B$
19	1 3	latjcl	$⊢ (K \in Lat \land Q \in B \land X \in B) \to Q \underset{˙}{\lor} X \in B$
20	9 17 18 19	syl3anc	$⊢ ((K \in HL \land W \in H) \land ((Q \in A \land \neg Q \underset{˙}{\leq} W) \land (S \in A \land \neg S \underset{˙}{\leq} W) \land (X \in B \land X \underset{˙}{\leq} W)) \land (g \in T \land g (Q) = S \land R (g) \underset{˙}{\leq} X)) \to Q \underset{˙}{\lor} X \in B$
21	2 3 4	hlatlej2	$⊢ (K \in HL \land Q \in A \land S \in A) \to S \underset{˙}{\leq} (Q \underset{˙}{\lor} S)$
22	8 13 10 21	syl3anc	$⊢ ((K \in HL \land W \in H) \land ((Q \in A \land \neg Q \underset{˙}{\leq} W) \land (S \in A \land \neg S \underset{˙}{\leq} W) \land (X \in B \land X \underset{˙}{\leq} W)) \land (g \in T \land g (Q) = S \land R (g) \underset{˙}{\leq} X)) \to S \underset{˙}{\leq} (Q \underset{˙}{\lor} S)$
23		simp1r	$⊢ ((K \in HL \land W \in H) \land ((Q \in A \land \neg Q \underset{˙}{\leq} W) \land (S \in A \land \neg S \underset{˙}{\leq} W) \land (X \in B \land X \underset{˙}{\leq} W)) \land (g \in T \land g (Q) = S \land R (g) \underset{˙}{\leq} X)) \to W \in H$
24	1 5	lhpbase	$⊢ W \in H \to W \in B$
25	23 24	syl	$⊢ ((K \in HL \land W \in H) \land ((Q \in A \land \neg Q \underset{˙}{\leq} W) \land (S \in A \land \neg S \underset{˙}{\leq} W) \land (X \in B \land X \underset{˙}{\leq} W)) \land (g \in T \land g (Q) = S \land R (g) \underset{˙}{\leq} X)) \to W \in B$
26	2 3 4	hlatlej1	$⊢ (K \in HL \land Q \in A \land S \in A) \to Q \underset{˙}{\leq} (Q \underset{˙}{\lor} S)$
27	8 13 10 26	syl3anc	$⊢ ((K \in HL \land W \in H) \land ((Q \in A \land \neg Q \underset{˙}{\leq} W) \land (S \in A \land \neg S \underset{˙}{\leq} W) \land (X \in B \land X \underset{˙}{\leq} W)) \land (g \in T \land g (Q) = S \land R (g) \underset{˙}{\leq} X)) \to Q \underset{˙}{\leq} (Q \underset{˙}{\lor} S)$
28		eqid	$⊢ meet (K) = meet (K)$
29	1 2 3 28 4	atmod3i1	$⊢ (K \in HL \land (Q \in A \land Q \underset{˙}{\lor} S \in B \land W \in B) \land Q \underset{˙}{\leq} (Q \underset{˙}{\lor} S)) \to Q \underset{˙}{\lor} ((Q \underset{˙}{\lor} S) meet (K) W) = (Q \underset{˙}{\lor} S) meet (K) (Q \underset{˙}{\lor} W)$
30	8 13 15 25 27 29	syl131anc	$⊢ ((K \in HL \land W \in H) \land ((Q \in A \land \neg Q \underset{˙}{\leq} W) \land (S \in A \land \neg S \underset{˙}{\leq} W) \land (X \in B \land X \underset{˙}{\leq} W)) \land (g \in T \land g (Q) = S \land R (g) \underset{˙}{\leq} X)) \to Q \underset{˙}{\lor} ((Q \underset{˙}{\lor} S) meet (K) W) = (Q \underset{˙}{\lor} S) meet (K) (Q \underset{˙}{\lor} W)$
31		simp1	$⊢ ((K \in HL \land W \in H) \land ((Q \in A \land \neg Q \underset{˙}{\leq} W) \land (S \in A \land \neg S \underset{˙}{\leq} W) \land (X \in B \land X \underset{˙}{\leq} W)) \land (g \in T \land g (Q) = S \land R (g) \underset{˙}{\leq} X)) \to (K \in HL \land W \in H)$
32		simp21	$⊢ ((K \in HL \land W \in H) \land ((Q \in A \land \neg Q \underset{˙}{\leq} W) \land (S \in A \land \neg S \underset{˙}{\leq} W) \land (X \in B \land X \underset{˙}{\leq} W)) \land (g \in T \land g (Q) = S \land R (g) \underset{˙}{\leq} X)) \to (Q \in A \land \neg Q \underset{˙}{\leq} W)$
33		eqid	$⊢ 1. (K) = 1. (K)$
34	2 3 33 4 5	lhpjat2	$⊢ ((K \in HL \land W \in H) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \to Q \underset{˙}{\lor} W = 1. (K)$
35	31 32 34	syl2anc	$⊢ ((K \in HL \land W \in H) \land ((Q \in A \land \neg Q \underset{˙}{\leq} W) \land (S \in A \land \neg S \underset{˙}{\leq} W) \land (X \in B \land X \underset{˙}{\leq} W)) \land (g \in T \land g (Q) = S \land R (g) \underset{˙}{\leq} X)) \to Q \underset{˙}{\lor} W = 1. (K)$
36	35	oveq2d	$⊢ ((K \in HL \land W \in H) \land ((Q \in A \land \neg Q \underset{˙}{\leq} W) \land (S \in A \land \neg S \underset{˙}{\leq} W) \land (X \in B \land X \underset{˙}{\leq} W)) \land (g \in T \land g (Q) = S \land R (g) \underset{˙}{\leq} X)) \to (Q \underset{˙}{\lor} S) meet (K) (Q \underset{˙}{\lor} W) = (Q \underset{˙}{\lor} S) meet (K) 1. (K)$
37		hlol	$⊢ K \in HL \to K \in OL$
38	8 37	syl	$⊢ ((K \in HL \land W \in H) \land ((Q \in A \land \neg Q \underset{˙}{\leq} W) \land (S \in A \land \neg S \underset{˙}{\leq} W) \land (X \in B \land X \underset{˙}{\leq} W)) \land (g \in T \land g (Q) = S \land R (g) \underset{˙}{\leq} X)) \to K \in OL$
39	1 28 33	olm11	$⊢ (K \in OL \land Q \underset{˙}{\lor} S \in B) \to (Q \underset{˙}{\lor} S) meet (K) 1. (K) = Q \underset{˙}{\lor} S$
40	38 15 39	syl2anc	$⊢ ((K \in HL \land W \in H) \land ((Q \in A \land \neg Q \underset{˙}{\leq} W) \land (S \in A \land \neg S \underset{˙}{\leq} W) \land (X \in B \land X \underset{˙}{\leq} W)) \land (g \in T \land g (Q) = S \land R (g) \underset{˙}{\leq} X)) \to (Q \underset{˙}{\lor} S) meet (K) 1. (K) = Q \underset{˙}{\lor} S$
41	30 36 40	3eqtrrd	$⊢ ((K \in HL \land W \in H) \land ((Q \in A \land \neg Q \underset{˙}{\leq} W) \land (S \in A \land \neg S \underset{˙}{\leq} W) \land (X \in B \land X \underset{˙}{\leq} W)) \land (g \in T \land g (Q) = S \land R (g) \underset{˙}{\leq} X)) \to Q \underset{˙}{\lor} S = Q \underset{˙}{\lor} ((Q \underset{˙}{\lor} S) meet (K) W)$
42		simp31	$⊢ ((K \in HL \land W \in H) \land ((Q \in A \land \neg Q \underset{˙}{\leq} W) \land (S \in A \land \neg S \underset{˙}{\leq} W) \land (X \in B \land X \underset{˙}{\leq} W)) \land (g \in T \land g (Q) = S \land R (g) \underset{˙}{\leq} X)) \to g \in T$
43	2 3 28 4 5 6 7	trlval2	$⊢ ((K \in HL \land W \in H) \land g \in T \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \to R (g) = (Q \underset{˙}{\lor} g (Q)) meet (K) W$
44	31 42 32 43	syl3anc	$⊢ ((K \in HL \land W \in H) \land ((Q \in A \land \neg Q \underset{˙}{\leq} W) \land (S \in A \land \neg S \underset{˙}{\leq} W) \land (X \in B \land X \underset{˙}{\leq} W)) \land (g \in T \land g (Q) = S \land R (g) \underset{˙}{\leq} X)) \to R (g) = (Q \underset{˙}{\lor} g (Q)) meet (K) W$
45		simp32	$⊢ ((K \in HL \land W \in H) \land ((Q \in A \land \neg Q \underset{˙}{\leq} W) \land (S \in A \land \neg S \underset{˙}{\leq} W) \land (X \in B \land X \underset{˙}{\leq} W)) \land (g \in T \land g (Q) = S \land R (g) \underset{˙}{\leq} X)) \to g (Q) = S$
46	45	oveq2d	$⊢ ((K \in HL \land W \in H) \land ((Q \in A \land \neg Q \underset{˙}{\leq} W) \land (S \in A \land \neg S \underset{˙}{\leq} W) \land (X \in B \land X \underset{˙}{\leq} W)) \land (g \in T \land g (Q) = S \land R (g) \underset{˙}{\leq} X)) \to Q \underset{˙}{\lor} g (Q) = Q \underset{˙}{\lor} S$
47	46	oveq1d	$⊢ ((K \in HL \land W \in H) \land ((Q \in A \land \neg Q \underset{˙}{\leq} W) \land (S \in A \land \neg S \underset{˙}{\leq} W) \land (X \in B \land X \underset{˙}{\leq} W)) \land (g \in T \land g (Q) = S \land R (g) \underset{˙}{\leq} X)) \to (Q \underset{˙}{\lor} g (Q)) meet (K) W = (Q \underset{˙}{\lor} S) meet (K) W$
48	44 47	eqtrd	$⊢ ((K \in HL \land W \in H) \land ((Q \in A \land \neg Q \underset{˙}{\leq} W) \land (S \in A \land \neg S \underset{˙}{\leq} W) \land (X \in B \land X \underset{˙}{\leq} W)) \land (g \in T \land g (Q) = S \land R (g) \underset{˙}{\leq} X)) \to R (g) = (Q \underset{˙}{\lor} S) meet (K) W$
49		simp33	$⊢ ((K \in HL \land W \in H) \land ((Q \in A \land \neg Q \underset{˙}{\leq} W) \land (S \in A \land \neg S \underset{˙}{\leq} W) \land (X \in B \land X \underset{˙}{\leq} W)) \land (g \in T \land g (Q) = S \land R (g) \underset{˙}{\leq} X)) \to R (g) \underset{˙}{\leq} X$
50	48 49	eqbrtrrd	$⊢ ((K \in HL \land W \in H) \land ((Q \in A \land \neg Q \underset{˙}{\leq} W) \land (S \in A \land \neg S \underset{˙}{\leq} W) \land (X \in B \land X \underset{˙}{\leq} W)) \land (g \in T \land g (Q) = S \land R (g) \underset{˙}{\leq} X)) \to ((Q \underset{˙}{\lor} S) meet (K) W) \underset{˙}{\leq} X$
51	1 28	latmcl	$⊢ (K \in Lat \land Q \underset{˙}{\lor} S \in B \land W \in B) \to (Q \underset{˙}{\lor} S) meet (K) W \in B$
52	9 15 25 51	syl3anc	$⊢ ((K \in HL \land W \in H) \land ((Q \in A \land \neg Q \underset{˙}{\leq} W) \land (S \in A \land \neg S \underset{˙}{\leq} W) \land (X \in B \land X \underset{˙}{\leq} W)) \land (g \in T \land g (Q) = S \land R (g) \underset{˙}{\leq} X)) \to (Q \underset{˙}{\lor} S) meet (K) W \in B$
53	1 2 3	latjlej2	$⊢ (K \in Lat \land ((Q \underset{˙}{\lor} S) meet (K) W \in B \land X \in B \land Q \in B)) \to (((Q \underset{˙}{\lor} S) meet (K) W) \underset{˙}{\leq} X \to (Q \underset{˙}{\lor} ((Q \underset{˙}{\lor} S) meet (K) W)) \underset{˙}{\leq} (Q \underset{˙}{\lor} X))$
54	9 52 18 17 53	syl13anc	$⊢ ((K \in HL \land W \in H) \land ((Q \in A \land \neg Q \underset{˙}{\leq} W) \land (S \in A \land \neg S \underset{˙}{\leq} W) \land (X \in B \land X \underset{˙}{\leq} W)) \land (g \in T \land g (Q) = S \land R (g) \underset{˙}{\leq} X)) \to (((Q \underset{˙}{\lor} S) meet (K) W) \underset{˙}{\leq} X \to (Q \underset{˙}{\lor} ((Q \underset{˙}{\lor} S) meet (K) W)) \underset{˙}{\leq} (Q \underset{˙}{\lor} X))$
55	50 54	mpd	$⊢ ((K \in HL \land W \in H) \land ((Q \in A \land \neg Q \underset{˙}{\leq} W) \land (S \in A \land \neg S \underset{˙}{\leq} W) \land (X \in B \land X \underset{˙}{\leq} W)) \land (g \in T \land g (Q) = S \land R (g) \underset{˙}{\leq} X)) \to (Q \underset{˙}{\lor} ((Q \underset{˙}{\lor} S) meet (K) W)) \underset{˙}{\leq} (Q \underset{˙}{\lor} X)$
56	41 55	eqbrtrd	$⊢ ((K \in HL \land W \in H) \land ((Q \in A \land \neg Q \underset{˙}{\leq} W) \land (S \in A \land \neg S \underset{˙}{\leq} W) \land (X \in B \land X \underset{˙}{\leq} W)) \land (g \in T \land g (Q) = S \land R (g) \underset{˙}{\leq} X)) \to (Q \underset{˙}{\lor} S) \underset{˙}{\leq} (Q \underset{˙}{\lor} X)$
57	1 2 9 12 15 20 22 56	lattrd	$⊢ ((K \in HL \land W \in H) \land ((Q \in A \land \neg Q \underset{˙}{\leq} W) \land (S \in A \land \neg S \underset{˙}{\leq} W) \land (X \in B \land X \underset{˙}{\leq} W)) \land (g \in T \land g (Q) = S \land R (g) \underset{˙}{\leq} X)) \to S \underset{˙}{\leq} (Q \underset{˙}{\lor} X)$

Metamath Proof Explorer

Theorem cdlemn10

Proof