Step | Hyp | Ref
| Expression |
1 | | simpl1l 1225 |
. . 3
β’ ((((πΎ β HL β§ π β π») β§ (πΉ β π β§ β β π) β§ (πΉ β ( I βΎ π΅) β§ β β ( I βΎ π΅) β§ (π
ββ) β (π
βπΉ))) β§ (π
β(β β πΉ)) β (AtomsβπΎ)) β πΎ β HL) |
2 | | simp1 1137 |
. . . . 5
β’ (((πΎ β HL β§ π β π») β§ (πΉ β π β§ β β π) β§ (πΉ β ( I βΎ π΅) β§ β β ( I βΎ π΅) β§ (π
ββ) β (π
βπΉ))) β (πΎ β HL β§ π β π»)) |
3 | | simp2r 1201 |
. . . . 5
β’ (((πΎ β HL β§ π β π») β§ (πΉ β π β§ β β π) β§ (πΉ β ( I βΎ π΅) β§ β β ( I βΎ π΅) β§ (π
ββ) β (π
βπΉ))) β β β π) |
4 | | simp32 1211 |
. . . . 5
β’ (((πΎ β HL β§ π β π») β§ (πΉ β π β§ β β π) β§ (πΉ β ( I βΎ π΅) β§ β β ( I βΎ π΅) β§ (π
ββ) β (π
βπΉ))) β β β ( I βΎ π΅)) |
5 | | cdlemg46.b |
. . . . . 6
β’ π΅ = (BaseβπΎ) |
6 | | eqid 2737 |
. . . . . 6
β’
(AtomsβπΎ) =
(AtomsβπΎ) |
7 | | cdlemg46.h |
. . . . . 6
β’ π» = (LHypβπΎ) |
8 | | cdlemg46.t |
. . . . . 6
β’ π = ((LTrnβπΎ)βπ) |
9 | | cdlemg46.r |
. . . . . 6
β’ π
= ((trLβπΎ)βπ) |
10 | 5, 6, 7, 8, 9 | trlnidat 38665 |
. . . . 5
β’ (((πΎ β HL β§ π β π») β§ β β π β§ β β ( I βΎ π΅)) β (π
ββ) β (AtomsβπΎ)) |
11 | 2, 3, 4, 10 | syl3anc 1372 |
. . . 4
β’ (((πΎ β HL β§ π β π») β§ (πΉ β π β§ β β π) β§ (πΉ β ( I βΎ π΅) β§ β β ( I βΎ π΅) β§ (π
ββ) β (π
βπΉ))) β (π
ββ) β (AtomsβπΎ)) |
12 | 11 | adantr 482 |
. . 3
β’ ((((πΎ β HL β§ π β π») β§ (πΉ β π β§ β β π) β§ (πΉ β ( I βΎ π΅) β§ β β ( I βΎ π΅) β§ (π
ββ) β (π
βπΉ))) β§ (π
β(β β πΉ)) β (AtomsβπΎ)) β (π
ββ) β (AtomsβπΎ)) |
13 | | simp2l 1200 |
. . . . 5
β’ (((πΎ β HL β§ π β π») β§ (πΉ β π β§ β β π) β§ (πΉ β ( I βΎ π΅) β§ β β ( I βΎ π΅) β§ (π
ββ) β (π
βπΉ))) β πΉ β π) |
14 | | simp31 1210 |
. . . . 5
β’ (((πΎ β HL β§ π β π») β§ (πΉ β π β§ β β π) β§ (πΉ β ( I βΎ π΅) β§ β β ( I βΎ π΅) β§ (π
ββ) β (π
βπΉ))) β πΉ β ( I βΎ π΅)) |
15 | 5, 6, 7, 8, 9 | trlnidat 38665 |
. . . . 5
β’ (((πΎ β HL β§ π β π») β§ πΉ β π β§ πΉ β ( I βΎ π΅)) β (π
βπΉ) β (AtomsβπΎ)) |
16 | 2, 13, 14, 15 | syl3anc 1372 |
. . . 4
β’ (((πΎ β HL β§ π β π») β§ (πΉ β π β§ β β π) β§ (πΉ β ( I βΎ π΅) β§ β β ( I βΎ π΅) β§ (π
ββ) β (π
βπΉ))) β (π
βπΉ) β (AtomsβπΎ)) |
17 | 16 | adantr 482 |
. . 3
β’ ((((πΎ β HL β§ π β π») β§ (πΉ β π β§ β β π) β§ (πΉ β ( I βΎ π΅) β§ β β ( I βΎ π΅) β§ (π
ββ) β (π
βπΉ))) β§ (π
β(β β πΉ)) β (AtomsβπΎ)) β (π
βπΉ) β (AtomsβπΎ)) |
18 | | simpl33 1257 |
. . 3
β’ ((((πΎ β HL β§ π β π») β§ (πΉ β π β§ β β π) β§ (πΉ β ( I βΎ π΅) β§ β β ( I βΎ π΅) β§ (π
ββ) β (π
βπΉ))) β§ (π
β(β β πΉ)) β (AtomsβπΎ)) β (π
ββ) β (π
βπΉ)) |
19 | | simpr 486 |
. . 3
β’ ((((πΎ β HL β§ π β π») β§ (πΉ β π β§ β β π) β§ (πΉ β ( I βΎ π΅) β§ β β ( I βΎ π΅) β§ (π
ββ) β (π
βπΉ))) β§ (π
β(β β πΉ)) β (AtomsβπΎ)) β (π
β(β β πΉ)) β (AtomsβπΎ)) |
20 | 7, 8 | ltrnco 39211 |
. . . . . . . 8
β’ (((πΎ β HL β§ π β π») β§ β β π β§ πΉ β π) β (β β πΉ) β π) |
21 | 2, 3, 13, 20 | syl3anc 1372 |
. . . . . . 7
β’ (((πΎ β HL β§ π β π») β§ (πΉ β π β§ β β π) β§ (πΉ β ( I βΎ π΅) β§ β β ( I βΎ π΅) β§ (π
ββ) β (π
βπΉ))) β (β β πΉ) β π) |
22 | 7, 8 | ltrncnv 38638 |
. . . . . . . 8
β’ (((πΎ β HL β§ π β π») β§ πΉ β π) β β‘πΉ β π) |
23 | 2, 13, 22 | syl2anc 585 |
. . . . . . 7
β’ (((πΎ β HL β§ π β π») β§ (πΉ β π β§ β β π) β§ (πΉ β ( I βΎ π΅) β§ β β ( I βΎ π΅) β§ (π
ββ) β (π
βπΉ))) β β‘πΉ β π) |
24 | | eqid 2737 |
. . . . . . . 8
β’
(leβπΎ) =
(leβπΎ) |
25 | | eqid 2737 |
. . . . . . . 8
β’
(joinβπΎ) =
(joinβπΎ) |
26 | 24, 25, 7, 8, 9 | trlco 39219 |
. . . . . . 7
β’ (((πΎ β HL β§ π β π») β§ (β β πΉ) β π β§ β‘πΉ β π) β (π
β((β β πΉ) β β‘πΉ))(leβπΎ)((π
β(β β πΉ))(joinβπΎ)(π
ββ‘πΉ))) |
27 | 2, 21, 23, 26 | syl3anc 1372 |
. . . . . 6
β’ (((πΎ β HL β§ π β π») β§ (πΉ β π β§ β β π) β§ (πΉ β ( I βΎ π΅) β§ β β ( I βΎ π΅) β§ (π
ββ) β (π
βπΉ))) β (π
β((β β πΉ) β β‘πΉ))(leβπΎ)((π
β(β β πΉ))(joinβπΎ)(π
ββ‘πΉ))) |
28 | | coass 6222 |
. . . . . . . 8
β’ ((β β πΉ) β β‘πΉ) = (β β (πΉ β β‘πΉ)) |
29 | 5, 7, 8 | ltrn1o 38616 |
. . . . . . . . . . . 12
β’ (((πΎ β HL β§ π β π») β§ πΉ β π) β πΉ:π΅β1-1-ontoβπ΅) |
30 | 2, 13, 29 | syl2anc 585 |
. . . . . . . . . . 11
β’ (((πΎ β HL β§ π β π») β§ (πΉ β π β§ β β π) β§ (πΉ β ( I βΎ π΅) β§ β β ( I βΎ π΅) β§ (π
ββ) β (π
βπΉ))) β πΉ:π΅β1-1-ontoβπ΅) |
31 | | f1ococnv2 6816 |
. . . . . . . . . . 11
β’ (πΉ:π΅β1-1-ontoβπ΅ β (πΉ β β‘πΉ) = ( I βΎ π΅)) |
32 | 30, 31 | syl 17 |
. . . . . . . . . 10
β’ (((πΎ β HL β§ π β π») β§ (πΉ β π β§ β β π) β§ (πΉ β ( I βΎ π΅) β§ β β ( I βΎ π΅) β§ (π
ββ) β (π
βπΉ))) β (πΉ β β‘πΉ) = ( I βΎ π΅)) |
33 | 32 | coeq2d 5823 |
. . . . . . . . 9
β’ (((πΎ β HL β§ π β π») β§ (πΉ β π β§ β β π) β§ (πΉ β ( I βΎ π΅) β§ β β ( I βΎ π΅) β§ (π
ββ) β (π
βπΉ))) β (β β (πΉ β β‘πΉ)) = (β β ( I βΎ π΅))) |
34 | 5, 7, 8 | ltrn1o 38616 |
. . . . . . . . . . 11
β’ (((πΎ β HL β§ π β π») β§ β β π) β β:π΅β1-1-ontoβπ΅) |
35 | 2, 3, 34 | syl2anc 585 |
. . . . . . . . . 10
β’ (((πΎ β HL β§ π β π») β§ (πΉ β π β§ β β π) β§ (πΉ β ( I βΎ π΅) β§ β β ( I βΎ π΅) β§ (π
ββ) β (π
βπΉ))) β β:π΅β1-1-ontoβπ΅) |
36 | | f1of 6789 |
. . . . . . . . . 10
β’ (β:π΅β1-1-ontoβπ΅ β β:π΅βΆπ΅) |
37 | | fcoi1 6721 |
. . . . . . . . . 10
β’ (β:π΅βΆπ΅ β (β β ( I βΎ π΅)) = β) |
38 | 35, 36, 37 | 3syl 18 |
. . . . . . . . 9
β’ (((πΎ β HL β§ π β π») β§ (πΉ β π β§ β β π) β§ (πΉ β ( I βΎ π΅) β§ β β ( I βΎ π΅) β§ (π
ββ) β (π
βπΉ))) β (β β ( I βΎ π΅)) = β) |
39 | 33, 38 | eqtrd 2777 |
. . . . . . . 8
β’ (((πΎ β HL β§ π β π») β§ (πΉ β π β§ β β π) β§ (πΉ β ( I βΎ π΅) β§ β β ( I βΎ π΅) β§ (π
ββ) β (π
βπΉ))) β (β β (πΉ β β‘πΉ)) = β) |
40 | 28, 39 | eqtrid 2789 |
. . . . . . 7
β’ (((πΎ β HL β§ π β π») β§ (πΉ β π β§ β β π) β§ (πΉ β ( I βΎ π΅) β§ β β ( I βΎ π΅) β§ (π
ββ) β (π
βπΉ))) β ((β β πΉ) β β‘πΉ) = β) |
41 | 40 | fveq2d 6851 |
. . . . . 6
β’ (((πΎ β HL β§ π β π») β§ (πΉ β π β§ β β π) β§ (πΉ β ( I βΎ π΅) β§ β β ( I βΎ π΅) β§ (π
ββ) β (π
βπΉ))) β (π
β((β β πΉ) β β‘πΉ)) = (π
ββ)) |
42 | 7, 8, 9 | trlcnv 38657 |
. . . . . . . 8
β’ (((πΎ β HL β§ π β π») β§ πΉ β π) β (π
ββ‘πΉ) = (π
βπΉ)) |
43 | 2, 13, 42 | syl2anc 585 |
. . . . . . 7
β’ (((πΎ β HL β§ π β π») β§ (πΉ β π β§ β β π) β§ (πΉ β ( I βΎ π΅) β§ β β ( I βΎ π΅) β§ (π
ββ) β (π
βπΉ))) β (π
ββ‘πΉ) = (π
βπΉ)) |
44 | 43 | oveq2d 7378 |
. . . . . 6
β’ (((πΎ β HL β§ π β π») β§ (πΉ β π β§ β β π) β§ (πΉ β ( I βΎ π΅) β§ β β ( I βΎ π΅) β§ (π
ββ) β (π
βπΉ))) β ((π
β(β β πΉ))(joinβπΎ)(π
ββ‘πΉ)) = ((π
β(β β πΉ))(joinβπΎ)(π
βπΉ))) |
45 | 27, 41, 44 | 3brtr3d 5141 |
. . . . 5
β’ (((πΎ β HL β§ π β π») β§ (πΉ β π β§ β β π) β§ (πΉ β ( I βΎ π΅) β§ β β ( I βΎ π΅) β§ (π
ββ) β (π
βπΉ))) β (π
ββ)(leβπΎ)((π
β(β β πΉ))(joinβπΎ)(π
βπΉ))) |
46 | 45 | adantr 482 |
. . . 4
β’ ((((πΎ β HL β§ π β π») β§ (πΉ β π β§ β β π) β§ (πΉ β ( I βΎ π΅) β§ β β ( I βΎ π΅) β§ (π
ββ) β (π
βπΉ))) β§ (π
β(β β πΉ)) β (AtomsβπΎ)) β (π
ββ)(leβπΎ)((π
β(β β πΉ))(joinβπΎ)(π
βπΉ))) |
47 | 24, 25, 6 | hlatlej2 37867 |
. . . . 5
β’ ((πΎ β HL β§ (π
β(β β πΉ)) β (AtomsβπΎ) β§ (π
βπΉ) β (AtomsβπΎ)) β (π
βπΉ)(leβπΎ)((π
β(β β πΉ))(joinβπΎ)(π
βπΉ))) |
48 | 1, 19, 17, 47 | syl3anc 1372 |
. . . 4
β’ ((((πΎ β HL β§ π β π») β§ (πΉ β π β§ β β π) β§ (πΉ β ( I βΎ π΅) β§ β β ( I βΎ π΅) β§ (π
ββ) β (π
βπΉ))) β§ (π
β(β β πΉ)) β (AtomsβπΎ)) β (π
βπΉ)(leβπΎ)((π
β(β β πΉ))(joinβπΎ)(π
βπΉ))) |
49 | 1 | hllatd 37855 |
. . . . 5
β’ ((((πΎ β HL β§ π β π») β§ (πΉ β π β§ β β π) β§ (πΉ β ( I βΎ π΅) β§ β β ( I βΎ π΅) β§ (π
ββ) β (π
βπΉ))) β§ (π
β(β β πΉ)) β (AtomsβπΎ)) β πΎ β Lat) |
50 | 5, 6 | atbase 37780 |
. . . . . 6
β’ ((π
ββ) β (AtomsβπΎ) β (π
ββ) β π΅) |
51 | 12, 50 | syl 17 |
. . . . 5
β’ ((((πΎ β HL β§ π β π») β§ (πΉ β π β§ β β π) β§ (πΉ β ( I βΎ π΅) β§ β β ( I βΎ π΅) β§ (π
ββ) β (π
βπΉ))) β§ (π
β(β β πΉ)) β (AtomsβπΎ)) β (π
ββ) β π΅) |
52 | 5, 6 | atbase 37780 |
. . . . . 6
β’ ((π
βπΉ) β (AtomsβπΎ) β (π
βπΉ) β π΅) |
53 | 17, 52 | syl 17 |
. . . . 5
β’ ((((πΎ β HL β§ π β π») β§ (πΉ β π β§ β β π) β§ (πΉ β ( I βΎ π΅) β§ β β ( I βΎ π΅) β§ (π
ββ) β (π
βπΉ))) β§ (π
β(β β πΉ)) β (AtomsβπΎ)) β (π
βπΉ) β π΅) |
54 | 5, 25, 6 | hlatjcl 37858 |
. . . . . 6
β’ ((πΎ β HL β§ (π
β(β β πΉ)) β (AtomsβπΎ) β§ (π
βπΉ) β (AtomsβπΎ)) β ((π
β(β β πΉ))(joinβπΎ)(π
βπΉ)) β π΅) |
55 | 1, 19, 17, 54 | syl3anc 1372 |
. . . . 5
β’ ((((πΎ β HL β§ π β π») β§ (πΉ β π β§ β β π) β§ (πΉ β ( I βΎ π΅) β§ β β ( I βΎ π΅) β§ (π
ββ) β (π
βπΉ))) β§ (π
β(β β πΉ)) β (AtomsβπΎ)) β ((π
β(β β πΉ))(joinβπΎ)(π
βπΉ)) β π΅) |
56 | 5, 24, 25 | latjle12 18346 |
. . . . 5
β’ ((πΎ β Lat β§ ((π
ββ) β π΅ β§ (π
βπΉ) β π΅ β§ ((π
β(β β πΉ))(joinβπΎ)(π
βπΉ)) β π΅)) β (((π
ββ)(leβπΎ)((π
β(β β πΉ))(joinβπΎ)(π
βπΉ)) β§ (π
βπΉ)(leβπΎ)((π
β(β β πΉ))(joinβπΎ)(π
βπΉ))) β ((π
ββ)(joinβπΎ)(π
βπΉ))(leβπΎ)((π
β(β β πΉ))(joinβπΎ)(π
βπΉ)))) |
57 | 49, 51, 53, 55, 56 | syl13anc 1373 |
. . . 4
β’ ((((πΎ β HL β§ π β π») β§ (πΉ β π β§ β β π) β§ (πΉ β ( I βΎ π΅) β§ β β ( I βΎ π΅) β§ (π
ββ) β (π
βπΉ))) β§ (π
β(β β πΉ)) β (AtomsβπΎ)) β (((π
ββ)(leβπΎ)((π
β(β β πΉ))(joinβπΎ)(π
βπΉ)) β§ (π
βπΉ)(leβπΎ)((π
β(β β πΉ))(joinβπΎ)(π
βπΉ))) β ((π
ββ)(joinβπΎ)(π
βπΉ))(leβπΎ)((π
β(β β πΉ))(joinβπΎ)(π
βπΉ)))) |
58 | 46, 48, 57 | mpbi2and 711 |
. . 3
β’ ((((πΎ β HL β§ π β π») β§ (πΉ β π β§ β β π) β§ (πΉ β ( I βΎ π΅) β§ β β ( I βΎ π΅) β§ (π
ββ) β (π
βπΉ))) β§ (π
β(β β πΉ)) β (AtomsβπΎ)) β ((π
ββ)(joinβπΎ)(π
βπΉ))(leβπΎ)((π
β(β β πΉ))(joinβπΎ)(π
βπΉ))) |
59 | 24, 25, 6 | 2atjlej 37971 |
. . 3
β’ ((πΎ β HL β§ ((π
ββ) β (AtomsβπΎ) β§ (π
βπΉ) β (AtomsβπΎ) β§ (π
ββ) β (π
βπΉ)) β§ ((π
β(β β πΉ)) β (AtomsβπΎ) β§ (π
βπΉ) β (AtomsβπΎ) β§ ((π
ββ)(joinβπΎ)(π
βπΉ))(leβπΎ)((π
β(β β πΉ))(joinβπΎ)(π
βπΉ)))) β (π
β(β β πΉ)) β (π
βπΉ)) |
60 | 1, 12, 17, 18, 19, 17, 58, 59 | syl133anc 1394 |
. 2
β’ ((((πΎ β HL β§ π β π») β§ (πΉ β π β§ β β π) β§ (πΉ β ( I βΎ π΅) β§ β β ( I βΎ π΅) β§ (π
ββ) β (π
βπΉ))) β§ (π
β(β β πΉ)) β (AtomsβπΎ)) β (π
β(β β πΉ)) β (π
βπΉ)) |
61 | | nelne2 3043 |
. . . 4
β’ (((π
βπΉ) β (AtomsβπΎ) β§ Β¬ (π
β(β β πΉ)) β (AtomsβπΎ)) β (π
βπΉ) β (π
β(β β πΉ))) |
62 | 61 | necomd 3000 |
. . 3
β’ (((π
βπΉ) β (AtomsβπΎ) β§ Β¬ (π
β(β β πΉ)) β (AtomsβπΎ)) β (π
β(β β πΉ)) β (π
βπΉ)) |
63 | 16, 62 | sylan 581 |
. 2
β’ ((((πΎ β HL β§ π β π») β§ (πΉ β π β§ β β π) β§ (πΉ β ( I βΎ π΅) β§ β β ( I βΎ π΅) β§ (π
ββ) β (π
βπΉ))) β§ Β¬ (π
β(β β πΉ)) β (AtomsβπΎ)) β (π
β(β β πΉ)) β (π
βπΉ)) |
64 | 60, 63 | pm2.61dan 812 |
1
β’ (((πΎ β HL β§ π β π») β§ (πΉ β π β§ β β π) β§ (πΉ β ( I βΎ π΅) β§ β β ( I βΎ π΅) β§ (π
ββ) β (π
βπΉ))) β (π
β(β β πΉ)) β (π
βπΉ)) |