mplascl1

Description: The one scalar as a polynomial. (Contributed by SN, 12-Mar-2025)

Step	Hyp	Ref	Expression
1		mplascl1.w	$⊢ W = I mPoly R$
2		mplascl1.a	$⊢ A = algSc (W)$
3		mplascl1.o	$⊢ O = 1_{R}$
4		mplascl1.1	$⊢ \underset{˙}{1} = 1_{W}$
5		mplascl1.i	$⊢ φ \to I \in V$
6		mplascl1.r	$⊢ φ \to R \in Ring$
7	1 5 6	mplsca	$⊢ φ \to R = Scalar (W)$
8	7	fveq2d	$⊢ φ \to 1_{R} = 1_{Scalar (W)}$
9	3 8	eqtrid	$⊢ φ \to O = 1_{Scalar (W)}$
10	9	fveq2d	$⊢ φ \to A (O) = A (1_{Scalar (W)})$
11		eqid	$⊢ Scalar (W) = Scalar (W)$
12	1 5 6	mpllmodd	$⊢ φ \to W \in LMod$
13	1 5 6	mplringd	$⊢ φ \to W \in Ring$
14	2 11 12 13	ascl1	$⊢ φ \to A (1_{Scalar (W)}) = 1_{W}$
15	10 14	eqtrd	$⊢ φ \to A (O) = 1_{W}$
16	15 4	eqtr4di	$⊢ φ \to A (O) = \underset{˙}{1}$

Metamath Proof Explorer