Theorem ply1scl0

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

	Ref	Expression
Hypotheses	ply1scl.p	⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
	ply1scl.a	⊢ 𝐴 = ( algSc ‘ 𝑃 )
	ply1scl0.z	⊢ 0 = ( 0g ‘ 𝑅 )
	ply1scl0.y	⊢ 𝑌 = ( 0g ‘ 𝑃 )
Assertion	ply1scl0	⊢ ( 𝑅 ∈ Ring → ( 𝐴 ‘ 0 ) = 𝑌 )

Proof

Step	Hyp	Ref	Expression
1		ply1scl.p	⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
2		ply1scl.a	⊢ 𝐴 = ( algSc ‘ 𝑃 )
3		ply1scl0.z	⊢ 0 = ( 0g ‘ 𝑅 )
4		ply1scl0.y	⊢ 𝑌 = ( 0g ‘ 𝑃 )
5		eqid	⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
6	5 3	ring0cl	⊢ ( 𝑅 ∈ Ring → 0 ∈ ( Base ‘ 𝑅 ) )
7	1	ply1sca2	⊢ ( I ‘ 𝑅 ) = ( Scalar ‘ 𝑃 )
8		df-base	⊢ Base = Slot 1
9	8 5	strfvi	⊢ ( Base ‘ 𝑅 ) = ( Base ‘ ( I ‘ 𝑅 ) )
10		eqid	⊢ ( ·𝑠 ‘ 𝑃 ) = ( ·𝑠 ‘ 𝑃 )
11		eqid	⊢ ( 1r ‘ 𝑃 ) = ( 1r ‘ 𝑃 )
12	2 7 9 10 11	asclval	⊢ ( 0 ∈ ( Base ‘ 𝑅 ) → ( 𝐴 ‘ 0 ) = ( 0 ( ·𝑠 ‘ 𝑃 ) ( 1r ‘ 𝑃 ) ) )
13	6 12	syl	⊢ ( 𝑅 ∈ Ring → ( 𝐴 ‘ 0 ) = ( 0 ( ·𝑠 ‘ 𝑃 ) ( 1r ‘ 𝑃 ) ) )
14		fvi	⊢ ( 𝑅 ∈ Ring → ( I ‘ 𝑅 ) = 𝑅 )
15	14	fveq2d	⊢ ( 𝑅 ∈ Ring → ( 0g ‘ ( I ‘ 𝑅 ) ) = ( 0g ‘ 𝑅 ) )
16	3 15	eqtr4id	⊢ ( 𝑅 ∈ Ring → 0 = ( 0g ‘ ( I ‘ 𝑅 ) ) )
17	16	oveq1d	⊢ ( 𝑅 ∈ Ring → ( 0 ( ·𝑠 ‘ 𝑃 ) ( 1r ‘ 𝑃 ) ) = ( ( 0g ‘ ( I ‘ 𝑅 ) ) ( ·𝑠 ‘ 𝑃 ) ( 1r ‘ 𝑃 ) ) )
18	1	ply1lmod	⊢ ( 𝑅 ∈ Ring → 𝑃 ∈ LMod )
19	1	ply1ring	⊢ ( 𝑅 ∈ Ring → 𝑃 ∈ Ring )
20		eqid	⊢ ( Base ‘ 𝑃 ) = ( Base ‘ 𝑃 )
21	20 11	ringidcl	⊢ ( 𝑃 ∈ Ring → ( 1r ‘ 𝑃 ) ∈ ( Base ‘ 𝑃 ) )
22	19 21	syl	⊢ ( 𝑅 ∈ Ring → ( 1r ‘ 𝑃 ) ∈ ( Base ‘ 𝑃 ) )
23		eqid	⊢ ( 0g ‘ ( I ‘ 𝑅 ) ) = ( 0g ‘ ( I ‘ 𝑅 ) )
24	20 7 10 23 4	lmod0vs	⊢ ( ( 𝑃 ∈ LMod ∧ ( 1r ‘ 𝑃 ) ∈ ( Base ‘ 𝑃 ) ) → ( ( 0g ‘ ( I ‘ 𝑅 ) ) ( ·𝑠 ‘ 𝑃 ) ( 1r ‘ 𝑃 ) ) = 𝑌 )
25	18 22 24	syl2anc	⊢ ( 𝑅 ∈ Ring → ( ( 0g ‘ ( I ‘ 𝑅 ) ) ( ·𝑠 ‘ 𝑃 ) ( 1r ‘ 𝑃 ) ) = 𝑌 )
26	13 17 25	3eqtrd	⊢ ( 𝑅 ∈ Ring → ( 𝐴 ‘ 0 ) = 𝑌 )