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 ) ) )
21 3 adantr 
 |-  ( ( ( 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 )