let R be Ring; :: thesis: for n being Nat
for S being Subring of R holds Matrix_ring (n,S) is Subring of Matrix_ring (n,R)
let n be Nat; :: thesis: for S being Subring of R holds Matrix_ring (n,S) is Subring of Matrix_ring (n,R)
let S be Subring of R; :: thesis: Matrix_ring (n,S) is Subring of Matrix_ring (n,R)
set MR = Matrix_ring (n,R);
set MS = Matrix_ring (n,S);
set U1 = the carrier of (Matrix_ring (n,S));
A1: n -Matrices_over S c= n -Matrices_over R by Th85;
A2: matrix_add (n,S) = (matrix_add (n,R)) || the carrier of (Matrix_ring (n,S)) by Th87;
A3: matrix_mult (n,S) = (matrix_mult (n,R)) || the carrier of (Matrix_ring (n,S)) by Th93;
( 1. (Matrix_ring (n,S)) = 1. (Matrix_ring (n,R)) & 0. (Matrix_ring (n,S)) = 0. (Matrix_ring (n,R)) ) by Th96;
hence Matrix_ring (n,S) is Subring of Matrix_ring (n,R) by A1, A2, A3, C0SP1:def 3; :: thesis: verum