Theorem dgrmulc

Description: Scalar multiplication by a nonzero constant does not change the degree of a function. (Contributed by Mario Carneiro, 24-Jul-2014)

	Ref	Expression
Assertion	dgrmulc	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐹 ∈ ( Poly ‘ 𝑆 ) ) → ( deg ‘ ( ( ℂ × { 𝐴 } ) ∘f · 𝐹 ) ) = ( deg ‘ 𝐹 ) )

Proof

Step	Hyp	Ref	Expression
1		oveq2	⊢ ( 𝐹 = 0𝑝 → ( ( ℂ × { 𝐴 } ) ∘f · 𝐹 ) = ( ( ℂ × { 𝐴 } ) ∘f · 0𝑝 ) )
2	1	fveq2d	⊢ ( 𝐹 = 0𝑝 → ( deg ‘ ( ( ℂ × { 𝐴 } ) ∘f · 𝐹 ) ) = ( deg ‘ ( ( ℂ × { 𝐴 } ) ∘f · 0𝑝 ) ) )
3		fveq2	⊢ ( 𝐹 = 0𝑝 → ( deg ‘ 𝐹 ) = ( deg ‘ 0𝑝 ) )
4		dgr0	⊢ ( deg ‘ 0𝑝 ) = 0
5	3 4	eqtrdi	⊢ ( 𝐹 = 0𝑝 → ( deg ‘ 𝐹 ) = 0 )
6	2 5	eqeq12d	⊢ ( 𝐹 = 0𝑝 → ( ( deg ‘ ( ( ℂ × { 𝐴 } ) ∘f · 𝐹 ) ) = ( deg ‘ 𝐹 ) ↔ ( deg ‘ ( ( ℂ × { 𝐴 } ) ∘f · 0𝑝 ) ) = 0 ) )
7		ssid	⊢ ℂ ⊆ ℂ
8		simpl1	⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐹 ∈ ( Poly ‘ 𝑆 ) ) ∧ 𝐹 ≠ 0𝑝 ) → 𝐴 ∈ ℂ )
9		plyconst	⊢ ( ( ℂ ⊆ ℂ ∧ 𝐴 ∈ ℂ ) → ( ℂ × { 𝐴 } ) ∈ ( Poly ‘ ℂ ) )
10	7 8 9	sylancr	⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐹 ∈ ( Poly ‘ 𝑆 ) ) ∧ 𝐹 ≠ 0𝑝 ) → ( ℂ × { 𝐴 } ) ∈ ( Poly ‘ ℂ ) )
11		0cn	⊢ 0 ∈ ℂ
12		fvconst2g	⊢ ( ( 𝐴 ∈ ℂ ∧ 0 ∈ ℂ ) → ( ( ℂ × { 𝐴 } ) ‘ 0 ) = 𝐴 )
13	8 11 12	sylancl	⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐹 ∈ ( Poly ‘ 𝑆 ) ) ∧ 𝐹 ≠ 0𝑝 ) → ( ( ℂ × { 𝐴 } ) ‘ 0 ) = 𝐴 )
14		simpl2	⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐹 ∈ ( Poly ‘ 𝑆 ) ) ∧ 𝐹 ≠ 0𝑝 ) → 𝐴 ≠ 0 )
15	13 14	eqnetrd	⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐹 ∈ ( Poly ‘ 𝑆 ) ) ∧ 𝐹 ≠ 0𝑝 ) → ( ( ℂ × { 𝐴 } ) ‘ 0 ) ≠ 0 )
16		ne0p	⊢ ( ( 0 ∈ ℂ ∧ ( ( ℂ × { 𝐴 } ) ‘ 0 ) ≠ 0 ) → ( ℂ × { 𝐴 } ) ≠ 0𝑝 )
17	11 15 16	sylancr	⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐹 ∈ ( Poly ‘ 𝑆 ) ) ∧ 𝐹 ≠ 0𝑝 ) → ( ℂ × { 𝐴 } ) ≠ 0𝑝 )
18		plyssc	⊢ ( Poly ‘ 𝑆 ) ⊆ ( Poly ‘ ℂ )
19		simpl3	⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐹 ∈ ( Poly ‘ 𝑆 ) ) ∧ 𝐹 ≠ 0𝑝 ) → 𝐹 ∈ ( Poly ‘ 𝑆 ) )
20	18 19	sselid	⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐹 ∈ ( Poly ‘ 𝑆 ) ) ∧ 𝐹 ≠ 0𝑝 ) → 𝐹 ∈ ( Poly ‘ ℂ ) )
21		simpr	⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐹 ∈ ( Poly ‘ 𝑆 ) ) ∧ 𝐹 ≠ 0𝑝 ) → 𝐹 ≠ 0𝑝 )
22		eqid	⊢ ( deg ‘ ( ℂ × { 𝐴 } ) ) = ( deg ‘ ( ℂ × { 𝐴 } ) )
23		eqid	⊢ ( deg ‘ 𝐹 ) = ( deg ‘ 𝐹 )
24	22 23	dgrmul	⊢ ( ( ( ( ℂ × { 𝐴 } ) ∈ ( Poly ‘ ℂ ) ∧ ( ℂ × { 𝐴 } ) ≠ 0𝑝 ) ∧ ( 𝐹 ∈ ( Poly ‘ ℂ ) ∧ 𝐹 ≠ 0𝑝 ) ) → ( deg ‘ ( ( ℂ × { 𝐴 } ) ∘f · 𝐹 ) ) = ( ( deg ‘ ( ℂ × { 𝐴 } ) ) + ( deg ‘ 𝐹 ) ) )
25	10 17 20 21 24	syl22anc	⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐹 ∈ ( Poly ‘ 𝑆 ) ) ∧ 𝐹 ≠ 0𝑝 ) → ( deg ‘ ( ( ℂ × { 𝐴 } ) ∘f · 𝐹 ) ) = ( ( deg ‘ ( ℂ × { 𝐴 } ) ) + ( deg ‘ 𝐹 ) ) )
26		0dgr	⊢ ( 𝐴 ∈ ℂ → ( deg ‘ ( ℂ × { 𝐴 } ) ) = 0 )
27	8 26	syl	⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐹 ∈ ( Poly ‘ 𝑆 ) ) ∧ 𝐹 ≠ 0𝑝 ) → ( deg ‘ ( ℂ × { 𝐴 } ) ) = 0 )
28	27	oveq1d	⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐹 ∈ ( Poly ‘ 𝑆 ) ) ∧ 𝐹 ≠ 0𝑝 ) → ( ( deg ‘ ( ℂ × { 𝐴 } ) ) + ( deg ‘ 𝐹 ) ) = ( 0 + ( deg ‘ 𝐹 ) ) )
29		dgrcl	⊢ ( 𝐹 ∈ ( Poly ‘ 𝑆 ) → ( deg ‘ 𝐹 ) ∈ ℕ0 )
30	19 29	syl	⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐹 ∈ ( Poly ‘ 𝑆 ) ) ∧ 𝐹 ≠ 0𝑝 ) → ( deg ‘ 𝐹 ) ∈ ℕ0 )
31	30	nn0cnd	⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐹 ∈ ( Poly ‘ 𝑆 ) ) ∧ 𝐹 ≠ 0𝑝 ) → ( deg ‘ 𝐹 ) ∈ ℂ )
32	31	addlidd	⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐹 ∈ ( Poly ‘ 𝑆 ) ) ∧ 𝐹 ≠ 0𝑝 ) → ( 0 + ( deg ‘ 𝐹 ) ) = ( deg ‘ 𝐹 ) )
33	25 28 32	3eqtrd	⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐹 ∈ ( Poly ‘ 𝑆 ) ) ∧ 𝐹 ≠ 0𝑝 ) → ( deg ‘ ( ( ℂ × { 𝐴 } ) ∘f · 𝐹 ) ) = ( deg ‘ 𝐹 ) )
34		cnex	⊢ ℂ ∈ V
35	34	a1i	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐹 ∈ ( Poly ‘ 𝑆 ) ) → ℂ ∈ V )
36		simp1	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐹 ∈ ( Poly ‘ 𝑆 ) ) → 𝐴 ∈ ℂ )
37	11	a1i	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐹 ∈ ( Poly ‘ 𝑆 ) ) → 0 ∈ ℂ )
38	35 36 37	ofc12	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐹 ∈ ( Poly ‘ 𝑆 ) ) → ( ( ℂ × { 𝐴 } ) ∘f · ( ℂ × { 0 } ) ) = ( ℂ × { ( 𝐴 · 0 ) } ) )
39	36	mul01d	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐹 ∈ ( Poly ‘ 𝑆 ) ) → ( 𝐴 · 0 ) = 0 )
40	39	sneqd	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐹 ∈ ( Poly ‘ 𝑆 ) ) → { ( 𝐴 · 0 ) } = { 0 } )
41	40	xpeq2d	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐹 ∈ ( Poly ‘ 𝑆 ) ) → ( ℂ × { ( 𝐴 · 0 ) } ) = ( ℂ × { 0 } ) )
42	38 41	eqtrd	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐹 ∈ ( Poly ‘ 𝑆 ) ) → ( ( ℂ × { 𝐴 } ) ∘f · ( ℂ × { 0 } ) ) = ( ℂ × { 0 } ) )
43		df-0p	⊢ 0𝑝 = ( ℂ × { 0 } )
44	43	oveq2i	⊢ ( ( ℂ × { 𝐴 } ) ∘f · 0𝑝 ) = ( ( ℂ × { 𝐴 } ) ∘f · ( ℂ × { 0 } ) )
45	42 44 43	3eqtr4g	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐹 ∈ ( Poly ‘ 𝑆 ) ) → ( ( ℂ × { 𝐴 } ) ∘f · 0𝑝 ) = 0𝑝 )
46	45	fveq2d	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐹 ∈ ( Poly ‘ 𝑆 ) ) → ( deg ‘ ( ( ℂ × { 𝐴 } ) ∘f · 0𝑝 ) ) = ( deg ‘ 0𝑝 ) )
47	46 4	eqtrdi	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐹 ∈ ( Poly ‘ 𝑆 ) ) → ( deg ‘ ( ( ℂ × { 𝐴 } ) ∘f · 0𝑝 ) ) = 0 )
48	6 33 47	pm2.61ne	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐹 ∈ ( Poly ‘ 𝑆 ) ) → ( deg ‘ ( ( ℂ × { 𝐴 } ) ∘f · 𝐹 ) ) = ( deg ‘ 𝐹 ) )