P. 355 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 35401-35500   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	hdmaprnlem7N 35401	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 35402	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 35403	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 35182 and mapdcnv11N 35202. 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 35404*	Lemma for hdmaprnN 35410. (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 35405*	Lemma for hdmaprnN 35410. 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 35406*	Lemma for hdmaprnN 35410. 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 35407*	Lemma for hdmaprnN 35410. 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 35408	Lemma for hdmaprnN 35410. 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 35409	Lemma for hdmaprnN 35410. 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 35410	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 35411	Part 12 in [Baer] p. 49. The map from vectors to functionals with closed kernels maps one-to-one onto. Combined with hdmapadd 35389, 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 35412	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 35413*	Prior to part 14 in [Baer] p. 49, line 25. TODO: fix to include F = .0. so it can be used in hdmap14lem10 35423. (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 35414	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 35415*	Prior to part 14 in [Baer] p. 49, line 25. TODO: fix to include F = Z so it can be used in hdmap14lem10 35423. (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 35416*	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 35417*	Simplify ( A \ { Q } ) in hdmap14lem3 35416 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 35418*	Simplify ( A \ { Q } ) in hdmap14lem3 35416 to provide a slightly simpler definition later. TODO: Use hdmap14lem4a 35417 if that one is also used directly elsewhere. Otherwise, merge hdmap14lem4a 35417 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 35419*	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 35420*	Combine cases of F. TODO: Can this be done at once in hdmap14lem3 35416, in order to get rid of hdmap14lem6 35419? Perhaps modify lspsneu 18351 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 35421	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 35422	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 35423	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 35424	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 35425*	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 35426*	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 35427*	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 35428*	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 35429	Extend class notation with g-map.
class HGMap
Definition	df-hgmap 35430*	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 35431*	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 35432*	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 35433*	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 35428. (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 35434	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 35435	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 35436	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 35437	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 35438	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 35439	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 35440	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 35441	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 35442	Lemma for hgmaprnN 35447. (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 35443	Lemma for hgmaprnN 35447. 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 35444*	Lemma for hgmaprnN 35447. 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 35445*	Lemma for hgmaprnN 35447. 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 35446	Lemma for hgmaprnN 35447. 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 35447	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 35448	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 35449	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 35450	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 35451	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 /\ W e. H ) )   &    |- ( ph -> X e. V )   &    |- ( ph -> Y e. V )   =>    |- ( ph -> ( ( S ` Y ) ` X ) e. B )
Theorem	hdmapln1 35452	Linearity property that will be used for inner product. TODO: try to combine hypotheses in hdmap*ln* series. (Contributed by NM, 7-Jun-2015.)
|- H = ( LHyp ` K )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- V = ( Base ` U )   &    |- .+ = ( +g ` U )   &    |- .x. = ( .s ` U )   &    |- R = (Scalar ` U )   &    |- B = ( Base ` R )   &    |- .+^ = ( +g ` R )   &    |- .X. = ( .r ` R )   &    |- S = ( (HDMap ` K ) ` W )   &    |- ( ph -> ( K e. HL /\ W e. H ) )   &    |- ( ph -> X e. V )   &    |- ( ph -> Y e. V )   &    |- ( ph -> Z e. V )   &    |- ( ph -> A e. B )   =>    |- ( ph -> ( ( S ` Z ) ` ( ( A .x. X ) .+ Y ) ) = ( ( A .X. ( ( S ` Z ) ` X ) ) .+^ ( ( S ` Z ) ` Y ) ) )
Theorem	hdmaplna1 35453	Additive property of first (inner product) argument. (Contributed by NM, 11-Jun-2015.)
|- H = ( LHyp ` K )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- V = ( Base ` U )   &    |- .+ = ( +g ` U )   &    |- R = (Scalar ` U )   &    |- .+^ = ( +g ` R )   &    |- S = ( (HDMap ` K ) ` W )   &    |- ( ph -> ( K e. HL /\ W e. H ) )   &    |- ( ph -> X e. V )   &    |- ( ph -> Y e. V )   &    |- ( ph -> Z e. V )   =>    |- ( ph -> ( ( S ` Z ) ` ( X .+ Y ) ) = ( ( ( S ` Z ) ` X ) .+^ ( ( S ` Z ) ` Y ) ) )
Theorem	hdmaplns1 35454	Subtraction property of first (inner product) argument. (Contributed by NM, 12-Jun-2015.)
|- H = ( LHyp ` K )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- V = ( Base ` U )   &    |- .- = ( -g ` U )   &    |- R = (Scalar ` U )   &    |- N = ( -g ` R )   &    |- S = ( (HDMap ` K ) ` W )   &    |- ( ph -> ( K e. HL /\ W e. H ) )   &    |- ( ph -> X e. V )   &    |- ( ph -> Y e. V )   &    |- ( ph -> Z e. V )   =>    |- ( ph -> ( ( S ` Z ) ` ( X .- Y ) ) = ( ( ( S ` Z ) ` X ) N ( ( S ` Z ) ` Y ) ) )
Theorem	hdmaplnm1 35455	Multiplicative property of first (inner product) argument. (Contributed by NM, 11-Jun-2015.)
|- H = ( LHyp ` K )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- V = ( Base ` U )   &    |- .x. = ( .s ` U )   &    |- R = (Scalar ` U )   &    |- B = ( Base ` R )   &    |- .X. = ( .r ` R )   &    |- S = ( (HDMap ` K ) ` W )   &    |- ( ph -> ( K e. HL /\ W e. H ) )   &    |- ( ph -> X e. V )   &    |- ( ph -> Y e. V )   &    |- ( ph -> A e. B )   =>    |- ( ph -> ( ( S ` Y ) ` ( A .x. X ) ) = ( A .X. ( ( S ` Y ) ` X ) ) )
Theorem	hdmaplna2 35456	Additive property of second (inner product) argument. (Contributed by NM, 10-Jun-2015.)
|- H = ( LHyp ` K )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- V = ( Base ` U )   &    |- .+ = ( +g ` U )   &    |- R = (Scalar ` U )   &    |- .+^ = ( +g ` R )   &    |- S = ( (HDMap ` K ) ` W )   &    |- ( ph -> ( K e. HL /\ W e. H ) )   &    |- ( ph -> X e. V )   &    |- ( ph -> Y e. V )   &    |- ( ph -> Z e. V )   =>    |- ( ph -> ( ( S ` ( Y .+ Z ) ) ` X ) = ( ( ( S ` Y ) ` X ) .+^ ( ( S ` Z ) ` X ) ) )
Theorem	hdmapglnm2 35457	g-linear property of second (inner product) argument. Line 19 in [Holland95] p. 14. (Contributed by NM, 10-Jun-2015.)
|- H = ( LHyp ` K )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- V = ( Base ` U )   &    |- .x. = ( .s ` U )   &    |- R = (Scalar ` U )   &    |- B = ( Base ` R )   &    |- .X. = ( .r ` R )   &    |- S = ( (HDMap ` K ) ` W )   &    |- G = ( (HGMap ` K ) ` W )   &    |- ( ph -> ( K e. HL /\ W e. H ) )   &    |- ( ph -> X e. V )   &    |- ( ph -> Y e. V )   &    |- ( ph -> A e. B )   =>    |- ( ph -> ( ( S ` ( A .x. Y ) ) ` X ) = ( ( ( S ` Y ) ` X ) .X. ( G ` A ) ) )
Theorem	hdmapgln2 35458	g-linear property that will be used for inner product. (Contributed by NM, 14-Jun-2015.)
|- H = ( LHyp ` K )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- V = ( Base ` U )   &    |- .+ = ( +g ` U )   &    |- .x. = ( .s ` U )   &    |- R = (Scalar ` U )   &    |- B = ( Base ` R )   &    |- .+^ = ( +g ` R )   &    |- .X. = ( .r ` R )   &    |- S = ( (HDMap ` K ) ` W )   &    |- G = ( (HGMap ` K ) ` W )   &    |- ( ph -> ( K e. HL /\ W e. H ) )   &    |- ( ph -> X e. V )   &    |- ( ph -> Y e. V )   &    |- ( ph -> Z e. V )   &    |- ( ph -> A e. B )   =>    |- ( ph -> ( ( S ` ( ( A .x. Y ) .+ Z ) ) ` X ) = ( ( ( ( S ` Y ) ` X ) .X. ( G ` A ) ) .+^ ( ( S ` Z ) ` X ) ) )
Theorem	hdmaplkr 35459	Kernel of the vector to dual map. Line 16 in [Holland95] p. 14. TODO: eliminate F hypothesis. (Contributed by NM, 9-Jun-2015.)
|- H = ( LHyp ` K )   &    |- O = ( ( ocH ` K ) ` W )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- V = ( Base ` U )   &    |- F = (LFnl ` U )   &    |- Y = (LKer ` U )   &    |- S = ( (HDMap ` K ) ` W )   &    |- ( ph -> ( K e. HL /\ W e. H ) )   &    |- ( ph -> X e. V )   =>    |- ( ph -> ( Y ` ( S ` X ) ) = ( O ` { X } ) )
Theorem	hdmapellkr 35460	Membership in the kernel (as shown by hdmaplkr 35459) of the vector to dual map. Line 17 in [Holland95] p. 14. (Contributed by NM, 16-Jun-2015.)
|- H = ( LHyp ` K )   &    |- O = ( ( ocH ` K ) ` W )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- V = ( Base ` U )   &    |- R = (Scalar ` U )   &    |- .0. = ( 0g ` R )   &    |- S = ( (HDMap ` K ) ` W )   &    |- ( ph -> ( K e. HL /\ W e. H ) )   &    |- ( ph -> X e. V )   &    |- ( ph -> Y e. V )   =>    |- ( ph -> ( ( ( S ` X ) ` Y ) = .0. <-> Y e. ( O ` { X } ) ) )
Theorem	hdmapip0 35461	Zero property that will be used for inner product. (Contributed by NM, 9-Jun-2015.)
|- H = ( LHyp ` K )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- V = ( Base ` U )   &    |- .0. = ( 0g ` U )   &    |- R = (Scalar ` U )   &    |- Z = ( 0g ` R )   &    |- S = ( (HDMap ` K ) ` W )   &    |- ( ph -> ( K e. HL /\ W e. H ) )   &    |- ( ph -> X e. V )   =>    |- ( ph -> ( ( ( S ` X ) ` X ) = Z <-> X = .0. ) )
Theorem	hdmapip1 35462	Construct a proportional vector Y whose inner product with the original X equals one. (Contributed by NM, 13-Jun-2015.)
|- H = ( LHyp ` K )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- V = ( Base ` U )   &    |- .x. = ( .s ` U )   &    |- .0. = ( 0g ` U )   &    |- R = (Scalar ` U )   &    |- .1. = ( 1r ` R )   &    |- N = ( invr ` R )   &    |- S = ( (HDMap ` K ) ` W )   &    |- ( ph -> ( K e. HL /\ W e. H ) )   &    |- ( ph -> X e. ( V \ { .0. } ) )   &    |- Y = ( ( N ` ( ( S ` X ) ` X ) ) .x. X )   =>    |- ( ph -> ( ( S ` X ) ` Y ) = .1. )
Theorem	hdmapip0com 35463	Commutation property of Baer's sigma map (Holland's A map). Line 20 of [Holland95] p. 14. Also part of Lemma 1 of [Baer] p. 110 line 7. (Contributed by NM, 9-Jun-2015.)
|- H = ( LHyp ` K )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- V = ( Base ` U )   &    |- R = (Scalar ` U )   &    |- .0. = ( 0g ` R )   &    |- S = ( (HDMap ` K ) ` W )   &    |- ( ph -> ( K e. HL /\ W e. H ) )   &    |- ( ph -> X e. V )   &    |- ( ph -> Y e. V )   =>    |- ( ph -> ( ( ( S ` X ) ` Y ) = .0. <-> ( ( S ` Y ) ` X ) = .0. ) )
Theorem	hdmapinvlem1 35464	Line 27 in [Baer] p. 110. We use C for Baer's u. Our unit vector E has the required properties for his w by hdmapevec2 35382. Our ( ( S ` E ) ` C ) means the inner product <. C , E >. i.e. his f(u,w) (note argument reversal). (Contributed by NM, 11-Jun-2015.)
|- H = ( LHyp ` K )   &    |- E = <. ( _I |` ( Base ` K ) ) , ( _I |` ( ( LTrn ` K ) ` W ) ) >.   &    |- O = ( ( ocH ` K ) ` W )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- V = ( Base ` U )   &    |- R = (Scalar ` U )   &    |- B = ( Base ` R )   &    |- .x. = ( .r ` R )   &    |- .0. = ( 0g ` R )   &    |- S = ( (HDMap ` K ) ` W )   &    |- ( ph -> ( K e. HL /\ W e. H ) )   &    |- ( ph -> C e. ( O ` { E } ) )   =>    |- ( ph -> ( ( S ` E ) ` C ) = .0. )
Theorem	hdmapinvlem2 35465	Line 28 in [Baer] p. 110, 0 = f(w,u). (Contributed by NM, 11-Jun-2015.)
|- H = ( LHyp ` K )   &    |- E = <. ( _I |` ( Base ` K ) ) , ( _I |` ( ( LTrn ` K ) ` W ) ) >.   &    |- O = ( ( ocH ` K ) ` W )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- V = ( Base ` U )   &    |- R = (Scalar ` U )   &    |- B = ( Base ` R )   &    |- .x. = ( .r ` R )   &    |- .0. = ( 0g ` R )   &    |- S = ( (HDMap ` K ) ` W )   &    |- ( ph -> ( K e. HL /\ W e. H ) )   &    |- ( ph -> C e. ( O ` { E } ) )   =>    |- ( ph -> ( ( S ` C ) ` E ) = .0. )
Theorem	hdmapinvlem3 35466	Line 30 in [Baer] p. 110, f(sw + u, tw - v) = 0. (Contributed by NM, 12-Jun-2015.)
|- H = ( LHyp ` K )   &    |- E = <. ( _I |` ( Base ` K ) ) , ( _I |` ( ( LTrn ` K ) ` W ) ) >.   &    |- O = ( ( ocH ` K ) ` W )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- V = ( Base ` U )   &    |- .+ = ( +g ` U )   &    |- .- = ( -g ` U )   &    |- .x. = ( .s ` U )   &    |- R = (Scalar ` U )   &    |- B = ( Base ` R )   &    |- .X. = ( .r ` R )   &    |- .0. = ( 0g ` R )   &    |- S = ( (HDMap ` K ) ` W )   &    |- G = ( (HGMap ` K ) ` W )   &    |- ( ph -> ( K e. HL /\ W e. H ) )   &    |- ( ph -> C e. ( O ` { E } ) )   &    |- ( ph -> D e. ( O ` { E } ) )   &    |- ( ph -> I e. B )   &    |- ( ph -> J e. B )   &    |- ( ph -> ( I .X. ( G ` J ) ) = ( ( S ` D ) ` C ) )   =>    |- ( ph -> ( ( S ` ( ( J .x. E ) .- D ) ) ` ( ( I .x. E ) .+ C ) ) = .0. )
Theorem	hdmapinvlem4 35467	Part 1.1 of Proposition 1 of [Baer] p. 110. We use C, D, I, and J for Baer's u, v, s, and t. Our unit vector E has the required properties for his w by hdmapevec2 35382. Our ( ( S ` D ) ` C ) means his f(u,v) (note argument reversal). (Contributed by NM, 12-Jun-2015.)
|- H = ( LHyp ` K )   &    |- E = <. ( _I |` ( Base ` K ) ) , ( _I |` ( ( LTrn ` K ) ` W ) ) >.   &    |- O = ( ( ocH ` K ) ` W )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- V = ( Base ` U )   &    |- .+ = ( +g ` U )   &    |- .- = ( -g ` U )   &    |- .x. = ( .s ` U )   &    |- R = (Scalar ` U )   &    |- B = ( Base ` R )   &    |- .X. = ( .r ` R )   &    |- .0. = ( 0g ` R )   &    |- S = ( (HDMap ` K ) ` W )   &    |- G = ( (HGMap ` K ) ` W )   &    |- ( ph -> ( K e. HL /\ W e. H ) )   &    |- ( ph -> C e. ( O ` { E } ) )   &    |- ( ph -> D e. ( O ` { E } ) )   &    |- ( ph -> I e. B )   &    |- ( ph -> J e. B )   &    |- ( ph -> ( I .X. ( G ` J ) ) = ( ( S ` D ) ` C ) )   =>    |- ( ph -> ( J .X. ( G ` I ) ) = ( ( S ` C ) ` D ) )
Theorem	hdmapglem5 35468	Part 1.2 in [Baer] p. 110 line 34, f(u,v) alpha = f(v,u). (Contributed by NM, 12-Jun-2015.)
|- H = ( LHyp ` K )   &    |- E = <. ( _I |` ( Base ` K ) ) , ( _I |` ( ( LTrn ` K ) ` W ) ) >.   &    |- O = ( ( ocH ` K ) ` W )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- V = ( Base ` U )   &    |- .+ = ( +g ` U )   &    |- .- = ( -g ` U )   &    |- .x. = ( .s ` U )   &    |- R = (Scalar ` U )   &    |- B = ( Base ` R )   &    |- .X. = ( .r ` R )   &    |- .0. = ( 0g ` R )   &    |- S = ( (HDMap ` K ) ` W )   &    |- G = ( (HGMap ` K ) ` W )   &    |- ( ph -> ( K e. HL /\ W e. H ) )   &    |- ( ph -> C e. ( O ` { E } ) )   &    |- ( ph -> D e. ( O ` { E } ) )   &    |- ( ph -> I e. B )   &    |- ( ph -> J e. B )   =>    |- ( ph -> ( G ` ( ( S ` D ) ` C ) ) = ( ( S ` C ) ` D ) )
Theorem	hgmapvvlem1 35469	Involution property of scalar sigma map. Line 10 in [Baer] p. 111, t sigma squared = t. Our E, C, D, Y, X correspond to Baer's w, h, k, s, t. (Contributed by NM, 13-Jun-2015.)
|- H = ( LHyp ` K )   &    |- E = <. ( _I |` ( Base ` K ) ) , ( _I |` ( ( LTrn ` K ) ` W ) ) >.   &    |- O = ( ( ocH ` K ) ` W )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- V = ( Base ` U )   &    |- .x. = ( .s ` U )   &    |- R = (Scalar ` U )   &    |- B = ( Base ` R )   &    |- .X. = ( .r ` R )   &    |- .0. = ( 0g ` R )   &    |- .1. = ( 1r ` R )   &    |- N = ( invr ` R )   &    |- S = ( (HDMap ` K ) ` W )   &    |- G = ( (HGMap ` K ) ` W )   &    |- ( ph -> ( K e. HL /\ W e. H ) )   &    |- ( ph -> X e. ( B \ { .0. } ) )   &    |- ( ph -> C e. ( O ` { E } ) )   &    |- ( ph -> D e. ( O ` { E } ) )   &    |- ( ph -> ( ( S ` D ) ` C ) = .1. )   &    |- ( ph -> Y e. ( B \ { .0. } ) )   &    |- ( ph -> ( Y .X. ( G ` X ) ) = .1. )   =>    |- ( ph -> ( G ` ( G ` X ) ) = X )
Theorem	hgmapvvlem2 35470	Lemma for hgmapvv 35472. Eliminate Y (Baer's s). (Contributed by NM, 13-Jun-2015.)
|- H = ( LHyp ` K )   &    |- E = <. ( _I |` ( Base ` K ) ) , ( _I |` ( ( LTrn ` K ) ` W ) ) >.   &    |- O = ( ( ocH ` K ) ` W )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- V = ( Base ` U )   &    |- .x. = ( .s ` U )   &    |- R = (Scalar ` U )   &    |- B = ( Base ` R )   &    |- .X. = ( .r ` R )   &    |- .0. = ( 0g ` R )   &    |- .1. = ( 1r ` R )   &    |- N = ( invr ` R )   &    |- S = ( (HDMap ` K ) ` W )   &    |- G = ( (HGMap ` K ) ` W )   &    |- ( ph -> ( K e. HL /\ W e. H ) )   &    |- ( ph -> X e. ( B \ { .0. } ) )   &    |- ( ph -> C e. ( O ` { E } ) )   &    |- ( ph -> D e. ( O ` { E } ) )   &    |- ( ph -> ( ( S ` D ) ` C ) = .1. )   =>    |- ( ph -> ( G ` ( G ` X ) ) = X )
Theorem	hgmapvvlem3 35471	Lemma for hgmapvv 35472. Eliminate ( ( S ` D ) ` C ) = .1. (Baer's f(h,k)=1). (Contributed by NM, 13-Jun-2015.)
|- H = ( LHyp ` K )   &    |- E = <. ( _I |` ( Base ` K ) ) , ( _I |` ( ( LTrn ` K ) ` W ) ) >.   &    |- O = ( ( ocH ` K ) ` W )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- V = ( Base ` U )   &    |- .x. = ( .s ` U )   &    |- R = (Scalar ` U )   &    |- B = ( Base ` R )   &    |- .X. = ( .r ` R )   &    |- .0. = ( 0g ` R )   &    |- .1. = ( 1r ` R )   &    |- N = ( invr ` R )   &    |- S = ( (HDMap ` K ) ` W )   &    |- G = ( (HGMap ` K ) ` W )   &    |- ( ph -> ( K e. HL /\ W e. H ) )   &    |- ( ph -> X e. ( B \ { .0. } ) )   =>    |- ( ph -> ( G ` ( G ` X ) ) = X )
Theorem	hgmapvv 35472	Value of a double involution. Part 1.2 of [Baer] p. 110 line 37. (Contributed by NM, 13-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 -> ( G ` ( G ` X ) ) = X )
Theorem	hdmapglem7a 35473*	Lemma for hdmapg 35476. (Contributed by NM, 14-Jun-2015.)
|- H = ( LHyp ` K )   &    |- E = <. ( _I |` ( Base ` K ) ) , ( _I |` ( ( LTrn ` K ) ` W ) ) >.   &    |- O = ( ( ocH ` K ) ` W )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- V = ( Base ` U )   &    |- .+ = ( +g ` U )   &    |- .x. = ( .s ` U )   &    |- R = (Scalar ` U )   &    |- B = ( Base ` R )   &    |- .(+) = ( LSSum ` U )   &    |- N = ( LSpan ` U )   &    |- ( ph -> ( K e. HL /\ W e. H ) )   &    |- ( ph -> X e. V )   =>    |- ( ph -> E. u e. ( O ` { E } ) E. k e. B X = ( ( k .x. E ) .+ u ) )
Theorem	hdmapglem7b 35474	Lemma for hdmapg 35476. (Contributed by NM, 14-Jun-2015.)
|- H = ( LHyp ` K )   &    |- E = <. ( _I |` ( Base ` K ) ) , ( _I |` ( ( LTrn ` K ) ` W ) ) >.   &    |- O = ( ( ocH ` K ) ` W )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- V = ( Base ` U )   &    |- .+ = ( +g ` U )   &    |- .x. = ( .s ` U )   &    |- R = (Scalar ` U )   &    |- B = ( Base ` R )   &    |- .(+) = ( LSSum ` U )   &    |- N = ( LSpan ` U )   &    |- ( ph -> ( K e. HL /\ W e. H ) )   &    |- ( ph -> X e. V )   &    |- .X. = ( .r ` R )   &    |- .0. = ( 0g ` R )   &    |- .+b = ( +g ` R )   &    |- S = ( (HDMap ` K ) ` W )   &    |- G = ( (HGMap ` K ) ` W )   &    |- ( ph -> x e. ( O ` { E } ) )   &    |- ( ph -> y e. ( O ` { E } ) )   &    |- ( ph -> m e. B )   &    |- ( ph -> n e. B )   =>    |- ( ph -> ( ( S ` ( ( m .x. E ) .+ x ) ) ` ( ( n .x. E ) .+ y ) ) = ( ( n .X. ( G ` m ) ) .+b ( ( S ` x ) ` y ) ) )
Theorem	hdmapglem7 35475	Lemma for hdmapg 35476. Line 15 in [Baer] p. 111, f(x,y) alpha = f(y,x). In the proof, our E, ( O ` { E } ) X, Y, k, u, l, v correspond to Baer's w, H, x, y, x', x'', y' , y'', and our ( ( S ` Y ) ` X ) corresponds to Baer's f(x,y). (Contributed by NM, 14-Jun-2015.)
|- H = ( LHyp ` K )   &    |- E = <. ( _I |` ( Base ` K ) ) , ( _I |` ( ( LTrn ` K ) ` W ) ) >.   &    |- O = ( ( ocH ` K ) ` W )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- V = ( Base ` U )   &    |- .+ = ( +g ` U )   &    |- .x. = ( .s ` U )   &    |- R = (Scalar ` U )   &    |- B = ( Base ` R )   &    |- .(+) = ( LSSum ` U )   &    |- N = ( LSpan ` U )   &    |- ( ph -> ( K e. HL /\ W e. H ) )   &    |- ( ph -> X e. V )   &    |- .X. = ( .r ` R )   &    |- .0. = ( 0g ` R )   &    |- .+b = ( +g ` R )   &    |- S = ( (HDMap ` K ) ` W )   &    |- G = ( (HGMap ` K ) ` W )   &    |- ( ph -> Y e. V )   =>    |- ( ph -> ( G ` ( ( S ` Y ) ` X ) ) = ( ( S ` X ) ` Y ) )
Theorem	hdmapg 35476	Apply the scalar sigma function (involution) G to an inner product reverses the arguments. The inner product of X and Y is represented by ( ( S ` Y ) ` X ). Line 15 in [Baer] p. 111, f(x,y) alpha = f(y,x). (Contributed by NM, 14-Jun-2015.)
|- H = ( LHyp ` K )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- V = ( Base ` U )   &    |- S = ( (HDMap ` K ) ` W )   &    |- G = ( (HGMap ` K ) ` W )   &    |- ( ph -> ( K e. HL /\ W e. H ) )   &    |- ( ph -> X e. V )   &    |- ( ph -> Y e. V )   =>    |- ( ph -> ( G ` ( ( S ` Y ) ` X ) ) = ( ( S ` X ) ` Y ) )
Theorem	hdmapoc 35477*	Express our constructed orthocomplement (polarity) in terms of the Hilbert space definition of orthocomplement. Lines 24 and 25 in [Holland95] p. 14. (Contributed by NM, 17-Jun-2015.)
|- H = ( LHyp ` K )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- V = ( Base ` U )   &    |- R = (Scalar ` U )   &    |- .0. = ( 0g ` R )   &    |- O = ( ( ocH ` K ) ` W )   &    |- S = ( (HDMap ` K ) ` W )   &    |- ( ph -> ( K e. HL /\ W e. H ) )   &    |- ( ph -> X C_ V )   =>    |- ( ph -> ( O ` X ) = { y e. V | A. z e. X ( ( S ` z ) ` y ) = .0. } )
Syntax	chlh 35478	Extend class notation with the final constructed Hilbert space.
class HLHil
Definition	df-hlhil 35479*	Define our final Hilbert space constructed from a Hilbert lattice. (Contributed by NM, 21-Jun-2015.) (Revised by Mario Carneiro, 28-Jun-2015.)
|- HLHil = ( k e. _V |-> ( w e. ( LHyp ` k ) |-> [_ ( ( DVecH ` k ) ` w ) / u ]_ [_ ( Base ` u ) / v ]_ ( { <. ( Base ` ndx ) , v >. , <. ( +g ` ndx ) , ( +g ` u ) >. , <. (Scalar ` ndx ) , ( ( ( EDRing ` k ) ` w ) sSet <. ( *r ` ndx ) , ( (HGMap ` k ) ` w ) >. ) >. } u. { <. ( .s ` ndx ) , ( .s ` u ) >. , <. ( .i ` ndx ) , ( x e. v , y e. v |-> ( ( ( (HDMap ` k ) ` w ) ` y ) ` x ) ) >. } ) ) )
Theorem	hlhilset 35480*	The final Hilbert space constructed from a Hilbert lattice K and an arbitrary hyperplane W in K. (Contributed by NM, 21-Jun-2015.) (Revised by Mario Carneiro, 28-Jun-2015.)
|- H = ( LHyp ` K )   &    |- L = ( (HLHil ` K ) ` W )   &    |- U = ( ( DVecH ` K ) ` W )   &    |- V = ( Base ` U )   &    |- .+ = ( +g ` U )   &    |- E = ( ( EDRing ` K ) ` W )   &    |- G = ( (HGMap ` K ) ` W )   &    |- R = ( E sSet <. ( *r ` ndx ) , G >. )   &    |- .x. = ( .s ` U )   &    |- S = ( (HDMap ` K ) ` W )   &    |- ., = ( x e. V , y e. V |-> ( ( S ` y ) ` x ) )   &    |- ( ph -> ( K e. HL /\ W e. H ) )   =>    |- ( ph -> L = ( { <. ( Base ` ndx ) , V >. , <. ( +g ` ndx ) , .+ >. , <. (Scalar ` ndx ) , R >. } u. { <. ( .s ` ndx ) , .x. >. , <. ( .i ` ndx ) , ., >. } ) )
Theorem	hlhilsca 35481	The scalar of the final constructed Hilbert space. (Contributed by NM, 22-Jun-2015.) (Revised by Mario Carneiro, 28-Jun-2015.)
|- H = ( LHyp ` K )   &    |- U = ( (HLHil ` K ) ` W )   &    |- ( ph -> ( K e. HL /\ W e. H ) )   &    |- E = ( ( EDRing ` K ) ` W )   &    |- G = ( (HGMap ` K ) ` W )   &    |- R = ( E sSet <. ( *r ` ndx ) , G >. )   =>    |- ( ph -> R = (Scalar ` U ) )
Theorem	hlhilbase 35482	The base set of the final constructed Hilbert space. (Contributed by NM, 21-Jun-2015.) (Revised by Mario Carneiro, 28-Jun-2015.)
|- H = ( LHyp ` K )   &    |- U = ( (HLHil ` K ) ` W )   &    |- ( ph -> ( K e. HL /\ W e. H ) )   &    |- L = ( ( DVecH ` K ) ` W )   &    |- M = ( Base ` L )   =>    |- ( ph -> M = ( Base ` U ) )
Theorem	hlhilplus 35483	The vector addition for the final constructed Hilbert space. (Contributed by NM, 21-Jun-2015.)
|- H = ( LHyp ` K )   &    |- U = ( (HLHil ` K ) ` W )   &    |- ( ph -> ( K e. HL /\ W e. H ) )   &    |- L = ( ( DVecH ` K ) ` W )   &    |- .+ = ( +g ` L )   =>    |- ( ph -> .+ = ( +g ` U ) )
Theorem	hlhilslem 35484	Lemma for hlhilsbase2 35488. (Contributed by Mario Carneiro, 28-Jun-2015.)
|- H = ( LHyp ` K )   &    |- E = ( ( EDRing ` K ) ` W )   &    |- U = ( (HLHil ` K ) ` W )   &    |- R = (Scalar ` U )   &    |- ( ph -> ( K e. HL /\ W e. H ) )   &    |- F = Slot N   &    |- N e. NN   &    |- N < 4   &    |- C = ( F ` E )   =>    |- ( ph -> C = ( F ` R ) )
Theorem	hlhilsbase 35485	The scalar base set of the final constructed Hilbert space. (Contributed by NM, 22-Jun-2015.) (Revised by Mario Carneiro, 28-Jun-2015.)
|- H = ( LHyp ` K )   &    |- E = ( ( EDRing ` K ) ` W )   &    |- U = ( (HLHil ` K ) ` W )   &    |- R = (Scalar ` U )   &    |- ( ph -> ( K e. HL /\ W e. H ) )   &    |- C = ( Base ` E )   =>    |- ( ph -> C = ( Base ` R ) )
Theorem	hlhilsplus 35486	Scalar addition for the final constructed Hilbert space. (Contributed by NM, 22-Jun-2015.) (Revised by Mario Carneiro, 28-Jun-2015.)
|- H = ( LHyp ` K )   &    |- E = ( ( EDRing ` K ) ` W )   &    |- U = ( (HLHil ` K ) ` W )   &    |- R = (Scalar ` U )   &    |- ( ph -> ( K e. HL /\ W e. H ) )   &    |- .+ = ( +g ` E )   =>    |- ( ph -> .+ = ( +g ` R ) )
Theorem	hlhilsmul 35487	Scalar multiplication for the final constructed Hilbert space. (Contributed by NM, 22-Jun-2015.) (Revised by Mario Carneiro, 28-Jun-2015.)
|- H = ( LHyp ` K )   &    |- E = ( ( EDRing ` K ) ` W )   &    |- U = ( (HLHil ` K ) ` W )   &    |- R = (Scalar ` U )   &    |- ( ph -> ( K e. HL /\ W e. H ) )   &    |- .x. = ( .r ` E )   =>    |- ( ph -> .x. = ( .r ` R ) )
Theorem	hlhilsbase2 35488	The scalar base set of the final constructed Hilbert space. (Contributed by NM, 22-Jun-2015.) (Revised by Mario Carneiro, 28-Jun-2015.)
|- H = ( LHyp ` K )   &    |- L = ( ( DVecH ` K ) ` W )   &    |- S = (Scalar ` L )   &    |- U = ( (HLHil ` K ) ` W )   &    |- R = (Scalar ` U )   &    |- ( ph -> ( K e. HL /\ W e. H ) )   &    |- C = ( Base ` S )   =>    |- ( ph -> C = ( Base ` R ) )
Theorem	hlhilsplus2 35489	Scalar addition for the final constructed Hilbert space. (Contributed by NM, 22-Jun-2015.) (Revised by Mario Carneiro, 28-Jun-2015.)
|- H = ( LHyp ` K )   &    |- L = ( ( DVecH ` K ) ` W )   &    |- S = (Scalar ` L )   &    |- U = ( (HLHil ` K ) ` W )   &    |- R = (Scalar ` U )   &    |- ( ph -> ( K e. HL /\ W e. H ) )   &    |- .+ = ( +g ` S )   =>    |- ( ph -> .+ = ( +g ` R ) )
Theorem	hlhilsmul2 35490	Scalar multiplication for the final constructed Hilbert space. (Contributed by NM, 22-Jun-2015.) (Revised by Mario Carneiro, 28-Jun-2015.)
|- H = ( LHyp ` K )   &    |- L = ( ( DVecH ` K ) ` W )   &    |- S = (Scalar ` L )   &    |- U = ( (HLHil ` K ) ` W )   &    |- R = (Scalar ` U )   &    |- ( ph -> ( K e. HL /\ W e. H ) )   &    |- .x. = ( .r ` S )   =>    |- ( ph -> .x. = ( .r ` R ) )
Theorem	hlhils0 35491	The scalar ring zero for the final constructed Hilbert space. (Contributed by NM, 22-Jun-2015.) (Revised by Mario Carneiro, 29-Jun-2015.)
|- H = ( LHyp ` K )   &    |- L = ( ( DVecH ` K ) ` W )   &    |- S = (Scalar ` L )   &    |- U = ( (HLHil ` K ) ` W )   &    |- R = (Scalar ` U )   &    |- ( ph -> ( K e. HL /\ W e. H ) )   &    |- .0. = ( 0g ` S )   =>    |- ( ph -> .0. = ( 0g ` R ) )
Theorem	hlhils1N 35492	The scalar ring unity for the final constructed Hilbert space. (Contributed by NM, 22-Jun-2015.) (Revised by Mario Carneiro, 29-Jun-2015.) (New usage is discouraged.)
|- H = ( LHyp ` K )   &    |- L = ( ( DVecH ` K ) ` W )   &    |- S = (Scalar ` L )   &    |- U = ( (HLHil ` K ) ` W )   &    |- R = (Scalar ` U )   &    |- ( ph -> ( K e. HL /\ W e. H ) )   &    |- .1. = ( 1r ` S )   =>    |- ( ph -> .1. = ( 1r ` R ) )
Theorem	hlhilvsca 35493	The scalar product for the final constructed Hilbert space. (Contributed by NM, 21-Jun-2015.) (Revised by Mario Carneiro, 28-Jun-2015.)
|- H = ( LHyp ` K )   &    |- L = ( ( DVecH ` K ) ` W )   &    |- .x. = ( .s ` L )   &    |- U = ( (HLHil ` K ) ` W )   &    |- ( ph -> ( K e. HL /\ W e. H ) )   =>    |- ( ph -> .x. = ( .s ` U ) )
Theorem	hlhilip 35494*	Inner product operation for the final constructed Hilbert space. (Contributed by NM, 22-Jun-2015.) (Revised by Mario Carneiro, 28-Jun-2015.)
|- H = ( LHyp ` K )   &    |- L = ( ( DVecH ` K ) ` W )   &    |- V = ( Base ` L )   &    |- S = ( (HDMap ` K ) ` W )   &    |- U = ( (HLHil ` K ) ` W )   &    |- ( ph -> ( K e. HL /\ W e. H ) )   &    |- ., = ( x e. V , y e. V |-> ( ( S ` y ) ` x ) )   =>    |- ( ph -> ., = ( .i ` U ) )
Theorem	hlhilipval 35495	Value of inner product operation for the final constructed Hilbert space. (Contributed by NM, 22-Jun-2015.) (Revised by Mario Carneiro, 28-Jun-2015.)
|- H = ( LHyp ` K )   &    |- L = ( ( DVecH ` K ) ` W )   &    |- V = ( Base ` L )   &    |- S = ( (HDMap ` K ) ` W )   &    |- U = ( (HLHil ` K ) ` W )   &    |- ( ph -> ( K e. HL /\ W e. H ) )   &    |- ., = ( .i ` U )   &    |- ( ph -> X e. V )   &    |- ( ph -> Y e. V )   =>    |- ( ph -> ( X ., Y ) = ( ( S ` Y ) ` X ) )
Theorem	hlhilnvl 35496	The involution operation of the star division ring for the final constructed Hilbert space. (Contributed by NM, 20-Jun-2015.) (Revised by Mario Carneiro, 28-Jun-2015.)
|- H = ( LHyp ` K )   &    |- U = ( (HLHil ` K ) ` W )   &    |- R = (Scalar ` U )   &    |- .* = ( (HGMap ` K ) ` W )   &    |- ( ph -> ( K e. HL /\ W e. H ) )   =>    |- ( ph -> .* = ( *r ` R ) )
Theorem	hlhillvec 35497	The final constructed Hilbert space is a vector space. (Contributed by NM, 22-Jun-2015.) (Revised by Mario Carneiro, 29-Jun-2015.)
|- H = ( LHyp ` K )   &    |- U = ( (HLHil ` K ) ` W )   &    |- ( ph -> ( K e. HL /\ W e. H ) )   =>    |- ( ph -> U e. LVec )
Theorem	hlhildrng 35498	The star division ring for the final constructed Hilbert space is a division ring. (Contributed by NM, 20-Jun-2015.) (Revised by Mario Carneiro, 28-Jun-2015.)
|- H = ( LHyp ` K )   &    |- U = ( (HLHil ` K ) ` W )   &    |- ( ph -> ( K e. HL /\ W e. H ) )   &    |- R = (Scalar ` U )   =>    |- ( ph -> R e. DivRing )
</