let X, Y be strict ConjNormAlgStr ; :: thesis: ( 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)%> ) ) & the carrier of Y = product <% the carrier of N, the carrier of N%> & the ZeroF of Y = <%(0. N),(0. N)%> & the OneF of Y = <%(1. N),(0. N)%> & ( for a1, a2, b1, b2 being Element of N holds
( the addF of Y . (<%a1,b1%>,<%a2,b2%>) = <%(a1 + a2),(b1 + b2)%> & the multF of Y . (<%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 Y . (r,<%a,b%>) = <%(r * a),(r * b)%> ) & ( for a, b being Element of N holds
( the normF of Y . <%a,b%> = sqrt ((||.a.|| ^2) + (||.b.|| ^2)) & the conjugateF of Y . <%a,b%> = <%(a *'),(- b)%> ) ) implies X = Y )
assume that
A35: the carrier of X = product <% the carrier of N, the carrier of N%> and
A36: the ZeroF of X = <%(0. N),(0. N)%> and
A37: the OneF of X = <%(1. N),(0. N)%> and
A38: 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 *')))%> ) and
A39: for r being Real
for a, b being Element of N holds the Mult of X . (r,<%a,b%>) = <%(r * a),(r * b)%> and
A40: 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)%> ) and
A41: the carrier of Y = product <% the carrier of N, the carrier of N%> and
A42: the ZeroF of Y = <%(0. N),(0. N)%> and
A43: the OneF of Y = <%(1. N),(0. N)%> and
A44: for a1, a2, b1, b2 being Element of N holds
( the addF of Y . (<%a1,b1%>,<%a2,b2%>) = <%(a1 + a2),(b1 + b2)%> & the multF of Y . (<%a1,b1%>,<%a2,b2%>) = <%((a1 * a2) - ((b2 *') * b1)),((b2 * a1) + (b1 * (a2 *')))%> ) and
A45: for r being Real
for a, b being Element of N holds the Mult of Y . (r,<%a,b%>) = <%(r * a),(r * b)%> and
A46: for a, b being Element of N holds
( the normF of Y . <%a,b%> = sqrt ((||.a.|| ^2) + (||.b.|| ^2)) & the conjugateF of Y . <%a,b%> = <%(a *'),(- b)%> ) ; :: thesis: X = Y
A47: the addF of X = the addF of Y
proof
dom the addF of X = [: the carrier of X, the carrier of X:] by A35, FUNCT_2:def 1;
hence dom the addF of X = dom the addF of Y by A35, A41, FUNCT_2:def 1; :: according to FUNCT_1:def 11 :: thesis: for b1 being object holds
( not b1 in dom the addF of X or the addF of X . b1 = the addF of Y . b1 )
let z be object ; :: thesis: ( not z in dom the addF of X or the addF of X . z = the addF of Y . z )
assume z in dom the addF of X ; :: thesis: the addF of X . z = the addF of Y . z
then consider z1, z2 being object such that
A48: z1 in the carrier of X and
A49: z2 in the carrier of X and
A50: z = [z1,z2] by ZFMISC_1:def 2;
consider a1, b1 being set such that
A51: ( a1 in the carrier of N & b1 in the carrier of N ) and
A52: z1 = <%a1,b1%> by A35, A48, Th7;
consider a2, b2 being set such that
A53: ( a2 in the carrier of N & b2 in the carrier of N ) and
A54: z2 = <%a2,b2%> by A35, A49, Th7;
reconsider a1 = a1, a2 = a2, b1 = b1, b2 = b2 as Element of N by A51, A53;
thus the addF of X . z = the addF of X . (z1,z2) by A50
.= <%(a1 + a2),(b1 + b2)%> by A52, A54, A38
.= the addF of Y . (z1,z2) by A52, A54, A44
.= the addF of Y . z by A50 ; :: thesis: verum
end;
A55: the multF of X = the multF of Y
proof
dom the multF of X = [: the carrier of X, the carrier of X:] by A35, FUNCT_2:def 1;
hence dom the multF of X = dom the multF of Y by A35, A41, FUNCT_2:def 1; :: according to FUNCT_1:def 11 :: thesis: for b1 being object holds
( not b1 in dom the multF of X or the multF of X . b1 = the multF of Y . b1 )
let z be object ; :: thesis: ( not z in dom the multF of X or the multF of X . z = the multF of Y . z )
assume z in dom the multF of X ; :: thesis: the multF of X . z = the multF of Y . z
then consider z1, z2 being object such that
A56: z1 in the carrier of X and
A57: z2 in the carrier of X and
A58: z = [z1,z2] by ZFMISC_1:def 2;
consider a1, b1 being set such that
A59: ( a1 in the carrier of N & b1 in the carrier of N ) and
A60: z1 = <%a1,b1%> by A35, A56, Th7;
consider a2, b2 being set such that
A61: ( a2 in the carrier of N & b2 in the carrier of N ) and
A62: z2 = <%a2,b2%> by A35, A57, Th7;
reconsider a1 = a1, a2 = a2, b1 = b1, b2 = b2 as Element of N by A59, A61;
thus the multF of X . z = the multF of X . (z1,z2) by A58
.= <%((a1 * a2) - ((b2 *') * b1)),((b2 * a1) + (b1 * (a2 *')))%> by A60, A62, A38
.= the multF of Y . (z1,z2) by A60, A62, A44
.= the multF of Y . z by A58 ; :: thesis: verum
end;
A63: the Mult of X = the Mult of Y
proof
dom the Mult of X = [:REAL, the carrier of X:] by A35, FUNCT_2:def 1;
hence dom the Mult of X = dom the Mult of Y by A35, A41, FUNCT_2:def 1; :: according to FUNCT_1:def 11 :: thesis: for b1 being object holds
( not b1 in dom the Mult of X or the Mult of X . b1 = the Mult of Y . b1 )
let z be object ; :: thesis: ( not z in dom the Mult of X or the Mult of X . z = the Mult of Y . z )
assume z in dom the Mult of X ; :: thesis: the Mult of X . z = the Mult of Y . z
then consider z1, z2 being object such that
A64: z1 in REAL and
A65: z2 in the carrier of X and
A66: z = [z1,z2] by ZFMISC_1:def 2;
consider a, b being set such that
A67: ( a in the carrier of N & b in the carrier of N ) and
A68: z2 = <%a,b%> by A35, A65, Th7;
reconsider z1 = z1 as Element of REAL by A64;
reconsider a = a, b = b as Element of N by A67;
thus the Mult of X . z = the Mult of X . (z1,z2) by A66
.= <%(z1 * a),(z1 * b)%> by A68, A39
.= the Mult of Y . (z1,z2) by A68, A45
.= the Mult of Y . z by A66 ; :: thesis: verum
end;
A69: the normF of X = the normF of Y
proof
dom the normF of X = the carrier of X by FUNCT_2:def 1;
hence dom the normF of X = dom the normF of Y by A35, A41, FUNCT_2:def 1; :: according to FUNCT_1:def 11 :: thesis: for b1 being object holds
( not b1 in dom the normF of X or the normF of X . b1 = the normF of Y . b1 )
let z be object ; :: thesis: ( not z in dom the normF of X or the normF of X . z = the normF of Y . z )
assume z in dom the normF of X ; :: thesis: the normF of X . z = the normF of Y . z
then consider a, b being set such that
A70: ( a in the carrier of N & b in the carrier of N ) and
A71: z = <%a,b%> by A35, Th7;
reconsider a = a, b = b as Element of N by A70;
thus the normF of X . z = sqrt ((||.a.|| ^2) + (||.b.|| ^2)) by A71, A40
.= the normF of Y . z by A71, A46 ; :: thesis: verum
end;
the conjugateF of X = the conjugateF of Y
proof
dom the conjugateF of X = the carrier of X by A35, FUNCT_2:def 1;
hence dom the conjugateF of X = dom the conjugateF of Y by A35, A41, FUNCT_2:def 1; :: according to FUNCT_1:def 11 :: thesis: for b1 being object holds
( not b1 in dom the conjugateF of X or the conjugateF of X . b1 = the conjugateF of Y . b1 )
let z be object ; :: thesis: ( not z in dom the conjugateF of X or the conjugateF of X . z = the conjugateF of Y . z )
assume z in dom the conjugateF of X ; :: thesis: the conjugateF of X . z = the conjugateF of Y . z
then consider a, b being set such that
A72: ( a in the carrier of N & b in the carrier of N ) and
A73: z = <%a,b%> by A35, Th7;
reconsider a = a, b = b as Element of N by A72;
thus the conjugateF of X . z = <%(a *'),(- b)%> by A73, A40
.= the conjugateF of Y . z by A73, A46 ; :: thesis: verum
end;
hence X = Y by A35, A36, A37, A41, A42, A43, A47, A55, A63, A69; :: thesis: verum