P. 356 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 35501-35600   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	hdmaprnlem10N 35501*	Lemma for hdmaprnN 35506. 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 35502*	Lemma for hdmaprnN 35506. 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 35503*	Lemma for hdmaprnN 35506. 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 35504	Lemma for hdmaprnN 35506. 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 35505	Lemma for hdmaprnN 35506. 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 35506	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 35507	Part 12 in [Baer] p. 49. The map from vectors to functionals with closed kernels maps one-to-one onto. Combined with hdmapadd 35485, 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 35508	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 35509*	Prior to part 14 in [Baer] p. 49, line 25. TODO: fix to include F = .0. so it can be used in hdmap14lem10 35519. (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 35510	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 35511*	Prior to part 14 in [Baer] p. 49, line 25. TODO: fix to include F = Z so it can be used in hdmap14lem10 35519. (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 35512*	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 35513*	Simplify ( A \ { Q } ) in hdmap14lem3 35512 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 35514*	Simplify ( A \ { Q } ) in hdmap14lem3 35512 to provide a slightly simpler definition later. TODO: Use hdmap14lem4a 35513 if that one is also used directly elsewhere. Otherwise, merge hdmap14lem4a 35513 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 35515*	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 35516*	Combine cases of F. TODO: Can this be done at once in hdmap14lem3 35512, in order to get rid of hdmap14lem6 35515? Perhaps modify lspsneu 18424 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 35517	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 35518	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 35519	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 35520	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 35521*	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 35522*	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 35523*	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 35524*	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 35525	Extend class notation with g-map.
class HGMap
Definition	df-hgmap 35526*	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 35527*	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 35528*	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 35529*	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 35524. (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 35530	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 35531	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 35532	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 35533	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 35534	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 35535	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 35536	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 35537	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 35538	Lemma for hgmaprnN 35543. (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 35539	Lemma for hgmaprnN 35543. 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 35540*	Lemma for hgmaprnN 35543. 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 35541*	Lemma for hgmaprnN 35543. 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 35542	Lemma for hgmaprnN 35543. 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 35543	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 35544	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 35545	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 35546	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 35547	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 35548	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 35549	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 35550	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 35551	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 35552	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 35553	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 35554	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 35555	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 35556	Membership in the kernel (as shown by hdmaplkr 35555) 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 35557	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 35558	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 35559	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 35560	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 35478. 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 35561	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 35562	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 35563	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 35478. 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 35564	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 35565	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 35566	Lemma for hgmapvv 35568. 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 35567	Lemma for hgmapvv 35568. 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 35568	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 35569*	Lemma for hdmapg 35572. (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 35570	Lemma for hdmapg 35572. (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 35571	Lemma for hdmapg 35572. 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 35572	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 35573*	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 35574	Extend class notation with the final constructed Hilbert space.
class HLHil
Definition	df-hlhil 35575*	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 35576*	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 35577	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 35578	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 35579	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 35580	Lemma for hlhilsbase2 35584. (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 35581	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 35582	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 35583	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 35584	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 35585	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 35586	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 35587	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 35588	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 35589	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 35590*	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 35591	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 35592	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 35593	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 35594	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 )
Theorem	hlhilsrnglem 35595	Lemma for hlhilsrng 35596. (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 ) )   &    |- R = (Scalar ` U )   &    |- L = ( ( DVecH ` K ) ` W )   &    |- S = (Scalar ` L )   &    |- B = ( Base ` S )   &    |- .+ = ( +g ` S )   &    |- .x. = ( .r ` S )   &    |- G = ( (HGMap ` K ) ` W )   =>    |- ( ph -> R e. *Ring )
Theorem	hlhilsrng 35596	The star division ring for the final constructed Hilbert space is a division ring. (Contributed by NM, 21-Jun-2015.)
|- H = ( LHyp ` K )   &    |- U = ( (HLHil ` K ) ` W )   &    |- ( ph -> ( K e. HL /\ W e. H ) )   &    |- R = (Scalar ` U )   =>    |- ( ph -> R e. *Ring )
Theorem	hlhil0 35597	The zero vector 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 )   &    |- U = ( (HLHil ` K ) ` W )   &    |- ( ph -> ( K e. HL /\ W e. H ) )   &    |- .0. = ( 0g ` L )   =>    |- ( ph -> .0. = ( 0g ` U ) )
Theorem	hlhillsm 35598	The vector sum operation for the final constructed Hilbert space. (Contributed by NM, 23-Jun-2015.) (Revised by Mario Carneiro, 29-Jun-2015.)
|- H = ( LHyp ` K )   &    |- L = ( ( DVecH ` K ) ` W )   &    |- U = ( (HLHil ` K ) ` W )   &    |- ( ph -> ( K e. HL /\ W e. H ) )   &    |- .(+) = ( LSSum ` L )   =>    |- ( ph -> .(+) = ( LSSum ` U ) )
Theorem	hlhilocv 35599	The orthocomplement for the final constructed Hilbert space. (Contributed by NM, 23-Jun-2015.) (Revised by Mario Carneiro, 29-Jun-2015.)
|- H = ( LHyp ` K )   &    |- L = ( ( DVecH ` K ) ` W )   &    |- U = ( (HLHil ` K ) ` W )   &    |- ( ph -> ( K e. HL /\ W e. H ) )   &    |- V = ( Base ` L )   &    |- N = ( ( ocH ` K ) ` W )   &    |- O = ( ocv ` U )   &    |- ( ph -> X C_ V )   =>    |- ( ph -> ( O ` X ) = ( N ` X ) )
Theorem	hlhillcs 35600	The closed subspaces of the final constructed Hilbert space. TODO: hlhilbase 35578 is applied over and over to conclusion rather than applied once to antecedent - would compressed proof be shorter if applied once to antecedent? (Contributed by NM, 23-Jun-2015.)
|- H = ( LHyp ` K )   &    |- I = ( ( DIsoH ` K ) ` W )   &    |- U = ( (HLHil ` K ) ` W )   &    |- C = ( CSubSp ` U )   &    |- ( ph -> ( K e. HL /\ W e. H ) )   =>    |- ( ph -> C = ran I )