cdleme10

Description: Part of proof of Lemma E in Crawley p. 113, 2nd paragraph on p. 114. D represents s_2. In their notation, we prove s \/ s_2 = s \/ r. (Contributed by NM, 9-Jun-2012)

	Ref	Expression
Hypotheses	cdleme10.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
	cdleme10.j	$⊢ \underset{˙}{\lor} = join (K)$
	cdleme10.m	$⊢ \underset{˙}{\land} = meet (K)$
	cdleme10.a	$⊢ A = Atoms (K)$
	cdleme10.h	$⊢ H = LHyp (K)$
	cdleme10.d	$⊢ D = (R \underset{˙}{\lor} S) \underset{˙}{\land} W$
Assertion	cdleme10	$⊢ ((K \in HL \land W \in H) \land R \in A \land (S \in A \land \neg S \underset{˙}{\leq} W)) \to S \underset{˙}{\lor} D = S \underset{˙}{\lor} R$

Proof

Step	Hyp	Ref	Expression
1		cdleme10.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
2		cdleme10.j	$⊢ \underset{˙}{\lor} = join (K)$
3		cdleme10.m	$⊢ \underset{˙}{\land} = meet (K)$
4		cdleme10.a	$⊢ A = Atoms (K)$
5		cdleme10.h	$⊢ H = LHyp (K)$
6		cdleme10.d	$⊢ D = (R \underset{˙}{\lor} S) \underset{˙}{\land} W$
7	6	oveq2i	$⊢ S \underset{˙}{\lor} D = S \underset{˙}{\lor} ((R \underset{˙}{\lor} S) \underset{˙}{\land} W)$
8		simp1l	$⊢ ((K \in HL \land W \in H) \land R \in A \land (S \in A \land \neg S \underset{˙}{\leq} W)) \to K \in HL$
9		simp3l	$⊢ ((K \in HL \land W \in H) \land R \in A \land (S \in A \land \neg S \underset{˙}{\leq} W)) \to S \in A$
10		simp2	$⊢ ((K \in HL \land W \in H) \land R \in A \land (S \in A \land \neg S \underset{˙}{\leq} W)) \to R \in A$
11		eqid	$⊢ {Base}_{K} = {Base}_{K}$
12	11 2 4	hlatjcl	$⊢ (K \in HL \land R \in A \land S \in A) \to R \underset{˙}{\lor} S \in {Base}_{K}$
13	8 10 9 12	syl3anc	$⊢ ((K \in HL \land W \in H) \land R \in A \land (S \in A \land \neg S \underset{˙}{\leq} W)) \to R \underset{˙}{\lor} S \in {Base}_{K}$
14		simp1r	$⊢ ((K \in HL \land W \in H) \land R \in A \land (S \in A \land \neg S \underset{˙}{\leq} W)) \to W \in H$
15	11 5	lhpbase	$⊢ W \in H \to W \in {Base}_{K}$
16	14 15	syl	$⊢ ((K \in HL \land W \in H) \land R \in A \land (S \in A \land \neg S \underset{˙}{\leq} W)) \to W \in {Base}_{K}$
17	8	hllatd	$⊢ ((K \in HL \land W \in H) \land R \in A \land (S \in A \land \neg S \underset{˙}{\leq} W)) \to K \in Lat$
18	11 4	atbase	$⊢ R \in A \to R \in {Base}_{K}$
19	18	3ad2ant2	$⊢ ((K \in HL \land W \in H) \land R \in A \land (S \in A \land \neg S \underset{˙}{\leq} W)) \to R \in {Base}_{K}$
20	11 4	atbase	$⊢ S \in A \to S \in {Base}_{K}$
21	9 20	syl	$⊢ ((K \in HL \land W \in H) \land R \in A \land (S \in A \land \neg S \underset{˙}{\leq} W)) \to S \in {Base}_{K}$
22	11 1 2	latlej2	$⊢ (K \in Lat \land R \in {Base}_{K} \land S \in {Base}_{K}) \to S \underset{˙}{\leq} (R \underset{˙}{\lor} S)$
23	17 19 21 22	syl3anc	$⊢ ((K \in HL \land W \in H) \land R \in A \land (S \in A \land \neg S \underset{˙}{\leq} W)) \to S \underset{˙}{\leq} (R \underset{˙}{\lor} S)$
24	11 1 2 3 4	atmod3i1	$⊢ (K \in HL \land (S \in A \land R \underset{˙}{\lor} S \in {Base}_{K} \land W \in {Base}_{K}) \land S \underset{˙}{\leq} (R \underset{˙}{\lor} S)) \to S \underset{˙}{\lor} ((R \underset{˙}{\lor} S) \underset{˙}{\land} W) = (R \underset{˙}{\lor} S) \underset{˙}{\land} (S \underset{˙}{\lor} W)$
25	8 9 13 16 23 24	syl131anc	$⊢ ((K \in HL \land W \in H) \land R \in A \land (S \in A \land \neg S \underset{˙}{\leq} W)) \to S \underset{˙}{\lor} ((R \underset{˙}{\lor} S) \underset{˙}{\land} W) = (R \underset{˙}{\lor} S) \underset{˙}{\land} (S \underset{˙}{\lor} W)$
26	11 2	latjcom	$⊢ (K \in Lat \land R \in {Base}_{K} \land S \in {Base}_{K}) \to R \underset{˙}{\lor} S = S \underset{˙}{\lor} R$
27	17 19 21 26	syl3anc	$⊢ ((K \in HL \land W \in H) \land R \in A \land (S \in A \land \neg S \underset{˙}{\leq} W)) \to R \underset{˙}{\lor} S = S \underset{˙}{\lor} R$
28		eqid	$⊢ 1. (K) = 1. (K)$
29	1 2 28 4 5	lhpjat2	$⊢ ((K \in HL \land W \in H) \land (S \in A \land \neg S \underset{˙}{\leq} W)) \to S \underset{˙}{\lor} W = 1. (K)$
30	29	3adant2	$⊢ ((K \in HL \land W \in H) \land R \in A \land (S \in A \land \neg S \underset{˙}{\leq} W)) \to S \underset{˙}{\lor} W = 1. (K)$
31	27 30	oveq12d	$⊢ ((K \in HL \land W \in H) \land R \in A \land (S \in A \land \neg S \underset{˙}{\leq} W)) \to (R \underset{˙}{\lor} S) \underset{˙}{\land} (S \underset{˙}{\lor} W) = (S \underset{˙}{\lor} R) \underset{˙}{\land} 1. (K)$
32		hlol	$⊢ K \in HL \to K \in OL$
33	8 32	syl	$⊢ ((K \in HL \land W \in H) \land R \in A \land (S \in A \land \neg S \underset{˙}{\leq} W)) \to K \in OL$
34	11 2	latjcl	$⊢ (K \in Lat \land S \in {Base}_{K} \land R \in {Base}_{K}) \to S \underset{˙}{\lor} R \in {Base}_{K}$
35	17 21 19 34	syl3anc	$⊢ ((K \in HL \land W \in H) \land R \in A \land (S \in A \land \neg S \underset{˙}{\leq} W)) \to S \underset{˙}{\lor} R \in {Base}_{K}$
36	11 3 28	olm11	$⊢ (K \in OL \land S \underset{˙}{\lor} R \in {Base}_{K}) \to (S \underset{˙}{\lor} R) \underset{˙}{\land} 1. (K) = S \underset{˙}{\lor} R$
37	33 35 36	syl2anc	$⊢ ((K \in HL \land W \in H) \land R \in A \land (S \in A \land \neg S \underset{˙}{\leq} W)) \to (S \underset{˙}{\lor} R) \underset{˙}{\land} 1. (K) = S \underset{˙}{\lor} R$
38	25 31 37	3eqtrd	$⊢ ((K \in HL \land W \in H) \land R \in A \land (S \in A \land \neg S \underset{˙}{\leq} W)) \to S \underset{˙}{\lor} ((R \underset{˙}{\lor} S) \underset{˙}{\land} W) = S \underset{˙}{\lor} R$
39	7 38	eqtrid	$⊢ ((K \in HL \land W \in H) \land R \in A \land (S \in A \land \neg S \underset{˙}{\leq} W)) \to S \underset{˙}{\lor} D = S \underset{˙}{\lor} R$

Metamath Proof Explorer

Theorem cdleme10

Proof