P. 158 of Theorem List - Metamath Proof Explorer

Mirrors  >  Metamath Home Page  >  MPE Home Page  >  Theorem List Contents  >  Recent Proofs       This page: Page List

Theorem List for Metamath Proof Explorer - 15701-15800   *Has distinct variable group(s)

Type	Label	Description
Statement
Definition	df-dvdsr 15701*	Define the (right) divisibility relation in a ring. Access to the left divisibility relation is available through ( ||r ` (oppr ` R ) ). (Contributed by Mario Carneiro, 1-Dec-2014.)
|- ||r = ( w e. _V |-> { <. x , y >. | ( x e. ( Base ` w ) /\ E. z e. ( Base ` w ) ( z ( .r ` w ) x ) = y ) } )
Definition	df-unit 15702	Define the set of units in a ring. (Contributed by Mario Carneiro, 1-Dec-2014.)
|- Unit = ( w e. _V |-> ( `' ( ( ||r ` w ) i^i ( ||r ` (oppr ` w ) ) ) " { ( 1r ` w ) } ) )
Definition	df-irred 15703*	Define the set of irreducible elements in a ring. (Contributed by Mario Carneiro, 4-Dec-2014.)
|- Irred = ( w e. _V |-> [_ ( ( Base ` w ) \ (Unit ` w ) ) / b ]_ { z e. b | A. x e. b A. y e. b ( x ( .r ` w ) y ) =/= z } )
Theorem	reldvdsr 15704	The divides relation is a relation. (Contributed by Mario Carneiro, 1-Dec-2014.)
|- .|| = ( ||r ` R )   =>    |- Rel .||
Theorem	dvdsrval 15705*	Value of the divides relation. (Contributed by Mario Carneiro, 1-Dec-2014.) (Revised by Mario Carneiro, 6-Jan-2015.)
|- B = ( Base ` R )   &    |- .|| = ( ||r ` R )   &    |- .x. = ( .r ` R )   =>    |- .|| = { <. x , y >. | ( x e. B /\ E. z e. B ( z .x. x ) = y ) }
Theorem	dvdsr 15706*	Value of the divides relation. (Contributed by Mario Carneiro, 1-Dec-2014.)
|- B = ( Base ` R )   &    |- .|| = ( ||r ` R )   &    |- .x. = ( .r ` R )   =>    |- ( X .|| Y <-> ( X e. B /\ E. z e. B ( z .x. X ) = Y ) )
Theorem	dvdsr2 15707*	Value of the divides relation. (Contributed by Mario Carneiro, 1-Dec-2014.)
|- B = ( Base ` R )   &    |- .|| = ( ||r ` R )   &    |- .x. = ( .r ` R )   =>    |- ( X e. B -> ( X .|| Y <-> E. z e. B ( z .x. X ) = Y ) )
Theorem	dvdsrmul 15708	A left-multiple of X is divisible by X. (Contributed by Mario Carneiro, 1-Dec-2014.)
|- B = ( Base ` R )   &    |- .|| = ( ||r ` R )   &    |- .x. = ( .r ` R )   =>    |- ( ( X e. B /\ Y e. B ) -> X .|| ( Y .x. X ) )
Theorem	dvdsrcl 15709	Closure of a dividing element. (Contributed by Mario Carneiro, 5-Dec-2014.)
|- B = ( Base ` R )   &    |- .|| = ( ||r ` R )   =>    |- ( X .|| Y -> X e. B )
Theorem	dvdsrcl2 15710	Closure of a dividing element. (Contributed by Mario Carneiro, 5-Dec-2014.)
|- B = ( Base ` R )   &    |- .|| = ( ||r ` R )   =>    |- ( ( R e. Ring /\ X .|| Y ) -> Y e. B )
Theorem	dvdsrid 15711	An element in a (unital) ring divides itself. (Contributed by Mario Carneiro, 1-Dec-2014.) (Revised by Mario Carneiro, 30-Apr-2015.)
|- B = ( Base ` R )   &    |- .|| = ( ||r ` R )   =>    |- ( ( R e. Ring /\ X e. B ) -> X .|| X )
Theorem	dvdsrtr 15712	Divisibility is transitive. (Contributed by Mario Carneiro, 1-Dec-2014.)
|- B = ( Base ` R )   &    |- .|| = ( ||r ` R )   =>    |- ( ( R e. Ring /\ Y .|| Z /\ Z .|| X ) -> Y .|| X )
Theorem	dvdsrmul1 15713	The divisibility relation is preserved under right-multiplication. (Contributed by Mario Carneiro, 1-Dec-2014.)
|- B = ( Base ` R )   &    |- .|| = ( ||r ` R )   &    |- .x. = ( .r ` R )   =>    |- ( ( R e. Ring /\ Z e. B /\ X .|| Y ) -> ( X .x. Z ) .|| ( Y .x. Z ) )
Theorem	dvdsrneg 15714	An element divides its negative. (Contributed by Mario Carneiro, 1-Dec-2014.)
|- B = ( Base ` R )   &    |- .|| = ( ||r ` R )   &    |- N = ( inv g ` R )   =>    |- ( ( R e. Ring /\ X e. B ) -> X .|| ( N ` X ) )
Theorem	dvdsr01 15715	In a ring, zero is divisible by all elements. ("Zero divisor" as a term has a somewhat different meaning, see df-rlreg 16298.) (Contributed by Stefan O'Rear, 29-Mar-2015.)
|- B = ( Base ` R )   &    |- .|| = ( ||r ` R )   &    |- .0. = ( 0g ` R )   =>    |- ( ( R e. Ring /\ X e. B ) -> X .|| .0. )
Theorem	dvdsr02 15716	Only zero is divisible by zero. (Contributed by Stefan O'Rear, 29-Mar-2015.)
|- B = ( Base ` R )   &    |- .|| = ( ||r ` R )   &    |- .0. = ( 0g ` R )   =>    |- ( ( R e. Ring /\ X e. B ) -> ( .0. .|| X <-> X = .0. ) )
Theorem	isunit 15717	Property of being a unit of a ring. A unit is an element that left- and right-divides one. (Contributed by Mario Carneiro, 1-Dec-2014.) (Revised by Mario Carneiro, 8-Dec-2015.)
|- U = (Unit ` R )   &    |- .1. = ( 1r ` R )   &    |- .|| = ( ||r ` R )   &    |- S = (oppr ` R )   &    |- E = ( ||r ` S )   =>    |- ( X e. U <-> ( X .|| .1. /\ X E .1. ) )
Theorem	1unit 15718	The multiplicative identity is a unit. (Contributed by Mario Carneiro, 1-Dec-2014.)
|- U = (Unit ` R )   &    |- .1. = ( 1r ` R )   =>    |- ( R e. Ring -> .1. e. U )
Theorem	unitcl 15719	A unit is an element of the base set. (Contributed by Mario Carneiro, 1-Dec-2014.)
|- B = ( Base ` R )   &    |- U = (Unit ` R )   =>    |- ( X e. U -> X e. B )
Theorem	unitss 15720	The set of units is contained in the base set. (Contributed by Mario Carneiro, 5-Oct-2015.)
|- B = ( Base ` R )   &    |- U = (Unit ` R )   =>    |- U C_ B
Theorem	opprunit 15721	Being a unit is a symmetric property, so it transfers to the opposite ring. (Contributed by Mario Carneiro, 4-Dec-2014.)
|- U = (Unit ` R )   &    |- S = (oppr ` R )   =>    |- U = (Unit ` S )
Theorem	crngunit 15722	Property of being a unit in a commutative ring. (Contributed by Mario Carneiro, 18-Apr-2016.)
|- U = (Unit ` R )   &    |- .1. = ( 1r ` R )   &    |- .|| = ( ||r ` R )   =>    |- ( R e. CRing -> ( X e. U <-> X .|| .1. ) )
Theorem	dvdsunit 15723	A divisor of a unit is a unit. (Contributed by Mario Carneiro, 18-Apr-2016.)
|- U = (Unit ` R )   &    |- .|| = ( ||r ` R )   =>    |- ( ( R e. CRing /\ Y .|| X /\ X e. U ) -> Y e. U )
Theorem	unitmulcl 15724	The product of units is a unit. (Contributed by Mario Carneiro, 2-Dec-2014.)
|- U = (Unit ` R )   &    |- .x. = ( .r ` R )   =>    |- ( ( R e. Ring /\ X e. U /\ Y e. U ) -> ( X .x. Y ) e. U )
Theorem	unitmulclb 15725	Reversal of unitmulcl 15724 in a commutative ring. (Contributed by Mario Carneiro, 18-Apr-2016.)
|- U = (Unit ` R )   &    |- .x. = ( .r ` R )   &    |- B = ( Base ` R )   =>    |- ( ( R e. CRing /\ X e. B /\ Y e. B ) -> ( ( X .x. Y ) e. U <-> ( X e. U /\ Y e. U ) ) )
Theorem	unitgrpbas 15726	The base set of the group of units. (Contributed by Mario Carneiro, 25-Dec-2014.)
|- U = (Unit ` R )   &    |- G = ( (mulGrp ` R ) ↾s U )   =>    |- U = ( Base ` G )
Theorem	unitgrp 15727	The group of units is a group under multiplication. (Contributed by Mario Carneiro, 2-Dec-2014.)
|- U = (Unit ` R )   &    |- G = ( (mulGrp ` R ) ↾s U )   =>    |- ( R e. Ring -> G e. Grp )
Theorem	unitabl 15728	The group of units of a commutative ring is abelian. (Contributed by Mario Carneiro, 19-Apr-2016.)
|- U = (Unit ` R )   &    |- G = ( (mulGrp ` R ) ↾s U )   =>    |- ( R e. CRing -> G e. Abel )
Theorem	unitgrpid 15729	The identity of the multiplicative group is 1r. (Contributed by Mario Carneiro, 2-Dec-2014.)
|- U = (Unit ` R )   &    |- G = ( (mulGrp ` R ) ↾s U )   &    |- .1. = ( 1r ` R )   =>    |- ( R e. Ring -> .1. = ( 0g ` G ) )
Theorem	unitsubm 15730	The group of units is a submonoid of the multiplicative monoid of the ring. (Contributed by Mario Carneiro, 18-Jun-2015.)
|- U = (Unit ` R )   &    |- M = (mulGrp ` R )   =>    |- ( R e. Ring -> U e. (SubMnd ` M ) )
Syntax	cinvr 15731	Extend class notation with multiplicative inverse.
class invr
Definition	df-invr 15732	Define multiplicative inverse. (Contributed by NM, 21-Sep-2011.)
|- invr = ( r e. _V |-> ( inv g ` ( (mulGrp ` r ) ↾s (Unit ` r ) ) ) )
Theorem	invrfval 15733	Multiplicative inverse function for a division ring. (Contributed by NM, 21-Sep-2011.) (Revised by Mario Carneiro, 25-Dec-2014.)
|- U = (Unit ` R )   &    |- G = ( (mulGrp ` R ) ↾s U )   &    |- I = ( invr ` R )   =>    |- I = ( inv g ` G )
Theorem	unitinvcl 15734	The inverse of a unit exists and is a unit. (Contributed by Mario Carneiro, 2-Dec-2014.)
|- U = (Unit ` R )   &    |- I = ( invr ` R )   =>    |- ( ( R e. Ring /\ X e. U ) -> ( I ` X ) e. U )
Theorem	unitinvinv 15735	The inverse of the inverse of a unit is the same element. (Contributed by Mario Carneiro, 4-Dec-2014.)
|- U = (Unit ` R )   &    |- I = ( invr ` R )   =>    |- ( ( R e. Ring /\ X e. U ) -> ( I ` ( I ` X ) ) = X )
Theorem	rnginvcl 15736	The inverse of a unit is an element of the ring. (Contributed by Mario Carneiro, 2-Dec-2014.)
|- U = (Unit ` R )   &    |- I = ( invr ` R )   &    |- B = ( Base ` R )   =>    |- ( ( R e. Ring /\ X e. U ) -> ( I ` X ) e. B )
Theorem	unitlinv 15737	A unit times its inverse is the identity. (Contributed by Mario Carneiro, 2-Dec-2014.)
|- U = (Unit ` R )   &    |- I = ( invr ` R )   &    |- .x. = ( .r ` R )   &    |- .1. = ( 1r ` R )   =>    |- ( ( R e. Ring /\ X e. U ) -> ( ( I ` X ) .x. X ) = .1. )
Theorem	unitrinv 15738	A unit times its inverse is the identity. (Contributed by Mario Carneiro, 2-Dec-2014.)
|- U = (Unit ` R )   &    |- I = ( invr ` R )   &    |- .x. = ( .r ` R )   &    |- .1. = ( 1r ` R )   =>    |- ( ( R e. Ring /\ X e. U ) -> ( X .x. ( I ` X ) ) = .1. )
Theorem	1rinv 15739	The inverse of the identity is the identity. (Contributed by Mario Carneiro, 18-Jun-2015.)
|- I = ( invr ` R )   &    |- .1. = ( 1r ` R )   =>    |- ( R e. Ring -> ( I ` .1. ) = .1. )
Theorem	0unit 15740	The additive identity is a unit if and only if 1 = 0, i.e. we are in the zero ring. (Contributed by Mario Carneiro, 4-Dec-2014.)
|- U = (Unit ` R )   &    |- .0. = ( 0g ` R )   &    |- .1. = ( 1r ` R )   =>    |- ( R e. Ring -> ( .0. e. U <-> .1. = .0. ) )
Theorem	unitnegcl 15741	The negative of a unit is a unit. (Contributed by Mario Carneiro, 4-Dec-2014.)
|- U = (Unit ` R )   &    |- N = ( inv g ` R )   =>    |- ( ( R e. Ring /\ X e. U ) -> ( N ` X ) e. U )
Syntax	cdvr 15742	Extend class notation with ring division.
class /r
Definition	df-dvr 15743*	Define ring division. (Contributed by Mario Carneiro, 2-Jul-2014.)
|- /r = ( r e. _V |-> ( x e. ( Base ` r ) , y e. (Unit ` r ) |-> ( x ( .r ` r ) ( ( invr ` r ) ` y ) ) ) )
Theorem	dvrfval 15744*	Division operation in a ring. (Contributed by Mario Carneiro, 2-Jul-2014.) (Revised by Mario Carneiro, 2-Dec-2014.)
|- B = ( Base ` R )   &    |- .x. = ( .r ` R )   &    |- U = (Unit ` R )   &    |- I = ( invr ` R )   &    |- ./ = (/r ` R )   =>    |- ./ = ( x e. B , y e. U |-> ( x .x. ( I ` y ) ) )
Theorem	dvrval 15745	Division operation in a ring. (Contributed by Mario Carneiro, 2-Jul-2014.) (Revised by Mario Carneiro, 2-Dec-2014.)
|- B = ( Base ` R )   &    |- .x. = ( .r ` R )   &    |- U = (Unit ` R )   &    |- I = ( invr ` R )   &    |- ./ = (/r ` R )   =>    |- ( ( X e. B /\ Y e. U ) -> ( X ./ Y ) = ( X .x. ( I ` Y ) ) )
Theorem	dvrcl 15746	Closure of division operation. (Contributed by Mario Carneiro, 2-Jul-2014.)
|- B = ( Base ` R )   &    |- U = (Unit ` R )   &    |- ./ = (/r ` R )   =>    |- ( ( R e. Ring /\ X e. B /\ Y e. U ) -> ( X ./ Y ) e. B )
Theorem	unitdvcl 15747	The units are closed under division. (Contributed by Mario Carneiro, 2-Jul-2014.)
|- U = (Unit ` R )   &    |- ./ = (/r ` R )   =>    |- ( ( R e. Ring /\ X e. U /\ Y e. U ) -> ( X ./ Y ) e. U )
Theorem	dvrid 15748	A cancellation law for division. (divid 9661 analog.) (Contributed by Mario Carneiro, 18-Jun-2015.)
|- U = (Unit ` R )   &    |- ./ = (/r ` R )   &    |- .1. = ( 1r ` R )   =>    |- ( ( R e. Ring /\ X e. U ) -> ( X ./ X ) = .1. )
Theorem	dvr1 15749	A cancellation law for division. (div1 9663 analog.) (Contributed by Mario Carneiro, 18-Jun-2015.)
|- B = ( Base ` R )   &    |- ./ = (/r ` R )   &    |- .1. = ( 1r ` R )   =>    |- ( ( R e. Ring /\ X e. B ) -> ( X ./ .1. ) = X )
Theorem	dvrass 15750	An associative law for division. (divass 9652 analog.) (Contributed by Mario Carneiro, 4-Dec-2014.)
|- B = ( Base ` R )   &    |- U = (Unit ` R )   &    |- ./ = (/r ` R )   &    |- .x. = ( .r ` R )   =>    |- ( ( R e. Ring /\ ( X e. B /\ Y e. B /\ Z e. U ) ) -> ( ( X .x. Y ) ./ Z ) = ( X .x. ( Y ./ Z ) ) )
Theorem	dvrcan1 15751	A cancellation law for division. (divcan1 9643 analog.) (Contributed by Mario Carneiro, 2-Jul-2014.) (Revised by Mario Carneiro, 2-Dec-2014.)
|- B = ( Base ` R )   &    |- U = (Unit ` R )   &    |- ./ = (/r ` R )   &    |- .x. = ( .r ` R )   =>    |- ( ( R e. Ring /\ X e. B /\ Y e. U ) -> ( ( X ./ Y ) .x. Y ) = X )
Theorem	dvrcan3 15752	A cancellation law for division. (divcan3 9658 analog.) (Contributed by Mario Carneiro, 2-Jul-2014.) (Revised by Mario Carneiro, 18-Jun-2015.)
|- B = ( Base ` R )   &    |- U = (Unit ` R )   &    |- ./ = (/r ` R )   &    |- .x. = ( .r ` R )   =>    |- ( ( R e. Ring /\ X e. B /\ Y e. U ) -> ( ( X .x. Y ) ./ Y ) = X )
Theorem	dvreq1 15753	A cancellation law for division. (diveq1 9664 analog.) (Contributed by Mario Carneiro, 28-Apr-2016.)
|- B = ( Base ` R )   &    |- U = (Unit ` R )   &    |- ./ = (/r ` R )   &    |- .1. = ( 1r ` R )   =>    |- ( ( R e. Ring /\ X e. B /\ Y e. U ) -> ( ( X ./ Y ) = .1. <-> X = Y ) )
Theorem	rnginvdv 15754	Write the inverse function in terms of division. (Contributed by Mario Carneiro, 2-Jul-2014.)
|- B = ( Base ` R )   &    |- U = (Unit ` R )   &    |- ./ = (/r ` R )   &    |- .1. = ( 1r ` R )   &    |- I = ( invr ` R )   =>    |- ( ( R e. Ring /\ X e. U ) -> ( I ` X ) = ( .1. ./ X ) )
Theorem	rngidpropd 15755*	The ring identity depends only on the ring's base set and multiplication operation. (Contributed by Mario Carneiro, 26-Dec-2014.)
|- ( ph -> B = ( Base ` K ) )   &    |- ( ph -> B = ( Base ` L ) )   &    |- ( ( ph /\ ( x e. B /\ y e. B ) ) -> ( x ( .r ` K ) y ) = ( x ( .r ` L ) y ) )   =>    |- ( ph -> ( 1r ` K ) = ( 1r ` L ) )
Theorem	dvdsrpropd 15756*	The divisibility relation depends only on the ring's base set and multiplication operation. (Contributed by Mario Carneiro, 26-Dec-2014.)
|- ( ph -> B = ( Base ` K ) )   &    |- ( ph -> B = ( Base ` L ) )   &    |- ( ( ph /\ ( x e. B /\ y e. B ) ) -> ( x ( .r ` K ) y ) = ( x ( .r ` L ) y ) )   =>    |- ( ph -> ( ||r ` K ) = ( ||r ` L ) )
Theorem	unitpropd 15757*	The set of units depends only on the ring's base set and multiplication operation. (Contributed by Mario Carneiro, 26-Dec-2014.)
|- ( ph -> B = ( Base ` K ) )   &    |- ( ph -> B = ( Base ` L ) )   &    |- ( ( ph /\ ( x e. B /\ y e. B ) ) -> ( x ( .r ` K ) y ) = ( x ( .r ` L ) y ) )   =>    |- ( ph -> (Unit ` K ) = (Unit ` L ) )
Theorem	invrpropd 15758*	The ring inverse function depends only on the ring's base set and multiplication operation. (Contributed by Mario Carneiro, 26-Dec-2014.) (Revised by Mario Carneiro, 5-Oct-2015.)
|- ( ph -> B = ( Base ` K ) )   &    |- ( ph -> B = ( Base ` L ) )   &    |- ( ( ph /\ ( x e. B /\ y e. B ) ) -> ( x ( .r ` K ) y ) = ( x ( .r ` L ) y ) )   =>    |- ( ph -> ( invr ` K ) = ( invr ` L ) )
Theorem	isirred 15759*	An irreducible element of a ring is a non-unit that is not the product of two non-units. (Contributed by Mario Carneiro, 4-Dec-2014.)
|- B = ( Base ` R )   &    |- U = (Unit ` R )   &    |- I = (Irred ` R )   &    |- N = ( B \ U )   &    |- .x. = ( .r ` R )   =>    |- ( X e. I <-> ( X e. N /\ A. x e. N A. y e. N ( x .x. y ) =/= X ) )
Theorem	isnirred 15760*	The property of being a non-irreducible (reducible) element in a ring. (Contributed by Mario Carneiro, 4-Dec-2014.)
|- B = ( Base ` R )   &    |- U = (Unit ` R )   &    |- I = (Irred ` R )   &    |- N = ( B \ U )   &    |- .x. = ( .r ` R )   =>    |- ( X e. B -> ( -. X e. I <-> ( X e. U \/ E. x e. N E. y e. N ( x .x. y ) = X ) ) )
Theorem	isirred2 15761*	Expand out the set differences from isirred 15759. (Contributed by Mario Carneiro, 4-Dec-2014.)
|- B = ( Base ` R )   &    |- U = (Unit ` R )   &    |- I = (Irred ` R )   &    |- .x. = ( .r ` R )   =>    |- ( X e. I <-> ( X e. B /\ -. X e. U /\ A. x e. B A. y e. B ( ( x .x. y ) = X -> ( x e. U \/ y e. U ) ) ) )
Theorem	opprirred 15762	Irreducibility is symmetric, so the irreducible elements of the opposite ring are the same as the original ring. (Contributed by Mario Carneiro, 4-Dec-2014.)
|- S = (oppr ` R )   &    |- I = (Irred ` R )   =>    |- I = (Irred ` S )
Theorem	irredn0 15763	The additive identity is not irreducible. (Contributed by Mario Carneiro, 4-Dec-2014.)
|- I = (Irred ` R )   &    |- .0. = ( 0g ` R )   =>    |- ( ( R e. Ring /\ X e. I ) -> X =/= .0. )
Theorem	irredcl 15764	An irreducible element is in the ring. (Contributed by Mario Carneiro, 4-Dec-2014.)
|- I = (Irred ` R )   &    |- B = ( Base ` R )   =>    |- ( X e. I -> X e. B )
Theorem	irrednu 15765	An irreducible element is not a unit. (Contributed by Mario Carneiro, 4-Dec-2014.)
|- I = (Irred ` R )   &    |- U = (Unit ` R )   =>    |- ( X e. I -> -. X e. U )
Theorem	irredn1 15766	The multiplicative identity is not irreducible. (Contributed by Mario Carneiro, 4-Dec-2014.)
|- I = (Irred ` R )   &    |- .1. = ( 1r ` R )   =>    |- ( ( R e. Ring /\ X e. I ) -> X =/= .1. )
Theorem	irredrmul 15767	The product of an irreducible element and a unit is irreducible. (Contributed by Mario Carneiro, 4-Dec-2014.)
|- I = (Irred ` R )   &    |- U = (Unit ` R )   &    |- .x. = ( .r ` R )   =>    |- ( ( R e. Ring /\ X e. I /\ Y e. U ) -> ( X .x. Y ) e. I )
Theorem	irredlmul 15768	The product of a unit and an irreducible element is irreducible. (Contributed by Mario Carneiro, 4-Dec-2014.)
|- I = (Irred ` R )   &    |- U = (Unit ` R )   &    |- .x. = ( .r ` R )   =>    |- ( ( R e. Ring /\ X e. U /\ Y e. I ) -> ( X .x. Y ) e. I )
Theorem	irredmul 15769	If product of two elements is irreducible, then one of the elements must be a unit. (Contributed by Mario Carneiro, 4-Dec-2014.)
|- I = (Irred ` R )   &    |- B = ( Base ` R )   &    |- U = (Unit ` R )   &    |- .x. = ( .r ` R )   =>    |- ( ( X e. B /\ Y e. B /\ ( X .x. Y ) e. I ) -> ( X e. U \/ Y e. U ) )
Theorem	irredneg 15770	The negative of an irreducible element is irreducible. (Contributed by Mario Carneiro, 4-Dec-2014.)
|- I = (Irred ` R )   &    |- N = ( inv g ` R )   =>    |- ( ( R e. Ring /\ X e. I ) -> ( N ` X ) e. I )
Theorem	irrednegb 15771	An element is irreducible iff its negative is. (Contributed by Mario Carneiro, 4-Dec-2014.)
|- I = (Irred ` R )   &    |- N = ( inv g ` R )   &    |- B = ( Base ` R )   =>    |- ( ( R e. Ring /\ X e. B ) -> ( X e. I <-> ( N ` X ) e. I ) )
10.4.5  Ring homomorphisms
Syntax	crh 15772	Ring homomorphisms.
class RingHom
Syntax	crs 15773	Ring isomorphisms.
class RingIso
Definition	df-rnghom 15774*	Define the set of ring homomorphisms from r to s. (Contributed by Stefan O'Rear, 7-Mar-2015.)
|- RingHom = ( r e. Ring , s e. Ring |-> [_ ( Base ` r ) / v ]_ [_ ( Base ` s ) / w ]_ { f e. ( w ^m v ) | ( ( f ` ( 1r ` r ) ) = ( 1r ` s ) /\ A. x e. v A. y e. v ( ( f ` ( x ( +g ` r ) y ) ) = ( ( f ` x ) ( +g ` s ) ( f ` y ) ) /\ ( f ` ( x ( .r ` r ) y ) ) = ( ( f ` x ) ( .r ` s ) ( f ` y ) ) ) ) } )
Definition	df-rngiso 15775*	Define the set of ring isomorphisms from r to s. (Contributed by Stefan O'Rear, 7-Mar-2015.)
|- RingIso = ( r e. _V , s e. _V |-> { f e. ( r RingHom s ) | `' f e. ( s RingHom r ) } )
Theorem	dfrhm2 15776*	The property of a ring homomorphism can be decomposed into separate homomorphic conditions for addition and multiplication. (Contributed by Stefan O'Rear, 7-Mar-2015.)
|- RingHom = ( r e. Ring , s e. Ring |-> ( ( r GrpHom s ) i^i ( (mulGrp ` r ) MndHom (mulGrp ` s ) ) ) )
Theorem	rhmrcl1 15777	Reverse closure of a ring homomorphism. (Contributed by Stefan O'Rear, 7-Mar-2015.)
|- ( F e. ( R RingHom S ) -> R e. Ring )
Theorem	rhmrcl2 15778	Reverse closure of a ring homomorphism. (Contributed by Stefan O'Rear, 7-Mar-2015.)
|- ( F e. ( R RingHom S ) -> S e. Ring )
Theorem	isrhm 15779	A function is a ring homomorphism iff it preserves both addition and multiplication. (Contributed by Stefan O'Rear, 7-Mar-2015.)
|- M = (mulGrp ` R )   &    |- N = (mulGrp ` S )   =>    |- ( F e. ( R RingHom S ) <-> ( ( R e. Ring /\ S e. Ring ) /\ ( F e. ( R GrpHom S ) /\ F e. ( M MndHom N ) ) ) )
Theorem	rhmmhm 15780	A ring homomorphism is a homomorphism of multiplicative monoids. (Contributed by Stefan O'Rear, 7-Mar-2015.)
|- M = (mulGrp ` R )   &    |- N = (mulGrp ` S )   =>    |- ( F e. ( R RingHom S ) -> F e. ( M MndHom N ) )
Theorem	rhmghm 15781	A ring homomorphism is an additive group homomorphism. (Contributed by Stefan O'Rear, 7-Mar-2015.)
|- ( F e. ( R RingHom S ) -> F e. ( R GrpHom S ) )
Theorem	rhmf 15782	A ring homomorphism is a function. (Contributed by Stefan O'Rear, 8-Mar-2015.)
|- B = ( Base ` R )   &    |- C = ( Base ` S )   =>    |- ( F e. ( R RingHom S ) -> F : B --> C )
Theorem	rhmmul 15783	A homomorphism of rings preserves multiplication. (Contributed by Mario Carneiro, 12-Jun-2015.)
|- X = ( Base ` R )   &    |- .x. = ( .r ` R )   &    |- .X. = ( .r ` S )   =>    |- ( ( F e. ( R RingHom S ) /\ A e. X /\ B e. X ) -> ( F ` ( A .x. B ) ) = ( ( F ` A ) .X. ( F ` B ) ) )
Theorem	isrhm2d 15784*	Demonstration of ring homomorphism. (Contributed by Mario Carneiro, 13-Jun-2015.)
|- B = ( Base ` R )   &    |- .1. = ( 1r ` R )   &    |- N = ( 1r ` S )   &    |- .x. = ( .r ` R )   &    |- .X. = ( .r ` S )   &    |- ( ph -> R e. Ring )   &    |- ( ph -> S e. Ring )   &    |- ( ph -> ( F ` .1. ) = N )   &    |- ( ( ph /\ ( x e. B /\ y e. B ) ) -> ( F ` ( x .x. y ) ) = ( ( F ` x ) .X. ( F ` y ) ) )   &    |- ( ph -> F e. ( R GrpHom S ) )   =>    |- ( ph -> F e. ( R RingHom S ) )
Theorem	isrhmd 15785*	Demonstration of ring homomorphism. (Contributed by Stefan O'Rear, 8-Mar-2015.)
|- B = ( Base ` R )   &    |- .1. = ( 1r ` R )   &    |- N = ( 1r ` S )   &    |- .x. = ( .r ` R )   &    |- .X. = ( .r ` S )   &    |- ( ph -> R e. Ring )   &    |- ( ph -> S e. Ring )   &    |- ( ph -> ( F ` .1. ) = N )   &    |- ( ( ph /\ ( x e. B /\ y e. B ) ) -> ( F ` ( x .x. y ) ) = ( ( F ` x ) .X. ( F ` y ) ) )   &    |- C = ( Base ` S )   &    |- .+ = ( +g ` R )   &    |- .+^ = ( +g ` S )   &    |- ( ph -> F : B --> C )   &    |- ( ( ph /\ ( x e. B /\ y e. B ) ) -> ( F ` ( x .+ y ) ) = ( ( F ` x ) .+^ ( F ` y ) ) )   =>    |- ( ph -> F e. ( R RingHom S ) )
Theorem	rhm1 15786	Ring homomorphisms are required to fix 1. (Contributed by Stefan O'Rear, 8-Mar-2015.)
|- .1. = ( 1r ` R )   &    |- N = ( 1r ` S )   =>    |- ( F e. ( R RingHom S ) -> ( F ` .1. ) = N )
Theorem	rhmco 15787	The composition of ring homomorphisms is a homomorphism. (Contributed by Mario Carneiro, 12-Jun-2015.)
|- ( ( F e. ( T RingHom U ) /\ G e. ( S RingHom T ) ) -> ( F o. G ) e. ( S RingHom U ) )
Theorem	pwsco1rhm 15788*	Right composition with a function on the index sets yields a ring homomorphism of structure powers. (Contributed by Mario Carneiro, 12-Jun-2015.)
|- Y = ( R ^s A )   &    |- Z = ( R ^s B )   &    |- C = ( Base ` Z )   &    |- ( ph -> R e. Ring )   &    |- ( ph -> A e. V )   &    |- ( ph -> B e. W )   &    |- ( ph -> F : A --> B )   =>    |- ( ph -> ( g e. C |-> ( g o. F ) ) e. ( Z RingHom Y ) )
Theorem	pwsco2rhm 15789*	Left composition with a ring homomorphism yields a ring homomorphism of structure powers. (Contributed by Mario Carneiro, 12-Jun-2015.)
|- Y = ( R ^s A )   &    |- Z = ( S ^s A )   &    |- B = ( Base ` Y )   &    |- ( ph -> A e. V )   &    |- ( ph -> F e. ( R RingHom S ) )   =>    |- ( ph -> ( g e. B |-> ( F o. g ) ) e. ( Y RingHom Z ) )
10.5  Division rings and fields
10.5.1  Definition and basic properties
Syntax	cdr 15790	Extend class notation with class of all division rings.
class DivRing
Syntax	cfield 15791	Class of fields.
class Field
Definition	df-drng 15792	Define class of all division rings. A division ring is a ring in which the set of units is exactly the nonzero elements of the ring. (Contributed by NM, 18-Oct-2012.)
|- DivRing = { r e. Ring | (Unit ` r ) = ( ( Base ` r ) \ { ( 0g ` r ) } ) }
Definition	df-field 15793	A field is a commutative division ring. (Contributed by Mario Carneiro, 17-Jun-2015.)
|- Field = ( DivRing i^i CRing )
Theorem	isdrng 15794	The predicate "is a division ring". (Contributed by NM, 18-Oct-2012.) (Revised by Mario Carneiro, 2-Dec-2014.)
|- B = ( Base ` R )   &    |- U = (Unit ` R )   &    |- .0. = ( 0g ` R )   =>    |- ( R e. DivRing <-> ( R e. Ring /\ U = ( B \ { .0. } ) ) )
Theorem	drngunit 15795	Elementhood in the set of units when R is a division ring. (Contributed by Mario Carneiro, 2-Dec-2014.)
|- B = ( Base ` R )   &    |- U = (Unit ` R )   &    |- .0. = ( 0g ` R )   =>    |- ( R e. DivRing -> ( X e. U <-> ( X e. B /\ X =/= .0. ) ) )
Theorem	drngui 15796	The set of units of a division ring. (Contributed by Mario Carneiro, 2-Dec-2014.)
|- B = ( Base ` R )   &    |- .0. = ( 0g ` R )   &    |- R e. DivRing   =>    |- ( B \ { .0. } ) = (Unit ` R )
Theorem	drngrng 15797	A division ring is a ring. (Contributed by NM, 8-Sep-2011.)
|- ( R e. DivRing -> R e. Ring )
Theorem	drnggrp 15798	A division ring is a group. (Contributed by NM, 8-Sep-2011.)
|- ( R e. DivRing -> R e. Grp )
Theorem	isfld 15799	A field is a commutative division ring. (Contributed by Mario Carneiro, 17-Jun-2015.)
|- ( R e. Field <-> ( R e. DivRing /\ R e. CRing ) )
Theorem	isdrng2 15800	A division ring can equivalently be defined as a ring such that the nonzero elements form a group under multiplication (from which it follows that this is the same group as the group of units). (Contributed by Mario Carneiro, 2-Dec-2014.)
|- B = ( Base ` R )   &    |- .0. = ( 0g ` R )   &    |- G = ( (mulGrp ` R ) ↾s ( B \ { .0. } ) )   =>    |- ( R e. DivRing <-> ( R e. Ring /\ G e. Grp ) )