Theorem cdleme3c 37368

Description: Part of proof of Lemma E in [Crawley] p. 113. Lemma leading to cdleme3fa 37374 and cdleme3 37375. (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 765	. . . 4 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ 𝑃 ≠ 𝑄) ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊))) → 𝐾 ∈ HL)
2		hllat 36501	. . . . . 6 ⊢ (𝐾 ∈ HL → 𝐾 ∈ Lat)
3	2	ad2antrr 724	. . . . 5 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ 𝑃 ≠ 𝑄) ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊))) → 𝐾 ∈ Lat)
4		simpr3l 1230	. . . . . 6 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ 𝑃 ≠ 𝑄) ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊))) → 𝑅 ∈ 𝐴)
5		eqid 2823	. . . . . . 7 ⊢ (Base‘𝐾) = (Base‘𝐾)
6		cdleme1.a	. . . . . . 7 ⊢ 𝐴 = (Atoms‘𝐾)
7	5, 6	atbase 36427	. . . . . 6 ⊢ (𝑅 ∈ 𝐴 → 𝑅 ∈ (Base‘𝐾))
8	4, 7	syl 17	. . . . 5 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ 𝑃 ≠ 𝑄) ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊))) → 𝑅 ∈ (Base‘𝐾))
9		hlop 36500	. . . . . . 7 ⊢ (𝐾 ∈ HL → 𝐾 ∈ OP)
10	9	ad2antrr 724	. . . . . 6 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ 𝑃 ≠ 𝑄) ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊))) → 𝐾 ∈ OP)
11		cdleme3c.z	. . . . . . 7 ⊢ 0 = (0.‘𝐾)
12	5, 11	op0cl 36322	. . . . . 6 ⊢ (𝐾 ∈ OP → 0 ∈ (Base‘𝐾))
13	10, 12	syl 17	. . . . 5 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ 𝑃 ≠ 𝑄) ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊))) → 0 ∈ (Base‘𝐾))
14		cdleme1.j	. . . . . 6 ⊢ ∨ = (join‘𝐾)
15	5, 14	latjcl 17663	. . . . 5 ⊢ ((𝐾 ∈ Lat ∧ 𝑅 ∈ (Base‘𝐾) ∧ 0 ∈ (Base‘𝐾)) → (𝑅 ∨ 0 ) ∈ (Base‘𝐾))
16	3, 8, 13, 15	syl3anc 1367	. . . 4 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ 𝑃 ≠ 𝑄) ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊))) → (𝑅 ∨ 0 ) ∈ (Base‘𝐾))
17		simpl 485	. . . . . 6 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ 𝑃 ≠ 𝑄) ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊))) → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))
18		simpr1l 1226	. . . . . 6 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ 𝑃 ≠ 𝑄) ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊))) → 𝑃 ∈ 𝐴)
19		simpr2l 1228	. . . . . 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 37364	. . . . . 6 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴)) → 𝐹 ∈ (Base‘𝐾))
26	17, 18, 19, 4, 25	syl13anc 1368	. . . . 5 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ 𝑃 ≠ 𝑄) ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊))) → 𝐹 ∈ (Base‘𝐾))
27	5, 14	latjcl 17663	. . . . 5 ⊢ ((𝐾 ∈ Lat ∧ 𝑅 ∈ (Base‘𝐾) ∧ 𝐹 ∈ (Base‘𝐾)) → (𝑅 ∨ 𝐹) ∈ (Base‘𝐾))
28	3, 8, 26, 27	syl3anc 1367	. . . 4 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ 𝑃 ≠ 𝑄) ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊))) → (𝑅 ∨ 𝐹) ∈ (Base‘𝐾))
29	5, 6	atbase 36427	. . . . . . . . . . . 12 ⊢ (𝑃 ∈ 𝐴 → 𝑃 ∈ (Base‘𝐾))
30	18, 29	syl 17	. . . . . . . . . . 11 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ 𝑃 ≠ 𝑄) ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊))) → 𝑃 ∈ (Base‘𝐾))
31	5, 6	atbase 36427	. . . . . . . . . . . 12 ⊢ (𝑄 ∈ 𝐴 → 𝑄 ∈ (Base‘𝐾))
32	19, 31	syl 17	. . . . . . . . . . 11 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ 𝑃 ≠ 𝑄) ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊))) → 𝑄 ∈ (Base‘𝐾))
33	5, 14	latjcl 17663	. . . . . . . . . . 11 ⊢ ((𝐾 ∈ Lat ∧ 𝑃 ∈ (Base‘𝐾) ∧ 𝑄 ∈ (Base‘𝐾)) → (𝑃 ∨ 𝑄) ∈ (Base‘𝐾))
34	3, 30, 32, 33	syl3anc 1367	. . . . . . . . . 10 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ 𝑃 ≠ 𝑄) ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊))) → (𝑃 ∨ 𝑄) ∈ (Base‘𝐾))
35	5, 22	lhpbase 37136	. . . . . . . . . . 11 ⊢ (𝑊 ∈ 𝐻 → 𝑊 ∈ (Base‘𝐾))
36	35	ad2antlr 725	. . . . . . . . . 10 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ 𝑃 ≠ 𝑄) ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊))) → 𝑊 ∈ (Base‘𝐾))
37	5, 20, 21	latmle2 17689	. . . . . . . . . 10 ⊢ ((𝐾 ∈ Lat ∧ (𝑃 ∨ 𝑄) ∈ (Base‘𝐾) ∧ 𝑊 ∈ (Base‘𝐾)) → ((𝑃 ∨ 𝑄) ∧ 𝑊) ≤ 𝑊)
38	3, 34, 36, 37	syl3anc 1367	. . . . . . . . 9 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ 𝑃 ≠ 𝑄) ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊))) → ((𝑃 ∨ 𝑄) ∧ 𝑊) ≤ 𝑊)
39	23, 38	eqbrtrid 5103	. . . . . . . 8 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ 𝑃 ≠ 𝑄) ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊))) → 𝑈 ≤ 𝑊)
40		simpr3r 1231	. . . . . . . 8 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ 𝑃 ≠ 𝑄) ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊))) → ¬ 𝑅 ≤ 𝑊)
41		nbrne2 5088	. . . . . . . 8 ⊢ ((𝑈 ≤ 𝑊 ∧ ¬ 𝑅 ≤ 𝑊) → 𝑈 ≠ 𝑅)
42	39, 40, 41	syl2anc 586	. . . . . . 7 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ 𝑃 ≠ 𝑄) ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊))) → 𝑈 ≠ 𝑅)
43	42	necomd 3073	. . . . . 6 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ 𝑃 ≠ 𝑄) ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊))) → 𝑅 ≠ 𝑈)
44	20, 14, 21, 6, 22, 23	lhpat2 37183	. . . . . . . 8 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ 𝑃 ≠ 𝑄)) → 𝑈 ∈ 𝐴)
45	44	3adant3r3 1180	. . . . . . 7 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ 𝑃 ≠ 𝑄) ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊))) → 𝑈 ∈ 𝐴)
46		eqid 2823	. . . . . . . 8 ⊢ ( ⋖ ‘𝐾) = ( ⋖ ‘𝐾)
47	14, 46, 6	atcvr1 36555	. . . . . . 7 ⊢ ((𝐾 ∈ HL ∧ 𝑅 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴) → (𝑅 ≠ 𝑈 ↔ 𝑅( ⋖ ‘𝐾)(𝑅 ∨ 𝑈)))
48	1, 4, 45, 47	syl3anc 1367	. . . . . 6 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ 𝑃 ≠ 𝑄) ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊))) → (𝑅 ≠ 𝑈 ↔ 𝑅( ⋖ ‘𝐾)(𝑅 ∨ 𝑈)))
49	43, 48	mpbid 234	. . . . 5 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ 𝑃 ≠ 𝑄) ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊))) → 𝑅( ⋖ ‘𝐾)(𝑅 ∨ 𝑈))
50		hlol 36499	. . . . . . 7 ⊢ (𝐾 ∈ HL → 𝐾 ∈ OL)
51	50	ad2antrr 724	. . . . . 6 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ 𝑃 ≠ 𝑄) ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊))) → 𝐾 ∈ OL)
52	5, 14, 11	olj01 36363	. . . . . 6 ⊢ ((𝐾 ∈ OL ∧ 𝑅 ∈ (Base‘𝐾)) → (𝑅 ∨ 0 ) = 𝑅)
53	51, 8, 52	syl2anc 586	. . . . 5 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ 𝑃 ≠ 𝑄) ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊))) → (𝑅 ∨ 0 ) = 𝑅)
54		simpr3 1192	. . . . . 6 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ 𝑃 ≠ 𝑄) ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊))) → (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊))
55	20, 14, 21, 6, 22, 23, 24	cdleme1 37365	. . . . . 6 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊))) → (𝑅 ∨ 𝐹) = (𝑅 ∨ 𝑈))
56	17, 18, 19, 54, 55	syl13anc 1368	. . . . 5 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ 𝑃 ≠ 𝑄) ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊))) → (𝑅 ∨ 𝐹) = (𝑅 ∨ 𝑈))
57	49, 53, 56	3brtr4d 5100	. . . 4 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ 𝑃 ≠ 𝑄) ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊))) → (𝑅 ∨ 0 )( ⋖ ‘𝐾)(𝑅 ∨ 𝐹))
58	5, 46	cvrne 36419	. . . 4 ⊢ (((𝐾 ∈ HL ∧ (𝑅 ∨ 0 ) ∈ (Base‘𝐾) ∧ (𝑅 ∨ 𝐹) ∈ (Base‘𝐾)) ∧ (𝑅 ∨ 0 )( ⋖ ‘𝐾)(𝑅 ∨ 𝐹)) → (𝑅 ∨ 0 ) ≠ (𝑅 ∨ 𝐹))
59	1, 16, 28, 57, 58	syl31anc 1369	. . 3 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ 𝑃 ≠ 𝑄) ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊))) → (𝑅 ∨ 0 ) ≠ (𝑅 ∨ 𝐹))
60		oveq2 7166	. . . 4 ⊢ ( 0 = 𝐹 → (𝑅 ∨ 0 ) = (𝑅 ∨ 𝐹))
61	60	necon3i 3050	. . 3 ⊢ ((𝑅 ∨ 0 ) ≠ (𝑅 ∨ 𝐹) → 0 ≠ 𝐹)
62	59, 61	syl 17	. 2 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ 𝑃 ≠ 𝑄) ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊))) → 0 ≠ 𝐹)
63	62	necomd 3073	1 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ 𝑃 ≠ 𝑄) ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊))) → 𝐹 ≠ 0 )

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 208   ∧ wa 398   ∧ w3a 1083   = wceq 1537   ∈ wcel 2114   ≠ wne 3018   class class class wbr 5068  ‘cfv 6357  (class class class)co 7158  Basecbs 16485  lecple 16574  joincjn 17556  meetcmee 17557  0.cp0 17649  Latclat 17657  OPcops 36310  OLcol 36312   ⋖ ccvr 36400  Atomscatm 36401  HLchlt 36488  LHypclh 37122

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2795  ax-rep 5192  ax-sep 5205  ax-nul 5212  ax-pow 5268  ax-pr 5332  ax-un 7463

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1085  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-mo 2622  df-eu 2654  df-clab 2802  df-cleq 2816  df-clel 2895  df-nfc 2965  df-ne 3019  df-ral 3145  df-rex 3146  df-reu 3147  df-rab 3149  df-v 3498  df-sbc 3775  df-csb 3886  df-dif 3941  df-un 3943  df-in 3945  df-ss 3954  df-nul 4294  df-if 4470  df-pw 4543  df-sn 4570  df-pr 4572  df-op 4576  df-uni 4841  df-iun 4923  df-iin 4924  df-br 5069  df-opab 5131  df-mpt 5149  df-id 5462  df-xp 5563  df-rel 5564  df-cnv 5565  df-co 5566  df-dm 5567  df-rn 5568  df-res 5569  df-ima 5570  df-iota 6316  df-fun 6359  df-fn 6360  df-f 6361  df-f1 6362  df-fo 6363  df-f1o 6364  df-fv 6365  df-riota 7116  df-ov 7161  df-oprab 7162  df-mpo 7163  df-1st 7691  df-2nd 7692  df-proset 17540  df-poset 17558  df-plt 17570  df-lub 17586  df-glb 17587  df-join 17588  df-meet 17589  df-p0 17651  df-p1 17652  df-lat 17658  df-clat 17720  df-oposet 36314  df-ol 36316  df-oml 36317  df-covers 36404  df-ats 36405  df-atl 36436  df-cvlat 36460  df-hlat 36489  df-psubsp 36641  df-pmap 36642  df-padd 36934  df-lhyp 37126

This theorem is referenced by:  cdleme3h  37373