Step |
Hyp |
Ref |
Expression |
1 |
|
fvi |
⊢ ( 𝑅 ∈ V → ( I ‘ 𝑅 ) = 𝑅 ) |
2 |
1
|
fveq2d |
⊢ ( 𝑅 ∈ V → ( Poly1 ‘ ( I ‘ 𝑅 ) ) = ( Poly1 ‘ 𝑅 ) ) |
3 |
2
|
fveq2d |
⊢ ( 𝑅 ∈ V → ( +g ‘ ( Poly1 ‘ ( I ‘ 𝑅 ) ) ) = ( +g ‘ ( Poly1 ‘ 𝑅 ) ) ) |
4 |
|
eqid |
⊢ ( Poly1 ‘ ∅ ) = ( Poly1 ‘ ∅ ) |
5 |
|
eqid |
⊢ ( 1o mPoly ∅ ) = ( 1o mPoly ∅ ) |
6 |
|
eqid |
⊢ ( +g ‘ ( Poly1 ‘ ∅ ) ) = ( +g ‘ ( Poly1 ‘ ∅ ) ) |
7 |
4 5 6
|
ply1plusg |
⊢ ( +g ‘ ( Poly1 ‘ ∅ ) ) = ( +g ‘ ( 1o mPoly ∅ ) ) |
8 |
|
eqid |
⊢ ( 1o mPwSer ∅ ) = ( 1o mPwSer ∅ ) |
9 |
|
eqid |
⊢ ( +g ‘ ( 1o mPoly ∅ ) ) = ( +g ‘ ( 1o mPoly ∅ ) ) |
10 |
5 8 9
|
mplplusg |
⊢ ( +g ‘ ( 1o mPoly ∅ ) ) = ( +g ‘ ( 1o mPwSer ∅ ) ) |
11 |
|
base0 |
⊢ ∅ = ( Base ‘ ∅ ) |
12 |
|
psr1baslem |
⊢ ( ℕ0 ↑m 1o ) = { 𝑎 ∈ ( ℕ0 ↑m 1o ) ∣ ( ◡ 𝑎 “ ℕ ) ∈ Fin } |
13 |
|
eqid |
⊢ ( Base ‘ ( 1o mPwSer ∅ ) ) = ( Base ‘ ( 1o mPwSer ∅ ) ) |
14 |
|
1on |
⊢ 1o ∈ On |
15 |
14
|
a1i |
⊢ ( ⊤ → 1o ∈ On ) |
16 |
8 11 12 13 15
|
psrbas |
⊢ ( ⊤ → ( Base ‘ ( 1o mPwSer ∅ ) ) = ( ∅ ↑m ( ℕ0 ↑m 1o ) ) ) |
17 |
16
|
mptru |
⊢ ( Base ‘ ( 1o mPwSer ∅ ) ) = ( ∅ ↑m ( ℕ0 ↑m 1o ) ) |
18 |
|
0nn0 |
⊢ 0 ∈ ℕ0 |
19 |
18
|
fconst6 |
⊢ ( 1o × { 0 } ) : 1o ⟶ ℕ0 |
20 |
|
nn0ex |
⊢ ℕ0 ∈ V |
21 |
|
1oex |
⊢ 1o ∈ V |
22 |
20 21
|
elmap |
⊢ ( ( 1o × { 0 } ) ∈ ( ℕ0 ↑m 1o ) ↔ ( 1o × { 0 } ) : 1o ⟶ ℕ0 ) |
23 |
19 22
|
mpbir |
⊢ ( 1o × { 0 } ) ∈ ( ℕ0 ↑m 1o ) |
24 |
|
ne0i |
⊢ ( ( 1o × { 0 } ) ∈ ( ℕ0 ↑m 1o ) → ( ℕ0 ↑m 1o ) ≠ ∅ ) |
25 |
|
map0b |
⊢ ( ( ℕ0 ↑m 1o ) ≠ ∅ → ( ∅ ↑m ( ℕ0 ↑m 1o ) ) = ∅ ) |
26 |
23 24 25
|
mp2b |
⊢ ( ∅ ↑m ( ℕ0 ↑m 1o ) ) = ∅ |
27 |
17 26
|
eqtr2i |
⊢ ∅ = ( Base ‘ ( 1o mPwSer ∅ ) ) |
28 |
|
eqid |
⊢ ( +g ‘ ∅ ) = ( +g ‘ ∅ ) |
29 |
|
eqid |
⊢ ( +g ‘ ( 1o mPwSer ∅ ) ) = ( +g ‘ ( 1o mPwSer ∅ ) ) |
30 |
8 27 28 29
|
psrplusg |
⊢ ( +g ‘ ( 1o mPwSer ∅ ) ) = ( ∘f ( +g ‘ ∅ ) ↾ ( ∅ × ∅ ) ) |
31 |
|
xp0 |
⊢ ( ∅ × ∅ ) = ∅ |
32 |
31
|
reseq2i |
⊢ ( ∘f ( +g ‘ ∅ ) ↾ ( ∅ × ∅ ) ) = ( ∘f ( +g ‘ ∅ ) ↾ ∅ ) |
33 |
10 30 32
|
3eqtri |
⊢ ( +g ‘ ( 1o mPoly ∅ ) ) = ( ∘f ( +g ‘ ∅ ) ↾ ∅ ) |
34 |
|
res0 |
⊢ ( ∘f ( +g ‘ ∅ ) ↾ ∅ ) = ∅ |
35 |
|
plusgid |
⊢ +g = Slot ( +g ‘ ndx ) |
36 |
35
|
str0 |
⊢ ∅ = ( +g ‘ ∅ ) |
37 |
34 36
|
eqtri |
⊢ ( ∘f ( +g ‘ ∅ ) ↾ ∅ ) = ( +g ‘ ∅ ) |
38 |
7 33 37
|
3eqtri |
⊢ ( +g ‘ ( Poly1 ‘ ∅ ) ) = ( +g ‘ ∅ ) |
39 |
|
fvprc |
⊢ ( ¬ 𝑅 ∈ V → ( I ‘ 𝑅 ) = ∅ ) |
40 |
39
|
fveq2d |
⊢ ( ¬ 𝑅 ∈ V → ( Poly1 ‘ ( I ‘ 𝑅 ) ) = ( Poly1 ‘ ∅ ) ) |
41 |
40
|
fveq2d |
⊢ ( ¬ 𝑅 ∈ V → ( +g ‘ ( Poly1 ‘ ( I ‘ 𝑅 ) ) ) = ( +g ‘ ( Poly1 ‘ ∅ ) ) ) |
42 |
|
fvprc |
⊢ ( ¬ 𝑅 ∈ V → ( Poly1 ‘ 𝑅 ) = ∅ ) |
43 |
42
|
fveq2d |
⊢ ( ¬ 𝑅 ∈ V → ( +g ‘ ( Poly1 ‘ 𝑅 ) ) = ( +g ‘ ∅ ) ) |
44 |
38 41 43
|
3eqtr4a |
⊢ ( ¬ 𝑅 ∈ V → ( +g ‘ ( Poly1 ‘ ( I ‘ 𝑅 ) ) ) = ( +g ‘ ( Poly1 ‘ 𝑅 ) ) ) |
45 |
3 44
|
pm2.61i |
⊢ ( +g ‘ ( Poly1 ‘ ( I ‘ 𝑅 ) ) ) = ( +g ‘ ( Poly1 ‘ 𝑅 ) ) |
46 |
45
|
eqcomi |
⊢ ( +g ‘ ( Poly1 ‘ 𝑅 ) ) = ( +g ‘ ( Poly1 ‘ ( I ‘ 𝑅 ) ) ) |