This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem pf1id

Description: The identity is a polynomial function. (Contributed by Mario Carneiro, 20-Mar-2015)

Ref Expression
Hypotheses pf1const.b ⊢ 𝐵 = ( Base ‘ 𝑅 )
pf1const.q ⊢ 𝑄 = ran ( eval1 ‘ 𝑅 )
Assertion pf1id ( 𝑅 ∈ CRing → ( I ↾ 𝐵 ) ∈ 𝑄 )

Proof

Step Hyp Ref Expression
1 pf1const.b ⊢ 𝐵 = ( Base ‘ 𝑅 )
2 pf1const.q ⊢ 𝑄 = ran ( eval1 ‘ 𝑅 )
3 eqid ⊢ ( eval1 ‘ 𝑅 ) = ( eval1 ‘ 𝑅 )
4 eqid ⊢ ( var1 ‘ 𝑅 ) = ( var1 ‘ 𝑅 )
5 3 4 1 evl1var ⊢ ( 𝑅 ∈ CRing → ( ( eval1 ‘ 𝑅 ) ‘ ( var1 ‘ 𝑅 ) ) = ( I ↾ 𝐵 ) )
6 eqid ⊢ ( Poly1 ‘ 𝑅 ) = ( Poly1 ‘ 𝑅 )
7 eqid ⊢ ( 𝑅 ↑s 𝐵 ) = ( 𝑅 ↑s 𝐵 )
8 3 6 7 1 evl1rhm ⊢ ( 𝑅 ∈ CRing → ( eval1 ‘ 𝑅 ) ∈ ( ( Poly1 ‘ 𝑅 ) RingHom ( 𝑅 ↑s 𝐵 ) ) )
9 eqid ⊢ ( Base ‘ ( Poly1 ‘ 𝑅 ) ) = ( Base ‘ ( Poly1 ‘ 𝑅 ) )
10 eqid ⊢ ( Base ‘ ( 𝑅 ↑s 𝐵 ) ) = ( Base ‘ ( 𝑅 ↑s 𝐵 ) )
11 9 10 rhmf ⊢ ( ( eval1 ‘ 𝑅 ) ∈ ( ( Poly1 ‘ 𝑅 ) RingHom ( 𝑅 ↑s 𝐵 ) ) → ( eval1 ‘ 𝑅 ) : ( Base ‘ ( Poly1 ‘ 𝑅 ) ) ⟶ ( Base ‘ ( 𝑅 ↑s 𝐵 ) ) )
12 ffn ⊢ ( ( eval1 ‘ 𝑅 ) : ( Base ‘ ( Poly1 ‘ 𝑅 ) ) ⟶ ( Base ‘ ( 𝑅 ↑s 𝐵 ) ) → ( eval1 ‘ 𝑅 ) Fn ( Base ‘ ( Poly1 ‘ 𝑅 ) ) )
13 8 11 12 3syl ⊢ ( 𝑅 ∈ CRing → ( eval1 ‘ 𝑅 ) Fn ( Base ‘ ( Poly1 ‘ 𝑅 ) ) )
14 crngring ⊢ ( 𝑅 ∈ CRing → 𝑅 ∈ Ring )
15 4 6 9 vr1cl ⊢ ( 𝑅 ∈ Ring → ( var1 ‘ 𝑅 ) ∈ ( Base ‘ ( Poly1 ‘ 𝑅 ) ) )
16 14 15 syl ⊢ ( 𝑅 ∈ CRing → ( var1 ‘ 𝑅 ) ∈ ( Base ‘ ( Poly1 ‘ 𝑅 ) ) )
17 fnfvelrn ⊢ ( ( ( eval1 ‘ 𝑅 ) Fn ( Base ‘ ( Poly1 ‘ 𝑅 ) ) ∧ ( var1 ‘ 𝑅 ) ∈ ( Base ‘ ( Poly1 ‘ 𝑅 ) ) ) → ( ( eval1 ‘ 𝑅 ) ‘ ( var1 ‘ 𝑅 ) ) ∈ ran ( eval1 ‘ 𝑅 ) )
18 13 16 17 syl2anc ⊢ ( 𝑅 ∈ CRing → ( ( eval1 ‘ 𝑅 ) ‘ ( var1 ‘ 𝑅 ) ) ∈ ran ( eval1 ‘ 𝑅 ) )
19 5 18 eqeltrrd ⊢ ( 𝑅 ∈ CRing → ( I ↾ 𝐵 ) ∈ ran ( eval1 ‘ 𝑅 ) )
20 19 2 eleqtrrdi ⊢ ( 𝑅 ∈ CRing → ( I ↾ 𝐵 ) ∈ 𝑄 )