cdleme42c

Description: Part of proof of Lemma E in Crawley p. 113. Match -. x .<_ W . (Contributed by NM, 6-Mar-2013)

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

Proof

Step	Hyp	Ref	Expression
1		cdleme42.b	$⊢ B = {Base}_{K}$
2		cdleme42.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
3		cdleme42.j	$⊢ \underset{˙}{\lor} = join (K)$
4		cdleme42.m	$⊢ \underset{˙}{\land} = meet (K)$
5		cdleme42.a	$⊢ A = Atoms (K)$
6		cdleme42.h	$⊢ H = LHyp (K)$
7		cdleme42.v	$⊢ V = (R \underset{˙}{\lor} S) \underset{˙}{\land} W$
8		simp2r	$⊢ ((K \in HL \land W \in H) \land (R \in A \land \neg R \underset{˙}{\leq} W) \land (S \in A \land \neg S \underset{˙}{\leq} W)) \to \neg R \underset{˙}{\leq} W$
9		simp1l	$⊢ ((K \in HL \land W \in H) \land (R \in A \land \neg R \underset{˙}{\leq} W) \land (S \in A \land \neg S \underset{˙}{\leq} W)) \to K \in HL$
10	9	hllatd	$⊢ ((K \in HL \land W \in H) \land (R \in A \land \neg R \underset{˙}{\leq} W) \land (S \in A \land \neg S \underset{˙}{\leq} W)) \to K \in Lat$
11		simp2l	$⊢ ((K \in HL \land W \in H) \land (R \in A \land \neg R \underset{˙}{\leq} W) \land (S \in A \land \neg S \underset{˙}{\leq} W)) \to R \in A$
12	1 5	atbase	$⊢ R \in A \to R \in B$
13	11 12	syl	$⊢ ((K \in HL \land W \in H) \land (R \in A \land \neg R \underset{˙}{\leq} W) \land (S \in A \land \neg S \underset{˙}{\leq} W)) \to R \in B$
14		simp3l	$⊢ ((K \in HL \land W \in H) \land (R \in A \land \neg R \underset{˙}{\leq} W) \land (S \in A \land \neg S \underset{˙}{\leq} W)) \to S \in A$
15	1 3 5	hlatjcl	$⊢ (K \in HL \land R \in A \land S \in A) \to R \underset{˙}{\lor} S \in B$
16	9 11 14 15	syl3anc	$⊢ ((K \in HL \land W \in H) \land (R \in A \land \neg R \underset{˙}{\leq} W) \land (S \in A \land \neg S \underset{˙}{\leq} W)) \to R \underset{˙}{\lor} S \in B$
17		simp1r	$⊢ ((K \in HL \land W \in H) \land (R \in A \land \neg R \underset{˙}{\leq} W) \land (S \in A \land \neg S \underset{˙}{\leq} W)) \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 (R \in A \land \neg R \underset{˙}{\leq} W) \land (S \in A \land \neg S \underset{˙}{\leq} W)) \to W \in B$
20	1 4	latmcl	$⊢ (K \in Lat \land R \underset{˙}{\lor} S \in B \land W \in B) \to (R \underset{˙}{\lor} S) \underset{˙}{\land} W \in B$
21	10 16 19 20	syl3anc	$⊢ ((K \in HL \land W \in H) \land (R \in A \land \neg R \underset{˙}{\leq} W) \land (S \in A \land \neg S \underset{˙}{\leq} W)) \to (R \underset{˙}{\lor} S) \underset{˙}{\land} W \in B$
22	7 21	eqeltrid	$⊢ ((K \in HL \land W \in H) \land (R \in A \land \neg R \underset{˙}{\leq} W) \land (S \in A \land \neg S \underset{˙}{\leq} W)) \to V \in B$
23	1 2 3	latjle12	$⊢ (K \in Lat \land (R \in B \land V \in B \land W \in B)) \to ((R \underset{˙}{\leq} W \land V \underset{˙}{\leq} W) \leftrightarrow (R \underset{˙}{\lor} V) \underset{˙}{\leq} W)$
24	10 13 22 19 23	syl13anc	$⊢ ((K \in HL \land W \in H) \land (R \in A \land \neg R \underset{˙}{\leq} W) \land (S \in A \land \neg S \underset{˙}{\leq} W)) \to ((R \underset{˙}{\leq} W \land V \underset{˙}{\leq} W) \leftrightarrow (R \underset{˙}{\lor} V) \underset{˙}{\leq} W)$
25		simpl	$⊢ (R \underset{˙}{\leq} W \land V \underset{˙}{\leq} W) \to R \underset{˙}{\leq} W$
26	24 25	biimtrrdi	$⊢ ((K \in HL \land W \in H) \land (R \in A \land \neg R \underset{˙}{\leq} W) \land (S \in A \land \neg S \underset{˙}{\leq} W)) \to ((R \underset{˙}{\lor} V) \underset{˙}{\leq} W \to R \underset{˙}{\leq} W)$
27	8 26	mtod	$⊢ ((K \in HL \land W \in H) \land (R \in A \land \neg R \underset{˙}{\leq} W) \land (S \in A \land \neg S \underset{˙}{\leq} W)) \to \neg (R \underset{˙}{\lor} V) \underset{˙}{\leq} W$

Metamath Proof Explorer

Theorem cdleme42c

Proof