begin
theorem Th1:
theorem Th2:
theorem Th3:
theorem
theorem Th5:
theorem
theorem Th7:
theorem Th8:
theorem Th9:
:: deftheorem Def1 defines ext-integer FVALUAT1:def 1 :
for x being number holds
( x is ext-integer iff ( x is integer or x = +infty ) );
theorem Th11:
theorem
:: deftheorem Def4 defines least-positive FVALUAT1:def 2 :
for X being ext-real-membered set st ex i0 being positive ExtInt st i0 in X holds
for b2 being positive ExtInt holds
( b2 = least-positive X iff ( b2 in X & ( for i being positive ExtInt st i in X holds
b2 <= i ) ) );
:: deftheorem Def5 defines e.i.-valued FVALUAT1:def 3 :
for f being Relation holds
( f is e.i.-valued iff for x being set st x in rng f holds
x is ext-integer );
begin
theorem Th13:
:: deftheorem Def6 defines |^ FVALUAT1:def 4 :
for K being non empty doubleLoopStr
for S being Subset of K
for n being Nat
for b4 being Subset of K holds
( ( n = 0 implies ( b4 = S |^ n iff b4 = the carrier of K ) ) & ( not n = 0 implies ( b4 = S |^ n iff ex f being FinSequence of bool the carrier of K st
( b4 = f . (len f) & len f = n & f . 1 = S & ( for i being Nat st i in dom f & i + 1 in dom f holds
f . (i + 1) = S *' (f /. i) ) ) ) ) );
theorem
theorem
:: deftheorem Def7 defines |^ FVALUAT1:def 5 :
for G being non empty doubleLoopStr
for g being Element of G
for i being Integer holds
( ( 0 <= i implies g |^ i = (power G) . (g,(abs i)) ) & ( not 0 <= i implies g |^ i = ((power G) . (g,(abs i))) " ) );
:: deftheorem defines |^ FVALUAT1:def 6 :
for G being non empty doubleLoopStr
for g being Element of G
for n being Nat holds g |^ n = (power G) . (g,n);
Lm4:
for n being Nat
for K being non empty non degenerated right_complementable associative distributive Abelian add-associative right_zeroed Field-like doubleLoopStr
for a being Element of K holds a |^ (n + 1) = (a |^ n) * a
theorem
Lm5:
for n being Nat
for K being non empty non degenerated right_complementable associative distributive Abelian add-associative right_zeroed Field-like doubleLoopStr
for a being Element of K st a <> 0. K holds
a |^ n <> 0. K
theorem Th17:
begin
:: deftheorem Def9 defines having_valuation FVALUAT1:def 7 :
for K being doubleLoopStr holds
( K is having_valuation iff ex f being e.i.-valued Function of K,ExtREAL st
( f . (0. K) = +infty & ( for a being Element of K st a <> 0. K holds
f . a in INT ) & ( for a, b being Element of K holds f . (a * b) = (f . a) + (f . b) ) & ( for a being Element of K st 0 <= f . a holds
0 <= f . ((1. K) + a) ) & ex a being Element of K st
( f . a <> 0 & f . a <> +infty ) ) );
:: deftheorem Def10 defines Valuation FVALUAT1:def 8 :
for K being doubleLoopStr st K is having_valuation holds
for b2 being e.i.-valued Function of K,ExtREAL holds
( b2 is Valuation of K iff ( b2 . (0. K) = +infty & ( for a being Element of K st a <> 0. K holds
b2 . a in INT ) & ( for a, b being Element of K holds b2 . (a * b) = (b2 . a) + (b2 . b) ) & ( for a being Element of K st 0 <= b2 . a holds
0 <= b2 . ((1. K) + a) ) & ex a being Element of K st
( b2 . a <> 0 & b2 . a <> +infty ) ) );
theorem Th18:
theorem Th19:
theorem Th20:
theorem Th21:
theorem Th22:
theorem Th23:
theorem Th24:
theorem Th25:
theorem Th26:
theorem Th27:
theorem Th28:
theorem Th29:
theorem Th30:
theorem Th31:
theorem
Lm6:
for a, b being ExtInt st a <= b holds
0 <= b - a
theorem
theorem Th34:
Th35:
for K being non empty non degenerated right_complementable associative distributive Abelian add-associative right_zeroed Field-like doubleLoopStr
for v being Valuation of K st K is having_valuation holds
least-positive (rng v) in rng v
theorem Th36:
theorem Th38:
Lm7:
for K being non empty non degenerated right_complementable associative distributive Abelian add-associative right_zeroed Field-like doubleLoopStr
for v being Valuation of K st K is having_valuation holds
least-positive (rng v) in REAL
theorem Th39:
:: deftheorem Def11 defines Pgenerator FVALUAT1:def 9 :
for K being non empty non degenerated right_complementable associative distributive Abelian add-associative right_zeroed Field-like doubleLoopStr
for v being Valuation of K st K is having_valuation holds
Pgenerator v = the Element of v " {(least-positive (rng v))};
:: deftheorem Def12 defines normal-valuation FVALUAT1:def 10 :
for K being non empty non degenerated right_complementable associative distributive Abelian add-associative right_zeroed Field-like doubleLoopStr
for v being Valuation of K st K is having_valuation holds
for b3 being Valuation of K holds
( b3 = normal-valuation v iff for a being Element of K holds v . a = (b3 . a) * (least-positive (rng v)) );
theorem Th40:
theorem Th41:
theorem
theorem Th43:
theorem Th44:
theorem
theorem Th46:
theorem
theorem
theorem
begin
:: deftheorem defines NonNegElements FVALUAT1:def 11 :
for K being non empty doubleLoopStr
for v being Valuation of K holds NonNegElements v = { x where x is Element of K : 0 <= v . x } ;
theorem Th50:
theorem Th51:
theorem Th52:
theorem Th53:
:: deftheorem Def14 defines ValuatRing FVALUAT1:def 12 :
for K being non empty non degenerated right_complementable associative distributive Abelian add-associative right_zeroed Field-like doubleLoopStr
for v being Valuation of K st K is having_valuation holds
for b3 being non degenerated strict commutative Ring holds
( b3 = ValuatRing v iff ( the carrier of b3 = NonNegElements v & the addF of b3 = the addF of K | [:(NonNegElements v),(NonNegElements v):] & the multF of b3 = the multF of K | [:(NonNegElements v),(NonNegElements v):] & the ZeroF of b3 = 0. K & the OneF of b3 = 1. K ) );
theorem Th54:
theorem Th55:
theorem Th56:
theorem Th57:
theorem Th58:
theorem
theorem
theorem
Lm8:
for K being non empty non degenerated right_complementable associative distributive Abelian add-associative right_zeroed Field-like doubleLoopStr
for a, b being Element of K st a <> 0. K holds
(a ") * (a * b) = b
Lm9:
for K being non empty non degenerated right_complementable associative distributive Abelian add-associative right_zeroed Field-like doubleLoopStr
for x, v being Element of K st x <> 0. K holds
x * ((x ") * v) = v
theorem
theorem Th63:
:: deftheorem Def15 defines PosElements FVALUAT1:def 13 :
for K being non empty non degenerated right_complementable associative distributive Abelian add-associative right_zeroed Field-like doubleLoopStr
for v being Valuation of K st K is having_valuation holds
PosElements v = { x where x is Element of K : 0 < v . x } ;
theorem Th64:
theorem
theorem Th66:
:: deftheorem Def16 defines min FVALUAT1:def 14 :
for K being non empty non degenerated right_complementable associative distributive Abelian add-associative right_zeroed Field-like doubleLoopStr
for v being Valuation of K
for S being non empty Subset of K st K is having_valuation & S is Subset of (ValuatRing v) holds
min (S,v) = (v " {(inf (v .: S))}) /\ S;
theorem Th67:
theorem Th68:
theorem
theorem
:: deftheorem Def17 defines Submodule FVALUAT1:def 15 :
for R being Ring
for P being RightIdeal of R
for b3 being Submodule of RightModule R holds
( b3 is Submodule of P iff the carrier of b3 = P );
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 #)
:: deftheorem defines scalar-linear FVALUAT1:def 16 :
for R being Ring
for M1, M2 being RightMod of R
for h being Function of M1,M2 holds
( h is scalar-linear iff for x being Element of M1
for r being Element of R holds h . (x * r) = (h . x) * r );
theorem
theorem
theorem
theorem Th75:
theorem
theorem Th77:
theorem
theorem Th79:
theorem Th80:
theorem
theorem Th82:
theorem
theorem
theorem Th85:
theorem