Metamath Proof Explorer

Theorem drnguc1p

Description: Over a division ring, all nonzero polynomials are unitic. (Contributed by Stefan O'Rear, 29-Mar-2015)

Ref Expression
Hypotheses drnguc1p.p ⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
drnguc1p.b ⊢ 𝐵 = ( Base ‘ 𝑃 )
drnguc1p.z ⊢ 0 = ( 0g ‘ 𝑃 )
drnguc1p.c ⊢ 𝐶 = ( Unic1p ‘ 𝑅 )
Assertion drnguc1p ( ( 𝑅 ∈ DivRing ∧ 𝐹 ∈ 𝐵 ∧ 𝐹 ≠ 0 ) → 𝐹 ∈ 𝐶 )

Proof

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 ffvelcdmd ⊢ ( ( 𝑅 ∈ 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 ) → 𝐹 ∈ 𝐶 )