Theorem hdmapval

Description: Value of map from vectors to functionals in the closed kernel dual space. This is the function sigma on line 27 above part 9 in Baer p. 48. We select a convenient fixed reference vector E to be <. 0 , 1 >. (corresponding to vector u on p. 48 line 7) whose span is the lattice isomorphism map of the fiducial atom P = ( ( ocK )W ) (see dvheveccl ). ( JE ) is a fixed reference functional determined by this vector (corresponding to u' on line 8; mapdhvmap shows in Baer's notation (Fu)* = Gu'). Baer's independent vectors v and w on line 7 correspond to our z that the A. z e. V ranges over. The middle term ( I<. E , ( JE ) , z >. ) provides isolation to allow E and T to assume the same value without conflict. Closure is shown by hdmapcl . If a separate auxiliary vector is known, hdmapval2 provides a version without quantification. (Contributed by NM, 15-May-2015)

	Ref	Expression
Hypotheses	hdmapval.h	|- H = ( LHyp ` K )
	hdmapfval.e	|- E = <. ( _I |` ( Base ` K ) ) , ( _I |` ( ( LTrn ` K ) ` W ) ) >.
	hdmapfval.u	|- U = ( ( DVecH ` K ) ` W )
	hdmapfval.v	|- V = ( Base ` U )
	hdmapfval.n	|- N = ( LSpan ` U )
	hdmapfval.c	|- C = ( ( LCDual ` K ) ` W )
	hdmapfval.d	|- D = ( Base ` C )
	hdmapfval.j	|- J = ( ( HVMap ` K ) ` W )
	hdmapfval.i	|- I = ( ( HDMap1 ` K ) ` W )
	hdmapfval.s	|- S = ( ( HDMap ` K ) ` W )
	hdmapfval.k	|- ( ph -> ( K e. A /\ W e. H ) )
	hdmapval.t	|- ( ph -> T e. V )
Assertion	hdmapval	|- ( ph -> ( S ` T ) = ( iota_ y e. D A. z e. V ( -. z e. ( ( N ` { E } ) u. ( N ` { T } ) ) -> y = ( I ` <. z , ( I ` <. E , ( J ` E ) , z >. ) , T >. ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		hdmapval.h	|- H = ( LHyp ` K )
2		hdmapfval.e	|- E = <. ( _I |` ( Base ` K ) ) , ( _I |` ( ( LTrn ` K ) ` W ) ) >.
3		hdmapfval.u	|- U = ( ( DVecH ` K ) ` W )
4		hdmapfval.v	|- V = ( Base ` U )
5		hdmapfval.n	|- N = ( LSpan ` U )
6		hdmapfval.c	|- C = ( ( LCDual ` K ) ` W )
7		hdmapfval.d	|- D = ( Base ` C )
8		hdmapfval.j	|- J = ( ( HVMap ` K ) ` W )
9		hdmapfval.i	|- I = ( ( HDMap1 ` K ) ` W )
10		hdmapfval.s	|- S = ( ( HDMap ` K ) ` W )
11		hdmapfval.k	|- ( ph -> ( K e. A /\ W e. H ) )
12		hdmapval.t	|- ( ph -> T e. V )
13	1 2 3 4 5 6 7 8 9 10 11	hdmapfval	|- ( ph -> S = ( t e. V |-> ( iota_ y e. D A. z e. V ( -. z e. ( ( N ` { E } ) u. ( N ` { t } ) ) -> y = ( I ` <. z , ( I ` <. E , ( J ` E ) , z >. ) , t >. ) ) ) ) )
14	13	fveq1d	|- ( ph -> ( S ` T ) = ( ( t e. V |-> ( iota_ y e. D A. z e. V ( -. z e. ( ( N ` { E } ) u. ( N ` { t } ) ) -> y = ( I ` <. z , ( I ` <. E , ( J ` E ) , z >. ) , t >. ) ) ) ) ` T ) )
15		riotaex	|- ( iota_ y e. D A. z e. V ( -. z e. ( ( N ` { E } ) u. ( N ` { T } ) ) -> y = ( I ` <. z , ( I ` <. E , ( J ` E ) , z >. ) , T >. ) ) ) e. _V
16		sneq	|- ( t = T -> { t } = { T } )
17	16	fveq2d	|- ( t = T -> ( N ` { t } ) = ( N ` { T } ) )
18	17	uneq2d	|- ( t = T -> ( ( N ` { E } ) u. ( N ` { t } ) ) = ( ( N ` { E } ) u. ( N ` { T } ) ) )
19	18	eleq2d	|- ( t = T -> ( z e. ( ( N ` { E } ) u. ( N ` { t } ) ) <-> z e. ( ( N ` { E } ) u. ( N ` { T } ) ) ) )
20	19	notbid	|- ( t = T -> ( -. z e. ( ( N ` { E } ) u. ( N ` { t } ) ) <-> -. z e. ( ( N ` { E } ) u. ( N ` { T } ) ) ) )
21		oteq3	|- ( t = T -> <. z , ( I ` <. E , ( J ` E ) , z >. ) , t >. = <. z , ( I ` <. E , ( J ` E ) , z >. ) , T >. )
22	21	fveq2d	|- ( t = T -> ( I ` <. z , ( I ` <. E , ( J ` E ) , z >. ) , t >. ) = ( I ` <. z , ( I ` <. E , ( J ` E ) , z >. ) , T >. ) )
23	22	eqeq2d	|- ( t = T -> ( y = ( I ` <. z , ( I ` <. E , ( J ` E ) , z >. ) , t >. ) <-> y = ( I ` <. z , ( I ` <. E , ( J ` E ) , z >. ) , T >. ) ) )
24	20 23	imbi12d	|- ( t = T -> ( ( -. z e. ( ( N ` { E } ) u. ( N ` { t } ) ) -> y = ( I ` <. z , ( I ` <. E , ( J ` E ) , z >. ) , t >. ) ) <-> ( -. z e. ( ( N ` { E } ) u. ( N ` { T } ) ) -> y = ( I ` <. z , ( I ` <. E , ( J ` E ) , z >. ) , T >. ) ) ) )
25	24	ralbidv	|- ( t = T -> ( A. z e. V ( -. z e. ( ( N ` { E } ) u. ( N ` { t } ) ) -> y = ( I ` <. z , ( I ` <. E , ( J ` E ) , z >. ) , t >. ) ) <-> A. z e. V ( -. z e. ( ( N ` { E } ) u. ( N ` { T } ) ) -> y = ( I ` <. z , ( I ` <. E , ( J ` E ) , z >. ) , T >. ) ) ) )
26	25	riotabidv	|- ( t = T -> ( iota_ y e. D A. z e. V ( -. z e. ( ( N ` { E } ) u. ( N ` { t } ) ) -> y = ( I ` <. z , ( I ` <. E , ( J ` E ) , z >. ) , t >. ) ) ) = ( iota_ y e. D A. z e. V ( -. z e. ( ( N ` { E } ) u. ( N ` { T } ) ) -> y = ( I ` <. z , ( I ` <. E , ( J ` E ) , z >. ) , T >. ) ) ) )
27		eqid	|- ( t e. V |-> ( iota_ y e. D A. z e. V ( -. z e. ( ( N ` { E } ) u. ( N ` { t } ) ) -> y = ( I ` <. z , ( I ` <. E , ( J ` E ) , z >. ) , t >. ) ) ) ) = ( t e. V |-> ( iota_ y e. D A. z e. V ( -. z e. ( ( N ` { E } ) u. ( N ` { t } ) ) -> y = ( I ` <. z , ( I ` <. E , ( J ` E ) , z >. ) , t >. ) ) ) )
28	26 27	fvmptg	|- ( ( T e. V /\ ( iota_ y e. D A. z e. V ( -. z e. ( ( N ` { E } ) u. ( N ` { T } ) ) -> y = ( I ` <. z , ( I ` <. E , ( J ` E ) , z >. ) , T >. ) ) ) e. _V ) -> ( ( t e. V |-> ( iota_ y e. D A. z e. V ( -. z e. ( ( N ` { E } ) u. ( N ` { t } ) ) -> y = ( I ` <. z , ( I ` <. E , ( J ` E ) , z >. ) , t >. ) ) ) ) ` T ) = ( iota_ y e. D A. z e. V ( -. z e. ( ( N ` { E } ) u. ( N ` { T } ) ) -> y = ( I ` <. z , ( I ` <. E , ( J ` E ) , z >. ) , T >. ) ) ) )
29	12 15 28	sylancl	|- ( ph -> ( ( t e. V |-> ( iota_ y e. D A. z e. V ( -. z e. ( ( N ` { E } ) u. ( N ` { t } ) ) -> y = ( I ` <. z , ( I ` <. E , ( J ` E ) , z >. ) , t >. ) ) ) ) ` T ) = ( iota_ y e. D A. z e. V ( -. z e. ( ( N ` { E } ) u. ( N ` { T } ) ) -> y = ( I ` <. z , ( I ` <. E , ( J ` E ) , z >. ) , T >. ) ) ) )
30	14 29	eqtrd	|- ( ph -> ( S ` T ) = ( iota_ y e. D A. z e. V ( -. z e. ( ( N ` { E } ) u. ( N ` { T } ) ) -> y = ( I ` <. z , ( I ` <. E , ( J ` E ) , z >. ) , T >. ) ) ) )