:: On Monomorphisms and Subfields
:: by Christoph Schwarzweller
::
:: Received May 27, 2019
:: Copyright (c) 2019-2026 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies ARYTM_3, VECTSP_1, ALGSTR_0, STRUCT_0, SUBSET_1, SUPINF_2,
BINOP_1, TARSKI, MESFUNC1, FUNCSDOM, ZFMISC_1, EC_PF_1, RLVECT_1,
GROUP_1, FUNCT_1, RELAT_1, LATTICES, REALSET1, XBOOLE_0, NUMBERS, RING_3,
VECTSP_2, FUNCT_2, ARYTM_1, MSSUBFAM, MOD_4, QUOFIELD, GROUP_2, WELLORD1,
GROEB_2, FIELD_2, C0SP1, FDIFF_1;
notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, FUNCT_1, RELSET_1, REALSET1,
PARTFUN1, FUNCT_2, BINOP_1, STRUCT_0, VECTSP_1, VECTSP_2, QUOFIELD,
TSEP_1, MOD_4, GROUP_1, GROUP_6, ALGSTR_0, ALGSTR_1, RLVECT_1, RINGCAT1,
C0SP1, EC_PF_1, RING_2, RING_3;
constructors FUNCT_2, FUNCT_1, XBOOLE_0, RELSET_1, REALSET1, STRUCT_0,
QUOFIELD, RLVECT_1, RINGCAT1, RING_3, C0SP1, EC_PF_1, TSEP_1;
registrations XBOOLE_0, RELSET_1, STRUCT_0, VECTSP_1, ALGSTR_0, REALSET1,
RLVECT_1, QUOFIELD, FUNCT_1, FUNCT_2, RELAT_1, MOD_4, RINGCAT1, RING_3;
requirements SUBSET, BOOLE;
equalities BINOP_1, REALSET1, STRUCT_0, ALGSTR_0;
expansions STRUCT_0, GROUP_1, ALGSTR_0, RLVECT_1, VECTSP_1, TARSKI, GROUP_6,
FUNCT_1, FUNCT_2;
theorems RLVECT_1, FUNCT_2, FUNCT_1, QUOFIELD, XBOOLE_0, BINOP_1, RELAT_1,
TARSKI, ALGSTR_0, MOD_4, VECTSP_1, VECTSP_2, GROUP_1, GROUP_6, RING_2,
XBOOLE_1, EC_PF_1, ZFMISC_1, TSEP_1, RING_3, RINGCAT1;
schemes BINOP_1, FUNCT_2;
begin
reserve R for Ring, S for R-monomorphic Ring,
K for Field, F for K-monomorphic Field,
T for K-monomorphic comRing;
definition
let R,S;
let f be Monomorphism of R,S;
redefine func f" -> Function of rng f,R; :: redefines " (FUNCT_1, definition)
coherence
proof
dom f = [#]R & rng f c= [#]S by FUNCT_2:def 1;
then f is Function of [#]R,(rng f) by FUNCT_2:2;
hence thesis by FUNCT_2:25;
end;
end;
theorem Th1:
for f being Monomorphism of R,S, a,b being Element of rng f
holds f".(a+b) = f".a + f".b & f".(a*b) = f".a * f".b
proof
let f be Monomorphism of R,S, a,b be Element of rng f;
consider x being object such that
A1: x in [#]R & f.x = a by FUNCT_2:11;
reconsider x as Element of R by A1;
consider y being object such that
A2: y in [#]R & f.y = b by FUNCT_2:11;
reconsider y as Element of R by A2;
A3: [#]R = dom f by FUNCT_2:def 1; then
A4: f".b = y by A2,FUNCT_1:34;
A5: [#]R = dom f by FUNCT_2:def 1;
f.(x + y) = a + b by A1,A2,VECTSP_1:def 20;
hence f".(a+b)=x+y by A5,FUNCT_1:34 .= f".a+f".b by A1,A3,A4,FUNCT_1:34;
f.(x*y) = a*b by A1,A2, GROUP_6:def 6;
hence f".(a*b)=x*y by A5,FUNCT_1:34 .= f".a*f".b by A1,A3,A4,FUNCT_1:34;
end;
theorem Th2:
for f being Monomorphism of R,S, a being Element of rng f
holds f".(a) = 0.R iff a = 0.S
proof
let f be Monomorphism of R,S, a be Element of rng f;
A1: now assume f".(a) = 0.R; then
f.(0.R) = a by FUNCT_1:35;
hence a = 0.S by RING_2:6;
end;
A2: dom f = [#]R by FUNCT_2:def 1;
now assume a = 0.S; then
f.(0.R) = a by RING_2:6;
hence f".(a) = 0.R by A2,FUNCT_1:34;
end;
hence thesis by A1;
end;
theorem Th3:
for f being Monomorphism of R,S holds f".(1.S) = 1.R & f".(0.S) = 0.R
proof
let f be Monomorphism of R,S;
A1: [#]R = dom f by FUNCT_2:def 1;
f.(1_R) = 1_S by GROUP_1:def 13;
hence f".(1.S) = 1.R by A1,FUNCT_1:34;
f.(0.R) = 0.S by RING_2:6; then
reconsider o = 0.S as Element of (rng f) by FUNCT_2:4;
f".(0.S) = f".(o + o) = f".o + f".o by Th1;
hence thesis by RLVECT_1:9;
end;
theorem
for f being Monomorphism of R,S holds f" is one-to-one onto
proof
let f be Monomorphism of R,S;
rng(f") = dom f by FUNCT_1:33 .= [#]R by FUNCT_2:def 1;
hence thesis;
end;
theorem Th4:
for f being Monomorphism of R,S, a being Element of R
holds f.a = 0.S iff a = 0.R
proof
let f be Monomorphism of R,S, a be Element of R;
now assume f.a = 0.S; then
f.a = f.(0.R) by RING_2:6;
hence a = 0.R by FUNCT_2:19;
end;
hence thesis by RING_2:6;
end;
theorem Th5:
for f being Monomorphism of K,F,a being Element of K
st a <> 0.K holds f.(a") = (f.a)"
proof
let f be Monomorphism of K,F, x be Element of K;
assume
AS: x <> 0.K;
A1: f.(x")*f.x = f.(x"*x) by GROUP_6:def 6 .= f.(1_K) by AS,VECTSP_1:def 10
.= 1_F by GROUP_1:def 13 .= 1.F;
f.x <> 0.F by AS,Th4;
hence thesis by A1,VECTSP_1:def 10;
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,S are_disjoint means :: redefines are_disjoint (FIELD_2, synonym) → misses (TSEP_1, definition)
[#]R /\ [#]S = {};
compatibility by TSEP_1:def 3,XBOOLE_0:def 7;
end;
definition
let R,S;
let f be Monomorphism of R,S;
func carr f -> non empty set equals
([#]S \ rng f) \/ [#]R;
coherence;
end;
Lm1:
for f being Monomorphism of R,S, a being Element of carr f
st not a in [#]R holds a in [#]S & not a in rng f
proof
let f be Monomorphism of R,S, a be Element of carr f;
assume not a in [#]R; then
a in [#]S \ rng f by XBOOLE_0:def 3;
hence thesis by XBOOLE_0:def 5;
end;
Lm2:
for f being Monomorphism of R,S,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
let f be Monomorphism of R,S, a,b be Element of carr f;
assume
A1: not a in [#]R & b in [#]R; then
reconsider y = b as Element of [#]R;
A2: a in [#]S \ rng f by A1,XBOOLE_0:def 3; then
A3: a in [#]S & not a in rng f by XBOOLE_0:def 5;
reconsider x = a as Element of [#]S by A2;
reconsider fy = f.y as Element of [#]S;
now assume (the addF of S).(x,f.y) in rng f; then
consider c being object such that
A4: c in dom f & f.c = (the addF of S).(x,f.y) by FUNCT_1:def 3;
reconsider z = c as Element of [#]R by A4;
f.z - fy = (x + fy) + -fy by A4 .= x + (fy + - fy) by RLVECT_1:def 3
.= x + 0.S by RLVECT_1:5; then
A5: x = f.(z - y) by RING_2:8;
dom f = [#]R by FUNCT_2:def 1;
hence contradiction by A3,A5,FUNCT_1:def 3;
end;
hence (the addF of S).(a,f.b) in ([#]S) \ (rng f) by XBOOLE_0:def 5;
end;
Lm3:
for f being Monomorphism of R,S, 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
let f be Monomorphism of R,S, a,b be Element of carr f;
assume
A1: a in [#]R & not b in [#]R; then
reconsider x = a as Element of [#]R;
A2: b in [#]S \ rng f by A1,XBOOLE_0:def 3; then
A3: b in [#]S & not(b in rng f) by XBOOLE_0:def 5;
reconsider y = b as Element of [#]S by A2;
reconsider fx = f.x as Element of [#]S;
now assume (the addF of S).(f.x,y) in rng f; then
consider c being object such that
A4: c in dom f & f.c = (the addF of S).(f.x,y) by FUNCT_1:def 3;
reconsider z = c as Element of [#]R by A4;
f.z - fx = (fx + y)+ -fx by A4 .= y +(fx + - fx) by RLVECT_1:def 3
.= y + 0.S by RLVECT_1:5; then
A5: y = f.(z - x) by RING_2:8;
dom f = [#]R by FUNCT_2:def 1;
hence contradiction by A3,A5,FUNCT_1:def 3;
end;
hence (the addF of S).(f.a,b) in ([#]S)\(rng f) by XBOOLE_0:def 5;
end;
Lm4:
for f being Monomorphism of K,T,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
let f be Monomorphism of K,T,a,b be Element of carr f;
assume
A1: not a in [#]K & b in [#]K & b <> 0.K; then
reconsider y = b as Element of [#]K;
reconsider fy1 = f.(y") as Element of T;
A2: a in [#]T \ rng f by A1,XBOOLE_0:def 3; then
A3: a in [#]T & not(a in (rng f)) by XBOOLE_0:def 5;
reconsider x = a as Element of [#]T by A2;
reconsider fy = f.y as Element of [#]T;
now assume (the multF of T).(x,f.y) in rng f; then
consider c being object such that
A4: c in dom f & f.c = (the multF of T).(x,f.y) by FUNCT_1:def 3;
reconsider z = c as Element of [#]K by A4;
f.z * fy1 = (x * fy) * fy1 by A4 .= x * (fy * fy1) by GROUP_1:def 3
.= x * f.(y * y") by GROUP_6:def 6 .= x * f.(y" * y) by GROUP_1:def 12
.= x * f.(1_K) by A1,VECTSP_1:def 10 .= x * 1_T by GROUP_1:def 13
.= x; then
A5: x = f.(z * y") by GROUP_6:def 6;
dom f = [#]K by FUNCT_2:def 1;
hence contradiction by A3,A5,FUNCT_1:def 3;
end;
hence (the multF of T).(a,f.b) in [#]T \ rng f by XBOOLE_0:def 5;
end;
Lm5:
for f being Monomorphism of K,T,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
let f be Monomorphism of K,T,a,b be Element of carr f;
assume
A1: not b in [#]K & a in [#]K & a <> 0.K; then
reconsider x = a as Element of [#]K;
reconsider fx1 = f.(x") as Element of T;
A2: b in ([#]T) \ (rng f) by A1,XBOOLE_0:def 3; then
A3: b in ([#]T) & not(b in (rng f)) by XBOOLE_0:def 5;
reconsider y = b as Element of [#]T by A2;
reconsider fx = f.x as Element of [#]T;
now assume (the multF of T).(f.x,y) in rng f; then
consider c being object such that
A4: c in dom f & f.c = (the multF of T).(f.x,y) by FUNCT_1:def 3;
reconsider z = c as Element of [#]K by A4;
f.z * fx1 = (f.x * y) * fx1 by A4 .= (y * f.x) * fx1 by GROUP_1:def 12
.= y * (fx * fx1) by GROUP_1:def 3 .= y * f.(x * x") by GROUP_6:def 6
.= y * f.(x" * x) by GROUP_1:def 12 .= y * f.(1_K) by A1,VECTSP_1:def 10
.= y * 1_T by GROUP_1:def 13 .= y; then
A5: y = f.(z * x") by GROUP_6:def 6;
dom f = [#]K by FUNCT_2:def 1;
hence contradiction by A3,A5,FUNCT_1:def 3;
end;
hence (the multF of T).(f.a,b) in [#]T \ rng f by XBOOLE_0:def 5;
end;
:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
::::::::: f: R >--> S,
::::::::: addemb(f,x,y): R x R -> (S\ rng f) \/ R
:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
definition
let R be Ring, 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:
(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
proof
set AddR = the addF of R;
set AddS = the addF of S;
thus (a in [#]R & b in [#]R) implies AddR.(a,b) is Element of carr f
proof
assume a in [#]R & b in [#]R; then
reconsider x = a, y = b as Element of [#]R;
AddR.(x,y) in ([#]S \ rng f) \/ [#]R by XBOOLE_0:def 3;
hence thesis;
end;
(a in [#]R & not b in [#]R) implies AddS.(f.a,b) in [#]S\rng f by Lm3;
hence (a in [#]R & not b in [#]R) implies AddS.(f.a,b) is Element of carr f
by XBOOLE_0:def 3;
(b in [#]R & not a in [#]R) implies AddS.(a,f.b) in ([#]S)\(rng f) by Lm2;
hence (b in [#]R & not a in [#]R) implies
AddS.(a,f.b) is Element of carr f by XBOOLE_0:def 3;
thus (not a in [#]R & not b in [#]R & AddS.(a,b) in rng f)
implies f".(AddS.(a,b)) is Element of carr f
proof
assume
B1: not a in [#]R & not b in [#]R & AddS.(a,b) in rng f;
B2: rng(f") = dom f by FUNCT_1:33 .= [#]R by FUNCT_2:def 1;
AddS.(a,b) in dom(f") by B1,FUNCT_1:33; then
f".(AddS.(a,b)) in [#]R by B2,FUNCT_1:3;
hence thesis by XBOOLE_0:def 3;
end;
(not a in [#]R & not b in [#]R & not AddS.(a,b) in rng f)
implies AddS.(a,b) is Element of carr f
proof
assume
A1: not a in [#]R & not b in [#]R & not AddS.(a,b) in rng f; then
a in ([#]S)\(rng f) & b in ([#]S)\(rng f) by XBOOLE_0:def 3; then
reconsider a1 = a, b1 = b as Element of [#]S;
AddS.(a1,b1) in ([#]S)\(rng f) by A1,XBOOLE_0:def 5;
hence AddS.(a,b) is Element of carr f by XBOOLE_0:def 3;
end;
hence thesis;
end;
consistency;
end;
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:
for a,b being Element of carr f holds it.(a,b) = addemb(f,a,b);
existence
proof
deffunc O(Element of carr f,Element of carr f) = addemb(f,$1,$2);
consider F being BinOp of carr f such that
A1: for a,b being Element of carr f holds F.(a,b)=O(a,b) from BINOP_1:sch 4;
take F;
thus thesis by A1;
end;
uniqueness
proof
let F1,F2 be BinOp of carr f such that
A2: for a,b being Element of carr f holds F1.(a,b) = addemb(f,a,b) and
A3: for a,b being Element of carr f holds F2.(a,b) = addemb(f,a,b);
now let a,b be Element of carr f;
thus F1.(a,b) = addemb(f,a,b) by A2 .= F2.(a,b) by A3;
end;
hence thesis by BINOP_1:2;
end;
end;
definition
let K be Field, 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:
(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
proof
thus
(a in [#]K & b in [#]K) implies (the multF of K).(a,b) is Element of carr f
proof
assume a in [#]K & b in [#]K; then
reconsider x = a, y = b as Element of [#]K;
(the multF of K).(x,y) in ([#]T \ rng f) \/ [#]K by XBOOLE_0:def 3;
hence thesis;
end;
thus (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) in [#]T \ rng f by Lm5;
hence (a in [#]K & a <> 0.K & not b in [#]K)
implies (the multF of T).(f.a,b) is Element of carr f by XBOOLE_0:def 3;
(b in [#]K & b <> 0.K & not a in [#]K)
implies (the multF of T).(a,f.b) in [#]T \ rng f by Lm4;
hence (b in [#]K & b <> 0.K & not a in [#]K)
implies (the multF of T).(a,f.b) is Element of carr f by XBOOLE_0:def 3;
thus
(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
proof
assume
A1: not a in [#]K & not b in [#]K & (the multF of T).(a,b) in rng f;
A2: rng(f") = dom f by FUNCT_1:33 .= [#]K by FUNCT_2:def 1;
(the multF of T).(a,b) in dom(f") by A1,FUNCT_1:33; then
f".((the multF of T).(a,b)) in [#]K by A2,FUNCT_1:3;
hence thesis by XBOOLE_0:def 3;
end;
(not a in [#]K & not b in [#]K & not (the multF of T).(a,b) in rng f)
implies (the multF of T).(a,b) is Element of carr f
proof
assume
A3: not a in [#]K & not b in [#]K & not (the multF of T).(a,b) in rng f; then
a in [#]T \ rng f & b in [#]T \ rng f by XBOOLE_0:def 3; then
reconsider a1 = a, b1 = b as Element of [#]T;
(the multF of T).(a1,b1) in ([#]T)\ rng f by A3,XBOOLE_0:def 5;
hence (the multF of T).(a,b) is Element of carr f by XBOOLE_0:def 3;
end;
hence thesis;
end;
consistency
proof
let x be Element of carr f;
now assume
A1: a in [#]K & b in [#]K & (a = 0.K or b = 0.K);
then reconsider a1 = a, b1 = b as Element of K;
per cases by A1;
suppose a = 0.K; then
0.K = a1 * b1 .= (the multF of K).(a,b);
hence (x = (the multF of K).(a,b) iff x = 0.K);
end;
suppose b = 0.K; then
0.K = a1 * b1 .= (the multF of K).(a,b);
hence (x = (the multF of K).(a,b) iff x = 0.K);
end;
end;
hence thesis;
end;
end;
definition
let K be Field, T be K-monomorphic comRing;
let f be Monomorphism of K,T;
func multemb f -> BinOp of carr f means :defmult:
for a,b being Element of carr f holds it.(a,b) = multemb(f,a,b);
existence
proof
deffunc O(Element of carr f,Element of carr f) = multemb(f,$1,$2);
consider F being BinOp of carr f such that
A1: for a,b being Element of carr f holds F.(a,b)=O(a,b) from BINOP_1:sch 4;
take F;
thus thesis by A1;
end;
uniqueness
proof
let F1,F2 be BinOp of carr f such that
A2: for a,b being Element of carr f holds F1.(a,b) = multemb(f,a,b) and
A3: for a,b being Element of carr f holds F2.(a,b) = multemb(f,a,b);
now let a,b be Element of carr f;
thus F1.(a,b) = multemb(f,a,b) by A2 .= F2.(a,b) by A3;
end;
hence thesis by BINOP_1:2;
end;
end;
definition
let K be Field, T be K-monomorphic comRing;
let f be Monomorphism of K,T;
func embField f -> strict doubleLoopStr means :defemb:
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
proof
reconsider e = 1.K, o = 0.K as Element of carr f by XBOOLE_0:def 3;
take doubleLoopStr (# carr f,addemb f, multemb f,e,o #);
thus thesis;
end;
uniqueness;
end;
registration
let K be Field,
T be K-monomorphic comRing;
let f be Monomorphism of K,T;
cluster embField f -> non degenerated;
coherence
proof
0.(embField f) = 0.K & 1.(embField f) = 1.K by defemb;
hence thesis;
end;
end;
Lm6:
for f being Monomorphism of K,T st K,T are_disjoint
for a,b being Element of embField f st a in [#]K & not b in [#]K
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
let f be Monomorphism of K,T;
assume
A1: K,T are_disjoint;
let a,b be Element of embField f;
assume
A2: a in [#]K & not b in [#]K;
let a1, b1 be Element of carr f;
assume
A3: a1 = a & b1 = b;
thus
A4: a + b = (addemb f).(a,b) by defemb .= addemb(f,a1,b1) by defadd,A3
.= (the addF of T).(f.a1,b1) by A2,A3,defaddf;
thus
A5: b + a = (addemb f).(b,a) by defemb .= addemb(f,b1,a1) by defadd,A3
.= (the addF of T).(b1,f.a1) by A3,A2,defaddf;
(the addF of T).(f.a1,b1) in ([#]T) \ (rng f) by A2,A3,Lm3;
hence not a + b in [#]K by A1,A4,XBOOLE_0:def 4;
(the addF of T).(b1,f.a1) in ([#]T) \ (rng f) by A3,A2,Lm2;
hence not b + a in [#]K by A1,A5,XBOOLE_0:def 4;
end;
Lm7:
for f being Monomorphism of K,T, a,b being Element of embField f,
a1,b1 being Element of K st a1 = a & b1 = b
holds a + b = a1 + b1 & b + a = b1 + a1
proof
let f be Monomorphism of K,T,a,b be Element of embField f,
a1,b1 be Element of K;
assume
A1: a1 = a & b1 = b;
reconsider ac = a, bc = b as Element of carr f by defemb;
thus a + b = (addemb f).(a,b) by defemb .= addemb(f,ac,bc) by defadd
.= a1 + b1 by A1,defaddf;
thus b + a = (addemb f).(b,a) by defemb .= addemb(f,bc,ac) by defadd
.= b1 + a1 by A1,defaddf;
end;
Lm8:
for f being Monomorphism of K,T,a,b being Element of embField f,
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
let f be Monomorphism of K,T,a,b be Element of embField f,
a1,b1 be Element of T;
assume
AS1: 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;
reconsider ac = a, bc = b as Element of carr f by defemb;
thus
D: a+b = (addemb f).(a,b) by defemb .= addemb(f,ac,bc) by defadd
.= a1 + b1 by AS1,defaddf;
C: (the addF of T).(a1,b1) = a1+b1 .= b1+a1 .= (the addF of T).(b1,a1);
thus
E: b+a = (addemb f).(b,a) by defemb .= addemb(f,bc,ac) by defadd
.= b1+a1 by C,AS1,defaddf;
thus not a + b in [#]K by D,AS1,XBOOLE_0:def 4;
thus not b + a in [#]K by E,AS1,XBOOLE_0:def 4;
end;
Lm9:
for f being Monomorphism of K,T,a,b being Element of embField f,
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
let f be Monomorphism of K,T,a,b be Element of embField f,
a1,b1 be Element of T;
assume
AS: not a in [#]K & not b in [#]K & (the addF of T).(a,b) in rng f &
a1 = a & b1 = b;
reconsider ac = a, bc = b as Element of carr f by defemb;
thus
D: a + b = (addemb f).(a,b) by defemb .= addemb(f,ac,bc) by defadd
.= f".(a1 + b1) by AS,defaddf;
C: (the addF of T).(a1,b1) = a1 + b1 .= b1 + a1 .= (the addF of T).(b1,a1);
thus
E: b + a = (addemb f).(b,a) by defemb .= addemb(f,bc,ac) by defadd
.= f".(b1 + a1) by C,AS,defaddf;
a1 + b1 in dom(f") by AS,FUNCT_1:33; then
F: f".(a1 + b1) in rng(f") by FUNCT_1:def 3;
hence a + b in [#]K by D;
thus b + a in [#]K by E,F;
end;
Lm10:
for f being Monomorphism of K,T, a,b being Element of embField f,
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
let f be Monomorphism of K,T, a,b be Element of embField f,
a1,b1 be Element of carr f;
assume
AS: K,T are_disjoint & a in [#]K & a <>0.K & not b in [#]K & a1 = a & b1 = b;
thus
C1: a*b = (multemb f).(a,b) by defemb .= multemb(f,a1,b1) by defmult,AS
.= (the multF of T).(f.a1,b1) by AS,defmultf;
thus
D1: b*a = (multemb f).(b,a) by defemb .= multemb(f,b1,a1) by defmult,AS
.= (the multF of T).(b1,f.a1) by AS,defmultf;
(the multF of T).(f.a1,b1) in ([#]T) \ (rng f) by AS,Lm5;
hence not a * b in [#]K by AS,C1,XBOOLE_0:def 4;
(the multF of T).(b1,f.a1) in ([#]T) \ (rng f) by AS,Lm4;
hence not b * a in [#]K by AS,D1,XBOOLE_0:def 4;
end;
Lm11:
for f being Monomorphism of K,T,a,b being Element of embField f,
a1,b1 being Element of K st a1 = a & b1 = b holds a*b = a1*b1 & b*a = b1*a1
proof
let f be Monomorphism of K,T,a,b be Element of embField f,
a1,b1 be Element of K;
assume
B1: a1 = a & b1 = b;
reconsider ac = a, bc = b as Element of carr f by defemb;
thus a * b = (multemb f).(a,b) by defemb .= multemb(f,ac,bc) by defmult
.= a1 * b1 by B1,defmultf;
thus b * a = (multemb f).(b,a) by defemb .= multemb(f,bc,ac) by defmult
.= b1 * a1 by B1,defmultf;
end;
Lm12:
for f being Monomorphism of K,T,a,b being Element of embField f,
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
let f be Monomorphism of K,T,a,b be Element of embField f,
a1,b1 be Element of T;
assume
AS: 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; then
B1: a <> 0.K & b <> 0.K;
reconsider ac = a, bc = b as Element of carr f by defemb;
thus
D1: a*b = (multemb f).(a,b) by defemb .= multemb(f,ac,bc) by defmult
.= a1 * b1 by B1,AS,defmultf;
C1: (the multF of T).(a1,b1) = a1 * b1 .= b1 * a1 by GROUP_1:def 12
.= (the multF of T).(b1,a1);
thus b*a = (multemb f).(b,a) by defemb .= multemb(f,bc,ac) by defmult
.= b1 * a1 by B1,C1,AS,defmultf;
hence not a*b in [#]K & not b*a in [#]K by D1,AS,XBOOLE_0:def 4;
end;
Lm13:
for f being Monomorphism of K,T,a,b being Element of embField f,
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
let f be Monomorphism of K,T,a,b be Element of embField f,
a1,b1 be Element of T;
assume
AS: not a in [#]K & not b in [#]K & (the multF of T).(a,b) in rng f &
a1 = a & b1 = b;
reconsider ac = a, bc = b as Element of carr f by defemb;
thus
D1: a*b = (multemb f).(a,b) by defemb .= multemb(f,ac,bc) by defmult
.= f".(a1 * b1) by AS,defmultf;
C1: (the multF of T).(a1,b1) = a1*b1 .= b1*a1 by GROUP_1:def 12
.= (the multF of T).(b1,a1);
thus
E1: b*a = (multemb f).(b,a) by defemb .= multemb(f,bc,ac) by defmult
.= f".(b1 * a1) by C1,AS,defmultf;
a1*b1 in dom(f") by AS,FUNCT_1:33; then
G1: f".(a1*b1) in rng(f") by FUNCT_1:def 3;
hence a*b in [#]K by D1;
f".(a1*b1) in dom f by G1,FUNCT_1:33; then
f".(b1*a1) in dom f by GROUP_1:def 12;
hence b*a in [#]K by E1;
end;
registration
let K be Field,
T be K-monomorphic comRing;
let f be Monomorphism of K,T;
cluster embField f -> Abelian right_zeroed;
coherence
proof
thus embField f is Abelian
proof
now let a,b be Element of embField f;
reconsider x = a, y = b as Element of carr f by defemb;
per cases;
suppose x in [#]K & y in [#]K; then
reconsider a1 = a, b1 = b as Element of K;
thus a + b = a1 + b1 by Lm7 .= b + a by Lm7;
end;
suppose
A2: x in [#]K & not y in [#]K; then
reconsider a1 = a as Element of K;
reconsider b1 = b as Element of T by A2,Lm1;
reconsider fa = f.a1 as Element of T;
thus a + b = (addemb f).(x,y) by defemb .= addemb(f,x,y) by defadd
.= fa + b1 by A2,defaddf .= b1 + fa
.= addemb(f,y,x) by A2,defaddf .= (addemb f).(y,x) by defadd
.= b + a by defemb;
end;
suppose
A3: y in [#]K & not x in [#]K; then
reconsider b1 = b as Element of K;
reconsider a1 = a as Element of T by A3,Lm1;
reconsider fb = f.b1 as Element of T;
thus a + b = (addemb f).(x,y) by defemb .= addemb(f,x,y) by defadd
.= a1+fb by A3,defaddf .= fb+a1 .= addemb(f,y,x) by A3,defaddf
.= (addemb f).(y,x) by defadd .= b + a by defemb;
end;
suppose
A4: not x in [#]K & not y in [#]K & (the addF of T).(x,y) in rng f; then
reconsider a1 = a, b1 = b as Element of T by Lm1;
B1: (the addF of T).(a,b) = a1+b1 .= b1+a1 .= (the addF of T).(b,a);
thus a+b = (addemb f).(x,y) by defemb .= addemb(f,x,y) by defadd
.= (f").(a1+b1) by A4,defaddf .= addemb(f,y,x) by A4,B1,defaddf
.= (addemb f).(y,x) by defadd .= b+a by defemb;
end;
suppose
A5: not x in [#]K & not y in [#]K & not (the addF of T).(x,y) in rng f;
then reconsider a1 = a, b1 = b as Element of T by Lm1;
B2: (the addF of T).(a,b) = a1+b1 .= b1+a1 .= (the addF of T).(b,a);
thus a+b = (addemb f).(x,y) by defemb .= addemb(f,x,y) by defadd
.= a1+b1 by A5,defaddf .= addemb(f,y,x) by A5,B2,defaddf
.= (addemb f).(y,x) by defadd .= b + a by defemb;
end;
end;
hence thesis;
end;
now let a be Element of embField f;
reconsider x = a as Element of carr f by defemb;
reconsider o = 0.(embField f) as Element of carr f by defemb;
B1: a+0.(embField f) = (addemb f).(x,o) by defemb .= addemb(f,x,o) by defadd;
C1: 0.(embField f) = 0.K by defemb;
per cases;
suppose x in [#]K; then
reconsider a1 = a as Element of K;
addemb(f,x,o) = a1+0.K by C1,defaddf;
hence a+0.(embField f) = a by B1;
end;
suppose
A1: not x in [#]K; then
reconsider a1 = a as Element of T by Lm1;
addemb(f,x,o) = (the addF of T).(a,f.o) by A1,C1,defaddf
.= a1+0.T by C1,RING_2:6;
hence a+0.(embField f) = a by B1;
end;
end;
hence thesis;
end;
end;
theorem Th6:
for f being Monomorphism of K,T st K,T are_disjoint
holds embField f is add-associative
proof
let f be Monomorphism of K,T;
assume
AS: K,T are_disjoint;
now let a,b,c be Element of embField f;
reconsider x = a, y = b, z = c as Element of carr f by defemb;
per cases;
suppose
X: x in [#]K; then
reconsider a1 = a as Element of K;
per cases;
suppose
Y: y in [#]K; then
reconsider b1 = b as Element of K;
X0: a + b = a1 + b1 by Lm7; then
reconsider ab = a + b as Element of carr f by XBOOLE_0:def 3;
per cases;
suppose z in [#]K; then
reconsider c1 = c as Element of K;
X1: b + c = b1 + c1 by Lm7; then
reconsider bc = b + c as Element of carr f by XBOOLE_0:def 3;
thus (a+b)+c = (addemb f).(a+b,z) by defemb
.= addemb(f,ab,z) by defadd .= (a1+b1)+c1 by X0,defaddf
.= a1+(b1+c1) by RLVECT_1:def 3
.= addemb(f,x,bc) by X1,defaddf
.= (addemb f).(x,b+c) by defadd .= a + (b + c) by defemb;
end;
suppose
Z: not z in [#]K; then
reconsider c1 = c as Element of T by Lm1;
reconsider bc = b + c as Element of carr f by defemb;
reconsider fa = f.a1, fb = f.b1 as Element of T;
X1: f.(a1+b1) = fa + fb by VECTSP_1:def 20;
X2: b + c = fb + c1 by AS,Y,Z,Lm6;
X3: not fb + c1 in [#]K by AS,XBOOLE_0:def 4;
thus (a+b)+c = (addemb f).(a+b,z) by defemb
.= addemb(f,ab,z) by defadd .=(fa + fb)+c1 by X1,X0,defaddf,Z
.= fa+(fb+c1) by RLVECT_1:def 3
.=addemb(f,x,bc) by X3,X2,defaddf
.= (addemb f).(x,b+c) by defadd .= a + (b + c) by defemb;
end;
end;
suppose
Y: not y in [#]K; then
reconsider b1 = b as Element of T by Lm1;
reconsider fa = f.a1 as Element of T;
X0: a + b = fa + b1 by AS,X,Y,Lm6;
then reconsider ab = fa + b1 as Element of carr f by defemb;
X1: not ab in [#]K by AS,XBOOLE_0:def 4;
per cases;
suppose Z: z in [#]K; then
reconsider c1 = c as Element of K;
reconsider fc = f.c1 as Element of T;
X2: b + c = b1 + fc by AS,Y,Z,Lm6;
then reconsider bc = b1 + fc as Element of carr f by defemb;
X3: not bc in [#]K by AS,XBOOLE_0:def 4;
thus (a + b) + c = (addemb f).(ab,z) by X0,defemb
.= addemb(f,ab,z) by defadd.= (fa + b1) + fc by X1,defaddf
.= fa+(b1+fc) by RLVECT_1:def 3
.= addemb(f,x,bc) by X3,defaddf
.= (addemb f).(x,bc) by defadd .=a +(b + c) by X2,defemb;
end;
suppose
Z: not z in [#]K; then
reconsider c1 = c as Element of T by Lm1;
reconsider fa1 = f.a1 as Element of (rng f) by FUNCT_2:4;
K5: (the addF of T).(ab,z) = (fa+b1)+c1
.= fa+(b1+c1) by RLVECT_1:def 3;
per cases;
suppose
K: (the addF of T).(ab,z) in rng f;
X2: (a+b)+c = (addemb f).(ab,z) by X0,defemb
.= addemb(f,ab,z) by defadd
.= f".((fa+b1)+c1) by X1,Z,defaddf,K
.= f".(fa + (b1+c1)) by RLVECT_1:def 3;
K1: now assume
K7: not (the addF of T).(y,z) in rng f;
X4: not (the addF of T).(b1,c1) in [#]K
by AS,XBOOLE_0:def 4;
X3: b + c = b1 + c1 by AS,K7,Y,Z,Lm8;
b1+c1 in ([#]T) \ rng f by K7,XBOOLE_0:def 5;then
reconsider bc1 = b1+c1 as Element of carr f by XBOOLE_0:def 3;
reconsider bce = bc1 as Element of embField f by X3;
(the addF of T).(f.a,bce) in [#]T\rng f by X,X4,Lm3;
hence contradiction by K5,K,XBOOLE_0:def 5;
end; then
X3: b + c = f".(b1+c1) by Y,Z,Lm9;
f".(b1+c1) in [#]K by K1,FUNCT_2:5; then
reconsider bc = f".(b1+c1) as Element of carr f by XBOOLE_0:def 3;
reconsider bc1 = b1+c1 as Element of rng f by K1;
thus (a+b)+c = f".fa1+f".bc1 by Th1,X2
.= a1+f".bc1 by FUNCT_2:26
.= addemb(f,x,bc) by defaddf
.= (addemb f).(x,bc) by defadd
.= a + (b + c) by X3,defemb;
end;
suppose
K0: not (the addF of T).(ab,z) in rng f;
X2: (a+b)+c = (addemb f).(ab,z) by X0,defemb
.= addemb(f,ab,z) by defadd
.= (fa+b1)+c1 by X1,Z,defaddf,K0
.= fa+(b1+c1) by RLVECT_1:def 3;
K1: now assume
K7: (the addF of T).(y,z) in rng f;
X7: dom f = [#]K by FUNCT_2:def 1;
consider x being object such that
X6: x in dom f & b1+c1 = f.x by K7,FUNCT_1:def 3;
reconsider xx = x as Element of K by X6;
f.(a1+xx) = fa + (b1 + c1) by X6,VECTSP_1:def 20;
hence contradiction by K5,K0,X7,FUNCT_1:3;
end; then
b1 + c1 in [#]T \ rng f by XBOOLE_0:def 5; then
reconsider bc=b1 + c1 as Element of carr f by XBOOLE_0:def 3;
X3: b + c = b1 + c1 by AS,Y,Z,K1,Lm8;
not b1 + c1 in [#]K by AS,XBOOLE_0:def 4;
hence
(a + b) + c = addemb(f,x,bc) by X2,defaddf
.= (addemb f).(x,bc) by defadd .= a+(b+c) by X3,defemb;
end;
end;
end;
end;
suppose
X4: not x in [#]K; then
reconsider a1 = a as Element of T by Lm1;
per cases;
suppose
Y0: y in [#]K; then
reconsider b1 = b as Element of K;
X0: a + b = a1 + f.b1 by AS,X4,Y0,Lm6;
reconsider ab = a + b as Element of carr f by defemb;
reconsider fb = f.b1 as Element of T;
X2: not ab in [#]K by AS,X4,Y0,Lm6;
per cases;
suppose z in [#]K; then
reconsider c1 = c as Element of K;
reconsider fc = f.c1 as Element of T;
X3: b+c = b1+c1 by Lm7; then
reconsider bc = b+c as Element of carr f by XBOOLE_0:def 3;
thus (a+b)+c = (addemb f).(ab,z) by defemb
.= addemb(f,ab,z) by defadd
.= (a1+fb)+fc by X0,X2,defaddf
.= a1+(fb+fc) by RLVECT_1:def 3
.= a1+f.(b1+c1) by VECTSP_1:def 20
.= addemb(f,x,bc) by defaddf,X3,X4
.= (addemb f).(x,bc) by defadd
.= a + (b + c) by defemb;
end;
suppose Z0: not z in [#]K; then
reconsider c1 = c as Element of T by Lm1;
X3: b + c = f.b1 + c1 by AS,Y0,Z0,Lm6;
reconsider bc = b + c as Element of carr f by defemb;
X5: not b+c in [#]K by AS,Y0,Z0,Lm6;
K5: (the addF of T).(ab,z) = (a1+fb)+c1 by AS,X4,Y0,Lm6
.= a1+(fb+c1) by RLVECT_1:def 3
.= (the addF of T).(x,bc) by AS,Y0,Z0,Lm6;
per cases;
suppose K0: not (the addF of T).(ab,z) in rng f;
thus (a+b)+c = (addemb f).(ab,z) by defemb
.= addemb(f,ab,z) by defadd
.= (a1+fb)+c1 by X0,K0,X2,Z0,defaddf
.= a1+(fb+c1) by RLVECT_1:def 3
.= addemb(f,x,bc) by K0,K5,X3,X4,X5,defaddf
.= (addemb f).(x,bc) by defadd
.= a + (b + c) by defemb;
end;
suppose K1: (the addF of T).(ab,z) in rng f;
thus (a+b)+c = (addemb f).(ab,z) by defemb
.= addemb(f,ab,z) by defadd
.= (f").((the addF of T).(ab,z))
by K1,X2,Z0,defaddf
.= addemb(f,x,bc) by K1,K5,X4,X5,defaddf
.= (addemb f).(x,bc) by defadd
.= a + (b + c) by defemb;
end;
end;
end;
suppose Y0: not y in [#]K; then
reconsider b1 = b as Element of T by Lm1;
per cases;
suppose K2: not (the addF of T).(x,y) in rng f;
K1: not (the addF of T).(a1,b1) in [#]K
by AS,XBOOLE_0:def 4;
X0: a + b = a1 + b1 by K2,Y0,X4,AS,Lm8;
a1 + b1 in [#]T \ rng f by K2,XBOOLE_0:def 5; then
reconsider ab = a1 + b1 as Element of carr f by XBOOLE_0:def 3;
D: not ab in [#]K by AS,XBOOLE_0:def 4;
per cases;
suppose
Z: z in [#]K; then
reconsider c1 = c as Element of K;
X1: b + c = b1 + f.c1 by AS,Y0,Z,Lm6;
[#]embField f = carr f by defemb; then
X3: b1 + f.c1 in ([#]T)\(rng f) by Y0,Lm2;
X2: not b1 + f.c1 in [#]K by AS,XBOOLE_0:def 4;
reconsider bc = b1 + f.c1 as Element of carr f by X3,XBOOLE_0:def 3;
X4a: (a+b)+c = (addemb f).(ab,z) by X0,defemb
.= addemb(f,ab,z) by defadd
.= (a1+b1)+f.c1 by K1,defaddf
.= a1+(b1+f.c1) by RLVECT_1:def 3;
X5: (the addF of T).(x,bc) = a1+(b1+f.c1)
.= (a1+b1)+f.c1 by RLVECT_1:def 3
.= (the addF of T).(ab,f.z);
(the addF of T).(ab,f.z) in [#]T \ rng f
by D,Lm2,Z; then
not (the addF of T).(x,bc) in rng f
by X5,XBOOLE_0:def 5;
hence (a+b)+c = addemb(f,x,bc)
by X4,X2,X4a,defaddf
.= (addemb f).(x,bc) by defadd
.= a+(b+c) by X1,defemb;
end;
suppose Z: not z in [#]K; then
reconsider c1 = c as Element of T by Lm1;
K5: (the addF of T).(ab,z) = (a1+b1)+c1
.= a1+(b1+c1) by RLVECT_1:def 3
.= (the addF of T).(a1,b1 + c1);
per cases;
suppose K:not(the addF of T).(ab,z) in rng f;
per cases;
suppose K6:not(the addF of T).(b1,c1)
in rng f;
then X1: b+c = b1+c1 by AS,Y0,Z,Lm8;
K9: (the addF of T).(b1,c1) in [#]T \ rng f
by K6,XBOOLE_0:def 5;
K8: not b1+c1 in [#]K by AS,XBOOLE_0:def 4;
reconsider bc = b1+c1 as Element of carr f by K9,XBOOLE_0:def 3;
thus (a+b)+c = (addemb f).(ab,z)
by X0,defemb
.= addemb(f,ab,z) by defadd
.= (a1+b1)+c1 by D,Z,defaddf,K
.= addemb(f,x,bc) by X4,K5,K,K8,defaddf
.= (addemb f).(x,bc) by defadd
.= a+(b+c) by X1,defemb;
end;
suppose K6:(the addF of T).(b1,c1)
in rng f; then
X1: b+c = f".(b1+c1) by Y0,Z,Lm9;
b1+c1 in dom(f") by K6,FUNCT_1:33; then
f".(b1+c1) in rng(f") by FUNCT_1:3;then
reconsider bc1 = f".(b1+c1) as Element of [#]K;
reconsider bc = bc1 as Element of carr f by XBOOLE_0:def 3;
thus
(a + b) + c = (addemb f).(ab,z)
by X0,defemb
.= addemb(f,ab,z) by defadd
.= (a1+b1)+c1 by D,Z,defaddf,K
.= a1+(b1+c1) by RLVECT_1:def 3
.= a1 + f.bc1 by K6,FUNCT_1:35
.= addemb(f,x,bc) by X4,defaddf
.= (addemb f).(x,bc) by defadd
.= a + (b + c) by X1,defemb;
end;
end;
suppose K7:(the addF of T).(ab,z) in rng f;
K6: now assume (the addF of T).(b1,c1)
in rng f; then
consider x being object such that
H1: x in dom f & f.x=b1 + c1
by FUNCT_1:def 3;
consider y being object such that
H2: y in dom f & f.y = (a1 + b1) + c1
by K7,FUNCT_1:def 3;
reconsider xx = x, yy = y as Element of K by H1,H2;
X1: f.(yy-xx) = f.yy - f.xx by RING_2:8
.= (a1+(b1+c1))-(b1+c1)
by H1,H2,RLVECT_1:def 3
.= a1+((b1+c1)+-(b1+c1))
by RLVECT_1:def 3
.= a1+0.T by RLVECT_1:5;
dom f = [#]K by FUNCT_2:def 1; then
a1 in rng f by X1,FUNCT_1:def 3;
hence contradiction by X4,Lm1;
end; then
X1: b + c = b1 + c1 by AS,Y0,Z,Lm8;
b1 + c1 in [#]T\rng f
by K6,XBOOLE_0:def 5; then
reconsider bc=b1 + c1 as Element of carr f by XBOOLE_0:def 3;
K9: not bc in [#]K by AS,XBOOLE_0:def 4;
thus
(a+b)+c = (addemb f).(ab,z) by X0,defemb
.= addemb(f,ab,z) by defadd
.= f".((a1+b1)+c1) by D,Z,defaddf,K7
.= addemb(f,x,bc) by X4,K5,K7,defaddf,K9
.= (addemb f).(x,bc) by defadd
.= a+(b+c) by X1,defemb;
end;
end;
end;
suppose L:(the addF of T).(x,y) in rng f; then
Z1: a + b = f".(a1 + b1) by X4,Y0,Lm9;
a1 + b1 in dom(f") by L,FUNCT_1:33; then
f".(a1 + b1) in rng(f") by FUNCT_1:3; then
reconsider ab1 = f".(a1 + b1) as Element of [#]K;
reconsider ab = ab1 as Element of carr f by XBOOLE_0:def 3;
per cases;
suppose Z: z in [#]K; then
reconsider c1 = c as Element of K;
Z2: b + c = b1 + f.c1 by AS,Y0,Z,Lm6; then
L0: b + c in ([#]T) \ (rng f) by Lm2,Y0,Z;
reconsider bc1 = b1 + f.c1 as Element of T;
reconsider bc=bc1 as Element of carr f by Z2,L0,XBOOLE_0:def 3;
Z3: (a+b)+c = (addemb f).(ab,z) by Z1,defemb
.=addemb(f,ab,z) by defadd
.= ab1 + c1 by defaddf;
Z4: not bc in [#]K by AS,XBOOLE_0:def 4;
Z9: dom f=[#]K &(rng f) c= [#]T
by FUNCT_2:def 1;
L2: dom f = [#]K by FUNCT_2:def 1; then
reconsider fc1 = f.c1 as Element of rng f by FUNCT_1:def 3;
reconsider ffc1 = f".fc1 as Element of K;
f".fc1 = c1 by L2,FUNCT_1:34; then
Z5: f".((a1 + b1) + fc1) = ab1 + c1 by L,Th1;
consider x1 being object such that
Z6: x1 in dom f & f.x1 = a1 + b1
by L,FUNCT_1:def 3;
reconsider xx = x1 as Element of K by Z6;
f.(xx + c1) = (a1 + b1) + f.c1
by Z6,VECTSP_1:def 20; then
(a1 + b1)+f.c1 in rng f
by Z9,FUNCT_1:def 3; then
L1: a1 + (b1 + f.c1) in rng f
by RLVECT_1:def 3;
thus
a+(b+c) = (addemb f).(x,bc) by Z2,defemb
.= addemb(f,x,bc) by defadd
.= f".(a1+bc1) by L1,Z4,X4,defaddf
.= (a+b)+c by Z3,Z5,RLVECT_1:def 3;
end;
suppose Z: not z in [#]K; then
reconsider c1 = c as Element of T by Lm1;
Z2: (a+b)+c = (addemb f).(ab,z) by Z1,defemb
.= addemb(f,ab,z) by defadd
.= f.ab1 + c1 by Z,defaddf
.= (a1+b1)+c1 by L,FUNCT_1:35
.= a1+(b1+c1) by RLVECT_1:def 3;
(the addF of T).(f.ab,z) in [#]T\rng f
by Z,Lm3; then
(a1 + b1) + c1 in [#]T\rng f
by FUNCT_1:35,L; then
a1+(b1+c1) in [#]T\rng f
by RLVECT_1:def 3; then
U2: not(the addF of T).(a,b1+c1) in (rng f)
by XBOOLE_0:def 5;
per cases;
suppose L1:not(the addF of T).(y,z)
in rng f; then
X3: b + c = b1 + c1 by AS,Y0,Z,Lm8;
X4a: b1+c1 in [#]T\rng f
by L1,XBOOLE_0:def 5;
reconsider bc1 = b1 + c1 as Element of T;
reconsider bc = bc1 as Element of carr f by X4a,XBOOLE_0:def 3;
not bc in [#]K by AS,XBOOLE_0:def 4;
hence (a + b) + c = addemb(f,x,bc)
by Z2,U2,X4,defaddf
.= (addemb f).(x,bc) by defadd
.= a + (b + c) by X3,defemb;
end;
suppose K6:(the addF of T).(y,z)
in rng f; then
X1: b + c = f".(b1 + c1) by Y0,Z,Lm9;
b1 + c1 in dom(f") by K6,FUNCT_1:33;
then
f".(b1 + c1) in rng(f") by FUNCT_1:3;
then
reconsider bc1 = f".(b1 + c1) as Element of [#]K;
reconsider bc = bc1 as Element of carr f by XBOOLE_0:def 3;
thus (a+b)+c = a1+f.bc1
by Z2,K6,FUNCT_1:35
.= addemb(f,x,bc) by X4,defaddf
.= (addemb f).(x,bc) by defadd
.= a+(b+c) by X1,defemb;
end;
end;
end;
end;
end;
end;
hence thesis;
end;
theorem Th7:
for f being Monomorphism of K,T st K,T are_disjoint
holds embField f is right_complementable
proof
let f be Monomorphism of K,T;
assume
AS: K,T are_disjoint;
now let a be Element of embField f;
reconsider x = a as Element of carr f by defemb;
per cases;
suppose x in [#]K; then
reconsider a1 = a as Element of K;
a1 is right_complementable; then
consider b1 being Element of K such that
B1: a1 + b1 = 0.K;
reconsider y = b1 as Element of carr f by XBOOLE_0:def 3;
reconsider b = y as Element of embField f by defemb;
a + b = a1 + b1 by Lm7 .= 0.(embField f) by B1,defemb;
hence a is right_complementable;
end;
suppose
A2: not x in [#]K; then
reconsider a1 = a as Element of T by Lm1;
a1 is right_complementable; then
consider b1 being Element of T such that
B2: a1 + b1 = 0.T;
dom f = [#]K &
(the addF of T).(a1,b1) = f.(0.K) by B2,RING_2:6,FUNCT_2:def 1; then
D0: (the addF of T).(a1,b1) in rng f by FUNCT_1:3; then
D1: not (the addF of T).(a1,b1) in [#]T \ rng f by XBOOLE_0:def 5;
per cases;
suppose b1 in rng f; then
consider b1r being object such that
C1: b1r in dom f & f.b1r = b1 by FUNCT_1:def 3;
reconsider b1r as Element of K by C1;
[#]embField f = carr f by defemb; then
reconsider bx = b1r as Element of embField f by XBOOLE_0:def 3;
reconsider y = bx as Element of carr f by defemb;
C2: [#]embField f = carr f by defemb; then
(the addF of T).(a1,f.bx) in [#]K by Lm2,A2,D1,C1;
hence a is right_complementable by Lm2,A2,D1,C1,C2;
end;
suppose not b1 in rng f;
then b1 in [#]T \ rng f by XBOOLE_0:def 5; then
reconsider y = b1 as Element of carr f by XBOOLE_0:def 3;
reconsider b = y as Element of embField f by defemb;
E1: not b in [#]K by AS,XBOOLE_0:def 4;
Y1: dom f = [#]K & f.(0.K) = 0.T by RING_2:6,FUNCT_2:def 1;
a + b = f".(0.T) by A2,B2,D0,E1,Lm9
.= 0.K by Y1,FUNCT_1:32 .= 0.(embField f) by defemb;
hence a is right_complementable;
end;
end;
end;
hence thesis;
end;
registration
let K be Field,
T be K-monomorphic comRing;
let f be Monomorphism of K,T;
cluster embField f -> commutative well-unital;
coherence
proof
thus embField f is commutative
proof
now let a,b be Element of embField f;
reconsider x = a, y = b as Element of carr f by defemb;
per cases;
suppose x in [#]K & y in [#]K; then
reconsider a1 = a, b1 = b as Element of K;
thus a*b = a1*b1 by Lm11 .= b1*a1 by GROUP_1:def 12 .= b * a by Lm11;
end;
suppose A: a = 0.K or b = 0.K;
per cases by A;
suppose A1: a = 0.K;
thus a * b=(multemb f).(x,y) by defemb .= multemb(f,x,y) by defmult
.= 0.K by A1,defmultf .= multemb(f,y,x) by A1,defmultf
.= (multemb f).(y,x) by defmult .= b * a by defemb;
end;
suppose A1: b = 0.K;
thus a * b = (multemb f).(x,y) by defemb .=multemb(f,x,y) by defmult
.= 0.K by A1,defmultf .= multemb(f,y,x) by A1,defmultf
.= (multemb f).(y,x) by defmult .= b * a by defemb;
end;
end;
suppose A: x in [#]K & x <> 0.K & not y in [#]K; then
reconsider a1 = a as Element of K;
reconsider b1 = b as Element of T by A,Lm1;
reconsider fa = f.a1 as Element of T;
thus a * b=(multemb f).(x,y) by defemb .= multemb(f,x,y) by defmult
.= fa * b1 by A,defmultf .= b1 * fa by GROUP_1:def 12
.= multemb(f,y,x) by A,defmultf
.= (multemb f).(y,x) by defmult .= b * a by defemb;
end;
suppose A: y in [#]K & y <> 0.K & not x in [#]K; then
reconsider b1 = b as Element of K;
reconsider a1 = a as Element of T by A,Lm1;
reconsider fb = f.b1 as Element of T;
thus a*b = (multemb f).(x,y) by defemb .= multemb(f,x,y) by defmult
.= a1*fb by A,defmultf .= fb*a1 by GROUP_1:def 12
.= multemb(f,y,x) by A,defmultf .= (multemb f).(y,x) by defmult
.= b*a by defemb;
end;
suppose A: not x in [#]K & not y in [#]K &
(the multF of T).(x,y) in rng f; then
reconsider a1 = a, b1 = b as Element of T by Lm1;
B: (the multF of T).(a,b) = a1*b1 .= b1*a1 by GROUP_1:def 12
.= (the multF of T).(b,a);
thus a*b = (multemb f).(x,y) by defemb
.= multemb(f,x,y) by defmult .= (f").(a1*b1) by A,defmultf
.= multemb(f,y,x) by A,B,defmultf
.= (multemb f).(y,x) by defmult .= b*a by defemb;
end;
suppose A: not x in [#]K & not y in [#]K &
not((the multF of T).(x,y) in rng f); then
reconsider a1 = a, b1 = b as Element of T by Lm1;
C: a <> 0.K & b <> 0.K by A;
B: (the multF of T).(a,b) = a1*b1 .= b1*a1 by GROUP_1:def 12
.= (the multF of T).(b,a);
thus
a*b = (multemb f).(x,y) by defemb .= multemb(f,x,y) by defmult
.= (the multF of T).(a,b) by C,A,defmultf
.= multemb(f,y,x) by C,A,B,defmultf .= (multemb f).(y,x) by defmult
.= b*a by defemb;
end;
end;
hence thesis;
end;
thus
embField f is well-unital
proof
now let a be Element of embField f;
reconsider x = a as Element of carr f by defemb;
reconsider e = 1.(embField f) as Element of carr f by defemb;
B: a*1.(embField f)=(multemb f).(x,e) by defemb .= multemb(f,x,e) by defmult;
D: 1.(embField f)*a=(multemb f).(e,x) by defemb .= multemb(f,e,x) by defmult;
C: 1.(embField f) = 1.K by defemb;
per cases;
suppose x in [#]K;
then reconsider a1 = a as Element of K;
multemb(f,x,e) = a1 * 1.K by C,defmultf;
hence a * 1.(embField f) = a by B;
multemb(f,e,x) = 1.K * a1 by C,defmultf;
hence 1.(embField f) * a = a by D;
end;
suppose A: not x in [#]K;
then
reconsider a1 = a as Element of T by Lm1;
E: e in [#]K & e <> 0.K by C; then
multemb(f,x,e) = (the multF of T).(a1,f.e) by A,defmultf
.= (the multF of T).(a1,f.(1_K)) by defemb .= a1*1_T by GROUP_1:def 13;
hence a * 1.(embField f) = a by B;
multemb(f,e,x) = (the multF of T).(f.e,a1) by E,A,defmultf
.= (the multF of T).(f.(1_K),a1) by defemb .= 1_T*a1 by GROUP_1:def 13;
hence 1.(embField f) * a = a by D;
end;
end;
hence thesis;
end;
end;
end;
theorem Th8:
for f being Monomorphism of K,F st K,F are_disjoint
holds embField f is associative
proof
let f be Monomorphism of K,F;
assume AS: K,F are_disjoint;
now let a,b,c be Element of embField f;
reconsider x = a, y = b, z = c as Element of carr f by defemb;
per cases;
suppose O: a = 0.K or b = 0.K or c = 0.K;
reconsider bb = b, ab = a*b, bc = b*c as Element of carr f by defemb;
per cases by O;
suppose A: a = 0.K;
A1: a*b = (multemb f).(x,bb) by defemb .= multemb(f,x,bb) by defmult
.= 0.K by A,defmultf;
A2: (a*b)*c = (multemb f).(ab,z) by defemb .= multemb(f,ab,z) by defmult
.= 0.K by A1,defmultf;
thus
a*(b*c) = (multemb f).(x,bc) by defemb .= multemb(f,x,bc) by defmult
.= (a*b)* c by A2,A,defmultf;
end;
suppose A: b = 0.K or c = 0.K;
A1: b*c = (multemb f).(y,z) by defemb .= multemb(f,y,z) by defmult
.= 0.K by A,defmultf;
A2: a*(b*c) = (multemb f).(x,bc) by defemb .= multemb(f,x,bc) by defmult
.= 0.K by A1,defmultf;
per cases by A;
suppose A3: b = 0.K;
A4: a*b = (multemb f).(x,bb) by defemb .= multemb(f,x,bb) by defmult
.= 0.K by A3,defmultf;
thus (a*b)*c = (multemb f).(ab,z) by defemb
.= multemb(f,ab,z) by defmult .= a*(b*c) by A4,A2,defmultf;
end;
suppose A3: c = 0.K;
thus (a*b)*c = (multemb f).(ab,z) by defemb
.= multemb(f,ab,z) by defmult .= a*(b*c) by A3,A2,defmultf;
end;
end;
end;
suppose O: a <> 0.K & b <> 0.K & c <> 0.K;
per cases;
suppose X: x in [#]K; then
reconsider a1 = a as Element of K;
per cases;
suppose Y: y in [#]K; then
reconsider b1 = b as Element of K;
X0: a * b = a1 * b1 by Lm11; then
reconsider ab = a * b as Element of carr f by XBOOLE_0:def 3;
per cases;
suppose z in [#]K; then
reconsider c1 = c as Element of K;
X1: b*c = b1*c1 by Lm11; then
reconsider bc = b * c as Element of carr f by XBOOLE_0:def 3;
thus (a*b)*c = (multemb f).(a*b,z) by defemb
.= multemb(f,ab,z) by defmult .= (a1*b1)*c1 by X0,defmultf
.= a1*(b1*c1) by GROUP_1:def 3.=multemb(f,x,bc) by X1,defmultf
.= (multemb f).(x,b*c) by defmult .= a*(b*c) by defemb;
end;
suppose Z: not z in [#]K; then
reconsider c1 = c as Element of F by Lm1;
reconsider bc = b * c as Element of carr f by defemb;
reconsider fa = f.a1, fb = f.b1 as Element of F;
X1: f.(a1*b1) = fa * fb by GROUP_6:def 6;
X2: b * c = fb * c1 by AS,O,Y,Z,Lm10;
X3: not fb * c1 in [#]K by AS,XBOOLE_0:def 4;
thus
(a*b)*c = (multemb f).(a*b,z) by defemb
.= multemb(f,ab,z) by defmult
.= (fa*fb)*c1 by O,VECTSP_2:def 1,X1,X0,defmultf,Z
.= fa*(fb*c1) by GROUP_1:def 3
.= multemb(f,x,bc) by O,X3,X2,defmultf
.= (multemb f).(x,b*c) by defmult .= a * (b * c) by defemb;
end;
end;
suppose Y: not y in [#]K; then
reconsider b1 = b as Element of F by Lm1;
reconsider fa = f.a1 as Element of F;
X0: a*b = fa*b1 by AS,O,X,Y,Lm10; then
reconsider ab = fa * b1 as Element of carr f by defemb;
X1: not ab in [#]K by AS,XBOOLE_0:def 4;
per cases;
suppose Z: z in [#]K; then
reconsider c1 = c as Element of K;
reconsider fc = f.c1 as Element of F;
X2: b * c = b1 * fc by AS,O,Y,Z,Lm10; then
reconsider bc = b1 * fc as Element of carr f by defemb;
X3: not bc in [#]K by AS,XBOOLE_0:def 4;
thus
(a*b)*c = (fa*b1)*fc by AS,O,X1,X0,Z,Lm10
.= fa*(b1*fc) by GROUP_1:def 3
.= a*(b*c) by AS,O,X,X2,X3,Lm10;
end;
suppose Z: not z in [#]K; then
reconsider c1 = c as Element of F by Lm1;
reconsider fa1 = f.a1 as Element of (rng f) by FUNCT_2:4;
K5: (the multF of F).(ab,z)=(fa*b1)*c1 .= fa*(b1*c1)
by GROUP_1:def 3;
per cases;
suppose K: (the multF of F).(ab,z) in rng f;
X2: (a*b)*c = (multemb f).(ab,z) by X0,defemb
.= multemb(f,ab,z) by defmult
.= f".((fa*b1)*c1) by X1,Z,defmultf,K
.= f".(fa*(b1*c1)) by GROUP_1:def 3;
K1: now assume K7: not (the multF of F).(y,z) in rng f;
X4: not (the multF of F).(b1,c1) in [#]K
by AS,XBOOLE_0:def 4;
X3: b*c = b1*c1 by AS,Y,Z,Lm12,K7;
b1*c1 in [#]F \ rng f by K7,XBOOLE_0:def 5; then
reconsider bc1 = b1*c1 as Element of carr f by XBOOLE_0:def 3;
reconsider bce = bc1 as Element of embField f by X3;
(the multF of F).(f.a,bce) in [#]F\rng f by O,X,X4,Lm5;
hence contradiction by K5,K,XBOOLE_0:def 5;
end; then
X3: b * c = f".(b1*c1) by Y,Z,Lm13;
f".(b1*c1) in [#]K by K1,FUNCT_2:5; then
reconsider bc=f".(b1*c1) as Element of carr f by XBOOLE_0:def 3;
reconsider bc1=b1*c1 as Element of (rng f) by K1;
thus
(a*b)*c = f".fa1 * f".bc1 by Th1,X2
.= a1*f".bc1 by FUNCT_2:26
.= multemb(f,x,bc) by defmultf
.= (multemb f).(x,bc) by defmult .= a*(b*c) by X3,defemb;
end;
suppose K: not (the multF of F).(ab,z) in rng f;
X4: ab <> 0.K by AS,XBOOLE_0:def 4;
X2: (a*b)*c = (multemb f).(ab,z) by X0,defemb
.= multemb(f,ab,z) by defmult
.= (fa*b1)*c1 by O,X4,X1,Z,defmultf,K
.= fa * (b1*c1) by GROUP_1:def 3;
K1: now assume K7: (the multF of F).(y,z) in rng f;
X7: dom f = [#]K by FUNCT_2:def 1;
consider x being object such that
X6: x in dom f & b1*c1 = f.x by K7,FUNCT_1:def 3;
reconsider xx = x as Element of K by X6;
f.(a1*xx) = fa*(b1*c1) by X6,GROUP_6:def 6;
hence contradiction by K5,K,X7,FUNCT_1:3;
end; then
b1*c1 in [#]F \ rng f by XBOOLE_0:def 5; then
reconsider bc = b1*c1 as Element of carr f by XBOOLE_0:def 3;
X3: b*c = b1*c1 by AS,K1,Y,Z,Lm12;
not b1 * c1 in [#]K by AS,XBOOLE_0:def 4;
hence (a*b)*c = multemb(f,x,bc) by O,X2,defmultf
.= (multemb f).(x,bc) by defmult .= a*(b*c) by X3,defemb;
end;
end;
end;
end;
suppose X: not x in [#]K; then
reconsider a1 = a as Element of F by Lm1;
per cases;
suppose Y: y in [#]K; then
reconsider b1 = b as Element of K;
X0: a*b = a1*f.b1 by AS,O,X,Y,Lm10;
reconsider ab = a*b as Element of carr f by defemb;
reconsider fb = f.b1 as Element of F;
X2: not ab in [#]K by AS,O,X,Y,Lm10;
per cases;
suppose z in [#]K; then
reconsider c1 = c as Element of K;
reconsider fc = f.c1 as Element of F;
X3: b*c = b1*c1 by Lm11; then
reconsider bc = b*c as Element of carr f by XBOOLE_0:def 3;
thus
(a*b)*c = (multemb f).(ab,z) by defemb
.= multemb(f,ab,z) by defmult
.= (a1*fb)*fc by O,X0,X2,defmultf
.= a1*(fb*fc) by GROUP_1:def 3
.= a1*f.(b1*c1) by GROUP_6:def 6
.= multemb(f,x,bc) by defmultf,X3,X,O,VECTSP_2:def 1
.= (multemb f).(x,bc) by defmult .= a*(b*c) by defemb;
end;
suppose Z: not z in [#]K; then
reconsider c1 = c as Element of F by Lm1;
X3: b*c = f.b1*c1 by AS,O,Y,Z,Lm10;
reconsider bc = b * c as Element of carr f by defemb;
X5: not b*c in [#]K by AS,O,Y,Z,Lm10;
K5: (the multF of F).(ab,z) = (a1*fb)*c1 by AS,O,X,Y,Lm10
.= a1*(fb*c1) by GROUP_1:def 3
.= (the multF of F).(x,bc) by AS,O,Y,Z,Lm10;
per cases;
suppose K: not (the multF of F).(ab,z) in rng f;
hence (a*b)*c = (a1*fb)*c1 by AS,X0,X2,Z,Lm12
.= a1*(fb*c1) by GROUP_1:def 3
.= a*(b*c) by AS,K,K5,X3,X,X5,Lm12;
end;
suppose K: (the multF of F).(ab,z) in rng f;
thus (a*b)*c = (multemb f).(ab,z) by defemb
.= multemb(f,ab,z) by defmult
.= (f").((the multF of F).(ab,z)) by K,X2,Z,defmultf
.= multemb(f,x,bc) by K,K5,X,X5,defmultf
.= (multemb f).(x,bc) by defmult .= a*(b*c) by defemb;
end;
end;
end;
suppose Y: not y in [#]K; then
reconsider b1 = b as Element of F by Lm1;
per cases;
suppose K: not (the multF of F).(x,y) in rng f;
then X0: a*b = a1*b1 by AS,Y,X,Lm12;
a1*b1 in [#]F \ rng f by K,XBOOLE_0:def 5; then
reconsider ab = a1 * b1 as Element of carr f by XBOOLE_0:def 3;
D: not ab in [#]K by AS,XBOOLE_0:def 4;
per cases;
suppose Z: z in [#]K; then
reconsider c1 = c as Element of K;
X1: b*c = b1*f.c1 by AS,O,Y,Z,Lm10;
[#](embField f) = carr f by defemb; then
X3: b1*f.c1 in [#]F\rng f by O,Y,Lm4;
X2: not b1 * f.c1 in [#]K by AS,XBOOLE_0:def 4;
reconsider bc=b1*f.c1 as Element of carr f by X3,XBOOLE_0:def 3;
X4: (a*b)*c = (a1*b1)*f.c1 by AS,O,X0,Z,D,Lm10
.= a1*(b1*f.c1) by GROUP_1:def 3;
X5: (the multF of F).(x,bc) = a1*(b1*f.c1)
.= (a1*b1)*f.c1 by GROUP_1:def 3
.= (the multF of F).(ab,f.z);
(the multF of F).(ab,f.z) in [#]F \ rng f
by O,D,Lm4,Z; then
H: not (the multF of F).(x,bc) in rng f
by X5,XBOOLE_0:def 5;
bc <> 0.K by AS,XBOOLE_0:def 4;
hence (a*b)*c = multemb(f,x,bc)
by O,H,X,X2,X4,defmultf
.=(multemb f).(x,bc) by defmult.=a*(b*c) by X1,defemb;
end;
suppose Z: not z in [#]K; then
reconsider c1 = c as Element of F by Lm1;
K5: (the multF of F).(ab,z) = (a1*b1)*c1
.= a1*(b1*c1) by GROUP_1:def 3
.= (the multF of F).(a1,b1*c1);
per cases;
suppose K: not (the multF of F).(ab,z) in rng f;
per cases;
suppose K6:not(the multF of F).(b1,c1) in rng f;
X1: b*c = (multemb f).(y,z) by defemb
.= multemb(f,y,z) by defmult
.= b1*c1 by O,defmultf,Y,Z,K6;
K9: (the multF of F).(b1,c1) in [#]F \ rng f
by K6,XBOOLE_0:def 5;
K8: not b1*c1 in [#]K by AS,XBOOLE_0:def 4;
reconsider bc=b1*c1 as Element of carr f by K9,XBOOLE_0:def 3;
X4: ab <> 0.K & bc <> 0.K by AS,XBOOLE_0:def 4;
thus
(a*b)*c = (multemb f).(ab,z) by X0,defemb
.= multemb(f,ab,z) by defmult
.= (a1*b1) * c1 by X4,O,D,Z,defmultf,K
.= multemb(f,x,bc) by X4,O,X,K5,K,K8,defmultf
.= (multemb f).(x,bc) by defmult
.= a*(b*c) by X1,defemb;
end;
suppose K6: (the multF of F).(b1,c1) in rng f;
X1: b * c = (multemb f).(y,z) by defemb
.=multemb(f,y,z) by defmult
.= f".(b1*c1) by defmultf,Y,Z,K6;
b1*c1 in dom(f") by K6,FUNCT_1:33; then
f".(b1 * c1) in rng(f") by FUNCT_1:3; then
reconsider bc1 = f".(b1 * c1) as Element of [#]K;
reconsider bc = bc1 as Element of carr f by XBOOLE_0:def 3;
M0: dom f = [#]K by FUNCT_2:def 1;
f.(0.K) = 0.F by RING_2:6; then
M1: 0.F in rng f by M0,FUNCT_1:def 3; then
M2: c1 <> 0.F by Z,Lm1;
b1 <> 0.F by M1,Y,Lm1; then
b1*c1 <> 0.F by M2,VECTSP_2:def 1; then
X4: bc<>0.K & ab<>0.K by AS,XBOOLE_0:def 4,K6,Th2;
thus
(a*b)*c = (multemb f).(ab,z) by X0,defemb
.= multemb(f,ab,z) by defmult
.= (a1*b1)*c1 by X4,O,D,Z,defmultf,K
.= a1*(b1*c1) by GROUP_1:def 3
.= a1*f.bc1 by K6,FUNCT_1:35
.= multemb(f,x,bc) by X4,X,defmultf
.= (multemb f).(x,bc) by defmult
.= a*(b*c) by X1,defemb;
end;
end;
suppose K7: (the multF of F).(ab,z) in rng f;
K6: now assume (the multF of F).(b1,c1) in rng f; then
consider x being object such that
H1: x in dom f & f.x = b1 * c1 by FUNCT_1:def 3;
consider y being object such that
H2: y in dom f & f.y = (a1*b1)*c1 by K7,FUNCT_1:def 3;
reconsider xx = x, yy = y as Element of K by H1,H2;
B3h: dom f = [#]K by FUNCT_2:def 1;
B3a: a in ([#]F) & not(a in (rng f)) by X,Lm1;
f.(0.K) = 0.F by RING_2:6; then
0.F in rng f by B3h,FUNCT_1:def 3; then
OO: a1<>0.F & b1<>0.F & c1<>0.F by X,Y,Z,Lm1; then
xx <> 0.K by H1,RING_2:6,VECTSP_2:def 1; then
f.(xx")=(b1*c1)" by Th5,H1
.= c1" * b1" by OO,VECTSP_2:11
.= b1" * c1" by GROUP_1:def 12; then
f.yy*f.(xx") = (a1*(b1*c1))*(b1" * c1")
by H2,GROUP_1:def 3
.= a1*((b1*c1)*(b1" * c1")) by GROUP_1:def 3
.= a1*(b1*(c1*(b1" * c1"))) by GROUP_1:def 3
.= a1*(b1*(c1*(c1" * b1"))) by GROUP_1:def 12
.= a1*(b1*((c1*c1")* b1")) by GROUP_1:def 3
.= a1*(b1*((c1" *c1)* b1")) by GROUP_1:def 12
.= a1*(b1*(1.F*b1")) by OO,VECTSP_1:def 10
.= a1*(b1" *b1) by GROUP_1:def 12
.= a1*1.F by OO,VECTSP_1:def 10; then
B4: a1 = f.(yy * xx") by GROUP_6:def 6;
dom f = [#]K by FUNCT_2:def 1;
hence contradiction by B3a,B4,FUNCT_1:def 3;
end;
X1: b*c = (multemb f).(y,z) by defemb
.= multemb(f,y,z) by defmult
.= b1*c1 by O,defmultf,Y,Z,K6;
b1*c1 in [#]F\rng f by K6,XBOOLE_0:def 5; then
reconsider bc = b1*c1 as Element of carr f by XBOOLE_0:def 3;
K9: not bc in [#]K by AS,XBOOLE_0:def 4;
thus
(a*b)*c = (multemb f).(ab,z) by X0,defemb
.= multemb(f,ab,z) by defmult
.= f".((a1*b1)*c1) by D,Z,defmultf,K7
.= multemb(f,x,bc) by X,K5,K7,defmultf,K9
.= (multemb f).(x,bc) by defmult
.= a*(b*c) by X1,defemb;
end;
end;
end;
suppose L: (the multF of F).(x,y) in rng f;
Z1: a*b = (multemb f).(x,y) by defemb
.= multemb(f,x,y) by defmult
.= f".(a1 * b1) by defmultf,X,Y,L;
a1*b1 in dom(f") by L,FUNCT_1:33; then
f".(a1 * b1) in rng(f") by FUNCT_1:3; then
reconsider ab1 = f".(a1 * b1) as Element of [#]K;
reconsider ab = ab1 as Element of carr f by XBOOLE_0:def 3;
per cases;
suppose Z: z in [#]K; then
reconsider c1 = c as Element of K;
Z2: b*c = (multemb f).(y,z) by defemb
.= multemb(f,y,z) by defmult
.= b1 * f.c1 by O,defmultf,Y; then
L0: b*c in [#]F \ rng f by O,Lm4,Y,Z;
reconsider bc1 = b1 * f.c1 as Element of F;
reconsider bc = bc1 as Element of carr f by Z2,L0,XBOOLE_0:def 3;
Z3: (a*b)*c = (multemb f).(ab,z) by Z1,defemb
.= multemb(f,ab,z) by defmult
.= ab1 * c1 by defmultf;
Z4: not bc in [#]K by AS,XBOOLE_0:def 4;
Z9: dom f = [#]K & (rng f) c= ([#]F) by FUNCT_2:def 1;
L2: dom f = [#]K by FUNCT_2:def 1; then
reconsider fc1 = f.c1 as Element of (rng f) by FUNCT_1:def 3;
reconsider ffc1 = f".fc1 as Element of K;
f".fc1 = c1 by L2,FUNCT_1:34; then
Z5: f".((a1*b1)*fc1) = ab1*c1 by L,Th1;
consider x1 being object such that
Z6: x1 in dom f & f.x1 = a1 * b1 by L,FUNCT_1:def 3;
reconsider xx = x1 as Element of K by Z6;
f.(xx*c1) = (a1*b1)*f.c1 by Z6,GROUP_6:def 6; then
(a1*b1)*f.c1 in rng f by Z9,FUNCT_1:def 3; then
L1: a1 * (b1 * f.c1) in rng f by GROUP_1:def 3;
thus
a*(b*c) = (multemb f).(x,bc) by Z2,defemb
.= multemb(f,x,bc) by defmult
.= f".(a1*bc1) by L1,Z4,X,defmultf
.= (a*b)*c by Z3,Z5,GROUP_1:def 3;
end;
suppose Z: not z in [#]K; then
reconsider c1 = c as Element of F by Lm1;
M0: dom f = [#]K by FUNCT_2:def 1;
f.(0.K) = 0.F by RING_2:6; then
M1: 0.F in rng f by M0,FUNCT_1:def 3; then
M2: a1 <> 0.F by X,Lm1;
b1 <> 0.F by M1,Y,Lm1; then
a1*b1 <> 0.F by M2,VECTSP_2:def 1; then
Z0: ab <> 0.K by L,Th2;
Z2: (a*b)*c = (multemb f).(ab,z) by Z1,defemb
.= multemb(f,ab,z) by defmult
.= f.ab1*c1 by Z,Z0,defmultf
.= (a1*b1)*c1 by L,FUNCT_1:35
.= a1*(b1*c1) by GROUP_1:def 3;
f.(f".(a1*b1)) = a1*b1 by FUNCT_1:35,L; then
(a1*b1)*c1 in ([#]F)\(rng f) by Z0,Z,Lm5; then
a1*(b1*c1) in ([#]F)\(rng f) by GROUP_1:def 3; then
U2: not (the multF of F).(a,b1*c1) in rng f
by XBOOLE_0:def 5;
per cases;
suppose L1: not (the multF of F).(y,z) in rng f;
X3: b*c = (multemb f).(y,z) by defemb
.= multemb(f,y,z) by defmult
.= b1 * c1 by O,L1,Y,Z,defmultf;
X4: b1*c1 in [#]F\rng f by L1,XBOOLE_0:def 5;
reconsider bc1 = b1*c1 as Element of F;
reconsider bc = bc1 as Element of carr f by X4,XBOOLE_0:def 3;
not bc in [#]K & bc <> 0.K by AS,XBOOLE_0:def 4;
hence
(a*b)*c =multemb(f,x,bc) by O,Z2,U2,X,defmultf
.= (multemb f).(x,bc) by defmult
.= a * (b * c) by X3,defemb;
end;
suppose K6: (the multF of F).(y,z) in rng f;
X1: b*c = (multemb f).(y,z) by defemb
.= multemb(f,y,z) by defmult
.= f".(b1 * c1) by defmultf,Y,Z,K6;
b1*c1 in dom(f") by K6,FUNCT_1:33; then
f".(b1 * c1) in rng(f") by FUNCT_1:3; then
reconsider bc1 = f".(b1 * c1) as Element of [#]K;
reconsider bc = bc1 as Element of carr f by XBOOLE_0:def 3;
M0: dom f = [#]K by FUNCT_2:def 1;
f.(0.K) = 0.F by RING_2:6; then
M1: 0.F in rng f by M0,FUNCT_1:def 3; then
M2: c1 <> 0.F by Z,Lm1;
b1 <> 0.F by M1,Y,Lm1; then
b1 * c1 <> 0.F by M2,VECTSP_2:def 1; then
X2: bc <> 0.K by K6,Th2;
thus
(a*b)*c = a1*f.bc1 by Z2,K6,FUNCT_1:35
.= multemb(f,x,bc) by X2,X,defmultf
.= (multemb f).(x,bc) by defmult
.= a*(b*c) by X1,defemb;
end;
end;
end;
end;
end;
end;
end;
hence thesis;
end;
theorem Th9:
for f being Monomorphism of K,T st K,T are_disjoint
holds embField f is distributive
proof
let f be Monomorphism of K,T;
assume AS: K,T are_disjoint;
now let a,b,c be Element of embField f;
reconsider x = a, y = b, z = c as Element of carr f by defemb;
per cases;
suppose A: a = 0.K;
A1: a * b = (multemb f).(x,y) by defemb .= multemb(f,x,y) by defmult
.= 0.K by A,defmultf;
A2: a * c = (multemb f).(x,z) by defemb .= multemb(f,x,z) by defmult
.= 0.K by A,defmultf;
reconsider bc = b + c as Element of carr f by defemb;
thus I: a*(b+c) = (multemb f).(x,b+c) by defemb
.= multemb(f,x,bc) by defmult .= 0.K by A,defmultf
.= 0.(embField f) by defemb
.= 0.(embField f) + 0.(embField f) by RLVECT_1:def 4
.= a*b + 0.(embField f) by A1,defemb .= a*b + a*c by A2,defemb;
thus (b + c) * a = a * (b + c) by GROUP_1:def 12
.= b*a + a*c by I,GROUP_1:def 12
.= b*a + c*a by GROUP_1:def 12;
end;
suppose A: a <> 0.K;
thus I: a * (b + c) = a*b + a*c
proof
per cases;
suppose B: b = 0.K;
A1: a*b=(multemb f).(x,y) by defemb
.= multemb(f,x,y) by defmult .= 0.K by B,defmultf;
b + c = 0.(embField f)+c by B,defemb .= c by RLVECT_1:def 4;
hence a*(b+c)= 0.(embField f)+a*c by RLVECT_1:def 4
.= a*b + a*c by A1,defemb;
end;
suppose C: c = 0.K;
A1: a*c = (multemb f).(x,z) by defemb
.= multemb(f,x,z) by defmult .= 0.K by C,defmultf;
b + c = b + 0.(embField f) by C,defemb .= b by RLVECT_1:def 4;
hence a * (b + c) = a*b + 0.(embField f) by RLVECT_1:def 4
.= a*b + a*c by A1,defemb;
end;
suppose BC: b <> 0.K & c <> 0.K;
per cases;
suppose X: x in [#]K; then
reconsider a1 = a as Element of K;
per cases;
suppose Y: y in [#]K; then
reconsider b1 = b as Element of K;
A1: a * b = a1 * b1 by Lm11;
reconsider ab = a*b as Element of carr f by defemb;
per cases;
suppose c in [#]K; then
reconsider c1 = c as Element of K;
A2: a * c = a1 * c1 by Lm11;
A3: b + c = b1 + c1 by Lm7;
reconsider bc=b+c, ac=a*c as Element of carr f by defemb;
thus a*(b+c)=a1*(b1+c1) by A3,Lm11
.= a1 * b1 + a1 * c1 by VECTSP_1:def 7
.= a*b + a*c by A2,A1,Lm7;
end;
suppose Z: not z in [#]K; then
reconsider c1 = c as Element of T by Lm1;
A2: a * c = f.a1 * c1 by AS,X,Z,A,Lm10;
A3: b + c = f.b1 + c1 by AS,Y,Z,Lm6;
then reconsider bc = f.b1 + c1 as Element of carr f by defemb;
reconsider ac = f.a1 * c1 as Element of carr f by A2,defemb;
A4: not bc in [#]K by AS,A3,Y,Z,Lm6;
A5: not ac in [#]K by A2,AS,A,X,Z,Lm10;
thus a*(b+c) = (multemb f).(x,bc) by A3,defemb
.= multemb(f,x,bc) by defmult
.= f.a1 * (f.b1 + c1) by A,A4,defmultf
.= f.a1 * f.b1 + f.a1 * c1 by VECTSP_1:def 7
.= f.(a1*b1) + f.a1 * c1 by GROUP_6:def 6
.= addemb(f,ab,ac) by A5,A1,defaddf
.= (addemb f).(ab,ac) by defadd
.= a*b + a*c by A2,defemb;
end;
end;
suppose Y: not y in [#]K; then
reconsider b1 = b as Element of T by Lm1;
A1: a * b = f.a1 * b1 by AS,X,Y,A,Lm10;
then reconsider ab = f.a1 * b1 as Element of carr f by defemb;
A5: not ab in [#]K by A1,AS,X,Y,A,Lm10;
per cases;
suppose Z: z in [#]K; then
reconsider c1 = c as Element of K;
A2: a * c = a1 * c1 by Lm11;
A3: b + c = b1 + f.c1 by AS,Y,Z,Lm6;
reconsider bc=b+c, ac=a*c as Element of carr f by defemb;
A4: not bc in [#]K by AS,Y,Z,Lm6;
reconsider fc1 = f.c1 as Element of T;
thus a*(b+c) = (multemb f).(x,bc) by defemb
.= multemb(f,x,bc) by defmult
.= f.a1 * (b1 + f.c1) by A,A3,A4,defmultf
.= f.a1 * b1 + f.a1 * f.c1 by VECTSP_1:def 7
.= f.a1 * b1 + f.(a1 * c1) by GROUP_6:def 6
.= addemb(f,ab,ac) by A5,A2,defaddf
.= (addemb f).(ab,ac) by defadd
.= a*b + a*c by A1,defemb;
end;
suppose Z: not z in [#]K; then
reconsider c1 = c as Element of T by Lm1;
A2: a*c = f.a1 * c1 by AS,X,Z,A,Lm10;
reconsider ac = a * c as Element of carr f by defemb;
A6: not ac in [#]K by AS,X,Z,A,Lm10;
per cases;
suppose Z1: not(the addF of T).(y,z) in rng f; then
A3: b + c = b1 + c1 by AS,Y,Z,Lm8;
reconsider bc = b + c as Element of carr f by defemb;
A4: not bc in [#]K by AS,A3,XBOOLE_0:def 4; then
A8: (the multF of T).(f.x,bc) in [#]T\rng f by A,X,Lm5;
(the multF of T).(f.x,bc)
= f.a1*(b1+c1) by Z1,AS,Y,Z,Lm8
.=f.a1*b1 + f.a1*c1 by VECTSP_1:def 7
.= (the addF of T).(ab,ac) by AS,X,Z,A,Lm10; then
A7: not (the addF of T).(ab,ac) in rng f
by A8,XBOOLE_0:def 5;
thus a*(b+c)=(multemb f).(x,bc) by defemb
.= multemb(f,x,bc) by defmult
.= f.a1 * (b1 + c1) by A,A3,A4,defmultf
.= f.a1 * b1 + f.a1 * c1 by VECTSP_1:def 7
.= addemb(f,ab,ac) by A2,A5,A6,A7,defaddf
.= (addemb f).(ab,ac) by defadd
.= a*b + a*c by A1,defemb;
end;
suppose Z1: (the addF of T).(y,z) in rng f; then
A3: b + c = f".(b1 + c1) by Y,Z,Lm9;
reconsider bc=b+c, ac=a*c as Element of carr f by defemb;
A0: dom f = [#]K by FUNCT_2:def 1;
b1 + c1 in dom(f") by Z1,FUNCT_1:33; then
b + c in rng(f") by A3,FUNCT_1:3; then
reconsider bc1 = b + c as Element of K;
A9: f.(a1*bc1) = f.a1 * f.bc1 by GROUP_6:def 6
.= f.a1 * (b1 + c1) by Z1,A3,FUNCT_1:35
.= f.a1*b1+f.a1*c1 by VECTSP_1:def 7; then
A4: (the addF of T).(ab,ac) in rng f
by A0,A2,FUNCT_1:def 3;
reconsider fa1 = f.a1 as Element of rng f by A0,FUNCT_1:3;
reconsider fbc1 = f. bc1 as Element of rng f by A0,FUNCT_1:3;
thus a * (b + c) = (multemb f).(x,bc) by defemb
.= multemb(f,x,bc) by defmult .= a1 * bc1
by defmultf
.= (f").(f.a1*b1+f.a1*c1) by A9,A0,FUNCT_1:34
.= addemb(f,ab,ac) by A2,A4,A5,A6,defaddf
.= (addemb f).(ab,ac) by defadd
.= a*b + a*c by A1,defemb;
end;
end;
end;
end;
suppose X: not x in [#]K; then
reconsider a1 = a as Element of T by Lm1;
B0: dom f = [#]K by FUNCT_2:def 1;
per cases;
suppose Y: y in [#]K; then
reconsider b1 = b as Element of K;
A1: a * b = a1 * f.b1 by AS,X,Y,BC,Lm10;
then reconsider ab = a1 * f.b1 as Element of carr f by defemb;
A2: not ab in [#]K by A1,AS,X,Y,BC,Lm10;
per cases;
suppose Z: z in [#]K; then
reconsider c1 = c as Element of K;
A3: a*c = a1*f.c1 by AS,X,Z,BC,Lm10;
then reconsider ac = a1 * f.c1 as Element of carr f by defemb;
A4: not ac in [#]K by A3,AS,X,Z,BC,Lm10;
A5: b + c = (addemb f).(y,z) by defemb
.= addemb(f,y,z) by defadd
.= b1 + c1 by defaddf; then
reconsider bc1 = b + c as Element of K;
reconsider bc = b + c as Element of carr f by defemb;
per cases;
suppose O: bc = 0.K;
A6: a * (b + c) = (multemb f).(x,bc) by defemb
.= multemb(f,x,bc) by defmult
.= 0.K by O,defmultf;
a1*f.b1+a1*f.c1=a1*(f.b1+f.c1)
by VECTSP_1:def 7
.= a1 * f.(b1 + c1) by VECTSP_1:def 20
.= a1 * 0.T by O,RING_2:6,A5
.= f.(0.K) by RING_2:6; then
A7: a1 * f.b1 + a1 * f.c1 in rng f
by B0,FUNCT_1:3;
a * b + a * c = (addemb f).(ab,ac)
by A1,A3,defemb
.= addemb(f,ab,ac) by defadd
.= f".(a1 * f.b1 + a1 * f.c1)
by A4,A2,A7,defaddf
.= f".(a1 * (f.b1 + f.c1))
by VECTSP_1:def 7
.= f".(a1 * f.(b1 + c1))
by VECTSP_1:def 20
.= f".(a1 * 0.T) by A5,O,RING_2:6
.= 0.K by Th3;
hence thesis by A6;
end;
suppose O: bc <> 0.K; then
A6: (the multF of T).(x,f.bc) in [#]T \ rng f
by A5,X,Lm4;
(the multF of T).(x,f.bc)
= a1*(f.b1 + f.c1) by A5,VECTSP_1:def 20
.= a1*f.b1 + a1*f.c1 by VECTSP_1:def 7;
then
A7: not a1*f.b1 + a1*f.c1 in rng f
by A6,XBOOLE_0:def 5;
thus a * (b + c) = (multemb f).(x,bc)
by defemb
.= multemb(f,x,bc) by defmult
.= a1*f.bc1 by O,X,defmultf
.= a1*(f.b1 + f.c1) by A5,VECTSP_1:def 20
.= a1*f.b1 + a1*f.c1 by VECTSP_1:def 7
.= addemb(f,ab,ac) by A2,A4,A7,defaddf
.= (addemb f).(ab,ac) by defadd
.= a*b + a*c by A1,A3,defemb;
end;
end;
suppose Z: not z in [#]K; then
reconsider c1 = c as Element of T by Lm1;
A3: b + c = f.b1 + c1 by AS,Y,Z,Lm6; then
reconsider bc = f.b1 + c1 as Element of carr f by defemb;
A4: not bc in [#]K by A3,AS,Lm6,Z,Y;
A7: (the multF of T).(x,bc) = a1 * (f.b1 + c1)
.= a1 * f.b1 + a1 * c1 by VECTSP_1:def 7;
per cases;
suppose Z1:(the multF of T).(x,bc) in rng f;
A5: now assume (the multF of T).(x,z) in rng f;
then
consider yy being object such that
C1: yy in dom f & f.yy = a1*c1 by FUNCT_1:def 3;
reconsider yy as Element of carr f by C1,XBOOLE_0:def 3;
(the addF of T).(ab,f.yy) in [#]T \ rng f
by C1,A2,Lm2;
hence contradiction
by Z1,A7,C1,XBOOLE_0:def 5;
end;
then A6: a * c = a1 * c1 by AS,X,Z,Lm12;
then reconsider ac = a1 * c1 as Element of carr f by defemb;
A9: not ac in [#]K by A6,AS,X,Z,A5,Lm12;
thus a * (b + c) = (multemb f).(x,bc)
by A3,defemb
.= multemb(f,x,bc) by defmult
.= f".(a1 * (f.b1 + c1)) by Z1,A4,X,defmultf
.= addemb(f,ab,ac) by defaddf,Z1,A7,A2,A9
.= (addemb f).(ab,ac) by defadd
.= a*b + a*c by A1,A6,defemb;
end;
suppose Z1: not(the multF of T).(x,bc)
in rng f;
A9: not x = 0.K & not bc=0.K by X,A3,AS,Lm6,Z,Y;
A10: a*(b + c) = (multemb f).(x,bc) by A3,defemb
.= multemb(f,x,bc) by defmult
.= a1 * (f.b1 + c1) by X,A4,Z1,A9,defmultf
.= a1 * f.b1 + a1 * c1 by VECTSP_1:def 7;
per cases;
suppose Z2: (the multF of T).(x,z) in rng f;
A7: a*c = (multemb f).(x,z) by defemb
.= multemb(f,x,z) by defmult
.= f".(a1 * c1) by X,Z2,Z,defmultf;
then
reconsider ac = f".(a1*c1) as Element of carr f by defemb;
a1 * c1 in dom(f") by Z2,FUNCT_1:33; then
f".(a1*c1) in rng(f") by FUNCT_1:def 3;
then
reconsider ac1 = ac as Element of K;
a*b + a*c = (addemb f).(ab,ac)
by A1,A7,defemb
.= addemb(f,ab,ac) by defadd
.= a1 * f.b1 + f.ac1 by defaddf,A2;
hence thesis by A10,Z2,FUNCT_1:35;
end;
suppose Z2: not(the multF of T).(x,z)
in rng f;
A9: a * c = (multemb f).(x,z) by defemb
.= multemb(f,x,z) by defmult
.= a1 * c1 by X,Z2,A,BC,Z,defmultf;
then reconsider ac = a1*c1 as Element of carr f by defemb;
A8: not ac in [#]K by AS,XBOOLE_0:def 4;
thus a*b+a*c = (addemb f).(ab,ac)
by A1,A9,defemb
.= addemb(f,ab,ac) by defadd
.= a*(b + c) by defaddf,A2,A7,A8,Z1,A10;
end;
end;
end;
end;
suppose Y: not y in [#]K; then
reconsider b1 = b as Element of T by Lm1;
per cases;
suppose Z: z in [#]K; then
reconsider c1 = c as Element of K;
B1: b + c = b1 + f.c1 by AS,Y,Z,Lm6; then
reconsider bc = b1 + f.c1 as Element of carr f by defemb;
B2: not bc in [#]K by Y,Z,AS,Lm6,B1;
B3: a * c = a1 * f.c1 by AS,X,Z,BC,Lm10; then
reconsider ac = a1 * f.c1 as Element of carr f by defemb;
B4: not ac in [#]K by B3,X,Z,BC,AS,Lm10;
per cases;
suppose Z1: not(the multF of T).(x,y)
in rng f;
B5: a * b = (multemb f).(x,y) by defemb
.= multemb(f,x,y) by defmult
.= a1 * b1 by Z1,X,Y,A,BC,defmultf;
then reconsider ab = a1 * b1 as Element of carr f by defemb;
B6: not ab in [#]K by AS,XBOOLE_0:def 4;
Z3: (the addF of T).(ab,ac)=a1*b1 + a1*f.c1
.= a1 * (b1 + f.c1) by VECTSP_1:def 7
.= (the multF of T).(x,bc);
per cases;
suppose Z2: (the multF of T).(x,bc)
in rng f;
thus a*(b + c)=(multemb f).(x,bc)
by B1,defemb
.= multemb(f,x,bc) by defmult
.= f".(a1*(b1 + f.c1))
by Z2,B2,X,defmultf
.= addemb(f,ab,ac)
by defaddf,Z2,Z3,B4,B6
.= (addemb f).(ab,ac) by defadd
.= a*b + a*c by B3,B5,defemb;
end;
suppose Z2: not(the multF of T).(x,bc)
in rng f;
B7: x <> 0.K & bc <> 0.K
by X,Y,Z,AS,Lm6,B1;
thus a*(b + c)=
(multemb f).(x,bc) by B1,defemb
.= multemb(f,x,bc) by defmult
.= a1*(b1 + f.c1)
by B7,X,B2,Z2,defmultf
.= addemb(f,ab,ac)
by defaddf,Z2,Z3,B4,B6
.= (addemb f).(ab,ac) by defadd
.= a*b + a*c by B3,B5,defemb;
end;
end;
suppose Z1: (the multF of T) .(x,y)
in rng f;
B5: a * b = (multemb f).(x,y) by defemb
.= multemb(f,x,y) by defmult
.= f".(a1 * b1) by Z1,X,Y,defmultf;
a1 * b1 in dom(f") by Z1,FUNCT_1:33;
then
f".(a1*b1) in rng(f")
by FUNCT_1:def 3; then
reconsider ab1 = f".(a1*b1) as Element of K;
reconsider ab = ab1 as Element of carr f by B5,defemb;
(the addF of T).(f.ab,ac)
in [#]T \ rng f by Lm3,B4; then
B7: not(the addF of T).(f.ab,ac) in rng f
by XBOOLE_0:def 5;
B9: now assume (the multF of T).(x,bc)
in rng f; then
consider yy being object such that
C1: yy in dom f & f.yy = a1*(b1+f.c1)
by FUNCT_1:def 3;
f.yy = a1*b1 + a1*f.c1
by C1,VECTSP_1:def 7
.= f.ab1 + a1*f.c1 by Z1,FUNCT_1:35;
hence contradiction
by B7,C1,FUNCT_1:def 3;
end;
B10: a <> 0.K & bc <> 0.K
by X,Y,Z,AS,Lm6,B1;
thus a*b + a*c = (addemb f).(ab,ac)
by B5,B3,defemb
.= addemb(f,ab,ac) by defadd
.= f.ab1 + a1 * f.c1 by defaddf,B4
.= a1*b1 + a1*f.c1 by Z1,FUNCT_1:35
.= a1*(b1 + f.c1) by VECTSP_1:def 7
.= multemb(f,x,bc)
by B10,X,B2,B9,defmultf
.= (multemb f).(x,bc) by defmult
.= a * (b + c) by B1,defemb;
end;
end;
suppose Z: not z in [#]K; then
reconsider c1 = c as Element of T by Lm1;
per cases;
suppose Z1:(the addF of T).(y,z)
in rng f;
B1: b + c = (addemb f).(y,z) by defemb
.= addemb(f,y,z) by defadd
.= f".(b1 + c1) by Y,Z,Z1,defaddf;
b1 + c1 in dom(f") by Z1,FUNCT_1:33;
then
f".(b1+c1) in rng(f") by FUNCT_1:def 3;
then
reconsider bc1 = f".(b1+c1) as Element of K;
reconsider bc = bc1 as Element of carr f by B1,defemb;
B0: dom f = [#]K by FUNCT_2:def 1;
per cases;
suppose B5: bc = 0.K; then
B2: b1 + c1 = 0.T by Z1,Th2;
B3: a*(b + c) = (multemb f).(x,bc)
by B1,defemb
.= multemb(f,x,bc) by defmult
.= 0.K by B5,defmultf;
A6: a1*b1 + a1*c1 = a1*0.T
by B2,VECTSP_1:def 7
.= f.(0.K) by RING_2:6; then
A7: a1*b1 + a1*c1 in rng f
by B0,FUNCT_1:3;
per cases;
suppose Z2:(the multF of T).(x,y)
in rng f;
B4: a*b = (multemb f).(x,y) by defemb
.= multemb(f,x,y) by defmult
.= f".(a1 * b1) by Y,X,Z2,defmultf;
a1*b1 in dom(f") by Z2,FUNCT_1:33;
then
f".(a1*b1) in rng(f")
by FUNCT_1:def 3;then
reconsider ab1 = f".(a1*b1) as Element of K;
reconsider ab = ab1 as Element of carr f by B4,defemb;
U: f.(0.K-ab1) = f.(0.K)-f.ab1
by RING_2:8
.= (a1*b1+a1*c1)-a1*b1
by A6,Z2,FUNCT_1:35
.= a1*c1 + (a1*b1 - a1*b1)
by RLVECT_1:def 3
.= a1 * c1 + 0.T by RLVECT_1:15
.= (the multF of T).(x,z); then
Z3: (the multF of T).(x,z) in rng f
by B0,FUNCT_1:def 3;
B5: a*c = (multemb f).(x,z) by defemb
.= multemb(f,x,z) by defmult
.= f".(a1 * c1) by Z,X,Z3,defmultf;
B11: a1*c1 in rng f by U,B0,FUNCT_1:def 3;
then
a1*c1 in dom(f") by FUNCT_1:33; then
f".(a1*c1) in rng(f")
by FUNCT_1:def 3;then
reconsider ac1 = f".(a1*c1) as Element of K;
reconsider ac = ac1 as Element of carr f by B5,defemb;
thus a*b + a*c = (addemb f).(ab,ac)
by B4,B5,defemb
.= addemb(f,ab,ac) by defadd
.= ab1 + ac1 by defaddf
.= f".(a1*b1 + a1*c1) by B11,Z2,Th1
.= a*(b + c) by A6,B3,B0,FUNCT_1:34;
end;
suppose Z2:not(the multF of T).(x,y)
in rng f;
B4: a*b = (multemb f).(x,y) by defemb
.= multemb(f,x,y) by defmult
.= a1*b1 by A,BC,Y,X,Z2,defmultf;
a1*b1 in [#]T \ rng f
by Z2,XBOOLE_0:def 5; then
reconsider ab=a1*b1 as Element of carr f by XBOOLE_0:def 3;
B9: not ab in [#]K by AS,XBOOLE_0:def 4;
Z3: now assume Z3:(the multF of T).(x,z)
in rng f;
B5: a*c = (multemb f).(x,z) by defemb
.= multemb(f,x,z) by defmult
.= f".(a1 * c1) by Z,X,Z3,defmultf;
a1*c1 in dom(f") by Z3,FUNCT_1:33;
then
f".(a1*c1) in rng(f")
by FUNCT_1:def 3;then
reconsider ac1 = f".(a1*c1) as Element of K;
reconsider ac = ac1 as Element of carr f by B5,defemb;
B12: (the addF of T).(ab,f.ac)
in [#]T\rng f by B9,Lm2;
(the addF of T).(ab,f.ac)=a1*b1+a1*c1
by Z3,FUNCT_1:35;
hence contradiction
by B12,A7,XBOOLE_0:def 5;
end;
B5: a * c = (multemb f).(x,z) by defemb
.= multemb(f,x,z) by defmult
.= a1 * c1 by A,BC,Z,X,Z3,defmultf;
a1*c1 in [#]T \ rng f
by Z3,XBOOLE_0:def 5; then
reconsider ac=a1*c1 as Element of carr f by XBOOLE_0:def 3;
B13: not ac in [#]K by AS,XBOOLE_0:def 4;
thus a * b + a * c = (addemb f).(ab,ac)
by B4,B5,defemb
.= addemb(f,ab,ac) by defadd
.= f".(a1*b1 + a1*c1)
by A7,B9,B13,defaddf
.= a * (b + c) by A6,B3,B0,FUNCT_1:34;
end;
end;
suppose B5: bc <> 0.K;
then B12: (the multF of T).(x,f.bc) in [#]T \ rng f
by X,Lm4;
B3: a*(b + c) = (multemb f).(x,bc) by B1,defemb
.= multemb(f,x,bc) by defmult
.= a1 * f.bc1 by B5,X,defmultf
.= a1 * (b1 + c1) by Z1,FUNCT_1:35
.= a1 * b1 + a1 * c1 by VECTSP_1:def 7;
per cases;
suppose Z2: (the multF of T).(x,y) in rng f;
B4: a * b = (multemb f).(x,y) by defemb
.= multemb(f,x,y) by defmult
.= f".(a1 * b1) by Y,X,Z2,defmultf;
a1 * b1 in dom(f") by Z2,FUNCT_1:33; then
f".(a1*b1) in rng(f") by FUNCT_1:def 3; then
reconsider ab1 = f".(a1*b1) as Element of K;
reconsider ab = ab1 as Element of carr f by B4,defemb;
B7: now assume (the multF of T).(x,z) in rng f;
then
consider xx being object such that
C1: xx in dom f & f.xx=a1*c1 by FUNCT_1:def 3;
reconsider xx as Element of K by C1;
consider yy being object such that
C2: yy in dom f & f.yy=a1*b1
by Z2,FUNCT_1:def 3;
reconsider yy as Element of K by C2;
C3: dom f = [#]K by FUNCT_2:def 1;
(the multF of T).(x,f.bc) = a1*(b1 + c1)
by Z1,FUNCT_1:35
.= f.yy + f.xx by C1,C2,VECTSP_1:def 7
.= f.(xx + yy) by VECTSP_1:def 20; then
(the multF of T).(x,f.bc) in rng f
by C3,FUNCT_1:def 3;
hence contradiction by B12,XBOOLE_0:def 5;
end;
B8: a*c = (multemb f).(x,z) by defemb
.= multemb(f,x,z) by defmult
.= a1 * c1 by Z,B7,A,BC,X,defmultf;
a1*c1 in [#]T \ rng f
by B7,XBOOLE_0:def 5; then
reconsider ac=a1*c1 as Element of carr f by XBOOLE_0:def 3;
B9: not ac in [#]K by AS,XBOOLE_0:def 4;
thus a*b + a*c = (addemb f).(ab,ac)
by B4,B8,defemb
.= addemb(f,ab,ac) by defadd
.= f.ab1 + a1 * c1 by defaddf,B9
.= a * (b + c) by B3,Z2,FUNCT_1:35;
end;
suppose Z2:not(the multF of T).(x,y) in rng f;
B4: a*b = (multemb f).(x,y) by defemb
.= multemb(f,x,y) by defmult
.= a1 * b1 by A,BC,Y,X,Z2,defmultf;
then
reconsider ab = a1 * b1 as Element of carr f by defemb;
B5: not ab in [#]K by AS,XBOOLE_0:def 4;
per cases;
suppose Z3:(the multF of T).(x,z) in rng f;
B8: a*c = (multemb f).(x,z) by defemb
.= multemb(f,x,z) by defmult
.= f".(a1 * c1) by Z,X,Z3,defmultf;
a1*c1 in dom(f") by Z3,FUNCT_1:33; then
f".(a1*c1) in rng(f") by FUNCT_1:def 3;then
reconsider ac1 = f".(a1*c1) as Element of K;
reconsider ac = ac1 as Element of carr f by B8,defemb;
thus a*b + a*c = (addemb f).(ab,ac)
by B4,B8,defemb
.= addemb(f,ab,ac) by defadd
.= a1 * b1 + f.ac1 by defaddf,B5
.= a * (b + c) by B3,Z3,FUNCT_1:35;
end;
suppose Z3:not(the multF of T).(x,z)
in rng f;
B8: a*c = (multemb f).(x,z) by defemb
.= multemb(f,x,z) by defmult
.= a1 * c1 by Z,Z3,A,BC,X,defmultf;
a1*c1 in [#]T \ rng f
by Z3,XBOOLE_0:def 5; then
reconsider ac=a1*c1 as Element of carr f by XBOOLE_0:def 3;
B9: not ac in [#]K by AS,XBOOLE_0:def 4;
(the multF of T).(x,f.bc) = a1*(b1+c1)
by Z1,FUNCT_1:35
.= a1*b1 + a1*c1 by VECTSP_1:def 7
.= (the addF of T).(ab,ac); then
B10: not(the addF of T).(ab,ac) in rng f
by B12,XBOOLE_0:def 5;
thus a*b + a*c = (addemb f).(ab,ac)
by B4,B8,defemb
.= addemb(f,ab,ac) by defadd
.= a * (b + c) by defaddf,B9,B5,B10,B3;
end;
end;
end;
end;
suppose Z1: not(the addF of T).(y,z) in rng f;
B1: b + c = (addemb f).(y,z) by defemb
.= addemb(f,y,z) by defadd
.= b1 + c1 by Y,Z,Z1,defaddf;
b1 + c1 in ([#]T) \ (rng f)
by Z1,XBOOLE_0:def 5; then
reconsider bc = b1+c1 as Element of carr f by XBOOLE_0:def 3;
B2: not bc in [#]K by AS,XBOOLE_0:def 4;
B5: not bc = 0.K by AS,XBOOLE_0:def 4;
per cases;
suppose Z2: (the multF of T).(x,bc) in rng f;
B3: a*(b + c) = (multemb f).(x,bc) by B1,defemb
.= multemb(f,x,bc) by defmult
.= f".(a1 * (b1 + c1)) by Z2,B2,X,defmultf
.= f".(a1 * b1 + a1 * c1) by VECTSP_1:def 7;
per cases;
suppose Z3: (the multF of T).(x,y) in rng f;
B4: a*b = (multemb f).(x,y) by defemb
.= multemb(f,x,y) by defmult
.= f".(a1*b1) by Y,X,Z3,defmultf;
a1 * b1 in dom(f") by Z3,FUNCT_1:33; then
f".(a1*b1) in rng(f") by FUNCT_1:def 3;then
reconsider ab1 = f".(a1*b1) as Element of K;
reconsider ab = ab1 as Element of carr f by B4,defemb;
B6: (the multF of T).(x,z) in rng f
proof
(the multF of T).(x,bc) = a1 * (b1 + c1)
.= a1 * b1 + a1 * c1 by VECTSP_1:def 7;then
consider xx being object such that
C1: xx in dom f & f.xx = a1*b1+a1*c1
by Z2,FUNCT_1:def 3;
reconsider xx as Element of K by C1;
consider yy being object such that
C2: yy in dom f & f.yy = a1*b1
by Z3,FUNCT_1:def 3;
reconsider yy as Element of K by C2;
C3: f.(xx-yy) = f.xx - f.yy by RING_2:8
.= a1*c1 + (a1*b1 + -(a1*b1))
by C1,C2,RLVECT_1:def 3
.= a1*c1 + 0.T by RLVECT_1:5;
[#]K = dom f by FUNCT_2:def 1;
hence thesis by C3,FUNCT_1:def 3;
end;
B7: a*c = (multemb f).(x,z) by defemb
.= multemb(f,x,z) by defmult
.= f".(a1 * c1) by X,Z,B6,defmultf;
a1*c1 in dom(f") by B6,FUNCT_1:33; then
f".(a1*c1) in rng(f") by FUNCT_1:def 3; then
reconsider ac1 = f".(a1*c1) as Element of K;
reconsider ac = ac1 as Element of carr f by B7,defemb;
reconsider abr = a1*b1 as Element of (rng f) by Z3;
reconsider acr = a1*c1 as Element of (rng f) by B6;
B8: f".abr + f".acr = f".(a1*b1 + a1*c1) by Th1;
thus a*b + a*c = (addemb f).(ab,ac)
by B4,B7,defemb
.= addemb(f,ab,ac) by defadd
.= a*(b+c) by defaddf,B8,B3;
end;
suppose Z3:not(the multF of T).(x,y) in rng f;
B4: a * b = (multemb f).(x,y) by defemb
.= multemb(f,x,y) by defmult
.= a1 * b1 by A,BC,Y,X,Z3,defmultf;
a1*b1 in [#]T \ rng f by Z3,XBOOLE_0:def 5;
then
reconsider ab = a1*b1 as Element of carr f by XBOOLE_0:def 3;
reconsider ab1 = ab as Element of T;
B6: not ab in [#]K by AS,XBOOLE_0:def 4;
Z4: now assume
Z4a: (the multF of T).(x,z) in rng f;
B7: a * c = (multemb f).(x,z) by defemb
.= multemb(f,x,z) by defmult
.= f".(a1 * c1) by Z4a,X,Z,defmultf;
a1 * c1 in dom(f") by Z4a,FUNCT_1:33; then
f".(a1*c1) in rng(f") by FUNCT_1:def 3;then
reconsider ac1 = f".(a1*c1) as Element of K;
reconsider ac = ac1 as Element of carr f by B7,defemb;
U: (the addF of T).(ab,f.ac) in ([#]T)\(rng f) by B6,Lm2;
f.ac1 = a1 * c1 by Z4a,FUNCT_1:35; then
ab1 + f.ac1 = a1*(b1 + c1) by VECTSP_1:def 7
.= (the multF of T).(x,bc);
hence contradiction by U,Z2,XBOOLE_0:def 5;
end;
B7: a * c = (multemb f).(x,z) by defemb
.= multemb(f,x,z) by defmult
.= a1 * c1 by Z4,A,BC,X,Z,defmultf;
a1*c1 in [#]T \ rng f by Z4,XBOOLE_0:def 5;
then
reconsider ac = a1*c1 as Element of carr f by XBOOLE_0:def 3;
reconsider ac1 = ac as Element of T;
B9: not ac in [#]K by AS,XBOOLE_0:def 4;
B10: a1*b1 + a1*c1=a1*(b1 + c1) by VECTSP_1:def 7
.= (the multF of T).(x,bc);
thus a*b + a*c = (addemb f).(ab,ac)
by B4,B7,defemb
.= addemb(f,ab,ac) by defadd
.= a * (b + c) by defaddf,B6,B9,B10,Z2,B3;
end;
end;
suppose
Z2: not (the multF of T).(x,bc) in rng f;
B3: a * (b + c) = (multemb f).(x,bc) by B1,defemb
.= multemb(f,x,bc) by defmult
.= a1 * (b1 + c1) by A,Z2,B2,B5,X,defmultf
.= a1 * b1 + a1 * c1 by VECTSP_1:def 7;
per cases;
suppose
Z3: (the multF of T).(x,y) in rng f;
B4: a * b = (multemb f).(x,y) by defemb
.= multemb(f,x,y) by defmult
.= f".(a1 * b1) by Y,X,Z3,defmultf;
a1 * b1 in dom(f") by Z3,FUNCT_1:33; then
f".(a1 * b1) in rng(f") by FUNCT_1:def 3;
then
reconsider ab1 = f".(a1*b1) as Element of K;
reconsider ab = ab1 as Element of carr f by B4,defemb;
Z4: now assume (the multF of T).(x,z) in rng f;
then
consider yy being object such that
C1: yy in dom f & f.yy=a1*c1 by FUNCT_1:def 3;
reconsider yy as Element of K by C1;
C2: (the multF of T).(x,bc) = a1 * (b1 + c1)
.= a1 * b1 + a1 * c1 by VECTSP_1:def 7;
C3: f.(ab1 + yy)=f.ab1 + f.yy by VECTSP_1:def 20
.= a1 * b1 + a1 * c1 by C1,Z3,FUNCT_1:35;
[#]K = dom f by FUNCT_2:def 1;
hence contradiction by C3,C2,Z2,FUNCT_1:def 3;
end;
B5: a * c = (multemb f).(x,z) by defemb
.= multemb(f,x,z) by defmult
.= a1 * c1 by A,BC,Z,X,Z4,defmultf;
a1 * c1 in [#]T \ rng f by Z4,XBOOLE_0:def 5;
then
reconsider ac = a1*c1 as Element of carr f by XBOOLE_0:def 3;
B9: not ac in [#]K by AS,XBOOLE_0:def 4;
thus a*b + a*c = (addemb f).(ab,ac)
by B4,B5,defemb
.= addemb(f,ab,ac) by defadd
.= f.ab1+a1*c1 by defaddf,B9
.= a*(b+c) by B3,Z3,FUNCT_1:35;
end;
suppose Z3: not(the multF of T).(x,y) in rng f;
B4: a*b = (multemb f).(x,y) by defemb
.= multemb(f,x,y) by defmult
.= a1*b1 by A,BC,Y,X,Z3,defmultf;
a1*b1 in [#]T \ rng f by Z3,XBOOLE_0:def 5;
then
reconsider ab=a1*b1 as Element of carr f by XBOOLE_0:def 3;
B9: not ab in [#]K by AS,XBOOLE_0:def 4;
per cases;
suppose Z4:(the multF of T).(x,z) in rng f;
B5: a*c = (multemb f).(x,z) by defemb
.= multemb(f,x,z) by defmult
.= f".(a1 * c1) by Z,X,Z4,defmultf;
a1*c1 in dom(f") by Z4,FUNCT_1:33; then
f".(a1 * c1) in rng(f") by FUNCT_1:def 3;
then
reconsider ac1 = f".(a1*c1) as Element of K;
reconsider ac = ac1 as Element of carr f by B5,defemb;
thus a * b + a * c = (addemb f).(ab,ac)
by B4,B5,defemb
.= addemb(f,ab,ac) by defadd
.= a1*b1+f.ac1 by defaddf,B9
.= a * (b + c) by B3,Z4,FUNCT_1:35;
end;
suppose Z4: not (the multF of T).(x,z)
in rng f;
B5: a*c = (multemb f).(x,z) by defemb
.= multemb(f,x,z) by defmult
.= a1 * c1 by A,BC,Z,X,Z4,defmultf;
a1*c1 in [#]T \ rng f by Z4,XBOOLE_0:def 5;
then
reconsider ac = a1*c1 as Element of carr f by XBOOLE_0:def 3;
B19: not ac in [#]K by AS,XBOOLE_0:def 4;
B20: (the addF of T).(ab,ac) = a1*b1+a1*c1
.= a1*(b1+c1) by VECTSP_1:def 7
.= (the multF of T).(x,bc);
thus a*b + a*c = (addemb f).(ab,ac)
by B4,B5,defemb
.= addemb(f,ab,ac) by defadd
.= a * (b + c) by Z2,B3,B9,B19,B20,defaddf;
end;
end;
end;
end;
end;
end;
end;
end;
end;
thus
(b+c)*a = a*(b+c) by GROUP_1:def 12
.= b*a + a*c by I,GROUP_1:def 12
.= b*a + c*a by GROUP_1:def 12;
end;
end;
hence thesis;
end;
theorem Th10:
for f being Monomorphism of K,F st K,F are_disjoint
holds embField f is almost_left_invertible
proof
let f be Monomorphism of K,F;
assume AS: K,F are_disjoint;
now let a be Element of embField f;
assume a <> 0.(embField f); then
X: a <> 0.K by defemb;
reconsider x = a as Element of carr f by defemb;
per cases;
suppose x in [#]K; then
reconsider a1 = a as Element of K;
a1 is left_invertible by X,ALGSTR_0:def 39; then
consider b1 being Element of K such that
B: b1 * a1 = 1.K;
reconsider y = b1 as Element of carr f by XBOOLE_0:def 3;
reconsider b = y as Element of embField f by defemb;
b*a = a*b by GROUP_1:def 12 .= a1*b1 by Lm11
.= b1*a1 by GROUP_1:def 12 .= 1.(embField f) by B,defemb;
hence a is left_invertible;
end;
suppose A: not x in [#]K; then
X: x in [#]F & not x in rng f by Lm1;
reconsider a1 = a as Element of F by A,Lm1;
Z: dom f = [#]K by FUNCT_2:def 1;
f.(0.K) = 0.F by RING_2:6; then
0.F in rng f by Z,FUNCT_1:def 3; then
a1 is left_invertible by X,ALGSTR_0:def 39; then
consider b1 being Element of F such that
B: b1 * a1 = 1.F;
U: b1 <> 0.F & a1 <> 0.F by B;
(the multF of F).(a1,b1) = a1 * b1
.= 1_F by B,GROUP_1:def 12 .= f.(1_K) by GROUP_1:def 13; then
D: (the multF of F).(a1,b1) in rng f by Z,FUNCT_1:3; then
D1: not(the multF of F).(a1,b1) in [#]F \ rng f by XBOOLE_0:def 5;
per cases;
suppose b1 in rng f; then
consider b1r being object such that
C1: b1r in dom f & f.b1r = b1 by FUNCT_1:def 3;
reconsider b1r as Element of K by C1;
[#]embField f = carr f by defemb; then
reconsider bx = b1r as Element of embField f by XBOOLE_0:def 3;
reconsider y = bx as Element of carr f by defemb;
C4: bx <> 0.K by U,C1,RING_2:6;
[#]embField f = carr f by defemb;
hence a is left_invertible by Lm4,A,D1,C1,C4;
end;
suppose not b1 in rng f; then
b1 in ([#]F) \ (rng f) by XBOOLE_0:def 5; then
b1 is Element of carr f by XBOOLE_0:def 3; then
reconsider b = b1 as Element of embField f by defemb;
E: not b in [#]K by AS,XBOOLE_0:def 4;
b*a = a*b by GROUP_1:def 12 .= f".(a1*b1) by A,D,E,Lm13
.= f".(1_F) by B,GROUP_1:def 12 .= 1.K by Th3
.= 1.(embField f) by defemb;
hence a is left_invertible;
end;
end;
end;
hence thesis;
end;
theorem
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 embField f, F means :defiso:
(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
proof
defpred P[object,object] means
(not $1 in K & $2 = $1) or ($1 in K & $2 = f.$1);
M: for x being object st x in [#]embField f
ex y being object st y in [#]F & P[x,y]
proof
let x be object;
assume M0: x in [#]embField f; then
reconsider x1 = x as Element of embField f;
per cases;
suppose M1: x in K; then
reconsider a = x as Element of K;
take b = f.a;
thus b in [#]F;
thus thesis by M1;
end;
suppose M1: not x in K;
take x;
reconsider x1 = x as Element of carr f by M0,defemb;
x1 in [#]F & not x1 in rng f by M1,Lm1;
hence x in [#]F;
thus thesis by M1;
end;
end;
consider g being Function of [#](embField f), [#]F such that
N: for x being object st x in [#]embField f holds P[x,g.x]
from FUNCT_2:sch 1(M);
reconsider g as Function of embField f,F;
take g;
thus thesis by N;
end;
uniqueness
proof
let g1,g2 be Function of embField f, F;
assume that
A1: (for a being Element of embField f st not a in K holds g1.a = a) &
(for a being Element of embField f st a in K holds g1.a = f.a) and
A2: (for a being Element of embField f st not a in K holds g2.a = a) &
(for a being Element of embField f st a in K holds g2.a = f.a);
now let o be object;
assume o in [#]embField f; then
reconsider a = o as Element of embField f;
per cases;
suppose A3: a in K; then
g1.a = f.a by A1 .= g2.a by A3,A2;
hence g1.o = g2.o;
end;
suppose A3: not a in K; then
g1.a = a by A1 .= g2.a by A3,A2;
hence g1.o = g2.o;
end;
end;
hence g1 = g2;
end;
end;
registration
let K be Field,
F be K-monomorphic Field;
let f be Monomorphism of K,F;
cluster emb_iso f -> unity-preserving;
coherence
proof
set g = emb_iso f, R = embField f;
1.R = 1.K by defemb; then
1.R in K; then
g.(1_R) = f.(1.R) by defiso .= f.(1_K) by defemb .= 1_F by GROUP_1:def 13;
hence g is unity-preserving;
end;
end;
theorem Th11:
for f being Monomorphism of K,F st K,F are_disjoint
holds emb_iso f is additive
proof
let f be Monomorphism of K,F;
assume AS: K,F are_disjoint;
set g = emb_iso f, R = embField f;
now let a,b be Element of R;
reconsider x = a, y = b as Element of carr f by defemb;
per cases;
suppose A: x in [#]K & y in [#]K; then
reconsider a1 = a, b1 = b as Element of K;
B: a + b = (addemb f).(x,y) by defemb .= addemb(f,x,y) by defadd
.= a1 + b1 by defaddf;
a in K & b in K by A; then
C: g.a = f.a & g.b = f.b by defiso;
a + b in K by B;
hence g.(a+b) = f.(a+b) by defiso .= g.a + g.b by C,B,VECTSP_1:def 20;
end;
suppose A: x in [#]K & not y in [#]K; then
reconsider a1 = a as Element of K;
reconsider b1 = b as Element of F by A,Lm1;
reconsider fa = f.a1 as Element of F;
B: a + b = (addemb f).(x,y) by defemb .= addemb(f,x,y) by defadd
.= fa + b1 by A,defaddf;
a in K & not b in K by A; then
C: g.a = f.a & g.b = b by defiso;
not fa + b1 in K by AS,XBOOLE_0:def 4;
hence g.(a+b) = g.a + g.b by C,B,defiso;
end;
suppose A: y in [#]K & not x in [#]K; then
reconsider b1 = b as Element of K;
reconsider a1 = a as Element of F by A,Lm1;
reconsider fb = f.b1 as Element of F;
B: a + b = (addemb f).(x,y) by defemb .= addemb(f,x,y) by defadd
.= a1 + fb by A,defaddf;
not a in K & b in K by A; then
C: g.a = a & g.b = f.b by defiso;
not a1 + fb in K by AS,XBOOLE_0:def 4;
hence g.(a+b) = g.a + g.b by C,B,defiso;
end;
suppose A: not x in [#]K & not y in [#]K &
(the addF of F).(x,y) in rng f; then
reconsider a1 = a, b1 = b as Element of F by Lm1;
C: a + b = (addemb f).(x,y) by defemb .= addemb(f,x,y) by defadd
.= (f").(a1 + b1) by A,defaddf;
not a in K & not b in K by A; then
D: g.a = a & g.b = b by defiso;
a1 + b1 in dom(f") by A,FUNCT_1:33; then
(f").(a1 + b1) in rng(f") by FUNCT_1:3; then
(f").(a1 + b1) in K;
hence g.(a+b) = f.((f").(a1 + b1)) by C,defiso
.= g.a + g.b by D,A,FUNCT_1:35;
end;
suppose A: not x in [#]K & not y in [#]K &
not (the addF of F).(x,y) in rng f; then
reconsider a1 = a, b1 = b as Element of F by Lm1;
C: a + b = (addemb f).(x,y) by defemb .= addemb(f,x,y) by defadd
.= a1 + b1 by A,defaddf;
not a in K & not b in K by A; then
D: g.a = a & g.b = b by defiso;
not a1 + b1 in K by AS,XBOOLE_0:def 4;
hence g.(a+b) = g.a + g.b by D,C,defiso;
end;
end;
hence g is additive;
end;
theorem Th12:
for f being Monomorphism of K,F st K,F are_disjoint
holds emb_iso f is multiplicative
proof
let f be Monomorphism of K,F;
assume
AS: K,F are_disjoint;
set g = emb_iso f, R = embField f;
now let a,b be Element of R;
reconsider x = a, y = b as Element of carr f by defemb;
per cases;
suppose
A1: x in [#]K & y in [#]K; then
reconsider a1 = a, b1 = b as Element of K;
B: a * b = a1 * b1 by Lm11;
a in K & b in K by A1; then
C: g.a = f.a & g.b = f.b by defiso;
a * b in K by B;
hence g.(a*b) = f.(a*b) by defiso .= g.a * g.b by C,B,GROUP_6:def 6;
end;
suppose
A2: x = 0.K or y = 0.K;
B: a*b = (multemb f).(x,y) by defemb .= multemb(f,x,y) by defmult
.= 0.K by A2,defmultf;
X: 0.K in K;
per cases by A2;
suppose x = 0.K; then
C: g.a = f.(0.K) by X,defiso .= 0.F by RING_2:6;
thus g.(a*b) = f.(0.K) by B,X,defiso .= g.a * g.b by C,RING_2:6;
end;
suppose y = 0.K; then
C: g.b = f.(0.K) by X,defiso .= 0.F by RING_2:6;
thus g.(a*b) = f.(0.K) by B,X,defiso .= g.a * g.b by C,RING_2:6;
end;
end;
suppose A: x in [#]K & x<>0.K ¬ y in [#]K; then
reconsider a1 = a as Element of K;
reconsider b1 = b as Element of F by A,Lm1;
reconsider fa = f.a1 as Element of F;
B: a * b = fa * b1 by AS,A,Lm10;
a in K & not b in K by A; then
C: g.a = f.a & g.b = b by defiso;
not a * b in K by AS,A,Lm10;
hence g.(a*b) = g.a * g.b by B,C,defiso;
end;
suppose A: y in [#]K & y<>0.K ¬ x in [#]K; then
reconsider b1 = b as Element of K;
reconsider a1 = a as Element of F by A,Lm1;
reconsider fb = f.b1 as Element of F;
B: a * b = a1 * fb by AS,A,Lm10;
b in K & not a in K by A; then
C: g.a = a & g.b = f.b by defiso;
not a * b in K by AS,A,Lm10;
hence g.(a*b) = g.a * g.b by B,C,defiso;
end;
suppose A: not x in [#]K & not y in [#]K & (the multF of F).(x,y) in rng f;
then
reconsider a1 = a, b1 = b as Element of F by Lm1;
C: a * b = (f").(a1 * b1) by A,Lm13;
not a in K & not b in K by A; then
D: g.a = a & g.b = b by defiso;
a1 * b1 in dom(f") by A,FUNCT_1:33; then
(f").(a1 * b1) in rng(f") by FUNCT_1:3; then
(f").(a1 * b1) in K;
hence g.(a*b)=f.((f").(a1*b1)) by C,defiso .= g.a*g.b by D,A,FUNCT_1:35;
end;
suppose A: not x in [#]K & not y in [#]K &
not((the multF of F).(x,y) in rng f); then
reconsider a1 = a, b1 = b as Element of F by Lm1;
C: a * b = a1 * b1 by AS,A,Lm12;
not a in K & not b in K by A; then
D: g.a = a & g.b = b by defiso;
not a1 * b1 in K by AS,XBOOLE_0:def 4;
hence g.(a*b) = g.a * g.b by D,C,defiso;
end;
end;
hence thesis;
end;
registration
let K be Field,
F be K-monomorphic Field;
let f be Monomorphism of K,F;
cluster emb_iso f -> one-to-one;
coherence
proof
set g = emb_iso f;
E: [#]embField f = carr f by defemb;
D: dom f = [#]K by FUNCT_2:def 1;
H: f is one-to-one;
now let x1,x2 be object;
assume A: x1 in dom g & x2 in dom g & g.x1 = g.x2; then
reconsider c = x2 as Element of embField f;
per cases;
suppose x1 in [#]K;
then reconsider a = x1 as Element of K;
a in K; then
B: f.a = g.a by A,defiso; then
C: g.a in rng f by D,FUNCT_1:def 3;
now assume C1: not x2 in K;
g.c = x2 by C1,defiso; then
not x2 in ([#]F)\(rng f) by C,A,XBOOLE_0:def 5;
hence contradiction by C1,A,E,XBOOLE_0:def 3;
end; then
reconsider b = x2 as Element of K;
b in K; then
f.b = f.a by A,B,defiso;
hence x1 = x2 by H,D;
end;
suppose Z: not x1 in [#]K;
reconsider a = x1 as Element of embField f by A;
not a in K by Z; then
B: g.a = a by defiso;
now assume C1: x2 in K; then
C2: x2 in dom f by FUNCT_2:def 1;
reconsider c = x2 as Element of embField f by A;
a = f.x2 by A,B,C1,defiso; then
a in rng f by C2,FUNCT_1:def 3; then
not a in ([#]F)\(rng f) by XBOOLE_0:def 5;
hence contradiction by Z,E,XBOOLE_0:def 3;
end;
hence x1 = x2 by A,B,defiso;
end;
end;
hence thesis;
end;
end;
theorem Th13:
for f being Monomorphism of K,F st K,F are_disjoint holds
emb_iso f is onto
proof
let f be Monomorphism of K,F;
assume
AS: K,F are_disjoint;
set g = emb_iso f;
E: [#]embField f = carr f by defemb;
F: dom g = [#]embField f by FUNCT_2:def 1;
A: now let o be object;
assume o in [#]F; then
reconsider u = o as Element of F;
per cases;
suppose u in rng f; then
consider y being object such that
B: y in dom f & f.y = u by FUNCT_1:def 3;
reconsider y as Element of K by B;
reconsider yy = y as Element of embField f by E,XBOOLE_0:def 3;
y in K; then g.yy = u by B,defiso;
hence o in rng g by F,FUNCT_1:3;
end;
suppose not u in rng f; then
u in ([#]F)\(rng f) by XBOOLE_0:def 5; then
reconsider uu = u as Element of embField f by E,XBOOLE_0:def 3;
not u in K by AS,XBOOLE_0:def 4; then
g.uu = u by defiso;
hence o in rng g by F,FUNCT_1:3;
end;
end;
for o being object st o in rng g holds o in [#]F;
hence g is onto by A,TARSKI:2;
end;
theorem Th14:
for f being Monomorphism of K,F st K,F are_disjoint
holds F, embField f are_isomorphic
proof
let f be Monomorphism of K,F;
assume AS: K,F are_disjoint;
set g = emb_iso f;
g is unity-preserving additive multiplicative by AS,Th11,Th12;
then g is isomorphism by AS,Th13,MOD_4:def 12;
hence thesis by QUOFIELD:def 23;
end;
theorem Th15:
for f being Monomorphism of K,F, E being Field st E = embField f holds
K is Subfield of E
proof
let f be Monomorphism of K,F, E be Field;
A2: [#]embField f = carr f by defemb;
assume
A1: E = embField f; then
[#]E = carr f by defemb; then
A3: [#]K c= [#]E by XBOOLE_0:def 3;
A4: dom the addF of E = [:[#]E,[#]E:] by FUNCT_2:def 1;
set g1 = (the addF of K), g2 = (the addF of E)|[:[#]K,[#]K:];
A5: dom g2 = dom(the addF of E) /\ [:[#]K,[#]K:] by RELAT_1:61
.= [:[#]K,[#]K:] by A3,ZFMISC_1:96,XBOOLE_1:28,A4
.= dom g1 by FUNCT_2:def 1;
now let x be set;
assume x in dom the addF of K; then
consider x1,x2 being object such that
A6: x1 in [#]K & x2 in [#]K & x = [x1,x2] by ZFMISC_1:def 2;
reconsider a = x1, b = x2 as Element of K by A6;
A7: [a,b] in [:[#]K,[#]K:] by ZFMISC_1:def 2;
reconsider a1=x1,b1=x2 as Element of embField f by A6,A2,XBOOLE_0:def 3;
((the addF of E)||[#]K).(a,b)=a1+b1 by A1,A7,FUNCT_1:49 .= a+b by Lm7;
hence (the addF of K).x = g2.x by A6;
end; then
A8: the addF of K = (the addF of E) || [#]K by A5;
set g1 = (the multF of K), g2 = (the multF of E)|[:[#]K,[#]K:];
A9: dom(the multF of E) = [:[#]E,[#]E:] by FUNCT_2:def 1;
A10: dom g2 = dom(the multF of E) /\ [:[#]K,[#]K:] by RELAT_1:61
.= [:[#]K,[#]K:] by A3,ZFMISC_1:96,XBOOLE_1:28,A9
.= dom g1 by FUNCT_2:def 1;
now let x be set;
assume x in dom (the multF of K); then
consider x1,x2 being object such that
A11: x1 in [#]K & x2 in [#]K & x = [x1,x2] by ZFMISC_1:def 2;
reconsider a = x1, b = x2 as Element of K by A11;
A12: [a,b] in [:[#]K,[#]K:] by ZFMISC_1:def 2;
reconsider a1=x1,b1=x2 as Element of embField f by A11,A2,XBOOLE_0:def 3;
((the multF of E)||[#]K).(a,b)=a1*b1 by A1,A12,FUNCT_1:49.=a*b by Lm11;
hence (the multF of K).x = g2.x by A11;
end; then
A13: the multF of K = (the multF of E) || [#]K by A10;
1.E = 1.K & 0.E = 0.K by defemb,A1;
hence thesis by A3,A8,A13,EC_PF_1:def 1;
end;
theorem Th16:
K,F are_disjoint implies
ex E being Field st E,F are_isomorphic & K is Subfield of E
proof
assume AS: K,F are_disjoint;
set f = the Monomorphism of K,F;
reconsider E = embField f as Field by AS,Th6,Th8,Th9,Th7,Th10;
take E;
thus thesis by AS,Th14,Th15;
end;
theorem
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
let K,F be Field;
assume AS: K,F are_disjoint;
now assume ex E being Field st E,F are_isomorphic & K is Subfield of E;
then consider E being Field such that
A: E,F are_isomorphic & K is Subfield of E;
K is Subring of E by A,RING_3:43; then
consider m being Function of K,E such that
B: m is RingHomomorphism monomorphism by RING_3:def 3,RING_3:71;
consider i being Function of E,F such that
C: i is RingIsomorphism by A,QUOFIELD:def 23;
set f = i * m;
f is linear by B,C,RINGCAT1:1;
hence F is K-monomorphic by B,C,RING_3:def 3;
end;
hence thesis by AS,Th16;
end;