Step | Hyp | Ref
| Expression |
1 | | hlclat 37823 |
. . . . . 6
β’ (πΎ β HL β πΎ β CLat) |
2 | 1 | 3ad2ant1 1134 |
. . . . 5
β’ ((πΎ β HL β§ π β πΆ β§ π β π΄) β πΎ β CLat) |
3 | | paddatcl.a |
. . . . . . . 8
β’ π΄ = (AtomsβπΎ) |
4 | | paddatcl.c |
. . . . . . . 8
β’ πΆ = (PSubClβπΎ) |
5 | 3, 4 | psubclssatN 38407 |
. . . . . . 7
β’ ((πΎ β HL β§ π β πΆ) β π β π΄) |
6 | | eqid 2737 |
. . . . . . . 8
β’
(BaseβπΎ) =
(BaseβπΎ) |
7 | 6, 3 | atssbase 37755 |
. . . . . . 7
β’ π΄ β (BaseβπΎ) |
8 | 5, 7 | sstrdi 3957 |
. . . . . 6
β’ ((πΎ β HL β§ π β πΆ) β π β (BaseβπΎ)) |
9 | 8 | 3adant3 1133 |
. . . . 5
β’ ((πΎ β HL β§ π β πΆ β§ π β π΄) β π β (BaseβπΎ)) |
10 | | eqid 2737 |
. . . . . 6
β’
(lubβπΎ) =
(lubβπΎ) |
11 | 6, 10 | clatlubcl 18393 |
. . . . 5
β’ ((πΎ β CLat β§ π β (BaseβπΎ)) β ((lubβπΎ)βπ) β (BaseβπΎ)) |
12 | 2, 9, 11 | syl2anc 585 |
. . . 4
β’ ((πΎ β HL β§ π β πΆ β§ π β π΄) β ((lubβπΎ)βπ) β (BaseβπΎ)) |
13 | | eqid 2737 |
. . . . 5
β’
(joinβπΎ) =
(joinβπΎ) |
14 | | eqid 2737 |
. . . . 5
β’
(pmapβπΎ) =
(pmapβπΎ) |
15 | | paddatcl.p |
. . . . 5
β’ + =
(+πβπΎ) |
16 | 6, 13, 3, 14, 15 | pmapjat1 38319 |
. . . 4
β’ ((πΎ β HL β§
((lubβπΎ)βπ) β (BaseβπΎ) β§ π β π΄) β ((pmapβπΎ)β(((lubβπΎ)βπ)(joinβπΎ)π)) = (((pmapβπΎ)β((lubβπΎ)βπ)) + ((pmapβπΎ)βπ))) |
17 | 12, 16 | syld3an2 1412 |
. . 3
β’ ((πΎ β HL β§ π β πΆ β§ π β π΄) β ((pmapβπΎ)β(((lubβπΎ)βπ)(joinβπΎ)π)) = (((pmapβπΎ)β((lubβπΎ)βπ)) + ((pmapβπΎ)βπ))) |
18 | 10, 14, 4 | pmapidclN 38408 |
. . . . 5
β’ ((πΎ β HL β§ π β πΆ) β ((pmapβπΎ)β((lubβπΎ)βπ)) = π) |
19 | 18 | 3adant3 1133 |
. . . 4
β’ ((πΎ β HL β§ π β πΆ β§ π β π΄) β ((pmapβπΎ)β((lubβπΎ)βπ)) = π) |
20 | 3, 14 | pmapat 38229 |
. . . . 5
β’ ((πΎ β HL β§ π β π΄) β ((pmapβπΎ)βπ) = {π}) |
21 | 20 | 3adant2 1132 |
. . . 4
β’ ((πΎ β HL β§ π β πΆ β§ π β π΄) β ((pmapβπΎ)βπ) = {π}) |
22 | 19, 21 | oveq12d 7376 |
. . 3
β’ ((πΎ β HL β§ π β πΆ β§ π β π΄) β (((pmapβπΎ)β((lubβπΎ)βπ)) + ((pmapβπΎ)βπ)) = (π + {π})) |
23 | 17, 22 | eqtr2d 2778 |
. 2
β’ ((πΎ β HL β§ π β πΆ β§ π β π΄) β (π + {π}) = ((pmapβπΎ)β(((lubβπΎ)βπ)(joinβπΎ)π))) |
24 | | simp1 1137 |
. . 3
β’ ((πΎ β HL β§ π β πΆ β§ π β π΄) β πΎ β HL) |
25 | | hllat 37828 |
. . . . 5
β’ (πΎ β HL β πΎ β Lat) |
26 | 25 | 3ad2ant1 1134 |
. . . 4
β’ ((πΎ β HL β§ π β πΆ β§ π β π΄) β πΎ β Lat) |
27 | 6, 3 | atbase 37754 |
. . . . 5
β’ (π β π΄ β π β (BaseβπΎ)) |
28 | 27 | 3ad2ant3 1136 |
. . . 4
β’ ((πΎ β HL β§ π β πΆ β§ π β π΄) β π β (BaseβπΎ)) |
29 | 6, 13 | latjcl 18329 |
. . . 4
β’ ((πΎ β Lat β§
((lubβπΎ)βπ) β (BaseβπΎ) β§ π β (BaseβπΎ)) β (((lubβπΎ)βπ)(joinβπΎ)π) β (BaseβπΎ)) |
30 | 26, 12, 28, 29 | syl3anc 1372 |
. . 3
β’ ((πΎ β HL β§ π β πΆ β§ π β π΄) β (((lubβπΎ)βπ)(joinβπΎ)π) β (BaseβπΎ)) |
31 | 6, 14, 4 | pmapsubclN 38412 |
. . 3
β’ ((πΎ β HL β§
(((lubβπΎ)βπ)(joinβπΎ)π) β (BaseβπΎ)) β ((pmapβπΎ)β(((lubβπΎ)βπ)(joinβπΎ)π)) β πΆ) |
32 | 24, 30, 31 | syl2anc 585 |
. 2
β’ ((πΎ β HL β§ π β πΆ β§ π β π΄) β ((pmapβπΎ)β(((lubβπΎ)βπ)(joinβπΎ)π)) β πΆ) |
33 | 23, 32 | eqeltrd 2838 |
1
β’ ((πΎ β HL β§ π β πΆ β§ π β π΄) β (π + {π}) β πΆ) |