cdleme23c

Description: Part of proof of Lemma E in Crawley p. 113, 4th paragraph, 6th line on p. 115. (Contributed by NM, 8-Dec-2012)

	Ref	Expression
Hypotheses	cdleme23.b	$⊢ B = {Base}_{K}$
	cdleme23.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
	cdleme23.j	$⊢ \underset{˙}{\lor} = join (K)$
	cdleme23.m	$⊢ \underset{˙}{\land} = meet (K)$
	cdleme23.a	$⊢ A = Atoms (K)$
	cdleme23.h	$⊢ H = LHyp (K)$
	cdleme23.v	$⊢ V = (S \underset{˙}{\lor} T) \underset{˙}{\land} (X \underset{˙}{\land} W)$
Assertion	cdleme23c	$⊢ (((K \in HL \land W \in H) \land (S \in A \land \neg S \underset{˙}{\leq} W) \land (T \in A \land \neg T \underset{˙}{\leq} W)) \land (X \in B \land \neg X \underset{˙}{\leq} W) \land (S \neq T \land S \underset{˙}{\lor} (X \underset{˙}{\land} W) = X \land T \underset{˙}{\lor} (X \underset{˙}{\land} W) = X)) \to S \underset{˙}{\leq} (T \underset{˙}{\lor} V)$

Proof

Step	Hyp	Ref	Expression
1		cdleme23.b	$⊢ B = {Base}_{K}$
2		cdleme23.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
3		cdleme23.j	$⊢ \underset{˙}{\lor} = join (K)$
4		cdleme23.m	$⊢ \underset{˙}{\land} = meet (K)$
5		cdleme23.a	$⊢ A = Atoms (K)$
6		cdleme23.h	$⊢ H = LHyp (K)$
7		cdleme23.v	$⊢ V = (S \underset{˙}{\lor} T) \underset{˙}{\land} (X \underset{˙}{\land} W)$
8		simp11l	$⊢ (((K \in HL \land W \in H) \land (S \in A \land \neg S \underset{˙}{\leq} W) \land (T \in A \land \neg T \underset{˙}{\leq} W)) \land (X \in B \land \neg X \underset{˙}{\leq} W) \land (S \neq T \land S \underset{˙}{\lor} (X \underset{˙}{\land} W) = X \land T \underset{˙}{\lor} (X \underset{˙}{\land} W) = X)) \to K \in HL$
9	8	hllatd	$⊢ (((K \in HL \land W \in H) \land (S \in A \land \neg S \underset{˙}{\leq} W) \land (T \in A \land \neg T \underset{˙}{\leq} W)) \land (X \in B \land \neg X \underset{˙}{\leq} W) \land (S \neq T \land S \underset{˙}{\lor} (X \underset{˙}{\land} W) = X \land T \underset{˙}{\lor} (X \underset{˙}{\land} W) = X)) \to K \in Lat$
10		simp12l	$⊢ (((K \in HL \land W \in H) \land (S \in A \land \neg S \underset{˙}{\leq} W) \land (T \in A \land \neg T \underset{˙}{\leq} W)) \land (X \in B \land \neg X \underset{˙}{\leq} W) \land (S \neq T \land S \underset{˙}{\lor} (X \underset{˙}{\land} W) = X \land T \underset{˙}{\lor} (X \underset{˙}{\land} W) = X)) \to S \in A$
11	1 5	atbase	$⊢ S \in A \to S \in B$
12	10 11	syl	$⊢ (((K \in HL \land W \in H) \land (S \in A \land \neg S \underset{˙}{\leq} W) \land (T \in A \land \neg T \underset{˙}{\leq} W)) \land (X \in B \land \neg X \underset{˙}{\leq} W) \land (S \neq T \land S \underset{˙}{\lor} (X \underset{˙}{\land} W) = X \land T \underset{˙}{\lor} (X \underset{˙}{\land} W) = X)) \to S \in B$
13		simp13l	$⊢ (((K \in HL \land W \in H) \land (S \in A \land \neg S \underset{˙}{\leq} W) \land (T \in A \land \neg T \underset{˙}{\leq} W)) \land (X \in B \land \neg X \underset{˙}{\leq} W) \land (S \neq T \land S \underset{˙}{\lor} (X \underset{˙}{\land} W) = X \land T \underset{˙}{\lor} (X \underset{˙}{\land} W) = X)) \to T \in A$
14	1 5	atbase	$⊢ T \in A \to T \in B$
15	13 14	syl	$⊢ (((K \in HL \land W \in H) \land (S \in A \land \neg S \underset{˙}{\leq} W) \land (T \in A \land \neg T \underset{˙}{\leq} W)) \land (X \in B \land \neg X \underset{˙}{\leq} W) \land (S \neq T \land S \underset{˙}{\lor} (X \underset{˙}{\land} W) = X \land T \underset{˙}{\lor} (X \underset{˙}{\land} W) = X)) \to T \in B$
16	1 2 3	latlej1	$⊢ (K \in Lat \land S \in B \land T \in B) \to S \underset{˙}{\leq} (S \underset{˙}{\lor} T)$
17	9 12 15 16	syl3anc	$⊢ (((K \in HL \land W \in H) \land (S \in A \land \neg S \underset{˙}{\leq} W) \land (T \in A \land \neg T \underset{˙}{\leq} W)) \land (X \in B \land \neg X \underset{˙}{\leq} W) \land (S \neq T \land S \underset{˙}{\lor} (X \underset{˙}{\land} W) = X \land T \underset{˙}{\lor} (X \underset{˙}{\land} W) = X)) \to S \underset{˙}{\leq} (S \underset{˙}{\lor} T)$
18		simp2l	$⊢ (((K \in HL \land W \in H) \land (S \in A \land \neg S \underset{˙}{\leq} W) \land (T \in A \land \neg T \underset{˙}{\leq} W)) \land (X \in B \land \neg X \underset{˙}{\leq} W) \land (S \neq T \land S \underset{˙}{\lor} (X \underset{˙}{\land} W) = X \land T \underset{˙}{\lor} (X \underset{˙}{\land} W) = X)) \to X \in B$
19		simp11r	$⊢ (((K \in HL \land W \in H) \land (S \in A \land \neg S \underset{˙}{\leq} W) \land (T \in A \land \neg T \underset{˙}{\leq} W)) \land (X \in B \land \neg X \underset{˙}{\leq} W) \land (S \neq T \land S \underset{˙}{\lor} (X \underset{˙}{\land} W) = X \land T \underset{˙}{\lor} (X \underset{˙}{\land} W) = X)) \to W \in H$
20	1 6	lhpbase	$⊢ W \in H \to W \in B$
21	19 20	syl	$⊢ (((K \in HL \land W \in H) \land (S \in A \land \neg S \underset{˙}{\leq} W) \land (T \in A \land \neg T \underset{˙}{\leq} W)) \land (X \in B \land \neg X \underset{˙}{\leq} W) \land (S \neq T \land S \underset{˙}{\lor} (X \underset{˙}{\land} W) = X \land T \underset{˙}{\lor} (X \underset{˙}{\land} W) = X)) \to W \in B$
22	1 4	latmcl	$⊢ (K \in Lat \land X \in B \land W \in B) \to X \underset{˙}{\land} W \in B$
23	9 18 21 22	syl3anc	$⊢ (((K \in HL \land W \in H) \land (S \in A \land \neg S \underset{˙}{\leq} W) \land (T \in A \land \neg T \underset{˙}{\leq} W)) \land (X \in B \land \neg X \underset{˙}{\leq} W) \land (S \neq T \land S \underset{˙}{\lor} (X \underset{˙}{\land} W) = X \land T \underset{˙}{\lor} (X \underset{˙}{\land} W) = X)) \to X \underset{˙}{\land} W \in B$
24	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))$
25	9 12 23 24	syl3anc	$⊢ (((K \in HL \land W \in H) \land (S \in A \land \neg S \underset{˙}{\leq} W) \land (T \in A \land \neg T \underset{˙}{\leq} W)) \land (X \in B \land \neg X \underset{˙}{\leq} W) \land (S \neq T \land S \underset{˙}{\lor} (X \underset{˙}{\land} W) = X \land T \underset{˙}{\lor} (X \underset{˙}{\land} W) = X)) \to S \underset{˙}{\leq} (S \underset{˙}{\lor} (X \underset{˙}{\land} W))$
26		simp32	$⊢ (((K \in HL \land W \in H) \land (S \in A \land \neg S \underset{˙}{\leq} W) \land (T \in A \land \neg T \underset{˙}{\leq} W)) \land (X \in B \land \neg X \underset{˙}{\leq} W) \land (S \neq T \land S \underset{˙}{\lor} (X \underset{˙}{\land} W) = X \land T \underset{˙}{\lor} (X \underset{˙}{\land} W) = X)) \to S \underset{˙}{\lor} (X \underset{˙}{\land} W) = X$
27		simp33	$⊢ (((K \in HL \land W \in H) \land (S \in A \land \neg S \underset{˙}{\leq} W) \land (T \in A \land \neg T \underset{˙}{\leq} W)) \land (X \in B \land \neg X \underset{˙}{\leq} W) \land (S \neq T \land S \underset{˙}{\lor} (X \underset{˙}{\land} W) = X \land T \underset{˙}{\lor} (X \underset{˙}{\land} W) = X)) \to T \underset{˙}{\lor} (X \underset{˙}{\land} W) = X$
28	26 27	eqtr4d	$⊢ (((K \in HL \land W \in H) \land (S \in A \land \neg S \underset{˙}{\leq} W) \land (T \in A \land \neg T \underset{˙}{\leq} W)) \land (X \in B \land \neg X \underset{˙}{\leq} W) \land (S \neq T \land S \underset{˙}{\lor} (X \underset{˙}{\land} W) = X \land T \underset{˙}{\lor} (X \underset{˙}{\land} W) = X)) \to S \underset{˙}{\lor} (X \underset{˙}{\land} W) = T \underset{˙}{\lor} (X \underset{˙}{\land} W)$
29	25 28	breqtrd	$⊢ (((K \in HL \land W \in H) \land (S \in A \land \neg S \underset{˙}{\leq} W) \land (T \in A \land \neg T \underset{˙}{\leq} W)) \land (X \in B \land \neg X \underset{˙}{\leq} W) \land (S \neq T \land S \underset{˙}{\lor} (X \underset{˙}{\land} W) = X \land T \underset{˙}{\lor} (X \underset{˙}{\land} W) = X)) \to S \underset{˙}{\leq} (T \underset{˙}{\lor} (X \underset{˙}{\land} W))$
30	1 3 5	hlatjcl	$⊢ (K \in HL \land S \in A \land T \in A) \to S \underset{˙}{\lor} T \in B$
31	8 10 13 30	syl3anc	$⊢ (((K \in HL \land W \in H) \land (S \in A \land \neg S \underset{˙}{\leq} W) \land (T \in A \land \neg T \underset{˙}{\leq} W)) \land (X \in B \land \neg X \underset{˙}{\leq} W) \land (S \neq T \land S \underset{˙}{\lor} (X \underset{˙}{\land} W) = X \land T \underset{˙}{\lor} (X \underset{˙}{\land} W) = X)) \to S \underset{˙}{\lor} T \in B$
32	1 3	latjcl	$⊢ (K \in Lat \land T \in B \land X \underset{˙}{\land} W \in B) \to T \underset{˙}{\lor} (X \underset{˙}{\land} W) \in B$
33	9 15 23 32	syl3anc	$⊢ (((K \in HL \land W \in H) \land (S \in A \land \neg S \underset{˙}{\leq} W) \land (T \in A \land \neg T \underset{˙}{\leq} W)) \land (X \in B \land \neg X \underset{˙}{\leq} W) \land (S \neq T \land S \underset{˙}{\lor} (X \underset{˙}{\land} W) = X \land T \underset{˙}{\lor} (X \underset{˙}{\land} W) = X)) \to T \underset{˙}{\lor} (X \underset{˙}{\land} W) \in B$
34	1 2 4	latlem12	$⊢ (K \in Lat \land (S \in B \land S \underset{˙}{\lor} T \in B \land T \underset{˙}{\lor} (X \underset{˙}{\land} W) \in B)) \to ((S \underset{˙}{\leq} (S \underset{˙}{\lor} T) \land S \underset{˙}{\leq} (T \underset{˙}{\lor} (X \underset{˙}{\land} W))) \leftrightarrow S \underset{˙}{\leq} ((S \underset{˙}{\lor} T) \underset{˙}{\land} (T \underset{˙}{\lor} (X \underset{˙}{\land} W))))$
35	9 12 31 33 34	syl13anc	$⊢ (((K \in HL \land W \in H) \land (S \in A \land \neg S \underset{˙}{\leq} W) \land (T \in A \land \neg T \underset{˙}{\leq} W)) \land (X \in B \land \neg X \underset{˙}{\leq} W) \land (S \neq T \land S \underset{˙}{\lor} (X \underset{˙}{\land} W) = X \land T \underset{˙}{\lor} (X \underset{˙}{\land} W) = X)) \to ((S \underset{˙}{\leq} (S \underset{˙}{\lor} T) \land S \underset{˙}{\leq} (T \underset{˙}{\lor} (X \underset{˙}{\land} W))) \leftrightarrow S \underset{˙}{\leq} ((S \underset{˙}{\lor} T) \underset{˙}{\land} (T \underset{˙}{\lor} (X \underset{˙}{\land} W))))$
36	17 29 35	mpbi2and	$⊢ (((K \in HL \land W \in H) \land (S \in A \land \neg S \underset{˙}{\leq} W) \land (T \in A \land \neg T \underset{˙}{\leq} W)) \land (X \in B \land \neg X \underset{˙}{\leq} W) \land (S \neq T \land S \underset{˙}{\lor} (X \underset{˙}{\land} W) = X \land T \underset{˙}{\lor} (X \underset{˙}{\land} W) = X)) \to S \underset{˙}{\leq} ((S \underset{˙}{\lor} T) \underset{˙}{\land} (T \underset{˙}{\lor} (X \underset{˙}{\land} W)))$
37	7	oveq2i	$⊢ T \underset{˙}{\lor} V = T \underset{˙}{\lor} ((S \underset{˙}{\lor} T) \underset{˙}{\land} (X \underset{˙}{\land} W))$
38	1 2 3	latlej2	$⊢ (K \in Lat \land S \in B \land T \in B) \to T \underset{˙}{\leq} (S \underset{˙}{\lor} T)$
39	9 12 15 38	syl3anc	$⊢ (((K \in HL \land W \in H) \land (S \in A \land \neg S \underset{˙}{\leq} W) \land (T \in A \land \neg T \underset{˙}{\leq} W)) \land (X \in B \land \neg X \underset{˙}{\leq} W) \land (S \neq T \land S \underset{˙}{\lor} (X \underset{˙}{\land} W) = X \land T \underset{˙}{\lor} (X \underset{˙}{\land} W) = X)) \to T \underset{˙}{\leq} (S \underset{˙}{\lor} T)$
40	1 2 3 4 5	atmod3i1	$⊢ (K \in HL \land (T \in A \land S \underset{˙}{\lor} T \in B \land X \underset{˙}{\land} W \in B) \land T \underset{˙}{\leq} (S \underset{˙}{\lor} T)) \to T \underset{˙}{\lor} ((S \underset{˙}{\lor} T) \underset{˙}{\land} (X \underset{˙}{\land} W)) = (S \underset{˙}{\lor} T) \underset{˙}{\land} (T \underset{˙}{\lor} (X \underset{˙}{\land} W))$
41	8 13 31 23 39 40	syl131anc	$⊢ (((K \in HL \land W \in H) \land (S \in A \land \neg S \underset{˙}{\leq} W) \land (T \in A \land \neg T \underset{˙}{\leq} W)) \land (X \in B \land \neg X \underset{˙}{\leq} W) \land (S \neq T \land S \underset{˙}{\lor} (X \underset{˙}{\land} W) = X \land T \underset{˙}{\lor} (X \underset{˙}{\land} W) = X)) \to T \underset{˙}{\lor} ((S \underset{˙}{\lor} T) \underset{˙}{\land} (X \underset{˙}{\land} W)) = (S \underset{˙}{\lor} T) \underset{˙}{\land} (T \underset{˙}{\lor} (X \underset{˙}{\land} W))$
42	37 41	eqtrid	$⊢ (((K \in HL \land W \in H) \land (S \in A \land \neg S \underset{˙}{\leq} W) \land (T \in A \land \neg T \underset{˙}{\leq} W)) \land (X \in B \land \neg X \underset{˙}{\leq} W) \land (S \neq T \land S \underset{˙}{\lor} (X \underset{˙}{\land} W) = X \land T \underset{˙}{\lor} (X \underset{˙}{\land} W) = X)) \to T \underset{˙}{\lor} V = (S \underset{˙}{\lor} T) \underset{˙}{\land} (T \underset{˙}{\lor} (X \underset{˙}{\land} W))$
43	36 42	breqtrrd	$⊢ (((K \in HL \land W \in H) \land (S \in A \land \neg S \underset{˙}{\leq} W) \land (T \in A \land \neg T \underset{˙}{\leq} W)) \land (X \in B \land \neg X \underset{˙}{\leq} W) \land (S \neq T \land S \underset{˙}{\lor} (X \underset{˙}{\land} W) = X \land T \underset{˙}{\lor} (X \underset{˙}{\land} W) = X)) \to S \underset{˙}{\leq} (T \underset{˙}{\lor} V)$

Metamath Proof Explorer

Theorem cdleme23c

Proof