:: by Christoph Schwarzweller

::

:: Received May 27, 2019

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

definition

let R be Ring;

let S be R -monomorphic Ring;

let f be Monomorphism of R,S;

:: original: "

redefine func f " -> Function of (rng f),R;

coherence

f " is Function of (rng f),R

end;
let S be R -monomorphic Ring;

let f be Monomorphism of R,S;

:: original: "

redefine func f " -> Function of (rng f),R;

coherence

f " is Function of (rng f),R

proof end;

theorem Th1: :: FIELD_2:1

for R being Ring

for S being b_{1} -monomorphic Ring

for f being Monomorphism of R,S

for a, b being Element of rng f holds

( (f ") . (a + b) = ((f ") . a) + ((f ") . b) & (f ") . (a * b) = ((f ") . a) * ((f ") . b) )

for S being b

for f being Monomorphism of R,S

for a, b being Element of rng f holds

( (f ") . (a + b) = ((f ") . a) + ((f ") . b) & (f ") . (a * b) = ((f ") . a) * ((f ") . b) )

proof end;

theorem Th2: :: FIELD_2:2

for R being Ring

for S being b_{1} -monomorphic Ring

for f being Monomorphism of R,S

for a being Element of rng f holds

( (f ") . a = 0. R iff a = 0. S )

for S being b

for f being Monomorphism of R,S

for a being Element of rng f holds

( (f ") . a = 0. R iff a = 0. S )

proof end;

theorem Th3: :: FIELD_2:3

for R being Ring

for S being b_{1} -monomorphic Ring

for f being Monomorphism of R,S holds

( (f ") . (1. S) = 1. R & (f ") . (0. S) = 0. R )

for S being b

for f being Monomorphism of R,S holds

( (f ") . (1. S) = 1. R & (f ") . (0. S) = 0. R )

proof end;

theorem :: FIELD_2:4

for R being Ring

for S being b_{1} -monomorphic Ring

for f being Monomorphism of R,S holds

( f " is one-to-one & f " is onto )

for S being b

for f being Monomorphism of R,S holds

( f " is one-to-one & f " is onto )

proof end;

theorem Th4: :: FIELD_2:5

for R being Ring

for S being b_{1} -monomorphic Ring

for f being Monomorphism of R,S

for a being Element of R holds

( f . a = 0. S iff a = 0. R )

for S being b

for f being Monomorphism of R,S

for a being Element of R holds

( f . a = 0. S iff a = 0. R )

proof end;

theorem Th5: :: FIELD_2:6

for K being Field

for F being b_{1} -monomorphic Field

for f being Monomorphism of K,F

for a being Element of K st a <> 0. K holds

f . (a ") = (f . a) "

for F being b

for f being Monomorphism of K,F

for a being Element of K st a <> 0. K holds

f . (a ") = (f . a) "

proof end;

definition

let R, S be Ring;

compatibility

( R,S are_disjoint iff ([#] R) /\ ([#] S) = {} ) by TSEP_1:def 3, XBOOLE_0:def 7;

end;
compatibility

( R,S are_disjoint iff ([#] R) /\ ([#] S) = {} ) by TSEP_1:def 3, XBOOLE_0:def 7;

:: deftheorem defines are_disjoint FIELD_2:def 1 :

for R, S being Ring holds

( R,S are_disjoint iff ([#] R) /\ ([#] S) = {} );

for R, S being Ring holds

( R,S are_disjoint iff ([#] R) /\ ([#] S) = {} );

definition

let R be Ring;

let S be R -monomorphic Ring;

let f be Monomorphism of R,S;

coherence

(([#] S) \ (rng f)) \/ ([#] R) is non empty set ;

end;
let S be R -monomorphic Ring;

let f be Monomorphism of R,S;

coherence

(([#] S) \ (rng f)) \/ ([#] R) is non empty set ;

:: deftheorem defines carr FIELD_2:def 2 :

for R being Ring

for S being b_{1} -monomorphic Ring

for f being Monomorphism of R,S holds carr f = (([#] S) \ (rng f)) \/ ([#] R);

for R being Ring

for S being b

for f being Monomorphism of R,S holds carr f = (([#] S) \ (rng f)) \/ ([#] R);

Lm1: for R being Ring

for S being b

for f being Monomorphism of R,S

for a being Element of carr f st not a in [#] R holds

( a in [#] S & not a in rng f )

proof end;

Lm2: for R being Ring

for S being b

for f being Monomorphism of R,S

for a, b being Element of carr f st not a in [#] R & b in [#] R holds

the addF of S . (a,(f . b)) in ([#] S) \ (rng f)

proof end;

Lm3: for R being Ring

for S being b

for f being Monomorphism of R,S

for a, b being Element of carr f st a in [#] R & not b in [#] R holds

the addF of S . ((f . a),b) in ([#] S) \ (rng f)

proof end;

Lm4: for K being Field

for T being b

for f being Monomorphism of K,T

for a, b being Element of carr f st not a in [#] K & b in [#] K & b <> 0. K holds

the multF of T . (a,(f . b)) in ([#] T) \ (rng f)

proof end;

Lm5: for K being Field

for T being b

for f being Monomorphism of K,T

for a, b being Element of carr f st not b in [#] K & a in [#] K & a <> 0. K holds

the multF of T . ((f . a),b) in ([#] T) \ (rng f)

proof end;

definition

let R be Ring;

let S be R -monomorphic Ring;

let f be Monomorphism of R,S;

let a, b be Element of carr f;

( ( a in [#] R & b in [#] R implies the addF of R . (a,b) is Element of carr f ) & ( a in [#] R & not b in [#] R implies the addF of S . ((f . a),b) is Element of carr f ) & ( b in [#] R & not a in [#] R implies the addF of S . (a,(f . b)) is Element of carr f ) & ( not a in [#] R & not b in [#] R & the addF of S . (a,b) in rng f implies (f ") . ( the addF of S . (a,b)) is Element of carr f ) & ( ( not a in [#] R or not b in [#] R ) & ( not a in [#] R or b in [#] R ) & ( not b in [#] R or a in [#] R ) & ( a in [#] R or b in [#] R or not the addF of S . (a,b) in rng f ) implies the addF of S . (a,b) is Element of carr f ) )

for b_{1} being Element of carr f holds

( ( a in [#] R & b in [#] R & a in [#] R & not b in [#] R implies ( b_{1} = the addF of R . (a,b) iff b_{1} = the addF of S . ((f . a),b) ) ) & ( a in [#] R & b in [#] R & b in [#] R & not a in [#] R implies ( b_{1} = the addF of R . (a,b) iff b_{1} = the addF of S . (a,(f . b)) ) ) & ( a in [#] R & b in [#] R & not a in [#] R & not b in [#] R & the addF of S . (a,b) in rng f implies ( b_{1} = the addF of R . (a,b) iff b_{1} = (f ") . ( the addF of S . (a,b)) ) ) & ( a in [#] R & not b in [#] R & b in [#] R & not a in [#] R implies ( b_{1} = the addF of S . ((f . a),b) iff b_{1} = the addF of S . (a,(f . b)) ) ) & ( a in [#] R & not b in [#] R & not a in [#] R & not b in [#] R & the addF of S . (a,b) in rng f implies ( b_{1} = the addF of S . ((f . a),b) iff b_{1} = (f ") . ( the addF of S . (a,b)) ) ) & ( b in [#] R & not a in [#] R & not a in [#] R & not b in [#] R & the addF of S . (a,b) in rng f implies ( b_{1} = the addF of S . (a,(f . b)) iff b_{1} = (f ") . ( the addF of S . (a,b)) ) ) )
;

end;
let S be R -monomorphic Ring;

let f be Monomorphism of R,S;

let a, b be Element of carr f;

func addemb (f,a,b) -> Element of carr f equals :defaddf: :: FIELD_2:def 3

the addF of R . (a,b) if ( a in [#] R & b in [#] R )

the addF of S . ((f . a),b) if ( a in [#] R & not b in [#] R )

the addF of S . (a,(f . b)) if ( b in [#] R & not a in [#] R )

(f ") . ( the addF of S . (a,b)) if ( not a in [#] R & not b in [#] R & the addF of S . (a,b) in rng f )

otherwise the addF of S . (a,b);

coherence the addF of R . (a,b) if ( a in [#] R & b in [#] R )

the addF of S . ((f . a),b) if ( a in [#] R & not b in [#] R )

the addF of S . (a,(f . b)) if ( b in [#] R & not a in [#] R )

(f ") . ( the addF of S . (a,b)) if ( not a in [#] R & not b in [#] R & the addF of S . (a,b) in rng f )

otherwise the addF of S . (a,b);

( ( a in [#] R & b in [#] R implies the addF of R . (a,b) is Element of carr f ) & ( a in [#] R & not b in [#] R implies the addF of S . ((f . a),b) is Element of carr f ) & ( b in [#] R & not a in [#] R implies the addF of S . (a,(f . b)) is Element of carr f ) & ( not a in [#] R & not b in [#] R & the addF of S . (a,b) in rng f implies (f ") . ( the addF of S . (a,b)) is Element of carr f ) & ( ( not a in [#] R or not b in [#] R ) & ( not a in [#] R or b in [#] R ) & ( not b in [#] R or a in [#] R ) & ( a in [#] R or b in [#] R or not the addF of S . (a,b) in rng f ) implies the addF of S . (a,b) is Element of carr f ) )

proof end;

consistency for b

( ( a in [#] R & b in [#] R & a in [#] R & not b in [#] R implies ( b

:: deftheorem defaddf defines addemb FIELD_2:def 3 :

for R being Ring

for S being b_{1} -monomorphic Ring

for f being Monomorphism of R,S

for a, b being Element of carr f holds

( ( a in [#] R & b in [#] R implies addemb (f,a,b) = the addF of R . (a,b) ) & ( a in [#] R & not b in [#] R implies addemb (f,a,b) = the addF of S . ((f . a),b) ) & ( b in [#] R & not a in [#] R implies addemb (f,a,b) = the addF of S . (a,(f . b)) ) & ( not a in [#] R & not b in [#] R & the addF of S . (a,b) in rng f implies addemb (f,a,b) = (f ") . ( the addF of S . (a,b)) ) & ( ( not a in [#] R or not b in [#] R ) & ( not a in [#] R or b in [#] R ) & ( not b in [#] R or a in [#] R ) & ( a in [#] R or b in [#] R or not the addF of S . (a,b) in rng f ) implies addemb (f,a,b) = the addF of S . (a,b) ) );

for R being Ring

for S being b

for f being Monomorphism of R,S

for a, b being Element of carr f holds

( ( a in [#] R & b in [#] R implies addemb (f,a,b) = the addF of R . (a,b) ) & ( a in [#] R & not b in [#] R implies addemb (f,a,b) = the addF of S . ((f . a),b) ) & ( b in [#] R & not a in [#] R implies addemb (f,a,b) = the addF of S . (a,(f . b)) ) & ( not a in [#] R & not b in [#] R & the addF of S . (a,b) in rng f implies addemb (f,a,b) = (f ") . ( the addF of S . (a,b)) ) & ( ( not a in [#] R or not b in [#] R ) & ( not a in [#] R or b in [#] R ) & ( not b in [#] R or a in [#] R ) & ( a in [#] R or b in [#] R or not the addF of S . (a,b) in rng f ) implies addemb (f,a,b) = the addF of S . (a,b) ) );

definition

let R be Ring;

let S be R -monomorphic Ring;

let f be Monomorphism of R,S;

ex b_{1} being BinOp of (carr f) st

for a, b being Element of carr f holds b_{1} . (a,b) = addemb (f,a,b)

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

b_{1} = b_{2}

end;
let S be R -monomorphic Ring;

let f be Monomorphism of R,S;

func addemb f -> BinOp of (carr f) means :defadd: :: FIELD_2:def 4

for a, b being Element of carr f holds it . (a,b) = addemb (f,a,b);

existence for a, b being Element of carr f holds it . (a,b) = addemb (f,a,b);

ex b

for a, b being Element of carr f holds b

proof end;

uniqueness for b

b

proof end;

:: deftheorem defadd defines addemb FIELD_2:def 4 :

for R being Ring

for S being b_{1} -monomorphic Ring

for f being Monomorphism of R,S

for b_{4} being BinOp of (carr f) holds

( b_{4} = addemb f iff for a, b being Element of carr f holds b_{4} . (a,b) = addemb (f,a,b) );

for R being Ring

for S being b

for f being Monomorphism of R,S

for b

( b

definition

let K be Field;

let T be K -monomorphic comRing;

let f be Monomorphism of K,T;

let a, b be Element of carr f;

( ( a in [#] K & b in [#] K implies the multF of K . (a,b) is Element of carr f ) & ( ( a = 0. K or b = 0. K ) implies 0. K is Element of carr f ) & ( a in [#] K & a <> 0. K & not b in [#] K implies the multF of T . ((f . a),b) is Element of carr f ) & ( b in [#] K & b <> 0. K & not a in [#] K implies the multF of T . (a,(f . b)) is Element of carr f ) & ( not a in [#] K & not b in [#] K & the multF of T . (a,b) in rng f implies (f ") . ( the multF of T . (a,b)) is Element of carr f ) & ( ( a in [#] K & b in [#] K ) or a = 0. K or b = 0. K or ( a in [#] K & a <> 0. K & not b in [#] K ) or ( b in [#] K & b <> 0. K & not a in [#] K ) or ( not a in [#] K & not b in [#] K & the multF of T . (a,b) in rng f ) or the multF of T . (a,b) is Element of carr f ) )

for b_{1} being Element of carr f holds

( ( a in [#] K & b in [#] K & ( a = 0. K or b = 0. K ) implies ( b_{1} = the multF of K . (a,b) iff b_{1} = 0. K ) ) & ( a in [#] K & b in [#] K & a in [#] K & a <> 0. K & not b in [#] K implies ( b_{1} = the multF of K . (a,b) iff b_{1} = the multF of T . ((f . a),b) ) ) & ( a in [#] K & b in [#] K & b in [#] K & b <> 0. K & not a in [#] K implies ( b_{1} = the multF of K . (a,b) iff b_{1} = the multF of T . (a,(f . b)) ) ) & ( a in [#] K & b in [#] K & not a in [#] K & not b in [#] K & the multF of T . (a,b) in rng f implies ( b_{1} = the multF of K . (a,b) iff b_{1} = (f ") . ( the multF of T . (a,b)) ) ) & ( ( a = 0. K or b = 0. K ) & a in [#] K & a <> 0. K & not b in [#] K implies ( b_{1} = 0. K iff b_{1} = the multF of T . ((f . a),b) ) ) & ( ( a = 0. K or b = 0. K ) & b in [#] K & b <> 0. K & not a in [#] K implies ( b_{1} = 0. K iff b_{1} = the multF of T . (a,(f . b)) ) ) & ( ( a = 0. K or b = 0. K ) & not a in [#] K & not b in [#] K & the multF of T . (a,b) in rng f implies ( b_{1} = 0. K iff b_{1} = (f ") . ( the multF of T . (a,b)) ) ) & ( a in [#] K & a <> 0. K & not b in [#] K & b in [#] K & b <> 0. K & not a in [#] K implies ( b_{1} = the multF of T . ((f . a),b) iff b_{1} = the multF of T . (a,(f . b)) ) ) & ( a in [#] K & a <> 0. K & not b in [#] K & not a in [#] K & not b in [#] K & the multF of T . (a,b) in rng f implies ( b_{1} = the multF of T . ((f . a),b) iff b_{1} = (f ") . ( the multF of T . (a,b)) ) ) & ( b in [#] K & b <> 0. K & not a in [#] K & not a in [#] K & not b in [#] K & the multF of T . (a,b) in rng f implies ( b_{1} = the multF of T . (a,(f . b)) iff b_{1} = (f ") . ( the multF of T . (a,b)) ) ) )

end;
let T be K -monomorphic comRing;

let f be Monomorphism of K,T;

let a, b be Element of carr f;

func multemb (f,a,b) -> Element of carr f equals :defmultf: :: FIELD_2:def 5

the multF of K . (a,b) if ( a in [#] K & b in [#] K )

0. K if ( a = 0. K or b = 0. K )

the multF of T . ((f . a),b) if ( a in [#] K & a <> 0. K & not b in [#] K )

the multF of T . (a,(f . b)) if ( b in [#] K & b <> 0. K & not a in [#] K )

(f ") . ( the multF of T . (a,b)) if ( not a in [#] K & not b in [#] K & the multF of T . (a,b) in rng f )

otherwise the multF of T . (a,b);

coherence the multF of K . (a,b) if ( a in [#] K & b in [#] K )

0. K if ( a = 0. K or b = 0. K )

the multF of T . ((f . a),b) if ( a in [#] K & a <> 0. K & not b in [#] K )

the multF of T . (a,(f . b)) if ( b in [#] K & b <> 0. K & not a in [#] K )

(f ") . ( the multF of T . (a,b)) if ( not a in [#] K & not b in [#] K & the multF of T . (a,b) in rng f )

otherwise the multF of T . (a,b);

( ( a in [#] K & b in [#] K implies the multF of K . (a,b) is Element of carr f ) & ( ( a = 0. K or b = 0. K ) implies 0. K is Element of carr f ) & ( a in [#] K & a <> 0. K & not b in [#] K implies the multF of T . ((f . a),b) is Element of carr f ) & ( b in [#] K & b <> 0. K & not a in [#] K implies the multF of T . (a,(f . b)) is Element of carr f ) & ( not a in [#] K & not b in [#] K & the multF of T . (a,b) in rng f implies (f ") . ( the multF of T . (a,b)) is Element of carr f ) & ( ( a in [#] K & b in [#] K ) or a = 0. K or b = 0. K or ( a in [#] K & a <> 0. K & not b in [#] K ) or ( b in [#] K & b <> 0. K & not a in [#] K ) or ( not a in [#] K & not b in [#] K & the multF of T . (a,b) in rng f ) or the multF of T . (a,b) is Element of carr f ) )

proof end;

consistency for b

( ( a in [#] K & b in [#] K & ( a = 0. K or b = 0. K ) implies ( b

proof end;

:: deftheorem defmultf defines multemb FIELD_2:def 5 :

for K being Field

for T being b_{1} -monomorphic comRing

for f being Monomorphism of K,T

for a, b being Element of carr f holds

( ( a in [#] K & b in [#] K implies multemb (f,a,b) = the multF of K . (a,b) ) & ( ( a = 0. K or b = 0. K ) implies multemb (f,a,b) = 0. K ) & ( a in [#] K & a <> 0. K & not b in [#] K implies multemb (f,a,b) = the multF of T . ((f . a),b) ) & ( b in [#] K & b <> 0. K & not a in [#] K implies multemb (f,a,b) = the multF of T . (a,(f . b)) ) & ( not a in [#] K & not b in [#] K & the multF of T . (a,b) in rng f implies multemb (f,a,b) = (f ") . ( the multF of T . (a,b)) ) & ( ( a in [#] K & b in [#] K ) or a = 0. K or b = 0. K or ( a in [#] K & a <> 0. K & not b in [#] K ) or ( b in [#] K & b <> 0. K & not a in [#] K ) or ( not a in [#] K & not b in [#] K & the multF of T . (a,b) in rng f ) or multemb (f,a,b) = the multF of T . (a,b) ) );

for K being Field

for T being b

for f being Monomorphism of K,T

for a, b being Element of carr f holds

( ( a in [#] K & b in [#] K implies multemb (f,a,b) = the multF of K . (a,b) ) & ( ( a = 0. K or b = 0. K ) implies multemb (f,a,b) = 0. K ) & ( a in [#] K & a <> 0. K & not b in [#] K implies multemb (f,a,b) = the multF of T . ((f . a),b) ) & ( b in [#] K & b <> 0. K & not a in [#] K implies multemb (f,a,b) = the multF of T . (a,(f . b)) ) & ( not a in [#] K & not b in [#] K & the multF of T . (a,b) in rng f implies multemb (f,a,b) = (f ") . ( the multF of T . (a,b)) ) & ( ( a in [#] K & b in [#] K ) or a = 0. K or b = 0. K or ( a in [#] K & a <> 0. K & not b in [#] K ) or ( b in [#] K & b <> 0. K & not a in [#] K ) or ( not a in [#] K & not b in [#] K & the multF of T . (a,b) in rng f ) or multemb (f,a,b) = the multF of T . (a,b) ) );

definition

let K be Field;

let T be K -monomorphic comRing;

let f be Monomorphism of K,T;

ex b_{1} being BinOp of (carr f) st

for a, b being Element of carr f holds b_{1} . (a,b) = multemb (f,a,b)

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

b_{1} = b_{2}

end;
let T be K -monomorphic comRing;

let f be Monomorphism of K,T;

func multemb f -> BinOp of (carr f) means :defmult: :: FIELD_2:def 6

for a, b being Element of carr f holds it . (a,b) = multemb (f,a,b);

existence for a, b being Element of carr f holds it . (a,b) = multemb (f,a,b);

ex b

for a, b being Element of carr f holds b

proof end;

uniqueness for b

b

proof end;

:: deftheorem defmult defines multemb FIELD_2:def 6 :

for K being Field

for T being b_{1} -monomorphic comRing

for f being Monomorphism of K,T

for b_{4} being BinOp of (carr f) holds

( b_{4} = multemb f iff for a, b being Element of carr f holds b_{4} . (a,b) = multemb (f,a,b) );

for K being Field

for T being b

for f being Monomorphism of K,T

for b

( b

definition

let K be Field;

let T be K -monomorphic comRing;

let f be Monomorphism of K,T;

ex b_{1} being strict doubleLoopStr st

( the carrier of b_{1} = carr f & the addF of b_{1} = addemb f & the multF of b_{1} = multemb f & the OneF of b_{1} = 1. K & the ZeroF of b_{1} = 0. K )

for b_{1}, b_{2} being strict doubleLoopStr st the carrier of b_{1} = carr f & the addF of b_{1} = addemb f & the multF of b_{1} = multemb f & the OneF of b_{1} = 1. K & the ZeroF of b_{1} = 0. K & the carrier of b_{2} = carr f & the addF of b_{2} = addemb f & the multF of b_{2} = multemb f & the OneF of b_{2} = 1. K & the ZeroF of b_{2} = 0. K holds

b_{1} = b_{2}
;

end;
let T be K -monomorphic comRing;

let f be Monomorphism of K,T;

func embField f -> strict doubleLoopStr means :defemb: :: FIELD_2:def 7

( the carrier of it = carr f & the addF of it = addemb f & the multF of it = multemb f & the OneF of it = 1. K & the ZeroF of it = 0. K );

existence ( the carrier of it = carr f & the addF of it = addemb f & the multF of it = multemb f & the OneF of it = 1. K & the ZeroF of it = 0. K );

ex b

( the carrier of b

proof end;

uniqueness for b

b

:: deftheorem defemb defines embField FIELD_2:def 7 :

for K being Field

for T being b_{1} -monomorphic comRing

for f being Monomorphism of K,T

for b_{4} being strict doubleLoopStr holds

( b_{4} = embField f iff ( the carrier of b_{4} = carr f & the addF of b_{4} = addemb f & the multF of b_{4} = multemb f & the OneF of b_{4} = 1. K & the ZeroF of b_{4} = 0. K ) );

for K being Field

for T being b

for f being Monomorphism of K,T

for b

( b

registration

let K be Field;

let T be K -monomorphic comRing;

let f be Monomorphism of K,T;

coherence

not embField f is degenerated

end;
let T be K -monomorphic comRing;

let f be Monomorphism of K,T;

coherence

not embField f is degenerated

proof end;

Lm6: for K being Field

for T being b

for f being Monomorphism of K,T st K,T are_disjoint holds

for a, b being Element of (embField f) st a in [#] K & not b in [#] K holds

for a1, b1 being Element of carr f st a1 = a & b1 = b holds

( a + b = the addF of T . ((f . a1),b1) & b + a = the addF of T . (b1,(f . a1)) & not a + b in [#] K & not b + a in [#] K )

proof end;

Lm7: for K being Field

for T being b

for f being Monomorphism of K,T

for a, b being Element of (embField f)

for a1, b1 being Element of K st a1 = a & b1 = b holds

( a + b = a1 + b1 & b + a = b1 + a1 )

proof end;

Lm8: for K being Field

for T being b

for f being Monomorphism of K,T

for a, b being Element of (embField f)

for a1, b1 being Element of T st K,T are_disjoint & not a in [#] K & not b in [#] K & not the addF of T . (a,b) in rng f & a1 = a & b1 = b holds

( a + b = a1 + b1 & b + a = b1 + a1 & not a + b in [#] K & not b + a in [#] K )

proof end;

Lm9: for K being Field

for T being b

for f being Monomorphism of K,T

for a, b being Element of (embField f)

for a1, b1 being Element of T st not a in [#] K & not b in [#] K & the addF of T . (a,b) in rng f & a1 = a & b1 = b holds

( a + b = (f ") . (a1 + b1) & b + a = (f ") . (b1 + a1) & a + b in [#] K & b + a in [#] K )

proof end;

Lm10: for K being Field

for T being b

for f being Monomorphism of K,T

for a, b being Element of (embField f)

for a1, b1 being Element of carr f st K,T are_disjoint & a in [#] K & a <> 0. K & not b in [#] K & a1 = a & b1 = b holds

( a * b = the multF of T . ((f . a1),b1) & b * a = the multF of T . (b1,(f . a1)) & not a * b in [#] K & not b * a in [#] K )

proof end;

Lm11: for K being Field

for T being b

for f being Monomorphism of K,T

for a, b being Element of (embField f)

for a1, b1 being Element of K st a1 = a & b1 = b holds

( a * b = a1 * b1 & b * a = b1 * a1 )

proof end;

Lm12: for K being Field

for T being b

for f being Monomorphism of K,T

for a, b being Element of (embField f)

for a1, b1 being Element of T st K,T are_disjoint & not a in [#] K & not b in [#] K & not the multF of T . (a,b) in rng f & a1 = a & b1 = b holds

( a * b = a1 * b1 & b * a = b1 * a1 & not a * b in [#] K & not b * a in [#] K )

proof end;

Lm13: for K being Field

for T being b

for f being Monomorphism of K,T

for a, b being Element of (embField f)

for a1, b1 being Element of T st not a in [#] K & not b in [#] K & the multF of T . (a,b) in rng f & a1 = a & b1 = b holds

( a * b = (f ") . (a1 * b1) & b * a = (f ") . (b1 * a1) & a * b in [#] K & b * a in [#] K )

proof end;

registration

let K be Field;

let T be K -monomorphic comRing;

let f be Monomorphism of K,T;

coherence

( embField f is Abelian & embField f is right_zeroed )

end;
let T be K -monomorphic comRing;

let f be Monomorphism of K,T;

coherence

( embField f is Abelian & embField f is right_zeroed )

proof end;

theorem Th6: :: FIELD_2:7

for K being Field

for T being b_{1} -monomorphic comRing

for f being Monomorphism of K,T st K,T are_disjoint holds

embField f is add-associative

for T being b

for f being Monomorphism of K,T st K,T are_disjoint holds

embField f is add-associative

proof end;

theorem Th7: :: FIELD_2:8

for K being Field

for T being b_{1} -monomorphic comRing

for f being Monomorphism of K,T st K,T are_disjoint holds

embField f is right_complementable

for T being b

for f being Monomorphism of K,T st K,T are_disjoint holds

embField f is right_complementable

proof end;

registration

let K be Field;

let T be K -monomorphic comRing;

let f be Monomorphism of K,T;

coherence

( embField f is commutative & embField f is well-unital )

end;
let T be K -monomorphic comRing;

let f be Monomorphism of K,T;

coherence

( embField f is commutative & embField f is well-unital )

proof end;

theorem Th8: :: FIELD_2:9

for K being Field

for F being b_{1} -monomorphic Field

for f being Monomorphism of K,F st K,F are_disjoint holds

embField f is associative

for F being b

for f being Monomorphism of K,F st K,F are_disjoint holds

embField f is associative

proof end;

theorem Th9: :: FIELD_2:10

for K being Field

for T being b_{1} -monomorphic comRing

for f being Monomorphism of K,T st K,T are_disjoint holds

embField f is distributive

for T being b

for f being Monomorphism of K,T st K,T are_disjoint holds

embField f is distributive

proof end;

theorem Th10: :: FIELD_2:11

for K being Field

for F being b_{1} -monomorphic Field

for f being Monomorphism of K,F st K,F are_disjoint holds

embField f is almost_left_invertible

for F being b

for f being Monomorphism of K,F st K,F are_disjoint holds

embField f is almost_left_invertible

proof end;

theorem :: FIELD_2:12

for K being Field

for F being b_{1} -monomorphic Field

for f being Monomorphism of K,F st K,F are_disjoint holds

embField f is Field by Th6, Th8, Th9, Th7, Th10;

for F being b

for f being Monomorphism of K,F st K,F are_disjoint holds

embField f is Field by Th6, Th8, Th9, Th7, Th10;

definition

let K be Field;

let F be K -monomorphic Field;

let f be Monomorphism of K,F;

ex b_{1} being Function of (embField f),F st

( ( for a being Element of (embField f) st not a in K holds

b_{1} . a = a ) & ( for a being Element of (embField f) st a in K holds

b_{1} . a = f . a ) )

for b_{1}, b_{2} being Function of (embField f),F st ( for a being Element of (embField f) st not a in K holds

b_{1} . a = a ) & ( for a being Element of (embField f) st a in K holds

b_{1} . a = f . a ) & ( for a being Element of (embField f) st not a in K holds

b_{2} . a = a ) & ( for a being Element of (embField f) st a in K holds

b_{2} . a = f . a ) holds

b_{1} = b_{2}

end;
let F be K -monomorphic Field;

let f be Monomorphism of K,F;

func emb_iso f -> Function of (embField f),F means :defiso: :: FIELD_2:def 8

( ( for a being Element of (embField f) st not a in K holds

it . a = a ) & ( for a being Element of (embField f) st a in K holds

it . a = f . a ) );

existence ( ( for a being Element of (embField f) st not a in K holds

it . a = a ) & ( for a being Element of (embField f) st a in K holds

it . a = f . a ) );

ex b

( ( for a being Element of (embField f) st not a in K holds

b

b

proof end;

uniqueness for b

b

b

b

b

b

proof end;

:: deftheorem defiso defines emb_iso FIELD_2:def 8 :

for K being Field

for F being b_{1} -monomorphic Field

for f being Monomorphism of K,F

for b_{4} being Function of (embField f),F holds

( b_{4} = emb_iso f iff ( ( for a being Element of (embField f) st not a in K holds

b_{4} . a = a ) & ( for a being Element of (embField f) st a in K holds

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

for K being Field

for F being b

for f being Monomorphism of K,F

for b

( b

b

b

registration

let K be Field;

let F be K -monomorphic Field;

let f be Monomorphism of K,F;

coherence

emb_iso f is unity-preserving

end;
let F be K -monomorphic Field;

let f be Monomorphism of K,F;

coherence

emb_iso f is unity-preserving

proof end;

theorem Th11: :: FIELD_2:13

for K being Field

for F being b_{1} -monomorphic Field

for f being Monomorphism of K,F st K,F are_disjoint holds

emb_iso f is additive

for F being b

for f being Monomorphism of K,F st K,F are_disjoint holds

emb_iso f is additive

proof end;

theorem Th12: :: FIELD_2:14

for K being Field

for F being b_{1} -monomorphic Field

for f being Monomorphism of K,F st K,F are_disjoint holds

emb_iso f is multiplicative

for F being b

for f being Monomorphism of K,F st K,F are_disjoint holds

emb_iso f is multiplicative

proof end;

registration

let K be Field;

let F be K -monomorphic Field;

let f be Monomorphism of K,F;

coherence

emb_iso f is one-to-one

end;
let F be K -monomorphic Field;

let f be Monomorphism of K,F;

coherence

emb_iso f is one-to-one

proof end;

theorem Th13: :: FIELD_2:15

for K being Field

for F being b_{1} -monomorphic Field

for f being Monomorphism of K,F st K,F are_disjoint holds

emb_iso f is onto

for F being b

for f being Monomorphism of K,F st K,F are_disjoint holds

emb_iso f is onto

proof end;

theorem Th14: :: FIELD_2:16

for K being Field

for F being b_{1} -monomorphic Field

for f being Monomorphism of K,F st K,F are_disjoint holds

F, embField f are_isomorphic

for F being b

for f being Monomorphism of K,F st K,F are_disjoint holds

F, embField f are_isomorphic

proof end;

theorem Th15: :: FIELD_2:17

for K being Field

for F being b_{1} -monomorphic Field

for f being Monomorphism of K,F

for E being Field st E = embField f holds

K is Subfield of E

for F being b

for f being Monomorphism of K,F

for E being Field st E = embField f holds

K is Subfield of E

proof end;

theorem Th16: :: FIELD_2:18

for K being Field

for F being b_{1} -monomorphic Field st K,F are_disjoint holds

ex E being Field st

( E,F are_isomorphic & K is Subfield of E )

for F being b

ex E being Field st

( E,F are_isomorphic & K is Subfield of E )

proof end;

theorem :: FIELD_2:19

for K, F being Field st K,F are_disjoint holds

( F is K -monomorphic iff ex E being Field st

( E,F are_isomorphic & K is Subfield of E ) )

( F is K -monomorphic iff ex E being Field st

( E,F are_isomorphic & K is Subfield of E ) )

proof end;

::::::::: f: R >--> S,

::::::::: addemb(f,x,y): R x R -> (S\ rng f) \/ R

:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::