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 GFnB$$

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\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\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\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\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)FnB$$
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\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(GFnB\leftrightarrow \left(k\in B⟼\left(\iota j\in B|\forall x\in {\mathrm{Base}}_U\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)FnB\right)$$
17	9 16	mpbiri	$$⊢\phi \to GFnB$$