:: On Monomorphisms and Subfields
:: by Christoph Schwarzweller
::
:: 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
proof end;
end;

theorem Th1: :: FIELD_2:1
for R being Ring
for S being b1 -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) )
proof end;

theorem Th2: :: FIELD_2:2
for R being Ring
for S being b1 -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 )
proof end;

theorem Th3: :: FIELD_2:3
for R being Ring
for S being b1 -monomorphic Ring
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 b1 -monomorphic Ring
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 b1 -monomorphic Ring
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 b1 -monomorphic Field
for f being Monomorphism of K,F
for a being Element of K st a <> 0. K holds
f . (a ") = (f . a) "
proof end;

notation
let R, S be Ring;
synonym R,S are_disjoint for R misses S;
end;

definition
let R, S be Ring;
redefine pred R misses S means :: FIELD_2:def 1
([#] R) /\ ([#] S) = {} ;
compatibility
( R,S are_disjoint iff ([#] R) /\ ([#] S) = {} )
by ;
end;

:: deftheorem defines are_disjoint FIELD_2:def 1 :
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;
func carr f -> non empty set equals :: FIELD_2:def 2
(([#] S) \ (rng f)) \/ ([#] R);
coherence
(([#] S) \ (rng f)) \/ ([#] R) is non empty set
;
end;

:: deftheorem defines carr FIELD_2:def 2 :
for R being Ring
for S being b1 -monomorphic Ring
for f being Monomorphism of R,S holds carr f = (([#] S) \ (rng f)) \/ ([#] R);

Lm1: for R being Ring
for S being b1 -monomorphic Ring
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 b1 -monomorphic Ring
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 b1 -monomorphic Ring
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 b1 -monomorphic comRing
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 b1 -monomorphic comRing
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;

:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
::::::::: f: R >--> S,
::::::::: addemb(f,x,y): R x R -> (S\ rng f) \/ R
:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
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;
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
( ( 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 b1 being Element of carr f holds
;
end;

for R being Ring
for S being b1 -monomorphic Ring
for f being Monomorphism of R,S
for a, b being Element of carr f holds

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

for R being Ring
for S being b1 -monomorphic Ring
for f being Monomorphism of R,S
for b4 being BinOp of (carr f) holds
( b4 = addemb f iff for a, b being Element of carr f holds b4 . (a,b) = addemb (f,a,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;
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
( ( 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 b1 being Element of carr f holds
( ( a in [#] K & b in [#] K & ( a = 0. K or b = 0. K ) implies ( b1 = the multF of K . (a,b) iff b1 = 0. K ) ) & ( a in [#] K & b in [#] K & a in [#] K & a <> 0. K & not b in [#] K implies ( b1 = the multF of K . (a,b) iff b1 = the multF of T . ((f . a),b) ) ) & ( a in [#] K & b in [#] K & b in [#] K & b <> 0. K & not a in [#] K implies ( b1 = the multF of K . (a,b) iff b1 = 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 ( b1 = the multF of K . (a,b) iff b1 = (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 ( b1 = 0. K iff b1 = 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 ( b1 = 0. K iff b1 = 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 ( b1 = 0. K iff b1 = (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 ( b1 = the multF of T . ((f . a),b) iff b1 = 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 ( b1 = the multF of T . ((f . a),b) iff b1 = (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 ( b1 = the multF of T . (a,(f . b)) iff b1 = (f ") . ( the multF of T . (a,b)) ) ) )
proof end;
end;

:: deftheorem defmultf defines multemb FIELD_2:def 5 :
for K being Field
for T being b1 -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) ) );

definition
let K be Field;
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
ex b1 being BinOp of (carr f) st
for a, b being Element of carr f holds b1 . (a,b) = multemb (f,a,b)
proof end;
uniqueness
for b1, b2 being BinOp of (carr f) st ( for a, b being Element of carr f holds b1 . (a,b) = multemb (f,a,b) ) & ( for a, b being Element of carr f holds b2 . (a,b) = multemb (f,a,b) ) holds
b1 = b2
proof end;
end;

:: deftheorem defmult defines multemb FIELD_2:def 6 :
for K being Field
for T being b1 -monomorphic comRing
for f being Monomorphism of K,T
for b4 being BinOp of (carr f) holds
( b4 = multemb f iff for a, b being Element of carr f holds b4 . (a,b) = multemb (f,a,b) );

definition
let K be Field;
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
ex b1 being strict doubleLoopStr st
( the carrier of b1 = carr f & the addF of b1 = addemb f & the multF of b1 = multemb f & the OneF of b1 = 1. K & the ZeroF of b1 = 0. K )
proof end;
uniqueness
for b1, b2 being strict doubleLoopStr st the carrier of b1 = carr f & the addF of b1 = addemb f & the multF of b1 = multemb f & the OneF of b1 = 1. K & the ZeroF of b1 = 0. K & the carrier of b2 = carr f & the addF of b2 = addemb f & the multF of b2 = multemb f & the OneF of b2 = 1. K & the ZeroF of b2 = 0. K holds
b1 = b2
;
end;

:: deftheorem defemb defines embField FIELD_2:def 7 :
for K being Field
for T being b1 -monomorphic comRing
for f being Monomorphism of K,T
for b4 being strict doubleLoopStr holds
( b4 = embField f iff ( the carrier of b4 = carr f & the addF of b4 = addemb f & the multF of b4 = multemb f & the OneF of b4 = 1. K & the ZeroF of b4 = 0. K ) );

registration
let K be Field;
let T be K -monomorphic comRing;
let f be Monomorphism of K,T;
coherence
not embField f is degenerated
proof end;
end;

Lm6: for K being Field
for T being b1 -monomorphic comRing
for f being Monomorphism of K,T st K,T are_disjoint holds
for a, b being Element of () 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 b1 -monomorphic comRing
for f being Monomorphism of K,T
for a, b being Element of ()
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 b1 -monomorphic comRing
for f being Monomorphism of K,T
for a, b being Element of ()
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 b1 -monomorphic comRing
for f being Monomorphism of K,T
for a, b being Element of ()
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 b1 -monomorphic comRing
for f being Monomorphism of K,T
for a, b being Element of ()
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 b1 -monomorphic comRing
for f being Monomorphism of K,T
for a, b being Element of ()
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 b1 -monomorphic comRing
for f being Monomorphism of K,T
for a, b being Element of ()
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 b1 -monomorphic comRing
for f being Monomorphism of K,T
for a, b being Element of ()
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 )
proof end;
end;

theorem Th6: :: FIELD_2:7
for K being Field
for T being b1 -monomorphic comRing
for f being Monomorphism of K,T st K,T are_disjoint holds
proof end;

theorem Th7: :: FIELD_2:8
for K being Field
for T being b1 -monomorphic comRing
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
proof end;
end;

theorem Th8: :: FIELD_2:9
for K being Field
for F being b1 -monomorphic Field
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 b1 -monomorphic comRing
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 b1 -monomorphic Field
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 b1 -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;

definition
let K be Field;
let F be K -monomorphic Field;
let f be Monomorphism of K,F;
func emb_iso f -> Function of (),F means :defiso: :: FIELD_2:def 8
( ( for a being Element of () st not a in K holds
it . a = a ) & ( for a being Element of () st a in K holds
it . a = f . a ) );
existence
ex b1 being Function of (),F st
( ( for a being Element of () st not a in K holds
b1 . a = a ) & ( for a being Element of () st a in K holds
b1 . a = f . a ) )
proof end;
uniqueness
for b1, b2 being Function of (),F st ( for a being Element of () st not a in K holds
b1 . a = a ) & ( for a being Element of () st a in K holds
b1 . a = f . a ) & ( for a being Element of () st not a in K holds
b2 . a = a ) & ( for a being Element of () st a in K holds
b2 . a = f . a ) holds
b1 = b2
proof end;
end;

:: deftheorem defiso defines emb_iso FIELD_2:def 8 :
for K being Field
for F being b1 -monomorphic Field
for f being Monomorphism of K,F
for b4 being Function of (),F holds
( b4 = emb_iso f iff ( ( for a being Element of () st not a in K holds
b4 . a = a ) & ( for a being Element of () st a in K holds
b4 . a = f . a ) ) );

registration
let K be Field;
let F be K -monomorphic Field;
let f be Monomorphism of K,F;
coherence
proof end;
end;

theorem Th11: :: FIELD_2:13
for K being Field
for F being b1 -monomorphic Field
for f being Monomorphism of K,F st K,F are_disjoint holds
proof end;

theorem Th12: :: FIELD_2:14
for K being Field
for F being b1 -monomorphic Field
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
proof end;
end;

theorem Th13: :: FIELD_2:15
for K being Field
for F being b1 -monomorphic Field
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 b1 -monomorphic Field
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 b1 -monomorphic Field
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 b1 -monomorphic Field st K,F are_disjoint holds
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 ) )
proof end;