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 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 ) → 𝐹𝐶 )