Step | Hyp | Ref
| Expression |
1 | | hgmapval.h |
. . . 4
β’ π» = (LHypβπΎ) |
2 | | hgmapfval.u |
. . . 4
β’ π = ((DVecHβπΎ)βπ) |
3 | | hgmapfval.v |
. . . 4
β’ π = (Baseβπ) |
4 | | hgmapfval.t |
. . . 4
β’ Β· = (
Β·π βπ) |
5 | | hgmapfval.r |
. . . 4
β’ π
= (Scalarβπ) |
6 | | hgmapfval.b |
. . . 4
β’ π΅ = (Baseβπ
) |
7 | | hgmapfval.c |
. . . 4
β’ πΆ = ((LCDualβπΎ)βπ) |
8 | | hgmapfval.s |
. . . 4
β’ β = (
Β·π βπΆ) |
9 | | hgmapfval.m |
. . . 4
β’ π = ((HDMapβπΎ)βπ) |
10 | | hgmapfval.i |
. . . 4
β’ πΌ = ((HGMapβπΎ)βπ) |
11 | | hgmapfval.k |
. . . 4
β’ (π β (πΎ β π β§ π β π»)) |
12 | 1, 2, 3, 4, 5, 6, 7, 8, 9, 10,
11 | hgmapfval 40352 |
. . 3
β’ (π β πΌ = (π₯ β π΅ β¦ (β©π¦ β π΅ βπ£ β π (πβ(π₯ Β· π£)) = (π¦ β (πβπ£))))) |
13 | 12 | fveq1d 6845 |
. 2
β’ (π β (πΌβπ) = ((π₯ β π΅ β¦ (β©π¦ β π΅ βπ£ β π (πβ(π₯ Β· π£)) = (π¦ β (πβπ£))))βπ)) |
14 | | hgmapval.x |
. . 3
β’ (π β π β π΅) |
15 | | riotaex 7318 |
. . 3
β’
(β©π¦
β π΅ βπ£ β π (πβ(π Β· π£)) = (π¦ β (πβπ£))) β V |
16 | | fvoveq1 7381 |
. . . . . . 7
β’ (π₯ = π β (πβ(π₯ Β· π£)) = (πβ(π Β· π£))) |
17 | 16 | eqeq1d 2739 |
. . . . . 6
β’ (π₯ = π β ((πβ(π₯ Β· π£)) = (π¦ β (πβπ£)) β (πβ(π Β· π£)) = (π¦ β (πβπ£)))) |
18 | 17 | ralbidv 3175 |
. . . . 5
β’ (π₯ = π β (βπ£ β π (πβ(π₯ Β· π£)) = (π¦ β (πβπ£)) β βπ£ β π (πβ(π Β· π£)) = (π¦ β (πβπ£)))) |
19 | 18 | riotabidv 7316 |
. . . 4
β’ (π₯ = π β (β©π¦ β π΅ βπ£ β π (πβ(π₯ Β· π£)) = (π¦ β (πβπ£))) = (β©π¦ β π΅ βπ£ β π (πβ(π Β· π£)) = (π¦ β (πβπ£)))) |
20 | | eqid 2737 |
. . . 4
β’ (π₯ β π΅ β¦ (β©π¦ β π΅ βπ£ β π (πβ(π₯ Β· π£)) = (π¦ β (πβπ£)))) = (π₯ β π΅ β¦ (β©π¦ β π΅ βπ£ β π (πβ(π₯ Β· π£)) = (π¦ β (πβπ£)))) |
21 | 19, 20 | fvmptg 6947 |
. . 3
β’ ((π β π΅ β§ (β©π¦ β π΅ βπ£ β π (πβ(π Β· π£)) = (π¦ β (πβπ£))) β V) β ((π₯ β π΅ β¦ (β©π¦ β π΅ βπ£ β π (πβ(π₯ Β· π£)) = (π¦ β (πβπ£))))βπ) = (β©π¦ β π΅ βπ£ β π (πβ(π Β· π£)) = (π¦ β (πβπ£)))) |
22 | 14, 15, 21 | sylancl 587 |
. 2
β’ (π β ((π₯ β π΅ β¦ (β©π¦ β π΅ βπ£ β π (πβ(π₯ Β· π£)) = (π¦ β (πβπ£))))βπ) = (β©π¦ β π΅ βπ£ β π (πβ(π Β· π£)) = (π¦ β (πβπ£)))) |
23 | 13, 22 | eqtrd 2777 |
1
β’ (π β (πΌβπ) = (β©π¦ β π΅ βπ£ β π (πβ(π Β· π£)) = (π¦ β (πβπ£)))) |