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 |
|
crngring |
|- ( R e. CRing -> R e. Ring ) |
8 |
2
|
matring |
|- ( ( N e. Fin /\ R e. Ring ) -> A e. Ring ) |
9 |
7 8
|
sylan2 |
|- ( ( N e. Fin /\ R e. CRing ) -> A e. Ring ) |
10 |
4
|
ply1ring |
|- ( R e. Ring -> P e. Ring ) |
11 |
7 10
|
syl |
|- ( R e. CRing -> P e. Ring ) |
12 |
5
|
matring |
|- ( ( N e. Fin /\ P e. Ring ) -> C e. Ring ) |
13 |
11 12
|
sylan2 |
|- ( ( N e. Fin /\ R e. CRing ) -> C e. Ring ) |
14 |
1 2 3 4 5 6
|
mat2pmatghm |
|- ( ( N e. Fin /\ R e. Ring ) -> T e. ( A GrpHom C ) ) |
15 |
7 14
|
sylan2 |
|- ( ( N e. Fin /\ R e. CRing ) -> T e. ( A GrpHom C ) ) |
16 |
1 2 3 4 5 6
|
mat2pmatmhm |
|- ( ( N e. Fin /\ R e. CRing ) -> T e. ( ( mulGrp ` A ) MndHom ( mulGrp ` C ) ) ) |
17 |
15 16
|
jca |
|- ( ( N e. Fin /\ R e. CRing ) -> ( T e. ( A GrpHom C ) /\ T e. ( ( mulGrp ` A ) MndHom ( mulGrp ` C ) ) ) ) |
18 |
|
eqid |
|- ( mulGrp ` A ) = ( mulGrp ` A ) |
19 |
|
eqid |
|- ( mulGrp ` C ) = ( mulGrp ` C ) |
20 |
18 19
|
isrhm |
|- ( T e. ( A RingHom C ) <-> ( ( A e. Ring /\ C e. Ring ) /\ ( T e. ( A GrpHom C ) /\ T e. ( ( mulGrp ` A ) MndHom ( mulGrp ` C ) ) ) ) ) |
21 |
9 13 17 20
|
syl21anbrc |
|- ( ( N e. Fin /\ R e. CRing ) -> T e. ( A RingHom C ) ) |