Step | Hyp | Ref
| Expression |
1 | | id 22 |
. . 3
β’ ((πΎ β HL β§ π β π») β (πΎ β HL β§ π β π»)) |
2 | | hlatl 38218 |
. . . . 5
β’ (πΎ β HL β πΎ β AtLat) |
3 | | dia0.b |
. . . . . 6
β’ π΅ = (BaseβπΎ) |
4 | | dia0.z |
. . . . . 6
β’ 0 =
(0.βπΎ) |
5 | 3, 4 | atl0cl 38161 |
. . . . 5
β’ (πΎ β AtLat β 0 β π΅) |
6 | 2, 5 | syl 17 |
. . . 4
β’ (πΎ β HL β 0 β π΅) |
7 | 6 | adantr 481 |
. . 3
β’ ((πΎ β HL β§ π β π») β 0 β π΅) |
8 | | dia0.h |
. . . . 5
β’ π» = (LHypβπΎ) |
9 | 3, 8 | lhpbase 38857 |
. . . 4
β’ (π β π» β π β π΅) |
10 | | eqid 2732 |
. . . . 5
β’
(leβπΎ) =
(leβπΎ) |
11 | 3, 10, 4 | atl0le 38162 |
. . . 4
β’ ((πΎ β AtLat β§ π β π΅) β 0 (leβπΎ)π) |
12 | 2, 9, 11 | syl2an 596 |
. . 3
β’ ((πΎ β HL β§ π β π») β 0 (leβπΎ)π) |
13 | | eqid 2732 |
. . . 4
β’
((LTrnβπΎ)βπ) = ((LTrnβπΎ)βπ) |
14 | | eqid 2732 |
. . . 4
β’
((trLβπΎ)βπ) = ((trLβπΎ)βπ) |
15 | | dia0.i |
. . . 4
β’ πΌ = ((DIsoAβπΎ)βπ) |
16 | 3, 10, 8, 13, 14, 15 | diaval 39891 |
. . 3
β’ (((πΎ β HL β§ π β π») β§ ( 0 β π΅ β§ 0 (leβπΎ)π)) β (πΌβ 0 ) = {π β ((LTrnβπΎ)βπ) β£ (((trLβπΎ)βπ)βπ)(leβπΎ) 0 }) |
17 | 1, 7, 12, 16 | syl12anc 835 |
. 2
β’ ((πΎ β HL β§ π β π») β (πΌβ 0 ) = {π β ((LTrnβπΎ)βπ) β£ (((trLβπΎ)βπ)βπ)(leβπΎ) 0 }) |
18 | 2 | ad2antrr 724 |
. . . . 5
β’ (((πΎ β HL β§ π β π») β§ π β ((LTrnβπΎ)βπ)) β πΎ β AtLat) |
19 | 3, 8, 13, 14 | trlcl 39023 |
. . . . 5
β’ (((πΎ β HL β§ π β π») β§ π β ((LTrnβπΎ)βπ)) β (((trLβπΎ)βπ)βπ) β π΅) |
20 | 3, 10, 4 | atlle0 38163 |
. . . . 5
β’ ((πΎ β AtLat β§
(((trLβπΎ)βπ)βπ) β π΅) β ((((trLβπΎ)βπ)βπ)(leβπΎ) 0 β (((trLβπΎ)βπ)βπ) = 0 )) |
21 | 18, 19, 20 | syl2anc 584 |
. . . 4
β’ (((πΎ β HL β§ π β π») β§ π β ((LTrnβπΎ)βπ)) β ((((trLβπΎ)βπ)βπ)(leβπΎ) 0 β (((trLβπΎ)βπ)βπ) = 0 )) |
22 | 3, 4, 8, 13, 14 | trlid0b 39037 |
. . . 4
β’ (((πΎ β HL β§ π β π») β§ π β ((LTrnβπΎ)βπ)) β (π = ( I βΎ π΅) β (((trLβπΎ)βπ)βπ) = 0 )) |
23 | 21, 22 | bitr4d 281 |
. . 3
β’ (((πΎ β HL β§ π β π») β§ π β ((LTrnβπΎ)βπ)) β ((((trLβπΎ)βπ)βπ)(leβπΎ) 0 β π = ( I βΎ π΅))) |
24 | 23 | rabbidva 3439 |
. 2
β’ ((πΎ β HL β§ π β π») β {π β ((LTrnβπΎ)βπ) β£ (((trLβπΎ)βπ)βπ)(leβπΎ) 0 } = {π β ((LTrnβπΎ)βπ) β£ π = ( I βΎ π΅)}) |
25 | 3, 8, 13 | idltrn 39009 |
. . 3
β’ ((πΎ β HL β§ π β π») β ( I βΎ π΅) β ((LTrnβπΎ)βπ)) |
26 | | rabsn 4724 |
. . 3
β’ (( I
βΎ π΅) β
((LTrnβπΎ)βπ) β {π β ((LTrnβπΎ)βπ) β£ π = ( I βΎ π΅)} = {( I βΎ π΅)}) |
27 | 25, 26 | syl 17 |
. 2
β’ ((πΎ β HL β§ π β π») β {π β ((LTrnβπΎ)βπ) β£ π = ( I βΎ π΅)} = {( I βΎ π΅)}) |
28 | 17, 24, 27 | 3eqtrd 2776 |
1
β’ ((πΎ β HL β§ π β π») β (πΌβ 0 ) = {( I βΎ π΅)}) |