P. 350 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 34901-35000   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	hgmaprnlem3N 34901*	Lemma for hgmaprnN 34904. 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 34902*	Lemma for hgmaprnN 34904. 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 34903	Lemma for hgmaprnN 34904. 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 34904	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 34905	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 34906	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 34907	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 34908	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 34909	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 34910	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 34911	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 34912	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 34913	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 34914	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 34915	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 34916	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 34917	Membership in the kernel (as shown by hdmaplkr 34916) 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 34918	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 34919	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 34920	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 34921	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 34839. 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 34922	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 34923	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 34924	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 34839. 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 34925	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 34926	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 34927	Lemma for hgmapvv 34929. 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 34928	Lemma for hgmapvv 34929. 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 34929	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 34930*	Lemma for hdmapg 34933. (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 34931	Lemma for hdmapg 34933. (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 34932	Lemma for hdmapg 34933. 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 34933	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 34934*	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 34935	Extend class notation with the final constructed Hilbert space.
class HLHil
Definition	df-hlhil 34936*	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 34937*	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 34938	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 34939	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 34940	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 34941	Lemma for hlhilsbase2 34945. (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 34942	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 34943	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 34944	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 34945	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 34946	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 34947	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 34948	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 34949	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 34950	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 34951*	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 34952	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 34953	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 34954	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 34955	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 34956	Lemma for hlhilsrng 34957. (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 34957	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 34958	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 34959	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 34960	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 34961	The closed subspaces of the final constructed Hilbert space. TODO: hlhilbase 34939 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 )
Theorem	hlhilphllem 34962*	Lemma for hlhil 22148. (Contributed by NM, 23-Jun-2015.)
|- H = ( LHyp ` K )   &    |- U = ( (HLHil ` K ) ` W )   &    |- ( ph -> ( K e. HL /\ W e. H ) )   &    |- F = (Scalar ` U )   &    |- L = ( ( DVecH ` K ) ` W )   &    |- V = ( Base ` L )   &    |- .+ = ( +g ` L )   &    |- .x. = ( .s ` L )   &    |- R = (Scalar ` L )   &    |- B = ( Base ` R )   &    |- .+^ = ( +g ` R )   &    |- .X. = ( .r ` R )   &    |- Q = ( 0g ` R )   &    |- .0. = ( 0g ` L )   &    |- ., = ( .i ` U )   &    |- J = ( (HDMap ` K ) ` W )   &    |- G = ( (HGMap ` K ) ` W )   &    |- E = ( x e. V , y e. V |-> ( ( J ` y ) ` x ) )   =>    |- ( ph -> U e. PreHil )
Theorem	hlhilhillem 34963*	Lemma for hlhil 22148. (Contributed by NM, 23-Jun-2015.)
|- H = ( LHyp ` K )   &    |- U = ( (HLHil ` K ) ` W )   &    |- ( ph -> ( K e. HL /\ W e. H ) )   &    |- F = (Scalar ` U )   &    |- L = ( ( DVecH ` K ) ` W )   &    |- V = ( Base ` L )   &    |- .+ = ( +g ` L )   &    |- .x. = ( .s ` L )   &    |- R = (Scalar ` L )   &    |- B = ( Base ` R )   &    |- .+^ = ( +g ` R )   &    |- .X. = ( .r ` R )   &    |- Q = ( 0g ` R )   &    |- .0. = ( 0g ` L )   &    |- ., = ( .i ` U )   &    |- J = ( (HDMap ` K ) ` W )   &    |- G = ( (HGMap ` K ) ` W )   &    |- E = ( x e. V , y e. V |-> ( ( J ` y ) ` x ) )   &    |- O = ( ocv ` U )   &    |- C = ( CSubSp ` U )   =>    |- ( ph -> U e. Hil )
Theorem	hlathil 34964	Construction of a Hilbert space (df-hil 19031) U from a Hilbert lattice (df-hlat 32349) K, where W is a fixed but arbitrary hyperplane (co-atom) in K. The Hilbert space U is identical to the vector space ( ( DVecH ` K ) ` W ) (see dvhlvec 34109) except that it is extended with involution and inner product components. The construction of these two components is provided by Theorem 3.6 in [Holland95] p. 13, whose proof we follow loosely. An example of involution is the complex conjugate when the division ring is the field of complex numbers. The nature of the division ring we constructed is indeterminate, however, until we specialize the initial Hilbert lattice with additional conditions found by Maria Solèr in 1995 and refined by René Mayet in 1998 that result in a division ring isomorphic to CC. See additional discussion at http://us.metamath.org/qlegif/mmql.html#what. W corresponds to the w in the proof of Theorem 13.4 of [Crawley] p. 111. Such a W always exists since HL has lattice rank of at least 4 by df-hil 19031. It can be eliminated if we just want to show the existence of a Hilbert space, as is done in the literature. (Contributed by NM, 23-Jun-2015.)
|- H = ( LHyp ` K )   &    |- U = ( (HLHil ` K ) ` W )   &    |- ( ph -> ( K e. HL /\ W e. H ) )   =>    |- ( ph -> U e. Hil )
21.22  Mathbox for OpenAI
Theorem	rntrclfvOAI 34965	The range of the transitive closure is equal to the range of the relation. (Contributed by OpenAI, 7-Jul-2020.)
|- ( R e. V -> ran ( t+ ` R ) = ran R )
21.23  Mathbox for Stefan O'Rear
21.23.1  Additional elementary logic and set theory
Theorem	moxfr 34966*	Transfer at-most-one between related expressions. (Contributed by Stefan O'Rear, 12-Feb-2015.)
|- A e. _V   &    |- E! y x = A   &    |- ( x = A -> ( ph <-> ps ) )   =>    |- ( E* x ph <-> E* y ps )
21.23.2  Additional theory of functions
Theorem	imaiinfv 34967*	Indexed intersection of an image. (Contributed by Stefan O'Rear, 22-Feb-2015.)
|- ( ( F Fn A /\ B C_ A ) -> |^|_ x e. B ( F ` x ) = |^| ( F " B ) )
21.23.3  Additional topology
Theorem	elrfi 34968*	Elementhood in a set of relative finite intersections. (Contributed by Stefan O'Rear, 22-Feb-2015.)
|- ( ( B e. V /\ C C_ ~P B ) -> ( A e. ( fi ` ( { B } u. C ) ) <-> E. v e. ( ~P C i^i Fin ) A = ( B i^i |^| v ) ) )
Theorem	elrfirn 34969*	Elementhood in a set of relative finite intersections of an indexed family of sets. (Contributed by Stefan O'Rear, 22-Feb-2015.)
|- ( ( B e. V /\ F : I --> ~P B ) -> ( A e. ( fi ` ( { B } u. ran F ) ) <-> E. v e. ( ~P I i^i Fin ) A = ( B i^i |^|_ y e. v ( F ` y ) ) ) )
Theorem	elrfirn2 34970*	Elementhood in a set of relative finite intersections of an indexed family of sets (implicit). (Contributed by Stefan O'Rear, 22-Feb-2015.)
|- ( ( B e. V /\ A. y e. I C C_ B ) -> ( A e. ( fi ` ( { B } u. ran ( y e. I |-> C ) ) ) <-> E. v e. ( ~P I i^i Fin ) A = ( B i^i |^|_ y e. v C ) ) )
Theorem	cmpfiiin 34971*	In a compact topology, a system of closed sets with nonempty finite intersections has a nonempty intersection. (Contributed by Stefan O'Rear, 22-Feb-2015.)
|- X = U. J   &    |- ( ph -> J e. Comp )   &    |- ( ( ph /\ k e. I ) -> S e. ( Clsd ` J ) )   &    |- ( ( ph /\ ( l C_ I /\ l e. Fin ) ) -> ( X i^i |^|_ k e. l S ) =/= (/) )   =>    |- ( ph -> ( X i^i |^|_ k e. I S ) =/= (/) )
21.23.4  Characterization of closure operators. Kuratowski closure axioms
Theorem	ismrcd1 34972*	Any function from the subsets of a set to itself, which is extensive (satisfies mrcssid 15229), isotone (satisfies mrcss 15228), and idempotent (satisfies mrcidm 15231) has a collection of fixed points which is a Moore collection, and itself is the closure operator for that collection. This can be taken as an alternate definition for the closure operators. This is the first half, ismrcd2 34973 is the second. (Contributed by Stefan O'Rear, 1-Feb-2015.)
|- ( ph -> B e. V )   &    |- ( ph -> F : ~P B --> ~P B )   &    |- ( ( ph /\ x C_ B ) -> x C_ ( F ` x ) )   &    |- ( ( ph /\ x C_ B /\ y C_ x ) -> ( F ` y ) C_ ( F ` x ) )   &    |- ( ( ph /\ x C_ B ) -> ( F ` ( F ` x ) ) = ( F ` x ) )   =>    |- ( ph -> dom ( F i^i _I ) e. (Moore ` B ) )
Theorem	ismrcd2 34973*	Second half of ismrcd1 34972. (Contributed by Stefan O'Rear, 1-Feb-2015.)
|- ( ph -> B e. V )   &    |- ( ph -> F : ~P B --> ~P B )   &    |- ( ( ph /\ x C_ B ) -> x C_ ( F ` x ) )   &    |- ( ( ph /\ x C_ B /\ y C_ x ) -> ( F ` y ) C_ ( F ` x ) )   &    |- ( ( ph /\ x C_ B ) -> ( F ` ( F ` x ) ) = ( F ` x ) )   =>    |- ( ph -> F = (mrCls ` dom ( F i^i _I ) ) )
Theorem	istopclsd 34974*	A closure function which satisfies sscls 19847, clsidm 19859, cls0 19872, and clsun 30543 defines a (unique) topology which it is the closure function on. (Contributed by Stefan O'Rear, 1-Feb-2015.)
|- ( ph -> B e. V )   &    |- ( ph -> F : ~P B --> ~P B )   &    |- ( ( ph /\ x C_ B ) -> x C_ ( F ` x ) )   &    |- ( ( ph /\ x C_ B ) -> ( F ` ( F ` x ) ) = ( F ` x ) )   &    |- ( ph -> ( F ` (/) ) = (/) )   &    |- ( ( ph /\ x C_ B /\ y C_ B ) -> ( F ` ( x u. y ) ) = ( ( F ` x ) u. ( F ` y ) ) )   &    |- J = { z e. ~P B | ( F ` ( B \ z ) ) = ( B \ z ) }   =>    |- ( ph -> ( J e. (TopOn ` B ) /\ ( cls ` J ) = F ) )
Theorem	ismrc 34975*	A function is a Moore closure operator iff it satisfies mrcssid 15229, mrcss 15228, and mrcidm 15231. (Contributed by Stefan O'Rear, 1-Feb-2015.)
|- ( F e. (mrCls " (Moore ` B ) ) <-> ( B e. _V /\ F : ~P B --> ~P B /\ A. x A. y ( ( x C_ B /\ y C_ x ) -> ( x C_ ( F ` x ) /\ ( F ` y ) C_ ( F ` x ) /\ ( F ` ( F ` x ) ) = ( F ` x ) ) ) ) )
21.23.5  Algebraic closure systems
Syntax	cnacs 34976	Class of Noetherian closure systems.
class NoeACS
Definition	df-nacs 34977*	Define a closure system of Noetherian type (not standard terminology) as an algebraic system where all closed sets are finitely generated. (Contributed by Stefan O'Rear, 4-Apr-2015.)
|- NoeACS = ( x e. _V |-> { c e. (ACS ` x ) | A. s e. c E. g e. ( ~P x i^i Fin ) s = ( (mrCls ` c ) ` g ) } )
Theorem	isnacs 34978*	Expand definition of Noetherian-type closure system. (Contributed by Stefan O'Rear, 4-Apr-2015.)
|- F = (mrCls ` C )   =>    |- ( C e. (NoeACS ` X ) <-> ( C e. (ACS ` X ) /\ A. s e. C E. g e. ( ~P X i^i Fin ) s = ( F ` g ) ) )
Theorem	nacsfg 34979*	In a Noetherian-type closure system, all closed sets are finitely generated. (Contributed by Stefan O'Rear, 4-Apr-2015.)
|- F = (mrCls ` C )   =>    |- ( ( C e. (NoeACS ` X ) /\ S e. C ) -> E. g e. ( ~P X i^i Fin ) S = ( F ` g ) )
Theorem	isnacs2 34980	Express Noetherian-type closure system with fewer quantifiers. (Contributed by Stefan O'Rear, 4-Apr-2015.)
|- F = (mrCls ` C )   =>    |- ( C e. (NoeACS ` X ) <-> ( C e. (ACS ` X ) /\ ( F " ( ~P X i^i Fin ) ) = C ) )
Theorem	mrefg2 34981*	Slight variation on finite genration for closure systems. (Contributed by Stefan O'Rear, 4-Apr-2015.)
|- F = (mrCls ` C )   =>    |- ( C e. (Moore ` X ) -> ( E. g e. ( ~P X i^i Fin ) S = ( F ` g ) <-> E. g e. ( ~P S i^i Fin ) S = ( F ` g ) ) )
Theorem	mrefg3 34982*	Slight variation on finite genration for closure systems. (Contributed by Stefan O'Rear, 4-Apr-2015.)
|- F = (mrCls ` C )   =>    |- ( ( C e. (Moore ` X ) /\ S e. C ) -> ( E. g e. ( ~P X i^i Fin ) S = ( F ` g ) <-> E. g e. ( ~P S i^i Fin ) S C_ ( F ` g ) ) )
Theorem	nacsacs 34983	A closure system of Noetherian type is algebraic. (Contributed by Stefan O'Rear, 4-Apr-2015.)
|- ( C e. (NoeACS ` X ) -> C e. (ACS ` X ) )
Theorem	isnacs3 34984*	A choice-free order equivalent to the Noetherian condition on a closure system. (Contributed by Stefan O'Rear, 4-Apr-2015.)
|- ( C e. (NoeACS ` X ) <-> ( C e. (Moore ` X ) /\ A. s e. ~P C ( (toInc ` s ) e. Dirset -> U. s e. s ) ) )
Theorem	incssnn0 34985*	Transitivity induction of subsets, lemma for nacsfix 34986. (Contributed by Stefan O'Rear, 4-Apr-2015.)
|- ( ( A. x e. NN0 ( F ` x ) C_ ( F ` ( x + 1 ) ) /\ A e. NN0 /\ B e. ( ZZ>= ` A ) ) -> ( F ` A ) C_ ( F ` B ) )
Theorem	nacsfix 34986*	An increasing sequence of closed sets in a Noetherian-type closure system eventually fixates. (Contributed by Stefan O'Rear, 4-Apr-2015.)
|- ( ( C e. (NoeACS ` X ) /\ F : NN0 --> C /\ A. x e. NN0 ( F ` x ) C_ ( F ` ( x + 1 ) ) ) -> E. y e. NN0 A. z e. ( ZZ>= ` y ) ( F ` z ) = ( F ` y ) )
21.23.6  Miscellanea 1. Map utilities
Theorem	constmap 34987	A constant (represented without dummy variables) is an element of a function set. _Note: In the following development, we will be quite often quantifying over functions and points in N-dimensional space (which are equivalent to functions from an "index set"). Many of the following theorems exist to transfer standard facts about functions to elements of function sets._ (Contributed by Stefan O'Rear, 30-Aug-2014.) (Revised by Stefan O'Rear, 5-May-2015.)
|- A e. _V   &    |- C e. _V   =>    |- ( B e. C -> ( A X. { B } ) e. ( C ^m A ) )
Theorem	mapco2g 34988	Renaming indexes in a tuple, with sethood as antecedents. (Contributed by Stefan O'Rear, 9-Oct-2014.) (Revised by Mario Carneiro, 5-May-2015.)
|- ( ( E e. _V /\ A e. ( B ^m C ) /\ D : E --> C ) -> ( A o. D ) e. ( B ^m E ) )
Theorem	mapco2 34989	Post-composition (renaming indexes) of a mapping viewed as a point. (Contributed by Stefan O'Rear, 5-Oct-2014.) (Revised by Stefan O'Rear, 5-May-2015.)
|- E e. _V   =>    |- ( ( A e. ( B ^m C ) /\ D : E --> C ) -> ( A o. D ) e. ( B ^m E ) )
Theorem	mapfzcons 34990	Extending a one-based mapping by adding a tuple at the end results in another mapping. (Contributed by Stefan O'Rear, 10-Oct-2014.) (Revised by Stefan O'Rear, 5-May-2015.)
|- M = ( N + 1 )   =>    |- ( ( N e. NN0 /\ A e. ( B ^m ( 1 ... N ) ) /\ C e. B ) -> ( A u. { <. M , C >. } ) e. ( B ^m ( 1 ... M ) ) )
Theorem	mapfzcons1 34991	Recover prefix mapping from an extended mapping. (Contributed by Stefan O'Rear, 10-Oct-2014.) (Revised by Stefan O'Rear, 5-May-2015.)
|- M = ( N + 1 )   =>    |- ( A e. ( B ^m ( 1 ... N ) ) -> ( ( A u. { <. M , C >. } ) |` ( 1 ... N ) ) = A )
Theorem	mapfzcons1cl 34992	A nonempty mapping has a prefix. (Contributed by Stefan O'Rear, 10-Oct-2014.) (Revised by Stefan O'Rear, 5-May-2015.)
|- M = ( N + 1 )   =>    |- ( A e. ( B ^m ( 1 ... M ) ) -> ( A |` ( 1 ... N ) ) e. ( B ^m ( 1 ... N ) ) )
Theorem	mapfzcons2 34993	Recover added element from an extended mapping. (Contributed by Stefan O'Rear, 10-Oct-2014.) (Revised by Stefan O'Rear, 5-May-2015.)
|- M = ( N + 1 )   =>    |- ( ( A e. ( B ^m ( 1 ... N ) ) /\ C e. B ) -> ( ( A u. { <. M , C >. } ) ` M ) = C )
21.23.7  Miscellanea for polynomials
Theorem	mptfcl 34994*	Interpret range of a maps-to notation as a constraint on the definition. (Contributed by Stefan O'Rear, 10-Oct-2014.)
|- ( ( t e. A |-> B ) : A --> C -> ( t e. A -> B e. C ) )
21.23.8  Multivariate polynomials over the integers
Syntax	cmzpcl 34995	Extend class notation to include pre-polynomial rings.
class mzPolyCld
Syntax	cmzp 34996	Extend class notation to include polynomial rings.
class mzPoly
Definition	df-mzpcl 34997*	Define the polynomially closed function rings over an arbitrary index set v. The set (mzPolyCld ` v ) contains all sets of functions from ( ZZ ^m v ) to ZZ which include all constants and projections and are closed under addition and multiplication. This is a "temporary" set used to define the polynomial function ring itself (mzPoly ` v ); see df-mzp 34998. (Contributed by Stefan O'Rear, 4-Oct-2014.)
|- mzPolyCld = ( v e. _V |-> { p e. ~P ( ZZ ^m ( ZZ ^m v ) ) | ( ( A. i e. ZZ ( ( ZZ ^m v ) X. { i } ) e. p /\ A. j e. v ( x e. ( ZZ ^m v ) |-> ( x ` j ) ) e. p ) /\ A. f e. p A. g e. p ( ( f oF + g ) e. p /\ ( f oF x. g ) e. p ) ) } )
Definition	df-mzp 34998	Polynomials over ZZ with an arbitrary index set, that is, the smallest ring of functions containing all constant functions and all projections. This is almost the most general reasonable definition; to reach full generality, we would need to be able to replace ZZ with an arbitrary (semi-)ring (and a coordinate subring), but rings have not been defined yet. (Contributed by Stefan O'Rear, 4-Oct-2014.)
|- mzPoly = ( v e. _V |-> |^| (mzPolyCld ` v ) )
Theorem	mzpclval 34999*	Substitution lemma for mzPolyCld. (Contributed by Stefan O'Rear, 4-Oct-2014.)
|- ( V e. _V -> (mzPolyCld ` V ) = { p e. ~P ( ZZ ^m ( ZZ ^m V ) ) | ( ( A. i e. ZZ ( ( ZZ ^m V ) X. { i } ) e. p /\ A. j e. V ( x e. ( ZZ ^m V ) |-> ( x ` j ) ) e. p ) /\ A. f e. p A. g e. p ( ( f oF + g ) e. p /\ ( f oF x. g ) e. p ) ) } )
Theorem	elmzpcl 35000*	Double substitution lemma for mzPolyCld. (Contributed by Stefan O'Rear, 4-Oct-2014.)
|- ( V e. _V -> ( P e. (mzPolyCld ` V ) <-> ( P C_ ( ZZ ^m ( ZZ ^m V ) ) /\ ( ( A. i e. ZZ ( ( ZZ ^m V ) X. { i } ) e. P /\ A. j e. V ( x e. ( ZZ ^m V ) |-> ( x ` j ) ) e. P ) /\ A. f e. P A. g e. P ( ( f oF + g ) e. P /\ ( f oF x. g ) e. P ) ) ) ) )