Theorem fply1

Description: Conditions for a function to be an univariate polynomial. (Contributed by Thierry Arnoux, 19-Aug-2023)

	Ref	Expression
Hypotheses	fply1.1	⊢ 0 = ( 0g ‘ 𝑅 )
	fply1.2	⊢ 𝐵 = ( Base ‘ 𝑅 )
	fply1.3	⊢ 𝑃 = ( Base ‘ ( Poly1 ‘ 𝑅 ) )
	fply1.4	⊢ ( 𝜑 → 𝐹 : ( ℕ0 ↑m 1o ) ⟶ 𝐵 )
	fply1.5	⊢ ( 𝜑 → 𝐹 finSupp 0 )
Assertion	fply1	⊢ ( 𝜑 → 𝐹 ∈ 𝑃 )

Proof

Step	Hyp	Ref	Expression
1		fply1.1	⊢ 0 = ( 0g ‘ 𝑅 )
2		fply1.2	⊢ 𝐵 = ( Base ‘ 𝑅 )
3		fply1.3	⊢ 𝑃 = ( Base ‘ ( Poly1 ‘ 𝑅 ) )
4		fply1.4	⊢ ( 𝜑 → 𝐹 : ( ℕ0 ↑m 1o ) ⟶ 𝐵 )
5		fply1.5	⊢ ( 𝜑 → 𝐹 finSupp 0 )
6	2	fvexi	⊢ 𝐵 ∈ V
7		ovex	⊢ ( ℕ0 ↑m 1o ) ∈ V
8	6 7	elmap	⊢ ( 𝐹 ∈ ( 𝐵 ↑m ( ℕ0 ↑m 1o ) ) ↔ 𝐹 : ( ℕ0 ↑m 1o ) ⟶ 𝐵 )
9	4 8	sylibr	⊢ ( 𝜑 → 𝐹 ∈ ( 𝐵 ↑m ( ℕ0 ↑m 1o ) ) )
10		df1o2	⊢ 1o = { ∅ }
11		snfi	⊢ { ∅ } ∈ Fin
12	10 11	eqeltri	⊢ 1o ∈ Fin
13	12	a1i	⊢ ( 𝑓 ∈ ( ℕ0 ↑m 1o ) → 1o ∈ Fin )
14		elmapi	⊢ ( 𝑓 ∈ ( ℕ0 ↑m 1o ) → 𝑓 : 1o ⟶ ℕ0 )
15	13 14	fisuppfi	⊢ ( 𝑓 ∈ ( ℕ0 ↑m 1o ) → ( ◡ 𝑓 “ ℕ ) ∈ Fin )
16	15	rabeqc	⊢ { 𝑓 ∈ ( ℕ0 ↑m 1o ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } = ( ℕ0 ↑m 1o )
17	16	oveq2i	⊢ ( 𝐵 ↑m { 𝑓 ∈ ( ℕ0 ↑m 1o ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ) = ( 𝐵 ↑m ( ℕ0 ↑m 1o ) )
18	9 17	eleqtrrdi	⊢ ( 𝜑 → 𝐹 ∈ ( 𝐵 ↑m { 𝑓 ∈ ( ℕ0 ↑m 1o ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ) )
19		eqid	⊢ ( 1o mPwSer 𝑅 ) = ( 1o mPwSer 𝑅 )
20		eqid	⊢ { 𝑓 ∈ ( ℕ0 ↑m 1o ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } = { 𝑓 ∈ ( ℕ0 ↑m 1o ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin }
21		eqid	⊢ ( Base ‘ ( 1o mPwSer 𝑅 ) ) = ( Base ‘ ( 1o mPwSer 𝑅 ) )
22		1oex	⊢ 1o ∈ V
23	22	a1i	⊢ ( 𝜑 → 1o ∈ V )
24	19 2 20 21 23	psrbas	⊢ ( 𝜑 → ( Base ‘ ( 1o mPwSer 𝑅 ) ) = ( 𝐵 ↑m { 𝑓 ∈ ( ℕ0 ↑m 1o ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ) )
25	18 24	eleqtrrd	⊢ ( 𝜑 → 𝐹 ∈ ( Base ‘ ( 1o mPwSer 𝑅 ) ) )
26		eqid	⊢ ( 1o mPoly 𝑅 ) = ( 1o mPoly 𝑅 )
27		eqid	⊢ ( Poly1 ‘ 𝑅 ) = ( Poly1 ‘ 𝑅 )
28		eqid	⊢ ( PwSer1 ‘ 𝑅 ) = ( PwSer1 ‘ 𝑅 )
29	27 28 3	ply1bas	⊢ 𝑃 = ( Base ‘ ( 1o mPoly 𝑅 ) )
30	26 19 21 1 29	mplelbas	⊢ ( 𝐹 ∈ 𝑃 ↔ ( 𝐹 ∈ ( Base ‘ ( 1o mPwSer 𝑅 ) ) ∧ 𝐹 finSupp 0 ) )
31	25 5 30	sylanbrc	⊢ ( 𝜑 → 𝐹 ∈ 𝑃 )