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

Metamath Proof Explorer

Theorem ply1scleq

Description: Equality of a constant polynomial is the same as equality of the constant term. (Contributed by Thierry Arnoux, 24-Jul-2024)

Ref Expression
Hypotheses ply1scleq.p ⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
ply1scleq.b ⊢ 𝐵 = ( Base ‘ 𝑅 )
ply1scleq.a ⊢ 𝐴 = ( algSc ‘ 𝑃 )
ply1scleq.r ⊢ ( 𝜑 → 𝑅 ∈ Ring )
ply1scleq.e ⊢ ( 𝜑 → 𝐸 ∈ 𝐵 )
ply1scleq.f ⊢ ( 𝜑 → 𝐹 ∈ 𝐵 )
Assertion ply1scleq ( 𝜑 → ( ( 𝐴 ‘ 𝐸 ) = ( 𝐴 ‘ 𝐹 ) ↔ 𝐸 = 𝐹 ) )

Proof

Step Hyp Ref Expression
1 ply1scleq.p ⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
2 ply1scleq.b ⊢ 𝐵 = ( Base ‘ 𝑅 )
3 ply1scleq.a ⊢ 𝐴 = ( algSc ‘ 𝑃 )
4 ply1scleq.r ⊢ ( 𝜑 → 𝑅 ∈ Ring )
5 ply1scleq.e ⊢ ( 𝜑 → 𝐸 ∈ 𝐵 )
6 ply1scleq.f ⊢ ( 𝜑 → 𝐹 ∈ 𝐵 )
7 fveq2 ⊢ ( 𝑑 = 0 → ( ( coe1 ‘ ( 𝐴 ‘ 𝐸 ) ) ‘ 𝑑 ) = ( ( coe1 ‘ ( 𝐴 ‘ 𝐸 ) ) ‘ 0 ) )
8 fveq2 ⊢ ( 𝑑 = 0 → ( ( coe1 ‘ ( 𝐴 ‘ 𝐹 ) ) ‘ 𝑑 ) = ( ( coe1 ‘ ( 𝐴 ‘ 𝐹 ) ) ‘ 0 ) )
9 7 8 eqeq12d ⊢ ( 𝑑 = 0 → ( ( ( coe1 ‘ ( 𝐴 ‘ 𝐸 ) ) ‘ 𝑑 ) = ( ( coe1 ‘ ( 𝐴 ‘ 𝐹 ) ) ‘ 𝑑 ) ↔ ( ( coe1 ‘ ( 𝐴 ‘ 𝐸 ) ) ‘ 0 ) = ( ( coe1 ‘ ( 𝐴 ‘ 𝐹 ) ) ‘ 0 ) ) )
10 eqid ⊢ ( Base ‘ 𝑃 ) = ( Base ‘ 𝑃 )
11 1 3 2 10 ply1sclcl ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐸 ∈ 𝐵 ) → ( 𝐴 ‘ 𝐸 ) ∈ ( Base ‘ 𝑃 ) )
12 4 5 11 syl2anc ⊢ ( 𝜑 → ( 𝐴 ‘ 𝐸 ) ∈ ( Base ‘ 𝑃 ) )
13 1 3 2 10 ply1sclcl ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ) → ( 𝐴 ‘ 𝐹 ) ∈ ( Base ‘ 𝑃 ) )
14 4 6 13 syl2anc ⊢ ( 𝜑 → ( 𝐴 ‘ 𝐹 ) ∈ ( Base ‘ 𝑃 ) )
15 eqid ⊢ ( coe1 ‘ ( 𝐴 ‘ 𝐸 ) ) = ( coe1 ‘ ( 𝐴 ‘ 𝐸 ) )
16 eqid ⊢ ( coe1 ‘ ( 𝐴 ‘ 𝐹 ) ) = ( coe1 ‘ ( 𝐴 ‘ 𝐹 ) )
17 1 10 15 16 ply1coe1eq ⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝐴 ‘ 𝐸 ) ∈ ( Base ‘ 𝑃 ) ∧ ( 𝐴 ‘ 𝐹 ) ∈ ( Base ‘ 𝑃 ) ) → ( ∀ 𝑑 ∈ ℕ0 ( ( coe1 ‘ ( 𝐴 ‘ 𝐸 ) ) ‘ 𝑑 ) = ( ( coe1 ‘ ( 𝐴 ‘ 𝐹 ) ) ‘ 𝑑 ) ↔ ( 𝐴 ‘ 𝐸 ) = ( 𝐴 ‘ 𝐹 ) ) )
18 4 12 14 17 syl3anc ⊢ ( 𝜑 → ( ∀ 𝑑 ∈ ℕ0 ( ( coe1 ‘ ( 𝐴 ‘ 𝐸 ) ) ‘ 𝑑 ) = ( ( coe1 ‘ ( 𝐴 ‘ 𝐹 ) ) ‘ 𝑑 ) ↔ ( 𝐴 ‘ 𝐸 ) = ( 𝐴 ‘ 𝐹 ) ) )
19 18 biimpar ⊢ ( ( 𝜑 ∧ ( 𝐴 ‘ 𝐸 ) = ( 𝐴 ‘ 𝐹 ) ) → ∀ 𝑑 ∈ ℕ0 ( ( coe1 ‘ ( 𝐴 ‘ 𝐸 ) ) ‘ 𝑑 ) = ( ( coe1 ‘ ( 𝐴 ‘ 𝐹 ) ) ‘ 𝑑 ) )
20 0nn0 ⊢ 0 ∈ ℕ0
21 20 a1i ⊢ ( ( 𝜑 ∧ ( 𝐴 ‘ 𝐸 ) = ( 𝐴 ‘ 𝐹 ) ) → 0 ∈ ℕ0 )
22 9 19 21 rspcdva ⊢ ( ( 𝜑 ∧ ( 𝐴 ‘ 𝐸 ) = ( 𝐴 ‘ 𝐹 ) ) → ( ( coe1 ‘ ( 𝐴 ‘ 𝐸 ) ) ‘ 0 ) = ( ( coe1 ‘ ( 𝐴 ‘ 𝐹 ) ) ‘ 0 ) )
23 1 3 2 ply1sclid ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐸 ∈ 𝐵 ) → 𝐸 = ( ( coe1 ‘ ( 𝐴 ‘ 𝐸 ) ) ‘ 0 ) )
24 4 5 23 syl2anc ⊢ ( 𝜑 → 𝐸 = ( ( coe1 ‘ ( 𝐴 ‘ 𝐸 ) ) ‘ 0 ) )
25 24 adantr ⊢ ( ( 𝜑 ∧ ( 𝐴 ‘ 𝐸 ) = ( 𝐴 ‘ 𝐹 ) ) → 𝐸 = ( ( coe1 ‘ ( 𝐴 ‘ 𝐸 ) ) ‘ 0 ) )
26 1 3 2 ply1sclid ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ) → 𝐹 = ( ( coe1 ‘ ( 𝐴 ‘ 𝐹 ) ) ‘ 0 ) )
27 4 6 26 syl2anc ⊢ ( 𝜑 → 𝐹 = ( ( coe1 ‘ ( 𝐴 ‘ 𝐹 ) ) ‘ 0 ) )
28 27 adantr ⊢ ( ( 𝜑 ∧ ( 𝐴 ‘ 𝐸 ) = ( 𝐴 ‘ 𝐹 ) ) → 𝐹 = ( ( coe1 ‘ ( 𝐴 ‘ 𝐹 ) ) ‘ 0 ) )
29 22 25 28 3eqtr4d ⊢ ( ( 𝜑 ∧ ( 𝐴 ‘ 𝐸 ) = ( 𝐴 ‘ 𝐹 ) ) → 𝐸 = 𝐹 )
30 fveq2 ⊢ ( 𝐸 = 𝐹 → ( 𝐴 ‘ 𝐸 ) = ( 𝐴 ‘ 𝐹 ) )
31 30 adantl ⊢ ( ( 𝜑 ∧ 𝐸 = 𝐹 ) → ( 𝐴 ‘ 𝐸 ) = ( 𝐴 ‘ 𝐹 ) )
32 29 31 impbida ⊢ ( 𝜑 → ( ( 𝐴 ‘ 𝐸 ) = ( 𝐴 ‘ 𝐹 ) ↔ 𝐸 = 𝐹 ) )