Metamath Proof Explorer

Theorem mat2pmatghm

Description: The transformation of matrices into polynomial matrices is an additive group homomorphism. (Contributed by AV, 28-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 mat2pmatghm 
|- ( ( N e. Fin /\ R e. Ring ) -> T e. ( A GrpHom C ) )

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 
 |-  ( +g ` A ) = ( +g ` A )
8 eqid 
 |-  ( +g ` C ) = ( +g ` C )
9 2 matgrp 
 |-  ( ( N e. Fin /\ R e. Ring ) -> A e. Grp )
10 4 5 pmatring 
 |-  ( ( N e. Fin /\ R e. Ring ) -> C e. Ring )
11 ringgrp 
 |-  ( C e. Ring -> C e. Grp )
12 10 11 syl 
 |-  ( ( N e. Fin /\ R e. Ring ) -> C e. Grp )
13 1 2 3 4 5 6 mat2pmatf 
 |-  ( ( N e. Fin /\ R e. Ring ) -> T : B --> H )
14 eqid 
 |-  ( Base ` P ) = ( Base ` P )
15 simpl 
 |-  ( ( N e. Fin /\ R e. Ring ) -> N e. Fin )
16 15 adantr 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( x e. B /\ y e. B ) ) -> N e. Fin )
17 4 ply1ring 
 |-  ( R e. Ring -> P e. Ring )
18 17 ad2antlr 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( x e. B /\ y e. B ) ) -> P e. Ring )
19 simp1lr 
 |-  ( ( ( ( N e. Fin /\ R e. Ring ) /\ ( x e. B /\ y e. B ) ) /\ i e. N /\ j e. N ) -> R e. Ring )
20 eqid 
 |-  ( Base ` R ) = ( Base ` R )
21 simp2 
 |-  ( ( ( ( N e. Fin /\ R e. Ring ) /\ ( x e. B /\ y e. B ) ) /\ i e. N /\ j e. N ) -> i e. N )
22 simp3 
 |-  ( ( ( ( N e. Fin /\ R e. Ring ) /\ ( x e. B /\ y e. B ) ) /\ i e. N /\ j e. N ) -> j e. N )
23 simp1rl 
 |-  ( ( ( ( N e. Fin /\ R e. Ring ) /\ ( x e. B /\ y e. B ) ) /\ i e. N /\ j e. N ) -> x e. B )
24 2 20 3 21 22 23 matecld 
 |-  ( ( ( ( N e. Fin /\ R e. Ring ) /\ ( x e. B /\ y e. B ) ) /\ i e. N /\ j e. N ) -> ( i x j ) e. ( Base ` R ) )
25 eqid 
 |-  ( algSc ` P ) = ( algSc ` P )
26 4 25 20 14 ply1sclcl 
 |-  ( ( R e. Ring /\ ( i x j ) e. ( Base ` R ) ) -> ( ( algSc ` P ) ` ( i x j ) ) e. ( Base ` P ) )
27 19 24 26 syl2anc 
 |-  ( ( ( ( N e. Fin /\ R e. Ring ) /\ ( x e. B /\ y e. B ) ) /\ i e. N /\ j e. N ) -> ( ( algSc ` P ) ` ( i x j ) ) e. ( Base ` P ) )
28 5 14 6 16 18 27 matbas2d 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( x e. B /\ y e. B ) ) -> ( i e. N , j e. N |-> ( ( algSc ` P ) ` ( i x j ) ) ) e. H )
29 simp1rr 
 |-  ( ( ( ( N e. Fin /\ R e. Ring ) /\ ( x e. B /\ y e. B ) ) /\ i e. N /\ j e. N ) -> y e. B )
30 2 20 3 21 22 29 matecld 
 |-  ( ( ( ( N e. Fin /\ R e. Ring ) /\ ( x e. B /\ y e. B ) ) /\ i e. N /\ j e. N ) -> ( i y j ) e. ( Base ` R ) )
31 4 25 20 14 ply1sclcl 
 |-  ( ( R e. Ring /\ ( i y j ) e. ( Base ` R ) ) -> ( ( algSc ` P ) ` ( i y j ) ) e. ( Base ` P ) )
32 19 30 31 syl2anc 
 |-  ( ( ( ( N e. Fin /\ R e. Ring ) /\ ( x e. B /\ y e. B ) ) /\ i e. N /\ j e. N ) -> ( ( algSc ` P ) ` ( i y j ) ) e. ( Base ` P ) )
33 5 14 6 16 18 32 matbas2d 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( x e. B /\ y e. B ) ) -> ( i e. N , j e. N |-> ( ( algSc ` P ) ` ( i y j ) ) ) e. H )
34 eqid 
 |-  ( +g ` P ) = ( +g ` P )
35 5 6 8 34 matplusg2 
 |-  ( ( ( i e. N , j e. N |-> ( ( algSc ` P ) ` ( i x j ) ) ) e. H /\ ( i e. N , j e. N |-> ( ( algSc ` P ) ` ( i y j ) ) ) e. H ) -> ( ( i e. N , j e. N |-> ( ( algSc ` P ) ` ( i x j ) ) ) ( +g ` C ) ( i e. N , j e. N |-> ( ( algSc ` P ) ` ( i y j ) ) ) ) = ( ( i e. N , j e. N |-> ( ( algSc ` P ) ` ( i x j ) ) ) oF ( +g ` P ) ( i e. N , j e. N |-> ( ( algSc ` P ) ` ( i y j ) ) ) ) )
36 28 33 35 syl2anc 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( x e. B /\ y e. B ) ) -> ( ( i e. N , j e. N |-> ( ( algSc ` P ) ` ( i x j ) ) ) ( +g ` C ) ( i e. N , j e. N |-> ( ( algSc ` P ) ` ( i y j ) ) ) ) = ( ( i e. N , j e. N |-> ( ( algSc ` P ) ` ( i x j ) ) ) oF ( +g ` P ) ( i e. N , j e. N |-> ( ( algSc ` P ) ` ( i y j ) ) ) ) )
37 fvexd 
 |-  ( ( ( ( N e. Fin /\ R e. Ring ) /\ ( x e. B /\ y e. B ) ) /\ i e. N /\ j e. N ) -> ( ( algSc ` P ) ` ( i x j ) ) e. _V )
38 fvexd 
 |-  ( ( ( ( N e. Fin /\ R e. Ring ) /\ ( x e. B /\ y e. B ) ) /\ i e. N /\ j e. N ) -> ( ( algSc ` P ) ` ( i y j ) ) e. _V )
39 eqidd 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( x e. B /\ y e. B ) ) -> ( i e. N , j e. N |-> ( ( algSc ` P ) ` ( i x j ) ) ) = ( i e. N , j e. N |-> ( ( algSc ` P ) ` ( i x j ) ) ) )
40 eqidd 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( x e. B /\ y e. B ) ) -> ( i e. N , j e. N |-> ( ( algSc ` P ) ` ( i y j ) ) ) = ( i e. N , j e. N |-> ( ( algSc ` P ) ` ( i y j ) ) ) )
41 16 16 37 38 39 40 offval22 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( x e. B /\ y e. B ) ) -> ( ( i e. N , j e. N |-> ( ( algSc ` P ) ` ( i x j ) ) ) oF ( +g ` P ) ( i e. N , j e. N |-> ( ( algSc ` P ) ` ( i y j ) ) ) ) = ( i e. N , j e. N |-> ( ( ( algSc ` P ) ` ( i x j ) ) ( +g ` P ) ( ( algSc ` P ) ` ( i y j ) ) ) ) )
42 simpr 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( x e. B /\ y e. B ) ) -> ( x e. B /\ y e. B ) )
43 42 3ad2ant1 
 |-  ( ( ( ( N e. Fin /\ R e. Ring ) /\ ( x e. B /\ y e. B ) ) /\ i e. N /\ j e. N ) -> ( x e. B /\ y e. B ) )
44 3simpc 
 |-  ( ( ( ( N e. Fin /\ R e. Ring ) /\ ( x e. B /\ y e. B ) ) /\ i e. N /\ j e. N ) -> ( i e. N /\ j e. N ) )
45 eqid 
 |-  ( +g ` R ) = ( +g ` R )
46 2 3 7 45 matplusgcell 
 |-  ( ( ( x e. B /\ y e. B ) /\ ( i e. N /\ j e. N ) ) -> ( i ( x ( +g ` A ) y ) j ) = ( ( i x j ) ( +g ` R ) ( i y j ) ) )
47 43 44 46 syl2anc 
 |-  ( ( ( ( N e. Fin /\ R e. Ring ) /\ ( x e. B /\ y e. B ) ) /\ i e. N /\ j e. N ) -> ( i ( x ( +g ` A ) y ) j ) = ( ( i x j ) ( +g ` R ) ( i y j ) ) )
48 4 ply1sca 
 |-  ( R e. Ring -> R = ( Scalar ` P ) )
49 48 adantl 
 |-  ( ( N e. Fin /\ R e. Ring ) -> R = ( Scalar ` P ) )
50 49 fveq2d 
 |-  ( ( N e. Fin /\ R e. Ring ) -> ( +g ` R ) = ( +g ` ( Scalar ` P ) ) )
51 50 oveqd 
 |-  ( ( N e. Fin /\ R e. Ring ) -> ( ( i x j ) ( +g ` R ) ( i y j ) ) = ( ( i x j ) ( +g ` ( Scalar ` P ) ) ( i y j ) ) )
52 51 adantr 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( x e. B /\ y e. B ) ) -> ( ( i x j ) ( +g ` R ) ( i y j ) ) = ( ( i x j ) ( +g ` ( Scalar ` P ) ) ( i y j ) ) )
53 52 3ad2ant1 
 |-  ( ( ( ( N e. Fin /\ R e. Ring ) /\ ( x e. B /\ y e. B ) ) /\ i e. N /\ j e. N ) -> ( ( i x j ) ( +g ` R ) ( i y j ) ) = ( ( i x j ) ( +g ` ( Scalar ` P ) ) ( i y j ) ) )
54 47 53 eqtrd 
 |-  ( ( ( ( N e. Fin /\ R e. Ring ) /\ ( x e. B /\ y e. B ) ) /\ i e. N /\ j e. N ) -> ( i ( x ( +g ` A ) y ) j ) = ( ( i x j ) ( +g ` ( Scalar ` P ) ) ( i y j ) ) )
55 54 fveq2d 
 |-  ( ( ( ( N e. Fin /\ R e. Ring ) /\ ( x e. B /\ y e. B ) ) /\ i e. N /\ j e. N ) -> ( ( algSc ` P ) ` ( i ( x ( +g ` A ) y ) j ) ) = ( ( algSc ` P ) ` ( ( i x j ) ( +g ` ( Scalar ` P ) ) ( i y j ) ) ) )
56 eqid 
 |-  ( Scalar ` P ) = ( Scalar ` P )
57 18 3ad2ant1 
 |-  ( ( ( ( N e. Fin /\ R e. Ring ) /\ ( x e. B /\ y e. B ) ) /\ i e. N /\ j e. N ) -> P e. Ring )
58 4 ply1lmod 
 |-  ( R e. Ring -> P e. LMod )
59 58 ad2antlr 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( x e. B /\ y e. B ) ) -> P e. LMod )
60 59 3ad2ant1 
 |-  ( ( ( ( N e. Fin /\ R e. Ring ) /\ ( x e. B /\ y e. B ) ) /\ i e. N /\ j e. N ) -> P e. LMod )
61 25 56 57 60 asclghm 
 |-  ( ( ( ( N e. Fin /\ R e. Ring ) /\ ( x e. B /\ y e. B ) ) /\ i e. N /\ j e. N ) -> ( algSc ` P ) e. ( ( Scalar ` P ) GrpHom P ) )
62 49 eqcomd 
 |-  ( ( N e. Fin /\ R e. Ring ) -> ( Scalar ` P ) = R )
63 62 fveq2d 
 |-  ( ( N e. Fin /\ R e. Ring ) -> ( Base ` ( Scalar ` P ) ) = ( Base ` R ) )
64 63 eleq2d 
 |-  ( ( N e. Fin /\ R e. Ring ) -> ( ( i x j ) e. ( Base ` ( Scalar ` P ) ) <-> ( i x j ) e. ( Base ` R ) ) )
65 64 adantr 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( x e. B /\ y e. B ) ) -> ( ( i x j ) e. ( Base ` ( Scalar ` P ) ) <-> ( i x j ) e. ( Base ` R ) ) )
66 65 3ad2ant1 
 |-  ( ( ( ( N e. Fin /\ R e. Ring ) /\ ( x e. B /\ y e. B ) ) /\ i e. N /\ j e. N ) -> ( ( i x j ) e. ( Base ` ( Scalar ` P ) ) <-> ( i x j ) e. ( Base ` R ) ) )
67 24 66 mpbird 
 |-  ( ( ( ( N e. Fin /\ R e. Ring ) /\ ( x e. B /\ y e. B ) ) /\ i e. N /\ j e. N ) -> ( i x j ) e. ( Base ` ( Scalar ` P ) ) )
68 63 eleq2d 
 |-  ( ( N e. Fin /\ R e. Ring ) -> ( ( i y j ) e. ( Base ` ( Scalar ` P ) ) <-> ( i y j ) e. ( Base ` R ) ) )
69 68 adantr 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( x e. B /\ y e. B ) ) -> ( ( i y j ) e. ( Base ` ( Scalar ` P ) ) <-> ( i y j ) e. ( Base ` R ) ) )
70 69 3ad2ant1 
 |-  ( ( ( ( N e. Fin /\ R e. Ring ) /\ ( x e. B /\ y e. B ) ) /\ i e. N /\ j e. N ) -> ( ( i y j ) e. ( Base ` ( Scalar ` P ) ) <-> ( i y j ) e. ( Base ` R ) ) )
71 30 70 mpbird 
 |-  ( ( ( ( N e. Fin /\ R e. Ring ) /\ ( x e. B /\ y e. B ) ) /\ i e. N /\ j e. N ) -> ( i y j ) e. ( Base ` ( Scalar ` P ) ) )
72 eqid 
 |-  ( Base ` ( Scalar ` P ) ) = ( Base ` ( Scalar ` P ) )
73 eqid 
 |-  ( +g ` ( Scalar ` P ) ) = ( +g ` ( Scalar ` P ) )
74 72 73 34 ghmlin 
 |-  ( ( ( algSc ` P ) e. ( ( Scalar ` P ) GrpHom P ) /\ ( i x j ) e. ( Base ` ( Scalar ` P ) ) /\ ( i y j ) e. ( Base ` ( Scalar ` P ) ) ) -> ( ( algSc ` P ) ` ( ( i x j ) ( +g ` ( Scalar ` P ) ) ( i y j ) ) ) = ( ( ( algSc ` P ) ` ( i x j ) ) ( +g ` P ) ( ( algSc ` P ) ` ( i y j ) ) ) )
75 61 67 71 74 syl3anc 
 |-  ( ( ( ( N e. Fin /\ R e. Ring ) /\ ( x e. B /\ y e. B ) ) /\ i e. N /\ j e. N ) -> ( ( algSc ` P ) ` ( ( i x j ) ( +g ` ( Scalar ` P ) ) ( i y j ) ) ) = ( ( ( algSc ` P ) ` ( i x j ) ) ( +g ` P ) ( ( algSc ` P ) ` ( i y j ) ) ) )
76 55 75 eqtr2d 
 |-  ( ( ( ( N e. Fin /\ R e. Ring ) /\ ( x e. B /\ y e. B ) ) /\ i e. N /\ j e. N ) -> ( ( ( algSc ` P ) ` ( i x j ) ) ( +g ` P ) ( ( algSc ` P ) ` ( i y j ) ) ) = ( ( algSc ` P ) ` ( i ( x ( +g ` A ) y ) j ) ) )
77 76 mpoeq3dva 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( x e. B /\ y e. B ) ) -> ( i e. N , j e. N |-> ( ( ( algSc ` P ) ` ( i x j ) ) ( +g ` P ) ( ( algSc ` P ) ` ( i y j ) ) ) ) = ( i e. N , j e. N |-> ( ( algSc ` P ) ` ( i ( x ( +g ` A ) y ) j ) ) ) )
78 41 77 eqtrd 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( x e. B /\ y e. B ) ) -> ( ( i e. N , j e. N |-> ( ( algSc ` P ) ` ( i x j ) ) ) oF ( +g ` P ) ( i e. N , j e. N |-> ( ( algSc ` P ) ` ( i y j ) ) ) ) = ( i e. N , j e. N |-> ( ( algSc ` P ) ` ( i ( x ( +g ` A ) y ) j ) ) ) )
79 36 78 eqtr2d 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( x e. B /\ y e. B ) ) -> ( i e. N , j e. N |-> ( ( algSc ` P ) ` ( i ( x ( +g ` A ) y ) j ) ) ) = ( ( i e. N , j e. N |-> ( ( algSc ` P ) ` ( i x j ) ) ) ( +g ` C ) ( i e. N , j e. N |-> ( ( algSc ` P ) ` ( i y j ) ) ) ) )
80 simpl 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( x e. B /\ y e. B ) ) -> ( N e. Fin /\ R e. Ring ) )
81 2 matring 
 |-  ( ( N e. Fin /\ R e. Ring ) -> A e. Ring )
82 ringmnd 
 |-  ( A e. Ring -> A e. Mnd )
83 81 82 syl 
 |-  ( ( N e. Fin /\ R e. Ring ) -> A e. Mnd )
84 83 anim1i 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( x e. B /\ y e. B ) ) -> ( A e. Mnd /\ ( x e. B /\ y e. B ) ) )
85 3anass 
 |-  ( ( A e. Mnd /\ x e. B /\ y e. B ) <-> ( A e. Mnd /\ ( x e. B /\ y e. B ) ) )
86 84 85 sylibr 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( x e. B /\ y e. B ) ) -> ( A e. Mnd /\ x e. B /\ y e. B ) )
87 3 7 mndcl 
 |-  ( ( A e. Mnd /\ x e. B /\ y e. B ) -> ( x ( +g ` A ) y ) e. B )
88 86 87 syl 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( x e. B /\ y e. B ) ) -> ( x ( +g ` A ) y ) e. B )
89 df-3an 
 |-  ( ( N e. Fin /\ R e. Ring /\ ( x ( +g ` A ) y ) e. B ) <-> ( ( N e. Fin /\ R e. Ring ) /\ ( x ( +g ` A ) y ) e. B ) )
90 80 88 89 sylanbrc 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( x e. B /\ y e. B ) ) -> ( N e. Fin /\ R e. Ring /\ ( x ( +g ` A ) y ) e. B ) )
91 1 2 3 4 25 mat2pmatval 
 |-  ( ( N e. Fin /\ R e. Ring /\ ( x ( +g ` A ) y ) e. B ) -> ( T ` ( x ( +g ` A ) y ) ) = ( i e. N , j e. N |-> ( ( algSc ` P ) ` ( i ( x ( +g ` A ) y ) j ) ) ) )
92 90 91 syl 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( x e. B /\ y e. B ) ) -> ( T ` ( x ( +g ` A ) y ) ) = ( i e. N , j e. N |-> ( ( algSc ` P ) ` ( i ( x ( +g ` A ) y ) j ) ) ) )
93 simpl 
 |-  ( ( x e. B /\ y e. B ) -> x e. B )
94 93 anim2i 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( x e. B /\ y e. B ) ) -> ( ( N e. Fin /\ R e. Ring ) /\ x e. B ) )
95 df-3an 
 |-  ( ( N e. Fin /\ R e. Ring /\ x e. B ) <-> ( ( N e. Fin /\ R e. Ring ) /\ x e. B ) )
96 94 95 sylibr 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( x e. B /\ y e. B ) ) -> ( N e. Fin /\ R e. Ring /\ x e. B ) )
97 1 2 3 4 25 mat2pmatval 
 |-  ( ( N e. Fin /\ R e. Ring /\ x e. B ) -> ( T ` x ) = ( i e. N , j e. N |-> ( ( algSc ` P ) ` ( i x j ) ) ) )
98 96 97 syl 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( x e. B /\ y e. B ) ) -> ( T ` x ) = ( i e. N , j e. N |-> ( ( algSc ` P ) ` ( i x j ) ) ) )
99 simpr 
 |-  ( ( x e. B /\ y e. B ) -> y e. B )
100 99 anim2i 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( x e. B /\ y e. B ) ) -> ( ( N e. Fin /\ R e. Ring ) /\ y e. B ) )
101 df-3an 
 |-  ( ( N e. Fin /\ R e. Ring /\ y e. B ) <-> ( ( N e. Fin /\ R e. Ring ) /\ y e. B ) )
102 100 101 sylibr 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( x e. B /\ y e. B ) ) -> ( N e. Fin /\ R e. Ring /\ y e. B ) )
103 1 2 3 4 25 mat2pmatval 
 |-  ( ( N e. Fin /\ R e. Ring /\ y e. B ) -> ( T ` y ) = ( i e. N , j e. N |-> ( ( algSc ` P ) ` ( i y j ) ) ) )
104 102 103 syl 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( x e. B /\ y e. B ) ) -> ( T ` y ) = ( i e. N , j e. N |-> ( ( algSc ` P ) ` ( i y j ) ) ) )
105 98 104 oveq12d 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( x e. B /\ y e. B ) ) -> ( ( T ` x ) ( +g ` C ) ( T ` y ) ) = ( ( i e. N , j e. N |-> ( ( algSc ` P ) ` ( i x j ) ) ) ( +g ` C ) ( i e. N , j e. N |-> ( ( algSc ` P ) ` ( i y j ) ) ) ) )
106 79 92 105 3eqtr4d 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( x e. B /\ y e. B ) ) -> ( T ` ( x ( +g ` A ) y ) ) = ( ( T ` x ) ( +g ` C ) ( T ` y ) ) )
107 3 6 7 8 9 12 13 106 isghmd 
 |-  ( ( N e. Fin /\ R e. Ring ) -> T e. ( A GrpHom C ) )