Theorem ply1coe

Description: Decompose a univariate polynomial as a sum of powers. (Contributed by Stefan O'Rear, 21-Mar-2015) (Revised by AV, 7-Oct-2019)

	Ref	Expression
Hypotheses	ply1coe.p	⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
	ply1coe.x	⊢ 𝑋 = ( var1 ‘ 𝑅 )
	ply1coe.b	⊢ 𝐵 = ( Base ‘ 𝑃 )
	ply1coe.n	⊢ · = ( ·𝑠 ‘ 𝑃 )
	ply1coe.m	⊢ 𝑀 = ( mulGrp ‘ 𝑃 )
	ply1coe.e	⊢ ↑ = ( .g ‘ 𝑀 )
	ply1coe.a	⊢ 𝐴 = ( coe1 ‘ 𝐾 )
Assertion	ply1coe	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ) → 𝐾 = ( 𝑃 Σg ( 𝑘 ∈ ℕ0 ↦ ( ( 𝐴 ‘ 𝑘 ) · ( 𝑘 ↑ 𝑋 ) ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		ply1coe.p	⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
2		ply1coe.x	⊢ 𝑋 = ( var1 ‘ 𝑅 )
3		ply1coe.b	⊢ 𝐵 = ( Base ‘ 𝑃 )
4		ply1coe.n	⊢ · = ( ·𝑠 ‘ 𝑃 )
5		ply1coe.m	⊢ 𝑀 = ( mulGrp ‘ 𝑃 )
6		ply1coe.e	⊢ ↑ = ( .g ‘ 𝑀 )
7		ply1coe.a	⊢ 𝐴 = ( coe1 ‘ 𝐾 )
8		eqid	⊢ ( 1o mPoly 𝑅 ) = ( 1o mPoly 𝑅 )
9		psr1baslem	⊢ ( ℕ0 ↑m 1o ) = { 𝑑 ∈ ( ℕ0 ↑m 1o ) ∣ ( ◡ 𝑑 “ ℕ ) ∈ Fin }
10		eqid	⊢ ( 0g ‘ 𝑅 ) = ( 0g ‘ 𝑅 )
11		eqid	⊢ ( 1r ‘ 𝑅 ) = ( 1r ‘ 𝑅 )
12		1onn	⊢ 1o ∈ ω
13	12	a1i	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ) → 1o ∈ ω )
14		eqid	⊢ ( PwSer1 ‘ 𝑅 ) = ( PwSer1 ‘ 𝑅 )
15	1 14 3	ply1bas	⊢ 𝐵 = ( Base ‘ ( 1o mPoly 𝑅 ) )
16	1 8 4	ply1vsca	⊢ · = ( ·𝑠 ‘ ( 1o mPoly 𝑅 ) )
17		simpl	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ) → 𝑅 ∈ Ring )
18		simpr	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ) → 𝐾 ∈ 𝐵 )
19	8 9 10 11 13 15 16 17 18	mplcoe1	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ) → 𝐾 = ( ( 1o mPoly 𝑅 ) Σg ( 𝑎 ∈ ( ℕ0 ↑m 1o ) ↦ ( ( 𝐾 ‘ 𝑎 ) · ( 𝑏 ∈ ( ℕ0 ↑m 1o ) ↦ if ( 𝑏 = 𝑎 , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) ) ) ) ) )
20	7	fvcoe1	⊢ ( ( 𝐾 ∈ 𝐵 ∧ 𝑎 ∈ ( ℕ0 ↑m 1o ) ) → ( 𝐾 ‘ 𝑎 ) = ( 𝐴 ‘ ( 𝑎 ‘ ∅ ) ) )
21	20	adantll	⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ) ∧ 𝑎 ∈ ( ℕ0 ↑m 1o ) ) → ( 𝐾 ‘ 𝑎 ) = ( 𝐴 ‘ ( 𝑎 ‘ ∅ ) ) )
22	12	a1i	⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ) ∧ 𝑎 ∈ ( ℕ0 ↑m 1o ) ) → 1o ∈ ω )
23		eqid	⊢ ( mulGrp ‘ ( 1o mPoly 𝑅 ) ) = ( mulGrp ‘ ( 1o mPoly 𝑅 ) )
24		eqid	⊢ ( .g ‘ ( mulGrp ‘ ( 1o mPoly 𝑅 ) ) ) = ( .g ‘ ( mulGrp ‘ ( 1o mPoly 𝑅 ) ) )
25		eqid	⊢ ( 1o mVar 𝑅 ) = ( 1o mVar 𝑅 )
26		simpll	⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ) ∧ 𝑎 ∈ ( ℕ0 ↑m 1o ) ) → 𝑅 ∈ Ring )
27		simpr	⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ) ∧ 𝑎 ∈ ( ℕ0 ↑m 1o ) ) → 𝑎 ∈ ( ℕ0 ↑m 1o ) )
28		eqidd	⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ) ∧ 𝑎 ∈ ( ℕ0 ↑m 1o ) ) → ( ( ( 1o mVar 𝑅 ) ‘ ∅ ) ( +g ‘ ( mulGrp ‘ ( 1o mPoly 𝑅 ) ) ) ( ( 1o mVar 𝑅 ) ‘ ∅ ) ) = ( ( ( 1o mVar 𝑅 ) ‘ ∅ ) ( +g ‘ ( mulGrp ‘ ( 1o mPoly 𝑅 ) ) ) ( ( 1o mVar 𝑅 ) ‘ ∅ ) ) )
29		0ex	⊢ ∅ ∈ V
30		fveq2	⊢ ( 𝑏 = ∅ → ( ( 1o mVar 𝑅 ) ‘ 𝑏 ) = ( ( 1o mVar 𝑅 ) ‘ ∅ ) )
31	30	oveq1d	⊢ ( 𝑏 = ∅ → ( ( ( 1o mVar 𝑅 ) ‘ 𝑏 ) ( +g ‘ ( mulGrp ‘ ( 1o mPoly 𝑅 ) ) ) ( ( 1o mVar 𝑅 ) ‘ ∅ ) ) = ( ( ( 1o mVar 𝑅 ) ‘ ∅ ) ( +g ‘ ( mulGrp ‘ ( 1o mPoly 𝑅 ) ) ) ( ( 1o mVar 𝑅 ) ‘ ∅ ) ) )
32	30	oveq2d	⊢ ( 𝑏 = ∅ → ( ( ( 1o mVar 𝑅 ) ‘ ∅ ) ( +g ‘ ( mulGrp ‘ ( 1o mPoly 𝑅 ) ) ) ( ( 1o mVar 𝑅 ) ‘ 𝑏 ) ) = ( ( ( 1o mVar 𝑅 ) ‘ ∅ ) ( +g ‘ ( mulGrp ‘ ( 1o mPoly 𝑅 ) ) ) ( ( 1o mVar 𝑅 ) ‘ ∅ ) ) )
33	31 32	eqeq12d	⊢ ( 𝑏 = ∅ → ( ( ( ( 1o mVar 𝑅 ) ‘ 𝑏 ) ( +g ‘ ( mulGrp ‘ ( 1o mPoly 𝑅 ) ) ) ( ( 1o mVar 𝑅 ) ‘ ∅ ) ) = ( ( ( 1o mVar 𝑅 ) ‘ ∅ ) ( +g ‘ ( mulGrp ‘ ( 1o mPoly 𝑅 ) ) ) ( ( 1o mVar 𝑅 ) ‘ 𝑏 ) ) ↔ ( ( ( 1o mVar 𝑅 ) ‘ ∅ ) ( +g ‘ ( mulGrp ‘ ( 1o mPoly 𝑅 ) ) ) ( ( 1o mVar 𝑅 ) ‘ ∅ ) ) = ( ( ( 1o mVar 𝑅 ) ‘ ∅ ) ( +g ‘ ( mulGrp ‘ ( 1o mPoly 𝑅 ) ) ) ( ( 1o mVar 𝑅 ) ‘ ∅ ) ) ) )
34	29 33	ralsn	⊢ ( ∀ 𝑏 ∈ { ∅ } ( ( ( 1o mVar 𝑅 ) ‘ 𝑏 ) ( +g ‘ ( mulGrp ‘ ( 1o mPoly 𝑅 ) ) ) ( ( 1o mVar 𝑅 ) ‘ ∅ ) ) = ( ( ( 1o mVar 𝑅 ) ‘ ∅ ) ( +g ‘ ( mulGrp ‘ ( 1o mPoly 𝑅 ) ) ) ( ( 1o mVar 𝑅 ) ‘ 𝑏 ) ) ↔ ( ( ( 1o mVar 𝑅 ) ‘ ∅ ) ( +g ‘ ( mulGrp ‘ ( 1o mPoly 𝑅 ) ) ) ( ( 1o mVar 𝑅 ) ‘ ∅ ) ) = ( ( ( 1o mVar 𝑅 ) ‘ ∅ ) ( +g ‘ ( mulGrp ‘ ( 1o mPoly 𝑅 ) ) ) ( ( 1o mVar 𝑅 ) ‘ ∅ ) ) )
35	28 34	sylibr	⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ) ∧ 𝑎 ∈ ( ℕ0 ↑m 1o ) ) → ∀ 𝑏 ∈ { ∅ } ( ( ( 1o mVar 𝑅 ) ‘ 𝑏 ) ( +g ‘ ( mulGrp ‘ ( 1o mPoly 𝑅 ) ) ) ( ( 1o mVar 𝑅 ) ‘ ∅ ) ) = ( ( ( 1o mVar 𝑅 ) ‘ ∅ ) ( +g ‘ ( mulGrp ‘ ( 1o mPoly 𝑅 ) ) ) ( ( 1o mVar 𝑅 ) ‘ 𝑏 ) ) )
36		fveq2	⊢ ( 𝑥 = ∅ → ( ( 1o mVar 𝑅 ) ‘ 𝑥 ) = ( ( 1o mVar 𝑅 ) ‘ ∅ ) )
37	36	oveq2d	⊢ ( 𝑥 = ∅ → ( ( ( 1o mVar 𝑅 ) ‘ 𝑏 ) ( +g ‘ ( mulGrp ‘ ( 1o mPoly 𝑅 ) ) ) ( ( 1o mVar 𝑅 ) ‘ 𝑥 ) ) = ( ( ( 1o mVar 𝑅 ) ‘ 𝑏 ) ( +g ‘ ( mulGrp ‘ ( 1o mPoly 𝑅 ) ) ) ( ( 1o mVar 𝑅 ) ‘ ∅ ) ) )
38	36	oveq1d	⊢ ( 𝑥 = ∅ → ( ( ( 1o mVar 𝑅 ) ‘ 𝑥 ) ( +g ‘ ( mulGrp ‘ ( 1o mPoly 𝑅 ) ) ) ( ( 1o mVar 𝑅 ) ‘ 𝑏 ) ) = ( ( ( 1o mVar 𝑅 ) ‘ ∅ ) ( +g ‘ ( mulGrp ‘ ( 1o mPoly 𝑅 ) ) ) ( ( 1o mVar 𝑅 ) ‘ 𝑏 ) ) )
39	37 38	eqeq12d	⊢ ( 𝑥 = ∅ → ( ( ( ( 1o mVar 𝑅 ) ‘ 𝑏 ) ( +g ‘ ( mulGrp ‘ ( 1o mPoly 𝑅 ) ) ) ( ( 1o mVar 𝑅 ) ‘ 𝑥 ) ) = ( ( ( 1o mVar 𝑅 ) ‘ 𝑥 ) ( +g ‘ ( mulGrp ‘ ( 1o mPoly 𝑅 ) ) ) ( ( 1o mVar 𝑅 ) ‘ 𝑏 ) ) ↔ ( ( ( 1o mVar 𝑅 ) ‘ 𝑏 ) ( +g ‘ ( mulGrp ‘ ( 1o mPoly 𝑅 ) ) ) ( ( 1o mVar 𝑅 ) ‘ ∅ ) ) = ( ( ( 1o mVar 𝑅 ) ‘ ∅ ) ( +g ‘ ( mulGrp ‘ ( 1o mPoly 𝑅 ) ) ) ( ( 1o mVar 𝑅 ) ‘ 𝑏 ) ) ) )
40	39	ralbidv	⊢ ( 𝑥 = ∅ → ( ∀ 𝑏 ∈ { ∅ } ( ( ( 1o mVar 𝑅 ) ‘ 𝑏 ) ( +g ‘ ( mulGrp ‘ ( 1o mPoly 𝑅 ) ) ) ( ( 1o mVar 𝑅 ) ‘ 𝑥 ) ) = ( ( ( 1o mVar 𝑅 ) ‘ 𝑥 ) ( +g ‘ ( mulGrp ‘ ( 1o mPoly 𝑅 ) ) ) ( ( 1o mVar 𝑅 ) ‘ 𝑏 ) ) ↔ ∀ 𝑏 ∈ { ∅ } ( ( ( 1o mVar 𝑅 ) ‘ 𝑏 ) ( +g ‘ ( mulGrp ‘ ( 1o mPoly 𝑅 ) ) ) ( ( 1o mVar 𝑅 ) ‘ ∅ ) ) = ( ( ( 1o mVar 𝑅 ) ‘ ∅ ) ( +g ‘ ( mulGrp ‘ ( 1o mPoly 𝑅 ) ) ) ( ( 1o mVar 𝑅 ) ‘ 𝑏 ) ) ) )
41	29 40	ralsn	⊢ ( ∀ 𝑥 ∈ { ∅ } ∀ 𝑏 ∈ { ∅ } ( ( ( 1o mVar 𝑅 ) ‘ 𝑏 ) ( +g ‘ ( mulGrp ‘ ( 1o mPoly 𝑅 ) ) ) ( ( 1o mVar 𝑅 ) ‘ 𝑥 ) ) = ( ( ( 1o mVar 𝑅 ) ‘ 𝑥 ) ( +g ‘ ( mulGrp ‘ ( 1o mPoly 𝑅 ) ) ) ( ( 1o mVar 𝑅 ) ‘ 𝑏 ) ) ↔ ∀ 𝑏 ∈ { ∅ } ( ( ( 1o mVar 𝑅 ) ‘ 𝑏 ) ( +g ‘ ( mulGrp ‘ ( 1o mPoly 𝑅 ) ) ) ( ( 1o mVar 𝑅 ) ‘ ∅ ) ) = ( ( ( 1o mVar 𝑅 ) ‘ ∅ ) ( +g ‘ ( mulGrp ‘ ( 1o mPoly 𝑅 ) ) ) ( ( 1o mVar 𝑅 ) ‘ 𝑏 ) ) )
42	35 41	sylibr	⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ) ∧ 𝑎 ∈ ( ℕ0 ↑m 1o ) ) → ∀ 𝑥 ∈ { ∅ } ∀ 𝑏 ∈ { ∅ } ( ( ( 1o mVar 𝑅 ) ‘ 𝑏 ) ( +g ‘ ( mulGrp ‘ ( 1o mPoly 𝑅 ) ) ) ( ( 1o mVar 𝑅 ) ‘ 𝑥 ) ) = ( ( ( 1o mVar 𝑅 ) ‘ 𝑥 ) ( +g ‘ ( mulGrp ‘ ( 1o mPoly 𝑅 ) ) ) ( ( 1o mVar 𝑅 ) ‘ 𝑏 ) ) )
43		df1o2	⊢ 1o = { ∅ }
44	43	raleqi	⊢ ( ∀ 𝑏 ∈ 1o ( ( ( 1o mVar 𝑅 ) ‘ 𝑏 ) ( +g ‘ ( mulGrp ‘ ( 1o mPoly 𝑅 ) ) ) ( ( 1o mVar 𝑅 ) ‘ 𝑥 ) ) = ( ( ( 1o mVar 𝑅 ) ‘ 𝑥 ) ( +g ‘ ( mulGrp ‘ ( 1o mPoly 𝑅 ) ) ) ( ( 1o mVar 𝑅 ) ‘ 𝑏 ) ) ↔ ∀ 𝑏 ∈ { ∅ } ( ( ( 1o mVar 𝑅 ) ‘ 𝑏 ) ( +g ‘ ( mulGrp ‘ ( 1o mPoly 𝑅 ) ) ) ( ( 1o mVar 𝑅 ) ‘ 𝑥 ) ) = ( ( ( 1o mVar 𝑅 ) ‘ 𝑥 ) ( +g ‘ ( mulGrp ‘ ( 1o mPoly 𝑅 ) ) ) ( ( 1o mVar 𝑅 ) ‘ 𝑏 ) ) )
45	43 44	raleqbii	⊢ ( ∀ 𝑥 ∈ 1o ∀ 𝑏 ∈ 1o ( ( ( 1o mVar 𝑅 ) ‘ 𝑏 ) ( +g ‘ ( mulGrp ‘ ( 1o mPoly 𝑅 ) ) ) ( ( 1o mVar 𝑅 ) ‘ 𝑥 ) ) = ( ( ( 1o mVar 𝑅 ) ‘ 𝑥 ) ( +g ‘ ( mulGrp ‘ ( 1o mPoly 𝑅 ) ) ) ( ( 1o mVar 𝑅 ) ‘ 𝑏 ) ) ↔ ∀ 𝑥 ∈ { ∅ } ∀ 𝑏 ∈ { ∅ } ( ( ( 1o mVar 𝑅 ) ‘ 𝑏 ) ( +g ‘ ( mulGrp ‘ ( 1o mPoly 𝑅 ) ) ) ( ( 1o mVar 𝑅 ) ‘ 𝑥 ) ) = ( ( ( 1o mVar 𝑅 ) ‘ 𝑥 ) ( +g ‘ ( mulGrp ‘ ( 1o mPoly 𝑅 ) ) ) ( ( 1o mVar 𝑅 ) ‘ 𝑏 ) ) )
46	42 45	sylibr	⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ) ∧ 𝑎 ∈ ( ℕ0 ↑m 1o ) ) → ∀ 𝑥 ∈ 1o ∀ 𝑏 ∈ 1o ( ( ( 1o mVar 𝑅 ) ‘ 𝑏 ) ( +g ‘ ( mulGrp ‘ ( 1o mPoly 𝑅 ) ) ) ( ( 1o mVar 𝑅 ) ‘ 𝑥 ) ) = ( ( ( 1o mVar 𝑅 ) ‘ 𝑥 ) ( +g ‘ ( mulGrp ‘ ( 1o mPoly 𝑅 ) ) ) ( ( 1o mVar 𝑅 ) ‘ 𝑏 ) ) )
47	8 9 10 11 22 23 24 25 26 27 46	mplcoe5	⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ) ∧ 𝑎 ∈ ( ℕ0 ↑m 1o ) ) → ( 𝑏 ∈ ( ℕ0 ↑m 1o ) ↦ if ( 𝑏 = 𝑎 , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) ) = ( ( mulGrp ‘ ( 1o mPoly 𝑅 ) ) Σg ( 𝑐 ∈ 1o ↦ ( ( 𝑎 ‘ 𝑐 ) ( .g ‘ ( mulGrp ‘ ( 1o mPoly 𝑅 ) ) ) ( ( 1o mVar 𝑅 ) ‘ 𝑐 ) ) ) ) )
48	43	mpteq1i	⊢ ( 𝑐 ∈ 1o ↦ ( ( 𝑎 ‘ 𝑐 ) ( .g ‘ ( mulGrp ‘ ( 1o mPoly 𝑅 ) ) ) ( ( 1o mVar 𝑅 ) ‘ 𝑐 ) ) ) = ( 𝑐 ∈ { ∅ } ↦ ( ( 𝑎 ‘ 𝑐 ) ( .g ‘ ( mulGrp ‘ ( 1o mPoly 𝑅 ) ) ) ( ( 1o mVar 𝑅 ) ‘ 𝑐 ) ) )
49	48	oveq2i	⊢ ( ( mulGrp ‘ ( 1o mPoly 𝑅 ) ) Σg ( 𝑐 ∈ 1o ↦ ( ( 𝑎 ‘ 𝑐 ) ( .g ‘ ( mulGrp ‘ ( 1o mPoly 𝑅 ) ) ) ( ( 1o mVar 𝑅 ) ‘ 𝑐 ) ) ) ) = ( ( mulGrp ‘ ( 1o mPoly 𝑅 ) ) Σg ( 𝑐 ∈ { ∅ } ↦ ( ( 𝑎 ‘ 𝑐 ) ( .g ‘ ( mulGrp ‘ ( 1o mPoly 𝑅 ) ) ) ( ( 1o mVar 𝑅 ) ‘ 𝑐 ) ) ) )
50	8	mplring	⊢ ( ( 1o ∈ ω ∧ 𝑅 ∈ Ring ) → ( 1o mPoly 𝑅 ) ∈ Ring )
51	12 50	mpan	⊢ ( 𝑅 ∈ Ring → ( 1o mPoly 𝑅 ) ∈ Ring )
52	23	ringmgp	⊢ ( ( 1o mPoly 𝑅 ) ∈ Ring → ( mulGrp ‘ ( 1o mPoly 𝑅 ) ) ∈ Mnd )
53	51 52	syl	⊢ ( 𝑅 ∈ Ring → ( mulGrp ‘ ( 1o mPoly 𝑅 ) ) ∈ Mnd )
54	53	ad2antrr	⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ) ∧ 𝑎 ∈ ( ℕ0 ↑m 1o ) ) → ( mulGrp ‘ ( 1o mPoly 𝑅 ) ) ∈ Mnd )
55	29	a1i	⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ) ∧ 𝑎 ∈ ( ℕ0 ↑m 1o ) ) → ∅ ∈ V )
56	23 15	mgpbas	⊢ 𝐵 = ( Base ‘ ( mulGrp ‘ ( 1o mPoly 𝑅 ) ) )
57	56	a1i	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ) → 𝐵 = ( Base ‘ ( mulGrp ‘ ( 1o mPoly 𝑅 ) ) ) )
58	5 3	mgpbas	⊢ 𝐵 = ( Base ‘ 𝑀 )
59	58	a1i	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ) → 𝐵 = ( Base ‘ 𝑀 ) )
60		ssv	⊢ 𝐵 ⊆ V
61	60	a1i	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ) → 𝐵 ⊆ V )
62		ovexd	⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ) ∧ ( 𝑎 ∈ V ∧ 𝑏 ∈ V ) ) → ( 𝑎 ( +g ‘ ( mulGrp ‘ ( 1o mPoly 𝑅 ) ) ) 𝑏 ) ∈ V )
63		eqid	⊢ ( .r ‘ 𝑃 ) = ( .r ‘ 𝑃 )
64	1 8 63	ply1mulr	⊢ ( .r ‘ 𝑃 ) = ( .r ‘ ( 1o mPoly 𝑅 ) )
65	23 64	mgpplusg	⊢ ( .r ‘ 𝑃 ) = ( +g ‘ ( mulGrp ‘ ( 1o mPoly 𝑅 ) ) )
66	5 63	mgpplusg	⊢ ( .r ‘ 𝑃 ) = ( +g ‘ 𝑀 )
67	65 66	eqtr3i	⊢ ( +g ‘ ( mulGrp ‘ ( 1o mPoly 𝑅 ) ) ) = ( +g ‘ 𝑀 )
68	67	oveqi	⊢ ( 𝑎 ( +g ‘ ( mulGrp ‘ ( 1o mPoly 𝑅 ) ) ) 𝑏 ) = ( 𝑎 ( +g ‘ 𝑀 ) 𝑏 )
69	68	a1i	⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ) ∧ ( 𝑎 ∈ V ∧ 𝑏 ∈ V ) ) → ( 𝑎 ( +g ‘ ( mulGrp ‘ ( 1o mPoly 𝑅 ) ) ) 𝑏 ) = ( 𝑎 ( +g ‘ 𝑀 ) 𝑏 ) )
70	24 6 57 59 61 62 69	mulgpropd	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ) → ( .g ‘ ( mulGrp ‘ ( 1o mPoly 𝑅 ) ) ) = ↑ )
71	70	oveqd	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ) → ( ( 𝑎 ‘ ∅ ) ( .g ‘ ( mulGrp ‘ ( 1o mPoly 𝑅 ) ) ) 𝑋 ) = ( ( 𝑎 ‘ ∅ ) ↑ 𝑋 ) )
72	71	adantr	⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ) ∧ 𝑎 ∈ ( ℕ0 ↑m 1o ) ) → ( ( 𝑎 ‘ ∅ ) ( .g ‘ ( mulGrp ‘ ( 1o mPoly 𝑅 ) ) ) 𝑋 ) = ( ( 𝑎 ‘ ∅ ) ↑ 𝑋 ) )
73	1	ply1ring	⊢ ( 𝑅 ∈ Ring → 𝑃 ∈ Ring )
74	5	ringmgp	⊢ ( 𝑃 ∈ Ring → 𝑀 ∈ Mnd )
75	73 74	syl	⊢ ( 𝑅 ∈ Ring → 𝑀 ∈ Mnd )
76	75	ad2antrr	⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ) ∧ 𝑎 ∈ ( ℕ0 ↑m 1o ) ) → 𝑀 ∈ Mnd )
77		elmapi	⊢ ( 𝑎 ∈ ( ℕ0 ↑m 1o ) → 𝑎 : 1o ⟶ ℕ0 )
78		0lt1o	⊢ ∅ ∈ 1o
79		ffvelcdm	⊢ ( ( 𝑎 : 1o ⟶ ℕ0 ∧ ∅ ∈ 1o ) → ( 𝑎 ‘ ∅ ) ∈ ℕ0 )
80	77 78 79	sylancl	⊢ ( 𝑎 ∈ ( ℕ0 ↑m 1o ) → ( 𝑎 ‘ ∅ ) ∈ ℕ0 )
81	80	adantl	⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ) ∧ 𝑎 ∈ ( ℕ0 ↑m 1o ) ) → ( 𝑎 ‘ ∅ ) ∈ ℕ0 )
82	2 1 3	vr1cl	⊢ ( 𝑅 ∈ Ring → 𝑋 ∈ 𝐵 )
83	82	ad2antrr	⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ) ∧ 𝑎 ∈ ( ℕ0 ↑m 1o ) ) → 𝑋 ∈ 𝐵 )
84	58 6 76 81 83	mulgnn0cld	⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ) ∧ 𝑎 ∈ ( ℕ0 ↑m 1o ) ) → ( ( 𝑎 ‘ ∅ ) ↑ 𝑋 ) ∈ 𝐵 )
85	72 84	eqeltrd	⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ) ∧ 𝑎 ∈ ( ℕ0 ↑m 1o ) ) → ( ( 𝑎 ‘ ∅ ) ( .g ‘ ( mulGrp ‘ ( 1o mPoly 𝑅 ) ) ) 𝑋 ) ∈ 𝐵 )
86		fveq2	⊢ ( 𝑐 = ∅ → ( 𝑎 ‘ 𝑐 ) = ( 𝑎 ‘ ∅ ) )
87		fveq2	⊢ ( 𝑐 = ∅ → ( ( 1o mVar 𝑅 ) ‘ 𝑐 ) = ( ( 1o mVar 𝑅 ) ‘ ∅ ) )
88	2	vr1val	⊢ 𝑋 = ( ( 1o mVar 𝑅 ) ‘ ∅ )
89	87 88	eqtr4di	⊢ ( 𝑐 = ∅ → ( ( 1o mVar 𝑅 ) ‘ 𝑐 ) = 𝑋 )
90	86 89	oveq12d	⊢ ( 𝑐 = ∅ → ( ( 𝑎 ‘ 𝑐 ) ( .g ‘ ( mulGrp ‘ ( 1o mPoly 𝑅 ) ) ) ( ( 1o mVar 𝑅 ) ‘ 𝑐 ) ) = ( ( 𝑎 ‘ ∅ ) ( .g ‘ ( mulGrp ‘ ( 1o mPoly 𝑅 ) ) ) 𝑋 ) )
91	56 90	gsumsn	⊢ ( ( ( mulGrp ‘ ( 1o mPoly 𝑅 ) ) ∈ Mnd ∧ ∅ ∈ V ∧ ( ( 𝑎 ‘ ∅ ) ( .g ‘ ( mulGrp ‘ ( 1o mPoly 𝑅 ) ) ) 𝑋 ) ∈ 𝐵 ) → ( ( mulGrp ‘ ( 1o mPoly 𝑅 ) ) Σg ( 𝑐 ∈ { ∅ } ↦ ( ( 𝑎 ‘ 𝑐 ) ( .g ‘ ( mulGrp ‘ ( 1o mPoly 𝑅 ) ) ) ( ( 1o mVar 𝑅 ) ‘ 𝑐 ) ) ) ) = ( ( 𝑎 ‘ ∅ ) ( .g ‘ ( mulGrp ‘ ( 1o mPoly 𝑅 ) ) ) 𝑋 ) )
92	54 55 85 91	syl3anc	⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ) ∧ 𝑎 ∈ ( ℕ0 ↑m 1o ) ) → ( ( mulGrp ‘ ( 1o mPoly 𝑅 ) ) Σg ( 𝑐 ∈ { ∅ } ↦ ( ( 𝑎 ‘ 𝑐 ) ( .g ‘ ( mulGrp ‘ ( 1o mPoly 𝑅 ) ) ) ( ( 1o mVar 𝑅 ) ‘ 𝑐 ) ) ) ) = ( ( 𝑎 ‘ ∅ ) ( .g ‘ ( mulGrp ‘ ( 1o mPoly 𝑅 ) ) ) 𝑋 ) )
93	49 92	eqtrid	⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ) ∧ 𝑎 ∈ ( ℕ0 ↑m 1o ) ) → ( ( mulGrp ‘ ( 1o mPoly 𝑅 ) ) Σg ( 𝑐 ∈ 1o ↦ ( ( 𝑎 ‘ 𝑐 ) ( .g ‘ ( mulGrp ‘ ( 1o mPoly 𝑅 ) ) ) ( ( 1o mVar 𝑅 ) ‘ 𝑐 ) ) ) ) = ( ( 𝑎 ‘ ∅ ) ( .g ‘ ( mulGrp ‘ ( 1o mPoly 𝑅 ) ) ) 𝑋 ) )
94	47 93 72	3eqtrd	⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ) ∧ 𝑎 ∈ ( ℕ0 ↑m 1o ) ) → ( 𝑏 ∈ ( ℕ0 ↑m 1o ) ↦ if ( 𝑏 = 𝑎 , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) ) = ( ( 𝑎 ‘ ∅ ) ↑ 𝑋 ) )
95	21 94	oveq12d	⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ) ∧ 𝑎 ∈ ( ℕ0 ↑m 1o ) ) → ( ( 𝐾 ‘ 𝑎 ) · ( 𝑏 ∈ ( ℕ0 ↑m 1o ) ↦ if ( 𝑏 = 𝑎 , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) ) ) = ( ( 𝐴 ‘ ( 𝑎 ‘ ∅ ) ) · ( ( 𝑎 ‘ ∅ ) ↑ 𝑋 ) ) )
96	95	mpteq2dva	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ) → ( 𝑎 ∈ ( ℕ0 ↑m 1o ) ↦ ( ( 𝐾 ‘ 𝑎 ) · ( 𝑏 ∈ ( ℕ0 ↑m 1o ) ↦ if ( 𝑏 = 𝑎 , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) ) ) ) = ( 𝑎 ∈ ( ℕ0 ↑m 1o ) ↦ ( ( 𝐴 ‘ ( 𝑎 ‘ ∅ ) ) · ( ( 𝑎 ‘ ∅ ) ↑ 𝑋 ) ) ) )
97	96	oveq2d	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ) → ( ( 1o mPoly 𝑅 ) Σg ( 𝑎 ∈ ( ℕ0 ↑m 1o ) ↦ ( ( 𝐾 ‘ 𝑎 ) · ( 𝑏 ∈ ( ℕ0 ↑m 1o ) ↦ if ( 𝑏 = 𝑎 , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) ) ) ) ) = ( ( 1o mPoly 𝑅 ) Σg ( 𝑎 ∈ ( ℕ0 ↑m 1o ) ↦ ( ( 𝐴 ‘ ( 𝑎 ‘ ∅ ) ) · ( ( 𝑎 ‘ ∅ ) ↑ 𝑋 ) ) ) ) )
98		nn0ex	⊢ ℕ0 ∈ V
99	98	mptex	⊢ ( 𝑘 ∈ ℕ0 ↦ ( ( 𝐴 ‘ 𝑘 ) · ( 𝑘 ↑ 𝑋 ) ) ) ∈ V
100	99	a1i	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ) → ( 𝑘 ∈ ℕ0 ↦ ( ( 𝐴 ‘ 𝑘 ) · ( 𝑘 ↑ 𝑋 ) ) ) ∈ V )
101	1	fvexi	⊢ 𝑃 ∈ V
102	101	a1i	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ) → 𝑃 ∈ V )
103		ovexd	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ) → ( 1o mPoly 𝑅 ) ∈ V )
104	3 15	eqtr3i	⊢ ( Base ‘ 𝑃 ) = ( Base ‘ ( 1o mPoly 𝑅 ) )
105	104	a1i	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ) → ( Base ‘ 𝑃 ) = ( Base ‘ ( 1o mPoly 𝑅 ) ) )
106		eqid	⊢ ( +g ‘ 𝑃 ) = ( +g ‘ 𝑃 )
107	1 8 106	ply1plusg	⊢ ( +g ‘ 𝑃 ) = ( +g ‘ ( 1o mPoly 𝑅 ) )
108	107	a1i	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ) → ( +g ‘ 𝑃 ) = ( +g ‘ ( 1o mPoly 𝑅 ) ) )
109	100 102 103 105 108	gsumpropd	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ) → ( 𝑃 Σg ( 𝑘 ∈ ℕ0 ↦ ( ( 𝐴 ‘ 𝑘 ) · ( 𝑘 ↑ 𝑋 ) ) ) ) = ( ( 1o mPoly 𝑅 ) Σg ( 𝑘 ∈ ℕ0 ↦ ( ( 𝐴 ‘ 𝑘 ) · ( 𝑘 ↑ 𝑋 ) ) ) ) )
110		eqid	⊢ ( 0g ‘ 𝑃 ) = ( 0g ‘ 𝑃 )
111	8 1 110	ply1mpl0	⊢ ( 0g ‘ 𝑃 ) = ( 0g ‘ ( 1o mPoly 𝑅 ) )
112	8	mpllmod	⊢ ( ( 1o ∈ ω ∧ 𝑅 ∈ Ring ) → ( 1o mPoly 𝑅 ) ∈ LMod )
113	12 17 112	sylancr	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ) → ( 1o mPoly 𝑅 ) ∈ LMod )
114		lmodcmn	⊢ ( ( 1o mPoly 𝑅 ) ∈ LMod → ( 1o mPoly 𝑅 ) ∈ CMnd )
115	113 114	syl	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ) → ( 1o mPoly 𝑅 ) ∈ CMnd )
116	98	a1i	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ) → ℕ0 ∈ V )
117	1	ply1lmod	⊢ ( 𝑅 ∈ Ring → 𝑃 ∈ LMod )
118	117	ad2antrr	⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ) ∧ 𝑘 ∈ ℕ0 ) → 𝑃 ∈ LMod )
119		eqid	⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
120	7 3 1 119	coe1f	⊢ ( 𝐾 ∈ 𝐵 → 𝐴 : ℕ0 ⟶ ( Base ‘ 𝑅 ) )
121	120	adantl	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ) → 𝐴 : ℕ0 ⟶ ( Base ‘ 𝑅 ) )
122	121	ffvelcdmda	⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ) ∧ 𝑘 ∈ ℕ0 ) → ( 𝐴 ‘ 𝑘 ) ∈ ( Base ‘ 𝑅 ) )
123	1	ply1sca	⊢ ( 𝑅 ∈ Ring → 𝑅 = ( Scalar ‘ 𝑃 ) )
124	123	eqcomd	⊢ ( 𝑅 ∈ Ring → ( Scalar ‘ 𝑃 ) = 𝑅 )
125	124	ad2antrr	⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ) ∧ 𝑘 ∈ ℕ0 ) → ( Scalar ‘ 𝑃 ) = 𝑅 )
126	125	fveq2d	⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ) ∧ 𝑘 ∈ ℕ0 ) → ( Base ‘ ( Scalar ‘ 𝑃 ) ) = ( Base ‘ 𝑅 ) )
127	122 126	eleqtrrd	⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ) ∧ 𝑘 ∈ ℕ0 ) → ( 𝐴 ‘ 𝑘 ) ∈ ( Base ‘ ( Scalar ‘ 𝑃 ) ) )
128	75	ad2antrr	⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ) ∧ 𝑘 ∈ ℕ0 ) → 𝑀 ∈ Mnd )
129		simpr	⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ) ∧ 𝑘 ∈ ℕ0 ) → 𝑘 ∈ ℕ0 )
130	82	ad2antrr	⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ) ∧ 𝑘 ∈ ℕ0 ) → 𝑋 ∈ 𝐵 )
131	58 6 128 129 130	mulgnn0cld	⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ) ∧ 𝑘 ∈ ℕ0 ) → ( 𝑘 ↑ 𝑋 ) ∈ 𝐵 )
132		eqid	⊢ ( Scalar ‘ 𝑃 ) = ( Scalar ‘ 𝑃 )
133		eqid	⊢ ( Base ‘ ( Scalar ‘ 𝑃 ) ) = ( Base ‘ ( Scalar ‘ 𝑃 ) )
134	3 132 4 133	lmodvscl	⊢ ( ( 𝑃 ∈ LMod ∧ ( 𝐴 ‘ 𝑘 ) ∈ ( Base ‘ ( Scalar ‘ 𝑃 ) ) ∧ ( 𝑘 ↑ 𝑋 ) ∈ 𝐵 ) → ( ( 𝐴 ‘ 𝑘 ) · ( 𝑘 ↑ 𝑋 ) ) ∈ 𝐵 )
135	118 127 131 134	syl3anc	⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ) ∧ 𝑘 ∈ ℕ0 ) → ( ( 𝐴 ‘ 𝑘 ) · ( 𝑘 ↑ 𝑋 ) ) ∈ 𝐵 )
136	135	fmpttd	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ) → ( 𝑘 ∈ ℕ0 ↦ ( ( 𝐴 ‘ 𝑘 ) · ( 𝑘 ↑ 𝑋 ) ) ) : ℕ0 ⟶ 𝐵 )
137	1 2 3 4 5 6 7	ply1coefsupp	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ) → ( 𝑘 ∈ ℕ0 ↦ ( ( 𝐴 ‘ 𝑘 ) · ( 𝑘 ↑ 𝑋 ) ) ) finSupp ( 0g ‘ 𝑃 ) )
138		eqid	⊢ ( 𝑎 ∈ ( ℕ0 ↑m 1o ) ↦ ( 𝑎 ‘ ∅ ) ) = ( 𝑎 ∈ ( ℕ0 ↑m 1o ) ↦ ( 𝑎 ‘ ∅ ) )
139	43 98 29 138	mapsnf1o2	⊢ ( 𝑎 ∈ ( ℕ0 ↑m 1o ) ↦ ( 𝑎 ‘ ∅ ) ) : ( ℕ0 ↑m 1o ) –1-1-onto→ ℕ0
140	139	a1i	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ) → ( 𝑎 ∈ ( ℕ0 ↑m 1o ) ↦ ( 𝑎 ‘ ∅ ) ) : ( ℕ0 ↑m 1o ) –1-1-onto→ ℕ0 )
141	15 111 115 116 136 137 140	gsumf1o	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ) → ( ( 1o mPoly 𝑅 ) Σg ( 𝑘 ∈ ℕ0 ↦ ( ( 𝐴 ‘ 𝑘 ) · ( 𝑘 ↑ 𝑋 ) ) ) ) = ( ( 1o mPoly 𝑅 ) Σg ( ( 𝑘 ∈ ℕ0 ↦ ( ( 𝐴 ‘ 𝑘 ) · ( 𝑘 ↑ 𝑋 ) ) ) ∘ ( 𝑎 ∈ ( ℕ0 ↑m 1o ) ↦ ( 𝑎 ‘ ∅ ) ) ) ) )
142		eqidd	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ) → ( 𝑎 ∈ ( ℕ0 ↑m 1o ) ↦ ( 𝑎 ‘ ∅ ) ) = ( 𝑎 ∈ ( ℕ0 ↑m 1o ) ↦ ( 𝑎 ‘ ∅ ) ) )
143		eqidd	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ) → ( 𝑘 ∈ ℕ0 ↦ ( ( 𝐴 ‘ 𝑘 ) · ( 𝑘 ↑ 𝑋 ) ) ) = ( 𝑘 ∈ ℕ0 ↦ ( ( 𝐴 ‘ 𝑘 ) · ( 𝑘 ↑ 𝑋 ) ) ) )
144		fveq2	⊢ ( 𝑘 = ( 𝑎 ‘ ∅ ) → ( 𝐴 ‘ 𝑘 ) = ( 𝐴 ‘ ( 𝑎 ‘ ∅ ) ) )
145		oveq1	⊢ ( 𝑘 = ( 𝑎 ‘ ∅ ) → ( 𝑘 ↑ 𝑋 ) = ( ( 𝑎 ‘ ∅ ) ↑ 𝑋 ) )
146	144 145	oveq12d	⊢ ( 𝑘 = ( 𝑎 ‘ ∅ ) → ( ( 𝐴 ‘ 𝑘 ) · ( 𝑘 ↑ 𝑋 ) ) = ( ( 𝐴 ‘ ( 𝑎 ‘ ∅ ) ) · ( ( 𝑎 ‘ ∅ ) ↑ 𝑋 ) ) )
147	81 142 143 146	fmptco	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ) → ( ( 𝑘 ∈ ℕ0 ↦ ( ( 𝐴 ‘ 𝑘 ) · ( 𝑘 ↑ 𝑋 ) ) ) ∘ ( 𝑎 ∈ ( ℕ0 ↑m 1o ) ↦ ( 𝑎 ‘ ∅ ) ) ) = ( 𝑎 ∈ ( ℕ0 ↑m 1o ) ↦ ( ( 𝐴 ‘ ( 𝑎 ‘ ∅ ) ) · ( ( 𝑎 ‘ ∅ ) ↑ 𝑋 ) ) ) )
148	147	oveq2d	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ) → ( ( 1o mPoly 𝑅 ) Σg ( ( 𝑘 ∈ ℕ0 ↦ ( ( 𝐴 ‘ 𝑘 ) · ( 𝑘 ↑ 𝑋 ) ) ) ∘ ( 𝑎 ∈ ( ℕ0 ↑m 1o ) ↦ ( 𝑎 ‘ ∅ ) ) ) ) = ( ( 1o mPoly 𝑅 ) Σg ( 𝑎 ∈ ( ℕ0 ↑m 1o ) ↦ ( ( 𝐴 ‘ ( 𝑎 ‘ ∅ ) ) · ( ( 𝑎 ‘ ∅ ) ↑ 𝑋 ) ) ) ) )
149	109 141 148	3eqtrrd	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ) → ( ( 1o mPoly 𝑅 ) Σg ( 𝑎 ∈ ( ℕ0 ↑m 1o ) ↦ ( ( 𝐴 ‘ ( 𝑎 ‘ ∅ ) ) · ( ( 𝑎 ‘ ∅ ) ↑ 𝑋 ) ) ) ) = ( 𝑃 Σg ( 𝑘 ∈ ℕ0 ↦ ( ( 𝐴 ‘ 𝑘 ) · ( 𝑘 ↑ 𝑋 ) ) ) ) )
150	19 97 149	3eqtrd	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ) → 𝐾 = ( 𝑃 Σg ( 𝑘 ∈ ℕ0 ↦ ( ( 𝐴 ‘ 𝑘 ) · ( 𝑘 ↑ 𝑋 ) ) ) ) )