Description: Unitic polynomials are not zero. (Contributed by Stefan O'Rear, 28-Mar-2015)
Ref | Expression | ||
---|---|---|---|
Hypotheses | uc1pn0.p | ⊢ 𝑃 = ( Poly1 ‘ 𝑅 ) | |
uc1pn0.z | ⊢ 0 = ( 0g ‘ 𝑃 ) | ||
uc1pn0.c | ⊢ 𝐶 = ( Unic1p ‘ 𝑅 ) | ||
Assertion | uc1pn0 | ⊢ ( 𝐹 ∈ 𝐶 → 𝐹 ≠ 0 ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | uc1pn0.p | ⊢ 𝑃 = ( Poly1 ‘ 𝑅 ) | |
2 | uc1pn0.z | ⊢ 0 = ( 0g ‘ 𝑃 ) | |
3 | uc1pn0.c | ⊢ 𝐶 = ( Unic1p ‘ 𝑅 ) | |
4 | eqid | ⊢ ( Base ‘ 𝑃 ) = ( Base ‘ 𝑃 ) | |
5 | eqid | ⊢ ( deg1 ‘ 𝑅 ) = ( deg1 ‘ 𝑅 ) | |
6 | eqid | ⊢ ( Unit ‘ 𝑅 ) = ( Unit ‘ 𝑅 ) | |
7 | 1 4 2 5 3 6 | isuc1p | ⊢ ( 𝐹 ∈ 𝐶 ↔ ( 𝐹 ∈ ( Base ‘ 𝑃 ) ∧ 𝐹 ≠ 0 ∧ ( ( coe1 ‘ 𝐹 ) ‘ ( ( deg1 ‘ 𝑅 ) ‘ 𝐹 ) ) ∈ ( Unit ‘ 𝑅 ) ) ) |
8 | 7 | simp2bi | ⊢ ( 𝐹 ∈ 𝐶 → 𝐹 ≠ 0 ) |