Step | Hyp | Ref
| Expression |
1 | | simpl 484 |
. . 3
β’ (((πΎ β HL β§ π β π») β§ (π β ran πΌ β§ π β ran πΌ)) β (πΎ β HL β§ π β π»)) |
2 | | diam.h |
. . . . 5
β’ π» = (LHypβπΎ) |
3 | | diam.i |
. . . . 5
β’ πΌ = ((DIsoAβπΎ)βπ) |
4 | 2, 3 | diacnvclN 39517 |
. . . 4
β’ (((πΎ β HL β§ π β π») β§ π β ran πΌ) β (β‘πΌβπ) β dom πΌ) |
5 | 4 | adantrr 716 |
. . 3
β’ (((πΎ β HL β§ π β π») β§ (π β ran πΌ β§ π β ran πΌ)) β (β‘πΌβπ) β dom πΌ) |
6 | 2, 3 | diacnvclN 39517 |
. . . 4
β’ (((πΎ β HL β§ π β π») β§ π β ran πΌ) β (β‘πΌβπ) β dom πΌ) |
7 | 6 | adantrl 715 |
. . 3
β’ (((πΎ β HL β§ π β π») β§ (π β ran πΌ β§ π β ran πΌ)) β (β‘πΌβπ) β dom πΌ) |
8 | | diam.m |
. . . 4
β’ β§ =
(meetβπΎ) |
9 | 8, 2, 3 | diameetN 39522 |
. . 3
β’ (((πΎ β HL β§ π β π») β§ ((β‘πΌβπ) β dom πΌ β§ (β‘πΌβπ) β dom πΌ)) β (πΌβ((β‘πΌβπ) β§ (β‘πΌβπ))) = ((πΌβ(β‘πΌβπ)) β© (πΌβ(β‘πΌβπ)))) |
10 | 1, 5, 7, 9 | syl12anc 836 |
. 2
β’ (((πΎ β HL β§ π β π») β§ (π β ran πΌ β§ π β ran πΌ)) β (πΌβ((β‘πΌβπ) β§ (β‘πΌβπ))) = ((πΌβ(β‘πΌβπ)) β© (πΌβ(β‘πΌβπ)))) |
11 | 2, 3 | diaf11N 39515 |
. . . . 5
β’ ((πΎ β HL β§ π β π») β πΌ:dom πΌβ1-1-ontoβran
πΌ) |
12 | 11 | adantr 482 |
. . . 4
β’ (((πΎ β HL β§ π β π») β§ (π β ran πΌ β§ π β ran πΌ)) β πΌ:dom πΌβ1-1-ontoβran
πΌ) |
13 | | simprl 770 |
. . . 4
β’ (((πΎ β HL β§ π β π») β§ (π β ran πΌ β§ π β ran πΌ)) β π β ran πΌ) |
14 | | f1ocnvfv2 7224 |
. . . 4
β’ ((πΌ:dom πΌβ1-1-ontoβran
πΌ β§ π β ran πΌ) β (πΌβ(β‘πΌβπ)) = π) |
15 | 12, 13, 14 | syl2anc 585 |
. . 3
β’ (((πΎ β HL β§ π β π») β§ (π β ran πΌ β§ π β ran πΌ)) β (πΌβ(β‘πΌβπ)) = π) |
16 | | simprr 772 |
. . . 4
β’ (((πΎ β HL β§ π β π») β§ (π β ran πΌ β§ π β ran πΌ)) β π β ran πΌ) |
17 | | f1ocnvfv2 7224 |
. . . 4
β’ ((πΌ:dom πΌβ1-1-ontoβran
πΌ β§ π β ran πΌ) β (πΌβ(β‘πΌβπ)) = π) |
18 | 12, 16, 17 | syl2anc 585 |
. . 3
β’ (((πΎ β HL β§ π β π») β§ (π β ran πΌ β§ π β ran πΌ)) β (πΌβ(β‘πΌβπ)) = π) |
19 | 15, 18 | ineq12d 4174 |
. 2
β’ (((πΎ β HL β§ π β π») β§ (π β ran πΌ β§ π β ran πΌ)) β ((πΌβ(β‘πΌβπ)) β© (πΌβ(β‘πΌβπ))) = (π β© π)) |
20 | 10, 19 | eqtr2d 2778 |
1
β’ (((πΎ β HL β§ π β π») β§ (π β ran πΌ β§ π β ran πΌ)) β (π β© π) = (πΌβ((β‘πΌβπ) β§ (β‘πΌβπ)))) |