Metamath Proof Explorer


Theorem 0dgr

Description: A constant function has degree 0. (Contributed by Mario Carneiro, 24-Jul-2014)

Ref Expression
Assertion 0dgr ( 𝐴 ∈ ℂ → ( deg ‘ ( ℂ × { 𝐴 } ) ) = 0 )

Proof

Step Hyp Ref Expression
1 ssid ℂ ⊆ ℂ
2 plyconst ( ( ℂ ⊆ ℂ ∧ 𝐴 ∈ ℂ ) → ( ℂ × { 𝐴 } ) ∈ ( Poly ‘ ℂ ) )
3 1 2 mpan ( 𝐴 ∈ ℂ → ( ℂ × { 𝐴 } ) ∈ ( Poly ‘ ℂ ) )
4 0nn0 0 ∈ ℕ0
5 4 a1i ( 𝐴 ∈ ℂ → 0 ∈ ℕ0 )
6 simpl ( ( 𝐴 ∈ ℂ ∧ 𝑘 ∈ ( 0 ... 0 ) ) → 𝐴 ∈ ℂ )
7 fconstmpt ( ℂ × { 𝐴 } ) = ( 𝑧 ∈ ℂ ↦ 𝐴 )
8 0z 0 ∈ ℤ
9 exp0 ( 𝑧 ∈ ℂ → ( 𝑧 ↑ 0 ) = 1 )
10 9 oveq2d ( 𝑧 ∈ ℂ → ( 𝐴 · ( 𝑧 ↑ 0 ) ) = ( 𝐴 · 1 ) )
11 mulid1 ( 𝐴 ∈ ℂ → ( 𝐴 · 1 ) = 𝐴 )
12 10 11 sylan9eqr ( ( 𝐴 ∈ ℂ ∧ 𝑧 ∈ ℂ ) → ( 𝐴 · ( 𝑧 ↑ 0 ) ) = 𝐴 )
13 simpl ( ( 𝐴 ∈ ℂ ∧ 𝑧 ∈ ℂ ) → 𝐴 ∈ ℂ )
14 12 13 eqeltrd ( ( 𝐴 ∈ ℂ ∧ 𝑧 ∈ ℂ ) → ( 𝐴 · ( 𝑧 ↑ 0 ) ) ∈ ℂ )
15 oveq2 ( 𝑘 = 0 → ( 𝑧𝑘 ) = ( 𝑧 ↑ 0 ) )
16 15 oveq2d ( 𝑘 = 0 → ( 𝐴 · ( 𝑧𝑘 ) ) = ( 𝐴 · ( 𝑧 ↑ 0 ) ) )
17 16 fsum1 ( ( 0 ∈ ℤ ∧ ( 𝐴 · ( 𝑧 ↑ 0 ) ) ∈ ℂ ) → Σ 𝑘 ∈ ( 0 ... 0 ) ( 𝐴 · ( 𝑧𝑘 ) ) = ( 𝐴 · ( 𝑧 ↑ 0 ) ) )
18 8 14 17 sylancr ( ( 𝐴 ∈ ℂ ∧ 𝑧 ∈ ℂ ) → Σ 𝑘 ∈ ( 0 ... 0 ) ( 𝐴 · ( 𝑧𝑘 ) ) = ( 𝐴 · ( 𝑧 ↑ 0 ) ) )
19 18 12 eqtrd ( ( 𝐴 ∈ ℂ ∧ 𝑧 ∈ ℂ ) → Σ 𝑘 ∈ ( 0 ... 0 ) ( 𝐴 · ( 𝑧𝑘 ) ) = 𝐴 )
20 19 mpteq2dva ( 𝐴 ∈ ℂ → ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 0 ) ( 𝐴 · ( 𝑧𝑘 ) ) ) = ( 𝑧 ∈ ℂ ↦ 𝐴 ) )
21 7 20 eqtr4id ( 𝐴 ∈ ℂ → ( ℂ × { 𝐴 } ) = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 0 ) ( 𝐴 · ( 𝑧𝑘 ) ) ) )
22 3 5 6 21 dgrle ( 𝐴 ∈ ℂ → ( deg ‘ ( ℂ × { 𝐴 } ) ) ≤ 0 )
23 dgrcl ( ( ℂ × { 𝐴 } ) ∈ ( Poly ‘ ℂ ) → ( deg ‘ ( ℂ × { 𝐴 } ) ) ∈ ℕ0 )
24 nn0le0eq0 ( ( deg ‘ ( ℂ × { 𝐴 } ) ) ∈ ℕ0 → ( ( deg ‘ ( ℂ × { 𝐴 } ) ) ≤ 0 ↔ ( deg ‘ ( ℂ × { 𝐴 } ) ) = 0 ) )
25 3 23 24 3syl ( 𝐴 ∈ ℂ → ( ( deg ‘ ( ℂ × { 𝐴 } ) ) ≤ 0 ↔ ( deg ‘ ( ℂ × { 𝐴 } ) ) = 0 ) )
26 22 25 mpbid ( 𝐴 ∈ ℂ → ( deg ‘ ( ℂ × { 𝐴 } ) ) = 0 )