cdleme9

Description: Part of proof of Lemma E in Crawley p. 113, 2nd paragraph on p. 114. C and F represent s_1 and f(s) respectively. In their notation, we prove f(s) \/ s_1 = q \/ s_1. (Contributed by NM, 10-Jun-2012)

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

Proof

Step	Hyp	Ref	Expression
1		cdleme9.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
2		cdleme9.j	$⊢ \underset{˙}{\lor} = join (K)$
3		cdleme9.m	$⊢ \underset{˙}{\land} = meet (K)$
4		cdleme9.a	$⊢ A = Atoms (K)$
5		cdleme9.h	$⊢ H = LHyp (K)$
6		cdleme9.u	$⊢ U = (P \underset{˙}{\lor} Q) \underset{˙}{\land} W$
7		cdleme9.f	$⊢ F = (S \underset{˙}{\lor} U) \underset{˙}{\land} (Q \underset{˙}{\lor} ((P \underset{˙}{\lor} S) \underset{˙}{\land} W))$
8		cdleme9.c	$⊢ C = (P \underset{˙}{\lor} S) \underset{˙}{\land} W$
9	1 2 3 4 5 6 7 8	cdleme3d	$⊢ F = (S \underset{˙}{\lor} U) \underset{˙}{\land} (Q \underset{˙}{\lor} C)$
10	9	oveq1i	$⊢ F \underset{˙}{\lor} C = ((S \underset{˙}{\lor} U) \underset{˙}{\land} (Q \underset{˙}{\lor} C)) \underset{˙}{\lor} C$
11		simp1l	$⊢ ((K \in HL \land W \in H) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land Q \in A \land (S \in A \land \neg S \underset{˙}{\leq} W)) \land \neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \to K \in HL$
12		simp1	$⊢ ((K \in HL \land W \in H) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land Q \in A \land (S \in A \land \neg S \underset{˙}{\leq} W)) \land \neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \to (K \in HL \land W \in H)$
13		simp21	$⊢ ((K \in HL \land W \in H) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land Q \in A \land (S \in A \land \neg S \underset{˙}{\leq} W)) \land \neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \to (P \in A \land \neg P \underset{˙}{\leq} W)$
14		simp23l	$⊢ ((K \in HL \land W \in H) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land Q \in A \land (S \in A \land \neg S \underset{˙}{\leq} W)) \land \neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \to S \in A$
15	11	hllatd	$⊢ ((K \in HL \land W \in H) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land Q \in A \land (S \in A \land \neg S \underset{˙}{\leq} W)) \land \neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \to K \in Lat$
16		eqid	$⊢ {Base}_{K} = {Base}_{K}$
17	16 4	atbase	$⊢ S \in A \to S \in {Base}_{K}$
18	14 17	syl	$⊢ ((K \in HL \land W \in H) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land Q \in A \land (S \in A \land \neg S \underset{˙}{\leq} W)) \land \neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \to S \in {Base}_{K}$
19		simp21l	$⊢ ((K \in HL \land W \in H) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land Q \in A \land (S \in A \land \neg S \underset{˙}{\leq} W)) \land \neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \to P \in A$
20	16 4	atbase	$⊢ P \in A \to P \in {Base}_{K}$
21	19 20	syl	$⊢ ((K \in HL \land W \in H) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land Q \in A \land (S \in A \land \neg S \underset{˙}{\leq} W)) \land \neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \to P \in {Base}_{K}$
22		simp22	$⊢ ((K \in HL \land W \in H) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land Q \in A \land (S \in A \land \neg S \underset{˙}{\leq} W)) \land \neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \to Q \in A$
23	16 4	atbase	$⊢ Q \in A \to Q \in {Base}_{K}$
24	22 23	syl	$⊢ ((K \in HL \land W \in H) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land Q \in A \land (S \in A \land \neg S \underset{˙}{\leq} W)) \land \neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \to Q \in {Base}_{K}$
25		simp3	$⊢ ((K \in HL \land W \in H) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land Q \in A \land (S \in A \land \neg S \underset{˙}{\leq} W)) \land \neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \to \neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q)$
26	16 1 2	latnlej1l	$⊢ (K \in Lat \land (S \in {Base}_{K} \land P \in {Base}_{K} \land Q \in {Base}_{K}) \land \neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \to S \neq P$
27	26	necomd	$⊢ (K \in Lat \land (S \in {Base}_{K} \land P \in {Base}_{K} \land Q \in {Base}_{K}) \land \neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \to P \neq S$
28	15 18 21 24 25 27	syl131anc	$⊢ ((K \in HL \land W \in H) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land Q \in A \land (S \in A \land \neg S \underset{˙}{\leq} W)) \land \neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \to P \neq S$
29	1 2 3 4 5 8	cdleme9a	$⊢ ((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (S \in A \land P \neq S)) \to C \in A$
30	12 13 14 28 29	syl112anc	$⊢ ((K \in HL \land W \in H) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land Q \in A \land (S \in A \land \neg S \underset{˙}{\leq} W)) \land \neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \to C \in A$
31	1 2 3 4 5 6 16	cdleme0aa	$⊢ ((K \in HL \land W \in H) \land P \in A \land Q \in A) \to U \in {Base}_{K}$
32	12 19 22 31	syl3anc	$⊢ ((K \in HL \land W \in H) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land Q \in A \land (S \in A \land \neg S \underset{˙}{\leq} W)) \land \neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \to U \in {Base}_{K}$
33	16 2	latjcl	$⊢ (K \in Lat \land S \in {Base}_{K} \land U \in {Base}_{K}) \to S \underset{˙}{\lor} U \in {Base}_{K}$
34	15 18 32 33	syl3anc	$⊢ ((K \in HL \land W \in H) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land Q \in A \land (S \in A \land \neg S \underset{˙}{\leq} W)) \land \neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \to S \underset{˙}{\lor} U \in {Base}_{K}$
35	16 2 4	hlatjcl	$⊢ (K \in HL \land Q \in A \land C \in A) \to Q \underset{˙}{\lor} C \in {Base}_{K}$
36	11 22 30 35	syl3anc	$⊢ ((K \in HL \land W \in H) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land Q \in A \land (S \in A \land \neg S \underset{˙}{\leq} W)) \land \neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \to Q \underset{˙}{\lor} C \in {Base}_{K}$
37	1 2 4	hlatlej2	$⊢ (K \in HL \land Q \in A \land C \in A) \to C \underset{˙}{\leq} (Q \underset{˙}{\lor} C)$
38	11 22 30 37	syl3anc	$⊢ ((K \in HL \land W \in H) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land Q \in A \land (S \in A \land \neg S \underset{˙}{\leq} W)) \land \neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \to C \underset{˙}{\leq} (Q \underset{˙}{\lor} C)$
39	16 1 2 3 4	atmod4i1	$⊢ (K \in HL \land (C \in A \land S \underset{˙}{\lor} U \in {Base}_{K} \land Q \underset{˙}{\lor} C \in {Base}_{K}) \land C \underset{˙}{\leq} (Q \underset{˙}{\lor} C)) \to ((S \underset{˙}{\lor} U) \underset{˙}{\land} (Q \underset{˙}{\lor} C)) \underset{˙}{\lor} C = ((S \underset{˙}{\lor} U) \underset{˙}{\lor} C) \underset{˙}{\land} (Q \underset{˙}{\lor} C)$
40	11 30 34 36 38 39	syl131anc	$⊢ ((K \in HL \land W \in H) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land Q \in A \land (S \in A \land \neg S \underset{˙}{\leq} W)) \land \neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \to ((S \underset{˙}{\lor} U) \underset{˙}{\land} (Q \underset{˙}{\lor} C)) \underset{˙}{\lor} C = ((S \underset{˙}{\lor} U) \underset{˙}{\lor} C) \underset{˙}{\land} (Q \underset{˙}{\lor} C)$
41	8	oveq2i	$⊢ S \underset{˙}{\lor} C = S \underset{˙}{\lor} ((P \underset{˙}{\lor} S) \underset{˙}{\land} W)$
42	16 2 4	hlatjcl	$⊢ (K \in HL \land P \in A \land S \in A) \to P \underset{˙}{\lor} S \in {Base}_{K}$
43	11 19 14 42	syl3anc	$⊢ ((K \in HL \land W \in H) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land Q \in A \land (S \in A \land \neg S \underset{˙}{\leq} W)) \land \neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \to P \underset{˙}{\lor} S \in {Base}_{K}$
44		simp1r	$⊢ ((K \in HL \land W \in H) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land Q \in A \land (S \in A \land \neg S \underset{˙}{\leq} W)) \land \neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \to W \in H$
45	16 5	lhpbase	$⊢ W \in H \to W \in {Base}_{K}$
46	44 45	syl	$⊢ ((K \in HL \land W \in H) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land Q \in A \land (S \in A \land \neg S \underset{˙}{\leq} W)) \land \neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \to W \in {Base}_{K}$
47	1 2 4	hlatlej2	$⊢ (K \in HL \land P \in A \land S \in A) \to S \underset{˙}{\leq} (P \underset{˙}{\lor} S)$
48	11 19 14 47	syl3anc	$⊢ ((K \in HL \land W \in H) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land Q \in A \land (S \in A \land \neg S \underset{˙}{\leq} W)) \land \neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \to S \underset{˙}{\leq} (P \underset{˙}{\lor} S)$
49	16 1 2 3 4	atmod3i1	$⊢ (K \in HL \land (S \in A \land P \underset{˙}{\lor} S \in {Base}_{K} \land W \in {Base}_{K}) \land S \underset{˙}{\leq} (P \underset{˙}{\lor} S)) \to S \underset{˙}{\lor} ((P \underset{˙}{\lor} S) \underset{˙}{\land} W) = (P \underset{˙}{\lor} S) \underset{˙}{\land} (S \underset{˙}{\lor} W)$
50	11 14 43 46 48 49	syl131anc	$⊢ ((K \in HL \land W \in H) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land Q \in A \land (S \in A \land \neg S \underset{˙}{\leq} W)) \land \neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \to S \underset{˙}{\lor} ((P \underset{˙}{\lor} S) \underset{˙}{\land} W) = (P \underset{˙}{\lor} S) \underset{˙}{\land} (S \underset{˙}{\lor} W)$
51		simp23r	$⊢ ((K \in HL \land W \in H) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land Q \in A \land (S \in A \land \neg S \underset{˙}{\leq} W)) \land \neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \to \neg S \underset{˙}{\leq} W$
52		eqid	$⊢ 1. (K) = 1. (K)$
53	1 2 52 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)$
54	12 14 51 53	syl12anc	$⊢ ((K \in HL \land W \in H) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land Q \in A \land (S \in A \land \neg S \underset{˙}{\leq} W)) \land \neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \to S \underset{˙}{\lor} W = 1. (K)$
55	54	oveq2d	$⊢ ((K \in HL \land W \in H) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land Q \in A \land (S \in A \land \neg S \underset{˙}{\leq} W)) \land \neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \to (P \underset{˙}{\lor} S) \underset{˙}{\land} (S \underset{˙}{\lor} W) = (P \underset{˙}{\lor} S) \underset{˙}{\land} 1. (K)$
56		hlol	$⊢ K \in HL \to K \in OL$
57	11 56	syl	$⊢ ((K \in HL \land W \in H) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land Q \in A \land (S \in A \land \neg S \underset{˙}{\leq} W)) \land \neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \to K \in OL$
58	16 3 52	olm11	$⊢ (K \in OL \land P \underset{˙}{\lor} S \in {Base}_{K}) \to (P \underset{˙}{\lor} S) \underset{˙}{\land} 1. (K) = P \underset{˙}{\lor} S$
59	57 43 58	syl2anc	$⊢ ((K \in HL \land W \in H) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land Q \in A \land (S \in A \land \neg S \underset{˙}{\leq} W)) \land \neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \to (P \underset{˙}{\lor} S) \underset{˙}{\land} 1. (K) = P \underset{˙}{\lor} S$
60	50 55 59	3eqtrrd	$⊢ ((K \in HL \land W \in H) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land Q \in A \land (S \in A \land \neg S \underset{˙}{\leq} W)) \land \neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \to P \underset{˙}{\lor} S = S \underset{˙}{\lor} ((P \underset{˙}{\lor} S) \underset{˙}{\land} W)$
61	41 60	eqtr4id	$⊢ ((K \in HL \land W \in H) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land Q \in A \land (S \in A \land \neg S \underset{˙}{\leq} W)) \land \neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \to S \underset{˙}{\lor} C = P \underset{˙}{\lor} S$
62	61	oveq1d	$⊢ ((K \in HL \land W \in H) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land Q \in A \land (S \in A \land \neg S \underset{˙}{\leq} W)) \land \neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \to (S \underset{˙}{\lor} C) \underset{˙}{\lor} U = (P \underset{˙}{\lor} S) \underset{˙}{\lor} U$
63	16 4	atbase	$⊢ C \in A \to C \in {Base}_{K}$
64	30 63	syl	$⊢ ((K \in HL \land W \in H) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land Q \in A \land (S \in A \land \neg S \underset{˙}{\leq} W)) \land \neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \to C \in {Base}_{K}$
65	16 2	latj32	$⊢ (K \in Lat \land (S \in {Base}_{K} \land U \in {Base}_{K} \land C \in {Base}_{K})) \to (S \underset{˙}{\lor} U) \underset{˙}{\lor} C = (S \underset{˙}{\lor} C) \underset{˙}{\lor} U$
66	15 18 32 64 65	syl13anc	$⊢ ((K \in HL \land W \in H) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land Q \in A \land (S \in A \land \neg S \underset{˙}{\leq} W)) \land \neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \to (S \underset{˙}{\lor} U) \underset{˙}{\lor} C = (S \underset{˙}{\lor} C) \underset{˙}{\lor} U$
67	2 4	hlatj32	$⊢ (K \in HL \land (P \in A \land S \in A \land Q \in A)) \to (P \underset{˙}{\lor} S) \underset{˙}{\lor} Q = (P \underset{˙}{\lor} Q) \underset{˙}{\lor} S$
68	11 19 14 22 67	syl13anc	$⊢ ((K \in HL \land W \in H) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land Q \in A \land (S \in A \land \neg S \underset{˙}{\leq} W)) \land \neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \to (P \underset{˙}{\lor} S) \underset{˙}{\lor} Q = (P \underset{˙}{\lor} Q) \underset{˙}{\lor} S$
69	16 2	latjcom	$⊢ (K \in Lat \land Q \in {Base}_{K} \land P \underset{˙}{\lor} S \in {Base}_{K}) \to Q \underset{˙}{\lor} (P \underset{˙}{\lor} S) = (P \underset{˙}{\lor} S) \underset{˙}{\lor} Q$
70	15 24 43 69	syl3anc	$⊢ ((K \in HL \land W \in H) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land Q \in A \land (S \in A \land \neg S \underset{˙}{\leq} W)) \land \neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \to Q \underset{˙}{\lor} (P \underset{˙}{\lor} S) = (P \underset{˙}{\lor} S) \underset{˙}{\lor} Q$
71	6	oveq2i	$⊢ P \underset{˙}{\lor} U = P \underset{˙}{\lor} ((P \underset{˙}{\lor} Q) \underset{˙}{\land} W)$
72	16 2 4	hlatjcl	$⊢ (K \in HL \land P \in A \land Q \in A) \to P \underset{˙}{\lor} Q \in {Base}_{K}$
73	11 19 22 72	syl3anc	$⊢ ((K \in HL \land W \in H) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land Q \in A \land (S \in A \land \neg S \underset{˙}{\leq} W)) \land \neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \to P \underset{˙}{\lor} Q \in {Base}_{K}$
74	1 2 4	hlatlej1	$⊢ (K \in HL \land P \in A \land Q \in A) \to P \underset{˙}{\leq} (P \underset{˙}{\lor} Q)$
75	11 19 22 74	syl3anc	$⊢ ((K \in HL \land W \in H) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land Q \in A \land (S \in A \land \neg S \underset{˙}{\leq} W)) \land \neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \to P \underset{˙}{\leq} (P \underset{˙}{\lor} Q)$
76	16 1 2 3 4	atmod3i1	$⊢ (K \in HL \land (P \in A \land P \underset{˙}{\lor} Q \in {Base}_{K} \land W \in {Base}_{K}) \land P \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \to P \underset{˙}{\lor} ((P \underset{˙}{\lor} Q) \underset{˙}{\land} W) = (P \underset{˙}{\lor} Q) \underset{˙}{\land} (P \underset{˙}{\lor} W)$
77	11 19 73 46 75 76	syl131anc	$⊢ ((K \in HL \land W \in H) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land Q \in A \land (S \in A \land \neg S \underset{˙}{\leq} W)) \land \neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \to P \underset{˙}{\lor} ((P \underset{˙}{\lor} Q) \underset{˙}{\land} W) = (P \underset{˙}{\lor} Q) \underset{˙}{\land} (P \underset{˙}{\lor} W)$
78	1 2 52 4 5	lhpjat2	$⊢ ((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W)) \to P \underset{˙}{\lor} W = 1. (K)$
79	12 13 78	syl2anc	$⊢ ((K \in HL \land W \in H) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land Q \in A \land (S \in A \land \neg S \underset{˙}{\leq} W)) \land \neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \to P \underset{˙}{\lor} W = 1. (K)$
80	79	oveq2d	$⊢ ((K \in HL \land W \in H) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land Q \in A \land (S \in A \land \neg S \underset{˙}{\leq} W)) \land \neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \to (P \underset{˙}{\lor} Q) \underset{˙}{\land} (P \underset{˙}{\lor} W) = (P \underset{˙}{\lor} Q) \underset{˙}{\land} 1. (K)$
81	16 3 52	olm11	$⊢ (K \in OL \land P \underset{˙}{\lor} Q \in {Base}_{K}) \to (P \underset{˙}{\lor} Q) \underset{˙}{\land} 1. (K) = P \underset{˙}{\lor} Q$
82	57 73 81	syl2anc	$⊢ ((K \in HL \land W \in H) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land Q \in A \land (S \in A \land \neg S \underset{˙}{\leq} W)) \land \neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \to (P \underset{˙}{\lor} Q) \underset{˙}{\land} 1. (K) = P \underset{˙}{\lor} Q$
83	77 80 82	3eqtrd	$⊢ ((K \in HL \land W \in H) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land Q \in A \land (S \in A \land \neg S \underset{˙}{\leq} W)) \land \neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \to P \underset{˙}{\lor} ((P \underset{˙}{\lor} Q) \underset{˙}{\land} W) = P \underset{˙}{\lor} Q$
84	71 83	syl5eq	$⊢ ((K \in HL \land W \in H) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land Q \in A \land (S \in A \land \neg S \underset{˙}{\leq} W)) \land \neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \to P \underset{˙}{\lor} U = P \underset{˙}{\lor} Q$
85	84	oveq1d	$⊢ ((K \in HL \land W \in H) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land Q \in A \land (S \in A \land \neg S \underset{˙}{\leq} W)) \land \neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \to (P \underset{˙}{\lor} U) \underset{˙}{\lor} S = (P \underset{˙}{\lor} Q) \underset{˙}{\lor} S$
86	68 70 85	3eqtr4d	$⊢ ((K \in HL \land W \in H) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land Q \in A \land (S \in A \land \neg S \underset{˙}{\leq} W)) \land \neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \to Q \underset{˙}{\lor} (P \underset{˙}{\lor} S) = (P \underset{˙}{\lor} U) \underset{˙}{\lor} S$
87	16 2	latj32	$⊢ (K \in Lat \land (P \in {Base}_{K} \land U \in {Base}_{K} \land S \in {Base}_{K})) \to (P \underset{˙}{\lor} U) \underset{˙}{\lor} S = (P \underset{˙}{\lor} S) \underset{˙}{\lor} U$
88	15 21 32 18 87	syl13anc	$⊢ ((K \in HL \land W \in H) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land Q \in A \land (S \in A \land \neg S \underset{˙}{\leq} W)) \land \neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \to (P \underset{˙}{\lor} U) \underset{˙}{\lor} S = (P \underset{˙}{\lor} S) \underset{˙}{\lor} U$
89	86 88	eqtrd	$⊢ ((K \in HL \land W \in H) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land Q \in A \land (S \in A \land \neg S \underset{˙}{\leq} W)) \land \neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \to Q \underset{˙}{\lor} (P \underset{˙}{\lor} S) = (P \underset{˙}{\lor} S) \underset{˙}{\lor} U$
90	62 66 89	3eqtr4d	$⊢ ((K \in HL \land W \in H) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land Q \in A \land (S \in A \land \neg S \underset{˙}{\leq} W)) \land \neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \to (S \underset{˙}{\lor} U) \underset{˙}{\lor} C = Q \underset{˙}{\lor} (P \underset{˙}{\lor} S)$
91	90	oveq1d	$⊢ ((K \in HL \land W \in H) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land Q \in A \land (S \in A \land \neg S \underset{˙}{\leq} W)) \land \neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \to ((S \underset{˙}{\lor} U) \underset{˙}{\lor} C) \underset{˙}{\land} (Q \underset{˙}{\lor} C) = (Q \underset{˙}{\lor} (P \underset{˙}{\lor} S)) \underset{˙}{\land} (Q \underset{˙}{\lor} C)$
92	16 1 3	latmle1	$⊢ (K \in Lat \land P \underset{˙}{\lor} S \in {Base}_{K} \land W \in {Base}_{K}) \to ((P \underset{˙}{\lor} S) \underset{˙}{\land} W) \underset{˙}{\leq} (P \underset{˙}{\lor} S)$
93	15 43 46 92	syl3anc	$⊢ ((K \in HL \land W \in H) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land Q \in A \land (S \in A \land \neg S \underset{˙}{\leq} W)) \land \neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \to ((P \underset{˙}{\lor} S) \underset{˙}{\land} W) \underset{˙}{\leq} (P \underset{˙}{\lor} S)$
94	8 93	eqbrtrid	$⊢ ((K \in HL \land W \in H) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land Q \in A \land (S \in A \land \neg S \underset{˙}{\leq} W)) \land \neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \to C \underset{˙}{\leq} (P \underset{˙}{\lor} S)$
95	16 1 2	latjlej2	$⊢ (K \in Lat \land (C \in {Base}_{K} \land P \underset{˙}{\lor} S \in {Base}_{K} \land Q \in {Base}_{K})) \to (C \underset{˙}{\leq} (P \underset{˙}{\lor} S) \to (Q \underset{˙}{\lor} C) \underset{˙}{\leq} (Q \underset{˙}{\lor} (P \underset{˙}{\lor} S)))$
96	15 64 43 24 95	syl13anc	$⊢ ((K \in HL \land W \in H) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land Q \in A \land (S \in A \land \neg S \underset{˙}{\leq} W)) \land \neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \to (C \underset{˙}{\leq} (P \underset{˙}{\lor} S) \to (Q \underset{˙}{\lor} C) \underset{˙}{\leq} (Q \underset{˙}{\lor} (P \underset{˙}{\lor} S)))$
97	94 96	mpd	$⊢ ((K \in HL \land W \in H) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land Q \in A \land (S \in A \land \neg S \underset{˙}{\leq} W)) \land \neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \to (Q \underset{˙}{\lor} C) \underset{˙}{\leq} (Q \underset{˙}{\lor} (P \underset{˙}{\lor} S))$
98	16 2	latjcl	$⊢ (K \in Lat \land Q \in {Base}_{K} \land P \underset{˙}{\lor} S \in {Base}_{K}) \to Q \underset{˙}{\lor} (P \underset{˙}{\lor} S) \in {Base}_{K}$
99	15 24 43 98	syl3anc	$⊢ ((K \in HL \land W \in H) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land Q \in A \land (S \in A \land \neg S \underset{˙}{\leq} W)) \land \neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \to Q \underset{˙}{\lor} (P \underset{˙}{\lor} S) \in {Base}_{K}$
100	16 1 3	latleeqm2	$⊢ (K \in Lat \land Q \underset{˙}{\lor} C \in {Base}_{K} \land Q \underset{˙}{\lor} (P \underset{˙}{\lor} S) \in {Base}_{K}) \to ((Q \underset{˙}{\lor} C) \underset{˙}{\leq} (Q \underset{˙}{\lor} (P \underset{˙}{\lor} S)) \leftrightarrow (Q \underset{˙}{\lor} (P \underset{˙}{\lor} S)) \underset{˙}{\land} (Q \underset{˙}{\lor} C) = Q \underset{˙}{\lor} C)$
101	15 36 99 100	syl3anc	$⊢ ((K \in HL \land W \in H) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land Q \in A \land (S \in A \land \neg S \underset{˙}{\leq} W)) \land \neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \to ((Q \underset{˙}{\lor} C) \underset{˙}{\leq} (Q \underset{˙}{\lor} (P \underset{˙}{\lor} S)) \leftrightarrow (Q \underset{˙}{\lor} (P \underset{˙}{\lor} S)) \underset{˙}{\land} (Q \underset{˙}{\lor} C) = Q \underset{˙}{\lor} C)$
102	97 101	mpbid	$⊢ ((K \in HL \land W \in H) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land Q \in A \land (S \in A \land \neg S \underset{˙}{\leq} W)) \land \neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \to (Q \underset{˙}{\lor} (P \underset{˙}{\lor} S)) \underset{˙}{\land} (Q \underset{˙}{\lor} C) = Q \underset{˙}{\lor} C$
103	40 91 102	3eqtrd	$⊢ ((K \in HL \land W \in H) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land Q \in A \land (S \in A \land \neg S \underset{˙}{\leq} W)) \land \neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \to ((S \underset{˙}{\lor} U) \underset{˙}{\land} (Q \underset{˙}{\lor} C)) \underset{˙}{\lor} C = Q \underset{˙}{\lor} C$
104	10 103	syl5eq	$⊢ ((K \in HL \land W \in H) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land Q \in A \land (S \in A \land \neg S \underset{˙}{\leq} W)) \land \neg S \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \to F \underset{˙}{\lor} C = Q \underset{˙}{\lor} C$

Metamath Proof Explorer

Theorem cdleme9

Proof