Step | Hyp | Ref
| Expression |
1 | | cdleme40.b |
. . . 4
β’ π΅ = (BaseβπΎ) |
2 | 1 | fvexi 6857 |
. . 3
β’ π΅ β V |
3 | | nfv 1918 |
. . . 4
β’
β²π£(((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β π β§ (π
β π΄ β§ Β¬ π
β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π
β€ (π β¨ π) β§ π β€ (π β¨ π) β§ π
β π)) |
4 | | nfcv 2904 |
. . . . . 6
β’
β²π£β¦π
/ π β¦π |
5 | | cdleme40a1.z |
. . . . . . 7
β’ π = (β©π§ β π΅ βπ£ β π΄ ((Β¬ π£ β€ π β§ Β¬ π£ β€ (π β¨ π)) β π§ = πΉ)) |
6 | | nfra1 3266 |
. . . . . . . 8
β’
β²π£βπ£ β π΄ ((Β¬ π£ β€ π β§ Β¬ π£ β€ (π β¨ π)) β π§ = πΉ) |
7 | | nfcv 2904 |
. . . . . . . 8
β’
β²π£π΅ |
8 | 6, 7 | nfriota 7327 |
. . . . . . 7
β’
β²π£(β©π§ β π΅ βπ£ β π΄ ((Β¬ π£ β€ π β§ Β¬ π£ β€ (π β¨ π)) β π§ = πΉ)) |
9 | 5, 8 | nfcxfr 2902 |
. . . . . 6
β’
β²π£π |
10 | 4, 9 | nfne 3042 |
. . . . 5
β’
β²π£β¦π
/ π β¦π β π |
11 | 10 | a1i 11 |
. . . 4
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β π β§ (π
β π΄ β§ Β¬ π
β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π
β€ (π β¨ π) β§ π β€ (π β¨ π) β§ π
β π)) β β²π£β¦π
/ π β¦π β π) |
12 | 5 | a1i 11 |
. . . 4
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β π β§ (π
β π΄ β§ Β¬ π
β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π
β€ (π β¨ π) β§ π β€ (π β¨ π) β§ π
β π)) β π = (β©π§ β π΅ βπ£ β π΄ ((Β¬ π£ β€ π β§ Β¬ π£ β€ (π β¨ π)) β π§ = πΉ))) |
13 | | neeq2 3004 |
. . . . 5
β’ (πΉ = π β (β¦π
/ π β¦π β πΉ β β¦π
/ π β¦π β π)) |
14 | 13 | adantl 483 |
. . . 4
β’
(((((πΎ β HL
β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β π β§ (π
β π΄ β§ Β¬ π
β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π
β€ (π β¨ π) β§ π β€ (π β¨ π) β§ π
β π)) β§ πΉ = π) β (β¦π
/ π β¦π β πΉ β β¦π
/ π β¦π β π)) |
15 | | simpl11 1249 |
. . . . . 6
β’
(((((πΎ β HL
β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β π β§ (π
β π΄ β§ Β¬ π
β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π
β€ (π β¨ π) β§ π β€ (π β¨ π) β§ π
β π)) β§ (π£ β π΄ β§ (Β¬ π£ β€ π β§ Β¬ π£ β€ (π β¨ π)))) β (πΎ β HL β§ π β π»)) |
16 | | simpl12 1250 |
. . . . . 6
β’
(((((πΎ β HL
β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β π β§ (π
β π΄ β§ Β¬ π
β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π
β€ (π β¨ π) β§ π β€ (π β¨ π) β§ π
β π)) β§ (π£ β π΄ β§ (Β¬ π£ β€ π β§ Β¬ π£ β€ (π β¨ π)))) β (π β π΄ β§ Β¬ π β€ π)) |
17 | | simpl13 1251 |
. . . . . 6
β’
(((((πΎ β HL
β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β π β§ (π
β π΄ β§ Β¬ π
β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π
β€ (π β¨ π) β§ π β€ (π β¨ π) β§ π
β π)) β§ (π£ β π΄ β§ (Β¬ π£ β€ π β§ Β¬ π£ β€ (π β¨ π)))) β (π β π΄ β§ Β¬ π β€ π)) |
18 | | simpl21 1252 |
. . . . . 6
β’
(((((πΎ β HL
β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β π β§ (π
β π΄ β§ Β¬ π
β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π
β€ (π β¨ π) β§ π β€ (π β¨ π) β§ π
β π)) β§ (π£ β π΄ β§ (Β¬ π£ β€ π β§ Β¬ π£ β€ (π β¨ π)))) β π β π) |
19 | | simpl22 1253 |
. . . . . 6
β’
(((((πΎ β HL
β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β π β§ (π
β π΄ β§ Β¬ π
β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π
β€ (π β¨ π) β§ π β€ (π β¨ π) β§ π
β π)) β§ (π£ β π΄ β§ (Β¬ π£ β€ π β§ Β¬ π£ β€ (π β¨ π)))) β (π
β π΄ β§ Β¬ π
β€ π)) |
20 | | simpl23 1254 |
. . . . . 6
β’
(((((πΎ β HL
β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β π β§ (π
β π΄ β§ Β¬ π
β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π
β€ (π β¨ π) β§ π β€ (π β¨ π) β§ π
β π)) β§ (π£ β π΄ β§ (Β¬ π£ β€ π β§ Β¬ π£ β€ (π β¨ π)))) β (π β π΄ β§ Β¬ π β€ π)) |
21 | | simpl3 1194 |
. . . . . 6
β’
(((((πΎ β HL
β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β π β§ (π
β π΄ β§ Β¬ π
β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π
β€ (π β¨ π) β§ π β€ (π β¨ π) β§ π
β π)) β§ (π£ β π΄ β§ (Β¬ π£ β€ π β§ Β¬ π£ β€ (π β¨ π)))) β (π
β€ (π β¨ π) β§ π β€ (π β¨ π) β§ π
β π)) |
22 | | simprl 770 |
. . . . . . 7
β’
(((((πΎ β HL
β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β π β§ (π
β π΄ β§ Β¬ π
β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π
β€ (π β¨ π) β§ π β€ (π β¨ π) β§ π
β π)) β§ (π£ β π΄ β§ (Β¬ π£ β€ π β§ Β¬ π£ β€ (π β¨ π)))) β π£ β π΄) |
23 | | simprrl 780 |
. . . . . . 7
β’
(((((πΎ β HL
β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β π β§ (π
β π΄ β§ Β¬ π
β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π
β€ (π β¨ π) β§ π β€ (π β¨ π) β§ π
β π)) β§ (π£ β π΄ β§ (Β¬ π£ β€ π β§ Β¬ π£ β€ (π β¨ π)))) β Β¬ π£ β€ π) |
24 | | simprrr 781 |
. . . . . . 7
β’
(((((πΎ β HL
β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β π β§ (π
β π΄ β§ Β¬ π
β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π
β€ (π β¨ π) β§ π β€ (π β¨ π) β§ π
β π)) β§ (π£ β π΄ β§ (Β¬ π£ β€ π β§ Β¬ π£ β€ (π β¨ π)))) β Β¬ π£ β€ (π β¨ π)) |
25 | 22, 23, 24 | 3jca 1129 |
. . . . . 6
β’
(((((πΎ β HL
β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β π β§ (π
β π΄ β§ Β¬ π
β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π
β€ (π β¨ π) β§ π β€ (π β¨ π) β§ π
β π)) β§ (π£ β π΄ β§ (Β¬ π£ β€ π β§ Β¬ π£ β€ (π β¨ π)))) β (π£ β π΄ β§ Β¬ π£ β€ π β§ Β¬ π£ β€ (π β¨ π))) |
26 | | cdleme40.l |
. . . . . . 7
β’ β€ =
(leβπΎ) |
27 | | cdleme40.j |
. . . . . . 7
β’ β¨ =
(joinβπΎ) |
28 | | cdleme40.m |
. . . . . . 7
β’ β§ =
(meetβπΎ) |
29 | | cdleme40.a |
. . . . . . 7
β’ π΄ = (AtomsβπΎ) |
30 | | cdleme40.h |
. . . . . . 7
β’ π» = (LHypβπΎ) |
31 | | cdleme40.u |
. . . . . . 7
β’ π = ((π β¨ π) β§ π) |
32 | | cdleme40.e |
. . . . . . 7
β’ πΈ = ((π‘ β¨ π) β§ (π β¨ ((π β¨ π‘) β§ π))) |
33 | | cdleme40.g |
. . . . . . 7
β’ πΊ = ((π β¨ π) β§ (πΈ β¨ ((π β¨ π‘) β§ π))) |
34 | | cdleme40.i |
. . . . . . 7
β’ πΌ = (β©π¦ β π΅ βπ‘ β π΄ ((Β¬ π‘ β€ π β§ Β¬ π‘ β€ (π β¨ π)) β π¦ = πΊ)) |
35 | | cdleme40.n |
. . . . . . 7
β’ π = if(π β€ (π β¨ π), πΌ, π·) |
36 | | cdleme40a1.y |
. . . . . . 7
β’ π = ((π β¨ π) β§ (πΈ β¨ ((π
β¨ π‘) β§ π))) |
37 | | cdleme40a1.c |
. . . . . . 7
β’ πΆ = (β©π¦ β π΅ βπ‘ β π΄ ((Β¬ π‘ β€ π β§ Β¬ π‘ β€ (π β¨ π)) β π¦ = π)) |
38 | | cdleme40.t |
. . . . . . 7
β’ π = ((π£ β¨ π) β§ (π β¨ ((π β¨ π£) β§ π))) |
39 | | cdleme40.f |
. . . . . . 7
β’ πΉ = ((π β¨ π) β§ (π β¨ ((π β¨ π£) β§ π))) |
40 | 1, 26, 27, 28, 29, 30, 31, 32, 33, 34, 35, 36, 37, 38, 39 | cdleme40m 38976 |
. . . . . 6
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β π β§ (π
β π΄ β§ Β¬ π
β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ ((π
β€ (π β¨ π) β§ π β€ (π β¨ π) β§ π
β π) β§ (π£ β π΄ β§ Β¬ π£ β€ π β§ Β¬ π£ β€ (π β¨ π)))) β β¦π
/ π β¦π β πΉ) |
41 | 15, 16, 17, 18, 19, 20, 21, 25, 40 | syl332anc 1402 |
. . . . 5
β’
(((((πΎ β HL
β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β π β§ (π
β π΄ β§ Β¬ π
β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π
β€ (π β¨ π) β§ π β€ (π β¨ π) β§ π
β π)) β§ (π£ β π΄ β§ (Β¬ π£ β€ π β§ Β¬ π£ β€ (π β¨ π)))) β β¦π
/ π β¦π β πΉ) |
42 | 41 | ex 414 |
. . . 4
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β π β§ (π
β π΄ β§ Β¬ π
β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π
β€ (π β¨ π) β§ π β€ (π β¨ π) β§ π
β π)) β ((π£ β π΄ β§ (Β¬ π£ β€ π β§ Β¬ π£ β€ (π β¨ π))) β β¦π
/ π β¦π β πΉ)) |
43 | | simp1 1137 |
. . . . 5
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β π β§ (π
β π΄ β§ Β¬ π
β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π
β€ (π β¨ π) β§ π β€ (π β¨ π) β§ π
β π)) β ((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π))) |
44 | | simp23l 1295 |
. . . . 5
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β π β§ (π
β π΄ β§ Β¬ π
β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π
β€ (π β¨ π) β§ π β€ (π β¨ π) β§ π
β π)) β π β π΄) |
45 | | simp23r 1296 |
. . . . 5
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β π β§ (π
β π΄ β§ Β¬ π
β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π
β€ (π β¨ π) β§ π β€ (π β¨ π) β§ π
β π)) β Β¬ π β€ π) |
46 | | simp21 1207 |
. . . . 5
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β π β§ (π
β π΄ β§ Β¬ π
β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π
β€ (π β¨ π) β§ π β€ (π β¨ π) β§ π
β π)) β π β π) |
47 | | simp32 1211 |
. . . . 5
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β π β§ (π
β π΄ β§ Β¬ π
β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π
β€ (π β¨ π) β§ π β€ (π β¨ π) β§ π
β π)) β π β€ (π β¨ π)) |
48 | 1, 26, 27, 28, 29, 30, 31, 38, 39, 5 | cdleme25cl 38866 |
. . . . 5
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π β§ π β€ (π β¨ π))) β π β π΅) |
49 | 43, 44, 45, 46, 47, 48 | syl122anc 1380 |
. . . 4
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β π β§ (π
β π΄ β§ Β¬ π
β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π
β€ (π β¨ π) β§ π β€ (π β¨ π) β§ π
β π)) β π β π΅) |
50 | | simp11 1204 |
. . . . 5
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β π β§ (π
β π΄ β§ Β¬ π
β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π
β€ (π β¨ π) β§ π β€ (π β¨ π) β§ π
β π)) β (πΎ β HL β§ π β π»)) |
51 | | simp12 1205 |
. . . . 5
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β π β§ (π
β π΄ β§ Β¬ π
β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π
β€ (π β¨ π) β§ π β€ (π β¨ π) β§ π
β π)) β (π β π΄ β§ Β¬ π β€ π)) |
52 | | simp13 1206 |
. . . . 5
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β π β§ (π
β π΄ β§ Β¬ π
β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π
β€ (π β¨ π) β§ π β€ (π β¨ π) β§ π
β π)) β (π β π΄ β§ Β¬ π β€ π)) |
53 | 26, 27, 29, 30 | cdlemb2 38550 |
. . . . 5
β’ (((πΎ β HL β§ π β π») β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ π β π) β βπ£ β π΄ (Β¬ π£ β€ π β§ Β¬ π£ β€ (π β¨ π))) |
54 | 50, 51, 52, 46, 53 | syl121anc 1376 |
. . . 4
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β π β§ (π
β π΄ β§ Β¬ π
β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π
β€ (π β¨ π) β§ π β€ (π β¨ π) β§ π
β π)) β βπ£ β π΄ (Β¬ π£ β€ π β§ Β¬ π£ β€ (π β¨ π))) |
55 | 3, 11, 12, 14, 42, 49, 54 | riotasv3d 37468 |
. . 3
β’
(((((πΎ β HL
β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β π β§ (π
β π΄ β§ Β¬ π
β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π
β€ (π β¨ π) β§ π β€ (π β¨ π) β§ π
β π)) β§ π΅ β V) β β¦π
/ π β¦π β π) |
56 | 2, 55 | mpan2 690 |
. 2
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β π β§ (π
β π΄ β§ Β¬ π
β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π
β€ (π β¨ π) β§ π β€ (π β¨ π) β§ π
β π)) β β¦π
/ π β¦π β π) |
57 | | cdleme40a1.x |
. . . 4
β’ π = ((π β¨ π) β§ (π β¨ ((π’ β¨ π£) β§ π))) |
58 | | cdleme40.o |
. . . 4
β’ π = (β©π§ β π΅ βπ£ β π΄ ((Β¬ π£ β€ π β§ Β¬ π£ β€ (π β¨ π)) β π§ = π)) |
59 | | cdleme40.v |
. . . 4
β’ π = if(π’ β€ (π β¨ π), π, < ) |
60 | 57, 58, 59, 39, 5 | cdleme31sn1c 38897 |
. . 3
β’ ((π β π΄ β§ π β€ (π β¨ π)) β β¦π / π’β¦π = π) |
61 | 44, 47, 60 | syl2anc 585 |
. 2
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β π β§ (π
β π΄ β§ Β¬ π
β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π
β€ (π β¨ π) β§ π β€ (π β¨ π) β§ π
β π)) β β¦π / π’β¦π = π) |
62 | 56, 61 | neeqtrrd 3015 |
1
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β π β§ (π
β π΄ β§ Β¬ π
β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π
β€ (π β¨ π) β§ π β€ (π β¨ π) β§ π
β π)) β β¦π
/ π β¦π β β¦π / π’β¦π) |