Theorem ply1scl1

Description: The one scalar is the unit polynomial. (Contributed by Stefan O'Rear, 1-Apr-2015)

	Ref	Expression
Hypotheses	ply1scl.p	⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
	ply1scl.a	⊢ 𝐴 = ( algSc ‘ 𝑃 )
	ply1scl1.o	⊢ 1 = ( 1r ‘ 𝑅 )
	ply1scl1.n	⊢ 𝑁 = ( 1r ‘ 𝑃 )
Assertion	ply1scl1	⊢ ( 𝑅 ∈ Ring → ( 𝐴 ‘ 1 ) = 𝑁 )

Proof

Step	Hyp	Ref	Expression
1		ply1scl.p	⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
2		ply1scl.a	⊢ 𝐴 = ( algSc ‘ 𝑃 )
3		ply1scl1.o	⊢ 1 = ( 1r ‘ 𝑅 )
4		ply1scl1.n	⊢ 𝑁 = ( 1r ‘ 𝑃 )
5		eqid	⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
6	5 3	ringidcl	⊢ ( 𝑅 ∈ Ring → 1 ∈ ( Base ‘ 𝑅 ) )
7	1	ply1sca2	⊢ ( I ‘ 𝑅 ) = ( Scalar ‘ 𝑃 )
8		baseid	⊢ Base = Slot ( Base ‘ ndx )
9	8 5	strfvi	⊢ ( Base ‘ 𝑅 ) = ( Base ‘ ( I ‘ 𝑅 ) )
10		eqid	⊢ ( ·𝑠 ‘ 𝑃 ) = ( ·𝑠 ‘ 𝑃 )
11	2 7 9 10 4	asclval	⊢ ( 1 ∈ ( Base ‘ 𝑅 ) → ( 𝐴 ‘ 1 ) = ( 1 ( ·𝑠 ‘ 𝑃 ) 𝑁 ) )
12	6 11	syl	⊢ ( 𝑅 ∈ Ring → ( 𝐴 ‘ 1 ) = ( 1 ( ·𝑠 ‘ 𝑃 ) 𝑁 ) )
13		fvi	⊢ ( 𝑅 ∈ Ring → ( I ‘ 𝑅 ) = 𝑅 )
14	13	fveq2d	⊢ ( 𝑅 ∈ Ring → ( 1r ‘ ( I ‘ 𝑅 ) ) = ( 1r ‘ 𝑅 ) )
15	14 3	eqtr4di	⊢ ( 𝑅 ∈ Ring → ( 1r ‘ ( I ‘ 𝑅 ) ) = 1 )
16	15	oveq1d	⊢ ( 𝑅 ∈ Ring → ( ( 1r ‘ ( I ‘ 𝑅 ) ) ( ·𝑠 ‘ 𝑃 ) 𝑁 ) = ( 1 ( ·𝑠 ‘ 𝑃 ) 𝑁 ) )
17	1	ply1lmod	⊢ ( 𝑅 ∈ Ring → 𝑃 ∈ LMod )
18	1	ply1ring	⊢ ( 𝑅 ∈ Ring → 𝑃 ∈ Ring )
19		eqid	⊢ ( Base ‘ 𝑃 ) = ( Base ‘ 𝑃 )
20	19 4	ringidcl	⊢ ( 𝑃 ∈ Ring → 𝑁 ∈ ( Base ‘ 𝑃 ) )
21	18 20	syl	⊢ ( 𝑅 ∈ Ring → 𝑁 ∈ ( Base ‘ 𝑃 ) )
22		eqid	⊢ ( 1r ‘ ( I ‘ 𝑅 ) ) = ( 1r ‘ ( I ‘ 𝑅 ) )
23	19 7 10 22	lmodvs1	⊢ ( ( 𝑃 ∈ LMod ∧ 𝑁 ∈ ( Base ‘ 𝑃 ) ) → ( ( 1r ‘ ( I ‘ 𝑅 ) ) ( ·𝑠 ‘ 𝑃 ) 𝑁 ) = 𝑁 )
24	17 21 23	syl2anc	⊢ ( 𝑅 ∈ Ring → ( ( 1r ‘ ( I ‘ 𝑅 ) ) ( ·𝑠 ‘ 𝑃 ) 𝑁 ) = 𝑁 )
25	12 16 24	3eqtr2d	⊢ ( 𝑅 ∈ Ring → ( 𝐴 ‘ 1 ) = 𝑁 )