let R be 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
let n be 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
let F be BinOp of (n -invertible_Matrices_over R); ( F = (matrix_mult (n,R)) || (n -invertible_Matrices_over R) implies matrix_inv (n,R) is_an_inverseOp_wrt F )
assume A1:
F = (matrix_mult (n,R)) || (n -invertible_Matrices_over R)
; matrix_inv (n,R) is_an_inverseOp_wrt F
set i = matrix_inv (n,R);
set U = n -invertible_Matrices_over R;
set mu = matrix_mult (n,R);
reconsider e1 = One (R,n) as Element of n -invertible_Matrices_over R by Th145;
A2:
e1 = the_unity_wrt F
by A1, Th153;
for x being Element of n -invertible_Matrices_over R holds
( F . (x,((matrix_inv (n,R)) . x)) = the_unity_wrt F & F . (((matrix_inv (n,R)) . x),x) = the_unity_wrt F )
proof
let x be
Element of
n -invertible_Matrices_over R;
( F . (x,((matrix_inv (n,R)) . x)) = the_unity_wrt F & F . (((matrix_inv (n,R)) . x),x) = the_unity_wrt F )
reconsider X =
x,
Y =
(matrix_inv (n,R)) . x as
invertible Matrix of
n,
R by Th145;
reconsider a =
x,
b =
(matrix_inv (n,R)) . x as
Element of
n -Matrices_over R by TARSKI:def 3;
A3:
(
[x,((matrix_inv (n,R)) . x)] in [:(n -invertible_Matrices_over R),(n -invertible_Matrices_over R):] &
[((matrix_inv (n,R)) . x),x] in [:(n -invertible_Matrices_over R),(n -invertible_Matrices_over R):] )
;
A4:
(matrix_inv (n,R)) . x = X ~
by Def12;
X ~ is_reverse_of X
by MATRIX_6:def 4;
then A5:
(
(X ~) * X = X * (X ~) &
(X ~) * X = 1. (
R,
n) )
by MATRIX_6:def 2;
thus F . (
x,
((matrix_inv (n,R)) . x)) =
(matrix_mult (n,R)) . (
a,
b)
by A1, A3, FUNCT_1:49
.=
the_unity_wrt F
by A2, A4, A5, Def5
;
F . (((matrix_inv (n,R)) . x),x) = the_unity_wrt F
thus F . (
((matrix_inv (n,R)) . x),
x) =
(matrix_mult (n,R)) . (
b,
a)
by A1, A3, FUNCT_1:49
.=
the_unity_wrt F
by A2, A4, A5, Def5
;
verum
end;
hence
matrix_inv (n,R) is_an_inverseOp_wrt F
by FINSEQOP:def 1; verum