Step | Hyp | Ref
| Expression |
1 | | eqid 2732 |
. . 3
β’
(leβπΎ) =
(leβπΎ) |
2 | | isline2.j |
. . 3
β’ β¨ =
(joinβπΎ) |
3 | | isline2.a |
. . 3
β’ π΄ = (AtomsβπΎ) |
4 | | isline2.n |
. . 3
β’ π = (LinesβπΎ) |
5 | 1, 2, 3, 4 | isline 38598 |
. 2
β’ (πΎ β Lat β (π β π β βπ β π΄ βπ β π΄ (π β π β§ π = {π β π΄ β£ π(leβπΎ)(π β¨ π)}))) |
6 | | simpl 483 |
. . . . . . 7
β’ ((πΎ β Lat β§ (π β π΄ β§ π β π΄)) β πΎ β Lat) |
7 | | eqid 2732 |
. . . . . . . . 9
β’
(BaseβπΎ) =
(BaseβπΎ) |
8 | 7, 3 | atbase 38147 |
. . . . . . . 8
β’ (π β π΄ β π β (BaseβπΎ)) |
9 | 8 | ad2antrl 726 |
. . . . . . 7
β’ ((πΎ β Lat β§ (π β π΄ β§ π β π΄)) β π β (BaseβπΎ)) |
10 | 7, 3 | atbase 38147 |
. . . . . . . 8
β’ (π β π΄ β π β (BaseβπΎ)) |
11 | 10 | ad2antll 727 |
. . . . . . 7
β’ ((πΎ β Lat β§ (π β π΄ β§ π β π΄)) β π β (BaseβπΎ)) |
12 | 7, 2 | latjcl 18388 |
. . . . . . 7
β’ ((πΎ β Lat β§ π β (BaseβπΎ) β§ π β (BaseβπΎ)) β (π β¨ π) β (BaseβπΎ)) |
13 | 6, 9, 11, 12 | syl3anc 1371 |
. . . . . 6
β’ ((πΎ β Lat β§ (π β π΄ β§ π β π΄)) β (π β¨ π) β (BaseβπΎ)) |
14 | | isline2.m |
. . . . . . 7
β’ π = (pmapβπΎ) |
15 | 7, 1, 3, 14 | pmapval 38616 |
. . . . . 6
β’ ((πΎ β Lat β§ (π β¨ π) β (BaseβπΎ)) β (πβ(π β¨ π)) = {π β π΄ β£ π(leβπΎ)(π β¨ π)}) |
16 | 13, 15 | syldan 591 |
. . . . 5
β’ ((πΎ β Lat β§ (π β π΄ β§ π β π΄)) β (πβ(π β¨ π)) = {π β π΄ β£ π(leβπΎ)(π β¨ π)}) |
17 | 16 | eqeq2d 2743 |
. . . 4
β’ ((πΎ β Lat β§ (π β π΄ β§ π β π΄)) β (π = (πβ(π β¨ π)) β π = {π β π΄ β£ π(leβπΎ)(π β¨ π)})) |
18 | 17 | anbi2d 629 |
. . 3
β’ ((πΎ β Lat β§ (π β π΄ β§ π β π΄)) β ((π β π β§ π = (πβ(π β¨ π))) β (π β π β§ π = {π β π΄ β£ π(leβπΎ)(π β¨ π)}))) |
19 | 18 | 2rexbidva 3217 |
. 2
β’ (πΎ β Lat β (βπ β π΄ βπ β π΄ (π β π β§ π = (πβ(π β¨ π))) β βπ β π΄ βπ β π΄ (π β π β§ π = {π β π΄ β£ π(leβπΎ)(π β¨ π)}))) |
20 | 5, 19 | bitr4d 281 |
1
β’ (πΎ β Lat β (π β π β βπ β π΄ βπ β π΄ (π β π β§ π = (πβ(π β¨ π))))) |