Theorem cayhamlem4 22866

Description: Lemma for cayleyhamilton 22868. (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 20220	. . . . . . 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 22421	. . . . . . . . . 10 ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → 𝐴 ∈ Ring)
11	4, 10	sylan2 594	. . . . . . . . 9 ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) → 𝐴 ∈ Ring)
12		ringcmn 20257	. . . . . . . . 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 12437	. . . . . . 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 20120	. . . . . . . . 9 ⊢ 𝐵 = (Base‘(mulGrp‘𝐴))
22		cayhamlem.e1	. . . . . . . . 9 ⊢ ↑ = (.g‘(mulGrp‘𝐴))
23	2, 5, 10	syl2anc 585	. . . . . . . . . . 11 ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) → 𝐴 ∈ Ring)
24	20	ringmgp 20214	. . . . . . . . . . 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 19065	. . . . . . . 8 ⊢ (((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ 𝑠 ∈ ℕ) ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠))) ∧ 𝑛 ∈ ℕ0) → (𝑛 ↑ 𝑀) ∈ 𝐵)
31		eqid 2737	. . . . . . . . . . . 12 ⊢ (𝑁 ConstPolyMat 𝑅) = (𝑁 ConstPolyMat 𝑅)
32		chcoeffeq.u	. . . . . . . . . . . 12 ⊢ 𝑈 = (𝑁 cPolyMatToMat 𝑅)
33	9, 7, 31, 32	cpm2mf 22730	. . . . . . . . . . 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 22833	. . . . . . . . . . 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 7031	. . . . . . . . 9 ⊢ (((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ 𝑠 ∈ ℕ) ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠))) ∧ 𝑛 ∈ ℕ0) → (𝐺‘𝑛) ∈ (𝑁 ConstPolyMat 𝑅))
48	35, 47	ffvelcdmd 7032	. . . . . . . 8 ⊢ (((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ 𝑠 ∈ ℕ) ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠))) ∧ 𝑛 ∈ ℕ0) → (𝑈‘(𝐺‘𝑛)) ∈ 𝐵)
49		eqid 2737	. . . . . . . . 9 ⊢ (.r‘𝐴) = (.r‘𝐴)
50	7, 49	ringcl 20225	. . . . . . . 8 ⊢ ((𝐴 ∈ Ring ∧ (𝑛 ↑ 𝑀) ∈ 𝐵 ∧ (𝑈‘(𝐺‘𝑛)) ∈ 𝐵) → ((𝑛 ↑ 𝑀)(.r‘𝐴)(𝑈‘(𝐺‘𝑛))) ∈ 𝐵)
51	19, 30, 48, 50	syl3anc 1374	. . . . . . 7 ⊢ (((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ 𝑠 ∈ ℕ) ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠))) ∧ 𝑛 ∈ ℕ0) → ((𝑛 ↑ 𝑀)(.r‘𝐴)(𝑈‘(𝐺‘𝑛))) ∈ 𝐵)
52	51	fmpttd 7062	. . . . . 6 ⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ 𝑠 ∈ ℕ) ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠))) → (𝑛 ∈ ℕ0 ↦ ((𝑛 ↑ 𝑀)(.r‘𝐴)(𝑈‘(𝐺‘𝑛)))):ℕ0⟶𝐵)
53		fvexd 6850	. . . . . . 7 ⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ 𝑠 ∈ ℕ) ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠))) → (0g‘𝐴) ∈ V)
54		ovexd 7396	. . . . . . 7 ⊢ (((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ 𝑠 ∈ ℕ) ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠))) ∧ 𝑛 ∈ ℕ0) → ((𝑛 ↑ 𝑀)(.r‘𝐴)(𝑈‘(𝐺‘𝑛))) ∈ V)
55	9, 7, 38, 39, 40, 41, 42, 43, 44	chfacffsupp 22834	. . . . . . . . 9 ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) → 𝐺 finSupp (0g‘𝑌))
56	55	anassrs 467	. . . . . . . 8 ⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ 𝑠 ∈ ℕ) ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠))) → 𝐺 finSupp (0g‘𝑌))
57		ovex 7394	. . . . . . . . . . . . 13 ⊢ (𝑁 ConstPolyMat 𝑅) ∈ V
58	57, 16	pm3.2i 470	. . . . . . . . . . . 12 ⊢ ((𝑁 ConstPolyMat 𝑅) ∈ V ∧ ℕ0 ∈ V)
59		elmapg 8780	. . . . . . . . . . . 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 6848	. . . . . . . . . 10 ⊢ (0g‘𝑌) ∈ V
63		fsuppmapnn0ub 13951	. . . . . . . . . 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 7407	. . . . . . . . . . . . . . . . 17 ⊢ (𝑧 ∈ ℕ0 → ⦋𝑧 / 𝑛⦌((𝑛 ↑ 𝑀)(.r‘𝐴)(𝑈‘(𝐺‘𝑛))) = (⦋𝑧 / 𝑛⦌(𝑛 ↑ 𝑀)(.r‘𝐴)⦋𝑧 / 𝑛⦌(𝑈‘(𝐺‘𝑛))))
66		csbov1g 7408	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑧 ∈ ℕ0 → ⦋𝑧 / 𝑛⦌(𝑛 ↑ 𝑀) = (⦋𝑧 / 𝑛⦌𝑛 ↑ 𝑀))
67		csbvarg 4375	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑧 ∈ ℕ0 → ⦋𝑧 / 𝑛⦌𝑛 = 𝑧)
68	67	oveq1d 7376	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑧 ∈ ℕ0 → (⦋𝑧 / 𝑛⦌𝑛 ↑ 𝑀) = (𝑧 ↑ 𝑀))
69	66, 68	eqtrd 2772	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑧 ∈ ℕ0 → ⦋𝑧 / 𝑛⦌(𝑛 ↑ 𝑀) = (𝑧 ↑ 𝑀))
70		csbfv2g 6881	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑧 ∈ ℕ0 → ⦋𝑧 / 𝑛⦌(𝑈‘(𝐺‘𝑛)) = (𝑈‘⦋𝑧 / 𝑛⦌(𝐺‘𝑛)))
71		csbfv 6882	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ⦋𝑧 / 𝑛⦌(𝐺‘𝑛) = (𝐺‘𝑧)
72	71	a1i 11	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑧 ∈ ℕ0 → ⦋𝑧 / 𝑛⦌(𝐺‘𝑛) = (𝐺‘𝑧))
73	72	fveq2d 6839	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑧 ∈ ℕ0 → (𝑈‘⦋𝑧 / 𝑛⦌(𝐺‘𝑛)) = (𝑈‘(𝐺‘𝑧)))
74	70, 73	eqtrd 2772	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑧 ∈ ℕ0 → ⦋𝑧 / 𝑛⦌(𝑈‘(𝐺‘𝑛)) = (𝑈‘(𝐺‘𝑧)))
75	69, 74	oveq12d 7379	. . . . . . . . . . . . . . . . 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 6835	. . . . . . . . . . . . . . . . 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 22739	. . . . . . . . . . . . . . . . . . 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 7377	. . . . . . . . . . . . . . 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 19065	. . . . . . . . . . . . . . . . . 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 20269	. . . . . . . . . . . . . . . 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 13953	. . . . . 6 ⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ 𝑠 ∈ ℕ) ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠))) → (𝑛 ∈ ℕ0 ↦ ((𝑛 ↑ 𝑀)(.r‘𝐴)(𝑈‘(𝐺‘𝑛)))) finSupp (0g‘𝐴))
105	7, 8, 15, 17, 52, 104	gsumcl 19884	. . . . 5 ⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ 𝑠 ∈ ℕ) ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠))) → (𝐴 Σg (𝑛 ∈ ℕ0 ↦ ((𝑛 ↑ 𝑀)(.r‘𝐴)(𝑈‘(𝐺‘𝑛))))) ∈ 𝐵)
106	32, 9, 7, 43	m2cpminvid 22731	. . . . 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 22670	. . . . . . . . . 10 ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → 𝑌 ∈ Ring)
109	2, 5, 108	syl2anc 585	. . . . . . . . 9 ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) → 𝑌 ∈ Ring)
110		ringmnd 20218	. . . . . . . . 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 22708	. . . . . . . . 9 ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → 𝑇 ∈ (𝐴 GrpHom 𝑌))
115	3, 6, 114	syl2anc 585	. . . . . . . 8 ⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ 𝑠 ∈ ℕ) ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠))) → 𝑇 ∈ (𝐴 GrpHom 𝑌))
116		ghmmhm 19195	. . . . . . . 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 7032	. . . . . . . 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 19909	. . . . . 6 ⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ 𝑠 ∈ ℕ) ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠))) → (𝑌 Σg (𝑛 ∈ ℕ0 ↦ (𝑇‘((𝑛 ↑ 𝑀)(.r‘𝐴)(𝑈‘(𝐺‘𝑛)))))) = (𝑇‘(𝐴 Σg (𝑛 ∈ ℕ0 ↦ ((𝑛 ↑ 𝑀)(.r‘𝐴)(𝑈‘(𝐺‘𝑛)))))))
125	43, 9, 7, 38, 39, 113	mat2pmatrhm 22712	. . . . . . . . . . . 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 20459	. . . . . . . . . 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 22711	. . . . . . . . . . . . 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 19085	. . . . . . . . . . 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 22733	. . . . . . . . . . 11 ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ (𝐺‘𝑛) ∈ (𝑁 ConstPolyMat 𝑅)) → (𝑇‘(𝑈‘(𝐺‘𝑛))) = (𝐺‘𝑛))
139	136, 137, 47, 138	syl3anc 1374	. . . . . . . . . 10 ⊢ (((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ 𝑠 ∈ ℕ) ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠))) ∧ 𝑛 ∈ ℕ0) → (𝑇‘(𝑈‘(𝐺‘𝑛))) = (𝐺‘𝑛))
140	135, 139	oveq12d 7379	. . . . . . . . 9 ⊢ (((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ 𝑠 ∈ ℕ) ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠))) ∧ 𝑛 ∈ ℕ0) → ((𝑇‘(𝑛 ↑ 𝑀)) × (𝑇‘(𝑈‘(𝐺‘𝑛)))) = ((𝑛𝐸(𝑇‘𝑀)) × (𝐺‘𝑛)))
141	129, 140	eqtrd 2772	. . . . . . . 8 ⊢ (((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ 𝑠 ∈ ℕ) ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠))) ∧ 𝑛 ∈ ℕ0) → (𝑇‘((𝑛 ↑ 𝑀)(.r‘𝐴)(𝑈‘(𝐺‘𝑛)))) = ((𝑛𝐸(𝑇‘𝑀)) × (𝐺‘𝑛)))
142	141	mpteq2dva 5179	. . . . . . 7 ⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ 𝑠 ∈ ℕ) ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠))) → (𝑛 ∈ ℕ0 ↦ (𝑇‘((𝑛 ↑ 𝑀)(.r‘𝐴)(𝑈‘(𝐺‘𝑛))))) = (𝑛 ∈ ℕ0 ↦ ((𝑛𝐸(𝑇‘𝑀)) × (𝐺‘𝑛))))
143	142	oveq2d 7377	. . . . . 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 6839	. . . 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 22865	. 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 3430  ⦋csb 3838  ifcif 4467   class class class wbr 5086   ↦ cmpt 5167  ⟶wf 6489  ‘cfv 6493  (class class class)co 7361   ↑_m cmap 8767  Fincfn 8887   finSupp cfsupp 9268  0cc0 11032  1c1 11033   + caddc 11035   < clt 11173   − cmin 11371  ℕcn 12168  ℕ₀cn0 12431  ...cfz 13455  Basecbs 17173  ._rcmulr 17215   ·_𝑠 cvsca 17218  0_gc0g 17396   Σ_g cgsu 17397  Mndcmnd 18696   MndHom cmhm 18743  -_gcsg 18905  ._gcmg 19037   GrpHom cghm 19181  CMndccmn 19749  mulGrpcmgp 20115  1_rcur 20156  Ringcrg 20208  CRingccrg 20209   RingHom crh 20443  Poly₁cpl1 22153  coe₁cco1 22154   Mat cmat 22385   ConstPolyMat ccpmat 22681   matToPolyMat cmat2pmat 22682   cPolyMatToMat ccpmat2mat 22683   CharPlyMat cchpmat 22804

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 5213  ax-sep 5232  ax-nul 5242  ax-pow 5303  ax-pr 5371  ax-un 7683  ax-cnex 11088  ax-resscn 11089  ax-1cn 11090  ax-icn 11091  ax-addcl 11092  ax-addrcl 11093  ax-mulcl 11094  ax-mulrcl 11095  ax-mulcom 11096  ax-addass 11097  ax-mulass 11098  ax-distr 11099  ax-i2m1 11100  ax-1ne0 11101  ax-1rid 11102  ax-rnegex 11103  ax-rrecex 11104  ax-cnre 11105  ax-pre-lttri 11106  ax-pre-lttrn 11107  ax-pre-ltadd 11108  ax-pre-mulgt0 11109  ax-addf 11111  ax-mulf 11112

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 3343  df-reu 3344  df-rab 3391  df-v 3432  df-sbc 3730  df-csb 3839  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-pss 3910  df-nul 4275  df-if 4468  df-pw 4544  df-sn 4569  df-pr 4571  df-tp 4573  df-op 4575  df-ot 4577  df-uni 4852  df-int 4891  df-iun 4936  df-iin 4937  df-br 5087  df-opab 5149  df-mpt 5168  df-tr 5194  df-id 5520  df-eprel 5525  df-po 5533  df-so 5534  df-fr 5578  df-se 5579  df-we 5580  df-xp 5631  df-rel 5632  df-cnv 5633  df-co 5634  df-dm 5635  df-rn 5636  df-res 5637  df-ima 5638  df-pred 6260  df-ord 6321  df-on 6322  df-lim 6323  df-suc 6324  df-iota 6449  df-fun 6495  df-fn 6496  df-f 6497  df-f1 6498  df-fo 6499  df-f1o 6500  df-fv 6501  df-isom 6502  df-riota 7318  df-ov 7364  df-oprab 7365  df-mpo 7366  df-of 7625  df-ofr 7626  df-om 7812  df-1st 7936  df-2nd 7937  df-supp 8105  df-tpos 8170  df-cur 8211  df-frecs 8225  df-wrecs 8256  df-recs 8305  df-rdg 8343  df-1o 8399  df-2o 8400  df-er 8637  df-map 8769  df-pm 8770  df-ixp 8840  df-en 8888  df-dom 8889  df-sdom 8890  df-fin 8891  df-fsupp 9269  df-sup 9349  df-oi 9419  df-card 9857  df-pnf 11175  df-mnf 11176  df-xr 11177  df-ltxr 11178  df-le 11179  df-sub 11373  df-neg 11374  df-div 11802  df-nn 12169  df-2 12238  df-3 12239  df-4 12240  df-5 12241  df-6 12242  df-7 12243  df-8 12244  df-9 12245  df-n0 12432  df-xnn0 12505  df-z 12519  df-dec 12639  df-uz 12783  df-rp 12937  df-fz 13456  df-fzo 13603  df-seq 13958  df-exp 14018  df-hash 14287  df-word 14470  df-lsw 14519  df-concat 14527  df-s1 14553  df-substr 14598  df-pfx 14628  df-splice 14706  df-reverse 14715  df-s2 14804  df-struct 17111  df-sets 17128  df-slot 17146  df-ndx 17158  df-base 17174  df-ress 17195  df-plusg 17227  df-mulr 17228  df-starv 17229  df-sca 17230  df-vsca 17231  df-ip 17232  df-tset 17233  df-ple 17234  df-ds 17236  df-unif 17237  df-hom 17238  df-cco 17239  df-0g 17398  df-gsum 17399  df-prds 17404  df-pws 17406  df-mre 17542  df-mrc 17543  df-acs 17545  df-mgm 18602  df-sgrp 18681  df-mnd 18697  df-mhm 18745  df-submnd 18746  df-efmnd 18831  df-grp 18906  df-minusg 18907  df-sbg 18908  df-mulg 19038  df-subg 19093  df-ghm 19182  df-gim 19228  df-cntz 19286  df-oppg 19315  df-symg 19339  df-pmtr 19411  df-psgn 19460  df-evpm 19461  df-cmn 19751  df-abl 19752  df-mgp 20116  df-rng 20128  df-ur 20157  df-srg 20162  df-ring 20210  df-cring 20211  df-oppr 20311  df-dvdsr 20331  df-unit 20332  df-invr 20362  df-dvr 20375  df-rhm 20446  df-subrng 20517  df-subrg 20541  df-drng 20702  df-lmod 20851  df-lss 20921  df-sra 21163  df-rgmod 21164  df-cnfld 21348  df-zring 21440  df-zrh 21496  df-dsmm 21725  df-frlm 21740  df-assa 21846  df-ascl 21848  df-psr 21902  df-mvr 21903  df-mpl 21904  df-opsr 21906  df-psr1 22156  df-vr1 22157  df-ply1 22158  df-coe1 22159  df-mamu 22369  df-mat 22386  df-mdet 22563  df-madu 22612  df-cpmat 22684  df-mat2pmat 22685  df-cpmat2mat 22686  df-decpmat 22741  df-pm2mp 22771  df-chpmat 22805

This theorem is referenced by:  cayleyhamilton0  22867  cayleyhamiltonALT  22869