P. 189 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 18801-18900   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	opprsubrg 18801	Being a subring is a symmetric property. (Contributed by Mario Carneiro, 6-Dec-2014.)
|- O = (oppr ` R )   =>    |- (SubRing ` R ) = (SubRing ` O )
Theorem	subrgint 18802	The intersection of a nonempty collection of subrings is a subring. (Contributed by Stefan O'Rear, 30-Nov-2014.) (Revised by Mario Carneiro, 7-Dec-2014.)
|- ( ( S C_ (SubRing ` R ) /\ S =/= (/) ) -> |^| S e. (SubRing ` R ) )
Theorem	subrgin 18803	The intersection of two subrings is a subring. (Contributed by Stefan O'Rear, 30-Nov-2014.) (Revised by Mario Carneiro, 7-Dec-2014.)
|- ( ( A e. (SubRing ` R ) /\ B e. (SubRing ` R ) ) -> ( A i^i B ) e. (SubRing ` R ) )
Theorem	subrgmre 18804	The subrings of a ring are a Moore system. (Contributed by Stefan O'Rear, 9-Mar-2015.)
|- B = ( Base ` R )   =>    |- ( R e. Ring -> (SubRing ` R ) e. (Moore ` B ) )
Theorem	issubdrg 18805*	Characterize the subfields of a division ring. (Contributed by Mario Carneiro, 3-Dec-2014.)
|- S = ( R ↾s A )   &    |- .0. = ( 0g ` R )   &    |- I = ( invr ` R )   =>    |- ( ( R e. DivRing /\ A e. (SubRing ` R ) ) -> ( S e. DivRing <-> A. x e. ( A \ { .0. } ) ( I ` x ) e. A ) )
Theorem	subsubrg 18806	A subring of a subring is a subring. (Contributed by Mario Carneiro, 4-Dec-2014.)
|- S = ( R ↾s A )   =>    |- ( A e. (SubRing ` R ) -> ( B e. (SubRing ` S ) <-> ( B e. (SubRing ` R ) /\ B C_ A ) ) )
Theorem	subsubrg2 18807	The set of subrings of a subring are the smaller subrings. (Contributed by Stefan O'Rear, 9-Mar-2015.)
|- S = ( R ↾s A )   =>    |- ( A e. (SubRing ` R ) -> (SubRing ` S ) = ( (SubRing ` R ) i^i ~P A ) )
Theorem	issubrg3 18808	A subring is an additive subgroup which is also a multiplicative submonoid. (Contributed by Mario Carneiro, 7-Mar-2015.)
|- M = (mulGrp ` R )   =>    |- ( R e. Ring -> ( S e. (SubRing ` R ) <-> ( S e. (SubGrp ` R ) /\ S e. (SubMnd ` M ) ) ) )
Theorem	resrhm 18809	Restriction of a ring homomorphism to a subring is a homomorphism. (Contributed by Mario Carneiro, 12-Mar-2015.)
|- U = ( S ↾s X )   =>    |- ( ( F e. ( S RingHom T ) /\ X e. (SubRing ` S ) ) -> ( F |` X ) e. ( U RingHom T ) )
Theorem	rhmeql 18810	The equalizer of two ring homomorphisms is a subring. (Contributed by Stefan O'Rear, 7-Mar-2015.) (Revised by Mario Carneiro, 6-May-2015.)
|- ( ( F e. ( S RingHom T ) /\ G e. ( S RingHom T ) ) -> dom ( F i^i G ) e. (SubRing ` S ) )
Theorem	rhmima 18811	The homomorphic image of a subring is a subring. (Contributed by Stefan O'Rear, 10-Mar-2015.) (Revised by Mario Carneiro, 6-May-2015.)
|- ( ( F e. ( M RingHom N ) /\ X e. (SubRing ` M ) ) -> ( F " X ) e. (SubRing ` N ) )
Theorem	cntzsubr 18812	Centralizers in a ring are subrings. (Contributed by Stefan O'Rear, 6-Sep-2015.) (Revised by Mario Carneiro, 19-Apr-2016.)
|- B = ( Base ` R )   &    |- M = (mulGrp ` R )   &    |- Z = (Cntz ` M )   =>    |- ( ( R e. Ring /\ S C_ B ) -> ( Z ` S ) e. (SubRing ` R ) )
Theorem	pwsdiagrhm 18813*	Diagonal homomorphism into a structure power (Rings). (Contributed by Mario Carneiro, 12-Mar-2015.) (Revised by Mario Carneiro, 6-May-2015.)
|- Y = ( R ^s I )   &    |- B = ( Base ` R )   &    |- F = ( x e. B |-> ( I X. { x } ) )   =>    |- ( ( R e. Ring /\ I e. W ) -> F e. ( R RingHom Y ) )
Theorem	subrgpropd 18814*	If two structures have the same group components (properties), they have the same set of subrings. (Contributed by Mario Carneiro, 9-Feb-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 -> (SubRing ` K ) = (SubRing ` L ) )
Theorem	rhmpropd 18815*	Ring homomorphism depends only on the ring attributes of structures. (Contributed by Mario Carneiro, 12-Jun-2015.)
|- ( ph -> B = ( Base ` J ) )   &    |- ( ph -> C = ( Base ` K ) )   &    |- ( ph -> B = ( Base ` L ) )   &    |- ( ph -> C = ( Base ` M ) )   &    |- ( ( ph /\ ( x e. B /\ y e. B ) ) -> ( x ( +g ` J ) y ) = ( x ( +g ` L ) y ) )   &    |- ( ( ph /\ ( x e. C /\ y e. C ) ) -> ( x ( +g ` K ) y ) = ( x ( +g ` M ) y ) )   &    |- ( ( ph /\ ( x e. B /\ y e. B ) ) -> ( x ( .r ` J ) y ) = ( x ( .r ` L ) y ) )   &    |- ( ( ph /\ ( x e. C /\ y e. C ) ) -> ( x ( .r ` K ) y ) = ( x ( .r ` M ) y ) )   =>    |- ( ph -> ( J RingHom K ) = ( L RingHom M ) )
10.5.3  Absolute value (abstract algebra)
Syntax	cabv 18816	The set of absolute values on a ring.
class AbsVal
Definition	df-abv 18817*	Define the set of absolute values on a ring. An absolute value is a generalization of the usual absolute value function df-abs 13976 to arbitrary rings. (Contributed by Mario Carneiro, 8-Sep-2014.)
|- AbsVal = ( r e. Ring |-> { f e. ( ( 0 [,) +oo ) ^m ( Base ` r ) ) | A. x e. ( Base ` r ) ( ( ( f ` x ) = 0 <-> x = ( 0g ` r ) ) /\ A. y e. ( Base ` r ) ( ( f ` ( x ( .r ` r ) y ) ) = ( ( f ` x ) x. ( f ` y ) ) /\ ( f ` ( x ( +g ` r ) y ) ) <_ ( ( f ` x ) + ( f ` y ) ) ) ) } )
Theorem	abvfval 18818*	Value of the set of absolute values. (Contributed by Mario Carneiro, 8-Sep-2014.)
|- A = (AbsVal ` R )   &    |- B = ( Base ` R )   &    |- .+ = ( +g ` R )   &    |- .x. = ( .r ` R )   &    |- .0. = ( 0g ` R )   =>    |- ( R e. Ring -> A = { f e. ( ( 0 [,) +oo ) ^m B ) | A. x e. B ( ( ( f ` x ) = 0 <-> x = .0. ) /\ A. y e. B ( ( f ` ( x .x. y ) ) = ( ( f ` x ) x. ( f ` y ) ) /\ ( f ` ( x .+ y ) ) <_ ( ( f ` x ) + ( f ` y ) ) ) ) } )
Theorem	isabv 18819*	Elementhood in the set of absolute values. (Contributed by Mario Carneiro, 8-Sep-2014.)
|- A = (AbsVal ` R )   &    |- B = ( Base ` R )   &    |- .+ = ( +g ` R )   &    |- .x. = ( .r ` R )   &    |- .0. = ( 0g ` R )   =>    |- ( R e. Ring -> ( F e. A <-> ( F : B --> ( 0 [,) +oo ) /\ A. x e. B ( ( ( F ` x ) = 0 <-> x = .0. ) /\ A. y e. B ( ( F ` ( x .x. y ) ) = ( ( F ` x ) x. ( F ` y ) ) /\ ( F ` ( x .+ y ) ) <_ ( ( F ` x ) + ( F ` y ) ) ) ) ) ) )
Theorem	isabvd 18820*	Properties that determine an absolute value. (Contributed by Mario Carneiro, 8-Sep-2014.) (Revised by Mario Carneiro, 4-Dec-2014.)
|- ( ph -> A = (AbsVal ` R ) )   &    |- ( ph -> B = ( Base ` R ) )   &    |- ( ph -> .+ = ( +g ` R ) )   &    |- ( ph -> .x. = ( .r ` R ) )   &    |- ( ph -> .0. = ( 0g ` R ) )   &    |- ( ph -> R e. Ring )   &    |- ( ph -> F : B --> RR )   &    |- ( ph -> ( F ` .0. ) = 0 )   &    |- ( ( ph /\ x e. B /\ x =/= .0. ) -> 0 < ( F ` x ) )   &    |- ( ( ph /\ ( x e. B /\ x =/= .0. ) /\ ( y e. B /\ y =/= .0. ) ) -> ( F ` ( x .x. y ) ) = ( ( F ` x ) x. ( F ` y ) ) )   &    |- ( ( ph /\ ( x e. B /\ x =/= .0. ) /\ ( y e. B /\ y =/= .0. ) ) -> ( F ` ( x .+ y ) ) <_ ( ( F ` x ) + ( F ` y ) ) )   =>    |- ( ph -> F e. A )
Theorem	abvrcl 18821	Reverse closure for the absolute value set. (Contributed by Mario Carneiro, 8-Sep-2014.)
|- A = (AbsVal ` R )   =>    |- ( F e. A -> R e. Ring )
Theorem	abvfge0 18822	An absolute value is a function from the ring to the nonnegative real numbers. (Contributed by Mario Carneiro, 8-Sep-2014.)
|- A = (AbsVal ` R )   &    |- B = ( Base ` R )   =>    |- ( F e. A -> F : B --> ( 0 [,) +oo ) )
Theorem	abvf 18823	An absolute value is a function from the ring to the real numbers. (Contributed by Mario Carneiro, 8-Sep-2014.)
|- A = (AbsVal ` R )   &    |- B = ( Base ` R )   =>    |- ( F e. A -> F : B --> RR )
Theorem	abvcl 18824	An absolute value is a function from the ring to the real numbers. (Contributed by Mario Carneiro, 8-Sep-2014.)
|- A = (AbsVal ` R )   &    |- B = ( Base ` R )   =>    |- ( ( F e. A /\ X e. B ) -> ( F ` X ) e. RR )
Theorem	abvge0 18825	The absolute value of a number is greater or equal to zero. (Contributed by Mario Carneiro, 8-Sep-2014.)
|- A = (AbsVal ` R )   &    |- B = ( Base ` R )   =>    |- ( ( F e. A /\ X e. B ) -> 0 <_ ( F ` X ) )
Theorem	abveq0 18826	The value of an absolute value is zero iff the argument is zero. (Contributed by Mario Carneiro, 8-Sep-2014.)
|- A = (AbsVal ` R )   &    |- B = ( Base ` R )   &    |- .0. = ( 0g ` R )   =>    |- ( ( F e. A /\ X e. B ) -> ( ( F ` X ) = 0 <-> X = .0. ) )
Theorem	abvne0 18827	The absolute value of a nonzero number is nonzero. (Contributed by Mario Carneiro, 8-Sep-2014.)
|- A = (AbsVal ` R )   &    |- B = ( Base ` R )   &    |- .0. = ( 0g ` R )   =>    |- ( ( F e. A /\ X e. B /\ X =/= .0. ) -> ( F ` X ) =/= 0 )
Theorem	abvgt0 18828	The absolute value of a nonzero number is strictly positive. (Contributed by Mario Carneiro, 8-Sep-2014.)
|- A = (AbsVal ` R )   &    |- B = ( Base ` R )   &    |- .0. = ( 0g ` R )   =>    |- ( ( F e. A /\ X e. B /\ X =/= .0. ) -> 0 < ( F ` X ) )
Theorem	abvmul 18829	An absolute value distributes under multiplication. (Contributed by Mario Carneiro, 8-Sep-2014.)
|- A = (AbsVal ` R )   &    |- B = ( Base ` R )   &    |- .x. = ( .r ` R )   =>    |- ( ( F e. A /\ X e. B /\ Y e. B ) -> ( F ` ( X .x. Y ) ) = ( ( F ` X ) x. ( F ` Y ) ) )
Theorem	abvtri 18830	An absolute value satisfies the triangle inequality. (Contributed by Mario Carneiro, 8-Sep-2014.)
|- A = (AbsVal ` R )   &    |- B = ( Base ` R )   &    |- .+ = ( +g ` R )   =>    |- ( ( F e. A /\ X e. B /\ Y e. B ) -> ( F ` ( X .+ Y ) ) <_ ( ( F ` X ) + ( F ` Y ) ) )
Theorem	abv0 18831	The absolute value of zero is zero. (Contributed by Mario Carneiro, 8-Sep-2014.)
|- A = (AbsVal ` R )   &    |- .0. = ( 0g ` R )   =>    |- ( F e. A -> ( F ` .0. ) = 0 )
Theorem	abv1z 18832	The absolute value of one is one in a non-trivial ring. (Contributed by Mario Carneiro, 8-Sep-2014.)
|- A = (AbsVal ` R )   &    |- .1. = ( 1r ` R )   &    |- .0. = ( 0g ` R )   =>    |- ( ( F e. A /\ .1. =/= .0. ) -> ( F ` .1. ) = 1 )
Theorem	abv1 18833	The absolute value of one is one in a division ring. (Contributed by Mario Carneiro, 8-Sep-2014.)
|- A = (AbsVal ` R )   &    |- .1. = ( 1r ` R )   =>    |- ( ( R e. DivRing /\ F e. A ) -> ( F ` .1. ) = 1 )
Theorem	abvneg 18834	The absolute value of a negative is the same as that of the positive. (Contributed by Mario Carneiro, 8-Sep-2014.)
|- A = (AbsVal ` R )   &    |- B = ( Base ` R )   &    |- N = ( invg ` R )   =>    |- ( ( F e. A /\ X e. B ) -> ( F ` ( N ` X ) ) = ( F ` X ) )
Theorem	abvsubtri 18835	An absolute value satisfies the triangle inequality. (Contributed by Mario Carneiro, 4-Oct-2015.)
|- A = (AbsVal ` R )   &    |- B = ( Base ` R )   &    |- .- = ( -g ` R )   =>    |- ( ( F e. A /\ X e. B /\ Y e. B ) -> ( F ` ( X .- Y ) ) <_ ( ( F ` X ) + ( F ` Y ) ) )
Theorem	abvrec 18836	The absolute value distributes under reciprocal. (Contributed by Mario Carneiro, 10-Sep-2014.)
|- A = (AbsVal ` R )   &    |- B = ( Base ` R )   &    |- .0. = ( 0g ` R )   &    |- I = ( invr ` R )   =>    |- ( ( ( R e. DivRing /\ F e. A ) /\ ( X e. B /\ X =/= .0. ) ) -> ( F ` ( I ` X ) ) = ( 1 / ( F ` X ) ) )
Theorem	abvdiv 18837	The absolute value distributes under division. (Contributed by Mario Carneiro, 10-Sep-2014.)
|- A = (AbsVal ` R )   &    |- B = ( Base ` R )   &    |- .0. = ( 0g ` R )   &    |- ./ = (/r ` R )   =>    |- ( ( ( R e. DivRing /\ F e. A ) /\ ( X e. B /\ Y e. B /\ Y =/= .0. ) ) -> ( F ` ( X ./ Y ) ) = ( ( F ` X ) / ( F ` Y ) ) )
Theorem	abvdom 18838	Any ring with an absolute value is a domain, which is to say that it contains no zero divisors. (Contributed by Mario Carneiro, 10-Sep-2014.)
|- A = (AbsVal ` R )   &    |- B = ( Base ` R )   &    |- .0. = ( 0g ` R )   &    |- .x. = ( .r ` R )   =>    |- ( ( F e. A /\ ( X e. B /\ X =/= .0. ) /\ ( Y e. B /\ Y =/= .0. ) ) -> ( X .x. Y ) =/= .0. )
Theorem	abvres 18839	The restriction of an absolute value to a subring is an absolute value. (Contributed by Mario Carneiro, 4-Dec-2014.)
|- A = (AbsVal ` R )   &    |- S = ( R ↾s C )   &    |- B = (AbsVal ` S )   =>    |- ( ( F e. A /\ C e. (SubRing ` R ) ) -> ( F |` C ) e. B )
Theorem	abvtrivd 18840*	The trivial absolute value. (Contributed by Mario Carneiro, 6-May-2015.)
|- A = (AbsVal ` R )   &    |- B = ( Base ` R )   &    |- .0. = ( 0g ` R )   &    |- F = ( x e. B |-> if ( x = .0. , 0 , 1 ) )   &    |- .x. = ( .r ` R )   &    |- ( ph -> R e. Ring )   &    |- ( ( ph /\ ( y e. B /\ y =/= .0. ) /\ ( z e. B /\ z =/= .0. ) ) -> ( y .x. z ) =/= .0. )   =>    |- ( ph -> F e. A )
Theorem	abvtriv 18841*	The trivial absolute value. (This theorem is true as long as R is a domain, but it is not true for rings with zero divisors, which violate the multiplication axiom; abvdom 18838 is the converse of this remark.) (Contributed by Mario Carneiro, 8-Sep-2014.) (Revised by Mario Carneiro, 6-May-2015.)
|- A = (AbsVal ` R )   &    |- B = ( Base ` R )   &    |- .0. = ( 0g ` R )   &    |- F = ( x e. B |-> if ( x = .0. , 0 , 1 ) )   =>    |- ( R e. DivRing -> F e. A )
Theorem	abvpropd 18842*	If two structures have the same ring components, they have the same collection of absolute values. (Contributed by Mario Carneiro, 4-Oct-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 -> (AbsVal ` K ) = (AbsVal ` L ) )
10.5.4  Star rings
Syntax	cstf 18843	Extend class notation with the functionalization of the *-ring involution.
class *rf
Syntax	csr 18844	Extend class notation with class of all *-rings.
class *Ring
Definition	df-staf 18845*	Define the functionalization of the involution in a star ring. This is not strictly necessary but by having *r as an actual function we can state the principal properties of an involution much more cleanly. (Contributed by Mario Carneiro, 6-Oct-2015.)
|- *rf = ( f e. _V |-> ( x e. ( Base ` f ) |-> ( ( *r ` f ) ` x ) ) )
Definition	df-srng 18846*	Define class of all star rings. A star ring is a ring with an involution (conjugation) function. Involution (unlike say the ring zero) is not unique and therefore must be added as a new component to the ring. For example, two possible involutions for complex numbers are the identity function and complex conjugation. Definition of involution in [Holland95] p. 204. (Contributed by NM, 22-Sep-2011.) (Revised by Mario Carneiro, 6-Oct-2015.)
|- *Ring = { f | [. ( *rf ` f ) / i ]. ( i e. ( f RingHom (oppr ` f ) ) /\ i = `' i ) }
Theorem	staffval 18847*	The functionalization of the involution component of a structure. (Contributed by Mario Carneiro, 6-Oct-2015.)
|- B = ( Base ` R )   &    |- .* = ( *r ` R )   &    |- .xb = ( *rf ` R )   =>    |- .xb = ( x e. B |-> ( .* ` x ) )
Theorem	stafval 18848	The functionalization of the involution component of a structure. (Contributed by Mario Carneiro, 6-Oct-2015.)
|- B = ( Base ` R )   &    |- .* = ( *r ` R )   &    |- .xb = ( *rf ` R )   =>    |- ( A e. B -> ( .xb ` A ) = ( .* ` A ) )
Theorem	staffn 18849	The functionalization is equal to the original function, if it is a function on the right base set. (Contributed by Mario Carneiro, 6-Oct-2015.)
|- B = ( Base ` R )   &    |- .* = ( *r ` R )   &    |- .xb = ( *rf ` R )   =>    |- ( .* Fn B -> .xb = .* )
Theorem	issrng 18850	The predicate "is a star ring." (Contributed by NM, 22-Sep-2011.) (Revised by Mario Carneiro, 6-Oct-2015.)
|- O = (oppr ` R )   &    |- .* = ( *rf ` R )   =>    |- ( R e. *Ring <-> ( .* e. ( R RingHom O ) /\ .* = `' .* ) )
Theorem	srngrhm 18851	The involution function in a star ring is an antiautomorphism. (Contributed by Mario Carneiro, 6-Oct-2015.)
|- O = (oppr ` R )   &    |- .* = ( *rf ` R )   =>    |- ( R e. *Ring -> .* e. ( R RingHom O ) )
Theorem	srngring 18852	A star ring is a ring. (Contributed by Mario Carneiro, 6-Oct-2015.)
|- ( R e. *Ring -> R e. Ring )
Theorem	srngcnv 18853	The involution function in a star ring is its own inverse function. (Contributed by Mario Carneiro, 6-Oct-2015.)
|- .* = ( *rf ` R )   =>    |- ( R e. *Ring -> .* = `' .* )
Theorem	srngf1o 18854	The involution function in a star ring is a bijection. (Contributed by Mario Carneiro, 6-Oct-2015.)
|- .* = ( *rf ` R )   &    |- B = ( Base ` R )   =>    |- ( R e. *Ring -> .* : B -1-1-onto-> B )
Theorem	srngcl 18855	The involution function in a star ring is closed in the ring. (Contributed by Mario Carneiro, 6-Oct-2015.)
|- .* = ( *r ` R )   &    |- B = ( Base ` R )   =>    |- ( ( R e. *Ring /\ X e. B ) -> ( .* ` X ) e. B )
Theorem	srngnvl 18856	The involution function in a star ring is an involution. (Contributed by Mario Carneiro, 6-Oct-2015.)
|- .* = ( *r ` R )   &    |- B = ( Base ` R )   =>    |- ( ( R e. *Ring /\ X e. B ) -> ( .* ` ( .* ` X ) ) = X )
Theorem	srngadd 18857	The involution function in a star ring distributes over addition. (Contributed by Mario Carneiro, 6-Oct-2015.)
|- .* = ( *r ` R )   &    |- B = ( Base ` R )   &    |- .+ = ( +g ` R )   =>    |- ( ( R e. *Ring /\ X e. B /\ Y e. B ) -> ( .* ` ( X .+ Y ) ) = ( ( .* ` X ) .+ ( .* ` Y ) ) )
Theorem	srngmul 18858	The involution function in a star ring distributes over multiplication, with a change in the order of the factors. (Contributed by Mario Carneiro, 6-Oct-2015.)
|- .* = ( *r ` R )   &    |- B = ( Base ` R )   &    |- .x. = ( .r ` R )   =>    |- ( ( R e. *Ring /\ X e. B /\ Y e. B ) -> ( .* ` ( X .x. Y ) ) = ( ( .* ` Y ) .x. ( .* ` X ) ) )
Theorem	srng1 18859	The conjugate of the ring identity is the identity. (This is sometimes taken as an axiom, and indeed the proof here follows because we defined *r to be a ring homomorphism, which preserves 1; nevertheless, it is redundant, as can be seen from the proof of issrngd 18861.) (Contributed by Mario Carneiro, 6-Oct-2015.)
|- .* = ( *r ` R )   &    |- .1. = ( 1r ` R )   =>    |- ( R e. *Ring -> ( .* ` .1. ) = .1. )
Theorem	srng0 18860	The conjugate of the ring zero is zero. (Contributed by Mario Carneiro, 7-Oct-2015.)
|- .* = ( *r ` R )   &    |- .0. = ( 0g ` R )   =>    |- ( R e. *Ring -> ( .* ` .0. ) = .0. )
Theorem	issrngd 18861*	Properties that determine a star ring. (Contributed by Mario Carneiro, 18-Nov-2013.) (Revised by Mario Carneiro, 6-Oct-2015.)
|- ( ph -> K = ( Base ` R ) )   &    |- ( ph -> .+ = ( +g ` R ) )   &    |- ( ph -> .x. = ( .r ` R ) )   &    |- ( ph -> .* = ( *r ` R ) )   &    |- ( ph -> R e. Ring )   &    |- ( ( ph /\ x e. K ) -> ( .* ` x ) e. K )   &    |- ( ( ph /\ x e. K /\ y e. K ) -> ( .* ` ( x .+ y ) ) = ( ( .* ` x ) .+ ( .* ` y ) ) )   &    |- ( ( ph /\ x e. K /\ y e. K ) -> ( .* ` ( x .x. y ) ) = ( ( .* ` y ) .x. ( .* ` x ) ) )   &    |- ( ( ph /\ x e. K ) -> ( .* ` ( .* ` x ) ) = x )   =>    |- ( ph -> R e. *Ring )
Theorem	idsrngd 18862*	A commutative ring is a star ring when the conjugate operation is the identity. (Contributed by Thierry Arnoux, 19-Apr-2019.)
|- B = ( Base ` R )   &    |- .* = ( *r ` R )   &    |- ( ph -> R e. CRing )   &    |- ( ( ph /\ x e. B ) -> ( .* ` x ) = x )   =>    |- ( ph -> R e. *Ring )
10.6  Left modules
10.6.1  Definition and basic properties
Syntax	clmod 18863	Extend class notation with class of all left modules.
class LMod
Syntax	cscaf 18864	The functionalization of the scalar multiplication operation.
class .sf
Definition	df-lmod 18865*	Define the class of all left modules, which are generalizations of left vector spaces. A left module over a ring is an (Abelian) group (vectors) together with a ring (scalars) and a left scalar product connecting them. (Contributed by NM, 4-Nov-2013.)
|- LMod = { g e. Grp | [. ( Base ` g ) / v ]. [. ( +g ` g ) / a ]. [. (Scalar ` g ) / f ]. [. ( .s ` g ) / s ]. [. ( Base ` f ) / k ]. [. ( +g ` f ) / p ]. [. ( .r ` f ) / t ]. ( f e. Ring /\ A. q e. k A. r e. k A. x e. v A. w e. v ( ( ( r s w ) e. v /\ ( r s ( w a x ) ) = ( ( r s w ) a ( r s x ) ) /\ ( ( q p r ) s w ) = ( ( q s w ) a ( r s w ) ) ) /\ ( ( ( q t r ) s w ) = ( q s ( r s w ) ) /\ ( ( 1r ` f ) s w ) = w ) ) ) }
Definition	df-scaf 18866*	Define the functionalization of the .s operator. This restricts the value of .s to the stated domain, which is necessary when working with restricted structures, whose operations may be defined on a larger set than the true base. (Contributed by Mario Carneiro, 5-Oct-2015.)
|- .sf = ( g e. _V |-> ( x e. ( Base ` (Scalar ` g ) ) , y e. ( Base ` g ) |-> ( x ( .s ` g ) y ) ) )
Theorem	islmod 18867*	The predicate "is a left module". (Contributed by NM, 4-Nov-2013.) (Revised by Mario Carneiro, 19-Jun-2014.)
|- V = ( Base ` W )   &    |- .+ = ( +g ` W )   &    |- .x. = ( .s ` W )   &    |- F = (Scalar ` W )   &    |- K = ( Base ` F )   &    |- .+^ = ( +g ` F )   &    |- .X. = ( .r ` F )   &    |- .1. = ( 1r ` F )   =>    |- ( W e. LMod <-> ( W e. Grp /\ F e. Ring /\ A. q e. K A. r e. K A. x e. V A. w e. V ( ( ( r .x. w ) e. V /\ ( r .x. ( w .+ x ) ) = ( ( r .x. w ) .+ ( r .x. x ) ) /\ ( ( q .+^ r ) .x. w ) = ( ( q .x. w ) .+ ( r .x. w ) ) ) /\ ( ( ( q .X. r ) .x. w ) = ( q .x. ( r .x. w ) ) /\ ( .1. .x. w ) = w ) ) ) )
Theorem	lmodlema 18868	Lemma for properties of a left module. (Contributed by NM, 8-Dec-2013.) (Revised by Mario Carneiro, 19-Jun-2014.)
|- V = ( Base ` W )   &    |- .+ = ( +g ` W )   &    |- .x. = ( .s ` W )   &    |- F = (Scalar ` W )   &    |- K = ( Base ` F )   &    |- .+^ = ( +g ` F )   &    |- .X. = ( .r ` F )   &    |- .1. = ( 1r ` F )   =>    |- ( ( W e. LMod /\ ( Q e. K /\ R e. K ) /\ ( X e. V /\ Y e. V ) ) -> ( ( ( R .x. Y ) e. V /\ ( R .x. ( Y .+ X ) ) = ( ( R .x. Y ) .+ ( R .x. X ) ) /\ ( ( Q .+^ R ) .x. Y ) = ( ( Q .x. Y ) .+ ( R .x. Y ) ) ) /\ ( ( ( Q .X. R ) .x. Y ) = ( Q .x. ( R .x. Y ) ) /\ ( .1. .x. Y ) = Y ) ) )
Theorem	islmodd 18869*	Properties that determine a left module. See note in isgrpd2 17442 regarding the ph on hypotheses that name structure components. (Contributed by Mario Carneiro, 22-Jun-2014.)
|- ( ph -> V = ( Base ` W ) )   &    |- ( ph -> .+ = ( +g ` W ) )   &    |- ( ph -> F = (Scalar ` W ) )   &    |- ( ph -> .x. = ( .s ` W ) )   &    |- ( ph -> B = ( Base ` F ) )   &    |- ( ph -> .+^ = ( +g ` F ) )   &    |- ( ph -> .X. = ( .r ` F ) )   &    |- ( ph -> .1. = ( 1r ` F ) )   &    |- ( ph -> F e. Ring )   &    |- ( ph -> W e. Grp )   &    |- ( ( ph /\ x e. B /\ y e. V ) -> ( x .x. y ) e. V )   &    |- ( ( ph /\ ( x e. B /\ y e. V /\ z e. V ) ) -> ( x .x. ( y .+ z ) ) = ( ( x .x. y ) .+ ( x .x. z ) ) )   &    |- ( ( ph /\ ( x e. B /\ y e. B /\ z e. V ) ) -> ( ( x .+^ y ) .x. z ) = ( ( x .x. z ) .+ ( y .x. z ) ) )   &    |- ( ( ph /\ ( x e. B /\ y e. B /\ z e. V ) ) -> ( ( x .X. y ) .x. z ) = ( x .x. ( y .x. z ) ) )   &    |- ( ( ph /\ x e. V ) -> ( .1. .x. x ) = x )   =>    |- ( ph -> W e. LMod )
Theorem	lmodgrp 18870	A left module is a group. (Contributed by NM, 8-Dec-2013.) (Revised by Mario Carneiro, 25-Jun-2014.)
|- ( W e. LMod -> W e. Grp )
Theorem	lmodring 18871	The scalar component of a left module is a ring. (Contributed by NM, 8-Dec-2013.) (Revised by Mario Carneiro, 19-Jun-2014.)
|- F = (Scalar ` W )   =>    |- ( W e. LMod -> F e. Ring )
Theorem	lmodfgrp 18872	The scalar component of a left module is an additive group. (Contributed by NM, 8-Dec-2013.) (Revised by Mario Carneiro, 19-Jun-2014.)
|- F = (Scalar ` W )   =>    |- ( W e. LMod -> F e. Grp )
Theorem	lmodbn0 18873	The base set of a left module is nonempty. (Contributed by NM, 8-Dec-2013.) (Revised by Mario Carneiro, 19-Jun-2014.)
|- B = ( Base ` W )   =>    |- ( W e. LMod -> B =/= (/) )
Theorem	lmodacl 18874	Closure of ring addition for a left module. (Contributed by NM, 14-Jan-2014.) (Revised by Mario Carneiro, 19-Jun-2014.)
|- F = (Scalar ` W )   &    |- K = ( Base ` F )   &    |- .+ = ( +g ` F )   =>    |- ( ( W e. LMod /\ X e. K /\ Y e. K ) -> ( X .+ Y ) e. K )
Theorem	lmodmcl 18875	Closure of ring multiplication for a left module. (Contributed by NM, 14-Jan-2014.) (Revised by Mario Carneiro, 19-Jun-2014.)
|- F = (Scalar ` W )   &    |- K = ( Base ` F )   &    |- .x. = ( .r ` F )   =>    |- ( ( W e. LMod /\ X e. K /\ Y e. K ) -> ( X .x. Y ) e. K )
Theorem	lmodsn0 18876	The set of scalars in a left module is nonempty. (Contributed by NM, 8-Dec-2013.) (Revised by Mario Carneiro, 19-Jun-2014.)
|- F = (Scalar ` W )   &    |- B = ( Base ` F )   =>    |- ( W e. LMod -> B =/= (/) )
Theorem	lmodvacl 18877	Closure of vector addition for a left module. (Contributed by NM, 8-Dec-2013.) (Revised by Mario Carneiro, 19-Jun-2014.)
|- V = ( Base ` W )   &    |- .+ = ( +g ` W )   =>    |- ( ( W e. LMod /\ X e. V /\ Y e. V ) -> ( X .+ Y ) e. V )
Theorem	lmodass 18878	Left module vector sum is associative. (Contributed by NM, 10-Jan-2014.) (Revised by Mario Carneiro, 19-Jun-2014.)
|- V = ( Base ` W )   &    |- .+ = ( +g ` W )   =>    |- ( ( W e. LMod /\ ( X e. V /\ Y e. V /\ Z e. V ) ) -> ( ( X .+ Y ) .+ Z ) = ( X .+ ( Y .+ Z ) ) )
Theorem	lmodlcan 18879	Left cancellation law for vector sum. (Contributed by NM, 12-Jan-2014.) (Revised by Mario Carneiro, 19-Jun-2014.)
|- V = ( Base ` W )   &    |- .+ = ( +g ` W )   =>    |- ( ( W e. LMod /\ ( X e. V /\ Y e. V /\ Z e. V ) ) -> ( ( Z .+ X ) = ( Z .+ Y ) <-> X = Y ) )
Theorem	lmodvscl 18880	Closure of scalar product for a left module. (hvmulcl 27870 analog.) (Contributed by NM, 8-Dec-2013.) (Revised by Mario Carneiro, 19-Jun-2014.)
|- V = ( Base ` W )   &    |- F = (Scalar ` W )   &    |- .x. = ( .s ` W )   &    |- K = ( Base ` F )   =>    |- ( ( W e. LMod /\ R e. K /\ X e. V ) -> ( R .x. X ) e. V )
Theorem	scaffval 18881*	The scalar multiplication operation as a function. (Contributed by Mario Carneiro, 5-Oct-2015.)
|- B = ( Base ` W )   &    |- F = (Scalar ` W )   &    |- K = ( Base ` F )   &    |- .xb = ( .sf ` W )   &    |- .x. = ( .s ` W )   =>    |- .xb = ( x e. K , y e. B |-> ( x .x. y ) )
Theorem	scafval 18882	The scalar multiplication operation as a function. (Contributed by Mario Carneiro, 5-Oct-2015.)
|- B = ( Base ` W )   &    |- F = (Scalar ` W )   &    |- K = ( Base ` F )   &    |- .xb = ( .sf ` W )   &    |- .x. = ( .s ` W )   =>    |- ( ( X e. K /\ Y e. B ) -> ( X .xb Y ) = ( X .x. Y ) )
Theorem	scafeq 18883	If the scalar multiplication operation is already a function, the functionalization of it is equal to the original operation. (Contributed by Mario Carneiro, 5-Oct-2015.)
|- B = ( Base ` W )   &    |- F = (Scalar ` W )   &    |- K = ( Base ` F )   &    |- .xb = ( .sf ` W )   &    |- .x. = ( .s ` W )   =>    |- ( .x. Fn ( K X. B ) -> .xb = .x. )
Theorem	scaffn 18884	The scalar multiplication operation is a function. (Contributed by Mario Carneiro, 5-Oct-2015.)
|- B = ( Base ` W )   &    |- F = (Scalar ` W )   &    |- K = ( Base ` F )   &    |- .xb = ( .sf ` W )   =>    |- .xb Fn ( K X. B )
Theorem	lmodscaf 18885	The scalar multiplication operation is a function. (Contributed by Mario Carneiro, 5-Oct-2015.)
|- B = ( Base ` W )   &    |- F = (Scalar ` W )   &    |- K = ( Base ` F )   &    |- .xb = ( .sf ` W )   =>    |- ( W e. LMod -> .xb : ( K X. B ) --> B )
Theorem	lmodvsdi 18886	Distributive law for scalar product (left-distributivity). (ax-hvdistr1 27865 analog.) (Contributed by NM, 10-Jan-2014.) (Revised by Mario Carneiro, 22-Sep-2015.)
|- V = ( Base ` W )   &    |- .+ = ( +g ` W )   &    |- F = (Scalar ` W )   &    |- .x. = ( .s ` W )   &    |- K = ( Base ` F )   =>    |- ( ( W e. LMod /\ ( R e. K /\ X e. V /\ Y e. V ) ) -> ( R .x. ( X .+ Y ) ) = ( ( R .x. X ) .+ ( R .x. Y ) ) )
Theorem	lmodvsdir 18887	Distributive law for scalar product (right-distributivity). (ax-hvdistr1 27865 analog.) (Contributed by NM, 10-Jan-2014.) (Revised by Mario Carneiro, 22-Sep-2015.)
|- V = ( Base ` W )   &    |- .+ = ( +g ` W )   &    |- F = (Scalar ` W )   &    |- .x. = ( .s ` W )   &    |- K = ( Base ` F )   &    |- .+^ = ( +g ` F )   =>    |- ( ( W e. LMod /\ ( Q e. K /\ R e. K /\ X e. V ) ) -> ( ( Q .+^ R ) .x. X ) = ( ( Q .x. X ) .+ ( R .x. X ) ) )
Theorem	lmodvsass 18888	Associative law for scalar product. (ax-hvmulass 27864 analog.) (Contributed by NM, 10-Jan-2014.) (Revised by Mario Carneiro, 22-Sep-2015.)
|- V = ( Base ` W )   &    |- F = (Scalar ` W )   &    |- .x. = ( .s ` W )   &    |- K = ( Base ` F )   &    |- .X. = ( .r ` F )   =>    |- ( ( W e. LMod /\ ( Q e. K /\ R e. K /\ X e. V ) ) -> ( ( Q .X. R ) .x. X ) = ( Q .x. ( R .x. X ) ) )
Theorem	lmod0cl 18889	The ring zero in a left module belongs to the ring base set. (Contributed by NM, 11-Jan-2014.) (Revised by Mario Carneiro, 19-Jun-2014.)
|- F = (Scalar ` W )   &    |- K = ( Base ` F )   &    |- .0. = ( 0g ` F )   =>    |- ( W e. LMod -> .0. e. K )
Theorem	lmod1cl 18890	The ring unit in a left module belongs to the ring base set. (Contributed by NM, 11-Jan-2014.) (Revised by Mario Carneiro, 19-Jun-2014.)
|- F = (Scalar ` W )   &    |- K = ( Base ` F )   &    |- .1. = ( 1r ` F )   =>    |- ( W e. LMod -> .1. e. K )
Theorem	lmodvs1 18891	Scalar product with ring unit. (ax-hvmulid 27863 analog.) (Contributed by NM, 10-Jan-2014.) (Revised by Mario Carneiro, 19-Jun-2014.)
|- V = ( Base ` W )   &    |- F = (Scalar ` W )   &    |- .x. = ( .s ` W )   &    |- .1. = ( 1r ` F )   =>    |- ( ( W e. LMod /\ X e. V ) -> ( .1. .x. X ) = X )
Theorem	lmod0vcl 18892	The zero vector is a vector. (ax-hv0cl 27860 analog.) (Contributed by NM, 10-Jan-2014.) (Revised by Mario Carneiro, 19-Jun-2014.)
|- V = ( Base ` W )   &    |- .0. = ( 0g ` W )   =>    |- ( W e. LMod -> .0. e. V )
Theorem	lmod0vlid 18893	Left identity law for the zero vector. (hvaddid2 27880 analog.) (Contributed by NM, 10-Jan-2014.) (Revised by Mario Carneiro, 19-Jun-2014.)
|- V = ( Base ` W )   &    |- .+ = ( +g ` W )   &    |- .0. = ( 0g ` W )   =>    |- ( ( W e. LMod /\ X e. V ) -> ( .0. .+ X ) = X )
Theorem	lmod0vrid 18894	Right identity law for the zero vector. (ax-hvaddid 27861 analog.) (Contributed by NM, 10-Jan-2014.) (Revised by Mario Carneiro, 19-Jun-2014.)
|- V = ( Base ` W )   &    |- .+ = ( +g ` W )   &    |- .0. = ( 0g ` W )   =>    |- ( ( W e. LMod /\ X e. V ) -> ( X .+ .0. ) = X )
Theorem	lmod0vid 18895	Identity equivalent to the value of the zero vector. Provides a convenient way to compute the value. (Contributed by NM, 9-Mar-2014.) (Revised by Mario Carneiro, 19-Jun-2014.)
|- V = ( Base ` W )   &    |- .+ = ( +g ` W )   &    |- .0. = ( 0g ` W )   =>    |- ( ( W e. LMod /\ X e. V ) -> ( ( X .+ X ) = X <-> .0. = X ) )
Theorem	lmod0vs 18896	Zero times a vector is the zero vector. Equation 1a of [Kreyszig] p. 51. (ax-hvmul0 27867 analog.) (Contributed by NM, 12-Jan-2014.) (Revised by Mario Carneiro, 19-Jun-2014.)
|- V = ( Base ` W )   &    |- F = (Scalar ` W )   &    |- .x. = ( .s ` W )   &    |- O = ( 0g ` F )   &    |- .0. = ( 0g ` W )   =>    |- ( ( W e. LMod /\ X e. V ) -> ( O .x. X ) = .0. )
Theorem	lmodvs0 18897	Anything times the zero vector is the zero vector. Equation 1b of [Kreyszig] p. 51. (hvmul0 27881 analog.) (Contributed by NM, 12-Jan-2014.) (Revised by Mario Carneiro, 19-Jun-2014.)
|- F = (Scalar ` W )   &    |- .x. = ( .s ` W )   &    |- K = ( Base ` F )   &    |- .0. = ( 0g ` W )   =>    |- ( ( W e. LMod /\ X e. K ) -> ( X .x. .0. ) = .0. )
Theorem	lmodvsmmulgdi 18898	Distributive law for a group multiple of a scalar multiplication. (Contributed by AV, 2-Sep-2019.)
|- V = ( Base ` W )   &    |- F = (Scalar ` W )   &    |- .x. = ( .s ` W )   &    |- K = ( Base ` F )   &    |- .^ = (.g ` W )   &    |- E = (.g ` F )   =>    |- ( ( W e. LMod /\ ( C e. K /\ N e. NN0 /\ X e. V ) ) -> ( N .^ ( C .x. X ) ) = ( ( N E C ) .x. X ) )
Theorem	lmodfopnelem1 18899	Lemma 1 for lmodfopne 18901. (Contributed by AV, 2-Oct-2021.)
|- .x. = ( .sf ` W )   &    |- .+ = ( +f ` W )   &    |- V = ( Base ` W )   &    |- S = (Scalar ` W )   &    |- K = ( Base ` S )   =>    |- ( ( W e. LMod /\ .+ = .x. ) -> V = K )
Theorem	lmodfopnelem2 18900	Lemma 2 for lmodfopne 18901. (Contributed by AV, 2-Oct-2021.)
|- .x. = ( .sf ` W )   &    |- .+ = ( +f ` W )   &    |- V = ( Base ` W )   &    |- S = (Scalar ` W )   &    |- K = ( Base ` S )   &    |- .0. = ( 0g ` S )   &    |- .1. = ( 1r ` S )   =>    |- ( ( W e. LMod /\ .+ = .x. ) -> ( .0. e. V /\ .1. e. V ) )