defpred S1[ object , object , object ] means for m, n, i being Integer
for mm being Element of INT.Ring
for z being Element of V st mm = m & n <> 0 & $1 = m / n & i <> 0 & $2 = Class ((EQRZM V),[z,i]) holds
$3 = Class ((EQRZM V),[(mm * z),(n * i)]);
set cF = RAT ;
set C = Class (EQRZM V);
A1:
now for q, A being object st q in RAT & A in Class (EQRZM V) holds
ex w being object st
( w in Class (EQRZM V) & S1[q,A,w] )let q,
A be
object ;
( q in RAT & A in Class (EQRZM V) implies ex w being object st
( w in Class (EQRZM V) & S1[q,A,w] ) )assume AS0:
(
q in RAT &
A in Class (EQRZM V) )
;
ex w being object st
( w in Class (EQRZM V) & S1[q,A,w] )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 z,
i being
object such that A3:
(
z in the
carrier of
V &
i in INT \ {0} &
A1 = [z,i] )
by A2, ZFMISC_1:def 2;
reconsider z =
z as
Element of
V by A3;
(
i in INT & not
i in {0} )
by XBOOLE_0:def 5, A3;
then A31:
(
i in INT &
i <> 0 )
by TARSKI:def 1;
reconsider i =
i as
Integer by A3;
consider m,
n being
Integer such that A4:
(
n > 0 &
q = m / n )
by AS0, RAT_1:1;
reconsider I =
i,
mn =
m,
no =
n as
Element of
INT.Ring by Lem1;
A61:
not
no * i in {0}
by A31, A4, TARSKI:def 1;
no * i in INT
by INT_1:def 2;
then
no * i in INT \ {0}
by XBOOLE_0:def 5, A61;
then X1:
[(mn * z),(no * i)] in [: the carrier of V,(INT \ {0}):]
by ZFMISC_1:87;
set w =
Class (
(EQRZM V),
[(mn * z),(no * i)]);
A7:
Class (
(EQRZM V),
[(mn * z),(no * i)])
in Class (EQRZM V)
by X1, EQREL_1:def 3;
S1[
q,
A,
Class (
(EQRZM V),
[(mn * z),(no * i)])]
proof
let mm,
nn,
ii be
Integer;
for mm being Element of INT.Ring
for z being Element of V st mm = mm & nn <> 0 & q = mm / nn & ii <> 0 & A = Class ((EQRZM V),[z,ii]) holds
Class ((EQRZM V),[(mn * z),(no * i)]) = Class ((EQRZM V),[(mm * z),(nn * ii)])let m1 be
Element of
INT.Ring;
for z being Element of V st m1 = mm & nn <> 0 & q = mm / nn & ii <> 0 & A = Class ((EQRZM V),[z,ii]) holds
Class ((EQRZM V),[(mn * z),(no * i)]) = Class ((EQRZM V),[(m1 * z),(nn * ii)])let zz be
Element of
V;
( m1 = mm & nn <> 0 & q = mm / nn & ii <> 0 & A = Class ((EQRZM V),[zz,ii]) implies Class ((EQRZM V),[(mn * z),(no * i)]) = Class ((EQRZM V),[(m1 * zz),(nn * ii)]) )
assume A71:
(
m1 = mm &
nn <> 0 &
q = mm / nn &
ii <> 0 &
A = Class (
(EQRZM V),
[zz,ii]) )
;
Class ((EQRZM V),[(mn * z),(no * i)]) = Class ((EQRZM V),[(m1 * zz),(nn * ii)])
then A72:
not
ii in {0}
by TARSKI:def 1;
ii in INT
by INT_1:def 2;
then
ii in INT \ {0}
by XBOOLE_0:def 5, A72;
then X2:
[zz,ii] in [: the carrier of V,(INT \ {0}):]
by ZFMISC_1:87;
reconsider i2 =
ii,
n1 =
nn as
Element of
INT.Ring by INT_1:def 2;
X51:
[[zz,i2],[z,I]] in EQRZM V
by X2, A2, A3, A71, EQREL_1:35;
(n1 * i2) * (mn * z) =
((n1 * i2) * mn) * z
by VECTSP_1:def 16
.=
((n1 * mn) * i2) * z
.=
(n1 * mn) * (i2 * z)
by VECTSP_1:def 16
.=
(n1 * mn) * (I * zz)
by AS, X51, LMEQR001
.=
(no * m1) * (I * zz)
by A4, A71, XCMPLX_1:95
.=
((no * m1) * I) * zz
by VECTSP_1:def 16
.=
((no * I) * m1) * zz
.=
(no * I) * (m1 * zz)
by VECTSP_1:def 16
;
then
[[(mn * z),(no * I)],[(m1 * zz),(n1 * i2)]] in EQRZM V
by A31, A4, A71, LMEQR001, AS;
hence
Class (
(EQRZM V),
[(mn * z),(no * i)])
= Class (
(EQRZM V),
[(m1 * zz),(nn * ii)])
by X1, EQREL_1:35;
verum
end; hence
ex
w being
object st
(
w in Class (EQRZM V) &
S1[
q,
A,
w] )
by A7;
verum end;
consider f being Function of [:RAT,(Class (EQRZM V)):],(Class (EQRZM V)) such that
A14:
for q, A being object st q in RAT & A in Class (EQRZM V) holds
S1[q,A,f . (q,A)]
from BINOP_1:sch 1(A1);
reconsider f = f as Function of [: the carrier of F_Rat,(Class (EQRZM V)):],(Class (EQRZM V)) ;
take
f
; for q, A being object st q in RAT & A in Class (EQRZM V) holds
for m, n, i being Integer
for mm being Element of INT.Ring
for z being Element of V st m = mm & n <> 0 & q = m / n & i <> 0 & A = Class ((EQRZM V),[z,i]) holds
f . (q,A) = Class ((EQRZM V),[(mm * z),(n * i)])
thus
for q, A being object st q in RAT & A in Class (EQRZM V) holds
for m, n, i being Integer
for mm being Element of INT.Ring
for z being Element of V st m = mm & n <> 0 & q = m / n & i <> 0 & A = Class ((EQRZM V),[z,i]) holds
f . (q,A) = Class ((EQRZM V),[(mm * z),(n * i)])
by A14; verum