Metamath Proof Explorer

Theorem matassa

Description: Existence of the matrix algebra, see also the statement in Lang p. 505: "Then Mat_n(R) is an algebra over R" . (Contributed by Stefan O'Rear, 5-Sep-2015)

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

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. CRing ) -> ( ( Base ` R ) ^m ( N X. N ) ) = ( Base ` A ) )
4 1 matsca2 
 |-  ( ( N e. Fin /\ R e. CRing ) -> R = ( Scalar ` A ) )
5 eqidd 
 |-  ( ( N e. Fin /\ R e. CRing ) -> ( Base ` R ) = ( Base ` R ) )
6 eqidd 
 |-  ( ( N e. Fin /\ R e. CRing ) -> ( .s ` A ) = ( .s ` A ) )
7 eqid 
 |-  ( R maMul <. N , N , N >. ) = ( R maMul <. N , N , N >. )
8 1 7 matmulr 
 |-  ( ( N e. Fin /\ R e. CRing ) -> ( R maMul <. N , N , N >. ) = ( .r ` A ) )
9 crngring 
 |-  ( R e. CRing -> R e. Ring )
10 1 matlmod 
 |-  ( ( N e. Fin /\ R e. Ring ) -> A e. LMod )
11 9 10 sylan2 
 |-  ( ( N e. Fin /\ R e. CRing ) -> A e. LMod )
12 1 matring 
 |-  ( ( N e. Fin /\ R e. Ring ) -> A e. Ring )
13 9 12 sylan2 
 |-  ( ( N e. Fin /\ R e. CRing ) -> A e. Ring )
14 9 ad2antlr 
 |-  ( ( ( N e. Fin /\ R e. CRing ) /\ ( x e. ( Base ` R ) /\ y e. ( ( Base ` R ) ^m ( N X. N ) ) /\ z e. ( ( Base ` R ) ^m ( N X. N ) ) ) ) -> R e. Ring )
15 simpll 
 |-  ( ( ( N e. Fin /\ R e. CRing ) /\ ( x e. ( Base ` R ) /\ y e. ( ( Base ` R ) ^m ( N X. N ) ) /\ z e. ( ( Base ` R ) ^m ( N X. N ) ) ) ) -> N e. Fin )
16 eqid 
 |-  ( .r ` R ) = ( .r ` R )
17 simpr1 
 |-  ( ( ( N e. Fin /\ R e. CRing ) /\ ( x e. ( Base ` R ) /\ y e. ( ( Base ` R ) ^m ( N X. N ) ) /\ z e. ( ( Base ` R ) ^m ( N X. N ) ) ) ) -> x e. ( Base ` R ) )
18 simpr2 
 |-  ( ( ( N e. Fin /\ R e. CRing ) /\ ( x e. ( Base ` R ) /\ y e. ( ( Base ` R ) ^m ( N X. N ) ) /\ z e. ( ( Base ` R ) ^m ( N X. N ) ) ) ) -> y e. ( ( Base ` R ) ^m ( N X. N ) ) )
19 simpr3 
 |-  ( ( ( N e. Fin /\ R e. CRing ) /\ ( x e. ( Base ` R ) /\ y e. ( ( Base ` R ) ^m ( N X. N ) ) /\ z e. ( ( Base ` R ) ^m ( N X. N ) ) ) ) -> z e. ( ( Base ` R ) ^m ( N X. N ) ) )
20 2 14 7 15 15 15 16 17 18 19 mamuvs1 
 |-  ( ( ( N e. Fin /\ R e. CRing ) /\ ( x e. ( Base ` R ) /\ y e. ( ( Base ` R ) ^m ( N X. N ) ) /\ z e. ( ( Base ` R ) ^m ( N X. N ) ) ) ) -> ( ( ( ( N X. N ) X. { x } ) oF ( .r ` R ) y ) ( R maMul <. N , N , N >. ) z ) = ( ( ( N X. N ) X. { x } ) oF ( .r ` R ) ( y ( R maMul <. N , N , N >. ) z ) ) )
21 3 adantr 
 |-  ( ( ( N e. Fin /\ R e. CRing ) /\ ( x e. ( Base ` R ) /\ 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 18 21 eleqtrd 
 |-  ( ( ( N e. Fin /\ R e. CRing ) /\ ( x e. ( Base ` R ) /\ y e. ( ( Base ` R ) ^m ( N X. N ) ) /\ z e. ( ( Base ` R ) ^m ( N X. N ) ) ) ) -> y e. ( Base ` A ) )
23 eqid 
 |-  ( Base ` A ) = ( Base ` A )
24 eqid 
 |-  ( .s ` A ) = ( .s ` A )
25 eqid 
 |-  ( N X. N ) = ( N X. N )
26 1 23 2 24 16 25 matvsca2 
 |-  ( ( x e. ( Base ` R ) /\ y e. ( Base ` A ) ) -> ( x ( .s ` A ) y ) = ( ( ( N X. N ) X. { x } ) oF ( .r ` R ) y ) )
27 17 22 26 syl2anc 
 |-  ( ( ( N e. Fin /\ R e. CRing ) /\ ( x e. ( Base ` R ) /\ y e. ( ( Base ` R ) ^m ( N X. N ) ) /\ z e. ( ( Base ` R ) ^m ( N X. N ) ) ) ) -> ( x ( .s ` A ) y ) = ( ( ( N X. N ) X. { x } ) oF ( .r ` R ) y ) )
28 27 oveq1d 
 |-  ( ( ( N e. Fin /\ R e. CRing ) /\ ( x e. ( Base ` R ) /\ y e. ( ( Base ` R ) ^m ( N X. N ) ) /\ z e. ( ( Base ` R ) ^m ( N X. N ) ) ) ) -> ( ( x ( .s ` A ) y ) ( R maMul <. N , N , N >. ) z ) = ( ( ( ( N X. N ) X. { x } ) oF ( .r ` R ) y ) ( R maMul <. N , N , N >. ) z ) )
29 2 14 7 15 15 15 18 19 mamucl 
 |-  ( ( ( N e. Fin /\ R e. CRing ) /\ ( x e. ( Base ` R ) /\ 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 ) ) )
30 29 21 eleqtrd 
 |-  ( ( ( N e. Fin /\ R e. CRing ) /\ ( x e. ( Base ` R ) /\ 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 ) )
31 1 23 2 24 16 25 matvsca2 
 |-  ( ( x e. ( Base ` R ) /\ ( y ( R maMul <. N , N , N >. ) z ) e. ( Base ` A ) ) -> ( x ( .s ` A ) ( y ( R maMul <. N , N , N >. ) z ) ) = ( ( ( N X. N ) X. { x } ) oF ( .r ` R ) ( y ( R maMul <. N , N , N >. ) z ) ) )
32 17 30 31 syl2anc 
 |-  ( ( ( N e. Fin /\ R e. CRing ) /\ ( x e. ( Base ` R ) /\ y e. ( ( Base ` R ) ^m ( N X. N ) ) /\ z e. ( ( Base ` R ) ^m ( N X. N ) ) ) ) -> ( x ( .s ` A ) ( y ( R maMul <. N , N , N >. ) z ) ) = ( ( ( N X. N ) X. { x } ) oF ( .r ` R ) ( y ( R maMul <. N , N , N >. ) z ) ) )
33 20 28 32 3eqtr4d 
 |-  ( ( ( N e. Fin /\ R e. CRing ) /\ ( x e. ( Base ` R ) /\ y e. ( ( Base ` R ) ^m ( N X. N ) ) /\ z e. ( ( Base ` R ) ^m ( N X. N ) ) ) ) -> ( ( x ( .s ` A ) y ) ( R maMul <. N , N , N >. ) z ) = ( x ( .s ` A ) ( y ( R maMul <. N , N , N >. ) z ) ) )
34 simplr 
 |-  ( ( ( N e. Fin /\ R e. CRing ) /\ ( x e. ( Base ` R ) /\ y e. ( ( Base ` R ) ^m ( N X. N ) ) /\ z e. ( ( Base ` R ) ^m ( N X. N ) ) ) ) -> R e. CRing )
35 34 2 16 7 15 15 15 18 17 19 mamuvs2 
 |-  ( ( ( N e. Fin /\ R e. CRing ) /\ ( x e. ( Base ` R ) /\ y e. ( ( Base ` R ) ^m ( N X. N ) ) /\ z e. ( ( Base ` R ) ^m ( N X. N ) ) ) ) -> ( y ( R maMul <. N , N , N >. ) ( ( ( N X. N ) X. { x } ) oF ( .r ` R ) z ) ) = ( ( ( N X. N ) X. { x } ) oF ( .r ` R ) ( y ( R maMul <. N , N , N >. ) z ) ) )
36 19 21 eleqtrd 
 |-  ( ( ( N e. Fin /\ R e. CRing ) /\ ( x e. ( Base ` R ) /\ y e. ( ( Base ` R ) ^m ( N X. N ) ) /\ z e. ( ( Base ` R ) ^m ( N X. N ) ) ) ) -> z e. ( Base ` A ) )
37 1 23 2 24 16 25 matvsca2 
 |-  ( ( x e. ( Base ` R ) /\ z e. ( Base ` A ) ) -> ( x ( .s ` A ) z ) = ( ( ( N X. N ) X. { x } ) oF ( .r ` R ) z ) )
38 17 36 37 syl2anc 
 |-  ( ( ( N e. Fin /\ R e. CRing ) /\ ( x e. ( Base ` R ) /\ y e. ( ( Base ` R ) ^m ( N X. N ) ) /\ z e. ( ( Base ` R ) ^m ( N X. N ) ) ) ) -> ( x ( .s ` A ) z ) = ( ( ( N X. N ) X. { x } ) oF ( .r ` R ) z ) )
39 38 oveq2d 
 |-  ( ( ( N e. Fin /\ R e. CRing ) /\ ( x e. ( Base ` R ) /\ y e. ( ( Base ` R ) ^m ( N X. N ) ) /\ z e. ( ( Base ` R ) ^m ( N X. N ) ) ) ) -> ( y ( R maMul <. N , N , N >. ) ( x ( .s ` A ) z ) ) = ( y ( R maMul <. N , N , N >. ) ( ( ( N X. N ) X. { x } ) oF ( .r ` R ) z ) ) )
40 35 39 32 3eqtr4d 
 |-  ( ( ( N e. Fin /\ R e. CRing ) /\ ( x e. ( Base ` R ) /\ y e. ( ( Base ` R ) ^m ( N X. N ) ) /\ z e. ( ( Base ` R ) ^m ( N X. N ) ) ) ) -> ( y ( R maMul <. N , N , N >. ) ( x ( .s ` A ) z ) ) = ( x ( .s ` A ) ( y ( R maMul <. N , N , N >. ) z ) ) )
41 3 4 5 6 8 11 13 33 40 isassad 
 |-  ( ( N e. Fin /\ R e. CRing ) -> A e. AssAlg )