Step | Hyp | Ref
| Expression |
1 | | simpl 484 |
. . . 4
β’ (((πΎ β HL β§ π β π») β§ π β dom πΌ) β (πΎ β HL β§ π β π»)) |
2 | | eqid 2737 |
. . . . 5
β’
(BaseβπΎ) =
(BaseβπΎ) |
3 | | diaoc.h |
. . . . 5
β’ π» = (LHypβπΎ) |
4 | | diaoc.i |
. . . . 5
β’ πΌ = ((DIsoAβπΎ)βπ) |
5 | 2, 3, 4 | diadmclN 39503 |
. . . 4
β’ (((πΎ β HL β§ π β π») β§ π β dom πΌ) β π β (BaseβπΎ)) |
6 | | eqid 2737 |
. . . . 5
β’
(leβπΎ) =
(leβπΎ) |
7 | 6, 3, 4 | diadmleN 39504 |
. . . 4
β’ (((πΎ β HL β§ π β π») β§ π β dom πΌ) β π(leβπΎ)π) |
8 | | diaoc.t |
. . . . 5
β’ π = ((LTrnβπΎ)βπ) |
9 | 2, 6, 3, 8, 4 | diass 39508 |
. . . 4
β’ (((πΎ β HL β§ π β π») β§ (π β (BaseβπΎ) β§ π(leβπΎ)π)) β (πΌβπ) β π) |
10 | 1, 5, 7, 9 | syl12anc 836 |
. . 3
β’ (((πΎ β HL β§ π β π») β§ π β dom πΌ) β (πΌβπ) β π) |
11 | | diaoc.j |
. . . 4
β’ β¨ =
(joinβπΎ) |
12 | | diaoc.m |
. . . 4
β’ β§ =
(meetβπΎ) |
13 | | diaoc.o |
. . . 4
β’ β₯ =
(ocβπΎ) |
14 | | diaoc.n |
. . . 4
β’ π = ((ocAβπΎ)βπ) |
15 | 11, 12, 13, 3, 8, 4,
14 | docavalN 39589 |
. . 3
β’ (((πΎ β HL β§ π β π») β§ (πΌβπ) β π) β (πβ(πΌβπ)) = (πΌβ((( β₯ β(β‘πΌββ© {π§ β ran πΌ β£ (πΌβπ) β π§})) β¨ ( β₯ βπ)) β§ π))) |
16 | 10, 15 | syldan 592 |
. 2
β’ (((πΎ β HL β§ π β π») β§ π β dom πΌ) β (πβ(πΌβπ)) = (πΌβ((( β₯ β(β‘πΌββ© {π§ β ran πΌ β£ (πΌβπ) β π§})) β¨ ( β₯ βπ)) β§ π))) |
17 | 3, 4 | diaclN 39516 |
. . . . . . . 8
β’ (((πΎ β HL β§ π β π») β§ π β dom πΌ) β (πΌβπ) β ran πΌ) |
18 | | intmin 4930 |
. . . . . . . 8
β’ ((πΌβπ) β ran πΌ β β© {π§ β ran πΌ β£ (πΌβπ) β π§} = (πΌβπ)) |
19 | 17, 18 | syl 17 |
. . . . . . 7
β’ (((πΎ β HL β§ π β π») β§ π β dom πΌ) β β© {π§ β ran πΌ β£ (πΌβπ) β π§} = (πΌβπ)) |
20 | 19 | fveq2d 6847 |
. . . . . 6
β’ (((πΎ β HL β§ π β π») β§ π β dom πΌ) β (β‘πΌββ© {π§ β ran πΌ β£ (πΌβπ) β π§}) = (β‘πΌβ(πΌβπ))) |
21 | 3, 4 | diaf11N 39515 |
. . . . . . 7
β’ ((πΎ β HL β§ π β π») β πΌ:dom πΌβ1-1-ontoβran
πΌ) |
22 | | f1ocnvfv1 7223 |
. . . . . . 7
β’ ((πΌ:dom πΌβ1-1-ontoβran
πΌ β§ π β dom πΌ) β (β‘πΌβ(πΌβπ)) = π) |
23 | 21, 22 | sylan 581 |
. . . . . 6
β’ (((πΎ β HL β§ π β π») β§ π β dom πΌ) β (β‘πΌβ(πΌβπ)) = π) |
24 | 20, 23 | eqtrd 2777 |
. . . . 5
β’ (((πΎ β HL β§ π β π») β§ π β dom πΌ) β (β‘πΌββ© {π§ β ran πΌ β£ (πΌβπ) β π§}) = π) |
25 | 24 | fveq2d 6847 |
. . . 4
β’ (((πΎ β HL β§ π β π») β§ π β dom πΌ) β ( β₯ β(β‘πΌββ© {π§ β ran πΌ β£ (πΌβπ) β π§})) = ( β₯ βπ)) |
26 | 25 | oveq1d 7373 |
. . 3
β’ (((πΎ β HL β§ π β π») β§ π β dom πΌ) β (( β₯ β(β‘πΌββ© {π§ β ran πΌ β£ (πΌβπ) β π§})) β¨ ( β₯ βπ)) = (( β₯ βπ) β¨ ( β₯ βπ))) |
27 | 26 | fvoveq1d 7380 |
. 2
β’ (((πΎ β HL β§ π β π») β§ π β dom πΌ) β (πΌβ((( β₯ β(β‘πΌββ© {π§ β ran πΌ β£ (πΌβπ) β π§})) β¨ ( β₯ βπ)) β§ π)) = (πΌβ((( β₯ βπ) β¨ ( β₯ βπ)) β§ π))) |
28 | 16, 27 | eqtr2d 2778 |
1
β’ (((πΎ β HL β§ π β π») β§ π β dom πΌ) β (πΌβ((( β₯ βπ) β¨ ( β₯ βπ)) β§ π)) = (πβ(πΌβπ))) |