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