Metamath Proof Explorer


Theorem plyremlem

Description: Closure of a linear factor. (Contributed by Mario Carneiro, 26-Jul-2014)

Ref Expression
Hypothesis plyrem.1 𝐺 = ( Xpf − ( ℂ × { 𝐴 } ) )
Assertion plyremlem ( 𝐴 ∈ ℂ → ( 𝐺 ∈ ( Poly ‘ ℂ ) ∧ ( deg ‘ 𝐺 ) = 1 ∧ ( 𝐺 “ { 0 } ) = { 𝐴 } ) )

Proof

Step Hyp Ref Expression
1 plyrem.1 𝐺 = ( Xpf − ( ℂ × { 𝐴 } ) )
2 ssid ℂ ⊆ ℂ
3 ax-1cn 1 ∈ ℂ
4 plyid ( ( ℂ ⊆ ℂ ∧ 1 ∈ ℂ ) → Xp ∈ ( Poly ‘ ℂ ) )
5 2 3 4 mp2an Xp ∈ ( Poly ‘ ℂ )
6 plyconst ( ( ℂ ⊆ ℂ ∧ 𝐴 ∈ ℂ ) → ( ℂ × { 𝐴 } ) ∈ ( Poly ‘ ℂ ) )
7 2 6 mpan ( 𝐴 ∈ ℂ → ( ℂ × { 𝐴 } ) ∈ ( Poly ‘ ℂ ) )
8 plysubcl ( ( Xp ∈ ( Poly ‘ ℂ ) ∧ ( ℂ × { 𝐴 } ) ∈ ( Poly ‘ ℂ ) ) → ( Xpf − ( ℂ × { 𝐴 } ) ) ∈ ( Poly ‘ ℂ ) )
9 5 7 8 sylancr ( 𝐴 ∈ ℂ → ( Xpf − ( ℂ × { 𝐴 } ) ) ∈ ( Poly ‘ ℂ ) )
10 1 9 eqeltrid ( 𝐴 ∈ ℂ → 𝐺 ∈ ( Poly ‘ ℂ ) )
11 negcl ( 𝐴 ∈ ℂ → - 𝐴 ∈ ℂ )
12 addcom ( ( - 𝐴 ∈ ℂ ∧ 𝑧 ∈ ℂ ) → ( - 𝐴 + 𝑧 ) = ( 𝑧 + - 𝐴 ) )
13 11 12 sylan ( ( 𝐴 ∈ ℂ ∧ 𝑧 ∈ ℂ ) → ( - 𝐴 + 𝑧 ) = ( 𝑧 + - 𝐴 ) )
14 negsub ( ( 𝑧 ∈ ℂ ∧ 𝐴 ∈ ℂ ) → ( 𝑧 + - 𝐴 ) = ( 𝑧𝐴 ) )
15 14 ancoms ( ( 𝐴 ∈ ℂ ∧ 𝑧 ∈ ℂ ) → ( 𝑧 + - 𝐴 ) = ( 𝑧𝐴 ) )
16 13 15 eqtrd ( ( 𝐴 ∈ ℂ ∧ 𝑧 ∈ ℂ ) → ( - 𝐴 + 𝑧 ) = ( 𝑧𝐴 ) )
17 16 mpteq2dva ( 𝐴 ∈ ℂ → ( 𝑧 ∈ ℂ ↦ ( - 𝐴 + 𝑧 ) ) = ( 𝑧 ∈ ℂ ↦ ( 𝑧𝐴 ) ) )
18 cnex ℂ ∈ V
19 18 a1i ( 𝐴 ∈ ℂ → ℂ ∈ V )
20 negex - 𝐴 ∈ V
21 20 a1i ( ( 𝐴 ∈ ℂ ∧ 𝑧 ∈ ℂ ) → - 𝐴 ∈ V )
22 simpr ( ( 𝐴 ∈ ℂ ∧ 𝑧 ∈ ℂ ) → 𝑧 ∈ ℂ )
23 fconstmpt ( ℂ × { - 𝐴 } ) = ( 𝑧 ∈ ℂ ↦ - 𝐴 )
24 23 a1i ( 𝐴 ∈ ℂ → ( ℂ × { - 𝐴 } ) = ( 𝑧 ∈ ℂ ↦ - 𝐴 ) )
25 df-idp Xp = ( I ↾ ℂ )
26 mptresid ( I ↾ ℂ ) = ( 𝑧 ∈ ℂ ↦ 𝑧 )
27 25 26 eqtri Xp = ( 𝑧 ∈ ℂ ↦ 𝑧 )
28 27 a1i ( 𝐴 ∈ ℂ → Xp = ( 𝑧 ∈ ℂ ↦ 𝑧 ) )
29 19 21 22 24 28 offval2 ( 𝐴 ∈ ℂ → ( ( ℂ × { - 𝐴 } ) ∘f + Xp ) = ( 𝑧 ∈ ℂ ↦ ( - 𝐴 + 𝑧 ) ) )
30 simpl ( ( 𝐴 ∈ ℂ ∧ 𝑧 ∈ ℂ ) → 𝐴 ∈ ℂ )
31 fconstmpt ( ℂ × { 𝐴 } ) = ( 𝑧 ∈ ℂ ↦ 𝐴 )
32 31 a1i ( 𝐴 ∈ ℂ → ( ℂ × { 𝐴 } ) = ( 𝑧 ∈ ℂ ↦ 𝐴 ) )
33 19 22 30 28 32 offval2 ( 𝐴 ∈ ℂ → ( Xpf − ( ℂ × { 𝐴 } ) ) = ( 𝑧 ∈ ℂ ↦ ( 𝑧𝐴 ) ) )
34 17 29 33 3eqtr4d ( 𝐴 ∈ ℂ → ( ( ℂ × { - 𝐴 } ) ∘f + Xp ) = ( Xpf − ( ℂ × { 𝐴 } ) ) )
35 34 1 eqtr4di ( 𝐴 ∈ ℂ → ( ( ℂ × { - 𝐴 } ) ∘f + Xp ) = 𝐺 )
36 35 fveq2d ( 𝐴 ∈ ℂ → ( deg ‘ ( ( ℂ × { - 𝐴 } ) ∘f + Xp ) ) = ( deg ‘ 𝐺 ) )
37 plyconst ( ( ℂ ⊆ ℂ ∧ - 𝐴 ∈ ℂ ) → ( ℂ × { - 𝐴 } ) ∈ ( Poly ‘ ℂ ) )
38 2 11 37 sylancr ( 𝐴 ∈ ℂ → ( ℂ × { - 𝐴 } ) ∈ ( Poly ‘ ℂ ) )
39 5 a1i ( 𝐴 ∈ ℂ → Xp ∈ ( Poly ‘ ℂ ) )
40 0dgr ( - 𝐴 ∈ ℂ → ( deg ‘ ( ℂ × { - 𝐴 } ) ) = 0 )
41 11 40 syl ( 𝐴 ∈ ℂ → ( deg ‘ ( ℂ × { - 𝐴 } ) ) = 0 )
42 0lt1 0 < 1
43 41 42 eqbrtrdi ( 𝐴 ∈ ℂ → ( deg ‘ ( ℂ × { - 𝐴 } ) ) < 1 )
44 eqid ( deg ‘ ( ℂ × { - 𝐴 } ) ) = ( deg ‘ ( ℂ × { - 𝐴 } ) )
45 dgrid ( deg ‘ Xp ) = 1
46 45 eqcomi 1 = ( deg ‘ Xp )
47 44 46 dgradd2 ( ( ( ℂ × { - 𝐴 } ) ∈ ( Poly ‘ ℂ ) ∧ Xp ∈ ( Poly ‘ ℂ ) ∧ ( deg ‘ ( ℂ × { - 𝐴 } ) ) < 1 ) → ( deg ‘ ( ( ℂ × { - 𝐴 } ) ∘f + Xp ) ) = 1 )
48 38 39 43 47 syl3anc ( 𝐴 ∈ ℂ → ( deg ‘ ( ( ℂ × { - 𝐴 } ) ∘f + Xp ) ) = 1 )
49 36 48 eqtr3d ( 𝐴 ∈ ℂ → ( deg ‘ 𝐺 ) = 1 )
50 1 33 syl5eq ( 𝐴 ∈ ℂ → 𝐺 = ( 𝑧 ∈ ℂ ↦ ( 𝑧𝐴 ) ) )
51 50 fveq1d ( 𝐴 ∈ ℂ → ( 𝐺𝑧 ) = ( ( 𝑧 ∈ ℂ ↦ ( 𝑧𝐴 ) ) ‘ 𝑧 ) )
52 51 adantr ( ( 𝐴 ∈ ℂ ∧ 𝑧 ∈ ℂ ) → ( 𝐺𝑧 ) = ( ( 𝑧 ∈ ℂ ↦ ( 𝑧𝐴 ) ) ‘ 𝑧 ) )
53 ovex ( 𝑧𝐴 ) ∈ V
54 eqid ( 𝑧 ∈ ℂ ↦ ( 𝑧𝐴 ) ) = ( 𝑧 ∈ ℂ ↦ ( 𝑧𝐴 ) )
55 54 fvmpt2 ( ( 𝑧 ∈ ℂ ∧ ( 𝑧𝐴 ) ∈ V ) → ( ( 𝑧 ∈ ℂ ↦ ( 𝑧𝐴 ) ) ‘ 𝑧 ) = ( 𝑧𝐴 ) )
56 22 53 55 sylancl ( ( 𝐴 ∈ ℂ ∧ 𝑧 ∈ ℂ ) → ( ( 𝑧 ∈ ℂ ↦ ( 𝑧𝐴 ) ) ‘ 𝑧 ) = ( 𝑧𝐴 ) )
57 52 56 eqtrd ( ( 𝐴 ∈ ℂ ∧ 𝑧 ∈ ℂ ) → ( 𝐺𝑧 ) = ( 𝑧𝐴 ) )
58 57 eqeq1d ( ( 𝐴 ∈ ℂ ∧ 𝑧 ∈ ℂ ) → ( ( 𝐺𝑧 ) = 0 ↔ ( 𝑧𝐴 ) = 0 ) )
59 subeq0 ( ( 𝑧 ∈ ℂ ∧ 𝐴 ∈ ℂ ) → ( ( 𝑧𝐴 ) = 0 ↔ 𝑧 = 𝐴 ) )
60 59 ancoms ( ( 𝐴 ∈ ℂ ∧ 𝑧 ∈ ℂ ) → ( ( 𝑧𝐴 ) = 0 ↔ 𝑧 = 𝐴 ) )
61 58 60 bitrd ( ( 𝐴 ∈ ℂ ∧ 𝑧 ∈ ℂ ) → ( ( 𝐺𝑧 ) = 0 ↔ 𝑧 = 𝐴 ) )
62 61 pm5.32da ( 𝐴 ∈ ℂ → ( ( 𝑧 ∈ ℂ ∧ ( 𝐺𝑧 ) = 0 ) ↔ ( 𝑧 ∈ ℂ ∧ 𝑧 = 𝐴 ) ) )
63 plyf ( 𝐺 ∈ ( Poly ‘ ℂ ) → 𝐺 : ℂ ⟶ ℂ )
64 ffn ( 𝐺 : ℂ ⟶ ℂ → 𝐺 Fn ℂ )
65 fniniseg ( 𝐺 Fn ℂ → ( 𝑧 ∈ ( 𝐺 “ { 0 } ) ↔ ( 𝑧 ∈ ℂ ∧ ( 𝐺𝑧 ) = 0 ) ) )
66 10 63 64 65 4syl ( 𝐴 ∈ ℂ → ( 𝑧 ∈ ( 𝐺 “ { 0 } ) ↔ ( 𝑧 ∈ ℂ ∧ ( 𝐺𝑧 ) = 0 ) ) )
67 eleq1a ( 𝐴 ∈ ℂ → ( 𝑧 = 𝐴𝑧 ∈ ℂ ) )
68 67 pm4.71rd ( 𝐴 ∈ ℂ → ( 𝑧 = 𝐴 ↔ ( 𝑧 ∈ ℂ ∧ 𝑧 = 𝐴 ) ) )
69 62 66 68 3bitr4d ( 𝐴 ∈ ℂ → ( 𝑧 ∈ ( 𝐺 “ { 0 } ) ↔ 𝑧 = 𝐴 ) )
70 velsn ( 𝑧 ∈ { 𝐴 } ↔ 𝑧 = 𝐴 )
71 69 70 bitr4di ( 𝐴 ∈ ℂ → ( 𝑧 ∈ ( 𝐺 “ { 0 } ) ↔ 𝑧 ∈ { 𝐴 } ) )
72 71 eqrdv ( 𝐴 ∈ ℂ → ( 𝐺 “ { 0 } ) = { 𝐴 } )
73 10 49 72 3jca ( 𝐴 ∈ ℂ → ( 𝐺 ∈ ( Poly ‘ ℂ ) ∧ ( deg ‘ 𝐺 ) = 1 ∧ ( 𝐺 “ { 0 } ) = { 𝐴 } ) )