let G be Group; :: thesis: for A being non empty Subset of G st ( for x, y being Element of G st x in A & y in A holds
x * y = y * x ) holds
gr A is commutative
let A be non empty Subset of G; :: thesis: ( ( for x, y being Element of G st x in A & y in A holds
x * y = y * x ) implies gr A is commutative )
assume A1: for x, y being Element of G st x in A & y in A holds
x * y = y * x ; :: thesis: gr A is commutative
A2: for x, y being Element of G
for i, j being Element of INT st x in A & y in A holds
(x |^ i) * (y |^ j) = (y |^ j) * (x |^ i)
proof
let x, y be Element of G; :: thesis: for i, j being Element of INT st x in A & y in A holds
(x |^ i) * (y |^ j) = (y |^ j) * (x |^ i)
let i, j be Element of INT ; :: thesis: ( x in A & y in A implies (x |^ i) * (y |^ j) = (y |^ j) * (x |^ i) )
assume ( x in A & y in A ) ; :: thesis: (x |^ i) * (y |^ j) = (y |^ j) * (x |^ i)
then x * y = y * x by A1;
hence (x |^ i) * (y |^ j) = (y |^ j) * (x |^ i) by GROUP_1:39; :: thesis: verum
end;
A3: for y being Element of G
for j being Element of INT st y in A holds
for F being FinSequence of G
for I being FinSequence of INT st len F = len I & rng F c= A holds
(Product (F |^ I)) * (y |^ j) = (y |^ j) * (Product (F |^ I))
proof
let y be Element of G; :: thesis: for j being Element of INT st y in A holds
for F being FinSequence of G
for I being FinSequence of INT st len F = len I & rng F c= A holds
(Product (F |^ I)) * (y |^ j) = (y |^ j) * (Product (F |^ I))
let j be Element of INT ; :: thesis: ( y in A implies for F being FinSequence of G
for I being FinSequence of INT st len F = len I & rng F c= A holds
(Product (F |^ I)) * (y |^ j) = (y |^ j) * (Product (F |^ I)) )
assume A4: y in A ; :: thesis: for F being FinSequence of G
for I being FinSequence of INT st len F = len I & rng F c= A holds
(Product (F |^ I)) * (y |^ j) = (y |^ j) * (Product (F |^ I))
set x = y |^ j;
defpred S1[ Nat] means for F being FinSequence of G
for I being FinSequence of INT st len F = $1 & len F = len I & rng F c= A holds
(Product (F |^ I)) * (y |^ j) = (y |^ j) * (Product (F |^ I));
A5: S1[ 0 ]
proof
let F be FinSequence of G; :: thesis: for I being FinSequence of INT st len F = 0 & len F = len I & rng F c= A holds
(Product (F |^ I)) * (y |^ j) = (y |^ j) * (Product (F |^ I))
let I be FinSequence of INT ; :: thesis: ( len F = 0 & len F = len I & rng F c= A implies (Product (F |^ I)) * (y |^ j) = (y |^ j) * (Product (F |^ I)) )
assume A6: ( len F = 0 & len F = len I & rng F c= A ) ; :: thesis: (Product (F |^ I)) * (y |^ j) = (y |^ j) * (Product (F |^ I))
( F = <*> ([#] G) & I = <*> INT ) by A6;
then F |^ I = <*> ([#] G) by GROUP_4:21;
then A7: Product (F |^ I) = 1_ G by GROUP_4:8;
hence (Product (F |^ I)) * (y |^ j) = y |^ j by GROUP_1:def 4
.= (y |^ j) * (Product (F |^ I)) by A7, GROUP_1:def 4 ;
:: thesis: verum
end;
A8: for k being Nat st S1[k] holds
S1[k + 1]
proof
let k be Nat; :: thesis: ( S1[k] implies S1[k + 1] )
assume A9: S1[k] ; :: thesis: S1[k + 1]
let F be FinSequence of G; :: thesis: for I being FinSequence of INT st len F = k + 1 & len F = len I & rng F c= A holds
(Product (F |^ I)) * (y |^ j) = (y |^ j) * (Product (F |^ I))
let I be FinSequence of INT ; :: thesis: ( len F = k + 1 & len F = len I & rng F c= A implies (Product (F |^ I)) * (y |^ j) = (y |^ j) * (Product (F |^ I)) )
assume A10: ( len F = k + 1 & len F = len I & rng F c= A ) ; :: thesis: (Product (F |^ I)) * (y |^ j) = (y |^ j) * (Product (F |^ I))
reconsider g = F /. (k + 1) as Element of G ;
reconsider i = I /. (k + 1) as Element of INT ;
reconsider F0 = F | k as FinSequence of G ;
reconsider I0 = I | k as FinSequence of INT ;
rng F0 c= rng F by RELAT_1:70;
then A11: rng F0 c= A by A10;
reconsider F1 = <*g*> as FinSequence of G ;
reconsider I1 = <*i*> as FinSequence of INT ;
A12: <*(@ i)*> = I1 by GROUP_4:def 1;
k + 1 in Seg (k + 1) by FINSEQ_1:4;
then A13: k + 1 in dom F by A10, FINSEQ_1:def 3;
then F /. (k + 1) = F . (k + 1) by PARTFUN1:def 6;
then A14: F = F0 ^ F1 by A10, FINSEQ_3:55;
k + 1 in Seg (k + 1) by FINSEQ_1:4;
then k + 1 in dom I by A10, FINSEQ_1:def 3;
then A15: I /. (k + 1) = I . (k + 1) by PARTFUN1:def 6;
g = F . (k + 1) by A13, PARTFUN1:def 6;
then A17: g in A by A10, A13, FUNCT_1:3;
( k <= len F & k <= len I ) by A10, XREAL_1:31;
then A18: ( len F0 = k & len I0 = k ) by FINSEQ_1:17;
A19: ( len F1 = 1 & len I1 = 1 ) by FINSEQ_1:39;
A20: F |^ I = (F0 ^ F1) |^ (I0 ^ I1) by A10, A14, A15, FINSEQ_3:55
.= (F0 |^ I0) ^ (F1 |^ I1) by A18, A19, GROUP_4:19
.= (F0 |^ I0) ^ <*(g |^ i)*> by A12, GROUP_4:22 ;
hence (Product (F |^ I)) * (y |^ j) = ((Product (F0 |^ I0)) * (g |^ i)) * (y |^ j) by GROUP_4:6
.= (Product (F0 |^ I0)) * ((g |^ i) * (y |^ j)) by GROUP_1:def 3
.= (Product (F0 |^ I0)) * ((y |^ j) * (g |^ i)) by A2, A4, A17
.= ((Product (F0 |^ I0)) * (y |^ j)) * (g |^ i) by GROUP_1:def 3
.= ((y |^ j) * (Product (F0 |^ I0))) * (g |^ i) by A9, A11, A18
.= (y |^ j) * ((Product (F0 |^ I0)) * (g |^ i)) by GROUP_1:def 3
.= (y |^ j) * (Product (F |^ I)) by A20, GROUP_4:6 ;
:: thesis: verum
end;
for k being Nat holds S1[k] from NAT_1:sch 2(A5, A8);
 hence for F being FinSequence of G
for I being FinSequence of INT st len F = len I & rng F c= A holds
(Product (F |^ I)) * (y |^ j) = (y |^ j) * (Product (F |^ I)) ; :: thesis: verum
end;
A22: for x, g being Element of G
for i being Element of INT st x in gr A & g in A holds
x * (g |^ i) = (g |^ i) * x
proof
let x, g be Element of G; :: thesis: for i being Element of INT st x in gr A & g in A holds
x * (g |^ i) = (g |^ i) * x
let i be Element of INT ; :: thesis: ( x in gr A & g in A implies x * (g |^ i) = (g |^ i) * x )
assume A23: ( x in gr A & g in A ) ; :: thesis: x * (g |^ i) = (g |^ i) * x
consider F being FinSequence of G, I being FinSequence of INT such that
A24: ( len F = len I & rng F c= A & Product (F |^ I) = x ) by A23, GROUP_4:28;
thus x * (g |^ i) = (g |^ i) * x by A3, A23, A24; :: thesis: verum
end;
A25: for x being Element of G st x in gr A holds
for F being FinSequence of G
for I being FinSequence of INT st len F = len I & rng F c= A holds
(Product (F |^ I)) * x = x * (Product (F |^ I))
proof
let x be Element of G; :: thesis: ( x in gr A implies for F being FinSequence of G
for I being FinSequence of INT st len F = len I & rng F c= A holds
(Product (F |^ I)) * x = x * (Product (F |^ I)) )
assume A26: x in gr A ; :: thesis: for F being FinSequence of G
for I being FinSequence of INT st len F = len I & rng F c= A holds
(Product (F |^ I)) * x = x * (Product (F |^ I))
defpred S1[ Nat] means for x being Element of G st x in gr A holds
for F being FinSequence of G
for I being FinSequence of INT st len F = $1 & len F = len I & rng F c= A holds
(Product (F |^ I)) * x = x * (Product (F |^ I));
A27: S1[ 0 ]
proof
let x be Element of G; :: thesis: ( x in gr A implies for F being FinSequence of G
for I being FinSequence of INT st len F = 0 & len F = len I & rng F c= A holds
(Product (F |^ I)) * x = x * (Product (F |^ I)) )
assume x in gr A ; :: thesis: for F being FinSequence of G
for I being FinSequence of INT st len F = 0 & len F = len I & rng F c= A holds
(Product (F |^ I)) * x = x * (Product (F |^ I))
let F be FinSequence of G; :: thesis: for I being FinSequence of INT st len F = 0 & len F = len I & rng F c= A holds
(Product (F |^ I)) * x = x * (Product (F |^ I))
let I be FinSequence of INT ; :: thesis: ( len F = 0 & len F = len I & rng F c= A implies (Product (F |^ I)) * x = x * (Product (F |^ I)) )
assume A29: ( len F = 0 & len F = len I & rng F c= A ) ; :: thesis: (Product (F |^ I)) * x = x * (Product (F |^ I))
( F = <*> ([#] G) & I = <*> INT ) by A29;
then F |^ I = <*> the carrier of G by GROUP_4:21;
then A30: Product (F |^ I) = 1_ G by GROUP_4:8;
hence (Product (F |^ I)) * x = x by GROUP_1:def 4
.= x * (Product (F |^ I)) by A30, GROUP_1:def 4 ;
:: thesis: verum
end;
A31: for k being Nat st S1[k] holds
S1[k + 1]
proof
let k be Nat; :: thesis: ( S1[k] implies S1[k + 1] )
assume A32: S1[k] ; :: thesis: S1[k + 1]
let x be Element of G; :: thesis: ( x in gr A implies for F being FinSequence of G
for I being FinSequence of INT st len F = k + 1 & len F = len I & rng F c= A holds
(Product (F |^ I)) * x = x * (Product (F |^ I)) )
assume A33: x in gr A ; :: thesis: for F being FinSequence of G
for I being FinSequence of INT st len F = k + 1 & len F = len I & rng F c= A holds
(Product (F |^ I)) * x = x * (Product (F |^ I))
let F be FinSequence of G; :: thesis: for I being FinSequence of INT st len F = k + 1 & len F = len I & rng F c= A holds
(Product (F |^ I)) * x = x * (Product (F |^ I))
let I be FinSequence of INT ; :: thesis: ( len F = k + 1 & len F = len I & rng F c= A implies (Product (F |^ I)) * x = x * (Product (F |^ I)) )
assume A34: ( len F = k + 1 & len F = len I & rng F c= A ) ; :: thesis: (Product (F |^ I)) * x = x * (Product (F |^ I))
reconsider g = F /. (k + 1) as Element of G ;
reconsider i = I /. (k + 1) as Element of INT ;
reconsider F0 = F | k as FinSequence of G ;
reconsider I0 = I | k as FinSequence of INT ;
rng F0 c= rng F by RELAT_1:70;
then A35: rng F0 c= A by A34;
reconsider F1 = <*g*> as FinSequence of G ;
reconsider I1 = <*i*> as FinSequence of INT ;
A36: <*(@ i)*> = I1 by GROUP_4:def 1;
k + 1 in Seg (k + 1) by FINSEQ_1:4;
then A37: k + 1 in dom F by A34, FINSEQ_1:def 3;
then F /. (k + 1) = F . (k + 1) by PARTFUN1:def 6;
then A38: F = F0 ^ F1 by A34, FINSEQ_3:55;
k + 1 in Seg (k + 1) by FINSEQ_1:4;
then k + 1 in dom I by A34, FINSEQ_1:def 3;
then A39: I /. (k + 1) = I . (k + 1) by PARTFUN1:def 6;
g = F . (k + 1) by A37, PARTFUN1:def 6;
then A40: g in A by A34, A37, FUNCT_1:3;
( k <= len F & k <= len I ) by A34, XREAL_1:31;
then A41: ( len F0 = k & len I0 = k ) by FINSEQ_1:17;
A42: ( len F1 = 1 & len I1 = 1 ) by FINSEQ_1:39;
A43: F |^ I = (F0 ^ F1) |^ (I0 ^ I1) by A34, A38, A39, FINSEQ_3:55
.= (F0 |^ I0) ^ (F1 |^ I1) by A41, A42, GROUP_4:19
.= (F0 |^ I0) ^ <*(g |^ i)*> by A36, GROUP_4:22 ;
hence (Product (F |^ I)) * x = ((Product (F0 |^ I0)) * (g |^ i)) * x by GROUP_4:6
.= (Product (F0 |^ I0)) * ((g |^ i) * x) by GROUP_1:def 3
.= (Product (F0 |^ I0)) * (x * (g |^ i)) by A22, A33, A40
.= ((Product (F0 |^ I0)) * x) * (g |^ i) by GROUP_1:def 3
.= (x * (Product (F0 |^ I0))) * (g |^ i) by A32, A33, A35, A41
.= x * ((Product (F0 |^ I0)) * (g |^ i)) by GROUP_1:def 3
.= x * (Product (F |^ I)) by A43, GROUP_4:6 ;
:: thesis: verum
end;
for k being Nat holds S1[k] from NAT_1:sch 2(A27, A31);
 hence for F being FinSequence of G
for I being FinSequence of INT st len F = len I & rng F c= A holds
(Product (F |^ I)) * x = x * (Product (F |^ I)) by A26; :: thesis: verum
end;
for x, y being Element of (gr A) holds x * y = y * x
proof
let x, y be Element of (gr A); :: thesis: x * y = y * x
A45: x in gr A ;
x in G by GROUP_2:41;
then reconsider x0 = x as Element of G ;
consider F being FinSequence of G, I being FinSequence of INT such that
A46: ( len F = len I & rng F c= A & Product (F |^ I) = x0 ) by A45, GROUP_4:28;
y in G by GROUP_2:41;
then reconsider z = y as Element of G ;
A47: z in gr A ;
thus x * y = (Product (F |^ I)) * z by A46, GROUP_2:43
.= z * (Product (F |^ I)) by A25, A46, A47
.= y * x by A46, GROUP_2:43 ; :: thesis: verum
end;
hence gr A is commutative by GROUP_1:def 12; :: thesis: verum