Metamath Proof Explorer

Theorem mat2pmatmul

Description: The transformation of matrices into polynomial matrices preserves the multiplication. (Contributed by AV, 29-Oct-2019) (Proof shortened by AV, 28-Nov-2019)

Ref Expression
Hypotheses mat2pmatbas.t 
|- T = ( N matToPolyMat R )
mat2pmatbas.a 
|- A = ( N Mat R )
mat2pmatbas.b 
|- B = ( Base ` A )
mat2pmatbas.p 
|- P = ( Poly1 ` R )
mat2pmatbas.c 
|- C = ( N Mat P )
mat2pmatbas0.h 
|- H = ( Base ` C )
Assertion mat2pmatmul 
|- ( ( N e. Fin /\ R e. CRing ) -> A. x e. B A. y e. B ( T ` ( x ( .r ` A ) y ) ) = ( ( T ` x ) ( .r ` C ) ( T ` y ) ) )

Proof

Step Hyp Ref Expression
1 mat2pmatbas.t 
 |-  T = ( N matToPolyMat R )
2 mat2pmatbas.a 
 |-  A = ( N Mat R )
3 mat2pmatbas.b 
 |-  B = ( Base ` A )
4 mat2pmatbas.p 
 |-  P = ( Poly1 ` R )
5 mat2pmatbas.c 
 |-  C = ( N Mat P )
6 mat2pmatbas0.h 
 |-  H = ( Base ` C )
7 eqid 
 |-  ( R maMul <. N , N , N >. ) = ( R maMul <. N , N , N >. )
8 2 7 matmulr 
 |-  ( ( N e. Fin /\ R e. CRing ) -> ( R maMul <. N , N , N >. ) = ( .r ` A ) )
9 8 eqcomd 
 |-  ( ( N e. Fin /\ R e. CRing ) -> ( .r ` A ) = ( R maMul <. N , N , N >. ) )
10 9 oveqdr 
 |-  ( ( ( N e. Fin /\ R e. CRing ) /\ ( x e. B /\ y e. B ) ) -> ( x ( .r ` A ) y ) = ( x ( R maMul <. N , N , N >. ) y ) )
11 eqid 
 |-  ( Base ` R ) = ( Base ` R )
12 eqid 
 |-  ( .r ` R ) = ( .r ` R )
13 crngring 
 |-  ( R e. CRing -> R e. Ring )
14 13 ad2antlr 
 |-  ( ( ( N e. Fin /\ R e. CRing ) /\ ( x e. B /\ y e. B ) ) -> R e. Ring )
15 simpll 
 |-  ( ( ( N e. Fin /\ R e. CRing ) /\ ( x e. B /\ y e. B ) ) -> N e. Fin )
16 3 eleq2i 
 |-  ( x e. B <-> x e. ( Base ` A ) )
17 16 birani 
 |-  ( ( x e. B /\ y e. B ) -> x e. ( Base ` A ) )
18 17 adantl 
 |-  ( ( ( N e. Fin /\ R e. CRing ) /\ ( x e. B /\ y e. B ) ) -> x e. ( Base ` A ) )
19 2 11 matbas2 
 |-  ( ( N e. Fin /\ R e. CRing ) -> ( ( Base ` R ) ^m ( N X. N ) ) = ( Base ` A ) )
20 19 adantr 
 |-  ( ( ( N e. Fin /\ R e. CRing ) /\ ( x e. B /\ y e. B ) ) -> ( ( Base ` R ) ^m ( N X. N ) ) = ( Base ` A ) )
21 18 20 eleqtrrd 
 |-  ( ( ( N e. Fin /\ R e. CRing ) /\ ( x e. B /\ y e. B ) ) -> x e. ( ( Base ` R ) ^m ( N X. N ) ) )
22 3 eleq2i 
 |-  ( y e. B <-> y e. ( Base ` A ) )
23 22 biimpi 
 |-  ( y e. B -> y e. ( Base ` A ) )
24 23 ad2antll 
 |-  ( ( ( N e. Fin /\ R e. CRing ) /\ ( x e. B /\ y e. B ) ) -> y e. ( Base ` A ) )
25 19 eleq2d 
 |-  ( ( N e. Fin /\ R e. CRing ) -> ( y e. ( ( Base ` R ) ^m ( N X. N ) ) <-> y e. ( Base ` A ) ) )
26 25 adantr 
 |-  ( ( ( N e. Fin /\ R e. CRing ) /\ ( x e. B /\ y e. B ) ) -> ( y e. ( ( Base ` R ) ^m ( N X. N ) ) <-> y e. ( Base ` A ) ) )
27 24 26 mpbird 
 |-  ( ( ( N e. Fin /\ R e. CRing ) /\ ( x e. B /\ y e. B ) ) -> y e. ( ( Base ` R ) ^m ( N X. N ) ) )
28 7 11 12 14 15 15 15 21 27 mamuval 
 |-  ( ( ( N e. Fin /\ R e. CRing ) /\ ( x e. B /\ y e. B ) ) -> ( x ( R maMul <. N , N , N >. ) y ) = ( i e. N , j e. N |-> ( R gsum ( m e. N |-> ( ( i x m ) ( .r ` R ) ( m y j ) ) ) ) ) )
29 10 28 eqtrd 
 |-  ( ( ( N e. Fin /\ R e. CRing ) /\ ( x e. B /\ y e. B ) ) -> ( x ( .r ` A ) y ) = ( i e. N , j e. N |-> ( R gsum ( m e. N |-> ( ( i x m ) ( .r ` R ) ( m y j ) ) ) ) ) )
30 29 3ad2ant1 
 |-  ( ( ( ( N e. Fin /\ R e. CRing ) /\ ( x e. B /\ y e. B ) ) /\ k e. N /\ l e. N ) -> ( x ( .r ` A ) y ) = ( i e. N , j e. N |-> ( R gsum ( m e. N |-> ( ( i x m ) ( .r ` R ) ( m y j ) ) ) ) ) )
31 oveq1 
 |-  ( i = k -> ( i x m ) = ( k x m ) )
32 oveq2 
 |-  ( j = l -> ( m y j ) = ( m y l ) )
33 31 32 oveqan12d 
 |-  ( ( i = k /\ j = l ) -> ( ( i x m ) ( .r ` R ) ( m y j ) ) = ( ( k x m ) ( .r ` R ) ( m y l ) ) )
34 33 mpteq2dv 
 |-  ( ( i = k /\ j = l ) -> ( m e. N |-> ( ( i x m ) ( .r ` R ) ( m y j ) ) ) = ( m e. N |-> ( ( k x m ) ( .r ` R ) ( m y l ) ) ) )
35 34 oveq2d 
 |-  ( ( i = k /\ j = l ) -> ( R gsum ( m e. N |-> ( ( i x m ) ( .r ` R ) ( m y j ) ) ) ) = ( R gsum ( m e. N |-> ( ( k x m ) ( .r ` R ) ( m y l ) ) ) ) )
36 35 adantl 
 |-  ( ( ( ( ( N e. Fin /\ R e. CRing ) /\ ( x e. B /\ y e. B ) ) /\ k e. N /\ l e. N ) /\ ( i = k /\ j = l ) ) -> ( R gsum ( m e. N |-> ( ( i x m ) ( .r ` R ) ( m y j ) ) ) ) = ( R gsum ( m e. N |-> ( ( k x m ) ( .r ` R ) ( m y l ) ) ) ) )
37 simp2 
 |-  ( ( ( ( N e. Fin /\ R e. CRing ) /\ ( x e. B /\ y e. B ) ) /\ k e. N /\ l e. N ) -> k e. N )
38 simp3 
 |-  ( ( ( ( N e. Fin /\ R e. CRing ) /\ ( x e. B /\ y e. B ) ) /\ k e. N /\ l e. N ) -> l e. N )
39 ovexd 
 |-  ( ( ( ( N e. Fin /\ R e. CRing ) /\ ( x e. B /\ y e. B ) ) /\ k e. N /\ l e. N ) -> ( R gsum ( m e. N |-> ( ( k x m ) ( .r ` R ) ( m y l ) ) ) ) e. _V )
40 30 36 37 38 39 ovmpod 
 |-  ( ( ( ( N e. Fin /\ R e. CRing ) /\ ( x e. B /\ y e. B ) ) /\ k e. N /\ l e. N ) -> ( k ( x ( .r ` A ) y ) l ) = ( R gsum ( m e. N |-> ( ( k x m ) ( .r ` R ) ( m y l ) ) ) ) )
41 40 fveq2d 
 |-  ( ( ( ( N e. Fin /\ R e. CRing ) /\ ( x e. B /\ y e. B ) ) /\ k e. N /\ l e. N ) -> ( ( algSc ` P ) ` ( k ( x ( .r ` A ) y ) l ) ) = ( ( algSc ` P ) ` ( R gsum ( m e. N |-> ( ( k x m ) ( .r ` R ) ( m y l ) ) ) ) ) )
42 eqid 
 |-  ( 0g ` R ) = ( 0g ` R )
43 ringcmn 
 |-  ( R e. Ring -> R e. CMnd )
44 13 43 syl 
 |-  ( R e. CRing -> R e. CMnd )
45 44 ad2antlr 
 |-  ( ( ( N e. Fin /\ R e. CRing ) /\ ( x e. B /\ y e. B ) ) -> R e. CMnd )
46 45 3ad2ant1 
 |-  ( ( ( ( N e. Fin /\ R e. CRing ) /\ ( x e. B /\ y e. B ) ) /\ k e. N /\ l e. N ) -> R e. CMnd )
47 4 ply1ring 
 |-  ( R e. Ring -> P e. Ring )
48 13 47 syl 
 |-  ( R e. CRing -> P e. Ring )
49 ringmnd 
 |-  ( P e. Ring -> P e. Mnd )
50 48 49 syl 
 |-  ( R e. CRing -> P e. Mnd )
51 50 ad2antlr 
 |-  ( ( ( N e. Fin /\ R e. CRing ) /\ ( x e. B /\ y e. B ) ) -> P e. Mnd )
52 51 3ad2ant1 
 |-  ( ( ( ( N e. Fin /\ R e. CRing ) /\ ( x e. B /\ y e. B ) ) /\ k e. N /\ l e. N ) -> P e. Mnd )
53 15 3ad2ant1 
 |-  ( ( ( ( N e. Fin /\ R e. CRing ) /\ ( x e. B /\ y e. B ) ) /\ k e. N /\ l e. N ) -> N e. Fin )
54 eqid 
 |-  ( algSc ` P ) = ( algSc ` P )
55 eqid 
 |-  ( Scalar ` P ) = ( Scalar ` P )
56 48 adantl 
 |-  ( ( N e. Fin /\ R e. CRing ) -> P e. Ring )
57 4 ply1lmod 
 |-  ( R e. Ring -> P e. LMod )
58 13 57 syl 
 |-  ( R e. CRing -> P e. LMod )
59 58 adantl 
 |-  ( ( N e. Fin /\ R e. CRing ) -> P e. LMod )
60 54 55 56 59 asclghm 
 |-  ( ( N e. Fin /\ R e. CRing ) -> ( algSc ` P ) e. ( ( Scalar ` P ) GrpHom P ) )
61 4 ply1sca 
 |-  ( R e. CRing -> R = ( Scalar ` P ) )
62 61 adantl 
 |-  ( ( N e. Fin /\ R e. CRing ) -> R = ( Scalar ` P ) )
63 62 oveq1d 
 |-  ( ( N e. Fin /\ R e. CRing ) -> ( R GrpHom P ) = ( ( Scalar ` P ) GrpHom P ) )
64 60 63 eleqtrrd 
 |-  ( ( N e. Fin /\ R e. CRing ) -> ( algSc ` P ) e. ( R GrpHom P ) )
65 ghmmhm 
 |-  ( ( algSc ` P ) e. ( R GrpHom P ) -> ( algSc ` P ) e. ( R MndHom P ) )
66 64 65 syl 
 |-  ( ( N e. Fin /\ R e. CRing ) -> ( algSc ` P ) e. ( R MndHom P ) )
67 66 adantr 
 |-  ( ( ( N e. Fin /\ R e. CRing ) /\ ( x e. B /\ y e. B ) ) -> ( algSc ` P ) e. ( R MndHom P ) )
68 67 3ad2ant1 
 |-  ( ( ( ( N e. Fin /\ R e. CRing ) /\ ( x e. B /\ y e. B ) ) /\ k e. N /\ l e. N ) -> ( algSc ` P ) e. ( R MndHom P ) )
69 14 3ad2ant1 
 |-  ( ( ( ( N e. Fin /\ R e. CRing ) /\ ( x e. B /\ y e. B ) ) /\ k e. N /\ l e. N ) -> R e. Ring )
70 69 adantr 
 |-  ( ( ( ( ( N e. Fin /\ R e. CRing ) /\ ( x e. B /\ y e. B ) ) /\ k e. N /\ l e. N ) /\ m e. N ) -> R e. Ring )
71 37 adantr 
 |-  ( ( ( ( ( N e. Fin /\ R e. CRing ) /\ ( x e. B /\ y e. B ) ) /\ k e. N /\ l e. N ) /\ m e. N ) -> k e. N )
72 simpr 
 |-  ( ( ( ( ( N e. Fin /\ R e. CRing ) /\ ( x e. B /\ y e. B ) ) /\ k e. N /\ l e. N ) /\ m e. N ) -> m e. N )
73 18 3ad2ant1 
 |-  ( ( ( ( N e. Fin /\ R e. CRing ) /\ ( x e. B /\ y e. B ) ) /\ k e. N /\ l e. N ) -> x e. ( Base ` A ) )
74 73 adantr 
 |-  ( ( ( ( ( N e. Fin /\ R e. CRing ) /\ ( x e. B /\ y e. B ) ) /\ k e. N /\ l e. N ) /\ m e. N ) -> x e. ( Base ` A ) )
75 74 16 sylibr 
 |-  ( ( ( ( ( N e. Fin /\ R e. CRing ) /\ ( x e. B /\ y e. B ) ) /\ k e. N /\ l e. N ) /\ m e. N ) -> x e. B )
76 2 11 3 71 72 75 matecld 
 |-  ( ( ( ( ( N e. Fin /\ R e. CRing ) /\ ( x e. B /\ y e. B ) ) /\ k e. N /\ l e. N ) /\ m e. N ) -> ( k x m ) e. ( Base ` R ) )
77 38 adantr 
 |-  ( ( ( ( ( N e. Fin /\ R e. CRing ) /\ ( x e. B /\ y e. B ) ) /\ k e. N /\ l e. N ) /\ m e. N ) -> l e. N )
78 2 fveq2i 
 |-  ( Base ` A ) = ( Base ` ( N Mat R ) )
79 3 78 eqtri 
 |-  B = ( Base ` ( N Mat R ) )
80 79 eleq2i 
 |-  ( y e. B <-> y e. ( Base ` ( N Mat R ) ) )
81 80 biimpi 
 |-  ( y e. B -> y e. ( Base ` ( N Mat R ) ) )
82 81 ad2antll 
 |-  ( ( ( N e. Fin /\ R e. CRing ) /\ ( x e. B /\ y e. B ) ) -> y e. ( Base ` ( N Mat R ) ) )
83 82 3ad2ant1 
 |-  ( ( ( ( N e. Fin /\ R e. CRing ) /\ ( x e. B /\ y e. B ) ) /\ k e. N /\ l e. N ) -> y e. ( Base ` ( N Mat R ) ) )
84 83 adantr 
 |-  ( ( ( ( ( N e. Fin /\ R e. CRing ) /\ ( x e. B /\ y e. B ) ) /\ k e. N /\ l e. N ) /\ m e. N ) -> y e. ( Base ` ( N Mat R ) ) )
85 84 80 sylibr 
 |-  ( ( ( ( ( N e. Fin /\ R e. CRing ) /\ ( x e. B /\ y e. B ) ) /\ k e. N /\ l e. N ) /\ m e. N ) -> y e. B )
86 2 11 3 72 77 85 matecld 
 |-  ( ( ( ( ( N e. Fin /\ R e. CRing ) /\ ( x e. B /\ y e. B ) ) /\ k e. N /\ l e. N ) /\ m e. N ) -> ( m y l ) e. ( Base ` R ) )
87 11 12 ringcl 
 |-  ( ( R e. Ring /\ ( k x m ) e. ( Base ` R ) /\ ( m y l ) e. ( Base ` R ) ) -> ( ( k x m ) ( .r ` R ) ( m y l ) ) e. ( Base ` R ) )
88 70 76 86 87 syl3anc 
 |-  ( ( ( ( ( N e. Fin /\ R e. CRing ) /\ ( x e. B /\ y e. B ) ) /\ k e. N /\ l e. N ) /\ m e. N ) -> ( ( k x m ) ( .r ` R ) ( m y l ) ) e. ( Base ` R ) )
89 eqid 
 |-  ( m e. N |-> ( ( k x m ) ( .r ` R ) ( m y l ) ) ) = ( m e. N |-> ( ( k x m ) ( .r ` R ) ( m y l ) ) )
90 ovexd 
 |-  ( ( ( ( ( N e. Fin /\ R e. CRing ) /\ ( x e. B /\ y e. B ) ) /\ k e. N /\ l e. N ) /\ m e. N ) -> ( ( k x m ) ( .r ` R ) ( m y l ) ) e. _V )
91 fvexd 
 |-  ( ( ( ( N e. Fin /\ R e. CRing ) /\ ( x e. B /\ y e. B ) ) /\ k e. N /\ l e. N ) -> ( 0g ` R ) e. _V )
92 89 53 90 91 fsuppmptdm 
 |-  ( ( ( ( N e. Fin /\ R e. CRing ) /\ ( x e. B /\ y e. B ) ) /\ k e. N /\ l e. N ) -> ( m e. N |-> ( ( k x m ) ( .r ` R ) ( m y l ) ) ) finSupp ( 0g ` R ) )
93 11 42 46 52 53 68 88 92 gsummptmhm 
 |-  ( ( ( ( N e. Fin /\ R e. CRing ) /\ ( x e. B /\ y e. B ) ) /\ k e. N /\ l e. N ) -> ( P gsum ( m e. N |-> ( ( algSc ` P ) ` ( ( k x m ) ( .r ` R ) ( m y l ) ) ) ) ) = ( ( algSc ` P ) ` ( R gsum ( m e. N |-> ( ( k x m ) ( .r ` R ) ( m y l ) ) ) ) ) )
94 4 ply1assa 
 |-  ( R e. CRing -> P e. AssAlg )
95 94 adantl 
 |-  ( ( N e. Fin /\ R e. CRing ) -> P e. AssAlg )
96 54 55 asclrhm 
 |-  ( P e. AssAlg -> ( algSc ` P ) e. ( ( Scalar ` P ) RingHom P ) )
97 95 96 syl 
 |-  ( ( N e. Fin /\ R e. CRing ) -> ( algSc ` P ) e. ( ( Scalar ` P ) RingHom P ) )
98 62 oveq1d 
 |-  ( ( N e. Fin /\ R e. CRing ) -> ( R RingHom P ) = ( ( Scalar ` P ) RingHom P ) )
99 97 98 eleqtrrd 
 |-  ( ( N e. Fin /\ R e. CRing ) -> ( algSc ` P ) e. ( R RingHom P ) )
100 99 adantr 
 |-  ( ( ( N e. Fin /\ R e. CRing ) /\ ( x e. B /\ y e. B ) ) -> ( algSc ` P ) e. ( R RingHom P ) )
101 100 3ad2ant1 
 |-  ( ( ( ( N e. Fin /\ R e. CRing ) /\ ( x e. B /\ y e. B ) ) /\ k e. N /\ l e. N ) -> ( algSc ` P ) e. ( R RingHom P ) )
102 101 adantr 
 |-  ( ( ( ( ( N e. Fin /\ R e. CRing ) /\ ( x e. B /\ y e. B ) ) /\ k e. N /\ l e. N ) /\ m e. N ) -> ( algSc ` P ) e. ( R RingHom P ) )
103 24 3ad2ant1 
 |-  ( ( ( ( N e. Fin /\ R e. CRing ) /\ ( x e. B /\ y e. B ) ) /\ k e. N /\ l e. N ) -> y e. ( Base ` A ) )
104 103 adantr 
 |-  ( ( ( ( ( N e. Fin /\ R e. CRing ) /\ ( x e. B /\ y e. B ) ) /\ k e. N /\ l e. N ) /\ m e. N ) -> y e. ( Base ` A ) )
105 104 22 sylibr 
 |-  ( ( ( ( ( N e. Fin /\ R e. CRing ) /\ ( x e. B /\ y e. B ) ) /\ k e. N /\ l e. N ) /\ m e. N ) -> y e. B )
106 2 11 3 72 77 105 matecld 
 |-  ( ( ( ( ( N e. Fin /\ R e. CRing ) /\ ( x e. B /\ y e. B ) ) /\ k e. N /\ l e. N ) /\ m e. N ) -> ( m y l ) e. ( Base ` R ) )
107 eqid 
 |-  ( .r ` P ) = ( .r ` P )
108 11 12 107 rhmmul 
 |-  ( ( ( algSc ` P ) e. ( R RingHom P ) /\ ( k x m ) e. ( Base ` R ) /\ ( m y l ) e. ( Base ` R ) ) -> ( ( algSc ` P ) ` ( ( k x m ) ( .r ` R ) ( m y l ) ) ) = ( ( ( algSc ` P ) ` ( k x m ) ) ( .r ` P ) ( ( algSc ` P ) ` ( m y l ) ) ) )
109 102 76 106 108 syl3anc 
 |-  ( ( ( ( ( N e. Fin /\ R e. CRing ) /\ ( x e. B /\ y e. B ) ) /\ k e. N /\ l e. N ) /\ m e. N ) -> ( ( algSc ` P ) ` ( ( k x m ) ( .r ` R ) ( m y l ) ) ) = ( ( ( algSc ` P ) ` ( k x m ) ) ( .r ` P ) ( ( algSc ` P ) ` ( m y l ) ) ) )
110 109 mpteq2dva 
 |-  ( ( ( ( N e. Fin /\ R e. CRing ) /\ ( x e. B /\ y e. B ) ) /\ k e. N /\ l e. N ) -> ( m e. N |-> ( ( algSc ` P ) ` ( ( k x m ) ( .r ` R ) ( m y l ) ) ) ) = ( m e. N |-> ( ( ( algSc ` P ) ` ( k x m ) ) ( .r ` P ) ( ( algSc ` P ) ` ( m y l ) ) ) ) )
111 110 oveq2d 
 |-  ( ( ( ( N e. Fin /\ R e. CRing ) /\ ( x e. B /\ y e. B ) ) /\ k e. N /\ l e. N ) -> ( P gsum ( m e. N |-> ( ( algSc ` P ) ` ( ( k x m ) ( .r ` R ) ( m y l ) ) ) ) ) = ( P gsum ( m e. N |-> ( ( ( algSc ` P ) ` ( k x m ) ) ( .r ` P ) ( ( algSc ` P ) ` ( m y l ) ) ) ) ) )
112 41 93 111 3eqtr2d 
 |-  ( ( ( ( N e. Fin /\ R e. CRing ) /\ ( x e. B /\ y e. B ) ) /\ k e. N /\ l e. N ) -> ( ( algSc ` P ) ` ( k ( x ( .r ` A ) y ) l ) ) = ( P gsum ( m e. N |-> ( ( ( algSc ` P ) ` ( k x m ) ) ( .r ` P ) ( ( algSc ` P ) ` ( m y l ) ) ) ) ) )
113 112 mpoeq3dva 
 |-  ( ( ( N e. Fin /\ R e. CRing ) /\ ( x e. B /\ y e. B ) ) -> ( k e. N , l e. N |-> ( ( algSc ` P ) ` ( k ( x ( .r ` A ) y ) l ) ) ) = ( k e. N , l e. N |-> ( P gsum ( m e. N |-> ( ( ( algSc ` P ) ` ( k x m ) ) ( .r ` P ) ( ( algSc ` P ) ` ( m y l ) ) ) ) ) ) )
114 eqid 
 |-  ( Base ` P ) = ( Base ` P )
115 eqid 
 |-  ( .r ` C ) = ( .r ` C )
116 48 ad2antlr 
 |-  ( ( ( N e. Fin /\ R e. CRing ) /\ ( x e. B /\ y e. B ) ) -> P e. Ring )
117 eqid 
 |-  ( i e. N , j e. N |-> ( ( algSc ` P ) ` ( i x j ) ) ) = ( i e. N , j e. N |-> ( ( algSc ` P ) ` ( i x j ) ) )
118 eqid 
 |-  ( i e. N , j e. N |-> ( ( algSc ` P ) ` ( i y j ) ) ) = ( i e. N , j e. N |-> ( ( algSc ` P ) ` ( i y j ) ) )
119 14 3ad2ant1 
 |-  ( ( ( ( N e. Fin /\ R e. CRing ) /\ ( x e. B /\ y e. B ) ) /\ i e. N /\ j e. N ) -> R e. Ring )
120 simp2 
 |-  ( ( ( ( N e. Fin /\ R e. CRing ) /\ ( x e. B /\ y e. B ) ) /\ i e. N /\ j e. N ) -> i e. N )
121 simp3 
 |-  ( ( ( ( N e. Fin /\ R e. CRing ) /\ ( x e. B /\ y e. B ) ) /\ i e. N /\ j e. N ) -> j e. N )
122 simp1rl 
 |-  ( ( ( ( N e. Fin /\ R e. CRing ) /\ ( x e. B /\ y e. B ) ) /\ i e. N /\ j e. N ) -> x e. B )
123 2 11 3 120 121 122 matecld 
 |-  ( ( ( ( N e. Fin /\ R e. CRing ) /\ ( x e. B /\ y e. B ) ) /\ i e. N /\ j e. N ) -> ( i x j ) e. ( Base ` R ) )
124 4 54 11 114 ply1sclcl 
 |-  ( ( R e. Ring /\ ( i x j ) e. ( Base ` R ) ) -> ( ( algSc ` P ) ` ( i x j ) ) e. ( Base ` P ) )
125 119 123 124 syl2anc 
 |-  ( ( ( ( N e. Fin /\ R e. CRing ) /\ ( x e. B /\ y e. B ) ) /\ i e. N /\ j e. N ) -> ( ( algSc ` P ) ` ( i x j ) ) e. ( Base ` P ) )
126 simp1rr 
 |-  ( ( ( ( N e. Fin /\ R e. CRing ) /\ ( x e. B /\ y e. B ) ) /\ i e. N /\ j e. N ) -> y e. B )
127 2 11 3 120 121 126 matecld 
 |-  ( ( ( ( N e. Fin /\ R e. CRing ) /\ ( x e. B /\ y e. B ) ) /\ i e. N /\ j e. N ) -> ( i y j ) e. ( Base ` R ) )
128 4 54 11 114 ply1sclcl 
 |-  ( ( R e. Ring /\ ( i y j ) e. ( Base ` R ) ) -> ( ( algSc ` P ) ` ( i y j ) ) e. ( Base ` P ) )
129 119 127 128 syl2anc 
 |-  ( ( ( ( N e. Fin /\ R e. CRing ) /\ ( x e. B /\ y e. B ) ) /\ i e. N /\ j e. N ) -> ( ( algSc ` P ) ` ( i y j ) ) e. ( Base ` P ) )
130 oveq12 
 |-  ( ( k = i /\ m = j ) -> ( k x m ) = ( i x j ) )
131 130 fveq2d 
 |-  ( ( k = i /\ m = j ) -> ( ( algSc ` P ) ` ( k x m ) ) = ( ( algSc ` P ) ` ( i x j ) ) )
132 131 adantl 
 |-  ( ( ( ( N e. Fin /\ R e. CRing ) /\ ( x e. B /\ y e. B ) ) /\ ( k = i /\ m = j ) ) -> ( ( algSc ` P ) ` ( k x m ) ) = ( ( algSc ` P ) ` ( i x j ) ) )
133 oveq12 
 |-  ( ( m = i /\ l = j ) -> ( m y l ) = ( i y j ) )
134 133 fveq2d 
 |-  ( ( m = i /\ l = j ) -> ( ( algSc ` P ) ` ( m y l ) ) = ( ( algSc ` P ) ` ( i y j ) ) )
135 134 adantl 
 |-  ( ( ( ( N e. Fin /\ R e. CRing ) /\ ( x e. B /\ y e. B ) ) /\ ( m = i /\ l = j ) ) -> ( ( algSc ` P ) ` ( m y l ) ) = ( ( algSc ` P ) ` ( i y j ) ) )
136 fvexd 
 |-  ( ( ( ( N e. Fin /\ R e. CRing ) /\ ( x e. B /\ y e. B ) ) /\ k e. N /\ m e. N ) -> ( ( algSc ` P ) ` ( k x m ) ) e. _V )
137 fvexd 
 |-  ( ( ( ( N e. Fin /\ R e. CRing ) /\ ( x e. B /\ y e. B ) ) /\ m e. N /\ l e. N ) -> ( ( algSc ` P ) ` ( m y l ) ) e. _V )
138 5 114 115 107 116 15 117 118 125 129 132 135 136 137 mpomatmul 
 |-  ( ( ( N e. Fin /\ R e. CRing ) /\ ( x e. B /\ y e. B ) ) -> ( ( i e. N , j e. N |-> ( ( algSc ` P ) ` ( i x j ) ) ) ( .r ` C ) ( i e. N , j e. N |-> ( ( algSc ` P ) ` ( i y j ) ) ) ) = ( k e. N , l e. N |-> ( P gsum ( m e. N |-> ( ( ( algSc ` P ) ` ( k x m ) ) ( .r ` P ) ( ( algSc ` P ) ` ( m y l ) ) ) ) ) ) )
139 113 138 eqtr4d 
 |-  ( ( ( N e. Fin /\ R e. CRing ) /\ ( x e. B /\ y e. B ) ) -> ( k e. N , l e. N |-> ( ( algSc ` P ) ` ( k ( x ( .r ` A ) y ) l ) ) ) = ( ( i e. N , j e. N |-> ( ( algSc ` P ) ` ( i x j ) ) ) ( .r ` C ) ( i e. N , j e. N |-> ( ( algSc ` P ) ` ( i y j ) ) ) ) )
140 2 matring 
 |-  ( ( N e. Fin /\ R e. Ring ) -> A e. Ring )
141 13 140 sylan2 
 |-  ( ( N e. Fin /\ R e. CRing ) -> A e. Ring )
142 141 anim1i 
 |-  ( ( ( N e. Fin /\ R e. CRing ) /\ ( x e. B /\ y e. B ) ) -> ( A e. Ring /\ ( x e. B /\ y e. B ) ) )
143 3anass 
 |-  ( ( A e. Ring /\ x e. B /\ y e. B ) <-> ( A e. Ring /\ ( x e. B /\ y e. B ) ) )
144 142 143 sylibr 
 |-  ( ( ( N e. Fin /\ R e. CRing ) /\ ( x e. B /\ y e. B ) ) -> ( A e. Ring /\ x e. B /\ y e. B ) )
145 eqid 
 |-  ( .r ` A ) = ( .r ` A )
146 3 145 ringcl 
 |-  ( ( A e. Ring /\ x e. B /\ y e. B ) -> ( x ( .r ` A ) y ) e. B )
147 144 146 syl 
 |-  ( ( ( N e. Fin /\ R e. CRing ) /\ ( x e. B /\ y e. B ) ) -> ( x ( .r ` A ) y ) e. B )
148 1 2 3 4 54 mat2pmatval 
 |-  ( ( N e. Fin /\ R e. Ring /\ ( x ( .r ` A ) y ) e. B ) -> ( T ` ( x ( .r ` A ) y ) ) = ( k e. N , l e. N |-> ( ( algSc ` P ) ` ( k ( x ( .r ` A ) y ) l ) ) ) )
149 15 14 147 148 syl3anc 
 |-  ( ( ( N e. Fin /\ R e. CRing ) /\ ( x e. B /\ y e. B ) ) -> ( T ` ( x ( .r ` A ) y ) ) = ( k e. N , l e. N |-> ( ( algSc ` P ) ` ( k ( x ( .r ` A ) y ) l ) ) ) )
150 simpl 
 |-  ( ( x e. B /\ y e. B ) -> x e. B )
151 150 anim2i 
 |-  ( ( ( N e. Fin /\ R e. CRing ) /\ ( x e. B /\ y e. B ) ) -> ( ( N e. Fin /\ R e. CRing ) /\ x e. B ) )
152 df-3an 
 |-  ( ( N e. Fin /\ R e. CRing /\ x e. B ) <-> ( ( N e. Fin /\ R e. CRing ) /\ x e. B ) )
153 151 152 sylibr 
 |-  ( ( ( N e. Fin /\ R e. CRing ) /\ ( x e. B /\ y e. B ) ) -> ( N e. Fin /\ R e. CRing /\ x e. B ) )
154 1 2 3 4 54 mat2pmatval 
 |-  ( ( N e. Fin /\ R e. CRing /\ x e. B ) -> ( T ` x ) = ( i e. N , j e. N |-> ( ( algSc ` P ) ` ( i x j ) ) ) )
155 153 154 syl 
 |-  ( ( ( N e. Fin /\ R e. CRing ) /\ ( x e. B /\ y e. B ) ) -> ( T ` x ) = ( i e. N , j e. N |-> ( ( algSc ` P ) ` ( i x j ) ) ) )
156 simpr 
 |-  ( ( x e. B /\ y e. B ) -> y e. B )
157 156 anim2i 
 |-  ( ( ( N e. Fin /\ R e. CRing ) /\ ( x e. B /\ y e. B ) ) -> ( ( N e. Fin /\ R e. CRing ) /\ y e. B ) )
158 df-3an 
 |-  ( ( N e. Fin /\ R e. CRing /\ y e. B ) <-> ( ( N e. Fin /\ R e. CRing ) /\ y e. B ) )
159 157 158 sylibr 
 |-  ( ( ( N e. Fin /\ R e. CRing ) /\ ( x e. B /\ y e. B ) ) -> ( N e. Fin /\ R e. CRing /\ y e. B ) )
160 1 2 3 4 54 mat2pmatval 
 |-  ( ( N e. Fin /\ R e. CRing /\ y e. B ) -> ( T ` y ) = ( i e. N , j e. N |-> ( ( algSc ` P ) ` ( i y j ) ) ) )
161 159 160 syl 
 |-  ( ( ( N e. Fin /\ R e. CRing ) /\ ( x e. B /\ y e. B ) ) -> ( T ` y ) = ( i e. N , j e. N |-> ( ( algSc ` P ) ` ( i y j ) ) ) )
162 155 161 oveq12d 
 |-  ( ( ( N e. Fin /\ R e. CRing ) /\ ( x e. B /\ y e. B ) ) -> ( ( T ` x ) ( .r ` C ) ( T ` y ) ) = ( ( i e. N , j e. N |-> ( ( algSc ` P ) ` ( i x j ) ) ) ( .r ` C ) ( i e. N , j e. N |-> ( ( algSc ` P ) ` ( i y j ) ) ) ) )
163 139 149 162 3eqtr4d 
 |-  ( ( ( N e. Fin /\ R e. CRing ) /\ ( x e. B /\ y e. B ) ) -> ( T ` ( x ( .r ` A ) y ) ) = ( ( T ` x ) ( .r ` C ) ( T ` y ) ) )
164 163 ralrimivva 
 |-  ( ( N e. Fin /\ R e. CRing ) -> A. x e. B A. y e. B ( T ` ( x ( .r ` A ) y ) ) = ( ( T ` x ) ( .r ` C ) ( T ` y ) ) )