Theorem deg1fvi

Description: Univariate polynomial degree respects protection. (Contributed by Stefan O'Rear, 28-Mar-2015)

	Ref	Expression
Assertion	deg1fvi	⊢ ( deg1 ‘ 𝑅 ) = ( deg1 ‘ ( I ‘ 𝑅 ) )

Proof

Step	Hyp	Ref	Expression
1		fvi	⊢ ( 𝑅 ∈ V → ( I ‘ 𝑅 ) = 𝑅 )
2	1	fveq2d	⊢ ( 𝑅 ∈ V → ( deg1 ‘ ( I ‘ 𝑅 ) ) = ( deg1 ‘ 𝑅 ) )
3		eqid	⊢ ( deg1 ‘ ∅ ) = ( deg1 ‘ ∅ )
4		eqid	⊢ ( Poly1 ‘ ∅ ) = ( Poly1 ‘ ∅ )
5		00ply1bas	⊢ ∅ = ( Base ‘ ( Poly1 ‘ ∅ ) )
6	3 4 5	deg1xrf	⊢ ( deg1 ‘ ∅ ) : ∅ ⟶ ℝ*
7		ffn	⊢ ( ( deg1 ‘ ∅ ) : ∅ ⟶ ℝ* → ( deg1 ‘ ∅ ) Fn ∅ )
8	6 7	ax-mp	⊢ ( deg1 ‘ ∅ ) Fn ∅
9		fn0	⊢ ( ( deg1 ‘ ∅ ) Fn ∅ ↔ ( deg1 ‘ ∅ ) = ∅ )
10	8 9	mpbi	⊢ ( deg1 ‘ ∅ ) = ∅
11		fvprc	⊢ ( ¬ 𝑅 ∈ V → ( I ‘ 𝑅 ) = ∅ )
12	11	fveq2d	⊢ ( ¬ 𝑅 ∈ V → ( deg1 ‘ ( I ‘ 𝑅 ) ) = ( deg1 ‘ ∅ ) )
13		fvprc	⊢ ( ¬ 𝑅 ∈ V → ( deg1 ‘ 𝑅 ) = ∅ )
14	10 12 13	3eqtr4a	⊢ ( ¬ 𝑅 ∈ V → ( deg1 ‘ ( I ‘ 𝑅 ) ) = ( deg1 ‘ 𝑅 ) )
15	2 14	pm2.61i	⊢ ( deg1 ‘ ( I ‘ 𝑅 ) ) = ( deg1 ‘ 𝑅 )
16	15	eqcomi	⊢ ( deg1 ‘ 𝑅 ) = ( deg1 ‘ ( I ‘ 𝑅 ) )