defpred S1[ object , object , object ] means for z1, z2 being Element of V
for i1, i2 being Element of INT.Ring st i1 <> 0 & i2 <> 0 & $1 = Class ((EQRZM V),[z1,i1]) & $2 = Class ((EQRZM V),[z2,i2]) holds
$3 = Class ((EQRZM V),[((i2 * z1) + (i1 * z2)),(i1 * i2)]);
set C = Class (EQRZM V);
A1:
now for A, B being object st A in Class (EQRZM V) & B in Class (EQRZM V) holds
ex z being object st
( z in Class (EQRZM V) & S1[A,B,z] )let A,
B be
object ;
( A in Class (EQRZM V) & B in Class (EQRZM V) implies ex z being object st
( z in Class (EQRZM V) & S1[A,B,z] ) )assume A10:
(
A in Class (EQRZM V) &
B in Class (EQRZM V) )
;
ex z being object st
( z in Class (EQRZM V) & S1[A,B,z] )then consider A1 being
object such that A2:
(
A1 in [: the carrier of V,(INT \ {0}):] &
A = Class (
(EQRZM V),
A1) )
by EQREL_1:def 3;
consider z1,
i1 being
object such that A3:
(
z1 in the
carrier of
V &
i1 in INT \ {0} &
A1 = [z1,i1] )
by A2, ZFMISC_1:def 2;
reconsider z1 =
z1 as
Element of
V by A3;
(
i1 in INT & not
i1 in {0} )
by XBOOLE_0:def 5, A3;
then A31:
(
i1 in INT &
i1 <> 0 )
by TARSKI:def 1;
reconsider i1 =
i1 as
Integer by A3;
reconsider i1 =
i1 as
Element of
INT.Ring by A3;
consider B1 being
object such that A4:
(
B1 in [: the carrier of V,(INT \ {0}):] &
B = Class (
(EQRZM V),
B1) )
by A10, EQREL_1:def 3;
consider z2,
i2 being
object such that A5:
(
z2 in the
carrier of
V &
i2 in INT \ {0} &
B1 = [z2,i2] )
by A4, ZFMISC_1:def 2;
reconsider z2 =
z2 as
Element of
V by A5;
(
i2 in INT & not
i2 in {0} )
by XBOOLE_0:def 5, A5;
then A51:
(
i2 in INT &
i2 <> 0 )
by TARSKI:def 1;
reconsider i2 =
i2 as
Integer by A5;
reconsider i2 =
i2 as
Element of
INT.Ring by A5;
A61:
not
i1 * i2 in {0}
by A31, A51, TARSKI:def 1;
i1 * i2 in INT \ {0}
by XBOOLE_0:def 5, A61;
then X1:
[((i2 * z1) + (i1 * z2)),(i1 * i2)] in [: the carrier of V,(INT \ {0}):]
by ZFMISC_1:87;
set z =
Class (
(EQRZM V),
[((i2 * z1) + (i1 * z2)),(i1 * i2)]);
A7:
Class (
(EQRZM V),
[((i2 * z1) + (i1 * z2)),(i1 * i2)])
in Class (EQRZM V)
by X1, EQREL_1:def 3;
S1[
A,
B,
Class (
(EQRZM V),
[((i2 * z1) + (i1 * z2)),(i1 * i2)])]
proof
let zz1,
zz2 be
Element of
V;
for i1, i2 being Element of INT.Ring st i1 <> 0 & i2 <> 0 & A = Class ((EQRZM V),[zz1,i1]) & B = Class ((EQRZM V),[zz2,i2]) holds
Class ((EQRZM V),[((i2 * z1) + (i1 * z2)),(i1 * i2)]) = Class ((EQRZM V),[((i2 * zz1) + (i1 * zz2)),(i1 * i2)])let ii1,
ii2 be
Element of
INT.Ring;
( ii1 <> 0 & ii2 <> 0 & A = Class ((EQRZM V),[zz1,ii1]) & B = Class ((EQRZM V),[zz2,ii2]) implies Class ((EQRZM V),[((i2 * z1) + (i1 * z2)),(i1 * i2)]) = Class ((EQRZM V),[((ii2 * zz1) + (ii1 * zz2)),(ii1 * ii2)]) )
assume A71:
(
ii1 <> 0 &
ii2 <> 0 &
A = Class (
(EQRZM V),
[zz1,ii1]) &
B = Class (
(EQRZM V),
[zz2,ii2]) )
;
Class ((EQRZM V),[((i2 * z1) + (i1 * z2)),(i1 * i2)]) = Class ((EQRZM V),[((ii2 * zz1) + (ii1 * zz2)),(ii1 * ii2)])
then A72:
not
ii1 in {0}
by TARSKI:def 1;
ii1 in INT \ {0}
by XBOOLE_0:def 5, A72;
then X2:
[zz1,ii1] in [: the carrier of V,(INT \ {0}):]
by ZFMISC_1:87;
X21:
not
ii2 in {0}
by TARSKI:def 1, A71;
ii2 in INT \ {0}
by XBOOLE_0:def 5, X21;
then X3:
[zz2,ii2] in [: the carrier of V,(INT \ {0}):]
by ZFMISC_1:87;
X5:
[[zz1,ii1],[z1,i1]] in EQRZM V
by X2, A2, A3, A71, EQREL_1:35;
then XX5:
(
ii1 <> 0 &
i1 <> 0 &
i1 * zz1 = ii1 * z1 )
by LMEQR001, AS;
X7:
[[zz2,ii2],[z2,i2]] in EQRZM V
by X3, A4, A5, A71, EQREL_1:35;
then XX7:
(
ii2 <> 0 &
i2 <> 0 &
i2 * zz2 = ii2 * z2 )
by LMEQR001, AS;
(ii1 * ii2) * ((i2 * z1) + (i1 * z2)) =
((ii1 * ii2) * (i2 * z1)) + ((ii1 * ii2) * (i1 * z2))
by VECTSP_1:def 14
.=
(((ii1 * ii2) * i2) * z1) + ((ii1 * ii2) * (i1 * z2))
by VECTSP_1:def 16
.=
(((ii2 * i2) * ii1) * z1) + (((ii1 * ii2) * i1) * z2)
by VECTSP_1:def 16
.=
((ii2 * i2) * (ii1 * z1)) + (((ii1 * i1) * ii2) * z2)
by VECTSP_1:def 16
.=
((ii2 * i2) * (ii1 * z1)) + ((ii1 * i1) * (ii2 * z2))
by VECTSP_1:def 16
.=
((ii2 * i2) * (i1 * zz1)) + ((ii1 * i1) * (ii2 * z2))
by AS, X5, LMEQR001
.=
((ii2 * i2) * (i1 * zz1)) + ((ii1 * i1) * (i2 * zz2))
by AS, X7, LMEQR001
.=
(((ii2 * i2) * i1) * zz1) + ((ii1 * i1) * (i2 * zz2))
by VECTSP_1:def 16
.=
(((i2 * i1) * ii2) * zz1) + (((ii1 * i1) * i2) * zz2)
by VECTSP_1:def 16
.=
((i1 * i2) * (ii2 * zz1)) + (((i1 * i2) * ii1) * zz2)
by VECTSP_1:def 16
.=
((i1 * i2) * (ii2 * zz1)) + ((i1 * i2) * (ii1 * zz2))
by VECTSP_1:def 16
.=
(i1 * i2) * ((ii2 * zz1) + (ii1 * zz2))
by VECTSP_1:def 14
;
then
[[((i2 * z1) + (i1 * z2)),(i1 * i2)],[((ii2 * zz1) + (ii1 * zz2)),(ii1 * ii2)]] in EQRZM V
by XX5, XX7, LMEQR001, AS;
hence
Class (
(EQRZM V),
[((i2 * z1) + (i1 * z2)),(i1 * i2)])
= Class (
(EQRZM V),
[((ii2 * zz1) + (ii1 * zz2)),(ii1 * ii2)])
by X1, EQREL_1:35;
verum
end; hence
ex
z being
object st
(
z in Class (EQRZM V) &
S1[
A,
B,
z] )
by A7;
verum end;
consider f being Function of [:(Class (EQRZM V)),(Class (EQRZM V)):],(Class (EQRZM V)) such that
A14:
for A, B being object st A in Class (EQRZM V) & B in Class (EQRZM V) holds
S1[A,B,f . (A,B)]
from BINOP_1:sch 1(A1);
reconsider f = f as BinOp of (Class (EQRZM V)) ;
take
f
; for A, B being object st A in Class (EQRZM V) & B in Class (EQRZM V) holds
for z1, z2 being Element of V
for i1, i2 being Element of INT.Ring st i1 <> 0. INT.Ring & i2 <> 0. INT.Ring & A = Class ((EQRZM V),[z1,i1]) & B = Class ((EQRZM V),[z2,i2]) holds
f . (A,B) = Class ((EQRZM V),[((i2 * z1) + (i1 * z2)),(i1 * i2)])
thus
for A, B being object st A in Class (EQRZM V) & B in Class (EQRZM V) holds
for z1, z2 being Element of V
for i1, i2 being Element of INT.Ring st i1 <> 0. INT.Ring & i2 <> 0. INT.Ring & A = Class ((EQRZM V),[z1,i1]) & B = Class ((EQRZM V),[z2,i2]) holds
f . (A,B) = Class ((EQRZM V),[((i2 * z1) + (i1 * z2)),(i1 * i2)])
by A14; verum