let R be Ring; :: thesis: for n being Nat
for X being invertible Matrix of n,R st n = 1 holds
( X in center (GL (n,R)) iff ex z being Element of R st
( z in center (UnitGroup R) & X = z * (1. (R,n)) ) )
let n be Nat; :: thesis: for X being invertible Matrix of n,R st n = 1 holds
( X in center (GL (n,R)) iff ex z being Element of R st
( z in center (UnitGroup R) & X = z * (1. (R,n)) ) )
let X be invertible Matrix of n,R; :: thesis: ( n = 1 implies ( X in center (GL (n,R)) iff ex z being Element of R st
( z in center (UnitGroup R) & X = z * (1. (R,n)) ) ) )
reconsider g = X as Element of (GL (n,R)) by Th126;
assume A1: n = 1 ; :: thesis: ( X in center (GL (n,R)) iff ex z being Element of R st
( z in center (UnitGroup R) & X = z * (1. (R,n)) ) )

hereby :: thesis: ( ex z being Element of R st
( z in center (UnitGroup R) & X = z * (1. (R,n)) ) implies X in center (GL (n,R)) )

assume A2: X in center (GL (n,R)) ; :: thesis: ex z being Element of R st
( z in center (UnitGroup R) & X = z * (1. (R,n)) )
for Y being invertible Matrix of n,R holds X * Y = Y * X

proof

let Y be invertible Matrix of n,R; :: thesis: X * Y = Y * X
reconsider h = Y as Element of (GL (n,R)) by Th126;
thus X * Y = g * h by Th127
.= h * g by A2, GROUP_5:77
.= Y * X by Th127 ; :: thesis: verum

end;

then consider z being Element of R such that
A3: ( z in center (UnitGroup R) & X = z * (1. (R,n)) ) by A1, Th123;
take z = z; :: thesis: ( z in center (UnitGroup R) & X = z * (1. (R,n)) )
thus z in center (UnitGroup R) by A3; :: thesis: X = z * (1. (R,n))
thus X = z * (1. (R,n)) by A3; :: thesis: verum

end;

given z being Element of R such that A4: ( z in center (UnitGroup R) & X = z * (1. (R,n)) ) ; :: thesis: X in center (GL (n,R))
for h being Element of (GL (n,R)) holds g * h = h * g

proof

let h be Element of (GL (n,R)); :: thesis: g * h = h * g
reconsider Y = h as invertible Matrix of n,R by Th126;
A5: Y = (Y * (1,1)) * (1. (R,1)) by A1, Th38;
set Y11 = Y * (1,1);
A6: Y * (1,1) in UnitGroup R by A1, A5, Th121;
thus h * g = Y * X by Th127
.= (((Y * (1,1)) * (1. (R,n))) * z) * (1. (R,n)) by A1, A4, A5, Th102
.= (((Y * (1,1)) * z) * (1. (R,n))) * (1. (R,n)) by Th101
.= ((z * (Y * (1,1))) * (1. (R,n))) * (1. (R,n)) by A4, A6, Th135
.= ((z * (1. (R,n))) * (Y * (1,1))) * (1. (R,n)) by Th101
.= (z * (1. (R,n))) * ((Y * (1,1)) * (1. (R,n))) by Th102
.= g * h by A1, A4, A5, Th127 ; :: thesis: verum

end;

hence X in center (GL (n,R)) by GROUP_5:77; :: thesis: verum