cdlemn2

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

	Ref	Expression
Hypotheses	cdlemn2.b	$⊢ B = {Base}_{K}$
	cdlemn2.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
	cdlemn2.j	$⊢ \underset{˙}{\lor} = join (K)$
	cdlemn2.a	$⊢ A = Atoms (K)$
	cdlemn2.h	$⊢ H = LHyp (K)$
	cdlemn2.t	$⊢ T = LTrn (K) (W)$
	cdlemn2.r	$⊢ R = trL (K) (W)$
	cdlemn2.f	$⊢ F = (ι h \in T \| h (Q) = S)$
Assertion	cdlemn2	$⊢ ((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 S \underset{˙}{\leq} (Q \underset{˙}{\lor} X)) \to R (F) \underset{˙}{\leq} X$

Proof

Step	Hyp	Ref	Expression
1		cdlemn2.b	$⊢ B = {Base}_{K}$
2		cdlemn2.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
3		cdlemn2.j	$⊢ \underset{˙}{\lor} = join (K)$
4		cdlemn2.a	$⊢ A = Atoms (K)$
5		cdlemn2.h	$⊢ H = LHyp (K)$
6		cdlemn2.t	$⊢ T = LTrn (K) (W)$
7		cdlemn2.r	$⊢ R = trL (K) (W)$
8		cdlemn2.f	$⊢ F = (ι h \in T \| h (Q) = S)$
9		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 S \underset{˙}{\leq} (Q \underset{˙}{\lor} X)) \to (K \in HL \land W \in H)$
10		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 S \underset{˙}{\leq} (Q \underset{˙}{\lor} X)) \to (Q \in A \land \neg Q \underset{˙}{\leq} W)$
11		simp22	$⊢ ((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 S \underset{˙}{\leq} (Q \underset{˙}{\lor} X)) \to (S \in A \land \neg S \underset{˙}{\leq} W)$
12	2 4 5 6 8	ltrniotacl	$⊢ ((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)) \to F \in T$
13	9 10 11 12	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 S \underset{˙}{\leq} (Q \underset{˙}{\lor} X)) \to F \in T$
14		eqid	$⊢ meet (K) = meet (K)$
15	2 3 14 4 5 6 7	trlval2	$⊢ ((K \in HL \land W \in H) \land F \in T \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \to R (F) = (Q \underset{˙}{\lor} F (Q)) meet (K) W$
16	9 13 10 15	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 S \underset{˙}{\leq} (Q \underset{˙}{\lor} X)) \to R (F) = (Q \underset{˙}{\lor} F (Q)) meet (K) W$
17	2 4 5 6 8	ltrniotaval	$⊢ ((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)) \to F (Q) = S$
18	9 10 11 17	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 S \underset{˙}{\leq} (Q \underset{˙}{\lor} X)) \to F (Q) = S$
19	18	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 S \underset{˙}{\leq} (Q \underset{˙}{\lor} X)) \to Q \underset{˙}{\lor} F (Q) = Q \underset{˙}{\lor} S$
20	19	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 S \underset{˙}{\leq} (Q \underset{˙}{\lor} X)) \to (Q \underset{˙}{\lor} F (Q)) meet (K) W = (Q \underset{˙}{\lor} S) meet (K) W$
21	16 20	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 S \underset{˙}{\leq} (Q \underset{˙}{\lor} X)) \to R (F) = (Q \underset{˙}{\lor} S) meet (K) W$
22		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 S \underset{˙}{\leq} (Q \underset{˙}{\lor} X)) \to K \in HL$
23	22	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 S \underset{˙}{\leq} (Q \underset{˙}{\lor} X)) \to K \in Lat$
24		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 S \underset{˙}{\leq} (Q \underset{˙}{\lor} X)) \to Q \in A$
25	1 4	atbase	$⊢ Q \in A \to Q \in B$
26	24 25	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 S \underset{˙}{\leq} (Q \underset{˙}{\lor} X)) \to Q \in B$
27		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 S \underset{˙}{\leq} (Q \underset{˙}{\lor} X)) \to X \in B$
28	1 2 3	latlej1	$⊢ (K \in Lat \land Q \in B \land X \in B) \to Q \underset{˙}{\leq} (Q \underset{˙}{\lor} X)$
29	23 26 27 28	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 S \underset{˙}{\leq} (Q \underset{˙}{\lor} X)) \to Q \underset{˙}{\leq} (Q \underset{˙}{\lor} X)$
30		simp3	$⊢ ((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 S \underset{˙}{\leq} (Q \underset{˙}{\lor} X)) \to S \underset{˙}{\leq} (Q \underset{˙}{\lor} X)$
31		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 S \underset{˙}{\leq} (Q \underset{˙}{\lor} X)) \to S \in A$
32	1 4	atbase	$⊢ S \in A \to S \in B$
33	31 32	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 S \underset{˙}{\leq} (Q \underset{˙}{\lor} X)) \to S \in B$
34	1 3	latjcl	$⊢ (K \in Lat \land Q \in B \land X \in B) \to Q \underset{˙}{\lor} X \in B$
35	23 26 27 34	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 S \underset{˙}{\leq} (Q \underset{˙}{\lor} X)) \to Q \underset{˙}{\lor} X \in B$
36	1 2 3	latjle12	$⊢ (K \in Lat \land (Q \in B \land S \in B \land Q \underset{˙}{\lor} X \in B)) \to ((Q \underset{˙}{\leq} (Q \underset{˙}{\lor} X) \land S \underset{˙}{\leq} (Q \underset{˙}{\lor} X)) \leftrightarrow (Q \underset{˙}{\lor} S) \underset{˙}{\leq} (Q \underset{˙}{\lor} X))$
37	23 26 33 35 36	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 S \underset{˙}{\leq} (Q \underset{˙}{\lor} X)) \to ((Q \underset{˙}{\leq} (Q \underset{˙}{\lor} X) \land S \underset{˙}{\leq} (Q \underset{˙}{\lor} X)) \leftrightarrow (Q \underset{˙}{\lor} S) \underset{˙}{\leq} (Q \underset{˙}{\lor} X))$
38	29 30 37	mpbi2and	$⊢ ((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 S \underset{˙}{\leq} (Q \underset{˙}{\lor} X)) \to (Q \underset{˙}{\lor} S) \underset{˙}{\leq} (Q \underset{˙}{\lor} X)$
39	1 3 4	hlatjcl	$⊢ (K \in HL \land Q \in A \land S \in A) \to Q \underset{˙}{\lor} S \in B$
40	22 24 31 39	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 S \underset{˙}{\leq} (Q \underset{˙}{\lor} X)) \to Q \underset{˙}{\lor} S \in B$
41		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 S \underset{˙}{\leq} (Q \underset{˙}{\lor} X)) \to W \in H$
42	1 5	lhpbase	$⊢ W \in H \to W \in B$
43	41 42	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 S \underset{˙}{\leq} (Q \underset{˙}{\lor} X)) \to W \in B$
44	1 2 14	latmlem1	$⊢ (K \in Lat \land (Q \underset{˙}{\lor} S \in B \land Q \underset{˙}{\lor} X \in B \land W \in B)) \to ((Q \underset{˙}{\lor} S) \underset{˙}{\leq} (Q \underset{˙}{\lor} X) \to ((Q \underset{˙}{\lor} S) meet (K) W) \underset{˙}{\leq} ((Q \underset{˙}{\lor} X) meet (K) W))$
45	23 40 35 43 44	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 S \underset{˙}{\leq} (Q \underset{˙}{\lor} X)) \to ((Q \underset{˙}{\lor} S) \underset{˙}{\leq} (Q \underset{˙}{\lor} X) \to ((Q \underset{˙}{\lor} S) meet (K) W) \underset{˙}{\leq} ((Q \underset{˙}{\lor} X) meet (K) W))$
46	38 45	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 S \underset{˙}{\leq} (Q \underset{˙}{\lor} X)) \to ((Q \underset{˙}{\lor} S) meet (K) W) \underset{˙}{\leq} ((Q \underset{˙}{\lor} X) meet (K) W)$
47	21 46	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 S \underset{˙}{\leq} (Q \underset{˙}{\lor} X)) \to R (F) \underset{˙}{\leq} ((Q \underset{˙}{\lor} X) meet (K) W)$
48		simp23	$⊢ ((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 S \underset{˙}{\leq} (Q \underset{˙}{\lor} X)) \to (X \in B \land X \underset{˙}{\leq} W)$
49	1 2 3 14 4 5	lhple	$⊢ ((K \in HL \land W \in H) \land (Q \in A \land \neg Q \underset{˙}{\leq} W) \land (X \in B \land X \underset{˙}{\leq} W)) \to (Q \underset{˙}{\lor} X) meet (K) W = X$
50	9 10 48 49	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 S \underset{˙}{\leq} (Q \underset{˙}{\lor} X)) \to (Q \underset{˙}{\lor} X) meet (K) W = X$
51	47 50	breqtrd	$⊢ ((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 S \underset{˙}{\leq} (Q \underset{˙}{\lor} X)) \to R (F) \underset{˙}{\leq} X$

Metamath Proof Explorer

Theorem cdlemn2

Proof