ply1scl1OLD

Description: Obsolete version of ply1scl1 as of 12-Mar-2025. (Contributed by Stefan O'Rear, 1-Apr-2015) (Proof modification is discouraged.) (New usage is discouraged.)

	Ref	Expression
Hypotheses	ply1scl.p	$⊢ P = {Poly}_{1} (R)$
	ply1scl.a	$⊢ A = algSc (P)$
	ply1scl1.o	$⊢ \underset{˙}{1} = 1_{R}$
	ply1scl1.n	$⊢ N = 1_{P}$
Assertion	ply1scl1OLD	$⊢ R \in Ring \to A (\underset{˙}{1}) = N$

Proof

Step	Hyp	Ref	Expression
1		ply1scl.p	$⊢ P = {Poly}_{1} (R)$
2		ply1scl.a	$⊢ A = algSc (P)$
3		ply1scl1.o	$⊢ \underset{˙}{1} = 1_{R}$
4		ply1scl1.n	$⊢ N = 1_{P}$
5		eqid	$⊢ {Base}_{R} = {Base}_{R}$
6	5 3	ringidcl	$⊢ R \in Ring \to \underset{˙}{1} \in {Base}_{R}$
7	1	ply1sca2	$⊢ I (R) = Scalar (P)$
8		baseid	$⊢ Base = Slot {Base}_{ndx}$
9	8 5	strfvi	$⊢ {Base}_{R} = {Base}_{I (R)}$
10		eqid	$⊢ \cdot_{P} = \cdot_{P}$
11	2 7 9 10 4	asclval	$⊢ \underset{˙}{1} \in {Base}_{R} \to A (\underset{˙}{1}) = \underset{˙}{1} \cdot_{P} N$
12	6 11	syl	$⊢ R \in Ring \to A (\underset{˙}{1}) = \underset{˙}{1} \cdot_{P} N$
13		fvi	$⊢ R \in Ring \to I (R) = R$
14	13	fveq2d	$⊢ R \in Ring \to 1_{I (R)} = 1_{R}$
15	14 3	eqtr4di	$⊢ R \in Ring \to 1_{I (R)} = \underset{˙}{1}$
16	15	oveq1d	$⊢ R \in Ring \to 1_{I (R)} \cdot_{P} N = \underset{˙}{1} \cdot_{P} N$
17	1	ply1lmod	$⊢ R \in Ring \to P \in LMod$
18	1	ply1ring	$⊢ R \in Ring \to P \in Ring$
19		eqid	$⊢ {Base}_{P} = {Base}_{P}$
20	19 4	ringidcl	$⊢ P \in Ring \to N \in {Base}_{P}$
21	18 20	syl	$⊢ R \in Ring \to N \in {Base}_{P}$
22		eqid	$⊢ 1_{I (R)} = 1_{I (R)}$
23	19 7 10 22	lmodvs1	$⊢ (P \in LMod \land N \in {Base}_{P}) \to 1_{I (R)} \cdot_{P} N = N$
24	17 21 23	syl2anc	$⊢ R \in Ring \to 1_{I (R)} \cdot_{P} N = N$
25	12 16 24	3eqtr2d	$⊢ R \in Ring \to A (\underset{˙}{1}) = N$

Metamath Proof Explorer

Theorem ply1scl1OLD

Proof