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

Metamath Proof Explorer

Theorem ply1ascl0

Description: The zero scalar as a polynomial. (Contributed by Thierry Arnoux, 20-Jan-2025)

Ref Expression
Hypotheses ply1ascl0.w ⊢ 𝑊 = ( Poly1 ‘ 𝑅 )
ply1ascl0.a ⊢ 𝐴 = ( algSc ‘ 𝑊 )
ply1ascl0.o ⊢ 𝑂 = ( 0g ‘ 𝑅 )
ply1ascl0.1 ⊢ 0 = ( 0g ‘ 𝑊 )
ply1ascl0.r ⊢ ( 𝜑 → 𝑅 ∈ Ring )
Assertion ply1ascl0 ( 𝜑 → ( 𝐴 ‘ 𝑂 ) = 0 )

Proof

Step Hyp Ref Expression
1 ply1ascl0.w ⊢ 𝑊 = ( Poly1 ‘ 𝑅 )
2 ply1ascl0.a ⊢ 𝐴 = ( algSc ‘ 𝑊 )
3 ply1ascl0.o ⊢ 𝑂 = ( 0g ‘ 𝑅 )
4 ply1ascl0.1 ⊢ 0 = ( 0g ‘ 𝑊 )
5 ply1ascl0.r ⊢ ( 𝜑 → 𝑅 ∈ Ring )
6 1 ply1sca ⊢ ( 𝑅 ∈ Ring → 𝑅 = ( Scalar ‘ 𝑊 ) )
7 5 6 syl ⊢ ( 𝜑 → 𝑅 = ( Scalar ‘ 𝑊 ) )
8 7 fveq2d ⊢ ( 𝜑 → ( 0g ‘ 𝑅 ) = ( 0g ‘ ( Scalar ‘ 𝑊 ) ) )
9 3 8 eqtrid ⊢ ( 𝜑 → 𝑂 = ( 0g ‘ ( Scalar ‘ 𝑊 ) ) )
10 9 fveq2d ⊢ ( 𝜑 → ( ( algSc ‘ 𝑊 ) ‘ 𝑂 ) = ( ( algSc ‘ 𝑊 ) ‘ ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ) )
11 eqid ⊢ ( algSc ‘ 𝑊 ) = ( algSc ‘ 𝑊 )
12 eqid ⊢ ( Scalar ‘ 𝑊 ) = ( Scalar ‘ 𝑊 )
13 1 ply1lmod ⊢ ( 𝑅 ∈ Ring → 𝑊 ∈ LMod )
14 5 13 syl ⊢ ( 𝜑 → 𝑊 ∈ LMod )
15 1 ply1ring ⊢ ( 𝑅 ∈ Ring → 𝑊 ∈ Ring )
16 5 15 syl ⊢ ( 𝜑 → 𝑊 ∈ Ring )
17 11 12 14 16 ascl0 ⊢ ( 𝜑 → ( ( algSc ‘ 𝑊 ) ‘ ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ) = ( 0g ‘ 𝑊 ) )
18 10 17 eqtrd ⊢ ( 𝜑 → ( ( algSc ‘ 𝑊 ) ‘ 𝑂 ) = ( 0g ‘ 𝑊 ) )
19 2 fveq1i ⊢ ( 𝐴 ‘ 𝑂 ) = ( ( algSc ‘ 𝑊 ) ‘ 𝑂 )
20 18 19 4 3eqtr4g ⊢ ( 𝜑 → ( 𝐴 ‘ 𝑂 ) = 0 )