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