Step | Hyp | Ref
| Expression |
1 | | hllat 37828 |
. . . 4
β’ (πΎ β HL β πΎ β Lat) |
2 | | eqid 2737 |
. . . . 5
β’
(joinβπΎ) =
(joinβπΎ) |
3 | | eqid 2737 |
. . . . 5
β’
(AtomsβπΎ) =
(AtomsβπΎ) |
4 | | linepsubcl.n |
. . . . 5
β’ π = (LinesβπΎ) |
5 | | eqid 2737 |
. . . . 5
β’
(pmapβπΎ) =
(pmapβπΎ) |
6 | 2, 3, 4, 5 | isline2 38240 |
. . . 4
β’ (πΎ β Lat β (π β π β βπ β (AtomsβπΎ)βπ β (AtomsβπΎ)(π β π β§ π = ((pmapβπΎ)β(π(joinβπΎ)π))))) |
7 | 1, 6 | syl 17 |
. . 3
β’ (πΎ β HL β (π β π β βπ β (AtomsβπΎ)βπ β (AtomsβπΎ)(π β π β§ π = ((pmapβπΎ)β(π(joinβπΎ)π))))) |
8 | 1 | adantr 482 |
. . . . . . . 8
β’ ((πΎ β HL β§ (π β (AtomsβπΎ) β§ π β (AtomsβπΎ))) β πΎ β Lat) |
9 | | eqid 2737 |
. . . . . . . . . 10
β’
(BaseβπΎ) =
(BaseβπΎ) |
10 | 9, 3 | atbase 37754 |
. . . . . . . . 9
β’ (π β (AtomsβπΎ) β π β (BaseβπΎ)) |
11 | 10 | ad2antrl 727 |
. . . . . . . 8
β’ ((πΎ β HL β§ (π β (AtomsβπΎ) β§ π β (AtomsβπΎ))) β π β (BaseβπΎ)) |
12 | 9, 3 | atbase 37754 |
. . . . . . . . 9
β’ (π β (AtomsβπΎ) β π β (BaseβπΎ)) |
13 | 12 | ad2antll 728 |
. . . . . . . 8
β’ ((πΎ β HL β§ (π β (AtomsβπΎ) β§ π β (AtomsβπΎ))) β π β (BaseβπΎ)) |
14 | 9, 2 | latjcl 18329 |
. . . . . . . 8
β’ ((πΎ β Lat β§ π β (BaseβπΎ) β§ π β (BaseβπΎ)) β (π(joinβπΎ)π) β (BaseβπΎ)) |
15 | 8, 11, 13, 14 | syl3anc 1372 |
. . . . . . 7
β’ ((πΎ β HL β§ (π β (AtomsβπΎ) β§ π β (AtomsβπΎ))) β (π(joinβπΎ)π) β (BaseβπΎ)) |
16 | | linepsubcl.c |
. . . . . . . 8
β’ πΆ = (PSubClβπΎ) |
17 | 9, 5, 16 | pmapsubclN 38412 |
. . . . . . 7
β’ ((πΎ β HL β§ (π(joinβπΎ)π) β (BaseβπΎ)) β ((pmapβπΎ)β(π(joinβπΎ)π)) β πΆ) |
18 | 15, 17 | syldan 592 |
. . . . . 6
β’ ((πΎ β HL β§ (π β (AtomsβπΎ) β§ π β (AtomsβπΎ))) β ((pmapβπΎ)β(π(joinβπΎ)π)) β πΆ) |
19 | | eleq1a 2833 |
. . . . . 6
β’
(((pmapβπΎ)β(π(joinβπΎ)π)) β πΆ β (π = ((pmapβπΎ)β(π(joinβπΎ)π)) β π β πΆ)) |
20 | 18, 19 | syl 17 |
. . . . 5
β’ ((πΎ β HL β§ (π β (AtomsβπΎ) β§ π β (AtomsβπΎ))) β (π = ((pmapβπΎ)β(π(joinβπΎ)π)) β π β πΆ)) |
21 | 20 | adantld 492 |
. . . 4
β’ ((πΎ β HL β§ (π β (AtomsβπΎ) β§ π β (AtomsβπΎ))) β ((π β π β§ π = ((pmapβπΎ)β(π(joinβπΎ)π))) β π β πΆ)) |
22 | 21 | rexlimdvva 3206 |
. . 3
β’ (πΎ β HL β (βπ β (AtomsβπΎ)βπ β (AtomsβπΎ)(π β π β§ π = ((pmapβπΎ)β(π(joinβπΎ)π))) β π β πΆ)) |
23 | 7, 22 | sylbid 239 |
. 2
β’ (πΎ β HL β (π β π β π β πΆ)) |
24 | 23 | imp 408 |
1
β’ ((πΎ β HL β§ π β π) β π β πΆ) |