Step |
Hyp |
Ref |
Expression |
1 |
|
simpr |
⊢ ( ( ( 𝐴 ∈ ℂ ∧ ( 𝑃 ‘ 𝐴 ) = 0 ) ∧ 𝑃 = ( ℂ × { ( 𝑃 ‘ 0 ) } ) ) → 𝑃 = ( ℂ × { ( 𝑃 ‘ 0 ) } ) ) |
2 |
1
|
fveq1d |
⊢ ( ( ( 𝐴 ∈ ℂ ∧ ( 𝑃 ‘ 𝐴 ) = 0 ) ∧ 𝑃 = ( ℂ × { ( 𝑃 ‘ 0 ) } ) ) → ( 𝑃 ‘ 𝐴 ) = ( ( ℂ × { ( 𝑃 ‘ 0 ) } ) ‘ 𝐴 ) ) |
3 |
|
simplr |
⊢ ( ( ( 𝐴 ∈ ℂ ∧ ( 𝑃 ‘ 𝐴 ) = 0 ) ∧ 𝑃 = ( ℂ × { ( 𝑃 ‘ 0 ) } ) ) → ( 𝑃 ‘ 𝐴 ) = 0 ) |
4 |
|
fvex |
⊢ ( 𝑃 ‘ 0 ) ∈ V |
5 |
4
|
fvconst2 |
⊢ ( 𝐴 ∈ ℂ → ( ( ℂ × { ( 𝑃 ‘ 0 ) } ) ‘ 𝐴 ) = ( 𝑃 ‘ 0 ) ) |
6 |
5
|
ad2antrr |
⊢ ( ( ( 𝐴 ∈ ℂ ∧ ( 𝑃 ‘ 𝐴 ) = 0 ) ∧ 𝑃 = ( ℂ × { ( 𝑃 ‘ 0 ) } ) ) → ( ( ℂ × { ( 𝑃 ‘ 0 ) } ) ‘ 𝐴 ) = ( 𝑃 ‘ 0 ) ) |
7 |
2 3 6
|
3eqtr3rd |
⊢ ( ( ( 𝐴 ∈ ℂ ∧ ( 𝑃 ‘ 𝐴 ) = 0 ) ∧ 𝑃 = ( ℂ × { ( 𝑃 ‘ 0 ) } ) ) → ( 𝑃 ‘ 0 ) = 0 ) |
8 |
7
|
sneqd |
⊢ ( ( ( 𝐴 ∈ ℂ ∧ ( 𝑃 ‘ 𝐴 ) = 0 ) ∧ 𝑃 = ( ℂ × { ( 𝑃 ‘ 0 ) } ) ) → { ( 𝑃 ‘ 0 ) } = { 0 } ) |
9 |
8
|
xpeq2d |
⊢ ( ( ( 𝐴 ∈ ℂ ∧ ( 𝑃 ‘ 𝐴 ) = 0 ) ∧ 𝑃 = ( ℂ × { ( 𝑃 ‘ 0 ) } ) ) → ( ℂ × { ( 𝑃 ‘ 0 ) } ) = ( ℂ × { 0 } ) ) |
10 |
1 9
|
eqtrd |
⊢ ( ( ( 𝐴 ∈ ℂ ∧ ( 𝑃 ‘ 𝐴 ) = 0 ) ∧ 𝑃 = ( ℂ × { ( 𝑃 ‘ 0 ) } ) ) → 𝑃 = ( ℂ × { 0 } ) ) |
11 |
|
df-0p |
⊢ 0𝑝 = ( ℂ × { 0 } ) |
12 |
10 11
|
eqtr4di |
⊢ ( ( ( 𝐴 ∈ ℂ ∧ ( 𝑃 ‘ 𝐴 ) = 0 ) ∧ 𝑃 = ( ℂ × { ( 𝑃 ‘ 0 ) } ) ) → 𝑃 = 0𝑝 ) |
13 |
12
|
ex |
⊢ ( ( 𝐴 ∈ ℂ ∧ ( 𝑃 ‘ 𝐴 ) = 0 ) → ( 𝑃 = ( ℂ × { ( 𝑃 ‘ 0 ) } ) → 𝑃 = 0𝑝 ) ) |
14 |
13
|
necon3ad |
⊢ ( ( 𝐴 ∈ ℂ ∧ ( 𝑃 ‘ 𝐴 ) = 0 ) → ( 𝑃 ≠ 0𝑝 → ¬ 𝑃 = ( ℂ × { ( 𝑃 ‘ 0 ) } ) ) ) |
15 |
14
|
impcom |
⊢ ( ( 𝑃 ≠ 0𝑝 ∧ ( 𝐴 ∈ ℂ ∧ ( 𝑃 ‘ 𝐴 ) = 0 ) ) → ¬ 𝑃 = ( ℂ × { ( 𝑃 ‘ 0 ) } ) ) |
16 |
15
|
adantll |
⊢ ( ( ( 𝑃 ∈ ( Poly ‘ 𝑆 ) ∧ 𝑃 ≠ 0𝑝 ) ∧ ( 𝐴 ∈ ℂ ∧ ( 𝑃 ‘ 𝐴 ) = 0 ) ) → ¬ 𝑃 = ( ℂ × { ( 𝑃 ‘ 0 ) } ) ) |
17 |
|
0dgrb |
⊢ ( 𝑃 ∈ ( Poly ‘ 𝑆 ) → ( ( deg ‘ 𝑃 ) = 0 ↔ 𝑃 = ( ℂ × { ( 𝑃 ‘ 0 ) } ) ) ) |
18 |
17
|
ad2antrr |
⊢ ( ( ( 𝑃 ∈ ( Poly ‘ 𝑆 ) ∧ 𝑃 ≠ 0𝑝 ) ∧ ( 𝐴 ∈ ℂ ∧ ( 𝑃 ‘ 𝐴 ) = 0 ) ) → ( ( deg ‘ 𝑃 ) = 0 ↔ 𝑃 = ( ℂ × { ( 𝑃 ‘ 0 ) } ) ) ) |
19 |
16 18
|
mtbird |
⊢ ( ( ( 𝑃 ∈ ( Poly ‘ 𝑆 ) ∧ 𝑃 ≠ 0𝑝 ) ∧ ( 𝐴 ∈ ℂ ∧ ( 𝑃 ‘ 𝐴 ) = 0 ) ) → ¬ ( deg ‘ 𝑃 ) = 0 ) |
20 |
|
dgrcl |
⊢ ( 𝑃 ∈ ( Poly ‘ 𝑆 ) → ( deg ‘ 𝑃 ) ∈ ℕ0 ) |
21 |
20
|
ad2antrr |
⊢ ( ( ( 𝑃 ∈ ( Poly ‘ 𝑆 ) ∧ 𝑃 ≠ 0𝑝 ) ∧ ( 𝐴 ∈ ℂ ∧ ( 𝑃 ‘ 𝐴 ) = 0 ) ) → ( deg ‘ 𝑃 ) ∈ ℕ0 ) |
22 |
|
elnn0 |
⊢ ( ( deg ‘ 𝑃 ) ∈ ℕ0 ↔ ( ( deg ‘ 𝑃 ) ∈ ℕ ∨ ( deg ‘ 𝑃 ) = 0 ) ) |
23 |
21 22
|
sylib |
⊢ ( ( ( 𝑃 ∈ ( Poly ‘ 𝑆 ) ∧ 𝑃 ≠ 0𝑝 ) ∧ ( 𝐴 ∈ ℂ ∧ ( 𝑃 ‘ 𝐴 ) = 0 ) ) → ( ( deg ‘ 𝑃 ) ∈ ℕ ∨ ( deg ‘ 𝑃 ) = 0 ) ) |
24 |
|
orel2 |
⊢ ( ¬ ( deg ‘ 𝑃 ) = 0 → ( ( ( deg ‘ 𝑃 ) ∈ ℕ ∨ ( deg ‘ 𝑃 ) = 0 ) → ( deg ‘ 𝑃 ) ∈ ℕ ) ) |
25 |
19 23 24
|
sylc |
⊢ ( ( ( 𝑃 ∈ ( Poly ‘ 𝑆 ) ∧ 𝑃 ≠ 0𝑝 ) ∧ ( 𝐴 ∈ ℂ ∧ ( 𝑃 ‘ 𝐴 ) = 0 ) ) → ( deg ‘ 𝑃 ) ∈ ℕ ) |