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 ) )