fply1

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

	Ref	Expression
Hypotheses	fply1.1	⊢ 0 = ( 0_g ‘ 𝑅 )
	fply1.2	⊢ 𝐵 = ( Base ‘ 𝑅 )
	fply1.3	⊢ 𝑃 = ( Base ‘ ( Poly₁ ‘ 𝑅 ) )
	fply1.4	⊢ ( 𝜑 → 𝐹 : ( ℕ₀ ↑_m 1_o ) ⟶ 𝐵 )
	fply1.5	⊢ ( 𝜑 → 𝐹 finSupp 0 )
Assertion	fply1	⊢ ( 𝜑 → 𝐹 ∈ 𝑃 )

Proof

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

Metamath Proof Explorer

Theorem fply1

Proof