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	hdmapinvlem1 35501	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 35419. 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 35502	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 35503	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 35504	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 35419. 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 35505	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 35506	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 35507	Lemma for hgmapvv 35509. 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 35508	Lemma for hgmapvv 35509. 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 35509	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 35510*	Lemma for hdmapg 35513. (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 35511	Lemma for hdmapg 35513. (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 35512	Lemma for hdmapg 35513. 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 35513	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 35514*	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 35515	Extend class notation with the final constructed Hilbert space.
class HLHil
Definition	df-hlhil 35516*	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 35517*	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 35518	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 35519	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 35520	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 35521	Lemma for hlhilsbase2 35525. (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 35522	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 35523	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 35524	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 35525	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 35526	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 35527	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 35528	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 35529	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 35530	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 35531*	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 35532	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 35533	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 35534	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 35535	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 35536	Lemma for hlhilsrng 35537. (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 35537	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 35538	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 35539	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 35540	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 35541	The closed subspaces of the final constructed Hilbert space. TODO: hlhilbase 35519 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 35542*	Lemma for hlhil 22409. (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 35543*	Lemma for hlhil 22409. (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 35544	Construction of a Hilbert space (df-hil 19279) U from a Hilbert lattice (df-hlat 32929) 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 34689) 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 19279. 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 35545	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 35546*	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 35547*	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 35548*	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 35549*	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 35550*	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 35551*	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 35552*	Any function from the subsets of a set to itself, which is extensive (satisfies mrcssid 15535), isotone (satisfies mrcss 15534), and idempotent (satisfies mrcidm 15537) 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 35553 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 35553*	Second half of ismrcd1 35552. (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 35554*	A closure function which satisfies sscls 20083, clsidm 20095, cls0 20108, and clsun 30996 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 35555*	A function is a Moore closure operator iff it satisfies mrcssid 15535, mrcss 15534, and mrcidm 15537. (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 35556	Class of Noetherian closure systems.
class NoeACS
Definition	df-nacs 35557*	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 35558*	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 35559*	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 35560	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 35561*	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 35562*	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 35563	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 35564*	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 35565*	Transitivity induction of subsets, lemma for nacsfix 35566. (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 35566*	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 35567	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 35568	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 35569	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 35570	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 35571	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 35572	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 35573	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 35574*	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 35575	Extend class notation to include pre-polynomial rings.
class mzPolyCld
Syntax	cmzp 35576	Extend class notation to include polynomial rings.
class mzPoly
Definition	df-mzpcl 35577*	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 35578. (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 35578	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 35579*	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 35580*	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 ) ) ) ) )
Theorem	mzpclall 35581	The set of all functions with the signature of a polynomial is a polynomially closed set. This is a lemma to show that the intersection in df-mzp 35578 is well-defined. (Contributed by Stefan O'Rear, 4-Oct-2014.)
|- ( V e. _V -> ( ZZ ^m ( ZZ ^m V ) ) e. (mzPolyCld ` V ) )
Theorem	mzpcln0 35582	Corrolary of mzpclall 35581: polynomially closed function sets are not empty. (Contributed by Stefan O'Rear, 4-Oct-2014.)
|- ( V e. _V -> (mzPolyCld ` V ) =/= (/) )
Theorem	mzpcl1 35583	Defining property 1 of a polynomially closed function set P: it contains all constant functions. (Contributed by Stefan O'Rear, 4-Oct-2014.)
|- ( ( P e. (mzPolyCld ` V ) /\ F e. ZZ ) -> ( ( ZZ ^m V ) X. { F } ) e. P )
Theorem	mzpcl2 35584*	Defining property 2 of a polynomially closed function set P: it contains all projections. (Contributed by Stefan O'Rear, 4-Oct-2014.)
|- ( ( P e. (mzPolyCld ` V ) /\ F e. V ) -> ( g e. ( ZZ ^m V ) |-> ( g ` F ) ) e. P )
Theorem	mzpcl34 35585	Defining properties 3 and 4 of a polynomially closed function set P: it is closed under pointwise addition and multiplication. (Contributed by Stefan O'Rear, 4-Oct-2014.)
|- ( ( P e. (mzPolyCld ` V ) /\ F e. P /\ G e. P ) -> ( ( F oF + G ) e. P /\ ( F oF x. G ) e. P ) )
Theorem	mzpval 35586	Value of the mzPoly function. (Contributed by Stefan O'Rear, 4-Oct-2014.)
|- ( V e. _V -> (mzPoly ` V ) = |^| (mzPolyCld ` V ) )
Theorem	dmmzp 35587	mzPoly is defined for all index sets which are sets. This is used with elfvdm 5896 to eliminate sethood antecedents. (Contributed by Stefan O'Rear, 4-Oct-2014.)
|- dom mzPoly = _V
Theorem	mzpincl 35588	Polynomial closedness is a universal first-order property and passes to intersections. This is where the closure properties of the polynomial ring itself are proved. (Contributed by Stefan O'Rear, 4-Oct-2014.)
|- ( V e. _V -> (mzPoly ` V ) e. (mzPolyCld ` V ) )
Theorem	mzpconst 35589	Constant functions are polynomial. See also mzpconstmpt 35594. (Contributed by Stefan O'Rear, 4-Oct-2014.)
|- ( ( V e. _V /\ C e. ZZ ) -> ( ( ZZ ^m V ) X. { C } ) e. (mzPoly ` V ) )
Theorem	mzpf 35590	A polynomial function is a function from the coordinate space to the integers. (Contributed by Stefan O'Rear, 5-Oct-2014.)
|- ( F e. (mzPoly ` V ) -> F : ( ZZ ^m V ) --> ZZ )
Theorem	mzpproj 35591*	A projection function is polynomial. (Contributed by Stefan O'Rear, 4-Oct-2014.)
|- ( ( V e. _V /\ X e. V ) -> ( g e. ( ZZ ^m V ) |-> ( g ` X ) ) e. (mzPoly ` V ) )
Theorem	mzpadd 35592	The pointwise sum of two polynomial functions is a polynomial function. See also mzpaddmpt 35595. (Contributed by Stefan O'Rear, 4-Oct-2014.)
|- ( ( A e. (mzPoly ` V ) /\ B e. (mzPoly ` V ) ) -> ( A oF + B ) e. (mzPoly ` V ) )
Theorem	mzpmul 35593	The pointwise product of two polynomial functions is a polynomial function. See also mzpmulmpt 35596. (Contributed by Stefan O'Rear, 4-Oct-2014.)
|- ( ( A e. (mzPoly ` V ) /\ B e. (mzPoly ` V ) ) -> ( A oF x. B ) e. (mzPoly ` V ) )
Theorem	mzpconstmpt 35594*	A constant function expressed in maps-to notation is polynomial. This theorem and the several that follow (mzpaddmpt 35595, mzpmulmpt 35596, mzpnegmpt 35598, mzpsubmpt 35597, mzpexpmpt 35599) can be used to build proofs that functions which are "manifestly polynomial", in the sense of being a maps-to containing constants, projections, and simple arithmetic operations, are actually polynomial functions. There is no mzpprojmpt because mzpproj 35591 is already expressed using maps-to notation. (Contributed by Stefan O'Rear, 5-Oct-2014.)
|- ( ( V e. _V /\ C e. ZZ ) -> ( x e. ( ZZ ^m V ) |-> C ) e. (mzPoly ` V ) )
Theorem	mzpaddmpt 35595*	Sum of polynomial functions is polynomial. Maps-to version of mzpadd 35592. (Contributed by Stefan O'Rear, 5-Oct-2014.)
|- ( ( ( x e. ( ZZ ^m V ) |-> A ) e. (mzPoly ` V ) /\ ( x e. ( ZZ ^m V ) |-> B ) e. (mzPoly ` V ) ) -> ( x e. ( ZZ ^m V ) |-> ( A + B ) ) e. (mzPoly ` V ) )
Theorem	mzpmulmpt 35596*	Product of polynomial functions is polynomial. Maps-to version of mzpmulmpt 35596. (Contributed by Stefan O'Rear, 5-Oct-2014.)
|- ( ( ( x e. ( ZZ ^m V ) |-> A ) e. (mzPoly ` V ) /\ ( x e. ( ZZ ^m V ) |-> B ) e. (mzPoly ` V ) ) -> ( x e. ( ZZ ^m V ) |-> ( A x. B ) ) e. (mzPoly ` V ) )
Theorem	mzpsubmpt 35597*	The difference of two polynomial functions is polynomial. (Contributed by Stefan O'Rear, 10-Oct-2014.)
|- ( ( ( x e. ( ZZ ^m V ) |-> A ) e. (mzPoly ` V ) /\ ( x e. ( ZZ ^m V ) |-> B ) e. (mzPoly ` V ) ) -> ( x e. ( ZZ ^m V ) |-> ( A - B ) ) e. (mzPoly ` V ) )
Theorem	mzpnegmpt 35598*	Negation of a polynomial function. (Contributed by Stefan O'Rear, 11-Oct-2014.)
|- ( ( x e. ( ZZ ^m V ) |-> A ) e. (mzPoly ` V ) -> ( x e. ( ZZ ^m V ) |-> -u A ) e. (mzPoly ` V ) )
Theorem	mzpexpmpt 35599*	Raise a polynomial function to a (fixed) exponent. (Contributed by Stefan O'Rear, 5-Oct-2014.)
|- ( ( ( x e. ( ZZ ^m V ) |-> A ) e. (mzPoly ` V ) /\ D e. NN0 ) -> ( x e. ( ZZ ^m V ) |-> ( A ^ D ) ) e. (mzPoly ` V ) )
Theorem	mzpindd 35600*	"Structural" induction to prove properties of all polynomial functions. (Contributed by Stefan O'Rear, 4-Oct-2014.)
|- ( ( ph /\ f e. ZZ ) -> ch )   &    |- ( ( ph /\ f e. V ) -> th )   &    |- ( ( ph /\ ( f : ( ZZ ^m V ) --> ZZ /\ ta ) /\ ( g : ( ZZ ^m V ) --> ZZ /\ et ) ) -> ze )   &    |- ( ( ph /\ ( f : ( ZZ ^m V ) --> ZZ /\ ta ) /\ ( g : ( ZZ ^m V ) --> ZZ /\ et ) ) -> si )   &    |- ( x = ( ( ZZ ^m V ) X. { f } ) -> ( ps <-> ch ) )   &    |- ( x = ( g e. ( ZZ ^m V ) |-> ( g ` f ) ) -> ( ps <-> th ) )   &    |- ( x = f -> ( ps <-> ta ) )   &    |- ( x = g -> ( ps <-> et ) )   &    |- ( x = ( f oF + g ) -> ( ps <-> ze ) )   &    |- ( x = ( f oF x. g ) -> ( ps <-> si ) )   &    |- ( x = A -> ( ps <-> rh ) )   =>    |- ( ( ph /\ A e. (mzPoly ` V ) ) -> rh )