:: by Christoph Schwarzweller

::

:: Received August 29, 2019

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

Th1: for n being Nat holds n = { m where m is Nat : m < n }

by AXIOMS:4;

theorem Th3: :: FIELD_3:2

for n being Nat

for x, y being object st n = {x,y} & x <> y & not ( x = 0 & y = 1 ) holds

( x = 1 & y = 0 )

for x, y being object st n = {x,y} & x <> y & not ( x = 0 & y = 1 ) holds

( x = 1 & y = 0 )

proof end;

registration
end;

registration

ex b_{1} being Field st b_{1} is finite

ex b_{1} being Field st b_{1} is infinite
end;

cluster non empty non degenerated non trivial finite left_add-cancelable right_add-cancelable add-cancelable left_complementable right_complementable complementable almost_left_cancelable almost_right_cancelable almost_cancelable almost_left_invertible almost_right_invertible almost_invertible right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed V128() unital associative commutative V196() Euclidian V218() V219() V220() V221() PID V309( INT.Ring ) V314() for doubleLoopStr ;

existence ex b

proof end;

cluster non empty non degenerated non trivial infinite left_add-cancelable right_add-cancelable add-cancelable left_complementable right_complementable complementable almost_left_cancelable almost_right_cancelable almost_cancelable almost_left_invertible almost_right_invertible almost_invertible right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed V128() unital associative commutative V196() Euclidian V218() V219() V220() V221() PID V309( INT.Ring ) V314() for doubleLoopStr ;

existence ex b

proof end;

definition

let L be non empty doubleLoopStr ;

end;
attr L is almost_trivial means :Def1: :: FIELD_3:def 1

for a being Element of L holds

( a = 1. L or a = 0. L );

for a being Element of L holds

( a = 1. L or a = 0. L );

:: deftheorem Def1 defines almost_trivial FIELD_3:def 1 :

for L being non empty doubleLoopStr holds

( L is almost_trivial iff for a being Element of L holds

( a = 1. L or a = 0. L ) );

for L being non empty doubleLoopStr holds

( L is almost_trivial iff for a being Element of L holds

( a = 1. L or a = 0. L ) );

registration

for b_{1} being Ring st b_{1} is degenerated holds

b_{1} is almost_trivial

not for b_{1} being Field holds b_{1} is almost_trivial
end;

cluster non empty degenerated right_complementable well-unital distributive Abelian add-associative right_zeroed associative -> almost_trivial for doubleLoopStr ;

coherence for b

b

proof end;

cluster non empty non degenerated non trivial left_add-cancelable right_add-cancelable add-cancelable left_complementable right_complementable complementable almost_left_cancelable almost_right_cancelable almost_cancelable almost_left_invertible almost_right_invertible almost_invertible right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed V128() unital associative commutative V196() Euclidian V218() V219() V220() V221() PID V309( INT.Ring ) V314() non almost_trivial for doubleLoopStr ;

existence not for b

proof end;

:: deftheorem Def2 defines trivial FIELD_3:def 2 :

for R being Ring

for a being Element of R holds

( a is trivial iff ( a = 1. R or a = 0. R ) );

for R being Ring

for a being Element of R holds

( a is trivial iff ( a = 1. R or a = 0. R ) );

registration

let R be non almost_trivial Ring;

not for b_{1} being Element of R holds b_{1} is trivial

end;
cluster left_add-cancelable right_add-cancelable add-cancelable left_complementable right_complementable complementable non trivial for Element of the carrier of R;

existence not for b

proof end;

:: deftheorem Def3 defines polynomial_disjoint FIELD_3:def 3 :

for R being Ring holds

( R is polynomial_disjoint iff ([#] R) /\ ([#] (Polynom-Ring R)) = {} );

for R being Ring holds

( R is polynomial_disjoint iff ([#] R) /\ ([#] (Polynom-Ring R)) = {} );

definition

let R be non almost_trivial Ring;

let x be non trivial Element of R;

let o be object ;

coherence

(([#] R) \ {x}) \/ {o} is non empty set ;

end;
let x be non trivial Element of R;

let o be object ;

coherence

(([#] R) \ {x}) \/ {o} is non empty set ;

:: deftheorem defines carr FIELD_3:def 4 :

for R being non almost_trivial Ring

for x being non trivial Element of R

for o being object holds carr (x,o) = (([#] R) \ {x}) \/ {o};

for R being non almost_trivial Ring

for x being non trivial Element of R

for o being object holds carr (x,o) = (([#] R) \ {x}) \/ {o};

definition

let R be non almost_trivial Ring;

let x be non trivial Element of R;

let o be object ;

let a, b be Element of carr (x,o);

( ( a = o & b = o & the addF of R . (x,x) <> x implies the addF of R . (x,x) is Element of carr (x,o) ) & ( a <> o & b = o & the addF of R . (a,x) <> x implies the addF of R . (a,x) is Element of carr (x,o) ) & ( a = o & b <> o & the addF of R . (x,b) <> x implies the addF of R . (x,b) is Element of carr (x,o) ) & ( a <> o & b <> o & the addF of R . (a,b) <> x implies the addF of R . (a,b) is Element of carr (x,o) ) & ( ( not a = o or not b = o or not the addF of R . (x,x) <> x ) & ( not a <> o or not b = o or not the addF of R . (a,x) <> x ) & ( not a = o or not b <> o or not the addF of R . (x,b) <> x ) & ( not a <> o or not b <> o or not the addF of R . (a,b) <> x ) implies o is Element of carr (x,o) ) )

for b_{1} being Element of carr (x,o) holds

( ( a = o & b = o & the addF of R . (x,x) <> x & a <> o & b = o & the addF of R . (a,x) <> x implies ( b_{1} = the addF of R . (x,x) iff b_{1} = the addF of R . (a,x) ) ) & ( a = o & b = o & the addF of R . (x,x) <> x & a = o & b <> o & the addF of R . (x,b) <> x implies ( b_{1} = the addF of R . (x,x) iff b_{1} = the addF of R . (x,b) ) ) & ( a = o & b = o & the addF of R . (x,x) <> x & a <> o & b <> o & the addF of R . (a,b) <> x implies ( b_{1} = the addF of R . (x,x) iff b_{1} = the addF of R . (a,b) ) ) & ( a <> o & b = o & the addF of R . (a,x) <> x & a = o & b <> o & the addF of R . (x,b) <> x implies ( b_{1} = the addF of R . (a,x) iff b_{1} = the addF of R . (x,b) ) ) & ( a <> o & b = o & the addF of R . (a,x) <> x & a <> o & b <> o & the addF of R . (a,b) <> x implies ( b_{1} = the addF of R . (a,x) iff b_{1} = the addF of R . (a,b) ) ) & ( a = o & b <> o & the addF of R . (x,b) <> x & a <> o & b <> o & the addF of R . (a,b) <> x implies ( b_{1} = the addF of R . (x,b) iff b_{1} = the addF of R . (a,b) ) ) )
;

end;
let x be non trivial Element of R;

let o be object ;

let a, b be Element of carr (x,o);

func addR (a,b) -> Element of carr (x,o) equals :Def4: :: FIELD_3:def 5

the addF of R . (x,x) if ( a = o & b = o & the addF of R . (x,x) <> x )

the addF of R . (a,x) if ( a <> o & b = o & the addF of R . (a,x) <> x )

the addF of R . (x,b) if ( a = o & b <> o & the addF of R . (x,b) <> x )

the addF of R . (a,b) if ( a <> o & b <> o & the addF of R . (a,b) <> x )

otherwise o;

coherence the addF of R . (x,x) if ( a = o & b = o & the addF of R . (x,x) <> x )

the addF of R . (a,x) if ( a <> o & b = o & the addF of R . (a,x) <> x )

the addF of R . (x,b) if ( a = o & b <> o & the addF of R . (x,b) <> x )

the addF of R . (a,b) if ( a <> o & b <> o & the addF of R . (a,b) <> x )

otherwise o;

( ( a = o & b = o & the addF of R . (x,x) <> x implies the addF of R . (x,x) is Element of carr (x,o) ) & ( a <> o & b = o & the addF of R . (a,x) <> x implies the addF of R . (a,x) is Element of carr (x,o) ) & ( a = o & b <> o & the addF of R . (x,b) <> x implies the addF of R . (x,b) is Element of carr (x,o) ) & ( a <> o & b <> o & the addF of R . (a,b) <> x implies the addF of R . (a,b) is Element of carr (x,o) ) & ( ( not a = o or not b = o or not the addF of R . (x,x) <> x ) & ( not a <> o or not b = o or not the addF of R . (a,x) <> x ) & ( not a = o or not b <> o or not the addF of R . (x,b) <> x ) & ( not a <> o or not b <> o or not the addF of R . (a,b) <> x ) implies o is Element of carr (x,o) ) )

proof end;

consistency for b

( ( a = o & b = o & the addF of R . (x,x) <> x & a <> o & b = o & the addF of R . (a,x) <> x implies ( b

:: deftheorem Def4 defines addR FIELD_3:def 5 :

for R being non almost_trivial Ring

for x being non trivial Element of R

for o being object

for a, b being Element of carr (x,o) holds

( ( a = o & b = o & the addF of R . (x,x) <> x implies addR (a,b) = the addF of R . (x,x) ) & ( a <> o & b = o & the addF of R . (a,x) <> x implies addR (a,b) = the addF of R . (a,x) ) & ( a = o & b <> o & the addF of R . (x,b) <> x implies addR (a,b) = the addF of R . (x,b) ) & ( a <> o & b <> o & the addF of R . (a,b) <> x implies addR (a,b) = the addF of R . (a,b) ) & ( ( not a = o or not b = o or not the addF of R . (x,x) <> x ) & ( not a <> o or not b = o or not the addF of R . (a,x) <> x ) & ( not a = o or not b <> o or not the addF of R . (x,b) <> x ) & ( not a <> o or not b <> o or not the addF of R . (a,b) <> x ) implies addR (a,b) = o ) );

for R being non almost_trivial Ring

for x being non trivial Element of R

for o being object

for a, b being Element of carr (x,o) holds

( ( a = o & b = o & the addF of R . (x,x) <> x implies addR (a,b) = the addF of R . (x,x) ) & ( a <> o & b = o & the addF of R . (a,x) <> x implies addR (a,b) = the addF of R . (a,x) ) & ( a = o & b <> o & the addF of R . (x,b) <> x implies addR (a,b) = the addF of R . (x,b) ) & ( a <> o & b <> o & the addF of R . (a,b) <> x implies addR (a,b) = the addF of R . (a,b) ) & ( ( not a = o or not b = o or not the addF of R . (x,x) <> x ) & ( not a <> o or not b = o or not the addF of R . (a,x) <> x ) & ( not a = o or not b <> o or not the addF of R . (x,b) <> x ) & ( not a <> o or not b <> o or not the addF of R . (a,b) <> x ) implies addR (a,b) = o ) );

definition

let R be non almost_trivial Ring;

let x be non trivial Element of R;

let o be object ;

ex b_{1} being BinOp of (carr (x,o)) st

for a, b being Element of carr (x,o) holds b_{1} . (a,b) = addR (a,b)

for b_{1}, b_{2} being BinOp of (carr (x,o)) st ( for a, b being Element of carr (x,o) holds b_{1} . (a,b) = addR (a,b) ) & ( for a, b being Element of carr (x,o) holds b_{2} . (a,b) = addR (a,b) ) holds

b_{1} = b_{2}

end;
let x be non trivial Element of R;

let o be object ;

func addR (x,o) -> BinOp of (carr (x,o)) means :Def5: :: FIELD_3:def 6

for a, b being Element of carr (x,o) holds it . (a,b) = addR (a,b);

existence for a, b being Element of carr (x,o) holds it . (a,b) = addR (a,b);

ex b

for a, b being Element of carr (x,o) holds b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def5 defines addR FIELD_3:def 6 :

for R being non almost_trivial Ring

for x being non trivial Element of R

for o being object

for b_{4} being BinOp of (carr (x,o)) holds

( b_{4} = addR (x,o) iff for a, b being Element of carr (x,o) holds b_{4} . (a,b) = addR (a,b) );

for R being non almost_trivial Ring

for x being non trivial Element of R

for o being object

for b

( b

definition

let R be non almost_trivial Ring;

let x be non trivial Element of R;

let o be object ;

let a, b be Element of carr (x,o);

( ( a = o & b = o & the multF of R . (x,x) <> x implies the multF of R . (x,x) is Element of carr (x,o) ) & ( a <> o & b = o & the multF of R . (a,x) <> x implies the multF of R . (a,x) is Element of carr (x,o) ) & ( a = o & b <> o & the multF of R . (x,b) <> x implies the multF of R . (x,b) is Element of carr (x,o) ) & ( a <> o & b <> o & the multF of R . (a,b) <> x implies the multF of R . (a,b) is Element of carr (x,o) ) & ( ( not a = o or not b = o or not the multF of R . (x,x) <> x ) & ( not a <> o or not b = o or not the multF of R . (a,x) <> x ) & ( not a = o or not b <> o or not the multF of R . (x,b) <> x ) & ( not a <> o or not b <> o or not the multF of R . (a,b) <> x ) implies o is Element of carr (x,o) ) )

for b_{1} being Element of carr (x,o) holds

( ( a = o & b = o & the multF of R . (x,x) <> x & a <> o & b = o & the multF of R . (a,x) <> x implies ( b_{1} = the multF of R . (x,x) iff b_{1} = the multF of R . (a,x) ) ) & ( a = o & b = o & the multF of R . (x,x) <> x & a = o & b <> o & the multF of R . (x,b) <> x implies ( b_{1} = the multF of R . (x,x) iff b_{1} = the multF of R . (x,b) ) ) & ( a = o & b = o & the multF of R . (x,x) <> x & a <> o & b <> o & the multF of R . (a,b) <> x implies ( b_{1} = the multF of R . (x,x) iff b_{1} = the multF of R . (a,b) ) ) & ( a <> o & b = o & the multF of R . (a,x) <> x & a = o & b <> o & the multF of R . (x,b) <> x implies ( b_{1} = the multF of R . (a,x) iff b_{1} = the multF of R . (x,b) ) ) & ( a <> o & b = o & the multF of R . (a,x) <> x & a <> o & b <> o & the multF of R . (a,b) <> x implies ( b_{1} = the multF of R . (a,x) iff b_{1} = the multF of R . (a,b) ) ) & ( a = o & b <> o & the multF of R . (x,b) <> x & a <> o & b <> o & the multF of R . (a,b) <> x implies ( b_{1} = the multF of R . (x,b) iff b_{1} = the multF of R . (a,b) ) ) )
;

end;
let x be non trivial Element of R;

let o be object ;

let a, b be Element of carr (x,o);

func multR (a,b) -> Element of carr (x,o) equals :Def6: :: FIELD_3:def 7

the multF of R . (x,x) if ( a = o & b = o & the multF of R . (x,x) <> x )

the multF of R . (a,x) if ( a <> o & b = o & the multF of R . (a,x) <> x )

the multF of R . (x,b) if ( a = o & b <> o & the multF of R . (x,b) <> x )

the multF of R . (a,b) if ( a <> o & b <> o & the multF of R . (a,b) <> x )

otherwise o;

coherence the multF of R . (x,x) if ( a = o & b = o & the multF of R . (x,x) <> x )

the multF of R . (a,x) if ( a <> o & b = o & the multF of R . (a,x) <> x )

the multF of R . (x,b) if ( a = o & b <> o & the multF of R . (x,b) <> x )

the multF of R . (a,b) if ( a <> o & b <> o & the multF of R . (a,b) <> x )

otherwise o;

( ( a = o & b = o & the multF of R . (x,x) <> x implies the multF of R . (x,x) is Element of carr (x,o) ) & ( a <> o & b = o & the multF of R . (a,x) <> x implies the multF of R . (a,x) is Element of carr (x,o) ) & ( a = o & b <> o & the multF of R . (x,b) <> x implies the multF of R . (x,b) is Element of carr (x,o) ) & ( a <> o & b <> o & the multF of R . (a,b) <> x implies the multF of R . (a,b) is Element of carr (x,o) ) & ( ( not a = o or not b = o or not the multF of R . (x,x) <> x ) & ( not a <> o or not b = o or not the multF of R . (a,x) <> x ) & ( not a = o or not b <> o or not the multF of R . (x,b) <> x ) & ( not a <> o or not b <> o or not the multF of R . (a,b) <> x ) implies o is Element of carr (x,o) ) )

proof end;

consistency for b

( ( a = o & b = o & the multF of R . (x,x) <> x & a <> o & b = o & the multF of R . (a,x) <> x implies ( b

:: deftheorem Def6 defines multR FIELD_3:def 7 :

for R being non almost_trivial Ring

for x being non trivial Element of R

for o being object

for a, b being Element of carr (x,o) holds

( ( a = o & b = o & the multF of R . (x,x) <> x implies multR (a,b) = the multF of R . (x,x) ) & ( a <> o & b = o & the multF of R . (a,x) <> x implies multR (a,b) = the multF of R . (a,x) ) & ( a = o & b <> o & the multF of R . (x,b) <> x implies multR (a,b) = the multF of R . (x,b) ) & ( a <> o & b <> o & the multF of R . (a,b) <> x implies multR (a,b) = the multF of R . (a,b) ) & ( ( not a = o or not b = o or not the multF of R . (x,x) <> x ) & ( not a <> o or not b = o or not the multF of R . (a,x) <> x ) & ( not a = o or not b <> o or not the multF of R . (x,b) <> x ) & ( not a <> o or not b <> o or not the multF of R . (a,b) <> x ) implies multR (a,b) = o ) );

for R being non almost_trivial Ring

for x being non trivial Element of R

for o being object

for a, b being Element of carr (x,o) holds

( ( a = o & b = o & the multF of R . (x,x) <> x implies multR (a,b) = the multF of R . (x,x) ) & ( a <> o & b = o & the multF of R . (a,x) <> x implies multR (a,b) = the multF of R . (a,x) ) & ( a = o & b <> o & the multF of R . (x,b) <> x implies multR (a,b) = the multF of R . (x,b) ) & ( a <> o & b <> o & the multF of R . (a,b) <> x implies multR (a,b) = the multF of R . (a,b) ) & ( ( not a = o or not b = o or not the multF of R . (x,x) <> x ) & ( not a <> o or not b = o or not the multF of R . (a,x) <> x ) & ( not a = o or not b <> o or not the multF of R . (x,b) <> x ) & ( not a <> o or not b <> o or not the multF of R . (a,b) <> x ) implies multR (a,b) = o ) );

definition

let R be non almost_trivial Ring;

let x be non trivial Element of R;

let o be object ;

ex b_{1} being BinOp of (carr (x,o)) st

for a, b being Element of carr (x,o) holds b_{1} . (a,b) = multR (a,b)

for b_{1}, b_{2} being BinOp of (carr (x,o)) st ( for a, b being Element of carr (x,o) holds b_{1} . (a,b) = multR (a,b) ) & ( for a, b being Element of carr (x,o) holds b_{2} . (a,b) = multR (a,b) ) holds

b_{1} = b_{2}

end;
let x be non trivial Element of R;

let o be object ;

func multR (x,o) -> BinOp of (carr (x,o)) means :Def7: :: FIELD_3:def 8

for a, b being Element of carr (x,o) holds it . (a,b) = multR (a,b);

existence for a, b being Element of carr (x,o) holds it . (a,b) = multR (a,b);

ex b

for a, b being Element of carr (x,o) holds b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def7 defines multR FIELD_3:def 8 :

for R being non almost_trivial Ring

for x being non trivial Element of R

for o being object

for b_{4} being BinOp of (carr (x,o)) holds

( b_{4} = multR (x,o) iff for a, b being Element of carr (x,o) holds b_{4} . (a,b) = multR (a,b) );

for R being non almost_trivial Ring

for x being non trivial Element of R

for o being object

for b

( b

definition

let F be non almost_trivial Field;

let x be non trivial Element of F;

let o be object ;

ex b_{1} being strict doubleLoopStr st

( the carrier of b_{1} = carr (x,o) & the addF of b_{1} = addR (x,o) & the multF of b_{1} = multR (x,o) & the OneF of b_{1} = 1. F & the ZeroF of b_{1} = 0. F )

for b_{1}, b_{2} being strict doubleLoopStr st the carrier of b_{1} = carr (x,o) & the addF of b_{1} = addR (x,o) & the multF of b_{1} = multR (x,o) & the OneF of b_{1} = 1. F & the ZeroF of b_{1} = 0. F & the carrier of b_{2} = carr (x,o) & the addF of b_{2} = addR (x,o) & the multF of b_{2} = multR (x,o) & the OneF of b_{2} = 1. F & the ZeroF of b_{2} = 0. F holds

b_{1} = b_{2}
;

end;
let x be non trivial Element of F;

let o be object ;

func ExField (x,o) -> strict doubleLoopStr means :Def8: :: FIELD_3:def 9

( the carrier of it = carr (x,o) & the addF of it = addR (x,o) & the multF of it = multR (x,o) & the OneF of it = 1. F & the ZeroF of it = 0. F );

existence ( the carrier of it = carr (x,o) & the addF of it = addR (x,o) & the multF of it = multR (x,o) & the OneF of it = 1. F & the ZeroF of it = 0. F );

ex b

( the carrier of b

proof end;

uniqueness for b

b

:: deftheorem Def8 defines ExField FIELD_3:def 9 :

for F being non almost_trivial Field

for x being non trivial Element of F

for o being object

for b_{4} being strict doubleLoopStr holds

( b_{4} = ExField (x,o) iff ( the carrier of b_{4} = carr (x,o) & the addF of b_{4} = addR (x,o) & the multF of b_{4} = multR (x,o) & the OneF of b_{4} = 1. F & the ZeroF of b_{4} = 0. F ) );

for F being non almost_trivial Field

for x being non trivial Element of F

for o being object

for b

( b

registration

let F be non almost_trivial Field;

let x be non trivial Element of F;

let o be object ;

coherence

not ExField (x,o) is degenerated

end;
let x be non trivial Element of F;

let o be object ;

coherence

not ExField (x,o) is degenerated

proof end;

registration

let F be non almost_trivial Field;

let x be non trivial Element of F;

let o be object ;

coherence

ExField (x,o) is Abelian

end;
let x be non trivial Element of F;

let o be object ;

coherence

ExField (x,o) is Abelian

proof end;

theorem Th7: :: FIELD_3:7

for F being non almost_trivial Field

for x being non trivial Element of F

for o being object st not o in [#] F holds

( ExField (x,o) is right_zeroed & ExField (x,o) is right_complementable )

for x being non trivial Element of F

for o being object st not o in [#] F holds

( ExField (x,o) is right_zeroed & ExField (x,o) is right_complementable )

proof end;

theorem Th8: :: FIELD_3:8

for F being non almost_trivial Field

for x being non trivial Element of F

for o being object st not o in [#] F holds

ExField (x,o) is add-associative

for x being non trivial Element of F

for o being object st not o in [#] F holds

ExField (x,o) is add-associative

proof end;

registration

let F be non almost_trivial Field;

let x be non trivial Element of F;

let o be object ;

coherence

ExField (x,o) is commutative

end;
let x be non trivial Element of F;

let o be object ;

coherence

ExField (x,o) is commutative

proof end;

theorem Th9: :: FIELD_3:9

for F being non almost_trivial Field

for x being non trivial Element of F

for o being object st not o in [#] F holds

ExField (x,o) is well-unital

for x being non trivial Element of F

for o being object st not o in [#] F holds

ExField (x,o) is well-unital

proof end;

theorem Th10: :: FIELD_3:10

for F being non almost_trivial Field

for x being non trivial Element of F

for o being object st not o in [#] F holds

ExField (x,o) is associative

for x being non trivial Element of F

for o being object st not o in [#] F holds

ExField (x,o) is associative

proof end;

theorem Th11: :: FIELD_3:11

for F being non almost_trivial Field

for x being non trivial Element of F

for o being object st not o in [#] F holds

ExField (x,o) is distributive

for x being non trivial Element of F

for o being object st not o in [#] F holds

ExField (x,o) is distributive

proof end;

theorem Th12: :: FIELD_3:12

for F being non almost_trivial Field

for x being non trivial Element of F

for o being object st not o in [#] F holds

ExField (x,o) is almost_left_invertible

for x being non trivial Element of F

for o being object st not o in [#] F holds

ExField (x,o) is almost_left_invertible

proof end;

theorem Th13: :: FIELD_3:13

for F being non almost_trivial Field

for x being non trivial Element of F

for P being Ring st P = ExField (x,<%(0. F),(1. F)%>) holds

<%(0. F),(1. F)%> in ([#] P) /\ ([#] (Polynom-Ring P))

for x being non trivial Element of F

for P being Ring st P = ExField (x,<%(0. F),(1. F)%>) holds

<%(0. F),(1. F)%> in ([#] P) /\ ([#] (Polynom-Ring P))

proof end;

theorem :: FIELD_3:15

for n being non zero Nat ex K being Field ex p being Polynomial of K st

( deg p = n & p in ([#] K) /\ ([#] (Polynom-Ring K)) )

( deg p = n & p in ([#] K) /\ ([#] (Polynom-Ring K)) )

proof end;

theorem :: FIELD_3:16

ex K being Field ex x being object st

( not x in rng (canHom K) & x in ([#] K) /\ ([#] (Polynom-Ring K)) )

( not x in rng (canHom K) & x in ([#] K) /\ ([#] (Polynom-Ring K)) )

proof end;

registration

not for b_{1} being Field holds b_{1} is polynomial_disjoint
end;

cluster non empty non degenerated non trivial left_add-cancelable right_add-cancelable add-cancelable left_complementable right_complementable complementable almost_left_cancelable almost_right_cancelable almost_cancelable almost_left_invertible almost_right_invertible almost_invertible right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed V128() unital associative commutative V196() Euclidian V218() V219() V220() V221() PID V309( INT.Ring ) V314() non polynomial_disjoint for doubleLoopStr ;

existence not for b

proof end;

definition

let F be non almost_trivial Field;

let x be non trivial Element of F;

let o be object ;

ex b_{1} being Function of F,(ExField (x,o)) st

( b_{1} . x = o & ( for a being Element of F st a <> x holds

b_{1} . a = a ) )

for b_{1}, b_{2} being Function of F,(ExField (x,o)) st b_{1} . x = o & ( for a being Element of F st a <> x holds

b_{1} . a = a ) & b_{2} . x = o & ( for a being Element of F st a <> x holds

b_{2} . a = a ) holds

b_{1} = b_{2}

end;
let x be non trivial Element of F;

let o be object ;

func isoR (x,o) -> Function of F,(ExField (x,o)) means :Def9: :: FIELD_3:def 10

( it . x = o & ( for a being Element of F st a <> x holds

it . a = a ) );

existence ( it . x = o & ( for a being Element of F st a <> x holds

it . a = a ) );

ex b

( b

b

proof end;

uniqueness for b

b

b

b

proof end;

:: deftheorem Def9 defines isoR FIELD_3:def 10 :

for F being non almost_trivial Field

for x being non trivial Element of F

for o being object

for b_{4} being Function of F,(ExField (x,o)) holds

( b_{4} = isoR (x,o) iff ( b_{4} . x = o & ( for a being Element of F st a <> x holds

b_{4} . a = a ) ) );

for F being non almost_trivial Field

for x being non trivial Element of F

for o being object

for b

( b

b

registration

let F be non almost_trivial Field;

let x be non trivial Element of F;

let o be object ;

coherence

isoR (x,o) is onto

end;
let x be non trivial Element of F;

let o be object ;

coherence

isoR (x,o) is onto

proof end;

theorem :: FIELD_3:17

for F being non almost_trivial Field

for x being non trivial Element of F

for o being object st not o in [#] F holds

isoR (x,o) is one-to-one

for x being non trivial Element of F

for o being object st not o in [#] F holds

isoR (x,o) is one-to-one

proof end;

theorem Th15: :: FIELD_3:18

for F being non almost_trivial Field

for x being non trivial Element of F

for u being object st not u in [#] F holds

( isoR (x,u) is additive & isoR (x,u) is multiplicative & isoR (x,u) is unity-preserving )

for x being non trivial Element of F

for u being object st not u in [#] F holds

( isoR (x,u) is additive & isoR (x,u) is multiplicative & isoR (x,u) is unity-preserving )

proof end;

theorem :: FIELD_3:20

for n being non zero Nat

for F being non almost_trivial Field ex K being non polynomial_disjoint Field ex p being Polynomial of K st

( K,F are_isomorphic & deg p = n & p in ([#] K) /\ ([#] (Polynom-Ring K)) )

for F being non almost_trivial Field ex K being non polynomial_disjoint Field ex p being Polynomial of K st

( K,F are_isomorphic & deg p = n & p in ([#] K) /\ ([#] (Polynom-Ring K)) )

proof end;

definition

let R be Ring;

end;
attr R is flat means :Def10: :: FIELD_3:def 11

for a, b being Element of R holds the_rank_of a = the_rank_of b;

for a, b being Element of R holds the_rank_of a = the_rank_of b;

:: deftheorem Def10 defines flat FIELD_3:def 11 :

for R being Ring holds

( R is flat iff for a, b being Element of R holds the_rank_of a = the_rank_of b );

for R being Ring holds

( R is flat iff for a, b being Element of R holds the_rank_of a = the_rank_of b );

registration

ex b_{1} being Ring st b_{1} is flat
end;

cluster non empty left_add-cancelable right_add-cancelable add-cancelable left_complementable right_complementable complementable right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed V128() unital associative V218() V219() V220() V221() V309( INT.Ring ) V309( INT.Ring ) flat for doubleLoopStr ;

existence ex b

proof end;

registration

for b_{1} being flat Ring holds b_{1} is polynomial_disjoint
end;

cluster non empty right_complementable well-unital distributive Abelian add-associative right_zeroed associative flat -> polynomial_disjoint flat for doubleLoopStr ;

coherence for b

proof end;

registration

coherence

not INT.Ring is flat by INT_3:def 3, Th17;

coherence

not F_Rat is flat by GAUSSINT:def 14, Th17;

coherence

not F_Real is flat by Th17;

end;
not INT.Ring is flat by INT_3:def 3, Th17;

coherence

not F_Rat is flat by GAUSSINT:def 14, Th17;

coherence

not F_Real is flat by Th17;

registration
end;

registration

ex b_{1} being finite Field st b_{1} is polynomial_disjoint
end;

cluster non empty non degenerated non trivial finite left_add-cancelable right_add-cancelable add-cancelable left_complementable right_complementable complementable almost_left_cancelable almost_right_cancelable almost_cancelable almost_left_invertible almost_right_invertible almost_invertible right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed V128() unital associative commutative V196() Euclidian V218() V219() V220() V221() PID V309( INT.Ring ) V314() V322() polynomial_disjoint for doubleLoopStr ;

existence ex b

proof end;

registration
end;

Lem2: for R being Ring

for p being Polynomial of R

for r being Rational st r in RAT+ & p = r holds

r = [1,2]

proof end;

Lem3: for R being Ring

for p being Polynomial of R holds p <> [1,2]

proof end;

registration
end;

Lem4: for R being Ring

for p being Polynomial of R

for r being Real st r in REAL+ holds

p <> r

proof end;

registration
end;

registration

ex b_{1} being infinite Field st b_{1} is polynomial_disjoint
end;

cluster non empty non degenerated non trivial infinite left_add-cancelable right_add-cancelable add-cancelable left_complementable right_complementable complementable almost_left_cancelable almost_right_cancelable almost_cancelable almost_left_invertible almost_right_invertible almost_invertible right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed V128() unital associative commutative V196() Euclidian V218() V219() V220() V221() PID V309( INT.Ring ) V314() polynomial_disjoint for doubleLoopStr ;

existence ex b

proof end;

registration
end;

registration

let F be Field;

let p be Element of [#] (Polynom-Ring F);

coherence

(Polynom-Ring F) / ({p} -Ideal) is polynomial_disjoint

end;
let p be Element of [#] (Polynom-Ring F);

coherence

(Polynom-Ring F) / ({p} -Ideal) is polynomial_disjoint

proof end;

registration

let F be polynomial_disjoint Field;

let p be non constant Element of the carrier of (Polynom-Ring F);

coherence

Polynom-Ring p is polynomial_disjoint

end;
let p be non constant Element of the carrier of (Polynom-Ring F);

coherence

Polynom-Ring p is polynomial_disjoint

proof end;