environ
vocabularies HIDDEN, ARYTM_3, FUNCT_1, RELAT_1, RLVECT_1, GCD_1, WELLORD1, ORDINAL4, VECTSP_1, CARD_3, ALGSTR_0, XBOOLE_0, TARSKI, INT_1, FUNCT_2, TREES_2, XCMPLX_0, VECTSP_2, VECTSP10, STRUCT_0, SUBSET_1, SUPINF_2, REARRAN1, NAT_1, CARD_1, MESFUNC1, INT_3, GROUP_1, ARYTM_1, FINSEQ_1, SETFAM_1, INT_2, YELLOW_8, QUOFIELD, MSSUBFAM, BINOP_1, GROUP_4, GROUP_6, MOD_4, LATTICES, HURWITZ, NUMBERS, IDEAL_1, REALSET1, C0SP1, RATFUNC1, EQREL_1, POLYNOM1, POLYNOM3, ZFMISC_1, FUNCSDOM, WAYBEL20, CARD_FIL, RING_1, RING_2, PARTFUN1, FINSEQ_3, WAYBEL_6, FUNCOP_1, XXREAL_0;
notations HIDDEN, TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, DOMAIN_1, RELAT_1, FUNCT_1, SETFAM_1, RELSET_1, PARTFUN1, FUNCT_2, FUNCOP_1, BINOP_1, REALSET1, FINSEQ_1, VFUNCT_1, ORDINAL1, EQREL_1, XCMPLX_0, XXREAL_0, NAT_1, INT_1, INT_2, INT_3, NUMBERS, VECTSP_1, VECTSP_2, QUOFIELD, STRUCT_0, ALGSTR_0, GROUP_1, RLVECT_1, GCD_1, POLYNOM3, HURWITZ, IDEAL_1, GROUP_4, GROUP_6, VECTSP10, MOD_4, C0SP1, RATFUNC1, RING_1;
definitions RELAT_1, FUNCT_2, VECTSP_1, GROUP_1, GROUP_6, IDEAL_1, INT_3;
theorems ALGSTR_0, GROUP_1, GROUP_6, VECTSP_1, VECTSP_2, RLVECT_1, IDEAL_1, GCD_1, SUBSET_1, FUNCT_2, TARSKI, FUNCT_1, C0SP1, POLYNOM3, RING_1, REALSET1, HURWITZ, INT_3, RATFUNC1, ZFMISC_1, NAT_1, INT_1, INT_2, INT_5, XBOOLE_0, FINSEQ_1, FINSEQ_2, ORDINAL1, XXREAL_0, FUNCOP_1, GROUP_4, XREAL_1, FINSEQ_3, POLYNOM2, PARTFUN1;
schemes NAT_1, FUNCT_2, RECDEF_1;
registrations XBOOLE_0, ORDINAL1, RELSET_1, XREAL_0, NAT_1, INT_1, MEMBERED, FINSEQ_1, STRUCT_0, VECTSP_1, ALGSTR_1, SUBSET_1, RELAT_1, FUNCT_2, ALGSTR_0, RLVECT_1, QUOFIELD, REALSET1, VFUNCT_1, RATFUNC1, IDEAL_1, MOD_4, RINGCAT1, RING_1, C0SP1, XCMPLX_0, XXREAL_0, INT_3, VALUED_0, FUNCT_1, PARTFUN1, CARD_1, GRCAT_1, GROUP_6;
constructors HIDDEN, RING_1, C0SP1, BINOM, RELSET_1, GCD_1, QUOFIELD, BINOP_2, VFUNCT_1, RATFUNC1, MOD_4, GROUP_6, REALSET1, INT_3, RINGCAT1, GROUP_4, HURWITZ, VECTSP10, INT_2;
requirements HIDDEN, NUMERALS, SUBSET, BOOLE, REAL, ARITHM;
equalities BINOP_1, REALSET1, XCMPLX_0, STRUCT_0, ALGSTR_0, FINSEQ_1, VECTSP10;
expansions STRUCT_0, GROUP_1, ALGSTR_0, RLVECT_1, VECTSP_1, IDEAL_1, XBOOLE_0, FUNCT_1, QUOFIELD, GROUP_6, TARSKI, GCD_1;
ch1:
for X being non empty set
for C being ascending Chain of X
for x being object
for i, j being Nat st i <= j & x in C . i holds
x in C . j
hom3:
for E, F being Field
for f being additive multiplicative Function of E,F holds
( ( f . (1. E) = 0. F & f = E --> (0. F) ) or ( f . (1. E) = 1. F & f is monomorphism ) )
ker1:
for R, S being non empty doubleLoopStr
for f being Function of R,S
for x being Element of R st x in ker f holds
f . x = 0. S
T0:
for R being Ring
for S being b1 -homomorphic Ring
for f being Homomorphism of R,S holds 0. S in rng f
T1:
for R being Ring
for S being b1 -homomorphic Ring
for f being Homomorphism of R,S holds 1. S in rng f
T3:
for R being Ring
for S being b1 -homomorphic Ring
for f being Homomorphism of R,S holds rng f is Preserv of the addF of S
T4:
for R being Ring
for S being b1 -homomorphic Ring
for f being Homomorphism of R,S holds rng f is Preserv of the multF of S
T5:
for R being Ring
for S being b1 -homomorphic Ring
for f being Homomorphism of R,S
for a, b being Element of (Image f)
for x, y being Element of S st a = x & b = y holds
( a + b = x + y & a * b = x * y )
T6:
for R being Ring
for S being b1 -homomorphic Ring
for f being Homomorphism of R,S
for a being Element of (Image f) ex x being Element of R st f . x = a
definition
let R be
Ring;
let S be
R -homomorphic Ring;
let f be
Homomorphism of
R,
S;
existence
ex b1 being Function of (R / (ker f)),(Image f) st
for a being Element of R holds b1 . (Class ((EqRel (R,(ker f))),a)) = f . a
uniqueness
for b1, b2 being Function of (R / (ker f)),(Image f) st ( for a being Element of R holds b1 . (Class ((EqRel (R,(ker f))),a)) = f . a ) & ( for a being Element of R holds b2 . (Class ((EqRel (R,(ker f))),a)) = f . a ) holds
b1 = b2
end;
lemintr:
for x, y being Integer
for a, b being Element of INT.Ring st x <> 0 & x = a & y = b holds
( x divides y iff a divides b )
fact1:
for R being non empty right_unital doubleLoopStr
for a being Element of R holds
( a is irreducible iff <*a*> is_a_factorization_of a )
lemfactunique1:
for R being domRing
for a, b, x being Element of R
for F being non empty FinSequence of R st x is prime & x divides a & a is_associated_to b & F is_a_factorization_of b holds
ex i being Element of dom F st F . i is_associated_to x
lemfactunique:
for R being PIDomain
for x, y being Element of R
for F, G being non empty FinSequence of R st F is_a_factorization_of x & G is_a_factorization_of y & x is_associated_to y holds
ex p being Function of (dom F),(dom G) st
( p is bijective & ( for i being Element of dom F holds G . (p . i) is_associated_to F . i ) )
thEucl2:
for L being Field ex f being Function of (Polynom-Ring L),NAT st
for p, q being Element of (Polynom-Ring L) st q <> 0. (Polynom-Ring L) holds
ex u, r being Element of (Polynom-Ring L) st
( p = (u * q) + r & ( r = 0. (Polynom-Ring L) or f . r < f . q ) )