Theorem cayhamlem4 23045

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

Hypotheses

Ref	Expression
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

Ref	Expression
cayhamlem4	⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) → ∃𝑠 ∈ ℕ ∃𝑏 ∈ (𝐵 ↑m (0...𝑠))(𝐴 Σg (𝑛 ∈ ℕ0 ↦ (((coe1‘𝐾)‘𝑛) ∗ (𝑛 ↑ 𝑀)))) = (𝑈‘(𝑌 Σg (𝑛 ∈ ℕ0 ↦ ((𝑛𝐸(𝑇‘𝑀)) × (𝐺‘𝑛))))))

Distinct variable groups:   𝐴,𝑛   𝐵,𝑛   𝑛,𝐺   𝑛,𝐾   𝑛,𝑀   𝑛,𝑁   𝑅,𝑛   𝑈,𝑛   𝑛,𝑌   1 ,𝑛   ∗ ,𝑛   𝑛,𝑏,𝑠,𝐴   𝐵,𝑏,𝑠   𝑀,𝑏,𝑠   𝑁,𝑏,𝑠   𝑃,𝑏,𝑛,𝑠   𝑅,𝑏,𝑠   𝑇,𝑏,𝑛,𝑠   𝑛,𝑊   𝑌,𝑏,𝑠   0 ,𝑛   × ,𝑛   − ,𝑏,𝑛,𝑠   ↑ ,𝑛

Allowed substitution hints:   𝐶(𝑛,𝑠,𝑏)   × (𝑠,𝑏)   𝑈(𝑠,𝑏)   1 (𝑠,𝑏)   𝐸(𝑛,𝑠,𝑏)   ↑ (𝑠,𝑏)   𝐺(𝑠,𝑏)   ∗ (𝑠,𝑏)   𝐾(𝑠,𝑏)   𝑊(𝑠,𝑏)   0 (𝑠,𝑏)

Proof of Theorem cayhamlem4

Dummy variables 𝑤 𝑧 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		id 23	. . 3 ⊢ ((𝐴 Σg (𝑛 ∈ ℕ0 ↦ (((coe1‘𝐾)‘𝑛) ∗ (𝑛 ↑ 𝑀)))) = (𝐴 Σg (𝑛 ∈ ℕ0 ↦ ((𝑛 ↑ 𝑀)(.r‘𝐴)(𝑈‘(𝐺‘𝑛))))) → (𝐴 Σg (𝑛 ∈ ℕ0 ↦ (((coe1‘𝐾)‘𝑛) ∗ (𝑛 ↑ 𝑀)))) = (𝐴 Σg (𝑛 ∈ ℕ0 ↦ ((𝑛 ↑ 𝑀)(.r‘𝐴)(𝑈‘(𝐺‘𝑛))))))
2		simp1 1154	. . . . . 6 ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) → 𝑁 ∈ Fin)
3	2	ad2antrr 738	. . . . 5 ⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ 𝑠 ∈ ℕ) ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠))) → 𝑁 ∈ Fin)
4		crngring 20322	. . . . . . 7 ⊢ (𝑅 ∈ CRing → 𝑅 ∈ Ring)
5	4	3ad2ant2 1152	. . . . . 6 ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) → 𝑅 ∈ Ring)
6	5	ad2antrr 738	. . . . 5 ⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ 𝑠 ∈ ℕ) ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠))) → 𝑅 ∈ Ring)
7		chcoeffeq.b	. . . . . 6 ⊢ 𝐵 = (Base‘𝐴)
8		eqid 2763	. . . . . 6 ⊢ (0g‘𝐴) = (0g‘𝐴)
9		chcoeffeq.a	. . . . . . . . . . 11 ⊢ 𝐴 = (𝑁 Mat 𝑅)
10	9	matring 22600	. . . . . . . . . 10 ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → 𝐴 ∈ Ring)
11	4, 10	sylan2 604	. . . . . . . . 9 ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) → 𝐴 ∈ Ring)
12		ringcmn 20361	. . . . . . . . 9 ⊢ (𝐴 ∈ Ring → 𝐴 ∈ CMnd)
13	11, 12	syl 18	. . . . . . . 8 ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) → 𝐴 ∈ CMnd)
14	13	3adant3 1150	. . . . . . 7 ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) → 𝐴 ∈ CMnd)
15	14	ad2antrr 738	. . . . . 6 ⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ 𝑠 ∈ ℕ) ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠))) → 𝐴 ∈ CMnd)
16		nn0ex 12505	. . . . . . 7 ⊢ ℕ0 ∈ V
17	16	a1i 11	. . . . . 6 ⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ 𝑠 ∈ ℕ) ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠))) → ℕ0 ∈ V)
18	3, 6, 10	syl2anc 595	. . . . . . . . 9 ⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ 𝑠 ∈ ℕ) ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠))) → 𝐴 ∈ Ring)
19	18	adantr 485	. . . . . . . 8 ⊢ (((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ 𝑠 ∈ ℕ) ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠))) ∧ 𝑛 ∈ ℕ0) → 𝐴 ∈ Ring)
20		eqid 2763	. . . . . . . . . 10 ⊢ (mulGrp‘𝐴) = (mulGrp‘𝐴)
21	20, 7	mgpbas 20216	. . . . . . . . 9 ⊢ 𝐵 = (Base‘(mulGrp‘𝐴))
22		cayhamlem.e1	. . . . . . . . 9 ⊢ ↑ = (.g‘(mulGrp‘𝐴))
23	2, 5, 10	syl2anc 595	. . . . . . . . . . 11 ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) → 𝐴 ∈ Ring)
24	20	ringmgp 20316	. . . . . . . . . . 11 ⊢ (𝐴 ∈ Ring → (mulGrp‘𝐴) ∈ Mnd)
25	23, 24	syl 18	. . . . . . . . . 10 ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) → (mulGrp‘𝐴) ∈ Mnd)
26	25	ad3antrrr 742	. . . . . . . . 9 ⊢ (((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ 𝑠 ∈ ℕ) ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠))) ∧ 𝑛 ∈ ℕ0) → (mulGrp‘𝐴) ∈ Mnd)
27		simpr 489	. . . . . . . . 9 ⊢ (((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ 𝑠 ∈ ℕ) ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠))) ∧ 𝑛 ∈ ℕ0) → 𝑛 ∈ ℕ0)
28		simpll3 1233	. . . . . . . . . 10 ⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ 𝑠 ∈ ℕ) ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠))) → 𝑀 ∈ 𝐵)
29	28	adantr 485	. . . . . . . . 9 ⊢ (((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ 𝑠 ∈ ℕ) ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠))) ∧ 𝑛 ∈ ℕ0) → 𝑀 ∈ 𝐵)
30	21, 22, 26, 27, 29	mulgnn0cld 19156	. . . . . . . 8 ⊢ (((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ 𝑠 ∈ ℕ) ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠))) ∧ 𝑛 ∈ ℕ0) → (𝑛 ↑ 𝑀) ∈ 𝐵)
31		eqid 2763	. . . . . . . . . . . 12 ⊢ (𝑁 ConstPolyMat 𝑅) = (𝑁 ConstPolyMat 𝑅)
32		chcoeffeq.u	. . . . . . . . . . . 12 ⊢ 𝑈 = (𝑁 cPolyMatToMat 𝑅)
33	9, 7, 31, 32	cpm2mf 22909	. . . . . . . . . . 11 ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → 𝑈:(𝑁 ConstPolyMat 𝑅)⟶𝐵)
34	2, 5, 33	syl2anc 595	. . . . . . . . . 10 ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) → 𝑈:(𝑁 ConstPolyMat 𝑅)⟶𝐵)
35	34	ad3antrrr 742	. . . . . . . . 9 ⊢ (((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ 𝑠 ∈ ℕ) ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠))) ∧ 𝑛 ∈ ℕ0) → 𝑈:(𝑁 ConstPolyMat 𝑅)⟶𝐵)
36		simplr 780	. . . . . . . . . . 11 ⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ 𝑠 ∈ ℕ) ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠))) → 𝑠 ∈ ℕ)
37		simpr 489	. . . . . . . . . . 11 ⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ 𝑠 ∈ ℕ) ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠))) → 𝑏 ∈ (𝐵 ↑m (0...𝑠)))
38		chcoeffeq.p	. . . . . . . . . . . 12 ⊢ 𝑃 = (Poly1‘𝑅)
39		chcoeffeq.y	. . . . . . . . . . . 12 ⊢ 𝑌 = (𝑁 Mat 𝑃)
40		chcoeffeq.r	. . . . . . . . . . . 12 ⊢ × = (.r‘𝑌)
41		chcoeffeq.s	. . . . . . . . . . . 12 ⊢ − = (-g‘𝑌)
42		chcoeffeq.0	. . . . . . . . . . . 12 ⊢ 0 = (0g‘𝑌)
43		chcoeffeq.t	. . . . . . . . . . . 12 ⊢ 𝑇 = (𝑁 matToPolyMat 𝑅)
44		chcoeffeq.g	. . . . . . . . . . . 12 ⊢ 𝐺 = (𝑛 ∈ ℕ0 ↦ if(𝑛 = 0, ( 0 − ((𝑇‘𝑀) × (𝑇‘(𝑏‘0)))), if(𝑛 = (𝑠 + 1), (𝑇‘(𝑏‘𝑠)), if((𝑠 + 1) < 𝑛, 0 , ((𝑇‘(𝑏‘(𝑛 − 1))) − ((𝑇‘𝑀) × (𝑇‘(𝑏‘𝑛))))))))
45	9, 7, 38, 39, 40, 41, 42, 43, 44, 31	chfacfisfcpmat 23012	. . . . . . . . . . 11 ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) → 𝐺:ℕ0⟶(𝑁 ConstPolyMat 𝑅))
46	3, 6, 28, 36, 37, 45	syl32anc 1405	. . . . . . . . . 10 ⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ 𝑠 ∈ ℕ) ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠))) → 𝐺:ℕ0⟶(𝑁 ConstPolyMat 𝑅))
47	46	ffvelcdmda 7079	. . . . . . . . 9 ⊢ (((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ 𝑠 ∈ ℕ) ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠))) ∧ 𝑛 ∈ ℕ0) → (𝐺‘𝑛) ∈ (𝑁 ConstPolyMat 𝑅))
48	35, 47	ffvelcdmd 7080	. . . . . . . 8 ⊢ (((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ 𝑠 ∈ ℕ) ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠))) ∧ 𝑛 ∈ ℕ0) → (𝑈‘(𝐺‘𝑛)) ∈ 𝐵)
49		eqid 2763	. . . . . . . . 9 ⊢ (.r‘𝐴) = (.r‘𝐴)
50	7, 49	ringcl 20327	. . . . . . . 8 ⊢ ((𝐴 ∈ Ring ∧ (𝑛 ↑ 𝑀) ∈ 𝐵 ∧ (𝑈‘(𝐺‘𝑛)) ∈ 𝐵) → ((𝑛 ↑ 𝑀)(.r‘𝐴)(𝑈‘(𝐺‘𝑛))) ∈ 𝐵)
51	19, 30, 48, 50	syl3anc 1398	. . . . . . 7 ⊢ (((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ 𝑠 ∈ ℕ) ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠))) ∧ 𝑛 ∈ ℕ0) → ((𝑛 ↑ 𝑀)(.r‘𝐴)(𝑈‘(𝐺‘𝑛))) ∈ 𝐵)
52	51	fmpttd 7110	. . . . . 6 ⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ 𝑠 ∈ ℕ) ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠))) → (𝑛 ∈ ℕ0 ↦ ((𝑛 ↑ 𝑀)(.r‘𝐴)(𝑈‘(𝐺‘𝑛)))):ℕ0⟶𝐵)
53		fvexd 6896	. . . . . . 7 ⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ 𝑠 ∈ ℕ) ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠))) → (0g‘𝐴) ∈ V)
54		ovexd 7445	. . . . . . 7 ⊢ (((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ 𝑠 ∈ ℕ) ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠))) ∧ 𝑛 ∈ ℕ0) → ((𝑛 ↑ 𝑀)(.r‘𝐴)(𝑈‘(𝐺‘𝑛))) ∈ V)
55	9, 7, 38, 39, 40, 41, 42, 43, 44	chfacffsupp 23013	. . . . . . . . 9 ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) → 𝐺 finSupp (0g‘𝑌))
56	55	anassrs 472	. . . . . . . 8 ⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ 𝑠 ∈ ℕ) ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠))) → 𝐺 finSupp (0g‘𝑌))
57		ovex 7443	. . . . . . . . . . . . 13 ⊢ (𝑁 ConstPolyMat 𝑅) ∈ V
58	57, 16	pm3.2i 475	. . . . . . . . . . . 12 ⊢ ((𝑁 ConstPolyMat 𝑅) ∈ V ∧ ℕ0 ∈ V)
59		elmapg 8832	. . . . . . . . . . . 12 ⊢ (((𝑁 ConstPolyMat 𝑅) ∈ V ∧ ℕ0 ∈ V) → (𝐺 ∈ ((𝑁 ConstPolyMat 𝑅) ↑m ℕ0) ↔ 𝐺:ℕ0⟶(𝑁 ConstPolyMat 𝑅)))
60	58, 59	mp1i 14	. . . . . . . . . . 11 ⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ 𝑠 ∈ ℕ) ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠))) → (𝐺 ∈ ((𝑁 ConstPolyMat 𝑅) ↑m ℕ0) ↔ 𝐺:ℕ0⟶(𝑁 ConstPolyMat 𝑅)))
61	46, 60	mpbird 260	. . . . . . . . . 10 ⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ 𝑠 ∈ ℕ) ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠))) → 𝐺 ∈ ((𝑁 ConstPolyMat 𝑅) ↑m ℕ0))
62		fvex 6894	. . . . . . . . . 10 ⊢ (0g‘𝑌) ∈ V
63		fsuppmapnn0ub 14027	. . . . . . . . . 10 ⊢ ((𝐺 ∈ ((𝑁 ConstPolyMat 𝑅) ↑m ℕ0) ∧ (0g‘𝑌) ∈ V) → (𝐺 finSupp (0g‘𝑌) → ∃𝑤 ∈ ℕ0 ∀𝑧 ∈ ℕ0 (𝑤 < 𝑧 → (𝐺‘𝑧) = (0g‘𝑌))))
64	61, 62, 63	sylancl 597	. . . . . . . . 9 ⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ 𝑠 ∈ ℕ) ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠))) → (𝐺 finSupp (0g‘𝑌) → ∃𝑤 ∈ ℕ0 ∀𝑧 ∈ ℕ0 (𝑤 < 𝑧 → (𝐺‘𝑧) = (0g‘𝑌))))
65		csbov12g 7456	. . . . . . . . . . . . . . . . 17 ⊢ (𝑧 ∈ ℕ0 → ⦋𝑧 / 𝑛⦌((𝑛 ↑ 𝑀)(.r‘𝐴)(𝑈‘(𝐺‘𝑛))) = (⦋𝑧 / 𝑛⦌(𝑛 ↑ 𝑀)(.r‘𝐴)⦋𝑧 / 𝑛⦌(𝑈‘(𝐺‘𝑛))))
66		csbov1g 7457	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑧 ∈ ℕ0 → ⦋𝑧 / 𝑛⦌(𝑛 ↑ 𝑀) = (⦋𝑧 / 𝑛⦌𝑛 ↑ 𝑀))
67		csbvarg 4399	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑧 ∈ ℕ0 → ⦋𝑧 / 𝑛⦌𝑛 = 𝑧)
68	67	oveq1d 7425	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑧 ∈ ℕ0 → (⦋𝑧 / 𝑛⦌𝑛 ↑ 𝑀) = (𝑧 ↑ 𝑀))
69	66, 68	eqtrd 2798	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑧 ∈ ℕ0 → ⦋𝑧 / 𝑛⦌(𝑛 ↑ 𝑀) = (𝑧 ↑ 𝑀))
70		csbfv2g 6927	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑧 ∈ ℕ0 → ⦋𝑧 / 𝑛⦌(𝑈‘(𝐺‘𝑛)) = (𝑈‘⦋𝑧 / 𝑛⦌(𝐺‘𝑛)))
71		csbfv 6928	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ⦋𝑧 / 𝑛⦌(𝐺‘𝑛) = (𝐺‘𝑧)
72	71	a1i 11	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑧 ∈ ℕ0 → ⦋𝑧 / 𝑛⦌(𝐺‘𝑛) = (𝐺‘𝑧))
73	72	fveq2d 6885	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑧 ∈ ℕ0 → (𝑈‘⦋𝑧 / 𝑛⦌(𝐺‘𝑛)) = (𝑈‘(𝐺‘𝑧)))
74	70, 73	eqtrd 2798	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑧 ∈ ℕ0 → ⦋𝑧 / 𝑛⦌(𝑈‘(𝐺‘𝑛)) = (𝑈‘(𝐺‘𝑧)))
75	69, 74	oveq12d 7428	. . . . . . . . . . . . . . . . 17 ⊢ (𝑧 ∈ ℕ0 → (⦋𝑧 / 𝑛⦌(𝑛 ↑ 𝑀)(.r‘𝐴)⦋𝑧 / 𝑛⦌(𝑈‘(𝐺‘𝑛))) = ((𝑧 ↑ 𝑀)(.r‘𝐴)(𝑈‘(𝐺‘𝑧))))
76	65, 75	eqtrd 2798	. . . . . . . . . . . . . . . 16 ⊢ (𝑧 ∈ ℕ0 → ⦋𝑧 / 𝑛⦌((𝑛 ↑ 𝑀)(.r‘𝐴)(𝑈‘(𝐺‘𝑛))) = ((𝑧 ↑ 𝑀)(.r‘𝐴)(𝑈‘(𝐺‘𝑧))))
77	76	ad2antlr 739	. . . . . . . . . . . . . . 15 ⊢ ((((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ 𝑠 ∈ ℕ) ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠))) ∧ 𝑧 ∈ ℕ0) ∧ (𝐺‘𝑧) = (0g‘𝑌)) → ⦋𝑧 / 𝑛⦌((𝑛 ↑ 𝑀)(.r‘𝐴)(𝑈‘(𝐺‘𝑛))) = ((𝑧 ↑ 𝑀)(.r‘𝐴)(𝑈‘(𝐺‘𝑧))))
78		fveq2 6881	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐺‘𝑧) = (0g‘𝑌) → (𝑈‘(𝐺‘𝑧)) = (𝑈‘(0g‘𝑌)))
79	2, 5	jca 520	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) → (𝑁 ∈ Fin ∧ 𝑅 ∈ Ring))
80	79	adantr 485	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ 𝑠 ∈ ℕ) → (𝑁 ∈ Fin ∧ 𝑅 ∈ Ring))
81		eqid 2763	. . . . . . . . . . . . . . . . . . . 20 ⊢ (0g‘𝑌) = (0g‘𝑌)
82	9, 32, 38, 39, 8, 81	m2cpminv0 22918	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → (𝑈‘(0g‘𝑌)) = (0g‘𝐴))
83	80, 82	syl 18	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ 𝑠 ∈ ℕ) → (𝑈‘(0g‘𝑌)) = (0g‘𝐴))
84	83	ad2antrr 738	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ 𝑠 ∈ ℕ) ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠))) ∧ 𝑧 ∈ ℕ0) → (𝑈‘(0g‘𝑌)) = (0g‘𝐴))
85	78, 84	sylan9eqr 2820	. . . . . . . . . . . . . . . 16 ⊢ ((((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ 𝑠 ∈ ℕ) ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠))) ∧ 𝑧 ∈ ℕ0) ∧ (𝐺‘𝑧) = (0g‘𝑌)) → (𝑈‘(𝐺‘𝑧)) = (0g‘𝐴))
86	85	oveq2d 7426	. . . . . . . . . . . . . . 15 ⊢ ((((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ 𝑠 ∈ ℕ) ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠))) ∧ 𝑧 ∈ ℕ0) ∧ (𝐺‘𝑧) = (0g‘𝑌)) → ((𝑧 ↑ 𝑀)(.r‘𝐴)(𝑈‘(𝐺‘𝑧))) = ((𝑧 ↑ 𝑀)(.r‘𝐴)(0g‘𝐴)))
87	18	adantr 485	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ 𝑠 ∈ ℕ) ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠))) ∧ 𝑧 ∈ ℕ0) → 𝐴 ∈ Ring)
88	25	ad3antrrr 742	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ 𝑠 ∈ ℕ) ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠))) ∧ 𝑧 ∈ ℕ0) → (mulGrp‘𝐴) ∈ Mnd)
89		simpr 489	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ 𝑠 ∈ ℕ) ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠))) ∧ 𝑧 ∈ ℕ0) → 𝑧 ∈ ℕ0)
90	28	adantr 485	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ 𝑠 ∈ ℕ) ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠))) ∧ 𝑧 ∈ ℕ0) → 𝑀 ∈ 𝐵)
91	21, 22, 88, 89, 90	mulgnn0cld 19156	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ 𝑠 ∈ ℕ) ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠))) ∧ 𝑧 ∈ ℕ0) → (𝑧 ↑ 𝑀) ∈ 𝐵)
92	87, 91	jca 520	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ 𝑠 ∈ ℕ) ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠))) ∧ 𝑧 ∈ ℕ0) → (𝐴 ∈ Ring ∧ (𝑧 ↑ 𝑀) ∈ 𝐵))
93	92	adantr 485	. . . . . . . . . . . . . . . 16 ⊢ ((((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ 𝑠 ∈ ℕ) ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠))) ∧ 𝑧 ∈ ℕ0) ∧ (𝐺‘𝑧) = (0g‘𝑌)) → (𝐴 ∈ Ring ∧ (𝑧 ↑ 𝑀) ∈ 𝐵))
94	7, 49, 8	ringrz 20373	. . . . . . . . . . . . . . . 16 ⊢ ((𝐴 ∈ Ring ∧ (𝑧 ↑ 𝑀) ∈ 𝐵) → ((𝑧 ↑ 𝑀)(.r‘𝐴)(0g‘𝐴)) = (0g‘𝐴))
95	93, 94	syl 18	. . . . . . . . . . . . . . 15 ⊢ ((((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ 𝑠 ∈ ℕ) ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠))) ∧ 𝑧 ∈ ℕ0) ∧ (𝐺‘𝑧) = (0g‘𝑌)) → ((𝑧 ↑ 𝑀)(.r‘𝐴)(0g‘𝐴)) = (0g‘𝐴))
96	77, 86, 95	3eqtrd 2802	. . . . . . . . . . . . . 14 ⊢ ((((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ 𝑠 ∈ ℕ) ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠))) ∧ 𝑧 ∈ ℕ0) ∧ (𝐺‘𝑧) = (0g‘𝑌)) → ⦋𝑧 / 𝑛⦌((𝑛 ↑ 𝑀)(.r‘𝐴)(𝑈‘(𝐺‘𝑛))) = (0g‘𝐴))
97	96	ex 417	. . . . . . . . . . . . 13 ⊢ (((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ 𝑠 ∈ ℕ) ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠))) ∧ 𝑧 ∈ ℕ0) → ((𝐺‘𝑧) = (0g‘𝑌) → ⦋𝑧 / 𝑛⦌((𝑛 ↑ 𝑀)(.r‘𝐴)(𝑈‘(𝐺‘𝑛))) = (0g‘𝐴)))
98	97	adantlr 727	. . . . . . . . . . . 12 ⊢ ((((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ 𝑠 ∈ ℕ) ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠))) ∧ 𝑤 ∈ ℕ0) ∧ 𝑧 ∈ ℕ0) → ((𝐺‘𝑧) = (0g‘𝑌) → ⦋𝑧 / 𝑛⦌((𝑛 ↑ 𝑀)(.r‘𝐴)(𝑈‘(𝐺‘𝑛))) = (0g‘𝐴)))
99	98	imim2d 58	. . . . . . . . . . 11 ⊢ ((((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ 𝑠 ∈ ℕ) ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠))) ∧ 𝑤 ∈ ℕ0) ∧ 𝑧 ∈ ℕ0) → ((𝑤 < 𝑧 → (𝐺‘𝑧) = (0g‘𝑌)) → (𝑤 < 𝑧 → ⦋𝑧 / 𝑛⦌((𝑛 ↑ 𝑀)(.r‘𝐴)(𝑈‘(𝐺‘𝑛))) = (0g‘𝐴))))
100	99	ralimdva 3177	. . . . . . . . . 10 ⊢ (((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ 𝑠 ∈ ℕ) ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠))) ∧ 𝑤 ∈ ℕ0) → (∀𝑧 ∈ ℕ0 (𝑤 < 𝑧 → (𝐺‘𝑧) = (0g‘𝑌)) → ∀𝑧 ∈ ℕ0 (𝑤 < 𝑧 → ⦋𝑧 / 𝑛⦌((𝑛 ↑ 𝑀)(.r‘𝐴)(𝑈‘(𝐺‘𝑛))) = (0g‘𝐴))))
101	100	reximdva 3178	. . . . . . . . 9 ⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ 𝑠 ∈ ℕ) ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠))) → (∃𝑤 ∈ ℕ0 ∀𝑧 ∈ ℕ0 (𝑤 < 𝑧 → (𝐺‘𝑧) = (0g‘𝑌)) → ∃𝑤 ∈ ℕ0 ∀𝑧 ∈ ℕ0 (𝑤 < 𝑧 → ⦋𝑧 / 𝑛⦌((𝑛 ↑ 𝑀)(.r‘𝐴)(𝑈‘(𝐺‘𝑛))) = (0g‘𝐴))))
102	64, 101	syld 48	. . . . . . . 8 ⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ 𝑠 ∈ ℕ) ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠))) → (𝐺 finSupp (0g‘𝑌) → ∃𝑤 ∈ ℕ0 ∀𝑧 ∈ ℕ0 (𝑤 < 𝑧 → ⦋𝑧 / 𝑛⦌((𝑛 ↑ 𝑀)(.r‘𝐴)(𝑈‘(𝐺‘𝑛))) = (0g‘𝐴))))
103	56, 102	mpd 16	. . . . . . 7 ⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ 𝑠 ∈ ℕ) ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠))) → ∃𝑤 ∈ ℕ0 ∀𝑧 ∈ ℕ0 (𝑤 < 𝑧 → ⦋𝑧 / 𝑛⦌((𝑛 ↑ 𝑀)(.r‘𝐴)(𝑈‘(𝐺‘𝑛))) = (0g‘𝐴)))
104	53, 54, 103	mptnn0fsupp 14029	. . . . . 6 ⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ 𝑠 ∈ ℕ) ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠))) → (𝑛 ∈ ℕ0 ↦ ((𝑛 ↑ 𝑀)(.r‘𝐴)(𝑈‘(𝐺‘𝑛)))) finSupp (0g‘𝐴))
105	7, 8, 15, 17, 52, 104	gsumcl 19980	. . . . 5 ⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ 𝑠 ∈ ℕ) ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠))) → (𝐴 Σg (𝑛 ∈ ℕ0 ↦ ((𝑛 ↑ 𝑀)(.r‘𝐴)(𝑈‘(𝐺‘𝑛))))) ∈ 𝐵)
106	32, 9, 7, 43	m2cpminvid 22910	. . . . 5 ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ (𝐴 Σg (𝑛 ∈ ℕ0 ↦ ((𝑛 ↑ 𝑀)(.r‘𝐴)(𝑈‘(𝐺‘𝑛))))) ∈ 𝐵) → (𝑈‘(𝑇‘(𝐴 Σg (𝑛 ∈ ℕ0 ↦ ((𝑛 ↑ 𝑀)(.r‘𝐴)(𝑈‘(𝐺‘𝑛))))))) = (𝐴 Σg (𝑛 ∈ ℕ0 ↦ ((𝑛 ↑ 𝑀)(.r‘𝐴)(𝑈‘(𝐺‘𝑛))))))
107	3, 6, 105, 106	syl3anc 1398	. . . 4 ⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ 𝑠 ∈ ℕ) ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠))) → (𝑈‘(𝑇‘(𝐴 Σg (𝑛 ∈ ℕ0 ↦ ((𝑛 ↑ 𝑀)(.r‘𝐴)(𝑈‘(𝐺‘𝑛))))))) = (𝐴 Σg (𝑛 ∈ ℕ0 ↦ ((𝑛 ↑ 𝑀)(.r‘𝐴)(𝑈‘(𝐺‘𝑛))))))
108	38, 39	pmatring 22849	. . . . . . . . . 10 ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → 𝑌 ∈ Ring)
109	2, 5, 108	syl2anc 595	. . . . . . . . 9 ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) → 𝑌 ∈ Ring)
110		ringmnd 20320	. . . . . . . . 9 ⊢ (𝑌 ∈ Ring → 𝑌 ∈ Mnd)
111	109, 110	syl 18	. . . . . . . 8 ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) → 𝑌 ∈ Mnd)
112	111	ad2antrr 738	. . . . . . 7 ⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ 𝑠 ∈ ℕ) ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠))) → 𝑌 ∈ Mnd)
113		chcoeffeq.w	. . . . . . . . . 10 ⊢ 𝑊 = (Base‘𝑌)
114	43, 9, 7, 38, 39, 113	mat2pmatghm 22887	. . . . . . . . 9 ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → 𝑇 ∈ (𝐴 GrpHom 𝑌))
115	3, 6, 114	syl2anc 595	. . . . . . . 8 ⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ 𝑠 ∈ ℕ) ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠))) → 𝑇 ∈ (𝐴 GrpHom 𝑌))
116		ghmmhm 19291	. . . . . . . 8 ⊢ (𝑇 ∈ (𝐴 GrpHom 𝑌) → 𝑇 ∈ (𝐴 MndHom 𝑌))
117	115, 116	syl 18	. . . . . . 7 ⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ 𝑠 ∈ ℕ) ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠))) → 𝑇 ∈ (𝐴 MndHom 𝑌))
118	23	ad3antrrr 742	. . . . . . . 8 ⊢ (((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ 𝑠 ∈ ℕ) ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠))) ∧ 𝑛 ∈ ℕ0) → 𝐴 ∈ Ring)
119	4, 33	sylan2 604	. . . . . . . . . . 11 ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) → 𝑈:(𝑁 ConstPolyMat 𝑅)⟶𝐵)
120	119	3adant3 1150	. . . . . . . . . 10 ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) → 𝑈:(𝑁 ConstPolyMat 𝑅)⟶𝐵)
121	120	ad3antrrr 742	. . . . . . . . 9 ⊢ (((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ 𝑠 ∈ ℕ) ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠))) ∧ 𝑛 ∈ ℕ0) → 𝑈:(𝑁 ConstPolyMat 𝑅)⟶𝐵)
122	121, 47	ffvelcdmd 7080	. . . . . . . 8 ⊢ (((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ 𝑠 ∈ ℕ) ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠))) ∧ 𝑛 ∈ ℕ0) → (𝑈‘(𝐺‘𝑛)) ∈ 𝐵)
123	118, 30, 122, 50	syl3anc 1398	. . . . . . 7 ⊢ (((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ 𝑠 ∈ ℕ) ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠))) ∧ 𝑛 ∈ ℕ0) → ((𝑛 ↑ 𝑀)(.r‘𝐴)(𝑈‘(𝐺‘𝑛))) ∈ 𝐵)
124	7, 8, 15, 112, 17, 117, 123, 104	gsummptmhm 20005	. . . . . 6 ⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ 𝑠 ∈ ℕ) ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠))) → (𝑌 Σg (𝑛 ∈ ℕ0 ↦ (𝑇‘((𝑛 ↑ 𝑀)(.r‘𝐴)(𝑈‘(𝐺‘𝑛)))))) = (𝑇‘(𝐴 Σg (𝑛 ∈ ℕ0 ↦ ((𝑛 ↑ 𝑀)(.r‘𝐴)(𝑈‘(𝐺‘𝑛)))))))
125	43, 9, 7, 38, 39, 113	mat2pmatrhm 22891	. . . . . . . . . . . 12 ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) → 𝑇 ∈ (𝐴 RingHom 𝑌))
126	125	3adant3 1150	. . . . . . . . . . 11 ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) → 𝑇 ∈ (𝐴 RingHom 𝑌))
127	126	ad3antrrr 742	. . . . . . . . . 10 ⊢ (((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ 𝑠 ∈ ℕ) ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠))) ∧ 𝑛 ∈ ℕ0) → 𝑇 ∈ (𝐴 RingHom 𝑌))
128	7, 49, 40	rhmmul 20568	. . . . . . . . . 10 ⊢ ((𝑇 ∈ (𝐴 RingHom 𝑌) ∧ (𝑛 ↑ 𝑀) ∈ 𝐵 ∧ (𝑈‘(𝐺‘𝑛)) ∈ 𝐵) → (𝑇‘((𝑛 ↑ 𝑀)(.r‘𝐴)(𝑈‘(𝐺‘𝑛)))) = ((𝑇‘(𝑛 ↑ 𝑀)) × (𝑇‘(𝑈‘(𝐺‘𝑛)))))
129	127, 30, 122, 128	syl3anc 1398	. . . . . . . . 9 ⊢ (((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ 𝑠 ∈ ℕ) ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠))) ∧ 𝑛 ∈ ℕ0) → (𝑇‘((𝑛 ↑ 𝑀)(.r‘𝐴)(𝑈‘(𝐺‘𝑛)))) = ((𝑇‘(𝑛 ↑ 𝑀)) × (𝑇‘(𝑈‘(𝐺‘𝑛)))))
130	43, 9, 7, 38, 39, 113	mat2pmatmhm 22890	. . . . . . . . . . . . 13 ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) → 𝑇 ∈ ((mulGrp‘𝐴) MndHom (mulGrp‘𝑌)))
131	130	3adant3 1150	. . . . . . . . . . . 12 ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) → 𝑇 ∈ ((mulGrp‘𝐴) MndHom (mulGrp‘𝑌)))
132	131	ad3antrrr 742	. . . . . . . . . . 11 ⊢ (((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ 𝑠 ∈ ℕ) ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠))) ∧ 𝑛 ∈ ℕ0) → 𝑇 ∈ ((mulGrp‘𝐴) MndHom (mulGrp‘𝑌)))
133		cayhamlem.e2	. . . . . . . . . . . 12 ⊢ 𝐸 = (.g‘(mulGrp‘𝑌))
134	21, 22, 133	mhmmulg 19176	. . . . . . . . . . 11 ⊢ ((𝑇 ∈ ((mulGrp‘𝐴) MndHom (mulGrp‘𝑌)) ∧ 𝑛 ∈ ℕ0 ∧ 𝑀 ∈ 𝐵) → (𝑇‘(𝑛 ↑ 𝑀)) = (𝑛𝐸(𝑇‘𝑀)))
135	132, 27, 29, 134	syl3anc 1398	. . . . . . . . . 10 ⊢ (((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ 𝑠 ∈ ℕ) ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠))) ∧ 𝑛 ∈ ℕ0) → (𝑇‘(𝑛 ↑ 𝑀)) = (𝑛𝐸(𝑇‘𝑀)))
136	2	ad3antrrr 742	. . . . . . . . . . 11 ⊢ (((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ 𝑠 ∈ ℕ) ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠))) ∧ 𝑛 ∈ ℕ0) → 𝑁 ∈ Fin)
137	5	ad3antrrr 742	. . . . . . . . . . 11 ⊢ (((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ 𝑠 ∈ ℕ) ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠))) ∧ 𝑛 ∈ ℕ0) → 𝑅 ∈ Ring)
138	31, 32, 43	m2cpminvid2 22912	. . . . . . . . . . 11 ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ (𝐺‘𝑛) ∈ (𝑁 ConstPolyMat 𝑅)) → (𝑇‘(𝑈‘(𝐺‘𝑛))) = (𝐺‘𝑛))
139	136, 137, 47, 138	syl3anc 1398	. . . . . . . . . 10 ⊢ (((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ 𝑠 ∈ ℕ) ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠))) ∧ 𝑛 ∈ ℕ0) → (𝑇‘(𝑈‘(𝐺‘𝑛))) = (𝐺‘𝑛))
140	135, 139	oveq12d 7428	. . . . . . . . 9 ⊢ (((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ 𝑠 ∈ ℕ) ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠))) ∧ 𝑛 ∈ ℕ0) → ((𝑇‘(𝑛 ↑ 𝑀)) × (𝑇‘(𝑈‘(𝐺‘𝑛)))) = ((𝑛𝐸(𝑇‘𝑀)) × (𝐺‘𝑛)))
141	129, 140	eqtrd 2798	. . . . . . . 8 ⊢ (((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ 𝑠 ∈ ℕ) ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠))) ∧ 𝑛 ∈ ℕ0) → (𝑇‘((𝑛 ↑ 𝑀)(.r‘𝐴)(𝑈‘(𝐺‘𝑛)))) = ((𝑛𝐸(𝑇‘𝑀)) × (𝐺‘𝑛)))
142	141	mpteq2dva 5204	. . . . . . 7 ⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ 𝑠 ∈ ℕ) ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠))) → (𝑛 ∈ ℕ0 ↦ (𝑇‘((𝑛 ↑ 𝑀)(.r‘𝐴)(𝑈‘(𝐺‘𝑛))))) = (𝑛 ∈ ℕ0 ↦ ((𝑛𝐸(𝑇‘𝑀)) × (𝐺‘𝑛))))
143	142	oveq2d 7426	. . . . . 6 ⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ 𝑠 ∈ ℕ) ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠))) → (𝑌 Σg (𝑛 ∈ ℕ0 ↦ (𝑇‘((𝑛 ↑ 𝑀)(.r‘𝐴)(𝑈‘(𝐺‘𝑛)))))) = (𝑌 Σg (𝑛 ∈ ℕ0 ↦ ((𝑛𝐸(𝑇‘𝑀)) × (𝐺‘𝑛)))))
144	124, 143	eqtr3d 2800	. . . . 5 ⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ 𝑠 ∈ ℕ) ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠))) → (𝑇‘(𝐴 Σg (𝑛 ∈ ℕ0 ↦ ((𝑛 ↑ 𝑀)(.r‘𝐴)(𝑈‘(𝐺‘𝑛)))))) = (𝑌 Σg (𝑛 ∈ ℕ0 ↦ ((𝑛𝐸(𝑇‘𝑀)) × (𝐺‘𝑛)))))
145	144	fveq2d 6885	. . . 4 ⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ 𝑠 ∈ ℕ) ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠))) → (𝑈‘(𝑇‘(𝐴 Σg (𝑛 ∈ ℕ0 ↦ ((𝑛 ↑ 𝑀)(.r‘𝐴)(𝑈‘(𝐺‘𝑛))))))) = (𝑈‘(𝑌 Σg (𝑛 ∈ ℕ0 ↦ ((𝑛𝐸(𝑇‘𝑀)) × (𝐺‘𝑛))))))
146	107, 145	eqtr3d 2800	. . 3 ⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ 𝑠 ∈ ℕ) ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠))) → (𝐴 Σg (𝑛 ∈ ℕ0 ↦ ((𝑛 ↑ 𝑀)(.r‘𝐴)(𝑈‘(𝐺‘𝑛))))) = (𝑈‘(𝑌 Σg (𝑛 ∈ ℕ0 ↦ ((𝑛𝐸(𝑇‘𝑀)) × (𝐺‘𝑛))))))
147	1, 146	sylan9eqr 2820	. 2 ⊢ (((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ 𝑠 ∈ ℕ) ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠))) ∧ (𝐴 Σg (𝑛 ∈ ℕ0 ↦ (((coe1‘𝐾)‘𝑛) ∗ (𝑛 ↑ 𝑀)))) = (𝐴 Σg (𝑛 ∈ ℕ0 ↦ ((𝑛 ↑ 𝑀)(.r‘𝐴)(𝑈‘(𝐺‘𝑛)))))) → (𝐴 Σg (𝑛 ∈ ℕ0 ↦ (((coe1‘𝐾)‘𝑛) ∗ (𝑛 ↑ 𝑀)))) = (𝑈‘(𝑌 Σg (𝑛 ∈ ℕ0 ↦ ((𝑛𝐸(𝑇‘𝑀)) × (𝐺‘𝑛))))))
148		chcoeffeq.c	. . 3 ⊢ 𝐶 = (𝑁 CharPlyMat 𝑅)
149		chcoeffeq.k	. . 3 ⊢ 𝐾 = (𝐶‘𝑀)
150		chcoeffeq.1	. . 3 ⊢ 1 = (1r‘𝐴)
151		chcoeffeq.m	. . 3 ⊢ ∗ = ( ·𝑠 ‘𝐴)
152	9, 7, 38, 39, 40, 41, 42, 43, 148, 149, 44, 113, 150, 151, 32, 22, 49	cayhamlem3 23044	. 2 ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) → ∃𝑠 ∈ ℕ ∃𝑏 ∈ (𝐵 ↑m (0...𝑠))(𝐴 Σg (𝑛 ∈ ℕ0 ↦ (((coe1‘𝐾)‘𝑛) ∗ (𝑛 ↑ 𝑀)))) = (𝐴 Σg (𝑛 ∈ ℕ0 ↦ ((𝑛 ↑ 𝑀)(.r‘𝐴)(𝑈‘(𝐺‘𝑛))))))
153	147, 152	reximddv2 3224	1 ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) → ∃𝑠 ∈ ℕ ∃𝑏 ∈ (𝐵 ↑m (0...𝑠))(𝐴 Σg (𝑛 ∈ ℕ0 ↦ (((coe1‘𝐾)‘𝑛) ∗ (𝑛 ↑ 𝑀)))) = (𝑈‘(𝑌 Σg (𝑛 ∈ ℕ0 ↦ ((𝑛𝐸(𝑇‘𝑀)) × (𝐺‘𝑛))))))

Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 400   ∧ w3a 1103   = wceq 1570   ∈ wcel 2143  ∀wral 3079  ∃wrex 3089  Vcvv 3455  ⦋csb 3853  ifcif 4487   class class class wbr 5109   ↦ cmpt 5192  ⟶wf 6532  ‘cfv 6536  (class class class)co 7410   ↑_m cmap 8820  Fincfn 8939   finSupp cfsupp 9317  0cc0 11095  1c1 11096   + caddc 11098   < clt 11238   − cmin 11436  ℕcn 12228  ℕ₀cn0 12499  ...cfz 13530  Basecbs 17264  ._rcmulr 17306   ·_𝑠 cvsca 17309  0_gc0g 17487   Σ_g cgsu 17488  Mndcmnd 18787   MndHom cmhm 18834  -_gcsg 18997  ._gcmg 19128   GrpHom cghm 19278  CMndccmn 19845  mulGrpcmgp 20211  1_rcur 20258  Ringcrg 20310  CRingccrg 20311   RingHom crh 20547  Poly₁cpl1 22337  coe₁cco1 22338   Mat cmat 22564   ConstPolyMat ccpmat 22860   matToPolyMat cmat2pmat 22861   cPolyMatToMat ccpmat2mat 22862   CharPlyMat cchpmat 22983

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-10 2176  ax-11 2192  ax-12 2213  ax-ext 2735  ax-rep 5238  ax-sep 5257  ax-nul 5269  ax-pow 5336  ax-pr 5404  ax-un 7732  ax-cnex 11151  ax-resscn 11152  ax-1cn 11153  ax-icn 11154  ax-addcl 11155  ax-addrcl 11156  ax-mulcl 11157  ax-mulrcl 11158  ax-mulcom 11159  ax-addass 11160  ax-mulass 11161  ax-distr 11162  ax-i2m1 11163  ax-1ne0 11164  ax-1rid 11165  ax-rnegex 11166  ax-rrecex 11167  ax-cnre 11168  ax-pre-lttri 11169  ax-pre-lttrn 11170  ax-pre-ltadd 11171  ax-pre-mulgt0 11172  ax-addf 11174  ax-mulf 11175

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3or 1104  df-3an 1105  df-xor 1542  df-tru 1573  df-fal 1583  df-ex 1810  df-nf 1814  df-sb 2097  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2838  df-nfc 2912  df-ne 2959  df-nel 3065  df-ral 3080  df-rex 3090  df-rmo 3369  df-reu 3370  df-rab 3417  df-v 3457  df-sbc 3745  df-csb 3854  df-dif 3908  df-un 3910  df-in 3912  df-ss 3922  df-pss 3925  df-nul 4287  df-if 4488  df-pw 4564  df-sn 4590  df-pr 4592  df-tp 4594  df-op 4596  df-ot 4598  df-uni 4873  df-int 4913  df-iun 4958  df-iin 4959  df-br 5110  df-opab 5174  df-mpt 5193  df-tr 5219  df-id 5556  df-eprel 5561  df-po 5569  df-so 5570  df-fr 5614  df-se 5615  df-we 5616  df-xp 5667  df-rel 5668  df-cnv 5669  df-co 5670  df-dm 5671  df-rn 5672  df-res 5673  df-ima 5674  df-pred 6302  df-ord 6363  df-on 6364  df-lim 6365  df-suc 6366  df-iota 6492  df-fun 6538  df-fn 6539  df-f 6540  df-f1 6541  df-fo 6542  df-f1o 6543  df-fv 6544  df-isom 6545  df-riota 7367  df-ov 7413  df-oprab 7414  df-mpo 7415  df-of 7674  df-ofr 7675  df-om 7859  df-1st 7982  df-2nd 7983  df-supp 8153  df-tpos 8218  df-cur 8259  df-frecs 8274  df-wrecs 8305  df-recs 8354  df-rdg 8393  df-1o 8449  df-2o 8450  df-er 8690  df-map 8822  df-pm 8823  df-ixp 8892  df-en 8940  df-dom 8941  df-sdom 8942  df-fin 8943  df-fsupp 9318  df-sup 9398  df-oi 9468  df-card 9921  df-pnf 11240  df-mnf 11241  df-xr 11242  df-ltxr 11243  df-le 11244  df-sub 11438  df-neg 11439  df-div 11867  df-nn 12229  df-2 12298  df-3 12299  df-4 12300  df-5 12301  df-6 12302  df-7 12303  df-8 12304  df-9 12305  df-n0 12500  df-xnn0 12573  df-z 12587  df-dec 12707  df-uz 12858  df-rp 13012  df-fz 13531  df-fzo 13679  df-seq 14034  df-exp 14094  df-hash 14363  df-word 14547  df-lsw 14596  df-concat 14604  df-s1 14630  df-substr 14675  df-pfx 14705  df-splice 14783  df-reverse 14792  df-s2 14881  df-struct 17202  df-sets 17219  df-slot 17237  df-ndx 17249  df-base 17265  df-ress 17286  df-plusg 17318  df-mulr 17319  df-starv 17320  df-sca 17321  df-vsca 17322  df-ip 17323  df-tset 17324  df-ple 17325  df-ds 17327  df-unif 17328  df-hom 17329  df-cco 17330  df-0g 17489  df-gsum 17490  df-prds 17495  df-pws 17497  df-mre 17633  df-mrc 17634  df-acs 17636  df-mgm 18693  df-sgrp 18772  df-mnd 18788  df-mhm 18836  df-submnd 18837  df-efmnd 18923  df-grp 18998  df-minusg 18999  df-sbg 19000  df-mulg 19129  df-subg 19184  df-ghm 19279  df-gim 19324  df-cntz 19382  df-oppg 19411  df-symg 19435  df-pmtr 19507  df-psgn 19556  df-evpm 19557  df-cmn 19847  df-abl 19848  df-mgp 20212  df-rng 20226  df-ur 20259  df-srg 20264  df-ring 20312  df-cring 20313  df-oppr 20415  df-dvdsr 20435  df-unit 20436  df-invr 20466  df-dvr 20479  df-rhm 20550  df-subrng 20645  df-subrg 20669  df-drng 20829  df-lmod 20983  df-lss 21053  df-sra 21294  df-rgmod 21295  df-cnfld 21523  df-zring 21597  df-zrh 21653  df-dsmm 21882  df-frlm 21897  df-assa 22003  df-ascl 22005  df-psr 22059  df-mvr 22060  df-mpl 22061  df-opsr 22063  df-psr1 22340  df-vr1 22341  df-ply1 22342  df-coe1 22343  df-mamu 22548  df-mat 22565  df-mdet 22742  df-madu 22791  df-cpmat 22863  df-mat2pmat 22864  df-cpmat2mat 22865  df-decpmat 22920  df-pm2mp 22950  df-chpmat 22984

This theorem is referenced by:  cayleyhamilton0  23046  cayleyhamiltonALT  23048