Metamath Proof Explorer


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 P = Poly 1 R
ply1idvr1.x X = var 1 R
ply1idvr1.n N = mulGrp P
ply1idvr1.e × ˙ = N
Assertion ply1idvr1 R Ring 0 × ˙ X = 1 P

Proof

Step Hyp Ref Expression
1 ply1idvr1.p P = Poly 1 R
2 ply1idvr1.x X = var 1 R
3 ply1idvr1.n N = mulGrp P
4 ply1idvr1.e × ˙ = N
5 eqid Base P = Base P
6 2 1 5 vr1cl R Ring X Base P
7 3 5 mgpbas Base P = Base N
8 eqid 1 P = 1 P
9 3 8 ringidval 1 P = 0 N
10 7 9 4 mulg0 X Base P 0 × ˙ X = 1 P
11 6 10 syl R Ring 0 × ˙ X = 1 P