Theorem chfacfscmulfsupp 22777

Description: A mapping of scaled values of the "characteristic factor function" is finitely supported. (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))) − ((𝑇‘𝑀) × (𝑇‘(𝑏‘𝑛))))))))
chfacfscmulcl.x	⊢ 𝑋 = (var1‘𝑅)
chfacfscmulcl.m	⊢ · = ( ·𝑠 ‘𝑌)
chfacfscmulcl.e	⊢ ↑ = (.g‘(mulGrp‘𝑃))

Assertion

Ref	Expression
chfacfscmulfsupp	⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) → (𝑖 ∈ ℕ0 ↦ ((𝑖 ↑ 𝑋) · (𝐺‘𝑖))) finSupp 0 )

Distinct variable groups:   𝐵,𝑛   𝑛,𝑀   𝑛,𝑁   𝑅,𝑛   𝑛,𝑌   𝑛,𝑏   𝑛,𝑠,𝐵   0 ,𝑛   𝐵,𝑖,𝑠   𝑖,𝐺   𝑖,𝑀   𝑖,𝑁   𝑅,𝑖   𝑖,𝑋   𝑖,𝑌   ↑ ,𝑖   · ,𝑏,𝑖

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

Proof of Theorem chfacfscmulfsupp

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

Step	Hyp	Ref	Expression
1		chfacfisf.0	. . . 4 ⊢ 0 = (0g‘𝑌)
2	1	fvexi 6844	. . 3 ⊢ 0 ∈ V
3	2	a1i 11	. 2 ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) → 0 ∈ V)
4		ovexd 7389	. 2 ⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) ∧ 𝑖 ∈ ℕ0) → ((𝑖 ↑ 𝑋) · (𝐺‘𝑖)) ∈ V)
5		nnnn0 12397	. . . . 5 ⊢ (𝑠 ∈ ℕ → 𝑠 ∈ ℕ0)
6		peano2nn0 12430	. . . . 5 ⊢ (𝑠 ∈ ℕ0 → (𝑠 + 1) ∈ ℕ0)
7	5, 6	syl 17	. . . 4 ⊢ (𝑠 ∈ ℕ → (𝑠 + 1) ∈ ℕ0)
8	7	ad2antrl 728	. . 3 ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) → (𝑠 + 1) ∈ ℕ0)
9		vex 3441	. . . . . . 7 ⊢ 𝑘 ∈ V
10		csbov12g 7400	. . . . . . . 8 ⊢ (𝑘 ∈ V → ⦋𝑘 / 𝑖⦌((𝑖 ↑ 𝑋) · (𝐺‘𝑖)) = (⦋𝑘 / 𝑖⦌(𝑖 ↑ 𝑋) · ⦋𝑘 / 𝑖⦌(𝐺‘𝑖)))
11		csbov1g 7401	. . . . . . . . . 10 ⊢ (𝑘 ∈ V → ⦋𝑘 / 𝑖⦌(𝑖 ↑ 𝑋) = (⦋𝑘 / 𝑖⦌𝑖 ↑ 𝑋))
12		csbvarg 4383	. . . . . . . . . . 11 ⊢ (𝑘 ∈ V → ⦋𝑘 / 𝑖⦌𝑖 = 𝑘)
13	12	oveq1d 7369	. . . . . . . . . 10 ⊢ (𝑘 ∈ V → (⦋𝑘 / 𝑖⦌𝑖 ↑ 𝑋) = (𝑘 ↑ 𝑋))
14	11, 13	eqtrd 2768	. . . . . . . . 9 ⊢ (𝑘 ∈ V → ⦋𝑘 / 𝑖⦌(𝑖 ↑ 𝑋) = (𝑘 ↑ 𝑋))
15		csbfv 6877	. . . . . . . . . 10 ⊢ ⦋𝑘 / 𝑖⦌(𝐺‘𝑖) = (𝐺‘𝑘)
16	15	a1i 11	. . . . . . . . 9 ⊢ (𝑘 ∈ V → ⦋𝑘 / 𝑖⦌(𝐺‘𝑖) = (𝐺‘𝑘))
17	14, 16	oveq12d 7372	. . . . . . . 8 ⊢ (𝑘 ∈ V → (⦋𝑘 / 𝑖⦌(𝑖 ↑ 𝑋) · ⦋𝑘 / 𝑖⦌(𝐺‘𝑖)) = ((𝑘 ↑ 𝑋) · (𝐺‘𝑘)))
18	10, 17	eqtrd 2768	. . . . . . 7 ⊢ (𝑘 ∈ V → ⦋𝑘 / 𝑖⦌((𝑖 ↑ 𝑋) · (𝐺‘𝑖)) = ((𝑘 ↑ 𝑋) · (𝐺‘𝑘)))
19	9, 18	mp1i 13	. . . . . 6 ⊢ (((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) ∧ 𝑘 ∈ ℕ0) ∧ (𝑠 + 1) < 𝑘) → ⦋𝑘 / 𝑖⦌((𝑖 ↑ 𝑋) · (𝐺‘𝑖)) = ((𝑘 ↑ 𝑋) · (𝐺‘𝑘)))
20		simplll 774	. . . . . . 7 ⊢ (((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) ∧ 𝑘 ∈ ℕ0) ∧ (𝑠 + 1) < 𝑘) → (𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵))
21		simpllr 775	. . . . . . 7 ⊢ (((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) ∧ 𝑘 ∈ ℕ0) ∧ (𝑠 + 1) < 𝑘) → (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠))))
22	5	adantr 480	. . . . . . . . . . . 12 ⊢ ((𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠))) → 𝑠 ∈ ℕ0)
23	22	ad2antlr 727	. . . . . . . . . . 11 ⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) ∧ 𝑘 ∈ ℕ0) → 𝑠 ∈ ℕ0)
24	23	nn0zd 12502	. . . . . . . . . 10 ⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) ∧ 𝑘 ∈ ℕ0) → 𝑠 ∈ ℤ)
25	24	adantr 480	. . . . . . . . 9 ⊢ (((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) ∧ 𝑘 ∈ ℕ0) ∧ (𝑠 + 1) < 𝑘) → 𝑠 ∈ ℤ)
26		2z 12512	. . . . . . . . . 10 ⊢ 2 ∈ ℤ
27	26	a1i 11	. . . . . . . . 9 ⊢ (((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) ∧ 𝑘 ∈ ℕ0) ∧ (𝑠 + 1) < 𝑘) → 2 ∈ ℤ)
28	25, 27	zaddcld 12589	. . . . . . . 8 ⊢ (((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) ∧ 𝑘 ∈ ℕ0) ∧ (𝑠 + 1) < 𝑘) → (𝑠 + 2) ∈ ℤ)
29		simplr 768	. . . . . . . . 9 ⊢ (((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) ∧ 𝑘 ∈ ℕ0) ∧ (𝑠 + 1) < 𝑘) → 𝑘 ∈ ℕ0)
30	29	nn0zd 12502	. . . . . . . 8 ⊢ (((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) ∧ 𝑘 ∈ ℕ0) ∧ (𝑠 + 1) < 𝑘) → 𝑘 ∈ ℤ)
31	8	nn0zd 12502	. . . . . . . . . . 11 ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) → (𝑠 + 1) ∈ ℤ)
32		nn0z 12501	. . . . . . . . . . 11 ⊢ (𝑘 ∈ ℕ0 → 𝑘 ∈ ℤ)
33		zltp1le 12530	. . . . . . . . . . 11 ⊢ (((𝑠 + 1) ∈ ℤ ∧ 𝑘 ∈ ℤ) → ((𝑠 + 1) < 𝑘 ↔ ((𝑠 + 1) + 1) ≤ 𝑘))
34	31, 32, 33	syl2an 596	. . . . . . . . . 10 ⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) ∧ 𝑘 ∈ ℕ0) → ((𝑠 + 1) < 𝑘 ↔ ((𝑠 + 1) + 1) ≤ 𝑘))
35	34	biimpa 476	. . . . . . . . 9 ⊢ (((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) ∧ 𝑘 ∈ ℕ0) ∧ (𝑠 + 1) < 𝑘) → ((𝑠 + 1) + 1) ≤ 𝑘)
36		nncn 12142	. . . . . . . . . . . . . . 15 ⊢ (𝑠 ∈ ℕ → 𝑠 ∈ ℂ)
37		add1p1 12381	. . . . . . . . . . . . . . 15 ⊢ (𝑠 ∈ ℂ → ((𝑠 + 1) + 1) = (𝑠 + 2))
38	36, 37	syl 17	. . . . . . . . . . . . . 14 ⊢ (𝑠 ∈ ℕ → ((𝑠 + 1) + 1) = (𝑠 + 2))
39	38	breq1d 5105	. . . . . . . . . . . . 13 ⊢ (𝑠 ∈ ℕ → (((𝑠 + 1) + 1) ≤ 𝑘 ↔ (𝑠 + 2) ≤ 𝑘))
40	39	bicomd 223	. . . . . . . . . . . 12 ⊢ (𝑠 ∈ ℕ → ((𝑠 + 2) ≤ 𝑘 ↔ ((𝑠 + 1) + 1) ≤ 𝑘))
41	40	adantr 480	. . . . . . . . . . 11 ⊢ ((𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠))) → ((𝑠 + 2) ≤ 𝑘 ↔ ((𝑠 + 1) + 1) ≤ 𝑘))
42	41	ad2antlr 727	. . . . . . . . . 10 ⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) ∧ 𝑘 ∈ ℕ0) → ((𝑠 + 2) ≤ 𝑘 ↔ ((𝑠 + 1) + 1) ≤ 𝑘))
43	42	adantr 480	. . . . . . . . 9 ⊢ (((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) ∧ 𝑘 ∈ ℕ0) ∧ (𝑠 + 1) < 𝑘) → ((𝑠 + 2) ≤ 𝑘 ↔ ((𝑠 + 1) + 1) ≤ 𝑘))
44	35, 43	mpbird 257	. . . . . . . 8 ⊢ (((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) ∧ 𝑘 ∈ ℕ0) ∧ (𝑠 + 1) < 𝑘) → (𝑠 + 2) ≤ 𝑘)
45		eluz2 12746	. . . . . . . 8 ⊢ (𝑘 ∈ (ℤ≥‘(𝑠 + 2)) ↔ ((𝑠 + 2) ∈ ℤ ∧ 𝑘 ∈ ℤ ∧ (𝑠 + 2) ≤ 𝑘))
46	28, 30, 44, 45	syl3anbrc 1344	. . . . . . 7 ⊢ (((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) ∧ 𝑘 ∈ ℕ0) ∧ (𝑠 + 1) < 𝑘) → 𝑘 ∈ (ℤ≥‘(𝑠 + 2)))
47		chfacfisf.a	. . . . . . . 8 ⊢ 𝐴 = (𝑁 Mat 𝑅)
48		chfacfisf.b	. . . . . . . 8 ⊢ 𝐵 = (Base‘𝐴)
49		chfacfisf.p	. . . . . . . 8 ⊢ 𝑃 = (Poly1‘𝑅)
50		chfacfisf.y	. . . . . . . 8 ⊢ 𝑌 = (𝑁 Mat 𝑃)
51		chfacfisf.r	. . . . . . . 8 ⊢ × = (.r‘𝑌)
52		chfacfisf.s	. . . . . . . 8 ⊢ − = (-g‘𝑌)
53		chfacfisf.t	. . . . . . . 8 ⊢ 𝑇 = (𝑁 matToPolyMat 𝑅)
54		chfacfisf.g	. . . . . . . 8 ⊢ 𝐺 = (𝑛 ∈ ℕ0 ↦ if(𝑛 = 0, ( 0 − ((𝑇‘𝑀) × (𝑇‘(𝑏‘0)))), if(𝑛 = (𝑠 + 1), (𝑇‘(𝑏‘𝑠)), if((𝑠 + 1) < 𝑛, 0 , ((𝑇‘(𝑏‘(𝑛 − 1))) − ((𝑇‘𝑀) × (𝑇‘(𝑏‘𝑛))))))))
55		chfacfscmulcl.x	. . . . . . . 8 ⊢ 𝑋 = (var1‘𝑅)
56		chfacfscmulcl.m	. . . . . . . 8 ⊢ · = ( ·𝑠 ‘𝑌)
57		chfacfscmulcl.e	. . . . . . . 8 ⊢ ↑ = (.g‘(mulGrp‘𝑃))
58	47, 48, 49, 50, 51, 52, 1, 53, 54, 55, 56, 57	chfacfscmul0 22776	. . . . . . 7 ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠))) ∧ 𝑘 ∈ (ℤ≥‘(𝑠 + 2))) → ((𝑘 ↑ 𝑋) · (𝐺‘𝑘)) = 0 )
59	20, 21, 46, 58	syl3anc 1373	. . . . . 6 ⊢ (((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) ∧ 𝑘 ∈ ℕ0) ∧ (𝑠 + 1) < 𝑘) → ((𝑘 ↑ 𝑋) · (𝐺‘𝑘)) = 0 )
60	19, 59	eqtrd 2768	. . . . 5 ⊢ (((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) ∧ 𝑘 ∈ ℕ0) ∧ (𝑠 + 1) < 𝑘) → ⦋𝑘 / 𝑖⦌((𝑖 ↑ 𝑋) · (𝐺‘𝑖)) = 0 )
61	60	ex 412	. . . 4 ⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) ∧ 𝑘 ∈ ℕ0) → ((𝑠 + 1) < 𝑘 → ⦋𝑘 / 𝑖⦌((𝑖 ↑ 𝑋) · (𝐺‘𝑖)) = 0 ))
62	61	ralrimiva 3125	. . 3 ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) → ∀𝑘 ∈ ℕ0 ((𝑠 + 1) < 𝑘 → ⦋𝑘 / 𝑖⦌((𝑖 ↑ 𝑋) · (𝐺‘𝑖)) = 0 ))
63		breq1 5098	. . . 4 ⊢ (𝑧 = (𝑠 + 1) → (𝑧 < 𝑘 ↔ (𝑠 + 1) < 𝑘))
64	63	rspceaimv 3579	. . 3 ⊢ (((𝑠 + 1) ∈ ℕ0 ∧ ∀𝑘 ∈ ℕ0 ((𝑠 + 1) < 𝑘 → ⦋𝑘 / 𝑖⦌((𝑖 ↑ 𝑋) · (𝐺‘𝑖)) = 0 )) → ∃𝑧 ∈ ℕ0 ∀𝑘 ∈ ℕ0 (𝑧 < 𝑘 → ⦋𝑘 / 𝑖⦌((𝑖 ↑ 𝑋) · (𝐺‘𝑖)) = 0 ))
65	8, 62, 64	syl2anc 584	. 2 ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) → ∃𝑧 ∈ ℕ0 ∀𝑘 ∈ ℕ0 (𝑧 < 𝑘 → ⦋𝑘 / 𝑖⦌((𝑖 ↑ 𝑋) · (𝐺‘𝑖)) = 0 ))
66	3, 4, 65	mptnn0fsupp 13908	1 ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) → (𝑖 ∈ ℕ0 ↦ ((𝑖 ↑ 𝑋) · (𝐺‘𝑖))) finSupp 0 )

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   ∧ w3a 1086   = wceq 1541   ∈ wcel 2113  ∀wral 3048  ∃wrex 3057  Vcvv 3437  ⦋csb 3846  ifcif 4476   class class class wbr 5095   ↦ cmpt 5176  ‘cfv 6488  (class class class)co 7354   ↑_m cmap 8758  Fincfn 8877   finSupp cfsupp 9254  ℂcc 11013  0cc0 11015  1c1 11016   + caddc 11018   < clt 11155   ≤ cle 11156   − cmin 11353  ℕcn 12134  2c2 12189  ℕ₀cn0 12390  ℤcz 12477  ℤ_≥cuz 12740  ...cfz 13411  Basecbs 17124  ._rcmulr 17166   ·_𝑠 cvsca 17169  0_gc0g 17347  -_gcsg 18852  ._gcmg 18984  mulGrpcmgp 20062  CRingccrg 20156  var₁cv1 22091  Poly₁cpl1 22092   Mat cmat 22325   matToPolyMat cmat2pmat 22622

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 2115  ax-9 2123  ax-10 2146  ax-11 2162  ax-12 2182  ax-ext 2705  ax-rep 5221  ax-sep 5238  ax-nul 5248  ax-pow 5307  ax-pr 5374  ax-un 7676  ax-cnex 11071  ax-resscn 11072  ax-1cn 11073  ax-icn 11074  ax-addcl 11075  ax-addrcl 11076  ax-mulcl 11077  ax-mulrcl 11078  ax-mulcom 11079  ax-addass 11080  ax-mulass 11081  ax-distr 11082  ax-i2m1 11083  ax-1ne0 11084  ax-1rid 11085  ax-rnegex 11086  ax-rrecex 11087  ax-cnre 11088  ax-pre-lttri 11089  ax-pre-lttrn 11090  ax-pre-ltadd 11091  ax-pre-mulgt0 11092

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 2537  df-eu 2566  df-clab 2712  df-cleq 2725  df-clel 2808  df-nfc 2882  df-ne 2930  df-nel 3034  df-ral 3049  df-rex 3058  df-rmo 3347  df-reu 3348  df-rab 3397  df-v 3439  df-sbc 3738  df-csb 3847  df-dif 3901  df-un 3903  df-in 3905  df-ss 3915  df-pss 3918  df-nul 4283  df-if 4477  df-pw 4553  df-sn 4578  df-pr 4580  df-tp 4582  df-op 4584  df-ot 4586  df-uni 4861  df-int 4900  df-iun 4945  df-iin 4946  df-br 5096  df-opab 5158  df-mpt 5177  df-tr 5203  df-id 5516  df-eprel 5521  df-po 5529  df-so 5530  df-fr 5574  df-se 5575  df-we 5576  df-xp 5627  df-rel 5628  df-cnv 5629  df-co 5630  df-dm 5631  df-rn 5632  df-res 5633  df-ima 5634  df-pred 6255  df-ord 6316  df-on 6317  df-lim 6318  df-suc 6319  df-iota 6444  df-fun 6490  df-fn 6491  df-f 6492  df-f1 6493  df-fo 6494  df-f1o 6495  df-fv 6496  df-isom 6497  df-riota 7311  df-ov 7357  df-oprab 7358  df-mpo 7359  df-of 7618  df-ofr 7619  df-om 7805  df-1st 7929  df-2nd 7930  df-supp 8099  df-frecs 8219  df-wrecs 8250  df-recs 8299  df-rdg 8337  df-1o 8393  df-2o 8394  df-er 8630  df-map 8760  df-pm 8761  df-ixp 8830  df-en 8878  df-dom 8879  df-sdom 8880  df-fin 8881  df-fsupp 9255  df-sup 9335  df-oi 9405  df-card 9841  df-pnf 11157  df-mnf 11158  df-xr 11159  df-ltxr 11160  df-le 11161  df-sub 11355  df-neg 11356  df-nn 12135  df-2 12197  df-3 12198  df-4 12199  df-5 12200  df-6 12201  df-7 12202  df-8 12203  df-9 12204  df-n0 12391  df-z 12478  df-dec 12597  df-uz 12741  df-rp 12895  df-fz 13412  df-fzo 13559  df-seq 13913  df-hash 14242  df-struct 17062  df-sets 17079  df-slot 17097  df-ndx 17109  df-base 17125  df-ress 17146  df-plusg 17178  df-mulr 17179  df-sca 17181  df-vsca 17182  df-ip 17183  df-tset 17184  df-ple 17185  df-ds 17187  df-hom 17189  df-cco 17190  df-0g 17349  df-gsum 17350  df-prds 17355  df-pws 17357  df-mre 17492  df-mrc 17493  df-acs 17495  df-mgm 18552  df-sgrp 18631  df-mnd 18647  df-mhm 18695  df-submnd 18696  df-grp 18853  df-minusg 18854  df-sbg 18855  df-mulg 18985  df-subg 19040  df-ghm 19129  df-cntz 19233  df-cmn 19698  df-abl 19699  df-mgp 20063  df-rng 20075  df-ur 20104  df-ring 20157  df-cring 20158  df-subrng 20465  df-subrg 20489  df-lmod 20799  df-lss 20869  df-sra 21111  df-rgmod 21112  df-dsmm 21673  df-frlm 21688  df-psr 21850  df-mvr 21851  df-mpl 21852  df-opsr 21854  df-psr1 22095  df-vr1 22096  df-ply1 22097  df-mat 22326

This theorem is referenced by:  chfacfscmulgsum  22778