cdleme3h

Description: Part of proof of Lemma E in Crawley p. 113. Lemma leading to cdleme3fa and cdleme3 . (Contributed by NM, 6-Jun-2012)

	Ref	Expression
Hypotheses	cdleme1.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
	cdleme1.j	$⊢ \underset{˙}{\lor} = join (K)$
	cdleme1.m	$⊢ \underset{˙}{\land} = meet (K)$
	cdleme1.a	$⊢ A = Atoms (K)$
	cdleme1.h	$⊢ H = LHyp (K)$
	cdleme1.u	$⊢ U = (P \underset{˙}{\lor} Q) \underset{˙}{\land} W$
	cdleme1.f	$⊢ F = (R \underset{˙}{\lor} U) \underset{˙}{\land} (Q \underset{˙}{\lor} ((P \underset{˙}{\lor} R) \underset{˙}{\land} W))$
	cdleme3.3	$⊢ V = (P \underset{˙}{\lor} R) \underset{˙}{\land} W$
Assertion	cdleme3h	$⊢ ((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$

Proof

Step	Hyp	Ref	Expression
1		cdleme1.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
2		cdleme1.j	$⊢ \underset{˙}{\lor} = join (K)$
3		cdleme1.m	$⊢ \underset{˙}{\land} = meet (K)$
4		cdleme1.a	$⊢ A = Atoms (K)$
5		cdleme1.h	$⊢ H = LHyp (K)$
6		cdleme1.u	$⊢ U = (P \underset{˙}{\lor} Q) \underset{˙}{\land} W$
7		cdleme1.f	$⊢ F = (R \underset{˙}{\lor} U) \underset{˙}{\land} (Q \underset{˙}{\lor} ((P \underset{˙}{\lor} R) \underset{˙}{\land} W))$
8		cdleme3.3	$⊢ V = (P \underset{˙}{\lor} R) \underset{˙}{\land} W$
9	1 2 3 4 5 6 7 8	cdleme3d	$⊢ F = (R \underset{˙}{\lor} U) \underset{˙}{\land} (Q \underset{˙}{\lor} V)$
10		simp1l	$⊢ ((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 K \in HL$
11		simp23l	$⊢ ((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 R \in A$
12		simp1	$⊢ ((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 (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 \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 (P \in A \land \neg P \underset{˙}{\leq} W)$
14		simp22l	$⊢ ((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 Q \in A$
15		simp3l	$⊢ ((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 P \neq Q$
16	1 2 3 4 5 6	lhpat2	$⊢ ((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$
17	12 13 14 15 16	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 (R \in A \land \neg R \underset{˙}{\leq} W)) \land (P \neq Q \land \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \to U \in A$
18		eqid	$⊢ {Base}_{K} = {Base}_{K}$
19	18 2 4	hlatjcl	$⊢ (K \in HL \land R \in A \land U \in A) \to R \underset{˙}{\lor} U \in {Base}_{K}$
20	10 11 17 19	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 (R \in A \land \neg R \underset{˙}{\leq} W)) \land (P \neq Q \land \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \to R \underset{˙}{\lor} U \in {Base}_{K}$
21		simp3r	$⊢ ((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 \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q)$
22	11 21	jca	$⊢ ((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 (R \in A \land \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q))$
23	1 2 3 4 5 6 7 8	cdleme3e	$⊢ ((K \in HL \land W \in H) \land ((P \in A \land \neg P \underset{˙}{\leq} W) \land Q \in A \land (R \in A \land \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q)))) \to V \in A$
24	12 13 14 22 23	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 (R \in A \land \neg R \underset{˙}{\leq} W)) \land (P \neq Q \land \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \to V \in A$
25	18 2 4	hlatjcl	$⊢ (K \in HL \land Q \in A \land V \in A) \to Q \underset{˙}{\lor} V \in {Base}_{K}$
26	10 14 24 25	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 (R \in A \land \neg R \underset{˙}{\leq} W)) \land (P \neq Q \land \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \to Q \underset{˙}{\lor} V \in {Base}_{K}$
27	10	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 (R \in A \land \neg R \underset{˙}{\leq} W)) \land (P \neq Q \land \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \to K \in Lat$
28		simp21l	$⊢ ((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 P \in A$
29	18 2 4	hlatjcl	$⊢ (K \in HL \land P \in A \land Q \in A) \to P \underset{˙}{\lor} Q \in {Base}_{K}$
30	10 28 14 29	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 (R \in A \land \neg R \underset{˙}{\leq} W)) \land (P \neq Q \land \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \to P \underset{˙}{\lor} Q \in {Base}_{K}$
31		simp1r	$⊢ ((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 W \in H$
32	18 5	lhpbase	$⊢ W \in H \to W \in {Base}_{K}$
33	31 32	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 (R \in A \land \neg R \underset{˙}{\leq} W)) \land (P \neq Q \land \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \to W \in {Base}_{K}$
34	18 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$
35	27 30 33 34	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 (R \in A \land \neg R \underset{˙}{\leq} W)) \land (P \neq Q \land \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \to ((P \underset{˙}{\lor} Q) \underset{˙}{\land} W) \underset{˙}{\leq} W$
36	6 35	eqbrtrid	$⊢ ((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 U \underset{˙}{\leq} W$
37		simp23r	$⊢ ((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 \neg R \underset{˙}{\leq} W$
38		nbrne2	$⊢ (U \underset{˙}{\leq} W \land \neg R \underset{˙}{\leq} W) \to U \neq R$
39	36 37 38	syl2anc	$⊢ ((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 U \neq R$
40	39	necomd	$⊢ ((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 R \neq U$
41		eqid	$⊢ Lines (K) = Lines (K)$
42		eqid	$⊢ pmap (K) = pmap (K)$
43	2 4 41 42	linepmap	$⊢ ((K \in Lat \land R \in A \land U \in A) \land R \neq U) \to pmap (K) (R \underset{˙}{\lor} U) \in Lines (K)$
44	27 11 17 40 43	syl31anc	$⊢ ((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 pmap (K) (R \underset{˙}{\lor} U) \in Lines (K)$
45	18 2 4	hlatjcl	$⊢ (K \in HL \land P \in A \land R \in A) \to P \underset{˙}{\lor} R \in {Base}_{K}$
46	10 28 11 45	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 (R \in A \land \neg R \underset{˙}{\leq} W)) \land (P \neq Q \land \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \to P \underset{˙}{\lor} R \in {Base}_{K}$
47	18 1 3	latmle2	$⊢ (K \in Lat \land P \underset{˙}{\lor} R \in {Base}_{K} \land W \in {Base}_{K}) \to ((P \underset{˙}{\lor} R) \underset{˙}{\land} W) \underset{˙}{\leq} W$
48	27 46 33 47	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 (R \in A \land \neg R \underset{˙}{\leq} W)) \land (P \neq Q \land \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \to ((P \underset{˙}{\lor} R) \underset{˙}{\land} W) \underset{˙}{\leq} W$
49	8 48	eqbrtrid	$⊢ ((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 V \underset{˙}{\leq} W$
50		simp22r	$⊢ ((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 \neg Q \underset{˙}{\leq} W$
51		nbrne2	$⊢ (V \underset{˙}{\leq} W \land \neg Q \underset{˙}{\leq} W) \to V \neq Q$
52	49 50 51	syl2anc	$⊢ ((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 V \neq Q$
53	52	necomd	$⊢ ((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 Q \neq V$
54	2 4 41 42	linepmap	$⊢ ((K \in Lat \land Q \in A \land V \in A) \land Q \neq V) \to pmap (K) (Q \underset{˙}{\lor} V) \in Lines (K)$
55	27 14 24 53 54	syl31anc	$⊢ ((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 pmap (K) (Q \underset{˙}{\lor} V) \in Lines (K)$
56	1 2 4	hlatlej1	$⊢ (K \in HL \land R \in A \land U \in A) \to R \underset{˙}{\leq} (R \underset{˙}{\lor} U)$
57	10 11 17 56	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 (R \in A \land \neg R \underset{˙}{\leq} W)) \land (P \neq Q \land \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \to R \underset{˙}{\leq} (R \underset{˙}{\lor} U)$
58		nbrne2	$⊢ (V \underset{˙}{\leq} W \land \neg R \underset{˙}{\leq} W) \to V \neq R$
59	49 37 58	syl2anc	$⊢ ((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 V \neq R$
60	59	necomd	$⊢ ((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 R \neq V$
61	1 2 4	hlatexch2	$⊢ (K \in HL \land (R \in A \land Q \in A \land V \in A) \land R \neq V) \to (R \underset{˙}{\leq} (Q \underset{˙}{\lor} V) \to Q \underset{˙}{\leq} (R \underset{˙}{\lor} V))$
62	10 11 14 24 60 61	syl131anc	$⊢ ((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 (R \underset{˙}{\leq} (Q \underset{˙}{\lor} V) \to Q \underset{˙}{\leq} (R \underset{˙}{\lor} V))$
63	8	oveq2i	$⊢ R \underset{˙}{\lor} V = R \underset{˙}{\lor} ((P \underset{˙}{\lor} R) \underset{˙}{\land} W)$
64	1 2 4	hlatlej2	$⊢ (K \in HL \land P \in A \land R \in A) \to R \underset{˙}{\leq} (P \underset{˙}{\lor} R)$
65	10 28 11 64	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 (R \in A \land \neg R \underset{˙}{\leq} W)) \land (P \neq Q \land \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \to R \underset{˙}{\leq} (P \underset{˙}{\lor} R)$
66	18 1 3	latmle1	$⊢ (K \in Lat \land P \underset{˙}{\lor} R \in {Base}_{K} \land W \in {Base}_{K}) \to ((P \underset{˙}{\lor} R) \underset{˙}{\land} W) \underset{˙}{\leq} (P \underset{˙}{\lor} R)$
67	27 46 33 66	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 (R \in A \land \neg R \underset{˙}{\leq} W)) \land (P \neq Q \land \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \to ((P \underset{˙}{\lor} R) \underset{˙}{\land} W) \underset{˙}{\leq} (P \underset{˙}{\lor} R)$
68	18 4	atbase	$⊢ R \in A \to R \in {Base}_{K}$
69	11 68	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 (R \in A \land \neg R \underset{˙}{\leq} W)) \land (P \neq Q \land \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \to R \in {Base}_{K}$
70	18 3	latmcl	$⊢ (K \in Lat \land P \underset{˙}{\lor} R \in {Base}_{K} \land W \in {Base}_{K}) \to (P \underset{˙}{\lor} R) \underset{˙}{\land} W \in {Base}_{K}$
71	27 46 33 70	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 (R \in A \land \neg R \underset{˙}{\leq} W)) \land (P \neq Q \land \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \to (P \underset{˙}{\lor} R) \underset{˙}{\land} W \in {Base}_{K}$
72	18 1 2	latjle12	$⊢ (K \in Lat \land (R \in {Base}_{K} \land (P \underset{˙}{\lor} R) \underset{˙}{\land} W \in {Base}_{K} \land P \underset{˙}{\lor} R \in {Base}_{K})) \to ((R \underset{˙}{\leq} (P \underset{˙}{\lor} R) \land ((P \underset{˙}{\lor} R) \underset{˙}{\land} W) \underset{˙}{\leq} (P \underset{˙}{\lor} R)) \leftrightarrow (R \underset{˙}{\lor} ((P \underset{˙}{\lor} R) \underset{˙}{\land} W)) \underset{˙}{\leq} (P \underset{˙}{\lor} R))$
73	27 69 71 46 72	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 (R \in A \land \neg R \underset{˙}{\leq} W)) \land (P \neq Q \land \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \to ((R \underset{˙}{\leq} (P \underset{˙}{\lor} R) \land ((P \underset{˙}{\lor} R) \underset{˙}{\land} W) \underset{˙}{\leq} (P \underset{˙}{\lor} R)) \leftrightarrow (R \underset{˙}{\lor} ((P \underset{˙}{\lor} R) \underset{˙}{\land} W)) \underset{˙}{\leq} (P \underset{˙}{\lor} R))$
74	65 67 73	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 (R \in A \land \neg R \underset{˙}{\leq} W)) \land (P \neq Q \land \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \to (R \underset{˙}{\lor} ((P \underset{˙}{\lor} R) \underset{˙}{\land} W)) \underset{˙}{\leq} (P \underset{˙}{\lor} R)$
75	63 74	eqbrtrid	$⊢ ((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 (R \underset{˙}{\lor} V) \underset{˙}{\leq} (P \underset{˙}{\lor} R)$
76	18 4	atbase	$⊢ Q \in A \to Q \in {Base}_{K}$
77	14 76	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 (R \in A \land \neg R \underset{˙}{\leq} W)) \land (P \neq Q \land \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \to Q \in {Base}_{K}$
78	18 2 4	hlatjcl	$⊢ (K \in HL \land R \in A \land V \in A) \to R \underset{˙}{\lor} V \in {Base}_{K}$
79	10 11 24 78	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 (R \in A \land \neg R \underset{˙}{\leq} W)) \land (P \neq Q \land \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \to R \underset{˙}{\lor} V \in {Base}_{K}$
80	18 1	lattr	$⊢ (K \in Lat \land (Q \in {Base}_{K} \land R \underset{˙}{\lor} V \in {Base}_{K} \land P \underset{˙}{\lor} R \in {Base}_{K})) \to ((Q \underset{˙}{\leq} (R \underset{˙}{\lor} V) \land (R \underset{˙}{\lor} V) \underset{˙}{\leq} (P \underset{˙}{\lor} R)) \to Q \underset{˙}{\leq} (P \underset{˙}{\lor} R))$
81	27 77 79 46 80	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 (R \in A \land \neg R \underset{˙}{\leq} W)) \land (P \neq Q \land \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q))) \to ((Q \underset{˙}{\leq} (R \underset{˙}{\lor} V) \land (R \underset{˙}{\lor} V) \underset{˙}{\leq} (P \underset{˙}{\lor} R)) \to Q \underset{˙}{\leq} (P \underset{˙}{\lor} R))$
82	75 81	mpan2d	$⊢ ((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 (Q \underset{˙}{\leq} (R \underset{˙}{\lor} V) \to Q \underset{˙}{\leq} (P \underset{˙}{\lor} R))$
83	15	necomd	$⊢ ((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 Q \neq P$
84	1 2 4	hlatexch1	$⊢ (K \in HL \land (Q \in A \land R \in A \land P \in A) \land Q \neq P) \to (Q \underset{˙}{\leq} (P \underset{˙}{\lor} R) \to R \underset{˙}{\leq} (P \underset{˙}{\lor} Q))$
85	10 14 11 28 83 84	syl131anc	$⊢ ((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 (Q \underset{˙}{\leq} (P \underset{˙}{\lor} R) \to R \underset{˙}{\leq} (P \underset{˙}{\lor} Q))$
86	62 82 85	3syld	$⊢ ((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 (R \underset{˙}{\leq} (Q \underset{˙}{\lor} V) \to R \underset{˙}{\leq} (P \underset{˙}{\lor} Q))$
87	21 86	mtod	$⊢ ((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 \neg R \underset{˙}{\leq} (Q \underset{˙}{\lor} V)$
88		nbrne1	$⊢ (R \underset{˙}{\leq} (R \underset{˙}{\lor} U) \land \neg R \underset{˙}{\leq} (Q \underset{˙}{\lor} V)) \to R \underset{˙}{\lor} U \neq Q \underset{˙}{\lor} V$
89	57 87 88	syl2anc	$⊢ ((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 R \underset{˙}{\lor} U \neq Q \underset{˙}{\lor} V$
90	14 15	jca	$⊢ ((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 (Q \in A \land P \neq Q)$
91		simp23	$⊢ ((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 (R \in A \land \neg R \underset{˙}{\leq} W)$
92		eqid	$⊢ 0. (K) = 0. (K)$
93	1 2 3 4 5 6 7 92	cdleme3c	$⊢ ((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) \land (R \in A \land \neg R \underset{˙}{\leq} W))) \to F \neq 0. (K)$
94	12 13 90 91 93	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 (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 0. (K)$
95	9 94	eqnetrrid	$⊢ ((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 (R \underset{˙}{\lor} U) \underset{˙}{\land} (Q \underset{˙}{\lor} V) \neq 0. (K)$
96	18 3 92 4 41 42	2lnat	$⊢ ((K \in HL \land R \underset{˙}{\lor} U \in {Base}_{K} \land Q \underset{˙}{\lor} V \in {Base}_{K}) \land (pmap (K) (R \underset{˙}{\lor} U) \in Lines (K) \land pmap (K) (Q \underset{˙}{\lor} V) \in Lines (K)) \land (R \underset{˙}{\lor} U \neq Q \underset{˙}{\lor} V \land (R \underset{˙}{\lor} U) \underset{˙}{\land} (Q \underset{˙}{\lor} V) \neq 0. (K))) \to (R \underset{˙}{\lor} U) \underset{˙}{\land} (Q \underset{˙}{\lor} V) \in A$
97	10 20 26 44 55 89 95 96	syl322anc	$⊢ ((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 (R \underset{˙}{\lor} U) \underset{˙}{\land} (Q \underset{˙}{\lor} V) \in A$
98	9 97	eqeltrid	$⊢ ((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$

Metamath Proof Explorer

Theorem cdleme3h

Proof