let R be Ring; :: thesis: for n being Nat
for A being Matrix of n,R
for z being Element of R st n > 0 & A = z * (1. (R,n)) & A is invertible holds
z in UnitGroup R
let n be Nat; :: thesis: for A being Matrix of n,R
for z being Element of R st n > 0 & A = z * (1. (R,n)) & A is invertible holds
z in UnitGroup R
let A be Matrix of n,R; :: thesis: for z being Element of R st n > 0 & A = z * (1. (R,n)) & A is invertible holds
z in UnitGroup R
let z be Element of R; :: thesis: ( n > 0 & A = z * (1. (R,n)) & A is invertible implies z in UnitGroup R )
assume A1: n > 0 ; :: thesis: ( not A = z * (1. (R,n)) or not A is invertible or z in UnitGroup R )
assume A2: A = z * (1. (R,n)) ; :: thesis: ( not A is invertible or z in UnitGroup R )
assume A is invertible ; :: thesis: z in UnitGroup R
then consider M2 being Matrix of n,R such that
A3: A is_reverse_of M2 by MATRIX_6:def 3;
A4: ( A * M2 = M2 * A & A * M2 = 1. (R,n) ) by A3, MATRIX_6:def 2;
then A5: 1. (R,n) = z * ((1. (R,n)) * M2) by A2, Th29
.= z * M2 by MATRIX_3:18 ;
A6: ( [1,1] in Indices M2 & [1,1] in Indices (1. (R,n)) )

proof

0 < 0 + n by A1;
then 1 <= n by NAT_1:19;
hence ( [1,1] in Indices M2 & [1,1] in Indices (1. (R,n)) ) by MATRIX_0:31; :: thesis: verum

end;

then A7: 1. R = (1. (R,n)) * (1,1) by MATRIX_1:def 3
.= z * (M2 * (1,1)) by A5, A6, MATRIX_3:def 5 ;
A8: 1. (R,n) = (M2 * z) * (1. (R,n)) by A2, A4, Th24
.= M2 * z by MATRIX_3:19 ;
1. R = (1. (R,n)) * (1,1) by A6, MATRIX_1:def 3
.= (M2 * (1,1)) * z by A6, A8, MATRIX_3:def 6 ;
then z is unital by A7, GCD_1:def 2;
then z in the carrier of (UnitGroup R) ;
hence z in UnitGroup R by STRUCT_0:def 5; :: thesis: verum