cdleme23b

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	cdleme23b	$⊢ (((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 V \in A$

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		hlol	$⊢ K \in HL \to K \in OL$
10	8 9	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 K \in OL$
11		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$
12		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$
13	1 3 5	hlatjcl	$⊢ (K \in HL \land S \in A \land T \in A) \to S \underset{˙}{\lor} T \in B$
14	8 11 12 13	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$
15	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$
16		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$
17		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$
18	1 6	lhpbase	$⊢ W \in H \to W \in B$
19	17 18	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$
20	1 4	latmcl	$⊢ (K \in Lat \land X \in B \land W \in B) \to X \underset{˙}{\land} W \in B$
21	15 16 19 20	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$
22	1 3	latjcl	$⊢ (K \in Lat \land S \underset{˙}{\lor} T \in B \land X \underset{˙}{\land} W \in B) \to (S \underset{˙}{\lor} T) \underset{˙}{\lor} (X \underset{˙}{\land} W) \in B$
23	15 14 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 (S \underset{˙}{\lor} T) \underset{˙}{\lor} (X \underset{˙}{\land} W) \in B$
24	1 4	latmassOLD	$⊢ (K \in OL \land (S \underset{˙}{\lor} T \in B \land (S \underset{˙}{\lor} T) \underset{˙}{\lor} (X \underset{˙}{\land} W) \in B \land W \in B)) \to ((S \underset{˙}{\lor} T) \underset{˙}{\land} ((S \underset{˙}{\lor} T) \underset{˙}{\lor} (X \underset{˙}{\land} W))) \underset{˙}{\land} W = (S \underset{˙}{\lor} T) \underset{˙}{\land} (((S \underset{˙}{\lor} T) \underset{˙}{\lor} (X \underset{˙}{\land} W)) \underset{˙}{\land} W)$
25	10 14 23 19 24	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{˙}{\lor} T) \underset{˙}{\land} ((S \underset{˙}{\lor} T) \underset{˙}{\lor} (X \underset{˙}{\land} W))) \underset{˙}{\land} W = (S \underset{˙}{\lor} T) \underset{˙}{\land} (((S \underset{˙}{\lor} T) \underset{˙}{\lor} (X \underset{˙}{\land} W)) \underset{˙}{\land} W)$
26	1 2 3	latlej1	$⊢ (K \in Lat \land S \underset{˙}{\lor} T \in B \land X \underset{˙}{\land} W \in B) \to (S \underset{˙}{\lor} T) \underset{˙}{\leq} ((S \underset{˙}{\lor} T) \underset{˙}{\lor} (X \underset{˙}{\land} W))$
27	15 14 21 26	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) \underset{˙}{\leq} ((S \underset{˙}{\lor} T) \underset{˙}{\lor} (X \underset{˙}{\land} W))$
28	1 2 4	latleeqm1	$⊢ (K \in Lat \land S \underset{˙}{\lor} T \in B \land (S \underset{˙}{\lor} T) \underset{˙}{\lor} (X \underset{˙}{\land} W) \in B) \to ((S \underset{˙}{\lor} T) \underset{˙}{\leq} ((S \underset{˙}{\lor} T) \underset{˙}{\lor} (X \underset{˙}{\land} W)) \leftrightarrow (S \underset{˙}{\lor} T) \underset{˙}{\land} ((S \underset{˙}{\lor} T) \underset{˙}{\lor} (X \underset{˙}{\land} W)) = S \underset{˙}{\lor} T)$
29	15 14 23 28	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) \underset{˙}{\leq} ((S \underset{˙}{\lor} T) \underset{˙}{\lor} (X \underset{˙}{\land} W)) \leftrightarrow (S \underset{˙}{\lor} T) \underset{˙}{\land} ((S \underset{˙}{\lor} T) \underset{˙}{\lor} (X \underset{˙}{\land} W)) = S \underset{˙}{\lor} T)$
30	27 29	mpbid	$⊢ (((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) \underset{˙}{\land} ((S \underset{˙}{\lor} T) \underset{˙}{\lor} (X \underset{˙}{\land} W)) = S \underset{˙}{\lor} T$
31	30	oveq1d	$⊢ (((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) \underset{˙}{\land} ((S \underset{˙}{\lor} T) \underset{˙}{\lor} (X \underset{˙}{\land} W))) \underset{˙}{\land} W = (S \underset{˙}{\lor} T) \underset{˙}{\land} W$
32	1 5	atbase	$⊢ S \in A \to S \in B$
33	11 32	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$
34	1 5	atbase	$⊢ T \in A \to T \in B$
35	12 34	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$
36	1 3	latjjdir	$⊢ (K \in Lat \land (S \in B \land T \in B \land X \underset{˙}{\land} W \in B)) \to (S \underset{˙}{\lor} T) \underset{˙}{\lor} (X \underset{˙}{\land} W) = (S \underset{˙}{\lor} (X \underset{˙}{\land} W)) \underset{˙}{\lor} (T \underset{˙}{\lor} (X \underset{˙}{\land} W))$
37	15 33 35 21 36	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{˙}{\lor} T) \underset{˙}{\lor} (X \underset{˙}{\land} W) = (S \underset{˙}{\lor} (X \underset{˙}{\land} W)) \underset{˙}{\lor} (T \underset{˙}{\lor} (X \underset{˙}{\land} W))$
38		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$
39		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$
40	38 39	oveq12d	$⊢ (((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)) \underset{˙}{\lor} (T \underset{˙}{\lor} (X \underset{˙}{\land} W)) = X \underset{˙}{\lor} X$
41	1 3	latjidm	$⊢ (K \in Lat \land X \in B) \to X \underset{˙}{\lor} X = X$
42	15 16 41	syl2anc	$⊢ (((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{˙}{\lor} X = X$
43	37 40 42	3eqtrd	$⊢ (((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) \underset{˙}{\lor} (X \underset{˙}{\land} W) = X$
44	43	oveq1d	$⊢ (((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) \underset{˙}{\lor} (X \underset{˙}{\land} W)) \underset{˙}{\land} W = X \underset{˙}{\land} W$
45	44	oveq2d	$⊢ (((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) \underset{˙}{\land} (((S \underset{˙}{\lor} T) \underset{˙}{\lor} (X \underset{˙}{\land} W)) \underset{˙}{\land} W) = (S \underset{˙}{\lor} T) \underset{˙}{\land} (X \underset{˙}{\land} W)$
46	25 31 45	3eqtr3d	$⊢ (((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) \underset{˙}{\land} W = (S \underset{˙}{\lor} T) \underset{˙}{\land} (X \underset{˙}{\land} W)$
47		simp12r	$⊢ (((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 \neg S \underset{˙}{\leq} W$
48		simp31	$⊢ (((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 \neq T$
49	2 3 4 5 6	lhpat	$⊢ ((K \in HL \land W \in H) \land (S \in A \land \neg S \underset{˙}{\leq} W) \land (T \in A \land S \neq T)) \to (S \underset{˙}{\lor} T) \underset{˙}{\land} W \in A$
50	8 17 11 47 12 48 49	syl222anc	$⊢ (((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) \underset{˙}{\land} W \in A$
51	46 50	eqeltrrd	$⊢ (((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) \underset{˙}{\land} (X \underset{˙}{\land} W) \in A$
52	7 51	eqeltrid	$⊢ (((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 V \in A$

Metamath Proof Explorer

Theorem cdleme23b

Proof