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) = the_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) = the_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) = the_inverseOp_wrt F )
assume A1:
F = (matrix_mult (n,R)) || (n -invertible_Matrices_over R)
; matrix_inv (n,R) = the_inverseOp_wrt F
then A2:
( F is having_a_unity & F is associative & F is having_an_inverseOp )
by Th156;
for x being Element of n -invertible_Matrices_over R holds (matrix_inv (n,R)) . x = (the_inverseOp_wrt F) . x
proof
let x be
Element of
n -invertible_Matrices_over R;
(matrix_inv (n,R)) . x = (the_inverseOp_wrt F) . x
reconsider X =
x as
invertible Matrix of
n,
R by Th145;
reconsider Y =
(the_inverseOp_wrt F) . x as
invertible Matrix of
n,
R by Th145;
reconsider a =
x as
Element of
n -Matrices_over R ;
(the_inverseOp_wrt F) . x in n -invertible_Matrices_over R
;
then reconsider b =
(the_inverseOp_wrt F) . x as
Element of
n -Matrices_over R ;
reconsider e1 =
One (
R,
n) as
Element of
n -invertible_Matrices_over R by Th145;
set U =
n -invertible_Matrices_over R;
set mu =
matrix_mult (
n,
R);
One (
R,
n)
= the_unity_wrt F
by A1, Th153;
then 1. (
R,
n) =
F . (
x,
((the_inverseOp_wrt F) . x))
by A2, FINSEQOP:59
.=
(matrix_mult (n,R)) . (
a,
b)
by A1, FUNCT_1:49, ZFMISC_1:87
.=
X * Y
by Def5
;
then
X is_reverse_of Y
by MATRIX_6:38;
then
Y = X ~
by MATRIX_6:def 4;
hence
(matrix_inv (n,R)) . x = (the_inverseOp_wrt F) . x
by Def12;
verum
end;
hence
matrix_inv (n,R) = the_inverseOp_wrt F
by FUNCT_2:def 8; verum