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 𝑇 = ( 𝑁 matToPolyMat 𝑅 )
mat2pmatbas.a 𝐴 = ( 𝑁 Mat 𝑅 )
mat2pmatbas.b 𝐵 = ( Base ‘ 𝐴 )
mat2pmatbas.p 𝑃 = ( Poly1𝑅 )
mat2pmatbas.c 𝐶 = ( 𝑁 Mat 𝑃 )
mat2pmatbas0.h 𝐻 = ( Base ‘ 𝐶 )
Assertion mat2pmatghm ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → 𝑇 ∈ ( 𝐴 GrpHom 𝐶 ) )

Proof

Step Hyp Ref Expression
1 mat2pmatbas.t 𝑇 = ( 𝑁 matToPolyMat 𝑅 )
2 mat2pmatbas.a 𝐴 = ( 𝑁 Mat 𝑅 )
3 mat2pmatbas.b 𝐵 = ( Base ‘ 𝐴 )
4 mat2pmatbas.p 𝑃 = ( Poly1𝑅 )
5 mat2pmatbas.c 𝐶 = ( 𝑁 Mat 𝑃 )
6 mat2pmatbas0.h 𝐻 = ( Base ‘ 𝐶 )
7 eqid ( +g𝐴 ) = ( +g𝐴 )
8 eqid ( +g𝐶 ) = ( +g𝐶 )
9 2 matgrp ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → 𝐴 ∈ Grp )
10 4 5 pmatring ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → 𝐶 ∈ Ring )
11 ringgrp ( 𝐶 ∈ Ring → 𝐶 ∈ Grp )
12 10 11 syl ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → 𝐶 ∈ Grp )
13 1 2 3 4 5 6 mat2pmatf ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → 𝑇 : 𝐵𝐻 )
14 eqid ( Base ‘ 𝑃 ) = ( Base ‘ 𝑃 )
15 simpl ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → 𝑁 ∈ Fin )
16 15 adantr ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑥𝐵𝑦𝐵 ) ) → 𝑁 ∈ Fin )
17 4 ply1ring ( 𝑅 ∈ Ring → 𝑃 ∈ Ring )
18 17 ad2antlr ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑥𝐵𝑦𝐵 ) ) → 𝑃 ∈ Ring )
19 simp1lr ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑥𝐵𝑦𝐵 ) ) ∧ 𝑖𝑁𝑗𝑁 ) → 𝑅 ∈ Ring )
20 eqid ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
21 simp2 ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑥𝐵𝑦𝐵 ) ) ∧ 𝑖𝑁𝑗𝑁 ) → 𝑖𝑁 )
22 simp3 ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑥𝐵𝑦𝐵 ) ) ∧ 𝑖𝑁𝑗𝑁 ) → 𝑗𝑁 )
23 simp1rl ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑥𝐵𝑦𝐵 ) ) ∧ 𝑖𝑁𝑗𝑁 ) → 𝑥𝐵 )
24 2 20 3 21 22 23 matecld ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑥𝐵𝑦𝐵 ) ) ∧ 𝑖𝑁𝑗𝑁 ) → ( 𝑖 𝑥 𝑗 ) ∈ ( Base ‘ 𝑅 ) )
25 eqid ( algSc ‘ 𝑃 ) = ( algSc ‘ 𝑃 )
26 4 25 20 14 ply1sclcl ( ( 𝑅 ∈ Ring ∧ ( 𝑖 𝑥 𝑗 ) ∈ ( Base ‘ 𝑅 ) ) → ( ( algSc ‘ 𝑃 ) ‘ ( 𝑖 𝑥 𝑗 ) ) ∈ ( Base ‘ 𝑃 ) )
27 19 24 26 syl2anc ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑥𝐵𝑦𝐵 ) ) ∧ 𝑖𝑁𝑗𝑁 ) → ( ( algSc ‘ 𝑃 ) ‘ ( 𝑖 𝑥 𝑗 ) ) ∈ ( Base ‘ 𝑃 ) )
28 5 14 6 16 18 27 matbas2d ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑥𝐵𝑦𝐵 ) ) → ( 𝑖𝑁 , 𝑗𝑁 ↦ ( ( algSc ‘ 𝑃 ) ‘ ( 𝑖 𝑥 𝑗 ) ) ) ∈ 𝐻 )
29 simp1rr ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑥𝐵𝑦𝐵 ) ) ∧ 𝑖𝑁𝑗𝑁 ) → 𝑦𝐵 )
30 2 20 3 21 22 29 matecld ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑥𝐵𝑦𝐵 ) ) ∧ 𝑖𝑁𝑗𝑁 ) → ( 𝑖 𝑦 𝑗 ) ∈ ( Base ‘ 𝑅 ) )
31 4 25 20 14 ply1sclcl ( ( 𝑅 ∈ Ring ∧ ( 𝑖 𝑦 𝑗 ) ∈ ( Base ‘ 𝑅 ) ) → ( ( algSc ‘ 𝑃 ) ‘ ( 𝑖 𝑦 𝑗 ) ) ∈ ( Base ‘ 𝑃 ) )
32 19 30 31 syl2anc ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑥𝐵𝑦𝐵 ) ) ∧ 𝑖𝑁𝑗𝑁 ) → ( ( algSc ‘ 𝑃 ) ‘ ( 𝑖 𝑦 𝑗 ) ) ∈ ( Base ‘ 𝑃 ) )
33 5 14 6 16 18 32 matbas2d ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑥𝐵𝑦𝐵 ) ) → ( 𝑖𝑁 , 𝑗𝑁 ↦ ( ( algSc ‘ 𝑃 ) ‘ ( 𝑖 𝑦 𝑗 ) ) ) ∈ 𝐻 )
34 eqid ( +g𝑃 ) = ( +g𝑃 )
35 5 6 8 34 matplusg2 ( ( ( 𝑖𝑁 , 𝑗𝑁 ↦ ( ( algSc ‘ 𝑃 ) ‘ ( 𝑖 𝑥 𝑗 ) ) ) ∈ 𝐻 ∧ ( 𝑖𝑁 , 𝑗𝑁 ↦ ( ( algSc ‘ 𝑃 ) ‘ ( 𝑖 𝑦 𝑗 ) ) ) ∈ 𝐻 ) → ( ( 𝑖𝑁 , 𝑗𝑁 ↦ ( ( algSc ‘ 𝑃 ) ‘ ( 𝑖 𝑥 𝑗 ) ) ) ( +g𝐶 ) ( 𝑖𝑁 , 𝑗𝑁 ↦ ( ( algSc ‘ 𝑃 ) ‘ ( 𝑖 𝑦 𝑗 ) ) ) ) = ( ( 𝑖𝑁 , 𝑗𝑁 ↦ ( ( algSc ‘ 𝑃 ) ‘ ( 𝑖 𝑥 𝑗 ) ) ) ∘f ( +g𝑃 ) ( 𝑖𝑁 , 𝑗𝑁 ↦ ( ( algSc ‘ 𝑃 ) ‘ ( 𝑖 𝑦 𝑗 ) ) ) ) )
36 28 33 35 syl2anc ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑥𝐵𝑦𝐵 ) ) → ( ( 𝑖𝑁 , 𝑗𝑁 ↦ ( ( algSc ‘ 𝑃 ) ‘ ( 𝑖 𝑥 𝑗 ) ) ) ( +g𝐶 ) ( 𝑖𝑁 , 𝑗𝑁 ↦ ( ( algSc ‘ 𝑃 ) ‘ ( 𝑖 𝑦 𝑗 ) ) ) ) = ( ( 𝑖𝑁 , 𝑗𝑁 ↦ ( ( algSc ‘ 𝑃 ) ‘ ( 𝑖 𝑥 𝑗 ) ) ) ∘f ( +g𝑃 ) ( 𝑖𝑁 , 𝑗𝑁 ↦ ( ( algSc ‘ 𝑃 ) ‘ ( 𝑖 𝑦 𝑗 ) ) ) ) )
37 fvexd ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑥𝐵𝑦𝐵 ) ) ∧ 𝑖𝑁𝑗𝑁 ) → ( ( algSc ‘ 𝑃 ) ‘ ( 𝑖 𝑥 𝑗 ) ) ∈ V )
38 fvexd ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑥𝐵𝑦𝐵 ) ) ∧ 𝑖𝑁𝑗𝑁 ) → ( ( algSc ‘ 𝑃 ) ‘ ( 𝑖 𝑦 𝑗 ) ) ∈ V )
39 eqidd ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑥𝐵𝑦𝐵 ) ) → ( 𝑖𝑁 , 𝑗𝑁 ↦ ( ( algSc ‘ 𝑃 ) ‘ ( 𝑖 𝑥 𝑗 ) ) ) = ( 𝑖𝑁 , 𝑗𝑁 ↦ ( ( algSc ‘ 𝑃 ) ‘ ( 𝑖 𝑥 𝑗 ) ) ) )
40 eqidd ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑥𝐵𝑦𝐵 ) ) → ( 𝑖𝑁 , 𝑗𝑁 ↦ ( ( algSc ‘ 𝑃 ) ‘ ( 𝑖 𝑦 𝑗 ) ) ) = ( 𝑖𝑁 , 𝑗𝑁 ↦ ( ( algSc ‘ 𝑃 ) ‘ ( 𝑖 𝑦 𝑗 ) ) ) )
41 16 16 37 38 39 40 offval22 ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑥𝐵𝑦𝐵 ) ) → ( ( 𝑖𝑁 , 𝑗𝑁 ↦ ( ( algSc ‘ 𝑃 ) ‘ ( 𝑖 𝑥 𝑗 ) ) ) ∘f ( +g𝑃 ) ( 𝑖𝑁 , 𝑗𝑁 ↦ ( ( algSc ‘ 𝑃 ) ‘ ( 𝑖 𝑦 𝑗 ) ) ) ) = ( 𝑖𝑁 , 𝑗𝑁 ↦ ( ( ( algSc ‘ 𝑃 ) ‘ ( 𝑖 𝑥 𝑗 ) ) ( +g𝑃 ) ( ( algSc ‘ 𝑃 ) ‘ ( 𝑖 𝑦 𝑗 ) ) ) ) )
42 simpr ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑥𝐵𝑦𝐵 ) ) → ( 𝑥𝐵𝑦𝐵 ) )
43 42 3ad2ant1 ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑥𝐵𝑦𝐵 ) ) ∧ 𝑖𝑁𝑗𝑁 ) → ( 𝑥𝐵𝑦𝐵 ) )
44 3simpc ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑥𝐵𝑦𝐵 ) ) ∧ 𝑖𝑁𝑗𝑁 ) → ( 𝑖𝑁𝑗𝑁 ) )
45 eqid ( +g𝑅 ) = ( +g𝑅 )
46 2 3 7 45 matplusgcell ( ( ( 𝑥𝐵𝑦𝐵 ) ∧ ( 𝑖𝑁𝑗𝑁 ) ) → ( 𝑖 ( 𝑥 ( +g𝐴 ) 𝑦 ) 𝑗 ) = ( ( 𝑖 𝑥 𝑗 ) ( +g𝑅 ) ( 𝑖 𝑦 𝑗 ) ) )
47 43 44 46 syl2anc ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑥𝐵𝑦𝐵 ) ) ∧ 𝑖𝑁𝑗𝑁 ) → ( 𝑖 ( 𝑥 ( +g𝐴 ) 𝑦 ) 𝑗 ) = ( ( 𝑖 𝑥 𝑗 ) ( +g𝑅 ) ( 𝑖 𝑦 𝑗 ) ) )
48 4 ply1sca ( 𝑅 ∈ Ring → 𝑅 = ( Scalar ‘ 𝑃 ) )
49 48 adantl ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → 𝑅 = ( Scalar ‘ 𝑃 ) )
50 49 fveq2d ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → ( +g𝑅 ) = ( +g ‘ ( Scalar ‘ 𝑃 ) ) )
51 50 oveqd ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → ( ( 𝑖 𝑥 𝑗 ) ( +g𝑅 ) ( 𝑖 𝑦 𝑗 ) ) = ( ( 𝑖 𝑥 𝑗 ) ( +g ‘ ( Scalar ‘ 𝑃 ) ) ( 𝑖 𝑦 𝑗 ) ) )
52 51 adantr ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑥𝐵𝑦𝐵 ) ) → ( ( 𝑖 𝑥 𝑗 ) ( +g𝑅 ) ( 𝑖 𝑦 𝑗 ) ) = ( ( 𝑖 𝑥 𝑗 ) ( +g ‘ ( Scalar ‘ 𝑃 ) ) ( 𝑖 𝑦 𝑗 ) ) )
53 52 3ad2ant1 ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑥𝐵𝑦𝐵 ) ) ∧ 𝑖𝑁𝑗𝑁 ) → ( ( 𝑖 𝑥 𝑗 ) ( +g𝑅 ) ( 𝑖 𝑦 𝑗 ) ) = ( ( 𝑖 𝑥 𝑗 ) ( +g ‘ ( Scalar ‘ 𝑃 ) ) ( 𝑖 𝑦 𝑗 ) ) )
54 47 53 eqtrd ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑥𝐵𝑦𝐵 ) ) ∧ 𝑖𝑁𝑗𝑁 ) → ( 𝑖 ( 𝑥 ( +g𝐴 ) 𝑦 ) 𝑗 ) = ( ( 𝑖 𝑥 𝑗 ) ( +g ‘ ( Scalar ‘ 𝑃 ) ) ( 𝑖 𝑦 𝑗 ) ) )
55 54 fveq2d ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑥𝐵𝑦𝐵 ) ) ∧ 𝑖𝑁𝑗𝑁 ) → ( ( algSc ‘ 𝑃 ) ‘ ( 𝑖 ( 𝑥 ( +g𝐴 ) 𝑦 ) 𝑗 ) ) = ( ( algSc ‘ 𝑃 ) ‘ ( ( 𝑖 𝑥 𝑗 ) ( +g ‘ ( Scalar ‘ 𝑃 ) ) ( 𝑖 𝑦 𝑗 ) ) ) )
56 eqid ( Scalar ‘ 𝑃 ) = ( Scalar ‘ 𝑃 )
57 18 3ad2ant1 ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑥𝐵𝑦𝐵 ) ) ∧ 𝑖𝑁𝑗𝑁 ) → 𝑃 ∈ Ring )
58 4 ply1lmod ( 𝑅 ∈ Ring → 𝑃 ∈ LMod )
59 58 ad2antlr ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑥𝐵𝑦𝐵 ) ) → 𝑃 ∈ LMod )
60 59 3ad2ant1 ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑥𝐵𝑦𝐵 ) ) ∧ 𝑖𝑁𝑗𝑁 ) → 𝑃 ∈ LMod )
61 25 56 57 60 asclghm ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑥𝐵𝑦𝐵 ) ) ∧ 𝑖𝑁𝑗𝑁 ) → ( algSc ‘ 𝑃 ) ∈ ( ( Scalar ‘ 𝑃 ) GrpHom 𝑃 ) )
62 49 eqcomd ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → ( Scalar ‘ 𝑃 ) = 𝑅 )
63 62 fveq2d ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → ( Base ‘ ( Scalar ‘ 𝑃 ) ) = ( Base ‘ 𝑅 ) )
64 63 eleq2d ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → ( ( 𝑖 𝑥 𝑗 ) ∈ ( Base ‘ ( Scalar ‘ 𝑃 ) ) ↔ ( 𝑖 𝑥 𝑗 ) ∈ ( Base ‘ 𝑅 ) ) )
65 64 adantr ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑥𝐵𝑦𝐵 ) ) → ( ( 𝑖 𝑥 𝑗 ) ∈ ( Base ‘ ( Scalar ‘ 𝑃 ) ) ↔ ( 𝑖 𝑥 𝑗 ) ∈ ( Base ‘ 𝑅 ) ) )
66 65 3ad2ant1 ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑥𝐵𝑦𝐵 ) ) ∧ 𝑖𝑁𝑗𝑁 ) → ( ( 𝑖 𝑥 𝑗 ) ∈ ( Base ‘ ( Scalar ‘ 𝑃 ) ) ↔ ( 𝑖 𝑥 𝑗 ) ∈ ( Base ‘ 𝑅 ) ) )
67 24 66 mpbird ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑥𝐵𝑦𝐵 ) ) ∧ 𝑖𝑁𝑗𝑁 ) → ( 𝑖 𝑥 𝑗 ) ∈ ( Base ‘ ( Scalar ‘ 𝑃 ) ) )
68 63 eleq2d ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → ( ( 𝑖 𝑦 𝑗 ) ∈ ( Base ‘ ( Scalar ‘ 𝑃 ) ) ↔ ( 𝑖 𝑦 𝑗 ) ∈ ( Base ‘ 𝑅 ) ) )
69 68 adantr ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑥𝐵𝑦𝐵 ) ) → ( ( 𝑖 𝑦 𝑗 ) ∈ ( Base ‘ ( Scalar ‘ 𝑃 ) ) ↔ ( 𝑖 𝑦 𝑗 ) ∈ ( Base ‘ 𝑅 ) ) )
70 69 3ad2ant1 ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑥𝐵𝑦𝐵 ) ) ∧ 𝑖𝑁𝑗𝑁 ) → ( ( 𝑖 𝑦 𝑗 ) ∈ ( Base ‘ ( Scalar ‘ 𝑃 ) ) ↔ ( 𝑖 𝑦 𝑗 ) ∈ ( Base ‘ 𝑅 ) ) )
71 30 70 mpbird ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑥𝐵𝑦𝐵 ) ) ∧ 𝑖𝑁𝑗𝑁 ) → ( 𝑖 𝑦 𝑗 ) ∈ ( Base ‘ ( Scalar ‘ 𝑃 ) ) )
72 eqid ( Base ‘ ( Scalar ‘ 𝑃 ) ) = ( Base ‘ ( Scalar ‘ 𝑃 ) )
73 eqid ( +g ‘ ( Scalar ‘ 𝑃 ) ) = ( +g ‘ ( Scalar ‘ 𝑃 ) )
74 72 73 34 ghmlin ( ( ( algSc ‘ 𝑃 ) ∈ ( ( Scalar ‘ 𝑃 ) GrpHom 𝑃 ) ∧ ( 𝑖 𝑥 𝑗 ) ∈ ( Base ‘ ( Scalar ‘ 𝑃 ) ) ∧ ( 𝑖 𝑦 𝑗 ) ∈ ( Base ‘ ( Scalar ‘ 𝑃 ) ) ) → ( ( algSc ‘ 𝑃 ) ‘ ( ( 𝑖 𝑥 𝑗 ) ( +g ‘ ( Scalar ‘ 𝑃 ) ) ( 𝑖 𝑦 𝑗 ) ) ) = ( ( ( algSc ‘ 𝑃 ) ‘ ( 𝑖 𝑥 𝑗 ) ) ( +g𝑃 ) ( ( algSc ‘ 𝑃 ) ‘ ( 𝑖 𝑦 𝑗 ) ) ) )
75 61 67 71 74 syl3anc ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑥𝐵𝑦𝐵 ) ) ∧ 𝑖𝑁𝑗𝑁 ) → ( ( algSc ‘ 𝑃 ) ‘ ( ( 𝑖 𝑥 𝑗 ) ( +g ‘ ( Scalar ‘ 𝑃 ) ) ( 𝑖 𝑦 𝑗 ) ) ) = ( ( ( algSc ‘ 𝑃 ) ‘ ( 𝑖 𝑥 𝑗 ) ) ( +g𝑃 ) ( ( algSc ‘ 𝑃 ) ‘ ( 𝑖 𝑦 𝑗 ) ) ) )
76 55 75 eqtr2d ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑥𝐵𝑦𝐵 ) ) ∧ 𝑖𝑁𝑗𝑁 ) → ( ( ( algSc ‘ 𝑃 ) ‘ ( 𝑖 𝑥 𝑗 ) ) ( +g𝑃 ) ( ( algSc ‘ 𝑃 ) ‘ ( 𝑖 𝑦 𝑗 ) ) ) = ( ( algSc ‘ 𝑃 ) ‘ ( 𝑖 ( 𝑥 ( +g𝐴 ) 𝑦 ) 𝑗 ) ) )
77 76 mpoeq3dva ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑥𝐵𝑦𝐵 ) ) → ( 𝑖𝑁 , 𝑗𝑁 ↦ ( ( ( algSc ‘ 𝑃 ) ‘ ( 𝑖 𝑥 𝑗 ) ) ( +g𝑃 ) ( ( algSc ‘ 𝑃 ) ‘ ( 𝑖 𝑦 𝑗 ) ) ) ) = ( 𝑖𝑁 , 𝑗𝑁 ↦ ( ( algSc ‘ 𝑃 ) ‘ ( 𝑖 ( 𝑥 ( +g𝐴 ) 𝑦 ) 𝑗 ) ) ) )
78 41 77 eqtrd ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑥𝐵𝑦𝐵 ) ) → ( ( 𝑖𝑁 , 𝑗𝑁 ↦ ( ( algSc ‘ 𝑃 ) ‘ ( 𝑖 𝑥 𝑗 ) ) ) ∘f ( +g𝑃 ) ( 𝑖𝑁 , 𝑗𝑁 ↦ ( ( algSc ‘ 𝑃 ) ‘ ( 𝑖 𝑦 𝑗 ) ) ) ) = ( 𝑖𝑁 , 𝑗𝑁 ↦ ( ( algSc ‘ 𝑃 ) ‘ ( 𝑖 ( 𝑥 ( +g𝐴 ) 𝑦 ) 𝑗 ) ) ) )
79 36 78 eqtr2d ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑥𝐵𝑦𝐵 ) ) → ( 𝑖𝑁 , 𝑗𝑁 ↦ ( ( algSc ‘ 𝑃 ) ‘ ( 𝑖 ( 𝑥 ( +g𝐴 ) 𝑦 ) 𝑗 ) ) ) = ( ( 𝑖𝑁 , 𝑗𝑁 ↦ ( ( algSc ‘ 𝑃 ) ‘ ( 𝑖 𝑥 𝑗 ) ) ) ( +g𝐶 ) ( 𝑖𝑁 , 𝑗𝑁 ↦ ( ( algSc ‘ 𝑃 ) ‘ ( 𝑖 𝑦 𝑗 ) ) ) ) )
80 simpl ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑥𝐵𝑦𝐵 ) ) → ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) )
81 2 matring ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → 𝐴 ∈ Ring )
82 ringmnd ( 𝐴 ∈ Ring → 𝐴 ∈ Mnd )
83 81 82 syl ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → 𝐴 ∈ Mnd )
84 83 anim1i ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑥𝐵𝑦𝐵 ) ) → ( 𝐴 ∈ Mnd ∧ ( 𝑥𝐵𝑦𝐵 ) ) )
85 3anass ( ( 𝐴 ∈ Mnd ∧ 𝑥𝐵𝑦𝐵 ) ↔ ( 𝐴 ∈ Mnd ∧ ( 𝑥𝐵𝑦𝐵 ) ) )
86 84 85 sylibr ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑥𝐵𝑦𝐵 ) ) → ( 𝐴 ∈ Mnd ∧ 𝑥𝐵𝑦𝐵 ) )
87 3 7 mndcl ( ( 𝐴 ∈ Mnd ∧ 𝑥𝐵𝑦𝐵 ) → ( 𝑥 ( +g𝐴 ) 𝑦 ) ∈ 𝐵 )
88 86 87 syl ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑥𝐵𝑦𝐵 ) ) → ( 𝑥 ( +g𝐴 ) 𝑦 ) ∈ 𝐵 )
89 df-3an ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ ( 𝑥 ( +g𝐴 ) 𝑦 ) ∈ 𝐵 ) ↔ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑥 ( +g𝐴 ) 𝑦 ) ∈ 𝐵 ) )
90 80 88 89 sylanbrc ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑥𝐵𝑦𝐵 ) ) → ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ ( 𝑥 ( +g𝐴 ) 𝑦 ) ∈ 𝐵 ) )
91 1 2 3 4 25 mat2pmatval ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ ( 𝑥 ( +g𝐴 ) 𝑦 ) ∈ 𝐵 ) → ( 𝑇 ‘ ( 𝑥 ( +g𝐴 ) 𝑦 ) ) = ( 𝑖𝑁 , 𝑗𝑁 ↦ ( ( algSc ‘ 𝑃 ) ‘ ( 𝑖 ( 𝑥 ( +g𝐴 ) 𝑦 ) 𝑗 ) ) ) )
92 90 91 syl ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑥𝐵𝑦𝐵 ) ) → ( 𝑇 ‘ ( 𝑥 ( +g𝐴 ) 𝑦 ) ) = ( 𝑖𝑁 , 𝑗𝑁 ↦ ( ( algSc ‘ 𝑃 ) ‘ ( 𝑖 ( 𝑥 ( +g𝐴 ) 𝑦 ) 𝑗 ) ) ) )
93 simpl ( ( 𝑥𝐵𝑦𝐵 ) → 𝑥𝐵 )
94 93 anim2i ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑥𝐵𝑦𝐵 ) ) → ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ 𝑥𝐵 ) )
95 df-3an ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑥𝐵 ) ↔ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ 𝑥𝐵 ) )
96 94 95 sylibr ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑥𝐵𝑦𝐵 ) ) → ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑥𝐵 ) )
97 1 2 3 4 25 mat2pmatval ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑥𝐵 ) → ( 𝑇𝑥 ) = ( 𝑖𝑁 , 𝑗𝑁 ↦ ( ( algSc ‘ 𝑃 ) ‘ ( 𝑖 𝑥 𝑗 ) ) ) )
98 96 97 syl ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑥𝐵𝑦𝐵 ) ) → ( 𝑇𝑥 ) = ( 𝑖𝑁 , 𝑗𝑁 ↦ ( ( algSc ‘ 𝑃 ) ‘ ( 𝑖 𝑥 𝑗 ) ) ) )
99 simpr ( ( 𝑥𝐵𝑦𝐵 ) → 𝑦𝐵 )
100 99 anim2i ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑥𝐵𝑦𝐵 ) ) → ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ 𝑦𝐵 ) )
101 df-3an ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑦𝐵 ) ↔ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ 𝑦𝐵 ) )
102 100 101 sylibr ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑥𝐵𝑦𝐵 ) ) → ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑦𝐵 ) )
103 1 2 3 4 25 mat2pmatval ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑦𝐵 ) → ( 𝑇𝑦 ) = ( 𝑖𝑁 , 𝑗𝑁 ↦ ( ( algSc ‘ 𝑃 ) ‘ ( 𝑖 𝑦 𝑗 ) ) ) )
104 102 103 syl ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑥𝐵𝑦𝐵 ) ) → ( 𝑇𝑦 ) = ( 𝑖𝑁 , 𝑗𝑁 ↦ ( ( algSc ‘ 𝑃 ) ‘ ( 𝑖 𝑦 𝑗 ) ) ) )
105 98 104 oveq12d ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑥𝐵𝑦𝐵 ) ) → ( ( 𝑇𝑥 ) ( +g𝐶 ) ( 𝑇𝑦 ) ) = ( ( 𝑖𝑁 , 𝑗𝑁 ↦ ( ( algSc ‘ 𝑃 ) ‘ ( 𝑖 𝑥 𝑗 ) ) ) ( +g𝐶 ) ( 𝑖𝑁 , 𝑗𝑁 ↦ ( ( algSc ‘ 𝑃 ) ‘ ( 𝑖 𝑦 𝑗 ) ) ) ) )
106 79 92 105 3eqtr4d ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑥𝐵𝑦𝐵 ) ) → ( 𝑇 ‘ ( 𝑥 ( +g𝐴 ) 𝑦 ) ) = ( ( 𝑇𝑥 ) ( +g𝐶 ) ( 𝑇𝑦 ) ) )
107 3 6 7 8 9 12 13 106 isghmd ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → 𝑇 ∈ ( 𝐴 GrpHom 𝐶 ) )