let n be Nat; :: thesis: for R being commutative Ring
for X being invertible Matrix of n,R holds
( X in center (GL (n,R)) iff ex z being Element of R st
( z in center R & z in UnitGroup R & X = z * (1. (R,n)) ) )
let R be commutative Ring; :: thesis: for X being invertible Matrix of n,R holds
( X in center (GL (n,R)) iff ex z being Element of R st
( z in center R & z in UnitGroup R & X = z * (1. (R,n)) ) )
let X be invertible Matrix of n,R; :: thesis: ( X in center (GL (n,R)) iff ex z being Element of R st
( z in center R & z in UnitGroup R & X = z * (1. (R,n)) ) )

per cases ( n = 1 or n <> 1 ) ;

suppose A1: n = 1 ; :: thesis: ( X in center (GL (n,R)) iff ex z being Element of R st
( z in center R & z in UnitGroup R & X = z * (1. (R,n)) ) )

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

assume X in center (GL (n,R)) ; :: thesis: ex z being Element of R st
( z in center R & z in UnitGroup R & X = z * (1. (R,n)) )
then consider z being Element of R such that
A2: ( z in center (UnitGroup R) & X = z * (1. (R,n)) ) by A1, Th136;
take z = z; :: thesis: ( z in center R & z in UnitGroup R & X = z * (1. (R,n)) )
thus ( z in center R & z in UnitGroup R ) by A2, Th118; :: thesis: X = z * (1. (R,n))
thus X = z * (1. (R,n)) by A2; :: thesis: verum

end;

given z being Element of R such that A3: ( z in center R & z in UnitGroup R & X = z * (1. (R,n)) ) ; :: thesis: X in center (GL (n,R))
z in center (UnitGroup R) by A3, Th118;
hence X in center (GL (n,R)) by A1, A3, Th136; :: thesis: verum

end;

suppose n <> 1 ; :: thesis: ( X in center (GL (n,R)) iff ex z being Element of R st
( z in center R & z in UnitGroup R & X = z * (1. (R,n)) ) )

hence ( X in center (GL (n,R)) iff ex z being Element of R st
( z in center R & z in UnitGroup R & X = z * (1. (R,n)) ) ) by Th134; :: thesis: verum

end;

end;