Step | Hyp | Ref
| Expression |
1 | | simp1 1137 |
. . . 4
β’ ((πΎ β HL β§ π β πΆ β§ π β πΆ) β πΎ β HL) |
2 | | hlclat 37823 |
. . . . . 6
β’ (πΎ β HL β πΎ β CLat) |
3 | 2 | 3ad2ant1 1134 |
. . . . 5
β’ ((πΎ β HL β§ π β πΆ β§ π β πΆ) β πΎ β CLat) |
4 | | eqid 2737 |
. . . . . . . 8
β’
(AtomsβπΎ) =
(AtomsβπΎ) |
5 | | psubclin.c |
. . . . . . . 8
β’ πΆ = (PSubClβπΎ) |
6 | 4, 5 | psubclssatN 38407 |
. . . . . . 7
β’ ((πΎ β HL β§ π β πΆ) β π β (AtomsβπΎ)) |
7 | 6 | 3adant3 1133 |
. . . . . 6
β’ ((πΎ β HL β§ π β πΆ β§ π β πΆ) β π β (AtomsβπΎ)) |
8 | | eqid 2737 |
. . . . . . 7
β’
(BaseβπΎ) =
(BaseβπΎ) |
9 | 8, 4 | atssbase 37755 |
. . . . . 6
β’
(AtomsβπΎ)
β (BaseβπΎ) |
10 | 7, 9 | sstrdi 3957 |
. . . . 5
β’ ((πΎ β HL β§ π β πΆ β§ π β πΆ) β π β (BaseβπΎ)) |
11 | | eqid 2737 |
. . . . . 6
β’
(lubβπΎ) =
(lubβπΎ) |
12 | 8, 11 | clatlubcl 18393 |
. . . . 5
β’ ((πΎ β CLat β§ π β (BaseβπΎ)) β ((lubβπΎ)βπ) β (BaseβπΎ)) |
13 | 3, 10, 12 | syl2anc 585 |
. . . 4
β’ ((πΎ β HL β§ π β πΆ β§ π β πΆ) β ((lubβπΎ)βπ) β (BaseβπΎ)) |
14 | 4, 5 | psubclssatN 38407 |
. . . . . . 7
β’ ((πΎ β HL β§ π β πΆ) β π β (AtomsβπΎ)) |
15 | 14 | 3adant2 1132 |
. . . . . 6
β’ ((πΎ β HL β§ π β πΆ β§ π β πΆ) β π β (AtomsβπΎ)) |
16 | 15, 9 | sstrdi 3957 |
. . . . 5
β’ ((πΎ β HL β§ π β πΆ β§ π β πΆ) β π β (BaseβπΎ)) |
17 | 8, 11 | clatlubcl 18393 |
. . . . 5
β’ ((πΎ β CLat β§ π β (BaseβπΎ)) β ((lubβπΎ)βπ) β (BaseβπΎ)) |
18 | 3, 16, 17 | syl2anc 585 |
. . . 4
β’ ((πΎ β HL β§ π β πΆ β§ π β πΆ) β ((lubβπΎ)βπ) β (BaseβπΎ)) |
19 | | eqid 2737 |
. . . . 5
β’
(meetβπΎ) =
(meetβπΎ) |
20 | | eqid 2737 |
. . . . 5
β’
(pmapβπΎ) =
(pmapβπΎ) |
21 | 8, 19, 4, 20 | pmapmeet 38239 |
. . . 4
β’ ((πΎ β HL β§
((lubβπΎ)βπ) β (BaseβπΎ) β§ ((lubβπΎ)βπ) β (BaseβπΎ)) β ((pmapβπΎ)β(((lubβπΎ)βπ)(meetβπΎ)((lubβπΎ)βπ))) = (((pmapβπΎ)β((lubβπΎ)βπ)) β© ((pmapβπΎ)β((lubβπΎ)βπ)))) |
22 | 1, 13, 18, 21 | syl3anc 1372 |
. . 3
β’ ((πΎ β HL β§ π β πΆ β§ π β πΆ) β ((pmapβπΎ)β(((lubβπΎ)βπ)(meetβπΎ)((lubβπΎ)βπ))) = (((pmapβπΎ)β((lubβπΎ)βπ)) β© ((pmapβπΎ)β((lubβπΎ)βπ)))) |
23 | 11, 20, 5 | pmapidclN 38408 |
. . . . 5
β’ ((πΎ β HL β§ π β πΆ) β ((pmapβπΎ)β((lubβπΎ)βπ)) = π) |
24 | 23 | 3adant3 1133 |
. . . 4
β’ ((πΎ β HL β§ π β πΆ β§ π β πΆ) β ((pmapβπΎ)β((lubβπΎ)βπ)) = π) |
25 | 11, 20, 5 | pmapidclN 38408 |
. . . . 5
β’ ((πΎ β HL β§ π β πΆ) β ((pmapβπΎ)β((lubβπΎ)βπ)) = π) |
26 | 25 | 3adant2 1132 |
. . . 4
β’ ((πΎ β HL β§ π β πΆ β§ π β πΆ) β ((pmapβπΎ)β((lubβπΎ)βπ)) = π) |
27 | 24, 26 | ineq12d 4174 |
. . 3
β’ ((πΎ β HL β§ π β πΆ β§ π β πΆ) β (((pmapβπΎ)β((lubβπΎ)βπ)) β© ((pmapβπΎ)β((lubβπΎ)βπ))) = (π β© π)) |
28 | 22, 27 | eqtrd 2777 |
. 2
β’ ((πΎ β HL β§ π β πΆ β§ π β πΆ) β ((pmapβπΎ)β(((lubβπΎ)βπ)(meetβπΎ)((lubβπΎ)βπ))) = (π β© π)) |
29 | | hllat 37828 |
. . . . 5
β’ (πΎ β HL β πΎ β Lat) |
30 | 29 | 3ad2ant1 1134 |
. . . 4
β’ ((πΎ β HL β§ π β πΆ β§ π β πΆ) β πΎ β Lat) |
31 | 8, 19 | latmcl 18330 |
. . . 4
β’ ((πΎ β Lat β§
((lubβπΎ)βπ) β (BaseβπΎ) β§ ((lubβπΎ)βπ) β (BaseβπΎ)) β (((lubβπΎ)βπ)(meetβπΎ)((lubβπΎ)βπ)) β (BaseβπΎ)) |
32 | 30, 13, 18, 31 | syl3anc 1372 |
. . 3
β’ ((πΎ β HL β§ π β πΆ β§ π β πΆ) β (((lubβπΎ)βπ)(meetβπΎ)((lubβπΎ)βπ)) β (BaseβπΎ)) |
33 | 8, 20, 5 | pmapsubclN 38412 |
. . 3
β’ ((πΎ β HL β§
(((lubβπΎ)βπ)(meetβπΎ)((lubβπΎ)βπ)) β (BaseβπΎ)) β ((pmapβπΎ)β(((lubβπΎ)βπ)(meetβπΎ)((lubβπΎ)βπ))) β πΆ) |
34 | 1, 32, 33 | syl2anc 585 |
. 2
β’ ((πΎ β HL β§ π β πΆ β§ π β πΆ) β ((pmapβπΎ)β(((lubβπΎ)βπ)(meetβπΎ)((lubβπΎ)βπ))) β πΆ) |
35 | 28, 34 | eqeltrrd 2839 |
1
β’ ((πΎ β HL β§ π β πΆ β§ π β πΆ) β (π β© π) β πΆ) |