cdleme5

Description: Part of proof of Lemma E in Crawley p. 113. G represents f_s(r). We show r \/ f_s(r)) = p \/ q at the top of p. 114. (Contributed by NM, 7-Jun-2012)

	Ref	Expression
Hypotheses	cdleme4.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
	cdleme4.j	$⊢ \underset{˙}{\lor} = join (K)$
	cdleme4.m	$⊢ \underset{˙}{\land} = meet (K)$
	cdleme4.a	$⊢ A = Atoms (K)$
	cdleme4.h	$⊢ H = LHyp (K)$
	cdleme4.u	$⊢ U = (P \underset{˙}{\lor} Q) \underset{˙}{\land} W$
	cdleme4.f	$⊢ F = (S \underset{˙}{\lor} U) \underset{˙}{\land} (Q \underset{˙}{\lor} ((P \underset{˙}{\lor} S) \underset{˙}{\land} W))$
	cdleme4.g	$⊢ G = (P \underset{˙}{\lor} Q) \underset{˙}{\land} (F \underset{˙}{\lor} ((R \underset{˙}{\lor} S) \underset{˙}{\land} W))$
Assertion	cdleme5	$⊢ ((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)) \land ((S \in A \land \neg S \underset{˙}{\leq} W) \land R \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \to R \underset{˙}{\lor} G = P \underset{˙}{\lor} Q$

Proof

Step	Hyp	Ref	Expression
1		cdleme4.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
2		cdleme4.j	$⊢ \underset{˙}{\lor} = join (K)$
3		cdleme4.m	$⊢ \underset{˙}{\land} = meet (K)$
4		cdleme4.a	$⊢ A = Atoms (K)$
5		cdleme4.h	$⊢ H = LHyp (K)$
6		cdleme4.u	$⊢ U = (P \underset{˙}{\lor} Q) \underset{˙}{\land} W$
7		cdleme4.f	$⊢ F = (S \underset{˙}{\lor} U) \underset{˙}{\land} (Q \underset{˙}{\lor} ((P \underset{˙}{\lor} S) \underset{˙}{\land} W))$
8		cdleme4.g	$⊢ G = (P \underset{˙}{\lor} Q) \underset{˙}{\land} (F \underset{˙}{\lor} ((R \underset{˙}{\lor} S) \underset{˙}{\land} W))$
9	8	oveq2i	$⊢ R \underset{˙}{\lor} G = R \underset{˙}{\lor} ((P \underset{˙}{\lor} Q) \underset{˙}{\land} (F \underset{˙}{\lor} ((R \underset{˙}{\lor} S) \underset{˙}{\land} W)))$
10		simp1l	$⊢ ((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)) \land ((S \in A \land \neg S \underset{˙}{\leq} W) \land R \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \to K \in HL$
11		simp23l	$⊢ ((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)) \land ((S \in A \land \neg S \underset{˙}{\leq} W) \land R \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \to R \in A$
12		simp21	$⊢ ((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)) \land ((S \in A \land \neg S \underset{˙}{\leq} W) \land R \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \to P \in A$
13		simp22	$⊢ ((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)) \land ((S \in A \land \neg S \underset{˙}{\leq} W) \land R \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \to Q \in A$
14		eqid	$⊢ {Base}_{K} = {Base}_{K}$
15	14 2 4	hlatjcl	$⊢ (K \in HL \land P \in A \land Q \in A) \to P \underset{˙}{\lor} Q \in {Base}_{K}$
16	10 12 13 15	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)) \land ((S \in A \land \neg S \underset{˙}{\leq} W) \land R \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \to P \underset{˙}{\lor} Q \in {Base}_{K}$
17	10	hllatd	$⊢ ((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)) \land ((S \in A \land \neg S \underset{˙}{\leq} W) \land R \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \to K \in Lat$
18		simp1	$⊢ ((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)) \land ((S \in A \land \neg S \underset{˙}{\leq} W) \land R \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \to (K \in HL \land W \in H)$
19		simp3ll	$⊢ ((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)) \land ((S \in A \land \neg S \underset{˙}{\leq} W) \land R \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \to S \in A$
20	1 2 3 4 5 6 7 14	cdleme1b	$⊢ ((K \in HL \land W \in H) \land (P \in A \land Q \in A \land S \in A)) \to F \in {Base}_{K}$
21	18 12 13 19 20	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)) \land ((S \in A \land \neg S \underset{˙}{\leq} W) \land R \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \to F \in {Base}_{K}$
22	14 2 4	hlatjcl	$⊢ (K \in HL \land R \in A \land S \in A) \to R \underset{˙}{\lor} S \in {Base}_{K}$
23	10 11 19 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)) \land ((S \in A \land \neg S \underset{˙}{\leq} W) \land R \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \to R \underset{˙}{\lor} S \in {Base}_{K}$
24		simp1r	$⊢ ((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)) \land ((S \in A \land \neg S \underset{˙}{\leq} W) \land R \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \to W \in H$
25	14 5	lhpbase	$⊢ W \in H \to W \in {Base}_{K}$
26	24 25	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)) \land ((S \in A \land \neg S \underset{˙}{\leq} W) \land R \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \to W \in {Base}_{K}$
27	14 3	latmcl	$⊢ (K \in Lat \land R \underset{˙}{\lor} S \in {Base}_{K} \land W \in {Base}_{K}) \to (R \underset{˙}{\lor} S) \underset{˙}{\land} W \in {Base}_{K}$
28	17 23 26 27	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)) \land ((S \in A \land \neg S \underset{˙}{\leq} W) \land R \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \to (R \underset{˙}{\lor} S) \underset{˙}{\land} W \in {Base}_{K}$
29	14 2	latjcl	$⊢ (K \in Lat \land F \in {Base}_{K} \land (R \underset{˙}{\lor} S) \underset{˙}{\land} W \in {Base}_{K}) \to F \underset{˙}{\lor} ((R \underset{˙}{\lor} S) \underset{˙}{\land} W) \in {Base}_{K}$
30	17 21 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)) \land ((S \in A \land \neg S \underset{˙}{\leq} W) \land R \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \to F \underset{˙}{\lor} ((R \underset{˙}{\lor} S) \underset{˙}{\land} W) \in {Base}_{K}$
31		simp3r	$⊢ ((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)) \land ((S \in A \land \neg S \underset{˙}{\leq} W) \land R \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \to R \underset{˙}{\leq} (P \underset{˙}{\lor} Q)$
32	14 1 2 3 4	atmod3i1	$⊢ (K \in HL \land (R \in A \land P \underset{˙}{\lor} Q \in {Base}_{K} \land F \underset{˙}{\lor} ((R \underset{˙}{\lor} S) \underset{˙}{\land} W) \in {Base}_{K}) \land R \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \to R \underset{˙}{\lor} ((P \underset{˙}{\lor} Q) \underset{˙}{\land} (F \underset{˙}{\lor} ((R \underset{˙}{\lor} S) \underset{˙}{\land} W))) = (P \underset{˙}{\lor} Q) \underset{˙}{\land} (R \underset{˙}{\lor} (F \underset{˙}{\lor} ((R \underset{˙}{\lor} S) \underset{˙}{\land} W)))$
33	10 11 16 30 31 32	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)) \land ((S \in A \land \neg S \underset{˙}{\leq} W) \land R \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \to R \underset{˙}{\lor} ((P \underset{˙}{\lor} Q) \underset{˙}{\land} (F \underset{˙}{\lor} ((R \underset{˙}{\lor} S) \underset{˙}{\land} W))) = (P \underset{˙}{\lor} Q) \underset{˙}{\land} (R \underset{˙}{\lor} (F \underset{˙}{\lor} ((R \underset{˙}{\lor} S) \underset{˙}{\land} W)))$
34	14 4	atbase	$⊢ S \in A \to S \in {Base}_{K}$
35	19 34	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)) \land ((S \in A \land \neg S \underset{˙}{\leq} W) \land R \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \to S \in {Base}_{K}$
36	14 1 2	latlej2	$⊢ (K \in Lat \land S \in {Base}_{K} \land P \underset{˙}{\lor} Q \in {Base}_{K}) \to (P \underset{˙}{\lor} Q) \underset{˙}{\leq} (S \underset{˙}{\lor} (P \underset{˙}{\lor} Q))$
37	17 35 16 36	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)) \land ((S \in A \land \neg S \underset{˙}{\leq} W) \land R \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \to (P \underset{˙}{\lor} Q) \underset{˙}{\leq} (S \underset{˙}{\lor} (P \underset{˙}{\lor} Q))$
38	14 4	atbase	$⊢ R \in A \to R \in {Base}_{K}$
39	11 38	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)) \land ((S \in A \land \neg S \underset{˙}{\leq} W) \land R \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \to R \in {Base}_{K}$
40	14 2	latj12	$⊢ (K \in Lat \land (R \in {Base}_{K} \land F \in {Base}_{K} \land S \in {Base}_{K})) \to R \underset{˙}{\lor} (F \underset{˙}{\lor} S) = F \underset{˙}{\lor} (R \underset{˙}{\lor} S)$
41	17 39 21 35 40	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)) \land ((S \in A \land \neg S \underset{˙}{\leq} W) \land R \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \to R \underset{˙}{\lor} (F \underset{˙}{\lor} S) = F \underset{˙}{\lor} (R \underset{˙}{\lor} S)$
42	1 2 3 4 5 6 14	cdleme0aa	$⊢ ((K \in HL \land W \in H) \land P \in A \land Q \in A) \to U \in {Base}_{K}$
43	18 12 13 42	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)) \land ((S \in A \land \neg S \underset{˙}{\leq} W) \land R \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \to U \in {Base}_{K}$
44	14 2	latj12	$⊢ (K \in Lat \land (S \in {Base}_{K} \land R \in {Base}_{K} \land U \in {Base}_{K})) \to S \underset{˙}{\lor} (R \underset{˙}{\lor} U) = R \underset{˙}{\lor} (S \underset{˙}{\lor} U)$
45	17 35 39 43 44	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)) \land ((S \in A \land \neg S \underset{˙}{\leq} W) \land R \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \to S \underset{˙}{\lor} (R \underset{˙}{\lor} U) = R \underset{˙}{\lor} (S \underset{˙}{\lor} U)$
46	1 2 3 4 5 6	cdleme4	$⊢ ((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)) \land R \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \to P \underset{˙}{\lor} Q = R \underset{˙}{\lor} U$
47	46	3adant3l	$⊢ ((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)) \land ((S \in A \land \neg S \underset{˙}{\leq} W) \land R \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \to P \underset{˙}{\lor} Q = R \underset{˙}{\lor} U$
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)) \land ((S \in A \land \neg S \underset{˙}{\leq} W) \land R \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \to S \underset{˙}{\lor} (P \underset{˙}{\lor} Q) = S \underset{˙}{\lor} (R \underset{˙}{\lor} U)$
49	14 2	latjcom	$⊢ (K \in Lat \land F \in {Base}_{K} \land S \in {Base}_{K}) \to F \underset{˙}{\lor} S = S \underset{˙}{\lor} F$
50	17 21 35 49	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)) \land ((S \in A \land \neg S \underset{˙}{\leq} W) \land R \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \to F \underset{˙}{\lor} S = S \underset{˙}{\lor} F$
51		simp3l	$⊢ ((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)) \land ((S \in A \land \neg S \underset{˙}{\leq} W) \land R \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \to (S \in A \land \neg S \underset{˙}{\leq} W)$
52	1 2 3 4 5 6 7	cdleme1	$⊢ ((K \in HL \land W \in H) \land (P \in A \land Q \in A \land (S \in A \land \neg S \underset{˙}{\leq} W))) \to S \underset{˙}{\lor} F = S \underset{˙}{\lor} U$
53	18 12 13 51 52	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)) \land ((S \in A \land \neg S \underset{˙}{\leq} W) \land R \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \to S \underset{˙}{\lor} F = S \underset{˙}{\lor} U$
54	50 53	eqtrd	$⊢ ((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)) \land ((S \in A \land \neg S \underset{˙}{\leq} W) \land R \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \to F \underset{˙}{\lor} S = S \underset{˙}{\lor} U$
55	54	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)) \land ((S \in A \land \neg S \underset{˙}{\leq} W) \land R \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \to R \underset{˙}{\lor} (F \underset{˙}{\lor} S) = R \underset{˙}{\lor} (S \underset{˙}{\lor} U)$
56	45 48 55	3eqtr4d	$⊢ ((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)) \land ((S \in A \land \neg S \underset{˙}{\leq} W) \land R \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \to S \underset{˙}{\lor} (P \underset{˙}{\lor} Q) = R \underset{˙}{\lor} (F \underset{˙}{\lor} S)$
57	1 2 4	hlatlej1	$⊢ (K \in HL \land R \in A \land S \in A) \to R \underset{˙}{\leq} (R \underset{˙}{\lor} S)$
58	10 11 19 57	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)) \land ((S \in A \land \neg S \underset{˙}{\leq} W) \land R \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \to R \underset{˙}{\leq} (R \underset{˙}{\lor} S)$
59	14 1 2 3 4	atmod3i1	$⊢ (K \in HL \land (R \in A \land R \underset{˙}{\lor} S \in {Base}_{K} \land W \in {Base}_{K}) \land R \underset{˙}{\leq} (R \underset{˙}{\lor} S)) \to R \underset{˙}{\lor} ((R \underset{˙}{\lor} S) \underset{˙}{\land} W) = (R \underset{˙}{\lor} S) \underset{˙}{\land} (R \underset{˙}{\lor} W)$
60	10 11 23 26 58 59	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)) \land ((S \in A \land \neg S \underset{˙}{\leq} W) \land R \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \to R \underset{˙}{\lor} ((R \underset{˙}{\lor} S) \underset{˙}{\land} W) = (R \underset{˙}{\lor} S) \underset{˙}{\land} (R \underset{˙}{\lor} W)$
61		simp23r	$⊢ ((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)) \land ((S \in A \land \neg S \underset{˙}{\leq} W) \land R \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \to \neg R \underset{˙}{\leq} W$
62		eqid	$⊢ 1. (K) = 1. (K)$
63	1 2 62 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)$
64	18 11 61 63	syl12anc	$⊢ ((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)) \land ((S \in A \land \neg S \underset{˙}{\leq} W) \land R \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \to R \underset{˙}{\lor} W = 1. (K)$
65	64	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)) \land ((S \in A \land \neg S \underset{˙}{\leq} W) \land R \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \to (R \underset{˙}{\lor} S) \underset{˙}{\land} (R \underset{˙}{\lor} W) = (R \underset{˙}{\lor} S) \underset{˙}{\land} 1. (K)$
66		hlol	$⊢ K \in HL \to K \in OL$
67	10 66	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)) \land ((S \in A \land \neg S \underset{˙}{\leq} W) \land R \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \to K \in OL$
68	14 3 62	olm11	$⊢ (K \in OL \land R \underset{˙}{\lor} S \in {Base}_{K}) \to (R \underset{˙}{\lor} S) \underset{˙}{\land} 1. (K) = R \underset{˙}{\lor} S$
69	67 23 68	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)) \land ((S \in A \land \neg S \underset{˙}{\leq} W) \land R \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \to (R \underset{˙}{\lor} S) \underset{˙}{\land} 1. (K) = R \underset{˙}{\lor} S$
70	65 69	eqtrd	$⊢ ((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)) \land ((S \in A \land \neg S \underset{˙}{\leq} W) \land R \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \to (R \underset{˙}{\lor} S) \underset{˙}{\land} (R \underset{˙}{\lor} W) = R \underset{˙}{\lor} S$
71	60 70	eqtrd	$⊢ ((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)) \land ((S \in A \land \neg S \underset{˙}{\leq} W) \land R \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \to R \underset{˙}{\lor} ((R \underset{˙}{\lor} S) \underset{˙}{\land} W) = R \underset{˙}{\lor} S$
72	71	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)) \land ((S \in A \land \neg S \underset{˙}{\leq} W) \land R \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \to F \underset{˙}{\lor} (R \underset{˙}{\lor} ((R \underset{˙}{\lor} S) \underset{˙}{\land} W)) = F \underset{˙}{\lor} (R \underset{˙}{\lor} S)$
73	41 56 72	3eqtr4d	$⊢ ((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)) \land ((S \in A \land \neg S \underset{˙}{\leq} W) \land R \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \to S \underset{˙}{\lor} (P \underset{˙}{\lor} Q) = F \underset{˙}{\lor} (R \underset{˙}{\lor} ((R \underset{˙}{\lor} S) \underset{˙}{\land} W))$
74	14 2	latj12	$⊢ (K \in Lat \land (F \in {Base}_{K} \land R \in {Base}_{K} \land (R \underset{˙}{\lor} S) \underset{˙}{\land} W \in {Base}_{K})) \to F \underset{˙}{\lor} (R \underset{˙}{\lor} ((R \underset{˙}{\lor} S) \underset{˙}{\land} W)) = R \underset{˙}{\lor} (F \underset{˙}{\lor} ((R \underset{˙}{\lor} S) \underset{˙}{\land} W))$
75	17 21 39 28 74	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)) \land ((S \in A \land \neg S \underset{˙}{\leq} W) \land R \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \to F \underset{˙}{\lor} (R \underset{˙}{\lor} ((R \underset{˙}{\lor} S) \underset{˙}{\land} W)) = R \underset{˙}{\lor} (F \underset{˙}{\lor} ((R \underset{˙}{\lor} S) \underset{˙}{\land} W))$
76	73 75	eqtrd	$⊢ ((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)) \land ((S \in A \land \neg S \underset{˙}{\leq} W) \land R \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \to S \underset{˙}{\lor} (P \underset{˙}{\lor} Q) = R \underset{˙}{\lor} (F \underset{˙}{\lor} ((R \underset{˙}{\lor} S) \underset{˙}{\land} W))$
77	37 76	breqtrd	$⊢ ((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)) \land ((S \in A \land \neg S \underset{˙}{\leq} W) \land R \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \to (P \underset{˙}{\lor} Q) \underset{˙}{\leq} (R \underset{˙}{\lor} (F \underset{˙}{\lor} ((R \underset{˙}{\lor} S) \underset{˙}{\land} W)))$
78	14 2	latjcl	$⊢ (K \in Lat \land R \in {Base}_{K} \land F \underset{˙}{\lor} ((R \underset{˙}{\lor} S) \underset{˙}{\land} W) \in {Base}_{K}) \to R \underset{˙}{\lor} (F \underset{˙}{\lor} ((R \underset{˙}{\lor} S) \underset{˙}{\land} W)) \in {Base}_{K}$
79	17 39 30 78	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)) \land ((S \in A \land \neg S \underset{˙}{\leq} W) \land R \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \to R \underset{˙}{\lor} (F \underset{˙}{\lor} ((R \underset{˙}{\lor} S) \underset{˙}{\land} W)) \in {Base}_{K}$
80	14 1 3	latleeqm1	$⊢ (K \in Lat \land P \underset{˙}{\lor} Q \in {Base}_{K} \land R \underset{˙}{\lor} (F \underset{˙}{\lor} ((R \underset{˙}{\lor} S) \underset{˙}{\land} W)) \in {Base}_{K}) \to ((P \underset{˙}{\lor} Q) \underset{˙}{\leq} (R \underset{˙}{\lor} (F \underset{˙}{\lor} ((R \underset{˙}{\lor} S) \underset{˙}{\land} W))) \leftrightarrow (P \underset{˙}{\lor} Q) \underset{˙}{\land} (R \underset{˙}{\lor} (F \underset{˙}{\lor} ((R \underset{˙}{\lor} S) \underset{˙}{\land} W))) = P \underset{˙}{\lor} Q)$
81	17 16 79 80	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)) \land ((S \in A \land \neg S \underset{˙}{\leq} W) \land R \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \to ((P \underset{˙}{\lor} Q) \underset{˙}{\leq} (R \underset{˙}{\lor} (F \underset{˙}{\lor} ((R \underset{˙}{\lor} S) \underset{˙}{\land} W))) \leftrightarrow (P \underset{˙}{\lor} Q) \underset{˙}{\land} (R \underset{˙}{\lor} (F \underset{˙}{\lor} ((R \underset{˙}{\lor} S) \underset{˙}{\land} W))) = P \underset{˙}{\lor} Q)$
82	77 81	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)) \land ((S \in A \land \neg S \underset{˙}{\leq} W) \land R \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \to (P \underset{˙}{\lor} Q) \underset{˙}{\land} (R \underset{˙}{\lor} (F \underset{˙}{\lor} ((R \underset{˙}{\lor} S) \underset{˙}{\land} W))) = P \underset{˙}{\lor} Q$
83	33 82	eqtrd	$⊢ ((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)) \land ((S \in A \land \neg S \underset{˙}{\leq} W) \land R \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \to R \underset{˙}{\lor} ((P \underset{˙}{\lor} Q) \underset{˙}{\land} (F \underset{˙}{\lor} ((R \underset{˙}{\lor} S) \underset{˙}{\land} W))) = P \underset{˙}{\lor} Q$
84	9 83	syl5eq	$⊢ ((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)) \land ((S \in A \land \neg S \underset{˙}{\leq} W) \land R \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \to R \underset{˙}{\lor} G = P \underset{˙}{\lor} Q$

Metamath Proof Explorer

Theorem cdleme5

Proof