let K be Field; for T being K -monomorphic comRing
for f being Monomorphism of K,T st K,T are_disjoint holds
embField f is add-associative
let T be K -monomorphic comRing; for f being Monomorphism of K,T st K,T are_disjoint holds
embField f is add-associative
let f be Monomorphism of K,T; ( K,T are_disjoint implies embField f is add-associative )
assume AS:
K,T are_disjoint
; embField f is add-associative
now for a, b, c being Element of (embField f) holds (a + b) + c = a + (b + c)let a,
b,
c be
Element of
(embField f);
(b1 + b2) + b3 = b1 + (b2 + b3)reconsider x =
a,
y =
b,
z =
c as
Element of
carr f by defemb;
per cases
( x in [#] K or not x in [#] K )
;
suppose X:
x in [#] K
;
(b1 + b2) + b3 = b1 + (b2 + b3)then reconsider a1 =
a as
Element of
K ;
per cases
( y in [#] K or not y in [#] K )
;
suppose Y:
y in [#] K
;
(b1 + b2) + b3 = b1 + (b2 + b3)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
( z in [#] K or not z in [#] K )
;
suppose Z:
not
z in [#] K
;
(b1 + b2) + b3 = b1 + (b2 + b3)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
;
verum end; end; suppose Y:
not
y in [#] K
;
(b1 + b2) + b3 = b1 + (b2 + b3)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
( z in [#] K or not z in [#] K )
;
suppose Z:
z in [#] K
;
(b1 + b2) + b3 = b1 + (b2 + b3)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
;
verum end; suppose Z:
not
z in [#] K
;
(b1 + b2) + b3 = b1 + (b2 + b3)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
( the addF of T . (ab,z) in rng f or not the addF of T . (ab,z) in rng f )
;
suppose K:
the
addF of
T . (
ab,
z)
in rng f
;
(b1 + b2) + b3 = b1 + (b2 + b3)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 the addF of T . (y,z) in rng fassume K7:
not the
addF of
T . (
y,
z)
in rng f
;
contradictionX4:
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;
verum 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
;
verum end; suppose K0:
not the
addF of
T . (
ab,
z)
in rng f
;
(b1 + b2) + b3 = b1 + (b2 + b3)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
;
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
;
verum end; end; end; end; suppose X4:
not
x in [#] K
;
(b1 + b2) + b3 = b1 + (b2 + b3)then reconsider a1 =
a as
Element of
T by Lm1;
per cases
( y in [#] K or not y in [#] K )
;
suppose Y0:
y in [#] K
;
(b1 + b2) + b3 = b1 + (b2 + b3)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
( z in [#] K or not z in [#] K )
;
suppose
z in [#] K
;
(b1 + b2) + b3 = b1 + (b2 + b3)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
;
verum end; suppose Z0:
not
z in [#] K
;
(b1 + b2) + b3 = b1 + (b2 + b3)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
( not the addF of T . (ab,z) in rng f or the addF of T . (ab,z) in rng f )
;
suppose K0:
not the
addF of
T . (
ab,
z)
in rng f
;
(b1 + b2) + b3 = b1 + (b2 + b3)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
;
verum end; suppose K1:
the
addF of
T . (
ab,
z)
in rng f
;
(b1 + b2) + b3 = b1 + (b2 + b3)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
;
verum end; end; end; suppose Y0:
not
y in [#] K
;
(b1 + b2) + b3 = b1 + (b2 + b3)then reconsider b1 =
b as
Element of
T by Lm1;
per cases
( not the addF of T . (x,y) in rng f or the addF of T . (x,y) in rng f )
;
suppose K2:
not the
addF of
T . (
x,
y)
in rng f
;
(b1 + b2) + b3 = b1 + (b2 + b3)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
( z in [#] K or not z in [#] K )
;
suppose Z:
z in [#] K
;
(b1 + b2) + b3 = b1 + (b2 + b3)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
;
verum end; suppose Z:
not
z in [#] K
;
(b1 + b2) + b3 = b1 + (b2 + b3)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
( not the addF of T . (ab,z) in rng f or the addF of T . (ab,z) in rng f )
;
suppose K:
not the
addF of
T . (
ab,
z)
in rng f
;
(b1 + b2) + b3 = b1 + (b2 + b3)per cases
( not the addF of T . (b1,c1) in rng f or the addF of T . (b1,c1) in rng f )
;
suppose K6:
not the
addF of
T . (
b1,
c1)
in rng f
;
(b1 + b2) + b3 = b1 + (b2 + b3)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
;
verum end; suppose K6:
the
addF of
T . (
b1,
c1)
in rng f
;
(b1 + b2) + b3 = b1 + (b2 + b3)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
;
verum end; suppose K7:
the
addF of
T . (
ab,
z)
in rng f
;
(b1 + b2) + b3 = b1 + (b2 + b3)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
;
verum end; end; end; suppose L:
the
addF of
T . (
x,
y)
in rng f
;
b1 + (b2 + b3) = (b1 + b2) + b3then 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
( z in [#] K or not z in [#] K )
;
suppose Z:
z in [#] K
;
b1 + (b2 + b3) = (b1 + b2) + b3then 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
;
verum end; suppose Z:
not
z in [#] K
;
(b1 + b2) + b3 = b1 + (b2 + b3)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
( not the addF of T . (y,z) in rng f or the addF of T . (y,z) in rng f )
;
suppose L1:
not the
addF of
T . (
y,
z)
in rng f
;
(b1 + b2) + b3 = b1 + (b2 + b3)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
;
verum end; suppose K6:
the
addF of
T . (
y,
z)
in rng f
;
(b1 + b2) + b3 = b1 + (b2 + b3)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
;
verum end; end; end; end; end; end;
hence
embField f is add-associative
; verum