set Z = EMbedding L;
set D = DivisibleMod L;
defpred S1[ object , object ] means ex vv, uu being Vector of (DivisibleMod L) ex v, u being Vector of (EMbedding L) ex a, b being Element of INT.Ring ex ai, bi being Element of INT st
( $1 = [vv,uu] & a = ai & b = bi & ai <> 0 & bi <> 0 & v = a * vv & u = b * uu & $2 = ((ai ") * (bi ")) * ((ScProductEM L) . (v,u)) );
A1:
for x being Element of [: the carrier of (DivisibleMod L), the carrier of (DivisibleMod L):] ex y being Element of F_Real st S1[x,y]
proof
let x be
Element of
[: the carrier of (DivisibleMod L), the carrier of (DivisibleMod L):];
ex y being Element of F_Real st S1[x,y]
consider vv,
uu being
object such that B1:
(
vv in the
carrier of
(DivisibleMod L) &
uu in the
carrier of
(DivisibleMod L) &
x = [vv,uu] )
by ZFMISC_1:def 2;
reconsider vv =
vv,
uu =
uu as
Vector of
(DivisibleMod L) by B1;
consider a being
Element of
INT.Ring such that B2:
(
a <> 0. INT.Ring &
a * vv in EMbedding L )
by ZMODUL08:29;
reconsider v =
a * vv as
Vector of
(EMbedding L) by B2;
consider b being
Element of
INT.Ring such that B3:
(
b <> 0. INT.Ring &
b * uu in EMbedding L )
by ZMODUL08:29;
reconsider u =
b * uu as
Vector of
(EMbedding L) by B3;
reconsider ai =
a,
bi =
b as
Element of
INT ;
take
((ai ") * (bi ")) * ((ScProductEM L) . (v,u))
;
( ((ai ") * (bi ")) * ((ScProductEM L) . (v,u)) is Element of F_Real & S1[x,((ai ") * (bi ")) * ((ScProductEM L) . (v,u))] )
thus
(
((ai ") * (bi ")) * ((ScProductEM L) . (v,u)) is
Element of
F_Real &
S1[
x,
((ai ") * (bi ")) * ((ScProductEM L) . (v,u))] )
by B1, B2, B3, XREAL_0:def 1;
verum
end;
consider f being Function of [: the carrier of (DivisibleMod L), the carrier of (DivisibleMod L):],F_Real such that
A2:
for x being Element of [: the carrier of (DivisibleMod L), the carrier of (DivisibleMod L):] holds S1[x,f . x]
from FUNCT_2:sch 3(A1);
take
f
; for vv, uu being Vector of (DivisibleMod L)
for v, u being Vector of (EMbedding L)
for a, b being Element of INT.Ring
for ai, bi being Element of F_Real st a = ai & b = bi & ai <> 0 & bi <> 0 & v = a * vv & u = b * uu holds
f . (vv,uu) = ((ai ") * (bi ")) * ((ScProductEM L) . (v,u))
for vv, uu being Vector of (DivisibleMod L)
for v, u being Vector of (EMbedding L)
for a, b being Element of INT.Ring
for ai, bi being Element of F_Real st a = ai & b = bi & ai <> 0 & bi <> 0 & v = a * vv & u = b * uu holds
f . (vv,uu) = ((ai ") * (bi ")) * ((ScProductEM L) . (v,u))
proof
let vv,
uu be
Vector of
(DivisibleMod L);
for v, u being Vector of (EMbedding L)
for a, b being Element of INT.Ring
for ai, bi being Element of F_Real st a = ai & b = bi & ai <> 0 & bi <> 0 & v = a * vv & u = b * uu holds
f . (vv,uu) = ((ai ") * (bi ")) * ((ScProductEM L) . (v,u))let v,
u be
Vector of
(EMbedding L);
for a, b being Element of INT.Ring
for ai, bi being Element of F_Real st a = ai & b = bi & ai <> 0 & bi <> 0 & v = a * vv & u = b * uu holds
f . (vv,uu) = ((ai ") * (bi ")) * ((ScProductEM L) . (v,u))let a,
b be
Element of
INT.Ring;
for ai, bi being Element of F_Real st a = ai & b = bi & ai <> 0 & bi <> 0 & v = a * vv & u = b * uu holds
f . (vv,uu) = ((ai ") * (bi ")) * ((ScProductEM L) . (v,u))let ai0,
bi0 be
Element of
F_Real;
( a = ai0 & b = bi0 & ai0 <> 0 & bi0 <> 0 & v = a * vv & u = b * uu implies f . (vv,uu) = ((ai0 ") * (bi0 ")) * ((ScProductEM L) . (v,u)) )
assume B1:
(
a = ai0 &
b = bi0 &
ai0 <> 0 &
bi0 <> 0 &
v = a * vv &
u = b * uu )
;
f . (vv,uu) = ((ai0 ") * (bi0 ")) * ((ScProductEM L) . (v,u))
reconsider ai =
ai0,
bi =
bi0 as
Element of
INT by B1;
consider vv1,
uu1 being
Vector of
(DivisibleMod L),
v1,
u1 being
Vector of
(EMbedding L),
a1,
b1 being
Element of
INT.Ring,
a1i,
b1i being
Element of
INT such that B2:
(
[vv1,uu1] = [vv,uu] &
a1 = a1i &
b1 = b1i &
a1i <> 0 &
b1i <> 0 &
v1 = a1 * vv1 &
u1 = b1 * uu1 &
f . (
vv,
uu)
= ((a1i ") * (b1i ")) * ((ScProductEM L) . (v1,u1)) )
by A2;
B3:
v1 = a1 * vv
by B2, XTUPLE_0:1;
B4:
u1 = b1 * uu
by B2, XTUPLE_0:1;
reconsider a1ga =
a1i gcd ai,
b1gb =
b1i gcd bi as
Element of
INT.Ring by INT_1:def 2;
BX:
EMbedding L is
Submodule of
DivisibleMod L
by ZMODUL08:24;
B5:
a1ga * vv in EMbedding L
proof
consider c10,
c20 being
Integer such that C10:
a1i gcd ai = (c10 * a1i) + (c20 * ai)
by NAT_D:68;
reconsider c1 =
c10,
c2 =
c20 as
Element of
INT.Ring by INT_1:def 2;
C2:
(c1 * a1) * vv =
c1 * (a1 * vv)
by VECTSP_1:def 16
.=
c1 * v1
by B3, BX, ZMODUL01:29
;
C3:
(c2 * a) * vv =
c2 * (a * vv)
by VECTSP_1:def 16
.=
c2 * v
by B1, BX, ZMODUL01:29
;
a1ga * vv =
((c1 * a1) + (c2 * a)) * vv
by B1, B2, C10
.=
((c1 * a1) * vv) + ((c2 * a) * vv)
by VECTSP_1:def 15
.=
(c1 * v1) + (c2 * v)
by C2, C3, BX, ZMODUL01:28
;
hence
a1ga * vv in EMbedding L
;
verum
end;
consider c10,
c20 being
Integer such that C10:
b1i gcd bi = (c10 * b1i) + (c20 * bi)
by NAT_D:68;
reconsider c1 =
c10,
c2 =
c20 as
Element of
INT.Ring by INT_1:def 2;
C2:
(c1 * b1) * uu =
c1 * (b1 * uu)
by VECTSP_1:def 16
.=
c1 * u1
by B4, BX, ZMODUL01:29
;
C3:
(c2 * b) * uu =
c2 * (b * uu)
by VECTSP_1:def 16
.=
c2 * u
by B1, BX, ZMODUL01:29
;
reconsider agv =
a1ga * vv as
Vector of
(EMbedding L) by B5;
b1gb * uu =
((c1 * b1) + (c2 * b)) * uu
by B1, B2, C10
.=
((c1 * b1) * uu) + ((c2 * b) * uu)
by VECTSP_1:def 15
.=
(c1 * u1) + (c2 * u)
by C2, C3, BX, ZMODUL01:28
;
then reconsider bgu =
b1gb * uu as
Vector of
(EMbedding L) ;
consider ci being
Integer such that B7:
ai = (a1i gcd ai) * ci
by INT_1:def 3, INT_2:21;
consider c1i being
Integer such that B8:
a1i = (a1i gcd ai) * c1i
by INT_1:def 3, INT_2:21;
consider di being
Integer such that B9:
bi = (b1i gcd bi) * di
by INT_1:def 3, INT_2:21;
reconsider c =
ci,
d =
di as
Element of
INT.Ring by INT_1:def 2;
consider d1i being
Integer such that B10:
b1i = (b1i gcd bi) * d1i
by INT_1:def 3, INT_2:21;
reconsider c =
ci,
c1 =
c1i,
d =
di,
d1 =
d1i as
Element of
INT.Ring by INT_1:def 2;
B11:
v =
(c * a1ga) * vv
by B1, B7
.=
c * (a1ga * vv)
by VECTSP_1:def 16
.=
c * agv
by BX, ZMODUL01:29
;
B12:
v1 =
(c1 * a1ga) * vv
by B2, B8, XTUPLE_0:1
.=
c1 * (a1ga * vv)
by VECTSP_1:def 16
.=
c1 * agv
by BX, ZMODUL01:29
;
B13:
u =
(d * b1gb) * uu
by B1, B9
.=
d * (b1gb * uu)
by VECTSP_1:def 16
.=
d * bgu
by BX, ZMODUL01:29
;
B14:
u1 =
(d1 * b1gb) * uu
by B2, B10, XTUPLE_0:1
.=
d1 * (b1gb * uu)
by VECTSP_1:def 16
.=
d1 * bgu
by BX, ZMODUL01:29
;
B15:
ci <> 0
by B1, B7;
B16:
c1i <> 0
by B2, B8;
B17:
di <> 0
by B1, B9;
B18:
d1i <> 0
by B2, B10;
B19:
f . (
vv,
uu) =
((a1i ") * (b1i ")) * (c1i * ((ScProductEM L) . (agv,(d1 * bgu))))
by B2, B12, B14, ThSPEM1
.=
((a1i ") * (b1i ")) * (c1i * ((ScProductEM L) . ((d1 * bgu),agv)))
by ThSPEM1
.=
((a1i ") * (b1i ")) * (c1i * (d1i * ((ScProductEM L) . (bgu,agv))))
by ThSPEM1
.=
((a1i ") * (b1i ")) * (c1i * (d1i * ((ScProductEM L) . (agv,bgu))))
by ThSPEM1
.=
((((a1i ") * (b1i ")) * c1i) * d1i) * ((ScProductEM L) . (agv,bgu))
.=
((((((a1i gcd ai) ") * (c1i ")) * (((b1i gcd bi) * d1i) ")) * c1i) * d1i) * ((ScProductEM L) . (agv,bgu))
by B8, B10, XCMPLX_1:204
.=
((((((a1i gcd ai) ") * c1i) * (c1i ")) * (((b1i gcd bi) * d1i) ")) * d1i) * ((ScProductEM L) . (agv,bgu))
.=
((((a1i gcd ai) ") * (((b1i gcd bi) * d1i) ")) * d1i) * ((ScProductEM L) . (agv,bgu))
by B16, XCMPLX_1:203
.=
(((((b1i gcd bi) * d1i) ") * d1i) * ((a1i gcd ai) ")) * ((ScProductEM L) . (agv,bgu))
.=
(((((b1i gcd bi) ") * (d1i ")) * d1i) * ((a1i gcd ai) ")) * ((ScProductEM L) . (agv,bgu))
by XCMPLX_1:204
.=
(((((b1i gcd bi) ") * d1i) * (d1i ")) * ((a1i gcd ai) ")) * ((ScProductEM L) . (agv,bgu))
.=
(((b1i gcd bi) ") * ((a1i gcd ai) ")) * ((ScProductEM L) . (agv,bgu))
by B18, XCMPLX_1:203
;
X1:
((ai ") * (bi ")) * ((ScProductEM L) . (v,u)) =
((ai ") * (bi ")) * (ci * ((ScProductEM L) . (agv,(d * bgu))))
by B11, B13, ThSPEM1
.=
((ai ") * (bi ")) * (ci * ((ScProductEM L) . ((d * bgu),agv)))
by ThSPEM1
.=
((ai ") * (bi ")) * (ci * (di * ((ScProductEM L) . (bgu,agv))))
by ThSPEM1
.=
((ai ") * (bi ")) * (ci * (di * ((ScProductEM L) . (agv,bgu))))
by ThSPEM1
.=
((((((a1i gcd ai) * ci) ") * (((b1i gcd bi) * di) ")) * ci) * di) * ((ScProductEM L) . (agv,bgu))
by B7, B9
.=
((((((a1i gcd ai) ") * (ci ")) * (((b1i gcd bi) * di) ")) * ci) * di) * ((ScProductEM L) . (agv,bgu))
by XCMPLX_1:204
.=
((((((a1i gcd ai) ") * ci) * (ci ")) * (((b1i gcd bi) * di) ")) * di) * ((ScProductEM L) . (agv,bgu))
.=
((((a1i gcd ai) ") * (((b1i gcd bi) * di) ")) * di) * ((ScProductEM L) . (agv,bgu))
by B15, XCMPLX_1:203
.=
(((((b1i gcd bi) * di) ") * di) * ((a1i gcd ai) ")) * ((ScProductEM L) . (agv,bgu))
.=
(((((b1i gcd bi) ") * (di ")) * di) * ((a1i gcd ai) ")) * ((ScProductEM L) . (agv,bgu))
by XCMPLX_1:204
.=
(((((b1i gcd bi) ") * di) * (di ")) * ((a1i gcd ai) ")) * ((ScProductEM L) . (agv,bgu))
.=
(((b1i gcd bi) ") * ((a1i gcd ai) ")) * ((ScProductEM L) . (agv,bgu))
by B17, XCMPLX_1:203
;
(
ai " = ai0 " &
bi " = bi0 " )
by LMINTFREAL1, B1;
hence
f . (
vv,
uu)
= ((ai0 ") * (bi0 ")) * ((ScProductEM L) . (v,u))
by X1, B19;
verum
end;
hence
for vv, uu being Vector of (DivisibleMod L)
for v, u being Vector of (EMbedding L)
for a, b being Element of INT.Ring
for ai, bi being Element of F_Real st a = ai & b = bi & ai <> 0 & bi <> 0 & v = a * vv & u = b * uu holds
f . (vv,uu) = ((ai ") * (bi ")) * ((ScProductEM L) . (v,u))
; verum