:: General Linear Group over Arbitrary Rings
:: by Alexander M. Nelson
::
:: Received June 18, 2026
:: Copyright (c) 2026 Association of Mizar Users

theorem Th1: :: MATGRP_0:1

for R1, R2 being Ring
for phi being Function of R1,R2 st phi is linear holds
phi . (1. R1) = 1. R2

proof end;

theorem :: MATGRP_0:2

for R1, R2 being Ring st R1,R2 are_isomorphic holds
( R2 is R1 -isomorphic & R1 is R2 -isomorphic )

proof end;

theorem :: MATGRP_0:3

for R1, R2 being Ring
for phi being Function of R1,R2 st phi is isomorphism holds
for psi being Function of R2,R1 st psi = phi " holds
psi is bijective

proof end;

theorem Th11: :: MATGRP_0:4

for R1, R2 being Ring
for phi being Function of R1,R2 st phi is isomorphism holds
for x being Element of R1 st phi . x = 1. R2 holds
x = 1. R1

proof end;

theorem Th12: :: MATGRP_0:5

for G1, G2 being Group st G1,G2 are_isomorphic holds
center G1, center G2 are_isomorphic

proof end;

Lm1: for R being Ring holds
( center R is commutative & center R is Subring of R )

proof end;

registration

let R be Ring;

cluster non empty left_add-cancelable right_add-cancelable add-cancelable left_complementable right_complementable complementable strict right-distributive left-distributive right_unital well-unital distributive left_unital Abelian add-associative right_zeroed zeroed unital associative commutative left_zeroed add-left-invertible add-right-invertible Loop-like for Subring of R;

existence
ex b₁ being Subring of R st
( b₁ is strict & b₁ is commutative & not b₁ is empty )

proof end;

end;

definition

let R be Ring;
:: original: center
redefine func center R -> non empty strict commutative Subring of R;
coherence
center R is non empty strict commutative Subring of R by Lm1;

end;

theorem Th13: :: MATGRP_0:6

for R being commutative Ring
for x being object st x in R holds
x in center R

proof end;

theorem Th14: :: MATGRP_0:7

for R being commutative Ring
for x being Element of R holds x in center R

proof end;

theorem Th15: :: MATGRP_0:8

for R being commutative Ring holds the carrier of (center R) = the carrier of R

proof end;

theorem :: MATGRP_0:9

for R being strict commutative Ring holds center R = R

proof end;

theorem Th17: :: MATGRP_0:10

for R being Ring
for m being Nat
for A being Matrix of R st width (0. (R,m,(len A))) = len A holds
(0. (R,m,(len A))) * A = 0. (R,m,(width A))

proof end;

theorem Th18: :: MATGRP_0:11

for n being Nat
for R being Ring
for A being Matrix of R st n = width (0. (R,(width A),n)) holds
A * (0. (R,(width A),n)) = 0. (R,(len A),n)

proof end;

theorem Th19: :: MATGRP_0:12

for R being Ring
for i, k, m, n being Nat
for A being Matrix of m,n,R st i in dom (0. (R,m)) holds
(Line ((0. (R,m)),i)) "*" (Col (A,k)) = 0. R

proof end;

theorem Th20: :: MATGRP_0:13

for R being Ring
for i, k, m, n being Nat
for A being Matrix of m,n,R st k in dom (0. (R,n)) holds
(Line (A,i)) "*" (Col ((0. (R,n)),k)) = 0. R

proof end;

theorem Th21: :: MATGRP_0:14

for R being Ring
for i, k, m, n being Nat
for A being Matrix of m,n,R st i in dom (1. (R,m)) & i in dom A holds
(Line ((1. (R,m)),i)) "*" (Col (A,k)) = A * (i,k)

proof end;

theorem Th23: :: MATGRP_0:15

for R being Ring
for i, k, m, n being Nat
for A being Matrix of m,n,R st k in dom A & k in dom (1. (R,n)) holds
(Line (A,i)) "*" (Col ((1. (R,n)),k)) = A * (i,k)

proof end;

theorem Th24: :: MATGRP_0:16

for R being Ring
for n, k, m being Nat st ( k = 0 implies m = 0 ) holds
for r being Element of R
for A being Matrix of k,m,R
for B being Matrix of m,n,R holds A * (r * B) = (A * r) * B

proof end;

theorem Th26: :: MATGRP_0:17

for R being Ring
for r1, r2 being Element of R
for A being Matrix of R holds (r1 * A) * r2 = r1 * (A * r2)

proof end;

theorem Th27: :: MATGRP_0:18

for R being Ring
for r1, r2 being Element of R
for A being Matrix of R holds r1 * (r2 * A) = (r1 * r2) * A

proof end;

:: MATRIX_5:24 generalized and weakened

theorem Th28: :: MATGRP_0:19

for R being Ring
for n being Nat
for r being Element of R holds r * (0. (R,n)) = 0. (R,n)

proof end;

theorem Th29: :: MATGRP_0:20

for R being Ring
for n, k, m being Nat st ( k = 0 implies m = 0 ) holds
for r being Element of R
for A being Matrix of k,m,R
for B being Matrix of m,n,R holds (r * A) * B = r * (A * B)

proof end;

theorem :: MATGRP_0:21

for R being Ring
for A being Matrix of R
for r being Element of R holds (- r) * A = - (r * A)

proof end;

theorem :: MATGRP_0:22

for R being Ring
for A being Matrix of R holds (1. R) * A = A ;

theorem Th33: :: MATGRP_0:23

for D being non empty set
for M being Matrix of 1,D holds M = <*<*(M * (1,1))*>*>

proof end;

theorem Th34: :: MATGRP_0:24

for L being non empty ZeroOneStr holds 1. (L,1) = <*<*(1. L)*>*>

proof end;

theorem Th35: :: MATGRP_0:25

for R being Ring
for x, y being Element of R
for M1, M2 being Matrix of 1,R st M1 = <*<*x*>*> & M2 = <*<*y*>*> holds
M1 * M2 = <*<*(x * y)*>*> by MATRIX_3:20;

theorem Th36: :: MATGRP_0:26

for R being Ring
for x, y being Element of R
for M1, M2 being Matrix of 1,R st M1 = <*<*x*>*> & M2 = <*<*y*>*> holds
M1 + M2 = <*<*(x + y)*>*>

proof end;

theorem :: MATGRP_0:27

for R being Ring
for r, s being Element of R holds
( r * <*<*s*>*> = <*<*(r * s)*>*> & <*<*s*>*> * r = <*<*(s * r)*>*> )

proof end;

theorem Th38: :: MATGRP_0:28

for R being Ring
for Y being Matrix of 1,R holds Y = (Y * (1,1)) * (1. (R,1))

proof end;

:: Bourbaki, Algebra~\cite{BourbakiAlgI}, II 10.3 defines these as E_{i,j}

definition

let R be non empty ZeroOneStr ;
let I, K, i, k be Nat;

func canMat (i,k,I,K,R) -> Matrix of I,K,R means :Def1: :: MATGRP_0:def 1
for i2, k2 being Nat st [i2,k2] in Indices it holds
( ( [i,k] = [i2,k2] implies it * (i2,k2) = 1. R ) & ( [i,k] <> [i2,k2] implies it * (i2,k2) = 0. R ) );

existence
ex b₁ being Matrix of I,K,R st
for i2, k2 being Nat st [i2,k2] in Indices b₁ holds
( ( [i,k] = [i2,k2] implies b₁ * (i2,k2) = 1. R ) & ( [i,k] <> [i2,k2] implies b₁ * (i2,k2) = 0. R ) )

proof end;

uniqueness
for b₁, b₂ being Matrix of I,K,R st ( for i2, k2 being Nat st [i2,k2] in Indices b₁ holds
( ( [i,k] = [i2,k2] implies b₁ * (i2,k2) = 1. R ) & ( [i,k] <> [i2,k2] implies b₁ * (i2,k2) = 0. R ) ) ) & ( for i2, k2 being Nat st [i2,k2] in Indices b₂ holds
( ( [i,k] = [i2,k2] implies b₂ * (i2,k2) = 1. R ) & ( [i,k] <> [i2,k2] implies b₂ * (i2,k2) = 0. R ) ) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def1 defines canMat MATGRP_0:def 1 :
for R being non empty ZeroOneStr
for I, K, i, k being Nat
for b₆ being Matrix of I,K,R holds
( b₆ = canMat (i,k,I,K,R) iff for i2, k2 being Nat st [i2,k2] in Indices b₆ holds
( ( [i,k] = [i2,k2] implies b₆ * (i2,k2) = 1. R ) & ( [i,k] <> [i2,k2] implies b₆ * (i2,k2) = 0. R ) ) );

theorem Th40: :: MATGRP_0:29

for R being Ring
for I, K, i, k, i2, k2 being Nat st [i2,k2] in Indices (canMat (i,k,I,K,R)) holds
( ( i <> i2 implies (canMat (i,k,I,K,R)) * (i2,k2) = 0. R ) & ( k <> k2 implies (canMat (i,k,I,K,R)) * (i2,k2) = 0. R ) & ( i = i2 & k = k2 implies (canMat (i,k,I,K,R)) * (i2,k2) = 1. R ) )

proof end;

theorem Th41: :: MATGRP_0:30

for R being Ring
for I, K, i, k being Nat st not [i,k] in Indices (canMat (i,k,I,K,R)) holds
canMat (i,k,I,K,R) = 0. (R,I,K)

proof end;

theorem :: MATGRP_0:31

for R being non empty ZeroOneStr
for I, K being Nat holds
not ( ( I = 0 implies K = 0 ) & ( K = 0 implies I = 0 ) & not for i, k being Nat holds (canMat (i,k,I,K,R)) @ = canMat (k,i,K,I,R) )

proof end;

theorem Th43: :: MATGRP_0:32

for R being Ring
for i, k, I, K being Nat holds
( len (canMat (i,k,I,K,R)) = I & ( I = 0 implies width (canMat (i,k,I,K,R)) = 0 ) & ( I <> 0 implies width (canMat (i,k,I,K,R)) = K ) ) by MATRIX_0:22, MATRIX_0:23, MATRIX_0:25;

theorem Th44: :: MATGRP_0:33

for R being Ring
for I, K, i, k, i2 being Nat st [i2,k] in Indices (canMat (i,k,I,K,R)) holds
( ( i2 = i implies Line ((canMat (i,k,I,K,R)),i2) = Line ((1. (R,K)),k) ) & ( i2 <> i implies Line ((canMat (i,k,I,K,R)),i2) = Line ((0. (R,K)),k) ) )

proof end;

theorem Th45: :: MATGRP_0:34

for R being Ring
for I, K, i, k, k2 being Nat st [i,k2] in Indices (canMat (i,k,I,K,R)) holds
( ( k2 = k implies Col ((canMat (i,k,I,K,R)),k2) = Col ((1. (R,I)),i) ) & ( k2 <> k implies Col ((canMat (i,k,I,K,R)),k2) = Col ((0. (R,I)),i) ) )

proof end;

:: Bourbaki, Algebra~\cite{BourbakiAlgI}, II 10.3 equation (9)

theorem Th46: :: MATGRP_0:35

for R being Ring
for I, K, L being Nat st I <> 0 & K <> 0 holds
for i, k1, k2, l being Nat st k1 <> k2 holds
(canMat (i,k1,I,K,R)) * (canMat (k2,l,K,L,R)) = 0. (R,I,L)

proof end;

:: Bourbaki, Algebra~\cite{BourbakiAlgI}, II 10.3 equation (9)

theorem Th47: :: MATGRP_0:36

for R being Ring
for I, K, L, i, k, l being Nat st i in Seg I & k in Seg K & l in Seg L holds
(canMat (i,k,I,K,R)) * (canMat (k,l,K,L,R)) = canMat (i,l,I,L,R)

proof end;

theorem Th48: :: MATGRP_0:37

for R being Ring
for I, K, L being Nat st ( I = 0 implies K = 0 ) holds
for i, k, l being Nat st k in Seg K holds
(canMat (i,k,I,K,R)) * (canMat (k,l,K,L,R)) = canMat (i,l,I,L,R)

proof end;

definition

let R be Ring;
let n be Nat;
let i, k be Nat;

func canMat (i,k,n,R) -> Matrix of n,R equals :: MATGRP_0:def 2
canMat (i,k,n,n,R);

coherence
canMat (i,k,n,n,R) is Matrix of n,R ;

end;

:: deftheorem defines canMat MATGRP_0:def 2 :
for R being Ring
for n, i, k being Nat holds canMat (i,k,n,R) = canMat (i,k,n,n,R);

theorem :: MATGRP_0:38

for R being Ring
for n, i, k, i2, k2 being Nat st [i2,k2] in Indices (canMat (i,k,n,R)) holds
( ( i <> i2 implies (canMat (i,k,n,R)) * (i2,k2) = 0. R ) & ( k <> k2 implies (canMat (i,k,n,R)) * (i2,k2) = 0. R ) & ( i = i2 & k = k2 implies (canMat (i,k,n,R)) * (i2,k2) = 1. R ) ) by Th40;

theorem Th50: :: MATGRP_0:39

for R being Ring
for I, i, j1, j2, k being Nat st j1 <> j2 holds
(canMat (i,j1,I,R)) * (canMat (j2,k,I,R)) = 0. (R,I)

proof end;

theorem :: MATGRP_0:40

for R being Ring
for n, i, j being Nat st not [i,j] in Indices (canMat (i,j,n,R)) holds
canMat (i,j,n,R) = 0. (R,n)

proof end;

theorem :: MATGRP_0:41

for R being Ring
for n, i, k, l being Nat st k in Seg n holds
(canMat (i,k,n,R)) * (canMat (k,l,n,R)) = canMat (i,l,n,R) by Th48;

theorem Th54: :: MATGRP_0:42

for R being Ring
for n, i, j being Nat st [i,j] in Indices (canMat (i,j,n,R)) holds
for A being Matrix of n,R
for i2, j2 being Nat st [i2,j2] in Indices A holds
( ( i = i2 implies ((canMat (i,j,n,R)) * A) * (i2,j2) = A * (j,j2) ) & ( i <> i2 implies ((canMat (i,j,n,R)) * A) * (i2,j2) = 0. R ) )

proof end;

theorem Th55: :: MATGRP_0:43

for R being Ring
for n, i, j being Nat st [i,j] in Indices (canMat (i,j,n,R)) holds
for A being Matrix of n,R
for i2, j2 being Nat st [i2,j2] in Indices A holds
( ( j = j2 implies (A * (canMat (i,j,n,R))) * (i2,j2) = A * (i2,i) ) & ( j <> j2 implies (A * (canMat (i,j,n,R))) * (i2,j2) = 0. R ) )

proof end;

theorem Th56: :: MATGRP_0:44

for R being Ring
for n being Nat
for r being Element of R
for i, j being Nat holds (canMat (i,j,n,R)) * r = r * (canMat (i,j,n,R))

proof end;

theorem Th57: :: MATGRP_0:45

for R being Ring
for n, i, j being Nat st i <> j holds
for r being Element of R holds (1. (R,n)) + (r * (canMat (i,j,n,R))) is invertible Matrix of n,R

proof end;

theorem Th58: :: MATGRP_0:46

for R being Ring
for n, i, j being Nat
for r being Element of R
for A being Matrix of n,R holds
( A * ((1. (R,n)) + (r * (canMat (i,j,n,R)))) = ((1. (R,n)) + (r * (canMat (i,j,n,R)))) * A iff A * (r * (canMat (i,j,n,R))) = (r * (canMat (i,j,n,R))) * A )

proof end;

theorem Th59: :: MATGRP_0:47

for R being Ring
for n, i, j being Nat
for A being Matrix of n,R holds
( A * ((1. (R,n)) + (canMat (i,j,n,R))) = ((1. (R,n)) + (canMat (i,j,n,R))) * A iff A * (canMat (i,j,n,R)) = (canMat (i,j,n,R)) * A )

proof end;

:: Now we can prove canMat(i,j,n,R) is triangular when i <> j

theorem Th60: :: MATGRP_0:48

for R being Ring
for n, i, j being Nat st i > j holds
canMat (i,j,n,R) is lower_triangular

proof end;

theorem Th61: :: MATGRP_0:49

for R being Ring
for n, i, j being Nat st i < j holds
canMat (i,j,n,R) is upper_triangular

proof end;

theorem Th62: :: MATGRP_0:50

for R being Ring
for n, i, j being Nat st i > j holds
for r being Element of R holds r * (canMat (i,j,n,R)) is lower_triangular

proof end;

theorem Th63: :: MATGRP_0:51

for R being Ring
for n, i, j being Nat st i < j holds
for r being Element of R holds r * (canMat (i,j,n,R)) is upper_triangular

proof end;

theorem :: MATGRP_0:52

for R being Ring
for n, i, j being Nat st i > j holds
for r being Element of R holds (1. (R,n)) + (r * (canMat (i,j,n,R))) is lower_triangular

proof end;

theorem :: MATGRP_0:53

for R being Ring
for n, i, j being Nat st i < j holds
for r being Element of R holds (1. (R,n)) + (r * (canMat (i,j,n,R))) is upper_triangular

proof end;

theorem Th66: :: MATGRP_0:54

for R being Ring
for n, i, j being Nat st i > j holds
for r being Element of R holds (canMat (i,j,n,R)) * r is lower_triangular

proof end;

theorem Th67: :: MATGRP_0:55

for R being Ring
for n, i, j being Nat st i < j holds
for r being Element of R holds (canMat (i,j,n,R)) * r is upper_triangular

proof end;

theorem :: MATGRP_0:56

for R being Ring
for n, i, j being Nat st i > j holds
for r being Element of R holds (1. (R,n)) + ((canMat (i,j,n,R)) * r) is lower_triangular

proof end;

theorem :: MATGRP_0:57

for R being Ring
for n, i, j being Nat st i < j holds
for r being Element of R holds (1. (R,n)) + ((canMat (i,j,n,R)) * r) is upper_triangular

proof end;

definition

let L be non empty 1-sorted ;
let n be Nat;
let IT be set ;

attr IT is n,L -matrix-membered means :Def3: :: MATGRP_0:def 3
for x being object st x in IT holds
x is Matrix of n,L;

end;

:: deftheorem Def3 defines -matrix-membered MATGRP_0:def 3 :
for L being non empty 1-sorted
for n being Nat
for IT being set holds
( IT is n,L -matrix-membered iff for x being object st x in IT holds
x is Matrix of n,L );

registration

let L be non empty doubleLoopStr ;
let n be Nat;

cluster n -Matrices_over L -> n,L -matrix-membered ;

coherence
n -Matrices_over L is n,L -matrix-membered

proof end;

end;

theorem Th70: :: MATGRP_0:58

for n being Nat
for L being non empty 1-sorted holds n -tuples_on (n -tuples_on the carrier of L) is n,L -matrix-membered

proof end;

registration

let L be non empty 1-sorted ;
let n be Nat;

cluster non empty n,L -matrix-membered for set ;

existence
ex b₁ being set st
( not b₁ is empty & b₁ is n,L -matrix-membered )

proof end;

end;

definition

let L be non empty 1-sorted ;
let n be Nat;
let A be non empty n,L -matrix-membered set ;
:: original: Element
redefine mode Element of A -> Matrix of n,L;
correctness
coherence
for b₁ being Element of A holds b₁ is Matrix of n,L;
by Def3;

end;

definition

let L be non empty 1-sorted ;
let n be Nat;
let IT be 1-sorted ;

attr IT is n,L -matrix-membered means :: MATGRP_0:def 4
the carrier of IT is n,L -matrix-membered ;

end;

:: deftheorem defines -matrix-membered MATGRP_0:def 4 :
for L being non empty 1-sorted
for n being Nat
for IT being 1-sorted holds
( IT is n,L -matrix-membered iff the carrier of IT is n,L -matrix-membered );

theorem :: MATGRP_0:59

for n being Nat
for L being non empty doubleLoopStr
for S being 1-sorted holds
( the carrier of S c= n -Matrices_over L iff S is n,L -matrix-membered )

proof end;

registration

let L be non empty 1-sorted ;
let n be Nat;

cluster non empty n,L -matrix-membered for 1-sorted ;

existence
ex b₁ being 1-sorted st
( not b₁ is empty & b₁ is n,L -matrix-membered )

proof end;

end;

registration

let L be non empty doubleLoopStr ;
let n be Nat;

cluster strict non empty n,L -matrix-membered for 1-sorted ;

existence
ex b₁ being 1-sorted st
( b₁ is strict & not b₁ is empty & b₁ is n,L -matrix-membered )

proof end;

end;

definition

let n be Nat;
let L be non empty doubleLoopStr ;

func matrix_mult (n,L) -> BinOp of (n -Matrices_over L) means :Def5: :: MATGRP_0:def 5
for A, B being Element of n -Matrices_over L holds it . (A,B) = A * B;

existence
ex b₁ being BinOp of (n -Matrices_over L) st
for A, B being Element of n -Matrices_over L holds b₁ . (A,B) = A * B

proof end;

uniqueness
for b₁, b₂ being BinOp of (n -Matrices_over L) st ( for A, B being Element of n -Matrices_over L holds b₁ . (A,B) = A * B ) & ( for A, B being Element of n -Matrices_over L holds b₂ . (A,B) = A * B ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def5 defines matrix_mult MATGRP_0:def 5 :
for n being Nat
for L being non empty doubleLoopStr
for b₃ being BinOp of (n -Matrices_over L) holds
( b₃ = matrix_mult (n,L) iff for A, B being Element of n -Matrices_over L holds b₃ . (A,B) = A * B );

definition

let n be Nat;
let L be non empty doubleLoopStr ;

func matrix_add (n,L) -> BinOp of (n -Matrices_over L) means :Def6: :: MATGRP_0:def 6
for A, B being Element of n -Matrices_over L holds it . (A,B) = A + B;

existence
ex b₁ being BinOp of (n -Matrices_over L) st
for A, B being Element of n -Matrices_over L holds b₁ . (A,B) = A + B

proof end;

uniqueness
for b₁, b₂ being BinOp of (n -Matrices_over L) st ( for A, B being Element of n -Matrices_over L holds b₁ . (A,B) = A + B ) & ( for A, B being Element of n -Matrices_over L holds b₂ . (A,B) = A + B ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def6 defines matrix_add MATGRP_0:def 6 :
for n being Nat
for L being non empty doubleLoopStr
for b₃ being BinOp of (n -Matrices_over L) holds
( b₃ = matrix_add (n,L) iff for A, B being Element of n -Matrices_over L holds b₃ . (A,B) = A + B );

notation

let L be non empty doubleLoopStr ;
let n be Nat;
synonym One (L,n) for 1. (L,n);
synonym Zero (L,n) for 0. (L,n);

end;

definition

let L be non empty doubleLoopStr ;
let n be Nat;
:: original: One
redefine func One (L,n) -> Element of n -Matrices_over L;
correctness
coherence
One (L,n) is Element of n -Matrices_over L;
by MATRIX_1:2;
:: original: Zero
redefine func Zero (L,n) -> Element of n -Matrices_over L;
correctness
coherence
Zero (L,n) is Element of n -Matrices_over L;
;

end;

definition

let L be non empty doubleLoopStr ;
let n be Nat;

func Matrix_ring (n,L) -> strict doubleLoopStr equals :: MATGRP_0:def 7
doubleLoopStr(# (n -Matrices_over L),(matrix_add (n,L)),(matrix_mult (n,L)),(One (L,n)),(Zero (L,n)) #);

coherence
doubleLoopStr(# (n -Matrices_over L),(matrix_add (n,L)),(matrix_mult (n,L)),(One (L,n)),(Zero (L,n)) #) is strict doubleLoopStr ;

end;

:: deftheorem defines Matrix_ring MATGRP_0:def 7 :
for L being non empty doubleLoopStr
for n being Nat holds Matrix_ring (n,L) = doubleLoopStr(# (n -Matrices_over L),(matrix_add (n,L)),(matrix_mult (n,L)),(One (L,n)),(Zero (L,n)) #);

registration

let L be non empty doubleLoopStr ;
let n be Nat;

cluster Matrix_ring (n,L) -> non empty strict n,L -matrix-membered ;

coherence
( Matrix_ring (n,L) is strict & not Matrix_ring (n,L) is empty & Matrix_ring (n,L) is n,L -matrix-membered ) ;

end;

theorem Th72: :: MATGRP_0:60

for n being Nat
for L being non empty doubleLoopStr
for x being object holds
( x is Element of (Matrix_ring (n,L)) iff x is Matrix of n,L ) by MATRIX_1:2;

registration

let L be non empty doubleLoopStr ;

cluster Matrix_ring (0,L) -> trivial strict ;

coherence
Matrix_ring (0,L) is trivial

proof end;

end;

theorem Th73: :: MATGRP_0:61

for n being Nat
for L being non empty doubleLoopStr
for A, B being Matrix of n,L
for X, Y being Element of (Matrix_ring (n,L)) st A = X & B = Y holds
A + B = X + Y by Def6;

theorem :: MATGRP_0:62

for n being Nat
for L being non empty doubleLoopStr
for X, Y being Matrix of n,L
for x, y being Element of n -Matrices_over L st X = x & Y = y holds
X * Y = (matrix_mult (n,L)) . (x,y) by Def5;

theorem Th75: :: MATGRP_0:63

for n being Nat
for L being non empty doubleLoopStr
for A, B being Matrix of n,L
for X, Y being Element of (Matrix_ring (n,L)) st A = X & B = Y holds
A * B = X * Y by Def5;

theorem :: MATGRP_0:64

for R being Ring
for n being Nat
for A, B, C being Matrix of n,R holds (A * B) * C = A * (B * C)

proof end;

theorem :: MATGRP_0:65

for n being Nat
for L being non empty doubleLoopStr holds 1. (L,n) is Element of (Matrix_ring (n,L)) ;

theorem :: MATGRP_0:66

for n being Nat
for L being non empty doubleLoopStr holds 0. (L,n) is Element of (Matrix_ring (n,L)) ;

:: When (the addLoopStr of R) is an Abelian Group, Matrix_ring(n,R)
:: forms an Abelian group under addition

registration

let n be Nat;
let R be non empty right_complementable Abelian add-associative right_zeroed doubleLoopStr ;

cluster Matrix_ring (n,R) -> strict add-associative ;

coherence
Matrix_ring (n,R) is add-associative

proof end;

cluster Matrix_ring (n,R) -> strict right_zeroed ;

coherence
Matrix_ring (n,R) is right_zeroed

proof end;

cluster Matrix_ring (n,R) -> right_complementable strict ;

coherence
Matrix_ring (n,R) is right_complementable

proof end;

cluster Matrix_ring (n,R) -> strict Abelian ;

coherence
Matrix_ring (n,R) is Abelian

proof end;

end;

:: N.B.: the condition that R is a ring could be weakened, if...

registration

let n be Nat;
let R be Ring;

cluster Matrix_ring (n,R) -> strict well-unital ;

coherence
Matrix_ring (n,R) is well-unital

proof end;

cluster Matrix_ring (n,R) -> strict distributive ;

coherence
Matrix_ring (n,R) is distributive

proof end;

cluster Matrix_ring (n,R) -> strict associative ;

coherence
Matrix_ring (n,R) is associative

proof end;

end;

theorem Th79: :: MATGRP_0:67

for R being Ring holds Matrix_ring (1,R),R are_isomorphic

proof end;

theorem Th80: :: MATGRP_0:68

for D, E being non empty set st D c= E holds
for X being Matrix of D holds X is Matrix of E

proof end;

theorem Th81: :: MATGRP_0:69

for m, n being Nat
for D, E being non empty set st D c= E holds
for X being Matrix of m,n,D holds X is Matrix of m,n,E

proof end;

theorem Th82: :: MATGRP_0:70

for R being Ring
for n being Nat
for S being Subring of R
for X being Matrix of n,S holds X is Matrix of n,R

proof end;

theorem Th83: :: MATGRP_0:71

for n being Nat
for S1, S2 being non empty 1-sorted
for X being Matrix of n,S2
for Y being Matrix of n,S1 holds
( ( for i, j being Nat st [i,j] in Indices X holds
X * (i,j) = Y * (i,j) ) iff X = Y )

proof end;

theorem Th85: :: MATGRP_0:72

for R being Ring
for n being Nat
for S being Subring of R holds n -Matrices_over S c= n -Matrices_over R

proof end;

theorem Th86: :: MATGRP_0:73

for R being Ring
for n being Nat
for S being Subring of R
for a, b being Matrix of n,S
for A, B being Matrix of n,R st a = A & b = B holds
a + b = A + B

proof end;

theorem Th87: :: MATGRP_0:74

for R being Ring
for n being Nat
for S being Subring of R holds matrix_add (n,S) = (matrix_add (n,R)) || (n -Matrices_over S)

proof end;

theorem Th88: :: MATGRP_0:75

for R being Ring
for n being Nat
for S being Subring of R
for a being Matrix of n,S
for A being Matrix of n,R st a = A holds
for i being Nat st i in dom a holds
Line (a,i) = Line (A,i)

proof end;

theorem Th89: :: MATGRP_0:76

for R being Ring
for n being Nat
for S being Subring of R
for b being Matrix of n,S
for B being Matrix of n,R st b = B holds
for j being Nat st j in Seg (width b) holds
Col (b,j) = Col (B,j)

proof end;

theorem Th90: :: MATGRP_0:77

for R being Ring
for S being Subring of R
for a being FinSequence of S
for A being FinSequence of R st a = A holds
Sum a = Sum A

proof end;

theorem Th91: :: MATGRP_0:78

for R being Ring
for S being Subring of R
for a, b being FinSequence of S
for A, B being FinSequence of R st a = A & b = B holds
mlt (a,b) = mlt (A,B)

proof end;

theorem Th92: :: MATGRP_0:79

for R being Ring
for n being Nat
for S being Subring of R
for a, b being Matrix of n,S
for A, B being Matrix of n,R st a = A & b = B holds
a * b = A * B

proof end;

theorem Th93: :: MATGRP_0:80

for R being Ring
for n being Nat
for S being Subring of R holds matrix_mult (n,S) = (matrix_mult (n,R)) || (n -Matrices_over S)

proof end;

theorem Th94: :: MATGRP_0:81

for R being Ring
for n being Nat
for S being Subring of R holds 0. (S,n) = 0. (R,n) by C0SP1:def 3;

theorem Th95: :: MATGRP_0:82

for R being Ring
for n being Nat
for S being Subring of R holds 1. (S,n) = 1. (R,n)

proof end;

theorem Th96: :: MATGRP_0:83

for R being Ring
for n being Nat
for S being Subring of R holds
( One (S,n) = One (R,n) & Zero (S,n) = Zero (R,n) ) by Th95, Th94;

:: Extension of scalars for matrix rings

theorem :: MATGRP_0:84

for R being Ring
for n being Nat
for S being Subring of R holds Matrix_ring (n,S) is Subring of Matrix_ring (n,R)

proof end;

theorem Th98: :: MATGRP_0:85

for R being Ring
for z being Element of R st z in center R holds
for A being Matrix of R holds A * z = z * A

proof end;

theorem Th99: :: MATGRP_0:86

for R being Ring
for n being Nat
for z being Element of R st z in center R holds
for A, B being Matrix of n,R st A * B = B * A holds
A * (z * B) = (z * B) * A

proof end;

theorem Th100: :: MATGRP_0:87

for R being Ring
for n being Nat
for z being Element of R st z in center R holds
for A being Matrix of n,R holds A * (z * (1. (R,n))) = (z * (1. (R,n))) * A

proof end;

theorem Th101: :: MATGRP_0:88

for R being Ring
for n being Nat
for x, y being Element of R holds (x * (1. (R,n))) * y = (x * y) * (1. (R,n))

proof end;

theorem Th102: :: MATGRP_0:89

for R being Ring
for n being Nat
for x, y being Element of R holds (x * (1. (R,n))) * (y * (1. (R,n))) = ((x * (1. (R,n))) * y) * (1. (R,n)) by Th24;

:: See, e.g., Bourbaki's "Algebra" VIII~\cite{bourbaki2023algebra} 5 no.3 corollary 2 to theorem 2

theorem Th103: :: MATGRP_0:90

for R being Ring
for n being Nat
for A being Matrix of n,R st ( for B being Matrix of n,R holds A * B = B * A ) holds
ex z being Element of R st
( z in center R & A = z * (1. (R,n)) )

proof end;

theorem Th105: :: MATGRP_0:91

for R being Ring
for n being Nat
for X being Element of (Matrix_ring (n,R))
for A being Matrix of n,R st A = X holds
( X in center (Matrix_ring (n,R)) iff for B being Matrix of n,R holds A * B = B * A )

proof end;

theorem :: MATGRP_0:92

for R being Ring
for n being Nat
for X being Element of (Matrix_ring (n,R)) holds
( X in center (Matrix_ring (n,R)) iff ex z being Element of R st
( z in center R & X = z * (1. (R,n)) ) )

proof end;

definition

let M be non empty multLoopStr ;

func units M -> Subset of M equals :: MATGRP_0:def 8
{ x where x is Element of M : x is unital } ;

coherence
{ x where x is Element of M : x is unital } is Subset of M

proof end;

end;

:: deftheorem defines units MATGRP_0:def 8 :
for M being non empty multLoopStr holds units M = { x where x is Element of M : x is unital } ;

theorem Th107: :: MATGRP_0:93

for M being non empty right_unital multLoopStr
for ell being Element of M holds
( ell is unital iff ell in units M )

proof end;

Th108: for M being non empty right_unital associative multLoopStr
for u, v being unital Element of M holds u * v is unital

proof end;

registration

let M be non empty right_unital associative multLoopStr ;
let u, v be unital Element of M;

cluster u * v -> unital ;

coherence
u * v is unital by Th108;

end;

registration

let M be non empty right_unital associative multLoopStr ;

cluster units M -> the multF of M -binopclosed ;

coherence
units M is the multF of M -binopclosed

proof end;

end;

definition

let M be non empty right_unital associative multLoopStr ;

func UnitGroup M -> strict multMagma equals :: MATGRP_0:def 9
multMagma(# (units M),( the multF of M || (units M)) #);

coherence
multMagma(# (units M),( the multF of M || (units M)) #) is strict multMagma ;

end;

:: deftheorem defines UnitGroup MATGRP_0:def 9 :
for M being non empty right_unital associative multLoopStr holds UnitGroup M = multMagma(# (units M),( the multF of M || (units M)) #);

theorem :: MATGRP_0:94

for M being non empty right_unital associative multLoopStr holds 1. M in UnitGroup M

proof end;

registration

let M be non empty right_unital associative multLoopStr ;

cluster UnitGroup M -> non empty strict ;

coherence
not UnitGroup M is empty

proof end;

end;

theorem Th110: :: MATGRP_0:95

for M being non empty right_unital associative multLoopStr
for a, b being Element of M
for x, y being Element of (UnitGroup M) st a = x & b = y holds
a * b = x * y by FUNCT_1:49, ZFMISC_1:87;

registration

let M be non empty right_unital associative multLoopStr ;

cluster UnitGroup M -> strict associative ;

coherence
UnitGroup M is associative

proof end;

end;

:: Importantly, M is a monoid for UnitGroup M to be Group-like

registration

let M be non empty right_unital left_unital associative multLoopStr ;

cluster UnitGroup M -> strict Group-like ;

coherence
UnitGroup M is Group-like

proof end;

end;

theorem Th111: :: MATGRP_0:96

for M being non empty well-unital associative multLoopStr holds 1_ (UnitGroup M) = 1. M

proof end;

Th112: for R being commutative Ring holds UnitGroup R is commutative

proof end;

registration

let R be commutative Ring;

cluster UnitGroup R -> strict commutative ;

coherence
UnitGroup R is commutative by Th112;

end;

theorem :: MATGRP_0:97

for M being non empty right_unital left_unital associative multLoopStr holds UnitGroup M is strict Group ;

theorem Th114: :: MATGRP_0:98

for G being non empty right_unital left_unital associative multLoopStr st G is Group-like holds
units G = the carrier of G

proof end;

:: Morally: UnitGroup of a strict group G is identical to G itself

theorem :: MATGRP_0:99

for G being non empty right_unital left_unital associative multLoopStr st G is Group-like holds
UnitGroup G = multMagma(# the carrier of G, the multF of G #)

proof end;

:: Now, we can see that UnitGroup R coincides with MultGroup R when R
:: is a Skew-Field. First, a useful lemma.

theorem Th116: :: MATGRP_0:100

for R being Skew-Field holds NonZero R = units R

proof end;

theorem Th117: :: MATGRP_0:101

for R being Skew-Field holds MultGroup R = UnitGroup R

proof end;

registration

let R be Skew-Field;

identify units R with NonZero R;

correctness
compatibility
units R = NonZero R;
by Th116;

identify UnitGroup R with MultGroup R;

correctness
compatibility
UnitGroup R = MultGroup R;
by Th117;

end;

theorem Th118: :: MATGRP_0:102

for R being commutative Ring
for x being object holds
( ( x in center R & x in UnitGroup R ) iff x in center (UnitGroup R) )

proof end;

:: The converse of this theorem is false for *noncommutative* rings in
:: general. See Tsit Yuen Lam's "First Course in Noncommutative Rings"
:: (Springer, GTM131, 1991), Example (1.7) for a counter-example to
:: the converse.
:: For a summary, see: https://math.stackexchange.com/a/342817/31693

theorem :: MATGRP_0:103

for R being Ring
for x being object st x in center R & x in UnitGroup R holds
x in center (UnitGroup R)

proof end;

theorem Th120: :: MATGRP_0:104

for R being Ring
for n being Nat
for A being Matrix of n,R
for z being Element of R st A = z * (1. (R,n)) & z in UnitGroup R holds
A is invertible

proof end;

theorem Th121: :: MATGRP_0:105

for R being Ring
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

proof end;

Th122: for R being Ring
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
ex z being Element of R st A = z * (1. (R,n))

proof end;

Lm3: for R being Ring
for n being Nat
for A being invertible Matrix of n,R st n = 0 holds
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)) )

proof end;

Th123: for R being Ring
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)) ) ) )

proof end;

theorem :: MATGRP_0:106

for R being Ring
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
ex z being Element of R st
( z in center (UnitGroup R) & A = z * (1. (R,n)) )

proof end;

theorem Th125: :: MATGRP_0:107

for R1, R2 being Ring st R1,R2 are_isomorphic holds
UnitGroup R1, UnitGroup R2 are_isomorphic

proof end;

:: This can be weakened to semirings

definition

let n be Nat;
let R be Ring;

func GL (n,R) -> strict Group equals :: MATGRP_0:def 10
UnitGroup (Matrix_ring (n,R));

coherence
UnitGroup (Matrix_ring (n,R)) is strict Group ;

end;

:: deftheorem defines GL MATGRP_0:def 10 :
for n being Nat
for R being Ring holds GL (n,R) = UnitGroup (Matrix_ring (n,R));

registration

let R be Ring;

cluster GL (0,R) -> trivial strict ;

coherence
GL (0,R) is trivial ;

end;

theorem Th126: :: MATGRP_0:108

for R being Ring
for n being Nat
for x being object holds
( x is Element of (GL (n,R)) iff x is invertible Matrix of n,R )

proof end;

registration

let R be Ring;
let n be Nat;

cluster GL (n,R) -> strict n,R -matrix-membered ;

coherence
GL (n,R) is n,R -matrix-membered

proof end;

end;

registration

let R be Ring;
let n be Nat;

cluster the carrier of (GL (n,R)) -> non empty ;

coherence
not the carrier of (GL (n,R)) is empty ;

cluster the carrier of (GL (n,R)) -> n,R -matrix-membered ;

coherence
the carrier of (GL (n,R)) is n,R -matrix-membered by Def3;

end;

theorem Th127: :: MATGRP_0:109

for R being Ring
for n being Nat
for x, y being Element of (GL (n,R))
for X, Y being Matrix of n,R st X = x & Y = y holds
X * Y = x * y

proof end;

scheme :: MATGRP_0:sch 1
GLSubset{ F₁() -> Nat, F₂() -> Ring, P₁[ Matrix of F₂()] } :

ex A being Subset of (GL (F₁(),F₂())) st
for X being invertible Matrix of F₁(),F₂() holds
( X in A iff P₁[X] )

proof end;

scheme :: MATGRP_0:sch 2
GLSubset2{ F₁() -> Nat, F₂() -> Ring, P₁[ Matrix of F₂()] } :

ex A being Subset of (GL (F₁(),F₂())) st
for X being Matrix of F₁(),F₂() st X is invertible holds
( X in A iff P₁[X] )

proof end;

theorem Th128: :: MATGRP_0:110

for R being Ring
for n being Nat
for X being Matrix of n,R holds
( X is Element of (GL (n,R)) iff X is invertible ) by Th126;

theorem Th129: :: MATGRP_0:111

for R being Ring
for n being Nat holds 1. (R,n) is Element of (GL (n,R)) by Th126;

theorem Th130: :: MATGRP_0:112

for R being Ring
for n being Nat holds 1_ (GL (n,R)) = 1. (R,n)

proof end;

theorem Th131: :: MATGRP_0:113

for R being Ring
for n being Nat
for x being Element of (GL (n,R))
for X being invertible Matrix of n,R st x = X holds
x " = X ~

proof end;

theorem :: MATGRP_0:114

for R being Ring
for n being Nat
for g being Element of (GL (n,R))
for X, Y being Matrix of n,R st X = g holds
( Y = (inverse_op (GL (n,R))) . g iff Y is_reverse_of X )

proof end;

scheme :: MATGRP_0:sch 3
GLSubgroup{ F₁() -> Nat, F₂() -> Ring, P₁[ Matrix of F₂()] } :

ex H being strict Subgroup of GL (F₁(),F₂()) st
for X being invertible Matrix of F₁(),F₂() holds
( X in H iff P₁[X] )

provided

A1: for X, Y being invertible Matrix of F₁(),F₂() st P₁[X] & P₁[Y] holds
P₁[X * Y] and
A2: for X being invertible Matrix of F₁(),F₂() st P₁[X] holds
P₁[X ~ ] and
A3: P₁[ 1. (F₂(),F₁())]

proof end;

scheme :: MATGRP_0:sch 4
GLSubgroup2{ F₁() -> Nat, F₂() -> Ring, P₁[ Matrix of F₁(),F₂()] } :

ex H being strict Subgroup of GL (F₁(),F₂()) st
for X being invertible Matrix of F₁(),F₂() holds
( X in H iff P₁[X] )

provided

A1: for X, Y being invertible Matrix of F₁(),F₂() st P₁[X] & P₁[Y] holds
P₁[X * Y] and
A2: for X being invertible Matrix of F₁(),F₂() st P₁[X] holds
P₁[X ~ ] and
A3: P₁[ 1. (F₂(),F₁())]

proof end;

theorem :: MATGRP_0:115

for R being Ring
for n being Nat
for X being Element of (GL (n,R)) st ex z being Element of R st
( z in center R & X = z * (1. (R,n)) ) holds
X in center (GL (n,R))

proof end;

theorem Th134: :: MATGRP_0:116

for R being Ring
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 R & z in UnitGroup R & X = z * (1. (R,n)) ) )

proof end;

theorem Th135: :: MATGRP_0:117

for R being Ring
for r being Element of R st r in center (UnitGroup R) holds
for s being Element of R st s in UnitGroup R holds
r * s = s * r

proof end;

theorem Th136: :: MATGRP_0:118

for R being Ring
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)) ) )

proof end;

:: The results about center GL(1,R) is so surprising at first glance,
:: because our intuition expects the commutative R case to generalize to
:: the general situation. But we're not mistaken, and here's a slick proof.

theorem :: MATGRP_0:119

for R being Ring holds center (GL (1,R)), center (UnitGroup R) are_isomorphic

proof end;

theorem :: MATGRP_0:120

for n being Nat
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)) ) )

proof end;

theorem Th139: :: MATGRP_0:121

for R being Ring
for n being Nat
for S being Subring of R
for M1 being Matrix of n,R
for M2 being Matrix of n,S st M1 = M2 & M2 is invertible holds
M1 is invertible

proof end;

theorem Th140: :: MATGRP_0:122

for R being Ring
for n being Nat
for S being Subring of R holds the carrier of (GL (n,S)) c= the carrier of (GL (n,R))

proof end;

theorem Th141: :: MATGRP_0:123

for R being Ring
for n being Nat
for S being Subring of R holds the multF of (GL (n,S)) = the multF of (GL (n,R)) || the carrier of (GL (n,S))

proof end;

theorem :: MATGRP_0:124

for R being Ring
for n being Nat
for S being Subring of R holds GL (n,S) is strict Subgroup of GL (n,R)

proof end;

theorem Th143: :: MATGRP_0:125

for R being Ring
for n being Nat
for x being Element of (Matrix_ring (n,R)) holds
( x is invertible iff ex X being invertible Matrix of n,R st X = x )

proof end;

registration

let n be Nat;
let R be Ring;

cluster left_add-cancelable right_add-cancelable add-cancelable left_complementable right_complementable complementable invertible for Element of the carrier of (Matrix_ring (n,R));

existence
ex b₁ being Element of (Matrix_ring (n,R)) st b₁ is invertible by Th143;

end;

theorem :: MATGRP_0:126

for R being Ring
for n being Nat
for x being object holds
( x is invertible Element of (Matrix_ring (n,R)) iff x is invertible Matrix of n,R )

proof end;

definition

let n be Nat;
let R be Ring;

func n -invertible_Matrices_over R -> Subset of (n -Matrices_over R) equals :: MATGRP_0:def 11
{ X where X is Element of n -Matrices_over R : X is invertible Matrix of n,R } ;

coherence
{ X where X is Element of n -Matrices_over R : X is invertible Matrix of n,R } is Subset of (n -Matrices_over R)

proof end;

end;

:: deftheorem defines -invertible_Matrices_over MATGRP_0:def 11 :
for n being Nat
for R being Ring holds n -invertible_Matrices_over R = { X where X is Element of n -Matrices_over R : X is invertible Matrix of n,R } ;

theorem Th145: :: MATGRP_0:127

for R being Ring
for n being Nat
for x being object holds
( x in n -invertible_Matrices_over R iff x is invertible Matrix of n,R )

proof end;

registration

let n be Nat;
let R be Ring;

cluster n -invertible_Matrices_over R -> non empty ;

coherence
not n -invertible_Matrices_over R is empty

proof end;

end;

theorem Th146: :: MATGRP_0:128

for R being Ring
for n being Nat holds the carrier of (GL (n,R)) = n -invertible_Matrices_over R

proof end;

theorem :: MATGRP_0:129

for R being Ring
for n being Nat holds n -invertible_Matrices_over R is matrix_mult (n,R) -binopclosed

proof end;

theorem Th148: :: MATGRP_0:130

for R being Ring
for n being Nat holds One (R,n) is_a_unity_wrt matrix_mult (n,R)

proof end;

registration

let n be Nat;
let R be Ring;

cluster matrix_mult (n,R) -> associative ;

coherence
matrix_mult (n,R) is associative

proof end;

cluster matrix_mult (n,R) -> having_a_unity ;

coherence
matrix_mult (n,R) is having_a_unity

proof end;

end;

theorem :: MATGRP_0:131

for R being Ring
for n being Nat holds One (R,n) = the_unity_wrt (matrix_mult (n,R))

proof end;

definition

let n be Nat;
let R be Ring;

func matrix_inv (n,R) -> UnOp of (n -invertible_Matrices_over R) means :Def12: :: MATGRP_0:def 12
for x being Element of n -invertible_Matrices_over R
for X being invertible Matrix of n,R st x = X holds
it . x = X ~ ;

existence
ex b₁ being UnOp of (n -invertible_Matrices_over R) st
for x being Element of n -invertible_Matrices_over R
for X being invertible Matrix of n,R st x = X holds
b₁ . x = X ~

proof end;

uniqueness
for b₁, b₂ being UnOp of (n -invertible_Matrices_over R) st ( for x being Element of n -invertible_Matrices_over R
for X being invertible Matrix of n,R st x = X holds
b₁ . x = X ~ ) & ( for x being Element of n -invertible_Matrices_over R
for X being invertible Matrix of n,R st x = X holds
b₂ . x = X ~ ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def12 defines matrix_inv MATGRP_0:def 12 :
for n being Nat
for R being Ring
for b₃ being UnOp of (n -invertible_Matrices_over R) holds
( b₃ = matrix_inv (n,R) iff for x being Element of n -invertible_Matrices_over R
for X being invertible Matrix of n,R st x = X holds
b₃ . x = X ~ );

theorem Th150: :: MATGRP_0:132

for R being Ring
for n being Nat holds inverse_op (GL (n,R)) = matrix_inv (n,R)

proof end;

theorem Th151: :: MATGRP_0:133

for R being Ring
for n being Nat
for F being BinOp of (n -invertible_Matrices_over R) st F = (matrix_mult (n,R)) || (n -invertible_Matrices_over R) holds
One (R,n) is_a_unity_wrt F

proof end;

Th152: for R being Ring
for n being Nat
for F being BinOp of (n -invertible_Matrices_over R) st F = (matrix_mult (n,R)) || (n -invertible_Matrices_over R) holds
ex e1 being Element of n -invertible_Matrices_over R st e1 is_a_unity_wrt F

proof end;

theorem Th153: :: MATGRP_0:134

for R being Ring
for n being Nat
for F being BinOp of (n -invertible_Matrices_over R) st F = (matrix_mult (n,R)) || (n -invertible_Matrices_over R) holds
One (R,n) = the_unity_wrt F

proof end;

theorem Th154: :: MATGRP_0:135

for R being Ring
for n being Nat
for F being BinOp of (n -invertible_Matrices_over R) st F = (matrix_mult (n,R)) || (n -invertible_Matrices_over R) holds
matrix_inv (n,R) is_an_inverseOp_wrt F

proof end;

Th155: for R being Ring
for n being Nat
for F being BinOp of (n -invertible_Matrices_over R) st F = (matrix_mult (n,R)) || (n -invertible_Matrices_over R) holds
F is having_an_inverseOp

proof end;

theorem Th156: :: MATGRP_0:136

for R being Ring
for n being Nat
for F being BinOp of (n -invertible_Matrices_over R) st F = (matrix_mult (n,R)) || (n -invertible_Matrices_over R) holds
( F is having_a_unity & F is associative & F is having_an_inverseOp )

proof end;

theorem :: MATGRP_0:137

for R being Ring
for n being Nat
for F being BinOp of (n -invertible_Matrices_over R) st F = (matrix_mult (n,R)) || (n -invertible_Matrices_over R) holds
matrix_inv (n,R) = the_inverseOp_wrt F

proof end;

Lm4: for R being Ring
for a, b being Element of R st a * b = 1. R & ( for b9 being Element of R st a * b9 = 1. R holds
b9 = b ) holds
for x being Element of R holds
( a * x <> 0. R or x = 0. R )

proof end;

Lm5: for R being Ring
for a, b being Element of R st a * b = 1. R & ( for x being Element of R holds
( a * x <> 0. R or x = 0. R ) ) holds
a is invertible

proof end;

Lm6: for R being Ring
for a, b being Element of R st a * b = 1. R & a is invertible holds
for b9 being Element of R st a * b9 = 1. R holds
b9 = b

proof end;

:: Rudin's results~\cite{rudin1985unique} concerning two-sided inverses and unique right invertibility, as discussed by Almira and Cid~\cite{almira2023ring}.

theorem :: MATGRP_0:138

for R being Ring
for a, b being Element of R st a * b = 1. R holds
( ( for b9 being Element of R st a * b9 = 1. R holds
b9 = b ) iff for x being Element of R holds
( a * x <> 0. R or x = 0. R ) )

proof end;

theorem :: MATGRP_0:139

for R being Ring
for a, b being Element of R st a * b = 1. R holds
( ( for x being Element of R holds
( a * x <> 0. R or x = 0. R ) ) iff a is invertible )

proof end;

theorem :: MATGRP_0:140

for R being Ring
for a, b being Element of R st a * b = 1. R holds
( ( for b9 being Element of R st a * b9 = 1. R holds
b9 = b ) iff a is invertible )

proof end;

theorem Th161: :: MATGRP_0:141

for G being Group holds multMagma(# the carrier of G, the multF of G #) is Subgroup of G

proof end;

registration

let G be Group;

cluster multMagma(# the carrier of G, the multF of G #) -> Group-like associative ;

coherence
( multMagma(# the carrier of G, the multF of G #) is associative & multMagma(# the carrier of G, the multF of G #) is Group-like ) by Th161;

end;

theorem Th162: :: MATGRP_0:142

for G being Group holds inverse_op G = inverse_op multMagma(# the carrier of G, the multF of G #)

proof end;

definition

let n be Nat;
let R be Ring;
let IT be Group;

attr IT is n,R -linear means :Def13: :: MATGRP_0:def 13
multMagma(# the carrier of IT, the multF of IT #) is Subgroup of GL (n,R);

end;

:: deftheorem Def13 defines -linear MATGRP_0:def 13 :
for n being Nat
for R being Ring
for IT being Group holds
( IT is n,R -linear iff multMagma(# the carrier of IT, the multF of IT #) is Subgroup of GL (n,R) );

registration

let n be Nat;
let R be Ring;

cluster GL (n,R) -> strict n,R -linear ;

coherence
GL (n,R) is n,R -linear by GROUP_2:54;

end;

registration

let n be Nat;
let R be Ring;

cluster non empty strict Group-like associative n,R -linear for multMagma ;

existence
ex b₁ being Group st
( b₁ is strict & b₁ is n,R -linear )

proof end;

end;

theorem Th163: :: MATGRP_0:143

for R being Ring
for n being Nat
for H being Subgroup of GL (n,R) holds H is n,R -linear

proof end;

registration

let n be Nat;
let R be Ring;

cluster -> n,R -linear for Subgroup of GL (n,R);

coherence
for b₁ being Subgroup of GL (n,R) holds b₁ is n,R -linear by Th163;

end;

theorem Th164: :: MATGRP_0:144

for R being Ring
for n being Nat
for G being b₂,b₁ -linear Group holds the carrier of G c= the carrier of (GL (n,R))

proof end;

theorem :: MATGRP_0:145

for R being Ring
for n being Nat
for G being b₂,b₁ -linear Group holds the carrier of G c= n -invertible_Matrices_over R

proof end;

registration

let n be Nat;
let R be Ring;

cluster non empty Group-like associative n,R -linear -> n,R -matrix-membered for multMagma ;

coherence
for b₁ being Group st b₁ is n,R -linear holds
b₁ is n,R -matrix-membered

proof end;

end;

theorem Th166: :: MATGRP_0:146

for R being Ring
for n being Nat
for G being b₂,b₁ -linear Group holds 1_ G = 1_ (GL (n,R))

proof end;

theorem :: MATGRP_0:147

for R being Ring
for n being Nat
for G being b₂,b₁ -linear Group holds 1_ G = 1. (R,n)

proof end;

registration

let n be Nat;
let R be Ring;
let G be n,R -linear Group;

cluster the carrier of G -> non empty n,R -matrix-membered ;

coherence
( not the carrier of G is empty & the carrier of G is n,R -matrix-membered )

proof end;

end;

theorem Th168: :: MATGRP_0:148

for R being Ring
for n being Nat
for G being b₂,b₁ -linear Group holds the multF of G = the multF of (GL (n,R)) || the carrier of G

proof end;

theorem :: MATGRP_0:149

for R being Ring
for n being Nat
for G being b₂,b₁ -linear Group holds the multF of G = (matrix_mult (n,R)) || the carrier of G

proof end;

theorem :: MATGRP_0:150

for R being Ring
for n being Nat holds the multF of (GL (n,R)) = (matrix_mult (n,R)) || (n -invertible_Matrices_over R) by Th146;

theorem Th171: :: MATGRP_0:151

for R being Ring
for n being Nat
for G being b₂,b₁ -linear Group
for H being Subgroup of G holds H is n,R -linear

proof end;

registration

let n be Nat;
let R be Ring;
let G be n,R -linear Group;

cluster -> n,R -linear for Subgroup of G;

coherence
for b₁ being Subgroup of G holds b₁ is n,R -linear by Th171;

end;

theorem Th172: :: MATGRP_0:152

for R being Ring
for n being Nat
for G being b₂,b₁ -linear Group holds inverse_op G = (inverse_op (GL (n,R))) | the carrier of G

proof end;

theorem :: MATGRP_0:153

for R being Ring
for n being Nat
for G being b₂,b₁ -linear Group holds inverse_op G = (matrix_inv (n,R)) | the carrier of G

proof end;

:: To *readably* distinguish the general (n,R)-linear Lie group from
:: the general (n,R)-linear algebraic group from the general
:: (n,R)-linear strict Group from ...

definition

let n be Nat;
let R be Ring;
let IT be n,R -linear Group;

attr IT is general means :Def14: :: MATGRP_0:def 14
for x being object holds
( x in IT iff x is invertible Matrix of n,R );

end;

:: deftheorem Def14 defines general MATGRP_0:def 14 :
for n being Nat
for R being Ring
for IT being b₁,b₂ -linear Group holds
( IT is general iff for x being object holds
( x in IT iff x is invertible Matrix of n,R ) );

registration

let n be Nat;
let R be Ring;

cluster GL (n,R) -> strict general ;

coherence
GL (n,R) is general

proof end;

end;

registration

let n be Nat;
let R be Ring;

cluster non empty strict Group-like associative n,R -matrix-membered n,R -linear general for multMagma ;

existence
ex b₁ being n,R -linear Group st
( b₁ is general & b₁ is strict )

proof end;

cluster non empty Group-like associative n,R -matrix-membered n,R -linear general for multMagma ;

existence
ex b₁ being n,R -linear Group st b₁ is general

proof end;

end;

theorem Th174: :: MATGRP_0:154

for R being Ring
for n being Nat
for G being b₂,b₁ -linear general Group holds the carrier of G = the carrier of (GL (n,R))

proof end;

theorem Th175: :: MATGRP_0:155

for R being Ring
for n being Nat
for G being b₂,b₁ -linear general Group holds the multF of G = the multF of (GL (n,R))

proof end;

theorem Th176: :: MATGRP_0:156

for R being Ring
for n being Nat
for G being b₂,b₁ -linear general Group holds multMagma(# the carrier of G, the multF of G #) = GL (n,R)

proof end;

theorem :: MATGRP_0:157

for R being Ring
for n being Nat holds the strict b₂,b₁ -linear general Group = GL (n,R) by Th176;