This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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	$⊢ \underset{˙}{\times} = \cdot_{N}$
	Assertion	ply1idvr1	$⊢ R \in Ring \to 0 \underset{˙}{\times} 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	$⊢ \underset{˙}{\times} = \cdot_{N}$
5		eqid	$⊢ {Base}_{P} = {Base}_{P}$
6	2 1 5	vr1cl	$⊢ R \in Ring \to X \in {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 \in {Base}_{P} \to 0 \underset{˙}{\times} X = 1_{P}$
11	6 10	syl	$⊢ R \in Ring \to 0 \underset{˙}{\times} X = 1_{P}$