cdlemc5

	Ref	Expression
Hypotheses	cdlemc3.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
	cdlemc3.j	$⊢ \underset{˙}{\lor} = join (K)$
	cdlemc3.m	$⊢ \underset{˙}{\land} = meet (K)$
	cdlemc3.a	$⊢ A = Atoms (K)$
	cdlemc3.h	$⊢ H = LHyp (K)$
	cdlemc3.t	$⊢ T = LTrn (K) (W)$
	cdlemc3.r	$⊢ R = trL (K) (W)$
Assertion	cdlemc5	$⊢ ((K \in HL \land W \in H) \land (F \in T \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land (\neg Q \underset{˙}{\leq} (P \underset{˙}{\lor} F (P)) \land F (P) \neq P)) \to F (Q) = (Q \underset{˙}{\lor} R (F)) \underset{˙}{\land} (F (P) \underset{˙}{\lor} ((P \underset{˙}{\lor} Q) \underset{˙}{\land} W))$

Proof

Step	Hyp	Ref	Expression
1		cdlemc3.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
2		cdlemc3.j	$⊢ \underset{˙}{\lor} = join (K)$
3		cdlemc3.m	$⊢ \underset{˙}{\land} = meet (K)$
4		cdlemc3.a	$⊢ A = Atoms (K)$
5		cdlemc3.h	$⊢ H = LHyp (K)$
6		cdlemc3.t	$⊢ T = LTrn (K) (W)$
7		cdlemc3.r	$⊢ R = trL (K) (W)$
8		simp1l	$⊢ ((K \in HL \land W \in H) \land (F \in T \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land (\neg Q \underset{˙}{\leq} (P \underset{˙}{\lor} F (P)) \land F (P) \neq P)) \to K \in HL$
9		simp23l	$⊢ ((K \in HL \land W \in H) \land (F \in T \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land (\neg Q \underset{˙}{\leq} (P \underset{˙}{\lor} F (P)) \land F (P) \neq P)) \to Q \in A$
10		simp1	$⊢ ((K \in HL \land W \in H) \land (F \in T \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land (\neg Q \underset{˙}{\leq} (P \underset{˙}{\lor} F (P)) \land F (P) \neq P)) \to (K \in HL \land W \in H)$
11		simp21	$⊢ ((K \in HL \land W \in H) \land (F \in T \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land (\neg Q \underset{˙}{\leq} (P \underset{˙}{\lor} F (P)) \land F (P) \neq P)) \to F \in T$
12	1 4 5 6	ltrnat	$⊢ ((K \in HL \land W \in H) \land F \in T \land Q \in A) \to F (Q) \in A$
13	10 11 9 12	syl3anc	$⊢ ((K \in HL \land W \in H) \land (F \in T \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land (\neg Q \underset{˙}{\leq} (P \underset{˙}{\lor} F (P)) \land F (P) \neq P)) \to F (Q) \in A$
14	1 2 4	hlatlej2	$⊢ (K \in HL \land Q \in A \land F (Q) \in A) \to F (Q) \underset{˙}{\leq} (Q \underset{˙}{\lor} F (Q))$
15	8 9 13 14	syl3anc	$⊢ ((K \in HL \land W \in H) \land (F \in T \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land (\neg Q \underset{˙}{\leq} (P \underset{˙}{\lor} F (P)) \land F (P) \neq P)) \to F (Q) \underset{˙}{\leq} (Q \underset{˙}{\lor} F (Q))$
16		simp23	$⊢ ((K \in HL \land W \in H) \land (F \in T \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land (\neg Q \underset{˙}{\leq} (P \underset{˙}{\lor} F (P)) \land F (P) \neq P)) \to (Q \in A \land \neg Q \underset{˙}{\leq} W)$
17	1 2 4 5 6 7	trljat1	$⊢ ((K \in HL \land W \in H) \land F \in T \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \to Q \underset{˙}{\lor} R (F) = Q \underset{˙}{\lor} F (Q)$
18	10 11 16 17	syl3anc	$⊢ ((K \in HL \land W \in H) \land (F \in T \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land (\neg Q \underset{˙}{\leq} (P \underset{˙}{\lor} F (P)) \land F (P) \neq P)) \to Q \underset{˙}{\lor} R (F) = Q \underset{˙}{\lor} F (Q)$
19	15 18	breqtrrd	$⊢ ((K \in HL \land W \in H) \land (F \in T \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land (\neg Q \underset{˙}{\leq} (P \underset{˙}{\lor} F (P)) \land F (P) \neq P)) \to F (Q) \underset{˙}{\leq} (Q \underset{˙}{\lor} R (F))$
20		simp22	$⊢ ((K \in HL \land W \in H) \land (F \in T \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land (\neg Q \underset{˙}{\leq} (P \underset{˙}{\lor} F (P)) \land F (P) \neq P)) \to (P \in A \land \neg P \underset{˙}{\leq} W)$
21	1 2 3 4 5 6	cdlemc2	$⊢ ((K \in HL \land W \in H) \land F \in T \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W))) \to F (Q) \underset{˙}{\leq} (F (P) \underset{˙}{\lor} ((P \underset{˙}{\lor} Q) \underset{˙}{\land} W))$
22	10 11 20 16 21	syl112anc	$⊢ ((K \in HL \land W \in H) \land (F \in T \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land (\neg Q \underset{˙}{\leq} (P \underset{˙}{\lor} F (P)) \land F (P) \neq P)) \to F (Q) \underset{˙}{\leq} (F (P) \underset{˙}{\lor} ((P \underset{˙}{\lor} Q) \underset{˙}{\land} W))$
23	8	hllatd	$⊢ ((K \in HL \land W \in H) \land (F \in T \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land (\neg Q \underset{˙}{\leq} (P \underset{˙}{\lor} F (P)) \land F (P) \neq P)) \to K \in Lat$
24		eqid	$⊢ {Base}_{K} = {Base}_{K}$
25	24 4	atbase	$⊢ Q \in A \to Q \in {Base}_{K}$
26	9 25	syl	$⊢ ((K \in HL \land W \in H) \land (F \in T \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land (\neg Q \underset{˙}{\leq} (P \underset{˙}{\lor} F (P)) \land F (P) \neq P)) \to Q \in {Base}_{K}$
27	24 5 6	ltrncl	$⊢ ((K \in HL \land W \in H) \land F \in T \land Q \in {Base}_{K}) \to F (Q) \in {Base}_{K}$
28	10 11 26 27	syl3anc	$⊢ ((K \in HL \land W \in H) \land (F \in T \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land (\neg Q \underset{˙}{\leq} (P \underset{˙}{\lor} F (P)) \land F (P) \neq P)) \to F (Q) \in {Base}_{K}$
29	24 5 6 7	trlcl	$⊢ ((K \in HL \land W \in H) \land F \in T) \to R (F) \in {Base}_{K}$
30	10 11 29	syl2anc	$⊢ ((K \in HL \land W \in H) \land (F \in T \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land (\neg Q \underset{˙}{\leq} (P \underset{˙}{\lor} F (P)) \land F (P) \neq P)) \to R (F) \in {Base}_{K}$
31	24 2	latjcl	$⊢ (K \in Lat \land Q \in {Base}_{K} \land R (F) \in {Base}_{K}) \to Q \underset{˙}{\lor} R (F) \in {Base}_{K}$
32	23 26 30 31	syl3anc	$⊢ ((K \in HL \land W \in H) \land (F \in T \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land (\neg Q \underset{˙}{\leq} (P \underset{˙}{\lor} F (P)) \land F (P) \neq P)) \to Q \underset{˙}{\lor} R (F) \in {Base}_{K}$
33		simp22l	$⊢ ((K \in HL \land W \in H) \land (F \in T \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land (\neg Q \underset{˙}{\leq} (P \underset{˙}{\lor} F (P)) \land F (P) \neq P)) \to P \in A$
34	24 4	atbase	$⊢ P \in A \to P \in {Base}_{K}$
35	33 34	syl	$⊢ ((K \in HL \land W \in H) \land (F \in T \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land (\neg Q \underset{˙}{\leq} (P \underset{˙}{\lor} F (P)) \land F (P) \neq P)) \to P \in {Base}_{K}$
36	24 5 6	ltrncl	$⊢ ((K \in HL \land W \in H) \land F \in T \land P \in {Base}_{K}) \to F (P) \in {Base}_{K}$
37	10 11 35 36	syl3anc	$⊢ ((K \in HL \land W \in H) \land (F \in T \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land (\neg Q \underset{˙}{\leq} (P \underset{˙}{\lor} F (P)) \land F (P) \neq P)) \to F (P) \in {Base}_{K}$
38	24 2 4	hlatjcl	$⊢ (K \in HL \land P \in A \land Q \in A) \to P \underset{˙}{\lor} Q \in {Base}_{K}$
39	8 33 9 38	syl3anc	$⊢ ((K \in HL \land W \in H) \land (F \in T \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land (\neg Q \underset{˙}{\leq} (P \underset{˙}{\lor} F (P)) \land F (P) \neq P)) \to P \underset{˙}{\lor} Q \in {Base}_{K}$
40		simp1r	$⊢ ((K \in HL \land W \in H) \land (F \in T \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land (\neg Q \underset{˙}{\leq} (P \underset{˙}{\lor} F (P)) \land F (P) \neq P)) \to W \in H$
41	24 5	lhpbase	$⊢ W \in H \to W \in {Base}_{K}$
42	40 41	syl	$⊢ ((K \in HL \land W \in H) \land (F \in T \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land (\neg Q \underset{˙}{\leq} (P \underset{˙}{\lor} F (P)) \land F (P) \neq P)) \to W \in {Base}_{K}$
43	24 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}$
44	23 39 42 43	syl3anc	$⊢ ((K \in HL \land W \in H) \land (F \in T \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land (\neg Q \underset{˙}{\leq} (P \underset{˙}{\lor} F (P)) \land F (P) \neq P)) \to (P \underset{˙}{\lor} Q) \underset{˙}{\land} W \in {Base}_{K}$
45	24 2	latjcl	$⊢ (K \in Lat \land F (P) \in {Base}_{K} \land (P \underset{˙}{\lor} Q) \underset{˙}{\land} W \in {Base}_{K}) \to F (P) \underset{˙}{\lor} ((P \underset{˙}{\lor} Q) \underset{˙}{\land} W) \in {Base}_{K}$
46	23 37 44 45	syl3anc	$⊢ ((K \in HL \land W \in H) \land (F \in T \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land (\neg Q \underset{˙}{\leq} (P \underset{˙}{\lor} F (P)) \land F (P) \neq P)) \to F (P) \underset{˙}{\lor} ((P \underset{˙}{\lor} Q) \underset{˙}{\land} W) \in {Base}_{K}$
47	24 1 3	latlem12	$⊢ (K \in Lat \land (F (Q) \in {Base}_{K} \land Q \underset{˙}{\lor} R (F) \in {Base}_{K} \land F (P) \underset{˙}{\lor} ((P \underset{˙}{\lor} Q) \underset{˙}{\land} W) \in {Base}_{K})) \to ((F (Q) \underset{˙}{\leq} (Q \underset{˙}{\lor} R (F)) \land F (Q) \underset{˙}{\leq} (F (P) \underset{˙}{\lor} ((P \underset{˙}{\lor} Q) \underset{˙}{\land} W))) \leftrightarrow F (Q) \underset{˙}{\leq} ((Q \underset{˙}{\lor} R (F)) \underset{˙}{\land} (F (P) \underset{˙}{\lor} ((P \underset{˙}{\lor} Q) \underset{˙}{\land} W))))$
48	23 28 32 46 47	syl13anc	$⊢ ((K \in HL \land W \in H) \land (F \in T \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land (\neg Q \underset{˙}{\leq} (P \underset{˙}{\lor} F (P)) \land F (P) \neq P)) \to ((F (Q) \underset{˙}{\leq} (Q \underset{˙}{\lor} R (F)) \land F (Q) \underset{˙}{\leq} (F (P) \underset{˙}{\lor} ((P \underset{˙}{\lor} Q) \underset{˙}{\land} W))) \leftrightarrow F (Q) \underset{˙}{\leq} ((Q \underset{˙}{\lor} R (F)) \underset{˙}{\land} (F (P) \underset{˙}{\lor} ((P \underset{˙}{\lor} Q) \underset{˙}{\land} W))))$
49	19 22 48	mpbi2and	$⊢ ((K \in HL \land W \in H) \land (F \in T \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land (\neg Q \underset{˙}{\leq} (P \underset{˙}{\lor} F (P)) \land F (P) \neq P)) \to F (Q) \underset{˙}{\leq} ((Q \underset{˙}{\lor} R (F)) \underset{˙}{\land} (F (P) \underset{˙}{\lor} ((P \underset{˙}{\lor} Q) \underset{˙}{\land} W)))$
50		hlatl	$⊢ K \in HL \to K \in AtLat$
51	8 50	syl	$⊢ ((K \in HL \land W \in H) \land (F \in T \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land (\neg Q \underset{˙}{\leq} (P \underset{˙}{\lor} F (P)) \land F (P) \neq P)) \to K \in AtLat$
52		simp3r	$⊢ ((K \in HL \land W \in H) \land (F \in T \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land (\neg Q \underset{˙}{\leq} (P \underset{˙}{\lor} F (P)) \land F (P) \neq P)) \to F (P) \neq P$
53	1 4 5 6 7	trlat	$⊢ ((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (F \in T \land F (P) \neq P)) \to R (F) \in A$
54	10 20 11 52 53	syl112anc	$⊢ ((K \in HL \land W \in H) \land (F \in T \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land (\neg Q \underset{˙}{\leq} (P \underset{˙}{\lor} F (P)) \land F (P) \neq P)) \to R (F) \in A$
55	1 5 6 7	trlle	$⊢ ((K \in HL \land W \in H) \land F \in T) \to R (F) \underset{˙}{\leq} W$
56	10 11 55	syl2anc	$⊢ ((K \in HL \land W \in H) \land (F \in T \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land (\neg Q \underset{˙}{\leq} (P \underset{˙}{\lor} F (P)) \land F (P) \neq P)) \to R (F) \underset{˙}{\leq} W$
57		simp23r	$⊢ ((K \in HL \land W \in H) \land (F \in T \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land (\neg Q \underset{˙}{\leq} (P \underset{˙}{\lor} F (P)) \land F (P) \neq P)) \to \neg Q \underset{˙}{\leq} W$
58		nbrne2	$⊢ (R (F) \underset{˙}{\leq} W \land \neg Q \underset{˙}{\leq} W) \to R (F) \neq Q$
59	58	necomd	$⊢ (R (F) \underset{˙}{\leq} W \land \neg Q \underset{˙}{\leq} W) \to Q \neq R (F)$
60	56 57 59	syl2anc	$⊢ ((K \in HL \land W \in H) \land (F \in T \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land (\neg Q \underset{˙}{\leq} (P \underset{˙}{\lor} F (P)) \land F (P) \neq P)) \to Q \neq R (F)$
61		eqid	$⊢ LLines (K) = LLines (K)$
62	2 4 61	llni2	$⊢ ((K \in HL \land Q \in A \land R (F) \in A) \land Q \neq R (F)) \to Q \underset{˙}{\lor} R (F) \in LLines (K)$
63	8 9 54 60 62	syl31anc	$⊢ ((K \in HL \land W \in H) \land (F \in T \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land (\neg Q \underset{˙}{\leq} (P \underset{˙}{\lor} F (P)) \land F (P) \neq P)) \to Q \underset{˙}{\lor} R (F) \in LLines (K)$
64	1 4 5 6	ltrnat	$⊢ ((K \in HL \land W \in H) \land F \in T \land P \in A) \to F (P) \in A$
65	10 11 33 64	syl3anc	$⊢ ((K \in HL \land W \in H) \land (F \in T \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land (\neg Q \underset{˙}{\leq} (P \underset{˙}{\lor} F (P)) \land F (P) \neq P)) \to F (P) \in A$
66	1 2 4	hlatlej1	$⊢ (K \in HL \land P \in A \land F (P) \in A) \to P \underset{˙}{\leq} (P \underset{˙}{\lor} F (P))$
67	8 33 65 66	syl3anc	$⊢ ((K \in HL \land W \in H) \land (F \in T \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land (\neg Q \underset{˙}{\leq} (P \underset{˙}{\lor} F (P)) \land F (P) \neq P)) \to P \underset{˙}{\leq} (P \underset{˙}{\lor} F (P))$
68		simp3l	$⊢ ((K \in HL \land W \in H) \land (F \in T \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land (\neg Q \underset{˙}{\leq} (P \underset{˙}{\lor} F (P)) \land F (P) \neq P)) \to \neg Q \underset{˙}{\leq} (P \underset{˙}{\lor} F (P))$
69		nbrne2	$⊢ (P \underset{˙}{\leq} (P \underset{˙}{\lor} F (P)) \land \neg Q \underset{˙}{\leq} (P \underset{˙}{\lor} F (P))) \to P \neq Q$
70	67 68 69	syl2anc	$⊢ ((K \in HL \land W \in H) \land (F \in T \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land (\neg Q \underset{˙}{\leq} (P \underset{˙}{\lor} F (P)) \land F (P) \neq P)) \to P \neq Q$
71	1 2 3 4 5	lhpat	$⊢ ((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 (P \underset{˙}{\lor} Q) \underset{˙}{\land} W \in A$
72	10 20 9 70 71	syl112anc	$⊢ ((K \in HL \land W \in H) \land (F \in T \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land (\neg Q \underset{˙}{\leq} (P \underset{˙}{\lor} F (P)) \land F (P) \neq P)) \to (P \underset{˙}{\lor} Q) \underset{˙}{\land} W \in A$
73	24 1 3	latmle2	$⊢ (K \in Lat \land P \underset{˙}{\lor} Q \in {Base}_{K} \land W \in {Base}_{K}) \to ((P \underset{˙}{\lor} Q) \underset{˙}{\land} W) \underset{˙}{\leq} W$
74	23 39 42 73	syl3anc	$⊢ ((K \in HL \land W \in H) \land (F \in T \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land (\neg Q \underset{˙}{\leq} (P \underset{˙}{\lor} F (P)) \land F (P) \neq P)) \to ((P \underset{˙}{\lor} Q) \underset{˙}{\land} W) \underset{˙}{\leq} W$
75	1 4 5 6	ltrnel	$⊢ ((K \in HL \land W \in H) \land F \in T \land (P \in A \land \neg P \underset{˙}{\leq} W)) \to (F (P) \in A \land \neg F (P) \underset{˙}{\leq} W)$
76	75	simprd	$⊢ ((K \in HL \land W \in H) \land F \in T \land (P \in A \land \neg P \underset{˙}{\leq} W)) \to \neg F (P) \underset{˙}{\leq} W$
77	10 11 20 76	syl3anc	$⊢ ((K \in HL \land W \in H) \land (F \in T \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land (\neg Q \underset{˙}{\leq} (P \underset{˙}{\lor} F (P)) \land F (P) \neq P)) \to \neg F (P) \underset{˙}{\leq} W$
78		nbrne2	$⊢ (((P \underset{˙}{\lor} Q) \underset{˙}{\land} W) \underset{˙}{\leq} W \land \neg F (P) \underset{˙}{\leq} W) \to (P \underset{˙}{\lor} Q) \underset{˙}{\land} W \neq F (P)$
79	78	necomd	$⊢ (((P \underset{˙}{\lor} Q) \underset{˙}{\land} W) \underset{˙}{\leq} W \land \neg F (P) \underset{˙}{\leq} W) \to F (P) \neq (P \underset{˙}{\lor} Q) \underset{˙}{\land} W$
80	74 77 79	syl2anc	$⊢ ((K \in HL \land W \in H) \land (F \in T \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land (\neg Q \underset{˙}{\leq} (P \underset{˙}{\lor} F (P)) \land F (P) \neq P)) \to F (P) \neq (P \underset{˙}{\lor} Q) \underset{˙}{\land} W$
81	2 4 61	llni2	$⊢ ((K \in HL \land F (P) \in A \land (P \underset{˙}{\lor} Q) \underset{˙}{\land} W \in A) \land F (P) \neq (P \underset{˙}{\lor} Q) \underset{˙}{\land} W) \to F (P) \underset{˙}{\lor} ((P \underset{˙}{\lor} Q) \underset{˙}{\land} W) \in LLines (K)$
82	8 65 72 80 81	syl31anc	$⊢ ((K \in HL \land W \in H) \land (F \in T \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land (\neg Q \underset{˙}{\leq} (P \underset{˙}{\lor} F (P)) \land F (P) \neq P)) \to F (P) \underset{˙}{\lor} ((P \underset{˙}{\lor} Q) \underset{˙}{\land} W) \in LLines (K)$
83	1 2 3 4 5 6 7	cdlemc4	$⊢ ((K \in HL \land W \in H) \land (F \in T \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land \neg Q \underset{˙}{\leq} (P \underset{˙}{\lor} F (P))) \to Q \underset{˙}{\lor} R (F) \neq F (P) \underset{˙}{\lor} ((P \underset{˙}{\lor} Q) \underset{˙}{\land} W)$
84	83	3adant3r	$⊢ ((K \in HL \land W \in H) \land (F \in T \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land (\neg Q \underset{˙}{\leq} (P \underset{˙}{\lor} F (P)) \land F (P) \neq P)) \to Q \underset{˙}{\lor} R (F) \neq F (P) \underset{˙}{\lor} ((P \underset{˙}{\lor} Q) \underset{˙}{\land} W)$
85	24 3	latmcl	$⊢ (K \in Lat \land Q \underset{˙}{\lor} R (F) \in {Base}_{K} \land F (P) \underset{˙}{\lor} ((P \underset{˙}{\lor} Q) \underset{˙}{\land} W) \in {Base}_{K}) \to (Q \underset{˙}{\lor} R (F)) \underset{˙}{\land} (F (P) \underset{˙}{\lor} ((P \underset{˙}{\lor} Q) \underset{˙}{\land} W)) \in {Base}_{K}$
86	23 32 46 85	syl3anc	$⊢ ((K \in HL \land W \in H) \land (F \in T \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land (\neg Q \underset{˙}{\leq} (P \underset{˙}{\lor} F (P)) \land F (P) \neq P)) \to (Q \underset{˙}{\lor} R (F)) \underset{˙}{\land} (F (P) \underset{˙}{\lor} ((P \underset{˙}{\lor} Q) \underset{˙}{\land} W)) \in {Base}_{K}$
87		eqid	$⊢ 0. (K) = 0. (K)$
88	24 1 87 4	atlen0	$⊢ ((K \in AtLat \land (Q \underset{˙}{\lor} R (F)) \underset{˙}{\land} (F (P) \underset{˙}{\lor} ((P \underset{˙}{\lor} Q) \underset{˙}{\land} W)) \in {Base}_{K} \land F (Q) \in A) \land F (Q) \underset{˙}{\leq} ((Q \underset{˙}{\lor} R (F)) \underset{˙}{\land} (F (P) \underset{˙}{\lor} ((P \underset{˙}{\lor} Q) \underset{˙}{\land} W)))) \to (Q \underset{˙}{\lor} R (F)) \underset{˙}{\land} (F (P) \underset{˙}{\lor} ((P \underset{˙}{\lor} Q) \underset{˙}{\land} W)) \neq 0. (K)$
89	51 86 13 49 88	syl31anc	$⊢ ((K \in HL \land W \in H) \land (F \in T \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land (\neg Q \underset{˙}{\leq} (P \underset{˙}{\lor} F (P)) \land F (P) \neq P)) \to (Q \underset{˙}{\lor} R (F)) \underset{˙}{\land} (F (P) \underset{˙}{\lor} ((P \underset{˙}{\lor} Q) \underset{˙}{\land} W)) \neq 0. (K)$
90	3 87 4 61	2llnmat	$⊢ ((K \in HL \land Q \underset{˙}{\lor} R (F) \in LLines (K) \land F (P) \underset{˙}{\lor} ((P \underset{˙}{\lor} Q) \underset{˙}{\land} W) \in LLines (K)) \land (Q \underset{˙}{\lor} R (F) \neq F (P) \underset{˙}{\lor} ((P \underset{˙}{\lor} Q) \underset{˙}{\land} W) \land (Q \underset{˙}{\lor} R (F)) \underset{˙}{\land} (F (P) \underset{˙}{\lor} ((P \underset{˙}{\lor} Q) \underset{˙}{\land} W)) \neq 0. (K))) \to (Q \underset{˙}{\lor} R (F)) \underset{˙}{\land} (F (P) \underset{˙}{\lor} ((P \underset{˙}{\lor} Q) \underset{˙}{\land} W)) \in A$
91	8 63 82 84 89 90	syl32anc	$⊢ ((K \in HL \land W \in H) \land (F \in T \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land (\neg Q \underset{˙}{\leq} (P \underset{˙}{\lor} F (P)) \land F (P) \neq P)) \to (Q \underset{˙}{\lor} R (F)) \underset{˙}{\land} (F (P) \underset{˙}{\lor} ((P \underset{˙}{\lor} Q) \underset{˙}{\land} W)) \in A$
92	1 4	atcmp	$⊢ (K \in AtLat \land F (Q) \in A \land (Q \underset{˙}{\lor} R (F)) \underset{˙}{\land} (F (P) \underset{˙}{\lor} ((P \underset{˙}{\lor} Q) \underset{˙}{\land} W)) \in A) \to (F (Q) \underset{˙}{\leq} ((Q \underset{˙}{\lor} R (F)) \underset{˙}{\land} (F (P) \underset{˙}{\lor} ((P \underset{˙}{\lor} Q) \underset{˙}{\land} W))) \leftrightarrow F (Q) = (Q \underset{˙}{\lor} R (F)) \underset{˙}{\land} (F (P) \underset{˙}{\lor} ((P \underset{˙}{\lor} Q) \underset{˙}{\land} W)))$
93	51 13 91 92	syl3anc	$⊢ ((K \in HL \land W \in H) \land (F \in T \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land (\neg Q \underset{˙}{\leq} (P \underset{˙}{\lor} F (P)) \land F (P) \neq P)) \to (F (Q) \underset{˙}{\leq} ((Q \underset{˙}{\lor} R (F)) \underset{˙}{\land} (F (P) \underset{˙}{\lor} ((P \underset{˙}{\lor} Q) \underset{˙}{\land} W))) \leftrightarrow F (Q) = (Q \underset{˙}{\lor} R (F)) \underset{˙}{\land} (F (P) \underset{˙}{\lor} ((P \underset{˙}{\lor} Q) \underset{˙}{\land} W)))$
94	49 93	mpbid	$⊢ ((K \in HL \land W \in H) \land (F \in T \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \land (\neg Q \underset{˙}{\leq} (P \underset{˙}{\lor} F (P)) \land F (P) \neq P)) \to F (Q) = (Q \underset{˙}{\lor} R (F)) \underset{˙}{\land} (F (P) \underset{˙}{\lor} ((P \underset{˙}{\lor} Q) \underset{˙}{\land} W))$

Metamath Proof Explorer

Theorem cdlemc5

Proof