Theorem hgmapval

Description: Value of map from the scalar division ring of the vector space to the scalar division ring of its closed kernel dual. Function sigma of scalar f in part 14 of Baer p. 50 line 4. TODO: variable names are inherited from older version. Maybe make more consistent with hdmap14lem15 . (Contributed by NM, 25-Mar-2015)

	Ref	Expression
Hypotheses	hgmapval.h	$$⊢H=\mathrm{LHyp}\left(K\right)$$
	hgmapfval.u	$$⊢U=\mathrm{DVecH}\left(K\right)\left(W\right)$$
	hgmapfval.v	$$⊢V={\mathrm{Base}}_U$$
	hgmapfval.t	$$⊢\underset{\dot{}}{·}={\cdot }_U$$
	hgmapfval.r	$$⊢R=\mathrm{Scalar}\left(U\right)$$
	hgmapfval.b	$$⊢B={\mathrm{Base}}_R$$
	hgmapfval.c	$$⊢C=\mathrm{LCDual}\left(K\right)\left(W\right)$$
	hgmapfval.s	$$⊢\underset{\dot{}}{\bullet }={\cdot }_C$$
	hgmapfval.m	$$⊢M=\mathrm{HDMap}\left(K\right)\left(W\right)$$
	hgmapfval.i	$$⊢I=\mathrm{HGMap}\left(K\right)\left(W\right)$$
	hgmapfval.k	$$⊢\phi \to \left(K\in Y\wedge W\in H\right)$$
	hgmapval.x	$$⊢\phi \to X\in B$$
Assertion	hgmapval	$$⊢\phi \to I\left(X\right)=\left(\iota y\in B|\forall v\in VM\left(X\underset{\dot{}}{·}v\right)=y\underset{\dot{}}{\bullet }M\left(v\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		hgmapval.h	$$⊢H=\mathrm{LHyp}\left(K\right)$$
2		hgmapfval.u	$$⊢U=\mathrm{DVecH}\left(K\right)\left(W\right)$$
3		hgmapfval.v	$$⊢V={\mathrm{Base}}_U$$
4		hgmapfval.t	$$⊢\underset{\dot{}}{·}={\cdot }_U$$
5		hgmapfval.r	$$⊢R=\mathrm{Scalar}\left(U\right)$$
6		hgmapfval.b	$$⊢B={\mathrm{Base}}_R$$
7		hgmapfval.c	$$⊢C=\mathrm{LCDual}\left(K\right)\left(W\right)$$
8		hgmapfval.s	$$⊢\underset{\dot{}}{\bullet }={\cdot }_C$$
9		hgmapfval.m	$$⊢M=\mathrm{HDMap}\left(K\right)\left(W\right)$$
10		hgmapfval.i	$$⊢I=\mathrm{HGMap}\left(K\right)\left(W\right)$$
11		hgmapfval.k	$$⊢\phi \to \left(K\in Y\wedge W\in H\right)$$
12		hgmapval.x	$$⊢\phi \to X\in B$$
13	1 2 3 4 5 6 7 8 9 10 11	hgmapfval	$$⊢\phi \to I=\left(x\in B⟼\left(\iota y\in B|\forall v\in VM\left(x\underset{\dot{}}{·}v\right)=y\underset{\dot{}}{\bullet }M\left(v\right)\right)\right)$$
14	13	fveq1d	$$⊢\phi \to I\left(X\right)=\left(x\in B⟼\left(\iota y\in B|\forall v\in VM\left(x\underset{\dot{}}{·}v\right)=y\underset{\dot{}}{\bullet }M\left(v\right)\right)\right)\left(X\right)$$
15		riotaex	$$⊢\left(\iota y\in B|\forall v\in VM\left(X\underset{\dot{}}{·}v\right)=y\underset{\dot{}}{\bullet }M\left(v\right)\right)\in \mathrm{V}$$
16		fvoveq1	$$⊢x=X\to M\left(x\underset{\dot{}}{·}v\right)=M\left(X\underset{\dot{}}{·}v\right)$$
17	16	eqeq1d	$$⊢x=X\to \left(M\left(x\underset{\dot{}}{·}v\right)=y\underset{\dot{}}{\bullet }M\left(v\right)\leftrightarrow M\left(X\underset{\dot{}}{·}v\right)=y\underset{\dot{}}{\bullet }M\left(v\right)\right)$$
18	17	ralbidv	$$⊢x=X\to \left(\forall v\in VM\left(x\underset{\dot{}}{·}v\right)=y\underset{\dot{}}{\bullet }M\left(v\right)\leftrightarrow \forall v\in VM\left(X\underset{\dot{}}{·}v\right)=y\underset{\dot{}}{\bullet }M\left(v\right)\right)$$
19	18	riotabidv	$$⊢x=X\to \left(\iota y\in B|\forall v\in VM\left(x\underset{\dot{}}{·}v\right)=y\underset{\dot{}}{\bullet }M\left(v\right)\right)=\left(\iota y\in B|\forall v\in VM\left(X\underset{\dot{}}{·}v\right)=y\underset{\dot{}}{\bullet }M\left(v\right)\right)$$
20		eqid	$$⊢\left(x\in B⟼\left(\iota y\in B|\forall v\in VM\left(x\underset{\dot{}}{·}v\right)=y\underset{\dot{}}{\bullet }M\left(v\right)\right)\right)=\left(x\in B⟼\left(\iota y\in B|\forall v\in VM\left(x\underset{\dot{}}{·}v\right)=y\underset{\dot{}}{\bullet }M\left(v\right)\right)\right)$$
21	19 20	fvmptg	$$⊢\left(X\in B\wedge \left(\iota y\in B|\forall v\in VM\left(X\underset{\dot{}}{·}v\right)=y\underset{\dot{}}{\bullet }M\left(v\right)\right)\in \mathrm{V}\right)\to \left(x\in B⟼\left(\iota y\in B|\forall v\in VM\left(x\underset{\dot{}}{·}v\right)=y\underset{\dot{}}{\bullet }M\left(v\right)\right)\right)\left(X\right)=\left(\iota y\in B|\forall v\in VM\left(X\underset{\dot{}}{·}v\right)=y\underset{\dot{}}{\bullet }M\left(v\right)\right)$$
22	12 15 21	sylancl	$$⊢\phi \to \left(x\in B⟼\left(\iota y\in B|\forall v\in VM\left(x\underset{\dot{}}{·}v\right)=y\underset{\dot{}}{\bullet }M\left(v\right)\right)\right)\left(X\right)=\left(\iota y\in B|\forall v\in VM\left(X\underset{\dot{}}{·}v\right)=y\underset{\dot{}}{\bullet }M\left(v\right)\right)$$
23	14 22	eqtrd	$$⊢\phi \to I\left(X\right)=\left(\iota y\in B|\forall v\in VM\left(X\underset{\dot{}}{·}v\right)=y\underset{\dot{}}{\bullet }M\left(v\right)\right)$$