Step | Hyp | Ref
| Expression |
1 | | eqid 2737 |
. . . 4
β’
(glbβπΎ) =
(glbβπΎ) |
2 | | diam.m |
. . . 4
β’ β§ =
(meetβπΎ) |
3 | | simpll 766 |
. . . 4
β’ (((πΎ β HL β§ π β π») β§ (π β dom πΌ β§ π β dom πΌ)) β πΎ β HL) |
4 | | eqid 2737 |
. . . . . 6
β’
(BaseβπΎ) =
(BaseβπΎ) |
5 | | diam.h |
. . . . . 6
β’ π» = (LHypβπΎ) |
6 | | diam.i |
. . . . . 6
β’ πΌ = ((DIsoAβπΎ)βπ) |
7 | 4, 5, 6 | diadmclN 39503 |
. . . . 5
β’ (((πΎ β HL β§ π β π») β§ π β dom πΌ) β π β (BaseβπΎ)) |
8 | 7 | adantrr 716 |
. . . 4
β’ (((πΎ β HL β§ π β π») β§ (π β dom πΌ β§ π β dom πΌ)) β π β (BaseβπΎ)) |
9 | 4, 5, 6 | diadmclN 39503 |
. . . . 5
β’ (((πΎ β HL β§ π β π») β§ π β dom πΌ) β π β (BaseβπΎ)) |
10 | 9 | adantrl 715 |
. . . 4
β’ (((πΎ β HL β§ π β π») β§ (π β dom πΌ β§ π β dom πΌ)) β π β (BaseβπΎ)) |
11 | 1, 2, 3, 8, 10 | meetval 18281 |
. . 3
β’ (((πΎ β HL β§ π β π») β§ (π β dom πΌ β§ π β dom πΌ)) β (π β§ π) = ((glbβπΎ)β{π, π})) |
12 | 11 | fveq2d 6847 |
. 2
β’ (((πΎ β HL β§ π β π») β§ (π β dom πΌ β§ π β dom πΌ)) β (πΌβ(π β§ π)) = (πΌβ((glbβπΎ)β{π, π}))) |
13 | | simpl 484 |
. . 3
β’ (((πΎ β HL β§ π β π») β§ (π β dom πΌ β§ π β dom πΌ)) β (πΎ β HL β§ π β π»)) |
14 | | prssi 4782 |
. . . 4
β’ ((π β dom πΌ β§ π β dom πΌ) β {π, π} β dom πΌ) |
15 | 14 | adantl 483 |
. . 3
β’ (((πΎ β HL β§ π β π») β§ (π β dom πΌ β§ π β dom πΌ)) β {π, π} β dom πΌ) |
16 | | prnzg 4740 |
. . . 4
β’ (π β dom πΌ β {π, π} β β
) |
17 | 16 | ad2antrl 727 |
. . 3
β’ (((πΎ β HL β§ π β π») β§ (π β dom πΌ β§ π β dom πΌ)) β {π, π} β β
) |
18 | 1, 5, 6 | diaglbN 39521 |
. . 3
β’ (((πΎ β HL β§ π β π») β§ ({π, π} β dom πΌ β§ {π, π} β β
)) β (πΌβ((glbβπΎ)β{π, π})) = β©
π₯ β {π, π} (πΌβπ₯)) |
19 | 13, 15, 17, 18 | syl12anc 836 |
. 2
β’ (((πΎ β HL β§ π β π») β§ (π β dom πΌ β§ π β dom πΌ)) β (πΌβ((glbβπΎ)β{π, π})) = β©
π₯ β {π, π} (πΌβπ₯)) |
20 | | fveq2 6843 |
. . . 4
β’ (π₯ = π β (πΌβπ₯) = (πΌβπ)) |
21 | | fveq2 6843 |
. . . 4
β’ (π₯ = π β (πΌβπ₯) = (πΌβπ)) |
22 | 20, 21 | iinxprg 5050 |
. . 3
β’ ((π β dom πΌ β§ π β dom πΌ) β β©
π₯ β {π, π} (πΌβπ₯) = ((πΌβπ) β© (πΌβπ))) |
23 | 22 | adantl 483 |
. 2
β’ (((πΎ β HL β§ π β π») β§ (π β dom πΌ β§ π β dom πΌ)) β β© π₯ β {π, π} (πΌβπ₯) = ((πΌβπ) β© (πΌβπ))) |
24 | 12, 19, 23 | 3eqtrd 2781 |
1
β’ (((πΎ β HL β§ π β π») β§ (π β dom πΌ β§ π β dom πΌ)) β (πΌβ(π β§ π)) = ((πΌβπ) β© (πΌβπ))) |