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 ↾ 𝐵 ) ∈ 𝑄 )