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 ‘ 𝑅 ) ) |