Step |
Hyp |
Ref |
Expression |
1 |
|
m2cpm.s |
|- S = ( N ConstPolyMat R ) |
2 |
|
m2cpm.t |
|- T = ( N matToPolyMat R ) |
3 |
|
m2cpm.a |
|- A = ( N Mat R ) |
4 |
|
m2cpm.b |
|- B = ( Base ` A ) |
5 |
|
m2cpmghm.p |
|- P = ( Poly1 ` R ) |
6 |
|
m2cpmghm.c |
|- C = ( N Mat P ) |
7 |
|
m2cpmghm.u |
|- U = ( C |`s S ) |
8 |
|
eqid |
|- ( Base ` C ) = ( Base ` C ) |
9 |
2 3 4 5 6 8
|
mat2pmatghm |
|- ( ( N e. Fin /\ R e. Ring ) -> T e. ( A GrpHom C ) ) |
10 |
1 5 6
|
cpmatsubgpmat |
|- ( ( N e. Fin /\ R e. Ring ) -> S e. ( SubGrp ` C ) ) |
11 |
1 2 3 4
|
m2cpmf |
|- ( ( N e. Fin /\ R e. Ring ) -> T : B --> S ) |
12 |
11
|
frnd |
|- ( ( N e. Fin /\ R e. Ring ) -> ran T C_ S ) |
13 |
7
|
resghm2b |
|- ( ( S e. ( SubGrp ` C ) /\ ran T C_ S ) -> ( T e. ( A GrpHom C ) <-> T e. ( A GrpHom U ) ) ) |
14 |
13
|
bicomd |
|- ( ( S e. ( SubGrp ` C ) /\ ran T C_ S ) -> ( T e. ( A GrpHom U ) <-> T e. ( A GrpHom C ) ) ) |
15 |
10 12 14
|
syl2anc |
|- ( ( N e. Fin /\ R e. Ring ) -> ( T e. ( A GrpHom U ) <-> T e. ( A GrpHom C ) ) ) |
16 |
9 15
|
mpbird |
|- ( ( N e. Fin /\ R e. Ring ) -> T e. ( A GrpHom U ) ) |