Theorem hgmapffval

Description: Map from the scalar division ring of the vector space to the scalar division ring of its closed kernel dual. (Contributed by NM, 25-Mar-2015)

	Ref	Expression
Hypothesis	hgmapval.h	$$⊢H=\mathrm{LHyp}\left(K\right)$$
Assertion	hgmapffval	$$⊢K\in X\to \mathrm{HGMap}\left(K\right)=\left(w\in H⟼\left\{a|\underset{\dot{}}{[}\mathrm{DVecH}\left(K\right)\left(w\right)/u\underset{\dot{}}{]}\underset{\dot{}}{[}{\mathrm{Base}}_{\mathrm{Scalar}\left(u\right)}/b\underset{\dot{}}{]}\underset{\dot{}}{[}\mathrm{HDMap}\left(K\right)\left(w\right)/m\underset{\dot{}}{]}a\in \left(x\in b⟼\left(\iota y\in b|\forall v\in {\mathrm{Base}}_{u}m\left(x{\cdot }_{u}v\right)=y{\cdot }_{\mathrm{LCDual}\left(K\right)\left(w\right)}m\left(v\right)\right)\right)\right\}\right)$$

Proof

Step	Hyp	Ref	Expression
1		hgmapval.h	$$⊢H=\mathrm{LHyp}\left(K\right)$$
2		elex	$$⊢K\in X\to K\in \mathrm{V}$$
3		fveq2	$$⊢k=K\to \mathrm{LHyp}\left(k\right)=\mathrm{LHyp}\left(K\right)$$
4	3 1	eqtr4di	$$⊢k=K\to \mathrm{LHyp}\left(k\right)=H$$
5		fveq2	$$⊢k=K\to \mathrm{DVecH}\left(k\right)=\mathrm{DVecH}\left(K\right)$$
6	5	fveq1d	$$⊢k=K\to \mathrm{DVecH}\left(k\right)\left(w\right)=\mathrm{DVecH}\left(K\right)\left(w\right)$$
7		fveq2	$$⊢k=K\to \mathrm{HDMap}\left(k\right)=\mathrm{HDMap}\left(K\right)$$
8	7	fveq1d	$$⊢k=K\to \mathrm{HDMap}\left(k\right)\left(w\right)=\mathrm{HDMap}\left(K\right)\left(w\right)$$
9		fveq2	$$⊢k=K\to \mathrm{LCDual}\left(k\right)=\mathrm{LCDual}\left(K\right)$$
10	9	fveq1d	$$⊢k=K\to \mathrm{LCDual}\left(k\right)\left(w\right)=\mathrm{LCDual}\left(K\right)\left(w\right)$$
11	10	fveq2d	$$⊢k=K\to {\cdot }_{\mathrm{LCDual}\left(k\right)\left(w\right)}={\cdot }_{\mathrm{LCDual}\left(K\right)\left(w\right)}$$
12	11	oveqd	$$⊢k=K\to y{\cdot }_{\mathrm{LCDual}\left(k\right)\left(w\right)}m\left(v\right)=y{\cdot }_{\mathrm{LCDual}\left(K\right)\left(w\right)}m\left(v\right)$$
13	12	eqeq2d	$$⊢k=K\to \left(m\left(x{\cdot }_{u}v\right)=y{\cdot }_{\mathrm{LCDual}\left(k\right)\left(w\right)}m\left(v\right)\leftrightarrow m\left(x{\cdot }_{u}v\right)=y{\cdot }_{\mathrm{LCDual}\left(K\right)\left(w\right)}m\left(v\right)\right)$$
14	13	ralbidv	$$⊢k=K\to \left(\forall v\in {\mathrm{Base}}_{u}m\left(x{\cdot }_{u}v\right)=y{\cdot }_{\mathrm{LCDual}\left(k\right)\left(w\right)}m\left(v\right)\leftrightarrow \forall v\in {\mathrm{Base}}_{u}m\left(x{\cdot }_{u}v\right)=y{\cdot }_{\mathrm{LCDual}\left(K\right)\left(w\right)}m\left(v\right)\right)$$
15	14	riotabidv	$$⊢k=K\to \left(\iota y\in b|\forall v\in {\mathrm{Base}}_{u}m\left(x{\cdot }_{u}v\right)=y{\cdot }_{\mathrm{LCDual}\left(k\right)\left(w\right)}m\left(v\right)\right)=\left(\iota y\in b|\forall v\in {\mathrm{Base}}_{u}m\left(x{\cdot }_{u}v\right)=y{\cdot }_{\mathrm{LCDual}\left(K\right)\left(w\right)}m\left(v\right)\right)$$
16	15	mpteq2dv	$$⊢k=K\to \left(x\in b⟼\left(\iota y\in b|\forall v\in {\mathrm{Base}}_{u}m\left(x{\cdot }_{u}v\right)=y{\cdot }_{\mathrm{LCDual}\left(k\right)\left(w\right)}m\left(v\right)\right)\right)=\left(x\in b⟼\left(\iota y\in b|\forall v\in {\mathrm{Base}}_{u}m\left(x{\cdot }_{u}v\right)=y{\cdot }_{\mathrm{LCDual}\left(K\right)\left(w\right)}m\left(v\right)\right)\right)$$
17	16	eleq2d	$$⊢k=K\to \left(a\in \left(x\in b⟼\left(\iota y\in b|\forall v\in {\mathrm{Base}}_{u}m\left(x{\cdot }_{u}v\right)=y{\cdot }_{\mathrm{LCDual}\left(k\right)\left(w\right)}m\left(v\right)\right)\right)\leftrightarrow a\in \left(x\in b⟼\left(\iota y\in b|\forall v\in {\mathrm{Base}}_{u}m\left(x{\cdot }_{u}v\right)=y{\cdot }_{\mathrm{LCDual}\left(K\right)\left(w\right)}m\left(v\right)\right)\right)\right)$$
18	8 17	sbceqbid	$$⊢k=K\to \left(\underset{\dot{}}{[}\mathrm{HDMap}\left(k\right)\left(w\right)/m\underset{\dot{}}{]}a\in \left(x\in b⟼\left(\iota y\in b|\forall v\in {\mathrm{Base}}_{u}m\left(x{\cdot }_{u}v\right)=y{\cdot }_{\mathrm{LCDual}\left(k\right)\left(w\right)}m\left(v\right)\right)\right)\leftrightarrow \underset{\dot{}}{[}\mathrm{HDMap}\left(K\right)\left(w\right)/m\underset{\dot{}}{]}a\in \left(x\in b⟼\left(\iota y\in b|\forall v\in {\mathrm{Base}}_{u}m\left(x{\cdot }_{u}v\right)=y{\cdot }_{\mathrm{LCDual}\left(K\right)\left(w\right)}m\left(v\right)\right)\right)\right)$$
19	18	sbcbidv	$$⊢k=K\to \left(\underset{\dot{}}{[}{\mathrm{Base}}_{\mathrm{Scalar}\left(u\right)}/b\underset{\dot{}}{]}\underset{\dot{}}{[}\mathrm{HDMap}\left(k\right)\left(w\right)/m\underset{\dot{}}{]}a\in \left(x\in b⟼\left(\iota y\in b|\forall v\in {\mathrm{Base}}_{u}m\left(x{\cdot }_{u}v\right)=y{\cdot }_{\mathrm{LCDual}\left(k\right)\left(w\right)}m\left(v\right)\right)\right)\leftrightarrow \underset{\dot{}}{[}{\mathrm{Base}}_{\mathrm{Scalar}\left(u\right)}/b\underset{\dot{}}{]}\underset{\dot{}}{[}\mathrm{HDMap}\left(K\right)\left(w\right)/m\underset{\dot{}}{]}a\in \left(x\in b⟼\left(\iota y\in b|\forall v\in {\mathrm{Base}}_{u}m\left(x{\cdot }_{u}v\right)=y{\cdot }_{\mathrm{LCDual}\left(K\right)\left(w\right)}m\left(v\right)\right)\right)\right)$$
20	6 19	sbceqbid	$$⊢k=K\to \left(\underset{\dot{}}{[}\mathrm{DVecH}\left(k\right)\left(w\right)/u\underset{\dot{}}{]}\underset{\dot{}}{[}{\mathrm{Base}}_{\mathrm{Scalar}\left(u\right)}/b\underset{\dot{}}{]}\underset{\dot{}}{[}\mathrm{HDMap}\left(k\right)\left(w\right)/m\underset{\dot{}}{]}a\in \left(x\in b⟼\left(\iota y\in b|\forall v\in {\mathrm{Base}}_{u}m\left(x{\cdot }_{u}v\right)=y{\cdot }_{\mathrm{LCDual}\left(k\right)\left(w\right)}m\left(v\right)\right)\right)\leftrightarrow \underset{\dot{}}{[}\mathrm{DVecH}\left(K\right)\left(w\right)/u\underset{\dot{}}{]}\underset{\dot{}}{[}{\mathrm{Base}}_{\mathrm{Scalar}\left(u\right)}/b\underset{\dot{}}{]}\underset{\dot{}}{[}\mathrm{HDMap}\left(K\right)\left(w\right)/m\underset{\dot{}}{]}a\in \left(x\in b⟼\left(\iota y\in b|\forall v\in {\mathrm{Base}}_{u}m\left(x{\cdot }_{u}v\right)=y{\cdot }_{\mathrm{LCDual}\left(K\right)\left(w\right)}m\left(v\right)\right)\right)\right)$$
21	20	abbidv	$$⊢k=K\to \left\{a|\underset{\dot{}}{[}\mathrm{DVecH}\left(k\right)\left(w\right)/u\underset{\dot{}}{]}\underset{\dot{}}{[}{\mathrm{Base}}_{\mathrm{Scalar}\left(u\right)}/b\underset{\dot{}}{]}\underset{\dot{}}{[}\mathrm{HDMap}\left(k\right)\left(w\right)/m\underset{\dot{}}{]}a\in \left(x\in b⟼\left(\iota y\in b|\forall v\in {\mathrm{Base}}_{u}m\left(x{\cdot }_{u}v\right)=y{\cdot }_{\mathrm{LCDual}\left(k\right)\left(w\right)}m\left(v\right)\right)\right)\right\}=\left\{a|\underset{\dot{}}{[}\mathrm{DVecH}\left(K\right)\left(w\right)/u\underset{\dot{}}{]}\underset{\dot{}}{[}{\mathrm{Base}}_{\mathrm{Scalar}\left(u\right)}/b\underset{\dot{}}{]}\underset{\dot{}}{[}\mathrm{HDMap}\left(K\right)\left(w\right)/m\underset{\dot{}}{]}a\in \left(x\in b⟼\left(\iota y\in b|\forall v\in {\mathrm{Base}}_{u}m\left(x{\cdot }_{u}v\right)=y{\cdot }_{\mathrm{LCDual}\left(K\right)\left(w\right)}m\left(v\right)\right)\right)\right\}$$
22	4 21	mpteq12dv	$$⊢k=K\to \left(w\in \mathrm{LHyp}\left(k\right)⟼\left\{a|\underset{\dot{}}{[}\mathrm{DVecH}\left(k\right)\left(w\right)/u\underset{\dot{}}{]}\underset{\dot{}}{[}{\mathrm{Base}}_{\mathrm{Scalar}\left(u\right)}/b\underset{\dot{}}{]}\underset{\dot{}}{[}\mathrm{HDMap}\left(k\right)\left(w\right)/m\underset{\dot{}}{]}a\in \left(x\in b⟼\left(\iota y\in b|\forall v\in {\mathrm{Base}}_{u}m\left(x{\cdot }_{u}v\right)=y{\cdot }_{\mathrm{LCDual}\left(k\right)\left(w\right)}m\left(v\right)\right)\right)\right\}\right)=\left(w\in H⟼\left\{a|\underset{\dot{}}{[}\mathrm{DVecH}\left(K\right)\left(w\right)/u\underset{\dot{}}{]}\underset{\dot{}}{[}{\mathrm{Base}}_{\mathrm{Scalar}\left(u\right)}/b\underset{\dot{}}{]}\underset{\dot{}}{[}\mathrm{HDMap}\left(K\right)\left(w\right)/m\underset{\dot{}}{]}a\in \left(x\in b⟼\left(\iota y\in b|\forall v\in {\mathrm{Base}}_{u}m\left(x{\cdot }_{u}v\right)=y{\cdot }_{\mathrm{LCDual}\left(K\right)\left(w\right)}m\left(v\right)\right)\right)\right\}\right)$$
23		df-hgmap	$$⊢\mathrm{HGMap}=\left(k\in \mathrm{V}⟼\left(w\in \mathrm{LHyp}\left(k\right)⟼\left\{a|\underset{\dot{}}{[}\mathrm{DVecH}\left(k\right)\left(w\right)/u\underset{\dot{}}{]}\underset{\dot{}}{[}{\mathrm{Base}}_{\mathrm{Scalar}\left(u\right)}/b\underset{\dot{}}{]}\underset{\dot{}}{[}\mathrm{HDMap}\left(k\right)\left(w\right)/m\underset{\dot{}}{]}a\in \left(x\in b⟼\left(\iota y\in b|\forall v\in {\mathrm{Base}}_{u}m\left(x{\cdot }_{u}v\right)=y{\cdot }_{\mathrm{LCDual}\left(k\right)\left(w\right)}m\left(v\right)\right)\right)\right\}\right)\right)$$
24	22 23 1	mptfvmpt	$$⊢K\in \mathrm{V}\to \mathrm{HGMap}\left(K\right)=\left(w\in H⟼\left\{a|\underset{\dot{}}{[}\mathrm{DVecH}\left(K\right)\left(w\right)/u\underset{\dot{}}{]}\underset{\dot{}}{[}{\mathrm{Base}}_{\mathrm{Scalar}\left(u\right)}/b\underset{\dot{}}{]}\underset{\dot{}}{[}\mathrm{HDMap}\left(K\right)\left(w\right)/m\underset{\dot{}}{]}a\in \left(x\in b⟼\left(\iota y\in b|\forall v\in {\mathrm{Base}}_{u}m\left(x{\cdot }_{u}v\right)=y{\cdot }_{\mathrm{LCDual}\left(K\right)\left(w\right)}m\left(v\right)\right)\right)\right\}\right)$$
25	2 24	syl	$$⊢K\in X\to \mathrm{HGMap}\left(K\right)=\left(w\in H⟼\left\{a|\underset{\dot{}}{[}\mathrm{DVecH}\left(K\right)\left(w\right)/u\underset{\dot{}}{]}\underset{\dot{}}{[}{\mathrm{Base}}_{\mathrm{Scalar}\left(u\right)}/b\underset{\dot{}}{]}\underset{\dot{}}{[}\mathrm{HDMap}\left(K\right)\left(w\right)/m\underset{\dot{}}{]}a\in \left(x\in b⟼\left(\iota y\in b|\forall v\in {\mathrm{Base}}_{u}m\left(x{\cdot }_{u}v\right)=y{\cdot }_{\mathrm{LCDual}\left(K\right)\left(w\right)}m\left(v\right)\right)\right)\right\}\right)$$