cdleme23a

Description: Part of proof of Lemma E in Crawley p. 113. (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	cdleme23a	$⊢ (((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 \underset{˙}{\leq} W$

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		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$
12	1 3 5	hlatjcl	$⊢ (K \in HL \land S \in A \land T \in A) \to S \underset{˙}{\lor} T \in B$
13	8 10 11 12	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$
14		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$
15		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$
16	1 6	lhpbase	$⊢ W \in H \to W \in B$
17	15 16	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$
18	1 4	latmcl	$⊢ (K \in Lat \land X \in B \land W \in B) \to X \underset{˙}{\land} W \in B$
19	9 14 17 18	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$
20	1 4	latmcl	$⊢ (K \in Lat \land S \underset{˙}{\lor} T \in B \land X \underset{˙}{\land} W \in B) \to (S \underset{˙}{\lor} T) \underset{˙}{\land} (X \underset{˙}{\land} W) \in B$
21	9 13 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 (S \underset{˙}{\lor} T) \underset{˙}{\land} (X \underset{˙}{\land} W) \in B$
22	1 2 4	latmle2	$⊢ (K \in Lat \land S \underset{˙}{\lor} T \in B \land X \underset{˙}{\land} W \in B) \to ((S \underset{˙}{\lor} T) \underset{˙}{\land} (X \underset{˙}{\land} W)) \underset{˙}{\leq} (X \underset{˙}{\land} W)$
23	9 13 19 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{˙}{\land} (X \underset{˙}{\land} W)) \underset{˙}{\leq} (X \underset{˙}{\land} W)$
24	1 2 4	latmle2	$⊢ (K \in Lat \land X \in B \land W \in B) \to (X \underset{˙}{\land} W) \underset{˙}{\leq} W$
25	9 14 17 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 (X \underset{˙}{\land} W) \underset{˙}{\leq} W$
26	1 2 9 21 19 17 23 25	lattrd	$⊢ (((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)) \underset{˙}{\leq} W$
27	7 26	eqbrtrid	$⊢ (((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 \underset{˙}{\leq} W$

Metamath Proof Explorer

Theorem cdleme23a

Proof