Theorem chcoeffeqlem

Description: Lemma for chcoeffeq . (Contributed by AV, 21-Nov-2019) (Proof shortened by AV, 7-Dec-2019) (Revised by AV, 15-Dec-2019)

	Ref	Expression
Hypotheses	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 𝑅 )
Assertion	chcoeffeqlem	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) → ( ( ( Poly1 ‘ 𝐴 ) Σg ( 𝑛 ∈ ℕ0 ↦ ( ( 𝑈 ‘ ( 𝐺 ‘ 𝑛 ) ) ( ·𝑠 ‘ ( Poly1 ‘ 𝐴 ) ) ( 𝑛 ( .g ‘ ( mulGrp ‘ ( Poly1 ‘ 𝐴 ) ) ) ( var1 ‘ 𝐴 ) ) ) ) ) = ( ( Poly1 ‘ 𝐴 ) Σg ( 𝑛 ∈ ℕ0 ↦ ( ( ( ( coe1 ‘ 𝐾 ) ‘ 𝑛 ) ∗ 1 ) ( ·𝑠 ‘ ( Poly1 ‘ 𝐴 ) ) ( 𝑛 ( .g ‘ ( mulGrp ‘ ( Poly1 ‘ 𝐴 ) ) ) ( var1 ‘ 𝐴 ) ) ) ) ) → ∀ 𝑛 ∈ ℕ0 ( 𝑈 ‘ ( 𝐺 ‘ 𝑛 ) ) = ( ( ( coe1 ‘ 𝐾 ) ‘ 𝑛 ) ∗ 1 ) ) )

Proof

Step	Hyp	Ref	Expression
1		chcoeffeq.a	⊢ 𝐴 = ( 𝑁 Mat 𝑅 )
2		chcoeffeq.b	⊢ 𝐵 = ( Base ‘ 𝐴 )
3		chcoeffeq.p	⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
4		chcoeffeq.y	⊢ 𝑌 = ( 𝑁 Mat 𝑃 )
5		chcoeffeq.r	⊢ × = ( .r ‘ 𝑌 )
6		chcoeffeq.s	⊢ − = ( -g ‘ 𝑌 )
7		chcoeffeq.0	⊢ 0 = ( 0g ‘ 𝑌 )
8		chcoeffeq.t	⊢ 𝑇 = ( 𝑁 matToPolyMat 𝑅 )
9		chcoeffeq.c	⊢ 𝐶 = ( 𝑁 CharPlyMat 𝑅 )
10		chcoeffeq.k	⊢ 𝐾 = ( 𝐶 ‘ 𝑀 )
11		chcoeffeq.g	⊢ 𝐺 = ( 𝑛 ∈ ℕ0 ↦ if ( 𝑛 = 0 , ( 0 − ( ( 𝑇 ‘ 𝑀 ) × ( 𝑇 ‘ ( 𝑏 ‘ 0 ) ) ) ) , if ( 𝑛 = ( 𝑠 + 1 ) , ( 𝑇 ‘ ( 𝑏 ‘ 𝑠 ) ) , if ( ( 𝑠 + 1 ) < 𝑛 , 0 , ( ( 𝑇 ‘ ( 𝑏 ‘ ( 𝑛 − 1 ) ) ) − ( ( 𝑇 ‘ 𝑀 ) × ( 𝑇 ‘ ( 𝑏 ‘ 𝑛 ) ) ) ) ) ) ) )
12		chcoeffeq.w	⊢ 𝑊 = ( Base ‘ 𝑌 )
13		chcoeffeq.1	⊢ 1 = ( 1r ‘ 𝐴 )
14		chcoeffeq.m	⊢ ∗ = ( ·𝑠 ‘ 𝐴 )
15		chcoeffeq.u	⊢ 𝑈 = ( 𝑁 cPolyMatToMat 𝑅 )
16		eqid	⊢ ( Poly1 ‘ 𝐴 ) = ( Poly1 ‘ 𝐴 )
17		eqid	⊢ ( var1 ‘ 𝐴 ) = ( var1 ‘ 𝐴 )
18		eqid	⊢ ( .g ‘ ( mulGrp ‘ ( Poly1 ‘ 𝐴 ) ) ) = ( .g ‘ ( mulGrp ‘ ( Poly1 ‘ 𝐴 ) ) )
19		crngring	⊢ ( 𝑅 ∈ CRing → 𝑅 ∈ Ring )
20	1	matring	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → 𝐴 ∈ Ring )
21	19 20	sylan2	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) → 𝐴 ∈ Ring )
22	21	3adant3	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) → 𝐴 ∈ Ring )
23	22	adantr	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) → 𝐴 ∈ Ring )
24		eqid	⊢ ( ·𝑠 ‘ ( Poly1 ‘ 𝐴 ) ) = ( ·𝑠 ‘ ( Poly1 ‘ 𝐴 ) )
25		eqid	⊢ ( 0g ‘ 𝐴 ) = ( 0g ‘ 𝐴 )
26		eqid	⊢ ( 𝑁 ConstPolyMat 𝑅 ) = ( 𝑁 ConstPolyMat 𝑅 )
27		eqid	⊢ ( ·𝑠 ‘ 𝑌 ) = ( ·𝑠 ‘ 𝑌 )
28		eqid	⊢ ( 1r ‘ 𝑌 ) = ( 1r ‘ 𝑌 )
29		eqid	⊢ ( var1 ‘ 𝑅 ) = ( var1 ‘ 𝑅 )
30		eqid	⊢ ( ( ( var1 ‘ 𝑅 ) ( ·𝑠 ‘ 𝑌 ) ( 1r ‘ 𝑌 ) ) − ( 𝑇 ‘ 𝑀 ) ) = ( ( ( var1 ‘ 𝑅 ) ( ·𝑠 ‘ 𝑌 ) ( 1r ‘ 𝑌 ) ) − ( 𝑇 ‘ 𝑀 ) )
31		eqid	⊢ ( 𝑁 maAdju 𝑃 ) = ( 𝑁 maAdju 𝑃 )
32	1 2 3 4 8 5 6 7 11 26 27 28 29 30 31 12 16 17 24 18 15	cpmadumatpolylem1	⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑠 ∈ ℕ ) ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) → ( 𝑈 ∘ 𝐺 ) ∈ ( 𝐵 ↑m ℕ0 ) )
33	32	anasss	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) → ( 𝑈 ∘ 𝐺 ) ∈ ( 𝐵 ↑m ℕ0 ) )
34	1 2 3 4 5 6 7 8 11 26	chfacfisfcpmat	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) → 𝐺 : ℕ0 ⟶ ( 𝑁 ConstPolyMat 𝑅 ) )
35	19 34	syl3anl2	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) → 𝐺 : ℕ0 ⟶ ( 𝑁 ConstPolyMat 𝑅 ) )
36	35	adantr	⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) ∧ ( 𝑈 ∘ 𝐺 ) ∈ ( 𝐵 ↑m ℕ0 ) ) → 𝐺 : ℕ0 ⟶ ( 𝑁 ConstPolyMat 𝑅 ) )
37		fvco3	⊢ ( ( 𝐺 : ℕ0 ⟶ ( 𝑁 ConstPolyMat 𝑅 ) ∧ 𝑙 ∈ ℕ0 ) → ( ( 𝑈 ∘ 𝐺 ) ‘ 𝑙 ) = ( 𝑈 ‘ ( 𝐺 ‘ 𝑙 ) ) )
38	37	eqcomd	⊢ ( ( 𝐺 : ℕ0 ⟶ ( 𝑁 ConstPolyMat 𝑅 ) ∧ 𝑙 ∈ ℕ0 ) → ( 𝑈 ‘ ( 𝐺 ‘ 𝑙 ) ) = ( ( 𝑈 ∘ 𝐺 ) ‘ 𝑙 ) )
39	36 38	sylan	⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) ∧ ( 𝑈 ∘ 𝐺 ) ∈ ( 𝐵 ↑m ℕ0 ) ) ∧ 𝑙 ∈ ℕ0 ) → ( 𝑈 ‘ ( 𝐺 ‘ 𝑙 ) ) = ( ( 𝑈 ∘ 𝐺 ) ‘ 𝑙 ) )
40		elmapi	⊢ ( ( 𝑈 ∘ 𝐺 ) ∈ ( 𝐵 ↑m ℕ0 ) → ( 𝑈 ∘ 𝐺 ) : ℕ0 ⟶ 𝐵 )
41	40	adantl	⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) ∧ ( 𝑈 ∘ 𝐺 ) ∈ ( 𝐵 ↑m ℕ0 ) ) → ( 𝑈 ∘ 𝐺 ) : ℕ0 ⟶ 𝐵 )
42	41	ffvelcdmda	⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) ∧ ( 𝑈 ∘ 𝐺 ) ∈ ( 𝐵 ↑m ℕ0 ) ) ∧ 𝑙 ∈ ℕ0 ) → ( ( 𝑈 ∘ 𝐺 ) ‘ 𝑙 ) ∈ 𝐵 )
43	39 42	eqeltrd	⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) ∧ ( 𝑈 ∘ 𝐺 ) ∈ ( 𝐵 ↑m ℕ0 ) ) ∧ 𝑙 ∈ ℕ0 ) → ( 𝑈 ‘ ( 𝐺 ‘ 𝑙 ) ) ∈ 𝐵 )
44	43	ralrimiva	⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) ∧ ( 𝑈 ∘ 𝐺 ) ∈ ( 𝐵 ↑m ℕ0 ) ) → ∀ 𝑙 ∈ ℕ0 ( 𝑈 ‘ ( 𝐺 ‘ 𝑙 ) ) ∈ 𝐵 )
45	33 44	mpdan	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) → ∀ 𝑙 ∈ ℕ0 ( 𝑈 ‘ ( 𝐺 ‘ 𝑙 ) ) ∈ 𝐵 )
46	19	anim2i	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) → ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) )
47	46	3adant3	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) → ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) )
48	47	adantr	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) → ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) )
49	1 2 26 15	cpm2mf	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → 𝑈 : ( 𝑁 ConstPolyMat 𝑅 ) ⟶ 𝐵 )
50	48 49	syl	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) → 𝑈 : ( 𝑁 ConstPolyMat 𝑅 ) ⟶ 𝐵 )
51		fcompt	⊢ ( ( 𝑈 : ( 𝑁 ConstPolyMat 𝑅 ) ⟶ 𝐵 ∧ 𝐺 : ℕ0 ⟶ ( 𝑁 ConstPolyMat 𝑅 ) ) → ( 𝑈 ∘ 𝐺 ) = ( 𝑙 ∈ ℕ0 ↦ ( 𝑈 ‘ ( 𝐺 ‘ 𝑙 ) ) ) )
52	50 35 51	syl2anc	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) → ( 𝑈 ∘ 𝐺 ) = ( 𝑙 ∈ ℕ0 ↦ ( 𝑈 ‘ ( 𝐺 ‘ 𝑙 ) ) ) )
53	1 2 3 4 8 5 6 7 11 26 27 28 29 30 31 12 16 17 24 18 15	cpmadumatpolylem2	⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑠 ∈ ℕ ) ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) → ( 𝑈 ∘ 𝐺 ) finSupp ( 0g ‘ 𝐴 ) )
54	53	anasss	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) → ( 𝑈 ∘ 𝐺 ) finSupp ( 0g ‘ 𝐴 ) )
55	52 54	eqbrtrrd	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) → ( 𝑙 ∈ ℕ0 ↦ ( 𝑈 ‘ ( 𝐺 ‘ 𝑙 ) ) ) finSupp ( 0g ‘ 𝐴 ) )
56		simpll1	⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) ∧ 𝑙 ∈ ℕ0 ) → 𝑁 ∈ Fin )
57	19	3ad2ant2	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) → 𝑅 ∈ Ring )
58	57	ad2antrr	⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) ∧ 𝑙 ∈ ℕ0 ) → 𝑅 ∈ Ring )
59		eqid	⊢ ( Base ‘ 𝑃 ) = ( Base ‘ 𝑃 )
60	9 1 2 3 59	chpmatply1	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) → ( 𝐶 ‘ 𝑀 ) ∈ ( Base ‘ 𝑃 ) )
61	10 60	eqeltrid	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) → 𝐾 ∈ ( Base ‘ 𝑃 ) )
62		eqid	⊢ ( coe1 ‘ 𝐾 ) = ( coe1 ‘ 𝐾 )
63		eqid	⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
64	62 59 3 63	coe1fvalcl	⊢ ( ( 𝐾 ∈ ( Base ‘ 𝑃 ) ∧ 𝑙 ∈ ℕ0 ) → ( ( coe1 ‘ 𝐾 ) ‘ 𝑙 ) ∈ ( Base ‘ 𝑅 ) )
65	61 64	sylan	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑙 ∈ ℕ0 ) → ( ( coe1 ‘ 𝐾 ) ‘ 𝑙 ) ∈ ( Base ‘ 𝑅 ) )
66	65	adantlr	⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) ∧ 𝑙 ∈ ℕ0 ) → ( ( coe1 ‘ 𝐾 ) ‘ 𝑙 ) ∈ ( Base ‘ 𝑅 ) )
67	2 13	ringidcl	⊢ ( 𝐴 ∈ Ring → 1 ∈ 𝐵 )
68	22 67	syl	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) → 1 ∈ 𝐵 )
69	68	ad2antrr	⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) ∧ 𝑙 ∈ ℕ0 ) → 1 ∈ 𝐵 )
70	63 1 2 14	matvscl	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( ( ( coe1 ‘ 𝐾 ) ‘ 𝑙 ) ∈ ( Base ‘ 𝑅 ) ∧ 1 ∈ 𝐵 ) ) → ( ( ( coe1 ‘ 𝐾 ) ‘ 𝑙 ) ∗ 1 ) ∈ 𝐵 )
71	56 58 66 69 70	syl22anc	⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) ∧ 𝑙 ∈ ℕ0 ) → ( ( ( coe1 ‘ 𝐾 ) ‘ 𝑙 ) ∗ 1 ) ∈ 𝐵 )
72	71	ralrimiva	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) → ∀ 𝑙 ∈ ℕ0 ( ( ( coe1 ‘ 𝐾 ) ‘ 𝑙 ) ∗ 1 ) ∈ 𝐵 )
73		nn0ex	⊢ ℕ0 ∈ V
74	73	a1i	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) → ℕ0 ∈ V )
75	1	matlmod	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → 𝐴 ∈ LMod )
76	19 75	sylan2	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) → 𝐴 ∈ LMod )
77	76	3adant3	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) → 𝐴 ∈ LMod )
78	77	adantr	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) → 𝐴 ∈ LMod )
79		eqidd	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) → ( Scalar ‘ 𝐴 ) = ( Scalar ‘ 𝐴 ) )
80		fvexd	⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) ∧ 𝑙 ∈ ℕ0 ) → ( ( coe1 ‘ 𝐾 ) ‘ 𝑙 ) ∈ V )
81		eqid	⊢ ( 0g ‘ ( Scalar ‘ 𝐴 ) ) = ( 0g ‘ ( Scalar ‘ 𝐴 ) )
82	1	matsca2	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) → 𝑅 = ( Scalar ‘ 𝐴 ) )
83	82	3adant3	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) → 𝑅 = ( Scalar ‘ 𝐴 ) )
84	83 57	eqeltrrd	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) → ( Scalar ‘ 𝐴 ) ∈ Ring )
85	83	eqcomd	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) → ( Scalar ‘ 𝐴 ) = 𝑅 )
86	85	fveq2d	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) → ( Poly1 ‘ ( Scalar ‘ 𝐴 ) ) = ( Poly1 ‘ 𝑅 ) )
87	86 3	eqtr4di	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) → ( Poly1 ‘ ( Scalar ‘ 𝐴 ) ) = 𝑃 )
88	87	fveq2d	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) → ( Base ‘ ( Poly1 ‘ ( Scalar ‘ 𝐴 ) ) ) = ( Base ‘ 𝑃 ) )
89	61 88	eleqtrrd	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) → 𝐾 ∈ ( Base ‘ ( Poly1 ‘ ( Scalar ‘ 𝐴 ) ) ) )
90		eqid	⊢ ( Poly1 ‘ ( Scalar ‘ 𝐴 ) ) = ( Poly1 ‘ ( Scalar ‘ 𝐴 ) )
91		eqid	⊢ ( Base ‘ ( Poly1 ‘ ( Scalar ‘ 𝐴 ) ) ) = ( Base ‘ ( Poly1 ‘ ( Scalar ‘ 𝐴 ) ) )
92	90 91 81	mptcoe1fsupp	⊢ ( ( ( Scalar ‘ 𝐴 ) ∈ Ring ∧ 𝐾 ∈ ( Base ‘ ( Poly1 ‘ ( Scalar ‘ 𝐴 ) ) ) ) → ( 𝑙 ∈ ℕ0 ↦ ( ( coe1 ‘ 𝐾 ) ‘ 𝑙 ) ) finSupp ( 0g ‘ ( Scalar ‘ 𝐴 ) ) )
93	84 89 92	syl2anc	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) → ( 𝑙 ∈ ℕ0 ↦ ( ( coe1 ‘ 𝐾 ) ‘ 𝑙 ) ) finSupp ( 0g ‘ ( Scalar ‘ 𝐴 ) ) )
94	93	adantr	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) → ( 𝑙 ∈ ℕ0 ↦ ( ( coe1 ‘ 𝐾 ) ‘ 𝑙 ) ) finSupp ( 0g ‘ ( Scalar ‘ 𝐴 ) ) )
95	74 78 79 2 80 69 25 81 14 94	mptscmfsupp0	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) → ( 𝑙 ∈ ℕ0 ↦ ( ( ( coe1 ‘ 𝐾 ) ‘ 𝑙 ) ∗ 1 ) ) finSupp ( 0g ‘ 𝐴 ) )
96		2fveq3	⊢ ( 𝑛 = 𝑙 → ( 𝑈 ‘ ( 𝐺 ‘ 𝑛 ) ) = ( 𝑈 ‘ ( 𝐺 ‘ 𝑙 ) ) )
97		oveq1	⊢ ( 𝑛 = 𝑙 → ( 𝑛 ( .g ‘ ( mulGrp ‘ ( Poly1 ‘ 𝐴 ) ) ) ( var1 ‘ 𝐴 ) ) = ( 𝑙 ( .g ‘ ( mulGrp ‘ ( Poly1 ‘ 𝐴 ) ) ) ( var1 ‘ 𝐴 ) ) )
98	96 97	oveq12d	⊢ ( 𝑛 = 𝑙 → ( ( 𝑈 ‘ ( 𝐺 ‘ 𝑛 ) ) ( ·𝑠 ‘ ( Poly1 ‘ 𝐴 ) ) ( 𝑛 ( .g ‘ ( mulGrp ‘ ( Poly1 ‘ 𝐴 ) ) ) ( var1 ‘ 𝐴 ) ) ) = ( ( 𝑈 ‘ ( 𝐺 ‘ 𝑙 ) ) ( ·𝑠 ‘ ( Poly1 ‘ 𝐴 ) ) ( 𝑙 ( .g ‘ ( mulGrp ‘ ( Poly1 ‘ 𝐴 ) ) ) ( var1 ‘ 𝐴 ) ) ) )
99	98	cbvmptv	⊢ ( 𝑛 ∈ ℕ0 ↦ ( ( 𝑈 ‘ ( 𝐺 ‘ 𝑛 ) ) ( ·𝑠 ‘ ( Poly1 ‘ 𝐴 ) ) ( 𝑛 ( .g ‘ ( mulGrp ‘ ( Poly1 ‘ 𝐴 ) ) ) ( var1 ‘ 𝐴 ) ) ) ) = ( 𝑙 ∈ ℕ0 ↦ ( ( 𝑈 ‘ ( 𝐺 ‘ 𝑙 ) ) ( ·𝑠 ‘ ( Poly1 ‘ 𝐴 ) ) ( 𝑙 ( .g ‘ ( mulGrp ‘ ( Poly1 ‘ 𝐴 ) ) ) ( var1 ‘ 𝐴 ) ) ) )
100	99	oveq2i	⊢ ( ( Poly1 ‘ 𝐴 ) Σg ( 𝑛 ∈ ℕ0 ↦ ( ( 𝑈 ‘ ( 𝐺 ‘ 𝑛 ) ) ( ·𝑠 ‘ ( Poly1 ‘ 𝐴 ) ) ( 𝑛 ( .g ‘ ( mulGrp ‘ ( Poly1 ‘ 𝐴 ) ) ) ( var1 ‘ 𝐴 ) ) ) ) ) = ( ( Poly1 ‘ 𝐴 ) Σg ( 𝑙 ∈ ℕ0 ↦ ( ( 𝑈 ‘ ( 𝐺 ‘ 𝑙 ) ) ( ·𝑠 ‘ ( Poly1 ‘ 𝐴 ) ) ( 𝑙 ( .g ‘ ( mulGrp ‘ ( Poly1 ‘ 𝐴 ) ) ) ( var1 ‘ 𝐴 ) ) ) ) )
101	100	a1i	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) → ( ( Poly1 ‘ 𝐴 ) Σg ( 𝑛 ∈ ℕ0 ↦ ( ( 𝑈 ‘ ( 𝐺 ‘ 𝑛 ) ) ( ·𝑠 ‘ ( Poly1 ‘ 𝐴 ) ) ( 𝑛 ( .g ‘ ( mulGrp ‘ ( Poly1 ‘ 𝐴 ) ) ) ( var1 ‘ 𝐴 ) ) ) ) ) = ( ( Poly1 ‘ 𝐴 ) Σg ( 𝑙 ∈ ℕ0 ↦ ( ( 𝑈 ‘ ( 𝐺 ‘ 𝑙 ) ) ( ·𝑠 ‘ ( Poly1 ‘ 𝐴 ) ) ( 𝑙 ( .g ‘ ( mulGrp ‘ ( Poly1 ‘ 𝐴 ) ) ) ( var1 ‘ 𝐴 ) ) ) ) ) )
102		fveq2	⊢ ( 𝑛 = 𝑙 → ( ( coe1 ‘ 𝐾 ) ‘ 𝑛 ) = ( ( coe1 ‘ 𝐾 ) ‘ 𝑙 ) )
103	102	oveq1d	⊢ ( 𝑛 = 𝑙 → ( ( ( coe1 ‘ 𝐾 ) ‘ 𝑛 ) ∗ 1 ) = ( ( ( coe1 ‘ 𝐾 ) ‘ 𝑙 ) ∗ 1 ) )
104	103 97	oveq12d	⊢ ( 𝑛 = 𝑙 → ( ( ( ( coe1 ‘ 𝐾 ) ‘ 𝑛 ) ∗ 1 ) ( ·𝑠 ‘ ( Poly1 ‘ 𝐴 ) ) ( 𝑛 ( .g ‘ ( mulGrp ‘ ( Poly1 ‘ 𝐴 ) ) ) ( var1 ‘ 𝐴 ) ) ) = ( ( ( ( coe1 ‘ 𝐾 ) ‘ 𝑙 ) ∗ 1 ) ( ·𝑠 ‘ ( Poly1 ‘ 𝐴 ) ) ( 𝑙 ( .g ‘ ( mulGrp ‘ ( Poly1 ‘ 𝐴 ) ) ) ( var1 ‘ 𝐴 ) ) ) )
105	104	cbvmptv	⊢ ( 𝑛 ∈ ℕ0 ↦ ( ( ( ( coe1 ‘ 𝐾 ) ‘ 𝑛 ) ∗ 1 ) ( ·𝑠 ‘ ( Poly1 ‘ 𝐴 ) ) ( 𝑛 ( .g ‘ ( mulGrp ‘ ( Poly1 ‘ 𝐴 ) ) ) ( var1 ‘ 𝐴 ) ) ) ) = ( 𝑙 ∈ ℕ0 ↦ ( ( ( ( coe1 ‘ 𝐾 ) ‘ 𝑙 ) ∗ 1 ) ( ·𝑠 ‘ ( Poly1 ‘ 𝐴 ) ) ( 𝑙 ( .g ‘ ( mulGrp ‘ ( Poly1 ‘ 𝐴 ) ) ) ( var1 ‘ 𝐴 ) ) ) )
106	105	oveq2i	⊢ ( ( Poly1 ‘ 𝐴 ) Σg ( 𝑛 ∈ ℕ0 ↦ ( ( ( ( coe1 ‘ 𝐾 ) ‘ 𝑛 ) ∗ 1 ) ( ·𝑠 ‘ ( Poly1 ‘ 𝐴 ) ) ( 𝑛 ( .g ‘ ( mulGrp ‘ ( Poly1 ‘ 𝐴 ) ) ) ( var1 ‘ 𝐴 ) ) ) ) ) = ( ( Poly1 ‘ 𝐴 ) Σg ( 𝑙 ∈ ℕ0 ↦ ( ( ( ( coe1 ‘ 𝐾 ) ‘ 𝑙 ) ∗ 1 ) ( ·𝑠 ‘ ( Poly1 ‘ 𝐴 ) ) ( 𝑙 ( .g ‘ ( mulGrp ‘ ( Poly1 ‘ 𝐴 ) ) ) ( var1 ‘ 𝐴 ) ) ) ) )
107	106	a1i	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) → ( ( Poly1 ‘ 𝐴 ) Σg ( 𝑛 ∈ ℕ0 ↦ ( ( ( ( coe1 ‘ 𝐾 ) ‘ 𝑛 ) ∗ 1 ) ( ·𝑠 ‘ ( Poly1 ‘ 𝐴 ) ) ( 𝑛 ( .g ‘ ( mulGrp ‘ ( Poly1 ‘ 𝐴 ) ) ) ( var1 ‘ 𝐴 ) ) ) ) ) = ( ( Poly1 ‘ 𝐴 ) Σg ( 𝑙 ∈ ℕ0 ↦ ( ( ( ( coe1 ‘ 𝐾 ) ‘ 𝑙 ) ∗ 1 ) ( ·𝑠 ‘ ( Poly1 ‘ 𝐴 ) ) ( 𝑙 ( .g ‘ ( mulGrp ‘ ( Poly1 ‘ 𝐴 ) ) ) ( var1 ‘ 𝐴 ) ) ) ) ) )
108	16 17 18 23 2 24 25 45 55 72 95 101 107	gsumply1eq	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) → ( ( ( Poly1 ‘ 𝐴 ) Σg ( 𝑛 ∈ ℕ0 ↦ ( ( 𝑈 ‘ ( 𝐺 ‘ 𝑛 ) ) ( ·𝑠 ‘ ( Poly1 ‘ 𝐴 ) ) ( 𝑛 ( .g ‘ ( mulGrp ‘ ( Poly1 ‘ 𝐴 ) ) ) ( var1 ‘ 𝐴 ) ) ) ) ) = ( ( Poly1 ‘ 𝐴 ) Σg ( 𝑛 ∈ ℕ0 ↦ ( ( ( ( coe1 ‘ 𝐾 ) ‘ 𝑛 ) ∗ 1 ) ( ·𝑠 ‘ ( Poly1 ‘ 𝐴 ) ) ( 𝑛 ( .g ‘ ( mulGrp ‘ ( Poly1 ‘ 𝐴 ) ) ) ( var1 ‘ 𝐴 ) ) ) ) ) ↔ ∀ 𝑙 ∈ ℕ0 ( 𝑈 ‘ ( 𝐺 ‘ 𝑙 ) ) = ( ( ( coe1 ‘ 𝐾 ) ‘ 𝑙 ) ∗ 1 ) ) )
109	108	biimpa	⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) ∧ ( ( Poly1 ‘ 𝐴 ) Σg ( 𝑛 ∈ ℕ0 ↦ ( ( 𝑈 ‘ ( 𝐺 ‘ 𝑛 ) ) ( ·𝑠 ‘ ( Poly1 ‘ 𝐴 ) ) ( 𝑛 ( .g ‘ ( mulGrp ‘ ( Poly1 ‘ 𝐴 ) ) ) ( var1 ‘ 𝐴 ) ) ) ) ) = ( ( Poly1 ‘ 𝐴 ) Σg ( 𝑛 ∈ ℕ0 ↦ ( ( ( ( coe1 ‘ 𝐾 ) ‘ 𝑛 ) ∗ 1 ) ( ·𝑠 ‘ ( Poly1 ‘ 𝐴 ) ) ( 𝑛 ( .g ‘ ( mulGrp ‘ ( Poly1 ‘ 𝐴 ) ) ) ( var1 ‘ 𝐴 ) ) ) ) ) ) → ∀ 𝑙 ∈ ℕ0 ( 𝑈 ‘ ( 𝐺 ‘ 𝑙 ) ) = ( ( ( coe1 ‘ 𝐾 ) ‘ 𝑙 ) ∗ 1 ) )
110	96 103	eqeq12d	⊢ ( 𝑛 = 𝑙 → ( ( 𝑈 ‘ ( 𝐺 ‘ 𝑛 ) ) = ( ( ( coe1 ‘ 𝐾 ) ‘ 𝑛 ) ∗ 1 ) ↔ ( 𝑈 ‘ ( 𝐺 ‘ 𝑙 ) ) = ( ( ( coe1 ‘ 𝐾 ) ‘ 𝑙 ) ∗ 1 ) ) )
111	110	cbvralvw	⊢ ( ∀ 𝑛 ∈ ℕ0 ( 𝑈 ‘ ( 𝐺 ‘ 𝑛 ) ) = ( ( ( coe1 ‘ 𝐾 ) ‘ 𝑛 ) ∗ 1 ) ↔ ∀ 𝑙 ∈ ℕ0 ( 𝑈 ‘ ( 𝐺 ‘ 𝑙 ) ) = ( ( ( coe1 ‘ 𝐾 ) ‘ 𝑙 ) ∗ 1 ) )
112	109 111	sylibr	⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) ∧ ( ( Poly1 ‘ 𝐴 ) Σg ( 𝑛 ∈ ℕ0 ↦ ( ( 𝑈 ‘ ( 𝐺 ‘ 𝑛 ) ) ( ·𝑠 ‘ ( Poly1 ‘ 𝐴 ) ) ( 𝑛 ( .g ‘ ( mulGrp ‘ ( Poly1 ‘ 𝐴 ) ) ) ( var1 ‘ 𝐴 ) ) ) ) ) = ( ( Poly1 ‘ 𝐴 ) Σg ( 𝑛 ∈ ℕ0 ↦ ( ( ( ( coe1 ‘ 𝐾 ) ‘ 𝑛 ) ∗ 1 ) ( ·𝑠 ‘ ( Poly1 ‘ 𝐴 ) ) ( 𝑛 ( .g ‘ ( mulGrp ‘ ( Poly1 ‘ 𝐴 ) ) ) ( var1 ‘ 𝐴 ) ) ) ) ) ) → ∀ 𝑛 ∈ ℕ0 ( 𝑈 ‘ ( 𝐺 ‘ 𝑛 ) ) = ( ( ( coe1 ‘ 𝐾 ) ‘ 𝑛 ) ∗ 1 ) )
113	112	ex	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝑠 ∈ ℕ ∧ 𝑏 ∈ ( 𝐵 ↑m ( 0 ... 𝑠 ) ) ) ) → ( ( ( Poly1 ‘ 𝐴 ) Σg ( 𝑛 ∈ ℕ0 ↦ ( ( 𝑈 ‘ ( 𝐺 ‘ 𝑛 ) ) ( ·𝑠 ‘ ( Poly1 ‘ 𝐴 ) ) ( 𝑛 ( .g ‘ ( mulGrp ‘ ( Poly1 ‘ 𝐴 ) ) ) ( var1 ‘ 𝐴 ) ) ) ) ) = ( ( Poly1 ‘ 𝐴 ) Σg ( 𝑛 ∈ ℕ0 ↦ ( ( ( ( coe1 ‘ 𝐾 ) ‘ 𝑛 ) ∗ 1 ) ( ·𝑠 ‘ ( Poly1 ‘ 𝐴 ) ) ( 𝑛 ( .g ‘ ( mulGrp ‘ ( Poly1 ‘ 𝐴 ) ) ) ( var1 ‘ 𝐴 ) ) ) ) ) → ∀ 𝑛 ∈ ℕ0 ( 𝑈 ‘ ( 𝐺 ‘ 𝑛 ) ) = ( ( ( coe1 ‘ 𝐾 ) ‘ 𝑛 ) ∗ 1 ) ) )