:: On the Intersection of Fields $F$ with $F[X]$
:: by Christoph Schwarzweller
::
:: 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 Th2: :: FIELD_3:1
for n being Nat
for x being object st n = {x} holds
x = 0
proof end;

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

theorem Th4: :: FIELD_3:3
for n being Nat st 1 < n holds
0. (Z/ n) = 0
proof end;

theorem Th5: :: FIELD_3:4
(1. (Z/ 2)) + (1. (Z/ 2)) = 0. (Z/ 2)
proof end;

theorem Th6: :: FIELD_3:5
for R being Ring
for n being non zero Nat holds () . ((0. R),n) = 0. R
proof end;

registration
coherence
( not Z/ 3 is degenerated & Z/ 3 is almost_left_invertible )
by PEPIN:41;
end;

registration
existence
ex b1 being Field st b1 is finite
proof end;
existence
ex b1 being Field st b1 is infinite
proof end;
end;

definition
let L be non empty doubleLoopStr ;
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 );
end;

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

registration
coherence
for b1 being Ring st b1 is degenerated holds
b1 is almost_trivial
proof end;
existence
not for b1 being Field holds b1 is almost_trivial
proof end;
end;

theorem :: FIELD_3:6
for R being Ring holds
( R is almost_trivial iff ( R is degenerated or R, Z/ 2 are_isomorphic ) )
proof end;

definition
let R be Ring;
let a be Element of R;
attr a is trivial means :Def2: :: FIELD_3:def 2
( a = 1. R or a = 0. R );
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 ) );

registration
let R be non almost_trivial Ring;
existence
not for b1 being Element of R holds b1 is trivial
proof end;
end;

definition
let R be Ring;
attr R is polynomial_disjoint means :Def3: :: FIELD_3:def 3
([#] R) /\ ([#] ()) = {} ;
end;

:: deftheorem Def3 defines polynomial_disjoint FIELD_3:def 3 :
for R being Ring holds
( R is polynomial_disjoint iff ([#] R) /\ ([#] ()) = {} );

definition
let R be non almost_trivial Ring;
let x be non trivial Element of R;
let o be object ;
func carr (x,o) -> non empty set equals :: FIELD_3:def 4
(([#] R) \ {x}) \/ {o};
coherence
(([#] R) \ {x}) \/ {o} is non empty set
;
end;

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

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);
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
( ( 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 b1 being Element of carr (x,o) holds
;
end;

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

definition
let R be non almost_trivial Ring;
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
ex b1 being BinOp of (carr (x,o)) st
for a, b being Element of carr (x,o) holds b1 . (a,b) = addR (a,b)
proof end;
uniqueness
for b1, b2 being BinOp of (carr (x,o)) st ( for a, b being Element of carr (x,o) holds b1 . (a,b) = addR (a,b) ) & ( for a, b being Element of carr (x,o) holds b2 . (a,b) = addR (a,b) ) holds
b1 = b2
proof end;
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 b4 being BinOp of (carr (x,o)) holds
( b4 = addR (x,o) iff for a, b being Element of carr (x,o) holds b4 . (a,b) = addR (a,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);
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
( ( 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 b1 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 ( b1 = the multF of R . (x,x) iff b1 = 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 ( b1 = the multF of R . (x,x) iff b1 = 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 ( b1 = the multF of R . (x,x) iff b1 = 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 ( b1 = the multF of R . (a,x) iff b1 = 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 ( b1 = the multF of R . (a,x) iff b1 = 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 ( b1 = the multF of R . (x,b) iff b1 = the multF of R . (a,b) ) ) )
;
end;

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

definition
let R be non almost_trivial Ring;
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
ex b1 being BinOp of (carr (x,o)) st
for a, b being Element of carr (x,o) holds b1 . (a,b) = multR (a,b)
proof end;
uniqueness
for b1, b2 being BinOp of (carr (x,o)) st ( for a, b being Element of carr (x,o) holds b1 . (a,b) = multR (a,b) ) & ( for a, b being Element of carr (x,o) holds b2 . (a,b) = multR (a,b) ) holds
b1 = b2
proof end;
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 b4 being BinOp of (carr (x,o)) holds
( b4 = multR (x,o) iff for a, b being Element of carr (x,o) holds b4 . (a,b) = multR (a,b) );

definition
let F be non almost_trivial Field;
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
ex b1 being strict doubleLoopStr st
( the carrier of b1 = carr (x,o) & the addF of b1 = addR (x,o) & the multF of b1 = multR (x,o) & the OneF of b1 = 1. F & the ZeroF of b1 = 0. F )
proof end;
uniqueness
for b1, b2 being strict doubleLoopStr st the carrier of b1 = carr (x,o) & the addF of b1 = addR (x,o) & the multF of b1 = multR (x,o) & the OneF of b1 = 1. F & the ZeroF of b1 = 0. F & the carrier of b2 = carr (x,o) & the addF of b2 = addR (x,o) & the multF of b2 = multR (x,o) & the OneF of b2 = 1. F & the ZeroF of b2 = 0. F holds
b1 = b2
;
end;

:: 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 b4 being strict doubleLoopStr holds
( b4 = ExField (x,o) iff ( the carrier of b4 = carr (x,o) & the addF of b4 = addR (x,o) & the multF of b4 = multR (x,o) & the OneF of b4 = 1. F & the ZeroF of b4 = 0. F ) );

registration
let F be non almost_trivial Field;
let x be non trivial Element of F;
let o be object ;
cluster ExField (x,o) -> non degenerated strict ;
coherence
not ExField (x,o) is degenerated
proof end;
end;

registration
let F be non almost_trivial Field;
let x be non trivial Element of F;
let o be object ;
cluster ExField (x,o) -> strict Abelian ;
coherence
ExField (x,o) is Abelian
proof end;
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 )
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
proof end;

registration
let F be non almost_trivial Field;
let x be non trivial Element of F;
let o be object ;
cluster ExField (x,o) -> strict commutative ;
coherence
ExField (x,o) is commutative
proof end;
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
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
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
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
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) /\ ([#] ())
proof end;

theorem Th14: :: FIELD_3:14
ex K being Field st ([#] K) /\ ([#] ()) <> {}
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) /\ ([#] ()) )
proof end;

theorem :: FIELD_3:16
ex K being Field ex x being object st
( not x in rng () & x in ([#] K) /\ ([#] ()) )
proof end;

registration
existence
not for b1 being Field holds b1 is polynomial_disjoint
proof end;
end;

definition
let F be non almost_trivial Field;
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
ex b1 being Function of F,(ExField (x,o)) st
( b1 . x = o & ( for a being Element of F st a <> x holds
b1 . a = a ) )
proof end;
uniqueness
for b1, b2 being Function of F,(ExField (x,o)) st b1 . x = o & ( for a being Element of F st a <> x holds
b1 . a = a ) & b2 . x = o & ( for a being Element of F st a <> x holds
b2 . a = a ) holds
b1 = b2
proof end;
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 b4 being Function of F,(ExField (x,o)) holds
( b4 = isoR (x,o) iff ( b4 . x = o & ( for a being Element of F st a <> x holds
b4 . a = a ) ) );

registration
let F be non almost_trivial Field;
let x be non trivial Element of F;
let o be object ;
cluster isoR (x,o) -> onto ;
coherence
isoR (x,o) is onto
proof end;
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
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 )
proof end;

theorem :: FIELD_3:19
for F being non almost_trivial Field ex K being non polynomial_disjoint Field st K,F are_isomorphic
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) /\ ([#] ()) )
proof end;

definition
let R be Ring;
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;
end;

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

registration
existence
ex b1 being Ring st b1 is flat
proof end;
end;

theorem Th16: :: FIELD_3:21
for R being flat Ring
for p being Polynomial of R holds not p in [#] R
proof end;

registration
coherence
for b1 being flat Ring holds b1 is polynomial_disjoint
proof end;
end;

theorem Th17: :: FIELD_3:22
for R being non degenerated Ring st 0 in the carrier of R holds
not R is flat
proof end;

registration
cluster INT.Ring -> non flat ;
coherence
not INT.Ring is flat
by ;
cluster F_Rat -> non flat ;
coherence
not F_Rat is flat
by ;
cluster F_Real -> non flat ;
coherence
not F_Real is flat
by Th17;
end;

registration
let n be non trivial Nat;
cluster INT.Ring n -> non flat ;
coherence
not Z/ n is flat
proof end;
end;

theorem Th18: :: FIELD_3:23
for R being Ring
for p being Polynomial of R
for n being Nat holds p <> n
proof end;

registration
let n be non trivial Nat;
coherence
proof end;
end;

registration
existence
ex b1 being finite Field st b1 is polynomial_disjoint
proof end;
end;

theorem Th19: :: FIELD_3:24
for R being Ring
for p being Polynomial of R
for i being Integer holds p <> i
proof end;

registration
coherence
proof end;
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;

theorem Th20: :: FIELD_3:25
for R being Ring
for p being Polynomial of R
for r being Rational holds p <> r
proof end;

registration
coherence
proof end;
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;

theorem Th21: :: FIELD_3:26
for R being Ring
for p being Polynomial of R
for r being Real holds p <> r
proof end;

registration
coherence
proof end;
end;

registration
existence
ex b1 being infinite Field st b1 is polynomial_disjoint
proof end;
end;

registration
let R be polynomial_disjoint Ring;
coherence
proof end;
end;

registration
let F be Field;
let p be Element of [#] ();
coherence
() / () is polynomial_disjoint
proof end;
end;

registration
let F be polynomial_disjoint Field;
let p be non constant Element of the carrier of ();
coherence
proof end;
end;