Theorem isuc1p

Description: Being a unitic polynomial. (Contributed by Stefan O'Rear, 28-Mar-2015)

	Ref	Expression
Hypotheses	uc1pval.p	⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
	uc1pval.b	⊢ 𝐵 = ( Base ‘ 𝑃 )
	uc1pval.z	⊢ 0 = ( 0g ‘ 𝑃 )
	uc1pval.d	⊢ 𝐷 = ( deg1 ‘ 𝑅 )
	uc1pval.c	⊢ 𝐶 = ( Unic1p ‘ 𝑅 )
	uc1pval.u	⊢ 𝑈 = ( Unit ‘ 𝑅 )
Assertion	isuc1p	⊢ ( 𝐹 ∈ 𝐶 ↔ ( 𝐹 ∈ 𝐵 ∧ 𝐹 ≠ 0 ∧ ( ( coe1 ‘ 𝐹 ) ‘ ( 𝐷 ‘ 𝐹 ) ) ∈ 𝑈 ) )

Proof

Step	Hyp	Ref	Expression
1		uc1pval.p	⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
2		uc1pval.b	⊢ 𝐵 = ( Base ‘ 𝑃 )
3		uc1pval.z	⊢ 0 = ( 0g ‘ 𝑃 )
4		uc1pval.d	⊢ 𝐷 = ( deg1 ‘ 𝑅 )
5		uc1pval.c	⊢ 𝐶 = ( Unic1p ‘ 𝑅 )
6		uc1pval.u	⊢ 𝑈 = ( Unit ‘ 𝑅 )
7		neeq1	⊢ ( 𝑓 = 𝐹 → ( 𝑓 ≠ 0 ↔ 𝐹 ≠ 0 ) )
8		fveq2	⊢ ( 𝑓 = 𝐹 → ( coe1 ‘ 𝑓 ) = ( coe1 ‘ 𝐹 ) )
9		fveq2	⊢ ( 𝑓 = 𝐹 → ( 𝐷 ‘ 𝑓 ) = ( 𝐷 ‘ 𝐹 ) )
10	8 9	fveq12d	⊢ ( 𝑓 = 𝐹 → ( ( coe1 ‘ 𝑓 ) ‘ ( 𝐷 ‘ 𝑓 ) ) = ( ( coe1 ‘ 𝐹 ) ‘ ( 𝐷 ‘ 𝐹 ) ) )
11	10	eleq1d	⊢ ( 𝑓 = 𝐹 → ( ( ( coe1 ‘ 𝑓 ) ‘ ( 𝐷 ‘ 𝑓 ) ) ∈ 𝑈 ↔ ( ( coe1 ‘ 𝐹 ) ‘ ( 𝐷 ‘ 𝐹 ) ) ∈ 𝑈 ) )
12	7 11	anbi12d	⊢ ( 𝑓 = 𝐹 → ( ( 𝑓 ≠ 0 ∧ ( ( coe1 ‘ 𝑓 ) ‘ ( 𝐷 ‘ 𝑓 ) ) ∈ 𝑈 ) ↔ ( 𝐹 ≠ 0 ∧ ( ( coe1 ‘ 𝐹 ) ‘ ( 𝐷 ‘ 𝐹 ) ) ∈ 𝑈 ) ) )
13	1 2 3 4 5 6	uc1pval	⊢ 𝐶 = { 𝑓 ∈ 𝐵 ∣ ( 𝑓 ≠ 0 ∧ ( ( coe1 ‘ 𝑓 ) ‘ ( 𝐷 ‘ 𝑓 ) ) ∈ 𝑈 ) }
14	12 13	elrab2	⊢ ( 𝐹 ∈ 𝐶 ↔ ( 𝐹 ∈ 𝐵 ∧ ( 𝐹 ≠ 0 ∧ ( ( coe1 ‘ 𝐹 ) ‘ ( 𝐷 ‘ 𝐹 ) ) ∈ 𝑈 ) ) )
15		3anass	⊢ ( ( 𝐹 ∈ 𝐵 ∧ 𝐹 ≠ 0 ∧ ( ( coe1 ‘ 𝐹 ) ‘ ( 𝐷 ‘ 𝐹 ) ) ∈ 𝑈 ) ↔ ( 𝐹 ∈ 𝐵 ∧ ( 𝐹 ≠ 0 ∧ ( ( coe1 ‘ 𝐹 ) ‘ ( 𝐷 ‘ 𝐹 ) ) ∈ 𝑈 ) ) )
16	14 15	bitr4i	⊢ ( 𝐹 ∈ 𝐶 ↔ ( 𝐹 ∈ 𝐵 ∧ 𝐹 ≠ 0 ∧ ( ( coe1 ‘ 𝐹 ) ‘ ( 𝐷 ‘ 𝐹 ) ) ∈ 𝑈 ) )