# Metamath Proof Explorer

## Theorem hgmapfnN

Description: Functionality of scalar sigma map. (Contributed by NM, 7-Jun-2015) (New usage is discouraged.)

Ref Expression
Hypotheses hgmapfn.h ${⊢}{H}=\mathrm{LHyp}\left({K}\right)$
hgmapfn.u ${⊢}{U}=\mathrm{DVecH}\left({K}\right)\left({W}\right)$
hgmapfn.r ${⊢}{R}=\mathrm{Scalar}\left({U}\right)$
hgmapfn.b ${⊢}{B}={\mathrm{Base}}_{{R}}$
hgmapfn.g ${⊢}{G}=\mathrm{HGMap}\left({K}\right)\left({W}\right)$
hgmapfn.k ${⊢}{\phi }\to \left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)$
Assertion hgmapfnN ${⊢}{\phi }\to {G}Fn{B}$

### Proof

Step Hyp Ref Expression
1 hgmapfn.h ${⊢}{H}=\mathrm{LHyp}\left({K}\right)$
2 hgmapfn.u ${⊢}{U}=\mathrm{DVecH}\left({K}\right)\left({W}\right)$
3 hgmapfn.r ${⊢}{R}=\mathrm{Scalar}\left({U}\right)$
4 hgmapfn.b ${⊢}{B}={\mathrm{Base}}_{{R}}$
5 hgmapfn.g ${⊢}{G}=\mathrm{HGMap}\left({K}\right)\left({W}\right)$
6 hgmapfn.k ${⊢}{\phi }\to \left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)$
7 riotaex ${⊢}\left(\iota {j}\in {B}|\forall {x}\in {\mathrm{Base}}_{{U}}\phantom{\rule{.4em}{0ex}}\mathrm{HDMap}\left({K}\right)\left({W}\right)\left({k}{\cdot }_{{U}}{x}\right)={j}{\cdot }_{\mathrm{LCDual}\left({K}\right)\left({W}\right)}\mathrm{HDMap}\left({K}\right)\left({W}\right)\left({x}\right)\right)\in \mathrm{V}$
8 eqid ${⊢}\left({k}\in {B}⟼\left(\iota {j}\in {B}|\forall {x}\in {\mathrm{Base}}_{{U}}\phantom{\rule{.4em}{0ex}}\mathrm{HDMap}\left({K}\right)\left({W}\right)\left({k}{\cdot }_{{U}}{x}\right)={j}{\cdot }_{\mathrm{LCDual}\left({K}\right)\left({W}\right)}\mathrm{HDMap}\left({K}\right)\left({W}\right)\left({x}\right)\right)\right)=\left({k}\in {B}⟼\left(\iota {j}\in {B}|\forall {x}\in {\mathrm{Base}}_{{U}}\phantom{\rule{.4em}{0ex}}\mathrm{HDMap}\left({K}\right)\left({W}\right)\left({k}{\cdot }_{{U}}{x}\right)={j}{\cdot }_{\mathrm{LCDual}\left({K}\right)\left({W}\right)}\mathrm{HDMap}\left({K}\right)\left({W}\right)\left({x}\right)\right)\right)$
9 7 8 fnmpti ${⊢}\left({k}\in {B}⟼\left(\iota {j}\in {B}|\forall {x}\in {\mathrm{Base}}_{{U}}\phantom{\rule{.4em}{0ex}}\mathrm{HDMap}\left({K}\right)\left({W}\right)\left({k}{\cdot }_{{U}}{x}\right)={j}{\cdot }_{\mathrm{LCDual}\left({K}\right)\left({W}\right)}\mathrm{HDMap}\left({K}\right)\left({W}\right)\left({x}\right)\right)\right)Fn{B}$
10 eqid ${⊢}{\mathrm{Base}}_{{U}}={\mathrm{Base}}_{{U}}$
11 eqid ${⊢}{\cdot }_{{U}}={\cdot }_{{U}}$
12 eqid ${⊢}\mathrm{LCDual}\left({K}\right)\left({W}\right)=\mathrm{LCDual}\left({K}\right)\left({W}\right)$
13 eqid ${⊢}{\cdot }_{\mathrm{LCDual}\left({K}\right)\left({W}\right)}={\cdot }_{\mathrm{LCDual}\left({K}\right)\left({W}\right)}$
14 eqid ${⊢}\mathrm{HDMap}\left({K}\right)\left({W}\right)=\mathrm{HDMap}\left({K}\right)\left({W}\right)$
15 1 2 10 11 3 4 12 13 14 5 6 hgmapfval ${⊢}{\phi }\to {G}=\left({k}\in {B}⟼\left(\iota {j}\in {B}|\forall {x}\in {\mathrm{Base}}_{{U}}\phantom{\rule{.4em}{0ex}}\mathrm{HDMap}\left({K}\right)\left({W}\right)\left({k}{\cdot }_{{U}}{x}\right)={j}{\cdot }_{\mathrm{LCDual}\left({K}\right)\left({W}\right)}\mathrm{HDMap}\left({K}\right)\left({W}\right)\left({x}\right)\right)\right)$
16 15 fneq1d ${⊢}{\phi }\to \left({G}Fn{B}↔\left({k}\in {B}⟼\left(\iota {j}\in {B}|\forall {x}\in {\mathrm{Base}}_{{U}}\phantom{\rule{.4em}{0ex}}\mathrm{HDMap}\left({K}\right)\left({W}\right)\left({k}{\cdot }_{{U}}{x}\right)={j}{\cdot }_{\mathrm{LCDual}\left({K}\right)\left({W}\right)}\mathrm{HDMap}\left({K}\right)\left({W}\right)\left({x}\right)\right)\right)Fn{B}\right)$
17 9 16 mpbiri ${⊢}{\phi }\to {G}Fn{B}$