FVALUAT1: Valuation Theory, Part {I}

:: Valuation Theory, Part {I}
:: by Grzegorz Bancerek , Hidetsune Kobayashi and Artur Korni{\l}owicz
::
:: Received April 7, 2011
:: Copyright (c) 2011-2021 Association of Mizar Users

theorem Th1: :: FVALUAT1:1

for x being ExtReal st x = - x holds
x = 0

proof end;

theorem Th2: :: FVALUAT1:2

for x being ExtReal st x + x = 0 holds
x = 0

proof end;

theorem Th3: :: FVALUAT1:3

for x, y, z, s being ExtReal st 0 <= x & x <= y & 0 <= s & s <= z holds
x * s <= y * z

proof end;

Lm1: now :: thesis:

let a, b be Real; :: thesis:
let c, d be ExtReal; :: thesis:
assume A1: ( a = c & b = d ) ; :: thesis:
then - b = - d by XXREAL_3:def 3;
hence a - b = c - d by A1, XXREAL_3:def 2; :: thesis:

end;

theorem :: FVALUAT1:4

for x, y being ExtReal st y <> +infty & 0 < x & 0 < y holds
0 < x / y

proof end;

theorem Th5: :: FVALUAT1:5

for x, y being ExtReal st y <> +infty & x < 0 & 0 < y holds
x / y < 0

proof end;

theorem :: FVALUAT1:6

for x, y being ExtReal st y <> -infty & 0 < x & y < 0 holds
x / y < 0

proof end;

theorem Th7: :: FVALUAT1:7

for x, y, z being ExtReal st ( ( x in REAL & y in REAL ) or z in REAL ) holds
(x + y) / z = (x / z) + (y / z)

proof end;

theorem Th8: :: FVALUAT1:8

for x, y being ExtReal st y <> +infty & y <> -infty & y <> 0 holds
(x / y) * y = x

proof end;

theorem Th9: :: FVALUAT1:9

for x, y being ExtReal st y <> -infty & y <> +infty & x <> 0 & y <> 0 holds
x / y <> 0

proof end;

definition

let x be object ;

attr x is ext-integer means :Def1: :: FVALUAT1:def 1
( x is integer or x = +infty );

end;

:: deftheorem Def1 defines ext-integer FVALUAT1:def 1 :

registration

cluster ext-integer -> ext-real for object ;

coherence ;

end;

registration

cluster +infty -> ext-integer ;

coherence ;

cluster -infty -> non ext-integer ;

coherence ;

cluster 1. -> positive real ext-integer ;

coherence ;

cluster integer -> ext-integer for object ;

coherence ;

cluster real ext-integer -> integer for object ;

coherence ;

end;

registration

cluster ext-real positive real ext-integer for Element of ExtREAL ;

existence

proof end;

cluster ext-real positive ext-integer for object ;

existence

proof end;

end;

definition

mode ExtInt is ext-integer object ;

end;

theorem Th10: :: FVALUAT1:10

for x, y being ExtInt st x < y holds
x + 1 <= y

proof end;

theorem :: FVALUAT1:11

for x being ExtInt holds -infty < x

proof end;

definition

let X be ext-real-membered set ;
given i0 being positive ExtInt such that A1: i0 in X ;

func least-positive X -> positive ExtInt means :Def2: :: FVALUAT1:def 2
( it in X & ( for i being positive ExtInt st i in X holds
it <= i ) );

existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def2 defines least-positive FVALUAT1:def 2 :

definition

let f be Relation;

attr f is e.i.-valued means :Def3: :: FVALUAT1:def 3
for x being set st x in rng f holds
x is ext-integer ;

end;

:: deftheorem Def3 defines e.i.-valued FVALUAT1:def 3 :

registration

cluster Relation-like Function-like e.i.-valued for set ;

existence

proof end;

end;

registration

let A be set ;

cluster Relation-like A -defined ExtREAL -valued Function-like V40(A, ExtREAL ) e.i.-valued for Element of bool [:A,ExtREAL:];

existence

proof end;

end;

registration

let f be e.i.-valued Function;
let x be set ;

cluster f . x -> ext-integer ;

coherence

proof end;

end;

theorem Th12: :: FVALUAT1:12

for K being non empty right_complementable distributive left_unital add-associative right_zeroed doubleLoopStr holds (- (1. K)) * (- (1. K)) = 1. K

proof end;

definition

let K be non empty doubleLoopStr ;
let S be Subset of K;
let n be Nat;

func S |^ n -> Subset of K means :Def4: :: FVALUAT1:def 4
it = the carrier of K if n = 0
otherwise ex f being FinSequence of bool the carrier of K st
( it = 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) ) );

consistency ;
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def4 defines |^ FVALUAT1:def 4 :

theorem :: FVALUAT1:13

for D being non empty doubleLoopStr
for A being Subset of D holds A |^ 1 = A

proof end;

theorem :: FVALUAT1:14

for D being non empty doubleLoopStr
for A being Subset of D holds A |^ 2 = A *' A

proof end;

registration

let R be Ring;
let S be Ideal of R;
let n be Nat;

cluster S |^ n -> non empty add-closed left-ideal right-ideal ;

coherence

proof end;

end;

definition

let G be non empty doubleLoopStr ;
let g be Element of G;
let i be Integer;

func g |^ i -> Element of G equals :Def5: :: FVALUAT1:def 5
(power G) . (g,|.i.|) if 0 <= i
otherwise / ((power G) . (g,|.i.|));

correctness ;

end;

:: deftheorem Def5 defines |^ FVALUAT1:def 5 :

definition

let G be non empty doubleLoopStr ;
let g be Element of G;
let n be Nat;

redefine func g |^ n equals :: FVALUAT1:def 6
(power G) . (g,n);

compatibility

proof end;

end;

:: deftheorem defines |^ FVALUAT1:def 6 :

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;

theorem :: FVALUAT1:15

for n, m 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 + m) = (a |^ n) * (a |^ m)

proof end;

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

proof end;

theorem Th16: :: FVALUAT1:16

for i being Integer
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 |^ i <> 0. K

proof end;

definition

let K be doubleLoopStr ;

attr K is having_valuation means :: FVALUAT1:def 7
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 ) );

end;

:: deftheorem defines having_valuation FVALUAT1:def 7 :

definition

let K be doubleLoopStr ;
assume A1: K is having_valuation ;

mode Valuation of K -> e.i.-valued Function of K,ExtREAL means :Def8: :: FVALUAT1:def 8
( it . (0. K) = +infty & ( for a being Element of K st a <> 0. K holds
it . a in INT ) & ( for a, b being Element of K holds it . (a * b) = (it . a) + (it . b) ) & ( for a being Element of K st 0 <= it . a holds
0 <= it . ((1. K) + a) ) & ex a being Element of K st
( it . a <> 0 & it . a <> +infty ) );

existence by A1;

end;

:: deftheorem Def8 defines Valuation FVALUAT1:def 8 :

theorem Th17: :: FVALUAT1:17

proof end;

theorem Th18: :: FVALUAT1:18

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
for v being Valuation of K st K is having_valuation & a <> 0. K holds
v . a <> +infty

proof end;

theorem Th19: :: FVALUAT1:19

proof end;

theorem Th20: :: FVALUAT1:20

proof end;

theorem Th21: :: FVALUAT1:21

proof end;

theorem Th22: :: FVALUAT1:22

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
for v being Valuation of K st K is having_valuation & b <> 0. K holds
v . (a / b) = (v . a) - (v . b)

proof end;

theorem Th23: :: FVALUAT1:23

proof end;

theorem Th24: :: FVALUAT1:24

proof end;

theorem Th25: :: FVALUAT1:25

proof end;

theorem Th26: :: FVALUAT1:26

proof end;

theorem Th27: :: FVALUAT1:27

proof end;

theorem Th28: :: FVALUAT1:28

proof end;

theorem Th29: :: FVALUAT1:29

proof end;

theorem Th30: :: FVALUAT1:30

proof end;

theorem :: FVALUAT1:31

proof end;

Lm4: for a, b being ExtInt st a <= b holds
0 <= b - a

proof end;

theorem :: FVALUAT1:32

proof end;

theorem Th33: :: FVALUAT1:33

proof end;

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

proof end;

theorem Th34: :: FVALUAT1:34

proof end;

theorem Th35: :: FVALUAT1:35

proof end;

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

proof end;

theorem Th36: :: FVALUAT1:36

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
for x being Element of K st x <> 0. K holds
ex i being Integer st v . x = i * (least-positive (rng v))

proof end;

definition

let K be non empty non degenerated right_complementable distributive Abelian add-associative right_zeroed associative Field-like doubleLoopStr ;
let v be Valuation of K;
assume A1: K is having_valuation ;

func Pgenerator v -> Element of K equals :Def9: :: FVALUAT1:def 9
the Element of v " {(least-positive (rng v))};

coherence

proof end;

end;

:: deftheorem Def9 defines Pgenerator FVALUAT1:def 9 :

definition

func normal-valuation v -> Valuation of K means :Def10: :: FVALUAT1:def 10
for a being Element of K holds v . a = (it . a) * (least-positive (rng v));

existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def10 defines normal-valuation FVALUAT1:def 10 :

theorem Th37: :: FVALUAT1:37

proof end;

theorem Th38: :: FVALUAT1:38

proof end;

theorem :: FVALUAT1:39

proof end;

theorem Th40: :: FVALUAT1:40

proof end;

theorem Th41: :: FVALUAT1:41

proof end;

theorem :: FVALUAT1:42

proof end;

theorem Th43: :: FVALUAT1:43

proof end;

theorem :: FVALUAT1:44

proof end;

theorem :: FVALUAT1:45

proof end;

theorem :: FVALUAT1:46

proof end;

definition

let K be non empty doubleLoopStr ;
let v be Valuation of K;

func NonNegElements v -> set equals :: FVALUAT1:def 11
{ x where x is Element of K : 0 <= v . x } ;

coherence ;

end;

:: deftheorem defines NonNegElements FVALUAT1:def 11 :

theorem Th47: :: FVALUAT1:47

for K being non empty doubleLoopStr
for v being Valuation of K
for a being Element of K holds
( a in NonNegElements v iff 0 <= v . a )

proof end;

theorem Th48: :: FVALUAT1:48

for K being non empty doubleLoopStr
for v being Valuation of K holds NonNegElements v c= the carrier of K

proof end;

theorem Th49: :: FVALUAT1:49

for K being non empty doubleLoopStr
for v being Valuation of K st K is having_valuation holds
0. K in NonNegElements v

proof end;

theorem Th50: :: FVALUAT1:50

proof end;

definition

func ValuatRing v -> non degenerated strict commutative Ring means :Def12: :: FVALUAT1:def 12
( the carrier of it = NonNegElements v & the addF of it = the addF of K | [:(NonNegElements v),(NonNegElements v):] & the multF of it = the multF of K | [:(NonNegElements v),(NonNegElements v):] & the ZeroF of it = 0. K & the OneF of it = 1. K );

existence

proof end;

uniqueness ;

end;

:: deftheorem Def12 defines ValuatRing FVALUAT1:def 12 :

theorem Th51: :: FVALUAT1:51

proof end;

theorem Th52: :: FVALUAT1:52

proof end;

theorem Th53: :: FVALUAT1:53

proof end;

theorem Th54: :: FVALUAT1:54

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
for x, y being Element of K
for x1, y1 being Element of (ValuatRing v) st x = x1 & y = y1 holds
x + y = x1 + y1

proof end;

theorem Th55: :: FVALUAT1:55

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
for x, y being Element of K
for x1, y1 being Element of (ValuatRing v) st x = x1 & y = y1 holds
x * y = x1 * y1

proof end;

theorem :: FVALUAT1:56

theorem :: FVALUAT1:57

theorem :: FVALUAT1:58

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
for x being Element of K
for y being Element of (ValuatRing v) st x = y holds
- x = - y

proof end;

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

proof end;

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

proof end;

theorem :: FVALUAT1:59

proof end;

theorem Th60: :: FVALUAT1:60

for n being Nat
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
for y being Element of (ValuatRing v) holds (power K) . (y,n) = (power (ValuatRing v)) . (y,n)

proof end;

Lm9: now :: thesis:

let K be non empty non degenerated right_complementable distributive Abelian add-associative right_zeroed associative Field-like doubleLoopStr ; :: thesis:
let v be Valuation of K; :: thesis:
assume K is having_valuation ; :: thesis:
then v . (0. K) = +infty by Def8;
hence 0. K in { x where x is Element of K : 0 < v . x } ; :: thesis:

end;

definition

func PosElements v -> Ideal of (ValuatRing v) equals :Def13: :: FVALUAT1:def 13
{ x where x is Element of K : 0 < v . x } ;

coherence

proof end;

end;

:: deftheorem Def13 defines PosElements FVALUAT1:def 13 :

notation

let K be non empty non degenerated right_complementable distributive Abelian add-associative right_zeroed associative Field-like doubleLoopStr ;
let v be Valuation of K;
synonym vp v for PosElements v;

end;

theorem Th61: :: FVALUAT1:61

proof end;

theorem :: FVALUAT1:62

proof end;

theorem Th63: :: FVALUAT1:63

proof end;

definition

let K be non empty non degenerated right_complementable distributive Abelian add-associative right_zeroed associative Field-like doubleLoopStr ;
let v be Valuation of K;
let S be non empty Subset of K;
assume that
A1: K is having_valuation and
A2: S is Subset of (ValuatRing v) ;

func min (S,v) -> Subset of (ValuatRing v) equals :Def14: :: FVALUAT1:def 14
(v " {(inf (v .: S))}) /\ S;

coherence

proof end;

end;

:: deftheorem Def14 defines min FVALUAT1:def 14 :

theorem Th64: :: FVALUAT1:64

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
for S being non empty Subset of K st K is having_valuation & S is Subset of (ValuatRing v) holds
min (S,v) c= S

proof end;

theorem Th65: :: FVALUAT1:65

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
for S being non empty Subset of K st K is having_valuation & S is Subset of (ValuatRing v) holds
for x being Element of K holds
( x in min (S,v) iff ( x in S & ( for y being Element of K st y in S holds
v . x <= v . y ) ) )

proof end;

theorem :: FVALUAT1:66

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
for I being non empty Subset of K
for x being Element of (ValuatRing v) st I is Ideal of (ValuatRing v) & x in min (I,v) holds
I = {x} -Ideal

proof end;

theorem :: FVALUAT1:67

for R being non empty doubleLoopStr
for I being non empty add-closed Subset of R holds I is Preserv of the addF of R

proof end;

Lm10: now :: thesis:

let R be Ring; :: thesis:
let P be RightIdeal of R; :: thesis:
thus ex S being strict Submodule of RightModule R st the carrier of S = P :: thesis:

proof

reconsider V1 = P as Subset of (RightModule R) ;
V1 is linearly-closed

proof

hereby :: according to RMOD_2:def 1 :: thesis:

let v, u be Vector of (RightModule R); :: thesis:
assume A1: ( v in V1 & u in V1 ) ; :: thesis:
reconsider v1 = v, u1 = u as Element of R ;
v1 + u1 = v + u ;
hence v + u in V1 by A1, IDEAL_1:def 1; :: thesis:

end;

let a be Scalar of R; :: thesis:
let v be Vector of (RightModule R); :: thesis:
assume A2: v in V1 ; :: thesis:
reconsider v1 = v as Element of R ;
v1 * a = v * a ;
hence v * a in V1 by A2, IDEAL_1:def 3; :: thesis:

end;

hence ex S being strict Submodule of RightModule R st the carrier of S = P by RMOD_2:34; :: thesis:

end;

definition

let R be Ring;
let P be RightIdeal of R;

mode Submodule of P -> Submodule of RightModule R means :Def15: :: FVALUAT1:def 15
the carrier of it = P;

existence

proof end;

end;

:: deftheorem Def15 defines Submodule FVALUAT1:def 15 :

registration

let R be Ring;
let P be RightIdeal of R;

cluster non empty left_add-cancelable right_add-cancelable add-cancelable right_complementable Abelian add-associative right_zeroed strict RightMod-like V251() V252() V253() V254() for Submodule of P;

existence

proof end;

end;

theorem :: FVALUAT1:68

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 #)

proof end;

definition