pf1id

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

Step	Hyp	Ref	Expression
1		pf1const.b	$⊢ B = {Base}_{R}$
2		pf1const.q	$⊢ Q = ran {eval}_{1} (R)$
3		eqid	$⊢ {eval}_{1} (R) = {eval}_{1} (R)$
4		eqid	$⊢ {var}_{1} (R) = {var}_{1} (R)$
5	3 4 1	evl1var	$⊢ R \in CRing \to {eval}_{1} (R) ({var}_{1} (R)) = {I ↾}_{B}$
6		eqid	$⊢ {Poly}_{1} (R) = {Poly}_{1} (R)$
7		eqid	$⊢ R ↑_{𝑠} B = R ↑_{𝑠} B$
8	3 6 7 1	evl1rhm	$⊢ R \in CRing \to {eval}_{1} (R) \in ({Poly}_{1} (R) RingHom (R ↑_{𝑠} B))$
9		eqid	$⊢ {Base}_{{Poly}_{1} (R)} = {Base}_{{Poly}_{1} (R)}$
10		eqid	$⊢ {Base}_{(R ↑_{𝑠} B)} = {Base}_{(R ↑_{𝑠} B)}$
11	9 10	rhmf	$⊢ {eval}_{1} (R) \in ({Poly}_{1} (R) RingHom (R ↑_{𝑠} B)) \to {eval}_{1} (R) : {Base}_{{Poly}_{1} (R)} ⟶ {Base}_{(R ↑_{𝑠} B)}$
12		ffn	$⊢ {eval}_{1} (R) : {Base}_{{Poly}_{1} (R)} ⟶ {Base}_{(R ↑_{𝑠} B)} \to {eval}_{1} (R) Fn {Base}_{{Poly}_{1} (R)}$
13	8 11 12	3syl	$⊢ R \in CRing \to {eval}_{1} (R) Fn {Base}_{{Poly}_{1} (R)}$
14		crngring	$⊢ R \in CRing \to R \in Ring$
15	4 6 9	vr1cl	$⊢ R \in Ring \to {var}_{1} (R) \in {Base}_{{Poly}_{1} (R)}$
16	14 15	syl	$⊢ R \in CRing \to {var}_{1} (R) \in {Base}_{{Poly}_{1} (R)}$
17		fnfvelrn	$⊢ ({eval}_{1} (R) Fn {Base}_{{Poly}_{1} (R)} \land {var}_{1} (R) \in {Base}_{{Poly}_{1} (R)}) \to {eval}_{1} (R) ({var}_{1} (R)) \in ran {eval}_{1} (R)$
18	13 16 17	syl2anc	$⊢ R \in CRing \to {eval}_{1} (R) ({var}_{1} (R)) \in ran {eval}_{1} (R)$
19	5 18	eqeltrrd	$⊢ R \in CRing \to {I ↾}_{B} \in ran {eval}_{1} (R)$
20	19 2	eleqtrrdi	$⊢ R \in CRing \to {I ↾}_{B} \in Q$

Metamath Proof Explorer