cdleme11g

Description: Part of proof of Lemma E in Crawley p. 113. Lemma leading to cdleme11 . (Contributed by NM, 14-Jun-2012)

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

Proof

Step	Hyp	Ref	Expression
1		cdleme11.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
2		cdleme11.j	$⊢ \underset{˙}{\lor} = join (K)$
3		cdleme11.m	$⊢ \underset{˙}{\land} = meet (K)$
4		cdleme11.a	$⊢ A = Atoms (K)$
5		cdleme11.h	$⊢ H = LHyp (K)$
6		cdleme11.u	$⊢ U = (P \underset{˙}{\lor} Q) \underset{˙}{\land} W$
7		cdleme11.c	$⊢ C = (P \underset{˙}{\lor} S) \underset{˙}{\land} W$
8		cdleme11.d	$⊢ D = (P \underset{˙}{\lor} T) \underset{˙}{\land} W$
9		cdleme11.f	$⊢ F = (S \underset{˙}{\lor} U) \underset{˙}{\land} (Q \underset{˙}{\lor} ((P \underset{˙}{\lor} S) \underset{˙}{\land} W))$
10	9	oveq2i	$⊢ Q \underset{˙}{\lor} F = Q \underset{˙}{\lor} ((S \underset{˙}{\lor} U) \underset{˙}{\land} (Q \underset{˙}{\lor} ((P \underset{˙}{\lor} S) \underset{˙}{\land} W)))$
11		simp1l	$⊢ ((K \in HL \land W \in H) \land (P \in A \land (Q \in A \land \neg Q \underset{˙}{\leq} W) \land S \in A) \land P \neq Q) \to K \in HL$
12		simp22l	$⊢ ((K \in HL \land W \in H) \land (P \in A \land (Q \in A \land \neg Q \underset{˙}{\leq} W) \land S \in A) \land P \neq Q) \to Q \in A$
13	11	hllatd	$⊢ ((K \in HL \land W \in H) \land (P \in A \land (Q \in A \land \neg Q \underset{˙}{\leq} W) \land S \in A) \land P \neq Q) \to K \in Lat$
14		simp23	$⊢ ((K \in HL \land W \in H) \land (P \in A \land (Q \in A \land \neg Q \underset{˙}{\leq} W) \land S \in A) \land P \neq Q) \to S \in A$
15		eqid	$⊢ {Base}_{K} = {Base}_{K}$
16	15 4	atbase	$⊢ S \in A \to S \in {Base}_{K}$
17	14 16	syl	$⊢ ((K \in HL \land W \in H) \land (P \in A \land (Q \in A \land \neg Q \underset{˙}{\leq} W) \land S \in A) \land P \neq Q) \to S \in {Base}_{K}$
18		simp1	$⊢ ((K \in HL \land W \in H) \land (P \in A \land (Q \in A \land \neg Q \underset{˙}{\leq} W) \land S \in A) \land P \neq Q) \to (K \in HL \land W \in H)$
19		simp21	$⊢ ((K \in HL \land W \in H) \land (P \in A \land (Q \in A \land \neg Q \underset{˙}{\leq} W) \land S \in A) \land P \neq Q) \to P \in A$
20	1 2 3 4 5 6 15	cdleme0aa	$⊢ ((K \in HL \land W \in H) \land P \in A \land Q \in A) \to U \in {Base}_{K}$
21	18 19 12 20	syl3anc	$⊢ ((K \in HL \land W \in H) \land (P \in A \land (Q \in A \land \neg Q \underset{˙}{\leq} W) \land S \in A) \land P \neq Q) \to U \in {Base}_{K}$
22	15 2	latjcl	$⊢ (K \in Lat \land S \in {Base}_{K} \land U \in {Base}_{K}) \to S \underset{˙}{\lor} U \in {Base}_{K}$
23	13 17 21 22	syl3anc	$⊢ ((K \in HL \land W \in H) \land (P \in A \land (Q \in A \land \neg Q \underset{˙}{\leq} W) \land S \in A) \land P \neq Q) \to S \underset{˙}{\lor} U \in {Base}_{K}$
24	15 4	atbase	$⊢ Q \in A \to Q \in {Base}_{K}$
25	12 24	syl	$⊢ ((K \in HL \land W \in H) \land (P \in A \land (Q \in A \land \neg Q \underset{˙}{\leq} W) \land S \in A) \land P \neq Q) \to Q \in {Base}_{K}$
26	15 4	atbase	$⊢ P \in A \to P \in {Base}_{K}$
27	19 26	syl	$⊢ ((K \in HL \land W \in H) \land (P \in A \land (Q \in A \land \neg Q \underset{˙}{\leq} W) \land S \in A) \land P \neq Q) \to P \in {Base}_{K}$
28	15 2	latjcl	$⊢ (K \in Lat \land P \in {Base}_{K} \land S \in {Base}_{K}) \to P \underset{˙}{\lor} S \in {Base}_{K}$
29	13 27 17 28	syl3anc	$⊢ ((K \in HL \land W \in H) \land (P \in A \land (Q \in A \land \neg Q \underset{˙}{\leq} W) \land S \in A) \land P \neq Q) \to P \underset{˙}{\lor} S \in {Base}_{K}$
30		simp1r	$⊢ ((K \in HL \land W \in H) \land (P \in A \land (Q \in A \land \neg Q \underset{˙}{\leq} W) \land S \in A) \land P \neq Q) \to W \in H$
31	15 5	lhpbase	$⊢ W \in H \to W \in {Base}_{K}$
32	30 31	syl	$⊢ ((K \in HL \land W \in H) \land (P \in A \land (Q \in A \land \neg Q \underset{˙}{\leq} W) \land S \in A) \land P \neq Q) \to W \in {Base}_{K}$
33	15 3	latmcl	$⊢ (K \in Lat \land P \underset{˙}{\lor} S \in {Base}_{K} \land W \in {Base}_{K}) \to (P \underset{˙}{\lor} S) \underset{˙}{\land} W \in {Base}_{K}$
34	13 29 32 33	syl3anc	$⊢ ((K \in HL \land W \in H) \land (P \in A \land (Q \in A \land \neg Q \underset{˙}{\leq} W) \land S \in A) \land P \neq Q) \to (P \underset{˙}{\lor} S) \underset{˙}{\land} W \in {Base}_{K}$
35	15 2	latjcl	$⊢ (K \in Lat \land Q \in {Base}_{K} \land (P \underset{˙}{\lor} S) \underset{˙}{\land} W \in {Base}_{K}) \to Q \underset{˙}{\lor} ((P \underset{˙}{\lor} S) \underset{˙}{\land} W) \in {Base}_{K}$
36	13 25 34 35	syl3anc	$⊢ ((K \in HL \land W \in H) \land (P \in A \land (Q \in A \land \neg Q \underset{˙}{\leq} W) \land S \in A) \land P \neq Q) \to Q \underset{˙}{\lor} ((P \underset{˙}{\lor} S) \underset{˙}{\land} W) \in {Base}_{K}$
37	15 1 2	latlej1	$⊢ (K \in Lat \land Q \in {Base}_{K} \land (P \underset{˙}{\lor} S) \underset{˙}{\land} W \in {Base}_{K}) \to Q \underset{˙}{\leq} (Q \underset{˙}{\lor} ((P \underset{˙}{\lor} S) \underset{˙}{\land} W))$
38	13 25 34 37	syl3anc	$⊢ ((K \in HL \land W \in H) \land (P \in A \land (Q \in A \land \neg Q \underset{˙}{\leq} W) \land S \in A) \land P \neq Q) \to Q \underset{˙}{\leq} (Q \underset{˙}{\lor} ((P \underset{˙}{\lor} S) \underset{˙}{\land} W))$
39	15 1 2 3 4	atmod1i1	$⊢ (K \in HL \land (Q \in A \land S \underset{˙}{\lor} U \in {Base}_{K} \land Q \underset{˙}{\lor} ((P \underset{˙}{\lor} S) \underset{˙}{\land} W) \in {Base}_{K}) \land Q \underset{˙}{\leq} (Q \underset{˙}{\lor} ((P \underset{˙}{\lor} S) \underset{˙}{\land} W))) \to Q \underset{˙}{\lor} ((S \underset{˙}{\lor} U) \underset{˙}{\land} (Q \underset{˙}{\lor} ((P \underset{˙}{\lor} S) \underset{˙}{\land} W))) = (Q \underset{˙}{\lor} (S \underset{˙}{\lor} U)) \underset{˙}{\land} (Q \underset{˙}{\lor} ((P \underset{˙}{\lor} S) \underset{˙}{\land} W))$
40	11 12 23 36 38 39	syl131anc	$⊢ ((K \in HL \land W \in H) \land (P \in A \land (Q \in A \land \neg Q \underset{˙}{\leq} W) \land S \in A) \land P \neq Q) \to Q \underset{˙}{\lor} ((S \underset{˙}{\lor} U) \underset{˙}{\land} (Q \underset{˙}{\lor} ((P \underset{˙}{\lor} S) \underset{˙}{\land} W))) = (Q \underset{˙}{\lor} (S \underset{˙}{\lor} U)) \underset{˙}{\land} (Q \underset{˙}{\lor} ((P \underset{˙}{\lor} S) \underset{˙}{\land} W))$
41	10 40	syl5eq	$⊢ ((K \in HL \land W \in H) \land (P \in A \land (Q \in A \land \neg Q \underset{˙}{\leq} W) \land S \in A) \land P \neq Q) \to Q \underset{˙}{\lor} F = (Q \underset{˙}{\lor} (S \underset{˙}{\lor} U)) \underset{˙}{\land} (Q \underset{˙}{\lor} ((P \underset{˙}{\lor} S) \underset{˙}{\land} W))$
42		simp22	$⊢ ((K \in HL \land W \in H) \land (P \in A \land (Q \in A \land \neg Q \underset{˙}{\leq} W) \land S \in A) \land P \neq Q) \to (Q \in A \land \neg Q \underset{˙}{\leq} W)$
43	1 2 3 4 5 6	cdleme0cq	$⊢ ((K \in HL \land W \in H) \land (P \in A \land (Q \in A \land \neg Q \underset{˙}{\leq} W))) \to Q \underset{˙}{\lor} U = P \underset{˙}{\lor} Q$
44	18 19 42 43	syl12anc	$⊢ ((K \in HL \land W \in H) \land (P \in A \land (Q \in A \land \neg Q \underset{˙}{\leq} W) \land S \in A) \land P \neq Q) \to Q \underset{˙}{\lor} U = P \underset{˙}{\lor} Q$
45	44	oveq2d	$⊢ ((K \in HL \land W \in H) \land (P \in A \land (Q \in A \land \neg Q \underset{˙}{\leq} W) \land S \in A) \land P \neq Q) \to S \underset{˙}{\lor} (Q \underset{˙}{\lor} U) = S \underset{˙}{\lor} (P \underset{˙}{\lor} Q)$
46	15 2	latj12	$⊢ (K \in Lat \land (Q \in {Base}_{K} \land S \in {Base}_{K} \land U \in {Base}_{K})) \to Q \underset{˙}{\lor} (S \underset{˙}{\lor} U) = S \underset{˙}{\lor} (Q \underset{˙}{\lor} U)$
47	13 25 17 21 46	syl13anc	$⊢ ((K \in HL \land W \in H) \land (P \in A \land (Q \in A \land \neg Q \underset{˙}{\leq} W) \land S \in A) \land P \neq Q) \to Q \underset{˙}{\lor} (S \underset{˙}{\lor} U) = S \underset{˙}{\lor} (Q \underset{˙}{\lor} U)$
48	15 2	latj13	$⊢ (K \in Lat \land (Q \in {Base}_{K} \land P \in {Base}_{K} \land S \in {Base}_{K})) \to Q \underset{˙}{\lor} (P \underset{˙}{\lor} S) = S \underset{˙}{\lor} (P \underset{˙}{\lor} Q)$
49	13 25 27 17 48	syl13anc	$⊢ ((K \in HL \land W \in H) \land (P \in A \land (Q \in A \land \neg Q \underset{˙}{\leq} W) \land S \in A) \land P \neq Q) \to Q \underset{˙}{\lor} (P \underset{˙}{\lor} S) = S \underset{˙}{\lor} (P \underset{˙}{\lor} Q)$
50	45 47 49	3eqtr4d	$⊢ ((K \in HL \land W \in H) \land (P \in A \land (Q \in A \land \neg Q \underset{˙}{\leq} W) \land S \in A) \land P \neq Q) \to Q \underset{˙}{\lor} (S \underset{˙}{\lor} U) = Q \underset{˙}{\lor} (P \underset{˙}{\lor} S)$
51	50	oveq1d	$⊢ ((K \in HL \land W \in H) \land (P \in A \land (Q \in A \land \neg Q \underset{˙}{\leq} W) \land S \in A) \land P \neq Q) \to (Q \underset{˙}{\lor} (S \underset{˙}{\lor} U)) \underset{˙}{\land} (Q \underset{˙}{\lor} ((P \underset{˙}{\lor} S) \underset{˙}{\land} W)) = (Q \underset{˙}{\lor} (P \underset{˙}{\lor} S)) \underset{˙}{\land} (Q \underset{˙}{\lor} ((P \underset{˙}{\lor} S) \underset{˙}{\land} W))$
52	15 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)$
53	13 29 32 52	syl3anc	$⊢ ((K \in HL \land W \in H) \land (P \in A \land (Q \in A \land \neg Q \underset{˙}{\leq} W) \land S \in A) \land P \neq Q) \to ((P \underset{˙}{\lor} S) \underset{˙}{\land} W) \underset{˙}{\leq} (P \underset{˙}{\lor} S)$
54	15 1 2	latjlej2	$⊢ (K \in Lat \land ((P \underset{˙}{\lor} S) \underset{˙}{\land} W \in {Base}_{K} \land P \underset{˙}{\lor} S \in {Base}_{K} \land Q \in {Base}_{K})) \to (((P \underset{˙}{\lor} S) \underset{˙}{\land} W) \underset{˙}{\leq} (P \underset{˙}{\lor} S) \to (Q \underset{˙}{\lor} ((P \underset{˙}{\lor} S) \underset{˙}{\land} W)) \underset{˙}{\leq} (Q \underset{˙}{\lor} (P \underset{˙}{\lor} S)))$
55	13 34 29 25 54	syl13anc	$⊢ ((K \in HL \land W \in H) \land (P \in A \land (Q \in A \land \neg Q \underset{˙}{\leq} W) \land S \in A) \land P \neq Q) \to (((P \underset{˙}{\lor} S) \underset{˙}{\land} W) \underset{˙}{\leq} (P \underset{˙}{\lor} S) \to (Q \underset{˙}{\lor} ((P \underset{˙}{\lor} S) \underset{˙}{\land} W)) \underset{˙}{\leq} (Q \underset{˙}{\lor} (P \underset{˙}{\lor} S)))$
56	53 55	mpd	$⊢ ((K \in HL \land W \in H) \land (P \in A \land (Q \in A \land \neg Q \underset{˙}{\leq} W) \land S \in A) \land P \neq Q) \to (Q \underset{˙}{\lor} ((P \underset{˙}{\lor} S) \underset{˙}{\land} W)) \underset{˙}{\leq} (Q \underset{˙}{\lor} (P \underset{˙}{\lor} S))$
57	15 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}$
58	13 25 29 57	syl3anc	$⊢ ((K \in HL \land W \in H) \land (P \in A \land (Q \in A \land \neg Q \underset{˙}{\leq} W) \land S \in A) \land P \neq Q) \to Q \underset{˙}{\lor} (P \underset{˙}{\lor} S) \in {Base}_{K}$
59	15 1 3	latleeqm2	$⊢ (K \in Lat \land Q \underset{˙}{\lor} ((P \underset{˙}{\lor} S) \underset{˙}{\land} W) \in {Base}_{K} \land Q \underset{˙}{\lor} (P \underset{˙}{\lor} S) \in {Base}_{K}) \to ((Q \underset{˙}{\lor} ((P \underset{˙}{\lor} S) \underset{˙}{\land} W)) \underset{˙}{\leq} (Q \underset{˙}{\lor} (P \underset{˙}{\lor} S)) \leftrightarrow (Q \underset{˙}{\lor} (P \underset{˙}{\lor} S)) \underset{˙}{\land} (Q \underset{˙}{\lor} ((P \underset{˙}{\lor} S) \underset{˙}{\land} W)) = Q \underset{˙}{\lor} ((P \underset{˙}{\lor} S) \underset{˙}{\land} W))$
60	13 36 58 59	syl3anc	$⊢ ((K \in HL \land W \in H) \land (P \in A \land (Q \in A \land \neg Q \underset{˙}{\leq} W) \land S \in A) \land P \neq Q) \to ((Q \underset{˙}{\lor} ((P \underset{˙}{\lor} S) \underset{˙}{\land} W)) \underset{˙}{\leq} (Q \underset{˙}{\lor} (P \underset{˙}{\lor} S)) \leftrightarrow (Q \underset{˙}{\lor} (P \underset{˙}{\lor} S)) \underset{˙}{\land} (Q \underset{˙}{\lor} ((P \underset{˙}{\lor} S) \underset{˙}{\land} W)) = Q \underset{˙}{\lor} ((P \underset{˙}{\lor} S) \underset{˙}{\land} W))$
61	56 60	mpbid	$⊢ ((K \in HL \land W \in H) \land (P \in A \land (Q \in A \land \neg Q \underset{˙}{\leq} W) \land S \in A) \land P \neq Q) \to (Q \underset{˙}{\lor} (P \underset{˙}{\lor} S)) \underset{˙}{\land} (Q \underset{˙}{\lor} ((P \underset{˙}{\lor} S) \underset{˙}{\land} W)) = Q \underset{˙}{\lor} ((P \underset{˙}{\lor} S) \underset{˙}{\land} W)$
62	7	oveq2i	$⊢ Q \underset{˙}{\lor} C = Q \underset{˙}{\lor} ((P \underset{˙}{\lor} S) \underset{˙}{\land} W)$
63	61 62	eqtr4di	$⊢ ((K \in HL \land W \in H) \land (P \in A \land (Q \in A \land \neg Q \underset{˙}{\leq} W) \land S \in A) \land P \neq Q) \to (Q \underset{˙}{\lor} (P \underset{˙}{\lor} S)) \underset{˙}{\land} (Q \underset{˙}{\lor} ((P \underset{˙}{\lor} S) \underset{˙}{\land} W)) = Q \underset{˙}{\lor} C$
64	41 51 63	3eqtrd	$⊢ ((K \in HL \land W \in H) \land (P \in A \land (Q \in A \land \neg Q \underset{˙}{\leq} W) \land S \in A) \land P \neq Q) \to Q \underset{˙}{\lor} F = Q \underset{˙}{\lor} C$

Metamath Proof Explorer

Theorem cdleme11g

Proof