Step | Hyp | Ref
| Expression |
1 | | oveq1 7365 |
. . . . . 6
β’ (π = π
β (π β¨ π
) = (π
β¨ π
)) |
2 | | simpr3 1197 |
. . . . . . 7
β’ ((πΎ β HL β§ (π β π΄ β§ π β π΄ β§ π
β π΄)) β π
β π΄) |
3 | | atltcvr.j |
. . . . . . . 8
β’ β¨ =
(joinβπΎ) |
4 | | atltcvr.a |
. . . . . . . 8
β’ π΄ = (AtomsβπΎ) |
5 | 3, 4 | hlatjidm 37877 |
. . . . . . 7
β’ ((πΎ β HL β§ π
β π΄) β (π
β¨ π
) = π
) |
6 | 2, 5 | syldan 592 |
. . . . . 6
β’ ((πΎ β HL β§ (π β π΄ β§ π β π΄ β§ π
β π΄)) β (π
β¨ π
) = π
) |
7 | 1, 6 | sylan9eqr 2795 |
. . . . 5
β’ (((πΎ β HL β§ (π β π΄ β§ π β π΄ β§ π
β π΄)) β§ π = π
) β (π β¨ π
) = π
) |
8 | 7 | breq2d 5118 |
. . . 4
β’ (((πΎ β HL β§ (π β π΄ β§ π β π΄ β§ π
β π΄)) β§ π = π
) β (π < (π β¨ π
) β π < π
)) |
9 | | hlatl 37868 |
. . . . . . . 8
β’ (πΎ β HL β πΎ β AtLat) |
10 | 9 | adantr 482 |
. . . . . . 7
β’ ((πΎ β HL β§ (π β π΄ β§ π β π΄ β§ π
β π΄)) β πΎ β AtLat) |
11 | | simpr1 1195 |
. . . . . . 7
β’ ((πΎ β HL β§ (π β π΄ β§ π β π΄ β§ π
β π΄)) β π β π΄) |
12 | | atltcvr.s |
. . . . . . . 8
β’ < =
(ltβπΎ) |
13 | 12, 4 | atnlt 37821 |
. . . . . . 7
β’ ((πΎ β AtLat β§ π β π΄ β§ π
β π΄) β Β¬ π < π
) |
14 | 10, 11, 2, 13 | syl3anc 1372 |
. . . . . 6
β’ ((πΎ β HL β§ (π β π΄ β§ π β π΄ β§ π
β π΄)) β Β¬ π < π
) |
15 | 14 | pm2.21d 121 |
. . . . 5
β’ ((πΎ β HL β§ (π β π΄ β§ π β π΄ β§ π
β π΄)) β (π < π
β ππΆ(π β¨ π
))) |
16 | 15 | adantr 482 |
. . . 4
β’ (((πΎ β HL β§ (π β π΄ β§ π β π΄ β§ π
β π΄)) β§ π = π
) β (π < π
β ππΆ(π β¨ π
))) |
17 | 8, 16 | sylbid 239 |
. . 3
β’ (((πΎ β HL β§ (π β π΄ β§ π β π΄ β§ π
β π΄)) β§ π = π
) β (π < (π β¨ π
) β ππΆ(π β¨ π
))) |
18 | | simpl 484 |
. . . . . 6
β’ ((πΎ β HL β§ (π β π΄ β§ π β π΄ β§ π
β π΄)) β πΎ β HL) |
19 | | hllat 37871 |
. . . . . . . 8
β’ (πΎ β HL β πΎ β Lat) |
20 | 19 | adantr 482 |
. . . . . . 7
β’ ((πΎ β HL β§ (π β π΄ β§ π β π΄ β§ π
β π΄)) β πΎ β Lat) |
21 | | simpr2 1196 |
. . . . . . . 8
β’ ((πΎ β HL β§ (π β π΄ β§ π β π΄ β§ π
β π΄)) β π β π΄) |
22 | | eqid 2733 |
. . . . . . . . 9
β’
(BaseβπΎ) =
(BaseβπΎ) |
23 | 22, 4 | atbase 37797 |
. . . . . . . 8
β’ (π β π΄ β π β (BaseβπΎ)) |
24 | 21, 23 | syl 17 |
. . . . . . 7
β’ ((πΎ β HL β§ (π β π΄ β§ π β π΄ β§ π
β π΄)) β π β (BaseβπΎ)) |
25 | 22, 4 | atbase 37797 |
. . . . . . . 8
β’ (π
β π΄ β π
β (BaseβπΎ)) |
26 | 2, 25 | syl 17 |
. . . . . . 7
β’ ((πΎ β HL β§ (π β π΄ β§ π β π΄ β§ π
β π΄)) β π
β (BaseβπΎ)) |
27 | 22, 3 | latjcl 18333 |
. . . . . . 7
β’ ((πΎ β Lat β§ π β (BaseβπΎ) β§ π
β (BaseβπΎ)) β (π β¨ π
) β (BaseβπΎ)) |
28 | 20, 24, 26, 27 | syl3anc 1372 |
. . . . . 6
β’ ((πΎ β HL β§ (π β π΄ β§ π β π΄ β§ π
β π΄)) β (π β¨ π
) β (BaseβπΎ)) |
29 | | eqid 2733 |
. . . . . . 7
β’
(leβπΎ) =
(leβπΎ) |
30 | 29, 12 | pltle 18227 |
. . . . . 6
β’ ((πΎ β HL β§ π β π΄ β§ (π β¨ π
) β (BaseβπΎ)) β (π < (π β¨ π
) β π(leβπΎ)(π β¨ π
))) |
31 | 18, 11, 28, 30 | syl3anc 1372 |
. . . . 5
β’ ((πΎ β HL β§ (π β π΄ β§ π β π΄ β§ π
β π΄)) β (π < (π β¨ π
) β π(leβπΎ)(π β¨ π
))) |
32 | 31 | adantr 482 |
. . . 4
β’ (((πΎ β HL β§ (π β π΄ β§ π β π΄ β§ π
β π΄)) β§ π β π
) β (π < (π β¨ π
) β π(leβπΎ)(π β¨ π
))) |
33 | | simpll 766 |
. . . . . . . 8
β’ (((πΎ β HL β§ (π β π΄ β§ π β π΄ β§ π
β π΄)) β§ (π β π
β§ π(leβπΎ)(π β¨ π
))) β πΎ β HL) |
34 | | simplr 768 |
. . . . . . . 8
β’ (((πΎ β HL β§ (π β π΄ β§ π β π΄ β§ π
β π΄)) β§ (π β π
β§ π(leβπΎ)(π β¨ π
))) β (π β π΄ β§ π β π΄ β§ π
β π΄)) |
35 | | simpr 486 |
. . . . . . . 8
β’ (((πΎ β HL β§ (π β π΄ β§ π β π΄ β§ π
β π΄)) β§ (π β π
β§ π(leβπΎ)(π β¨ π
))) β (π β π
β§ π(leβπΎ)(π β¨ π
))) |
36 | 33, 34, 35 | 3jca 1129 |
. . . . . . 7
β’ (((πΎ β HL β§ (π β π΄ β§ π β π΄ β§ π
β π΄)) β§ (π β π
β§ π(leβπΎ)(π β¨ π
))) β (πΎ β HL β§ (π β π΄ β§ π β π΄ β§ π
β π΄) β§ (π β π
β§ π(leβπΎ)(π β¨ π
)))) |
37 | 36 | anassrs 469 |
. . . . . 6
β’ ((((πΎ β HL β§ (π β π΄ β§ π β π΄ β§ π
β π΄)) β§ π β π
) β§ π(leβπΎ)(π β¨ π
)) β (πΎ β HL β§ (π β π΄ β§ π β π΄ β§ π
β π΄) β§ (π β π
β§ π(leβπΎ)(π β¨ π
)))) |
38 | | atltcvr.c |
. . . . . . 7
β’ πΆ = ( β βπΎ) |
39 | 29, 3, 38, 4 | atcvrj2 37942 |
. . . . . 6
β’ ((πΎ β HL β§ (π β π΄ β§ π β π΄ β§ π
β π΄) β§ (π β π
β§ π(leβπΎ)(π β¨ π
))) β ππΆ(π β¨ π
)) |
40 | 37, 39 | syl 17 |
. . . . 5
β’ ((((πΎ β HL β§ (π β π΄ β§ π β π΄ β§ π
β π΄)) β§ π β π
) β§ π(leβπΎ)(π β¨ π
)) β ππΆ(π β¨ π
)) |
41 | 40 | ex 414 |
. . . 4
β’ (((πΎ β HL β§ (π β π΄ β§ π β π΄ β§ π
β π΄)) β§ π β π
) β (π(leβπΎ)(π β¨ π
) β ππΆ(π β¨ π
))) |
42 | 32, 41 | syld 47 |
. . 3
β’ (((πΎ β HL β§ (π β π΄ β§ π β π΄ β§ π
β π΄)) β§ π β π
) β (π < (π β¨ π
) β ππΆ(π β¨ π
))) |
43 | 17, 42 | pm2.61dane 3029 |
. 2
β’ ((πΎ β HL β§ (π β π΄ β§ π β π΄ β§ π
β π΄)) β (π < (π β¨ π
) β ππΆ(π β¨ π
))) |
44 | 22, 4 | atbase 37797 |
. . . 4
β’ (π β π΄ β π β (BaseβπΎ)) |
45 | 11, 44 | syl 17 |
. . 3
β’ ((πΎ β HL β§ (π β π΄ β§ π β π΄ β§ π
β π΄)) β π β (BaseβπΎ)) |
46 | 22, 12, 38 | cvrlt 37778 |
. . . 4
β’ (((πΎ β HL β§ π β (BaseβπΎ) β§ (π β¨ π
) β (BaseβπΎ)) β§ ππΆ(π β¨ π
)) β π < (π β¨ π
)) |
47 | 46 | ex 414 |
. . 3
β’ ((πΎ β HL β§ π β (BaseβπΎ) β§ (π β¨ π
) β (BaseβπΎ)) β (ππΆ(π β¨ π
) β π < (π β¨ π
))) |
48 | 18, 45, 28, 47 | syl3anc 1372 |
. 2
β’ ((πΎ β HL β§ (π β π΄ β§ π β π΄ β§ π
β π΄)) β (ππΆ(π β¨ π
) β π < (π β¨ π
))) |
49 | 43, 48 | impbid 211 |
1
β’ ((πΎ β HL β§ (π β π΄ β§ π β π΄ β§ π
β π΄)) β (π < (π β¨ π
) β ππΆ(π β¨ π
))) |