set X = [:(n -roots_of_1),(n -roots_of_1):];
set mru = the multF of F_Complex || (n -roots_of_1);
n -roots_of_1 c= the carrier of F_Complex ;
then n -roots_of_1 c= COMPLEX by COMPLFLD:def 1;
then [:(n -roots_of_1),(n -roots_of_1):] c= [:COMPLEX,COMPLEX:] by ZFMISC_1:96;
then A1: [:(n -roots_of_1),(n -roots_of_1):] c= dom multcomplex by FUNCT_2:def 1;
A2: multcomplex = the multF of F_Complex by COMPLFLD:def 1;
then A3: dom ( the multF of F_Complex || (n -roots_of_1)) = (dom multcomplex) /\ [:(n -roots_of_1),(n -roots_of_1):] by RELAT_1:61;
then A4: dom ( the multF of F_Complex || (n -roots_of_1)) = [:(n -roots_of_1),(n -roots_of_1):] by A1, XBOOLE_1:28;
for x being object st x in [:(n -roots_of_1),(n -roots_of_1):] holds
( the multF of F_Complex || (n -roots_of_1)) . x in n -roots_of_1
proof
let x be object ; :: thesis: ( x in [:(n -roots_of_1),(n -roots_of_1):] implies ( the multF of F_Complex || (n -roots_of_1)) . x in n -roots_of_1 )
assume A5: x in [:(n -roots_of_1),(n -roots_of_1):] ; :: thesis: ( the multF of F_Complex || (n -roots_of_1)) . x in n -roots_of_1
consider a, b being object such that
A6: [a,b] = x by A5, RELAT_1:def 1;
A7: b in n -roots_of_1 by A5, A6, ZFMISC_1:87;
A8: a in n -roots_of_1 by A5, A6, ZFMISC_1:87;
reconsider b = b as Element of COMPLEX by A7, COMPLFLD:def 1;
reconsider a = a as Element of COMPLEX by A8, COMPLFLD:def 1;
( multcomplex . (a,b) = a * b & ( the multF of F_Complex || (n -roots_of_1)) . [a,b] = multcomplex . [a,b] ) by A2, A4, A5, A6, BINOP_2:def 5, FUNCT_1:47;
hence ( the multF of F_Complex || (n -roots_of_1)) . x in n -roots_of_1 by A6, A8, A7, Th25; :: thesis: verum
end;
then reconsider uM = the multF of F_Complex || (n -roots_of_1) as BinOp of (n -roots_of_1) by A1, A3, FUNCT_2:3, XBOOLE_1:28;
set H = multMagma(# (n -roots_of_1),uM #);
reconsider 1F = 1_ F_Complex as Element of multMagma(# (n -roots_of_1),uM #) by Th22;
A9: 1_ F_Complex = [**(cos (((2 * PI) * 0) / n)),(sin (((2 * PI) * 0) / n))**] by COMPLFLD:8, SIN_COS:31;
A10: for s1 being Element of multMagma(# (n -roots_of_1),uM #) holds
( s1 * 1F = s1 & 1F * s1 = s1 & ex s2 being Element of multMagma(# (n -roots_of_1),uM #) st
( s1 * s2 = 1_ F_Complex & s2 * s1 = 1_ F_Complex ) )
proof
let s1 be Element of multMagma(# (n -roots_of_1),uM #); :: thesis: ( s1 * 1F = s1 & 1F * s1 = s1 & ex s2 being Element of multMagma(# (n -roots_of_1),uM #) st
( s1 * s2 = 1_ F_Complex & s2 * s1 = 1_ F_Complex ) )
A11: ex s2 being Element of multMagma(# (n -roots_of_1),uM #) st
( s1 * s2 = 1_ F_Complex & s2 * s1 = 1_ F_Complex )
proof
s1 in the carrier of F_Complex by TARSKI:def 3;
then consider k being Element of NAT such that
A12: s1 = [**(cos (((2 * PI) * k) / n)),(sin (((2 * PI) * k) / n))**] by Th24;
reconsider e1 = [**(cos (((2 * PI) * k) / n)),(sin (((2 * PI) * k) / n))**] as Element of F_Complex ;
ex j being Element of NAT st (k + j) mod n = 0
proof
set r = k mod n;
k mod n < n by NAT_D:1;
then consider j being Nat such that
A13: (k mod n) + j = n by NAT_1:10;
k = (n * (k div n)) + (k mod n) by NAT_D:2;
then ( j in NAT & (k + j) mod n = (((k div n) + 1) * n) mod n ) by A13, ORDINAL1:def 12;
hence ex j being Element of NAT st (k + j) mod n = 0 by NAT_D:13; :: thesis: verum
end;
then consider j being Element of NAT such that
A14: (k + j) mod n = 0 ;
set ss2 = [**(cos (((2 * PI) * j) / n)),(sin (((2 * PI) * j) / n))**];
reconsider s2 = [**(cos (((2 * PI) * j) / n)),(sin (((2 * PI) * j) / n))**] as Element of multMagma(# (n -roots_of_1),uM #) by Th24;
reconsider e2 = s2 as Element of F_Complex ;
( e2 * e1 = [**(cos (((2 * PI) * ((j + k) mod n)) / n)),(sin (((2 * PI) * ((j + k) mod n)) / n))**] & [s2,s1] in dom ( the multF of F_Complex || (n -roots_of_1)) ) by A4, Th11, ZFMISC_1:87;
then A15: s2 * s1 = 1_ F_Complex by A12, A14, COMPLFLD:8, FUNCT_1:47, SIN_COS:31;
( e1 * e2 = [**(cos (((2 * PI) * ((j + k) mod n)) / n)),(sin (((2 * PI) * ((j + k) mod n)) / n))**] & [s1,s2] in dom ( the multF of F_Complex || (n -roots_of_1)) ) by A4, Th11, ZFMISC_1:87;
then s1 * s2 = 1_ F_Complex by A12, A14, COMPLFLD:8, FUNCT_1:47, SIN_COS:31;
hence ex s2 being Element of multMagma(# (n -roots_of_1),uM #) st
( s1 * s2 = 1_ F_Complex & s2 * s1 = 1_ F_Complex ) by A15; :: thesis: verum
end;
( s1 * 1F = s1 & 1F * s1 = s1 )
proof
A16: ( [s1,1F] in dom ( the multF of F_Complex || (n -roots_of_1)) & [1F,s1] in dom ( the multF of F_Complex || (n -roots_of_1)) ) by A4, ZFMISC_1:87;
reconsider e1 = s1 as Element of F_Complex by TARSKI:def 3;
consider k being Element of NAT such that
A17: e1 = [**(cos (((2 * PI) * k) / n)),(sin (((2 * PI) * k) / n))**] by Th24;
A18: (1_ F_Complex) * e1 = [**(cos (((2 * PI) * ((k + 0) mod n)) / n)),(sin (((2 * PI) * ((k + 0) mod n)) / n))**] by A9, A17, Th11
.= s1 by A17, Th10 ;
e1 * (1_ F_Complex) = [**(cos (((2 * PI) * ((k + 0) mod n)) / n)),(sin (((2 * PI) * ((k + 0) mod n)) / n))**] by A9, A17, Th11
.= s1 by A17, Th10 ;
hence ( s1 * 1F = s1 & 1F * s1 = s1 ) by A18, A16, FUNCT_1:47; :: thesis: verum
end;
hence ( s1 * 1F = s1 & 1F * s1 = s1 & ex s2 being Element of multMagma(# (n -roots_of_1),uM #) st
( s1 * s2 = 1_ F_Complex & s2 * s1 = 1_ F_Complex ) ) by A11; :: thesis: verum
end;
A19: rng uM c= n -roots_of_1 by RELAT_1:def 19;
for r, s, t being Element of multMagma(# (n -roots_of_1),uM #) holds (r * s) * t = r * (s * t)
proof
set mc = multcomplex ;
let r, s, t be Element of multMagma(# (n -roots_of_1),uM #); :: thesis: (r * s) * t = r * (s * t)
r in the carrier of F_Complex by TARSKI:def 3;
then A20: r is Element of COMPLEX by COMPLFLD:def 1;
s in the carrier of F_Complex by TARSKI:def 3;
then A21: s is Element of COMPLEX by COMPLFLD:def 1;
A22: [r,s] in dom ( the multF of F_Complex || (n -roots_of_1)) by A4, ZFMISC_1:87;
then ( the multF of F_Complex || (n -roots_of_1)) . [r,s] in rng ( the multF of F_Complex || (n -roots_of_1)) by FUNCT_1:3;
then A23: [(( the multF of F_Complex || (n -roots_of_1)) . [r,s]),t] in dom ( the multF of F_Complex || (n -roots_of_1)) by A4, A19, ZFMISC_1:87;
A24: [s,t] in dom ( the multF of F_Complex || (n -roots_of_1)) by A4, ZFMISC_1:87;
then ( the multF of F_Complex || (n -roots_of_1)) . [s,t] in rng ( the multF of F_Complex || (n -roots_of_1)) by FUNCT_1:3;
then A25: [r,(( the multF of F_Complex || (n -roots_of_1)) . [s,t])] in dom ( the multF of F_Complex || (n -roots_of_1)) by A4, A19, ZFMISC_1:87;
( the multF of F_Complex || (n -roots_of_1)) . [s,t] = multcomplex . [s,t] by A2, A24, FUNCT_1:47;
then A26: ( the multF of F_Complex || (n -roots_of_1)) . [r,(( the multF of F_Complex || (n -roots_of_1)) . [s,t])] = multcomplex . (r,(multcomplex . (s,t))) by A2, A25, FUNCT_1:47;
t in the carrier of F_Complex by TARSKI:def 3;
then A27: t is Element of COMPLEX by COMPLFLD:def 1;
( the multF of F_Complex || (n -roots_of_1)) . [r,s] = multcomplex . [r,s] by A2, A22, FUNCT_1:47;
then ( the multF of F_Complex || (n -roots_of_1)) . [(( the multF of F_Complex || (n -roots_of_1)) . [r,s]),t] = multcomplex . ((multcomplex . (r,s)),t) by A2, A23, FUNCT_1:47;
hence (r * s) * t = r * (s * t) by A20, A21, A27, A26, BINOP_1:def 3; :: thesis: verum
end;
then multMagma(# (n -roots_of_1),uM #) is Group by A10, GROUP_1:1;
hence ex b1 being strict Group st
( the carrier of b1 = n -roots_of_1 & the multF of b1 = the multF of F_Complex || (n -roots_of_1) ) ; :: thesis: verum