Step | Hyp | Ref
| Expression |
1 | | simpl3l 1229 |
. . . . . . 7
β’ (((πΎ β HL β§ (π β π΄ β§ π β π΄ β§ π
β π΄) β§ (π β π
β§ π β€ (π β¨ π
))) β§ π = π
) β π β π
) |
2 | 1 | necomd 2996 |
. . . . . 6
β’ (((πΎ β HL β§ (π β π΄ β§ π β π΄ β§ π
β π΄) β§ (π β π
β§ π β€ (π β¨ π
))) β§ π = π
) β π
β π) |
3 | | simpl1 1192 |
. . . . . . 7
β’ (((πΎ β HL β§ (π β π΄ β§ π β π΄ β§ π
β π΄) β§ (π β π
β§ π β€ (π β¨ π
))) β§ π = π
) β πΎ β HL) |
4 | | simpl23 1254 |
. . . . . . 7
β’ (((πΎ β HL β§ (π β π΄ β§ π β π΄ β§ π
β π΄) β§ (π β π
β§ π β€ (π β¨ π
))) β§ π = π
) β π
β π΄) |
5 | | simpl22 1253 |
. . . . . . 7
β’ (((πΎ β HL β§ (π β π΄ β§ π β π΄ β§ π
β π΄) β§ (π β π
β§ π β€ (π β¨ π
))) β§ π = π
) β π β π΄) |
6 | | atcvrj1x.j |
. . . . . . . 8
β’ β¨ =
(joinβπΎ) |
7 | | atcvrj1x.c |
. . . . . . . 8
β’ πΆ = ( β βπΎ) |
8 | | atcvrj1x.a |
. . . . . . . 8
β’ π΄ = (AtomsβπΎ) |
9 | 6, 7, 8 | atcvr2 37927 |
. . . . . . 7
β’ ((πΎ β HL β§ π
β π΄ β§ π β π΄) β (π
β π β π
πΆ(π β¨ π
))) |
10 | 3, 4, 5, 9 | syl3anc 1372 |
. . . . . 6
β’ (((πΎ β HL β§ (π β π΄ β§ π β π΄ β§ π
β π΄) β§ (π β π
β§ π β€ (π β¨ π
))) β§ π = π
) β (π
β π β π
πΆ(π β¨ π
))) |
11 | 2, 10 | mpbid 231 |
. . . . 5
β’ (((πΎ β HL β§ (π β π΄ β§ π β π΄ β§ π
β π΄) β§ (π β π
β§ π β€ (π β¨ π
))) β§ π = π
) β π
πΆ(π β¨ π
)) |
12 | | breq1 5109 |
. . . . . 6
β’ (π = π
β (ππΆ(π β¨ π
) β π
πΆ(π β¨ π
))) |
13 | 12 | adantl 483 |
. . . . 5
β’ (((πΎ β HL β§ (π β π΄ β§ π β π΄ β§ π
β π΄) β§ (π β π
β§ π β€ (π β¨ π
))) β§ π = π
) β (ππΆ(π β¨ π
) β π
πΆ(π β¨ π
))) |
14 | 11, 13 | mpbird 257 |
. . . 4
β’ (((πΎ β HL β§ (π β π΄ β§ π β π΄ β§ π
β π΄) β§ (π β π
β§ π β€ (π β¨ π
))) β§ π = π
) β ππΆ(π β¨ π
)) |
15 | | simpl1 1192 |
. . . . 5
β’ (((πΎ β HL β§ (π β π΄ β§ π β π΄ β§ π
β π΄) β§ (π β π
β§ π β€ (π β¨ π
))) β§ π β π
) β πΎ β HL) |
16 | | simpl2 1193 |
. . . . 5
β’ (((πΎ β HL β§ (π β π΄ β§ π β π΄ β§ π
β π΄) β§ (π β π
β§ π β€ (π β¨ π
))) β§ π β π
) β (π β π΄ β§ π β π΄ β§ π
β π΄)) |
17 | | simpr 486 |
. . . . 5
β’ (((πΎ β HL β§ (π β π΄ β§ π β π΄ β§ π
β π΄) β§ (π β π
β§ π β€ (π β¨ π
))) β§ π β π
) β π β π
) |
18 | | simpl3r 1230 |
. . . . 5
β’ (((πΎ β HL β§ (π β π΄ β§ π β π΄ β§ π
β π΄) β§ (π β π
β§ π β€ (π β¨ π
))) β§ π β π
) β π β€ (π β¨ π
)) |
19 | | atcvrj1x.l |
. . . . . 6
β’ β€ =
(leβπΎ) |
20 | 19, 6, 7, 8 | atcvrj1 37940 |
. . . . 5
β’ ((πΎ β HL β§ (π β π΄ β§ π β π΄ β§ π
β π΄) β§ (π β π
β§ π β€ (π β¨ π
))) β ππΆ(π β¨ π
)) |
21 | 15, 16, 17, 18, 20 | syl112anc 1375 |
. . . 4
β’ (((πΎ β HL β§ (π β π΄ β§ π β π΄ β§ π
β π΄) β§ (π β π
β§ π β€ (π β¨ π
))) β§ π β π
) β ππΆ(π β¨ π
)) |
22 | 14, 21 | pm2.61dane 3029 |
. . 3
β’ ((πΎ β HL β§ (π β π΄ β§ π β π΄ β§ π
β π΄) β§ (π β π
β§ π β€ (π β¨ π
))) β ππΆ(π β¨ π
)) |
23 | 22 | 3expia 1122 |
. 2
β’ ((πΎ β HL β§ (π β π΄ β§ π β π΄ β§ π
β π΄)) β ((π β π
β§ π β€ (π β¨ π
)) β ππΆ(π β¨ π
))) |
24 | | hlatl 37868 |
. . . . . . 7
β’ (πΎ β HL β πΎ β AtLat) |
25 | 24 | ad2antrr 725 |
. . . . . 6
β’ (((πΎ β HL β§ (π β π΄ β§ π β π΄ β§ π
β π΄)) β§ ππΆ(π β¨ π
)) β πΎ β AtLat) |
26 | | simplr1 1216 |
. . . . . 6
β’ (((πΎ β HL β§ (π β π΄ β§ π β π΄ β§ π
β π΄)) β§ ππΆ(π β¨ π
)) β π β π΄) |
27 | | eqid 2733 |
. . . . . . 7
β’
(0.βπΎ) =
(0.βπΎ) |
28 | 27, 8 | atn0 37816 |
. . . . . 6
β’ ((πΎ β AtLat β§ π β π΄) β π β (0.βπΎ)) |
29 | 25, 26, 28 | syl2anc 585 |
. . . . 5
β’ (((πΎ β HL β§ (π β π΄ β§ π β π΄ β§ π
β π΄)) β§ ππΆ(π β¨ π
)) β π β (0.βπΎ)) |
30 | | simpll 766 |
. . . . . . 7
β’ (((πΎ β HL β§ (π β π΄ β§ π β π΄ β§ π
β π΄)) β§ ππΆ(π β¨ π
)) β πΎ β HL) |
31 | | eqid 2733 |
. . . . . . . . 9
β’
(BaseβπΎ) =
(BaseβπΎ) |
32 | 31, 8 | atbase 37797 |
. . . . . . . 8
β’ (π β π΄ β π β (BaseβπΎ)) |
33 | 26, 32 | syl 17 |
. . . . . . 7
β’ (((πΎ β HL β§ (π β π΄ β§ π β π΄ β§ π
β π΄)) β§ ππΆ(π β¨ π
)) β π β (BaseβπΎ)) |
34 | | simplr2 1217 |
. . . . . . 7
β’ (((πΎ β HL β§ (π β π΄ β§ π β π΄ β§ π
β π΄)) β§ ππΆ(π β¨ π
)) β π β π΄) |
35 | | simplr3 1218 |
. . . . . . 7
β’ (((πΎ β HL β§ (π β π΄ β§ π β π΄ β§ π
β π΄)) β§ ππΆ(π β¨ π
)) β π
β π΄) |
36 | | simpr 486 |
. . . . . . 7
β’ (((πΎ β HL β§ (π β π΄ β§ π β π΄ β§ π
β π΄)) β§ ππΆ(π β¨ π
)) β ππΆ(π β¨ π
)) |
37 | 31, 6, 27, 7, 8 | atcvrj0 37937 |
. . . . . . 7
β’ ((πΎ β HL β§ (π β (BaseβπΎ) β§ π β π΄ β§ π
β π΄) β§ ππΆ(π β¨ π
)) β (π = (0.βπΎ) β π = π
)) |
38 | 30, 33, 34, 35, 36, 37 | syl131anc 1384 |
. . . . . 6
β’ (((πΎ β HL β§ (π β π΄ β§ π β π΄ β§ π
β π΄)) β§ ππΆ(π β¨ π
)) β (π = (0.βπΎ) β π = π
)) |
39 | 38 | necon3bid 2985 |
. . . . 5
β’ (((πΎ β HL β§ (π β π΄ β§ π β π΄ β§ π
β π΄)) β§ ππΆ(π β¨ π
)) β (π β (0.βπΎ) β π β π
)) |
40 | 29, 39 | mpbid 231 |
. . . 4
β’ (((πΎ β HL β§ (π β π΄ β§ π β π΄ β§ π
β π΄)) β§ ππΆ(π β¨ π
)) β π β π
) |
41 | | hllat 37871 |
. . . . . . . 8
β’ (πΎ β HL β πΎ β Lat) |
42 | 41 | ad2antrr 725 |
. . . . . . 7
β’ (((πΎ β HL β§ (π β π΄ β§ π β π΄ β§ π
β π΄)) β§ ππΆ(π β¨ π
)) β πΎ β Lat) |
43 | 31, 8 | atbase 37797 |
. . . . . . . 8
β’ (π β π΄ β π β (BaseβπΎ)) |
44 | 34, 43 | syl 17 |
. . . . . . 7
β’ (((πΎ β HL β§ (π β π΄ β§ π β π΄ β§ π
β π΄)) β§ ππΆ(π β¨ π
)) β π β (BaseβπΎ)) |
45 | 31, 8 | atbase 37797 |
. . . . . . . 8
β’ (π
β π΄ β π
β (BaseβπΎ)) |
46 | 35, 45 | syl 17 |
. . . . . . 7
β’ (((πΎ β HL β§ (π β π΄ β§ π β π΄ β§ π
β π΄)) β§ ππΆ(π β¨ π
)) β π
β (BaseβπΎ)) |
47 | 31, 6 | latjcl 18333 |
. . . . . . 7
β’ ((πΎ β Lat β§ π β (BaseβπΎ) β§ π
β (BaseβπΎ)) β (π β¨ π
) β (BaseβπΎ)) |
48 | 42, 44, 46, 47 | syl3anc 1372 |
. . . . . 6
β’ (((πΎ β HL β§ (π β π΄ β§ π β π΄ β§ π
β π΄)) β§ ππΆ(π β¨ π
)) β (π β¨ π
) β (BaseβπΎ)) |
49 | 30, 33, 48 | 3jca 1129 |
. . . . 5
β’ (((πΎ β HL β§ (π β π΄ β§ π β π΄ β§ π
β π΄)) β§ ππΆ(π β¨ π
)) β (πΎ β HL β§ π β (BaseβπΎ) β§ (π β¨ π
) β (BaseβπΎ))) |
50 | 31, 19, 7 | cvrle 37786 |
. . . . 5
β’ (((πΎ β HL β§ π β (BaseβπΎ) β§ (π β¨ π
) β (BaseβπΎ)) β§ ππΆ(π β¨ π
)) β π β€ (π β¨ π
)) |
51 | 49, 50 | sylancom 589 |
. . . 4
β’ (((πΎ β HL β§ (π β π΄ β§ π β π΄ β§ π
β π΄)) β§ ππΆ(π β¨ π
)) β π β€ (π β¨ π
)) |
52 | 40, 51 | jca 513 |
. . 3
β’ (((πΎ β HL β§ (π β π΄ β§ π β π΄ β§ π
β π΄)) β§ ππΆ(π β¨ π
)) β (π β π
β§ π β€ (π β¨ π
))) |
53 | 52 | ex 414 |
. 2
β’ ((πΎ β HL β§ (π β π΄ β§ π β π΄ β§ π
β π΄)) β (ππΆ(π β¨ π
) β (π β π
β§ π β€ (π β¨ π
)))) |
54 | 23, 53 | impbid 211 |
1
β’ ((πΎ β HL β§ (π β π΄ β§ π β π΄ β§ π
β π΄)) β ((π β π
β§ π β€ (π β¨ π
)) β ππΆ(π β¨ π
))) |