Step | Hyp | Ref
| Expression |
1 | | hlclat 38314 |
. . . . . 6
β’ (πΎ β HL β πΎ β CLat) |
2 | 1 | 3ad2ant1 1133 |
. . . . 5
β’ ((πΎ β HL β§ π β πΆ β§ π β π΄) β πΎ β CLat) |
3 | | paddatcl.a |
. . . . . . . 8
β’ π΄ = (AtomsβπΎ) |
4 | | paddatcl.c |
. . . . . . . 8
β’ πΆ = (PSubClβπΎ) |
5 | 3, 4 | psubclssatN 38898 |
. . . . . . 7
β’ ((πΎ β HL β§ π β πΆ) β π β π΄) |
6 | | eqid 2732 |
. . . . . . . 8
β’
(BaseβπΎ) =
(BaseβπΎ) |
7 | 6, 3 | atssbase 38246 |
. . . . . . 7
β’ π΄ β (BaseβπΎ) |
8 | 5, 7 | sstrdi 3994 |
. . . . . 6
β’ ((πΎ β HL β§ π β πΆ) β π β (BaseβπΎ)) |
9 | 8 | 3adant3 1132 |
. . . . 5
β’ ((πΎ β HL β§ π β πΆ β§ π β π΄) β π β (BaseβπΎ)) |
10 | | eqid 2732 |
. . . . . 6
β’
(lubβπΎ) =
(lubβπΎ) |
11 | 6, 10 | clatlubcl 18458 |
. . . . 5
β’ ((πΎ β CLat β§ π β (BaseβπΎ)) β ((lubβπΎ)βπ) β (BaseβπΎ)) |
12 | 2, 9, 11 | syl2anc 584 |
. . . 4
β’ ((πΎ β HL β§ π β πΆ β§ π β π΄) β ((lubβπΎ)βπ) β (BaseβπΎ)) |
13 | | eqid 2732 |
. . . . 5
β’
(joinβπΎ) =
(joinβπΎ) |
14 | | eqid 2732 |
. . . . 5
β’
(pmapβπΎ) =
(pmapβπΎ) |
15 | | paddatcl.p |
. . . . 5
β’ + =
(+πβπΎ) |
16 | 6, 13, 3, 14, 15 | pmapjat1 38810 |
. . . 4
β’ ((πΎ β HL β§
((lubβπΎ)βπ) β (BaseβπΎ) β§ π β π΄) β ((pmapβπΎ)β(((lubβπΎ)βπ)(joinβπΎ)π)) = (((pmapβπΎ)β((lubβπΎ)βπ)) + ((pmapβπΎ)βπ))) |
17 | 12, 16 | syld3an2 1411 |
. . 3
β’ ((πΎ β HL β§ π β πΆ β§ π β π΄) β ((pmapβπΎ)β(((lubβπΎ)βπ)(joinβπΎ)π)) = (((pmapβπΎ)β((lubβπΎ)βπ)) + ((pmapβπΎ)βπ))) |
18 | 10, 14, 4 | pmapidclN 38899 |
. . . . 5
β’ ((πΎ β HL β§ π β πΆ) β ((pmapβπΎ)β((lubβπΎ)βπ)) = π) |
19 | 18 | 3adant3 1132 |
. . . 4
β’ ((πΎ β HL β§ π β πΆ β§ π β π΄) β ((pmapβπΎ)β((lubβπΎ)βπ)) = π) |
20 | 3, 14 | pmapat 38720 |
. . . . 5
β’ ((πΎ β HL β§ π β π΄) β ((pmapβπΎ)βπ) = {π}) |
21 | 20 | 3adant2 1131 |
. . . 4
β’ ((πΎ β HL β§ π β πΆ β§ π β π΄) β ((pmapβπΎ)βπ) = {π}) |
22 | 19, 21 | oveq12d 7429 |
. . 3
β’ ((πΎ β HL β§ π β πΆ β§ π β π΄) β (((pmapβπΎ)β((lubβπΎ)βπ)) + ((pmapβπΎ)βπ)) = (π + {π})) |
23 | 17, 22 | eqtr2d 2773 |
. 2
β’ ((πΎ β HL β§ π β πΆ β§ π β π΄) β (π + {π}) = ((pmapβπΎ)β(((lubβπΎ)βπ)(joinβπΎ)π))) |
24 | | simp1 1136 |
. . 3
β’ ((πΎ β HL β§ π β πΆ β§ π β π΄) β πΎ β HL) |
25 | | hllat 38319 |
. . . . 5
β’ (πΎ β HL β πΎ β Lat) |
26 | 25 | 3ad2ant1 1133 |
. . . 4
β’ ((πΎ β HL β§ π β πΆ β§ π β π΄) β πΎ β Lat) |
27 | 6, 3 | atbase 38245 |
. . . . 5
β’ (π β π΄ β π β (BaseβπΎ)) |
28 | 27 | 3ad2ant3 1135 |
. . . 4
β’ ((πΎ β HL β§ π β πΆ β§ π β π΄) β π β (BaseβπΎ)) |
29 | 6, 13 | latjcl 18394 |
. . . 4
β’ ((πΎ β Lat β§
((lubβπΎ)βπ) β (BaseβπΎ) β§ π β (BaseβπΎ)) β (((lubβπΎ)βπ)(joinβπΎ)π) β (BaseβπΎ)) |
30 | 26, 12, 28, 29 | syl3anc 1371 |
. . 3
β’ ((πΎ β HL β§ π β πΆ β§ π β π΄) β (((lubβπΎ)βπ)(joinβπΎ)π) β (BaseβπΎ)) |
31 | 6, 14, 4 | pmapsubclN 38903 |
. . 3
β’ ((πΎ β HL β§
(((lubβπΎ)βπ)(joinβπΎ)π) β (BaseβπΎ)) β ((pmapβπΎ)β(((lubβπΎ)βπ)(joinβπΎ)π)) β πΆ) |
32 | 24, 30, 31 | syl2anc 584 |
. 2
β’ ((πΎ β HL β§ π β πΆ β§ π β π΄) β ((pmapβπΎ)β(((lubβπΎ)βπ)(joinβπΎ)π)) β πΆ) |
33 | 23, 32 | eqeltrd 2833 |
1
β’ ((πΎ β HL β§ π β πΆ β§ π β π΄) β (π + {π}) β πΆ) |