Theorem cayhamlem4 22844

Description: Lemma for cayleyhamilton 22846. (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 22	. . 3 ⊢ ((𝐴 Σg (𝑛 ∈ ℕ0 ↦ (((coe1‘𝐾)‘𝑛) ∗ (𝑛 ↑ 𝑀)))) = (𝐴 Σg (𝑛 ∈ ℕ0 ↦ ((𝑛 ↑ 𝑀)(.r‘𝐴)(𝑈‘(𝐺‘𝑛))))) → (𝐴 Σg (𝑛 ∈ ℕ0 ↦ (((coe1‘𝐾)‘𝑛) ∗ (𝑛 ↑ 𝑀)))) = (𝐴 Σg (𝑛 ∈ ℕ0 ↦ ((𝑛 ↑ 𝑀)(.r‘𝐴)(𝑈‘(𝐺‘𝑛))))))
2		simp1 1137	. . . . . 6 ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) → 𝑁 ∈ Fin)
3	2	ad2antrr 727	. . . . 5 ⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ 𝑠 ∈ ℕ) ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠))) → 𝑁 ∈ Fin)
4		crngring 20192	. . . . . . 7 ⊢ (𝑅 ∈ CRing → 𝑅 ∈ Ring)
5	4	3ad2ant2 1135	. . . . . 6 ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) → 𝑅 ∈ Ring)
6	5	ad2antrr 727	. . . . 5 ⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ 𝑠 ∈ ℕ) ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠))) → 𝑅 ∈ Ring)
7		chcoeffeq.b	. . . . . 6 ⊢ 𝐵 = (Base‘𝐴)
8		eqid 2737	. . . . . 6 ⊢ (0g‘𝐴) = (0g‘𝐴)
9		chcoeffeq.a	. . . . . . . . . . 11 ⊢ 𝐴 = (𝑁 Mat 𝑅)
10	9	matring 22399	. . . . . . . . . 10 ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → 𝐴 ∈ Ring)
11	4, 10	sylan2 594	. . . . . . . . 9 ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) → 𝐴 ∈ Ring)
12		ringcmn 20229	. . . . . . . . 9 ⊢ (𝐴 ∈ Ring → 𝐴 ∈ CMnd)
13	11, 12	syl 17	. . . . . . . 8 ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) → 𝐴 ∈ CMnd)
14	13	3adant3 1133	. . . . . . 7 ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) → 𝐴 ∈ CMnd)
15	14	ad2antrr 727	. . . . . 6 ⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ 𝑠 ∈ ℕ) ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠))) → 𝐴 ∈ CMnd)
16		nn0ex 12419	. . . . . . 7 ⊢ ℕ0 ∈ V
17	16	a1i 11	. . . . . 6 ⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ 𝑠 ∈ ℕ) ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠))) → ℕ0 ∈ V)
18	3, 6, 10	syl2anc 585	. . . . . . . . 9 ⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ 𝑠 ∈ ℕ) ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠))) → 𝐴 ∈ Ring)
19	18	adantr 480	. . . . . . . 8 ⊢ (((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ 𝑠 ∈ ℕ) ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠))) ∧ 𝑛 ∈ ℕ0) → 𝐴 ∈ Ring)
20		eqid 2737	. . . . . . . . . 10 ⊢ (mulGrp‘𝐴) = (mulGrp‘𝐴)
21	20, 7	mgpbas 20092	. . . . . . . . 9 ⊢ 𝐵 = (Base‘(mulGrp‘𝐴))
22		cayhamlem.e1	. . . . . . . . 9 ⊢ ↑ = (.g‘(mulGrp‘𝐴))
23	2, 5, 10	syl2anc 585	. . . . . . . . . . 11 ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) → 𝐴 ∈ Ring)
24	20	ringmgp 20186	. . . . . . . . . . 11 ⊢ (𝐴 ∈ Ring → (mulGrp‘𝐴) ∈ Mnd)
25	23, 24	syl 17	. . . . . . . . . 10 ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) → (mulGrp‘𝐴) ∈ Mnd)
26	25	ad3antrrr 731	. . . . . . . . 9 ⊢ (((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ 𝑠 ∈ ℕ) ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠))) ∧ 𝑛 ∈ ℕ0) → (mulGrp‘𝐴) ∈ Mnd)
27		simpr 484	. . . . . . . . 9 ⊢ (((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ 𝑠 ∈ ℕ) ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠))) ∧ 𝑛 ∈ ℕ0) → 𝑛 ∈ ℕ0)
28		simpll3 1216	. . . . . . . . . 10 ⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ 𝑠 ∈ ℕ) ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠))) → 𝑀 ∈ 𝐵)
29	28	adantr 480	. . . . . . . . 9 ⊢ (((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ 𝑠 ∈ ℕ) ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠))) ∧ 𝑛 ∈ ℕ0) → 𝑀 ∈ 𝐵)
30	21, 22, 26, 27, 29	mulgnn0cld 19037	. . . . . . . 8 ⊢ (((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ 𝑠 ∈ ℕ) ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠))) ∧ 𝑛 ∈ ℕ0) → (𝑛 ↑ 𝑀) ∈ 𝐵)
31		eqid 2737	. . . . . . . . . . . 12 ⊢ (𝑁 ConstPolyMat 𝑅) = (𝑁 ConstPolyMat 𝑅)
32		chcoeffeq.u	. . . . . . . . . . . 12 ⊢ 𝑈 = (𝑁 cPolyMatToMat 𝑅)
33	9, 7, 31, 32	cpm2mf 22708	. . . . . . . . . . 11 ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → 𝑈:(𝑁 ConstPolyMat 𝑅)⟶𝐵)
34	2, 5, 33	syl2anc 585	. . . . . . . . . 10 ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) → 𝑈:(𝑁 ConstPolyMat 𝑅)⟶𝐵)
35	34	ad3antrrr 731	. . . . . . . . 9 ⊢ (((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ 𝑠 ∈ ℕ) ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠))) ∧ 𝑛 ∈ ℕ0) → 𝑈:(𝑁 ConstPolyMat 𝑅)⟶𝐵)
36		simplr 769	. . . . . . . . . . 11 ⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ 𝑠 ∈ ℕ) ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠))) → 𝑠 ∈ ℕ)
37		simpr 484	. . . . . . . . . . 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 22811	. . . . . . . . . . 11 ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) → 𝐺:ℕ0⟶(𝑁 ConstPolyMat 𝑅))
46	3, 6, 28, 36, 37, 45	syl32anc 1381	. . . . . . . . . 10 ⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ 𝑠 ∈ ℕ) ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠))) → 𝐺:ℕ0⟶(𝑁 ConstPolyMat 𝑅))
47	46	ffvelcdmda 7038	. . . . . . . . 9 ⊢ (((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ 𝑠 ∈ ℕ) ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠))) ∧ 𝑛 ∈ ℕ0) → (𝐺‘𝑛) ∈ (𝑁 ConstPolyMat 𝑅))
48	35, 47	ffvelcdmd 7039	. . . . . . . 8 ⊢ (((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ 𝑠 ∈ ℕ) ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠))) ∧ 𝑛 ∈ ℕ0) → (𝑈‘(𝐺‘𝑛)) ∈ 𝐵)
49		eqid 2737	. . . . . . . . 9 ⊢ (.r‘𝐴) = (.r‘𝐴)
50	7, 49	ringcl 20197	. . . . . . . 8 ⊢ ((𝐴 ∈ Ring ∧ (𝑛 ↑ 𝑀) ∈ 𝐵 ∧ (𝑈‘(𝐺‘𝑛)) ∈ 𝐵) → ((𝑛 ↑ 𝑀)(.r‘𝐴)(𝑈‘(𝐺‘𝑛))) ∈ 𝐵)
51	19, 30, 48, 50	syl3anc 1374	. . . . . . 7 ⊢ (((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ 𝑠 ∈ ℕ) ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠))) ∧ 𝑛 ∈ ℕ0) → ((𝑛 ↑ 𝑀)(.r‘𝐴)(𝑈‘(𝐺‘𝑛))) ∈ 𝐵)
52	51	fmpttd 7069	. . . . . 6 ⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ 𝑠 ∈ ℕ) ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠))) → (𝑛 ∈ ℕ0 ↦ ((𝑛 ↑ 𝑀)(.r‘𝐴)(𝑈‘(𝐺‘𝑛)))):ℕ0⟶𝐵)
53		fvexd 6857	. . . . . . 7 ⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ 𝑠 ∈ ℕ) ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠))) → (0g‘𝐴) ∈ V)
54		ovexd 7403	. . . . . . 7 ⊢ (((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ 𝑠 ∈ ℕ) ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠))) ∧ 𝑛 ∈ ℕ0) → ((𝑛 ↑ 𝑀)(.r‘𝐴)(𝑈‘(𝐺‘𝑛))) ∈ V)
55	9, 7, 38, 39, 40, 41, 42, 43, 44	chfacffsupp 22812	. . . . . . . . 9 ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) → 𝐺 finSupp (0g‘𝑌))
56	55	anassrs 467	. . . . . . . 8 ⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ 𝑠 ∈ ℕ) ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠))) → 𝐺 finSupp (0g‘𝑌))
57		ovex 7401	. . . . . . . . . . . . 13 ⊢ (𝑁 ConstPolyMat 𝑅) ∈ V
58	57, 16	pm3.2i 470	. . . . . . . . . . . 12 ⊢ ((𝑁 ConstPolyMat 𝑅) ∈ V ∧ ℕ0 ∈ V)
59		elmapg 8788	. . . . . . . . . . . 12 ⊢ (((𝑁 ConstPolyMat 𝑅) ∈ V ∧ ℕ0 ∈ V) → (𝐺 ∈ ((𝑁 ConstPolyMat 𝑅) ↑m ℕ0) ↔ 𝐺:ℕ0⟶(𝑁 ConstPolyMat 𝑅)))
60	58, 59	mp1i 13	. . . . . . . . . . 11 ⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ 𝑠 ∈ ℕ) ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠))) → (𝐺 ∈ ((𝑁 ConstPolyMat 𝑅) ↑m ℕ0) ↔ 𝐺:ℕ0⟶(𝑁 ConstPolyMat 𝑅)))
61	46, 60	mpbird 257	. . . . . . . . . 10 ⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ 𝑠 ∈ ℕ) ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠))) → 𝐺 ∈ ((𝑁 ConstPolyMat 𝑅) ↑m ℕ0))
62		fvex 6855	. . . . . . . . . 10 ⊢ (0g‘𝑌) ∈ V
63		fsuppmapnn0ub 13930	. . . . . . . . . 10 ⊢ ((𝐺 ∈ ((𝑁 ConstPolyMat 𝑅) ↑m ℕ0) ∧ (0g‘𝑌) ∈ V) → (𝐺 finSupp (0g‘𝑌) → ∃𝑤 ∈ ℕ0 ∀𝑧 ∈ ℕ0 (𝑤 < 𝑧 → (𝐺‘𝑧) = (0g‘𝑌))))
64	61, 62, 63	sylancl 587	. . . . . . . . 9 ⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ 𝑠 ∈ ℕ) ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠))) → (𝐺 finSupp (0g‘𝑌) → ∃𝑤 ∈ ℕ0 ∀𝑧 ∈ ℕ0 (𝑤 < 𝑧 → (𝐺‘𝑧) = (0g‘𝑌))))
65		csbov12g 7414	. . . . . . . . . . . . . . . . 17 ⊢ (𝑧 ∈ ℕ0 → ⦋𝑧 / 𝑛⦌((𝑛 ↑ 𝑀)(.r‘𝐴)(𝑈‘(𝐺‘𝑛))) = (⦋𝑧 / 𝑛⦌(𝑛 ↑ 𝑀)(.r‘𝐴)⦋𝑧 / 𝑛⦌(𝑈‘(𝐺‘𝑛))))
66		csbov1g 7415	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑧 ∈ ℕ0 → ⦋𝑧 / 𝑛⦌(𝑛 ↑ 𝑀) = (⦋𝑧 / 𝑛⦌𝑛 ↑ 𝑀))
67		csbvarg 4388	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑧 ∈ ℕ0 → ⦋𝑧 / 𝑛⦌𝑛 = 𝑧)
68	67	oveq1d 7383	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑧 ∈ ℕ0 → (⦋𝑧 / 𝑛⦌𝑛 ↑ 𝑀) = (𝑧 ↑ 𝑀))
69	66, 68	eqtrd 2772	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑧 ∈ ℕ0 → ⦋𝑧 / 𝑛⦌(𝑛 ↑ 𝑀) = (𝑧 ↑ 𝑀))
70		csbfv2g 6888	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑧 ∈ ℕ0 → ⦋𝑧 / 𝑛⦌(𝑈‘(𝐺‘𝑛)) = (𝑈‘⦋𝑧 / 𝑛⦌(𝐺‘𝑛)))
71		csbfv 6889	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ⦋𝑧 / 𝑛⦌(𝐺‘𝑛) = (𝐺‘𝑧)
72	71	a1i 11	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑧 ∈ ℕ0 → ⦋𝑧 / 𝑛⦌(𝐺‘𝑛) = (𝐺‘𝑧))
73	72	fveq2d 6846	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑧 ∈ ℕ0 → (𝑈‘⦋𝑧 / 𝑛⦌(𝐺‘𝑛)) = (𝑈‘(𝐺‘𝑧)))
74	70, 73	eqtrd 2772	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑧 ∈ ℕ0 → ⦋𝑧 / 𝑛⦌(𝑈‘(𝐺‘𝑛)) = (𝑈‘(𝐺‘𝑧)))
75	69, 74	oveq12d 7386	. . . . . . . . . . . . . . . . 17 ⊢ (𝑧 ∈ ℕ0 → (⦋𝑧 / 𝑛⦌(𝑛 ↑ 𝑀)(.r‘𝐴)⦋𝑧 / 𝑛⦌(𝑈‘(𝐺‘𝑛))) = ((𝑧 ↑ 𝑀)(.r‘𝐴)(𝑈‘(𝐺‘𝑧))))
76	65, 75	eqtrd 2772	. . . . . . . . . . . . . . . 16 ⊢ (𝑧 ∈ ℕ0 → ⦋𝑧 / 𝑛⦌((𝑛 ↑ 𝑀)(.r‘𝐴)(𝑈‘(𝐺‘𝑛))) = ((𝑧 ↑ 𝑀)(.r‘𝐴)(𝑈‘(𝐺‘𝑧))))
77	76	ad2antlr 728	. . . . . . . . . . . . . . 15 ⊢ ((((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ 𝑠 ∈ ℕ) ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠))) ∧ 𝑧 ∈ ℕ0) ∧ (𝐺‘𝑧) = (0g‘𝑌)) → ⦋𝑧 / 𝑛⦌((𝑛 ↑ 𝑀)(.r‘𝐴)(𝑈‘(𝐺‘𝑛))) = ((𝑧 ↑ 𝑀)(.r‘𝐴)(𝑈‘(𝐺‘𝑧))))
78		fveq2 6842	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐺‘𝑧) = (0g‘𝑌) → (𝑈‘(𝐺‘𝑧)) = (𝑈‘(0g‘𝑌)))
79	2, 5	jca 511	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) → (𝑁 ∈ Fin ∧ 𝑅 ∈ Ring))
80	79	adantr 480	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ 𝑠 ∈ ℕ) → (𝑁 ∈ Fin ∧ 𝑅 ∈ Ring))
81		eqid 2737	. . . . . . . . . . . . . . . . . . . 20 ⊢ (0g‘𝑌) = (0g‘𝑌)
82	9, 32, 38, 39, 8, 81	m2cpminv0 22717	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → (𝑈‘(0g‘𝑌)) = (0g‘𝐴))
83	80, 82	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ 𝑠 ∈ ℕ) → (𝑈‘(0g‘𝑌)) = (0g‘𝐴))
84	83	ad2antrr 727	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ 𝑠 ∈ ℕ) ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠))) ∧ 𝑧 ∈ ℕ0) → (𝑈‘(0g‘𝑌)) = (0g‘𝐴))
85	78, 84	sylan9eqr 2794	. . . . . . . . . . . . . . . 16 ⊢ ((((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ 𝑠 ∈ ℕ) ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠))) ∧ 𝑧 ∈ ℕ0) ∧ (𝐺‘𝑧) = (0g‘𝑌)) → (𝑈‘(𝐺‘𝑧)) = (0g‘𝐴))
86	85	oveq2d 7384	. . . . . . . . . . . . . . 15 ⊢ ((((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ 𝑠 ∈ ℕ) ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠))) ∧ 𝑧 ∈ ℕ0) ∧ (𝐺‘𝑧) = (0g‘𝑌)) → ((𝑧 ↑ 𝑀)(.r‘𝐴)(𝑈‘(𝐺‘𝑧))) = ((𝑧 ↑ 𝑀)(.r‘𝐴)(0g‘𝐴)))
87	18	adantr 480	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ 𝑠 ∈ ℕ) ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠))) ∧ 𝑧 ∈ ℕ0) → 𝐴 ∈ Ring)
88	25	ad3antrrr 731	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ 𝑠 ∈ ℕ) ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠))) ∧ 𝑧 ∈ ℕ0) → (mulGrp‘𝐴) ∈ Mnd)
89		simpr 484	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ 𝑠 ∈ ℕ) ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠))) ∧ 𝑧 ∈ ℕ0) → 𝑧 ∈ ℕ0)
90	28	adantr 480	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ 𝑠 ∈ ℕ) ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠))) ∧ 𝑧 ∈ ℕ0) → 𝑀 ∈ 𝐵)
91	21, 22, 88, 89, 90	mulgnn0cld 19037	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ 𝑠 ∈ ℕ) ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠))) ∧ 𝑧 ∈ ℕ0) → (𝑧 ↑ 𝑀) ∈ 𝐵)
92	87, 91	jca 511	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ 𝑠 ∈ ℕ) ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠))) ∧ 𝑧 ∈ ℕ0) → (𝐴 ∈ Ring ∧ (𝑧 ↑ 𝑀) ∈ 𝐵))
93	92	adantr 480	. . . . . . . . . . . . . . . 16 ⊢ ((((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ 𝑠 ∈ ℕ) ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠))) ∧ 𝑧 ∈ ℕ0) ∧ (𝐺‘𝑧) = (0g‘𝑌)) → (𝐴 ∈ Ring ∧ (𝑧 ↑ 𝑀) ∈ 𝐵))
94	7, 49, 8	ringrz 20241	. . . . . . . . . . . . . . . 16 ⊢ ((𝐴 ∈ Ring ∧ (𝑧 ↑ 𝑀) ∈ 𝐵) → ((𝑧 ↑ 𝑀)(.r‘𝐴)(0g‘𝐴)) = (0g‘𝐴))
95	93, 94	syl 17	. . . . . . . . . . . . . . 15 ⊢ ((((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ 𝑠 ∈ ℕ) ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠))) ∧ 𝑧 ∈ ℕ0) ∧ (𝐺‘𝑧) = (0g‘𝑌)) → ((𝑧 ↑ 𝑀)(.r‘𝐴)(0g‘𝐴)) = (0g‘𝐴))
96	77, 86, 95	3eqtrd 2776	. . . . . . . . . . . . . 14 ⊢ ((((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ 𝑠 ∈ ℕ) ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠))) ∧ 𝑧 ∈ ℕ0) ∧ (𝐺‘𝑧) = (0g‘𝑌)) → ⦋𝑧 / 𝑛⦌((𝑛 ↑ 𝑀)(.r‘𝐴)(𝑈‘(𝐺‘𝑛))) = (0g‘𝐴))
97	96	ex 412	. . . . . . . . . . . . 13 ⊢ (((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ 𝑠 ∈ ℕ) ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠))) ∧ 𝑧 ∈ ℕ0) → ((𝐺‘𝑧) = (0g‘𝑌) → ⦋𝑧 / 𝑛⦌((𝑛 ↑ 𝑀)(.r‘𝐴)(𝑈‘(𝐺‘𝑛))) = (0g‘𝐴)))
98	97	adantlr 716	. . . . . . . . . . . 12 ⊢ ((((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ 𝑠 ∈ ℕ) ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠))) ∧ 𝑤 ∈ ℕ0) ∧ 𝑧 ∈ ℕ0) → ((𝐺‘𝑧) = (0g‘𝑌) → ⦋𝑧 / 𝑛⦌((𝑛 ↑ 𝑀)(.r‘𝐴)(𝑈‘(𝐺‘𝑛))) = (0g‘𝐴)))
99	98	imim2d 57	. . . . . . . . . . 11 ⊢ ((((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ 𝑠 ∈ ℕ) ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠))) ∧ 𝑤 ∈ ℕ0) ∧ 𝑧 ∈ ℕ0) → ((𝑤 < 𝑧 → (𝐺‘𝑧) = (0g‘𝑌)) → (𝑤 < 𝑧 → ⦋𝑧 / 𝑛⦌((𝑛 ↑ 𝑀)(.r‘𝐴)(𝑈‘(𝐺‘𝑛))) = (0g‘𝐴))))
100	99	ralimdva 3150	. . . . . . . . . 10 ⊢ (((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ 𝑠 ∈ ℕ) ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠))) ∧ 𝑤 ∈ ℕ0) → (∀𝑧 ∈ ℕ0 (𝑤 < 𝑧 → (𝐺‘𝑧) = (0g‘𝑌)) → ∀𝑧 ∈ ℕ0 (𝑤 < 𝑧 → ⦋𝑧 / 𝑛⦌((𝑛 ↑ 𝑀)(.r‘𝐴)(𝑈‘(𝐺‘𝑛))) = (0g‘𝐴))))
101	100	reximdva 3151	. . . . . . . . 9 ⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ 𝑠 ∈ ℕ) ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠))) → (∃𝑤 ∈ ℕ0 ∀𝑧 ∈ ℕ0 (𝑤 < 𝑧 → (𝐺‘𝑧) = (0g‘𝑌)) → ∃𝑤 ∈ ℕ0 ∀𝑧 ∈ ℕ0 (𝑤 < 𝑧 → ⦋𝑧 / 𝑛⦌((𝑛 ↑ 𝑀)(.r‘𝐴)(𝑈‘(𝐺‘𝑛))) = (0g‘𝐴))))
102	64, 101	syld 47	. . . . . . . 8 ⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ 𝑠 ∈ ℕ) ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠))) → (𝐺 finSupp (0g‘𝑌) → ∃𝑤 ∈ ℕ0 ∀𝑧 ∈ ℕ0 (𝑤 < 𝑧 → ⦋𝑧 / 𝑛⦌((𝑛 ↑ 𝑀)(.r‘𝐴)(𝑈‘(𝐺‘𝑛))) = (0g‘𝐴))))
103	56, 102	mpd 15	. . . . . . 7 ⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ 𝑠 ∈ ℕ) ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠))) → ∃𝑤 ∈ ℕ0 ∀𝑧 ∈ ℕ0 (𝑤 < 𝑧 → ⦋𝑧 / 𝑛⦌((𝑛 ↑ 𝑀)(.r‘𝐴)(𝑈‘(𝐺‘𝑛))) = (0g‘𝐴)))
104	53, 54, 103	mptnn0fsupp 13932	. . . . . 6 ⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ 𝑠 ∈ ℕ) ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠))) → (𝑛 ∈ ℕ0 ↦ ((𝑛 ↑ 𝑀)(.r‘𝐴)(𝑈‘(𝐺‘𝑛)))) finSupp (0g‘𝐴))
105	7, 8, 15, 17, 52, 104	gsumcl 19856	. . . . 5 ⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ 𝑠 ∈ ℕ) ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠))) → (𝐴 Σg (𝑛 ∈ ℕ0 ↦ ((𝑛 ↑ 𝑀)(.r‘𝐴)(𝑈‘(𝐺‘𝑛))))) ∈ 𝐵)
106	32, 9, 7, 43	m2cpminvid 22709	. . . . 5 ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ (𝐴 Σg (𝑛 ∈ ℕ0 ↦ ((𝑛 ↑ 𝑀)(.r‘𝐴)(𝑈‘(𝐺‘𝑛))))) ∈ 𝐵) → (𝑈‘(𝑇‘(𝐴 Σg (𝑛 ∈ ℕ0 ↦ ((𝑛 ↑ 𝑀)(.r‘𝐴)(𝑈‘(𝐺‘𝑛))))))) = (𝐴 Σg (𝑛 ∈ ℕ0 ↦ ((𝑛 ↑ 𝑀)(.r‘𝐴)(𝑈‘(𝐺‘𝑛))))))
107	3, 6, 105, 106	syl3anc 1374	. . . 4 ⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ 𝑠 ∈ ℕ) ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠))) → (𝑈‘(𝑇‘(𝐴 Σg (𝑛 ∈ ℕ0 ↦ ((𝑛 ↑ 𝑀)(.r‘𝐴)(𝑈‘(𝐺‘𝑛))))))) = (𝐴 Σg (𝑛 ∈ ℕ0 ↦ ((𝑛 ↑ 𝑀)(.r‘𝐴)(𝑈‘(𝐺‘𝑛))))))
108	38, 39	pmatring 22648	. . . . . . . . . 10 ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → 𝑌 ∈ Ring)
109	2, 5, 108	syl2anc 585	. . . . . . . . 9 ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) → 𝑌 ∈ Ring)
110		ringmnd 20190	. . . . . . . . 9 ⊢ (𝑌 ∈ Ring → 𝑌 ∈ Mnd)
111	109, 110	syl 17	. . . . . . . 8 ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) → 𝑌 ∈ Mnd)
112	111	ad2antrr 727	. . . . . . 7 ⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ 𝑠 ∈ ℕ) ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠))) → 𝑌 ∈ Mnd)
113		chcoeffeq.w	. . . . . . . . . 10 ⊢ 𝑊 = (Base‘𝑌)
114	43, 9, 7, 38, 39, 113	mat2pmatghm 22686	. . . . . . . . 9 ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → 𝑇 ∈ (𝐴 GrpHom 𝑌))
115	3, 6, 114	syl2anc 585	. . . . . . . 8 ⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ 𝑠 ∈ ℕ) ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠))) → 𝑇 ∈ (𝐴 GrpHom 𝑌))
116		ghmmhm 19167	. . . . . . . 8 ⊢ (𝑇 ∈ (𝐴 GrpHom 𝑌) → 𝑇 ∈ (𝐴 MndHom 𝑌))
117	115, 116	syl 17	. . . . . . 7 ⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ 𝑠 ∈ ℕ) ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠))) → 𝑇 ∈ (𝐴 MndHom 𝑌))
118	23	ad3antrrr 731	. . . . . . . 8 ⊢ (((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ 𝑠 ∈ ℕ) ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠))) ∧ 𝑛 ∈ ℕ0) → 𝐴 ∈ Ring)
119	4, 33	sylan2 594	. . . . . . . . . . 11 ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) → 𝑈:(𝑁 ConstPolyMat 𝑅)⟶𝐵)
120	119	3adant3 1133	. . . . . . . . . 10 ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) → 𝑈:(𝑁 ConstPolyMat 𝑅)⟶𝐵)
121	120	ad3antrrr 731	. . . . . . . . 9 ⊢ (((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ 𝑠 ∈ ℕ) ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠))) ∧ 𝑛 ∈ ℕ0) → 𝑈:(𝑁 ConstPolyMat 𝑅)⟶𝐵)
122	121, 47	ffvelcdmd 7039	. . . . . . . 8 ⊢ (((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ 𝑠 ∈ ℕ) ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠))) ∧ 𝑛 ∈ ℕ0) → (𝑈‘(𝐺‘𝑛)) ∈ 𝐵)
123	118, 30, 122, 50	syl3anc 1374	. . . . . . 7 ⊢ (((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ 𝑠 ∈ ℕ) ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠))) ∧ 𝑛 ∈ ℕ0) → ((𝑛 ↑ 𝑀)(.r‘𝐴)(𝑈‘(𝐺‘𝑛))) ∈ 𝐵)
124	7, 8, 15, 112, 17, 117, 123, 104	gsummptmhm 19881	. . . . . 6 ⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ 𝑠 ∈ ℕ) ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠))) → (𝑌 Σg (𝑛 ∈ ℕ0 ↦ (𝑇‘((𝑛 ↑ 𝑀)(.r‘𝐴)(𝑈‘(𝐺‘𝑛)))))) = (𝑇‘(𝐴 Σg (𝑛 ∈ ℕ0 ↦ ((𝑛 ↑ 𝑀)(.r‘𝐴)(𝑈‘(𝐺‘𝑛)))))))
125	43, 9, 7, 38, 39, 113	mat2pmatrhm 22690	. . . . . . . . . . . 12 ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) → 𝑇 ∈ (𝐴 RingHom 𝑌))
126	125	3adant3 1133	. . . . . . . . . . 11 ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) → 𝑇 ∈ (𝐴 RingHom 𝑌))
127	126	ad3antrrr 731	. . . . . . . . . 10 ⊢ (((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ 𝑠 ∈ ℕ) ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠))) ∧ 𝑛 ∈ ℕ0) → 𝑇 ∈ (𝐴 RingHom 𝑌))
128	7, 49, 40	rhmmul 20433	. . . . . . . . . 10 ⊢ ((𝑇 ∈ (𝐴 RingHom 𝑌) ∧ (𝑛 ↑ 𝑀) ∈ 𝐵 ∧ (𝑈‘(𝐺‘𝑛)) ∈ 𝐵) → (𝑇‘((𝑛 ↑ 𝑀)(.r‘𝐴)(𝑈‘(𝐺‘𝑛)))) = ((𝑇‘(𝑛 ↑ 𝑀)) × (𝑇‘(𝑈‘(𝐺‘𝑛)))))
129	127, 30, 122, 128	syl3anc 1374	. . . . . . . . 9 ⊢ (((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ 𝑠 ∈ ℕ) ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠))) ∧ 𝑛 ∈ ℕ0) → (𝑇‘((𝑛 ↑ 𝑀)(.r‘𝐴)(𝑈‘(𝐺‘𝑛)))) = ((𝑇‘(𝑛 ↑ 𝑀)) × (𝑇‘(𝑈‘(𝐺‘𝑛)))))
130	43, 9, 7, 38, 39, 113	mat2pmatmhm 22689	. . . . . . . . . . . . 13 ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) → 𝑇 ∈ ((mulGrp‘𝐴) MndHom (mulGrp‘𝑌)))
131	130	3adant3 1133	. . . . . . . . . . . 12 ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) → 𝑇 ∈ ((mulGrp‘𝐴) MndHom (mulGrp‘𝑌)))
132	131	ad3antrrr 731	. . . . . . . . . . 11 ⊢ (((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ 𝑠 ∈ ℕ) ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠))) ∧ 𝑛 ∈ ℕ0) → 𝑇 ∈ ((mulGrp‘𝐴) MndHom (mulGrp‘𝑌)))
133		cayhamlem.e2	. . . . . . . . . . . 12 ⊢ 𝐸 = (.g‘(mulGrp‘𝑌))
134	21, 22, 133	mhmmulg 19057	. . . . . . . . . . 11 ⊢ ((𝑇 ∈ ((mulGrp‘𝐴) MndHom (mulGrp‘𝑌)) ∧ 𝑛 ∈ ℕ0 ∧ 𝑀 ∈ 𝐵) → (𝑇‘(𝑛 ↑ 𝑀)) = (𝑛𝐸(𝑇‘𝑀)))
135	132, 27, 29, 134	syl3anc 1374	. . . . . . . . . 10 ⊢ (((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ 𝑠 ∈ ℕ) ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠))) ∧ 𝑛 ∈ ℕ0) → (𝑇‘(𝑛 ↑ 𝑀)) = (𝑛𝐸(𝑇‘𝑀)))
136	2	ad3antrrr 731	. . . . . . . . . . 11 ⊢ (((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ 𝑠 ∈ ℕ) ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠))) ∧ 𝑛 ∈ ℕ0) → 𝑁 ∈ Fin)
137	5	ad3antrrr 731	. . . . . . . . . . 11 ⊢ (((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ 𝑠 ∈ ℕ) ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠))) ∧ 𝑛 ∈ ℕ0) → 𝑅 ∈ Ring)
138	31, 32, 43	m2cpminvid2 22711	. . . . . . . . . . 11 ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ (𝐺‘𝑛) ∈ (𝑁 ConstPolyMat 𝑅)) → (𝑇‘(𝑈‘(𝐺‘𝑛))) = (𝐺‘𝑛))
139	136, 137, 47, 138	syl3anc 1374	. . . . . . . . . 10 ⊢ (((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ 𝑠 ∈ ℕ) ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠))) ∧ 𝑛 ∈ ℕ0) → (𝑇‘(𝑈‘(𝐺‘𝑛))) = (𝐺‘𝑛))
140	135, 139	oveq12d 7386	. . . . . . . . 9 ⊢ (((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ 𝑠 ∈ ℕ) ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠))) ∧ 𝑛 ∈ ℕ0) → ((𝑇‘(𝑛 ↑ 𝑀)) × (𝑇‘(𝑈‘(𝐺‘𝑛)))) = ((𝑛𝐸(𝑇‘𝑀)) × (𝐺‘𝑛)))
141	129, 140	eqtrd 2772	. . . . . . . 8 ⊢ (((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ 𝑠 ∈ ℕ) ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠))) ∧ 𝑛 ∈ ℕ0) → (𝑇‘((𝑛 ↑ 𝑀)(.r‘𝐴)(𝑈‘(𝐺‘𝑛)))) = ((𝑛𝐸(𝑇‘𝑀)) × (𝐺‘𝑛)))
142	141	mpteq2dva 5193	. . . . . . 7 ⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ 𝑠 ∈ ℕ) ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠))) → (𝑛 ∈ ℕ0 ↦ (𝑇‘((𝑛 ↑ 𝑀)(.r‘𝐴)(𝑈‘(𝐺‘𝑛))))) = (𝑛 ∈ ℕ0 ↦ ((𝑛𝐸(𝑇‘𝑀)) × (𝐺‘𝑛))))
143	142	oveq2d 7384	. . . . . 6 ⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ 𝑠 ∈ ℕ) ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠))) → (𝑌 Σg (𝑛 ∈ ℕ0 ↦ (𝑇‘((𝑛 ↑ 𝑀)(.r‘𝐴)(𝑈‘(𝐺‘𝑛)))))) = (𝑌 Σg (𝑛 ∈ ℕ0 ↦ ((𝑛𝐸(𝑇‘𝑀)) × (𝐺‘𝑛)))))
144	124, 143	eqtr3d 2774	. . . . 5 ⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ 𝑠 ∈ ℕ) ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠))) → (𝑇‘(𝐴 Σg (𝑛 ∈ ℕ0 ↦ ((𝑛 ↑ 𝑀)(.r‘𝐴)(𝑈‘(𝐺‘𝑛)))))) = (𝑌 Σg (𝑛 ∈ ℕ0 ↦ ((𝑛𝐸(𝑇‘𝑀)) × (𝐺‘𝑛)))))
145	144	fveq2d 6846	. . . 4 ⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ 𝑠 ∈ ℕ) ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠))) → (𝑈‘(𝑇‘(𝐴 Σg (𝑛 ∈ ℕ0 ↦ ((𝑛 ↑ 𝑀)(.r‘𝐴)(𝑈‘(𝐺‘𝑛))))))) = (𝑈‘(𝑌 Σg (𝑛 ∈ ℕ0 ↦ ((𝑛𝐸(𝑇‘𝑀)) × (𝐺‘𝑛))))))
146	107, 145	eqtr3d 2774	. . 3 ⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ 𝑠 ∈ ℕ) ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠))) → (𝐴 Σg (𝑛 ∈ ℕ0 ↦ ((𝑛 ↑ 𝑀)(.r‘𝐴)(𝑈‘(𝐺‘𝑛))))) = (𝑈‘(𝑌 Σg (𝑛 ∈ ℕ0 ↦ ((𝑛𝐸(𝑇‘𝑀)) × (𝐺‘𝑛))))))
147	1, 146	sylan9eqr 2794	. 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 22843	. 2 ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) → ∃𝑠 ∈ ℕ ∃𝑏 ∈ (𝐵 ↑m (0...𝑠))(𝐴 Σg (𝑛 ∈ ℕ0 ↦ (((coe1‘𝐾)‘𝑛) ∗ (𝑛 ↑ 𝑀)))) = (𝐴 Σg (𝑛 ∈ ℕ0 ↦ ((𝑛 ↑ 𝑀)(.r‘𝐴)(𝑈‘(𝐺‘𝑛))))))
153	147, 152	reximddv2 3197	1 ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) → ∃𝑠 ∈ ℕ ∃𝑏 ∈ (𝐵 ↑m (0...𝑠))(𝐴 Σg (𝑛 ∈ ℕ0 ↦ (((coe1‘𝐾)‘𝑛) ∗ (𝑛 ↑ 𝑀)))) = (𝑈‘(𝑌 Σg (𝑛 ∈ ℕ0 ↦ ((𝑛𝐸(𝑇‘𝑀)) × (𝐺‘𝑛))))))

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   ∧ w3a 1087   = wceq 1542   ∈ wcel 2114  ∀wral 3052  ∃wrex 3062  Vcvv 3442  ⦋csb 3851  ifcif 4481   class class class wbr 5100   ↦ cmpt 5181  ⟶wf 6496  ‘cfv 6500  (class class class)co 7368   ↑_m cmap 8775  Fincfn 8895   finSupp cfsupp 9276  0cc0 11038  1c1 11039   + caddc 11041   < clt 11178   − cmin 11376  ℕcn 12157  ℕ₀cn0 12413  ...cfz 13435  Basecbs 17148  ._rcmulr 17190   ·_𝑠 cvsca 17193  0_gc0g 17371   Σ_g cgsu 17372  Mndcmnd 18671   MndHom cmhm 18718  -_gcsg 18877  ._gcmg 19009   GrpHom cghm 19153  CMndccmn 19721  mulGrpcmgp 20087  1_rcur 20128  Ringcrg 20180  CRingccrg 20181   RingHom crh 20417  Poly₁cpl1 22129  coe₁cco1 22130   Mat cmat 22363   ConstPolyMat ccpmat 22659   matToPolyMat cmat2pmat 22660   cPolyMatToMat ccpmat2mat 22661   CharPlyMat cchpmat 22782

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2709  ax-rep 5226  ax-sep 5243  ax-nul 5253  ax-pow 5312  ax-pr 5379  ax-un 7690  ax-cnex 11094  ax-resscn 11095  ax-1cn 11096  ax-icn 11097  ax-addcl 11098  ax-addrcl 11099  ax-mulcl 11100  ax-mulrcl 11101  ax-mulcom 11102  ax-addass 11103  ax-mulass 11104  ax-distr 11105  ax-i2m1 11106  ax-1ne0 11107  ax-1rid 11108  ax-rnegex 11109  ax-rrecex 11110  ax-cnre 11111  ax-pre-lttri 11112  ax-pre-lttrn 11113  ax-pre-ltadd 11114  ax-pre-mulgt0 11115  ax-addf 11117  ax-mulf 11118

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-xor 1514  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ne 2934  df-nel 3038  df-ral 3053  df-rex 3063  df-rmo 3352  df-reu 3353  df-rab 3402  df-v 3444  df-sbc 3743  df-csb 3852  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-pss 3923  df-nul 4288  df-if 4482  df-pw 4558  df-sn 4583  df-pr 4585  df-tp 4587  df-op 4589  df-ot 4591  df-uni 4866  df-int 4905  df-iun 4950  df-iin 4951  df-br 5101  df-opab 5163  df-mpt 5182  df-tr 5208  df-id 5527  df-eprel 5532  df-po 5540  df-so 5541  df-fr 5585  df-se 5586  df-we 5587  df-xp 5638  df-rel 5639  df-cnv 5640  df-co 5641  df-dm 5642  df-rn 5643  df-res 5644  df-ima 5645  df-pred 6267  df-ord 6328  df-on 6329  df-lim 6330  df-suc 6331  df-iota 6456  df-fun 6502  df-fn 6503  df-f 6504  df-f1 6505  df-fo 6506  df-f1o 6507  df-fv 6508  df-isom 6509  df-riota 7325  df-ov 7371  df-oprab 7372  df-mpo 7373  df-of 7632  df-ofr 7633  df-om 7819  df-1st 7943  df-2nd 7944  df-supp 8113  df-tpos 8178  df-cur 8219  df-frecs 8233  df-wrecs 8264  df-recs 8313  df-rdg 8351  df-1o 8407  df-2o 8408  df-er 8645  df-map 8777  df-pm 8778  df-ixp 8848  df-en 8896  df-dom 8897  df-sdom 8898  df-fin 8899  df-fsupp 9277  df-sup 9357  df-oi 9427  df-card 9863  df-pnf 11180  df-mnf 11181  df-xr 11182  df-ltxr 11183  df-le 11184  df-sub 11378  df-neg 11379  df-div 11807  df-nn 12158  df-2 12220  df-3 12221  df-4 12222  df-5 12223  df-6 12224  df-7 12225  df-8 12226  df-9 12227  df-n0 12414  df-xnn0 12487  df-z 12501  df-dec 12620  df-uz 12764  df-rp 12918  df-fz 13436  df-fzo 13583  df-seq 13937  df-exp 13997  df-hash 14266  df-word 14449  df-lsw 14498  df-concat 14506  df-s1 14532  df-substr 14577  df-pfx 14607  df-splice 14685  df-reverse 14694  df-s2 14783  df-struct 17086  df-sets 17103  df-slot 17121  df-ndx 17133  df-base 17149  df-ress 17170  df-plusg 17202  df-mulr 17203  df-starv 17204  df-sca 17205  df-vsca 17206  df-ip 17207  df-tset 17208  df-ple 17209  df-ds 17211  df-unif 17212  df-hom 17213  df-cco 17214  df-0g 17373  df-gsum 17374  df-prds 17379  df-pws 17381  df-mre 17517  df-mrc 17518  df-acs 17520  df-mgm 18577  df-sgrp 18656  df-mnd 18672  df-mhm 18720  df-submnd 18721  df-efmnd 18806  df-grp 18878  df-minusg 18879  df-sbg 18880  df-mulg 19010  df-subg 19065  df-ghm 19154  df-gim 19200  df-cntz 19258  df-oppg 19287  df-symg 19311  df-pmtr 19383  df-psgn 19432  df-evpm 19433  df-cmn 19723  df-abl 19724  df-mgp 20088  df-rng 20100  df-ur 20129  df-srg 20134  df-ring 20182  df-cring 20183  df-oppr 20285  df-dvdsr 20305  df-unit 20306  df-invr 20336  df-dvr 20349  df-rhm 20420  df-subrng 20491  df-subrg 20515  df-drng 20676  df-lmod 20825  df-lss 20895  df-sra 21137  df-rgmod 21138  df-cnfld 21322  df-zring 21414  df-zrh 21470  df-dsmm 21699  df-frlm 21714  df-assa 21820  df-ascl 21822  df-psr 21877  df-mvr 21878  df-mpl 21879  df-opsr 21881  df-psr1 22132  df-vr1 22133  df-ply1 22134  df-coe1 22135  df-mamu 22347  df-mat 22364  df-mdet 22541  df-madu 22590  df-cpmat 22662  df-mat2pmat 22663  df-cpmat2mat 22664  df-decpmat 22719  df-pm2mp 22749  df-chpmat 22783

This theorem is referenced by:  cayleyhamilton0  22845  cayleyhamiltonALT  22847