let R be Ring; :: thesis: for n being Nat
for A being invertible Matrix of n,R st ( for B being invertible Matrix of n,R holds A * B = B * A ) holds
( ( n = 1 implies ex z being Element of R st
( z in center (UnitGroup R) & A = z * (1. (R,n)) ) ) & ( n <> 1 implies ex z being Element of R st
( z in center R & z in UnitGroup R & A = z * (1. (R,n)) ) ) )
let n be Nat; :: thesis: for A being invertible Matrix of n,R st ( for B being invertible Matrix of n,R holds A * B = B * A ) holds
( ( n = 1 implies ex z being Element of R st
( z in center (UnitGroup R) & A = z * (1. (R,n)) ) ) & ( n <> 1 implies ex z being Element of R st
( z in center R & z in UnitGroup R & A = z * (1. (R,n)) ) ) )
let A be invertible Matrix of n,R; :: thesis: ( ( for B being invertible Matrix of n,R holds A * B = B * A ) implies ( ( n = 1 implies ex z being Element of R st
( z in center (UnitGroup R) & A = z * (1. (R,n)) ) ) & ( n <> 1 implies ex z being Element of R st
( z in center R & z in UnitGroup R & A = z * (1. (R,n)) ) ) ) )
assume A1: for B being invertible Matrix of n,R holds A * B = B * A ; :: thesis: ( ( n = 1 implies ex z being Element of R st
( z in center (UnitGroup R) & A = z * (1. (R,n)) ) ) & ( n <> 1 implies ex z being Element of R st
( z in center R & z in UnitGroup R & A = z * (1. (R,n)) ) ) )
thus ( n = 1 implies ex z being Element of R st
( z in center (UnitGroup R) & A = z * (1. (R,n)) ) ) :: thesis: ( n <> 1 implies ex z being Element of R st
( z in center R & z in UnitGroup R & A = z * (1. (R,n)) ) )

proof

assume A2: n = 1 ; :: thesis: ex z being Element of R st
( z in center (UnitGroup R) & A = z * (1. (R,n)) )
consider z being Element of R such that
A3: A = z * (1. (R,n)) by A1, Th122;
take z ; :: thesis: ( z in center (UnitGroup R) & A = z * (1. (R,n)) )
z in UnitGroup R by A2, A3, Th121;
then reconsider z9 = z as Element of (UnitGroup R) by STRUCT_0:def 5;
A4: ( [1,1] in Indices A & [1,1] in Indices (1. (R,n)) ) by A2, MATRIX_0:31;
for x9 being Element of (UnitGroup R) holds z9 * x9 = x9 * z9

proof

let x9 be Element of (UnitGroup R); :: thesis: z9 * x9 = x9 * z9
x9 in units R ;
then reconsider x = x9 as Element of R ;
A5: x * (1. (R,n)) is invertible by Th120, STRUCT_0:def 5;
A6: (x * z) * (1. (R,n)) = ((x * z) * (1. (R,n))) * (1. (R,n)) by MATRIX_3:19
.= ((x * (1. (R,n))) * z) * (1. (R,n)) by Th101
.= (x * (1. (R,n))) * (z * (1. (R,n))) by Th102
.= A * (x * (1. (R,n))) by A5, A1, A3
.= ((z * (1. (R,n))) * x) * (1. (R,n)) by A3, Th102
.= ((z * x) * (1. (R,n))) * (1. (R,n)) by Th101
.= (z * x) * (1. (R,n)) by MATRIX_3:19 ;
thus x9 * z9 = (x * z) * (1. R) by Th110
.= (x * z) * ((1. (R,n)) * (1,1)) by A4, MATRIX_1:def 3
.= ((x * z) * (1. (R,n))) * (1,1) by A4, MATRIX_3:def 5
.= (z * x) * ((1. (R,n)) * (1,1)) by A6, A4, MATRIX_3:def 5
.= (z * x) * (1. R) by A4, MATRIX_1:def 3
.= z9 * x9 by Th110 ; :: thesis: verum

end;

hence z in center (UnitGroup R) by GROUP_5:77; :: thesis: A = z * (1. (R,n))
thus A = z * (1. (R,n)) by A3; :: thesis: verum

end;

assume A7: n <> 1 ; :: thesis: ex z being Element of R st
( z in center R & z in UnitGroup R & A = z * (1. (R,n)) )

per cases ( n = 0 or n > 0 ) ;

suppose n = 0 ; :: thesis: ex z being Element of R st
( z in center R & z in UnitGroup R & A = z * (1. (R,n)) )

then ex z being Element of R st
( z in center R & z in UnitGroup R & z in center (UnitGroup R) & A = z * (1. (R,n)) ) by Lm3;
hence ex z being Element of R st
( z in center R & z in UnitGroup R & A = z * (1. (R,n)) ) ; :: thesis: verum

end;

suppose A8: n > 0 ; :: thesis: ex z being Element of R st
( z in center R & z in UnitGroup R & A = z * (1. (R,n)) )

then A9: n >= 2 by A7, NAT_1:23;
consider z being Element of R such that
A10: A = z * (1. (R,n)) by A1, Th122;
take z ; :: thesis: ( z in center R & z in UnitGroup R & A = z * (1. (R,n)) )
for x being Element of R holds x * z = z * x

proof

let x be Element of R; :: thesis: x * z = z * x
set M = (1. (R,n)) + (x * (canMat (1,2,n,R)));
(1. (R,n)) + (x * (canMat (1,2,n,R))) is invertible Matrix of n,R by Th57;
then ((1. (R,n)) + (x * (canMat (1,2,n,R)))) * A = A * ((1. (R,n)) + (x * (canMat (1,2,n,R)))) by A1;
then A * (x * (canMat (1,2,n,R))) = (x * (canMat (1,2,n,R))) * A by Th58
.= ((x * (canMat (1,2,n,R))) * z) * (1. (R,n)) by A10, Th24
.= (x * (canMat (1,2,n,R))) * z by MATRIX_3:19
.= x * ((canMat (1,2,n,R)) * z) by Th26
.= x * (z * (canMat (1,2,n,R))) by Th56
.= (x * z) * (canMat (1,2,n,R)) by Th27 ;
then A11: (x * z) * (canMat (1,2,n,R)) = ((z * (1. (R,n))) * x) * (canMat (1,2,n,R)) by A10, Th24
.= ((z * x) * (1. (R,n))) * (canMat (1,2,n,R)) by Th101
.= (z * x) * ((1. (R,n)) * (canMat (1,2,n,R))) by Th29
.= (z * x) * (canMat (1,2,n,R)) by MATRIX_3:18 ;
( 1 <= 2 & 2 <= n & 1 <= 1 & 1 <= n ) by A9, XXREAL_0:2;
then A12: [1,2] in Indices (canMat (1,2,n,R)) by MATRIX_0:31;
thus x * z = (x * z) * (1. R)
.= (x * z) * ((canMat (1,2,n,R)) * (1,2)) by A12, Def1
.= ((x * z) * (canMat (1,2,n,R))) * (1,2) by A12, MATRIX_3:def 5
.= (z * x) * ((canMat (1,2,n,R)) * (1,2)) by A11, A12, MATRIX_3:def 5
.= (z * x) * (1. R) by A12, Def1
.= z * x ; :: thesis: verum

end;

hence z in center R by WEDDWITT:17; :: thesis: ( z in UnitGroup R & A = z * (1. (R,n)) )
thus z in UnitGroup R by A8, A10, Th121; :: thesis: A = z * (1. (R,n))
thus A = z * (1. (R,n)) by A10; :: thesis: verum

end;

end;