Step | Hyp | Ref
| Expression |
1 | | dihw.k |
. . 3
β’ (π β (πΎ β HL β§ π β π»)) |
2 | 1 | simprd 497 |
. . . . 5
β’ (π β π β π») |
3 | | dihw.b |
. . . . . 6
β’ π΅ = (BaseβπΎ) |
4 | | dihw.h |
. . . . . 6
β’ π» = (LHypβπΎ) |
5 | 3, 4 | lhpbase 38511 |
. . . . 5
β’ (π β π» β π β π΅) |
6 | 2, 5 | syl 17 |
. . . 4
β’ (π β π β π΅) |
7 | 1 | simpld 496 |
. . . . . 6
β’ (π β πΎ β HL) |
8 | 7 | hllatd 37876 |
. . . . 5
β’ (π β πΎ β Lat) |
9 | | eqid 2733 |
. . . . . 6
β’
(leβπΎ) =
(leβπΎ) |
10 | 3, 9 | latref 18338 |
. . . . 5
β’ ((πΎ β Lat β§ π β π΅) β π(leβπΎ)π) |
11 | 8, 6, 10 | syl2anc 585 |
. . . 4
β’ (π β π(leβπΎ)π) |
12 | 6, 11 | jca 513 |
. . 3
β’ (π β (π β π΅ β§ π(leβπΎ)π)) |
13 | | dihw.i |
. . . 4
β’ πΌ = ((DIsoHβπΎ)βπ) |
14 | | eqid 2733 |
. . . 4
β’
((DIsoBβπΎ)βπ) = ((DIsoBβπΎ)βπ) |
15 | 3, 9, 4, 13, 14 | dihvalb 39750 |
. . 3
β’ (((πΎ β HL β§ π β π») β§ (π β π΅ β§ π(leβπΎ)π)) β (πΌβπ) = (((DIsoBβπΎ)βπ)βπ)) |
16 | 1, 12, 15 | syl2anc 585 |
. 2
β’ (π β (πΌβπ) = (((DIsoBβπΎ)βπ)βπ)) |
17 | | dihw.t |
. . . 4
β’ π = ((LTrnβπΎ)βπ) |
18 | | dihw.o |
. . . 4
β’ 0 = (π β π β¦ ( I βΎ π΅)) |
19 | | eqid 2733 |
. . . 4
β’
((DIsoAβπΎ)βπ) = ((DIsoAβπΎ)βπ) |
20 | 3, 9, 4, 17, 18, 19, 14 | dibval2 39657 |
. . 3
β’ (((πΎ β HL β§ π β π») β§ (π β π΅ β§ π(leβπΎ)π)) β (((DIsoBβπΎ)βπ)βπ) = ((((DIsoAβπΎ)βπ)βπ) Γ { 0 })) |
21 | 1, 12, 20 | syl2anc 585 |
. 2
β’ (π β (((DIsoBβπΎ)βπ)βπ) = ((((DIsoAβπΎ)βπ)βπ) Γ { 0 })) |
22 | | eqid 2733 |
. . . . . 6
β’
((trLβπΎ)βπ) = ((trLβπΎ)βπ) |
23 | 3, 9, 4, 17, 22, 19 | diaval 39545 |
. . . . 5
β’ (((πΎ β HL β§ π β π») β§ (π β π΅ β§ π(leβπΎ)π)) β (((DIsoAβπΎ)βπ)βπ) = {π β π β£ (((trLβπΎ)βπ)βπ)(leβπΎ)π}) |
24 | 1, 12, 23 | syl2anc 585 |
. . . 4
β’ (π β (((DIsoAβπΎ)βπ)βπ) = {π β π β£ (((trLβπΎ)βπ)βπ)(leβπΎ)π}) |
25 | 9, 4, 17, 22 | trlle 38697 |
. . . . . . 7
β’ (((πΎ β HL β§ π β π») β§ π β π) β (((trLβπΎ)βπ)βπ)(leβπΎ)π) |
26 | 1, 25 | sylan 581 |
. . . . . 6
β’ ((π β§ π β π) β (((trLβπΎ)βπ)βπ)(leβπΎ)π) |
27 | 26 | ralrimiva 3140 |
. . . . 5
β’ (π β βπ β π (((trLβπΎ)βπ)βπ)(leβπΎ)π) |
28 | | rabid2 3438 |
. . . . 5
β’ (π = {π β π β£ (((trLβπΎ)βπ)βπ)(leβπΎ)π} β βπ β π (((trLβπΎ)βπ)βπ)(leβπΎ)π) |
29 | 27, 28 | sylibr 233 |
. . . 4
β’ (π β π = {π β π β£ (((trLβπΎ)βπ)βπ)(leβπΎ)π}) |
30 | 24, 29 | eqtr4d 2776 |
. . 3
β’ (π β (((DIsoAβπΎ)βπ)βπ) = π) |
31 | 30 | xpeq1d 5666 |
. 2
β’ (π β ((((DIsoAβπΎ)βπ)βπ) Γ { 0 }) = (π Γ { 0 })) |
32 | 16, 21, 31 | 3eqtrd 2777 |
1
β’ (π β (πΌβπ) = (π Γ { 0 })) |