Theorem mon1pldg

Description: Unitic polynomials have one leading coefficients. (Contributed by Stefan O'Rear, 28-Mar-2015)

	Ref	Expression
Hypotheses	mon1pldg.d	⊢ 𝐷 = ( deg1 ‘ 𝑅 )
	mon1pldg.o	⊢ 1 = ( 1r ‘ 𝑅 )
	mon1pldg.m	⊢ 𝑀 = ( Monic1p ‘ 𝑅 )
Assertion	mon1pldg	⊢ ( 𝐹 ∈ 𝑀 → ( ( coe1 ‘ 𝐹 ) ‘ ( 𝐷 ‘ 𝐹 ) ) = 1 )

Proof

Step	Hyp	Ref	Expression
1		mon1pldg.d	⊢ 𝐷 = ( deg1 ‘ 𝑅 )
2		mon1pldg.o	⊢ 1 = ( 1r ‘ 𝑅 )
3		mon1pldg.m	⊢ 𝑀 = ( Monic1p ‘ 𝑅 )
4		eqid	⊢ ( Poly1 ‘ 𝑅 ) = ( Poly1 ‘ 𝑅 )
5		eqid	⊢ ( Base ‘ ( Poly1 ‘ 𝑅 ) ) = ( Base ‘ ( Poly1 ‘ 𝑅 ) )
6		eqid	⊢ ( 0g ‘ ( Poly1 ‘ 𝑅 ) ) = ( 0g ‘ ( Poly1 ‘ 𝑅 ) )
7	4 5 6 1 3 2	ismon1p	⊢ ( 𝐹 ∈ 𝑀 ↔ ( 𝐹 ∈ ( Base ‘ ( Poly1 ‘ 𝑅 ) ) ∧ 𝐹 ≠ ( 0g ‘ ( Poly1 ‘ 𝑅 ) ) ∧ ( ( coe1 ‘ 𝐹 ) ‘ ( 𝐷 ‘ 𝐹 ) ) = 1 ) )
8	7	simp3bi	⊢ ( 𝐹 ∈ 𝑀 → ( ( coe1 ‘ 𝐹 ) ‘ ( 𝐷 ‘ 𝐹 ) ) = 1 )