Step | Hyp | Ref
| Expression |
1 | | eqid 2727 |
. . . 4
β’
(BaseβπΎ) =
(BaseβπΎ) |
2 | | dihatexv2.a |
. . . 4
β’ π΄ = (AtomsβπΎ) |
3 | 1, 2 | atbase 38765 |
. . 3
β’ (π β π΄ β π β (BaseβπΎ)) |
4 | 3 | anim2i 615 |
. 2
β’ ((π β§ π β π΄) β (π β§ π β (BaseβπΎ))) |
5 | | dihatexv2.k |
. . . . . . 7
β’ (π β (πΎ β HL β§ π β π»)) |
6 | 5 | adantr 479 |
. . . . . 6
β’ ((π β§ π₯ β (π β { 0 })) β (πΎ β HL β§ π β π»)) |
7 | | eldifi 4125 |
. . . . . . 7
β’ (π₯ β (π β { 0 }) β π₯ β π) |
8 | | dihatexv2.h |
. . . . . . . 8
β’ π» = (LHypβπΎ) |
9 | | dihatexv2.u |
. . . . . . . 8
β’ π = ((DVecHβπΎ)βπ) |
10 | | dihatexv2.v |
. . . . . . . 8
β’ π = (Baseβπ) |
11 | | dihatexv2.n |
. . . . . . . 8
β’ π = (LSpanβπ) |
12 | | dihatexv2.i |
. . . . . . . 8
β’ πΌ = ((DIsoHβπΎ)βπ) |
13 | 8, 9, 10, 11, 12 | dihlsprn 40808 |
. . . . . . 7
β’ (((πΎ β HL β§ π β π») β§ π₯ β π) β (πβ{π₯}) β ran πΌ) |
14 | 5, 7, 13 | syl2an 594 |
. . . . . 6
β’ ((π β§ π₯ β (π β { 0 })) β (πβ{π₯}) β ran πΌ) |
15 | 1, 8, 12 | dihcnvcl 40748 |
. . . . . 6
β’ (((πΎ β HL β§ π β π») β§ (πβ{π₯}) β ran πΌ) β (β‘πΌβ(πβ{π₯})) β (BaseβπΎ)) |
16 | 6, 14, 15 | syl2anc 582 |
. . . . 5
β’ ((π β§ π₯ β (π β { 0 })) β (β‘πΌβ(πβ{π₯})) β (BaseβπΎ)) |
17 | | eleq1a 2823 |
. . . . 5
β’ ((β‘πΌβ(πβ{π₯})) β (BaseβπΎ) β (π = (β‘πΌβ(πβ{π₯})) β π β (BaseβπΎ))) |
18 | 16, 17 | syl 17 |
. . . 4
β’ ((π β§ π₯ β (π β { 0 })) β (π = (β‘πΌβ(πβ{π₯})) β π β (BaseβπΎ))) |
19 | 18 | rexlimdva 3151 |
. . 3
β’ (π β (βπ₯ β (π β { 0 })π = (β‘πΌβ(πβ{π₯})) β π β (BaseβπΎ))) |
20 | 19 | imdistani 567 |
. 2
β’ ((π β§ βπ₯ β (π β { 0 })π = (β‘πΌβ(πβ{π₯}))) β (π β§ π β (BaseβπΎ))) |
21 | | dihatexv2.o |
. . . 4
β’ 0 =
(0gβπ) |
22 | 5 | adantr 479 |
. . . 4
β’ ((π β§ π β (BaseβπΎ)) β (πΎ β HL β§ π β π»)) |
23 | | simpr 483 |
. . . 4
β’ ((π β§ π β (BaseβπΎ)) β π β (BaseβπΎ)) |
24 | 1, 2, 8, 9, 10, 21, 11, 12, 22, 23 | dihatexv 40815 |
. . 3
β’ ((π β§ π β (BaseβπΎ)) β (π β π΄ β βπ₯ β (π β { 0 })(πΌβπ) = (πβ{π₯}))) |
25 | 22 | adantr 479 |
. . . . . . 7
β’ (((π β§ π β (BaseβπΎ)) β§ π₯ β (π β { 0 })) β (πΎ β HL β§ π β π»)) |
26 | 22, 7, 13 | syl2an 594 |
. . . . . . 7
β’ (((π β§ π β (BaseβπΎ)) β§ π₯ β (π β { 0 })) β (πβ{π₯}) β ran πΌ) |
27 | 8, 12 | dihcnvid2 40750 |
. . . . . . 7
β’ (((πΎ β HL β§ π β π») β§ (πβ{π₯}) β ran πΌ) β (πΌβ(β‘πΌβ(πβ{π₯}))) = (πβ{π₯})) |
28 | 25, 26, 27 | syl2anc 582 |
. . . . . 6
β’ (((π β§ π β (BaseβπΎ)) β§ π₯ β (π β { 0 })) β (πΌβ(β‘πΌβ(πβ{π₯}))) = (πβ{π₯})) |
29 | 28 | eqeq2d 2738 |
. . . . 5
β’ (((π β§ π β (BaseβπΎ)) β§ π₯ β (π β { 0 })) β ((πΌβπ) = (πΌβ(β‘πΌβ(πβ{π₯}))) β (πΌβπ) = (πβ{π₯}))) |
30 | | simplr 767 |
. . . . . 6
β’ (((π β§ π β (BaseβπΎ)) β§ π₯ β (π β { 0 })) β π β (BaseβπΎ)) |
31 | 25, 26, 15 | syl2anc 582 |
. . . . . 6
β’ (((π β§ π β (BaseβπΎ)) β§ π₯ β (π β { 0 })) β (β‘πΌβ(πβ{π₯})) β (BaseβπΎ)) |
32 | 1, 8, 12 | dih11 40742 |
. . . . . 6
β’ (((πΎ β HL β§ π β π») β§ π β (BaseβπΎ) β§ (β‘πΌβ(πβ{π₯})) β (BaseβπΎ)) β ((πΌβπ) = (πΌβ(β‘πΌβ(πβ{π₯}))) β π = (β‘πΌβ(πβ{π₯})))) |
33 | 25, 30, 31, 32 | syl3anc 1368 |
. . . . 5
β’ (((π β§ π β (BaseβπΎ)) β§ π₯ β (π β { 0 })) β ((πΌβπ) = (πΌβ(β‘πΌβ(πβ{π₯}))) β π = (β‘πΌβ(πβ{π₯})))) |
34 | 29, 33 | bitr3d 280 |
. . . 4
β’ (((π β§ π β (BaseβπΎ)) β§ π₯ β (π β { 0 })) β ((πΌβπ) = (πβ{π₯}) β π = (β‘πΌβ(πβ{π₯})))) |
35 | 34 | rexbidva 3172 |
. . 3
β’ ((π β§ π β (BaseβπΎ)) β (βπ₯ β (π β { 0 })(πΌβπ) = (πβ{π₯}) β βπ₯ β (π β { 0 })π = (β‘πΌβ(πβ{π₯})))) |
36 | 24, 35 | bitrd 278 |
. 2
β’ ((π β§ π β (BaseβπΎ)) β (π β π΄ β βπ₯ β (π β { 0 })π = (β‘πΌβ(πβ{π₯})))) |
37 | 4, 20, 36 | pm5.21nd 800 |
1
β’ (π β (π β π΄ β βπ₯ β (π β { 0 })π = (β‘πΌβ(πβ{π₯})))) |