P. 352 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 35101-35200   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	hdmap1eulem 35101*	Lemma for hdmap1eu 35103. TODO: combine with hdmap1eu 35103 or at least share some hypotheses. (Contributed by NM, 15-May-2015.)
|- H = ( LHyp ` K )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- V = ( Base ` U )   &    |- .- = ( -g ` U )   &    |- .0. = ( 0g ` U )   &    |- N = ( LSpan ` U )   &    |- C = ( (LCDual ` K ) ` W )   &    |- D = ( Base ` C )   &    |- R = ( -g ` C )   &    |- Q = ( 0g ` C )   &    |- J = ( LSpan ` C )   &    |- M = ( (mapd ` K ) ` W )   &    |- I = ( (HDMap1 ` K ) ` W )   &    |- ( ph -> ( K e. HL /\ W e. H ) )   &    |- ( ph -> ( M ` ( N ` { X } ) ) = ( J ` { F } ) )   &    |- ( ph -> X e. ( V \ { .0. } ) )   &    |- ( ph -> F e. D )   &    |- ( ph -> T e. V )   &    |- L = ( x e. _V |-> if ( ( 2nd ` x ) = .0. , Q , ( iota_ h e. D ( ( M ` ( N ` { ( 2nd ` x ) } ) ) = ( J ` { h } ) /\ ( M ` ( N ` { ( ( 1st ` ( 1st ` x ) ) .- ( 2nd ` x ) ) } ) ) = ( J ` { ( ( 2nd ` ( 1st ` x ) ) R h ) } ) ) ) ) )   =>    |- ( ph -> E! y e. D A. z e. V ( -. z e. ( ( N ` { X } ) u. ( N ` { T } ) ) -> y = ( I ` <. z , ( I ` <. X , F , z >. ) , T >. ) ) )
Theorem	hdmap1eulemOLDN 35102*	Lemma for hdmap1euOLDN 35104. TODO: combine with hdmap1euOLDN 35104 or at least share some hypotheses. (Contributed by NM, 15-May-2015.) (New usage is discouraged.)
|- H = ( LHyp ` K )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- V = ( Base ` U )   &    |- .- = ( -g ` U )   &    |- .0. = ( 0g ` U )   &    |- N = ( LSpan ` U )   &    |- C = ( (LCDual ` K ) ` W )   &    |- D = ( Base ` C )   &    |- R = ( -g ` C )   &    |- Q = ( 0g ` C )   &    |- J = ( LSpan ` C )   &    |- M = ( (mapd ` K ) ` W )   &    |- I = ( (HDMap1 ` K ) ` W )   &    |- ( ph -> ( K e. HL /\ W e. H ) )   &    |- ( ph -> ( M ` ( N ` { X } ) ) = ( J ` { F } ) )   &    |- ( ph -> X e. ( V \ { .0. } ) )   &    |- ( ph -> F e. D )   &    |- ( ph -> T e. V )   &    |- L = ( x e. _V |-> if ( ( 2nd ` x ) = .0. , Q , ( iota_ h e. D ( ( M ` ( N ` { ( 2nd ` x ) } ) ) = ( J ` { h } ) /\ ( M ` ( N ` { ( ( 1st ` ( 1st ` x ) ) .- ( 2nd ` x ) ) } ) ) = ( J ` { ( ( 2nd ` ( 1st ` x ) ) R h ) } ) ) ) ) )   =>    |- ( ph -> E! y e. D A. z e. V ( -. z e. ( N ` { X , T } ) -> y = ( I ` <. z , ( I ` <. X , F , z >. ) , T >. ) ) )
Theorem	hdmap1eu 35103*	Convert mapdh9a 35067 to use the HDMap1 notation. (Contributed by NM, 15-May-2015.)
|- H = ( LHyp ` K )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- V = ( Base ` U )   &    |- .0. = ( 0g ` U )   &    |- N = ( LSpan ` U )   &    |- C = ( (LCDual ` K ) ` W )   &    |- D = ( Base ` C )   &    |- L = ( LSpan ` C )   &    |- M = ( (mapd ` K ) ` W )   &    |- I = ( (HDMap1 ` K ) ` W )   &    |- ( ph -> ( K e. HL /\ W e. H ) )   &    |- ( ph -> ( M ` ( N ` { X } ) ) = ( L ` { F } ) )   &    |- ( ph -> X e. ( V \ { .0. } ) )   &    |- ( ph -> F e. D )   &    |- ( ph -> T e. V )   =>    |- ( ph -> E! y e. D A. z e. V ( -. z e. ( ( N ` { X } ) u. ( N ` { T } ) ) -> y = ( I ` <. z , ( I ` <. X , F , z >. ) , T >. ) ) )
Theorem	hdmap1euOLDN 35104*	Convert mapdh9aOLDN 35068 to use the HDMap1 notation. (Contributed by NM, 15-May-2015.) (New usage is discouraged.)
|- H = ( LHyp ` K )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- V = ( Base ` U )   &    |- .0. = ( 0g ` U )   &    |- N = ( LSpan ` U )   &    |- C = ( (LCDual ` K ) ` W )   &    |- D = ( Base ` C )   &    |- L = ( LSpan ` C )   &    |- M = ( (mapd ` K ) ` W )   &    |- I = ( (HDMap1 ` K ) ` W )   &    |- ( ph -> ( K e. HL /\ W e. H ) )   &    |- ( ph -> ( M ` ( N ` { X } ) ) = ( L ` { F } ) )   &    |- ( ph -> X e. ( V \ { .0. } ) )   &    |- ( ph -> F e. D )   &    |- ( ph -> T e. V )   =>    |- ( ph -> E! y e. D A. z e. V ( -. z e. ( N ` { X , T } ) -> y = ( I ` <. z , ( I ` <. X , F , z >. ) , T >. ) ) )
Theorem	hdmap1neglem1N 35105	Lemma for hdmapneg 35126. TODO: Not used; delete. (Contributed by NM, 23-May-2015.) (New usage is discouraged.)
|- H = ( LHyp ` K )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- V = ( Base ` U )   &    |- R = ( invg ` U )   &    |- .0. = ( 0g ` U )   &    |- N = ( LSpan ` U )   &    |- C = ( (LCDual ` K ) ` W )   &    |- D = ( Base ` C )   &    |- S = ( invg ` C )   &    |- L = ( LSpan ` C )   &    |- M = ( (mapd ` K ) ` W )   &    |- I = ( (HDMap1 ` K ) ` W )   &    |- ( ph -> ( K e. HL /\ W e. H ) )   &    |- ( ph -> F e. D )   &    |- ( ph -> ( M ` ( N ` { X } ) ) = ( L ` { F } ) )   &    |- ( ph -> ( N ` { X } ) =/= ( N ` { Y } ) )   &    |- ( ph -> X e. ( V \ { .0. } ) )   &    |- ( ph -> Y e. ( V \ { .0. } ) )   &    |- ( ph -> ( I ` <. X , F , Y >. ) = G )   =>    |- ( ph -> ( I ` <. ( R ` X ) , ( S ` F ) , ( R ` Y ) >. ) = ( S ` G ) )
Theorem	hdmapffval 35106*	Map from vectors to functionals in the closed kernel dual space. (Contributed by NM, 15-May-2015.)
|- H = ( LHyp ` K )   =>    |- ( K e. X -> (HDMap ` K ) = ( w e. H |-> { a | [. <. ( _I |` ( Base ` K ) ) , ( _I |` ( ( LTrn ` K ) ` w ) ) >. / e ]. [. ( ( DVecH ` K ) ` w ) / u ]. [. ( Base ` u ) / v ]. [. ( (HDMap1 ` K ) ` w ) / i ]. a e. ( t e. v |-> ( iota_ y e. ( Base ` ( (LCDual ` K ) ` w ) ) A. z e. v ( -. z e. ( ( ( LSpan ` u ) ` { e } ) u. ( ( LSpan ` u ) ` { t } ) ) -> y = ( i ` <. z , ( i ` <. e , ( ( (HVMap ` K ) ` w ) ` e ) , z >. ) , t >. ) ) ) ) } ) )
Theorem	hdmapfval 35107*	Map from vectors to functionals in the closed kernel dual space. (Contributed by NM, 15-May-2015.)
|- H = ( LHyp ` K )   &    |- E = <. ( _I |` ( Base ` K ) ) , ( _I |` ( ( LTrn ` K ) ` W ) ) >.   &    |- U = ( ( DVecH ` K ) ` W )   &    |- V = ( Base ` U )   &    |- N = ( LSpan ` U )   &    |- C = ( (LCDual ` K ) ` W )   &    |- D = ( Base ` C )   &    |- J = ( (HVMap ` K ) ` W )   &    |- I = ( (HDMap1 ` K ) ` W )   &    |- S = ( (HDMap ` K ) ` W )   &    |- ( ph -> ( K e. A /\ W e. H ) )   =>    |- ( 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 >. ) ) ) ) )
Theorem	hdmapval 35108*	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 = ( ( oc ` K ) ` W ) (see dvheveccl 34389). ( J ` E ) is a fixed reference functional determined by this vector (corresponding to u' on line 8; mapdhvmap 35046 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 , ( J ` E ) , z >. ) provides isolation to allow E and T to assume the same value without conflict. Closure is shown by hdmapcl 35110. If a separate auxiliary vector is known, hdmapval2 35112 provides a version without quantification. (Contributed by NM, 15-May-2015.)
|- H = ( LHyp ` K )   &    |- E = <. ( _I |` ( Base ` K ) ) , ( _I |` ( ( LTrn ` K ) ` W ) ) >.   &    |- U = ( ( DVecH ` K ) ` W )   &    |- V = ( Base ` U )   &    |- N = ( LSpan ` U )   &    |- C = ( (LCDual ` K ) ` W )   &    |- D = ( Base ` C )   &    |- J = ( (HVMap ` K ) ` W )   &    |- I = ( (HDMap1 ` K ) ` W )   &    |- S = ( (HDMap ` K ) ` W )   &    |- ( ph -> ( K e. A /\ W e. H ) )   &    |- ( ph -> T e. V )   =>    |- ( 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 >. ) ) ) )
Theorem	hdmapfnN 35109	Functionality of map from vectors to functionals with closed kernels. (Contributed by NM, 30-May-2015.) (New usage is discouraged.)
|- H = ( LHyp ` K )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- V = ( Base ` U )   &    |- S = ( (HDMap ` K ) ` W )   &    |- ( ph -> ( K e. HL /\ W e. H ) )   =>    |- ( ph -> S Fn V )
Theorem	hdmapcl 35110	Closure of map from vectors to functionals with closed kernels. (Contributed by NM, 15-May-2015.)
|- H = ( LHyp ` K )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- V = ( Base ` U )   &    |- C = ( (LCDual ` K ) ` W )   &    |- D = ( Base ` C )   &    |- S = ( (HDMap ` K ) ` W )   &    |- ( ph -> ( K e. HL /\ W e. H ) )   &    |- ( ph -> T e. V )   =>    |- ( ph -> ( S ` T ) e. D )
Theorem	hdmapval2lem 35111*	Lemma for hdmapval2 35112. (Contributed by NM, 15-May-2015.)
|- H = ( LHyp ` K )   &    |- E = <. ( _I |` ( Base ` K ) ) , ( _I |` ( ( LTrn ` K ) ` W ) ) >.   &    |- U = ( ( DVecH ` K ) ` W )   &    |- V = ( Base ` U )   &    |- N = ( LSpan ` U )   &    |- C = ( (LCDual ` K ) ` W )   &    |- D = ( Base ` C )   &    |- J = ( (HVMap ` K ) ` W )   &    |- I = ( (HDMap1 ` K ) ` W )   &    |- S = ( (HDMap ` K ) ` W )   &    |- ( ph -> ( K e. HL /\ W e. H ) )   &    |- ( ph -> T e. V )   &    |- ( ph -> F e. D )   =>    |- ( ph -> ( ( S ` T ) = F <-> A. z e. V ( -. z e. ( ( N ` { E } ) u. ( N ` { T } ) ) -> F = ( I ` <. z , ( I ` <. E , ( J ` E ) , z >. ) , T >. ) ) ) )
Theorem	hdmapval2 35112	Value of map from vectors to functionals with a specific auxiliary vector. TODO: Would shorter proofs result if the .ne hypothesis were changed to two =/= hypothesis? Consider hdmaplem1 35048 through hdmaplem4 35051, which would become obsolete. (Contributed by NM, 15-May-2015.)
|- H = ( LHyp ` K )   &    |- E = <. ( _I |` ( Base ` K ) ) , ( _I |` ( ( LTrn ` K ) ` W ) ) >.   &    |- U = ( ( DVecH ` K ) ` W )   &    |- V = ( Base ` U )   &    |- N = ( LSpan ` U )   &    |- C = ( (LCDual ` K ) ` W )   &    |- D = ( Base ` C )   &    |- J = ( (HVMap ` K ) ` W )   &    |- I = ( (HDMap1 ` K ) ` W )   &    |- S = ( (HDMap ` K ) ` W )   &    |- ( ph -> ( K e. HL /\ W e. H ) )   &    |- ( ph -> T e. V )   &    |- ( ph -> X e. V )   &    |- ( ph -> -. X e. ( ( N ` { E } ) u. ( N ` { T } ) ) )   =>    |- ( ph -> ( S ` T ) = ( I ` <. X , ( I ` <. E , ( J ` E ) , X >. ) , T >. ) )
Theorem	hdmapval0 35113	Value of map from vectors to functionals at zero. Note: we use dvh3dim 34723 for convenience, even though 3 dimensions aren't necessary at this point. TODO: I think either this or hdmapeq0 35124 could be derived from the other to shorten proof. (Contributed by NM, 17-May-2015.)
|- H = ( LHyp ` K )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- .0. = ( 0g ` U )   &    |- C = ( (LCDual ` K ) ` W )   &    |- Q = ( 0g ` C )   &    |- S = ( (HDMap ` K ) ` W )   &    |- ( ph -> ( K e. HL /\ W e. H ) )   =>    |- ( ph -> ( S ` .0. ) = Q )
Theorem	hdmapeveclem 35114	Lemma for hdmapevec 35115. TODO: combine with hdmapevec 35115 if it shortens overall. (Contributed by NM, 16-May-2015.)
|- H = ( LHyp ` K )   &    |- E = <. ( _I |` ( Base ` K ) ) , ( _I |` ( ( LTrn ` K ) ` W ) ) >.   &    |- J = ( (HVMap ` K ) ` W )   &    |- S = ( (HDMap ` K ) ` W )   &    |- ( ph -> ( K e. HL /\ W e. H ) )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- V = ( Base ` U )   &    |- N = ( LSpan ` U )   &    |- C = ( (LCDual ` K ) ` W )   &    |- D = ( Base ` C )   &    |- I = ( (HDMap1 ` K ) ` W )   &    |- ( ph -> X e. V )   &    |- ( ph -> -. X e. ( ( N ` { E } ) u. ( N ` { E } ) ) )   =>    |- ( ph -> ( S ` E ) = ( J ` E ) )
Theorem	hdmapevec 35115	Value of map from vectors to functionals at the reference vector E. (Contributed by NM, 16-May-2015.)
|- H = ( LHyp ` K )   &    |- E = <. ( _I |` ( Base ` K ) ) , ( _I |` ( ( LTrn ` K ) ` W ) ) >.   &    |- J = ( (HVMap ` K ) ` W )   &    |- S = ( (HDMap ` K ) ` W )   &    |- ( ph -> ( K e. HL /\ W e. H ) )   =>    |- ( ph -> ( S ` E ) = ( J ` E ) )
Theorem	hdmapevec2 35116	The inner product of the reference vector E with itself is nonzero. This shows the inner product condition in the proof of Theorem 3.6 of [Holland95] p. 14 line 32, [ e , e ] =/= 0 is satisfied. TODO: remove redundant hypothesis hdmapevec.j. (Contributed by NM, 1-Jun-2015.)
|- H = ( LHyp ` K )   &    |- E = <. ( _I |` ( Base ` K ) ) , ( _I |` ( ( LTrn ` K ) ` W ) ) >.   &    |- J = ( (HVMap ` K ) ` W )   &    |- S = ( (HDMap ` K ) ` W )   &    |- ( ph -> ( K e. HL /\ W e. H ) )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- R = (Scalar ` U )   &    |- .1. = ( 1r ` R )   =>    |- ( ph -> ( ( S ` E ) ` E ) = .1. )
Theorem	hdmapval3lemN 35117	Value of map from vectors to functionals at arguments not colinear with the reference vector E. (Contributed by NM, 17-May-2015.) (New usage is discouraged.)
|- H = ( LHyp ` K )   &    |- E = <. ( _I |` ( Base ` K ) ) , ( _I |` ( ( LTrn ` K ) ` W ) ) >.   &    |- U = ( ( DVecH ` K ) ` W )   &    |- V = ( Base ` U )   &    |- N = ( LSpan ` U )   &    |- C = ( (LCDual ` K ) ` W )   &    |- D = ( Base ` C )   &    |- J = ( (HVMap ` K ) ` W )   &    |- I = ( (HDMap1 ` K ) ` W )   &    |- S = ( (HDMap ` K ) ` W )   &    |- ( ph -> ( K e. HL /\ W e. H ) )   &    |- ( ph -> ( N ` { T } ) =/= ( N ` { E } ) )   &    |- ( ph -> T e. ( V \ { ( 0g ` U ) } ) )   &    |- ( ph -> x e. V )   &    |- ( ph -> -. x e. ( N ` { E , T } ) )   =>    |- ( ph -> ( S ` T ) = ( I ` <. E , ( J ` E ) , T >. ) )
Theorem	hdmapval3N 35118	Value of map from vectors to functionals at arguments not colinear with the reference vector E. (Contributed by NM, 17-May-2015.) (New usage is discouraged.)
|- H = ( LHyp ` K )   &    |- E = <. ( _I |` ( Base ` K ) ) , ( _I |` ( ( LTrn ` K ) ` W ) ) >.   &    |- U = ( ( DVecH ` K ) ` W )   &    |- V = ( Base ` U )   &    |- N = ( LSpan ` U )   &    |- C = ( (LCDual ` K ) ` W )   &    |- D = ( Base ` C )   &    |- J = ( (HVMap ` K ) ` W )   &    |- I = ( (HDMap1 ` K ) ` W )   &    |- S = ( (HDMap ` K ) ` W )   &    |- ( ph -> ( K e. HL /\ W e. H ) )   &    |- ( ph -> ( N ` { T } ) =/= ( N ` { E } ) )   &    |- ( ph -> T e. V )   =>    |- ( ph -> ( S ` T ) = ( I ` <. E , ( J ` E ) , T >. ) )
Theorem	hdmap10lem 35119	Lemma for hdmap10 35120. (Contributed by NM, 17-May-2015.)
|- H = ( LHyp ` K )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- V = ( Base ` U )   &    |- N = ( LSpan ` U )   &    |- C = ( (LCDual ` K ) ` W )   &    |- L = ( LSpan ` C )   &    |- M = ( (mapd ` K ) ` W )   &    |- S = ( (HDMap ` K ) ` W )   &    |- ( ph -> ( K e. HL /\ W e. H ) )   &    |- E = <. ( _I |` ( Base ` K ) ) , ( _I |` ( ( LTrn ` K ) ` W ) ) >.   &    |- .0. = ( 0g ` U )   &    |- D = ( Base ` C )   &    |- J = ( (HVMap ` K ) ` W )   &    |- I = ( (HDMap1 ` K ) ` W )   &    |- ( ph -> T e. ( V \ { .0. } ) )   =>    |- ( ph -> ( M ` ( N ` { T } ) ) = ( L ` { ( S ` T ) } ) )
Theorem	hdmap10 35120	Part 10 in [Baer] p. 48 line 33, (Ft)* = G(tS) in their notation (S = sigma). (Contributed by NM, 17-May-2015.)
|- H = ( LHyp ` K )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- V = ( Base ` U )   &    |- N = ( LSpan ` U )   &    |- C = ( (LCDual ` K ) ` W )   &    |- L = ( LSpan ` C )   &    |- M = ( (mapd ` K ) ` W )   &    |- S = ( (HDMap ` K ) ` W )   &    |- ( ph -> ( K e. HL /\ W e. H ) )   &    |- ( ph -> T e. V )   =>    |- ( ph -> ( M ` ( N ` { T } ) ) = ( L ` { ( S ` T ) } ) )
Theorem	hdmap11lem1 35121	Lemma for hdmapadd 35123. (Contributed by NM, 26-May-2015.)
|- H = ( LHyp ` K )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- V = ( Base ` U )   &    |- .+ = ( +g ` U )   &    |- C = ( (LCDual ` K ) ` W )   &    |- .+b = ( +g ` C )   &    |- S = ( (HDMap ` K ) ` W )   &    |- ( ph -> ( K e. HL /\ W e. H ) )   &    |- ( ph -> X e. V )   &    |- ( ph -> Y e. V )   &    |- E = <. ( _I |` ( Base ` K ) ) , ( _I |` ( ( LTrn ` K ) ` W ) ) >.   &    |- .0. = ( 0g ` U )   &    |- N = ( LSpan ` U )   &    |- D = ( Base ` C )   &    |- L = ( LSpan ` C )   &    |- M = ( (mapd ` K ) ` W )   &    |- J = ( (HVMap ` K ) ` W )   &    |- I = ( (HDMap1 ` K ) ` W )   &    |- ( ph -> z e. V )   &    |- ( ph -> -. z e. ( N ` { X , Y } ) )   &    |- ( ph -> ( N ` { z } ) =/= ( N ` { E } ) )   =>    |- ( ph -> ( S ` ( X .+ Y ) ) = ( ( S ` X ) .+b ( S ` Y ) ) )
Theorem	hdmap11lem2 35122	Lemma for hdmapadd 35123. (Contributed by NM, 26-May-2015.)
|- H = ( LHyp ` K )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- V = ( Base ` U )   &    |- .+ = ( +g ` U )   &    |- C = ( (LCDual ` K ) ` W )   &    |- .+b = ( +g ` C )   &    |- S = ( (HDMap ` K ) ` W )   &    |- ( ph -> ( K e. HL /\ W e. H ) )   &    |- ( ph -> X e. V )   &    |- ( ph -> Y e. V )   &    |- E = <. ( _I |` ( Base ` K ) ) , ( _I |` ( ( LTrn ` K ) ` W ) ) >.   &    |- .0. = ( 0g ` U )   &    |- N = ( LSpan ` U )   &    |- D = ( Base ` C )   &    |- L = ( LSpan ` C )   &    |- M = ( (mapd ` K ) ` W )   &    |- J = ( (HVMap ` K ) ` W )   &    |- I = ( (HDMap1 ` K ) ` W )   =>    |- ( ph -> ( S ` ( X .+ Y ) ) = ( ( S ` X ) .+b ( S ` Y ) ) )
Theorem	hdmapadd 35123	Part 11 in [Baer] p. 48 line 35, (a+b)S = aS+bS in their notation (S = sigma). (Contributed by NM, 22-May-2015.)
|- H = ( LHyp ` K )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- V = ( Base ` U )   &    |- .+ = ( +g ` U )   &    |- C = ( (LCDual ` K ) ` W )   &    |- .+b = ( +g ` C )   &    |- S = ( (HDMap ` K ) ` W )   &    |- ( ph -> ( K e. HL /\ W e. H ) )   &    |- ( ph -> X e. V )   &    |- ( ph -> Y e. V )   =>    |- ( ph -> ( S ` ( X .+ Y ) ) = ( ( S ` X ) .+b ( S ` Y ) ) )
Theorem	hdmapeq0 35124	Part of proof of part 12 in [Baer] p. 49 line 3. (Contributed by NM, 22-May-2015.)
|- H = ( LHyp ` K )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- V = ( Base ` U )   &    |- .0. = ( 0g ` U )   &    |- C = ( (LCDual ` K ) ` W )   &    |- Q = ( 0g ` C )   &    |- S = ( (HDMap ` K ) ` W )   &    |- ( ph -> ( K e. HL /\ W e. H ) )   &    |- ( ph -> T e. V )   =>    |- ( ph -> ( ( S ` T ) = Q <-> T = .0. ) )
Theorem	hdmapnzcl 35125	Nonzero vector closure of map from vectors to functionals with closed kernels. (Contributed by NM, 27-May-2015.)
|- H = ( LHyp ` K )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- V = ( Base ` U )   &    |- .0. = ( 0g ` U )   &    |- C = ( (LCDual ` K ) ` W )   &    |- Q = ( 0g ` C )   &    |- D = ( Base ` C )   &    |- S = ( (HDMap ` K ) ` W )   &    |- ( ph -> ( K e. HL /\ W e. H ) )   &    |- ( ph -> T e. ( V \ { .0. } ) )   =>    |- ( ph -> ( S ` T ) e. ( D \ { Q } ) )
Theorem	hdmapneg 35126	Part of proof of part 12 in [Baer] p. 49 line 4. The sigma map of a negative is the negative of the sigma map. (Contributed by NM, 24-May-2015.)
|- H = ( LHyp ` K )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- V = ( Base ` U )   &    |- M = ( invg ` U )   &    |- C = ( (LCDual ` K ) ` W )   &    |- I = ( invg ` C )   &    |- S = ( (HDMap ` K ) ` W )   &    |- ( ph -> ( K e. HL /\ W e. H ) )   &    |- ( ph -> T e. V )   =>    |- ( ph -> ( S ` ( M ` T ) ) = ( I ` ( S ` T ) ) )
Theorem	hdmapsub 35127	Part of proof of part 12 in [Baer] p. 49 line 5, (a-b)S = aS-bS in their notation (S = sigma). (Contributed by NM, 26-May-2015.)
|- H = ( LHyp ` K )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- V = ( Base ` U )   &    |- .- = ( -g ` U )   &    |- C = ( (LCDual ` K ) ` W )   &    |- N = ( -g ` C )   &    |- S = ( (HDMap ` K ) ` W )   &    |- ( ph -> ( K e. HL /\ W e. H ) )   &    |- ( ph -> X e. V )   &    |- ( ph -> Y e. V )   =>    |- ( ph -> ( S ` ( X .- Y ) ) = ( ( S ` X ) N ( S ` Y ) ) )
Theorem	hdmap11 35128	Part of proof of part 12 in [Baer] p. 49 line 4, aS=bS iff a=b in their notation (S = sigma). The sigma map is one-to-one. (Contributed by NM, 26-May-2015.)
|- H = ( LHyp ` K )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- V = ( Base ` U )   &    |- S = ( (HDMap ` K ) ` W )   &    |- ( ph -> ( K e. HL /\ W e. H ) )   &    |- ( ph -> X e. V )   &    |- ( ph -> Y e. V )   =>    |- ( ph -> ( ( S ` X ) = ( S ` Y ) <-> X = Y ) )
Theorem	hdmaprnlem1N 35129	Part of proof of part 12 in [Baer] p. 49 line 10, Gu' =/= Gs. Our ( N ` { v } ) is Baer's T. (Contributed by NM, 26-May-2015.) (New usage is discouraged.)
|- H = ( LHyp ` K )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- V = ( Base ` U )   &    |- N = ( LSpan ` U )   &    |- C = ( (LCDual ` K ) ` W )   &    |- L = ( LSpan ` C )   &    |- M = ( (mapd ` K ) ` W )   &    |- S = ( (HDMap ` K ) ` W )   &    |- ( ph -> ( K e. HL /\ W e. H ) )   &    |- ( ph -> s e. ( D \ { Q } ) )   &    |- ( ph -> v e. V )   &    |- ( ph -> ( M ` ( N ` { v } ) ) = ( L ` { s } ) )   &    |- ( ph -> u e. V )   &    |- ( ph -> -. u e. ( N ` { v } ) )   =>    |- ( ph -> ( L ` { ( S ` u ) } ) =/= ( L ` { s } ) )
Theorem	hdmaprnlem3N 35130	Part of proof of part 12 in [Baer] p. 49 line 15, T =/= P. Our ( `' M ` ( L ` { ( ( S ` u ) .+b s ) } ) ) is Baer's P, where P* = G(u'+s). (Contributed by NM, 27-May-2015.) (New usage is discouraged.)
|- H = ( LHyp ` K )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- V = ( Base ` U )   &    |- N = ( LSpan ` U )   &    |- C = ( (LCDual ` K ) ` W )   &    |- L = ( LSpan ` C )   &    |- M = ( (mapd ` K ) ` W )   &    |- S = ( (HDMap ` K ) ` W )   &    |- ( ph -> ( K e. HL /\ W e. H ) )   &    |- ( ph -> s e. ( D \ { Q } ) )   &    |- ( ph -> v e. V )   &    |- ( ph -> ( M ` ( N ` { v } ) ) = ( L ` { s } ) )   &    |- ( ph -> u e. V )   &    |- ( ph -> -. u e. ( N ` { v } ) )   &    |- D = ( Base ` C )   &    |- Q = ( 0g ` C )   &    |- .0. = ( 0g ` U )   &    |- .+b = ( +g ` C )   =>    |- ( ph -> ( N ` { v } ) =/= ( `' M ` ( L ` { ( ( S ` u ) .+b s ) } ) ) )
Theorem	hdmaprnlem3uN 35131	Part of proof of part 12 in [Baer] p. 49. (Contributed by NM, 29-May-2015.) (New usage is discouraged.)
|- H = ( LHyp ` K )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- V = ( Base ` U )   &    |- N = ( LSpan ` U )   &    |- C = ( (LCDual ` K ) ` W )   &    |- L = ( LSpan ` C )   &    |- M = ( (mapd ` K ) ` W )   &    |- S = ( (HDMap ` K ) ` W )   &    |- ( ph -> ( K e. HL /\ W e. H ) )   &    |- ( ph -> s e. ( D \ { Q } ) )   &    |- ( ph -> v e. V )   &    |- ( ph -> ( M ` ( N ` { v } ) ) = ( L ` { s } ) )   &    |- ( ph -> u e. V )   &    |- ( ph -> -. u e. ( N ` { v } ) )   &    |- D = ( Base ` C )   &    |- Q = ( 0g ` C )   &    |- .0. = ( 0g ` U )   &    |- .+b = ( +g ` C )   =>    |- ( ph -> ( N ` { u } ) =/= ( `' M ` ( L ` { ( ( S ` u ) .+b s ) } ) ) )
Theorem	hdmaprnlem4tN 35132	Lemma for hdmaprnN 35144. TODO: This lemma doesn't quite pay for itself even though used 4 times. Maybe prove this directly instead. (Contributed by NM, 27-May-2015.) (New usage is discouraged.)
|- H = ( LHyp ` K )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- V = ( Base ` U )   &    |- N = ( LSpan ` U )   &    |- C = ( (LCDual ` K ) ` W )   &    |- L = ( LSpan ` C )   &    |- M = ( (mapd ` K ) ` W )   &    |- S = ( (HDMap ` K ) ` W )   &    |- ( ph -> ( K e. HL /\ W e. H ) )   &    |- ( ph -> s e. ( D \ { Q } ) )   &    |- ( ph -> v e. V )   &    |- ( ph -> ( M ` ( N ` { v } ) ) = ( L ` { s } ) )   &    |- ( ph -> u e. V )   &    |- ( ph -> -. u e. ( N ` { v } ) )   &    |- D = ( Base ` C )   &    |- Q = ( 0g ` C )   &    |- .0. = ( 0g ` U )   &    |- .+b = ( +g ` C )   &    |- ( ph -> t e. ( ( N ` { v } ) \ { .0. } ) )   =>    |- ( ph -> t e. V )
Theorem	hdmaprnlem4N 35133	Part of proof of part 12 in [Baer] p. 49 line 19. (T* =) (Ft)* = Gs. (Contributed by NM, 27-May-2015.) (New usage is discouraged.)
|- H = ( LHyp ` K )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- V = ( Base ` U )   &    |- N = ( LSpan ` U )   &    |- C = ( (LCDual ` K ) ` W )   &    |- L = ( LSpan ` C )   &    |- M = ( (mapd ` K ) ` W )   &    |- S = ( (HDMap ` K ) ` W )   &    |- ( ph -> ( K e. HL /\ W e. H ) )   &    |- ( ph -> s e. ( D \ { Q } ) )   &    |- ( ph -> v e. V )   &    |- ( ph -> ( M ` ( N ` { v } ) ) = ( L ` { s } ) )   &    |- ( ph -> u e. V )   &    |- ( ph -> -. u e. ( N ` { v } ) )   &    |- D = ( Base ` C )   &    |- Q = ( 0g ` C )   &    |- .0. = ( 0g ` U )   &    |- .+b = ( +g ` C )   &    |- ( ph -> t e. ( ( N ` { v } ) \ { .0. } ) )   =>    |- ( ph -> ( M ` ( N ` { t } ) ) = ( L ` { s } ) )
Theorem	hdmaprnlem6N 35134	Part of proof of part 12 in [Baer] p. 49 line 18, G(u'+s) = G(u'+t). (Contributed by NM, 27-May-2015.) (New usage is discouraged.)
|- H = ( LHyp ` K )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- V = ( Base ` U )   &    |- N = ( LSpan ` U )   &    |- C = ( (LCDual ` K ) ` W )   &    |- L = ( LSpan ` C )   &    |- M = ( (mapd ` K ) ` W )   &    |- S = ( (HDMap ` K ) ` W )   &    |- ( ph -> ( K e. HL /\ W e. H ) )   &    |- ( ph -> s e. ( D \ { Q } ) )   &    |- ( ph -> v e. V )   &    |- ( ph -> ( M ` ( N ` { v } ) ) = ( L ` { s } ) )   &    |- ( ph -> u e. V )   &    |- ( ph -> -. u e. ( N ` { v } ) )   &    |- D = ( Base ` C )   &    |- Q = ( 0g ` C )   &    |- .0. = ( 0g ` U )   &    |- .+b = ( +g ` C )   &    |- ( ph -> t e. ( ( N ` { v } ) \ { .0. } ) )   &    |- .+ = ( +g ` U )   &    |- ( ph -> ( L ` { ( ( S ` u ) .+b s ) } ) = ( M ` ( N ` { ( u .+ t ) } ) ) )   =>    |- ( ph -> ( L ` { ( ( S ` u ) .+b s ) } ) = ( L ` { ( ( S ` u ) .+b ( S ` t ) ) } ) )
Theorem	hdmaprnlem7N 35135	Part of proof of part 12 in [Baer] p. 49 line 19, s-St e. G(u'+s) = P*. (Contributed by NM, 27-May-2015.) (New usage is discouraged.)
|- H = ( LHyp ` K )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- V = ( Base ` U )   &    |- N = ( LSpan ` U )   &    |- C = ( (LCDual ` K ) ` W )   &    |- L = ( LSpan ` C )   &    |- M = ( (mapd ` K ) ` W )   &    |- S = ( (HDMap ` K ) ` W )   &    |- ( ph -> ( K e. HL /\ W e. H ) )   &    |- ( ph -> s e. ( D \ { Q } ) )   &    |- ( ph -> v e. V )   &    |- ( ph -> ( M ` ( N ` { v } ) ) = ( L ` { s } ) )   &    |- ( ph -> u e. V )   &    |- ( ph -> -. u e. ( N ` { v } ) )   &    |- D = ( Base ` C )   &    |- Q = ( 0g ` C )   &    |- .0. = ( 0g ` U )   &    |- .+b = ( +g ` C )   &    |- ( ph -> t e. ( ( N ` { v } ) \ { .0. } ) )   &    |- .+ = ( +g ` U )   &    |- ( ph -> ( L ` { ( ( S ` u ) .+b s ) } ) = ( M ` ( N ` { ( u .+ t ) } ) ) )   =>    |- ( ph -> ( s ( -g ` C ) ( S ` t ) ) e. ( L ` { ( ( S ` u ) .+b s ) } ) )
Theorem	hdmaprnlem8N 35136	Part of proof of part 12 in [Baer] p. 49 line 19, s-St e. (Ft)* = T*. (Contributed by NM, 27-May-2015.) (New usage is discouraged.)
|- H = ( LHyp ` K )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- V = ( Base ` U )   &    |- N = ( LSpan ` U )   &    |- C = ( (LCDual ` K ) ` W )   &    |- L = ( LSpan ` C )   &    |- M = ( (mapd ` K ) ` W )   &    |- S = ( (HDMap ` K ) ` W )   &    |- ( ph -> ( K e. HL /\ W e. H ) )   &    |- ( ph -> s e. ( D \ { Q } ) )   &    |- ( ph -> v e. V )   &    |- ( ph -> ( M ` ( N ` { v } ) ) = ( L ` { s } ) )   &    |- ( ph -> u e. V )   &    |- ( ph -> -. u e. ( N ` { v } ) )   &    |- D = ( Base ` C )   &    |- Q = ( 0g ` C )   &    |- .0. = ( 0g ` U )   &    |- .+b = ( +g ` C )   &    |- ( ph -> t e. ( ( N ` { v } ) \ { .0. } ) )   &    |- .+ = ( +g ` U )   &    |- ( ph -> ( L ` { ( ( S ` u ) .+b s ) } ) = ( M ` ( N ` { ( u .+ t ) } ) ) )   =>    |- ( ph -> ( s ( -g ` C ) ( S ` t ) ) e. ( M ` ( N ` { t } ) ) )
Theorem	hdmaprnlem9N 35137	Part of proof of part 12 in [Baer] p. 49 line 21, s=S(t). TODO: we seem to be going back and forth with mapd11 34916 and mapdcnv11N 34936. Use better hypotheses and/or theorems? (Contributed by NM, 27-May-2015.) (New usage is discouraged.)
|- H = ( LHyp ` K )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- V = ( Base ` U )   &    |- N = ( LSpan ` U )   &    |- C = ( (LCDual ` K ) ` W )   &    |- L = ( LSpan ` C )   &    |- M = ( (mapd ` K ) ` W )   &    |- S = ( (HDMap ` K ) ` W )   &    |- ( ph -> ( K e. HL /\ W e. H ) )   &    |- ( ph -> s e. ( D \ { Q } ) )   &    |- ( ph -> v e. V )   &    |- ( ph -> ( M ` ( N ` { v } ) ) = ( L ` { s } ) )   &    |- ( ph -> u e. V )   &    |- ( ph -> -. u e. ( N ` { v } ) )   &    |- D = ( Base ` C )   &    |- Q = ( 0g ` C )   &    |- .0. = ( 0g ` U )   &    |- .+b = ( +g ` C )   &    |- ( ph -> t e. ( ( N ` { v } ) \ { .0. } ) )   &    |- .+ = ( +g ` U )   &    |- ( ph -> ( L ` { ( ( S ` u ) .+b s ) } ) = ( M ` ( N ` { ( u .+ t ) } ) ) )   =>    |- ( ph -> s = ( S ` t ) )
Theorem	hdmaprnlem3eN 35138*	Lemma for hdmaprnN 35144. (Contributed by NM, 29-May-2015.) (New usage is discouraged.)
|- H = ( LHyp ` K )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- V = ( Base ` U )   &    |- N = ( LSpan ` U )   &    |- C = ( (LCDual ` K ) ` W )   &    |- L = ( LSpan ` C )   &    |- M = ( (mapd ` K ) ` W )   &    |- S = ( (HDMap ` K ) ` W )   &    |- ( ph -> ( K e. HL /\ W e. H ) )   &    |- ( ph -> s e. ( D \ { Q } ) )   &    |- ( ph -> v e. V )   &    |- ( ph -> ( M ` ( N ` { v } ) ) = ( L ` { s } ) )   &    |- ( ph -> u e. V )   &    |- ( ph -> -. u e. ( N ` { v } ) )   &    |- D = ( Base ` C )   &    |- Q = ( 0g ` C )   &    |- .0. = ( 0g ` U )   &    |- .+b = ( +g ` C )   &    |- .+ = ( +g ` U )   =>    |- ( ph -> E. t e. ( ( N ` { v } ) \ { .0. } ) ( L ` { ( ( S ` u ) .+b s ) } ) = ( M ` ( N ` { ( u .+ t ) } ) ) )
Theorem	hdmaprnlem10N 35139*	Lemma for hdmaprnN 35144. Show s is in the range of S. (Contributed by NM, 29-May-2015.) (New usage is discouraged.)
|- H = ( LHyp ` K )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- V = ( Base ` U )   &    |- N = ( LSpan ` U )   &    |- C = ( (LCDual ` K ) ` W )   &    |- L = ( LSpan ` C )   &    |- M = ( (mapd ` K ) ` W )   &    |- S = ( (HDMap ` K ) ` W )   &    |- ( ph -> ( K e. HL /\ W e. H ) )   &    |- ( ph -> s e. ( D \ { Q } ) )   &    |- ( ph -> v e. V )   &    |- ( ph -> ( M ` ( N ` { v } ) ) = ( L ` { s } ) )   &    |- ( ph -> u e. V )   &    |- ( ph -> -. u e. ( N ` { v } ) )   &    |- D = ( Base ` C )   &    |- Q = ( 0g ` C )   &    |- .0. = ( 0g ` U )   &    |- .+b = ( +g ` C )   &    |- .+ = ( +g ` U )   =>    |- ( ph -> E. t e. V ( S ` t ) = s )
Theorem	hdmaprnlem11N 35140*	Lemma for hdmaprnN 35144. Show s is in the range of S. (Contributed by NM, 29-May-2015.) (New usage is discouraged.)
|- H = ( LHyp ` K )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- V = ( Base ` U )   &    |- N = ( LSpan ` U )   &    |- C = ( (LCDual ` K ) ` W )   &    |- L = ( LSpan ` C )   &    |- M = ( (mapd ` K ) ` W )   &    |- S = ( (HDMap ` K ) ` W )   &    |- ( ph -> ( K e. HL /\ W e. H ) )   &    |- ( ph -> s e. ( D \ { Q } ) )   &    |- ( ph -> v e. V )   &    |- ( ph -> ( M ` ( N ` { v } ) ) = ( L ` { s } ) )   &    |- ( ph -> u e. V )   &    |- ( ph -> -. u e. ( N ` { v } ) )   &    |- D = ( Base ` C )   &    |- Q = ( 0g ` C )   &    |- .0. = ( 0g ` U )   &    |- .+b = ( +g ` C )   &    |- .+ = ( +g ` U )   =>    |- ( ph -> s e. ran S )
Theorem	hdmaprnlem15N 35141*	Lemma for hdmaprnN 35144. Eliminate u. (Contributed by NM, 30-May-2015.) (New usage is discouraged.)
|- H = ( LHyp ` K )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- V = ( Base ` U )   &    |- N = ( LSpan ` U )   &    |- C = ( (LCDual ` K ) ` W )   &    |- D = ( Base ` C )   &    |- .0. = ( 0g ` C )   &    |- L = ( LSpan ` C )   &    |- M = ( (mapd ` K ) ` W )   &    |- S = ( (HDMap ` K ) ` W )   &    |- ( ph -> ( K e. HL /\ W e. H ) )   &    |- ( ph -> s e. ( D \ { .0. } ) )   &    |- ( ph -> v e. V )   &    |- ( ph -> ( M ` ( N ` { v } ) ) = ( L ` { s } ) )   =>    |- ( ph -> s e. ran S )
Theorem	hdmaprnlem16N 35142	Lemma for hdmaprnN 35144. Eliminate v. (Contributed by NM, 30-May-2015.) (New usage is discouraged.)
|- H = ( LHyp ` K )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- V = ( Base ` U )   &    |- N = ( LSpan ` U )   &    |- C = ( (LCDual ` K ) ` W )   &    |- D = ( Base ` C )   &    |- .0. = ( 0g ` C )   &    |- L = ( LSpan ` C )   &    |- M = ( (mapd ` K ) ` W )   &    |- S = ( (HDMap ` K ) ` W )   &    |- ( ph -> ( K e. HL /\ W e. H ) )   &    |- ( ph -> s e. ( D \ { .0. } ) )   =>    |- ( ph -> s e. ran S )
Theorem	hdmaprnlem17N 35143	Lemma for hdmaprnN 35144. Include zero. (Contributed by NM, 30-May-2015.) (New usage is discouraged.)
|- H = ( LHyp ` K )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- V = ( Base ` U )   &    |- N = ( LSpan ` U )   &    |- C = ( (LCDual ` K ) ` W )   &    |- D = ( Base ` C )   &    |- .0. = ( 0g ` C )   &    |- L = ( LSpan ` C )   &    |- M = ( (mapd ` K ) ` W )   &    |- S = ( (HDMap ` K ) ` W )   &    |- ( ph -> ( K e. HL /\ W e. H ) )   &    |- ( ph -> s e. D )   =>    |- ( ph -> s e. ran S )
Theorem	hdmaprnN 35144	Part of proof of part 12 in [Baer] p. 49 line 21, As=B. (Contributed by NM, 30-May-2015.) (New usage is discouraged.)
|- H = ( LHyp ` K )   &    |- C = ( (LCDual ` K ) ` W )   &    |- D = ( Base ` C )   &    |- S = ( (HDMap ` K ) ` W )   &    |- ( ph -> ( K e. HL /\ W e. H ) )   =>    |- ( ph -> ran S = D )
Theorem	hdmapf1oN 35145	Part 12 in [Baer] p. 49. The map from vectors to functionals with closed kernels maps one-to-one onto. Combined with hdmapadd 35123, this shows the map is an automorphism from the additive group of vectors to the additive group of functionals with closed kernels. (Contributed by NM, 30-May-2015.) (New usage is discouraged.)
|- H = ( LHyp ` K )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- V = ( Base ` U )   &    |- C = ( (LCDual ` K ) ` W )   &    |- D = ( Base ` C )   &    |- S = ( (HDMap ` K ) ` W )   &    |- ( ph -> ( K e. HL /\ W e. H ) )   =>    |- ( ph -> S : V -1-1-onto-> D )
Theorem	hdmap14lem1a 35146	Prior to part 14 in [Baer] p. 49, line 25. (Contributed by NM, 31-May-2015.)
|- H = ( LHyp ` K )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- V = ( Base ` U )   &    |- .x. = ( .s ` U )   &    |- R = (Scalar ` U )   &    |- B = ( Base ` R )   &    |- C = ( (LCDual ` K ) ` W )   &    |- .xb = ( .s ` C )   &    |- L = ( LSpan ` C )   &    |- P = (Scalar ` C )   &    |- A = ( Base ` P )   &    |- S = ( (HDMap ` K ) ` W )   &    |- ( ph -> ( K e. HL /\ W e. H ) )   &    |- ( ph -> X e. V )   &    |- ( ph -> F e. B )   &    |- .0. = ( 0g ` R )   &    |- ( ph -> F =/= .0. )   =>    |- ( ph -> ( L ` { ( S ` X ) } ) = ( L ` { ( S ` ( F .x. X ) ) } ) )
Theorem	hdmap14lem2a 35147*	Prior to part 14 in [Baer] p. 49, line 25. TODO: fix to include F = .0. so it can be used in hdmap14lem10 35157. (Contributed by NM, 31-May-2015.)
|- H = ( LHyp ` K )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- V = ( Base ` U )   &    |- .x. = ( .s ` U )   &    |- R = (Scalar ` U )   &    |- B = ( Base ` R )   &    |- C = ( (LCDual ` K ) ` W )   &    |- .xb = ( .s ` C )   &    |- L = ( LSpan ` C )   &    |- P = (Scalar ` C )   &    |- A = ( Base ` P )   &    |- S = ( (HDMap ` K ) ` W )   &    |- ( ph -> ( K e. HL /\ W e. H ) )   &    |- ( ph -> X e. V )   &    |- ( ph -> F e. B )   =>    |- ( ph -> E. g e. A ( S ` ( F .x. X ) ) = ( g .xb ( S ` X ) ) )
Theorem	hdmap14lem1 35148	Prior to part 14 in [Baer] p. 49, line 25. (Contributed by NM, 31-May-2015.)
|- H = ( LHyp ` K )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- V = ( Base ` U )   &    |- .x. = ( .s ` U )   &    |- .0. = ( 0g ` U )   &    |- R = (Scalar ` U )   &    |- B = ( Base ` R )   &    |- Z = ( 0g ` R )   &    |- C = ( (LCDual ` K ) ` W )   &    |- .xb = ( .s ` C )   &    |- L = ( LSpan ` C )   &    |- P = (Scalar ` C )   &    |- A = ( Base ` P )   &    |- Q = ( 0g ` P )   &    |- S = ( (HDMap ` K ) ` W )   &    |- ( ph -> ( K e. HL /\ W e. H ) )   &    |- ( ph -> X e. ( V \ { .0. } ) )   &    |- ( ph -> F e. ( B \ { Z } ) )   =>    |- ( ph -> ( L ` { ( S ` X ) } ) = ( L ` { ( S ` ( F .x. X ) ) } ) )
Theorem	hdmap14lem2N 35149*	Prior to part 14 in [Baer] p. 49, line 25. TODO: fix to include F = Z so it can be used in hdmap14lem10 35157. (Contributed by NM, 31-May-2015.) (New usage is discouraged.)
|- H = ( LHyp ` K )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- V = ( Base ` U )   &    |- .x. = ( .s ` U )   &    |- .0. = ( 0g ` U )   &    |- R = (Scalar ` U )   &    |- B = ( Base ` R )   &    |- Z = ( 0g ` R )   &    |- C = ( (LCDual ` K ) ` W )   &    |- .xb = ( .s ` C )   &    |- L = ( LSpan ` C )   &    |- P = (Scalar ` C )   &    |- A = ( Base ` P )   &    |- Q = ( 0g ` P )   &    |- S = ( (HDMap ` K ) ` W )   &    |- ( ph -> ( K e. HL /\ W e. H ) )   &    |- ( ph -> X e. ( V \ { .0. } ) )   &    |- ( ph -> F e. ( B \ { Z } ) )   =>    |- ( ph -> E. g e. ( A \ { Q } ) ( S ` ( F .x. X ) ) = ( g .xb ( S ` X ) ) )
Theorem	hdmap14lem3 35150*	Prior to part 14 in [Baer] p. 49, line 26. (Contributed by NM, 31-May-2015.)
|- H = ( LHyp ` K )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- V = ( Base ` U )   &    |- .x. = ( .s ` U )   &    |- .0. = ( 0g ` U )   &    |- R = (Scalar ` U )   &    |- B = ( Base ` R )   &    |- Z = ( 0g ` R )   &    |- C = ( (LCDual ` K ) ` W )   &    |- .xb = ( .s ` C )   &    |- L = ( LSpan ` C )   &    |- P = (Scalar ` C )   &    |- A = ( Base ` P )   &    |- Q = ( 0g ` P )   &    |- S = ( (HDMap ` K ) ` W )   &    |- ( ph -> ( K e. HL /\ W e. H ) )   &    |- ( ph -> X e. ( V \ { .0. } ) )   &    |- ( ph -> F e. ( B \ { Z } ) )   =>    |- ( ph -> E! g e. ( A \ { Q } ) ( S ` ( F .x. X ) ) = ( g .xb ( S ` X ) ) )
Theorem	hdmap14lem4a 35151*	Simplify ( A \ { Q } ) in hdmap14lem3 35150 to provide a slightly simpler definition later. (Contributed by NM, 31-May-2015.)
|- H = ( LHyp ` K )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- V = ( Base ` U )   &    |- .x. = ( .s ` U )   &    |- .0. = ( 0g ` U )   &    |- R = (Scalar ` U )   &    |- B = ( Base ` R )   &    |- Z = ( 0g ` R )   &    |- C = ( (LCDual ` K ) ` W )   &    |- .xb = ( .s ` C )   &    |- L = ( LSpan ` C )   &    |- P = (Scalar ` C )   &    |- A = ( Base ` P )   &    |- Q = ( 0g ` P )   &    |- S = ( (HDMap ` K ) ` W )   &    |- ( ph -> ( K e. HL /\ W e. H ) )   &    |- ( ph -> X e. ( V \ { .0. } ) )   &    |- ( ph -> F e. ( B \ { Z } ) )   =>    |- ( ph -> ( E! g e. ( A \ { Q } ) ( S ` ( F .x. X ) ) = ( g .xb ( S ` X ) ) <-> E! g e. A ( S ` ( F .x. X ) ) = ( g .xb ( S ` X ) ) ) )
Theorem	hdmap14lem4 35152*	Simplify ( A \ { Q } ) in hdmap14lem3 35150 to provide a slightly simpler definition later. TODO: Use hdmap14lem4a 35151 if that one is also used directly elsewhere. Otherwise, merge hdmap14lem4a 35151 into this one. (Contributed by NM, 31-May-2015.)
|- H = ( LHyp ` K )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- V = ( Base ` U )   &    |- .x. = ( .s ` U )   &    |- .0. = ( 0g ` U )   &    |- R = (Scalar ` U )   &    |- B = ( Base ` R )   &    |- Z = ( 0g ` R )   &    |- C = ( (LCDual ` K ) ` W )   &    |- .xb = ( .s ` C )   &    |- L = ( LSpan ` C )   &    |- P = (Scalar ` C )   &    |- A = ( Base ` P )   &    |- Q = ( 0g ` P )   &    |- S = ( (HDMap ` K ) ` W )   &    |- ( ph -> ( K e. HL /\ W e. H ) )   &    |- ( ph -> X e. ( V \ { .0. } ) )   &    |- ( ph -> F e. ( B \ { Z } ) )   =>    |- ( ph -> E! g e. A ( S ` ( F .x. X ) ) = ( g .xb ( S ` X ) ) )
Theorem	hdmap14lem6 35153*	Case where F is zero. (Contributed by NM, 1-Jun-2015.)
|- H = ( LHyp ` K )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- V = ( Base ` U )   &    |- .x. = ( .s ` U )   &    |- .0. = ( 0g ` U )   &    |- R = (Scalar ` U )   &    |- B = ( Base ` R )   &    |- Z = ( 0g ` R )   &    |- C = ( (LCDual ` K ) ` W )   &    |- .xb = ( .s ` C )   &    |- L = ( LSpan ` C )   &    |- P = (Scalar ` C )   &    |- A = ( Base ` P )   &    |- Q = ( 0g ` P )   &    |- S = ( (HDMap ` K ) ` W )   &    |- ( ph -> ( K e. HL /\ W e. H ) )   &    |- ( ph -> X e. ( V \ { .0. } ) )   &    |- ( ph -> F = Z )   =>    |- ( ph -> E! g e. A ( S ` ( F .x. X ) ) = ( g .xb ( S ` X ) ) )
Theorem	hdmap14lem7 35154*	Combine cases of F. TODO: Can this be done at once in hdmap14lem3 35150, in order to get rid of hdmap14lem6 35153? Perhaps modify lspsneu 18274 to become E! k e. K instead of E! k e. ( K \ { .0. } )? (Contributed by NM, 1-Jun-2015.)
|- H = ( LHyp ` K )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- V = ( Base ` U )   &    |- .x. = ( .s ` U )   &    |- .0. = ( 0g ` U )   &    |- R = (Scalar ` U )   &    |- B = ( Base ` R )   &    |- C = ( (LCDual ` K ) ` W )   &    |- .xb = ( .s ` C )   &    |- P = (Scalar ` C )   &    |- A = ( Base ` P )   &    |- S = ( (HDMap ` K ) ` W )   &    |- ( ph -> ( K e. HL /\ W e. H ) )   &    |- ( ph -> X e. ( V \ { .0. } ) )   &    |- ( ph -> F e. B )   =>    |- ( ph -> E! g e. A ( S ` ( F .x. X ) ) = ( g .xb ( S ` X ) ) )
Theorem	hdmap14lem8 35155	Part of proof of part 14 in [Baer] p. 49 lines 33-35. (Contributed by NM, 1-Jun-2015.)
|- H = ( LHyp ` K )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- V = ( Base ` U )   &    |- .+ = ( +g ` U )   &    |- .x. = ( .s ` U )   &    |- .0. = ( 0g ` U )   &    |- N = ( LSpan ` U )   &    |- R = (Scalar ` U )   &    |- B = ( Base ` R )   &    |- C = ( (LCDual ` K ) ` W )   &    |- .+b = ( +g ` C )   &    |- .xb = ( .s ` C )   &    |- P = (Scalar ` C )   &    |- A = ( Base ` P )   &    |- S = ( (HDMap ` K ) ` W )   &    |- ( ph -> ( K e. HL /\ W e. H ) )   &    |- ( ph -> X e. ( V \ { .0. } ) )   &    |- ( ph -> Y e. ( V \ { .0. } ) )   &    |- ( ph -> F e. B )   &    |- ( ph -> G e. A )   &    |- ( ph -> I e. A )   &    |- ( ph -> ( S ` ( F .x. X ) ) = ( G .xb ( S ` X ) ) )   &    |- ( ph -> ( S ` ( F .x. Y ) ) = ( I .xb ( S ` Y ) ) )   &    |- ( ph -> ( N ` { X } ) =/= ( N ` { Y } ) )   &    |- ( ph -> J e. A )   &    |- ( ph -> ( S ` ( F .x. ( X .+ Y ) ) ) = ( J .xb ( S ` ( X .+ Y ) ) ) )   =>    |- ( ph -> ( ( J .xb ( S ` X ) ) .+b ( J .xb ( S ` Y ) ) ) = ( ( G .xb ( S ` X ) ) .+b ( I .xb ( S ` Y ) ) ) )
Theorem	hdmap14lem9 35156	Part of proof of part 14 in [Baer] p. 49 line 38. (Contributed by NM, 1-Jun-2015.)
|- H = ( LHyp ` K )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- V = ( Base ` U )   &    |- .+ = ( +g ` U )   &    |- .x. = ( .s ` U )   &    |- .0. = ( 0g ` U )   &    |- N = ( LSpan ` U )   &    |- R = (Scalar ` U )   &    |- B = ( Base ` R )   &    |- C = ( (LCDual ` K ) ` W )   &    |- .+b = ( +g ` C )   &    |- .xb = ( .s ` C )   &    |- P = (Scalar ` C )   &    |- A = ( Base ` P )   &    |- S = ( (HDMap ` K ) ` W )   &    |- ( ph -> ( K e. HL /\ W e. H ) )   &    |- ( ph -> X e. ( V \ { .0. } ) )   &    |- ( ph -> Y e. ( V \ { .0. } ) )   &    |- ( ph -> F e. B )   &    |- ( ph -> G e. A )   &    |- ( ph -> I e. A )   &    |- ( ph -> ( S ` ( F .x. X ) ) = ( G .xb ( S ` X ) ) )   &    |- ( ph -> ( S ` ( F .x. Y ) ) = ( I .xb ( S ` Y ) ) )   &    |- ( ph -> ( N ` { X } ) =/= ( N ` { Y } ) )   &    |- ( ph -> J e. A )   &    |- ( ph -> ( S ` ( F .x. ( X .+ Y ) ) ) = ( J .xb ( S ` ( X .+ Y ) ) ) )   =>    |- ( ph -> G = I )
Theorem	hdmap14lem10 35157	Part of proof of part 14 in [Baer] p. 49 line 38. (Contributed by NM, 3-Jun-2015.)
|- H = ( LHyp ` K )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- V = ( Base ` U )   &    |- .+ = ( +g ` U )   &    |- .x. = ( .s ` U )   &    |- .0. = ( 0g ` U )   &    |- N = ( LSpan ` U )   &    |- R = (Scalar ` U )   &    |- B = ( Base ` R )   &    |- C = ( (LCDual ` K ) ` W )   &    |- .+b = ( +g ` C )   &    |- .xb = ( .s ` C )   &    |- P = (Scalar ` C )   &    |- A = ( Base ` P )   &    |- S = ( (HDMap ` K ) ` W )   &    |- ( ph -> ( K e. HL /\ W e. H ) )   &    |- ( ph -> X e. ( V \ { .0. } ) )   &    |- ( ph -> Y e. ( V \ { .0. } ) )   &    |- ( ph -> F e. B )   &    |- ( ph -> G e. A )   &    |- ( ph -> I e. A )   &    |- ( ph -> ( S ` ( F .x. X ) ) = ( G .xb ( S ` X ) ) )   &    |- ( ph -> ( S ` ( F .x. Y ) ) = ( I .xb ( S ` Y ) ) )   &    |- ( ph -> ( N ` { X } ) =/= ( N ` { Y } ) )   =>    |- ( ph -> G = I )
Theorem	hdmap14lem11 35158	Part of proof of part 14 in [Baer] p. 50 line 3. (Contributed by NM, 3-Jun-2015.)
|- H = ( LHyp ` K )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- V = ( Base ` U )   &    |- .+ = ( +g ` U )   &    |- .x. = ( .s ` U )   &    |- .0. = ( 0g ` U )   &    |- N = ( LSpan ` U )   &    |- R = (Scalar ` U )   &    |- B = ( Base ` R )   &    |- C = ( (LCDual ` K ) ` W )   &    |- .+b = ( +g ` C )   &    |- .xb = ( .s ` C )   &    |- P = (Scalar ` C )   &    |- A = ( Base ` P )   &    |- S = ( (HDMap ` K ) ` W )   &    |- ( ph -> ( K e. HL /\ W e. H ) )   &    |- ( ph -> X e. ( V \ { .0. } ) )   &    |- ( ph -> Y e. ( V \ { .0. } ) )   &    |- ( ph -> F e. B )   &    |- ( ph -> G e. A )   &    |- ( ph -> I e. A )   &    |- ( ph -> ( S ` ( F .x. X ) ) = ( G .xb ( S ` X ) ) )   &    |- ( ph -> ( S ` ( F .x. Y ) ) = ( I .xb ( S ` Y ) ) )   =>    |- ( ph -> G = I )
Theorem	hdmap14lem12 35159*	Lemma for proof of part 14 in [Baer] p. 50. (Contributed by NM, 6-Jun-2015.)
|- H = ( LHyp ` K )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- V = ( Base ` U )   &    |- .x. = ( .s ` U )   &    |- R = (Scalar ` U )   &    |- B = ( Base ` R )   &    |- C = ( (LCDual ` K ) ` W )   &    |- .xb = ( .s ` C )   &    |- S = ( (HDMap ` K ) ` W )   &    |- ( ph -> ( K e. HL /\ W e. H ) )   &    |- ( ph -> F e. B )   &    |- P = (Scalar ` C )   &    |- A = ( Base ` P )   &    |- .0. = ( 0g ` U )   &    |- ( ph -> X e. ( V \ { .0. } ) )   &    |- ( ph -> G e. A )   =>    |- ( ph -> ( ( S ` ( F .x. X ) ) = ( G .xb ( S ` X ) ) <-> A. y e. ( V \ { .0. } ) ( S ` ( F .x. y ) ) = ( G .xb ( S ` y ) ) ) )
Theorem	hdmap14lem13 35160*	Lemma for proof of part 14 in [Baer] p. 50. (Contributed by NM, 6-Jun-2015.)
|- H = ( LHyp ` K )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- V = ( Base ` U )   &    |- .x. = ( .s ` U )   &    |- R = (Scalar ` U )   &    |- B = ( Base ` R )   &    |- C = ( (LCDual ` K ) ` W )   &    |- .xb = ( .s ` C )   &    |- S = ( (HDMap ` K ) ` W )   &    |- ( ph -> ( K e. HL /\ W e. H ) )   &    |- ( ph -> F e. B )   &    |- P = (Scalar ` C )   &    |- A = ( Base ` P )   &    |- .0. = ( 0g ` U )   &    |- ( ph -> X e. ( V \ { .0. } ) )   &    |- ( ph -> G e. A )   =>    |- ( ph -> ( ( S ` ( F .x. X ) ) = ( G .xb ( S ` X ) ) <-> A. y e. V ( S ` ( F .x. y ) ) = ( G .xb ( S ` y ) ) ) )
Theorem	hdmap14lem14 35161*	Part of proof of part 14 in [Baer] p. 50 line 3. (Contributed by NM, 6-Jun-2015.)
|- H = ( LHyp ` K )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- V = ( Base ` U )   &    |- .x. = ( .s ` U )   &    |- R = (Scalar ` U )   &    |- B = ( Base ` R )   &    |- C = ( (LCDual ` K ) ` W )   &    |- .xb = ( .s ` C )   &    |- S = ( (HDMap ` K ) ` W )   &    |- ( ph -> ( K e. HL /\ W e. H ) )   &    |- ( ph -> F e. B )   &    |- P = (Scalar ` C )   &    |- A = ( Base ` P )   =>    |- ( ph -> E! g e. A A. x e. V ( S ` ( F .x. x ) ) = ( g .xb ( S ` x ) ) )
Theorem	hdmap14lem15 35162*	Part of proof of part 14 in [Baer] p. 50 line 3. Convert scalar base of dual to scalar base of vector space. (Contributed by NM, 6-Jun-2015.)
|- H = ( LHyp ` K )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- V = ( Base ` U )   &    |- .x. = ( .s ` U )   &    |- R = (Scalar ` U )   &    |- B = ( Base ` R )   &    |- C = ( (LCDual ` K ) ` W )   &    |- .xb = ( .s ` C )   &    |- S = ( (HDMap ` K ) ` W )   &    |- ( ph -> ( K e. HL /\ W e. H ) )   &    |- ( ph -> F e. B )   =>    |- ( ph -> E! g e. B A. x e. V ( S ` ( F .x. x ) ) = ( g .xb ( S ` x ) ) )
Syntax	chg 35163	Extend class notation with g-map.
class HGMap
Definition	df-hgmap 35164*	Define 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.)
|- HGMap = ( k e. _V |-> ( w e. ( LHyp ` k ) |-> { a | [. ( ( DVecH ` k ) ` w ) / u ]. [. ( Base ` (Scalar ` u ) ) / b ]. [. ( (HDMap ` k ) ` w ) / m ]. a e. ( x e. b |-> ( iota_ y e. b A. v e. ( Base ` u ) ( m ` ( x ( .s ` u ) v ) ) = ( y ( .s ` ( (LCDual ` k ) ` w ) ) ( m ` v ) ) ) ) } ) )
Theorem	hgmapffval 35165*	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.)
|- H = ( LHyp ` K )   =>    |- ( K e. X -> (HGMap ` K ) = ( w e. H |-> { a | [. ( ( DVecH ` K ) ` w ) / u ]. [. ( Base ` (Scalar ` u ) ) / b ]. [. ( (HDMap ` K ) ` w ) / m ]. a e. ( x e. b |-> ( iota_ y e. b A. v e. ( Base ` u ) ( m ` ( x ( .s ` u ) v ) ) = ( y ( .s ` ( (LCDual ` K ) ` w ) ) ( m ` v ) ) ) ) } ) )
Theorem	hgmapfval 35166*	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.)
|- H = ( LHyp ` K )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- V = ( Base ` U )   &    |- .x. = ( .s ` U )   &    |- R = (Scalar ` U )   &    |- B = ( Base ` R )   &    |- C = ( (LCDual ` K ) ` W )   &    |- .xb = ( .s ` C )   &    |- M = ( (HDMap ` K ) ` W )   &    |- I = ( (HGMap ` K ) ` W )   &    |- ( ph -> ( K e. Y /\ W e. H ) )   =>    |- ( ph -> I = ( x e. B |-> ( iota_ y e. B A. v e. V ( M ` ( x .x. v ) ) = ( y .xb ( M ` v ) ) ) ) )
Theorem	hgmapval 35167*	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 35162. (Contributed by NM, 25-Mar-2015.)
|- H = ( LHyp ` K )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- V = ( Base ` U )   &    |- .x. = ( .s ` U )   &    |- R = (Scalar ` U )   &    |- B = ( Base ` R )   &    |- C = ( (LCDual ` K ) ` W )   &    |- .xb = ( .s ` C )   &    |- M = ( (HDMap ` K ) ` W )   &    |- I = ( (HGMap ` K ) ` W )   &    |- ( ph -> ( K e. Y /\ W e. H ) )   &    |- ( ph -> X e. B )   =>    |- ( ph -> ( I ` X ) = ( iota_ y e. B A. v e. V ( M ` ( X .x. v ) ) = ( y .xb ( M ` v ) ) ) )
Theorem	hgmapfnN 35168	Functionality of scalar sigma map. (Contributed by NM, 7-Jun-2015.) (New usage is discouraged.)
|- H = ( LHyp ` K )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- R = (Scalar ` U )   &    |- B = ( Base ` R )   &    |- G = ( (HGMap ` K ) ` W )   &    |- ( ph -> ( K e. HL /\ W e. H ) )   =>    |- ( ph -> G Fn B )
Theorem	hgmapcl 35169	Closure of scalar sigma map i.e. the map from the vector space scalar base to the dual space scalar base. (Contributed by NM, 6-Jun-2015.)
|- H = ( LHyp ` K )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- R = (Scalar ` U )   &    |- B = ( Base ` R )   &    |- G = ( (HGMap ` K ) ` W )   &    |- ( ph -> ( K e. HL /\ W e. H ) )   &    |- ( ph -> F e. B )   =>    |- ( ph -> ( G ` F ) e. B )
Theorem	hgmapdcl 35170	Closure of the vector space to dual space scalar map, in the scalar sigma map. (Contributed by NM, 6-Jun-2015.)
|- H = ( LHyp ` K )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- R = (Scalar ` U )   &    |- B = ( Base ` R )   &    |- C = ( (LCDual ` K ) ` W )   &    |- Q = (Scalar ` C )   &    |- A = ( Base ` Q )   &    |- G = ( (HGMap ` K ) ` W )   &    |- ( ph -> ( K e. HL /\ W e. H ) )   &    |- ( ph -> F e. B )   =>    |- ( ph -> ( G ` F ) e. A )
Theorem	hgmapvs 35171	Part 15 of [Baer] p. 50 line 6. Also line 15 in [Holland95] p. 14. (Contributed by NM, 6-Jun-2015.)
|- H = ( LHyp ` K )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- V = ( Base ` U )   &    |- .x. = ( .s ` U )   &    |- R = (Scalar ` U )   &    |- B = ( Base ` R )   &    |- C = ( (LCDual ` K ) ` W )   &    |- .xb = ( .s ` C )   &    |- S = ( (HDMap ` K ) ` W )   &    |- G = ( (HGMap ` K ) ` W )   &    |- ( ph -> ( K e. HL /\ W e. H ) )   &    |- ( ph -> X e. V )   &    |- ( ph -> F e. B )   =>    |- ( ph -> ( S ` ( F .x. X ) ) = ( ( G ` F ) .xb ( S ` X ) ) )
Theorem	hgmapval0 35172	Value of the scalar sigma map at zero. (Contributed by NM, 12-Jun-2015.)
|- H = ( LHyp ` K )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- R = (Scalar ` U )   &    |- .0. = ( 0g ` R )   &    |- G = ( (HGMap ` K ) ` W )   &    |- ( ph -> ( K e. HL /\ W e. H ) )   =>    |- ( ph -> ( G ` .0. ) = .0. )
Theorem	hgmapval1 35173	Value of the scalar sigma map at one. (Contributed by NM, 12-Jun-2015.)
|- H = ( LHyp ` K )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- R = (Scalar ` U )   &    |- .1. = ( 1r ` R )   &    |- G = ( (HGMap ` K ) ` W )   &    |- ( ph -> ( K e. HL /\ W e. H ) )   =>    |- ( ph -> ( G ` .1. ) = .1. )
Theorem	hgmapadd 35174	Part 15 of [Baer] p. 50 line 13. (Contributed by NM, 6-Jun-2015.)
|- H = ( LHyp ` K )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- R = (Scalar ` U )   &    |- B = ( Base ` R )   &    |- .+ = ( +g ` R )   &    |- G = ( (HGMap ` K ) ` W )   &    |- ( ph -> ( K e. HL /\ W e. H ) )   &    |- ( ph -> X e. B )   &    |- ( ph -> Y e. B )   =>    |- ( ph -> ( G ` ( X .+ Y ) ) = ( ( G ` X ) .+ ( G ` Y ) ) )
Theorem	hgmapmul 35175	Part 15 of [Baer] p. 50 line 16. The multiplication is reversed after converting to the dual space scalar to the vector space scalar. (Contributed by NM, 7-Jun-2015.)
|- H = ( LHyp ` K )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- R = (Scalar ` U )   &    |- B = ( Base ` R )   &    |- .x. = ( .r ` R )   &    |- G = ( (HGMap ` K ) ` W )   &    |- ( ph -> ( K e. HL /\ W e. H ) )   &    |- ( ph -> X e. B )   &    |- ( ph -> Y e. B )   =>    |- ( ph -> ( G ` ( X .x. Y ) ) = ( ( G ` Y ) .x. ( G ` X ) ) )
Theorem	hgmaprnlem1N 35176	Lemma for hgmaprnN 35181. (Contributed by NM, 7-Jun-2015.) (New usage is discouraged.)
|- H = ( LHyp ` K )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- V = ( Base ` U )   &    |- R = (Scalar ` U )   &    |- B = ( Base ` R )   &    |- .x. = ( .s ` U )   &    |- .0. = ( 0g ` U )   &    |- C = ( (LCDual ` K ) ` W )   &    |- D = ( Base ` C )   &    |- P = (Scalar ` C )   &    |- A = ( Base ` P )   &    |- .xb = ( .s ` C )   &    |- Q = ( 0g ` C )   &    |- S = ( (HDMap ` K ) ` W )   &    |- G = ( (HGMap ` K ) ` W )   &    |- ( ph -> ( K e. HL /\ W e. H ) )   &    |- ( ph -> z e. A )   &    |- ( ph -> t e. ( V \ { .0. } ) )   &    |- ( ph -> s e. V )   &    |- ( ph -> ( S ` s ) = ( z .xb ( S ` t ) ) )   &    |- ( ph -> k e. B )   &    |- ( ph -> s = ( k .x. t ) )   =>    |- ( ph -> z e. ran G )
Theorem	hgmaprnlem2N 35177	Lemma for hgmaprnN 35181. Part 15 of [Baer] p. 50 line 20. We only require a subset relation, rather than equality, so that the case of zero z is taken care of automatically. (Contributed by NM, 7-Jun-2015.) (New usage is discouraged.)
|- H = ( LHyp ` K )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- V = ( Base ` U )   &    |- R = (Scalar ` U )   &    |- B = ( Base ` R )   &    |- .x. = ( .s ` U )   &    |- .0. = ( 0g ` U )   &    |- C = ( (LCDual ` K ) ` W )   &    |- D = ( Base ` C )   &    |- P = (Scalar ` C )   &    |- A = ( Base ` P )   &    |- .xb = ( .s ` C )   &    |- Q = ( 0g ` C )   &    |- S = ( (HDMap ` K ) ` W )   &    |- G = ( (HGMap ` K ) ` W )   &    |- ( ph -> ( K e. HL /\ W e. H ) )   &    |- ( ph -> z e. A )   &    |- ( ph -> t e. ( V \ { .0. } ) )   &    |- ( ph -> s e. V )   &    |- ( ph -> ( S ` s ) = ( z .xb ( S ` t ) ) )   &    |- M = ( (mapd ` K ) ` W )   &    |- N = ( LSpan ` U )   &    |- L = ( LSpan ` C )   =>    |- ( ph -> ( N ` { s } ) C_ ( N ` { t } ) )
Theorem	hgmaprnlem3N 35178*	Lemma for hgmaprnN 35181. Eliminate k. (Contributed by NM, 7-Jun-2015.) (New usage is discouraged.)
|- H = ( LHyp ` K )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- V = ( Base ` U )   &    |- R = (Scalar ` U )   &    |- B = ( Base ` R )   &    |- .x. = ( .s ` U )   &    |- .0. = ( 0g ` U )   &    |- C = ( (LCDual ` K ) ` W )   &    |- D = ( Base ` C )   &    |- P = (Scalar ` C )   &    |- A = ( Base ` P )   &    |- .xb = ( .s ` C )   &    |- Q = ( 0g ` C )   &    |- S = ( (HDMap ` K ) ` W )   &    |- G = ( (HGMap ` K ) ` W )   &    |- ( ph -> ( K e. HL /\ W e. H ) )   &    |- ( ph -> z e. A )   &    |- ( ph -> t e. ( V \ { .0. } ) )   &    |- ( ph -> s e. V )   &    |- ( ph -> ( S ` s ) = ( z .xb ( S ` t ) ) )   &    |- M = ( (mapd ` K ) ` W )   &    |- N = ( LSpan ` U )   &    |- L = ( LSpan ` C )   =>    |- ( ph -> z e. ran G )
Theorem	hgmaprnlem4N 35179*	Lemma for hgmaprnN 35181. Eliminate s. (Contributed by NM, 7-Jun-2015.) (New usage is discouraged.)
|- H = ( LHyp ` K )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- V = ( Base ` U )   &    |- R = (Scalar ` U )   &    |- B = ( Base ` R )   &    |- .x. = ( .s ` U )   &    |- .0. = ( 0g ` U )   &    |- C = ( (LCDual ` K ) ` W )   &    |- D = ( Base ` C )   &    |- P = (Scalar ` C )   &    |- A = ( Base ` P )   &    |- .xb = ( .s ` C )   &    |- Q = ( 0g ` C )   &    |- S = ( (HDMap ` K ) ` W )   &    |- G = ( (HGMap ` K ) ` W )   &    |- ( ph -> ( K e. HL /\ W e. H ) )   &    |- ( ph -> z e. A )   &    |- ( ph -> t e. ( V \ { .0. } ) )   =>    |- ( ph -> z e. ran G )
Theorem	hgmaprnlem5N 35180	Lemma for hgmaprnN 35181. Eliminate t. (Contributed by NM, 7-Jun-2015.) (New usage is discouraged.)
|- H = ( LHyp ` K )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- V = ( Base ` U )   &    |- R = (Scalar ` U )   &    |- B = ( Base ` R )   &    |- .x. = ( .s ` U )   &    |- .0. = ( 0g ` U )   &    |- C = ( (LCDual ` K ) ` W )   &    |- D = ( Base ` C )   &    |- P = (Scalar ` C )   &    |- A = ( Base ` P )   &    |- .xb = ( .s ` C )   &    |- Q = ( 0g ` C )   &    |- S = ( (HDMap ` K ) ` W )   &    |- G = ( (HGMap ` K ) ` W )   &    |- ( ph -> ( K e. HL /\ W e. H ) )   &    |- ( ph -> z e. A )   =>    |- ( ph -> z e. ran G )
Theorem	hgmaprnN 35181	Part of proof of part 16 in [Baer] p. 50 line 23, Fs=G, except that we use the original vector space scalars for the range. (Contributed by NM, 7-Jun-2015.) (New usage is discouraged.)
|- H = ( LHyp ` K )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- R = (Scalar ` U )   &    |- B = ( Base ` R )   &    |- G = ( (HGMap ` K ) ` W )   &    |- ( ph -> ( K e. HL /\ W e. H ) )   =>    |- ( ph -> ran G = B )
Theorem	hgmap11 35182	The scalar sigma map is one-to-one. (Contributed by NM, 7-Jun-2015.)
|- H = ( LHyp ` K )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- R = (Scalar ` U )   &    |- B = ( Base ` R )   &    |- G = ( (HGMap ` K ) ` W )   &    |- ( ph -> ( K e. HL /\ W e. H ) )   &    |- ( ph -> X e. B )   &    |- ( ph -> Y e. B )   =>    |- ( ph -> ( ( G ` X ) = ( G ` Y ) <-> X = Y ) )
Theorem	hgmapf1oN 35183	The scalar sigma map is a one-to-one onto function. (Contributed by NM, 7-Jun-2015.) (New usage is discouraged.)
|- H = ( LHyp ` K )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- R = (Scalar ` U )   &    |- B = ( Base ` R )   &    |- G = ( (HGMap ` K ) ` W )   &    |- ( ph -> ( K e. HL /\ W e. H ) )   =>    |- ( ph -> G : B -1-1-onto-> B )
Theorem	hgmapeq0 35184	The scalar sigma map is zero iff its argument is zero. (Contributed by NM, 12-Jun-2015.)
|- H = ( LHyp ` K )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- R = (Scalar ` U )   &    |- B = ( Base ` R )   &    |- .0. = ( 0g ` R )   &    |- G = ( (HGMap ` K ) ` W )   &    |- ( ph -> ( K e. HL /\ W e. H ) )   &    |- ( ph -> X e. B )   =>    |- ( ph -> ( ( G ` X ) = .0. <-> X = .0. ) )
Theorem	hdmapipcl 35185	The inner product (Hermitian form) ( X , Y ) will be defined as ( ( S ` Y ) ` X ). Show closure. (Contributed by NM, 7-Jun-2015.)
|- H = ( LHyp ` K )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- V = ( Base ` U )   &    |- R = (Scalar ` U )   &    |- B = ( Base ` R )   &    |- S = ( (HDMap ` K ) ` W )   &    |- ( ph -> ( K e. HL /\