cdleme1

Description: Part of proof of Lemma E in Crawley p. 113. F represents their f(r). Here we show r \/ f(r) = r \/ u (7th through 5th lines from bottom on p. 113). (Contributed by NM, 4-Jun-2012)

	Ref	Expression
Hypotheses	cdleme1.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
	cdleme1.j	$⊢ \underset{˙}{\lor} = join (K)$
	cdleme1.m	$⊢ \underset{˙}{\land} = meet (K)$
	cdleme1.a	$⊢ A = Atoms (K)$
	cdleme1.h	$⊢ H = LHyp (K)$
	cdleme1.u	$⊢ U = (P \underset{˙}{\lor} Q) \underset{˙}{\land} W$
	cdleme1.f	$⊢ F = (R \underset{˙}{\lor} U) \underset{˙}{\land} (Q \underset{˙}{\lor} ((P \underset{˙}{\lor} R) \underset{˙}{\land} W))$
Assertion	cdleme1	$⊢ ((K \in HL \land W \in H) \land (P \in A \land Q \in A \land (R \in A \land \neg R \underset{˙}{\leq} W))) \to R \underset{˙}{\lor} F = R \underset{˙}{\lor} U$

Proof

Step	Hyp	Ref	Expression
1		cdleme1.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
2		cdleme1.j	$⊢ \underset{˙}{\lor} = join (K)$
3		cdleme1.m	$⊢ \underset{˙}{\land} = meet (K)$
4		cdleme1.a	$⊢ A = Atoms (K)$
5		cdleme1.h	$⊢ H = LHyp (K)$
6		cdleme1.u	$⊢ U = (P \underset{˙}{\lor} Q) \underset{˙}{\land} W$
7		cdleme1.f	$⊢ F = (R \underset{˙}{\lor} U) \underset{˙}{\land} (Q \underset{˙}{\lor} ((P \underset{˙}{\lor} R) \underset{˙}{\land} W))$
8	7	oveq2i	$⊢ R \underset{˙}{\lor} F = R \underset{˙}{\lor} ((R \underset{˙}{\lor} U) \underset{˙}{\land} (Q \underset{˙}{\lor} ((P \underset{˙}{\lor} R) \underset{˙}{\land} W)))$
9		simpll	$⊢ ((K \in HL \land W \in H) \land (P \in A \land Q \in A \land (R \in A \land \neg R \underset{˙}{\leq} W))) \to K \in HL$
10		simpr3l	$⊢ ((K \in HL \land W \in H) \land (P \in A \land Q \in A \land (R \in A \land \neg R \underset{˙}{\leq} W))) \to R \in A$
11		hllat	$⊢ K \in HL \to K \in Lat$
12	11	ad2antrr	$⊢ ((K \in HL \land W \in H) \land (P \in A \land Q \in A \land (R \in A \land \neg R \underset{˙}{\leq} W))) \to K \in Lat$
13		eqid	$⊢ {Base}_{K} = {Base}_{K}$
14	13 4	atbase	$⊢ R \in A \to R \in {Base}_{K}$
15	10 14	syl	$⊢ ((K \in HL \land W \in H) \land (P \in A \land Q \in A \land (R \in A \land \neg R \underset{˙}{\leq} W))) \to R \in {Base}_{K}$
16		simpr1	$⊢ ((K \in HL \land W \in H) \land (P \in A \land Q \in A \land (R \in A \land \neg R \underset{˙}{\leq} W))) \to P \in A$
17	13 4	atbase	$⊢ P \in A \to P \in {Base}_{K}$
18	16 17	syl	$⊢ ((K \in HL \land W \in H) \land (P \in A \land Q \in A \land (R \in A \land \neg R \underset{˙}{\leq} W))) \to P \in {Base}_{K}$
19		simpr2	$⊢ ((K \in HL \land W \in H) \land (P \in A \land Q \in A \land (R \in A \land \neg R \underset{˙}{\leq} W))) \to Q \in A$
20	13 4	atbase	$⊢ Q \in A \to Q \in {Base}_{K}$
21	19 20	syl	$⊢ ((K \in HL \land W \in H) \land (P \in A \land Q \in A \land (R \in A \land \neg R \underset{˙}{\leq} W))) \to Q \in {Base}_{K}$
22	13 2	latjcl	$⊢ (K \in Lat \land P \in {Base}_{K} \land Q \in {Base}_{K}) \to P \underset{˙}{\lor} Q \in {Base}_{K}$
23	12 18 21 22	syl3anc	$⊢ ((K \in HL \land W \in H) \land (P \in A \land Q \in A \land (R \in A \land \neg R \underset{˙}{\leq} W))) \to P \underset{˙}{\lor} Q \in {Base}_{K}$
24	13 5	lhpbase	$⊢ W \in H \to W \in {Base}_{K}$
25	24	ad2antlr	$⊢ ((K \in HL \land W \in H) \land (P \in A \land Q \in A \land (R \in A \land \neg R \underset{˙}{\leq} W))) \to W \in {Base}_{K}$
26	13 3	latmcl	$⊢ (K \in Lat \land P \underset{˙}{\lor} Q \in {Base}_{K} \land W \in {Base}_{K}) \to (P \underset{˙}{\lor} Q) \underset{˙}{\land} W \in {Base}_{K}$
27	12 23 25 26	syl3anc	$⊢ ((K \in HL \land W \in H) \land (P \in A \land Q \in A \land (R \in A \land \neg R \underset{˙}{\leq} W))) \to (P \underset{˙}{\lor} Q) \underset{˙}{\land} W \in {Base}_{K}$
28	6 27	eqeltrid	$⊢ ((K \in HL \land W \in H) \land (P \in A \land Q \in A \land (R \in A \land \neg R \underset{˙}{\leq} W))) \to U \in {Base}_{K}$
29	13 2	latjcl	$⊢ (K \in Lat \land R \in {Base}_{K} \land U \in {Base}_{K}) \to R \underset{˙}{\lor} U \in {Base}_{K}$
30	12 15 28 29	syl3anc	$⊢ ((K \in HL \land W \in H) \land (P \in A \land Q \in A \land (R \in A \land \neg R \underset{˙}{\leq} W))) \to R \underset{˙}{\lor} U \in {Base}_{K}$
31	13 2	latjcl	$⊢ (K \in Lat \land P \in {Base}_{K} \land R \in {Base}_{K}) \to P \underset{˙}{\lor} R \in {Base}_{K}$
32	12 18 15 31	syl3anc	$⊢ ((K \in HL \land W \in H) \land (P \in A \land Q \in A \land (R \in A \land \neg R \underset{˙}{\leq} W))) \to P \underset{˙}{\lor} R \in {Base}_{K}$
33	13 3	latmcl	$⊢ (K \in Lat \land P \underset{˙}{\lor} R \in {Base}_{K} \land W \in {Base}_{K}) \to (P \underset{˙}{\lor} R) \underset{˙}{\land} W \in {Base}_{K}$
34	12 32 25 33	syl3anc	$⊢ ((K \in HL \land W \in H) \land (P \in A \land Q \in A \land (R \in A \land \neg R \underset{˙}{\leq} W))) \to (P \underset{˙}{\lor} R) \underset{˙}{\land} W \in {Base}_{K}$
35	13 2	latjcl	$⊢ (K \in Lat \land Q \in {Base}_{K} \land (P \underset{˙}{\lor} R) \underset{˙}{\land} W \in {Base}_{K}) \to Q \underset{˙}{\lor} ((P \underset{˙}{\lor} R) \underset{˙}{\land} W) \in {Base}_{K}$
36	12 21 34 35	syl3anc	$⊢ ((K \in HL \land W \in H) \land (P \in A \land Q \in A \land (R \in A \land \neg R \underset{˙}{\leq} W))) \to Q \underset{˙}{\lor} ((P \underset{˙}{\lor} R) \underset{˙}{\land} W) \in {Base}_{K}$
37	13 1 2	latlej1	$⊢ (K \in Lat \land R \in {Base}_{K} \land U \in {Base}_{K}) \to R \underset{˙}{\leq} (R \underset{˙}{\lor} U)$
38	12 15 28 37	syl3anc	$⊢ ((K \in HL \land W \in H) \land (P \in A \land Q \in A \land (R \in A \land \neg R \underset{˙}{\leq} W))) \to R \underset{˙}{\leq} (R \underset{˙}{\lor} U)$
39	13 1 2 3 4	atmod3i1	$⊢ (K \in HL \land (R \in A \land R \underset{˙}{\lor} U \in {Base}_{K} \land Q \underset{˙}{\lor} ((P \underset{˙}{\lor} R) \underset{˙}{\land} W) \in {Base}_{K}) \land R \underset{˙}{\leq} (R \underset{˙}{\lor} U)) \to R \underset{˙}{\lor} ((R \underset{˙}{\lor} U) \underset{˙}{\land} (Q \underset{˙}{\lor} ((P \underset{˙}{\lor} R) \underset{˙}{\land} W))) = (R \underset{˙}{\lor} U) \underset{˙}{\land} (R \underset{˙}{\lor} (Q \underset{˙}{\lor} ((P \underset{˙}{\lor} R) \underset{˙}{\land} W)))$
40	9 10 30 36 38 39	syl131anc	$⊢ ((K \in HL \land W \in H) \land (P \in A \land Q \in A \land (R \in A \land \neg R \underset{˙}{\leq} W))) \to R \underset{˙}{\lor} ((R \underset{˙}{\lor} U) \underset{˙}{\land} (Q \underset{˙}{\lor} ((P \underset{˙}{\lor} R) \underset{˙}{\land} W))) = (R \underset{˙}{\lor} U) \underset{˙}{\land} (R \underset{˙}{\lor} (Q \underset{˙}{\lor} ((P \underset{˙}{\lor} R) \underset{˙}{\land} W)))$
41	13 1 2	latlej2	$⊢ (K \in Lat \land P \in {Base}_{K} \land R \in {Base}_{K}) \to R \underset{˙}{\leq} (P \underset{˙}{\lor} R)$
42	12 18 15 41	syl3anc	$⊢ ((K \in HL \land W \in H) \land (P \in A \land Q \in A \land (R \in A \land \neg R \underset{˙}{\leq} W))) \to R \underset{˙}{\leq} (P \underset{˙}{\lor} R)$
43	13 1 2 3 4	atmod3i1	$⊢ (K \in HL \land (R \in A \land P \underset{˙}{\lor} R \in {Base}_{K} \land W \in {Base}_{K}) \land R \underset{˙}{\leq} (P \underset{˙}{\lor} R)) \to R \underset{˙}{\lor} ((P \underset{˙}{\lor} R) \underset{˙}{\land} W) = (P \underset{˙}{\lor} R) \underset{˙}{\land} (R \underset{˙}{\lor} W)$
44	9 10 32 25 42 43	syl131anc	$⊢ ((K \in HL \land W \in H) \land (P \in A \land Q \in A \land (R \in A \land \neg R \underset{˙}{\leq} W))) \to R \underset{˙}{\lor} ((P \underset{˙}{\lor} R) \underset{˙}{\land} W) = (P \underset{˙}{\lor} R) \underset{˙}{\land} (R \underset{˙}{\lor} W)$
45		eqid	$⊢ 1. (K) = 1. (K)$
46	1 2 45 4 5	lhpjat2	$⊢ ((K \in HL \land W \in H) \land (R \in A \land \neg R \underset{˙}{\leq} W)) \to R \underset{˙}{\lor} W = 1. (K)$
47	46	3ad2antr3	$⊢ ((K \in HL \land W \in H) \land (P \in A \land Q \in A \land (R \in A \land \neg R \underset{˙}{\leq} W))) \to R \underset{˙}{\lor} W = 1. (K)$
48	47	oveq2d	$⊢ ((K \in HL \land W \in H) \land (P \in A \land Q \in A \land (R \in A \land \neg R \underset{˙}{\leq} W))) \to (P \underset{˙}{\lor} R) \underset{˙}{\land} (R \underset{˙}{\lor} W) = (P \underset{˙}{\lor} R) \underset{˙}{\land} 1. (K)$
49		hlol	$⊢ K \in HL \to K \in OL$
50	49	ad2antrr	$⊢ ((K \in HL \land W \in H) \land (P \in A \land Q \in A \land (R \in A \land \neg R \underset{˙}{\leq} W))) \to K \in OL$
51	13 3 45	olm11	$⊢ (K \in OL \land P \underset{˙}{\lor} R \in {Base}_{K}) \to (P \underset{˙}{\lor} R) \underset{˙}{\land} 1. (K) = P \underset{˙}{\lor} R$
52	50 32 51	syl2anc	$⊢ ((K \in HL \land W \in H) \land (P \in A \land Q \in A \land (R \in A \land \neg R \underset{˙}{\leq} W))) \to (P \underset{˙}{\lor} R) \underset{˙}{\land} 1. (K) = P \underset{˙}{\lor} R$
53	44 48 52	3eqtrd	$⊢ ((K \in HL \land W \in H) \land (P \in A \land Q \in A \land (R \in A \land \neg R \underset{˙}{\leq} W))) \to R \underset{˙}{\lor} ((P \underset{˙}{\lor} R) \underset{˙}{\land} W) = P \underset{˙}{\lor} R$
54	53	oveq2d	$⊢ ((K \in HL \land W \in H) \land (P \in A \land Q \in A \land (R \in A \land \neg R \underset{˙}{\leq} W))) \to Q \underset{˙}{\lor} (R \underset{˙}{\lor} ((P \underset{˙}{\lor} R) \underset{˙}{\land} W)) = Q \underset{˙}{\lor} (P \underset{˙}{\lor} R)$
55	13 2	latj12	$⊢ (K \in Lat \land (Q \in {Base}_{K} \land R \in {Base}_{K} \land (P \underset{˙}{\lor} R) \underset{˙}{\land} W \in {Base}_{K})) \to Q \underset{˙}{\lor} (R \underset{˙}{\lor} ((P \underset{˙}{\lor} R) \underset{˙}{\land} W)) = R \underset{˙}{\lor} (Q \underset{˙}{\lor} ((P \underset{˙}{\lor} R) \underset{˙}{\land} W))$
56	12 21 15 34 55	syl13anc	$⊢ ((K \in HL \land W \in H) \land (P \in A \land Q \in A \land (R \in A \land \neg R \underset{˙}{\leq} W))) \to Q \underset{˙}{\lor} (R \underset{˙}{\lor} ((P \underset{˙}{\lor} R) \underset{˙}{\land} W)) = R \underset{˙}{\lor} (Q \underset{˙}{\lor} ((P \underset{˙}{\lor} R) \underset{˙}{\land} W))$
57	13 2	latj13	$⊢ (K \in Lat \land (Q \in {Base}_{K} \land P \in {Base}_{K} \land R \in {Base}_{K})) \to Q \underset{˙}{\lor} (P \underset{˙}{\lor} R) = R \underset{˙}{\lor} (P \underset{˙}{\lor} Q)$
58	12 21 18 15 57	syl13anc	$⊢ ((K \in HL \land W \in H) \land (P \in A \land Q \in A \land (R \in A \land \neg R \underset{˙}{\leq} W))) \to Q \underset{˙}{\lor} (P \underset{˙}{\lor} R) = R \underset{˙}{\lor} (P \underset{˙}{\lor} Q)$
59	54 56 58	3eqtr3rd	$⊢ ((K \in HL \land W \in H) \land (P \in A \land Q \in A \land (R \in A \land \neg R \underset{˙}{\leq} W))) \to R \underset{˙}{\lor} (P \underset{˙}{\lor} Q) = R \underset{˙}{\lor} (Q \underset{˙}{\lor} ((P \underset{˙}{\lor} R) \underset{˙}{\land} W))$
60	59	oveq2d	$⊢ ((K \in HL \land W \in H) \land (P \in A \land Q \in A \land (R \in A \land \neg R \underset{˙}{\leq} W))) \to (R \underset{˙}{\lor} U) \underset{˙}{\land} (R \underset{˙}{\lor} (P \underset{˙}{\lor} Q)) = (R \underset{˙}{\lor} U) \underset{˙}{\land} (R \underset{˙}{\lor} (Q \underset{˙}{\lor} ((P \underset{˙}{\lor} R) \underset{˙}{\land} W)))$
61	1 2 3 4 5 6	cdlemeulpq	$⊢ ((K \in HL \land W \in H) \land (P \in A \land Q \in A)) \to U \underset{˙}{\leq} (P \underset{˙}{\lor} Q)$
62	61	3adantr3	$⊢ ((K \in HL \land W \in H) \land (P \in A \land Q \in A \land (R \in A \land \neg R \underset{˙}{\leq} W))) \to U \underset{˙}{\leq} (P \underset{˙}{\lor} Q)$
63	13 1 2	latjlej2	$⊢ (K \in Lat \land (U \in {Base}_{K} \land P \underset{˙}{\lor} Q \in {Base}_{K} \land R \in {Base}_{K})) \to (U \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \to (R \underset{˙}{\lor} U) \underset{˙}{\leq} (R \underset{˙}{\lor} (P \underset{˙}{\lor} Q)))$
64	12 28 23 15 63	syl13anc	$⊢ ((K \in HL \land W \in H) \land (P \in A \land Q \in A \land (R \in A \land \neg R \underset{˙}{\leq} W))) \to (U \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \to (R \underset{˙}{\lor} U) \underset{˙}{\leq} (R \underset{˙}{\lor} (P \underset{˙}{\lor} Q)))$
65	62 64	mpd	$⊢ ((K \in HL \land W \in H) \land (P \in A \land Q \in A \land (R \in A \land \neg R \underset{˙}{\leq} W))) \to (R \underset{˙}{\lor} U) \underset{˙}{\leq} (R \underset{˙}{\lor} (P \underset{˙}{\lor} Q))$
66	13 2	latjcl	$⊢ (K \in Lat \land R \in {Base}_{K} \land P \underset{˙}{\lor} Q \in {Base}_{K}) \to R \underset{˙}{\lor} (P \underset{˙}{\lor} Q) \in {Base}_{K}$
67	12 15 23 66	syl3anc	$⊢ ((K \in HL \land W \in H) \land (P \in A \land Q \in A \land (R \in A \land \neg R \underset{˙}{\leq} W))) \to R \underset{˙}{\lor} (P \underset{˙}{\lor} Q) \in {Base}_{K}$
68	13 1 3	latleeqm1	$⊢ (K \in Lat \land R \underset{˙}{\lor} U \in {Base}_{K} \land R \underset{˙}{\lor} (P \underset{˙}{\lor} Q) \in {Base}_{K}) \to ((R \underset{˙}{\lor} U) \underset{˙}{\leq} (R \underset{˙}{\lor} (P \underset{˙}{\lor} Q)) \leftrightarrow (R \underset{˙}{\lor} U) \underset{˙}{\land} (R \underset{˙}{\lor} (P \underset{˙}{\lor} Q)) = R \underset{˙}{\lor} U)$
69	12 30 67 68	syl3anc	$⊢ ((K \in HL \land W \in H) \land (P \in A \land Q \in A \land (R \in A \land \neg R \underset{˙}{\leq} W))) \to ((R \underset{˙}{\lor} U) \underset{˙}{\leq} (R \underset{˙}{\lor} (P \underset{˙}{\lor} Q)) \leftrightarrow (R \underset{˙}{\lor} U) \underset{˙}{\land} (R \underset{˙}{\lor} (P \underset{˙}{\lor} Q)) = R \underset{˙}{\lor} U)$
70	65 69	mpbid	$⊢ ((K \in HL \land W \in H) \land (P \in A \land Q \in A \land (R \in A \land \neg R \underset{˙}{\leq} W))) \to (R \underset{˙}{\lor} U) \underset{˙}{\land} (R \underset{˙}{\lor} (P \underset{˙}{\lor} Q)) = R \underset{˙}{\lor} U$
71	40 60 70	3eqtr2rd	$⊢ ((K \in HL \land W \in H) \land (P \in A \land Q \in A \land (R \in A \land \neg R \underset{˙}{\leq} W))) \to R \underset{˙}{\lor} U = R \underset{˙}{\lor} ((R \underset{˙}{\lor} U) \underset{˙}{\land} (Q \underset{˙}{\lor} ((P \underset{˙}{\lor} R) \underset{˙}{\land} W)))$
72	8 71	eqtr4id	$⊢ ((K \in HL \land W \in H) \land (P \in A \land Q \in A \land (R \in A \land \neg R \underset{˙}{\leq} W))) \to R \underset{˙}{\lor} F = R \underset{˙}{\lor} U$

Metamath Proof Explorer

Theorem cdleme1

Proof