Description: Unitic polynomials have unit leading coefficients. (Contributed by Stefan O'Rear, 28-Mar-2015)
Ref | Expression | ||
---|---|---|---|
Hypotheses | uc1pldg.d | ⊢ 𝐷 = ( deg1 ‘ 𝑅 ) | |
uc1pldg.u | ⊢ 𝑈 = ( Unit ‘ 𝑅 ) | ||
uc1pldg.c | ⊢ 𝐶 = ( Unic1p ‘ 𝑅 ) | ||
Assertion | uc1pldg | ⊢ ( 𝐹 ∈ 𝐶 → ( ( coe1 ‘ 𝐹 ) ‘ ( 𝐷 ‘ 𝐹 ) ) ∈ 𝑈 ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | uc1pldg.d | ⊢ 𝐷 = ( deg1 ‘ 𝑅 ) | |
2 | uc1pldg.u | ⊢ 𝑈 = ( Unit ‘ 𝑅 ) | |
3 | uc1pldg.c | ⊢ 𝐶 = ( Unic1p ‘ 𝑅 ) | |
4 | eqid | ⊢ ( Poly1 ‘ 𝑅 ) = ( Poly1 ‘ 𝑅 ) | |
5 | eqid | ⊢ ( Base ‘ ( Poly1 ‘ 𝑅 ) ) = ( Base ‘ ( Poly1 ‘ 𝑅 ) ) | |
6 | eqid | ⊢ ( 0g ‘ ( Poly1 ‘ 𝑅 ) ) = ( 0g ‘ ( Poly1 ‘ 𝑅 ) ) | |
7 | 4 5 6 1 3 2 | isuc1p | ⊢ ( 𝐹 ∈ 𝐶 ↔ ( 𝐹 ∈ ( Base ‘ ( Poly1 ‘ 𝑅 ) ) ∧ 𝐹 ≠ ( 0g ‘ ( Poly1 ‘ 𝑅 ) ) ∧ ( ( coe1 ‘ 𝐹 ) ‘ ( 𝐷 ‘ 𝐹 ) ) ∈ 𝑈 ) ) |
8 | 7 | simp3bi | ⊢ ( 𝐹 ∈ 𝐶 → ( ( coe1 ‘ 𝐹 ) ‘ ( 𝐷 ‘ 𝐹 ) ) ∈ 𝑈 ) |