P. 148 of Theorem List - Intuitionistic Logic Explorer

Theorem List for Intuitionistic Logic Explorer - 14701-14800   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	zrhrhmb 14701	The ZRHom homomorphism is the unique ring homomorphism from ZZ. (Contributed by Mario Carneiro, 15-Jun-2015.) (Revised by AV, 12-Jun-2019.)
|- L = ( ZRHom ` R )   =>    |- ( R e. Ring -> ( F e. (ℤring RingHom R ) <-> F = L ) )
Theorem	zrhrhm 14702	The ZRHom homomorphism is a homomorphism. (Contributed by Mario Carneiro, 12-Jun-2015.) (Revised by AV, 12-Jun-2019.)
|- L = ( ZRHom ` R )   =>    |- ( R e. Ring -> L e. (ℤring RingHom R ) )
Theorem	zrh1 14703	Interpretation of 1 in a ring. (Contributed by Stefan O'Rear, 6-Sep-2015.)
|- L = ( ZRHom ` R )   &    |- .1. = ( 1r ` R )   =>    |- ( R e. Ring -> ( L ` 1 ) = .1. )
Theorem	zrh0 14704	Interpretation of 0 in a ring. (Contributed by Stefan O'Rear, 6-Sep-2015.)
|- L = ( ZRHom ` R )   &    |- .0. = ( 0g ` R )   =>    |- ( R e. Ring -> ( L ` 0 ) = .0. )
Theorem	zrhpropd 14705*	The ZZ ring homomorphism depends only on the ring attributes of a structure. (Contributed by Mario Carneiro, 15-Jun-2015.)
|- ( ph -> B = ( Base ` K ) )   &    |- ( ph -> B = ( Base ` L ) )   &    |- ( ( ph /\ ( x e. B /\ y e. B ) ) -> ( x ( +g ` K ) y ) = ( x ( +g ` L ) y ) )   &    |- ( ( ph /\ ( x e. B /\ y e. B ) ) -> ( x ( .r ` K ) y ) = ( x ( .r ` L ) y ) )   =>    |- ( ph -> ( ZRHom ` K ) = ( ZRHom ` L ) )
Theorem	zlmval 14706	Augment an abelian group with vector space operations to turn it into a ZZ-module. (Contributed by Mario Carneiro, 2-Oct-2015.) (Revised by AV, 12-Jun-2019.)
|- W = ( ZMod ` G )   &    |- .x. = (.g ` G )   =>    |- ( G e. V -> W = ( ( G sSet <. (Scalar ` ndx ) , ℤring >. ) sSet <. ( .s ` ndx ) , .x. >. ) )
Theorem	zlmlemg 14707	Lemma for zlmbasg 14708 and zlmplusgg 14709. (Contributed by Mario Carneiro, 2-Oct-2015.) (Revised by AV, 3-Nov-2024.)
|- W = ( ZMod ` G )   &    |- E = Slot ( E ` ndx )   &    |- ( E ` ndx ) e. NN   &    |- ( E ` ndx ) =/= (Scalar ` ndx )   &    |- ( E ` ndx ) =/= ( .s ` ndx )   =>    |- ( G e. V -> ( E ` G ) = ( E ` W ) )
Theorem	zlmbasg 14708	Base set of a ZZ-module. (Contributed by Mario Carneiro, 2-Oct-2015.) (Revised by AV, 3-Nov-2024.)
|- W = ( ZMod ` G )   &    |- B = ( Base ` G )   =>    |- ( G e. V -> B = ( Base ` W ) )
Theorem	zlmplusgg 14709	Group operation of a ZZ-module. (Contributed by Mario Carneiro, 2-Oct-2015.) (Revised by AV, 3-Nov-2024.)
|- W = ( ZMod ` G )   &    |- .+ = ( +g ` G )   =>    |- ( G e. V -> .+ = ( +g ` W ) )
Theorem	zlmmulrg 14710	Ring operation of a ZZ-module (if present). (Contributed by Mario Carneiro, 2-Oct-2015.) (Revised by AV, 3-Nov-2024.)
|- W = ( ZMod ` G )   &    |- .x. = ( .r ` G )   =>    |- ( G e. V -> .x. = ( .r ` W ) )
Theorem	zlmsca 14711	Scalar ring of a ZZ-module. (Contributed by Mario Carneiro, 2-Oct-2015.) (Revised by AV, 12-Jun-2019.) (Proof shortened by AV, 2-Nov-2024.)
|- W = ( ZMod ` G )   =>    |- ( G e. V -> ℤring = (Scalar ` W ) )
Theorem	zlmvscag 14712	Scalar multiplication operation of a ZZ-module. (Contributed by Mario Carneiro, 2-Oct-2015.)
|- W = ( ZMod ` G )   &    |- .x. = (.g ` G )   =>    |- ( G e. V -> .x. = ( .s ` W ) )
Theorem	znlidl 14713	The set n ZZ is an ideal in ZZ. (Contributed by Mario Carneiro, 14-Jun-2015.) (Revised by AV, 13-Jun-2019.)
|- S = (RSpan ` ℤring )   =>    |- ( N e. ZZ -> ( S ` { N } ) e. (LIdeal ` ℤring ) )
Theorem	zncrng2 14714	Making a commutative ring as a quotient of ZZ and n ZZ. (Contributed by Mario Carneiro, 12-Jun-2015.) (Revised by AV, 13-Jun-2019.)
|- S = (RSpan ` ℤring )   &    |- U = (ℤring /.s (ℤring ~QG ( S ` { N } ) ) )   =>    |- ( N e. ZZ -> U e. CRing )
Theorem	znval 14715	The value of the ℤ/nℤ structure. It is defined as the quotient ring ZZ / n ZZ, with an "artificial" ordering added. (In other words, ℤ/nℤ is a ring with an order , but it is not an ordered ring , which as a term implies that the order is compatible with the ring operations in some way.) (Contributed by Mario Carneiro, 14-Jun-2015.) (Revised by Mario Carneiro, 2-May-2016.) (Revised by AV, 13-Jun-2019.)
|- S = (RSpan ` ℤring )   &    |- U = (ℤring /.s (ℤring ~QG ( S ` { N } ) ) )   &    |- Y = (ℤ/nℤ ` N )   &    |- F = ( ( ZRHom ` U ) |` W )   &    |- W = if ( N = 0 , ZZ , ( 0..^ N ) )   &    |- .<_ = ( ( F o. <_ ) o. `' F )   =>    |- ( N e. NN0 -> Y = ( U sSet <. ( le ` ndx ) , .<_ >. ) )
Theorem	znle 14716	The value of the ℤ/nℤ structure. It is defined as the quotient ring ZZ / n ZZ, with an "artificial" ordering added. (In other words, ℤ/nℤ is a ring with an order , but it is not an ordered ring , which as a term implies that the order is compatible with the ring operations in some way.) (Contributed by Mario Carneiro, 14-Jun-2015.) (Revised by AV, 13-Jun-2019.)
|- S = (RSpan ` ℤring )   &    |- U = (ℤring /.s (ℤring ~QG ( S ` { N } ) ) )   &    |- Y = (ℤ/nℤ ` N )   &    |- F = ( ( ZRHom ` U ) |` W )   &    |- W = if ( N = 0 , ZZ , ( 0..^ N ) )   &    |- .<_ = ( le ` Y )   =>    |- ( N e. NN0 -> .<_ = ( ( F o. <_ ) o. `' F ) )
Theorem	znval2 14717	Self-referential expression for the ℤ/nℤ structure. (Contributed by Mario Carneiro, 14-Jun-2015.) (Revised by AV, 13-Jun-2019.)
|- S = (RSpan ` ℤring )   &    |- U = (ℤring /.s (ℤring ~QG ( S ` { N } ) ) )   &    |- Y = (ℤ/nℤ ` N )   &    |- .<_ = ( le ` Y )   =>    |- ( N e. NN0 -> Y = ( U sSet <. ( le ` ndx ) , .<_ >. ) )
Theorem	znbaslemnn 14718	Lemma for znbas 14723. (Contributed by Mario Carneiro, 14-Jun-2015.) (Revised by Mario Carneiro, 14-Aug-2015.) (Revised by AV, 13-Jun-2019.) (Revised by AV, 9-Sep-2021.) (Revised by AV, 3-Nov-2024.)
|- S = (RSpan ` ℤring )   &    |- U = (ℤring /.s (ℤring ~QG ( S ` { N } ) ) )   &    |- Y = (ℤ/nℤ ` N )   &    |- E = Slot ( E ` ndx )   &    |- ( E ` ndx ) e. NN   &    |- ( E ` ndx ) =/= ( le ` ndx )   =>    |- ( N e. NN0 -> ( E ` U ) = ( E ` Y ) )
Theorem	znbas2 14719	The base set of ℤ/nℤ is the same as the quotient ring it is based on. (Contributed by Mario Carneiro, 15-Jun-2015.) (Revised by AV, 13-Jun-2019.) (Revised by AV, 3-Nov-2024.)
|- S = (RSpan ` ℤring )   &    |- U = (ℤring /.s (ℤring ~QG ( S ` { N } ) ) )   &    |- Y = (ℤ/nℤ ` N )   =>    |- ( N e. NN0 -> ( Base ` U ) = ( Base ` Y ) )
Theorem	znadd 14720	The additive structure of ℤ/nℤ is the same as the quotient ring it is based on. (Contributed by Mario Carneiro, 15-Jun-2015.) (Revised by AV, 13-Jun-2019.) (Revised by AV, 3-Nov-2024.)
|- S = (RSpan ` ℤring )   &    |- U = (ℤring /.s (ℤring ~QG ( S ` { N } ) ) )   &    |- Y = (ℤ/nℤ ` N )   =>    |- ( N e. NN0 -> ( +g ` U ) = ( +g ` Y ) )
Theorem	znmul 14721	The multiplicative structure of ℤ/nℤ is the same as the quotient ring it is based on. (Contributed by Mario Carneiro, 15-Jun-2015.) (Revised by AV, 13-Jun-2019.) (Revised by AV, 3-Nov-2024.)
|- S = (RSpan ` ℤring )   &    |- U = (ℤring /.s (ℤring ~QG ( S ` { N } ) ) )   &    |- Y = (ℤ/nℤ ` N )   =>    |- ( N e. NN0 -> ( .r ` U ) = ( .r ` Y ) )
Theorem	znzrh 14722	The ZZ ring homomorphism of ℤ/nℤ is inherited from the quotient ring it is based on. (Contributed by Mario Carneiro, 14-Jun-2015.) (Revised by AV, 13-Jun-2019.)
|- S = (RSpan ` ℤring )   &    |- U = (ℤring /.s (ℤring ~QG ( S ` { N } ) ) )   &    |- Y = (ℤ/nℤ ` N )   =>    |- ( N e. NN0 -> ( ZRHom ` U ) = ( ZRHom ` Y ) )
Theorem	znbas 14723	The base set of ℤ/nℤ structure. (Contributed by Mario Carneiro, 15-Jun-2015.) (Revised by AV, 13-Jun-2019.)
|- S = (RSpan ` ℤring )   &    |- Y = (ℤ/nℤ ` N )   &    |- R = (ℤring ~QG ( S ` { N } ) )   =>    |- ( N e. NN0 -> ( ZZ /. R ) = ( Base ` Y ) )
Theorem	zncrng 14724	ℤ/nℤ is a commutative ring. (Contributed by Mario Carneiro, 15-Jun-2015.)
|- Y = (ℤ/nℤ ` N )   =>    |- ( N e. NN0 -> Y e. CRing )
Theorem	znzrh2 14725*	The ZZ ring homomorphism maps elements to their equivalence classes. (Contributed by Mario Carneiro, 15-Jun-2015.) (Revised by AV, 13-Jun-2019.)
|- S = (RSpan ` ℤring )   &    |- .~ = (ℤring ~QG ( S ` { N } ) )   &    |- Y = (ℤ/nℤ ` N )   &    |- L = ( ZRHom ` Y )   =>    |- ( N e. NN0 -> L = ( x e. ZZ |-> [ x ] .~ ) )
Theorem	znzrhval 14726	The ZZ ring homomorphism maps elements to their equivalence classes. (Contributed by Mario Carneiro, 15-Jun-2015.) (Revised by AV, 13-Jun-2019.)
|- S = (RSpan ` ℤring )   &    |- .~ = (ℤring ~QG ( S ` { N } ) )   &    |- Y = (ℤ/nℤ ` N )   &    |- L = ( ZRHom ` Y )   =>    |- ( ( N e. NN0 /\ A e. ZZ ) -> ( L ` A ) = [ A ] .~ )
Theorem	znzrhfo 14727	The ZZ ring homomorphism is a surjection onto ℤ/nℤ. (Contributed by Mario Carneiro, 15-Jun-2015.)
|- Y = (ℤ/nℤ ` N )   &    |- B = ( Base ` Y )   &    |- L = ( ZRHom ` Y )   =>    |- ( N e. NN0 -> L : ZZ -onto-> B )
Theorem	zndvds 14728	Express equality of equivalence classes in ZZ / n ZZ in terms of divisibility. (Contributed by Mario Carneiro, 15-Jun-2015.)
|- Y = (ℤ/nℤ ` N )   &    |- L = ( ZRHom ` Y )   =>    |- ( ( N e. NN0 /\ A e. ZZ /\ B e. ZZ ) -> ( ( L ` A ) = ( L ` B ) <-> N || ( A - B ) ) )
Theorem	zndvds0 14729	Special case of zndvds 14728 when one argument is zero. (Contributed by Mario Carneiro, 15-Jun-2015.)
|- Y = (ℤ/nℤ ` N )   &    |- L = ( ZRHom ` Y )   &    |- .0. = ( 0g ` Y )   =>    |- ( ( N e. NN0 /\ A e. ZZ ) -> ( ( L ` A ) = .0. <-> N || A ) )
Theorem	znf1o 14730	The function F enumerates all equivalence classes in ℤ/nℤ for each n. When n = 0, ZZ / 0 ZZ = ZZ / { 0 } ~~ ZZ so we let W = ZZ; otherwise W = { 0 , ... , n - 1 } enumerates all the equivalence classes. (Contributed by Mario Carneiro, 15-Jun-2015.) (Revised by Mario Carneiro, 2-May-2016.) (Revised by AV, 13-Jun-2019.)
|- Y = (ℤ/nℤ ` N )   &    |- B = ( Base ` Y )   &    |- F = ( ( ZRHom ` Y ) |` W )   &    |- W = if ( N = 0 , ZZ , ( 0..^ N ) )   =>    |- ( N e. NN0 -> F : W -1-1-onto-> B )
Theorem	znle2 14731	The ordering of the ℤ/nℤ structure. (Contributed by Mario Carneiro, 15-Jun-2015.) (Revised by AV, 13-Jun-2019.)
|- Y = (ℤ/nℤ ` N )   &    |- F = ( ( ZRHom ` Y ) |` W )   &    |- W = if ( N = 0 , ZZ , ( 0..^ N ) )   &    |- .<_ = ( le ` Y )   =>    |- ( N e. NN0 -> .<_ = ( ( F o. <_ ) o. `' F ) )
Theorem	znleval 14732	The ordering of the ℤ/nℤ structure. (Contributed by Mario Carneiro, 15-Jun-2015.) (Revised by AV, 13-Jun-2019.)
|- Y = (ℤ/nℤ ` N )   &    |- F = ( ( ZRHom ` Y ) |` W )   &    |- W = if ( N = 0 , ZZ , ( 0..^ N ) )   &    |- .<_ = ( le ` Y )   &    |- X = ( Base ` Y )   =>    |- ( N e. NN0 -> ( A .<_ B <-> ( A e. X /\ B e. X /\ ( `' F ` A ) <_ ( `' F ` B ) ) ) )
Theorem	znleval2 14733	The ordering of the ℤ/nℤ structure. (Contributed by Mario Carneiro, 15-Jun-2015.) (Revised by AV, 13-Jun-2019.)
|- Y = (ℤ/nℤ ` N )   &    |- F = ( ( ZRHom ` Y ) |` W )   &    |- W = if ( N = 0 , ZZ , ( 0..^ N ) )   &    |- .<_ = ( le ` Y )   &    |- X = ( Base ` Y )   =>    |- ( ( N e. NN0 /\ A e. X /\ B e. X ) -> ( A .<_ B <-> ( `' F ` A ) <_ ( `' F ` B ) ) )
Theorem	znfi 14734	The ℤ/nℤ structure is a finite ring. (Contributed by Mario Carneiro, 2-May-2016.)
|- Y = (ℤ/nℤ ` N )   &    |- B = ( Base ` Y )   =>    |- ( N e. NN -> B e. Fin )
Theorem	znhash 14735	The ℤ/nℤ structure has n elements. (Contributed by Mario Carneiro, 15-Jun-2015.)
|- Y = (ℤ/nℤ ` N )   &    |- B = ( Base ` Y )   =>    |- ( N e. NN -> (♯ ` B ) = N )
Theorem	znidom 14736	The ℤ/nℤ structure is an integral domain when n is prime. (Contributed by Mario Carneiro, 15-Jun-2015.) (Revised by Jim Kingdon, 13-Aug-2025.)
|- Y = (ℤ/nℤ ` N )   =>    |- ( N e. Prime -> Y e. IDomn )
Theorem	znidomb 14737	The ℤ/nℤ structure is a domain precisely when n is prime. (Contributed by Mario Carneiro, 15-Jun-2015.)
|- Y = (ℤ/nℤ ` N )   =>    |- ( N e. NN -> ( Y e. IDomn <-> N e. Prime ) )
Theorem	znunit 14738	The units of ℤ/nℤ are the integers coprime to the base. (Contributed by Mario Carneiro, 18-Apr-2016.)
|- Y = (ℤ/nℤ ` N )   &    |- U = (Unit ` Y )   &    |- L = ( ZRHom ` Y )   =>    |- ( ( N e. NN0 /\ A e. ZZ ) -> ( ( L ` A ) e. U <-> ( A gcd N ) = 1 ) )
Theorem	znrrg 14739	The regular elements of ℤ/nℤ are exactly the units. (This theorem fails for N = 0, where all nonzero integers are regular, but only pm 1 are units.) (Contributed by Mario Carneiro, 18-Apr-2016.)
|- Y = (ℤ/nℤ ` N )   &    |- U = (Unit ` Y )   &    |- E = (RLReg ` Y )   =>    |- ( N e. NN -> E = U )
PART 8  BASIC LINEAR ALGEBRA According to Wikipedia ("Linear algebra", 03-Mar-2019, https://en.wikipedia.org/wiki/Linear_algebra) "Linear algebra is the branch of mathematics concerning linear equations [...], linear functions [...] and their representations through matrices and vector spaces." Or according to the Merriam-Webster dictionary ("linear algebra", 12-Mar-2019, https://www.merriam-webster.com/dictionary/linear%20algebra) "Definition of linear algebra: a branch of mathematics that is concerned with mathematical structures closed under the operations of addition and scalar multiplication and that includes the theory of systems of linear equations, matrices, determinants, vector spaces, and linear transformations." Dealing with modules (over rings) instead of vector spaces (over fields) allows for a more unified approach. Therefore, linear equations, matrices, determinants, are usually regarded as "over a ring" in this part. Unless otherwise stated, the rings of scalars need not be commutative (see df-cring 14076), but the existence of a unity element is always assumed (our rings are unital, see df-ring 14075). For readers knowing vector spaces but unfamiliar with modules: the elements of a module are still called "vectors" and they still form a group under addition, with a zero vector as neutral element, like in a vector space. Like in a vector space, vectors can be multiplied by scalars, with the usual rules, the only difference being that the scalars are only required to form a ring, and not necessarily a field or a division ring. Note that any vector space is a (special kind of) module, so any theorem proved below for modules applies to any vector space.
8.1  Abstract multivariate polynomials
8.1.1  Definition and basic properties
Syntax	cmps 14740	Multivariate power series.
class mPwSer
Syntax	cmpl 14741	Multivariate polynomials.
class mPoly
Definition	df-psr 14742*	Define the algebra of power series over the index set i and with coefficients from the ring r. (Contributed by Mario Carneiro, 21-Mar-2015.)
|- mPwSer = ( i e. _V , r e. _V |-> [_ { h e. ( NN0 ^m i ) | ( `' h " NN ) e. Fin } / d ]_ [_ ( ( Base ` r ) ^m d ) / b ]_ ( { <. ( Base ` ndx ) , b >. , <. ( +g ` ndx ) , ( oF ( +g ` r ) |` ( b X. b ) ) >. , <. ( .r ` ndx ) , ( f e. b , g e. b |-> ( k e. d |-> ( r gsumg ( x e. { y e. d | y oR <_ k } |-> ( ( f ` x ) ( .r ` r ) ( g ` ( k oF - x ) ) ) ) ) ) ) >. } u. { <. (Scalar ` ndx ) , r >. , <. ( .s ` ndx ) , ( x e. ( Base ` r ) , f e. b |-> ( ( d X. { x } ) oF ( .r ` r ) f ) ) >. , <. (TopSet ` ndx ) , ( Xt_ ` ( d X. { ( TopOpen ` r ) } ) ) >. } ) )
Definition	df-mplcoe 14743*	Define the subalgebra of the power series algebra generated by the variables; this is the polynomial algebra (the set of power series with finite degree). The index set (which has an element for each variable) is i, the coefficients are in ring r, and for each variable there is a "degree" such that the coefficient is zero for a term where the powers are all greater than those degrees. (Degree is in quotes because there is no guarantee that coefficients below that degree are nonzero, as we do not assume decidable equality for r). (Contributed by Mario Carneiro, 7-Jan-2015.) (Revised by AV, 25-Jun-2019.) (Revised by Jim Kingdon, 7-Oct-2025.)
|- mPoly = ( i e. _V , r e. _V |-> [_ ( i mPwSer r ) / w ]_ ( w ↾s { f e. ( Base ` w ) | E. a e. ( NN0 ^m i ) A. b e. ( NN0 ^m i ) ( A. k e. i ( a ` k ) < ( b ` k ) -> ( f ` b ) = ( 0g ` r ) ) } ) )
Theorem	reldmpsr 14744	The multivariate power series constructor is a proper binary operator. (Contributed by Mario Carneiro, 21-Mar-2015.)
|- Rel dom mPwSer
Theorem	psrval 14745*	Value of the multivariate power series structure. (Contributed by Mario Carneiro, 29-Dec-2014.)
|- S = ( I mPwSer R )   &    |- K = ( Base ` R )   &    |- .+ = ( +g ` R )   &    |- .x. = ( .r ` R )   &    |- O = ( TopOpen ` R )   &    |- D = { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin }   &    |- ( ph -> B = ( K ^m D ) )   &    |- .+b = ( oF .+ |` ( B X. B ) )   &    |- .X. = ( f e. B , g e. B |-> ( k e. D |-> ( R gsumg ( x e. { y e. D | y oR <_ k } |-> ( ( f ` x ) .x. ( g ` ( k oF - x ) ) ) ) ) ) )   &    |- .xb = ( x e. K , f e. B |-> ( ( D X. { x } ) oF .x. f ) )   &    |- ( ph -> J = ( Xt_ ` ( D X. { O } ) ) )   &    |- ( ph -> I e. W )   &    |- ( ph -> R e. X )   =>    |- ( ph -> S = ( { <. ( Base ` ndx ) , B >. , <. ( +g ` ndx ) , .+b >. , <. ( .r ` ndx ) , .X. >. } u. { <. (Scalar ` ndx ) , R >. , <. ( .s ` ndx ) , .xb >. , <. (TopSet ` ndx ) , J >. } ) )
Theorem	fnpsr 14746	The multivariate power series constructor has a universal domain. (Contributed by Jim Kingdon, 16-Jun-2025.)
|- mPwSer Fn ( _V X. _V )
Theorem	psrvalstrd 14747	The multivariate power series structure is a function. (Contributed by Mario Carneiro, 8-Feb-2015.)
|- ( ph -> B e. X )   &    |- ( ph -> .+ e. Y )   &    |- ( ph -> .X. e. Z )   &    |- ( ph -> R e. W )   &    |- ( ph -> .x. e. P )   &    |- ( ph -> J e. Q )   =>    |- ( ph -> ( { <. ( Base ` ndx ) , B >. , <. ( +g ` ndx ) , .+ >. , <. ( .r ` ndx ) , .X. >. } u. { <. (Scalar ` ndx ) , R >. , <. ( .s ` ndx ) , .x. >. , <. (TopSet ` ndx ) , J >. } ) Struct <. 1 , 9 >. )
Theorem	psrbag 14748*	Elementhood in the set of finite bags. (Contributed by Mario Carneiro, 29-Dec-2014.)
|- D = { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin }   =>    |- ( I e. V -> ( F e. D <-> ( F : I --> NN0 /\ ( `' F " NN ) e. Fin ) ) )
Theorem	psrbagf 14749*	A finite bag is a function. (Contributed by Mario Carneiro, 29-Dec-2014.) Remove a sethood antecedent. (Revised by SN, 30-Jul-2024.)
|- D = { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin }   =>    |- ( F e. D -> F : I --> NN0 )
Theorem	fczpsrbag 14750*	The constant function equal to zero is a finite bag. (Contributed by AV, 8-Jul-2019.)
|- D = { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin }   =>    |- ( I e. V -> ( x e. I |-> 0 ) e. D )
Theorem	psrbaglesuppg 14751*	The support of a dominated bag is smaller than the dominating bag. (Contributed by Mario Carneiro, 29-Dec-2014.)
|- D = { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin }   =>    |- ( ( I e. V /\ ( F e. D /\ G : I --> NN0 /\ G oR <_ F ) ) -> ( `' G " NN ) C_ ( `' F " NN ) )
Theorem	psrbaglesupp 14752*	The support of a dominated bag is smaller than the dominating bag. (Contributed by Mario Carneiro, 29-Dec-2014.) Remove a sethood antecedent. (Revised by SN, 5-Aug-2024.)
|- D = { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin }   =>    |- ( ( F e. D /\ G : I --> NN0 /\ G oR <_ F ) -> ( `' G " NN ) C_ ( `' F " NN ) )
Theorem	psrbagfi 14753*	A finite index set gives a simpler expression for finite bags. (Contributed by Jim Kingdon, 23-Nov-2025.)
|- D = { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin }   =>    |- ( I e. Fin -> D = ( NN0 ^m I ) )
Theorem	psrbaglecl 14754*	The set of finite bags is downward-closed. (Contributed by Mario Carneiro, 29-Dec-2014.) Remove a sethood antecedent. (Revised by SN, 5-Aug-2024.)
|- D = { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin }   =>    |- ( ( F e. D /\ G : I --> NN0 /\ G oR <_ F ) -> G e. D )
Theorem	psrbagcon 14755*	The analogue of the statement " 0 <_ G <_ F implies 0 <_ F - G <_ F " for finite bags. (Contributed by Mario Carneiro, 29-Dec-2014.) Remove a sethood antecedent. (Revised by SN, 5-Aug-2024.)
|- D = { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin }   =>    |- ( ( F e. D /\ G : I --> NN0 /\ G oR <_ F ) -> ( ( F oF - G ) e. D /\ ( F oF - G ) oR <_ F ) )
Theorem	psrbagconcl 14756*	The complement of a bag is a bag. (Contributed by Mario Carneiro, 29-Dec-2014.) Remove a sethood antecedent. (Revised by SN, 6-Aug-2024.)
|- D = { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin }   &    |- S = { y e. D | y oR <_ F }   =>    |- ( ( F e. D /\ X e. S ) -> ( F oF - X ) e. S )
Theorem	psrbagconf1o 14757*	Bag complementation is a bijection on the set of bags dominated by a given bag F. (Contributed by Mario Carneiro, 29-Dec-2014.) Remove a sethood antecedent. (Revised by SN, 6-Aug-2024.)
|- D = { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin }   &    |- S = { y e. D | y oR <_ F }   =>    |- ( F e. D -> ( x e. S |-> ( F oF - x ) ) : S -1-1-onto-> S )
Theorem	psrbasg 14758*	The base set of the multivariate power series structure. (Contributed by Mario Carneiro, 28-Dec-2014.) (Revised by Mario Carneiro, 2-Oct-2015.) (Proof shortened by AV, 8-Jul-2019.)
|- S = ( I mPwSer R )   &    |- K = ( Base ` R )   &    |- D = { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin }   &    |- B = ( Base ` S )   &    |- ( ph -> I e. V )   &    |- ( ph -> R e. W )   =>    |- ( ph -> B = ( K ^m D ) )
Theorem	psrelbas 14759*	An element of the set of power series is a function on the coefficients. (Contributed by Mario Carneiro, 28-Dec-2014.)
|- S = ( I mPwSer R )   &    |- K = ( Base ` R )   &    |- D = { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin }   &    |- B = ( Base ` S )   &    |- ( ph -> X e. B )   =>    |- ( ph -> X : D --> K )
Theorem	psrelbasfi 14760	Simpler form of psrelbas 14759 when the index set is finite. (Contributed by Jim Kingdon, 27-Nov-2025.)
|- S = ( I mPwSer R )   &    |- K = ( Base ` R )   &    |- ( ph -> I e. Fin )   &    |- B = ( Base ` S )   &    |- ( ph -> X e. B )   =>    |- ( ph -> X : ( NN0 ^m I ) --> K )
Theorem	psrelbasfun 14761	An element of the set of power series is a function. (Contributed by AV, 17-Jul-2019.)
|- S = ( I mPwSer R )   &    |- B = ( Base ` S )   =>    |- ( X e. B -> Fun X )
Theorem	psrplusgg 14762	The addition operation of the multivariate power series structure. (Contributed by Mario Carneiro, 28-Dec-2014.) (Revised by Mario Carneiro, 2-Oct-2015.)
|- S = ( I mPwSer R )   &    |- B = ( Base ` S )   &    |- .+ = ( +g ` R )   &    |- .+b = ( +g ` S )   =>    |- ( ( I e. V /\ R e. W ) -> .+b = ( oF .+ |` ( B X. B ) ) )
Theorem	psradd 14763	The addition operation of the multivariate power series structure. (Contributed by Mario Carneiro, 28-Dec-2014.)
|- S = ( I mPwSer R )   &    |- B = ( Base ` S )   &    |- .+ = ( +g ` R )   &    |- .+b = ( +g ` S )   &    |- ( ph -> X e. B )   &    |- ( ph -> Y e. B )   =>    |- ( ph -> ( X .+b Y ) = ( X oF .+ Y ) )
Theorem	psraddcl 14764	Closure of the power series addition operation. (Contributed by Mario Carneiro, 28-Dec-2014.) Generalize to magmas. (Revised by SN, 12-Apr-2025.)
|- S = ( I mPwSer R )   &    |- B = ( Base ` S )   &    |- .+ = ( +g ` S )   &    |- ( ph -> R e. Mgm )   &    |- ( ph -> X e. B )   &    |- ( ph -> Y e. B )   =>    |- ( ph -> ( X .+ Y ) e. B )
Theorem	psr0cl 14765*	The zero element of the ring of power series. (Contributed by Mario Carneiro, 29-Dec-2014.)
|- S = ( I mPwSer R )   &    |- ( ph -> I e. V )   &    |- ( ph -> R e. Grp )   &    |- D = { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin }   &    |- .0. = ( 0g ` R )   &    |- B = ( Base ` S )   =>    |- ( ph -> ( D X. { .0. } ) e. B )
Theorem	psr0lid 14766*	The zero element of the ring of power series is a left identity. (Contributed by Mario Carneiro, 29-Dec-2014.)
|- S = ( I mPwSer R )   &    |- ( ph -> I e. V )   &    |- ( ph -> R e. Grp )   &    |- D = { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin }   &    |- .0. = ( 0g ` R )   &    |- B = ( Base ` S )   &    |- .+ = ( +g ` S )   &    |- ( ph -> X e. B )   =>    |- ( ph -> ( ( D X. { .0. } ) .+ X ) = X )
Theorem	psrnegcl 14767*	The negative function in the ring of power series. (Contributed by Mario Carneiro, 29-Dec-2014.)
|- S = ( I mPwSer R )   &    |- ( ph -> I e. V )   &    |- ( ph -> R e. Grp )   &    |- D = { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin }   &    |- N = ( invg ` R )   &    |- B = ( Base ` S )   &    |- ( ph -> X e. B )   =>    |- ( ph -> ( N o. X ) e. B )
Theorem	psrlinv 14768*	The negative function in the ring of power series. (Contributed by Mario Carneiro, 29-Dec-2014.)
|- S = ( I mPwSer R )   &    |- ( ph -> I e. V )   &    |- ( ph -> R e. Grp )   &    |- D = { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin }   &    |- N = ( invg ` R )   &    |- B = ( Base ` S )   &    |- ( ph -> X e. B )   &    |- .0. = ( 0g ` R )   &    |- .+ = ( +g ` S )   =>    |- ( ph -> ( ( N o. X ) .+ X ) = ( D X. { .0. } ) )
Theorem	psrgrp 14769	The ring of power series is a group. (Contributed by Mario Carneiro, 29-Dec-2014.) (Proof shortened by SN, 7-Feb-2025.)
|- S = ( I mPwSer R )   &    |- ( ph -> I e. V )   &    |- ( ph -> R e. Grp )   =>    |- ( ph -> S e. Grp )
Theorem	psr0 14770*	The zero element of the ring of power series. (Contributed by Mario Carneiro, 29-Dec-2014.)
|- S = ( I mPwSer R )   &    |- ( ph -> I e. V )   &    |- ( ph -> R e. Grp )   &    |- D = { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin }   &    |- O = ( 0g ` R )   &    |- .0. = ( 0g ` S )   =>    |- ( ph -> .0. = ( D X. { O } ) )
Theorem	psrneg 14771*	The negative function of the ring of power series. (Contributed by Mario Carneiro, 29-Dec-2014.)
|- S = ( I mPwSer R )   &    |- ( ph -> I e. V )   &    |- ( ph -> R e. Grp )   &    |- D = { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin }   &    |- N = ( invg ` R )   &    |- B = ( Base ` S )   &    |- M = ( invg ` S )   &    |- ( ph -> X e. B )   =>    |- ( ph -> ( M ` X ) = ( N o. X ) )
Theorem	psr1clfi 14772*	The identity element of the ring of power series. (Contributed by Mario Carneiro, 29-Dec-2014.)
|- S = ( I mPwSer R )   &    |- ( ph -> I e. Fin )   &    |- ( ph -> R e. Ring )   &    |- D = { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin }   &    |- .0. = ( 0g ` R )   &    |- .1. = ( 1r ` R )   &    |- U = ( x e. D |-> if ( x = ( I X. { 0 } ) , .1. , .0. ) )   &    |- B = ( Base ` S )   =>    |- ( ph -> U e. B )
Theorem	reldmmpl 14773	The multivariate polynomial constructor is a proper binary operator. (Contributed by Mario Carneiro, 21-Mar-2015.)
|- Rel dom mPoly
Theorem	mplvalcoe 14774*	Value of the set of multivariate polynomials. (Contributed by Mario Carneiro, 7-Jan-2015.) (Revised by AV, 25-Jun-2019.) (Revised by Jim Kingdon, 4-Nov-2025.)
|- P = ( I mPoly R )   &    |- S = ( I mPwSer R )   &    |- B = ( Base ` S )   &    |- .0. = ( 0g ` R )   &    |- U = { f e. B | E. a e. ( NN0 ^m I ) A. b e. ( NN0 ^m I ) ( A. k e. I ( a ` k ) < ( b ` k ) -> ( f ` b ) = .0. ) }   =>    |- ( ( I e. V /\ R e. W ) -> P = ( S ↾s U ) )
Theorem	mplbascoe 14775*	Base set of the set of multivariate polynomials. (Contributed by Mario Carneiro, 7-Jan-2015.) (Revised by AV, 25-Jun-2019.) (Revised by Jim Kingdon, 4-Nov-2025.)
|- P = ( I mPoly R )   &    |- S = ( I mPwSer R )   &    |- B = ( Base ` S )   &    |- .0. = ( 0g ` R )   &    |- U = ( Base ` P )   =>    |- ( ( I e. V /\ R e. W ) -> U = { f e. B | E. a e. ( NN0 ^m I ) A. b e. ( NN0 ^m I ) ( A. k e. I ( a ` k ) < ( b ` k ) -> ( f ` b ) = .0. ) } )
Theorem	mplelbascoe 14776*	Property of being a polynomial. (Contributed by Mario Carneiro, 7-Jan-2015.) (Revised by Mario Carneiro, 2-Oct-2015.) (Revised by AV, 25-Jun-2019.) (Revised by Jim Kingdon, 4-Nov-2025.)
|- P = ( I mPoly R )   &    |- S = ( I mPwSer R )   &    |- B = ( Base ` S )   &    |- .0. = ( 0g ` R )   &    |- U = ( Base ` P )   =>    |- ( ( I e. V /\ R e. W ) -> ( X e. U <-> ( X e. B /\ E. a e. ( NN0 ^m I ) A. b e. ( NN0 ^m I ) ( A. k e. I ( a ` k ) < ( b ` k ) -> ( X ` b ) = .0. ) ) ) )
Theorem	fnmpl 14777	mPoly has universal domain. (Contributed by Jim Kingdon, 5-Nov-2025.)
|- mPoly Fn ( _V X. _V )
Theorem	mplrcl 14778	Reverse closure for the polynomial index set. (Contributed by Stefan O'Rear, 19-Mar-2015.) (Revised by Mario Carneiro, 30-Aug-2015.)
|- P = ( I mPoly R )   &    |- B = ( Base ` P )   =>    |- ( X e. B -> I e. _V )
Theorem	mplval2g 14779	Self-referential expression for the set of multivariate polynomials. (Contributed by Mario Carneiro, 7-Jan-2015.) (Revised by Mario Carneiro, 2-Oct-2015.)
|- P = ( I mPoly R )   &    |- S = ( I mPwSer R )   &    |- U = ( Base ` P )   =>    |- ( ( I e. V /\ R e. W ) -> P = ( S ↾s U ) )
Theorem	mplbasss 14780	The set of polynomials is a subset of the set of power series. (Contributed by Mario Carneiro, 7-Jan-2015.) (Revised by Mario Carneiro, 2-Oct-2015.)
|- P = ( I mPoly R )   &    |- S = ( I mPwSer R )   &    |- U = ( Base ` P )   &    |- B = ( Base ` S )   =>    |- U C_ B
Theorem	mplelf 14781*	A polynomial is defined as a function on the coefficients. (Contributed by Mario Carneiro, 7-Jan-2015.) (Revised by Mario Carneiro, 2-Oct-2015.)
|- P = ( I mPoly R )   &    |- K = ( Base ` R )   &    |- B = ( Base ` P )   &    |- D = { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin }   &    |- ( ph -> X e. B )   =>    |- ( ph -> X : D --> K )
Theorem	mplsubgfilemm 14782*	Lemma for mplsubgfi 14785. There exists a polynomial. (Contributed by Jim Kingdon, 21-Nov-2025.)
|- S = ( I mPwSer R )   &    |- P = ( I mPoly R )   &    |- U = ( Base ` P )   &    |- ( ph -> I e. Fin )   &    |- ( ph -> R e. Grp )   =>    |- ( ph -> E. j j e. U )
Theorem	mplsubgfilemcl 14783	Lemma for mplsubgfi 14785. The sum of two polynomials is a polynomial. (Contributed by Jim Kingdon, 26-Nov-2025.)
|- S = ( I mPwSer R )   &    |- P = ( I mPoly R )   &    |- U = ( Base ` P )   &    |- ( ph -> I e. Fin )   &    |- ( ph -> R e. Grp )   &    |- ( ph -> X e. U )   &    |- ( ph -> Y e. U )   &    |- .+ = ( +g ` S )   =>    |- ( ph -> ( X .+ Y ) e. U )
Theorem	mplsubgfileminv 14784	Lemma for mplsubgfi 14785. The additive inverse of a polynomial is a polynomial. (Contributed by Jim Kingdon, 26-Nov-2025.)
|- S = ( I mPwSer R )   &    |- P = ( I mPoly R )   &    |- U = ( Base ` P )   &    |- ( ph -> I e. Fin )   &    |- ( ph -> R e. Grp )   &    |- ( ph -> X e. U )   &    |- N = ( invg ` S )   =>    |- ( ph -> ( N ` X ) e. U )
Theorem	mplsubgfi 14785	The set of polynomials is closed under addition, i.e. it is a subgroup of the set of power series. (Contributed by Mario Carneiro, 8-Jan-2015.) (Proof shortened by AV, 16-Jul-2019.)
|- S = ( I mPwSer R )   &    |- P = ( I mPoly R )   &    |- U = ( Base ` P )   &    |- ( ph -> I e. Fin )   &    |- ( ph -> R e. Grp )   =>    |- ( ph -> U e. (SubGrp ` S ) )
Theorem	mpl0fi 14786*	The zero polynomial. (Contributed by Mario Carneiro, 9-Jan-2015.)
|- P = ( I mPoly R )   &    |- O = ( 0g ` R )   &    |- .0. = ( 0g ` P )   &    |- ( ph -> I e. Fin )   &    |- ( ph -> R e. Grp )   =>    |- ( ph -> .0. = ( x e. ( NN0 ^m I ) |-> O ) )
Theorem	mplplusgg 14787	Value of addition in a polynomial ring. (Contributed by Stefan O'Rear, 21-Mar-2015.) (Revised by Mario Carneiro, 2-Oct-2015.)
|- Y = ( I mPoly R )   &    |- S = ( I mPwSer R )   &    |- .+ = ( +g ` Y )   =>    |- ( ( I e. V /\ R e. W ) -> .+ = ( +g ` S ) )
Theorem	mpladd 14788	The addition operation on multivariate polynomials. (Contributed by Mario Carneiro, 9-Jan-2015.) (Revised by Mario Carneiro, 2-Oct-2015.)
|- P = ( I mPoly R )   &    |- B = ( Base ` P )   &    |- .+ = ( +g ` R )   &    |- .+b = ( +g ` P )   &    |- ( ph -> X e. B )   &    |- ( ph -> Y e. B )   =>    |- ( ph -> ( X .+b Y ) = ( X oF .+ Y ) )
Theorem	mplnegfi 14789	The negative function on multivariate polynomials. (Contributed by SN, 25-May-2024.)
|- P = ( I mPoly R )   &    |- B = ( Base ` P )   &    |- N = ( invg ` R )   &    |- M = ( invg ` P )   &    |- ( ph -> I e. Fin )   &    |- ( ph -> R e. Grp )   &    |- ( ph -> X e. B )   =>    |- ( ph -> ( M ` X ) = ( N o. X ) )
Theorem	mplgrpfi 14790	The polynomial ring is a group. (Contributed by Mario Carneiro, 9-Jan-2015.)
|- P = ( I mPoly R )   =>    |- ( ( I e. Fin /\ R e. Grp ) -> P e. Grp )
PART 9  BASIC TOPOLOGY
9.1  Topology
9.1.1  Topological spaces A topology on a set is a set of subsets of that set, called open sets, which satisfy certain conditions. One condition is that the whole set be an open set. Therefore, a set is recoverable from a topology on it (as its union), and it may sometimes be more convenient to consider topologies without reference to the underlying set.
9.1.1.1  Topologies
Syntax	ctop 14791	Syntax for the class of topologies.
class Top
Definition	df-top 14792*	Define the class of topologies. It is a proper class. See istopg 14793 and istopfin 14794 for the corresponding characterizations, using respectively binary intersections like in this definition and nonempty finite intersections. The final form of the definition is due to Bourbaki (Def. 1 of [BourbakiTop1] p. I.1), while the idea of defining a topology in terms of its open sets is due to Aleksandrov. For the convoluted history of the definitions of these notions, see Gregory H. Moore, The emergence of open sets, closed sets, and limit points in analysis and topology, Historia Mathematica 35 (2008) 220--241. (Contributed by NM, 3-Mar-2006.) (Revised by BJ, 20-Oct-2018.)
|- Top = { x | ( A. y e. ~P x U. y e. x /\ A. y e. x A. z e. x ( y i^i z ) e. x ) }
Theorem	istopg 14793*	Express the predicate " J is a topology". See istopfin 14794 for another characterization using nonempty finite intersections instead of binary intersections. Note: In the literature, a topology is often represented by a calligraphic letter T, which resembles the letter J. This confusion may have led to J being used by some authors (e.g., K. D. Joshi, Introduction to General Topology (1983), p. 114) and it is convenient for us since we later use T to represent linear transformations (operators). (Contributed by Stefan Allan, 3-Mar-2006.) (Revised by Mario Carneiro, 11-Nov-2013.)
|- ( J e. A -> ( J e. Top <-> ( A. x ( x C_ J -> U. x e. J ) /\ A. x e. J A. y e. J ( x i^i y ) e. J ) ) )
Theorem	istopfin 14794*	Express the predicate " J is a topology" using nonempty finite intersections instead of binary intersections as in istopg 14793. It is not clear we can prove the converse without adding additional conditions. (Contributed by NM, 19-Jul-2006.) (Revised by Jim Kingdon, 14-Jan-2023.)
|- ( J e. Top -> ( A. x ( x C_ J -> U. x e. J ) /\ A. x ( ( x C_ J /\ x =/= (/) /\ x e. Fin ) -> |^| x e. J ) ) )
Theorem	uniopn 14795	The union of a subset of a topology (that is, the union of any family of open sets of a topology) is an open set. (Contributed by Stefan Allan, 27-Feb-2006.)
|- ( ( J e. Top /\ A C_ J ) -> U. A e. J )
Theorem	iunopn 14796*	The indexed union of a subset of a topology is an open set. (Contributed by NM, 5-Oct-2006.)
|- ( ( J e. Top /\ A. x e. A B e. J ) -> U_ x e. A B e. J )
Theorem	inopn 14797	The intersection of two open sets of a topology is an open set. (Contributed by NM, 17-Jul-2006.)
|- ( ( J e. Top /\ A e. J /\ B e. J ) -> ( A i^i B ) e. J )
Theorem	fiinopn 14798	The intersection of a nonempty finite family of open sets is open. (Contributed by FL, 20-Apr-2012.)
|- ( J e. Top -> ( ( A C_ J /\ A =/= (/) /\ A e. Fin ) -> |^| A e. J ) )
Theorem	unopn 14799	The union of two open sets is open. (Contributed by Jeff Madsen, 2-Sep-2009.)
|- ( ( J e. Top /\ A e. J /\ B e. J ) -> ( A u. B ) e. J )
Theorem	0opn 14800	The empty set is an open subset of any topology. (Contributed by Stefan Allan, 27-Feb-2006.)
|- ( J e. Top -> (/) e. J )