Theorem ply1idvr1

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

	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		eqid	⊢ ( 1r ‘ 𝑅 ) = ( 1r ‘ 𝑅 )
7	5 6	ringidcl	⊢ ( 𝑅 ∈ Ring → ( 1r ‘ 𝑅 ) ∈ ( Base ‘ 𝑅 ) )
8		eqid	⊢ ( ·𝑠 ‘ 𝑃 ) = ( ·𝑠 ‘ 𝑃 )
9		eqid	⊢ ( algSc ‘ 𝑃 ) = ( algSc ‘ 𝑃 )
10	5 1 2 8 3 4 9	ply1scltm	⊢ ( ( 𝑅 ∈ Ring ∧ ( 1r ‘ 𝑅 ) ∈ ( Base ‘ 𝑅 ) ) → ( ( algSc ‘ 𝑃 ) ‘ ( 1r ‘ 𝑅 ) ) = ( ( 1r ‘ 𝑅 ) ( ·𝑠 ‘ 𝑃 ) ( 0 ↑ 𝑋 ) ) )
11	7 10	mpdan	⊢ ( 𝑅 ∈ Ring → ( ( algSc ‘ 𝑃 ) ‘ ( 1r ‘ 𝑅 ) ) = ( ( 1r ‘ 𝑅 ) ( ·𝑠 ‘ 𝑃 ) ( 0 ↑ 𝑋 ) ) )
12	1	ply1sca	⊢ ( 𝑅 ∈ Ring → 𝑅 = ( Scalar ‘ 𝑃 ) )
13	12	fveq2d	⊢ ( 𝑅 ∈ Ring → ( 1r ‘ 𝑅 ) = ( 1r ‘ ( Scalar ‘ 𝑃 ) ) )
14	13	oveq1d	⊢ ( 𝑅 ∈ Ring → ( ( 1r ‘ 𝑅 ) ( ·𝑠 ‘ 𝑃 ) ( 0 ↑ 𝑋 ) ) = ( ( 1r ‘ ( Scalar ‘ 𝑃 ) ) ( ·𝑠 ‘ 𝑃 ) ( 0 ↑ 𝑋 ) ) )
15	1	ply1lmod	⊢ ( 𝑅 ∈ Ring → 𝑃 ∈ LMod )
16		0nn0	⊢ 0 ∈ ℕ0
17		eqid	⊢ ( Base ‘ 𝑃 ) = ( Base ‘ 𝑃 )
18	1 2 3 4 17	ply1moncl	⊢ ( ( 𝑅 ∈ Ring ∧ 0 ∈ ℕ0 ) → ( 0 ↑ 𝑋 ) ∈ ( Base ‘ 𝑃 ) )
19	16 18	mpan2	⊢ ( 𝑅 ∈ Ring → ( 0 ↑ 𝑋 ) ∈ ( Base ‘ 𝑃 ) )
20		eqid	⊢ ( Scalar ‘ 𝑃 ) = ( Scalar ‘ 𝑃 )
21		eqid	⊢ ( 1r ‘ ( Scalar ‘ 𝑃 ) ) = ( 1r ‘ ( Scalar ‘ 𝑃 ) )
22	17 20 8 21	lmodvs1	⊢ ( ( 𝑃 ∈ LMod ∧ ( 0 ↑ 𝑋 ) ∈ ( Base ‘ 𝑃 ) ) → ( ( 1r ‘ ( Scalar ‘ 𝑃 ) ) ( ·𝑠 ‘ 𝑃 ) ( 0 ↑ 𝑋 ) ) = ( 0 ↑ 𝑋 ) )
23	15 19 22	syl2anc	⊢ ( 𝑅 ∈ Ring → ( ( 1r ‘ ( Scalar ‘ 𝑃 ) ) ( ·𝑠 ‘ 𝑃 ) ( 0 ↑ 𝑋 ) ) = ( 0 ↑ 𝑋 ) )
24	11 14 23	3eqtrrd	⊢ ( 𝑅 ∈ Ring → ( 0 ↑ 𝑋 ) = ( ( algSc ‘ 𝑃 ) ‘ ( 1r ‘ 𝑅 ) ) )
25		eqid	⊢ ( 1r ‘ 𝑃 ) = ( 1r ‘ 𝑃 )
26	1 9 6 25	ply1scl1	⊢ ( 𝑅 ∈ Ring → ( ( algSc ‘ 𝑃 ) ‘ ( 1r ‘ 𝑅 ) ) = ( 1r ‘ 𝑃 ) )
27	24 26	eqtrd	⊢ ( 𝑅 ∈ Ring → ( 0 ↑ 𝑋 ) = ( 1r ‘ 𝑃 ) )