Step | Hyp | Ref
| Expression |
1 | | simpl3l 1225 |
. . . . . . 7
β’ (((πΎ β HL β§ (π β π΄ β§ π β π΄ β§ π
β π΄) β§ (π β π
β§ π β€ (π β¨ π
))) β§ π = π
) β π β π
) |
2 | 1 | necomd 2990 |
. . . . . 6
β’ (((πΎ β HL β§ (π β π΄ β§ π β π΄ β§ π
β π΄) β§ (π β π
β§ π β€ (π β¨ π
))) β§ π = π
) β π
β π) |
3 | | simpl1 1188 |
. . . . . . 7
β’ (((πΎ β HL β§ (π β π΄ β§ π β π΄ β§ π
β π΄) β§ (π β π
β§ π β€ (π β¨ π
))) β§ π = π
) β πΎ β HL) |
4 | | simpl23 1250 |
. . . . . . 7
β’ (((πΎ β HL β§ (π β π΄ β§ π β π΄ β§ π
β π΄) β§ (π β π
β§ π β€ (π β¨ π
))) β§ π = π
) β π
β π΄) |
5 | | simpl22 1249 |
. . . . . . 7
β’ (((πΎ β HL β§ (π β π΄ β§ π β π΄ β§ π
β π΄) β§ (π β π
β§ π β€ (π β¨ π
))) β§ π = π
) β π β π΄) |
6 | | atcvrj1x.j |
. . . . . . . 8
β’ β¨ =
(joinβπΎ) |
7 | | atcvrj1x.c |
. . . . . . . 8
β’ πΆ = ( β βπΎ) |
8 | | atcvrj1x.a |
. . . . . . . 8
β’ π΄ = (AtomsβπΎ) |
9 | 6, 7, 8 | atcvr2 38802 |
. . . . . . 7
β’ ((πΎ β HL β§ π
β π΄ β§ π β π΄) β (π
β π β π
πΆ(π β¨ π
))) |
10 | 3, 4, 5, 9 | syl3anc 1368 |
. . . . . 6
β’ (((πΎ β HL β§ (π β π΄ β§ π β π΄ β§ π
β π΄) β§ (π β π
β§ π β€ (π β¨ π
))) β§ π = π
) β (π
β π β π
πΆ(π β¨ π
))) |
11 | 2, 10 | mpbid 231 |
. . . . 5
β’ (((πΎ β HL β§ (π β π΄ β§ π β π΄ β§ π
β π΄) β§ (π β π
β§ π β€ (π β¨ π
))) β§ π = π
) β π
πΆ(π β¨ π
)) |
12 | | breq1 5144 |
. . . . . 6
β’ (π = π
β (ππΆ(π β¨ π
) β π
πΆ(π β¨ π
))) |
13 | 12 | adantl 481 |
. . . . 5
β’ (((πΎ β HL β§ (π β π΄ β§ π β π΄ β§ π
β π΄) β§ (π β π
β§ π β€ (π β¨ π
))) β§ π = π
) β (ππΆ(π β¨ π
) β π
πΆ(π β¨ π
))) |
14 | 11, 13 | mpbird 257 |
. . . 4
β’ (((πΎ β HL β§ (π β π΄ β§ π β π΄ β§ π
β π΄) β§ (π β π
β§ π β€ (π β¨ π
))) β§ π = π
) β ππΆ(π β¨ π
)) |
15 | | simpl1 1188 |
. . . . 5
β’ (((πΎ β HL β§ (π β π΄ β§ π β π΄ β§ π
β π΄) β§ (π β π
β§ π β€ (π β¨ π
))) β§ π β π
) β πΎ β HL) |
16 | | simpl2 1189 |
. . . . 5
β’ (((πΎ β HL β§ (π β π΄ β§ π β π΄ β§ π
β π΄) β§ (π β π
β§ π β€ (π β¨ π
))) β§ π β π
) β (π β π΄ β§ π β π΄ β§ π
β π΄)) |
17 | | simpr 484 |
. . . . 5
β’ (((πΎ β HL β§ (π β π΄ β§ π β π΄ β§ π
β π΄) β§ (π β π
β§ π β€ (π β¨ π
))) β§ π β π
) β π β π
) |
18 | | simpl3r 1226 |
. . . . 5
β’ (((πΎ β HL β§ (π β π΄ β§ π β π΄ β§ π
β π΄) β§ (π β π
β§ π β€ (π β¨ π
))) β§ π β π
) β π β€ (π β¨ π
)) |
19 | | atcvrj1x.l |
. . . . . 6
β’ β€ =
(leβπΎ) |
20 | 19, 6, 7, 8 | atcvrj1 38815 |
. . . . 5
β’ ((πΎ β HL β§ (π β π΄ β§ π β π΄ β§ π
β π΄) β§ (π β π
β§ π β€ (π β¨ π
))) β ππΆ(π β¨ π
)) |
21 | 15, 16, 17, 18, 20 | syl112anc 1371 |
. . . 4
β’ (((πΎ β HL β§ (π β π΄ β§ π β π΄ β§ π
β π΄) β§ (π β π
β§ π β€ (π β¨ π
))) β§ π β π
) β ππΆ(π β¨ π
)) |
22 | 14, 21 | pm2.61dane 3023 |
. . 3
β’ ((πΎ β HL β§ (π β π΄ β§ π β π΄ β§ π
β π΄) β§ (π β π
β§ π β€ (π β¨ π
))) β ππΆ(π β¨ π
)) |
23 | 22 | 3expia 1118 |
. 2
β’ ((πΎ β HL β§ (π β π΄ β§ π β π΄ β§ π
β π΄)) β ((π β π
β§ π β€ (π β¨ π
)) β ππΆ(π β¨ π
))) |
24 | | hlatl 38743 |
. . . . . . 7
β’ (πΎ β HL β πΎ β AtLat) |
25 | 24 | ad2antrr 723 |
. . . . . 6
β’ (((πΎ β HL β§ (π β π΄ β§ π β π΄ β§ π
β π΄)) β§ ππΆ(π β¨ π
)) β πΎ β AtLat) |
26 | | simplr1 1212 |
. . . . . 6
β’ (((πΎ β HL β§ (π β π΄ β§ π β π΄ β§ π
β π΄)) β§ ππΆ(π β¨ π
)) β π β π΄) |
27 | | eqid 2726 |
. . . . . . 7
β’
(0.βπΎ) =
(0.βπΎ) |
28 | 27, 8 | atn0 38691 |
. . . . . 6
β’ ((πΎ β AtLat β§ π β π΄) β π β (0.βπΎ)) |
29 | 25, 26, 28 | syl2anc 583 |
. . . . 5
β’ (((πΎ β HL β§ (π β π΄ β§ π β π΄ β§ π
β π΄)) β§ ππΆ(π β¨ π
)) β π β (0.βπΎ)) |
30 | | simpll 764 |
. . . . . . 7
β’ (((πΎ β HL β§ (π β π΄ β§ π β π΄ β§ π
β π΄)) β§ ππΆ(π β¨ π
)) β πΎ β HL) |
31 | | eqid 2726 |
. . . . . . . . 9
β’
(BaseβπΎ) =
(BaseβπΎ) |
32 | 31, 8 | atbase 38672 |
. . . . . . . 8
β’ (π β π΄ β π β (BaseβπΎ)) |
33 | 26, 32 | syl 17 |
. . . . . . 7
β’ (((πΎ β HL β§ (π β π΄ β§ π β π΄ β§ π
β π΄)) β§ ππΆ(π β¨ π
)) β π β (BaseβπΎ)) |
34 | | simplr2 1213 |
. . . . . . 7
β’ (((πΎ β HL β§ (π β π΄ β§ π β π΄ β§ π
β π΄)) β§ ππΆ(π β¨ π
)) β π β π΄) |
35 | | simplr3 1214 |
. . . . . . 7
β’ (((πΎ β HL β§ (π β π΄ β§ π β π΄ β§ π
β π΄)) β§ ππΆ(π β¨ π
)) β π
β π΄) |
36 | | simpr 484 |
. . . . . . 7
β’ (((πΎ β HL β§ (π β π΄ β§ π β π΄ β§ π
β π΄)) β§ ππΆ(π β¨ π
)) β ππΆ(π β¨ π
)) |
37 | 31, 6, 27, 7, 8 | atcvrj0 38812 |
. . . . . . 7
β’ ((πΎ β HL β§ (π β (BaseβπΎ) β§ π β π΄ β§ π
β π΄) β§ ππΆ(π β¨ π
)) β (π = (0.βπΎ) β π = π
)) |
38 | 30, 33, 34, 35, 36, 37 | syl131anc 1380 |
. . . . . 6
β’ (((πΎ β HL β§ (π β π΄ β§ π β π΄ β§ π
β π΄)) β§ ππΆ(π β¨ π
)) β (π = (0.βπΎ) β π = π
)) |
39 | 38 | necon3bid 2979 |
. . . . 5
β’ (((πΎ β HL β§ (π β π΄ β§ π β π΄ β§ π
β π΄)) β§ ππΆ(π β¨ π
)) β (π β (0.βπΎ) β π β π
)) |
40 | 29, 39 | mpbid 231 |
. . . 4
β’ (((πΎ β HL β§ (π β π΄ β§ π β π΄ β§ π
β π΄)) β§ ππΆ(π β¨ π
)) β π β π
) |
41 | | hllat 38746 |
. . . . . . . 8
β’ (πΎ β HL β πΎ β Lat) |
42 | 41 | ad2antrr 723 |
. . . . . . 7
β’ (((πΎ β HL β§ (π β π΄ β§ π β π΄ β§ π
β π΄)) β§ ππΆ(π β¨ π
)) β πΎ β Lat) |
43 | 31, 8 | atbase 38672 |
. . . . . . . 8
β’ (π β π΄ β π β (BaseβπΎ)) |
44 | 34, 43 | syl 17 |
. . . . . . 7
β’ (((πΎ β HL β§ (π β π΄ β§ π β π΄ β§ π
β π΄)) β§ ππΆ(π β¨ π
)) β π β (BaseβπΎ)) |
45 | 31, 8 | atbase 38672 |
. . . . . . . 8
β’ (π
β π΄ β π
β (BaseβπΎ)) |
46 | 35, 45 | syl 17 |
. . . . . . 7
β’ (((πΎ β HL β§ (π β π΄ β§ π β π΄ β§ π
β π΄)) β§ ππΆ(π β¨ π
)) β π
β (BaseβπΎ)) |
47 | 31, 6 | latjcl 18404 |
. . . . . . 7
β’ ((πΎ β Lat β§ π β (BaseβπΎ) β§ π
β (BaseβπΎ)) β (π β¨ π
) β (BaseβπΎ)) |
48 | 42, 44, 46, 47 | syl3anc 1368 |
. . . . . 6
β’ (((πΎ β HL β§ (π β π΄ β§ π β π΄ β§ π
β π΄)) β§ ππΆ(π β¨ π
)) β (π β¨ π
) β (BaseβπΎ)) |
49 | 30, 33, 48 | 3jca 1125 |
. . . . 5
β’ (((πΎ β HL β§ (π β π΄ β§ π β π΄ β§ π
β π΄)) β§ ππΆ(π β¨ π
)) β (πΎ β HL β§ π β (BaseβπΎ) β§ (π β¨ π
) β (BaseβπΎ))) |
50 | 31, 19, 7 | cvrle 38661 |
. . . . 5
β’ (((πΎ β HL β§ π β (BaseβπΎ) β§ (π β¨ π
) β (BaseβπΎ)) β§ ππΆ(π β¨ π
)) β π β€ (π β¨ π
)) |
51 | 49, 50 | sylancom 587 |
. . . 4
β’ (((πΎ β HL β§ (π β π΄ β§ π β π΄ β§ π
β π΄)) β§ ππΆ(π β¨ π
)) β π β€ (π β¨ π
)) |
52 | 40, 51 | jca 511 |
. . 3
β’ (((πΎ β HL β§ (π β π΄ β§ π β π΄ β§ π
β π΄)) β§ ππΆ(π β¨ π
)) β (π β π
β§ π β€ (π β¨ π
))) |
53 | 52 | ex 412 |
. 2
β’ ((πΎ β HL β§ (π β π΄ β§ π β π΄ β§ π
β π΄)) β (ππΆ(π β¨ π
) β (π β π
β§ π β€ (π β¨ π
)))) |
54 | 23, 53 | impbid 211 |
1
β’ ((πΎ β HL β§ (π β π΄ β§ π β π΄ β§ π
β π΄)) β ((π β π
β§ π β€ (π β¨ π
)) β ππΆ(π β¨ π
))) |