Step |
Hyp |
Ref |
Expression |
1 |
|
deg1z.d |
⊢ 𝐷 = ( deg1 ‘ 𝑅 ) |
2 |
|
deg1z.p |
⊢ 𝑃 = ( Poly1 ‘ 𝑅 ) |
3 |
|
deg1z.z |
⊢ 0 = ( 0g ‘ 𝑃 ) |
4 |
|
deg1nn0cl.b |
⊢ 𝐵 = ( Base ‘ 𝑃 ) |
5 |
|
deg1ldg.y |
⊢ 𝑌 = ( 0g ‘ 𝑅 ) |
6 |
|
deg1ldg.a |
⊢ 𝐴 = ( coe1 ‘ 𝐹 ) |
7 |
1
|
deg1fval |
⊢ 𝐷 = ( 1o mDeg 𝑅 ) |
8 |
|
eqid |
⊢ ( 1o mPoly 𝑅 ) = ( 1o mPoly 𝑅 ) |
9 |
|
eqid |
⊢ ( PwSer1 ‘ 𝑅 ) = ( PwSer1 ‘ 𝑅 ) |
10 |
2 9 4
|
ply1bas |
⊢ 𝐵 = ( Base ‘ ( 1o mPoly 𝑅 ) ) |
11 |
|
psr1baslem |
⊢ ( ℕ0 ↑m 1o ) = { 𝑐 ∈ ( ℕ0 ↑m 1o ) ∣ ( ◡ 𝑐 “ ℕ ) ∈ Fin } |
12 |
|
tdeglem2 |
⊢ ( 𝑎 ∈ ( ℕ0 ↑m 1o ) ↦ ( 𝑎 ‘ ∅ ) ) = ( 𝑎 ∈ ( ℕ0 ↑m 1o ) ↦ ( ℂfld Σg 𝑎 ) ) |
13 |
8 2 3
|
ply1mpl0 |
⊢ 0 = ( 0g ‘ ( 1o mPoly 𝑅 ) ) |
14 |
7 8 10 5 11 12 13
|
mdegldg |
⊢ ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐹 ≠ 0 ) → ∃ 𝑏 ∈ ( ℕ0 ↑m 1o ) ( ( 𝐹 ‘ 𝑏 ) ≠ 𝑌 ∧ ( ( 𝑎 ∈ ( ℕ0 ↑m 1o ) ↦ ( 𝑎 ‘ ∅ ) ) ‘ 𝑏 ) = ( 𝐷 ‘ 𝐹 ) ) ) |
15 |
6
|
fvcoe1 |
⊢ ( ( 𝐹 ∈ 𝐵 ∧ 𝑏 ∈ ( ℕ0 ↑m 1o ) ) → ( 𝐹 ‘ 𝑏 ) = ( 𝐴 ‘ ( 𝑏 ‘ ∅ ) ) ) |
16 |
15
|
3ad2antl2 |
⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐹 ≠ 0 ) ∧ 𝑏 ∈ ( ℕ0 ↑m 1o ) ) → ( 𝐹 ‘ 𝑏 ) = ( 𝐴 ‘ ( 𝑏 ‘ ∅ ) ) ) |
17 |
|
fveq1 |
⊢ ( 𝑎 = 𝑏 → ( 𝑎 ‘ ∅ ) = ( 𝑏 ‘ ∅ ) ) |
18 |
|
eqid |
⊢ ( 𝑎 ∈ ( ℕ0 ↑m 1o ) ↦ ( 𝑎 ‘ ∅ ) ) = ( 𝑎 ∈ ( ℕ0 ↑m 1o ) ↦ ( 𝑎 ‘ ∅ ) ) |
19 |
|
fvex |
⊢ ( 𝑏 ‘ ∅ ) ∈ V |
20 |
17 18 19
|
fvmpt |
⊢ ( 𝑏 ∈ ( ℕ0 ↑m 1o ) → ( ( 𝑎 ∈ ( ℕ0 ↑m 1o ) ↦ ( 𝑎 ‘ ∅ ) ) ‘ 𝑏 ) = ( 𝑏 ‘ ∅ ) ) |
21 |
20
|
fveq2d |
⊢ ( 𝑏 ∈ ( ℕ0 ↑m 1o ) → ( 𝐴 ‘ ( ( 𝑎 ∈ ( ℕ0 ↑m 1o ) ↦ ( 𝑎 ‘ ∅ ) ) ‘ 𝑏 ) ) = ( 𝐴 ‘ ( 𝑏 ‘ ∅ ) ) ) |
22 |
21
|
adantl |
⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐹 ≠ 0 ) ∧ 𝑏 ∈ ( ℕ0 ↑m 1o ) ) → ( 𝐴 ‘ ( ( 𝑎 ∈ ( ℕ0 ↑m 1o ) ↦ ( 𝑎 ‘ ∅ ) ) ‘ 𝑏 ) ) = ( 𝐴 ‘ ( 𝑏 ‘ ∅ ) ) ) |
23 |
16 22
|
eqtr4d |
⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐹 ≠ 0 ) ∧ 𝑏 ∈ ( ℕ0 ↑m 1o ) ) → ( 𝐹 ‘ 𝑏 ) = ( 𝐴 ‘ ( ( 𝑎 ∈ ( ℕ0 ↑m 1o ) ↦ ( 𝑎 ‘ ∅ ) ) ‘ 𝑏 ) ) ) |
24 |
23
|
neeq1d |
⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐹 ≠ 0 ) ∧ 𝑏 ∈ ( ℕ0 ↑m 1o ) ) → ( ( 𝐹 ‘ 𝑏 ) ≠ 𝑌 ↔ ( 𝐴 ‘ ( ( 𝑎 ∈ ( ℕ0 ↑m 1o ) ↦ ( 𝑎 ‘ ∅ ) ) ‘ 𝑏 ) ) ≠ 𝑌 ) ) |
25 |
24
|
anbi1d |
⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐹 ≠ 0 ) ∧ 𝑏 ∈ ( ℕ0 ↑m 1o ) ) → ( ( ( 𝐹 ‘ 𝑏 ) ≠ 𝑌 ∧ ( ( 𝑎 ∈ ( ℕ0 ↑m 1o ) ↦ ( 𝑎 ‘ ∅ ) ) ‘ 𝑏 ) = ( 𝐷 ‘ 𝐹 ) ) ↔ ( ( 𝐴 ‘ ( ( 𝑎 ∈ ( ℕ0 ↑m 1o ) ↦ ( 𝑎 ‘ ∅ ) ) ‘ 𝑏 ) ) ≠ 𝑌 ∧ ( ( 𝑎 ∈ ( ℕ0 ↑m 1o ) ↦ ( 𝑎 ‘ ∅ ) ) ‘ 𝑏 ) = ( 𝐷 ‘ 𝐹 ) ) ) ) |
26 |
25
|
biancomd |
⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐹 ≠ 0 ) ∧ 𝑏 ∈ ( ℕ0 ↑m 1o ) ) → ( ( ( 𝐹 ‘ 𝑏 ) ≠ 𝑌 ∧ ( ( 𝑎 ∈ ( ℕ0 ↑m 1o ) ↦ ( 𝑎 ‘ ∅ ) ) ‘ 𝑏 ) = ( 𝐷 ‘ 𝐹 ) ) ↔ ( ( ( 𝑎 ∈ ( ℕ0 ↑m 1o ) ↦ ( 𝑎 ‘ ∅ ) ) ‘ 𝑏 ) = ( 𝐷 ‘ 𝐹 ) ∧ ( 𝐴 ‘ ( ( 𝑎 ∈ ( ℕ0 ↑m 1o ) ↦ ( 𝑎 ‘ ∅ ) ) ‘ 𝑏 ) ) ≠ 𝑌 ) ) ) |
27 |
26
|
rexbidva |
⊢ ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐹 ≠ 0 ) → ( ∃ 𝑏 ∈ ( ℕ0 ↑m 1o ) ( ( 𝐹 ‘ 𝑏 ) ≠ 𝑌 ∧ ( ( 𝑎 ∈ ( ℕ0 ↑m 1o ) ↦ ( 𝑎 ‘ ∅ ) ) ‘ 𝑏 ) = ( 𝐷 ‘ 𝐹 ) ) ↔ ∃ 𝑏 ∈ ( ℕ0 ↑m 1o ) ( ( ( 𝑎 ∈ ( ℕ0 ↑m 1o ) ↦ ( 𝑎 ‘ ∅ ) ) ‘ 𝑏 ) = ( 𝐷 ‘ 𝐹 ) ∧ ( 𝐴 ‘ ( ( 𝑎 ∈ ( ℕ0 ↑m 1o ) ↦ ( 𝑎 ‘ ∅ ) ) ‘ 𝑏 ) ) ≠ 𝑌 ) ) ) |
28 |
|
df1o2 |
⊢ 1o = { ∅ } |
29 |
|
nn0ex |
⊢ ℕ0 ∈ V |
30 |
|
0ex |
⊢ ∅ ∈ V |
31 |
28 29 30 18
|
mapsnf1o2 |
⊢ ( 𝑎 ∈ ( ℕ0 ↑m 1o ) ↦ ( 𝑎 ‘ ∅ ) ) : ( ℕ0 ↑m 1o ) –1-1-onto→ ℕ0 |
32 |
|
f1ofo |
⊢ ( ( 𝑎 ∈ ( ℕ0 ↑m 1o ) ↦ ( 𝑎 ‘ ∅ ) ) : ( ℕ0 ↑m 1o ) –1-1-onto→ ℕ0 → ( 𝑎 ∈ ( ℕ0 ↑m 1o ) ↦ ( 𝑎 ‘ ∅ ) ) : ( ℕ0 ↑m 1o ) –onto→ ℕ0 ) |
33 |
|
eqeq1 |
⊢ ( ( ( 𝑎 ∈ ( ℕ0 ↑m 1o ) ↦ ( 𝑎 ‘ ∅ ) ) ‘ 𝑏 ) = 𝑑 → ( ( ( 𝑎 ∈ ( ℕ0 ↑m 1o ) ↦ ( 𝑎 ‘ ∅ ) ) ‘ 𝑏 ) = ( 𝐷 ‘ 𝐹 ) ↔ 𝑑 = ( 𝐷 ‘ 𝐹 ) ) ) |
34 |
|
fveq2 |
⊢ ( ( ( 𝑎 ∈ ( ℕ0 ↑m 1o ) ↦ ( 𝑎 ‘ ∅ ) ) ‘ 𝑏 ) = 𝑑 → ( 𝐴 ‘ ( ( 𝑎 ∈ ( ℕ0 ↑m 1o ) ↦ ( 𝑎 ‘ ∅ ) ) ‘ 𝑏 ) ) = ( 𝐴 ‘ 𝑑 ) ) |
35 |
34
|
neeq1d |
⊢ ( ( ( 𝑎 ∈ ( ℕ0 ↑m 1o ) ↦ ( 𝑎 ‘ ∅ ) ) ‘ 𝑏 ) = 𝑑 → ( ( 𝐴 ‘ ( ( 𝑎 ∈ ( ℕ0 ↑m 1o ) ↦ ( 𝑎 ‘ ∅ ) ) ‘ 𝑏 ) ) ≠ 𝑌 ↔ ( 𝐴 ‘ 𝑑 ) ≠ 𝑌 ) ) |
36 |
33 35
|
anbi12d |
⊢ ( ( ( 𝑎 ∈ ( ℕ0 ↑m 1o ) ↦ ( 𝑎 ‘ ∅ ) ) ‘ 𝑏 ) = 𝑑 → ( ( ( ( 𝑎 ∈ ( ℕ0 ↑m 1o ) ↦ ( 𝑎 ‘ ∅ ) ) ‘ 𝑏 ) = ( 𝐷 ‘ 𝐹 ) ∧ ( 𝐴 ‘ ( ( 𝑎 ∈ ( ℕ0 ↑m 1o ) ↦ ( 𝑎 ‘ ∅ ) ) ‘ 𝑏 ) ) ≠ 𝑌 ) ↔ ( 𝑑 = ( 𝐷 ‘ 𝐹 ) ∧ ( 𝐴 ‘ 𝑑 ) ≠ 𝑌 ) ) ) |
37 |
36
|
cbvexfo |
⊢ ( ( 𝑎 ∈ ( ℕ0 ↑m 1o ) ↦ ( 𝑎 ‘ ∅ ) ) : ( ℕ0 ↑m 1o ) –onto→ ℕ0 → ( ∃ 𝑏 ∈ ( ℕ0 ↑m 1o ) ( ( ( 𝑎 ∈ ( ℕ0 ↑m 1o ) ↦ ( 𝑎 ‘ ∅ ) ) ‘ 𝑏 ) = ( 𝐷 ‘ 𝐹 ) ∧ ( 𝐴 ‘ ( ( 𝑎 ∈ ( ℕ0 ↑m 1o ) ↦ ( 𝑎 ‘ ∅ ) ) ‘ 𝑏 ) ) ≠ 𝑌 ) ↔ ∃ 𝑑 ∈ ℕ0 ( 𝑑 = ( 𝐷 ‘ 𝐹 ) ∧ ( 𝐴 ‘ 𝑑 ) ≠ 𝑌 ) ) ) |
38 |
31 32 37
|
mp2b |
⊢ ( ∃ 𝑏 ∈ ( ℕ0 ↑m 1o ) ( ( ( 𝑎 ∈ ( ℕ0 ↑m 1o ) ↦ ( 𝑎 ‘ ∅ ) ) ‘ 𝑏 ) = ( 𝐷 ‘ 𝐹 ) ∧ ( 𝐴 ‘ ( ( 𝑎 ∈ ( ℕ0 ↑m 1o ) ↦ ( 𝑎 ‘ ∅ ) ) ‘ 𝑏 ) ) ≠ 𝑌 ) ↔ ∃ 𝑑 ∈ ℕ0 ( 𝑑 = ( 𝐷 ‘ 𝐹 ) ∧ ( 𝐴 ‘ 𝑑 ) ≠ 𝑌 ) ) |
39 |
27 38
|
bitrdi |
⊢ ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐹 ≠ 0 ) → ( ∃ 𝑏 ∈ ( ℕ0 ↑m 1o ) ( ( 𝐹 ‘ 𝑏 ) ≠ 𝑌 ∧ ( ( 𝑎 ∈ ( ℕ0 ↑m 1o ) ↦ ( 𝑎 ‘ ∅ ) ) ‘ 𝑏 ) = ( 𝐷 ‘ 𝐹 ) ) ↔ ∃ 𝑑 ∈ ℕ0 ( 𝑑 = ( 𝐷 ‘ 𝐹 ) ∧ ( 𝐴 ‘ 𝑑 ) ≠ 𝑌 ) ) ) |
40 |
1 2 3 4
|
deg1nn0cl |
⊢ ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐹 ≠ 0 ) → ( 𝐷 ‘ 𝐹 ) ∈ ℕ0 ) |
41 |
|
fveq2 |
⊢ ( 𝑑 = ( 𝐷 ‘ 𝐹 ) → ( 𝐴 ‘ 𝑑 ) = ( 𝐴 ‘ ( 𝐷 ‘ 𝐹 ) ) ) |
42 |
41
|
neeq1d |
⊢ ( 𝑑 = ( 𝐷 ‘ 𝐹 ) → ( ( 𝐴 ‘ 𝑑 ) ≠ 𝑌 ↔ ( 𝐴 ‘ ( 𝐷 ‘ 𝐹 ) ) ≠ 𝑌 ) ) |
43 |
42
|
ceqsrexv |
⊢ ( ( 𝐷 ‘ 𝐹 ) ∈ ℕ0 → ( ∃ 𝑑 ∈ ℕ0 ( 𝑑 = ( 𝐷 ‘ 𝐹 ) ∧ ( 𝐴 ‘ 𝑑 ) ≠ 𝑌 ) ↔ ( 𝐴 ‘ ( 𝐷 ‘ 𝐹 ) ) ≠ 𝑌 ) ) |
44 |
40 43
|
syl |
⊢ ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐹 ≠ 0 ) → ( ∃ 𝑑 ∈ ℕ0 ( 𝑑 = ( 𝐷 ‘ 𝐹 ) ∧ ( 𝐴 ‘ 𝑑 ) ≠ 𝑌 ) ↔ ( 𝐴 ‘ ( 𝐷 ‘ 𝐹 ) ) ≠ 𝑌 ) ) |
45 |
39 44
|
bitrd |
⊢ ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐹 ≠ 0 ) → ( ∃ 𝑏 ∈ ( ℕ0 ↑m 1o ) ( ( 𝐹 ‘ 𝑏 ) ≠ 𝑌 ∧ ( ( 𝑎 ∈ ( ℕ0 ↑m 1o ) ↦ ( 𝑎 ‘ ∅ ) ) ‘ 𝑏 ) = ( 𝐷 ‘ 𝐹 ) ) ↔ ( 𝐴 ‘ ( 𝐷 ‘ 𝐹 ) ) ≠ 𝑌 ) ) |
46 |
14 45
|
mpbid |
⊢ ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐹 ≠ 0 ) → ( 𝐴 ‘ ( 𝐷 ‘ 𝐹 ) ) ≠ 𝑌 ) |