let R be Ring; for n being Nat
for S being Subring of R holds matrix_add (n,S) = (matrix_add (n,R)) || (n -Matrices_over S)
let n be Nat; for S being Subring of R holds matrix_add (n,S) = (matrix_add (n,R)) || (n -Matrices_over S)
let S be Subring of R; matrix_add (n,S) = (matrix_add (n,R)) || (n -Matrices_over S)
set US = n -Matrices_over S;
set UR = n -Matrices_over R;
A1:
n -Matrices_over S c= n -Matrices_over R
by Th85;
then A2:
[:(n -Matrices_over S),(n -Matrices_over S):] c= [:(n -Matrices_over R),(n -Matrices_over R):]
by ZFMISC_1:96;
A3:
(matrix_add (n,R)) || (n -Matrices_over S) is Function of [:(n -Matrices_over S),(n -Matrices_over S):],(n -Matrices_over R)
by A2, FUNCT_2:32;
A4:
matrix_add (n,S) is Function of [:(n -Matrices_over S),(n -Matrices_over S):],(n -Matrices_over R)
by A1, FUNCT_2:7;
for x, y being Element of n -Matrices_over S holds (matrix_add (n,S)) . (x,y) = ((matrix_add (n,R)) || (n -Matrices_over S)) . (x,y)
proof
let x,
y be
Element of
n -Matrices_over S;
(matrix_add (n,S)) . (x,y) = ((matrix_add (n,R)) || (n -Matrices_over S)) . (x,y)
reconsider a =
x,
b =
y as
Matrix of
n,
S ;
reconsider A =
a,
B =
b as
Matrix of
n,
R by Th82;
reconsider X =
x,
Y =
y as
Element of
n -Matrices_over R by Th85, TARSKI:def 3;
thus (matrix_add (n,S)) . (
x,
y) =
a + b
by Def6
.=
A + B
by Th86
.=
(matrix_add (n,R)) . (
X,
Y)
by Def6
.=
((matrix_add (n,R)) || (n -Matrices_over S)) . (
x,
y)
by FUNCT_1:49, ZFMISC_1:87
;
verum
end;
hence
matrix_add (n,S) = (matrix_add (n,R)) || (n -Matrices_over S)
by A3, A4, BINOP_1:2; verum