Theorem ply1idvr1

Description: The identity of a polynomial ring expressed as power of the polynomial variable. (Contributed by AV, 14-Aug-2019) (Proof shortened by SN, 3-Jul-2025)

	Ref	Expression
Hypotheses	ply1idvr1.p	⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
	ply1idvr1.x	⊢ 𝑋 = ( var1 ‘ 𝑅 )
	ply1idvr1.n	⊢ 𝑁 = ( mulGrp ‘ 𝑃 )
	ply1idvr1.e	⊢ ↑ = ( .g ‘ 𝑁 )
Assertion	ply1idvr1	⊢ ( 𝑅 ∈ Ring → ( 0 ↑ 𝑋 ) = ( 1r ‘ 𝑃 ) )

Proof

Step	Hyp	Ref	Expression
1		ply1idvr1.p	⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
2		ply1idvr1.x	⊢ 𝑋 = ( var1 ‘ 𝑅 )
3		ply1idvr1.n	⊢ 𝑁 = ( mulGrp ‘ 𝑃 )
4		ply1idvr1.e	⊢ ↑ = ( .g ‘ 𝑁 )
5		eqid	⊢ ( Base ‘ 𝑃 ) = ( Base ‘ 𝑃 )
6	2 1 5	vr1cl	⊢ ( 𝑅 ∈ Ring → 𝑋 ∈ ( Base ‘ 𝑃 ) )
7	3 5	mgpbas	⊢ ( Base ‘ 𝑃 ) = ( Base ‘ 𝑁 )
8		eqid	⊢ ( 1r ‘ 𝑃 ) = ( 1r ‘ 𝑃 )
9	3 8	ringidval	⊢ ( 1r ‘ 𝑃 ) = ( 0g ‘ 𝑁 )
10	7 9 4	mulg0	⊢ ( 𝑋 ∈ ( Base ‘ 𝑃 ) → ( 0 ↑ 𝑋 ) = ( 1r ‘ 𝑃 ) )
11	6 10	syl	⊢ ( 𝑅 ∈ Ring → ( 0 ↑ 𝑋 ) = ( 1r ‘ 𝑃 ) )