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 𝑅 ) ↑m ℕ0 ) ↔ 𝐺 : ℕ0 ⟶ ( 𝑁 ConstPolyMat 𝑅 ) ) )
66 64 65 mp1i ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑠 ∈ ℕ ) ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) → ( 𝐺 ∈ ( ( 𝑁 ConstPolyMat 𝑅 ) ↑m ℕ0 ) ↔ 𝐺 : ℕ0 ⟶ ( 𝑁 ConstPolyMat 𝑅 ) ) )
67 52 66 mpbird ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑠 ∈ ℕ ) ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) → 𝐺 ∈ ( ( 𝑁 ConstPolyMat 𝑅 ) ↑m ℕ0 ) )
68 fvex ⊢ ( 0g ‘ 𝑌 ) ∈ V
69 fsuppmapnn0ub ⊢ ( ( 𝐺 ∈ ( ( 𝑁 ConstPolyMat 𝑅 ) ↑m ℕ0 ) ∧ ( 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 ↦ ( ( 𝑛 𝐸 ( 𝑇 ‘ 𝑀 ) ) × ( 𝐺 ‘ 𝑛 ) ) ) ) ) )