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 simpr 
 |-  ( ( N e. Fin /\ R e. CRing ) -> R e. CRing )
15 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 )
16 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 )
17 eqid 
 |-  ( .r ` R ) = ( .r ` R )
18 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 ) )
19 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 ) ) )
20 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 ) ) )
21 2 15 7 16 16 16 17 18 19 20 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 ) ) )
22 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 ) )
23 19 22 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 ) )
24 eqid 
 |-  ( Base ` A ) = ( Base ` A )
25 eqid 
 |-  ( .s ` A ) = ( .s ` A )
26 eqid 
 |-  ( N X. N ) = ( N X. N )
27 1 24 2 25 17 26 matvsca2 
 |-  ( ( x e. ( Base ` R ) /\ y e. ( Base ` A ) ) -> ( x ( .s ` A ) y ) = ( ( ( N X. N ) X. { x } ) oF ( .r ` R ) y ) )
28 18 23 27 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 ) )
29 28 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 ) )
30 2 15 7 16 16 16 19 20 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 ) ) )
31 30 22 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 ) )
32 1 24 2 25 17 26 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 ) ) )
33 18 31 32 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 ) ) )
34 21 29 33 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 ) ) )
35 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 )
36 35 2 17 7 16 16 16 19 18 20 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 ) ) )
37 20 22 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 ) )
38 1 24 2 25 17 26 matvsca2 
 |-  ( ( x e. ( Base ` R ) /\ z e. ( Base ` A ) ) -> ( x ( .s ` A ) z ) = ( ( ( N X. N ) X. { x } ) oF ( .r ` R ) z ) )
39 18 37 38 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 ) )
40 39 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 ) ) )
41 36 40 33 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 ) ) )
42 3 4 5 6 8 11 13 14 34 41 isassad 
 |-  ( ( N e. Fin /\ R e. CRing ) -> A e. AssAlg )