Theorem cdleme3c 40213

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

Hypotheses

Ref	Expression
cdleme1.l	⊢ ≤ = (le‘𝐾)
cdleme1.j	⊢ ∨ = (join‘𝐾)
cdleme1.m	⊢ ∧ = (meet‘𝐾)
cdleme1.a	⊢ 𝐴 = (Atoms‘𝐾)
cdleme1.h	⊢ 𝐻 = (LHyp‘𝐾)
cdleme1.u	⊢ 𝑈 = ((𝑃 ∨ 𝑄) ∧ 𝑊)
cdleme1.f	⊢ 𝐹 = ((𝑅 ∨ 𝑈) ∧ (𝑄 ∨ ((𝑃 ∨ 𝑅) ∧ 𝑊)))
cdleme3c.z	⊢ 0 = (0.‘𝐾)

Assertion

Ref	Expression
cdleme3c	⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ 𝑃 ≠ 𝑄) ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊))) → 𝐹 ≠ 0 )

Proof of Theorem cdleme3c

Step	Hyp	Ref	Expression
1		simpll 767	. . . 4 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ 𝑃 ≠ 𝑄) ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊))) → 𝐾 ∈ HL)
2		hllat 39345	. . . . . 6 ⊢ (𝐾 ∈ HL → 𝐾 ∈ Lat)
3	2	ad2antrr 726	. . . . 5 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ 𝑃 ≠ 𝑄) ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊))) → 𝐾 ∈ Lat)
4		simpr3l 1233	. . . . . 6 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ 𝑃 ≠ 𝑄) ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊))) → 𝑅 ∈ 𝐴)
5		eqid 2735	. . . . . . 7 ⊢ (Base‘𝐾) = (Base‘𝐾)
6		cdleme1.a	. . . . . . 7 ⊢ 𝐴 = (Atoms‘𝐾)
7	5, 6	atbase 39271	. . . . . 6 ⊢ (𝑅 ∈ 𝐴 → 𝑅 ∈ (Base‘𝐾))
8	4, 7	syl 17	. . . . 5 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ 𝑃 ≠ 𝑄) ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊))) → 𝑅 ∈ (Base‘𝐾))
9		hlop 39344	. . . . . . 7 ⊢ (𝐾 ∈ HL → 𝐾 ∈ OP)
10	9	ad2antrr 726	. . . . . 6 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ 𝑃 ≠ 𝑄) ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊))) → 𝐾 ∈ OP)
11		cdleme3c.z	. . . . . . 7 ⊢ 0 = (0.‘𝐾)
12	5, 11	op0cl 39166	. . . . . 6 ⊢ (𝐾 ∈ OP → 0 ∈ (Base‘𝐾))
13	10, 12	syl 17	. . . . 5 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ 𝑃 ≠ 𝑄) ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊))) → 0 ∈ (Base‘𝐾))
14		cdleme1.j	. . . . . 6 ⊢ ∨ = (join‘𝐾)
15	5, 14	latjcl 18497	. . . . 5 ⊢ ((𝐾 ∈ Lat ∧ 𝑅 ∈ (Base‘𝐾) ∧ 0 ∈ (Base‘𝐾)) → (𝑅 ∨ 0 ) ∈ (Base‘𝐾))
16	3, 8, 13, 15	syl3anc 1370	. . . 4 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ 𝑃 ≠ 𝑄) ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊))) → (𝑅 ∨ 0 ) ∈ (Base‘𝐾))
17		simpl 482	. . . . . 6 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ 𝑃 ≠ 𝑄) ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊))) → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))
18		simpr1l 1229	. . . . . 6 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ 𝑃 ≠ 𝑄) ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊))) → 𝑃 ∈ 𝐴)
19		simpr2l 1231	. . . . . 6 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ 𝑃 ≠ 𝑄) ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊))) → 𝑄 ∈ 𝐴)
20		cdleme1.l	. . . . . . 7 ⊢ ≤ = (le‘𝐾)
21		cdleme1.m	. . . . . . 7 ⊢ ∧ = (meet‘𝐾)
22		cdleme1.h	. . . . . . 7 ⊢ 𝐻 = (LHyp‘𝐾)
23		cdleme1.u	. . . . . . 7 ⊢ 𝑈 = ((𝑃 ∨ 𝑄) ∧ 𝑊)
24		cdleme1.f	. . . . . . 7 ⊢ 𝐹 = ((𝑅 ∨ 𝑈) ∧ (𝑄 ∨ ((𝑃 ∨ 𝑅) ∧ 𝑊)))
25	20, 14, 21, 6, 22, 23, 24, 5	cdleme1b 40209	. . . . . 6 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴)) → 𝐹 ∈ (Base‘𝐾))
26	17, 18, 19, 4, 25	syl13anc 1371	. . . . 5 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ 𝑃 ≠ 𝑄) ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊))) → 𝐹 ∈ (Base‘𝐾))
27	5, 14	latjcl 18497	. . . . 5 ⊢ ((𝐾 ∈ Lat ∧ 𝑅 ∈ (Base‘𝐾) ∧ 𝐹 ∈ (Base‘𝐾)) → (𝑅 ∨ 𝐹) ∈ (Base‘𝐾))
28	3, 8, 26, 27	syl3anc 1370	. . . 4 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ 𝑃 ≠ 𝑄) ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊))) → (𝑅 ∨ 𝐹) ∈ (Base‘𝐾))
29	5, 6	atbase 39271	. . . . . . . . . . . 12 ⊢ (𝑃 ∈ 𝐴 → 𝑃 ∈ (Base‘𝐾))
30	18, 29	syl 17	. . . . . . . . . . 11 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ 𝑃 ≠ 𝑄) ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊))) → 𝑃 ∈ (Base‘𝐾))
31	5, 6	atbase 39271	. . . . . . . . . . . 12 ⊢ (𝑄 ∈ 𝐴 → 𝑄 ∈ (Base‘𝐾))
32	19, 31	syl 17	. . . . . . . . . . 11 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ 𝑃 ≠ 𝑄) ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊))) → 𝑄 ∈ (Base‘𝐾))
33	5, 14	latjcl 18497	. . . . . . . . . . 11 ⊢ ((𝐾 ∈ Lat ∧ 𝑃 ∈ (Base‘𝐾) ∧ 𝑄 ∈ (Base‘𝐾)) → (𝑃 ∨ 𝑄) ∈ (Base‘𝐾))
34	3, 30, 32, 33	syl3anc 1370	. . . . . . . . . 10 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ 𝑃 ≠ 𝑄) ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊))) → (𝑃 ∨ 𝑄) ∈ (Base‘𝐾))
35	5, 22	lhpbase 39981	. . . . . . . . . . 11 ⊢ (𝑊 ∈ 𝐻 → 𝑊 ∈ (Base‘𝐾))
36	35	ad2antlr 727	. . . . . . . . . 10 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ 𝑃 ≠ 𝑄) ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊))) → 𝑊 ∈ (Base‘𝐾))
37	5, 20, 21	latmle2 18523	. . . . . . . . . 10 ⊢ ((𝐾 ∈ Lat ∧ (𝑃 ∨ 𝑄) ∈ (Base‘𝐾) ∧ 𝑊 ∈ (Base‘𝐾)) → ((𝑃 ∨ 𝑄) ∧ 𝑊) ≤ 𝑊)
38	3, 34, 36, 37	syl3anc 1370	. . . . . . . . 9 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ 𝑃 ≠ 𝑄) ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊))) → ((𝑃 ∨ 𝑄) ∧ 𝑊) ≤ 𝑊)
39	23, 38	eqbrtrid 5183	. . . . . . . 8 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ 𝑃 ≠ 𝑄) ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊))) → 𝑈 ≤ 𝑊)
40		simpr3r 1234	. . . . . . . 8 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ 𝑃 ≠ 𝑄) ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊))) → ¬ 𝑅 ≤ 𝑊)
41		nbrne2 5168	. . . . . . . 8 ⊢ ((𝑈 ≤ 𝑊 ∧ ¬ 𝑅 ≤ 𝑊) → 𝑈 ≠ 𝑅)
42	39, 40, 41	syl2anc 584	. . . . . . 7 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ 𝑃 ≠ 𝑄) ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊))) → 𝑈 ≠ 𝑅)
43	42	necomd 2994	. . . . . 6 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ 𝑃 ≠ 𝑄) ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊))) → 𝑅 ≠ 𝑈)
44	20, 14, 21, 6, 22, 23	lhpat2 40028	. . . . . . . 8 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ 𝑃 ≠ 𝑄)) → 𝑈 ∈ 𝐴)
45	44	3adant3r3 1183	. . . . . . 7 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ 𝑃 ≠ 𝑄) ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊))) → 𝑈 ∈ 𝐴)
46		eqid 2735	. . . . . . . 8 ⊢ ( ⋖ ‘𝐾) = ( ⋖ ‘𝐾)
47	14, 46, 6	atcvr1 39400	. . . . . . 7 ⊢ ((𝐾 ∈ HL ∧ 𝑅 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴) → (𝑅 ≠ 𝑈 ↔ 𝑅( ⋖ ‘𝐾)(𝑅 ∨ 𝑈)))
48	1, 4, 45, 47	syl3anc 1370	. . . . . 6 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ 𝑃 ≠ 𝑄) ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊))) → (𝑅 ≠ 𝑈 ↔ 𝑅( ⋖ ‘𝐾)(𝑅 ∨ 𝑈)))
49	43, 48	mpbid 232	. . . . 5 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ 𝑃 ≠ 𝑄) ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊))) → 𝑅( ⋖ ‘𝐾)(𝑅 ∨ 𝑈))
50		hlol 39343	. . . . . . 7 ⊢ (𝐾 ∈ HL → 𝐾 ∈ OL)
51	50	ad2antrr 726	. . . . . 6 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ 𝑃 ≠ 𝑄) ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊))) → 𝐾 ∈ OL)
52	5, 14, 11	olj01 39207	. . . . . 6 ⊢ ((𝐾 ∈ OL ∧ 𝑅 ∈ (Base‘𝐾)) → (𝑅 ∨ 0 ) = 𝑅)
53	51, 8, 52	syl2anc 584	. . . . 5 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ 𝑃 ≠ 𝑄) ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊))) → (𝑅 ∨ 0 ) = 𝑅)
54		simpr3 1195	. . . . . 6 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ 𝑃 ≠ 𝑄) ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊))) → (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊))
55	20, 14, 21, 6, 22, 23, 24	cdleme1 40210	. . . . . 6 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊))) → (𝑅 ∨ 𝐹) = (𝑅 ∨ 𝑈))
56	17, 18, 19, 54, 55	syl13anc 1371	. . . . 5 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ 𝑃 ≠ 𝑄) ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊))) → (𝑅 ∨ 𝐹) = (𝑅 ∨ 𝑈))
57	49, 53, 56	3brtr4d 5180	. . . 4 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ 𝑃 ≠ 𝑄) ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊))) → (𝑅 ∨ 0 )( ⋖ ‘𝐾)(𝑅 ∨ 𝐹))
58	5, 46	cvrne 39263	. . . 4 ⊢ (((𝐾 ∈ HL ∧ (𝑅 ∨ 0 ) ∈ (Base‘𝐾) ∧ (𝑅 ∨ 𝐹) ∈ (Base‘𝐾)) ∧ (𝑅 ∨ 0 )( ⋖ ‘𝐾)(𝑅 ∨ 𝐹)) → (𝑅 ∨ 0 ) ≠ (𝑅 ∨ 𝐹))
59	1, 16, 28, 57, 58	syl31anc 1372	. . 3 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ 𝑃 ≠ 𝑄) ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊))) → (𝑅 ∨ 0 ) ≠ (𝑅 ∨ 𝐹))
60		oveq2 7439	. . . 4 ⊢ ( 0 = 𝐹 → (𝑅 ∨ 0 ) = (𝑅 ∨ 𝐹))
61	60	necon3i 2971	. . 3 ⊢ ((𝑅 ∨ 0 ) ≠ (𝑅 ∨ 𝐹) → 0 ≠ 𝐹)
62	59, 61	syl 17	. 2 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ 𝑃 ≠ 𝑄) ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊))) → 0 ≠ 𝐹)
63	62	necomd 2994	1 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ 𝑃 ≠ 𝑄) ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊))) → 𝐹 ≠ 0 )

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 206   ∧ wa 395   ∧ w3a 1086   = wceq 1537   ∈ wcel 2106   ≠ wne 2938   class class class wbr 5148  ‘cfv 6563  (class class class)co 7431  Basecbs 17245  lecple 17305  joincjn 18369  meetcmee 18370  0.cp0 18481  Latclat 18489  OPcops 39154  OLcol 39156   ⋖ ccvr 39244  Atomscatm 39245  HLchlt 39332  LHypclh 39967

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-10 2139  ax-11 2155  ax-12 2175  ax-ext 2706  ax-rep 5285  ax-sep 5302  ax-nul 5312  ax-pow 5371  ax-pr 5438  ax-un 7754

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1540  df-fal 1550  df-ex 1777  df-nf 1781  df-sb 2063  df-mo 2538  df-eu 2567  df-clab 2713  df-cleq 2727  df-clel 2814  df-nfc 2890  df-ne 2939  df-ral 3060  df-rex 3069  df-rmo 3378  df-reu 3379  df-rab 3434  df-v 3480  df-sbc 3792  df-csb 3909  df-dif 3966  df-un 3968  df-in 3970  df-ss 3980  df-nul 4340  df-if 4532  df-pw 4607  df-sn 4632  df-pr 4634  df-op 4638  df-uni 4913  df-iun 4998  df-iin 4999  df-br 5149  df-opab 5211  df-mpt 5232  df-id 5583  df-xp 5695  df-rel 5696  df-cnv 5697  df-co 5698  df-dm 5699  df-rn 5700  df-res 5701  df-ima 5702  df-iota 6516  df-fun 6565  df-fn 6566  df-f 6567  df-f1 6568  df-fo 6569  df-f1o 6570  df-fv 6571  df-riota 7388  df-ov 7434  df-oprab 7435  df-mpo 7436  df-1st 8013  df-2nd 8014  df-proset 18352  df-poset 18371  df-plt 18388  df-lub 18404  df-glb 18405  df-join 18406  df-meet 18407  df-p0 18483  df-p1 18484  df-lat 18490  df-clat 18557  df-oposet 39158  df-ol 39160  df-oml 39161  df-covers 39248  df-ats 39249  df-atl 39280  df-cvlat 39304  df-hlat 39333  df-psubsp 39486  df-pmap 39487  df-padd 39779  df-lhyp 39971

This theorem is referenced by:  cdleme3h  40218