Step |
Hyp |
Ref |
Expression |
1 |
|
drnguc1p.p |
⊢ 𝑃 = ( Poly1 ‘ 𝑅 ) |
2 |
|
drnguc1p.b |
⊢ 𝐵 = ( Base ‘ 𝑃 ) |
3 |
|
drnguc1p.z |
⊢ 0 = ( 0g ‘ 𝑃 ) |
4 |
|
drnguc1p.c |
⊢ 𝐶 = ( Unic1p ‘ 𝑅 ) |
5 |
|
simp2 |
⊢ ( ( 𝑅 ∈ DivRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐹 ≠ 0 ) → 𝐹 ∈ 𝐵 ) |
6 |
|
simp3 |
⊢ ( ( 𝑅 ∈ DivRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐹 ≠ 0 ) → 𝐹 ≠ 0 ) |
7 |
|
eqid |
⊢ ( coe1 ‘ 𝐹 ) = ( coe1 ‘ 𝐹 ) |
8 |
|
eqid |
⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 ) |
9 |
7 2 1 8
|
coe1f |
⊢ ( 𝐹 ∈ 𝐵 → ( coe1 ‘ 𝐹 ) : ℕ0 ⟶ ( Base ‘ 𝑅 ) ) |
10 |
9
|
3ad2ant2 |
⊢ ( ( 𝑅 ∈ DivRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐹 ≠ 0 ) → ( coe1 ‘ 𝐹 ) : ℕ0 ⟶ ( Base ‘ 𝑅 ) ) |
11 |
|
drngring |
⊢ ( 𝑅 ∈ DivRing → 𝑅 ∈ Ring ) |
12 |
|
eqid |
⊢ ( deg1 ‘ 𝑅 ) = ( deg1 ‘ 𝑅 ) |
13 |
12 1 3 2
|
deg1nn0cl |
⊢ ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐹 ≠ 0 ) → ( ( deg1 ‘ 𝑅 ) ‘ 𝐹 ) ∈ ℕ0 ) |
14 |
11 13
|
syl3an1 |
⊢ ( ( 𝑅 ∈ DivRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐹 ≠ 0 ) → ( ( deg1 ‘ 𝑅 ) ‘ 𝐹 ) ∈ ℕ0 ) |
15 |
10 14
|
ffvelrnd |
⊢ ( ( 𝑅 ∈ DivRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐹 ≠ 0 ) → ( ( coe1 ‘ 𝐹 ) ‘ ( ( deg1 ‘ 𝑅 ) ‘ 𝐹 ) ) ∈ ( Base ‘ 𝑅 ) ) |
16 |
|
eqid |
⊢ ( 0g ‘ 𝑅 ) = ( 0g ‘ 𝑅 ) |
17 |
12 1 3 2 16 7
|
deg1ldg |
⊢ ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐹 ≠ 0 ) → ( ( coe1 ‘ 𝐹 ) ‘ ( ( deg1 ‘ 𝑅 ) ‘ 𝐹 ) ) ≠ ( 0g ‘ 𝑅 ) ) |
18 |
11 17
|
syl3an1 |
⊢ ( ( 𝑅 ∈ DivRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐹 ≠ 0 ) → ( ( coe1 ‘ 𝐹 ) ‘ ( ( deg1 ‘ 𝑅 ) ‘ 𝐹 ) ) ≠ ( 0g ‘ 𝑅 ) ) |
19 |
|
eqid |
⊢ ( Unit ‘ 𝑅 ) = ( Unit ‘ 𝑅 ) |
20 |
8 19 16
|
drngunit |
⊢ ( 𝑅 ∈ DivRing → ( ( ( coe1 ‘ 𝐹 ) ‘ ( ( deg1 ‘ 𝑅 ) ‘ 𝐹 ) ) ∈ ( Unit ‘ 𝑅 ) ↔ ( ( ( coe1 ‘ 𝐹 ) ‘ ( ( deg1 ‘ 𝑅 ) ‘ 𝐹 ) ) ∈ ( Base ‘ 𝑅 ) ∧ ( ( coe1 ‘ 𝐹 ) ‘ ( ( deg1 ‘ 𝑅 ) ‘ 𝐹 ) ) ≠ ( 0g ‘ 𝑅 ) ) ) ) |
21 |
20
|
3ad2ant1 |
⊢ ( ( 𝑅 ∈ DivRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐹 ≠ 0 ) → ( ( ( coe1 ‘ 𝐹 ) ‘ ( ( deg1 ‘ 𝑅 ) ‘ 𝐹 ) ) ∈ ( Unit ‘ 𝑅 ) ↔ ( ( ( coe1 ‘ 𝐹 ) ‘ ( ( deg1 ‘ 𝑅 ) ‘ 𝐹 ) ) ∈ ( Base ‘ 𝑅 ) ∧ ( ( coe1 ‘ 𝐹 ) ‘ ( ( deg1 ‘ 𝑅 ) ‘ 𝐹 ) ) ≠ ( 0g ‘ 𝑅 ) ) ) ) |
22 |
15 18 21
|
mpbir2and |
⊢ ( ( 𝑅 ∈ DivRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐹 ≠ 0 ) → ( ( coe1 ‘ 𝐹 ) ‘ ( ( deg1 ‘ 𝑅 ) ‘ 𝐹 ) ) ∈ ( Unit ‘ 𝑅 ) ) |
23 |
1 2 3 12 4 19
|
isuc1p |
⊢ ( 𝐹 ∈ 𝐶 ↔ ( 𝐹 ∈ 𝐵 ∧ 𝐹 ≠ 0 ∧ ( ( coe1 ‘ 𝐹 ) ‘ ( ( deg1 ‘ 𝑅 ) ‘ 𝐹 ) ) ∈ ( Unit ‘ 𝑅 ) ) ) |
24 |
5 6 22 23
|
syl3anbrc |
⊢ ( ( 𝑅 ∈ DivRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐹 ≠ 0 ) → 𝐹 ∈ 𝐶 ) |