environ
vocabularies HIDDEN, ARYTM_3, POLYNOM2, POLYNOM1, ARYTM_1, FUNCT_1, FINSEQ_5, POLYNOM3, RELAT_1, RLVECT_1, FINSEQ_1, GCD_1, VECTSP_1, CARD_1, ALGSEQ_1, ALGSTR_1, CARD_3, SGRAPH1, INT_1, FUNCT_4, ALGSTR_0, POLYNOM5, RFINSEQ, MCART_1, HURWITZ, ZFMISC_1, XBOOLE_0, TARSKI, YELLOW_8, LATTICES, XCMPLX_0, VECTSP_2, MSALIMIT, STRUCT_0, SUBSET_1, SUPINF_2, NAT_1, NUMBERS, MESFUNC1, XXREAL_0, RATFUNC1, GROUP_1, FINSEQ_3, BINOP_1, PARTFUN1, ORDINAL4, ORDINAL1;
notations HIDDEN, TARSKI, SUBSET_1, ORDINAL1, XCMPLX_0, PARTFUN1, XXREAL_0, NAT_D, GROUP_4, FUNCT_7, VECTSP_2, NUMBERS, XTUPLE_0, MCART_1, ALGSTR_0, ALGSTR_1, VECTSP_1, RLVECT_1, ARYTM_3, RELSET_1, FINSEQ_1, FUNCT_1, FUNCT_2, GROUP_1, INT_1, NAT_1, FINSEQ_3, VFUNCT_1, RFINSEQ, NORMSP_1, POLYNOM3, POLYNOM4, FINSEQ_5, POLYNOM5, STRUCT_0, ALGSEQ_1, HURWITZ;
definitions STRUCT_0, ALGSTR_0, VECTSP_2;
theorems GROUP_1, VECTSP_1, ALGSEQ_1, NAT_1, FUNCT_1, FUNCT_2, XREAL_1, VECTSP_2, INT_1, FINSEQ_1, RLVECT_1, POLYNOM4, FUNCT_7, TARSKI, POLYNOM3, POLYNOM2, FUNCOP_1, POLYNOM5, XXREAL_0, FINSEQ_3, ORDINAL1, PARTFUN1, HURWITZ, STRUCT_0, XREAL_0, FINSEQ_4, GROUP_4, ALGSTR_0, FINSEQ_5, RFINSEQ, XTUPLE_0;
schemes NAT_1, INT_1;
registrations XBOOLE_0, ORDINAL1, RELSET_1, XCMPLX_0, XXREAL_0, XREAL_0, NAT_1, INT_1, MEMBERED, FINSEQ_1, STRUCT_0, VECTSP_1, ALGSTR_1, GCD_1, POLYNOM3, POLYNOM4, POLYNOM5, POLYNOM1, FUNCT_2, VFUNCT_1, CARD_1, RELAT_1, XTUPLE_0;
constructors HIDDEN, BINOP_1, REAL_1, SQUARE_1, VECTSP_2, POLYNOM4, POLYNOM5, XTUPLE_0, ALGSTR_2, HURWITZ, FUNCT_4, RELSET_1, ARYTM_3, FUNCT_7, GROUP_4, NAT_D, VFUNCT_1, RFINSEQ, FINSEQ_5, NAT_1, ALGSEQ_1;
requirements HIDDEN, NUMERALS, SUBSET, REAL, BOOLE, ARITHM;
equalities FINSEQ_1, POLYNOM3, VECTSP_1, FINSEQ_5, HURWITZ, ALGSTR_0;
expansions FINSEQ_1, STRUCT_0, ALGSTR_0, VECTSP_2, HURWITZ;
Lm1:
for L being non trivial right_complementable well-unital distributive Abelian add-associative right_zeroed associative commutative domRing-like doubleLoopStr
for z being rational_function of L st z is irreducible holds
ex z1 being rational_function of L ex z2 being non zero Polynomial of L st
( z = [(z2 *' (z1 `1)),(z2 *' (z1 `2))] & z1 is irreducible & ex f being FinSequence of (Polynom-Ring L) st
( z2 = Product f & ( for i being Element of NAT st i in dom f holds
ex x being Element of L st
( x is_a_common_root_of z `1 ,z `2 & f . i = rpoly (1,x) ) ) ) )
Lm2:
for L being non trivial right_complementable almost_left_invertible well-unital distributive Abelian add-associative right_zeroed associative commutative domRing-like doubleLoopStr
for z being rational_function of L st z is irreducible holds
for z1 being rational_function of L
for z2 being non zero Polynomial of L st z = [(z2 *' (z1 `1)),(z2 *' (z1 `2))] & z1 is irreducible & ex f being FinSequence of (Polynom-Ring L) st
( z2 = Product f & ( for i being Element of NAT st i in dom f holds
ex x being Element of L st
( x is_a_common_root_of z `1 ,z `2 & f . i = rpoly (1,x) ) ) ) holds
for g1 being rational_function of L
for g2 being non zero Polynomial of L st z = [(g2 *' (g1 `1)),(g2 *' (g1 `2))] & g1 is irreducible & ex f being FinSequence of (Polynom-Ring L) st
( g2 = Product f & ( for i being Element of NAT st i in dom f holds
ex x being Element of L st
( x is_a_common_root_of z `1 ,z `2 & f . i = rpoly (1,x) ) ) ) holds
( z2 = 1_. L & g2 = 1_. L & z1 = g1 )
Lm3:
for L being non trivial right_complementable almost_left_invertible well-unital distributive Abelian add-associative right_zeroed associative commutative domRing-like doubleLoopStr
for z being non zero rational_function of L
for z1 being rational_function of L
for z2 being non zero Polynomial of L st z = [(z2 *' (z1 `1)),(z2 *' (z1 `2))] & z1 is irreducible & ex f being FinSequence of (Polynom-Ring L) st
( z2 = Product f & ( for i being Element of NAT st i in dom f holds
ex x being Element of L st
( x is_a_common_root_of z `1 ,z `2 & f . i = rpoly (1,x) ) ) ) holds
for g1 being rational_function of L
for g2 being non zero Polynomial of L st z = [(g2 *' (g1 `1)),(g2 *' (g1 `2))] & g1 is irreducible & ex g being FinSequence of (Polynom-Ring L) st
( g2 = Product g & ( for i being Element of NAT st i in dom g holds
ex x being Element of L st
( x is_a_common_root_of z `1 ,z `2 & g . i = rpoly (1,x) ) ) ) holds
z1 = g1
definition
let L be non
trivial right_complementable almost_left_invertible well-unital distributive Abelian add-associative right_zeroed associative commutative domRing-like doubleLoopStr ;
let z be
rational_function of
L;
existence
( ( not z is zero implies ex b1, z1 being rational_function of L ex z2 being non zero Polynomial of L st
( z = [(z2 *' (z1 `1)),(z2 *' (z1 `2))] & z1 is irreducible & b1 = NormRationalFunction z1 & ex f being FinSequence of (Polynom-Ring L) st
( z2 = Product f & ( for i being Element of NAT st i in dom f holds
ex x being Element of L st
( x is_a_common_root_of z `1 ,z `2 & f . i = rpoly (1,x) ) ) ) ) ) & ( z is zero implies ex b1 being rational_function of L st b1 = 0._ L ) )
uniqueness
for b1, b2 being rational_function of L holds
( ( not z is zero & ex z1 being rational_function of L ex z2 being non zero Polynomial of L st
( z = [(z2 *' (z1 `1)),(z2 *' (z1 `2))] & z1 is irreducible & b1 = NormRationalFunction z1 & ex f being FinSequence of (Polynom-Ring L) st
( z2 = Product f & ( for i being Element of NAT st i in dom f holds
ex x being Element of L st
( x is_a_common_root_of z `1 ,z `2 & f . i = rpoly (1,x) ) ) ) ) & ex z1 being rational_function of L ex z2 being non zero Polynomial of L st
( z = [(z2 *' (z1 `1)),(z2 *' (z1 `2))] & z1 is irreducible & b2 = NormRationalFunction z1 & ex f being FinSequence of (Polynom-Ring L) st
( z2 = Product f & ( for i being Element of NAT st i in dom f holds
ex x being Element of L st
( x is_a_common_root_of z `1 ,z `2 & f . i = rpoly (1,x) ) ) ) ) implies b1 = b2 ) & ( z is zero & b1 = 0._ L & b2 = 0._ L implies b1 = b2 ) )
by Lm3;
consistency
for b1 being rational_function of L holds verum
;
end;
Lm4:
for L being non trivial right_complementable almost_left_invertible well-unital distributive Abelian add-associative right_zeroed associative commutative domRing-like doubleLoopStr
for z being non zero irreducible rational_function of L holds NF z = NormRationalFunction z
Lm5:
for L being non trivial right_complementable distributive Abelian add-associative right_zeroed unital domRing-like left_zeroed doubleLoopStr
for p1, p2 being Polynomial of L holds
( not p1 *' p2 = 0_. L or p1 = 0_. L or p2 = 0_. L )
Lm6:
for L being non trivial right_complementable almost_left_invertible well-unital distributive Abelian add-associative right_zeroed associative commutative domRing-like doubleLoopStr
for z being non zero rational_function of L st z is irreducible holds
degree z = max ((degree (z `1)),(degree (z `2)))