P. 337 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 33601-33700   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	ismtycnv 33601	The inverse of an isometry is an isometry. (Contributed by Jeff Madsen, 2-Sep-2009.)
|- ( ( M e. ( *Met ` X ) /\ N e. ( *Met ` Y ) ) -> ( F e. ( M Ismty N ) -> `' F e. ( N Ismty M ) ) )
Theorem	ismtyima 33602	The image of a ball under an isometry is another ball. (Contributed by Jeff Madsen, 31-Jan-2014.)
|- ( ( ( M e. ( *Met ` X ) /\ N e. ( *Met ` Y ) /\ F e. ( M Ismty N ) ) /\ ( P e. X /\ R e. RR* ) ) -> ( F " ( P ( ball ` M ) R ) ) = ( ( F ` P ) ( ball ` N ) R ) )
Theorem	ismtyhmeolem 33603	Lemma for ismtyhmeo 33604. (Contributed by Jeff Madsen, 2-Sep-2009.) (Revised by Mario Carneiro, 12-Sep-2015.)
|- J = ( MetOpen ` M )   &    |- K = ( MetOpen ` N )   &    |- ( ph -> M e. ( *Met ` X ) )   &    |- ( ph -> N e. ( *Met ` Y ) )   &    |- ( ph -> F e. ( M Ismty N ) )   =>    |- ( ph -> F e. ( J Cn K ) )
Theorem	ismtyhmeo 33604	An isometry is a homeomorphism on the induced topology. (Contributed by Jeff Madsen, 2-Sep-2009.) (Revised by Mario Carneiro, 12-Sep-2015.)
|- J = ( MetOpen ` M )   &    |- K = ( MetOpen ` N )   =>    |- ( ( M e. ( *Met ` X ) /\ N e. ( *Met ` Y ) ) -> ( M Ismty N ) C_ ( J Homeo K ) )
Theorem	ismtybndlem 33605	Lemma for ismtybnd 33606. (Contributed by Jeff Madsen, 2-Sep-2009.) (Proof shortened by Mario Carneiro, 19-Jan-2014.)
|- ( ( N e. ( *Met ` Y ) /\ F e. ( M Ismty N ) ) -> ( M e. ( Bnd ` X ) -> N e. ( Bnd ` Y ) ) )
Theorem	ismtybnd 33606	Isometries preserve boundedness. (Contributed by Jeff Madsen, 2-Sep-2009.) (Revised by Mario Carneiro, 19-Jan-2014.)
|- ( ( M e. ( *Met ` X ) /\ N e. ( *Met ` Y ) /\ F e. ( M Ismty N ) ) -> ( M e. ( Bnd ` X ) <-> N e. ( Bnd ` Y ) ) )
Theorem	ismtyres 33607	A restriction of an isometry is an isometry. The condition A C_ X is not necessary but makes the proof easier. (Contributed by Jeff Madsen, 2-Sep-2009.) (Revised by Mario Carneiro, 12-Sep-2015.)
|- B = ( F " A )   &    |- S = ( M |` ( A X. A ) )   &    |- T = ( N |` ( B X. B ) )   =>    |- ( ( ( M e. ( *Met ` X ) /\ N e. ( *Met ` Y ) ) /\ ( F e. ( M Ismty N ) /\ A C_ X ) ) -> ( F |` A ) e. ( S Ismty T ) )
20.19.9  Heine-Borel Theorem
Theorem	heibor1lem 33608	Lemma for heibor1 33609. A compact metric space is complete. This proof works by considering the collection cls ( F " ( ZZ>= ` n ) ) for each n e. NN, which has the finite intersection property because any finite intersection of upper integer sets is another upper integer set, so any finite intersection of the image closures will contain ( F " ( ZZ>= ` m ) ) for some m. Thus, by compactness, the intersection contains a point y, which must then be the convergent point of F. (Contributed by Jeff Madsen, 17-Jan-2014.) (Revised by Mario Carneiro, 5-Jun-2014.)
|- J = ( MetOpen ` D )   &    |- ( ph -> D e. ( Met ` X ) )   &    |- ( ph -> J e. Comp )   &    |- ( ph -> F e. ( Cau ` D ) )   &    |- ( ph -> F : NN --> X )   =>    |- ( ph -> F e. dom ( ~~> t ` J ) )
Theorem	heibor1 33609	One half of heibor 33620, that does not require any Choice. A compact metric space is complete and totally bounded. We prove completeness in cmpcmet 23116 and total boundedness here, which follows trivially from the fact that the set of all r-balls is an open cover of X, so finitely many cover X. (Contributed by Jeff Madsen, 16-Jan-2014.)
|- J = ( MetOpen ` D )   =>    |- ( ( D e. ( Met ` X ) /\ J e. Comp ) -> ( D e. ( CMet ` X ) /\ D e. ( TotBnd ` X ) ) )
Theorem	heiborlem1 33610*	Lemma for heibor 33620. We work with a fixed open cover U throughout. The set K is the set of all subsets of X that admit no finite subcover of U. (We wish to prove that K is empty.) If a set C has no finite subcover, then any finite cover of C must contain a set that also has no finite subcover. (Contributed by Jeff Madsen, 23-Jan-2014.)
|- J = ( MetOpen ` D )   &    |- K = { u | -. E. v e. ( ~P U i^i Fin ) u C_ U. v }   &    |- B e. _V   =>    |- ( ( A e. Fin /\ C C_ U_ x e. A B /\ C e. K ) -> E. x e. A B e. K )
Theorem	heiborlem2 33611*	Lemma for heibor 33620. Substitutions for the set G. (Contributed by Jeff Madsen, 23-Jan-2014.)
|- J = ( MetOpen ` D )   &    |- K = { u | -. E. v e. ( ~P U i^i Fin ) u C_ U. v }   &    |- G = { <. y , n >. | ( n e. NN0 /\ y e. ( F ` n ) /\ ( y B n ) e. K ) }   &    |- A e. _V   &    |- C e. _V   =>    |- ( A G C <-> ( C e. NN0 /\ A e. ( F ` C ) /\ ( A B C ) e. K ) )
Theorem	heiborlem3 33612*	Lemma for heibor 33620. Using countable choice ax-cc 9257, we have fixed in advance a collection of finite 2 ^ -u n nets ( F ` n ) for X (note that an r-net is a set of points in X whose r -balls cover X). The set G is the subset of these points whose corresponding balls have no finite subcover (i.e. in the set K). If the theorem was false, then X would be in K, and so some ball at each level would also be in K. But we can say more than this; given a ball ( y B n ) on level n, since level n + 1 covers the space and thus also ( y B n ), using heiborlem1 33610 there is a ball on the next level whose intersection with ( y B n ) also has no finite subcover. Now since the set G is a countable union of finite sets, it is countable (which needs ax-cc 9257 via iunctb 9396), and so we can apply ax-cc 9257 to G directly to get a function from G to itself, which points from each ball in K to a ball on the next level in K, and such that the intersection between these balls is also in K. (Contributed by Jeff Madsen, 18-Jan-2014.)
|- J = ( MetOpen ` D )   &    |- K = { u | -. E. v e. ( ~P U i^i Fin ) u C_ U. v }   &    |- G = { <. y , n >. | ( n e. NN0 /\ y e. ( F ` n ) /\ ( y B n ) e. K ) }   &    |- B = ( z e. X , m e. NN0 |-> ( z ( ball ` D ) ( 1 / ( 2 ^ m ) ) ) )   &    |- ( ph -> D e. ( CMet ` X ) )   &    |- ( ph -> F : NN0 --> ( ~P X i^i Fin ) )   &    |- ( ph -> A. n e. NN0 X = U_ y e. ( F ` n ) ( y B n ) )   =>    |- ( ph -> E. g A. x e. G ( ( g ` x ) G ( ( 2nd ` x ) + 1 ) /\ ( ( B ` x ) i^i ( ( g ` x ) B ( ( 2nd ` x ) + 1 ) ) ) e. K ) )
Theorem	heiborlem4 33613*	Lemma for heibor 33620. Using the function T constructed in heiborlem3 33612, construct an infinite path in G. (Contributed by Jeff Madsen, 23-Jan-2014.)
|- J = ( MetOpen ` D )   &    |- K = { u | -. E. v e. ( ~P U i^i Fin ) u C_ U. v }   &    |- G = { <. y , n >. | ( n e. NN0 /\ y e. ( F ` n ) /\ ( y B n ) e. K ) }   &    |- B = ( z e. X , m e. NN0 |-> ( z ( ball ` D ) ( 1 / ( 2 ^ m ) ) ) )   &    |- ( ph -> D e. ( CMet ` X ) )   &    |- ( ph -> F : NN0 --> ( ~P X i^i Fin ) )   &    |- ( ph -> A. n e. NN0 X = U_ y e. ( F ` n ) ( y B n ) )   &    |- ( ph -> A. x e. G ( ( T ` x ) G ( ( 2nd ` x ) + 1 ) /\ ( ( B ` x ) i^i ( ( T ` x ) B ( ( 2nd ` x ) + 1 ) ) ) e. K ) )   &    |- ( ph -> C G 0 )   &    |- S = seq 0 ( T , ( m e. NN0 |-> if ( m = 0 , C , ( m - 1 ) ) ) )   =>    |- ( ( ph /\ A e. NN0 ) -> ( S ` A ) G A )
Theorem	heiborlem5 33614*	Lemma for heibor 33620. The function M is a set of point-and-radius pairs suitable for application to caubl 23106. (Contributed by Jeff Madsen, 23-Jan-2014.)
|- J = ( MetOpen ` D )   &    |- K = { u | -. E. v e. ( ~P U i^i Fin ) u C_ U. v }   &    |- G = { <. y , n >. | ( n e. NN0 /\ y e. ( F ` n ) /\ ( y B n ) e. K ) }   &    |- B = ( z e. X , m e. NN0 |-> ( z ( ball ` D ) ( 1 / ( 2 ^ m ) ) ) )   &    |- ( ph -> D e. ( CMet ` X ) )   &    |- ( ph -> F : NN0 --> ( ~P X i^i Fin ) )   &    |- ( ph -> A. n e. NN0 X = U_ y e. ( F ` n ) ( y B n ) )   &    |- ( ph -> A. x e. G ( ( T ` x ) G ( ( 2nd ` x ) + 1 ) /\ ( ( B ` x ) i^i ( ( T ` x ) B ( ( 2nd ` x ) + 1 ) ) ) e. K ) )   &    |- ( ph -> C G 0 )   &    |- S = seq 0 ( T , ( m e. NN0 |-> if ( m = 0 , C , ( m - 1 ) ) ) )   &    |- M = ( n e. NN |-> <. ( S ` n ) , ( 3 / ( 2 ^ n ) ) >. )   =>    |- ( ph -> M : NN --> ( X X. RR+ ) )
Theorem	heiborlem6 33615*	Lemma for heibor 33620. Since the sequence of balls connected by the function T ensures that each ball nontrivially intersects with the next (since the empty set has a finite subcover, the intersection of any two successive balls in the sequence is nonempty), and each ball is half the size of the previous one, the distance between the centers is at most 3 / 2 times the size of the larger, and so if we expand each ball by a factor of 3 we get a nested sequence of balls. (Contributed by Jeff Madsen, 23-Jan-2014.)
|- J = ( MetOpen ` D )   &    |- K = { u | -. E. v e. ( ~P U i^i Fin ) u C_ U. v }   &    |- G = { <. y , n >. | ( n e. NN0 /\ y e. ( F ` n ) /\ ( y B n ) e. K ) }   &    |- B = ( z e. X , m e. NN0 |-> ( z ( ball ` D ) ( 1 / ( 2 ^ m ) ) ) )   &    |- ( ph -> D e. ( CMet ` X ) )   &    |- ( ph -> F : NN0 --> ( ~P X i^i Fin ) )   &    |- ( ph -> A. n e. NN0 X = U_ y e. ( F ` n ) ( y B n ) )   &    |- ( ph -> A. x e. G ( ( T ` x ) G ( ( 2nd ` x ) + 1 ) /\ ( ( B ` x ) i^i ( ( T ` x ) B ( ( 2nd ` x ) + 1 ) ) ) e. K ) )   &    |- ( ph -> C G 0 )   &    |- S = seq 0 ( T , ( m e. NN0 |-> if ( m = 0 , C , ( m - 1 ) ) ) )   &    |- M = ( n e. NN |-> <. ( S ` n ) , ( 3 / ( 2 ^ n ) ) >. )   =>    |- ( ph -> A. k e. NN ( ( ball ` D ) ` ( M ` ( k + 1 ) ) ) C_ ( ( ball ` D ) ` ( M ` k ) ) )
Theorem	heiborlem7 33616*	Lemma for heibor 33620. Since the sizes of the balls decrease exponentially, the sequence converges to zero. (Contributed by Jeff Madsen, 23-Jan-2014.)
|- J = ( MetOpen ` D )   &    |- K = { u | -. E. v e. ( ~P U i^i Fin ) u C_ U. v }   &    |- G = { <. y , n >. | ( n e. NN0 /\ y e. ( F ` n ) /\ ( y B n ) e. K ) }   &    |- B = ( z e. X , m e. NN0 |-> ( z ( ball ` D ) ( 1 / ( 2 ^ m ) ) ) )   &    |- ( ph -> D e. ( CMet ` X ) )   &    |- ( ph -> F : NN0 --> ( ~P X i^i Fin ) )   &    |- ( ph -> A. n e. NN0 X = U_ y e. ( F ` n ) ( y B n ) )   &    |- ( ph -> A. x e. G ( ( T ` x ) G ( ( 2nd ` x ) + 1 ) /\ ( ( B ` x ) i^i ( ( T ` x ) B ( ( 2nd ` x ) + 1 ) ) ) e. K ) )   &    |- ( ph -> C G 0 )   &    |- S = seq 0 ( T , ( m e. NN0 |-> if ( m = 0 , C , ( m - 1 ) ) ) )   &    |- M = ( n e. NN |-> <. ( S ` n ) , ( 3 / ( 2 ^ n ) ) >. )   =>    |- A. r e. RR+ E. k e. NN ( 2nd ` ( M ` k ) ) < r
Theorem	heiborlem8 33617*	Lemma for heibor 33620. The previous lemmas establish that the sequence M is Cauchy, so using completeness we now consider the convergent point Y. By assumption, U is an open cover, so Y is an element of some Z e. U, and some ball centered at Y is contained in Z. But the sequence contains arbitrarily small balls close to Y, so some element ball ( M ` n ) of the sequence is contained in Z. And finally we arrive at a contradiction, because { Z } is a finite subcover of U that covers ball ( M ` n ), yet ball ( M ` n ) e. K. For convenience, we write this contradiction as ph -> ps where ph is all the accumulated hypotheses and ps is anything at all. (Contributed by Jeff Madsen, 22-Jan-2014.)
|- J = ( MetOpen ` D )   &    |- K = { u | -. E. v e. ( ~P U i^i Fin ) u C_ U. v }   &    |- G = { <. y , n >. | ( n e. NN0 /\ y e. ( F ` n ) /\ ( y B n ) e. K ) }   &    |- B = ( z e. X , m e. NN0 |-> ( z ( ball ` D ) ( 1 / ( 2 ^ m ) ) ) )   &    |- ( ph -> D e. ( CMet ` X ) )   &    |- ( ph -> F : NN0 --> ( ~P X i^i Fin ) )   &    |- ( ph -> A. n e. NN0 X = U_ y e. ( F ` n ) ( y B n ) )   &    |- ( ph -> A. x e. G ( ( T ` x ) G ( ( 2nd ` x ) + 1 ) /\ ( ( B ` x ) i^i ( ( T ` x ) B ( ( 2nd ` x ) + 1 ) ) ) e. K ) )   &    |- ( ph -> C G 0 )   &    |- S = seq 0 ( T , ( m e. NN0 |-> if ( m = 0 , C , ( m - 1 ) ) ) )   &    |- M = ( n e. NN |-> <. ( S ` n ) , ( 3 / ( 2 ^ n ) ) >. )   &    |- ( ph -> U C_ J )   &    |- Y e. _V   &    |- ( ph -> Y e. Z )   &    |- ( ph -> Z e. U )   &    |- ( ph -> ( 1st o. M ) ( ~~> t ` J ) Y )   =>    |- ( ph -> ps )
Theorem	heiborlem9 33618*	Lemma for heibor 33620. Discharge the hypotheses of heiborlem8 33617 by applying caubl 23106 to get a convergent point and adding the open cover assumption. (Contributed by Jeff Madsen, 20-Jan-2014.)
|- J = ( MetOpen ` D )   &    |- K = { u | -. E. v e. ( ~P U i^i Fin ) u C_ U. v }   &    |- G = { <. y , n >. | ( n e. NN0 /\ y e. ( F ` n ) /\ ( y B n ) e. K ) }   &    |- B = ( z e. X , m e. NN0 |-> ( z ( ball ` D ) ( 1 / ( 2 ^ m ) ) ) )   &    |- ( ph -> D e. ( CMet ` X ) )   &    |- ( ph -> F : NN0 --> ( ~P X i^i Fin ) )   &    |- ( ph -> A. n e. NN0 X = U_ y e. ( F ` n ) ( y B n ) )   &    |- ( ph -> A. x e. G ( ( T ` x ) G ( ( 2nd ` x ) + 1 ) /\ ( ( B ` x ) i^i ( ( T ` x ) B ( ( 2nd ` x ) + 1 ) ) ) e. K ) )   &    |- ( ph -> C G 0 )   &    |- S = seq 0 ( T , ( m e. NN0 |-> if ( m = 0 , C , ( m - 1 ) ) ) )   &    |- M = ( n e. NN |-> <. ( S ` n ) , ( 3 / ( 2 ^ n ) ) >. )   &    |- ( ph -> U C_ J )   &    |- ( ph -> U. U = X )   =>    |- ( ph -> ps )
Theorem	heiborlem10 33619*	Lemma for heibor 33620. The last remaining piece of the proof is to find an element C such that C G 0, i.e. C is an element of ( F ` 0 ) that has no finite subcover, which is true by heiborlem1 33610, since ( F ` 0 ) is a finite cover of X, which has no finite subcover. Thus, the rest of the proof follows to a contradiction, and thus there must be a finite subcover of U that covers X, i.e. X is compact. (Contributed by Jeff Madsen, 22-Jan-2014.)
|- J = ( MetOpen ` D )   &    |- K = { u | -. E. v e. ( ~P U i^i Fin ) u C_ U. v }   &    |- G = { <. y , n >. | ( n e. NN0 /\ y e. ( F ` n ) /\ ( y B n ) e. K ) }   &    |- B = ( z e. X , m e. NN0 |-> ( z ( ball ` D ) ( 1 / ( 2 ^ m ) ) ) )   &    |- ( ph -> D e. ( CMet ` X ) )   &    |- ( ph -> F : NN0 --> ( ~P X i^i Fin ) )   &    |- ( ph -> A. n e. NN0 X = U_ y e. ( F ` n ) ( y B n ) )   =>    |- ( ( ph /\ ( U C_ J /\ U. J = U. U ) ) -> E. v e. ( ~P U i^i Fin ) U. J = U. v )
Theorem	heibor 33620	Generalized Heine-Borel Theorem. A metric space is compact iff it is complete and totally bounded. See heibor1 33609 and heiborlem1 33610 for a description of the proof. (Contributed by Jeff Madsen, 2-Sep-2009.) (Revised by Mario Carneiro, 28-Jan-2014.)
|- J = ( MetOpen ` D )   =>    |- ( ( D e. ( Met ` X ) /\ J e. Comp ) <-> ( D e. ( CMet ` X ) /\ D e. ( TotBnd ` X ) ) )
20.19.10  Banach Fixed Point Theorem
Theorem	bfplem1 33621*	Lemma for bfp 33623. The sequence G, which simply starts from any point in the space and iterates F, satisfies the property that the distance from G ( n ) to G ( n + 1 ) decreases by at least K after each step. Thus, the total distance from any G ( i ) to G ( j ) is bounded by a geometric series, and the sequence is Cauchy. Therefore, it converges to a point ( ( ~~> t ` J ) ` G ) since the space is complete. (Contributed by Jeff Madsen, 17-Jun-2014.)
|- ( ph -> D e. ( CMet ` X ) )   &    |- ( ph -> X =/= (/) )   &    |- ( ph -> K e. RR+ )   &    |- ( ph -> K < 1 )   &    |- ( ph -> F : X --> X )   &    |- ( ( ph /\ ( x e. X /\ y e. X ) ) -> ( ( F ` x ) D ( F ` y ) ) <_ ( K x. ( x D y ) ) )   &    |- J = ( MetOpen ` D )   &    |- ( ph -> A e. X )   &    |- G = seq 1 ( ( F o. 1st ) , ( NN X. { A } ) )   =>    |- ( ph -> G ( ~~> t ` J ) ( ( ~~> t ` J ) ` G ) )
Theorem	bfplem2 33622*	Lemma for bfp 33623. Using the point found in bfplem1 33621, we show that this convergent point is a fixed point of F. Since for any positive x, the sequence G is in B ( x / 2 , P ) for all k e. ( ZZ>= ` j ) (where P = ( ( ~~> t ` J ) ` G )), we have D ( G ( j + 1 ) , F ( P ) ) <_ D ( G ( j ) , P ) < x / 2 and D ( G ( j + 1 ) , P ) < x / 2, so F ( P ) is in every neighborhood of P and P is a fixed point of F. (Contributed by Jeff Madsen, 5-Jun-2014.)
|- ( ph -> D e. ( CMet ` X ) )   &    |- ( ph -> X =/= (/) )   &    |- ( ph -> K e. RR+ )   &    |- ( ph -> K < 1 )   &    |- ( ph -> F : X --> X )   &    |- ( ( ph /\ ( x e. X /\ y e. X ) ) -> ( ( F ` x ) D ( F ` y ) ) <_ ( K x. ( x D y ) ) )   &    |- J = ( MetOpen ` D )   &    |- ( ph -> A e. X )   &    |- G = seq 1 ( ( F o. 1st ) , ( NN X. { A } ) )   =>    |- ( ph -> E. z e. X ( F ` z ) = z )
Theorem	bfp 33623*	Banach fixed point theorem, also known as contraction mapping theorem. A contraction on a complete metric space has a unique fixed point. We show existence in the lemmas, and uniqueness here - if F has two fixed points, then the distance between them is less than K times itself, a contradiction. (Contributed by Jeff Madsen, 2-Sep-2009.) (Proof shortened by Mario Carneiro, 5-Jun-2014.)
|- ( ph -> D e. ( CMet ` X ) )   &    |- ( ph -> X =/= (/) )   &    |- ( ph -> K e. RR+ )   &    |- ( ph -> K < 1 )   &    |- ( ph -> F : X --> X )   &    |- ( ( ph /\ ( x e. X /\ y e. X ) ) -> ( ( F ` x ) D ( F ` y ) ) <_ ( K x. ( x D y ) ) )   =>    |- ( ph -> E! z e. X ( F ` z ) = z )
20.19.11  Euclidean space
Syntax	crrn 33624	Extend class notation with the n-dimensional Euclidean space.
class Rn
Definition	df-rrn 33625*	Define n-dimensional Euclidean space as a metric space with the standard Euclidean norm given by the quadratic mean. (Contributed by Jeff Madsen, 2-Sep-2009.)
|- Rn = ( i e. Fin |-> ( x e. ( RR ^m i ) , y e. ( RR ^m i ) |-> ( sqr ` sum_ k e. i ( ( ( x ` k ) - ( y ` k ) ) ^ 2 ) ) ) )
Theorem	rrnval 33626*	The n-dimensional Euclidean space. (Contributed by Jeff Madsen, 2-Sep-2009.) (Revised by Mario Carneiro, 13-Sep-2015.)
|- X = ( RR ^m I )   =>    |- ( I e. Fin -> ( Rn ` I ) = ( x e. X , y e. X |-> ( sqr ` sum_ k e. I ( ( ( x ` k ) - ( y ` k ) ) ^ 2 ) ) ) )
Theorem	rrnmval 33627*	The value of the Euclidean metric. (Contributed by Jeff Madsen, 2-Sep-2009.) (Revised by Mario Carneiro, 13-Sep-2015.)
|- X = ( RR ^m I )   =>    |- ( ( I e. Fin /\ F e. X /\ G e. X ) -> ( F ( Rn ` I ) G ) = ( sqr ` sum_ k e. I ( ( ( F ` k ) - ( G ` k ) ) ^ 2 ) ) )
Theorem	rrnmet 33628	Euclidean space is a metric space. (Contributed by Jeff Madsen, 2-Sep-2009.) (Proof shortened by Mario Carneiro, 5-Jun-2014.)
|- X = ( RR ^m I )   =>    |- ( I e. Fin -> ( Rn ` I ) e. ( Met ` X ) )
Theorem	rrndstprj1 33629	The distance between two points in Euclidean space is greater than the distance between the projections onto one coordinate. (Contributed by Jeff Madsen, 2-Sep-2009.) (Revised by Mario Carneiro, 13-Sep-2015.)
|- X = ( RR ^m I )   &    |- M = ( ( abs o. - ) |` ( RR X. RR ) )   =>    |- ( ( ( I e. Fin /\ A e. I ) /\ ( F e. X /\ G e. X ) ) -> ( ( F ` A ) M ( G ` A ) ) <_ ( F ( Rn ` I ) G ) )
Theorem	rrndstprj2 33630*	Bound on the distance between two points in Euclidean space given bounds on the distances in each coordinate. This theorem and rrndstprj1 33629 can be used to show that the supremum norm and Euclidean norm are equivalent. (Contributed by Jeff Madsen, 2-Sep-2009.) (Revised by Mario Carneiro, 13-Sep-2015.)
|- X = ( RR ^m I )   &    |- M = ( ( abs o. - ) |` ( RR X. RR ) )   =>    |- ( ( ( I e. ( Fin \ { (/) } ) /\ F e. X /\ G e. X ) /\ ( R e. RR+ /\ A. n e. I ( ( F ` n ) M ( G ` n ) ) < R ) ) -> ( F ( Rn ` I ) G ) < ( R x. ( sqr ` ( # ` I ) ) ) )
Theorem	rrncmslem 33631*	Lemma for rrncms 33632. (Contributed by Jeff Madsen, 6-Jun-2014.) (Revised by Mario Carneiro, 13-Sep-2015.)
|- X = ( RR ^m I )   &    |- M = ( ( abs o. - ) |` ( RR X. RR ) )   &    |- J = ( MetOpen ` ( Rn ` I ) )   &    |- ( ph -> I e. Fin )   &    |- ( ph -> F e. ( Cau ` ( Rn ` I ) ) )   &    |- ( ph -> F : NN --> X )   &    |- P = ( m e. I |-> ( ~~> ` ( t e. NN |-> ( ( F ` t ) ` m ) ) ) )   =>    |- ( ph -> F e. dom ( ~~> t ` J ) )
Theorem	rrncms 33632	Euclidean space is complete. (Contributed by Jeff Madsen, 2-Sep-2009.) (Revised by Mario Carneiro, 13-Sep-2015.)
|- X = ( RR ^m I )   =>    |- ( I e. Fin -> ( Rn ` I ) e. ( CMet ` X ) )
Theorem	repwsmet 33633	The supremum metric on RR ^ I is a metric. (Contributed by Jeff Madsen, 15-Sep-2015.)
|- Y = ( (ℂfld ↾s RR ) ^s I )   &    |- D = ( dist ` Y )   &    |- X = ( RR ^m I )   =>    |- ( I e. Fin -> D e. ( Met ` X ) )
Theorem	rrnequiv 33634	The supremum metric on RR ^ I is equivalent to the Rn metric. (Contributed by Jeff Madsen, 15-Sep-2015.)
|- Y = ( (ℂfld ↾s RR ) ^s I )   &    |- D = ( dist ` Y )   &    |- X = ( RR ^m I )   &    |- ( ph -> I e. Fin )   =>    |- ( ( ph /\ ( F e. X /\ G e. X ) ) -> ( ( F D G ) <_ ( F ( Rn ` I ) G ) /\ ( F ( Rn ` I ) G ) <_ ( ( sqr ` ( # ` I ) ) x. ( F D G ) ) ) )
Theorem	rrntotbnd 33635	A set in Euclidean space is totally bounded iff its is bounded. (Contributed by Jeff Madsen, 2-Sep-2009.) (Revised by Mario Carneiro, 16-Sep-2015.)
|- X = ( RR ^m I )   &    |- M = ( ( Rn ` I ) |` ( Y X. Y ) )   =>    |- ( I e. Fin -> ( M e. ( TotBnd ` Y ) <-> M e. ( Bnd ` Y ) ) )
Theorem	rrnheibor 33636	Heine-Borel theorem for Euclidean space. A subset of Euclidean space is compact iff it is closed and bounded. (Contributed by Jeff Madsen, 2-Sep-2009.) (Revised by Mario Carneiro, 22-Sep-2015.)
|- X = ( RR ^m I )   &    |- M = ( ( Rn ` I ) |` ( Y X. Y ) )   &    |- T = ( MetOpen ` M )   &    |- U = ( MetOpen ` ( Rn ` I ) )   =>    |- ( ( I e. Fin /\ Y C_ X ) -> ( T e. Comp <-> ( Y e. ( Clsd ` U ) /\ M e. ( Bnd ` Y ) ) ) )
20.19.12  Intervals (continued)
Theorem	ismrer1 33637*	An isometry between RR and RR ^ 1. (Contributed by Jeff Madsen, 2-Sep-2009.) (Revised by Mario Carneiro, 22-Sep-2015.)
|- R = ( ( abs o. - ) |` ( RR X. RR ) )   &    |- F = ( x e. RR |-> ( { A } X. { x } ) )   =>    |- ( A e. V -> F e. ( R Ismty ( Rn ` { A } ) ) )
Theorem	reheibor 33638	Heine-Borel theorem for real numbers. A subset of RR is compact iff it is closed and bounded. (Contributed by Jeff Madsen, 2-Sep-2009.) (Revised by Mario Carneiro, 22-Sep-2015.)
|- M = ( ( abs o. - ) |` ( Y X. Y ) )   &    |- T = ( MetOpen ` M )   &    |- U = ( topGen ` ran (,) )   =>    |- ( Y C_ RR -> ( T e. Comp <-> ( Y e. ( Clsd ` U ) /\ M e. ( Bnd ` Y ) ) ) )
Theorem	iccbnd 33639	A closed interval in RR is bounded. (Contributed by Jeff Madsen, 2-Sep-2009.) (Proof shortened by Mario Carneiro, 22-Sep-2015.)
|- J = ( A [,] B )   &    |- M = ( ( abs o. - ) |` ( J X. J ) )   =>    |- ( ( A e. RR /\ B e. RR ) -> M e. ( Bnd ` J ) )
Theorem	icccmpALT 33640	A closed interval in RR is compact. Alternate proof of icccmp 22628 using the Heine-Borel theorem heibor 33620. (Contributed by Jeff Madsen, 2-Sep-2009.) (Proof shortened by Mario Carneiro, 14-Aug-2014.) (New usage is discouraged.) (Proof modification is discouraged.)
|- J = ( A [,] B )   &    |- M = ( ( abs o. - ) |` ( J X. J ) )   &    |- T = ( MetOpen ` M )   =>    |- ( ( A e. RR /\ B e. RR ) -> T e. Comp )
20.19.13  Operation properties
Syntax	cass 33641	Extend class notation with a device to add associativity to internal operations.
class Ass
Definition	df-ass 33642*	A device to add associativity to various sorts of internal operations. The definition is meaningful when g is a magma at least. (Contributed by FL, 1-Nov-2009.) (New usage is discouraged.)
|- Ass = { g | A. x e. dom dom g A. y e. dom dom g A. z e. dom dom g ( ( x g y ) g z ) = ( x g ( y g z ) ) }
Syntax	cexid 33643	Extend class notation with the class of all the internal operations with an identity element.
class ExId
Definition	df-exid 33644*	A device to add an identity element to various sorts of internal operations. (Contributed by FL, 2-Nov-2009.) (New usage is discouraged.)
|- ExId = { g | E. x e. dom dom g A. y e. dom dom g ( ( x g y ) = y /\ ( y g x ) = y ) }
Theorem	isass 33645*	The predicate "is an associative operation". (Contributed by FL, 1-Nov-2009.) (New usage is discouraged.)
|- X = dom dom G   =>    |- ( G e. A -> ( G e. Ass <-> A. x e. X A. y e. X A. z e. X ( ( x G y ) G z ) = ( x G ( y G z ) ) ) )
Theorem	isexid 33646*	The predicate G has a left and right identity element. (Contributed by FL, 2-Nov-2009.) (Revised by Mario Carneiro, 22-Dec-2013.) (New usage is discouraged.)
|- X = dom dom G   =>    |- ( G e. A -> ( G e. ExId <-> E. x e. X A. y e. X ( ( x G y ) = y /\ ( y G x ) = y ) ) )
20.19.14  Groups and related structures
Syntax	cmagm 33647	Extend class notation with the class of all magmas.
class Magma
Definition	df-mgmOLD 33648*	Obsolete version of df-mgm 17242 as of 3-Feb-2020. A magma is a binary internal operation. (Contributed by FL, 2-Nov-2009.) (New usage is discouraged.)
|- Magma = { g | E. t g : ( t X. t ) --> t }
Theorem	ismgmOLD 33649	Obsolete version of ismgm 17243 as of 3-Feb-2020. The predicate "is a magma". (Contributed by FL, 2-Nov-2009.) (New usage is discouraged.) (Proof modification is discouraged.)
|- X = dom dom G   =>    |- ( G e. A -> ( G e. Magma <-> G : ( X X. X ) --> X ) )
Theorem	clmgmOLD 33650	Obsolete version of mgmcl 17245 as of 3-Feb-2020. Closure of a magma. (Contributed by FL, 14-Sep-2010.) (New usage is discouraged.) (Proof modification is discouraged.)
|- X = dom dom G   =>    |- ( ( G e. Magma /\ A e. X /\ B e. X ) -> ( A G B ) e. X )
Theorem	opidonOLD 33651	Obsolete version of mndpfo 17314 as of 23-Jan-2020. An operation with a left and right identity element is onto. (Contributed by FL, 2-Nov-2009.) (Revised by Mario Carneiro, 22-Dec-2013.) (New usage is discouraged.) (Proof modification is discouraged.)
|- X = dom dom G   =>    |- ( G e. ( Magma i^i ExId ) -> G : ( X X. X ) -onto-> X )
Theorem	rngopidOLD 33652	Obsolete version of mndpfo 17314 as of 23-Jan-2020. Range of an operation with a left and right identity element. (Contributed by FL, 2-Nov-2009.) (New usage is discouraged.) (Proof modification is discouraged.)
|- ( G e. ( Magma i^i ExId ) -> ran G = dom dom G )
Theorem	opidon2OLD 33653	Obsolete version of mndpfo 17314 as of 23-Jan-2020. An operation with a left and right identity element is onto. (Contributed by FL, 2-Nov-2009.) (New usage is discouraged.) (Proof modification is discouraged.)
|- X = ran G   =>    |- ( G e. ( Magma i^i ExId ) -> G : ( X X. X ) -onto-> X )
Theorem	isexid2 33654*	If G e. ( Magma i^i ExId ), then it has a left and right identity element that belongs to the range of the operation. (Contributed by FL, 12-Dec-2009.) (Revised by Mario Carneiro, 22-Dec-2013.) (New usage is discouraged.)
|- X = ran G   =>    |- ( G e. ( Magma i^i ExId ) -> E. u e. X A. x e. X ( ( u G x ) = x /\ ( x G u ) = x ) )
Theorem	exidu1 33655*	Unicity of the left and right identity element of a magma when it exists. (Contributed by FL, 12-Dec-2009.) (Revised by Mario Carneiro, 22-Dec-2013.) (New usage is discouraged.)
|- X = ran G   =>    |- ( G e. ( Magma i^i ExId ) -> E! u e. X A. x e. X ( ( u G x ) = x /\ ( x G u ) = x ) )
Theorem	idrval 33656*	The value of the identity element. (Contributed by FL, 12-Dec-2009.) (Revised by Mario Carneiro, 22-Dec-2013.) (New usage is discouraged.)
|- X = ran G   &    |- U = (GId ` G )   =>    |- ( G e. A -> U = ( iota_ u e. X A. x e. X ( ( u G x ) = x /\ ( x G u ) = x ) ) )
Theorem	iorlid 33657	A magma right and left identity belongs to the underlying set of the operation. (Contributed by FL, 12-Dec-2009.) (Revised by Mario Carneiro, 22-Dec-2013.) (New usage is discouraged.)
|- X = ran G   &    |- U = (GId ` G )   =>    |- ( G e. ( Magma i^i ExId ) -> U e. X )
Theorem	cmpidelt 33658	A magma right and left identity element keeps the other elements unchanged. (Contributed by FL, 12-Dec-2009.) (Revised by Mario Carneiro, 22-Dec-2013.) (New usage is discouraged.)
|- X = ran G   &    |- U = (GId ` G )   =>    |- ( ( G e. ( Magma i^i ExId ) /\ A e. X ) -> ( ( U G A ) = A /\ ( A G U ) = A ) )
Syntax	csem 33659	Extend class notation with the class of all semi-groups.
class SemiGrp
Definition	df-sgrOLD 33660	Obsolete version of df-sgrp 17284 as of 3-Feb-2020. A semi-group is an associative magma. (Contributed by FL, 2-Nov-2009.) (New usage is discouraged.)
|- SemiGrp = ( Magma i^i Ass )
Theorem	smgrpismgmOLD 33661	Obsolete version of sgrpmgm 17289 as of 3-Feb-2020. A semi-group is a magma. (Contributed by FL, 2-Nov-2009.) (New usage is discouraged.) (Proof modification is discouraged.)
|- ( G e. SemiGrp -> G e. Magma )
Theorem	issmgrpOLD 33662*	Obsolete version of issgrp 17285 as of 3-Feb-2020. The predicate "is a semi-group". (Contributed by FL, 2-Nov-2009.) (New usage is discouraged.) (Proof modification is discouraged.)
|- X = dom dom G   =>    |- ( G e. A -> ( G e. SemiGrp <-> ( G : ( X X. X ) --> X /\ A. x e. X A. y e. X A. z e. X ( ( x G y ) G z ) = ( x G ( y G z ) ) ) ) )
Theorem	smgrpmgm 33663	A semi-group is a magma. (Contributed by FL, 2-Nov-2009.) (New usage is discouraged.)
|- X = dom dom G   =>    |- ( G e. SemiGrp -> G : ( X X. X ) --> X )
Theorem	smgrpassOLD 33664*	Obsolete version of sgrpass 17290 as of 3-Feb-2020. A semi-group is associative. (Contributed by FL, 2-Nov-2009.) (New usage is discouraged.) (Proof modification is discouraged.)
|- X = dom dom G   =>    |- ( G e. SemiGrp -> A. x e. X A. y e. X A. z e. X ( ( x G y ) G z ) = ( x G ( y G z ) ) )
Syntax	cmndo 33665	Extend class notation with the class of all monoids.
class MndOp
Definition	df-mndo 33666	A monoid is a semi-group with an identity element. (Contributed by FL, 2-Nov-2009.) (New usage is discouraged.)
|- MndOp = ( SemiGrp i^i ExId )
Theorem	mndoissmgrpOLD 33667	Obsolete version of mndsgrp 17299 as of 3-Feb-2020. A monoid is a semi-group. (Contributed by FL, 2-Nov-2009.) (New usage is discouraged.) (Proof modification is discouraged.)
|- ( G e. MndOp -> G e. SemiGrp )
Theorem	mndoisexid 33668	A monoid has an identity element. (Contributed by FL, 2-Nov-2009.) (New usage is discouraged.)
|- ( G e. MndOp -> G e. ExId )
Theorem	mndoismgmOLD 33669	Obsolete version of mndmgm 17300 as of 3-Feb-2020. A monoid is a magma. (Contributed by FL, 2-Nov-2009.) (New usage is discouraged.) (Proof modification is discouraged.)
|- ( G e. MndOp -> G e. Magma )
Theorem	mndomgmid 33670	A monoid is a magma with an identity element. (Contributed by FL, 18-Feb-2010.) (New usage is discouraged.)
|- ( G e. MndOp -> G e. ( Magma i^i ExId ) )
Theorem	ismndo 33671*	The predicate "is a monoid". (Contributed by FL, 2-Nov-2009.) (Revised by Mario Carneiro, 22-Dec-2013.) (New usage is discouraged.)
|- X = dom dom G   =>    |- ( G e. A -> ( G e. MndOp <-> ( G e. SemiGrp /\ E. x e. X A. y e. X ( ( x G y ) = y /\ ( y G x ) = y ) ) ) )
Theorem	ismndo1 33672*	The predicate "is a monoid". (Contributed by FL, 2-Nov-2009.) (Revised by Mario Carneiro, 22-Dec-2013.) (New usage is discouraged.)
|- X = dom dom G   =>    |- ( G e. A -> ( G e. MndOp <-> ( G : ( X X. X ) --> X /\ A. x e. X A. y e. X A. z e. X ( ( x G y ) G z ) = ( x G ( y G z ) ) /\ E. x e. X A. y e. X ( ( x G y ) = y /\ ( y G x ) = y ) ) ) )
Theorem	ismndo2 33673*	The predicate "is a monoid". (Contributed by FL, 2-Nov-2009.) (Revised by Mario Carneiro, 22-Dec-2013.) (New usage is discouraged.)
|- X = ran G   =>    |- ( G e. A -> ( G e. MndOp <-> ( G : ( X X. X ) --> X /\ A. x e. X A. y e. X A. z e. X ( ( x G y ) G z ) = ( x G ( y G z ) ) /\ E. x e. X A. y e. X ( ( x G y ) = y /\ ( y G x ) = y ) ) ) )
Theorem	grpomndo 33674	A group is a monoid. (Contributed by FL, 2-Nov-2009.) (Revised by Mario Carneiro, 22-Dec-2013.) (New usage is discouraged.)
|- ( G e. GrpOp -> G e. MndOp )
Theorem	exidcl 33675	Closure of the binary operation of a magma with identity. (Contributed by Jeff Madsen, 16-Jun-2011.)
|- X = ran G   =>    |- ( ( G e. ( Magma i^i ExId ) /\ A e. X /\ B e. X ) -> ( A G B ) e. X )
Theorem	exidreslem 33676*	Lemma for exidres 33677 and exidresid 33678. (Contributed by Jeff Madsen, 8-Jun-2010.) (Revised by Mario Carneiro, 23-Dec-2013.)
|- X = ran G   &    |- U = (GId ` G )   &    |- H = ( G |` ( Y X. Y ) )   =>    |- ( ( G e. ( Magma i^i ExId ) /\ Y C_ X /\ U e. Y ) -> ( U e. dom dom H /\ A. x e. dom dom H ( ( U H x ) = x /\ ( x H U ) = x ) ) )
Theorem	exidres 33677	The restriction of a binary operation with identity to a subset containing the identity has an identity element. (Contributed by Jeff Madsen, 8-Jun-2010.) (Revised by Mario Carneiro, 23-Dec-2013.)
|- X = ran G   &    |- U = (GId ` G )   &    |- H = ( G |` ( Y X. Y ) )   =>    |- ( ( G e. ( Magma i^i ExId ) /\ Y C_ X /\ U e. Y ) -> H e. ExId )
Theorem	exidresid 33678	The restriction of a binary operation with identity to a subset containing the identity has the same identity element. (Contributed by Jeff Madsen, 8-Jun-2010.) (Revised by Mario Carneiro, 23-Dec-2013.)
|- X = ran G   &    |- U = (GId ` G )   &    |- H = ( G |` ( Y X. Y ) )   =>    |- ( ( ( G e. ( Magma i^i ExId ) /\ Y C_ X /\ U e. Y ) /\ H e. Magma ) -> (GId ` H ) = U )
Theorem	ablo4pnp 33679	A commutative/associative law for Abelian groups. (Contributed by Jeff Madsen, 11-Jun-2010.)
|- X = ran G   &    |- D = ( /g ` G )   =>    |- ( ( G e. AbelOp /\ ( ( A e. X /\ B e. X ) /\ ( C e. X /\ F e. X ) ) ) -> ( ( A G B ) D ( C G F ) ) = ( ( A D C ) G ( B D F ) ) )
Theorem	grpoeqdivid 33680	Two group elements are equal iff their quotient is the identity. (Contributed by Jeff Madsen, 6-Jan-2011.)
|- X = ran G   &    |- U = (GId ` G )   &    |- D = ( /g ` G )   =>    |- ( ( G e. GrpOp /\ A e. X /\ B e. X ) -> ( A = B <-> ( A D B ) = U ) )
Theorem	grposnOLD 33681	The group operation for the singleton group. Obsolete, use grp1 17522. instead (Contributed by NM, 4-Nov-2006.) (New usage is discouraged.) (Proof modification is discouraged.)
|- A e. _V   =>    |- { <. <. A , A >. , A >. } e. GrpOp
20.19.15  Group homomorphism and isomorphism
Syntax	cghomOLD 33682	Obsolete version of cghm 17657 as of 15-Mar-2020. Extend class notation to include the class of group homomorphisms. (New usage is discouraged.)
class GrpOpHom
Definition	df-ghomOLD 33683*	Obsolete version of df-ghm 17658 as of 15-Mar-2020. Define the set of group homomorphisms from g to h. (Contributed by Paul Chapman, 25-Feb-2008.) (New usage is discouraged.)
|- GrpOpHom = ( g e. GrpOp , h e. GrpOp |-> { f | ( f : ran g --> ran h /\ A. x e. ran g A. y e. ran g ( ( f ` x ) h ( f ` y ) ) = ( f ` ( x g y ) ) ) } )
Theorem	elghomlem1OLD 33684*	Obsolete as of 15-Mar-2020. Lemma for elghomOLD 33686. (Contributed by Paul Chapman, 25-Feb-2008.) (New usage is discouraged.) (Proof modification is discouraged.)
|- S = { f | ( f : ran G --> ran H /\ A. x e. ran G A. y e. ran G ( ( f ` x ) H ( f ` y ) ) = ( f ` ( x G y ) ) ) }   =>    |- ( ( G e. GrpOp /\ H e. GrpOp ) -> ( G GrpOpHom H ) = S )
Theorem	elghomlem2OLD 33685*	Obsolete as of 15-Mar-2020. Lemma for elghomOLD 33686. (Contributed by Paul Chapman, 25-Feb-2008.) (New usage is discouraged.) (Proof modification is discouraged.)
|- S = { f | ( f : ran G --> ran H /\ A. x e. ran G A. y e. ran G ( ( f ` x ) H ( f ` y ) ) = ( f ` ( x G y ) ) ) }   =>    |- ( ( G e. GrpOp /\ H e. GrpOp ) -> ( F e. ( G GrpOpHom H ) <-> ( F : ran G --> ran H /\ A. x e. ran G A. y e. ran G ( ( F ` x ) H ( F ` y ) ) = ( F ` ( x G y ) ) ) ) )
Theorem	elghomOLD 33686*	Obsolete version of isghm 17660 as of 15-Mar-2020. Membership in the set of group homomorphisms from G to H. (Contributed by Paul Chapman, 3-Mar-2008.) (New usage is discouraged.) (Proof modification is discouraged.)
|- X = ran G   &    |- W = ran H   =>    |- ( ( G e. GrpOp /\ H e. GrpOp ) -> ( F e. ( G GrpOpHom H ) <-> ( F : X --> W /\ A. x e. X A. y e. X ( ( F ` x ) H ( F ` y ) ) = ( F ` ( x G y ) ) ) ) )
Theorem	ghomlinOLD 33687	Obsolete version of ghmlin 17665 as of 15-Mar-2020. Linearity of a group homomorphism. (Contributed by Paul Chapman, 3-Mar-2008.) (New usage is discouraged.) (Proof modification is discouraged.)
|- X = ran G   =>    |- ( ( ( G e. GrpOp /\ H e. GrpOp /\ F e. ( G GrpOpHom H ) ) /\ ( A e. X /\ B e. X ) ) -> ( ( F ` A ) H ( F ` B ) ) = ( F ` ( A G B ) ) )
Theorem	ghomidOLD 33688	Obsolete version of ghmid 17666 as of 15-Mar-2020. A group homomorphism maps identity element to identity element. (Contributed by Paul Chapman, 3-Mar-2008.) (New usage is discouraged.) (Proof modification is discouraged.)
|- U = (GId ` G )   &    |- T = (GId ` H )   =>    |- ( ( G e. GrpOp /\ H e. GrpOp /\ F e. ( G GrpOpHom H ) ) -> ( F ` U ) = T )
Theorem	ghomf 33689	Mapping property of a group homomorphism. (Contributed by Jeff Madsen, 1-Dec-2009.)
|- X = ran G   &    |- W = ran H   =>    |- ( ( G e. GrpOp /\ H e. GrpOp /\ F e. ( G GrpOpHom H ) ) -> F : X --> W )
Theorem	ghomco 33690	The composition of two group homomorphisms is a group homomorphism. (Contributed by Jeff Madsen, 1-Dec-2009.) (Revised by Mario Carneiro, 27-Dec-2014.)
|- ( ( ( G e. GrpOp /\ H e. GrpOp /\ K e. GrpOp ) /\ ( S e. ( G GrpOpHom H ) /\ T e. ( H GrpOpHom K ) ) ) -> ( T o. S ) e. ( G GrpOpHom K ) )
Theorem	ghomdiv 33691	Group homomorphisms preserve division. (Contributed by Jeff Madsen, 16-Jun-2011.)
|- X = ran G   &    |- D = ( /g ` G )   &    |- C = ( /g ` H )   =>    |- ( ( ( G e. GrpOp /\ H e. GrpOp /\ F e. ( G GrpOpHom H ) ) /\ ( A e. X /\ B e. X ) ) -> ( F ` ( A D B ) ) = ( ( F ` A ) C ( F ` B ) ) )
Theorem	grpokerinj 33692	A group homomorphism is injective if and only if its kernel is zero. (Contributed by Jeff Madsen, 16-Jun-2011.)
|- X = ran G   &    |- W = (GId ` G )   &    |- Y = ran H   &    |- U = (GId ` H )   =>    |- ( ( G e. GrpOp /\ H e. GrpOp /\ F e. ( G GrpOpHom H ) ) -> ( F : X -1-1-> Y <-> ( `' F " { U } ) = { W } ) )
20.19.16  Rings
Syntax	crngo 33693	Extend class notation with the class of all unital rings.
class RingOps
Definition	df-rngo 33694*	Define the class of all unital rings. (Contributed by Jeff Hankins, 21-Nov-2006.) (New usage is discouraged.)
|- RingOps = { <. g , h >. | ( ( g e. AbelOp /\ h : ( ran g X. ran g ) --> ran g ) /\ ( A. x e. ran g A. y e. ran g A. z e. ran g ( ( ( x h y ) h z ) = ( x h ( y h z ) ) /\ ( x h ( y g z ) ) = ( ( x h y ) g ( x h z ) ) /\ ( ( x g y ) h z ) = ( ( x h z ) g ( y h z ) ) ) /\ E. x e. ran g A. y e. ran g ( ( x h y ) = y /\ ( y h x ) = y ) ) ) }
Theorem	relrngo 33695	The class of all unital rings is a relation. (Contributed by FL, 31-Aug-2009.) (Revised by Mario Carneiro, 21-Dec-2013.) (New usage is discouraged.)
|- Rel RingOps
Theorem	isrngo 33696*	The predicate "is a (unital) ring." Definition of ring with unit in [Schechter] p. 187. (Contributed by Jeff Hankins, 21-Nov-2006.) (Revised by Mario Carneiro, 21-Dec-2013.) (New usage is discouraged.)
|- X = ran G   =>    |- ( H e. A -> ( <. G , H >. e. RingOps <-> ( ( G e. AbelOp /\ H : ( X X. X ) --> X ) /\ ( A. x e. X A. y e. X A. z e. X ( ( ( x H y ) H z ) = ( x H ( y H z ) ) /\ ( x H ( y G z ) ) = ( ( x H y ) G ( x H z ) ) /\ ( ( x G y ) H z ) = ( ( x H z ) G ( y H z ) ) ) /\ E. x e. X A. y e. X ( ( x H y ) = y /\ ( y H x ) = y ) ) ) ) )
Theorem	isrngod 33697*	Conditions that determine a ring. (Changed label from isringd 18585 to isrngod 33697-NM 2-Aug-2013.) (Contributed by Jeff Madsen, 19-Jun-2010.) (Revised by Mario Carneiro, 21-Dec-2013.) (New usage is discouraged.)
|- ( ph -> G e. AbelOp )   &    |- ( ph -> X = ran G )   &    |- ( ph -> H : ( X X. X ) --> X )   &    |- ( ( ph /\ ( x e. X /\ y e. X /\ z e. X ) ) -> ( ( x H y ) H z ) = ( x H ( y H z ) ) )   &    |- ( ( ph /\ ( x e. X /\ y e. X /\ z e. X ) ) -> ( x H ( y G z ) ) = ( ( x H y ) G ( x H z ) ) )   &    |- ( ( ph /\ ( x e. X /\ y e. X /\ z e. X ) ) -> ( ( x G y ) H z ) = ( ( x H z ) G ( y H z ) ) )   &    |- ( ph -> U e. X )   &    |- ( ( ph /\ y e. X ) -> ( U H y ) = y )   &    |- ( ( ph /\ y e. X ) -> ( y H U ) = y )   =>    |- ( ph -> <. G , H >. e. RingOps )
Theorem	rngoi 33698*	The properties of a unital ring. (Contributed by Steve Rodriguez, 8-Sep-2007.) (Proof shortened by Mario Carneiro, 21-Dec-2013.) (New usage is discouraged.)
|- G = ( 1st ` R )   &    |- H = ( 2nd ` R )   &    |- X = ran G   =>    |- ( R e. RingOps -> ( ( G e. AbelOp /\ H : ( X X. X ) --> X ) /\ ( A. x e. X A. y e. X A. z e. X ( ( ( x H y ) H z ) = ( x H ( y H z ) ) /\ ( x H ( y G z ) ) = ( ( x H y ) G ( x H z ) ) /\ ( ( x G y ) H z ) = ( ( x H z ) G ( y H z ) ) ) /\ E. x e. X A. y e. X ( ( x H y ) = y /\ ( y H x ) = y ) ) ) )
Theorem	rngosm 33699	Functionality of the multiplication operation of a ring. (Contributed by Steve Rodriguez, 9-Sep-2007.) (Revised by Mario Carneiro, 21-Dec-2013.) (New usage is discouraged.)
|- G = ( 1st ` R )   &    |- H = ( 2nd ` R )   &    |- X = ran G   =>    |- ( R e. RingOps -> H : ( X X. X ) --> X )
Theorem	rngocl 33700	Closure of the multiplication operation of a ring. (Contributed by Steve Rodriguez, 9-Sep-2007.) (New usage is discouraged.)
|- G = ( 1st ` R )   &    |- H = ( 2nd ` R )   &    |- X = ran G   =>    |- ( ( R e. RingOps /\ A e. X /\ B e. X ) -> ( A H B ) e. X )