FIELD_3: On the Intersection of Fields $F$ with $F[X]$

:: On the Intersection of Fields $F$ with $F[X]$
:: 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 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 (power R) . ((0. R),n) = 0. R

proof end;

registration

cluster INT.Ring 3 -> non degenerated almost_left_invertible ;

coherence by PEPIN:41;

end;

registration

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

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

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 :

registration

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

coherence

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

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 :

registration

let R be non almost_trivial Ring;

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

existence

proof end;

end;

definition

let R be Ring;

attr R is polynomial_disjoint means :Def3: :: FIELD_3:def 3
([#] R) /\ ([#] (Polynom-Ring R)) = {} ;

end;

:: deftheorem Def3 defines polynomial_disjoint FIELD_3:def 3 :

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 ;

end;

:: deftheorem defines carr FIELD_3:def 4 :

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

proof end;

consistency ;

end;

:: deftheorem Def4 defines addR FIELD_3:def 5 :

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

proof end;

uniqueness

proof end;

end;

:: deftheorem Def5 defines addR FIELD_3:def 6 :

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

proof end;

consistency ;

end;

:: deftheorem Def6 defines multR FIELD_3:def 7 :

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

proof end;

uniqueness

proof end;

end;

:: deftheorem Def7 defines multR FIELD_3:def 8 :

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

proof end;

uniqueness ;

end;

:: deftheorem Def8 defines ExField FIELD_3:def 9 :

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

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

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

cluster ExField (x,o) -> strict commutative ;

coherence

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) /\ ([#] (Polynom-Ring P))

proof end;

theorem Th14: :: FIELD_3:14

ex K being Field st ([#] K) /\ ([#] (Polynom-Ring 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) /\ ([#] (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)) )

proof end;

registration 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

proof end;

uniqueness

proof end;

end;

:: deftheorem Def9 defines isoR FIELD_3:def 10 :

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

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