Metamath Proof Explorer


Theorem cayhamlem4

Description: Lemma for cayleyhamilton . (Contributed by AV, 25-Nov-2019) (Revised by AV, 15-Dec-2019)

Ref Expression
Hypotheses chcoeffeq.a 𝐴 = ( 𝑁 Mat 𝑅 )
chcoeffeq.b 𝐵 = ( Base ‘ 𝐴 )
chcoeffeq.p 𝑃 = ( Poly1𝑅 )
chcoeffeq.y 𝑌 = ( 𝑁 Mat 𝑃 )
chcoeffeq.r × = ( .r𝑌 )
chcoeffeq.s = ( -g𝑌 )
chcoeffeq.0 0 = ( 0g𝑌 )
chcoeffeq.t 𝑇 = ( 𝑁 matToPolyMat 𝑅 )
chcoeffeq.c 𝐶 = ( 𝑁 CharPlyMat 𝑅 )
chcoeffeq.k 𝐾 = ( 𝐶𝑀 )
chcoeffeq.g 𝐺 = ( 𝑛 ∈ ℕ0 ↦ if ( 𝑛 = 0 , ( 0 ( ( 𝑇𝑀 ) × ( 𝑇 ‘ ( 𝑏 ‘ 0 ) ) ) ) , if ( 𝑛 = ( 𝑠 + 1 ) , ( 𝑇 ‘ ( 𝑏𝑠 ) ) , if ( ( 𝑠 + 1 ) < 𝑛 , 0 , ( ( 𝑇 ‘ ( 𝑏 ‘ ( 𝑛 − 1 ) ) ) ( ( 𝑇𝑀 ) × ( 𝑇 ‘ ( 𝑏𝑛 ) ) ) ) ) ) ) )
chcoeffeq.w 𝑊 = ( Base ‘ 𝑌 )
chcoeffeq.1 1 = ( 1r𝐴 )
chcoeffeq.m = ( ·𝑠𝐴 )
chcoeffeq.u 𝑈 = ( 𝑁 cPolyMatToMat 𝑅 )
cayhamlem.e1 = ( .g ‘ ( mulGrp ‘ 𝐴 ) )
cayhamlem.e2 𝐸 = ( .g ‘ ( mulGrp ‘ 𝑌 ) )
Assertion cayhamlem4 ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵 ) → ∃ 𝑠 ∈ ℕ ∃ 𝑏 ∈ ( 𝐵m ( 0 ... 𝑠 ) ) ( 𝐴 Σg ( 𝑛 ∈ ℕ0 ↦ ( ( ( coe1𝐾 ) ‘ 𝑛 ) ( 𝑛 𝑀 ) ) ) ) = ( 𝑈 ‘ ( 𝑌 Σg ( 𝑛 ∈ ℕ0 ↦ ( ( 𝑛 𝐸 ( 𝑇𝑀 ) ) × ( 𝐺𝑛 ) ) ) ) ) )

Proof

Step Hyp Ref Expression
1 chcoeffeq.a 𝐴 = ( 𝑁 Mat 𝑅 )
2 chcoeffeq.b 𝐵 = ( Base ‘ 𝐴 )
3 chcoeffeq.p 𝑃 = ( Poly1𝑅 )
4 chcoeffeq.y 𝑌 = ( 𝑁 Mat 𝑃 )
5 chcoeffeq.r × = ( .r𝑌 )
6 chcoeffeq.s = ( -g𝑌 )
7 chcoeffeq.0 0 = ( 0g𝑌 )
8 chcoeffeq.t 𝑇 = ( 𝑁 matToPolyMat 𝑅 )
9 chcoeffeq.c 𝐶 = ( 𝑁 CharPlyMat 𝑅 )
10 chcoeffeq.k 𝐾 = ( 𝐶𝑀 )
11 chcoeffeq.g 𝐺 = ( 𝑛 ∈ ℕ0 ↦ if ( 𝑛 = 0 , ( 0 ( ( 𝑇𝑀 ) × ( 𝑇 ‘ ( 𝑏 ‘ 0 ) ) ) ) , if ( 𝑛 = ( 𝑠 + 1 ) , ( 𝑇 ‘ ( 𝑏𝑠 ) ) , if ( ( 𝑠 + 1 ) < 𝑛 , 0 , ( ( 𝑇 ‘ ( 𝑏 ‘ ( 𝑛 − 1 ) ) ) ( ( 𝑇𝑀 ) × ( 𝑇 ‘ ( 𝑏𝑛 ) ) ) ) ) ) ) )
12 chcoeffeq.w 𝑊 = ( Base ‘ 𝑌 )
13 chcoeffeq.1 1 = ( 1r𝐴 )
14 chcoeffeq.m = ( ·𝑠𝐴 )
15 chcoeffeq.u 𝑈 = ( 𝑁 cPolyMatToMat 𝑅 )
16 cayhamlem.e1 = ( .g ‘ ( mulGrp ‘ 𝐴 ) )
17 cayhamlem.e2 𝐸 = ( .g ‘ ( mulGrp ‘ 𝑌 ) )
18 id ( ( 𝐴 Σg ( 𝑛 ∈ ℕ0 ↦ ( ( ( coe1𝐾 ) ‘ 𝑛 ) ( 𝑛 𝑀 ) ) ) ) = ( 𝐴 Σg ( 𝑛 ∈ ℕ0 ↦ ( ( 𝑛 𝑀 ) ( .r𝐴 ) ( 𝑈 ‘ ( 𝐺𝑛 ) ) ) ) ) → ( 𝐴 Σg ( 𝑛 ∈ ℕ0 ↦ ( ( ( coe1𝐾 ) ‘ 𝑛 ) ( 𝑛 𝑀 ) ) ) ) = ( 𝐴 Σg ( 𝑛 ∈ ℕ0 ↦ ( ( 𝑛 𝑀 ) ( .r𝐴 ) ( 𝑈 ‘ ( 𝐺𝑛 ) ) ) ) ) )
19 simp1 ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵 ) → 𝑁 ∈ Fin )
20 19 ad2antrr ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵 ) ∧ 𝑠 ∈ ℕ ) ∧ 𝑏 ∈ ( 𝐵m ( 0 ... 𝑠 ) ) ) → 𝑁 ∈ Fin )
21 crngring ( 𝑅 ∈ CRing → 𝑅 ∈ Ring )
22 21 3ad2ant2 ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵 ) → 𝑅 ∈ Ring )
23 22 ad2antrr ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵 ) ∧ 𝑠 ∈ ℕ ) ∧ 𝑏 ∈ ( 𝐵m ( 0 ... 𝑠 ) ) ) → 𝑅 ∈ Ring )
24 eqid ( 0g𝐴 ) = ( 0g𝐴 )
25 1 matring ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → 𝐴 ∈ Ring )
26 21 25 sylan2 ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) → 𝐴 ∈ Ring )
27 ringcmn ( 𝐴 ∈ Ring → 𝐴 ∈ CMnd )
28 26 27 syl ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) → 𝐴 ∈ CMnd )
29 28 3adant3 ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵 ) → 𝐴 ∈ CMnd )
30 29 ad2antrr ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵 ) ∧ 𝑠 ∈ ℕ ) ∧ 𝑏 ∈ ( 𝐵m ( 0 ... 𝑠 ) ) ) → 𝐴 ∈ CMnd )
31 nn0ex 0 ∈ V
32 31 a1i ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵 ) ∧ 𝑠 ∈ ℕ ) ∧ 𝑏 ∈ ( 𝐵m ( 0 ... 𝑠 ) ) ) → ℕ0 ∈ V )
33 20 23 25 syl2anc ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵 ) ∧ 𝑠 ∈ ℕ ) ∧ 𝑏 ∈ ( 𝐵m ( 0 ... 𝑠 ) ) ) → 𝐴 ∈ Ring )
34 33 adantr ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵 ) ∧ 𝑠 ∈ ℕ ) ∧ 𝑏 ∈ ( 𝐵m ( 0 ... 𝑠 ) ) ) ∧ 𝑛 ∈ ℕ0 ) → 𝐴 ∈ Ring )
35 eqid ( mulGrp ‘ 𝐴 ) = ( mulGrp ‘ 𝐴 )
36 35 2 mgpbas 𝐵 = ( Base ‘ ( mulGrp ‘ 𝐴 ) )
37 19 22 25 syl2anc ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵 ) → 𝐴 ∈ Ring )
38 35 ringmgp ( 𝐴 ∈ Ring → ( mulGrp ‘ 𝐴 ) ∈ Mnd )
39 37 38 syl ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵 ) → ( mulGrp ‘ 𝐴 ) ∈ Mnd )
40 39 ad3antrrr ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵 ) ∧ 𝑠 ∈ ℕ ) ∧ 𝑏 ∈ ( 𝐵m ( 0 ... 𝑠 ) ) ) ∧ 𝑛 ∈ ℕ0 ) → ( mulGrp ‘ 𝐴 ) ∈ Mnd )
41 simpr ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵 ) ∧ 𝑠 ∈ ℕ ) ∧ 𝑏 ∈ ( 𝐵m ( 0 ... 𝑠 ) ) ) ∧ 𝑛 ∈ ℕ0 ) → 𝑛 ∈ ℕ0 )
42 simpll3 ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵 ) ∧ 𝑠 ∈ ℕ ) ∧ 𝑏 ∈ ( 𝐵m ( 0 ... 𝑠 ) ) ) → 𝑀𝐵 )
43 42 adantr ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵 ) ∧ 𝑠 ∈ ℕ ) ∧ 𝑏 ∈ ( 𝐵m ( 0 ... 𝑠 ) ) ) ∧ 𝑛 ∈ ℕ0 ) → 𝑀𝐵 )
44 36 16 40 41 43 mulgnn0cld ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵 ) ∧ 𝑠 ∈ ℕ ) ∧ 𝑏 ∈ ( 𝐵m ( 0 ... 𝑠 ) ) ) ∧ 𝑛 ∈ ℕ0 ) → ( 𝑛 𝑀 ) ∈ 𝐵 )
45 eqid ( 𝑁 ConstPolyMat 𝑅 ) = ( 𝑁 ConstPolyMat 𝑅 )
46 1 2 45 15 cpm2mf ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → 𝑈 : ( 𝑁 ConstPolyMat 𝑅 ) ⟶ 𝐵 )
47 19 22 46 syl2anc ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵 ) → 𝑈 : ( 𝑁 ConstPolyMat 𝑅 ) ⟶ 𝐵 )
48 47 ad3antrrr ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵 ) ∧ 𝑠 ∈ ℕ ) ∧ 𝑏 ∈ ( 𝐵m ( 0 ... 𝑠 ) ) ) ∧ 𝑛 ∈ ℕ0 ) → 𝑈 : ( 𝑁 ConstPolyMat 𝑅 ) ⟶ 𝐵 )
49 simplr ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵 ) ∧ 𝑠 ∈ ℕ ) ∧ 𝑏 ∈ ( 𝐵m ( 0 ... 𝑠 ) ) ) → 𝑠 ∈ ℕ )
50 simpr ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵 ) ∧ 𝑠 ∈ ℕ ) ∧ 𝑏 ∈ ( 𝐵m ( 0 ... 𝑠 ) ) ) → 𝑏 ∈ ( 𝐵m ( 0 ... 𝑠 ) ) )
51 1 2 3 4 5 6 7 8 11 45 chfacfisfcpmat ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵m ( 0 ... 𝑠 ) ) ) ) → 𝐺 : ℕ0 ⟶ ( 𝑁 ConstPolyMat 𝑅 ) )
52 20 23 42 49 50 51 syl32anc ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵 ) ∧ 𝑠 ∈ ℕ ) ∧ 𝑏 ∈ ( 𝐵m ( 0 ... 𝑠 ) ) ) → 𝐺 : ℕ0 ⟶ ( 𝑁 ConstPolyMat 𝑅 ) )
53 52 ffvelcdmda ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵 ) ∧ 𝑠 ∈ ℕ ) ∧ 𝑏 ∈ ( 𝐵m ( 0 ... 𝑠 ) ) ) ∧ 𝑛 ∈ ℕ0 ) → ( 𝐺𝑛 ) ∈ ( 𝑁 ConstPolyMat 𝑅 ) )
54 48 53 ffvelcdmd ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵 ) ∧ 𝑠 ∈ ℕ ) ∧ 𝑏 ∈ ( 𝐵m ( 0 ... 𝑠 ) ) ) ∧ 𝑛 ∈ ℕ0 ) → ( 𝑈 ‘ ( 𝐺𝑛 ) ) ∈ 𝐵 )
55 eqid ( .r𝐴 ) = ( .r𝐴 )
56 2 55 ringcl ( ( 𝐴 ∈ Ring ∧ ( 𝑛 𝑀 ) ∈ 𝐵 ∧ ( 𝑈 ‘ ( 𝐺𝑛 ) ) ∈ 𝐵 ) → ( ( 𝑛 𝑀 ) ( .r𝐴 ) ( 𝑈 ‘ ( 𝐺𝑛 ) ) ) ∈ 𝐵 )
57 34 44 54 56 syl3anc ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵 ) ∧ 𝑠 ∈ ℕ ) ∧ 𝑏 ∈ ( 𝐵m ( 0 ... 𝑠 ) ) ) ∧ 𝑛 ∈ ℕ0 ) → ( ( 𝑛 𝑀 ) ( .r𝐴 ) ( 𝑈 ‘ ( 𝐺𝑛 ) ) ) ∈ 𝐵 )
58 57 fmpttd ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵 ) ∧ 𝑠 ∈ ℕ ) ∧ 𝑏 ∈ ( 𝐵m ( 0 ... 𝑠 ) ) ) → ( 𝑛 ∈ ℕ0 ↦ ( ( 𝑛 𝑀 ) ( .r𝐴 ) ( 𝑈 ‘ ( 𝐺𝑛 ) ) ) ) : ℕ0𝐵 )
59 fvexd ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵 ) ∧ 𝑠 ∈ ℕ ) ∧ 𝑏 ∈ ( 𝐵m ( 0 ... 𝑠 ) ) ) → ( 0g𝐴 ) ∈ V )
60 ovexd ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵 ) ∧ 𝑠 ∈ ℕ ) ∧ 𝑏 ∈ ( 𝐵m ( 0 ... 𝑠 ) ) ) ∧ 𝑛 ∈ ℕ0 ) → ( ( 𝑛 𝑀 ) ( .r𝐴 ) ( 𝑈 ‘ ( 𝐺𝑛 ) ) ) ∈ V )
61 1 2 3 4 5 6 7 8 11 chfacffsupp ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵m ( 0 ... 𝑠 ) ) ) ) → 𝐺 finSupp ( 0g𝑌 ) )
62 61 anassrs ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵 ) ∧ 𝑠 ∈ ℕ ) ∧ 𝑏 ∈ ( 𝐵m ( 0 ... 𝑠 ) ) ) → 𝐺 finSupp ( 0g𝑌 ) )
63 ovex ( 𝑁 ConstPolyMat 𝑅 ) ∈ V
64 63 31 pm3.2i ( ( 𝑁 ConstPolyMat 𝑅 ) ∈ V ∧ ℕ0 ∈ V )
65 elmapg ( ( ( 𝑁 ConstPolyMat 𝑅 ) ∈ V ∧ ℕ0 ∈ V ) → ( 𝐺 ∈ ( ( 𝑁 ConstPolyMat 𝑅 ) ↑m0 ) ↔ 𝐺 : ℕ0 ⟶ ( 𝑁 ConstPolyMat 𝑅 ) ) )
66 64 65 mp1i ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵 ) ∧ 𝑠 ∈ ℕ ) ∧ 𝑏 ∈ ( 𝐵m ( 0 ... 𝑠 ) ) ) → ( 𝐺 ∈ ( ( 𝑁 ConstPolyMat 𝑅 ) ↑m0 ) ↔ 𝐺 : ℕ0 ⟶ ( 𝑁 ConstPolyMat 𝑅 ) ) )
67 52 66 mpbird ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵 ) ∧ 𝑠 ∈ ℕ ) ∧ 𝑏 ∈ ( 𝐵m ( 0 ... 𝑠 ) ) ) → 𝐺 ∈ ( ( 𝑁 ConstPolyMat 𝑅 ) ↑m0 ) )
68 fvex ( 0g𝑌 ) ∈ V
69 fsuppmapnn0ub ( ( 𝐺 ∈ ( ( 𝑁 ConstPolyMat 𝑅 ) ↑m0 ) ∧ ( 0g𝑌 ) ∈ V ) → ( 𝐺 finSupp ( 0g𝑌 ) → ∃ 𝑤 ∈ ℕ0𝑧 ∈ ℕ0 ( 𝑤 < 𝑧 → ( 𝐺𝑧 ) = ( 0g𝑌 ) ) ) )
70 67 68 69 sylancl ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵 ) ∧ 𝑠 ∈ ℕ ) ∧ 𝑏 ∈ ( 𝐵m ( 0 ... 𝑠 ) ) ) → ( 𝐺 finSupp ( 0g𝑌 ) → ∃ 𝑤 ∈ ℕ0𝑧 ∈ ℕ0 ( 𝑤 < 𝑧 → ( 𝐺𝑧 ) = ( 0g𝑌 ) ) ) )
71 csbov12g ( 𝑧 ∈ ℕ0 𝑧 / 𝑛 ( ( 𝑛 𝑀 ) ( .r𝐴 ) ( 𝑈 ‘ ( 𝐺𝑛 ) ) ) = ( 𝑧 / 𝑛 ( 𝑛 𝑀 ) ( .r𝐴 ) 𝑧 / 𝑛 ( 𝑈 ‘ ( 𝐺𝑛 ) ) ) )
72 csbov1g ( 𝑧 ∈ ℕ0 𝑧 / 𝑛 ( 𝑛 𝑀 ) = ( 𝑧 / 𝑛 𝑛 𝑀 ) )
73 csbvarg ( 𝑧 ∈ ℕ0 𝑧 / 𝑛 𝑛 = 𝑧 )
74 73 oveq1d ( 𝑧 ∈ ℕ0 → ( 𝑧 / 𝑛 𝑛 𝑀 ) = ( 𝑧 𝑀 ) )
75 72 74 eqtrd ( 𝑧 ∈ ℕ0 𝑧 / 𝑛 ( 𝑛 𝑀 ) = ( 𝑧 𝑀 ) )
76 csbfv2g ( 𝑧 ∈ ℕ0 𝑧 / 𝑛 ( 𝑈 ‘ ( 𝐺𝑛 ) ) = ( 𝑈 𝑧 / 𝑛 ( 𝐺𝑛 ) ) )
77 csbfv 𝑧 / 𝑛 ( 𝐺𝑛 ) = ( 𝐺𝑧 )
78 77 a1i ( 𝑧 ∈ ℕ0 𝑧 / 𝑛 ( 𝐺𝑛 ) = ( 𝐺𝑧 ) )
79 78 fveq2d ( 𝑧 ∈ ℕ0 → ( 𝑈 𝑧 / 𝑛 ( 𝐺𝑛 ) ) = ( 𝑈 ‘ ( 𝐺𝑧 ) ) )
80 76 79 eqtrd ( 𝑧 ∈ ℕ0 𝑧 / 𝑛 ( 𝑈 ‘ ( 𝐺𝑛 ) ) = ( 𝑈 ‘ ( 𝐺𝑧 ) ) )
81 75 80 oveq12d ( 𝑧 ∈ ℕ0 → ( 𝑧 / 𝑛 ( 𝑛 𝑀 ) ( .r𝐴 ) 𝑧 / 𝑛 ( 𝑈 ‘ ( 𝐺𝑛 ) ) ) = ( ( 𝑧 𝑀 ) ( .r𝐴 ) ( 𝑈 ‘ ( 𝐺𝑧 ) ) ) )
82 71 81 eqtrd ( 𝑧 ∈ ℕ0 𝑧 / 𝑛 ( ( 𝑛 𝑀 ) ( .r𝐴 ) ( 𝑈 ‘ ( 𝐺𝑛 ) ) ) = ( ( 𝑧 𝑀 ) ( .r𝐴 ) ( 𝑈 ‘ ( 𝐺𝑧 ) ) ) )
83 82 ad2antlr ( ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵 ) ∧ 𝑠 ∈ ℕ ) ∧ 𝑏 ∈ ( 𝐵m ( 0 ... 𝑠 ) ) ) ∧ 𝑧 ∈ ℕ0 ) ∧ ( 𝐺𝑧 ) = ( 0g𝑌 ) ) → 𝑧 / 𝑛 ( ( 𝑛 𝑀 ) ( .r𝐴 ) ( 𝑈 ‘ ( 𝐺𝑛 ) ) ) = ( ( 𝑧 𝑀 ) ( .r𝐴 ) ( 𝑈 ‘ ( 𝐺𝑧 ) ) ) )
84 fveq2 ( ( 𝐺𝑧 ) = ( 0g𝑌 ) → ( 𝑈 ‘ ( 𝐺𝑧 ) ) = ( 𝑈 ‘ ( 0g𝑌 ) ) )
85 19 22 jca ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵 ) → ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) )
86 85 adantr ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵 ) ∧ 𝑠 ∈ ℕ ) → ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) )
87 eqid ( 0g𝑌 ) = ( 0g𝑌 )
88 1 15 3 4 24 87 m2cpminv0 ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → ( 𝑈 ‘ ( 0g𝑌 ) ) = ( 0g𝐴 ) )
89 86 88 syl ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵 ) ∧ 𝑠 ∈ ℕ ) → ( 𝑈 ‘ ( 0g𝑌 ) ) = ( 0g𝐴 ) )
90 89 ad2antrr ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵 ) ∧ 𝑠 ∈ ℕ ) ∧ 𝑏 ∈ ( 𝐵m ( 0 ... 𝑠 ) ) ) ∧ 𝑧 ∈ ℕ0 ) → ( 𝑈 ‘ ( 0g𝑌 ) ) = ( 0g𝐴 ) )
91 84 90 sylan9eqr ( ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵 ) ∧ 𝑠 ∈ ℕ ) ∧ 𝑏 ∈ ( 𝐵m ( 0 ... 𝑠 ) ) ) ∧ 𝑧 ∈ ℕ0 ) ∧ ( 𝐺𝑧 ) = ( 0g𝑌 ) ) → ( 𝑈 ‘ ( 𝐺𝑧 ) ) = ( 0g𝐴 ) )
92 91 oveq2d ( ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵 ) ∧ 𝑠 ∈ ℕ ) ∧ 𝑏 ∈ ( 𝐵m ( 0 ... 𝑠 ) ) ) ∧ 𝑧 ∈ ℕ0 ) ∧ ( 𝐺𝑧 ) = ( 0g𝑌 ) ) → ( ( 𝑧 𝑀 ) ( .r𝐴 ) ( 𝑈 ‘ ( 𝐺𝑧 ) ) ) = ( ( 𝑧 𝑀 ) ( .r𝐴 ) ( 0g𝐴 ) ) )
93 33 adantr ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵 ) ∧ 𝑠 ∈ ℕ ) ∧ 𝑏 ∈ ( 𝐵m ( 0 ... 𝑠 ) ) ) ∧ 𝑧 ∈ ℕ0 ) → 𝐴 ∈ Ring )
94 39 ad3antrrr ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵 ) ∧ 𝑠 ∈ ℕ ) ∧ 𝑏 ∈ ( 𝐵m ( 0 ... 𝑠 ) ) ) ∧ 𝑧 ∈ ℕ0 ) → ( mulGrp ‘ 𝐴 ) ∈ Mnd )
95 simpr ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵 ) ∧ 𝑠 ∈ ℕ ) ∧ 𝑏 ∈ ( 𝐵m ( 0 ... 𝑠 ) ) ) ∧ 𝑧 ∈ ℕ0 ) → 𝑧 ∈ ℕ0 )
96 42 adantr ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵 ) ∧ 𝑠 ∈ ℕ ) ∧ 𝑏 ∈ ( 𝐵m ( 0 ... 𝑠 ) ) ) ∧ 𝑧 ∈ ℕ0 ) → 𝑀𝐵 )
97 36 16 94 95 96 mulgnn0cld ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵 ) ∧ 𝑠 ∈ ℕ ) ∧ 𝑏 ∈ ( 𝐵m ( 0 ... 𝑠 ) ) ) ∧ 𝑧 ∈ ℕ0 ) → ( 𝑧 𝑀 ) ∈ 𝐵 )
98 93 97 jca ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵 ) ∧ 𝑠 ∈ ℕ ) ∧ 𝑏 ∈ ( 𝐵m ( 0 ... 𝑠 ) ) ) ∧ 𝑧 ∈ ℕ0 ) → ( 𝐴 ∈ Ring ∧ ( 𝑧 𝑀 ) ∈ 𝐵 ) )
99 98 adantr ( ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵 ) ∧ 𝑠 ∈ ℕ ) ∧ 𝑏 ∈ ( 𝐵m ( 0 ... 𝑠 ) ) ) ∧ 𝑧 ∈ ℕ0 ) ∧ ( 𝐺𝑧 ) = ( 0g𝑌 ) ) → ( 𝐴 ∈ Ring ∧ ( 𝑧 𝑀 ) ∈ 𝐵 ) )
100 2 55 24 ringrz ( ( 𝐴 ∈ Ring ∧ ( 𝑧 𝑀 ) ∈ 𝐵 ) → ( ( 𝑧 𝑀 ) ( .r𝐴 ) ( 0g𝐴 ) ) = ( 0g𝐴 ) )
101 99 100 syl ( ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵 ) ∧ 𝑠 ∈ ℕ ) ∧ 𝑏 ∈ ( 𝐵m ( 0 ... 𝑠 ) ) ) ∧ 𝑧 ∈ ℕ0 ) ∧ ( 𝐺𝑧 ) = ( 0g𝑌 ) ) → ( ( 𝑧 𝑀 ) ( .r𝐴 ) ( 0g𝐴 ) ) = ( 0g𝐴 ) )
102 83 92 101 3eqtrd ( ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵 ) ∧ 𝑠 ∈ ℕ ) ∧ 𝑏 ∈ ( 𝐵m ( 0 ... 𝑠 ) ) ) ∧ 𝑧 ∈ ℕ0 ) ∧ ( 𝐺𝑧 ) = ( 0g𝑌 ) ) → 𝑧 / 𝑛 ( ( 𝑛 𝑀 ) ( .r𝐴 ) ( 𝑈 ‘ ( 𝐺𝑛 ) ) ) = ( 0g𝐴 ) )
103 102 ex ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵 ) ∧ 𝑠 ∈ ℕ ) ∧ 𝑏 ∈ ( 𝐵m ( 0 ... 𝑠 ) ) ) ∧ 𝑧 ∈ ℕ0 ) → ( ( 𝐺𝑧 ) = ( 0g𝑌 ) → 𝑧 / 𝑛 ( ( 𝑛 𝑀 ) ( .r𝐴 ) ( 𝑈 ‘ ( 𝐺𝑛 ) ) ) = ( 0g𝐴 ) ) )
104 103 adantlr ( ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵 ) ∧ 𝑠 ∈ ℕ ) ∧ 𝑏 ∈ ( 𝐵m ( 0 ... 𝑠 ) ) ) ∧ 𝑤 ∈ ℕ0 ) ∧ 𝑧 ∈ ℕ0 ) → ( ( 𝐺𝑧 ) = ( 0g𝑌 ) → 𝑧 / 𝑛 ( ( 𝑛 𝑀 ) ( .r𝐴 ) ( 𝑈 ‘ ( 𝐺𝑛 ) ) ) = ( 0g𝐴 ) ) )
105 104 imim2d ( ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵 ) ∧ 𝑠 ∈ ℕ ) ∧ 𝑏 ∈ ( 𝐵m ( 0 ... 𝑠 ) ) ) ∧ 𝑤 ∈ ℕ0 ) ∧ 𝑧 ∈ ℕ0 ) → ( ( 𝑤 < 𝑧 → ( 𝐺𝑧 ) = ( 0g𝑌 ) ) → ( 𝑤 < 𝑧 𝑧 / 𝑛 ( ( 𝑛 𝑀 ) ( .r𝐴 ) ( 𝑈 ‘ ( 𝐺𝑛 ) ) ) = ( 0g𝐴 ) ) ) )
106 105 ralimdva ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵 ) ∧ 𝑠 ∈ ℕ ) ∧ 𝑏 ∈ ( 𝐵m ( 0 ... 𝑠 ) ) ) ∧ 𝑤 ∈ ℕ0 ) → ( ∀ 𝑧 ∈ ℕ0 ( 𝑤 < 𝑧 → ( 𝐺𝑧 ) = ( 0g𝑌 ) ) → ∀ 𝑧 ∈ ℕ0 ( 𝑤 < 𝑧 𝑧 / 𝑛 ( ( 𝑛 𝑀 ) ( .r𝐴 ) ( 𝑈 ‘ ( 𝐺𝑛 ) ) ) = ( 0g𝐴 ) ) ) )
107 106 reximdva ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵 ) ∧ 𝑠 ∈ ℕ ) ∧ 𝑏 ∈ ( 𝐵m ( 0 ... 𝑠 ) ) ) → ( ∃ 𝑤 ∈ ℕ0𝑧 ∈ ℕ0 ( 𝑤 < 𝑧 → ( 𝐺𝑧 ) = ( 0g𝑌 ) ) → ∃ 𝑤 ∈ ℕ0𝑧 ∈ ℕ0 ( 𝑤 < 𝑧 𝑧 / 𝑛 ( ( 𝑛 𝑀 ) ( .r𝐴 ) ( 𝑈 ‘ ( 𝐺𝑛 ) ) ) = ( 0g𝐴 ) ) ) )
108 70 107 syld ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵 ) ∧ 𝑠 ∈ ℕ ) ∧ 𝑏 ∈ ( 𝐵m ( 0 ... 𝑠 ) ) ) → ( 𝐺 finSupp ( 0g𝑌 ) → ∃ 𝑤 ∈ ℕ0𝑧 ∈ ℕ0 ( 𝑤 < 𝑧 𝑧 / 𝑛 ( ( 𝑛 𝑀 ) ( .r𝐴 ) ( 𝑈 ‘ ( 𝐺𝑛 ) ) ) = ( 0g𝐴 ) ) ) )
109 62 108 mpd ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵 ) ∧ 𝑠 ∈ ℕ ) ∧ 𝑏 ∈ ( 𝐵m ( 0 ... 𝑠 ) ) ) → ∃ 𝑤 ∈ ℕ0𝑧 ∈ ℕ0 ( 𝑤 < 𝑧 𝑧 / 𝑛 ( ( 𝑛 𝑀 ) ( .r𝐴 ) ( 𝑈 ‘ ( 𝐺𝑛 ) ) ) = ( 0g𝐴 ) ) )
110 59 60 109 mptnn0fsupp ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵 ) ∧ 𝑠 ∈ ℕ ) ∧ 𝑏 ∈ ( 𝐵m ( 0 ... 𝑠 ) ) ) → ( 𝑛 ∈ ℕ0 ↦ ( ( 𝑛 𝑀 ) ( .r𝐴 ) ( 𝑈 ‘ ( 𝐺𝑛 ) ) ) ) finSupp ( 0g𝐴 ) )
111 2 24 30 32 58 110 gsumcl ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵 ) ∧ 𝑠 ∈ ℕ ) ∧ 𝑏 ∈ ( 𝐵m ( 0 ... 𝑠 ) ) ) → ( 𝐴 Σg ( 𝑛 ∈ ℕ0 ↦ ( ( 𝑛 𝑀 ) ( .r𝐴 ) ( 𝑈 ‘ ( 𝐺𝑛 ) ) ) ) ) ∈ 𝐵 )
112 15 1 2 8 m2cpminvid ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ ( 𝐴 Σg ( 𝑛 ∈ ℕ0 ↦ ( ( 𝑛 𝑀 ) ( .r𝐴 ) ( 𝑈 ‘ ( 𝐺𝑛 ) ) ) ) ) ∈ 𝐵 ) → ( 𝑈 ‘ ( 𝑇 ‘ ( 𝐴 Σg ( 𝑛 ∈ ℕ0 ↦ ( ( 𝑛 𝑀 ) ( .r𝐴 ) ( 𝑈 ‘ ( 𝐺𝑛 ) ) ) ) ) ) ) = ( 𝐴 Σg ( 𝑛 ∈ ℕ0 ↦ ( ( 𝑛 𝑀 ) ( .r𝐴 ) ( 𝑈 ‘ ( 𝐺𝑛 ) ) ) ) ) )
113 20 23 111 112 syl3anc ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵 ) ∧ 𝑠 ∈ ℕ ) ∧ 𝑏 ∈ ( 𝐵m ( 0 ... 𝑠 ) ) ) → ( 𝑈 ‘ ( 𝑇 ‘ ( 𝐴 Σg ( 𝑛 ∈ ℕ0 ↦ ( ( 𝑛 𝑀 ) ( .r𝐴 ) ( 𝑈 ‘ ( 𝐺𝑛 ) ) ) ) ) ) ) = ( 𝐴 Σg ( 𝑛 ∈ ℕ0 ↦ ( ( 𝑛 𝑀 ) ( .r𝐴 ) ( 𝑈 ‘ ( 𝐺𝑛 ) ) ) ) ) )
114 3 4 pmatring ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → 𝑌 ∈ Ring )
115 19 22 114 syl2anc ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵 ) → 𝑌 ∈ Ring )
116 ringmnd ( 𝑌 ∈ Ring → 𝑌 ∈ Mnd )
117 115 116 syl ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵 ) → 𝑌 ∈ Mnd )
118 117 ad2antrr ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵 ) ∧ 𝑠 ∈ ℕ ) ∧ 𝑏 ∈ ( 𝐵m ( 0 ... 𝑠 ) ) ) → 𝑌 ∈ Mnd )
119 8 1 2 3 4 12 mat2pmatghm ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → 𝑇 ∈ ( 𝐴 GrpHom 𝑌 ) )
120 20 23 119 syl2anc ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵 ) ∧ 𝑠 ∈ ℕ ) ∧ 𝑏 ∈ ( 𝐵m ( 0 ... 𝑠 ) ) ) → 𝑇 ∈ ( 𝐴 GrpHom 𝑌 ) )
121 ghmmhm ( 𝑇 ∈ ( 𝐴 GrpHom 𝑌 ) → 𝑇 ∈ ( 𝐴 MndHom 𝑌 ) )
122 120 121 syl ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵 ) ∧ 𝑠 ∈ ℕ ) ∧ 𝑏 ∈ ( 𝐵m ( 0 ... 𝑠 ) ) ) → 𝑇 ∈ ( 𝐴 MndHom 𝑌 ) )
123 37 ad3antrrr ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵 ) ∧ 𝑠 ∈ ℕ ) ∧ 𝑏 ∈ ( 𝐵m ( 0 ... 𝑠 ) ) ) ∧ 𝑛 ∈ ℕ0 ) → 𝐴 ∈ Ring )
124 21 46 sylan2 ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) → 𝑈 : ( 𝑁 ConstPolyMat 𝑅 ) ⟶ 𝐵 )
125 124 3adant3 ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵 ) → 𝑈 : ( 𝑁 ConstPolyMat 𝑅 ) ⟶ 𝐵 )
126 125 ad3antrrr ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵 ) ∧ 𝑠 ∈ ℕ ) ∧ 𝑏 ∈ ( 𝐵m ( 0 ... 𝑠 ) ) ) ∧ 𝑛 ∈ ℕ0 ) → 𝑈 : ( 𝑁 ConstPolyMat 𝑅 ) ⟶ 𝐵 )
127 126 53 ffvelcdmd ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵 ) ∧ 𝑠 ∈ ℕ ) ∧ 𝑏 ∈ ( 𝐵m ( 0 ... 𝑠 ) ) ) ∧ 𝑛 ∈ ℕ0 ) → ( 𝑈 ‘ ( 𝐺𝑛 ) ) ∈ 𝐵 )
128 123 44 127 56 syl3anc ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵 ) ∧ 𝑠 ∈ ℕ ) ∧ 𝑏 ∈ ( 𝐵m ( 0 ... 𝑠 ) ) ) ∧ 𝑛 ∈ ℕ0 ) → ( ( 𝑛 𝑀 ) ( .r𝐴 ) ( 𝑈 ‘ ( 𝐺𝑛 ) ) ) ∈ 𝐵 )
129 2 24 30 118 32 122 128 110 gsummptmhm ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵 ) ∧ 𝑠 ∈ ℕ ) ∧ 𝑏 ∈ ( 𝐵m ( 0 ... 𝑠 ) ) ) → ( 𝑌 Σg ( 𝑛 ∈ ℕ0 ↦ ( 𝑇 ‘ ( ( 𝑛 𝑀 ) ( .r𝐴 ) ( 𝑈 ‘ ( 𝐺𝑛 ) ) ) ) ) ) = ( 𝑇 ‘ ( 𝐴 Σg ( 𝑛 ∈ ℕ0 ↦ ( ( 𝑛 𝑀 ) ( .r𝐴 ) ( 𝑈 ‘ ( 𝐺𝑛 ) ) ) ) ) ) )
130 8 1 2 3 4 12 mat2pmatrhm ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) → 𝑇 ∈ ( 𝐴 RingHom 𝑌 ) )
131 130 3adant3 ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵 ) → 𝑇 ∈ ( 𝐴 RingHom 𝑌 ) )
132 131 ad3antrrr ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵 ) ∧ 𝑠 ∈ ℕ ) ∧ 𝑏 ∈ ( 𝐵m ( 0 ... 𝑠 ) ) ) ∧ 𝑛 ∈ ℕ0 ) → 𝑇 ∈ ( 𝐴 RingHom 𝑌 ) )
133 2 55 5 rhmmul ( ( 𝑇 ∈ ( 𝐴 RingHom 𝑌 ) ∧ ( 𝑛 𝑀 ) ∈ 𝐵 ∧ ( 𝑈 ‘ ( 𝐺𝑛 ) ) ∈ 𝐵 ) → ( 𝑇 ‘ ( ( 𝑛 𝑀 ) ( .r𝐴 ) ( 𝑈 ‘ ( 𝐺𝑛 ) ) ) ) = ( ( 𝑇 ‘ ( 𝑛 𝑀 ) ) × ( 𝑇 ‘ ( 𝑈 ‘ ( 𝐺𝑛 ) ) ) ) )
134 132 44 127 133 syl3anc ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵 ) ∧ 𝑠 ∈ ℕ ) ∧ 𝑏 ∈ ( 𝐵m ( 0 ... 𝑠 ) ) ) ∧ 𝑛 ∈ ℕ0 ) → ( 𝑇 ‘ ( ( 𝑛 𝑀 ) ( .r𝐴 ) ( 𝑈 ‘ ( 𝐺𝑛 ) ) ) ) = ( ( 𝑇 ‘ ( 𝑛 𝑀 ) ) × ( 𝑇 ‘ ( 𝑈 ‘ ( 𝐺𝑛 ) ) ) ) )
135 8 1 2 3 4 12 mat2pmatmhm ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) → 𝑇 ∈ ( ( mulGrp ‘ 𝐴 ) MndHom ( mulGrp ‘ 𝑌 ) ) )
136 135 3adant3 ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵 ) → 𝑇 ∈ ( ( mulGrp ‘ 𝐴 ) MndHom ( mulGrp ‘ 𝑌 ) ) )
137 136 ad3antrrr ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵 ) ∧ 𝑠 ∈ ℕ ) ∧ 𝑏 ∈ ( 𝐵m ( 0 ... 𝑠 ) ) ) ∧ 𝑛 ∈ ℕ0 ) → 𝑇 ∈ ( ( mulGrp ‘ 𝐴 ) MndHom ( mulGrp ‘ 𝑌 ) ) )
138 36 16 17 mhmmulg ( ( 𝑇 ∈ ( ( mulGrp ‘ 𝐴 ) MndHom ( mulGrp ‘ 𝑌 ) ) ∧ 𝑛 ∈ ℕ0𝑀𝐵 ) → ( 𝑇 ‘ ( 𝑛 𝑀 ) ) = ( 𝑛 𝐸 ( 𝑇𝑀 ) ) )
139 137 41 43 138 syl3anc ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵 ) ∧ 𝑠 ∈ ℕ ) ∧ 𝑏 ∈ ( 𝐵m ( 0 ... 𝑠 ) ) ) ∧ 𝑛 ∈ ℕ0 ) → ( 𝑇 ‘ ( 𝑛 𝑀 ) ) = ( 𝑛 𝐸 ( 𝑇𝑀 ) ) )
140 19 ad3antrrr ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵 ) ∧ 𝑠 ∈ ℕ ) ∧ 𝑏 ∈ ( 𝐵m ( 0 ... 𝑠 ) ) ) ∧ 𝑛 ∈ ℕ0 ) → 𝑁 ∈ Fin )
141 22 ad3antrrr ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵 ) ∧ 𝑠 ∈ ℕ ) ∧ 𝑏 ∈ ( 𝐵m ( 0 ... 𝑠 ) ) ) ∧ 𝑛 ∈ ℕ0 ) → 𝑅 ∈ Ring )
142 45 15 8 m2cpminvid2 ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ ( 𝐺𝑛 ) ∈ ( 𝑁 ConstPolyMat 𝑅 ) ) → ( 𝑇 ‘ ( 𝑈 ‘ ( 𝐺𝑛 ) ) ) = ( 𝐺𝑛 ) )
143 140 141 53 142 syl3anc ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵 ) ∧ 𝑠 ∈ ℕ ) ∧ 𝑏 ∈ ( 𝐵m ( 0 ... 𝑠 ) ) ) ∧ 𝑛 ∈ ℕ0 ) → ( 𝑇 ‘ ( 𝑈 ‘ ( 𝐺𝑛 ) ) ) = ( 𝐺𝑛 ) )
144 139 143 oveq12d ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵 ) ∧ 𝑠 ∈ ℕ ) ∧ 𝑏 ∈ ( 𝐵m ( 0 ... 𝑠 ) ) ) ∧ 𝑛 ∈ ℕ0 ) → ( ( 𝑇 ‘ ( 𝑛 𝑀 ) ) × ( 𝑇 ‘ ( 𝑈 ‘ ( 𝐺𝑛 ) ) ) ) = ( ( 𝑛 𝐸 ( 𝑇𝑀 ) ) × ( 𝐺𝑛 ) ) )
145 134 144 eqtrd ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵 ) ∧ 𝑠 ∈ ℕ ) ∧ 𝑏 ∈ ( 𝐵m ( 0 ... 𝑠 ) ) ) ∧ 𝑛 ∈ ℕ0 ) → ( 𝑇 ‘ ( ( 𝑛 𝑀 ) ( .r𝐴 ) ( 𝑈 ‘ ( 𝐺𝑛 ) ) ) ) = ( ( 𝑛 𝐸 ( 𝑇𝑀 ) ) × ( 𝐺𝑛 ) ) )
146 145 mpteq2dva ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵 ) ∧ 𝑠 ∈ ℕ ) ∧ 𝑏 ∈ ( 𝐵m ( 0 ... 𝑠 ) ) ) → ( 𝑛 ∈ ℕ0 ↦ ( 𝑇 ‘ ( ( 𝑛 𝑀 ) ( .r𝐴 ) ( 𝑈 ‘ ( 𝐺𝑛 ) ) ) ) ) = ( 𝑛 ∈ ℕ0 ↦ ( ( 𝑛 𝐸 ( 𝑇𝑀 ) ) × ( 𝐺𝑛 ) ) ) )
147 146 oveq2d ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵 ) ∧ 𝑠 ∈ ℕ ) ∧ 𝑏 ∈ ( 𝐵m ( 0 ... 𝑠 ) ) ) → ( 𝑌 Σg ( 𝑛 ∈ ℕ0 ↦ ( 𝑇 ‘ ( ( 𝑛 𝑀 ) ( .r𝐴 ) ( 𝑈 ‘ ( 𝐺𝑛 ) ) ) ) ) ) = ( 𝑌 Σg ( 𝑛 ∈ ℕ0 ↦ ( ( 𝑛 𝐸 ( 𝑇𝑀 ) ) × ( 𝐺𝑛 ) ) ) ) )
148 129 147 eqtr3d ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵 ) ∧ 𝑠 ∈ ℕ ) ∧ 𝑏 ∈ ( 𝐵m ( 0 ... 𝑠 ) ) ) → ( 𝑇 ‘ ( 𝐴 Σg ( 𝑛 ∈ ℕ0 ↦ ( ( 𝑛 𝑀 ) ( .r𝐴 ) ( 𝑈 ‘ ( 𝐺𝑛 ) ) ) ) ) ) = ( 𝑌 Σg ( 𝑛 ∈ ℕ0 ↦ ( ( 𝑛 𝐸 ( 𝑇𝑀 ) ) × ( 𝐺𝑛 ) ) ) ) )
149 148 fveq2d ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵 ) ∧ 𝑠 ∈ ℕ ) ∧ 𝑏 ∈ ( 𝐵m ( 0 ... 𝑠 ) ) ) → ( 𝑈 ‘ ( 𝑇 ‘ ( 𝐴 Σg ( 𝑛 ∈ ℕ0 ↦ ( ( 𝑛 𝑀 ) ( .r𝐴 ) ( 𝑈 ‘ ( 𝐺𝑛 ) ) ) ) ) ) ) = ( 𝑈 ‘ ( 𝑌 Σg ( 𝑛 ∈ ℕ0 ↦ ( ( 𝑛 𝐸 ( 𝑇𝑀 ) ) × ( 𝐺𝑛 ) ) ) ) ) )
150 113 149 eqtr3d ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵 ) ∧ 𝑠 ∈ ℕ ) ∧ 𝑏 ∈ ( 𝐵m ( 0 ... 𝑠 ) ) ) → ( 𝐴 Σg ( 𝑛 ∈ ℕ0 ↦ ( ( 𝑛 𝑀 ) ( .r𝐴 ) ( 𝑈 ‘ ( 𝐺𝑛 ) ) ) ) ) = ( 𝑈 ‘ ( 𝑌 Σg ( 𝑛 ∈ ℕ0 ↦ ( ( 𝑛 𝐸 ( 𝑇𝑀 ) ) × ( 𝐺𝑛 ) ) ) ) ) )
151 18 150 sylan9eqr ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵 ) ∧ 𝑠 ∈ ℕ ) ∧ 𝑏 ∈ ( 𝐵m ( 0 ... 𝑠 ) ) ) ∧ ( 𝐴 Σg ( 𝑛 ∈ ℕ0 ↦ ( ( ( coe1𝐾 ) ‘ 𝑛 ) ( 𝑛 𝑀 ) ) ) ) = ( 𝐴 Σg ( 𝑛 ∈ ℕ0 ↦ ( ( 𝑛 𝑀 ) ( .r𝐴 ) ( 𝑈 ‘ ( 𝐺𝑛 ) ) ) ) ) ) → ( 𝐴 Σg ( 𝑛 ∈ ℕ0 ↦ ( ( ( coe1𝐾 ) ‘ 𝑛 ) ( 𝑛 𝑀 ) ) ) ) = ( 𝑈 ‘ ( 𝑌 Σg ( 𝑛 ∈ ℕ0 ↦ ( ( 𝑛 𝐸 ( 𝑇𝑀 ) ) × ( 𝐺𝑛 ) ) ) ) ) )
152 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 55 cayhamlem3 ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵 ) → ∃ 𝑠 ∈ ℕ ∃ 𝑏 ∈ ( 𝐵m ( 0 ... 𝑠 ) ) ( 𝐴 Σg ( 𝑛 ∈ ℕ0 ↦ ( ( ( coe1𝐾 ) ‘ 𝑛 ) ( 𝑛 𝑀 ) ) ) ) = ( 𝐴 Σg ( 𝑛 ∈ ℕ0 ↦ ( ( 𝑛 𝑀 ) ( .r𝐴 ) ( 𝑈 ‘ ( 𝐺𝑛 ) ) ) ) ) )
153 151 152 reximddv2 ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵 ) → ∃ 𝑠 ∈ ℕ ∃ 𝑏 ∈ ( 𝐵m ( 0 ... 𝑠 ) ) ( 𝐴 Σg ( 𝑛 ∈ ℕ0 ↦ ( ( ( coe1𝐾 ) ‘ 𝑛 ) ( 𝑛 𝑀 ) ) ) ) = ( 𝑈 ‘ ( 𝑌 Σg ( 𝑛 ∈ ℕ0 ↦ ( ( 𝑛 𝐸 ( 𝑇𝑀 ) ) × ( 𝐺𝑛 ) ) ) ) ) )