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

Metamath Proof Explorer

Theorem ply1scl1

Description: The one scalar is the unit polynomial. (Contributed by Stefan O'Rear, 1-Apr-2015) (Proof shortened by SN, 12-Mar-2025)

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 1 ply1sca ⊢ ( 𝑅 ∈ Ring → 𝑅 = ( Scalar ‘ 𝑃 ) )
6 5 fveq2d ⊢ ( 𝑅 ∈ Ring → ( 1r ‘ 𝑅 ) = ( 1r ‘ ( Scalar ‘ 𝑃 ) ) )
7 3 6 eqtrid ⊢ ( 𝑅 ∈ Ring → 1 = ( 1r ‘ ( Scalar ‘ 𝑃 ) ) )
8 7 fveq2d ⊢ ( 𝑅 ∈ Ring → ( 𝐴 ‘ 1 ) = ( 𝐴 ‘ ( 1r ‘ ( Scalar ‘ 𝑃 ) ) ) )
9 eqid ⊢ ( Scalar ‘ 𝑃 ) = ( Scalar ‘ 𝑃 )
10 1 ply1lmod ⊢ ( 𝑅 ∈ Ring → 𝑃 ∈ LMod )
11 1 ply1ring ⊢ ( 𝑅 ∈ Ring → 𝑃 ∈ Ring )
12 2 9 10 11 ascl1 ⊢ ( 𝑅 ∈ Ring → ( 𝐴 ‘ ( 1r ‘ ( Scalar ‘ 𝑃 ) ) ) = ( 1r ‘ 𝑃 ) )
13 8 12 eqtrd ⊢ ( 𝑅 ∈ Ring → ( 𝐴 ‘ 1 ) = ( 1r ‘ 𝑃 ) )
14 13 4 eqtr4di ⊢ ( 𝑅 ∈ Ring → ( 𝐴 ‘ 1 ) = 𝑁 )