This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem 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 ⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
ply1scl.a ⊢ 𝐴 = ( algSc ‘ 𝑃 )
ply1scl0.z ⊢ 0 = ( 0g ‘ 𝑅 )
ply1scl0.y ⊢ 𝑌 = ( 0g ‘ 𝑃 )
Assertion ply1scl0OLD ( 𝑅 ∈ 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 baseid ⊢ Base = Slot ( Base ‘ ndx )
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 ) = 𝑌 )