environ
vocabularies HIDDEN, INT_1, VECTSP_1, FUNCT_1, ARYTM_3, ZFMISC_1, RELAT_1, RLVECT_1, FUNCOP_1, ARYTM_1, BINOP_1, FUNCSDOM, REALSET1, LATTICES, GROUP_1, ORDINAL2, IDEAL_1, FINSEQ_1, SUBSET_1, VECTSP_2, FUNCT_3, NUMBERS, GROUP_4, STRUCT_0, RLSUB_1, XXREAL_2, ALGSTR_0, XCMPLX_0, REALSET2, NAT_1, REAL_1, INT_2, XXREAL_0, TARSKI, XREAL_0, XBOOLE_0, NEWTON, CARD_FIL, RMOD_2, CARD_1, SUPINF_2, MESFUNC1, PARTFUN1, COMPLEX1, MEMBERED, MSSUBFAM, FVALUAT1;
notations HIDDEN, TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, ORDINAL1, NUMBERS, DOMAIN_1, RELAT_1, FUNCT_1, RELSET_1, PARTFUN1, FUNCT_2, FUNCOP_1, XXREAL_0, XREAL_0, XXREAL_2, XXREAL_3, XCMPLX_0, REAL_1, INT_1, MEMBERED, SUPINF_2, EXTREAL1, INT_2, MESFUNC1, FINSEQ_1, FINSEQ_4, REALSET1, BINOP_1, STRUCT_0, ALGSTR_0, RLVECT_1, GRCAT_1, GROUP_1, YELLOW_9, VECTSP_1, VECTSP_2, REALSET2, RMOD_2, IDEAL_1, RING_1;
definitions TARSKI, XBOOLE_0, SUBSET_1, FUNCT_2, XREAL_0, XXREAL_2, REALSET1, RING_1, STRUCT_0, ALGSTR_0, RLVECT_1, GROUP_1, VECTSP_1, VECTSP_2, IDEAL_1, RMOD_2;
theorems VECTSP_1, FUNCOP_1, TARSKI, FUNCT_1, INT_1, RLVECT_1, XREAL_0, VECTSP_2, XBOOLE_0, FUNCT_2, ABSVALUE, NAT_1, ZFMISC_1, REALSET1, FINSEQ_1, FINSEQ_3, XBOOLE_1, TOPREALA, FINSEQ_5, GROUP_1, IDEAL_1, RMOD_2, YELLOW_9, RELAT_1, RING_1, XXREAL_0, ORDINAL1, XXREAL_3, PARTFUN1, ALGSTR_0, XXREAL_2, SUBSET_1, CARD_1;
schemes NAT_1, INT_1, RECDEF_1, FUNCT_2;
registrations RELSET_1, VECTSP_1, INT_1, XREAL_0, ALGSTR_1, VECTSP_2, STRUCT_0, NAT_1, SUBSET_1, WAYBEL_2, XBOOLE_0, RMOD_2, XCMPLX_0, IDEAL_1, RING_1, XXREAL_0, NUMBERS, MEMBERED, ORDINAL1, ALGSTR_0, XXREAL_3, REALSET2, FINSEQ_1, CARD_1;
constructors HIDDEN, REAL_1, FINSEQ_4, SUPINF_2, EXTREAL1, MESFUNC1, RMOD_2, YELLOW_9, RING_1, BINOM, FUNCOP_1, REALSET2, RELSET_1, GRCAT_1, NEWTON;
requirements HIDDEN, NUMERALS, ARITHM, REAL, BOOLE, SUBSET;
equalities BINOP_1, XCMPLX_0, XXREAL_3, REALSET1, MESFUNC1, STRUCT_0, ALGSTR_0, VECTSP_2, IDEAL_1, SUPINF_2;
expansions TARSKI, XBOOLE_0, SUBSET_1, VECTSP_1, IDEAL_1;
Lm2:
for n being Nat
for K being non empty non degenerated right_complementable distributive Abelian add-associative right_zeroed associative Field-like doubleLoopStr
for a being Element of K holds a |^ (n + 1) = (a |^ n) * a
by GROUP_1:def 7;
Lm3:
for n being Nat
for K being non empty non degenerated right_complementable distributive Abelian add-associative right_zeroed associative Field-like doubleLoopStr
for a being Element of K st a <> 0. K holds
a |^ n <> 0. K
Lm4:
for a, b being ExtInt st a <= b holds
0 <= b - a
Lm5:
for K being non empty non degenerated right_complementable distributive Abelian add-associative right_zeroed associative Field-like doubleLoopStr
for v being Valuation of K st K is having_valuation holds
least-positive (rng v) in rng v
Lm6:
for K being non empty non degenerated right_complementable distributive Abelian add-associative right_zeroed associative Field-like doubleLoopStr
for v being Valuation of K st K is having_valuation holds
least-positive (rng v) in REAL
Lm7:
for K being non empty non degenerated right_complementable distributive Abelian add-associative right_zeroed associative Field-like doubleLoopStr
for a, b being Element of K st a <> 0. K holds
(a ") * (a * b) = b
Lm8:
for K being non empty non degenerated right_complementable distributive Abelian add-associative right_zeroed associative Field-like doubleLoopStr
for x, v being Element of K st x <> 0. K holds
x * ((x ") * v) = v
theorem
for
R being
Ring for
P being
Ideal of
R for
M being
Submodule of
P for
a being
BinOp of
P for
z being
Element of
P for
m being
Function of
[:P, the carrier of R:],
P st
a = the
addF of
R | [:P,P:] &
m = the
multF of
R | [:P, the carrier of R:] &
z = the
ZeroF of
R holds
RightModStr(# the
carrier of
M, the
addF of
M, the
ZeroF of
M, the
rmult of
M #)
= RightModStr(#
P,
a,
z,
m #)