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		ffvelrn	⊢ ( ( 𝑎 : 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	mulgnn0cl	⊢ ( ( 𝑀 ∈ Mnd ∧ ( 𝑎 ‘ ∅ ) ∈ ℕ0 ∧ 𝑋 ∈ 𝐵 ) → ( ( 𝑎 ‘ ∅ ) ↑ 𝑋 ) ∈ 𝐵 )
85	76 81 83 84	syl3anc	⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ) ∧ 𝑎 ∈ ( ℕ0 ↑m 1o ) ) → ( ( 𝑎 ‘ ∅ ) ↑ 𝑋 ) ∈ 𝐵 )
86	72 85	eqeltrd	⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ) ∧ 𝑎 ∈ ( ℕ0 ↑m 1o ) ) → ( ( 𝑎 ‘ ∅ ) ( .g ‘ ( mulGrp ‘ ( 1o mPoly 𝑅 ) ) ) 𝑋 ) ∈ 𝐵 )
87		fveq2	⊢ ( 𝑐 = ∅ → ( 𝑎 ‘ 𝑐 ) = ( 𝑎 ‘ ∅ ) )
88		fveq2	⊢ ( 𝑐 = ∅ → ( ( 1o mVar 𝑅 ) ‘ 𝑐 ) = ( ( 1o mVar 𝑅 ) ‘ ∅ ) )
89	2	vr1val	⊢ 𝑋 = ( ( 1o mVar 𝑅 ) ‘ ∅ )
90	88 89	eqtr4di	⊢ ( 𝑐 = ∅ → ( ( 1o mVar 𝑅 ) ‘ 𝑐 ) = 𝑋 )
91	87 90	oveq12d	⊢ ( 𝑐 = ∅ → ( ( 𝑎 ‘ 𝑐 ) ( .g ‘ ( mulGrp ‘ ( 1o mPoly 𝑅 ) ) ) ( ( 1o mVar 𝑅 ) ‘ 𝑐 ) ) = ( ( 𝑎 ‘ ∅ ) ( .g ‘ ( mulGrp ‘ ( 1o mPoly 𝑅 ) ) ) 𝑋 ) )
92	56 91	gsumsn	⊢ ( ( ( mulGrp ‘ ( 1o mPoly 𝑅 ) ) ∈ Mnd ∧ ∅ ∈ V ∧ ( ( 𝑎 ‘ ∅ ) ( .g ‘ ( mulGrp ‘ ( 1o mPoly 𝑅 ) ) ) 𝑋 ) ∈ 𝐵 ) → ( ( mulGrp ‘ ( 1o mPoly 𝑅 ) ) Σg ( 𝑐 ∈ { ∅ } ↦ ( ( 𝑎 ‘ 𝑐 ) ( .g ‘ ( mulGrp ‘ ( 1o mPoly 𝑅 ) ) ) ( ( 1o mVar 𝑅 ) ‘ 𝑐 ) ) ) ) = ( ( 𝑎 ‘ ∅ ) ( .g ‘ ( mulGrp ‘ ( 1o mPoly 𝑅 ) ) ) 𝑋 ) )
93	54 55 86 92	syl3anc	⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ) ∧ 𝑎 ∈ ( ℕ0 ↑m 1o ) ) → ( ( mulGrp ‘ ( 1o mPoly 𝑅 ) ) Σg ( 𝑐 ∈ { ∅ } ↦ ( ( 𝑎 ‘ 𝑐 ) ( .g ‘ ( mulGrp ‘ ( 1o mPoly 𝑅 ) ) ) ( ( 1o mVar 𝑅 ) ‘ 𝑐 ) ) ) ) = ( ( 𝑎 ‘ ∅ ) ( .g ‘ ( mulGrp ‘ ( 1o mPoly 𝑅 ) ) ) 𝑋 ) )
94	49 93	syl5eq	⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ) ∧ 𝑎 ∈ ( ℕ0 ↑m 1o ) ) → ( ( mulGrp ‘ ( 1o mPoly 𝑅 ) ) Σg ( 𝑐 ∈ 1o ↦ ( ( 𝑎 ‘ 𝑐 ) ( .g ‘ ( mulGrp ‘ ( 1o mPoly 𝑅 ) ) ) ( ( 1o mVar 𝑅 ) ‘ 𝑐 ) ) ) ) = ( ( 𝑎 ‘ ∅ ) ( .g ‘ ( mulGrp ‘ ( 1o mPoly 𝑅 ) ) ) 𝑋 ) )
95	47 94 72	3eqtrd	⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ) ∧ 𝑎 ∈ ( ℕ0 ↑m 1o ) ) → ( 𝑏 ∈ ( ℕ0 ↑m 1o ) ↦ if ( 𝑏 = 𝑎 , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) ) = ( ( 𝑎 ‘ ∅ ) ↑ 𝑋 ) )
96	21 95	oveq12d	⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ) ∧ 𝑎 ∈ ( ℕ0 ↑m 1o ) ) → ( ( 𝐾 ‘ 𝑎 ) · ( 𝑏 ∈ ( ℕ0 ↑m 1o ) ↦ if ( 𝑏 = 𝑎 , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) ) ) = ( ( 𝐴 ‘ ( 𝑎 ‘ ∅ ) ) · ( ( 𝑎 ‘ ∅ ) ↑ 𝑋 ) ) )
97	96	mpteq2dva	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ) → ( 𝑎 ∈ ( ℕ0 ↑m 1o ) ↦ ( ( 𝐾 ‘ 𝑎 ) · ( 𝑏 ∈ ( ℕ0 ↑m 1o ) ↦ if ( 𝑏 = 𝑎 , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) ) ) ) = ( 𝑎 ∈ ( ℕ0 ↑m 1o ) ↦ ( ( 𝐴 ‘ ( 𝑎 ‘ ∅ ) ) · ( ( 𝑎 ‘ ∅ ) ↑ 𝑋 ) ) ) )
98	97	oveq2d	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ) → ( ( 1o mPoly 𝑅 ) Σg ( 𝑎 ∈ ( ℕ0 ↑m 1o ) ↦ ( ( 𝐾 ‘ 𝑎 ) · ( 𝑏 ∈ ( ℕ0 ↑m 1o ) ↦ if ( 𝑏 = 𝑎 , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) ) ) ) ) = ( ( 1o mPoly 𝑅 ) Σg ( 𝑎 ∈ ( ℕ0 ↑m 1o ) ↦ ( ( 𝐴 ‘ ( 𝑎 ‘ ∅ ) ) · ( ( 𝑎 ‘ ∅ ) ↑ 𝑋 ) ) ) ) )
99		nn0ex	⊢ ℕ0 ∈ V
100	99	mptex	⊢ ( 𝑘 ∈ ℕ0 ↦ ( ( 𝐴 ‘ 𝑘 ) · ( 𝑘 ↑ 𝑋 ) ) ) ∈ V
101	100	a1i	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ) → ( 𝑘 ∈ ℕ0 ↦ ( ( 𝐴 ‘ 𝑘 ) · ( 𝑘 ↑ 𝑋 ) ) ) ∈ V )
102	1	fvexi	⊢ 𝑃 ∈ V
103	102	a1i	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ) → 𝑃 ∈ V )
104		ovexd	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ) → ( 1o mPoly 𝑅 ) ∈ V )
105	3 15	eqtr3i	⊢ ( Base ‘ 𝑃 ) = ( Base ‘ ( 1o mPoly 𝑅 ) )
106	105	a1i	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ) → ( Base ‘ 𝑃 ) = ( Base ‘ ( 1o mPoly 𝑅 ) ) )
107		eqid	⊢ ( +g ‘ 𝑃 ) = ( +g ‘ 𝑃 )
108	1 8 107	ply1plusg	⊢ ( +g ‘ 𝑃 ) = ( +g ‘ ( 1o mPoly 𝑅 ) )
109	108	a1i	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ) → ( +g ‘ 𝑃 ) = ( +g ‘ ( 1o mPoly 𝑅 ) ) )
110	101 103 104 106 109	gsumpropd	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ) → ( 𝑃 Σg ( 𝑘 ∈ ℕ0 ↦ ( ( 𝐴 ‘ 𝑘 ) · ( 𝑘 ↑ 𝑋 ) ) ) ) = ( ( 1o mPoly 𝑅 ) Σg ( 𝑘 ∈ ℕ0 ↦ ( ( 𝐴 ‘ 𝑘 ) · ( 𝑘 ↑ 𝑋 ) ) ) ) )
111		eqid	⊢ ( 0g ‘ 𝑃 ) = ( 0g ‘ 𝑃 )
112	8 1 111	ply1mpl0	⊢ ( 0g ‘ 𝑃 ) = ( 0g ‘ ( 1o mPoly 𝑅 ) )
113	8	mpllmod	⊢ ( ( 1o ∈ ω ∧ 𝑅 ∈ Ring ) → ( 1o mPoly 𝑅 ) ∈ LMod )
114	12 17 113	sylancr	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ) → ( 1o mPoly 𝑅 ) ∈ LMod )
115		lmodcmn	⊢ ( ( 1o mPoly 𝑅 ) ∈ LMod → ( 1o mPoly 𝑅 ) ∈ CMnd )
116	114 115	syl	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ) → ( 1o mPoly 𝑅 ) ∈ CMnd )
117	99	a1i	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ) → ℕ0 ∈ V )
118	1	ply1lmod	⊢ ( 𝑅 ∈ Ring → 𝑃 ∈ LMod )
119	118	ad2antrr	⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ) ∧ 𝑘 ∈ ℕ0 ) → 𝑃 ∈ LMod )
120		eqid	⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
121	7 3 1 120	coe1f	⊢ ( 𝐾 ∈ 𝐵 → 𝐴 : ℕ0 ⟶ ( Base ‘ 𝑅 ) )
122	121	adantl	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ) → 𝐴 : ℕ0 ⟶ ( Base ‘ 𝑅 ) )
123	122	ffvelrnda	⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ) ∧ 𝑘 ∈ ℕ0 ) → ( 𝐴 ‘ 𝑘 ) ∈ ( Base ‘ 𝑅 ) )
124	1	ply1sca	⊢ ( 𝑅 ∈ Ring → 𝑅 = ( Scalar ‘ 𝑃 ) )
125	124	eqcomd	⊢ ( 𝑅 ∈ Ring → ( Scalar ‘ 𝑃 ) = 𝑅 )
126	125	ad2antrr	⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ) ∧ 𝑘 ∈ ℕ0 ) → ( Scalar ‘ 𝑃 ) = 𝑅 )
127	126	fveq2d	⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ) ∧ 𝑘 ∈ ℕ0 ) → ( Base ‘ ( Scalar ‘ 𝑃 ) ) = ( Base ‘ 𝑅 ) )
128	123 127	eleqtrrd	⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ) ∧ 𝑘 ∈ ℕ0 ) → ( 𝐴 ‘ 𝑘 ) ∈ ( Base ‘ ( Scalar ‘ 𝑃 ) ) )
129	75	ad2antrr	⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ) ∧ 𝑘 ∈ ℕ0 ) → 𝑀 ∈ Mnd )
130		simpr	⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ) ∧ 𝑘 ∈ ℕ0 ) → 𝑘 ∈ ℕ0 )
131	82	ad2antrr	⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ) ∧ 𝑘 ∈ ℕ0 ) → 𝑋 ∈ 𝐵 )
132	58 6	mulgnn0cl	⊢ ( ( 𝑀 ∈ Mnd ∧ 𝑘 ∈ ℕ0 ∧ 𝑋 ∈ 𝐵 ) → ( 𝑘 ↑ 𝑋 ) ∈ 𝐵 )
133	129 130 131 132	syl3anc	⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ) ∧ 𝑘 ∈ ℕ0 ) → ( 𝑘 ↑ 𝑋 ) ∈ 𝐵 )
134		eqid	⊢ ( Scalar ‘ 𝑃 ) = ( Scalar ‘ 𝑃 )
135		eqid	⊢ ( Base ‘ ( Scalar ‘ 𝑃 ) ) = ( Base ‘ ( Scalar ‘ 𝑃 ) )
136	3 134 4 135	lmodvscl	⊢ ( ( 𝑃 ∈ LMod ∧ ( 𝐴 ‘ 𝑘 ) ∈ ( Base ‘ ( Scalar ‘ 𝑃 ) ) ∧ ( 𝑘 ↑ 𝑋 ) ∈ 𝐵 ) → ( ( 𝐴 ‘ 𝑘 ) · ( 𝑘 ↑ 𝑋 ) ) ∈ 𝐵 )
137	119 128 133 136	syl3anc	⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ) ∧ 𝑘 ∈ ℕ0 ) → ( ( 𝐴 ‘ 𝑘 ) · ( 𝑘 ↑ 𝑋 ) ) ∈ 𝐵 )
138	137	fmpttd	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ) → ( 𝑘 ∈ ℕ0 ↦ ( ( 𝐴 ‘ 𝑘 ) · ( 𝑘 ↑ 𝑋 ) ) ) : ℕ0 ⟶ 𝐵 )
139	1 2 3 4 5 6 7	ply1coefsupp	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ) → ( 𝑘 ∈ ℕ0 ↦ ( ( 𝐴 ‘ 𝑘 ) · ( 𝑘 ↑ 𝑋 ) ) ) finSupp ( 0g ‘ 𝑃 ) )
140		eqid	⊢ ( 𝑎 ∈ ( ℕ0 ↑m 1o ) ↦ ( 𝑎 ‘ ∅ ) ) = ( 𝑎 ∈ ( ℕ0 ↑m 1o ) ↦ ( 𝑎 ‘ ∅ ) )
141	43 99 29 140	mapsnf1o2	⊢ ( 𝑎 ∈ ( ℕ0 ↑m 1o ) ↦ ( 𝑎 ‘ ∅ ) ) : ( ℕ0 ↑m 1o ) –1-1-onto→ ℕ0
142	141	a1i	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ) → ( 𝑎 ∈ ( ℕ0 ↑m 1o ) ↦ ( 𝑎 ‘ ∅ ) ) : ( ℕ0 ↑m 1o ) –1-1-onto→ ℕ0 )
143	15 112 116 117 138 139 142	gsumf1o	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ) → ( ( 1o mPoly 𝑅 ) Σg ( 𝑘 ∈ ℕ0 ↦ ( ( 𝐴 ‘ 𝑘 ) · ( 𝑘 ↑ 𝑋 ) ) ) ) = ( ( 1o mPoly 𝑅 ) Σg ( ( 𝑘 ∈ ℕ0 ↦ ( ( 𝐴 ‘ 𝑘 ) · ( 𝑘 ↑ 𝑋 ) ) ) ∘ ( 𝑎 ∈ ( ℕ0 ↑m 1o ) ↦ ( 𝑎 ‘ ∅ ) ) ) ) )
144		eqidd	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ) → ( 𝑎 ∈ ( ℕ0 ↑m 1o ) ↦ ( 𝑎 ‘ ∅ ) ) = ( 𝑎 ∈ ( ℕ0 ↑m 1o ) ↦ ( 𝑎 ‘ ∅ ) ) )
145		eqidd	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ) → ( 𝑘 ∈ ℕ0 ↦ ( ( 𝐴 ‘ 𝑘 ) · ( 𝑘 ↑ 𝑋 ) ) ) = ( 𝑘 ∈ ℕ0 ↦ ( ( 𝐴 ‘ 𝑘 ) · ( 𝑘 ↑ 𝑋 ) ) ) )
146		fveq2	⊢ ( 𝑘 = ( 𝑎 ‘ ∅ ) → ( 𝐴 ‘ 𝑘 ) = ( 𝐴 ‘ ( 𝑎 ‘ ∅ ) ) )
147		oveq1	⊢ ( 𝑘 = ( 𝑎 ‘ ∅ ) → ( 𝑘 ↑ 𝑋 ) = ( ( 𝑎 ‘ ∅ ) ↑ 𝑋 ) )
148	146 147	oveq12d	⊢ ( 𝑘 = ( 𝑎 ‘ ∅ ) → ( ( 𝐴 ‘ 𝑘 ) · ( 𝑘 ↑ 𝑋 ) ) = ( ( 𝐴 ‘ ( 𝑎 ‘ ∅ ) ) · ( ( 𝑎 ‘ ∅ ) ↑ 𝑋 ) ) )
149	81 144 145 148	fmptco	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ) → ( ( 𝑘 ∈ ℕ0 ↦ ( ( 𝐴 ‘ 𝑘 ) · ( 𝑘 ↑ 𝑋 ) ) ) ∘ ( 𝑎 ∈ ( ℕ0 ↑m 1o ) ↦ ( 𝑎 ‘ ∅ ) ) ) = ( 𝑎 ∈ ( ℕ0 ↑m 1o ) ↦ ( ( 𝐴 ‘ ( 𝑎 ‘ ∅ ) ) · ( ( 𝑎 ‘ ∅ ) ↑ 𝑋 ) ) ) )
150	149	oveq2d	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ) → ( ( 1o mPoly 𝑅 ) Σg ( ( 𝑘 ∈ ℕ0 ↦ ( ( 𝐴 ‘ 𝑘 ) · ( 𝑘 ↑ 𝑋 ) ) ) ∘ ( 𝑎 ∈ ( ℕ0 ↑m 1o ) ↦ ( 𝑎 ‘ ∅ ) ) ) ) = ( ( 1o mPoly 𝑅 ) Σg ( 𝑎 ∈ ( ℕ0 ↑m 1o ) ↦ ( ( 𝐴 ‘ ( 𝑎 ‘ ∅ ) ) · ( ( 𝑎 ‘ ∅ ) ↑ 𝑋 ) ) ) ) )
151	110 143 150	3eqtrrd	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ) → ( ( 1o mPoly 𝑅 ) Σg ( 𝑎 ∈ ( ℕ0 ↑m 1o ) ↦ ( ( 𝐴 ‘ ( 𝑎 ‘ ∅ ) ) · ( ( 𝑎 ‘ ∅ ) ↑ 𝑋 ) ) ) ) = ( 𝑃 Σg ( 𝑘 ∈ ℕ0 ↦ ( ( 𝐴 ‘ 𝑘 ) · ( 𝑘 ↑ 𝑋 ) ) ) ) )
152	19 98 151	3eqtrd	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ) → 𝐾 = ( 𝑃 Σg ( 𝑘 ∈ ℕ0 ↦ ( ( 𝐴 ‘ 𝑘 ) · ( 𝑘 ↑ 𝑋 ) ) ) ) )