# Metamath Proof Explorer

## Theorem matring

Description: Existence of the matrix ring, see also the statement in Lang p. 504: "For a given integer n > 0 the set of square n x n matrices form a ring." (Contributed by Stefan O'Rear, 5-Sep-2015)

Ref Expression
Hypothesis matassa.a
`|- A = ( N Mat R )`
Assertion matring
`|- ( ( N e. Fin /\ R e. Ring ) -> A e. Ring )`

### Proof

Step Hyp Ref Expression
1 matassa.a
` |-  A = ( N Mat R )`
2 eqid
` |-  ( Base ` R ) = ( Base ` R )`
3 1 2 matbas2
` |-  ( ( N e. Fin /\ R e. Ring ) -> ( ( Base ` R ) ^m ( N X. N ) ) = ( Base ` A ) )`
4 eqidd
` |-  ( ( N e. Fin /\ R e. Ring ) -> ( +g ` A ) = ( +g ` A ) )`
5 eqid
` |-  ( R maMul <. N , N , N >. ) = ( R maMul <. N , N , N >. )`
6 1 5 matmulr
` |-  ( ( N e. Fin /\ R e. Ring ) -> ( R maMul <. N , N , N >. ) = ( .r ` A ) )`
7 1 matgrp
` |-  ( ( N e. Fin /\ R e. Ring ) -> A e. Grp )`
8 simp1r
` |-  ( ( ( N e. Fin /\ R e. Ring ) /\ x e. ( ( Base ` R ) ^m ( N X. N ) ) /\ y e. ( ( Base ` R ) ^m ( N X. N ) ) ) -> R e. Ring )`
9 simp1l
` |-  ( ( ( N e. Fin /\ R e. Ring ) /\ x e. ( ( Base ` R ) ^m ( N X. N ) ) /\ y e. ( ( Base ` R ) ^m ( N X. N ) ) ) -> N e. Fin )`
10 simp2
` |-  ( ( ( N e. Fin /\ R e. Ring ) /\ x e. ( ( Base ` R ) ^m ( N X. N ) ) /\ y e. ( ( Base ` R ) ^m ( N X. N ) ) ) -> x e. ( ( Base ` R ) ^m ( N X. N ) ) )`
11 simp3
` |-  ( ( ( N e. Fin /\ R e. Ring ) /\ x e. ( ( Base ` R ) ^m ( N X. N ) ) /\ y e. ( ( Base ` R ) ^m ( N X. N ) ) ) -> y e. ( ( Base ` R ) ^m ( N X. N ) ) )`
12 2 8 5 9 9 9 10 11 mamucl
` |-  ( ( ( N e. Fin /\ R e. Ring ) /\ x e. ( ( Base ` R ) ^m ( N X. N ) ) /\ y e. ( ( Base ` R ) ^m ( N X. N ) ) ) -> ( x ( R maMul <. N , N , N >. ) y ) e. ( ( Base ` R ) ^m ( N X. N ) ) )`
13 simplr
` |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( x e. ( ( Base ` R ) ^m ( N X. N ) ) /\ y e. ( ( Base ` R ) ^m ( N X. N ) ) /\ z e. ( ( Base ` R ) ^m ( N X. N ) ) ) ) -> R e. Ring )`
14 simpll
` |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( x e. ( ( Base ` R ) ^m ( N X. N ) ) /\ y e. ( ( Base ` R ) ^m ( N X. N ) ) /\ z e. ( ( Base ` R ) ^m ( N X. N ) ) ) ) -> N e. Fin )`
15 simpr1
` |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( x e. ( ( Base ` R ) ^m ( N X. N ) ) /\ y e. ( ( Base ` R ) ^m ( N X. N ) ) /\ z e. ( ( Base ` R ) ^m ( N X. N ) ) ) ) -> x e. ( ( Base ` R ) ^m ( N X. N ) ) )`
16 simpr2
` |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( x e. ( ( Base ` R ) ^m ( N X. N ) ) /\ y e. ( ( Base ` R ) ^m ( N X. N ) ) /\ z e. ( ( Base ` R ) ^m ( N X. N ) ) ) ) -> y e. ( ( Base ` R ) ^m ( N X. N ) ) )`
17 simpr3
` |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( x e. ( ( Base ` R ) ^m ( N X. N ) ) /\ y e. ( ( Base ` R ) ^m ( N X. N ) ) /\ z e. ( ( Base ` R ) ^m ( N X. N ) ) ) ) -> z e. ( ( Base ` R ) ^m ( N X. N ) ) )`
18 2 13 14 14 14 14 15 16 17 5 5 5 5 mamuass
` |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( x e. ( ( Base ` R ) ^m ( N X. N ) ) /\ y e. ( ( Base ` R ) ^m ( N X. N ) ) /\ z e. ( ( Base ` R ) ^m ( N X. N ) ) ) ) -> ( ( x ( R maMul <. N , N , N >. ) y ) ( R maMul <. N , N , N >. ) z ) = ( x ( R maMul <. N , N , N >. ) ( y ( R maMul <. N , N , N >. ) z ) ) )`
19 eqid
` |-  ( +g ` R ) = ( +g ` R )`
20 2 13 5 14 14 14 19 15 16 17 mamudir
` |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( x e. ( ( Base ` R ) ^m ( N X. N ) ) /\ y e. ( ( Base ` R ) ^m ( N X. N ) ) /\ z e. ( ( Base ` R ) ^m ( N X. N ) ) ) ) -> ( x ( R maMul <. N , N , N >. ) ( y oF ( +g ` R ) z ) ) = ( ( x ( R maMul <. N , N , N >. ) y ) oF ( +g ` R ) ( x ( R maMul <. N , N , N >. ) z ) ) )`
` |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( x e. ( ( Base ` R ) ^m ( N X. N ) ) /\ y e. ( ( Base ` R ) ^m ( N X. N ) ) /\ z e. ( ( Base ` R ) ^m ( N X. N ) ) ) ) -> ( ( Base ` R ) ^m ( N X. N ) ) = ( Base ` A ) )`
22 16 21 eleqtrd
` |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( x e. ( ( Base ` R ) ^m ( N X. N ) ) /\ y e. ( ( Base ` R ) ^m ( N X. N ) ) /\ z e. ( ( Base ` R ) ^m ( N X. N ) ) ) ) -> y e. ( Base ` A ) )`
23 17 21 eleqtrd
` |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( x e. ( ( Base ` R ) ^m ( N X. N ) ) /\ y e. ( ( Base ` R ) ^m ( N X. N ) ) /\ z e. ( ( Base ` R ) ^m ( N X. N ) ) ) ) -> z e. ( Base ` A ) )`
24 eqid
` |-  ( Base ` A ) = ( Base ` A )`
25 eqid
` |-  ( +g ` A ) = ( +g ` A )`
26 1 24 25 19 matplusg2
` |-  ( ( y e. ( Base ` A ) /\ z e. ( Base ` A ) ) -> ( y ( +g ` A ) z ) = ( y oF ( +g ` R ) z ) )`
27 22 23 26 syl2anc
` |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( x e. ( ( Base ` R ) ^m ( N X. N ) ) /\ y e. ( ( Base ` R ) ^m ( N X. N ) ) /\ z e. ( ( Base ` R ) ^m ( N X. N ) ) ) ) -> ( y ( +g ` A ) z ) = ( y oF ( +g ` R ) z ) )`
28 27 oveq2d
` |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( x e. ( ( Base ` R ) ^m ( N X. N ) ) /\ y e. ( ( Base ` R ) ^m ( N X. N ) ) /\ z e. ( ( Base ` R ) ^m ( N X. N ) ) ) ) -> ( x ( R maMul <. N , N , N >. ) ( y ( +g ` A ) z ) ) = ( x ( R maMul <. N , N , N >. ) ( y oF ( +g ` R ) z ) ) )`
29 2 13 5 14 14 14 15 16 mamucl
` |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( x e. ( ( Base ` R ) ^m ( N X. N ) ) /\ y e. ( ( Base ` R ) ^m ( N X. N ) ) /\ z e. ( ( Base ` R ) ^m ( N X. N ) ) ) ) -> ( x ( R maMul <. N , N , N >. ) y ) e. ( ( Base ` R ) ^m ( N X. N ) ) )`
30 29 21 eleqtrd
` |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( x e. ( ( Base ` R ) ^m ( N X. N ) ) /\ y e. ( ( Base ` R ) ^m ( N X. N ) ) /\ z e. ( ( Base ` R ) ^m ( N X. N ) ) ) ) -> ( x ( R maMul <. N , N , N >. ) y ) e. ( Base ` A ) )`
31 2 13 5 14 14 14 15 17 mamucl
` |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( x e. ( ( Base ` R ) ^m ( N X. N ) ) /\ y e. ( ( Base ` R ) ^m ( N X. N ) ) /\ z e. ( ( Base ` R ) ^m ( N X. N ) ) ) ) -> ( x ( R maMul <. N , N , N >. ) z ) e. ( ( Base ` R ) ^m ( N X. N ) ) )`
32 31 21 eleqtrd
` |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( x e. ( ( Base ` R ) ^m ( N X. N ) ) /\ y e. ( ( Base ` R ) ^m ( N X. N ) ) /\ z e. ( ( Base ` R ) ^m ( N X. N ) ) ) ) -> ( x ( R maMul <. N , N , N >. ) z ) e. ( Base ` A ) )`
33 1 24 25 19 matplusg2
` |-  ( ( ( x ( R maMul <. N , N , N >. ) y ) e. ( Base ` A ) /\ ( x ( R maMul <. N , N , N >. ) z ) e. ( Base ` A ) ) -> ( ( x ( R maMul <. N , N , N >. ) y ) ( +g ` A ) ( x ( R maMul <. N , N , N >. ) z ) ) = ( ( x ( R maMul <. N , N , N >. ) y ) oF ( +g ` R ) ( x ( R maMul <. N , N , N >. ) z ) ) )`
34 30 32 33 syl2anc
` |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( x e. ( ( Base ` R ) ^m ( N X. N ) ) /\ y e. ( ( Base ` R ) ^m ( N X. N ) ) /\ z e. ( ( Base ` R ) ^m ( N X. N ) ) ) ) -> ( ( x ( R maMul <. N , N , N >. ) y ) ( +g ` A ) ( x ( R maMul <. N , N , N >. ) z ) ) = ( ( x ( R maMul <. N , N , N >. ) y ) oF ( +g ` R ) ( x ( R maMul <. N , N , N >. ) z ) ) )`
35 20 28 34 3eqtr4d
` |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( x e. ( ( Base ` R ) ^m ( N X. N ) ) /\ y e. ( ( Base ` R ) ^m ( N X. N ) ) /\ z e. ( ( Base ` R ) ^m ( N X. N ) ) ) ) -> ( x ( R maMul <. N , N , N >. ) ( y ( +g ` A ) z ) ) = ( ( x ( R maMul <. N , N , N >. ) y ) ( +g ` A ) ( x ( R maMul <. N , N , N >. ) z ) ) )`
36 2 13 5 14 14 14 19 15 16 17 mamudi
` |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( x e. ( ( Base ` R ) ^m ( N X. N ) ) /\ y e. ( ( Base ` R ) ^m ( N X. N ) ) /\ z e. ( ( Base ` R ) ^m ( N X. N ) ) ) ) -> ( ( x oF ( +g ` R ) y ) ( R maMul <. N , N , N >. ) z ) = ( ( x ( R maMul <. N , N , N >. ) z ) oF ( +g ` R ) ( y ( R maMul <. N , N , N >. ) z ) ) )`
37 15 21 eleqtrd
` |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( x e. ( ( Base ` R ) ^m ( N X. N ) ) /\ y e. ( ( Base ` R ) ^m ( N X. N ) ) /\ z e. ( ( Base ` R ) ^m ( N X. N ) ) ) ) -> x e. ( Base ` A ) )`
38 1 24 25 19 matplusg2
` |-  ( ( x e. ( Base ` A ) /\ y e. ( Base ` A ) ) -> ( x ( +g ` A ) y ) = ( x oF ( +g ` R ) y ) )`
39 37 22 38 syl2anc
` |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( x e. ( ( Base ` R ) ^m ( N X. N ) ) /\ y e. ( ( Base ` R ) ^m ( N X. N ) ) /\ z e. ( ( Base ` R ) ^m ( N X. N ) ) ) ) -> ( x ( +g ` A ) y ) = ( x oF ( +g ` R ) y ) )`
40 39 oveq1d
` |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( x e. ( ( Base ` R ) ^m ( N X. N ) ) /\ y e. ( ( Base ` R ) ^m ( N X. N ) ) /\ z e. ( ( Base ` R ) ^m ( N X. N ) ) ) ) -> ( ( x ( +g ` A ) y ) ( R maMul <. N , N , N >. ) z ) = ( ( x oF ( +g ` R ) y ) ( R maMul <. N , N , N >. ) z ) )`
41 2 13 5 14 14 14 16 17 mamucl
` |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( x e. ( ( Base ` R ) ^m ( N X. N ) ) /\ y e. ( ( Base ` R ) ^m ( N X. N ) ) /\ z e. ( ( Base ` R ) ^m ( N X. N ) ) ) ) -> ( y ( R maMul <. N , N , N >. ) z ) e. ( ( Base ` R ) ^m ( N X. N ) ) )`
42 41 21 eleqtrd
` |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( x e. ( ( Base ` R ) ^m ( N X. N ) ) /\ y e. ( ( Base ` R ) ^m ( N X. N ) ) /\ z e. ( ( Base ` R ) ^m ( N X. N ) ) ) ) -> ( y ( R maMul <. N , N , N >. ) z ) e. ( Base ` A ) )`
43 1 24 25 19 matplusg2
` |-  ( ( ( x ( R maMul <. N , N , N >. ) z ) e. ( Base ` A ) /\ ( y ( R maMul <. N , N , N >. ) z ) e. ( Base ` A ) ) -> ( ( x ( R maMul <. N , N , N >. ) z ) ( +g ` A ) ( y ( R maMul <. N , N , N >. ) z ) ) = ( ( x ( R maMul <. N , N , N >. ) z ) oF ( +g ` R ) ( y ( R maMul <. N , N , N >. ) z ) ) )`
44 32 42 43 syl2anc
` |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( x e. ( ( Base ` R ) ^m ( N X. N ) ) /\ y e. ( ( Base ` R ) ^m ( N X. N ) ) /\ z e. ( ( Base ` R ) ^m ( N X. N ) ) ) ) -> ( ( x ( R maMul <. N , N , N >. ) z ) ( +g ` A ) ( y ( R maMul <. N , N , N >. ) z ) ) = ( ( x ( R maMul <. N , N , N >. ) z ) oF ( +g ` R ) ( y ( R maMul <. N , N , N >. ) z ) ) )`
45 36 40 44 3eqtr4d
` |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( x e. ( ( Base ` R ) ^m ( N X. N ) ) /\ y e. ( ( Base ` R ) ^m ( N X. N ) ) /\ z e. ( ( Base ` R ) ^m ( N X. N ) ) ) ) -> ( ( x ( +g ` A ) y ) ( R maMul <. N , N , N >. ) z ) = ( ( x ( R maMul <. N , N , N >. ) z ) ( +g ` A ) ( y ( R maMul <. N , N , N >. ) z ) ) )`
46 simpr
` |-  ( ( N e. Fin /\ R e. Ring ) -> R e. Ring )`
47 eqid
` |-  ( 1r ` R ) = ( 1r ` R )`
48 eqid
` |-  ( 0g ` R ) = ( 0g ` R )`
49 eqid
` |-  ( a e. N , b e. N |-> if ( a = b , ( 1r ` R ) , ( 0g ` R ) ) ) = ( a e. N , b e. N |-> if ( a = b , ( 1r ` R ) , ( 0g ` R ) ) )`
50 simpl
` |-  ( ( N e. Fin /\ R e. Ring ) -> N e. Fin )`
51 2 46 47 48 49 50 mamumat1cl
` |-  ( ( N e. Fin /\ R e. Ring ) -> ( a e. N , b e. N |-> if ( a = b , ( 1r ` R ) , ( 0g ` R ) ) ) e. ( ( Base ` R ) ^m ( N X. N ) ) )`
52 simplr
` |-  ( ( ( N e. Fin /\ R e. Ring ) /\ x e. ( ( Base ` R ) ^m ( N X. N ) ) ) -> R e. Ring )`
53 simpll
` |-  ( ( ( N e. Fin /\ R e. Ring ) /\ x e. ( ( Base ` R ) ^m ( N X. N ) ) ) -> N e. Fin )`
54 simpr
` |-  ( ( ( N e. Fin /\ R e. Ring ) /\ x e. ( ( Base ` R ) ^m ( N X. N ) ) ) -> x e. ( ( Base ` R ) ^m ( N X. N ) ) )`
55 2 52 47 48 49 53 53 5 54 mamulid
` |-  ( ( ( N e. Fin /\ R e. Ring ) /\ x e. ( ( Base ` R ) ^m ( N X. N ) ) ) -> ( ( a e. N , b e. N |-> if ( a = b , ( 1r ` R ) , ( 0g ` R ) ) ) ( R maMul <. N , N , N >. ) x ) = x )`
56 2 52 47 48 49 53 53 5 54 mamurid
` |-  ( ( ( N e. Fin /\ R e. Ring ) /\ x e. ( ( Base ` R ) ^m ( N X. N ) ) ) -> ( x ( R maMul <. N , N , N >. ) ( a e. N , b e. N |-> if ( a = b , ( 1r ` R ) , ( 0g ` R ) ) ) ) = x )`
57 3 4 6 7 12 18 35 45 51 55 56 isringd
` |-  ( ( N e. Fin /\ R e. Ring ) -> A e. Ring )`