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	⊢ 𝑃 = ( Poly₁ ‘ 𝑅 )
	ply1coe.x	⊢ 𝑋 = ( var₁ ‘ 𝑅 )
	ply1coe.b	⊢ 𝐵 = ( Base ‘ 𝑃 )
	ply1coe.n	⊢ · = ( ·_𝑠 ‘ 𝑃 )
	ply1coe.m	⊢ 𝑀 = ( mulGrp ‘ 𝑃 )
	ply1coe.e	⊢ ↑ = ( ._g ‘ 𝑀 )
	ply1coe.a	⊢ 𝐴 = ( coe₁ ‘ 𝐾 )
Assertion	ply1coe	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐾 ∈ 𝐵 ) → 𝐾 = ( 𝑃 Σ_g ( 𝑘 ∈ ℕ₀ ↦ ( ( 𝐴 ‘ 𝑘 ) · ( 𝑘 ↑ 𝑋 ) ) ) ) )

Proof

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

Metamath Proof Explorer

Theorem ply1coe

Proof