:: by Grzegorz Bancerek , Hidetsune Kobayashi and Artur Korni{\l}owicz

::

:: Received April 7, 2011

:: Copyright (c) 2011-2021 Association of Mizar Users

Lm1: now :: thesis: for a, b being Real

for c, d being ExtReal st a = c & b = d holds

a - b = c - d

for c, d being ExtReal st a = c & b = d holds

a - b = c - d

let a, b be Real; :: thesis: for c, d being ExtReal st a = c & b = d holds

a - b = c - d

let c, d be ExtReal; :: thesis: ( a = c & b = d implies a - b = c - d )

assume A1: ( a = c & b = d ) ; :: thesis: a - b = c - d

then - b = - d by XXREAL_3:def 3;

hence a - b = c - d by A1, XXREAL_3:def 2; :: thesis: verum

end;
a - b = c - d

let c, d be ExtReal; :: thesis: ( a = c & b = d implies a - b = c - d )

assume A1: ( a = c & b = d ) ; :: thesis: a - b = c - d

then - b = - d by XXREAL_3:def 3;

hence a - b = c - d by A1, XXREAL_3:def 2; :: thesis: verum

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)

(x + y) / z = (x / z) + (y / z)

proof end;

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

for x being object holds

( x is ext-integer iff ( x is integer or x = +infty ) );

for x being object holds

( x is ext-integer iff ( x is integer or x = +infty ) );

registration
end;

registration

coherence

+infty is ext-integer ;

coherence

not -infty is ext-integer ;

coherence

( 1. is ext-integer & 1. is positive & 1. is real ) ;

coherence

for b_{1} being object st b_{1} is integer holds

b_{1} is ext-integer
;

coherence

for b_{1} being object st b_{1} is real & b_{1} is ext-integer holds

b_{1} is integer
;

end;
+infty is ext-integer ;

coherence

not -infty is ext-integer ;

coherence

( 1. is ext-integer & 1. is positive & 1. is real ) ;

coherence

for b

b

coherence

for b

b

registration

existence

ex b_{1} being Element of ExtREAL st

( b_{1} is real & b_{1} is ext-integer & b_{1} is positive )

ex b_{1} being ext-integer object st b_{1} is positive

end;
ex b

( b

proof end;

existence ex b

proof end;

definition

let X be ext-real-membered set ;

given i0 being positive ExtInt such that A1: i0 in X ;

ex b_{1} being positive ExtInt st

( b_{1} in X & ( for i being positive ExtInt st i in X holds

b_{1} <= i ) )

for b_{1}, b_{2} being positive ExtInt st b_{1} in X & ( for i being positive ExtInt st i in X holds

b_{1} <= i ) & b_{2} in X & ( for i being positive ExtInt st i in X holds

b_{2} <= i ) holds

b_{1} = b_{2}

end;
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 ( it in X & ( for i being positive ExtInt st i in X holds

it <= i ) );

ex b

( b

b

proof end;

uniqueness for b

b

b

b

proof end;

:: deftheorem Def2 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 b_{2} being positive ExtInt holds

( b_{2} = least-positive X iff ( b_{2} in X & ( for i being positive ExtInt st i in X holds

b_{2} <= i ) ) );

for X being ext-real-membered set st ex i0 being positive ExtInt st i0 in X holds

for b

( b

b

definition

let f be Relation;

end;
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 ;

for x being set st x in rng f holds

x is ext-integer ;

:: deftheorem Def3 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 );

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

registration

let A be set ;

ex b_{1} being Function of A,ExtREAL st b_{1} is e.i.-valued

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

existence ex b

proof end;

registration
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;

for b_{1} being Subset of K holds verum
;

existence

( ( n = 0 implies ex b_{1} being Subset of K st b_{1} = the carrier of K ) & ( not n = 0 implies ex b_{1} being Subset of K ex f being FinSequence of bool the carrier of K st

( b_{1} = 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) ) ) ) )

for b_{1}, b_{2} being Subset of K holds

( ( n = 0 & b_{1} = the carrier of K & b_{2} = the carrier of K implies b_{1} = b_{2} ) & ( not n = 0 & ex f being FinSequence of bool the carrier of K st

( b_{1} = 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) ) ) & ex f being FinSequence of bool the carrier of K st

( b_{2} = 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) ) ) implies b_{1} = b_{2} ) )

end;
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 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) ) );

for b

existence

( ( n = 0 implies ex b

( b

f . (i + 1) = S *' (f /. i) ) ) ) )

proof end;

uniqueness for b

( ( n = 0 & b

( b

f . (i + 1) = S *' (f /. i) ) ) & ex f being FinSequence of bool the carrier of K st

( b

f . (i + 1) = S *' (f /. i) ) ) implies b

proof end;

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

for K being non empty doubleLoopStr

for S being Subset of K

for n being Nat

for b_{4} being Subset of K holds

( ( n = 0 implies ( b_{4} = S |^ n iff b_{4} = the carrier of K ) ) & ( not n = 0 implies ( b_{4} = S |^ n iff ex f being FinSequence of bool the carrier of K st

( b_{4} = 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) ) ) ) ) );

for K being non empty doubleLoopStr

for S being Subset of K

for n being Nat

for b

( ( n = 0 implies ( b

( b

f . (i + 1) = S *' (f /. i) ) ) ) ) );

registration

let R be Ring;

let S be Ideal of R;

let n be Nat;

coherence

( not S |^ n is empty & S |^ n is add-closed & S |^ n is left-ideal & S |^ n is right-ideal )

end;
let S be Ideal of R;

let n be Nat;

coherence

( not S |^ n is empty & S |^ n is add-closed & S |^ n is left-ideal & S |^ n is right-ideal )

proof end;

definition

let G be non empty doubleLoopStr ;

let g be Element of G;

let i be Integer;

coherence

( ( 0 <= i implies (power G) . (g,|.i.|) is Element of G ) & ( not 0 <= i implies / ((power G) . (g,|.i.|)) is Element of G ) );

consistency

for b_{1} being Element of G holds verum;

;

end;
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 (power G) . (g,|.i.|) if 0 <= i

otherwise / ((power G) . (g,|.i.|));

coherence

( ( 0 <= i implies (power G) . (g,|.i.|) is Element of G ) & ( not 0 <= i implies / ((power G) . (g,|.i.|)) is Element of G ) );

consistency

for b

;

:: deftheorem Def5 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,|.i.|) ) & ( not 0 <= i implies g |^ i = / ((power G) . (g,|.i.|)) ) );

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,|.i.|) ) & ( not 0 <= i implies g |^ i = / ((power G) . (g,|.i.|)) ) );

definition

let G be non empty doubleLoopStr ;

let g be Element of G;

let n be Nat;

compatibility

for b_{1} being Element of G holds

( b_{1} = g |^ n iff b_{1} = (power G) . (g,n) )

end;
let g be Element of G;

let n be Nat;

compatibility

for b

( b

proof end;

:: 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);

for G being non empty doubleLoopStr

for g being Element of G

for n being Nat holds g |^ n = (power G) . (g,n);

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)

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

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 ;

end;
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 ) );

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

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

definition

let K be doubleLoopStr ;

assume A1: K is having_valuation ;

ex b_{1} being e.i.-valued Function of K,ExtREAL st

( b_{1} . (0. K) = +infty & ( for a being Element of K st a <> 0. K holds

b_{1} . a in INT ) & ( for a, b being Element of K holds b_{1} . (a * b) = (b_{1} . a) + (b_{1} . b) ) & ( for a being Element of K st 0 <= b_{1} . a holds

0 <= b_{1} . ((1. K) + a) ) & ex a being Element of K st

( b_{1} . a <> 0 & b_{1} . a <> +infty ) )
by A1;

end;
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 ( 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 ) );

ex b

( b

b

0 <= b

( b

:: deftheorem Def8 defines Valuation FVALUAT1:def 8 :

for K being doubleLoopStr st K is having_valuation holds

for b_{2} being e.i.-valued Function of K,ExtREAL holds

( b_{2} is Valuation of K iff ( b_{2} . (0. K) = +infty & ( for a being Element of K st a <> 0. K holds

b_{2} . a in INT ) & ( for a, b being Element of K holds b_{2} . (a * b) = (b_{2} . a) + (b_{2} . b) ) & ( for a being Element of K st 0 <= b_{2} . a holds

0 <= b_{2} . ((1. K) + a) ) & ex a being Element of K st

( b_{2} . a <> 0 & b_{2} . a <> +infty ) ) );

for K being doubleLoopStr st K is having_valuation holds

for b

( b

b

0 <= b

( b

theorem Th17: :: FVALUAT1:17

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

v . (1. K) = 0

for v being Valuation of K st K is having_valuation holds

v . (1. K) = 0

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

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

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

v . (- (1. K)) = 0

for v being Valuation of K st K is having_valuation holds

v . (- (1. K)) = 0

proof end;

theorem Th20: :: FVALUAT1:20

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 holds

v . (- a) = v . a

for a being Element of K

for v being Valuation of K st K is having_valuation holds

v . (- a) = v . a

proof end;

theorem Th21: :: FVALUAT1:21

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 ") = - (v . a)

for a being Element of K

for v being Valuation of K st K is having_valuation & a <> 0. K holds

v . (a ") = - (v . a)

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)

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

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 & a <> 0. K & b <> 0. K holds

v . (a / b) = - (v . (b / a))

for a, b being Element of K

for v being Valuation of K st K is having_valuation & a <> 0. K & b <> 0. K holds

v . (a / b) = - (v . (b / a))

proof end;

theorem Th24: :: FVALUAT1:24

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 & 0 <= v . (a / b) holds

v . b <= v . a

for a, b being Element of K

for v being Valuation of K st K is having_valuation & b <> 0. K & 0 <= v . (a / b) holds

v . b <= v . a

proof end;

theorem Th25: :: FVALUAT1:25

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 & a <> 0. K & b <> 0. K & v . (a / b) <= 0 holds

0 <= v . (b / a)

for a, b being Element of K

for v being Valuation of K st K is having_valuation & a <> 0. K & b <> 0. K & v . (a / b) <= 0 holds

0 <= v . (b / a)

proof end;

theorem Th26: :: FVALUAT1:26

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 & v . (a / b) <= 0 holds

v . a <= v . b

for a, b being Element of K

for v being Valuation of K st K is having_valuation & b <> 0. K & v . (a / b) <= 0 holds

v . a <= v . b

proof end;

theorem Th27: :: FVALUAT1:27

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 holds

min ((v . a),(v . b)) <= v . (a + b)

for a, b being Element of K

for v being Valuation of K st K is having_valuation holds

min ((v . a),(v . b)) <= v . (a + b)

proof end;

theorem Th28: :: FVALUAT1:28

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 & v . a < v . b holds

v . a = v . (a + b)

for a, b being Element of K

for v being Valuation of K st K is having_valuation & v . a < v . b holds

v . a = v . (a + b)

proof end;

theorem Th29: :: FVALUAT1:29

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

for v being Valuation of K st K is having_valuation & a <> 0. K holds

v . (a |^ i) = i * (v . a)

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 |^ i) = i * (v . a)

proof end;

theorem Th30: :: FVALUAT1:30

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 & 0 <= v . ((1. K) + a) holds

0 <= v . a

for a being Element of K

for v being Valuation of K st K is having_valuation & 0 <= v . ((1. K) + a) holds

0 <= v . a

proof end;

theorem :: FVALUAT1:31

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 & 0 <= v . ((1. K) - a) holds

0 <= v . a

for a being Element of K

for v being Valuation of K st K is having_valuation & 0 <= v . ((1. K) - a) holds

0 <= v . a

proof end;

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

0 <= b - a

proof end;

theorem :: FVALUAT1:32

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 & a <> 0. K & v . a <= v . b holds

0 <= v . (b / a)

for a, b being Element of K

for v being Valuation of K st K is having_valuation & a <> 0. K & v . a <= v . b holds

0 <= v . (b / a)

proof end;

theorem Th33: :: FVALUAT1:33

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

+infty in rng v

for v being Valuation of K st K is having_valuation holds

+infty in rng v

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

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 v . a = 1 holds

least-positive (rng v) = 1

for a being Element of K

for v being Valuation of K st v . a = 1 holds

least-positive (rng v) = 1

proof end;

theorem Th35: :: FVALUAT1:35

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) is integer

for v being Valuation of K st K is having_valuation holds

least-positive (rng v) is integer

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

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 ;

the Element of v " {(least-positive (rng v))} is Element of K

end;
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 the Element of v " {(least-positive (rng v))};

the Element of v " {(least-positive (rng v))} is Element of K

proof end;

:: deftheorem Def9 defines Pgenerator FVALUAT1:def 9 :

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

Pgenerator v = the Element of v " {(least-positive (rng v))};

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

Pgenerator v = the Element of v " {(least-positive (rng v))};

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 ;

ex b_{1} being Valuation of K st

for a being Element of K holds v . a = (b_{1} . a) * (least-positive (rng v))

for b_{1}, b_{2} being Valuation of K st ( for a being Element of K holds v . a = (b_{1} . a) * (least-positive (rng v)) ) & ( for a being Element of K holds v . a = (b_{2} . a) * (least-positive (rng v)) ) holds

b_{1} = b_{2}

end;
let v be Valuation of K;

assume A1: K is having_valuation ;

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 for a being Element of K holds v . a = (it . a) * (least-positive (rng v));

ex b

for a being Element of K holds v . a = (b

proof end;

uniqueness for b

b

proof end;

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

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 b_{3} being Valuation of K holds

( b_{3} = normal-valuation v iff for a being Element of K holds v . a = (b_{3} . a) * (least-positive (rng v)) );

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 b

( b

theorem Th37: :: FVALUAT1:37

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 holds

( v . a = 0 iff (normal-valuation v) . a = 0 )

for a being Element of K

for v being Valuation of K st K is having_valuation holds

( v . a = 0 iff (normal-valuation v) . a = 0 )

proof end;

theorem Th38: :: FVALUAT1:38

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 holds

( v . a = +infty iff (normal-valuation v) . a = +infty )

for a being Element of K

for v being Valuation of K st K is having_valuation holds

( v . a = +infty iff (normal-valuation v) . a = +infty )

proof end;

theorem :: FVALUAT1:39

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 holds

( v . a = v . b iff (normal-valuation v) . a = (normal-valuation v) . b )

for a, b being Element of K

for v being Valuation of K st K is having_valuation holds

( v . a = v . b iff (normal-valuation v) . a = (normal-valuation v) . b )

proof end;

theorem Th40: :: FVALUAT1:40

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 holds

( v . a is positive iff (normal-valuation v) . a is positive )

for a being Element of K

for v being Valuation of K st K is having_valuation holds

( v . a is positive iff (normal-valuation v) . a is positive )

proof end;

theorem Th41: :: FVALUAT1:41

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 holds

( 0 <= v . a iff 0 <= (normal-valuation v) . a )

for a being Element of K

for v being Valuation of K st K is having_valuation holds

( 0 <= v . a iff 0 <= (normal-valuation v) . a )

proof end;

theorem :: FVALUAT1:42

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 holds

( not v . a is negative iff not (normal-valuation v) . a is negative )

for a being Element of K

for v being Valuation of K st K is having_valuation holds

( not v . a is negative iff not (normal-valuation v) . a is negative )

proof end;

theorem Th43: :: FVALUAT1:43

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

(normal-valuation v) . (Pgenerator v) = 1

for v being Valuation of K st K is having_valuation holds

(normal-valuation v) . (Pgenerator v) = 1

proof end;

theorem :: FVALUAT1:44

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 & 0 <= v . a holds

(normal-valuation v) . a <= v . a

for a being Element of K

for v being Valuation of K st K is having_valuation & 0 <= v . a holds

(normal-valuation v) . a <= v . a

proof end;

theorem :: FVALUAT1:45

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 & v . a = 1 holds

normal-valuation v = v

for a being Element of K

for v being Valuation of K st K is having_valuation & v . a = 1 holds

normal-valuation v = v

proof end;

theorem :: FVALUAT1:46

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

normal-valuation (normal-valuation v) = normal-valuation v

for v being Valuation of K st K is having_valuation holds

normal-valuation (normal-valuation v) = normal-valuation v

proof end;

definition

let K be non empty doubleLoopStr ;

let v be Valuation of K;

coherence

{ x where x is Element of K : 0 <= v . x } is set ;

end;
let v be Valuation of K;

coherence

{ x where x is Element of K : 0 <= v . x } is set ;

:: 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 } ;

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

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

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

for v being Valuation of K st K is having_valuation holds

0. K in NonNegElements v

proof end;

theorem Th50: :: FVALUAT1:50

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

1. K in NonNegElements v

for v being Valuation of K st K is having_valuation holds

1. K in NonNegElements 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 ;

ex b_{1} being non degenerated strict commutative Ring st

( the carrier of b_{1} = NonNegElements v & the addF of b_{1} = the addF of K | [:(NonNegElements v),(NonNegElements v):] & the multF of b_{1} = the multF of K | [:(NonNegElements v),(NonNegElements v):] & the ZeroF of b_{1} = 0. K & the OneF of b_{1} = 1. K )

for b_{1}, b_{2} being non degenerated strict commutative Ring st the carrier of b_{1} = NonNegElements v & the addF of b_{1} = the addF of K | [:(NonNegElements v),(NonNegElements v):] & the multF of b_{1} = the multF of K | [:(NonNegElements v),(NonNegElements v):] & the ZeroF of b_{1} = 0. K & the OneF of b_{1} = 1. K & the carrier of b_{2} = NonNegElements v & the addF of b_{2} = the addF of K | [:(NonNegElements v),(NonNegElements v):] & the multF of b_{2} = the multF of K | [:(NonNegElements v),(NonNegElements v):] & the ZeroF of b_{2} = 0. K & the OneF of b_{2} = 1. K holds

b_{1} = b_{2}
;

end;
let v be Valuation of K;

assume A1: K is having_valuation ;

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 ( 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 );

ex b

( the carrier of b

proof end;

uniqueness for b

b

:: deftheorem Def12 defines ValuatRing FVALUAT1:def 12 :

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 b_{3} being non degenerated strict commutative Ring holds

( b_{3} = ValuatRing v iff ( the carrier of b_{3} = NonNegElements v & the addF of b_{3} = the addF of K | [:(NonNegElements v),(NonNegElements v):] & the multF of b_{3} = the multF of K | [:(NonNegElements v),(NonNegElements v):] & the ZeroF of b_{3} = 0. K & the OneF of b_{3} = 1. K ) );

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 b

( b

theorem Th51: :: FVALUAT1:51

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 (ValuatRing v) holds x is Element of K

for v being Valuation of K st K is having_valuation holds

for x being Element of (ValuatRing v) holds x is Element of K

proof end;

theorem Th52: :: FVALUAT1:52

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 holds

( 0 <= v . a iff a is Element of (ValuatRing v) )

for a being Element of K

for v being Valuation of K st K is having_valuation holds

( 0 <= v . a iff a is Element of (ValuatRing v) )

proof end;

theorem Th53: :: FVALUAT1:53

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 S being Subset of (ValuatRing v) holds 0 is LowerBound of v .: S

for v being Valuation of K st K is having_valuation holds

for S being Subset of (ValuatRing v) holds 0 is LowerBound of v .: S

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

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

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

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

0. (ValuatRing v) = 0. K by Def12;

for v being Valuation of K st K is having_valuation holds

0. (ValuatRing v) = 0. K by Def12;

theorem :: FVALUAT1:57

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

1. (ValuatRing v) = 1. K by Def12;

for v being Valuation of K st K is having_valuation holds

1. (ValuatRing v) = 1. K by Def12;

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

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

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

ValuatRing v is domRing-like

for v being Valuation of K st K is having_valuation holds

ValuatRing v is domRing-like

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)

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: 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

0. K in { x where x is Element of K : 0 < v . x }

for v being Valuation of K st K is having_valuation holds

0. K in { x where x is Element of K : 0 < v . x }

let K be non empty non degenerated right_complementable distributive Abelian add-associative right_zeroed associative Field-like doubleLoopStr ; :: thesis: for v being Valuation of K st K is having_valuation holds

0. K in { x where x is Element of K : 0 < v . x }

let v be Valuation of K; :: thesis: ( K is having_valuation implies 0. K in { x where x is Element of K : 0 < v . x } )

assume K is having_valuation ; :: thesis: 0. K in { x where x is Element of K : 0 < v . x }

then v . (0. K) = +infty by Def8;

hence 0. K in { x where x is Element of K : 0 < v . x } ; :: thesis: verum

end;
0. K in { x where x is Element of K : 0 < v . x }

let v be Valuation of K; :: thesis: ( K is having_valuation implies 0. K in { x where x is Element of K : 0 < v . x } )

assume K is having_valuation ; :: thesis: 0. K in { x where x is Element of K : 0 < v . x }

then v . (0. K) = +infty by Def8;

hence 0. K in { x where x is Element of K : 0 < v . x } ; :: thesis: verum

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 ;

{ x where x is Element of K : 0 < v . x } is Ideal of (ValuatRing v)

end;
let v be Valuation of K;

assume A1: K is having_valuation ;

func PosElements v -> Ideal of (ValuatRing v) equals :Def13: :: FVALUAT1:def 13

{ x where x is Element of K : 0 < v . x } ;

coherence { x where x is Element of K : 0 < v . x } ;

{ x where x is Element of K : 0 < v . x } is Ideal of (ValuatRing v)

proof end;

:: deftheorem Def13 defines PosElements FVALUAT1:def 13 :

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

PosElements v = { x where x is Element of K : 0 < v . x } ;

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

PosElements v = { x where x is Element of K : 0 < v . x } ;

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;
let v be Valuation of K;

synonym vp v for PosElements v;

theorem Th61: :: FVALUAT1:61

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 holds

( a in vp v iff 0 < v . a )

for a being Element of K

for v being Valuation of K st K is having_valuation holds

( a in vp v iff 0 < v . a )

proof end;

theorem :: FVALUAT1:62

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

0. K in vp v

for v being Valuation of K st K is having_valuation holds

0. K in vp v

proof end;

theorem Th63: :: FVALUAT1:63

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

not 1. K in vp v

for v being Valuation of K st K is having_valuation holds

not 1. K in vp 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;

let S be non empty Subset of K;

assume that

A1: K is having_valuation and

A2: S is Subset of (ValuatRing v) ;

(v " {(inf (v .: S))}) /\ S is Subset of (ValuatRing v)

end;
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 (v " {(inf (v .: S))}) /\ S;

(v " {(inf (v .: S))}) /\ S is Subset of (ValuatRing v)

proof end;

:: deftheorem Def14 defines min FVALUAT1:def 14 :

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) = (v " {(inf (v .: S))}) /\ S;

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) = (v " {(inf (v .: S))}) /\ S;

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

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

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

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

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

proof end;

Lm10: now :: thesis: for R being Ring

for P being RightIdeal of R ex S being strict Submodule of RightModule R st the carrier of S = P

for P being RightIdeal of R ex S being strict Submodule of RightModule R st the carrier of S = P

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

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

thus ex S being strict Submodule of RightModule R st the carrier of S = P :: thesis: verum

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

thus ex S being strict Submodule of RightModule R st the carrier of S = P :: thesis: verum

proof

reconsider V1 = P as Subset of (RightModule R) ;

V1 is linearly-closed

end;
V1 is linearly-closed

proof
_{1} being Element of the carrier of (RightModule R) holds

( not b_{1} in V1 or b_{1} * a in V1 )

let v be Vector of (RightModule R); :: thesis: ( not v in V1 or v * a in V1 )

assume A2: v in V1 ; :: thesis: v * a in V1

reconsider v1 = v as Element of R ;

v1 * a = v * a ;

hence v * a in V1 by A2, IDEAL_1:def 3; :: thesis: verum

end;

hence
ex S being strict Submodule of RightModule R st the carrier of S = P
by RMOD_2:34; :: thesis: verum
hereby :: according to RMOD_2:def 1 :: thesis: for b_{1} being Element of the carrier of R

for b_{2} being Element of the carrier of (RightModule R) holds

( not b_{2} in V1 or b_{2} * b_{1} in V1 )

let a be Scalar of R; :: thesis: for bfor b

( not b

let v, u be Vector of (RightModule R); :: thesis: ( v in V1 & u in V1 implies v + u in V1 )

assume A1: ( v in V1 & u in V1 ) ; :: thesis: v + u in V1

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: verum

end;
assume A1: ( v in V1 & u in V1 ) ; :: thesis: v + u in V1

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: verum

( not b

let v be Vector of (RightModule R); :: thesis: ( not v in V1 or v * a in V1 )

assume A2: v in V1 ; :: thesis: v * a in V1

reconsider v1 = v as Element of R ;

v1 * a = v * a ;

hence v * a in V1 by A2, IDEAL_1:def 3; :: thesis: verum

definition

let R be Ring;

let P be RightIdeal of R;

ex b_{1} being Submodule of RightModule R st the carrier of b_{1} = P

end;
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 the carrier of it = P;

ex b

proof end;

:: deftheorem Def15 defines Submodule FVALUAT1:def 15 :

for R being Ring

for P being RightIdeal of R

for b_{3} being Submodule of RightModule R holds

( b_{3} is Submodule of P iff the carrier of b_{3} = P );

for R being Ring

for P being RightIdeal of R

for b

( b

registration

let R be Ring;

let P be RightIdeal of R;

ex b_{1} being Submodule of P st b_{1} is strict

end;
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 ex b

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

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

let R be Ring;

let M1, M2 be RightMod of R;

let h be Function of M1,M2;

end;
let M1, M2 be RightMod of R;

let h be Function of M1,M2;

attr h is scalar-linear means :: FVALUAT1:def 16

for x being Element of M1

for r being Element of R holds h . (x * r) = (h . x) * r;

for x being Element of M1

for r being Element of R holds h . (x * r) = (h . x) * r;

:: 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 );

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

registration

let R be Ring;

let M1 be RightMod of R;

let M2 be Submodule of M1;

coherence

( incl (M2,M1) is additive & incl (M2,M1) is scalar-linear )

end;
let M1 be RightMod of R;

let M2 be Submodule of M1;

coherence

( incl (M2,M1) is additive & incl (M2,M1) is scalar-linear )

proof end;

theorem :: FVALUAT1:69

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 is Element of (ValuatRing v) holds

v . a <= (v . a) + (v . b)

for a, b being Element of K

for v being Valuation of K st K is having_valuation & b is Element of (ValuatRing v) holds

v . a <= (v . a) + (v . b)

proof end;

theorem :: FVALUAT1:70

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

for v being Valuation of K st K is having_valuation & a is Element of (ValuatRing v) holds

(power K) . (a,n) is Element of (ValuatRing v)

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 is Element of (ValuatRing v) holds

(power K) . (a,n) is Element of (ValuatRing v)

proof end;

theorem :: FVALUAT1:71

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 x being Element of (ValuatRing v) st x <> 0. K holds

(power K) . (x,n) <> 0. K

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 (ValuatRing v) st x <> 0. K holds

(power K) . (x,n) <> 0. K

proof end;

theorem Th72: :: FVALUAT1:72

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 & v . a = 0 holds

( a is Element of (ValuatRing v) & a " is Element of (ValuatRing v) )

for a being Element of K

for v being Valuation of K st K is having_valuation & v . a = 0 holds

( a is Element of (ValuatRing v) & a " is Element of (ValuatRing v) )

proof end;

theorem :: FVALUAT1:73

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 & a is Element of (ValuatRing v) & a " is Element of (ValuatRing v) holds

v . a = 0

for a being Element of K

for v being Valuation of K st K is having_valuation & a <> 0. K & a is Element of (ValuatRing v) & a " is Element of (ValuatRing v) holds

v . a = 0

proof end;

theorem Th74: :: FVALUAT1:74

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 & v . a = 0 holds

for I being Ideal of (ValuatRing v) holds

( a in I iff I = the carrier of (ValuatRing v) )

for a being Element of K

for v being Valuation of K st K is having_valuation & v . a = 0 holds

for I being Ideal of (ValuatRing v) holds

( a in I iff I = the carrier of (ValuatRing v) )

proof end;

theorem :: FVALUAT1:75

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

Pgenerator v is Element of (ValuatRing v)

for v being Valuation of K st K is having_valuation holds

Pgenerator v is Element of (ValuatRing v)

proof end;

theorem Th76: :: FVALUAT1:76

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

vp v is proper

for v being Valuation of K st K is having_valuation holds

vp v is proper

proof end;

theorem Th77: :: FVALUAT1:77

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 (ValuatRing v) st not x in vp v holds

v . x = 0

for v being Valuation of K st K is having_valuation holds

for x being Element of (ValuatRing v) st not x in vp v holds

v . x = 0

proof end;

theorem :: FVALUAT1:78

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

vp v is prime

for v being Valuation of K st K is having_valuation holds

vp v is prime

proof end;

theorem Th79: :: FVALUAT1:79

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 proper Ideal of (ValuatRing v) holds I c= vp v

for v being Valuation of K st K is having_valuation holds

for I being proper Ideal of (ValuatRing v) holds I c= vp v

proof end;

theorem :: FVALUAT1:80

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

vp v is maximal

for v being Valuation of K st K is having_valuation holds

vp v is maximal

proof end;

theorem :: FVALUAT1:81

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 maximal Ideal of (ValuatRing v) holds I = vp v

for v being Valuation of K st K is having_valuation holds

for I being maximal Ideal of (ValuatRing v) holds I = vp v

proof end;

theorem Th82: :: FVALUAT1:82

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

NonNegElements (normal-valuation v) = NonNegElements v

for v being Valuation of K st K is having_valuation holds

NonNegElements (normal-valuation v) = NonNegElements v

proof end;

theorem :: FVALUAT1:83

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

ValuatRing (normal-valuation v) = ValuatRing v

for v being Valuation of K st K is having_valuation holds

ValuatRing (normal-valuation v) = ValuatRing v

proof end;