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 = ( LHyp ` K )
	hgmapfval.u	|- U = ( ( DVecH ` K ) ` W )
	hgmapfval.v	|- V = ( Base ` U )
	hgmapfval.t	|- .x. = ( .s ` U )
	hgmapfval.r	|- R = ( Scalar ` U )
	hgmapfval.b	|- B = ( Base ` R )
	hgmapfval.c	|- C = ( ( LCDual ` K ) ` W )
	hgmapfval.s	|- .xb = ( .s ` C )
	hgmapfval.m	|- M = ( ( HDMap ` K ) ` W )
	hgmapfval.i	|- I = ( ( HGMap ` K ) ` W )
	hgmapfval.k	|- ( ph -> ( K e. Y /\ W e. H ) )
	hgmapval.x	|- ( ph -> X e. B )
Assertion	hgmapval	|- ( ph -> ( I ` X ) = ( iota_ y e. B A. v e. V ( M ` ( X .x. v ) ) = ( y .xb ( M ` v ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		hgmapval.h	|- H = ( LHyp ` K )
2		hgmapfval.u	|- U = ( ( DVecH ` K ) ` W )
3		hgmapfval.v	|- V = ( Base ` U )
4		hgmapfval.t	|- .x. = ( .s ` U )
5		hgmapfval.r	|- R = ( Scalar ` U )
6		hgmapfval.b	|- B = ( Base ` R )
7		hgmapfval.c	|- C = ( ( LCDual ` K ) ` W )
8		hgmapfval.s	|- .xb = ( .s ` C )
9		hgmapfval.m	|- M = ( ( HDMap ` K ) ` W )
10		hgmapfval.i	|- I = ( ( HGMap ` K ) ` W )
11		hgmapfval.k	|- ( ph -> ( K e. Y /\ W e. H ) )
12		hgmapval.x	|- ( ph -> X e. B )
13	1 2 3 4 5 6 7 8 9 10 11	hgmapfval	|- ( ph -> I = ( x e. B |-> ( iota_ y e. B A. v e. V ( M ` ( x .x. v ) ) = ( y .xb ( M ` v ) ) ) ) )
14	13	fveq1d	|- ( ph -> ( I ` X ) = ( ( x e. B |-> ( iota_ y e. B A. v e. V ( M ` ( x .x. v ) ) = ( y .xb ( M ` v ) ) ) ) ` X ) )
15		riotaex	|- ( iota_ y e. B A. v e. V ( M ` ( X .x. v ) ) = ( y .xb ( M ` v ) ) ) e. _V
16		fvoveq1	|- ( x = X -> ( M ` ( x .x. v ) ) = ( M ` ( X .x. v ) ) )
17	16	eqeq1d	|- ( x = X -> ( ( M ` ( x .x. v ) ) = ( y .xb ( M ` v ) ) <-> ( M ` ( X .x. v ) ) = ( y .xb ( M ` v ) ) ) )
18	17	ralbidv	|- ( x = X -> ( A. v e. V ( M ` ( x .x. v ) ) = ( y .xb ( M ` v ) ) <-> A. v e. V ( M ` ( X .x. v ) ) = ( y .xb ( M ` v ) ) ) )
19	18	riotabidv	|- ( x = X -> ( iota_ y e. B A. v e. V ( M ` ( x .x. v ) ) = ( y .xb ( M ` v ) ) ) = ( iota_ y e. B A. v e. V ( M ` ( X .x. v ) ) = ( y .xb ( M ` v ) ) ) )
20		eqid	|- ( x e. B |-> ( iota_ y e. B A. v e. V ( M ` ( x .x. v ) ) = ( y .xb ( M ` v ) ) ) ) = ( x e. B |-> ( iota_ y e. B A. v e. V ( M ` ( x .x. v ) ) = ( y .xb ( M ` v ) ) ) )
21	19 20	fvmptg	|- ( ( X e. B /\ ( iota_ y e. B A. v e. V ( M ` ( X .x. v ) ) = ( y .xb ( M ` v ) ) ) e. _V ) -> ( ( x e. B |-> ( iota_ y e. B A. v e. V ( M ` ( x .x. v ) ) = ( y .xb ( M ` v ) ) ) ) ` X ) = ( iota_ y e. B A. v e. V ( M ` ( X .x. v ) ) = ( y .xb ( M ` v ) ) ) )
22	12 15 21	sylancl	|- ( ph -> ( ( x e. B |-> ( iota_ y e. B A. v e. V ( M ` ( x .x. v ) ) = ( y .xb ( M ` v ) ) ) ) ` X ) = ( iota_ y e. B A. v e. V ( M ` ( X .x. v ) ) = ( y .xb ( M ` v ) ) ) )
23	14 22	eqtrd	|- ( ph -> ( I ` X ) = ( iota_ y e. B A. v e. V ( M ` ( X .x. v ) ) = ( y .xb ( M ` v ) ) ) )