Description: Univariate polynomial base set elements are functions. (Contributed by Stefan O'Rear, 21-Mar-2015)
Ref | Expression | ||
---|---|---|---|
Hypotheses | ply1rcl.p | ⊢ 𝑃 = ( Poly1 ‘ 𝑅 ) | |
ply1rcl.b | ⊢ 𝐵 = ( Base ‘ 𝑃 ) | ||
ply1basf.k | ⊢ 𝐾 = ( Base ‘ 𝑅 ) | ||
Assertion | ply1basf | ⊢ ( 𝐹 ∈ 𝐵 → 𝐹 : ( ℕ0 ↑m 1o ) ⟶ 𝐾 ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ply1rcl.p | ⊢ 𝑃 = ( Poly1 ‘ 𝑅 ) | |
2 | ply1rcl.b | ⊢ 𝐵 = ( Base ‘ 𝑃 ) | |
3 | ply1basf.k | ⊢ 𝐾 = ( Base ‘ 𝑅 ) | |
4 | eqid | ⊢ ( 1o mPoly 𝑅 ) = ( 1o mPoly 𝑅 ) | |
5 | eqid | ⊢ ( Base ‘ ( 1o mPoly 𝑅 ) ) = ( Base ‘ ( 1o mPoly 𝑅 ) ) | |
6 | psr1baslem | ⊢ ( ℕ0 ↑m 1o ) = { 𝑎 ∈ ( ℕ0 ↑m 1o ) ∣ ( ◡ 𝑎 “ ℕ ) ∈ Fin } | |
7 | id | ⊢ ( 𝐹 ∈ 𝐵 → 𝐹 ∈ 𝐵 ) | |
8 | 1 2 | ply1bas | ⊢ 𝐵 = ( Base ‘ ( 1o mPoly 𝑅 ) ) |
9 | 7 8 | eleqtrdi | ⊢ ( 𝐹 ∈ 𝐵 → 𝐹 ∈ ( Base ‘ ( 1o mPoly 𝑅 ) ) ) |
10 | 4 3 5 6 9 | mplelf | ⊢ ( 𝐹 ∈ 𝐵 → 𝐹 : ( ℕ0 ↑m 1o ) ⟶ 𝐾 ) |