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

Metamath Proof Explorer

Theorem ply1sclid

Description: Recover the base scalar from a scalar polynomial. (Contributed by Stefan O'Rear, 28-Mar-2015)

Ref Expression
Hypotheses ply1scl.p ⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
ply1scl.a ⊢ 𝐴 = ( algSc ‘ 𝑃 )
ply1sclid.k ⊢ 𝐾 = ( Base ‘ 𝑅 )
Assertion ply1sclid ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐾 ) → 𝑋 = ( ( coe1 ‘ ( 𝐴 ‘ 𝑋 ) ) ‘ 0 ) )

Proof

Step Hyp Ref Expression
1 ply1scl.p ⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
2 ply1scl.a ⊢ 𝐴 = ( algSc ‘ 𝑃 )
3 ply1sclid.k ⊢ 𝐾 = ( Base ‘ 𝑅 )
4 eqid ⊢ ( 0g ‘ 𝑅 ) = ( 0g ‘ 𝑅 )
5 1 2 3 4 coe1scl ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐾 ) → ( coe1 ‘ ( 𝐴 ‘ 𝑋 ) ) = ( 𝑥 ∈ ℕ0 ↦ if ( 𝑥 = 0 , 𝑋 , ( 0g ‘ 𝑅 ) ) ) )
6 5 fveq1d ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐾 ) → ( ( coe1 ‘ ( 𝐴 ‘ 𝑋 ) ) ‘ 0 ) = ( ( 𝑥 ∈ ℕ0 ↦ if ( 𝑥 = 0 , 𝑋 , ( 0g ‘ 𝑅 ) ) ) ‘ 0 ) )
7 0nn0 ⊢ 0 ∈ ℕ0
8 iftrue ⊢ ( 𝑥 = 0 → if ( 𝑥 = 0 , 𝑋 , ( 0g ‘ 𝑅 ) ) = 𝑋 )
9 eqid ⊢ ( 𝑥 ∈ ℕ0 ↦ if ( 𝑥 = 0 , 𝑋 , ( 0g ‘ 𝑅 ) ) ) = ( 𝑥 ∈ ℕ0 ↦ if ( 𝑥 = 0 , 𝑋 , ( 0g ‘ 𝑅 ) ) )
10 8 9 fvmptg ⊢ ( ( 0 ∈ ℕ0 ∧ 𝑋 ∈ 𝐾 ) → ( ( 𝑥 ∈ ℕ0 ↦ if ( 𝑥 = 0 , 𝑋 , ( 0g ‘ 𝑅 ) ) ) ‘ 0 ) = 𝑋 )
11 7 10 mpan ⊢ ( 𝑋 ∈ 𝐾 → ( ( 𝑥 ∈ ℕ0 ↦ if ( 𝑥 = 0 , 𝑋 , ( 0g ‘ 𝑅 ) ) ) ‘ 0 ) = 𝑋 )
12 11 adantl ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐾 ) → ( ( 𝑥 ∈ ℕ0 ↦ if ( 𝑥 = 0 , 𝑋 , ( 0g ‘ 𝑅 ) ) ) ‘ 0 ) = 𝑋 )
13 6 12 eqtr2d ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐾 ) → 𝑋 = ( ( coe1 ‘ ( 𝐴 ‘ 𝑋 ) ) ‘ 0 ) )