Step | Hyp | Ref
| Expression |
1 | | id 22 |
. . 3
β’ ((πΎ β HL β§ π β π») β (πΎ β HL β§ π β π»)) |
2 | | hlatl 37825 |
. . . . 5
β’ (πΎ β HL β πΎ β AtLat) |
3 | | dia0.b |
. . . . . 6
β’ π΅ = (BaseβπΎ) |
4 | | dia0.z |
. . . . . 6
β’ 0 =
(0.βπΎ) |
5 | 3, 4 | atl0cl 37768 |
. . . . 5
β’ (πΎ β AtLat β 0 β π΅) |
6 | 2, 5 | syl 17 |
. . . 4
β’ (πΎ β HL β 0 β π΅) |
7 | 6 | adantr 482 |
. . 3
β’ ((πΎ β HL β§ π β π») β 0 β π΅) |
8 | | dia0.h |
. . . . 5
β’ π» = (LHypβπΎ) |
9 | 3, 8 | lhpbase 38464 |
. . . 4
β’ (π β π» β π β π΅) |
10 | | eqid 2737 |
. . . . 5
β’
(leβπΎ) =
(leβπΎ) |
11 | 3, 10, 4 | atl0le 37769 |
. . . 4
β’ ((πΎ β AtLat β§ π β π΅) β 0 (leβπΎ)π) |
12 | 2, 9, 11 | syl2an 597 |
. . 3
β’ ((πΎ β HL β§ π β π») β 0 (leβπΎ)π) |
13 | | eqid 2737 |
. . . 4
β’
((LTrnβπΎ)βπ) = ((LTrnβπΎ)βπ) |
14 | | eqid 2737 |
. . . 4
β’
((trLβπΎ)βπ) = ((trLβπΎ)βπ) |
15 | | dia0.i |
. . . 4
β’ πΌ = ((DIsoAβπΎ)βπ) |
16 | 3, 10, 8, 13, 14, 15 | diaval 39498 |
. . 3
β’ (((πΎ β HL β§ π β π») β§ ( 0 β π΅ β§ 0 (leβπΎ)π)) β (πΌβ 0 ) = {π β ((LTrnβπΎ)βπ) β£ (((trLβπΎ)βπ)βπ)(leβπΎ) 0 }) |
17 | 1, 7, 12, 16 | syl12anc 836 |
. 2
β’ ((πΎ β HL β§ π β π») β (πΌβ 0 ) = {π β ((LTrnβπΎ)βπ) β£ (((trLβπΎ)βπ)βπ)(leβπΎ) 0 }) |
18 | 2 | ad2antrr 725 |
. . . . 5
β’ (((πΎ β HL β§ π β π») β§ π β ((LTrnβπΎ)βπ)) β πΎ β AtLat) |
19 | 3, 8, 13, 14 | trlcl 38630 |
. . . . 5
β’ (((πΎ β HL β§ π β π») β§ π β ((LTrnβπΎ)βπ)) β (((trLβπΎ)βπ)βπ) β π΅) |
20 | 3, 10, 4 | atlle0 37770 |
. . . . 5
β’ ((πΎ β AtLat β§
(((trLβπΎ)βπ)βπ) β π΅) β ((((trLβπΎ)βπ)βπ)(leβπΎ) 0 β (((trLβπΎ)βπ)βπ) = 0 )) |
21 | 18, 19, 20 | syl2anc 585 |
. . . 4
β’ (((πΎ β HL β§ π β π») β§ π β ((LTrnβπΎ)βπ)) β ((((trLβπΎ)βπ)βπ)(leβπΎ) 0 β (((trLβπΎ)βπ)βπ) = 0 )) |
22 | 3, 4, 8, 13, 14 | trlid0b 38644 |
. . . 4
β’ (((πΎ β HL β§ π β π») β§ π β ((LTrnβπΎ)βπ)) β (π = ( I βΎ π΅) β (((trLβπΎ)βπ)βπ) = 0 )) |
23 | 21, 22 | bitr4d 282 |
. . 3
β’ (((πΎ β HL β§ π β π») β§ π β ((LTrnβπΎ)βπ)) β ((((trLβπΎ)βπ)βπ)(leβπΎ) 0 β π = ( I βΎ π΅))) |
24 | 23 | rabbidva 3415 |
. 2
β’ ((πΎ β HL β§ π β π») β {π β ((LTrnβπΎ)βπ) β£ (((trLβπΎ)βπ)βπ)(leβπΎ) 0 } = {π β ((LTrnβπΎ)βπ) β£ π = ( I βΎ π΅)}) |
25 | 3, 8, 13 | idltrn 38616 |
. . 3
β’ ((πΎ β HL β§ π β π») β ( I βΎ π΅) β ((LTrnβπΎ)βπ)) |
26 | | rabsn 4683 |
. . 3
β’ (( I
βΎ π΅) β
((LTrnβπΎ)βπ) β {π β ((LTrnβπΎ)βπ) β£ π = ( I βΎ π΅)} = {( I βΎ π΅)}) |
27 | 25, 26 | syl 17 |
. 2
β’ ((πΎ β HL β§ π β π») β {π β ((LTrnβπΎ)βπ) β£ π = ( I βΎ π΅)} = {( I βΎ π΅)}) |
28 | 17, 24, 27 | 3eqtrd 2781 |
1
β’ ((πΎ β HL β§ π β π») β (πΌβ 0 ) = {( I βΎ π΅)}) |