Theorem chfacfisf 22770

Description: The "characteristic factor function" is a function from the nonnegative integers to polynomial matrices. (Contributed by AV, 8-Nov-2019.)

Hypotheses

Ref	Expression
chfacfisf.a	⊢ 𝐴 = (𝑁 Mat 𝑅)
chfacfisf.b	⊢ 𝐵 = (Base‘𝐴)
chfacfisf.p	⊢ 𝑃 = (Poly1‘𝑅)
chfacfisf.y	⊢ 𝑌 = (𝑁 Mat 𝑃)
chfacfisf.r	⊢ × = (.r‘𝑌)
chfacfisf.s	⊢ − = (-g‘𝑌)
chfacfisf.0	⊢ 0 = (0g‘𝑌)
chfacfisf.t	⊢ 𝑇 = (𝑁 matToPolyMat 𝑅)
chfacfisf.g	⊢ 𝐺 = (𝑛 ∈ ℕ0 ↦ if(𝑛 = 0, ( 0 − ((𝑇‘𝑀) × (𝑇‘(𝑏‘0)))), if(𝑛 = (𝑠 + 1), (𝑇‘(𝑏‘𝑠)), if((𝑠 + 1) < 𝑛, 0 , ((𝑇‘(𝑏‘(𝑛 − 1))) − ((𝑇‘𝑀) × (𝑇‘(𝑏‘𝑛))))))))

Assertion

Ref	Expression
chfacfisf	⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) → 𝐺:ℕ0⟶(Base‘𝑌))

Distinct variable groups:   𝐵,𝑛   𝑛,𝑀   𝑛,𝑁   𝑅,𝑛   𝑛,𝑌   𝑛,𝑏   𝑛,𝑠

Allowed substitution hints:   𝐴(𝑛,𝑠,𝑏)   𝐵(𝑠,𝑏)   𝑃(𝑛,𝑠,𝑏)   𝑅(𝑠,𝑏)   𝑇(𝑛,𝑠,𝑏)   × (𝑛,𝑠,𝑏)   𝐺(𝑛,𝑠,𝑏)   𝑀(𝑠,𝑏)   − (𝑛,𝑠,𝑏)   𝑁(𝑠,𝑏)   𝑌(𝑠,𝑏)   0 (𝑛,𝑠,𝑏)

Proof of Theorem chfacfisf

Step	Hyp	Ref	Expression
1		chfacfisf.p	. . . . . . . . 9 ⊢ 𝑃 = (Poly1‘𝑅)
2		chfacfisf.y	. . . . . . . . 9 ⊢ 𝑌 = (𝑁 Mat 𝑃)
3	1, 2	pmatring 22608	. . . . . . . 8 ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → 𝑌 ∈ Ring)
4	3	3adant3 1132	. . . . . . 7 ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) → 𝑌 ∈ Ring)
5		ringgrp 20157	. . . . . . 7 ⊢ (𝑌 ∈ Ring → 𝑌 ∈ Grp)
6	4, 5	syl 17	. . . . . 6 ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) → 𝑌 ∈ Grp)
7	6	adantr 480	. . . . 5 ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) → 𝑌 ∈ Grp)
8		eqid 2731	. . . . . . . 8 ⊢ (Base‘𝑌) = (Base‘𝑌)
9		chfacfisf.0	. . . . . . . 8 ⊢ 0 = (0g‘𝑌)
10	8, 9	ring0cl 20186	. . . . . . 7 ⊢ (𝑌 ∈ Ring → 0 ∈ (Base‘𝑌))
11	4, 10	syl 17	. . . . . 6 ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) → 0 ∈ (Base‘𝑌))
12	11	adantr 480	. . . . 5 ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) → 0 ∈ (Base‘𝑌))
13	4	adantr 480	. . . . . 6 ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) → 𝑌 ∈ Ring)
14		chfacfisf.t	. . . . . . . 8 ⊢ 𝑇 = (𝑁 matToPolyMat 𝑅)
15		chfacfisf.a	. . . . . . . 8 ⊢ 𝐴 = (𝑁 Mat 𝑅)
16		chfacfisf.b	. . . . . . . 8 ⊢ 𝐵 = (Base‘𝐴)
17	14, 15, 16, 1, 2	mat2pmatbas 22642	. . . . . . 7 ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) → (𝑇‘𝑀) ∈ (Base‘𝑌))
18	17	adantr 480	. . . . . 6 ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) → (𝑇‘𝑀) ∈ (Base‘𝑌))
19		3simpa 1148	. . . . . . . . 9 ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) → (𝑁 ∈ Fin ∧ 𝑅 ∈ Ring))
20		elmapi 8773	. . . . . . . . . . 11 ⊢ (𝑏 ∈ (𝐵 ↑m (0...𝑠)) → 𝑏:(0...𝑠)⟶𝐵)
21	20	adantl 481	. . . . . . . . . 10 ⊢ ((𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠))) → 𝑏:(0...𝑠)⟶𝐵)
22		nnnn0 12388	. . . . . . . . . . . . 13 ⊢ (𝑠 ∈ ℕ → 𝑠 ∈ ℕ0)
23		nn0uz 12774	. . . . . . . . . . . . 13 ⊢ ℕ0 = (ℤ≥‘0)
24	22, 23	eleqtrdi 2841	. . . . . . . . . . . 12 ⊢ (𝑠 ∈ ℕ → 𝑠 ∈ (ℤ≥‘0))
25		eluzfz1 13431	. . . . . . . . . . . 12 ⊢ (𝑠 ∈ (ℤ≥‘0) → 0 ∈ (0...𝑠))
26	24, 25	syl 17	. . . . . . . . . . 11 ⊢ (𝑠 ∈ ℕ → 0 ∈ (0...𝑠))
27	26	adantr 480	. . . . . . . . . 10 ⊢ ((𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠))) → 0 ∈ (0...𝑠))
28	21, 27	ffvelcdmd 7018	. . . . . . . . 9 ⊢ ((𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠))) → (𝑏‘0) ∈ 𝐵)
29	19, 28	anim12i 613	. . . . . . . 8 ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) → ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑏‘0) ∈ 𝐵))
30		df-3an 1088	. . . . . . . 8 ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ (𝑏‘0) ∈ 𝐵) ↔ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑏‘0) ∈ 𝐵))
31	29, 30	sylibr 234	. . . . . . 7 ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) → (𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ (𝑏‘0) ∈ 𝐵))
32	14, 15, 16, 1, 2	mat2pmatbas 22642	. . . . . . 7 ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ (𝑏‘0) ∈ 𝐵) → (𝑇‘(𝑏‘0)) ∈ (Base‘𝑌))
33	31, 32	syl 17	. . . . . 6 ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) → (𝑇‘(𝑏‘0)) ∈ (Base‘𝑌))
34		chfacfisf.r	. . . . . . 7 ⊢ × = (.r‘𝑌)
35	8, 34	ringcl 20169	. . . . . 6 ⊢ ((𝑌 ∈ Ring ∧ (𝑇‘𝑀) ∈ (Base‘𝑌) ∧ (𝑇‘(𝑏‘0)) ∈ (Base‘𝑌)) → ((𝑇‘𝑀) × (𝑇‘(𝑏‘0))) ∈ (Base‘𝑌))
36	13, 18, 33, 35	syl3anc 1373	. . . . 5 ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) → ((𝑇‘𝑀) × (𝑇‘(𝑏‘0))) ∈ (Base‘𝑌))
37		chfacfisf.s	. . . . . 6 ⊢ − = (-g‘𝑌)
38	8, 37	grpsubcl 18933	. . . . 5 ⊢ ((𝑌 ∈ Grp ∧ 0 ∈ (Base‘𝑌) ∧ ((𝑇‘𝑀) × (𝑇‘(𝑏‘0))) ∈ (Base‘𝑌)) → ( 0 − ((𝑇‘𝑀) × (𝑇‘(𝑏‘0)))) ∈ (Base‘𝑌))
39	7, 12, 36, 38	syl3anc 1373	. . . 4 ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) → ( 0 − ((𝑇‘𝑀) × (𝑇‘(𝑏‘0)))) ∈ (Base‘𝑌))
40	39	ad2antrr 726	. . 3 ⊢ (((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) ∧ 𝑛 ∈ ℕ0) ∧ 𝑛 = 0) → ( 0 − ((𝑇‘𝑀) × (𝑇‘(𝑏‘0)))) ∈ (Base‘𝑌))
41	22	adantr 480	. . . . . . . . 9 ⊢ ((𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠))) → 𝑠 ∈ ℕ0)
42	19, 41	anim12i 613	. . . . . . . 8 ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) → ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ 𝑠 ∈ ℕ0))
43		df-3an 1088	. . . . . . . 8 ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑠 ∈ ℕ0) ↔ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ 𝑠 ∈ ℕ0))
44	42, 43	sylibr 234	. . . . . . 7 ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) → (𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑠 ∈ ℕ0))
45		eluzfz2 13432	. . . . . . . . . 10 ⊢ (𝑠 ∈ (ℤ≥‘0) → 𝑠 ∈ (0...𝑠))
46	24, 45	syl 17	. . . . . . . . 9 ⊢ (𝑠 ∈ ℕ → 𝑠 ∈ (0...𝑠))
47	46	anim1ci 616	. . . . . . . 8 ⊢ ((𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠))) → (𝑏 ∈ (𝐵 ↑m (0...𝑠)) ∧ 𝑠 ∈ (0...𝑠)))
48	47	adantl 481	. . . . . . 7 ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) → (𝑏 ∈ (𝐵 ↑m (0...𝑠)) ∧ 𝑠 ∈ (0...𝑠)))
49	15, 16, 1, 2, 14	m2pmfzmap 22663	. . . . . . 7 ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑠 ∈ ℕ0) ∧ (𝑏 ∈ (𝐵 ↑m (0...𝑠)) ∧ 𝑠 ∈ (0...𝑠))) → (𝑇‘(𝑏‘𝑠)) ∈ (Base‘𝑌))
50	44, 48, 49	syl2anc 584	. . . . . 6 ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) → (𝑇‘(𝑏‘𝑠)) ∈ (Base‘𝑌))
51	50	adantr 480	. . . . 5 ⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) ∧ 𝑛 ∈ ℕ0) → (𝑇‘(𝑏‘𝑠)) ∈ (Base‘𝑌))
52	51	ad2antrr 726	. . . 4 ⊢ ((((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) ∧ 𝑛 ∈ ℕ0) ∧ ¬ 𝑛 = 0) ∧ 𝑛 = (𝑠 + 1)) → (𝑇‘(𝑏‘𝑠)) ∈ (Base‘𝑌))
53	12	ad4antr 732	. . . . 5 ⊢ (((((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) ∧ 𝑛 ∈ ℕ0) ∧ ¬ 𝑛 = 0) ∧ ¬ 𝑛 = (𝑠 + 1)) ∧ (𝑠 + 1) < 𝑛) → 0 ∈ (Base‘𝑌))
54		nn0re 12390	. . . . . . . . . . . . . . 15 ⊢ (𝑛 ∈ ℕ0 → 𝑛 ∈ ℝ)
55	54	adantl 481	. . . . . . . . . . . . . 14 ⊢ ((𝑠 ∈ ℕ ∧ 𝑛 ∈ ℕ0) → 𝑛 ∈ ℝ)
56		peano2nn 12137	. . . . . . . . . . . . . . . 16 ⊢ (𝑠 ∈ ℕ → (𝑠 + 1) ∈ ℕ)
57	56	nnred 12140	. . . . . . . . . . . . . . 15 ⊢ (𝑠 ∈ ℕ → (𝑠 + 1) ∈ ℝ)
58	57	adantr 480	. . . . . . . . . . . . . 14 ⊢ ((𝑠 ∈ ℕ ∧ 𝑛 ∈ ℕ0) → (𝑠 + 1) ∈ ℝ)
59	55, 58	lenltd 11259	. . . . . . . . . . . . 13 ⊢ ((𝑠 ∈ ℕ ∧ 𝑛 ∈ ℕ0) → (𝑛 ≤ (𝑠 + 1) ↔ ¬ (𝑠 + 1) < 𝑛))
60		nesym 2984	. . . . . . . . . . . . . . 15 ⊢ ((𝑠 + 1) ≠ 𝑛 ↔ ¬ 𝑛 = (𝑠 + 1))
61		ltlen 11214	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑛 ∈ ℝ ∧ (𝑠 + 1) ∈ ℝ) → (𝑛 < (𝑠 + 1) ↔ (𝑛 ≤ (𝑠 + 1) ∧ (𝑠 + 1) ≠ 𝑛)))
62	54, 57, 61	syl2anr 597	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑠 ∈ ℕ ∧ 𝑛 ∈ ℕ0) → (𝑛 < (𝑠 + 1) ↔ (𝑛 ≤ (𝑠 + 1) ∧ (𝑠 + 1) ≠ 𝑛)))
63	62	biimprd 248	. . . . . . . . . . . . . . . 16 ⊢ ((𝑠 ∈ ℕ ∧ 𝑛 ∈ ℕ0) → ((𝑛 ≤ (𝑠 + 1) ∧ (𝑠 + 1) ≠ 𝑛) → 𝑛 < (𝑠 + 1)))
64	63	expcomd 416	. . . . . . . . . . . . . . 15 ⊢ ((𝑠 ∈ ℕ ∧ 𝑛 ∈ ℕ0) → ((𝑠 + 1) ≠ 𝑛 → (𝑛 ≤ (𝑠 + 1) → 𝑛 < (𝑠 + 1))))
65	60, 64	biimtrrid 243	. . . . . . . . . . . . . 14 ⊢ ((𝑠 ∈ ℕ ∧ 𝑛 ∈ ℕ0) → (¬ 𝑛 = (𝑠 + 1) → (𝑛 ≤ (𝑠 + 1) → 𝑛 < (𝑠 + 1))))
66	65	com23 86	. . . . . . . . . . . . 13 ⊢ ((𝑠 ∈ ℕ ∧ 𝑛 ∈ ℕ0) → (𝑛 ≤ (𝑠 + 1) → (¬ 𝑛 = (𝑠 + 1) → 𝑛 < (𝑠 + 1))))
67	59, 66	sylbird 260	. . . . . . . . . . . 12 ⊢ ((𝑠 ∈ ℕ ∧ 𝑛 ∈ ℕ0) → (¬ (𝑠 + 1) < 𝑛 → (¬ 𝑛 = (𝑠 + 1) → 𝑛 < (𝑠 + 1))))
68	67	impcomd 411	. . . . . . . . . . 11 ⊢ ((𝑠 ∈ ℕ ∧ 𝑛 ∈ ℕ0) → ((¬ 𝑛 = (𝑠 + 1) ∧ ¬ (𝑠 + 1) < 𝑛) → 𝑛 < (𝑠 + 1)))
69	68	ex 412	. . . . . . . . . 10 ⊢ (𝑠 ∈ ℕ → (𝑛 ∈ ℕ0 → ((¬ 𝑛 = (𝑠 + 1) ∧ ¬ (𝑠 + 1) < 𝑛) → 𝑛 < (𝑠 + 1))))
70	69	ad2antrl 728	. . . . . . . . 9 ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) → (𝑛 ∈ ℕ0 → ((¬ 𝑛 = (𝑠 + 1) ∧ ¬ (𝑠 + 1) < 𝑛) → 𝑛 < (𝑠 + 1))))
71	70	imp 406	. . . . . . . 8 ⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) ∧ 𝑛 ∈ ℕ0) → ((¬ 𝑛 = (𝑠 + 1) ∧ ¬ (𝑠 + 1) < 𝑛) → 𝑛 < (𝑠 + 1)))
72	71	adantr 480	. . . . . . 7 ⊢ (((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) ∧ 𝑛 ∈ ℕ0) ∧ ¬ 𝑛 = 0) → ((¬ 𝑛 = (𝑠 + 1) ∧ ¬ (𝑠 + 1) < 𝑛) → 𝑛 < (𝑠 + 1)))
73	3, 5	syl 17	. . . . . . . . . . 11 ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → 𝑌 ∈ Grp)
74	73	3adant3 1132	. . . . . . . . . 10 ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) → 𝑌 ∈ Grp)
75	74	ad4antr 732	. . . . . . . . 9 ⊢ ((((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) ∧ 𝑛 ∈ ℕ0) ∧ ¬ 𝑛 = 0) ∧ 𝑛 < (𝑠 + 1)) → 𝑌 ∈ Grp)
76	19	ad4antr 732	. . . . . . . . . . 11 ⊢ ((((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) ∧ 𝑛 ∈ ℕ0) ∧ ¬ 𝑛 = 0) ∧ 𝑛 < (𝑠 + 1)) → (𝑁 ∈ Fin ∧ 𝑅 ∈ Ring))
77	21	ad4antlr 733	. . . . . . . . . . . 12 ⊢ ((((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) ∧ 𝑛 ∈ ℕ0) ∧ ¬ 𝑛 = 0) ∧ 𝑛 < (𝑠 + 1)) → 𝑏:(0...𝑠)⟶𝐵)
78		neqne 2936	. . . . . . . . . . . . . . . . 17 ⊢ (¬ 𝑛 = 0 → 𝑛 ≠ 0)
79	78	anim2i 617	. . . . . . . . . . . . . . . 16 ⊢ ((𝑛 ∈ ℕ0 ∧ ¬ 𝑛 = 0) → (𝑛 ∈ ℕ0 ∧ 𝑛 ≠ 0))
80		elnnne0 12395	. . . . . . . . . . . . . . . 16 ⊢ (𝑛 ∈ ℕ ↔ (𝑛 ∈ ℕ0 ∧ 𝑛 ≠ 0))
81	79, 80	sylibr 234	. . . . . . . . . . . . . . 15 ⊢ ((𝑛 ∈ ℕ0 ∧ ¬ 𝑛 = 0) → 𝑛 ∈ ℕ)
82		nnm1nn0 12422	. . . . . . . . . . . . . . 15 ⊢ (𝑛 ∈ ℕ → (𝑛 − 1) ∈ ℕ0)
83	81, 82	syl 17	. . . . . . . . . . . . . 14 ⊢ ((𝑛 ∈ ℕ0 ∧ ¬ 𝑛 = 0) → (𝑛 − 1) ∈ ℕ0)
84	83	ad4ant23 753	. . . . . . . . . . . . 13 ⊢ ((((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) ∧ 𝑛 ∈ ℕ0) ∧ ¬ 𝑛 = 0) ∧ 𝑛 < (𝑠 + 1)) → (𝑛 − 1) ∈ ℕ0)
85	41	ad4antlr 733	. . . . . . . . . . . . 13 ⊢ ((((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) ∧ 𝑛 ∈ ℕ0) ∧ ¬ 𝑛 = 0) ∧ 𝑛 < (𝑠 + 1)) → 𝑠 ∈ ℕ0)
86	62	simprbda 498	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑠 ∈ ℕ ∧ 𝑛 ∈ ℕ0) ∧ 𝑛 < (𝑠 + 1)) → 𝑛 ≤ (𝑠 + 1))
87	55	adantr 480	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑠 ∈ ℕ ∧ 𝑛 ∈ ℕ0) ∧ 𝑛 < (𝑠 + 1)) → 𝑛 ∈ ℝ)
88		1red 11113	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑠 ∈ ℕ ∧ 𝑛 ∈ ℕ0) ∧ 𝑛 < (𝑠 + 1)) → 1 ∈ ℝ)
89		nnre 12132	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑠 ∈ ℕ → 𝑠 ∈ ℝ)
90	89	ad2antrr 726	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑠 ∈ ℕ ∧ 𝑛 ∈ ℕ0) ∧ 𝑛 < (𝑠 + 1)) → 𝑠 ∈ ℝ)
91	87, 88, 90	lesubaddd 11714	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑠 ∈ ℕ ∧ 𝑛 ∈ ℕ0) ∧ 𝑛 < (𝑠 + 1)) → ((𝑛 − 1) ≤ 𝑠 ↔ 𝑛 ≤ (𝑠 + 1)))
92	86, 91	mpbird 257	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑠 ∈ ℕ ∧ 𝑛 ∈ ℕ0) ∧ 𝑛 < (𝑠 + 1)) → (𝑛 − 1) ≤ 𝑠)
93	92	exp31 419	. . . . . . . . . . . . . . . . 17 ⊢ (𝑠 ∈ ℕ → (𝑛 ∈ ℕ0 → (𝑛 < (𝑠 + 1) → (𝑛 − 1) ≤ 𝑠)))
94	93	ad2antrl 728	. . . . . . . . . . . . . . . 16 ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) → (𝑛 ∈ ℕ0 → (𝑛 < (𝑠 + 1) → (𝑛 − 1) ≤ 𝑠)))
95	94	imp 406	. . . . . . . . . . . . . . 15 ⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) ∧ 𝑛 ∈ ℕ0) → (𝑛 < (𝑠 + 1) → (𝑛 − 1) ≤ 𝑠))
96	95	adantr 480	. . . . . . . . . . . . . 14 ⊢ (((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) ∧ 𝑛 ∈ ℕ0) ∧ ¬ 𝑛 = 0) → (𝑛 < (𝑠 + 1) → (𝑛 − 1) ≤ 𝑠))
97	96	imp 406	. . . . . . . . . . . . 13 ⊢ ((((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) ∧ 𝑛 ∈ ℕ0) ∧ ¬ 𝑛 = 0) ∧ 𝑛 < (𝑠 + 1)) → (𝑛 − 1) ≤ 𝑠)
98		elfz2nn0 13518	. . . . . . . . . . . . 13 ⊢ ((𝑛 − 1) ∈ (0...𝑠) ↔ ((𝑛 − 1) ∈ ℕ0 ∧ 𝑠 ∈ ℕ0 ∧ (𝑛 − 1) ≤ 𝑠))
99	84, 85, 97, 98	syl3anbrc 1344	. . . . . . . . . . . 12 ⊢ ((((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) ∧ 𝑛 ∈ ℕ0) ∧ ¬ 𝑛 = 0) ∧ 𝑛 < (𝑠 + 1)) → (𝑛 − 1) ∈ (0...𝑠))
100	77, 99	ffvelcdmd 7018	. . . . . . . . . . 11 ⊢ ((((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) ∧ 𝑛 ∈ ℕ0) ∧ ¬ 𝑛 = 0) ∧ 𝑛 < (𝑠 + 1)) → (𝑏‘(𝑛 − 1)) ∈ 𝐵)
101		df-3an 1088	. . . . . . . . . . 11 ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ (𝑏‘(𝑛 − 1)) ∈ 𝐵) ↔ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑏‘(𝑛 − 1)) ∈ 𝐵))
102	76, 100, 101	sylanbrc 583	. . . . . . . . . 10 ⊢ ((((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) ∧ 𝑛 ∈ ℕ0) ∧ ¬ 𝑛 = 0) ∧ 𝑛 < (𝑠 + 1)) → (𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ (𝑏‘(𝑛 − 1)) ∈ 𝐵))
103	14, 15, 16, 1, 2	mat2pmatbas 22642	. . . . . . . . . 10 ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ (𝑏‘(𝑛 − 1)) ∈ 𝐵) → (𝑇‘(𝑏‘(𝑛 − 1))) ∈ (Base‘𝑌))
104	102, 103	syl 17	. . . . . . . . 9 ⊢ ((((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) ∧ 𝑛 ∈ ℕ0) ∧ ¬ 𝑛 = 0) ∧ 𝑛 < (𝑠 + 1)) → (𝑇‘(𝑏‘(𝑛 − 1))) ∈ (Base‘𝑌))
105	13	ad2antrr 726	. . . . . . . . . . 11 ⊢ (((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) ∧ 𝑛 ∈ ℕ0) ∧ 𝑛 < (𝑠 + 1)) → 𝑌 ∈ Ring)
106	18	ad2antrr 726	. . . . . . . . . . 11 ⊢ (((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) ∧ 𝑛 ∈ ℕ0) ∧ 𝑛 < (𝑠 + 1)) → (𝑇‘𝑀) ∈ (Base‘𝑌))
107	44	ad2antrr 726	. . . . . . . . . . . 12 ⊢ (((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) ∧ 𝑛 ∈ ℕ0) ∧ 𝑛 < (𝑠 + 1)) → (𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑠 ∈ ℕ0))
108		simprr 772	. . . . . . . . . . . . 13 ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) → 𝑏 ∈ (𝐵 ↑m (0...𝑠)))
109	108	ad2antrr 726	. . . . . . . . . . . 12 ⊢ (((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) ∧ 𝑛 ∈ ℕ0) ∧ 𝑛 < (𝑠 + 1)) → 𝑏 ∈ (𝐵 ↑m (0...𝑠)))
110		simplr 768	. . . . . . . . . . . . . . . 16 ⊢ (((𝑠 ∈ ℕ ∧ 𝑛 ∈ ℕ0) ∧ 𝑛 < (𝑠 + 1)) → 𝑛 ∈ ℕ0)
111	22	ad2antrr 726	. . . . . . . . . . . . . . . 16 ⊢ (((𝑠 ∈ ℕ ∧ 𝑛 ∈ ℕ0) ∧ 𝑛 < (𝑠 + 1)) → 𝑠 ∈ ℕ0)
112		nn0z 12493	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑛 ∈ ℕ0 → 𝑛 ∈ ℤ)
113		nnz 12489	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑠 ∈ ℕ → 𝑠 ∈ ℤ)
114		zleltp1 12523	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑛 ∈ ℤ ∧ 𝑠 ∈ ℤ) → (𝑛 ≤ 𝑠 ↔ 𝑛 < (𝑠 + 1)))
115	112, 113, 114	syl2anr 597	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑠 ∈ ℕ ∧ 𝑛 ∈ ℕ0) → (𝑛 ≤ 𝑠 ↔ 𝑛 < (𝑠 + 1)))
116	115	biimpar 477	. . . . . . . . . . . . . . . 16 ⊢ (((𝑠 ∈ ℕ ∧ 𝑛 ∈ ℕ0) ∧ 𝑛 < (𝑠 + 1)) → 𝑛 ≤ 𝑠)
117		elfz2nn0 13518	. . . . . . . . . . . . . . . 16 ⊢ (𝑛 ∈ (0...𝑠) ↔ (𝑛 ∈ ℕ0 ∧ 𝑠 ∈ ℕ0 ∧ 𝑛 ≤ 𝑠))
118	110, 111, 116, 117	syl3anbrc 1344	. . . . . . . . . . . . . . 15 ⊢ (((𝑠 ∈ ℕ ∧ 𝑛 ∈ ℕ0) ∧ 𝑛 < (𝑠 + 1)) → 𝑛 ∈ (0...𝑠))
119	118	exp31 419	. . . . . . . . . . . . . 14 ⊢ (𝑠 ∈ ℕ → (𝑛 ∈ ℕ0 → (𝑛 < (𝑠 + 1) → 𝑛 ∈ (0...𝑠))))
120	119	ad2antrl 728	. . . . . . . . . . . . 13 ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) → (𝑛 ∈ ℕ0 → (𝑛 < (𝑠 + 1) → 𝑛 ∈ (0...𝑠))))
121	120	imp31 417	. . . . . . . . . . . 12 ⊢ (((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) ∧ 𝑛 ∈ ℕ0) ∧ 𝑛 < (𝑠 + 1)) → 𝑛 ∈ (0...𝑠))
122	15, 16, 1, 2, 14	m2pmfzmap 22663	. . . . . . . . . . . 12 ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑠 ∈ ℕ0) ∧ (𝑏 ∈ (𝐵 ↑m (0...𝑠)) ∧ 𝑛 ∈ (0...𝑠))) → (𝑇‘(𝑏‘𝑛)) ∈ (Base‘𝑌))
123	107, 109, 121, 122	syl12anc 836	. . . . . . . . . . 11 ⊢ (((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) ∧ 𝑛 ∈ ℕ0) ∧ 𝑛 < (𝑠 + 1)) → (𝑇‘(𝑏‘𝑛)) ∈ (Base‘𝑌))
124	8, 34	ringcl 20169	. . . . . . . . . . 11 ⊢ ((𝑌 ∈ Ring ∧ (𝑇‘𝑀) ∈ (Base‘𝑌) ∧ (𝑇‘(𝑏‘𝑛)) ∈ (Base‘𝑌)) → ((𝑇‘𝑀) × (𝑇‘(𝑏‘𝑛))) ∈ (Base‘𝑌))
125	105, 106, 123, 124	syl3anc 1373	. . . . . . . . . 10 ⊢ (((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) ∧ 𝑛 ∈ ℕ0) ∧ 𝑛 < (𝑠 + 1)) → ((𝑇‘𝑀) × (𝑇‘(𝑏‘𝑛))) ∈ (Base‘𝑌))
126	125	adantlr 715	. . . . . . . . 9 ⊢ ((((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) ∧ 𝑛 ∈ ℕ0) ∧ ¬ 𝑛 = 0) ∧ 𝑛 < (𝑠 + 1)) → ((𝑇‘𝑀) × (𝑇‘(𝑏‘𝑛))) ∈ (Base‘𝑌))
127	8, 37	grpsubcl 18933	. . . . . . . . 9 ⊢ ((𝑌 ∈ Grp ∧ (𝑇‘(𝑏‘(𝑛 − 1))) ∈ (Base‘𝑌) ∧ ((𝑇‘𝑀) × (𝑇‘(𝑏‘𝑛))) ∈ (Base‘𝑌)) → ((𝑇‘(𝑏‘(𝑛 − 1))) − ((𝑇‘𝑀) × (𝑇‘(𝑏‘𝑛)))) ∈ (Base‘𝑌))
128	75, 104, 126, 127	syl3anc 1373	. . . . . . . 8 ⊢ ((((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) ∧ 𝑛 ∈ ℕ0) ∧ ¬ 𝑛 = 0) ∧ 𝑛 < (𝑠 + 1)) → ((𝑇‘(𝑏‘(𝑛 − 1))) − ((𝑇‘𝑀) × (𝑇‘(𝑏‘𝑛)))) ∈ (Base‘𝑌))
129	128	ex 412	. . . . . . 7 ⊢ (((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) ∧ 𝑛 ∈ ℕ0) ∧ ¬ 𝑛 = 0) → (𝑛 < (𝑠 + 1) → ((𝑇‘(𝑏‘(𝑛 − 1))) − ((𝑇‘𝑀) × (𝑇‘(𝑏‘𝑛)))) ∈ (Base‘𝑌)))
130	72, 129	syld 47	. . . . . 6 ⊢ (((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) ∧ 𝑛 ∈ ℕ0) ∧ ¬ 𝑛 = 0) → ((¬ 𝑛 = (𝑠 + 1) ∧ ¬ (𝑠 + 1) < 𝑛) → ((𝑇‘(𝑏‘(𝑛 − 1))) − ((𝑇‘𝑀) × (𝑇‘(𝑏‘𝑛)))) ∈ (Base‘𝑌)))
131	130	impl 455	. . . . 5 ⊢ (((((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) ∧ 𝑛 ∈ ℕ0) ∧ ¬ 𝑛 = 0) ∧ ¬ 𝑛 = (𝑠 + 1)) ∧ ¬ (𝑠 + 1) < 𝑛) → ((𝑇‘(𝑏‘(𝑛 − 1))) − ((𝑇‘𝑀) × (𝑇‘(𝑏‘𝑛)))) ∈ (Base‘𝑌))
132	53, 131	ifclda 4511	. . . 4 ⊢ ((((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) ∧ 𝑛 ∈ ℕ0) ∧ ¬ 𝑛 = 0) ∧ ¬ 𝑛 = (𝑠 + 1)) → if((𝑠 + 1) < 𝑛, 0 , ((𝑇‘(𝑏‘(𝑛 − 1))) − ((𝑇‘𝑀) × (𝑇‘(𝑏‘𝑛))))) ∈ (Base‘𝑌))
133	52, 132	ifclda 4511	. . 3 ⊢ (((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) ∧ 𝑛 ∈ ℕ0) ∧ ¬ 𝑛 = 0) → if(𝑛 = (𝑠 + 1), (𝑇‘(𝑏‘𝑠)), if((𝑠 + 1) < 𝑛, 0 , ((𝑇‘(𝑏‘(𝑛 − 1))) − ((𝑇‘𝑀) × (𝑇‘(𝑏‘𝑛)))))) ∈ (Base‘𝑌))
134	40, 133	ifclda 4511	. 2 ⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) ∧ 𝑛 ∈ ℕ0) → if(𝑛 = 0, ( 0 − ((𝑇‘𝑀) × (𝑇‘(𝑏‘0)))), if(𝑛 = (𝑠 + 1), (𝑇‘(𝑏‘𝑠)), if((𝑠 + 1) < 𝑛, 0 , ((𝑇‘(𝑏‘(𝑛 − 1))) − ((𝑇‘𝑀) × (𝑇‘(𝑏‘𝑛))))))) ∈ (Base‘𝑌))
135		chfacfisf.g	. 2 ⊢ 𝐺 = (𝑛 ∈ ℕ0 ↦ if(𝑛 = 0, ( 0 − ((𝑇‘𝑀) × (𝑇‘(𝑏‘0)))), if(𝑛 = (𝑠 + 1), (𝑇‘(𝑏‘𝑠)), if((𝑠 + 1) < 𝑛, 0 , ((𝑇‘(𝑏‘(𝑛 − 1))) − ((𝑇‘𝑀) × (𝑇‘(𝑏‘𝑛))))))))
136	134, 135	fmptd 7047	1 ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) → 𝐺:ℕ0⟶(Base‘𝑌))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 206   ∧ wa 395   ∧ w3a 1086   = wceq 1541   ∈ wcel 2111   ≠ wne 2928  ifcif 4475   class class class wbr 5091   ↦ cmpt 5172  ⟶wf 6477  ‘cfv 6481  (class class class)co 7346   ↑_m cmap 8750  Fincfn 8869  ℝcr 11005  0cc0 11006  1c1 11007   + caddc 11009   < clt 11146   ≤ cle 11147   − cmin 11344  ℕcn 12125  ℕ₀cn0 12381  ℤcz 12468  ℤ_≥cuz 12732  ...cfz 13407  Basecbs 17120  ._rcmulr 17162  0_gc0g 17343  Grpcgrp 18846  -_gcsg 18848  Ringcrg 20152  Poly₁cpl1 22090   Mat cmat 22323   matToPolyMat cmat2pmat 22620

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-10 2144  ax-11 2160  ax-12 2180  ax-ext 2703  ax-rep 5217  ax-sep 5234  ax-nul 5244  ax-pow 5303  ax-pr 5370  ax-un 7668  ax-cnex 11062  ax-resscn 11063  ax-1cn 11064  ax-icn 11065  ax-addcl 11066  ax-addrcl 11067  ax-mulcl 11068  ax-mulrcl 11069  ax-mulcom 11070  ax-addass 11071  ax-mulass 11072  ax-distr 11073  ax-i2m1 11074  ax-1ne0 11075  ax-1rid 11076  ax-rnegex 11077  ax-rrecex 11078  ax-cnre 11079  ax-pre-lttri 11080  ax-pre-lttrn 11081  ax-pre-ltadd 11082  ax-pre-mulgt0 11083

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2068  df-mo 2535  df-eu 2564  df-clab 2710  df-cleq 2723  df-clel 2806  df-nfc 2881  df-ne 2929  df-nel 3033  df-ral 3048  df-rex 3057  df-rmo 3346  df-reu 3347  df-rab 3396  df-v 3438  df-sbc 3742  df-csb 3851  df-dif 3905  df-un 3907  df-in 3909  df-ss 3919  df-pss 3922  df-nul 4284  df-if 4476  df-pw 4552  df-sn 4577  df-pr 4579  df-tp 4581  df-op 4583  df-ot 4585  df-uni 4860  df-int 4898  df-iun 4943  df-iin 4944  df-br 5092  df-opab 5154  df-mpt 5173  df-tr 5199  df-id 5511  df-eprel 5516  df-po 5524  df-so 5525  df-fr 5569  df-se 5570  df-we 5571  df-xp 5622  df-rel 5623  df-cnv 5624  df-co 5625  df-dm 5626  df-rn 5627  df-res 5628  df-ima 5629  df-pred 6248  df-ord 6309  df-on 6310  df-lim 6311  df-suc 6312  df-iota 6437  df-fun 6483  df-fn 6484  df-f 6485  df-f1 6486  df-fo 6487  df-f1o 6488  df-fv 6489  df-isom 6490  df-riota 7303  df-ov 7349  df-oprab 7350  df-mpo 7351  df-of 7610  df-ofr 7611  df-om 7797  df-1st 7921  df-2nd 7922  df-supp 8091  df-frecs 8211  df-wrecs 8242  df-recs 8291  df-rdg 8329  df-1o 8385  df-2o 8386  df-er 8622  df-map 8752  df-pm 8753  df-ixp 8822  df-en 8870  df-dom 8871  df-sdom 8872  df-fin 8873  df-fsupp 9246  df-sup 9326  df-oi 9396  df-card 9832  df-pnf 11148  df-mnf 11149  df-xr 11150  df-ltxr 11151  df-le 11152  df-sub 11346  df-neg 11347  df-nn 12126  df-2 12188  df-3 12189  df-4 12190  df-5 12191  df-6 12192  df-7 12193  df-8 12194  df-9 12195  df-n0 12382  df-z 12469  df-dec 12589  df-uz 12733  df-fz 13408  df-fzo 13555  df-seq 13909  df-hash 14238  df-struct 17058  df-sets 17075  df-slot 17093  df-ndx 17105  df-base 17121  df-ress 17142  df-plusg 17174  df-mulr 17175  df-sca 17177  df-vsca 17178  df-ip 17179  df-tset 17180  df-ple 17181  df-ds 17183  df-hom 17185  df-cco 17186  df-0g 17345  df-gsum 17346  df-prds 17351  df-pws 17353  df-mre 17488  df-mrc 17489  df-acs 17491  df-mgm 18548  df-sgrp 18627  df-mnd 18643  df-mhm 18691  df-submnd 18692  df-grp 18849  df-minusg 18850  df-sbg 18851  df-mulg 18981  df-subg 19036  df-ghm 19126  df-cntz 19230  df-cmn 19695  df-abl 19696  df-mgp 20060  df-rng 20072  df-ur 20101  df-ring 20154  df-subrng 20462  df-subrg 20486  df-lmod 20796  df-lss 20866  df-sra 21108  df-rgmod 21109  df-dsmm 21670  df-frlm 21685  df-ascl 21793  df-psr 21847  df-mpl 21849  df-opsr 21851  df-psr1 22093  df-ply1 22095  df-mamu 22307  df-mat 22324  df-mat2pmat 22623

This theorem is referenced by:  chfacfscmulcl  22773  chfacfscmulgsum  22776  chfacfpmmulcl  22777  chfacfpmmulgsum  22780