set A = the carrier of N;
set C = product <% the carrier of N, the carrier of N%>;
defpred S1[ Element of product <% the carrier of N, the carrier of N%>, Element of product <% the carrier of N, the carrier of N%>, set ] means ex a1, a2, b1, b2 being Element of N st
( $1 = <%a1,b1%> & $2 = <%a2,b2%> & $3 = <%(a1 + a2),(b1 + b2)%> );
A1:
for x, y being Element of product <% the carrier of N, the carrier of N%> ex z being Element of product <% the carrier of N, the carrier of N%> st S1[x,y,z]
proof
let a,
b be
Element of
product <% the carrier of N, the carrier of N%>;
ex z being Element of product <% the carrier of N, the carrier of N%> st S1[a,b,z]
consider a1,
b1 being
set such that A2:
(
a1 in the
carrier of
N &
b1 in the
carrier of
N )
and A3:
a = <%a1,b1%>
by Th7;
consider a2,
b2 being
set such that A4:
(
a2 in the
carrier of
N &
b2 in the
carrier of
N )
and A5:
b = <%a2,b2%>
by Th7;
reconsider a1 =
a1,
a2 =
a2,
b1 =
b1,
b2 =
b2 as
Element of the
carrier of
N by A2, A4;
take c =
<%(a1 + a2),(b1 + b2)%>;
( c is Element of product <% the carrier of N, the carrier of N%> & S1[a,b,c] )
thus
c is
Element of
product <% the carrier of N, the carrier of N%>
by Th6;
S1[a,b,c]
thus
S1[
a,
b,
c]
by A3, A5;
verum
end;
consider add being Function of [:(product <% the carrier of N, the carrier of N%>),(product <% the carrier of N, the carrier of N%>):],(product <% the carrier of N, the carrier of N%>) such that
A6:
for x, y being Element of product <% the carrier of N, the carrier of N%> holds S1[x,y,add . (x,y)]
from BINOP_1:sch 3(A1);
defpred S2[ Element of product <% the carrier of N, the carrier of N%>, Element of product <% the carrier of N, the carrier of N%>, set ] means ex a1, a2, b1, b2 being Element of N st
( $1 = <%a1,b1%> & $2 = <%a2,b2%> & $3 = <%((a1 * a2) - ((b2 *') * b1)),((b2 * a1) + (b1 * (a2 *')))%> );
A7:
for x, y being Element of product <% the carrier of N, the carrier of N%> ex z being Element of product <% the carrier of N, the carrier of N%> st S2[x,y,z]
proof
let a,
b be
Element of
product <% the carrier of N, the carrier of N%>;
ex z being Element of product <% the carrier of N, the carrier of N%> st S2[a,b,z]
consider a1,
b1 being
set such that A8:
(
a1 in the
carrier of
N &
b1 in the
carrier of
N )
and A9:
a = <%a1,b1%>
by Th7;
consider a2,
b2 being
set such that A10:
(
a2 in the
carrier of
N &
b2 in the
carrier of
N )
and A11:
b = <%a2,b2%>
by Th7;
reconsider a1 =
a1,
a2 =
a2,
b1 =
b1,
b2 =
b2 as
Element of the
carrier of
N by A8, A10;
take z =
<%((a1 * a2) - ((b2 *') * b1)),((b2 * a1) + (b1 * (a2 *')))%>;
( z is Element of product <% the carrier of N, the carrier of N%> & S2[a,b,z] )
thus
z is
Element of
product <% the carrier of N, the carrier of N%>
by Th6;
S2[a,b,z]
thus
S2[
a,
b,
z]
by A9, A11;
verum
end;
consider mult being Function of [:(product <% the carrier of N, the carrier of N%>),(product <% the carrier of N, the carrier of N%>):],(product <% the carrier of N, the carrier of N%>) such that
A12:
for x, y being Element of product <% the carrier of N, the carrier of N%> holds S2[x,y,mult . (x,y)]
from BINOP_1:sch 3(A7);
defpred S3[ Element of REAL , Element of product <% the carrier of N, the carrier of N%>, set ] means ex a, b being Element of N st
( $2 = <%a,b%> & $3 = <%($1 * a),($1 * b)%> );
A13:
for x being Element of REAL
for y being Element of product <% the carrier of N, the carrier of N%> ex z being Element of product <% the carrier of N, the carrier of N%> st S3[x,y,z]
proof
let r be
Element of
REAL ;
for y being Element of product <% the carrier of N, the carrier of N%> ex z being Element of product <% the carrier of N, the carrier of N%> st S3[r,y,z]let c be
Element of
product <% the carrier of N, the carrier of N%>;
ex z being Element of product <% the carrier of N, the carrier of N%> st S3[r,c,z]
consider a,
b being
set such that A14:
(
a in the
carrier of
N &
b in the
carrier of
N )
and A15:
c = <%a,b%>
by Th7;
reconsider a =
a,
b =
b as
Element of the
carrier of
N by A14;
take z =
<%(r * a),(r * b)%>;
( z is Element of product <% the carrier of N, the carrier of N%> & S3[r,c,z] )
thus
z is
Element of
product <% the carrier of N, the carrier of N%>
by Th6;
S3[r,c,z]
thus
S3[
r,
c,
z]
by A15;
verum
end;
consider MU being Function of [:REAL,(product <% the carrier of N, the carrier of N%>):],(product <% the carrier of N, the carrier of N%>) such that
A16:
for x being Element of REAL
for y being Element of product <% the carrier of N, the carrier of N%> holds S3[x,y,MU . (x,y)]
from BINOP_1:sch 3(A13);
defpred S4[ Element of product <% the carrier of N, the carrier of N%>, set ] means ex a, b being Element of N st
( $1 = <%a,b%> & $2 = sqrt ((||.a.|| ^2) + (||.b.|| ^2)) );
A17:
for x being Element of product <% the carrier of N, the carrier of N%> ex y being Element of REAL st S4[x,y]
consider norm being Function of (product <% the carrier of N, the carrier of N%>),REAL such that
A20:
for x being Element of product <% the carrier of N, the carrier of N%> holds S4[x,norm . x]
from FUNCT_2:sch 3(A17);
defpred S5[ Element of product <% the carrier of N, the carrier of N%>, set ] means ex a, b being Element of N st
( $1 = <%a,b%> & $2 = <%(a *'),(- b)%> );
A21:
for x being Element of product <% the carrier of N, the carrier of N%> ex y being Element of product <% the carrier of N, the carrier of N%> st S5[x,y]
proof
let c be
Element of
product <% the carrier of N, the carrier of N%>;
ex y being Element of product <% the carrier of N, the carrier of N%> st S5[c,y]
consider a,
b being
set such that A22:
(
a in the
carrier of
N &
b in the
carrier of
N )
and A23:
c = <%a,b%>
by Th7;
reconsider a =
a,
b =
b as
Element of the
carrier of
N by A22;
take
<%(a *'),(- b)%>
;
( <%(a *'),(- b)%> is Element of product <% the carrier of N, the carrier of N%> & S5[c,<%(a *'),(- b)%>] )
thus
(
<%(a *'),(- b)%> is
Element of
product <% the carrier of N, the carrier of N%> &
S5[
c,
<%(a *'),(- b)%>] )
by A23, Th6;
verum
end;
consider conj being Function of (product <% the carrier of N, the carrier of N%>),(product <% the carrier of N, the carrier of N%>) such that
A24:
for x being Element of product <% the carrier of N, the carrier of N%> holds S5[x,conj . x]
from FUNCT_2:sch 3(A21);
reconsider Z = <%(0. N),(0. N)%>, O = <%(1. N),(0. N)%> as Element of product <% the carrier of N, the carrier of N%> by Th6;
take X = ConjNormAlgStr(# (product <% the carrier of N, the carrier of N%>),mult,add,MU,O,Z,norm,conj #); ( the carrier of X = product <% the carrier of N, the carrier of N%> & the ZeroF of X = <%(0. N),(0. N)%> & the OneF of X = <%(1. N),(0. N)%> & ( for a1, a2, b1, b2 being Element of N holds
( the addF of X . (<%a1,b1%>,<%a2,b2%>) = <%(a1 + a2),(b1 + b2)%> & the multF of X . (<%a1,b1%>,<%a2,b2%>) = <%((a1 * a2) - ((b2 *') * b1)),((b2 * a1) + (b1 * (a2 *')))%> ) ) & ( for r being Real
for a, b being Element of N holds the Mult of X . (r,<%a,b%>) = <%(r * a),(r * b)%> ) & ( for a, b being Element of N holds
( the normF of X . <%a,b%> = sqrt ((||.a.|| ^2) + (||.b.|| ^2)) & the conjugateF of X . <%a,b%> = <%(a *'),(- b)%> ) ) )
thus
( the carrier of X = product <% the carrier of N, the carrier of N%> & the ZeroF of X = <%(0. N),(0. N)%> & the OneF of X = <%(1. N),(0. N)%> )
; ( ( for a1, a2, b1, b2 being Element of N holds
( the addF of X . (<%a1,b1%>,<%a2,b2%>) = <%(a1 + a2),(b1 + b2)%> & the multF of X . (<%a1,b1%>,<%a2,b2%>) = <%((a1 * a2) - ((b2 *') * b1)),((b2 * a1) + (b1 * (a2 *')))%> ) ) & ( for r being Real
for a, b being Element of N holds the Mult of X . (r,<%a,b%>) = <%(r * a),(r * b)%> ) & ( for a, b being Element of N holds
( the normF of X . <%a,b%> = sqrt ((||.a.|| ^2) + (||.b.|| ^2)) & the conjugateF of X . <%a,b%> = <%(a *'),(- b)%> ) ) )
hereby ( ( for r being Real
for a, b being Element of N holds the Mult of X . (r,<%a,b%>) = <%(r * a),(r * b)%> ) & ( for a, b being Element of N holds
( the normF of X . <%a,b%> = sqrt ((||.a.|| ^2) + (||.b.|| ^2)) & the conjugateF of X . <%a,b%> = <%(a *'),(- b)%> ) ) )
let a1,
a2,
b1,
b2 be
Element of
N;
( the addF of X . (<%a1,b1%>,<%a2,b2%>) = <%(a1 + a2),(b1 + b2)%> & the multF of X . (<%a1,b1%>,<%a2,b2%>) = <%((a1 * a2) - ((b2 *') * b1)),((b2 * a1) + (b1 * (a2 *')))%> )reconsider a =
<%a1,b1%>,
b =
<%a2,b2%> as
Element of
product <% the carrier of N, the carrier of N%> by Th6;
consider x1,
x2,
y1,
y2 being
Element of
N such that A25:
(
a = <%x1,y1%> &
b = <%x2,y2%> )
and A26:
add . (
a,
b)
= <%(x1 + x2),(y1 + y2)%>
by A6;
(
a1 = x1 &
a2 = x2 &
b1 = y1 &
b2 = y2 )
by A25, Th3;
hence
the
addF of
X . (
<%a1,b1%>,
<%a2,b2%>)
= <%(a1 + a2),(b1 + b2)%>
by A26;
the multF of X . (<%a1,b1%>,<%a2,b2%>) = <%((a1 * a2) - ((b2 *') * b1)),((b2 * a1) + (b1 * (a2 *')))%>consider x1,
x2,
y1,
y2 being
Element of
N such that A27:
(
a = <%x1,y1%> &
b = <%x2,y2%> )
and A28:
mult . (
a,
b)
= <%((x1 * x2) - ((y2 *') * y1)),((y2 * x1) + (y1 * (x2 *')))%>
by A12;
(
a1 = x1 &
a2 = x2 &
b1 = y1 &
b2 = y2 )
by A27, Th3;
hence
the
multF of
X . (
<%a1,b1%>,
<%a2,b2%>)
= <%((a1 * a2) - ((b2 *') * b1)),((b2 * a1) + (b1 * (a2 *')))%>
by A28;
verum
end;
hereby for a, b being Element of N holds
( the normF of X . <%a,b%> = sqrt ((||.a.|| ^2) + (||.b.|| ^2)) & the conjugateF of X . <%a,b%> = <%(a *'),(- b)%> )
let r be
Real;
for a, b being Element of N holds the Mult of X . (r,<%a,b%>) = <%(r * a),(r * b)%>let a,
b be
Element of
N;
the Mult of X . (r,<%a,b%>) = <%(r * a),(r * b)%>reconsider c =
<%a,b%> as
Element of
product <% the carrier of N, the carrier of N%> by Th6;
r in REAL
by XREAL_0:def 1;
then consider x,
y being
Element of
N such that A29:
c = <%x,y%>
and A30:
MU . (
r,
c)
= <%(r * x),(r * y)%>
by A16;
(
a = x &
b = y )
by A29, Th3;
hence
the
Mult of
X . (
r,
<%a,b%>)
= <%(r * a),(r * b)%>
by A30;
verum
end;
hereby verum
let a,
b be
Element of
N;
( the normF of X . <%a,b%> = sqrt ((||.a.|| ^2) + (||.b.|| ^2)) & the conjugateF of X . <%a,b%> = <%(a *'),(- b)%> )reconsider c =
<%a,b%> as
Element of
product <% the carrier of N, the carrier of N%> by Th6;
consider x,
y being
Element of
N such that A31:
c = <%x,y%>
and A32:
norm . c = sqrt ((||.x.|| ^2) + (||.y.|| ^2))
by A20;
(
a = x &
b = y )
by A31, Th3;
hence
the
normF of
X . <%a,b%> = sqrt ((||.a.|| ^2) + (||.b.|| ^2))
by A32;
the conjugateF of X . <%a,b%> = <%(a *'),(- b)%>consider x,
y being
Element of
N such that A33:
c = <%x,y%>
and A34:
conj . c = <%(x *'),(- y)%>
by A24;
(
a = x &
b = y )
by A33, Th3;
hence
the
conjugateF of
X . <%a,b%> = <%(a *'),(- b)%>
by A34;
verum
end;