ply1scl0

Description: The zero scalar is zero. (Contributed by Stefan O'Rear, 29-Mar-2015)

Step	Hyp	Ref	Expression
1		ply1scl.p	$⊢ P = {Poly}_{1} (R)$
2		ply1scl.a	$⊢ A = algSc (P)$
3		ply1scl0.z	$⊢ \underset{˙}{0} = 0_{R}$
4		ply1scl0.y	$⊢ Y = 0_{P}$
5	1	ply1sca	$⊢ R \in Ring \to R = Scalar (P)$
6	5	fveq2d	$⊢ R \in Ring \to 0_{R} = 0_{Scalar (P)}$
7	3 6	eqtrid	$⊢ R \in Ring \to \underset{˙}{0} = 0_{Scalar (P)}$
8	7	fveq2d	$⊢ R \in Ring \to A (\underset{˙}{0}) = A (0_{Scalar (P)})$
9		eqid	$⊢ Scalar (P) = Scalar (P)$
10	1	ply1lmod	$⊢ R \in Ring \to P \in LMod$
11	1	ply1ring	$⊢ R \in Ring \to P \in Ring$
12	2 9 10 11	ascl0	$⊢ R \in Ring \to A (0_{Scalar (P)}) = 0_{P}$
13	8 12	eqtrd	$⊢ R \in Ring \to A (\underset{˙}{0}) = 0_{P}$
14	13 4	eqtr4di	$⊢ R \in Ring \to A (\underset{˙}{0}) = Y$

Metamath Proof Explorer