# Metamath Proof Explorer

## Theorem pm2mpghm

Description: The transformation of polynomial matrices into polynomials over matrices is an additive group homomorphism. (Contributed by AV, 16-Oct-2019) (Revised by AV, 6-Dec-2019)

Ref Expression
Hypotheses pm2mpfo.p ${⊢}{P}={\mathrm{Poly}}_{1}\left({R}\right)$
pm2mpfo.c ${⊢}{C}={N}\mathrm{Mat}{P}$
pm2mpfo.b ${⊢}{B}={\mathrm{Base}}_{{C}}$
pm2mpfo.m
pm2mpfo.e
pm2mpfo.x ${⊢}{X}={\mathrm{var}}_{1}\left({A}\right)$
pm2mpfo.a ${⊢}{A}={N}\mathrm{Mat}{R}$
pm2mpfo.q ${⊢}{Q}={\mathrm{Poly}}_{1}\left({A}\right)$
pm2mpfo.l ${⊢}{L}={\mathrm{Base}}_{{Q}}$
pm2mpfo.t ${⊢}{T}={N}\mathrm{pMatToMatPoly}{R}$
Assertion pm2mpghm ${⊢}\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\to {T}\in \left({C}\mathrm{GrpHom}{Q}\right)$

### Proof

Step Hyp Ref Expression
1 pm2mpfo.p ${⊢}{P}={\mathrm{Poly}}_{1}\left({R}\right)$
2 pm2mpfo.c ${⊢}{C}={N}\mathrm{Mat}{P}$
3 pm2mpfo.b ${⊢}{B}={\mathrm{Base}}_{{C}}$
4 pm2mpfo.m
5 pm2mpfo.e
6 pm2mpfo.x ${⊢}{X}={\mathrm{var}}_{1}\left({A}\right)$
7 pm2mpfo.a ${⊢}{A}={N}\mathrm{Mat}{R}$
8 pm2mpfo.q ${⊢}{Q}={\mathrm{Poly}}_{1}\left({A}\right)$
9 pm2mpfo.l ${⊢}{L}={\mathrm{Base}}_{{Q}}$
10 pm2mpfo.t ${⊢}{T}={N}\mathrm{pMatToMatPoly}{R}$
11 eqid ${⊢}{+}_{{C}}={+}_{{C}}$
12 eqid ${⊢}{+}_{{Q}}={+}_{{Q}}$
13 1 2 pmatring ${⊢}\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\to {C}\in \mathrm{Ring}$
14 ringgrp ${⊢}{C}\in \mathrm{Ring}\to {C}\in \mathrm{Grp}$
15 13 14 syl ${⊢}\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\to {C}\in \mathrm{Grp}$
16 7 matring ${⊢}\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\to {A}\in \mathrm{Ring}$
17 8 ply1ring ${⊢}{A}\in \mathrm{Ring}\to {Q}\in \mathrm{Ring}$
18 16 17 syl ${⊢}\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\to {Q}\in \mathrm{Ring}$
19 ringgrp ${⊢}{Q}\in \mathrm{Ring}\to {Q}\in \mathrm{Grp}$
20 18 19 syl ${⊢}\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\to {Q}\in \mathrm{Grp}$
21 1 2 3 4 5 6 7 8 10 9 pm2mpf ${⊢}\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\to {T}:{B}⟶{L}$
22 ringmnd ${⊢}{C}\in \mathrm{Ring}\to {C}\in \mathrm{Mnd}$
23 13 22 syl ${⊢}\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\to {C}\in \mathrm{Mnd}$
24 23 anim1i ${⊢}\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\wedge \left({a}\in {B}\wedge {b}\in {B}\right)\right)\to \left({C}\in \mathrm{Mnd}\wedge \left({a}\in {B}\wedge {b}\in {B}\right)\right)$
25 3anass ${⊢}\left({C}\in \mathrm{Mnd}\wedge {a}\in {B}\wedge {b}\in {B}\right)↔\left({C}\in \mathrm{Mnd}\wedge \left({a}\in {B}\wedge {b}\in {B}\right)\right)$
26 24 25 sylibr ${⊢}\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\wedge \left({a}\in {B}\wedge {b}\in {B}\right)\right)\to \left({C}\in \mathrm{Mnd}\wedge {a}\in {B}\wedge {b}\in {B}\right)$
27 3 11 mndcl ${⊢}\left({C}\in \mathrm{Mnd}\wedge {a}\in {B}\wedge {b}\in {B}\right)\to {a}{+}_{{C}}{b}\in {B}$
28 26 27 syl ${⊢}\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\wedge \left({a}\in {B}\wedge {b}\in {B}\right)\right)\to {a}{+}_{{C}}{b}\in {B}$
29 2 3 decpmatval ${⊢}\left({a}{+}_{{C}}{b}\in {B}\wedge {k}\in {ℕ}_{0}\right)\to \left({a}{+}_{{C}}{b}\right)\mathrm{decompPMat}{k}=\left({i}\in {N},{j}\in {N}⟼{\mathrm{coe}}_{1}\left({i}\left({a}{+}_{{C}}{b}\right){j}\right)\left({k}\right)\right)$
30 28 29 sylan ${⊢}\left(\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\wedge \left({a}\in {B}\wedge {b}\in {B}\right)\right)\wedge {k}\in {ℕ}_{0}\right)\to \left({a}{+}_{{C}}{b}\right)\mathrm{decompPMat}{k}=\left({i}\in {N},{j}\in {N}⟼{\mathrm{coe}}_{1}\left({i}\left({a}{+}_{{C}}{b}\right){j}\right)\left({k}\right)\right)$
31 simplll ${⊢}\left(\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\wedge \left({a}\in {B}\wedge {b}\in {B}\right)\right)\wedge {k}\in {ℕ}_{0}\right)\to {N}\in \mathrm{Fin}$
32 fvexd ${⊢}\left(\left(\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\wedge \left({a}\in {B}\wedge {b}\in {B}\right)\right)\wedge {k}\in {ℕ}_{0}\right)\wedge {i}\in {N}\wedge {j}\in {N}\right)\to {\mathrm{coe}}_{1}\left({i}{a}{j}\right)\left({k}\right)\in \mathrm{V}$
33 fvexd ${⊢}\left(\left(\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\wedge \left({a}\in {B}\wedge {b}\in {B}\right)\right)\wedge {k}\in {ℕ}_{0}\right)\wedge {i}\in {N}\wedge {j}\in {N}\right)\to {\mathrm{coe}}_{1}\left({i}{b}{j}\right)\left({k}\right)\in \mathrm{V}$
34 eqidd ${⊢}\left(\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\wedge \left({a}\in {B}\wedge {b}\in {B}\right)\right)\wedge {k}\in {ℕ}_{0}\right)\to \left({i}\in {N},{j}\in {N}⟼{\mathrm{coe}}_{1}\left({i}{a}{j}\right)\left({k}\right)\right)=\left({i}\in {N},{j}\in {N}⟼{\mathrm{coe}}_{1}\left({i}{a}{j}\right)\left({k}\right)\right)$
35 eqidd ${⊢}\left(\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\wedge \left({a}\in {B}\wedge {b}\in {B}\right)\right)\wedge {k}\in {ℕ}_{0}\right)\to \left({i}\in {N},{j}\in {N}⟼{\mathrm{coe}}_{1}\left({i}{b}{j}\right)\left({k}\right)\right)=\left({i}\in {N},{j}\in {N}⟼{\mathrm{coe}}_{1}\left({i}{b}{j}\right)\left({k}\right)\right)$
36 31 31 32 33 34 35 offval22 ${⊢}\left(\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\wedge \left({a}\in {B}\wedge {b}\in {B}\right)\right)\wedge {k}\in {ℕ}_{0}\right)\to \left({i}\in {N},{j}\in {N}⟼{\mathrm{coe}}_{1}\left({i}{a}{j}\right)\left({k}\right)\right){{+}_{{R}}}_{f}\left({i}\in {N},{j}\in {N}⟼{\mathrm{coe}}_{1}\left({i}{b}{j}\right)\left({k}\right)\right)=\left({i}\in {N},{j}\in {N}⟼{\mathrm{coe}}_{1}\left({i}{a}{j}\right)\left({k}\right){+}_{{R}}{\mathrm{coe}}_{1}\left({i}{b}{j}\right)\left({k}\right)\right)$
37 eqid ${⊢}{\mathrm{Base}}_{{R}}={\mathrm{Base}}_{{R}}$
38 eqid ${⊢}{\mathrm{Base}}_{{A}}={\mathrm{Base}}_{{A}}$
39 simpllr ${⊢}\left(\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\wedge \left({a}\in {B}\wedge {b}\in {B}\right)\right)\wedge {k}\in {ℕ}_{0}\right)\to {R}\in \mathrm{Ring}$
40 simprl ${⊢}\left(\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\wedge {a}\in {B}\right)\wedge \left({i}\in {N}\wedge {j}\in {N}\right)\right)\to {i}\in {N}$
41 simprr ${⊢}\left(\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\wedge {a}\in {B}\right)\wedge \left({i}\in {N}\wedge {j}\in {N}\right)\right)\to {j}\in {N}$
42 3 eleq2i ${⊢}{a}\in {B}↔{a}\in {\mathrm{Base}}_{{C}}$
43 42 biimpi ${⊢}{a}\in {B}\to {a}\in {\mathrm{Base}}_{{C}}$
44 43 ad2antlr ${⊢}\left(\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\wedge {a}\in {B}\right)\wedge \left({i}\in {N}\wedge {j}\in {N}\right)\right)\to {a}\in {\mathrm{Base}}_{{C}}$
45 eqid ${⊢}{\mathrm{Base}}_{{P}}={\mathrm{Base}}_{{P}}$
46 2 45 matecl ${⊢}\left({i}\in {N}\wedge {j}\in {N}\wedge {a}\in {\mathrm{Base}}_{{C}}\right)\to {i}{a}{j}\in {\mathrm{Base}}_{{P}}$
47 40 41 44 46 syl3anc ${⊢}\left(\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\wedge {a}\in {B}\right)\wedge \left({i}\in {N}\wedge {j}\in {N}\right)\right)\to {i}{a}{j}\in {\mathrm{Base}}_{{P}}$
48 47 ex ${⊢}\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\wedge {a}\in {B}\right)\to \left(\left({i}\in {N}\wedge {j}\in {N}\right)\to {i}{a}{j}\in {\mathrm{Base}}_{{P}}\right)$
49 48 adantrr ${⊢}\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\wedge \left({a}\in {B}\wedge {b}\in {B}\right)\right)\to \left(\left({i}\in {N}\wedge {j}\in {N}\right)\to {i}{a}{j}\in {\mathrm{Base}}_{{P}}\right)$
50 49 adantr ${⊢}\left(\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\wedge \left({a}\in {B}\wedge {b}\in {B}\right)\right)\wedge {k}\in {ℕ}_{0}\right)\to \left(\left({i}\in {N}\wedge {j}\in {N}\right)\to {i}{a}{j}\in {\mathrm{Base}}_{{P}}\right)$
51 50 3impib ${⊢}\left(\left(\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\wedge \left({a}\in {B}\wedge {b}\in {B}\right)\right)\wedge {k}\in {ℕ}_{0}\right)\wedge {i}\in {N}\wedge {j}\in {N}\right)\to {i}{a}{j}\in {\mathrm{Base}}_{{P}}$
52 simpr ${⊢}\left(\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\wedge \left({a}\in {B}\wedge {b}\in {B}\right)\right)\wedge {k}\in {ℕ}_{0}\right)\to {k}\in {ℕ}_{0}$
53 52 3ad2ant1 ${⊢}\left(\left(\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\wedge \left({a}\in {B}\wedge {b}\in {B}\right)\right)\wedge {k}\in {ℕ}_{0}\right)\wedge {i}\in {N}\wedge {j}\in {N}\right)\to {k}\in {ℕ}_{0}$
54 eqid ${⊢}{\mathrm{coe}}_{1}\left({i}{a}{j}\right)={\mathrm{coe}}_{1}\left({i}{a}{j}\right)$
55 54 45 1 37 coe1fvalcl ${⊢}\left({i}{a}{j}\in {\mathrm{Base}}_{{P}}\wedge {k}\in {ℕ}_{0}\right)\to {\mathrm{coe}}_{1}\left({i}{a}{j}\right)\left({k}\right)\in {\mathrm{Base}}_{{R}}$
56 51 53 55 syl2anc ${⊢}\left(\left(\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\wedge \left({a}\in {B}\wedge {b}\in {B}\right)\right)\wedge {k}\in {ℕ}_{0}\right)\wedge {i}\in {N}\wedge {j}\in {N}\right)\to {\mathrm{coe}}_{1}\left({i}{a}{j}\right)\left({k}\right)\in {\mathrm{Base}}_{{R}}$
57 7 37 38 31 39 56 matbas2d ${⊢}\left(\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\wedge \left({a}\in {B}\wedge {b}\in {B}\right)\right)\wedge {k}\in {ℕ}_{0}\right)\to \left({i}\in {N},{j}\in {N}⟼{\mathrm{coe}}_{1}\left({i}{a}{j}\right)\left({k}\right)\right)\in {\mathrm{Base}}_{{A}}$
58 simprl ${⊢}\left(\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\wedge {b}\in {B}\right)\wedge \left({i}\in {N}\wedge {j}\in {N}\right)\right)\to {i}\in {N}$
59 simprr ${⊢}\left(\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\wedge {b}\in {B}\right)\wedge \left({i}\in {N}\wedge {j}\in {N}\right)\right)\to {j}\in {N}$
60 3 eleq2i ${⊢}{b}\in {B}↔{b}\in {\mathrm{Base}}_{{C}}$
61 60 biimpi ${⊢}{b}\in {B}\to {b}\in {\mathrm{Base}}_{{C}}$
62 61 ad2antlr ${⊢}\left(\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\wedge {b}\in {B}\right)\wedge \left({i}\in {N}\wedge {j}\in {N}\right)\right)\to {b}\in {\mathrm{Base}}_{{C}}$
63 2 45 matecl ${⊢}\left({i}\in {N}\wedge {j}\in {N}\wedge {b}\in {\mathrm{Base}}_{{C}}\right)\to {i}{b}{j}\in {\mathrm{Base}}_{{P}}$
64 58 59 62 63 syl3anc ${⊢}\left(\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\wedge {b}\in {B}\right)\wedge \left({i}\in {N}\wedge {j}\in {N}\right)\right)\to {i}{b}{j}\in {\mathrm{Base}}_{{P}}$
65 64 ex ${⊢}\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\wedge {b}\in {B}\right)\to \left(\left({i}\in {N}\wedge {j}\in {N}\right)\to {i}{b}{j}\in {\mathrm{Base}}_{{P}}\right)$
66 65 adantrl ${⊢}\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\wedge \left({a}\in {B}\wedge {b}\in {B}\right)\right)\to \left(\left({i}\in {N}\wedge {j}\in {N}\right)\to {i}{b}{j}\in {\mathrm{Base}}_{{P}}\right)$
67 66 adantr ${⊢}\left(\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\wedge \left({a}\in {B}\wedge {b}\in {B}\right)\right)\wedge {k}\in {ℕ}_{0}\right)\to \left(\left({i}\in {N}\wedge {j}\in {N}\right)\to {i}{b}{j}\in {\mathrm{Base}}_{{P}}\right)$
68 67 3impib ${⊢}\left(\left(\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\wedge \left({a}\in {B}\wedge {b}\in {B}\right)\right)\wedge {k}\in {ℕ}_{0}\right)\wedge {i}\in {N}\wedge {j}\in {N}\right)\to {i}{b}{j}\in {\mathrm{Base}}_{{P}}$
69 eqid ${⊢}{\mathrm{coe}}_{1}\left({i}{b}{j}\right)={\mathrm{coe}}_{1}\left({i}{b}{j}\right)$
70 69 45 1 37 coe1fvalcl ${⊢}\left({i}{b}{j}\in {\mathrm{Base}}_{{P}}\wedge {k}\in {ℕ}_{0}\right)\to {\mathrm{coe}}_{1}\left({i}{b}{j}\right)\left({k}\right)\in {\mathrm{Base}}_{{R}}$
71 68 53 70 syl2anc ${⊢}\left(\left(\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\wedge \left({a}\in {B}\wedge {b}\in {B}\right)\right)\wedge {k}\in {ℕ}_{0}\right)\wedge {i}\in {N}\wedge {j}\in {N}\right)\to {\mathrm{coe}}_{1}\left({i}{b}{j}\right)\left({k}\right)\in {\mathrm{Base}}_{{R}}$
72 7 37 38 31 39 71 matbas2d ${⊢}\left(\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\wedge \left({a}\in {B}\wedge {b}\in {B}\right)\right)\wedge {k}\in {ℕ}_{0}\right)\to \left({i}\in {N},{j}\in {N}⟼{\mathrm{coe}}_{1}\left({i}{b}{j}\right)\left({k}\right)\right)\in {\mathrm{Base}}_{{A}}$
73 eqid ${⊢}{+}_{{A}}={+}_{{A}}$
74 eqid ${⊢}{+}_{{R}}={+}_{{R}}$
75 7 38 73 74 matplusg2 ${⊢}\left(\left({i}\in {N},{j}\in {N}⟼{\mathrm{coe}}_{1}\left({i}{a}{j}\right)\left({k}\right)\right)\in {\mathrm{Base}}_{{A}}\wedge \left({i}\in {N},{j}\in {N}⟼{\mathrm{coe}}_{1}\left({i}{b}{j}\right)\left({k}\right)\right)\in {\mathrm{Base}}_{{A}}\right)\to \left({i}\in {N},{j}\in {N}⟼{\mathrm{coe}}_{1}\left({i}{a}{j}\right)\left({k}\right)\right){+}_{{A}}\left({i}\in {N},{j}\in {N}⟼{\mathrm{coe}}_{1}\left({i}{b}{j}\right)\left({k}\right)\right)=\left({i}\in {N},{j}\in {N}⟼{\mathrm{coe}}_{1}\left({i}{a}{j}\right)\left({k}\right)\right){{+}_{{R}}}_{f}\left({i}\in {N},{j}\in {N}⟼{\mathrm{coe}}_{1}\left({i}{b}{j}\right)\left({k}\right)\right)$
76 57 72 75 syl2anc ${⊢}\left(\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\wedge \left({a}\in {B}\wedge {b}\in {B}\right)\right)\wedge {k}\in {ℕ}_{0}\right)\to \left({i}\in {N},{j}\in {N}⟼{\mathrm{coe}}_{1}\left({i}{a}{j}\right)\left({k}\right)\right){+}_{{A}}\left({i}\in {N},{j}\in {N}⟼{\mathrm{coe}}_{1}\left({i}{b}{j}\right)\left({k}\right)\right)=\left({i}\in {N},{j}\in {N}⟼{\mathrm{coe}}_{1}\left({i}{a}{j}\right)\left({k}\right)\right){{+}_{{R}}}_{f}\left({i}\in {N},{j}\in {N}⟼{\mathrm{coe}}_{1}\left({i}{b}{j}\right)\left({k}\right)\right)$
77 simplr ${⊢}\left(\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\wedge \left({a}\in {B}\wedge {b}\in {B}\right)\right)\wedge {k}\in {ℕ}_{0}\right)\to \left({a}\in {B}\wedge {b}\in {B}\right)$
78 77 anim1i ${⊢}\left(\left(\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\wedge \left({a}\in {B}\wedge {b}\in {B}\right)\right)\wedge {k}\in {ℕ}_{0}\right)\wedge \left({i}\in {N}\wedge {j}\in {N}\right)\right)\to \left(\left({a}\in {B}\wedge {b}\in {B}\right)\wedge \left({i}\in {N}\wedge {j}\in {N}\right)\right)$
79 78 3impb ${⊢}\left(\left(\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\wedge \left({a}\in {B}\wedge {b}\in {B}\right)\right)\wedge {k}\in {ℕ}_{0}\right)\wedge {i}\in {N}\wedge {j}\in {N}\right)\to \left(\left({a}\in {B}\wedge {b}\in {B}\right)\wedge \left({i}\in {N}\wedge {j}\in {N}\right)\right)$
80 eqid ${⊢}{+}_{{P}}={+}_{{P}}$
81 2 3 11 80 matplusgcell ${⊢}\left(\left({a}\in {B}\wedge {b}\in {B}\right)\wedge \left({i}\in {N}\wedge {j}\in {N}\right)\right)\to {i}\left({a}{+}_{{C}}{b}\right){j}=\left({i}{a}{j}\right){+}_{{P}}\left({i}{b}{j}\right)$
82 79 81 syl ${⊢}\left(\left(\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\wedge \left({a}\in {B}\wedge {b}\in {B}\right)\right)\wedge {k}\in {ℕ}_{0}\right)\wedge {i}\in {N}\wedge {j}\in {N}\right)\to {i}\left({a}{+}_{{C}}{b}\right){j}=\left({i}{a}{j}\right){+}_{{P}}\left({i}{b}{j}\right)$
83 82 fveq2d ${⊢}\left(\left(\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\wedge \left({a}\in {B}\wedge {b}\in {B}\right)\right)\wedge {k}\in {ℕ}_{0}\right)\wedge {i}\in {N}\wedge {j}\in {N}\right)\to {\mathrm{coe}}_{1}\left({i}\left({a}{+}_{{C}}{b}\right){j}\right)={\mathrm{coe}}_{1}\left(\left({i}{a}{j}\right){+}_{{P}}\left({i}{b}{j}\right)\right)$
84 83 fveq1d ${⊢}\left(\left(\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\wedge \left({a}\in {B}\wedge {b}\in {B}\right)\right)\wedge {k}\in {ℕ}_{0}\right)\wedge {i}\in {N}\wedge {j}\in {N}\right)\to {\mathrm{coe}}_{1}\left({i}\left({a}{+}_{{C}}{b}\right){j}\right)\left({k}\right)={\mathrm{coe}}_{1}\left(\left({i}{a}{j}\right){+}_{{P}}\left({i}{b}{j}\right)\right)\left({k}\right)$
85 39 3ad2ant1 ${⊢}\left(\left(\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\wedge \left({a}\in {B}\wedge {b}\in {B}\right)\right)\wedge {k}\in {ℕ}_{0}\right)\wedge {i}\in {N}\wedge {j}\in {N}\right)\to {R}\in \mathrm{Ring}$
86 1 45 80 74 coe1addfv ${⊢}\left(\left({R}\in \mathrm{Ring}\wedge {i}{a}{j}\in {\mathrm{Base}}_{{P}}\wedge {i}{b}{j}\in {\mathrm{Base}}_{{P}}\right)\wedge {k}\in {ℕ}_{0}\right)\to {\mathrm{coe}}_{1}\left(\left({i}{a}{j}\right){+}_{{P}}\left({i}{b}{j}\right)\right)\left({k}\right)={\mathrm{coe}}_{1}\left({i}{a}{j}\right)\left({k}\right){+}_{{R}}{\mathrm{coe}}_{1}\left({i}{b}{j}\right)\left({k}\right)$
87 85 51 68 53 86 syl31anc ${⊢}\left(\left(\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\wedge \left({a}\in {B}\wedge {b}\in {B}\right)\right)\wedge {k}\in {ℕ}_{0}\right)\wedge {i}\in {N}\wedge {j}\in {N}\right)\to {\mathrm{coe}}_{1}\left(\left({i}{a}{j}\right){+}_{{P}}\left({i}{b}{j}\right)\right)\left({k}\right)={\mathrm{coe}}_{1}\left({i}{a}{j}\right)\left({k}\right){+}_{{R}}{\mathrm{coe}}_{1}\left({i}{b}{j}\right)\left({k}\right)$
88 84 87 eqtrd ${⊢}\left(\left(\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\wedge \left({a}\in {B}\wedge {b}\in {B}\right)\right)\wedge {k}\in {ℕ}_{0}\right)\wedge {i}\in {N}\wedge {j}\in {N}\right)\to {\mathrm{coe}}_{1}\left({i}\left({a}{+}_{{C}}{b}\right){j}\right)\left({k}\right)={\mathrm{coe}}_{1}\left({i}{a}{j}\right)\left({k}\right){+}_{{R}}{\mathrm{coe}}_{1}\left({i}{b}{j}\right)\left({k}\right)$
89 88 mpoeq3dva ${⊢}\left(\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\wedge \left({a}\in {B}\wedge {b}\in {B}\right)\right)\wedge {k}\in {ℕ}_{0}\right)\to \left({i}\in {N},{j}\in {N}⟼{\mathrm{coe}}_{1}\left({i}\left({a}{+}_{{C}}{b}\right){j}\right)\left({k}\right)\right)=\left({i}\in {N},{j}\in {N}⟼{\mathrm{coe}}_{1}\left({i}{a}{j}\right)\left({k}\right){+}_{{R}}{\mathrm{coe}}_{1}\left({i}{b}{j}\right)\left({k}\right)\right)$
90 36 76 89 3eqtr4rd ${⊢}\left(\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\wedge \left({a}\in {B}\wedge {b}\in {B}\right)\right)\wedge {k}\in {ℕ}_{0}\right)\to \left({i}\in {N},{j}\in {N}⟼{\mathrm{coe}}_{1}\left({i}\left({a}{+}_{{C}}{b}\right){j}\right)\left({k}\right)\right)=\left({i}\in {N},{j}\in {N}⟼{\mathrm{coe}}_{1}\left({i}{a}{j}\right)\left({k}\right)\right){+}_{{A}}\left({i}\in {N},{j}\in {N}⟼{\mathrm{coe}}_{1}\left({i}{b}{j}\right)\left({k}\right)\right)$
91 8 ply1sca ${⊢}{A}\in \mathrm{Ring}\to {A}=\mathrm{Scalar}\left({Q}\right)$
92 16 91 syl ${⊢}\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\to {A}=\mathrm{Scalar}\left({Q}\right)$
93 92 ad2antrr ${⊢}\left(\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\wedge \left({a}\in {B}\wedge {b}\in {B}\right)\right)\wedge {k}\in {ℕ}_{0}\right)\to {A}=\mathrm{Scalar}\left({Q}\right)$
94 93 fveq2d ${⊢}\left(\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\wedge \left({a}\in {B}\wedge {b}\in {B}\right)\right)\wedge {k}\in {ℕ}_{0}\right)\to {+}_{{A}}={+}_{\mathrm{Scalar}\left({Q}\right)}$
95 simprl ${⊢}\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\wedge \left({a}\in {B}\wedge {b}\in {B}\right)\right)\to {a}\in {B}$
96 2 3 decpmatval ${⊢}\left({a}\in {B}\wedge {k}\in {ℕ}_{0}\right)\to {a}\mathrm{decompPMat}{k}=\left({i}\in {N},{j}\in {N}⟼{\mathrm{coe}}_{1}\left({i}{a}{j}\right)\left({k}\right)\right)$
97 95 96 sylan ${⊢}\left(\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\wedge \left({a}\in {B}\wedge {b}\in {B}\right)\right)\wedge {k}\in {ℕ}_{0}\right)\to {a}\mathrm{decompPMat}{k}=\left({i}\in {N},{j}\in {N}⟼{\mathrm{coe}}_{1}\left({i}{a}{j}\right)\left({k}\right)\right)$
98 97 eqcomd ${⊢}\left(\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\wedge \left({a}\in {B}\wedge {b}\in {B}\right)\right)\wedge {k}\in {ℕ}_{0}\right)\to \left({i}\in {N},{j}\in {N}⟼{\mathrm{coe}}_{1}\left({i}{a}{j}\right)\left({k}\right)\right)={a}\mathrm{decompPMat}{k}$
99 simprr ${⊢}\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\wedge \left({a}\in {B}\wedge {b}\in {B}\right)\right)\to {b}\in {B}$
100 2 3 decpmatval ${⊢}\left({b}\in {B}\wedge {k}\in {ℕ}_{0}\right)\to {b}\mathrm{decompPMat}{k}=\left({i}\in {N},{j}\in {N}⟼{\mathrm{coe}}_{1}\left({i}{b}{j}\right)\left({k}\right)\right)$
101 99 100 sylan ${⊢}\left(\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\wedge \left({a}\in {B}\wedge {b}\in {B}\right)\right)\wedge {k}\in {ℕ}_{0}\right)\to {b}\mathrm{decompPMat}{k}=\left({i}\in {N},{j}\in {N}⟼{\mathrm{coe}}_{1}\left({i}{b}{j}\right)\left({k}\right)\right)$
102 101 eqcomd ${⊢}\left(\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\wedge \left({a}\in {B}\wedge {b}\in {B}\right)\right)\wedge {k}\in {ℕ}_{0}\right)\to \left({i}\in {N},{j}\in {N}⟼{\mathrm{coe}}_{1}\left({i}{b}{j}\right)\left({k}\right)\right)={b}\mathrm{decompPMat}{k}$
103 94 98 102 oveq123d ${⊢}\left(\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\wedge \left({a}\in {B}\wedge {b}\in {B}\right)\right)\wedge {k}\in {ℕ}_{0}\right)\to \left({i}\in {N},{j}\in {N}⟼{\mathrm{coe}}_{1}\left({i}{a}{j}\right)\left({k}\right)\right){+}_{{A}}\left({i}\in {N},{j}\in {N}⟼{\mathrm{coe}}_{1}\left({i}{b}{j}\right)\left({k}\right)\right)=\left({a}\mathrm{decompPMat}{k}\right){+}_{\mathrm{Scalar}\left({Q}\right)}\left({b}\mathrm{decompPMat}{k}\right)$
104 30 90 103 3eqtrd ${⊢}\left(\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\wedge \left({a}\in {B}\wedge {b}\in {B}\right)\right)\wedge {k}\in {ℕ}_{0}\right)\to \left({a}{+}_{{C}}{b}\right)\mathrm{decompPMat}{k}=\left({a}\mathrm{decompPMat}{k}\right){+}_{\mathrm{Scalar}\left({Q}\right)}\left({b}\mathrm{decompPMat}{k}\right)$
105 104 oveq1d
106 8 ply1lmod ${⊢}{A}\in \mathrm{Ring}\to {Q}\in \mathrm{LMod}$
107 16 106 syl ${⊢}\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\to {Q}\in \mathrm{LMod}$
108 107 ad2antrr ${⊢}\left(\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\wedge \left({a}\in {B}\wedge {b}\in {B}\right)\right)\wedge {k}\in {ℕ}_{0}\right)\to {Q}\in \mathrm{LMod}$
109 simpl ${⊢}\left({a}\in {B}\wedge {b}\in {B}\right)\to {a}\in {B}$
110 109 ad2antlr ${⊢}\left(\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\wedge \left({a}\in {B}\wedge {b}\in {B}\right)\right)\wedge {k}\in {ℕ}_{0}\right)\to {a}\in {B}$
111 1 2 3 7 38 decpmatcl ${⊢}\left({R}\in \mathrm{Ring}\wedge {a}\in {B}\wedge {k}\in {ℕ}_{0}\right)\to {a}\mathrm{decompPMat}{k}\in {\mathrm{Base}}_{{A}}$
112 39 110 52 111 syl3anc ${⊢}\left(\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\wedge \left({a}\in {B}\wedge {b}\in {B}\right)\right)\wedge {k}\in {ℕ}_{0}\right)\to {a}\mathrm{decompPMat}{k}\in {\mathrm{Base}}_{{A}}$
113 92 eqcomd ${⊢}\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\to \mathrm{Scalar}\left({Q}\right)={A}$
114 113 ad2antrr ${⊢}\left(\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\wedge \left({a}\in {B}\wedge {b}\in {B}\right)\right)\wedge {k}\in {ℕ}_{0}\right)\to \mathrm{Scalar}\left({Q}\right)={A}$
115 114 fveq2d ${⊢}\left(\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\wedge \left({a}\in {B}\wedge {b}\in {B}\right)\right)\wedge {k}\in {ℕ}_{0}\right)\to {\mathrm{Base}}_{\mathrm{Scalar}\left({Q}\right)}={\mathrm{Base}}_{{A}}$
116 112 115 eleqtrrd ${⊢}\left(\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\wedge \left({a}\in {B}\wedge {b}\in {B}\right)\right)\wedge {k}\in {ℕ}_{0}\right)\to {a}\mathrm{decompPMat}{k}\in {\mathrm{Base}}_{\mathrm{Scalar}\left({Q}\right)}$
117 simpr ${⊢}\left({a}\in {B}\wedge {b}\in {B}\right)\to {b}\in {B}$
118 117 ad2antlr ${⊢}\left(\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\wedge \left({a}\in {B}\wedge {b}\in {B}\right)\right)\wedge {k}\in {ℕ}_{0}\right)\to {b}\in {B}$
119 1 2 3 7 38 decpmatcl ${⊢}\left({R}\in \mathrm{Ring}\wedge {b}\in {B}\wedge {k}\in {ℕ}_{0}\right)\to {b}\mathrm{decompPMat}{k}\in {\mathrm{Base}}_{{A}}$
120 39 118 52 119 syl3anc ${⊢}\left(\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\wedge \left({a}\in {B}\wedge {b}\in {B}\right)\right)\wedge {k}\in {ℕ}_{0}\right)\to {b}\mathrm{decompPMat}{k}\in {\mathrm{Base}}_{{A}}$
121 120 115 eleqtrrd ${⊢}\left(\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\wedge \left({a}\in {B}\wedge {b}\in {B}\right)\right)\wedge {k}\in {ℕ}_{0}\right)\to {b}\mathrm{decompPMat}{k}\in {\mathrm{Base}}_{\mathrm{Scalar}\left({Q}\right)}$
122 eqid ${⊢}{\mathrm{mulGrp}}_{{Q}}={\mathrm{mulGrp}}_{{Q}}$
123 122 ringmgp ${⊢}{Q}\in \mathrm{Ring}\to {\mathrm{mulGrp}}_{{Q}}\in \mathrm{Mnd}$
124 18 123 syl ${⊢}\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\to {\mathrm{mulGrp}}_{{Q}}\in \mathrm{Mnd}$
125 124 ad2antrr ${⊢}\left(\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\wedge \left({a}\in {B}\wedge {b}\in {B}\right)\right)\wedge {k}\in {ℕ}_{0}\right)\to {\mathrm{mulGrp}}_{{Q}}\in \mathrm{Mnd}$
126 6 8 9 vr1cl ${⊢}{A}\in \mathrm{Ring}\to {X}\in {L}$
127 16 126 syl ${⊢}\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\to {X}\in {L}$
128 127 ad2antrr ${⊢}\left(\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\wedge \left({a}\in {B}\wedge {b}\in {B}\right)\right)\wedge {k}\in {ℕ}_{0}\right)\to {X}\in {L}$
129 122 9 mgpbas ${⊢}{L}={\mathrm{Base}}_{{\mathrm{mulGrp}}_{{Q}}}$
130 129 5 mulgnn0cl
131 125 52 128 130 syl3anc
132 eqid ${⊢}\mathrm{Scalar}\left({Q}\right)=\mathrm{Scalar}\left({Q}\right)$
133 eqid ${⊢}{\mathrm{Base}}_{\mathrm{Scalar}\left({Q}\right)}={\mathrm{Base}}_{\mathrm{Scalar}\left({Q}\right)}$
134 eqid ${⊢}{+}_{\mathrm{Scalar}\left({Q}\right)}={+}_{\mathrm{Scalar}\left({Q}\right)}$
135 9 12 132 4 133 134 lmodvsdir
136 108 116 121 131 135 syl13anc
137 105 136 eqtrd
138 137 mpteq2dva
139 138 oveq2d
140 eqid ${⊢}{0}_{{Q}}={0}_{{Q}}$
141 ringcmn ${⊢}{Q}\in \mathrm{Ring}\to {Q}\in \mathrm{CMnd}$
142 18 141 syl ${⊢}\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\to {Q}\in \mathrm{CMnd}$
143 142 adantr ${⊢}\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\wedge \left({a}\in {B}\wedge {b}\in {B}\right)\right)\to {Q}\in \mathrm{CMnd}$
144 nn0ex ${⊢}{ℕ}_{0}\in \mathrm{V}$
145 144 a1i ${⊢}\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\wedge \left({a}\in {B}\wedge {b}\in {B}\right)\right)\to {ℕ}_{0}\in \mathrm{V}$
146 109 anim2i ${⊢}\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\wedge \left({a}\in {B}\wedge {b}\in {B}\right)\right)\to \left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\wedge {a}\in {B}\right)$
147 df-3an ${⊢}\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\wedge {a}\in {B}\right)↔\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\wedge {a}\in {B}\right)$
148 146 147 sylibr ${⊢}\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\wedge \left({a}\in {B}\wedge {b}\in {B}\right)\right)\to \left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\wedge {a}\in {B}\right)$
149 1 2 3 4 5 6 7 8 9 pm2mpghmlem1
150 148 149 sylan
151 117 anim2i ${⊢}\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\wedge \left({a}\in {B}\wedge {b}\in {B}\right)\right)\to \left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\wedge {b}\in {B}\right)$
152 df-3an ${⊢}\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\wedge {b}\in {B}\right)↔\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\wedge {b}\in {B}\right)$
153 151 152 sylibr ${⊢}\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\wedge \left({a}\in {B}\wedge {b}\in {B}\right)\right)\to \left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\wedge {b}\in {B}\right)$
154 1 2 3 4 5 6 7 8 9 pm2mpghmlem1
155 153 154 sylan
156 eqidd
157 eqidd
158 1 2 3 4 5 6 7 8 pm2mpghmlem2
159 148 158 syl
160 1 2 3 4 5 6 7 8 pm2mpghmlem2
161 153 160 syl
162 9 140 12 143 145 150 155 156 157 159 161 gsummptfsadd
163 139 162 eqtrd
164 simpll ${⊢}\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\wedge \left({a}\in {B}\wedge {b}\in {B}\right)\right)\to {N}\in \mathrm{Fin}$
165 simplr ${⊢}\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\wedge \left({a}\in {B}\wedge {b}\in {B}\right)\right)\to {R}\in \mathrm{Ring}$
166 1 2 3 4 5 6 7 8 10 pm2mpfval
167 164 165 28 166 syl3anc
168 1 2 3 4 5 6 7 8 10 pm2mpfval
169 164 165 95 168 syl3anc
170 1 2 3 4 5 6 7 8 10 pm2mpfval
171 164 165 99 170 syl3anc
172 169 171 oveq12d
173 163 167 172 3eqtr4d ${⊢}\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\wedge \left({a}\in {B}\wedge {b}\in {B}\right)\right)\to {T}\left({a}{+}_{{C}}{b}\right)={T}\left({a}\right){+}_{{Q}}{T}\left({b}\right)$
174 3 9 11 12 15 20 21 173 isghmd ${⊢}\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\to {T}\in \left({C}\mathrm{GrpHom}{Q}\right)$