Metamath Proof Explorer

Theorem plyremlem

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

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

Proof

Step Hyp Ref Expression
1 plyrem.1 ⊢ 𝐺 = ( Xp ∘f − ( ℂ × { 𝐴 } ) )
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 ‘ ℂ ) ) → ( Xp ∘f − ( ℂ × { 𝐴 } ) ) ∈ ( Poly ‘ ℂ ) )
9 5 7 8 sylancr ⊢ ( 𝐴 ∈ ℂ → ( Xp ∘f − ( ℂ × { 𝐴 } ) ) ∈ ( 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 ⊢ ( 𝐴 ∈ ℂ → ( Xp ∘f − ( ℂ × { 𝐴 } ) ) = ( 𝑧 ∈ ℂ ↦ ( 𝑧 − 𝐴 ) ) )
34 17 29 33 3eqtr4d ⊢ ( 𝐴 ∈ ℂ → ( ( ℂ × { - 𝐴 } ) ∘f + Xp ) = ( Xp ∘f − ( ℂ × { 𝐴 } ) ) )
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 syl6bbr ⊢ ( 𝐴 ∈ ℂ → ( 𝑧 ∈ ( ◡ 𝐺 “ { 0 } ) ↔ 𝑧 ∈ { 𝐴 } ) )
72 71 eqrdv ⊢ ( 𝐴 ∈ ℂ → ( ◡ 𝐺 “ { 0 } ) = { 𝐴 } )
73 10 49 72 3jca ⊢ ( 𝐴 ∈ ℂ → ( 𝐺 ∈ ( Poly ‘ ℂ ) ∧ ( deg ‘ 𝐺 ) = 1 ∧ ( ◡ 𝐺 “ { 0 } ) = { 𝐴 } ) )