Home | Metamath
Proof Explorer Theorem List (p. 194 of 426) | < Previous Next > |
Browser slow? Try the
Unicode version. |
||
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
Color key: | Metamath Proof Explorer
(1-27775) |
Hilbert Space Explorer
(27776-29300) |
Users' Mathboxes
(29301-42551) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | opprdomn 19301 | The opposite of a domain is also a domain. (Contributed by Mario Carneiro, 15-Jun-2015.) |
oppr Domn Domn | ||
Theorem | abvn0b 19302 | Another characterization of domains, hinted at in abvtriv 18841: a nonzero ring is a domain iff it has an absolute value. (Contributed by Mario Carneiro, 6-May-2015.) |
AbsVal Domn NzRing | ||
Theorem | drngdomn 19303 | A division ring is a domain. (Contributed by Mario Carneiro, 29-Mar-2015.) |
Domn | ||
Theorem | isidom 19304 | An integral domain is a commutative domain. (Contributed by Mario Carneiro, 17-Jun-2015.) |
IDomn Domn | ||
Theorem | fldidom 19305 | A field is an integral domain. (Contributed by Mario Carneiro, 29-Mar-2015.) |
Field IDomn | ||
Theorem | fidomndrnglem 19306* | Lemma for fidomndrng 19307. (Contributed by Mario Carneiro, 15-Jun-2015.) |
r Domn | ||
Theorem | fidomndrng 19307 | A finite domain is a division ring. (Contributed by Mario Carneiro, 15-Jun-2015.) |
Domn | ||
Theorem | fiidomfld 19308 | A finite integral domain is a field. (Contributed by Mario Carneiro, 15-Jun-2015.) |
IDomn Field | ||
Syntax | casa 19309 | Associative algebra. |
AssAlg | ||
Syntax | casp 19310 | Algebraic span function. |
AlgSpan | ||
Syntax | cascl 19311 | Class of algebra scalar injection function. |
algSc | ||
Definition | df-assa 19312* | Definition of an associative algebra. An associative algebra is a set equipped with a left-module structure on a (commutative) ring, coupled with a multiplicative internal operation on the vectors of the module that is associative and distributive for the additive structure of the left-module (so giving the vectors a ring structure) and that is also bilinear under the scalar product. (Contributed by Mario Carneiro, 29-Dec-2014.) |
AssAlg Scalar | ||
Definition | df-asp 19313* | Define the algebraic span of a set of vectors in an algebra. (Contributed by Mario Carneiro, 7-Jan-2015.) |
AlgSpan AssAlg SubRing | ||
Definition | df-ascl 19314* | Every unital algebra contains a canonical homomorphic image of its ring of scalars as scalar multiples of the unit. This names the homomorphism. (Contributed by Mario Carneiro, 8-Mar-2015.) |
algSc Scalar | ||
Theorem | isassa 19315* | The properties of an associative algebra. (Contributed by Mario Carneiro, 29-Dec-2014.) |
Scalar AssAlg | ||
Theorem | assalem 19316 | The properties of an associative algebra. (Contributed by Mario Carneiro, 29-Dec-2014.) |
Scalar AssAlg | ||
Theorem | assaass 19317 | Left-associative property of an associative algebra. (Contributed by Mario Carneiro, 29-Dec-2014.) |
Scalar AssAlg | ||
Theorem | assaassr 19318 | Right-associative property of an associative algebra. (Contributed by Mario Carneiro, 29-Dec-2014.) |
Scalar AssAlg | ||
Theorem | assalmod 19319 | An associative algebra is a left module. (Contributed by Mario Carneiro, 5-Dec-2014.) |
AssAlg | ||
Theorem | assaring 19320 | An associative algebra is a ring. (Contributed by Mario Carneiro, 5-Dec-2014.) |
AssAlg | ||
Theorem | assasca 19321 | An associative algebra's scalar field is a commutative ring. (Contributed by Mario Carneiro, 7-Jan-2015.) |
Scalar AssAlg | ||
Theorem | assa2ass 19322 | Left- and right-associative property of an associative algebra. Notice that the scalars are commuted! (Contributed by AV, 14-Aug-2019.) |
Scalar AssAlg | ||
Theorem | isassad 19323* | Sufficient condition for being an associative algebra. (Contributed by Mario Carneiro, 5-Dec-2014.) |
Scalar AssAlg | ||
Theorem | issubassa 19324 | The subalgebras of an associative algebra are exactly the subrings (under the ring multiplication) that are simultaneously subspaces (under the scalar multiplication from the vector space). (Contributed by Mario Carneiro, 7-Jan-2015.) |
↾s AssAlg AssAlg SubRing | ||
Theorem | sraassa 19325 | The subring algebra over a commutative ring is an associative algebra. (Contributed by Mario Carneiro, 6-Oct-2015.) |
subringAlg SubRing AssAlg | ||
Theorem | rlmassa 19326 | The ring module over a commutative ring is an associative algebra. (Contributed by Mario Carneiro, 6-Oct-2015.) |
ringLMod AssAlg | ||
Theorem | assapropd 19327* | If two structures have the same components (properties), one is an associative algebra iff the other one is. (Contributed by Mario Carneiro, 8-Feb-2015.) |
Scalar Scalar AssAlg AssAlg | ||
Theorem | aspval 19328* | Value of the algebraic closure operation inside an associative algebra. (Contributed by Mario Carneiro, 7-Jan-2015.) |
AlgSpan AssAlg SubRing | ||
Theorem | asplss 19329 | The algebraic span of a set of vectors is a vector subspace. (Contributed by Mario Carneiro, 7-Jan-2015.) |
AlgSpan AssAlg | ||
Theorem | aspid 19330 | The algebraic span of a subalgebra is itself. (spanid 28206 analog.) (Contributed by Mario Carneiro, 7-Jan-2015.) |
AlgSpan AssAlg SubRing | ||
Theorem | aspsubrg 19331 | The algebraic span of a set of vectors is a subring of the algebra. (Contributed by Mario Carneiro, 7-Jan-2015.) |
AlgSpan AssAlg SubRing | ||
Theorem | aspss 19332 | Span preserves subset ordering. (spanss 28207 analog.) (Contributed by Mario Carneiro, 7-Jan-2015.) |
AlgSpan AssAlg | ||
Theorem | aspssid 19333 | A set of vectors is a subset of its span. (spanss2 28204 analog.) (Contributed by Mario Carneiro, 7-Jan-2015.) |
AlgSpan AssAlg | ||
Theorem | asclfval 19334* | Function value of the algebraic scalars function. (Contributed by Mario Carneiro, 8-Mar-2015.) |
algSc Scalar | ||
Theorem | asclval 19335 | Value of a mapped algebra scalar. (Contributed by Mario Carneiro, 8-Mar-2015.) |
algSc Scalar | ||
Theorem | asclfn 19336 | Unconditional functionality of the algebra scalars function. (Contributed by Mario Carneiro, 9-Mar-2015.) |
algSc Scalar | ||
Theorem | asclf 19337 | The algebra scalars function is a function into the base set. (Contributed by Mario Carneiro, 4-Jul-2015.) |
algSc Scalar | ||
Theorem | asclghm 19338 | The algebra scalars function is a group homomorphism. (Contributed by Mario Carneiro, 4-Jul-2015.) |
algSc Scalar | ||
Theorem | asclmul1 19339 | Left multiplication by a lifted scalar is the same as the scalar operation. (Contributed by Mario Carneiro, 9-Mar-2015.) |
algSc Scalar AssAlg | ||
Theorem | asclmul2 19340 | Right multiplication by a lifted scalar is the same as the scalar operation. (Contributed by Mario Carneiro, 9-Mar-2015.) |
algSc Scalar AssAlg | ||
Theorem | asclinvg 19341 | The group inverse (negation) of a lifted scalar is the lifted negation of the scalar. (Contributed by AV, 2-Sep-2019.) |
algSc Scalar | ||
Theorem | asclrhm 19342 | The scalar injection is a ring homomorphism. (Contributed by Mario Carneiro, 8-Mar-2015.) |
algSc Scalar AssAlg RingHom | ||
Theorem | rnascl 19343 | The set of injected scalars is also interpretable as the span of the identity. (Contributed by Mario Carneiro, 9-Mar-2015.) |
algSc AssAlg | ||
Theorem | ressascl 19344 | The injection of scalars is invariant between subalgebras and superalgebras. (Contributed by Mario Carneiro, 9-Mar-2015.) |
algSc ↾s SubRing algSc | ||
Theorem | issubassa2 19345 | A subring of a unital algebra is a subspace and thus a subalgebra iff it contains all scalar multiples of the identity. (Contributed by Mario Carneiro, 9-Mar-2015.) |
algSc AssAlg SubRing | ||
Theorem | asclpropd 19346* | If two structures have the same components (properties), one is an associative algebra iff the other one is. The last hypotheses on can be discharged either by letting (if strong equality is known on ) or assuming is a ring. (Contributed by Mario Carneiro, 5-Jul-2015.) |
Scalar Scalar algSc algSc | ||
Theorem | aspval2 19347 | The algebraic closure is the ring closure when the generating set is expanded to include all scalars. EDITORIAL : In light of this, is AlgSpan independently needed? (Contributed by Stefan O'Rear, 9-Mar-2015.) |
AlgSpan algSc mrClsSubRing AssAlg | ||
Theorem | assamulgscmlem1 19348 | Lemma 1 for assamulgscm 19350 (induction base). (Contributed by AV, 26-Aug-2019.) |
Scalar mulGrp .g mulGrp .g AssAlg | ||
Theorem | assamulgscmlem2 19349 | Lemma for assamulgscm 19350 (induction step). (Contributed by AV, 26-Aug-2019.) |
Scalar mulGrp .g mulGrp .g AssAlg | ||
Theorem | assamulgscm 19350 | Exponentiation of a scalar multiplication in an associative algebra: . (Contributed by AV, 26-Aug-2019.) |
Scalar mulGrp .g mulGrp .g AssAlg | ||
Syntax | cmps 19351 | Multivariate power series. |
mPwSer | ||
Syntax | cmvr 19352 | Multivariate power series variables. |
mVar | ||
Syntax | cmpl 19353 | Multivariate polynomials. |
mPoly | ||
Syntax | cltb 19354 | Ordering on terms of a multivariate polynomial. |
bag | ||
Syntax | copws 19355 | Ordered set of power series. |
ordPwSer | ||
Definition | df-psr 19356* | Define the algebra of power series over the index set and with coefficients from the ring . (Contributed by Mario Carneiro, 21-Mar-2015.) |
mPwSer g Scalar TopSet | ||
Definition | df-mvr 19357* | Define the generating elements of the power series algebra. (Contributed by Mario Carneiro, 7-Jan-2015.) |
mVar | ||
Definition | df-mpl 19358* | 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). (Contributed by Mario Carneiro, 7-Jan-2015.) (Revised by AV, 25-Jun-2019.) |
mPoly mPwSer ↾s finSupp | ||
Definition | df-ltbag 19359* | Define a well-order on the set of all finite bags from the index set given a wellordering of . (Contributed by Mario Carneiro, 8-Feb-2015.) |
bag | ||
Definition | df-opsr 19360* | Define a total order on the set of all power series in from the index set given a wellordering of and a totally ordered base ring . (Contributed by Mario Carneiro, 8-Feb-2015.) |
ordPwSer mPwSer sSet bag | ||
Theorem | reldmpsr 19361 | The multivariate power series constructor is a proper binary operator. (Contributed by Mario Carneiro, 21-Mar-2015.) |
mPwSer | ||
Theorem | psrval 19362* | Value of the multivariate power series structure. (Contributed by Mario Carneiro, 29-Dec-2014.) |
mPwSer g Scalar TopSet | ||
Theorem | psrvalstr 19363 | The multivariate power series structure is a function. (Contributed by Mario Carneiro, 8-Feb-2015.) |
Scalar TopSet Struct | ||
Theorem | psrbag 19364* | Elementhood in the set of finite bags. (Contributed by Mario Carneiro, 29-Dec-2014.) |
Theorem | psrbagf 19365* | A finite bag is a function. (Contributed by Mario Carneiro, 29-Dec-2014.) |
Theorem | snifpsrbag 19366* | A bag containing one element is a finite bag. (Contributed by Mario Carneiro, 7-Jan-2015.) (Revised by AV, 8-Jul-2019.) |
Theorem | fczpsrbag 19367* | The constant function equal to zero is a finite bag. (Contributed by AV, 8-Jul-2019.) |
Theorem | psrbaglesupp 19368* | The support of a dominated bag is smaller than the dominating bag. (Contributed by Mario Carneiro, 29-Dec-2014.) |
Theorem | psrbaglecl 19369* | The set of finite bags is downward-closed. (Contributed by Mario Carneiro, 29-Dec-2014.) |
Theorem | psrbagaddcl 19370* | The sum of two finite bags is a finite bag. (Contributed by Mario Carneiro, 9-Jan-2015.) |
Theorem | psrbagcon 19371* | The analogue of the statement " implies " for finite bags. (Contributed by Mario Carneiro, 29-Dec-2014.) |
Theorem | psrbaglefi 19372* | There are finitely many bags dominated by a given bag. (Contributed by Mario Carneiro, 29-Dec-2014.) (Revised by Mario Carneiro, 25-Jan-2015.) |
Theorem | psrbagconcl 19373* | The complement of a bag is a bag. (Contributed by Mario Carneiro, 29-Dec-2014.) |
Theorem | psrbagconf1o 19374* | Bag complementation is a bijection on the set of bags dominated by a given bag . (Contributed by Mario Carneiro, 29-Dec-2014.) |
Theorem | gsumbagdiaglem 19375* | Lemma for gsumbagdiag 19376. (Contributed by Mario Carneiro, 5-Jan-2015.) |
Theorem | gsumbagdiag 19376* | Two-dimensional commutation of a group sum over a "triangular" region. fsum0diag 14509 analogue for finite bags. (Contributed by Mario Carneiro, 5-Jan-2015.) |
CMnd g g | ||
Theorem | psrass1lem 19377* | A group sum commutation used by psrass1 19405. (Contributed by Mario Carneiro, 5-Jan-2015.) |
CMnd g g g g | ||
Theorem | psrbas 19378* | 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.) |
mPwSer | ||
Theorem | psrelbas 19379* | An element of the set of power series is a function on the coefficients. (Contributed by Mario Carneiro, 28-Dec-2014.) |
mPwSer | ||
Theorem | psrelbasfun 19380 | An element of the set of power series is a function. (Contributed by AV, 17-Jul-2019.) |
mPwSer | ||
Theorem | psrplusg 19381 | The addition operation of the multivariate power series structure. (Contributed by Mario Carneiro, 28-Dec-2014.) (Revised by Mario Carneiro, 2-Oct-2015.) |
mPwSer | ||
Theorem | psradd 19382 | The addition operation of the multivariate power series structure. (Contributed by Mario Carneiro, 28-Dec-2014.) |
mPwSer | ||
Theorem | psraddcl 19383 | Closure of the power series addition operation. (Contributed by Mario Carneiro, 28-Dec-2014.) |
mPwSer | ||
Theorem | psrmulr 19384* | The multiplication operation of the multivariate power series structure. (Contributed by Mario Carneiro, 28-Dec-2014.) (Revised by Mario Carneiro, 2-Oct-2015.) |
mPwSer g | ||
Theorem | psrmulfval 19385* | The multiplication operation of the multivariate power series structure. (Contributed by Mario Carneiro, 28-Dec-2014.) |
mPwSer g | ||
Theorem | psrmulval 19386* | The multiplication operation of the multivariate power series structure. (Contributed by Mario Carneiro, 28-Dec-2014.) |
mPwSer g | ||
Theorem | psrmulcllem 19387* | Closure of the power series multiplication operation. (Contributed by Mario Carneiro, 29-Dec-2014.) |
mPwSer | ||
Theorem | psrmulcl 19388 | Closure of the power series multiplication operation. (Contributed by Mario Carneiro, 29-Dec-2014.) |
mPwSer | ||
Theorem | psrsca 19389 | The scalar field of the multivariate power series structure. (Contributed by Mario Carneiro, 28-Dec-2014.) |
mPwSer Scalar | ||
Theorem | psrvscafval 19390* | The scalar multiplication operation of the multivariate power series structure. (Contributed by Mario Carneiro, 28-Dec-2014.) (Revised by Mario Carneiro, 2-Oct-2015.) |
mPwSer | ||
Theorem | psrvsca 19391* | The scalar multiplication operation of the multivariate power series structure. (Contributed by Mario Carneiro, 28-Dec-2014.) |
mPwSer | ||
Theorem | psrvscaval 19392* | The scalar multiplication operation of the multivariate power series structure. (Contributed by Mario Carneiro, 28-Dec-2014.) |
mPwSer | ||
Theorem | psrvscacl 19393 | Closure of the power series scalar multiplication operation. (Contributed by Mario Carneiro, 29-Dec-2014.) |
mPwSer | ||
Theorem | psr0cl 19394* | The zero element of the ring of power series. (Contributed by Mario Carneiro, 29-Dec-2014.) |
mPwSer | ||
Theorem | psr0lid 19395* | The zero element of the ring of power series is a left identity. (Contributed by Mario Carneiro, 29-Dec-2014.) |
mPwSer | ||
Theorem | psrnegcl 19396* | The negative function in the ring of power series. (Contributed by Mario Carneiro, 29-Dec-2014.) |
mPwSer | ||
Theorem | psrlinv 19397* | The negative function in the ring of power series. (Contributed by Mario Carneiro, 29-Dec-2014.) |
mPwSer | ||
Theorem | psrgrp 19398 | The ring of power series is a group. (Contributed by Mario Carneiro, 29-Dec-2014.) |
mPwSer | ||
Theorem | psr0 19399* | The zero element of the ring of power series. (Contributed by Mario Carneiro, 29-Dec-2014.) |
mPwSer | ||
Theorem | psrneg 19400* | The negative function of the ring of power series. (Contributed by Mario Carneiro, 29-Dec-2014.) |
mPwSer |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |