Step | Hyp | Ref
| Expression |
1 | | riotaex 7318 |
. . 3
β’
(β©π
β π΅ βπ₯ β (Baseβπ)(((HDMapβπΎ)βπ)β(π( Β·π
βπ)π₯)) = (π( Β·π
β((LCDualβπΎ)βπ))(((HDMapβπΎ)βπ)βπ₯))) β V |
2 | | eqid 2737 |
. . 3
β’ (π β π΅ β¦ (β©π β π΅ βπ₯ β (Baseβπ)(((HDMapβπΎ)βπ)β(π( Β·π
βπ)π₯)) = (π( Β·π
β((LCDualβπΎ)βπ))(((HDMapβπΎ)βπ)βπ₯)))) = (π β π΅ β¦ (β©π β π΅ βπ₯ β (Baseβπ)(((HDMapβπΎ)βπ)β(π( Β·π
βπ)π₯)) = (π( Β·π
β((LCDualβπΎ)βπ))(((HDMapβπΎ)βπ)βπ₯)))) |
3 | 1, 2 | fnmpti 6645 |
. 2
β’ (π β π΅ β¦ (β©π β π΅ βπ₯ β (Baseβπ)(((HDMapβπΎ)βπ)β(π( Β·π
βπ)π₯)) = (π( Β·π
β((LCDualβπΎ)βπ))(((HDMapβπΎ)βπ)βπ₯)))) Fn π΅ |
4 | | hgmapfn.h |
. . . 4
β’ π» = (LHypβπΎ) |
5 | | hgmapfn.u |
. . . 4
β’ π = ((DVecHβπΎ)βπ) |
6 | | eqid 2737 |
. . . 4
β’
(Baseβπ) =
(Baseβπ) |
7 | | eqid 2737 |
. . . 4
β’ (
Β·π βπ) = ( Β·π
βπ) |
8 | | hgmapfn.r |
. . . 4
β’ π
= (Scalarβπ) |
9 | | hgmapfn.b |
. . . 4
β’ π΅ = (Baseβπ
) |
10 | | eqid 2737 |
. . . 4
β’
((LCDualβπΎ)βπ) = ((LCDualβπΎ)βπ) |
11 | | eqid 2737 |
. . . 4
β’ (
Β·π β((LCDualβπΎ)βπ)) = ( Β·π
β((LCDualβπΎ)βπ)) |
12 | | eqid 2737 |
. . . 4
β’
((HDMapβπΎ)βπ) = ((HDMapβπΎ)βπ) |
13 | | hgmapfn.g |
. . . 4
β’ πΊ = ((HGMapβπΎ)βπ) |
14 | | hgmapfn.k |
. . . 4
β’ (π β (πΎ β HL β§ π β π»)) |
15 | 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14 | hgmapfval 40352 |
. . 3
β’ (π β πΊ = (π β π΅ β¦ (β©π β π΅ βπ₯ β (Baseβπ)(((HDMapβπΎ)βπ)β(π( Β·π
βπ)π₯)) = (π( Β·π
β((LCDualβπΎ)βπ))(((HDMapβπΎ)βπ)βπ₯))))) |
16 | 15 | fneq1d 6596 |
. 2
β’ (π β (πΊ Fn π΅ β (π β π΅ β¦ (β©π β π΅ βπ₯ β (Baseβπ)(((HDMapβπΎ)βπ)β(π( Β·π
βπ)π₯)) = (π( Β·π
β((LCDualβπΎ)βπ))(((HDMapβπΎ)βπ)βπ₯)))) Fn π΅)) |
17 | 3, 16 | mpbiri 258 |
1
β’ (π β πΊ Fn π΅) |