ply1scl0OLD

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

	Ref	Expression
Hypotheses	ply1scl.p	\|- P = ( Poly1 ` R )
	ply1scl.a	\|- A = ( algSc ` P )
	ply1scl0.z	\|- .0. = ( 0g ` R )
	ply1scl0.y	\|- Y = ( 0g ` P )
Assertion	ply1scl0OLD	\|- ( R e. Ring -> ( A ` .0. ) = Y )

Proof

Step	Hyp	Ref	Expression
1		ply1scl.p	\|- P = ( Poly1 ` R )
2		ply1scl.a	\|- A = ( algSc ` P )
3		ply1scl0.z	\|- .0. = ( 0g ` R )
4		ply1scl0.y	\|- Y = ( 0g ` P )
5		eqid	\|- ( Base ` R ) = ( Base ` R )
6	5 3	ring0cl	\|- ( R e. Ring -> .0. e. ( 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	\|- ( .s ` P ) = ( .s ` P )
11		eqid	\|- ( 1r ` P ) = ( 1r ` P )
12	2 7 9 10 11	asclval	\|- ( .0. e. ( Base ` R ) -> ( A ` .0. ) = ( .0. ( .s ` P ) ( 1r ` P ) ) )
13	6 12	syl	\|- ( R e. Ring -> ( A ` .0. ) = ( .0. ( .s ` P ) ( 1r ` P ) ) )
14		fvi	\|- ( R e. Ring -> ( _I ` R ) = R )
15	14	fveq2d	\|- ( R e. Ring -> ( 0g ` ( _I ` R ) ) = ( 0g ` R ) )
16	3 15	eqtr4id	\|- ( R e. Ring -> .0. = ( 0g ` ( _I ` R ) ) )
17	16	oveq1d	\|- ( R e. Ring -> ( .0. ( .s ` P ) ( 1r ` P ) ) = ( ( 0g ` ( _I ` R ) ) ( .s ` P ) ( 1r ` P ) ) )
18	1	ply1lmod	\|- ( R e. Ring -> P e. LMod )
19	1	ply1ring	\|- ( R e. Ring -> P e. Ring )
20		eqid	\|- ( Base ` P ) = ( Base ` P )
21	20 11	ringidcl	\|- ( P e. Ring -> ( 1r ` P ) e. ( Base ` P ) )
22	19 21	syl	\|- ( R e. Ring -> ( 1r ` P ) e. ( Base ` P ) )
23		eqid	\|- ( 0g ` ( _I ` R ) ) = ( 0g ` ( _I ` R ) )
24	20 7 10 23 4	lmod0vs	\|- ( ( P e. LMod /\ ( 1r ` P ) e. ( Base ` P ) ) -> ( ( 0g ` ( _I ` R ) ) ( .s ` P ) ( 1r ` P ) ) = Y )
25	18 22 24	syl2anc	\|- ( R e. Ring -> ( ( 0g ` ( _I ` R ) ) ( .s ` P ) ( 1r ` P ) ) = Y )
26	13 17 25	3eqtrd	\|- ( R e. Ring -> ( A ` .0. ) = Y )

Metamath Proof Explorer

Theorem ply1scl0OLD

Proof