Step | Hyp | Ref
| Expression |
1 | | simp33 1211 |
. 2
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (πΉ β π β§ πΊ β π β§ π β π) β§ (Β¬ (π
βπΉ) β€ (π β¨ π) β§ Β¬ (π
βπΊ) β€ (π β¨ π) β§ (π
βπΉ) β (π
βπΊ))) β (π
βπΉ) β (π
βπΊ)) |
2 | | simpl1 1191 |
. . . . . . . 8
β’
(((((πΎ β HL
β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (πΉ β π β§ πΊ β π β§ π β π) β§ (Β¬ (π
βπΉ) β€ (π β¨ π) β§ Β¬ (π
βπΊ) β€ (π β¨ π) β§ (π
βπΉ) β (π
βπΊ))) β§ (((πΉβ(πΊβπ)) β¨ π) β§ ((πΉβ(πΊβπ)) β¨ π)) = 0 ) β ((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π))) |
3 | | simpl21 1251 |
. . . . . . . 8
β’
(((((πΎ β HL
β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (πΉ β π β§ πΊ β π β§ π β π) β§ (Β¬ (π
βπΉ) β€ (π β¨ π) β§ Β¬ (π
βπΊ) β€ (π β¨ π) β§ (π
βπΉ) β (π
βπΊ))) β§ (((πΉβ(πΊβπ)) β¨ π) β§ ((πΉβ(πΊβπ)) β¨ π)) = 0 ) β πΉ β π) |
4 | | simpl22 1252 |
. . . . . . . 8
β’
(((((πΎ β HL
β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (πΉ β π β§ πΊ β π β§ π β π) β§ (Β¬ (π
βπΉ) β€ (π β¨ π) β§ Β¬ (π
βπΊ) β€ (π β¨ π) β§ (π
βπΉ) β (π
βπΊ))) β§ (((πΉβ(πΊβπ)) β¨ π) β§ ((πΉβ(πΊβπ)) β¨ π)) = 0 ) β πΊ β π) |
5 | | simpl23 1253 |
. . . . . . . 8
β’
(((((πΎ β HL
β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (πΉ β π β§ πΊ β π β§ π β π) β§ (Β¬ (π
βπΉ) β€ (π β¨ π) β§ Β¬ (π
βπΊ) β€ (π β¨ π) β§ (π
βπΉ) β (π
βπΊ))) β§ (((πΉβ(πΊβπ)) β¨ π) β§ ((πΉβ(πΊβπ)) β¨ π)) = 0 ) β π β π) |
6 | | simpl31 1254 |
. . . . . . . 8
β’
(((((πΎ β HL
β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (πΉ β π β§ πΊ β π β§ π β π) β§ (Β¬ (π
βπΉ) β€ (π β¨ π) β§ Β¬ (π
βπΊ) β€ (π β¨ π) β§ (π
βπΉ) β (π
βπΊ))) β§ (((πΉβ(πΊβπ)) β¨ π) β§ ((πΉβ(πΊβπ)) β¨ π)) = 0 ) β Β¬ (π
βπΉ) β€ (π β¨ π)) |
7 | | simpl32 1255 |
. . . . . . . 8
β’
(((((πΎ β HL
β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (πΉ β π β§ πΊ β π β§ π β π) β§ (Β¬ (π
βπΉ) β€ (π β¨ π) β§ Β¬ (π
βπΊ) β€ (π β¨ π) β§ (π
βπΉ) β (π
βπΊ))) β§ (((πΉβ(πΊβπ)) β¨ π) β§ ((πΉβ(πΊβπ)) β¨ π)) = 0 ) β Β¬ (π
βπΊ) β€ (π β¨ π)) |
8 | | cdlemg12.l |
. . . . . . . . 9
β’ β€ =
(leβπΎ) |
9 | | cdlemg12.j |
. . . . . . . . 9
β’ β¨ =
(joinβπΎ) |
10 | | cdlemg12.m |
. . . . . . . . 9
β’ β§ =
(meetβπΎ) |
11 | | cdlemg12.a |
. . . . . . . . 9
β’ π΄ = (AtomsβπΎ) |
12 | | cdlemg12.h |
. . . . . . . . 9
β’ π» = (LHypβπΎ) |
13 | | cdlemg12.t |
. . . . . . . . 9
β’ π = ((LTrnβπΎ)βπ) |
14 | | cdlemg12b.r |
. . . . . . . . 9
β’ π
= ((trLβπΎ)βπ) |
15 | 8, 9, 10, 11, 12, 13, 14 | cdlemg12d 39215 |
. . . . . . . 8
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (πΉ β π β§ πΊ β π) β§ (π β π β§ Β¬ (π
βπΉ) β€ (π β¨ π) β§ Β¬ (π
βπΊ) β€ (π β¨ π))) β (π
βπΊ) β€ ((π
βπΉ) β¨ (((πΉβ(πΊβπ)) β¨ π) β§ ((πΉβ(πΊβπ)) β¨ π)))) |
16 | 2, 3, 4, 5, 6, 7, 15 | syl123anc 1387 |
. . . . . . 7
β’
(((((πΎ β HL
β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (πΉ β π β§ πΊ β π β§ π β π) β§ (Β¬ (π
βπΉ) β€ (π β¨ π) β§ Β¬ (π
βπΊ) β€ (π β¨ π) β§ (π
βπΉ) β (π
βπΊ))) β§ (((πΉβ(πΊβπ)) β¨ π) β§ ((πΉβ(πΊβπ)) β¨ π)) = 0 ) β (π
βπΊ) β€ ((π
βπΉ) β¨ (((πΉβ(πΊβπ)) β¨ π) β§ ((πΉβ(πΊβπ)) β¨ π)))) |
17 | | simpr 485 |
. . . . . . . . 9
β’
(((((πΎ β HL
β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (πΉ β π β§ πΊ β π β§ π β π) β§ (Β¬ (π
βπΉ) β€ (π β¨ π) β§ Β¬ (π
βπΊ) β€ (π β¨ π) β§ (π
βπΉ) β (π
βπΊ))) β§ (((πΉβ(πΊβπ)) β¨ π) β§ ((πΉβ(πΊβπ)) β¨ π)) = 0 ) β (((πΉβ(πΊβπ)) β¨ π) β§ ((πΉβ(πΊβπ)) β¨ π)) = 0 ) |
18 | 17 | oveq2d 7393 |
. . . . . . . 8
β’
(((((πΎ β HL
β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (πΉ β π β§ πΊ β π β§ π β π) β§ (Β¬ (π
βπΉ) β€ (π β¨ π) β§ Β¬ (π
βπΊ) β€ (π β¨ π) β§ (π
βπΉ) β (π
βπΊ))) β§ (((πΉβ(πΊβπ)) β¨ π) β§ ((πΉβ(πΊβπ)) β¨ π)) = 0 ) β ((π
βπΉ) β¨ (((πΉβ(πΊβπ)) β¨ π) β§ ((πΉβ(πΊβπ)) β¨ π))) = ((π
βπΉ) β¨ 0 )) |
19 | | simp11l 1284 |
. . . . . . . . . . 11
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (πΉ β π β§ πΊ β π β§ π β π) β§ (Β¬ (π
βπΉ) β€ (π β¨ π) β§ Β¬ (π
βπΊ) β€ (π β¨ π) β§ (π
βπΉ) β (π
βπΊ))) β πΎ β HL) |
20 | 19 | adantr 481 |
. . . . . . . . . 10
β’
(((((πΎ β HL
β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (πΉ β π β§ πΊ β π β§ π β π) β§ (Β¬ (π
βπΉ) β€ (π β¨ π) β§ Β¬ (π
βπΊ) β€ (π β¨ π) β§ (π
βπΉ) β (π
βπΊ))) β§ (((πΉβ(πΊβπ)) β¨ π) β§ ((πΉβ(πΊβπ)) β¨ π)) = 0 ) β πΎ β HL) |
21 | | hlol 37929 |
. . . . . . . . . 10
β’ (πΎ β HL β πΎ β OL) |
22 | 20, 21 | syl 17 |
. . . . . . . . 9
β’
(((((πΎ β HL
β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (πΉ β π β§ πΊ β π β§ π β π) β§ (Β¬ (π
βπΉ) β€ (π β¨ π) β§ Β¬ (π
βπΊ) β€ (π β¨ π) β§ (π
βπΉ) β (π
βπΊ))) β§ (((πΉβ(πΊβπ)) β¨ π) β§ ((πΉβ(πΊβπ)) β¨ π)) = 0 ) β πΎ β OL) |
23 | | simpl11 1248 |
. . . . . . . . . 10
β’
(((((πΎ β HL
β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (πΉ β π β§ πΊ β π β§ π β π) β§ (Β¬ (π
βπΉ) β€ (π β¨ π) β§ Β¬ (π
βπΊ) β€ (π β¨ π) β§ (π
βπΉ) β (π
βπΊ))) β§ (((πΉβ(πΊβπ)) β¨ π) β§ ((πΉβ(πΊβπ)) β¨ π)) = 0 ) β (πΎ β HL β§ π β π»)) |
24 | | eqid 2731 |
. . . . . . . . . . 11
β’
(BaseβπΎ) =
(BaseβπΎ) |
25 | 24, 12, 13, 14 | trlcl 38733 |
. . . . . . . . . 10
β’ (((πΎ β HL β§ π β π») β§ πΉ β π) β (π
βπΉ) β (BaseβπΎ)) |
26 | 23, 3, 25 | syl2anc 584 |
. . . . . . . . 9
β’
(((((πΎ β HL
β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (πΉ β π β§ πΊ β π β§ π β π) β§ (Β¬ (π
βπΉ) β€ (π β¨ π) β§ Β¬ (π
βπΊ) β€ (π β¨ π) β§ (π
βπΉ) β (π
βπΊ))) β§ (((πΉβ(πΊβπ)) β¨ π) β§ ((πΉβ(πΊβπ)) β¨ π)) = 0 ) β (π
βπΉ) β (BaseβπΎ)) |
27 | | cdlemg12e.z |
. . . . . . . . . 10
β’ 0 =
(0.βπΎ) |
28 | 24, 9, 27 | olj01 37793 |
. . . . . . . . 9
β’ ((πΎ β OL β§ (π
βπΉ) β (BaseβπΎ)) β ((π
βπΉ) β¨ 0 ) = (π
βπΉ)) |
29 | 22, 26, 28 | syl2anc 584 |
. . . . . . . 8
β’
(((((πΎ β HL
β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (πΉ β π β§ πΊ β π β§ π β π) β§ (Β¬ (π
βπΉ) β€ (π β¨ π) β§ Β¬ (π
βπΊ) β€ (π β¨ π) β§ (π
βπΉ) β (π
βπΊ))) β§ (((πΉβ(πΊβπ)) β¨ π) β§ ((πΉβ(πΊβπ)) β¨ π)) = 0 ) β ((π
βπΉ) β¨ 0 ) = (π
βπΉ)) |
30 | 18, 29 | eqtrd 2771 |
. . . . . . 7
β’
(((((πΎ β HL
β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (πΉ β π β§ πΊ β π β§ π β π) β§ (Β¬ (π
βπΉ) β€ (π β¨ π) β§ Β¬ (π
βπΊ) β€ (π β¨ π) β§ (π
βπΉ) β (π
βπΊ))) β§ (((πΉβ(πΊβπ)) β¨ π) β§ ((πΉβ(πΊβπ)) β¨ π)) = 0 ) β ((π
βπΉ) β¨ (((πΉβ(πΊβπ)) β¨ π) β§ ((πΉβ(πΊβπ)) β¨ π))) = (π
βπΉ)) |
31 | 16, 30 | breqtrd 5151 |
. . . . . 6
β’
(((((πΎ β HL
β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (πΉ β π β§ πΊ β π β§ π β π) β§ (Β¬ (π
βπΉ) β€ (π β¨ π) β§ Β¬ (π
βπΊ) β€ (π β¨ π) β§ (π
βπΉ) β (π
βπΊ))) β§ (((πΉβ(πΊβπ)) β¨ π) β§ ((πΉβ(πΊβπ)) β¨ π)) = 0 ) β (π
βπΊ) β€ (π
βπΉ)) |
32 | | hlatl 37928 |
. . . . . . . 8
β’ (πΎ β HL β πΎ β AtLat) |
33 | 20, 32 | syl 17 |
. . . . . . 7
β’
(((((πΎ β HL
β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (πΉ β π β§ πΊ β π β§ π β π) β§ (Β¬ (π
βπΉ) β€ (π β¨ π) β§ Β¬ (π
βπΊ) β€ (π β¨ π) β§ (π
βπΉ) β (π
βπΊ))) β§ (((πΉβ(πΊβπ)) β¨ π) β§ ((πΉβ(πΊβπ)) β¨ π)) = 0 ) β πΎ β AtLat) |
34 | | hlop 37930 |
. . . . . . . . . 10
β’ (πΎ β HL β πΎ β OP) |
35 | 20, 34 | syl 17 |
. . . . . . . . 9
β’
(((((πΎ β HL
β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (πΉ β π β§ πΊ β π β§ π β π) β§ (Β¬ (π
βπΉ) β€ (π β¨ π) β§ Β¬ (π
βπΊ) β€ (π β¨ π) β§ (π
βπΉ) β (π
βπΊ))) β§ (((πΉβ(πΊβπ)) β¨ π) β§ ((πΉβ(πΊβπ)) β¨ π)) = 0 ) β πΎ β OP) |
36 | 24, 12, 13, 14 | trlcl 38733 |
. . . . . . . . . 10
β’ (((πΎ β HL β§ π β π») β§ πΊ β π) β (π
βπΊ) β (BaseβπΎ)) |
37 | 23, 4, 36 | syl2anc 584 |
. . . . . . . . 9
β’
(((((πΎ β HL
β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (πΉ β π β§ πΊ β π β§ π β π) β§ (Β¬ (π
βπΉ) β€ (π β¨ π) β§ Β¬ (π
βπΊ) β€ (π β¨ π) β§ (π
βπΉ) β (π
βπΊ))) β§ (((πΉβ(πΊβπ)) β¨ π) β§ ((πΉβ(πΊβπ)) β¨ π)) = 0 ) β (π
βπΊ) β (BaseβπΎ)) |
38 | | simp12l 1286 |
. . . . . . . . . . 11
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (πΉ β π β§ πΊ β π β§ π β π) β§ (Β¬ (π
βπΉ) β€ (π β¨ π) β§ Β¬ (π
βπΊ) β€ (π β¨ π) β§ (π
βπΉ) β (π
βπΊ))) β π β π΄) |
39 | 38 | adantr 481 |
. . . . . . . . . 10
β’
(((((πΎ β HL
β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (πΉ β π β§ πΊ β π β§ π β π) β§ (Β¬ (π
βπΉ) β€ (π β¨ π) β§ Β¬ (π
βπΊ) β€ (π β¨ π) β§ (π
βπΉ) β (π
βπΊ))) β§ (((πΉβ(πΊβπ)) β¨ π) β§ ((πΉβ(πΊβπ)) β¨ π)) = 0 ) β π β π΄) |
40 | | simp13l 1288 |
. . . . . . . . . . 11
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (πΉ β π β§ πΊ β π β§ π β π) β§ (Β¬ (π
βπΉ) β€ (π β¨ π) β§ Β¬ (π
βπΊ) β€ (π β¨ π) β§ (π
βπΉ) β (π
βπΊ))) β π β π΄) |
41 | 40 | adantr 481 |
. . . . . . . . . 10
β’
(((((πΎ β HL
β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (πΉ β π β§ πΊ β π β§ π β π) β§ (Β¬ (π
βπΉ) β€ (π β¨ π) β§ Β¬ (π
βπΊ) β€ (π β¨ π) β§ (π
βπΉ) β (π
βπΊ))) β§ (((πΉβ(πΊβπ)) β¨ π) β§ ((πΉβ(πΊβπ)) β¨ π)) = 0 ) β π β π΄) |
42 | 24, 9, 11 | hlatjcl 37935 |
. . . . . . . . . 10
β’ ((πΎ β HL β§ π β π΄ β§ π β π΄) β (π β¨ π) β (BaseβπΎ)) |
43 | 20, 39, 41, 42 | syl3anc 1371 |
. . . . . . . . 9
β’
(((((πΎ β HL
β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (πΉ β π β§ πΊ β π β§ π β π) β§ (Β¬ (π
βπΉ) β€ (π β¨ π) β§ Β¬ (π
βπΊ) β€ (π β¨ π) β§ (π
βπΉ) β (π
βπΊ))) β§ (((πΉβ(πΊβπ)) β¨ π) β§ ((πΉβ(πΊβπ)) β¨ π)) = 0 ) β (π β¨ π) β (BaseβπΎ)) |
44 | 24, 8, 27 | opnlen0 37756 |
. . . . . . . . 9
β’ (((πΎ β OP β§ (π
βπΊ) β (BaseβπΎ) β§ (π β¨ π) β (BaseβπΎ)) β§ Β¬ (π
βπΊ) β€ (π β¨ π)) β (π
βπΊ) β 0 ) |
45 | 35, 37, 43, 7, 44 | syl31anc 1373 |
. . . . . . . 8
β’
(((((πΎ β HL
β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (πΉ β π β§ πΊ β π β§ π β π) β§ (Β¬ (π
βπΉ) β€ (π β¨ π) β§ Β¬ (π
βπΊ) β€ (π β¨ π) β§ (π
βπΉ) β (π
βπΊ))) β§ (((πΉβ(πΊβπ)) β¨ π) β§ ((πΉβ(πΊβπ)) β¨ π)) = 0 ) β (π
βπΊ) β 0 ) |
46 | | simp11r 1285 |
. . . . . . . . . 10
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (πΉ β π β§ πΊ β π β§ π β π) β§ (Β¬ (π
βπΉ) β€ (π β¨ π) β§ Β¬ (π
βπΊ) β€ (π β¨ π) β§ (π
βπΉ) β (π
βπΊ))) β π β π») |
47 | 46 | adantr 481 |
. . . . . . . . 9
β’
(((((πΎ β HL
β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (πΉ β π β§ πΊ β π β§ π β π) β§ (Β¬ (π
βπΉ) β€ (π β¨ π) β§ Β¬ (π
βπΊ) β€ (π β¨ π) β§ (π
βπΉ) β (π
βπΊ))) β§ (((πΉβ(πΊβπ)) β¨ π) β§ ((πΉβ(πΊβπ)) β¨ π)) = 0 ) β π β π») |
48 | 27, 11, 12, 13, 14 | trlatn0 38741 |
. . . . . . . . 9
β’ (((πΎ β HL β§ π β π») β§ πΊ β π) β ((π
βπΊ) β π΄ β (π
βπΊ) β 0 )) |
49 | 20, 47, 4, 48 | syl21anc 836 |
. . . . . . . 8
β’
(((((πΎ β HL
β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (πΉ β π β§ πΊ β π β§ π β π) β§ (Β¬ (π
βπΉ) β€ (π β¨ π) β§ Β¬ (π
βπΊ) β€ (π β¨ π) β§ (π
βπΉ) β (π
βπΊ))) β§ (((πΉβ(πΊβπ)) β¨ π) β§ ((πΉβ(πΊβπ)) β¨ π)) = 0 ) β ((π
βπΊ) β π΄ β (π
βπΊ) β 0 )) |
50 | 45, 49 | mpbird 256 |
. . . . . . 7
β’
(((((πΎ β HL
β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (πΉ β π β§ πΊ β π β§ π β π) β§ (Β¬ (π
βπΉ) β€ (π β¨ π) β§ Β¬ (π
βπΊ) β€ (π β¨ π) β§ (π
βπΉ) β (π
βπΊ))) β§ (((πΉβ(πΊβπ)) β¨ π) β§ ((πΉβ(πΊβπ)) β¨ π)) = 0 ) β (π
βπΊ) β π΄) |
51 | 24, 8, 27 | opnlen0 37756 |
. . . . . . . . 9
β’ (((πΎ β OP β§ (π
βπΉ) β (BaseβπΎ) β§ (π β¨ π) β (BaseβπΎ)) β§ Β¬ (π
βπΉ) β€ (π β¨ π)) β (π
βπΉ) β 0 ) |
52 | 35, 26, 43, 6, 51 | syl31anc 1373 |
. . . . . . . 8
β’
(((((πΎ β HL
β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (πΉ β π β§ πΊ β π β§ π β π) β§ (Β¬ (π
βπΉ) β€ (π β¨ π) β§ Β¬ (π
βπΊ) β€ (π β¨ π) β§ (π
βπΉ) β (π
βπΊ))) β§ (((πΉβ(πΊβπ)) β¨ π) β§ ((πΉβ(πΊβπ)) β¨ π)) = 0 ) β (π
βπΉ) β 0 ) |
53 | 27, 11, 12, 13, 14 | trlatn0 38741 |
. . . . . . . . 9
β’ (((πΎ β HL β§ π β π») β§ πΉ β π) β ((π
βπΉ) β π΄ β (π
βπΉ) β 0 )) |
54 | 20, 47, 3, 53 | syl21anc 836 |
. . . . . . . 8
β’
(((((πΎ β HL
β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (πΉ β π β§ πΊ β π β§ π β π) β§ (Β¬ (π
βπΉ) β€ (π β¨ π) β§ Β¬ (π
βπΊ) β€ (π β¨ π) β§ (π
βπΉ) β (π
βπΊ))) β§ (((πΉβ(πΊβπ)) β¨ π) β§ ((πΉβ(πΊβπ)) β¨ π)) = 0 ) β ((π
βπΉ) β π΄ β (π
βπΉ) β 0 )) |
55 | 52, 54 | mpbird 256 |
. . . . . . 7
β’
(((((πΎ β HL
β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (πΉ β π β§ πΊ β π β§ π β π) β§ (Β¬ (π
βπΉ) β€ (π β¨ π) β§ Β¬ (π
βπΊ) β€ (π β¨ π) β§ (π
βπΉ) β (π
βπΊ))) β§ (((πΉβ(πΊβπ)) β¨ π) β§ ((πΉβ(πΊβπ)) β¨ π)) = 0 ) β (π
βπΉ) β π΄) |
56 | 8, 11 | atcmp 37879 |
. . . . . . 7
β’ ((πΎ β AtLat β§ (π
βπΊ) β π΄ β§ (π
βπΉ) β π΄) β ((π
βπΊ) β€ (π
βπΉ) β (π
βπΊ) = (π
βπΉ))) |
57 | 33, 50, 55, 56 | syl3anc 1371 |
. . . . . 6
β’
(((((πΎ β HL
β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (πΉ β π β§ πΊ β π β§ π β π) β§ (Β¬ (π
βπΉ) β€ (π β¨ π) β§ Β¬ (π
βπΊ) β€ (π β¨ π) β§ (π
βπΉ) β (π
βπΊ))) β§ (((πΉβ(πΊβπ)) β¨ π) β§ ((πΉβ(πΊβπ)) β¨ π)) = 0 ) β ((π
βπΊ) β€ (π
βπΉ) β (π
βπΊ) = (π
βπΉ))) |
58 | 31, 57 | mpbid 231 |
. . . . 5
β’
(((((πΎ β HL
β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (πΉ β π β§ πΊ β π β§ π β π) β§ (Β¬ (π
βπΉ) β€ (π β¨ π) β§ Β¬ (π
βπΊ) β€ (π β¨ π) β§ (π
βπΉ) β (π
βπΊ))) β§ (((πΉβ(πΊβπ)) β¨ π) β§ ((πΉβ(πΊβπ)) β¨ π)) = 0 ) β (π
βπΊ) = (π
βπΉ)) |
59 | 58 | eqcomd 2737 |
. . . 4
β’
(((((πΎ β HL
β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (πΉ β π β§ πΊ β π β§ π β π) β§ (Β¬ (π
βπΉ) β€ (π β¨ π) β§ Β¬ (π
βπΊ) β€ (π β¨ π) β§ (π
βπΉ) β (π
βπΊ))) β§ (((πΉβ(πΊβπ)) β¨ π) β§ ((πΉβ(πΊβπ)) β¨ π)) = 0 ) β (π
βπΉ) = (π
βπΊ)) |
60 | 59 | ex 413 |
. . 3
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (πΉ β π β§ πΊ β π β§ π β π) β§ (Β¬ (π
βπΉ) β€ (π β¨ π) β§ Β¬ (π
βπΊ) β€ (π β¨ π) β§ (π
βπΉ) β (π
βπΊ))) β ((((πΉβ(πΊβπ)) β¨ π) β§ ((πΉβ(πΊβπ)) β¨ π)) = 0 β (π
βπΉ) = (π
βπΊ))) |
61 | 60 | necon3d 2960 |
. 2
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (πΉ β π β§ πΊ β π β§ π β π) β§ (Β¬ (π
βπΉ) β€ (π β¨ π) β§ Β¬ (π
βπΊ) β€ (π β¨ π) β§ (π
βπΉ) β (π
βπΊ))) β ((π
βπΉ) β (π
βπΊ) β (((πΉβ(πΊβπ)) β¨ π) β§ ((πΉβ(πΊβπ)) β¨ π)) β 0 )) |
62 | 1, 61 | mpd 15 |
1
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (πΉ β π β§ πΊ β π β§ π β π) β§ (Β¬ (π
βπΉ) β€ (π β¨ π) β§ Β¬ (π
βπΊ) β€ (π β¨ π) β§ (π
βπΉ) β (π
βπΊ))) β (((πΉβ(πΊβπ)) β¨ π) β§ ((πΉβ(πΊβπ)) β¨ π)) β 0 ) |