Theorem hgmapdcl

Description: Closure of the vector space to dual space scalar map, in the scalar sigma map. (Contributed by NM, 6-Jun-2015)

	Ref	Expression
Hypotheses	hgmapdcl.h	$$⊢H=\mathrm{LHyp}\left(K\right)$$
	hgmapdcl.u	$$⊢U=\mathrm{DVecH}\left(K\right)\left(W\right)$$
	hgmapdcl.r	$$⊢R=\mathrm{Scalar}\left(U\right)$$
	hgmapdcl.b	$$⊢B={\mathrm{Base}}_R$$
	hgmapdcl.c	$$⊢C=\mathrm{LCDual}\left(K\right)\left(W\right)$$
	hgmapdcl.q	$$⊢Q=\mathrm{Scalar}\left(C\right)$$
	hgmapdcl.a	$$⊢A={\mathrm{Base}}_Q$$
	hgmapdcl.g	$$⊢G=\mathrm{HGMap}\left(K\right)\left(W\right)$$
	hgmapdcl.k	$$⊢\phi \to \left(K\in \mathrm{HL}\wedge W\in H\right)$$
	hgmapdcl.f	$$⊢\phi \to F\in B$$
Assertion	hgmapdcl	$$⊢\phi \to G\left(F\right)\in A$$

Proof

Step	Hyp	Ref	Expression
1		hgmapdcl.h	$$⊢H=\mathrm{LHyp}\left(K\right)$$
2		hgmapdcl.u	$$⊢U=\mathrm{DVecH}\left(K\right)\left(W\right)$$
3		hgmapdcl.r	$$⊢R=\mathrm{Scalar}\left(U\right)$$
4		hgmapdcl.b	$$⊢B={\mathrm{Base}}_R$$
5		hgmapdcl.c	$$⊢C=\mathrm{LCDual}\left(K\right)\left(W\right)$$
6		hgmapdcl.q	$$⊢Q=\mathrm{Scalar}\left(C\right)$$
7		hgmapdcl.a	$$⊢A={\mathrm{Base}}_Q$$
8		hgmapdcl.g	$$⊢G=\mathrm{HGMap}\left(K\right)\left(W\right)$$
9		hgmapdcl.k	$$⊢\phi \to \left(K\in \mathrm{HL}\wedge W\in H\right)$$
10		hgmapdcl.f	$$⊢\phi \to F\in B$$
11	1 2 3 4 8 9 10	hgmapcl	$$⊢\phi \to G\left(F\right)\in B$$
12	1 2 3 4 5 6 7 9	lcdsbase	$$⊢\phi \to A=B$$
13	11 12	eleqtrrd	$$⊢\phi \to G\left(F\right)\in A$$