cdleme35a

Description: Part of proof of Lemma E in Crawley p. 113. TODO: FIX COMMENT. (Contributed by NM, 10-Mar-2013)

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

Proof

Step	Hyp	Ref	Expression
1		cdleme35.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
2		cdleme35.j	$⊢ \underset{˙}{\lor} = join (K)$
3		cdleme35.m	$⊢ \underset{˙}{\land} = meet (K)$
4		cdleme35.a	$⊢ A = Atoms (K)$
5		cdleme35.h	$⊢ H = LHyp (K)$
6		cdleme35.u	$⊢ U = (P \underset{˙}{\lor} Q) \underset{˙}{\land} W$
7		cdleme35.f	$⊢ F = (R \underset{˙}{\lor} U) \underset{˙}{\land} (Q \underset{˙}{\lor} ((P \underset{˙}{\lor} R) \underset{˙}{\land} W))$
8		simp11l	$⊢ (((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land (P \neq Q \land (R \in A \land \neg R \underset{˙}{\leq} W)) \land \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \to K \in HL$
9	8	hllatd	$⊢ (((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land (P \neq Q \land (R \in A \land \neg R \underset{˙}{\leq} W)) \land \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \to K \in Lat$
10		simp2rl	$⊢ (((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land (P \neq Q \land (R \in A \land \neg R \underset{˙}{\leq} W)) \land \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \to R \in A$
11		eqid	$⊢ {Base}_{K} = {Base}_{K}$
12	11 4	atbase	$⊢ R \in A \to R \in {Base}_{K}$
13	10 12	syl	$⊢ (((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land (P \neq Q \land (R \in A \land \neg R \underset{˙}{\leq} W)) \land \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \to R \in {Base}_{K}$
14		simp11	$⊢ (((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land (P \neq Q \land (R \in A \land \neg R \underset{˙}{\leq} W)) \land \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \to (K \in HL \land W \in H)$
15		simp12	$⊢ (((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land (P \neq Q \land (R \in A \land \neg R \underset{˙}{\leq} W)) \land \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \to (P \in A \land \neg P \underset{˙}{\leq} W)$
16		simp13	$⊢ (((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land (P \neq Q \land (R \in A \land \neg R \underset{˙}{\leq} W)) \land \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \to (Q \in A \land \neg Q \underset{˙}{\leq} W)$
17		simp2r	$⊢ (((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land (P \neq Q \land (R \in A \land \neg R \underset{˙}{\leq} W)) \land \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \to (R \in A \land \neg R \underset{˙}{\leq} W)$
18		simp2l	$⊢ (((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land (P \neq Q \land (R \in A \land \neg R \underset{˙}{\leq} W)) \land \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \to P \neq Q$
19		simp3	$⊢ (((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land (P \neq Q \land (R \in A \land \neg R \underset{˙}{\leq} W)) \land \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \to \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q)$
20	1 2 3 4 5 6 7	cdleme3fa	$⊢ ((K \in HL \land W \in H) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W) \land (R \in A \land \neg R \underset{˙}{\leq} W)) \land (P \neq Q \land \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \to F \in A$
21	14 15 16 17 18 19 20	syl132anc	$⊢ (((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land (P \neq Q \land (R \in A \land \neg R \underset{˙}{\leq} W)) \land \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \to F \in A$
22	11 4	atbase	$⊢ F \in A \to F \in {Base}_{K}$
23	21 22	syl	$⊢ (((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land (P \neq Q \land (R \in A \land \neg R \underset{˙}{\leq} W)) \land \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \to F \in {Base}_{K}$
24	11 1 2	latlej2	$⊢ (K \in Lat \land R \in {Base}_{K} \land F \in {Base}_{K}) \to F \underset{˙}{\leq} (R \underset{˙}{\lor} F)$
25	9 13 23 24	syl3anc	$⊢ (((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land (P \neq Q \land (R \in A \land \neg R \underset{˙}{\leq} W)) \land \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \to F \underset{˙}{\leq} (R \underset{˙}{\lor} F)$
26		simp12l	$⊢ (((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land (P \neq Q \land (R \in A \land \neg R \underset{˙}{\leq} W)) \land \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \to P \in A$
27		simp13l	$⊢ (((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land (P \neq Q \land (R \in A \land \neg R \underset{˙}{\leq} W)) \land \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \to Q \in A$
28	1 2 3 4 5 6 7	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$
29	14 26 27 17 28	syl13anc	$⊢ (((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land (P \neq Q \land (R \in A \land \neg R \underset{˙}{\leq} W)) \land \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \to R \underset{˙}{\lor} F = R \underset{˙}{\lor} U$
30	25 29	breqtrd	$⊢ (((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land (P \neq Q \land (R \in A \land \neg R \underset{˙}{\leq} W)) \land \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \to F \underset{˙}{\leq} (R \underset{˙}{\lor} U)$
31	1 2 3 4 5 6	cdleme0a	$⊢ ((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land P \neq Q)) \to U \in A$
32	14 15 27 18 31	syl112anc	$⊢ (((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land (P \neq Q \land (R \in A \land \neg R \underset{˙}{\leq} W)) \land \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \to U \in A$
33	11 4	atbase	$⊢ U \in A \to U \in {Base}_{K}$
34	32 33	syl	$⊢ (((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land (P \neq Q \land (R \in A \land \neg R \underset{˙}{\leq} W)) \land \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \to U \in {Base}_{K}$
35	11 1 2	latlej2	$⊢ (K \in Lat \land R \in {Base}_{K} \land U \in {Base}_{K}) \to U \underset{˙}{\leq} (R \underset{˙}{\lor} U)$
36	9 13 34 35	syl3anc	$⊢ (((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land (P \neq Q \land (R \in A \land \neg R \underset{˙}{\leq} W)) \land \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \to U \underset{˙}{\leq} (R \underset{˙}{\lor} U)$
37	11 2 4	hlatjcl	$⊢ (K \in HL \land R \in A \land U \in A) \to R \underset{˙}{\lor} U \in {Base}_{K}$
38	8 10 32 37	syl3anc	$⊢ (((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land (P \neq Q \land (R \in A \land \neg R \underset{˙}{\leq} W)) \land \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \to R \underset{˙}{\lor} U \in {Base}_{K}$
39	11 1 2	latjle12	$⊢ (K \in Lat \land (F \in {Base}_{K} \land U \in {Base}_{K} \land R \underset{˙}{\lor} U \in {Base}_{K})) \to ((F \underset{˙}{\leq} (R \underset{˙}{\lor} U) \land U \underset{˙}{\leq} (R \underset{˙}{\lor} U)) \leftrightarrow (F \underset{˙}{\lor} U) \underset{˙}{\leq} (R \underset{˙}{\lor} U))$
40	9 23 34 38 39	syl13anc	$⊢ (((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land (P \neq Q \land (R \in A \land \neg R \underset{˙}{\leq} W)) \land \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \to ((F \underset{˙}{\leq} (R \underset{˙}{\lor} U) \land U \underset{˙}{\leq} (R \underset{˙}{\lor} U)) \leftrightarrow (F \underset{˙}{\lor} U) \underset{˙}{\leq} (R \underset{˙}{\lor} U))$
41	30 36 40	mpbi2and	$⊢ (((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land (P \neq Q \land (R \in A \land \neg R \underset{˙}{\leq} W)) \land \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \to (F \underset{˙}{\lor} U) \underset{˙}{\leq} (R \underset{˙}{\lor} U)$
42		eqid	$⊢ (P \underset{˙}{\lor} R) \underset{˙}{\land} W = (P \underset{˙}{\lor} R) \underset{˙}{\land} W$
43	1 2 3 4 5 6 7 42	cdleme3g	$⊢ ((K \in HL \land W \in H) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W) \land (R \in A \land \neg R \underset{˙}{\leq} W)) \land (P \neq Q \land \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \to F \neq U$
44	14 15 16 17 18 19 43	syl132anc	$⊢ (((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land (P \neq Q \land (R \in A \land \neg R \underset{˙}{\leq} W)) \land \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \to F \neq U$
45	1 2 4	ps-1	$⊢ (K \in HL \land (F \in A \land U \in A \land F \neq U) \land (R \in A \land U \in A)) \to ((F \underset{˙}{\lor} U) \underset{˙}{\leq} (R \underset{˙}{\lor} U) \leftrightarrow F \underset{˙}{\lor} U = R \underset{˙}{\lor} U)$
46	8 21 32 44 10 32 45	syl132anc	$⊢ (((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land (P \neq Q \land (R \in A \land \neg R \underset{˙}{\leq} W)) \land \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \to ((F \underset{˙}{\lor} U) \underset{˙}{\leq} (R \underset{˙}{\lor} U) \leftrightarrow F \underset{˙}{\lor} U = R \underset{˙}{\lor} U)$
47	41 46	mpbid	$⊢ (((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land (P \neq Q \land (R \in A \land \neg R \underset{˙}{\leq} W)) \land \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q)) \to F \underset{˙}{\lor} U = R \underset{˙}{\lor} U$

Metamath Proof Explorer

Theorem cdleme35a

Proof