Metamath Proof Explorer


Theorem ply1plusgfvi

Description: Protection compatibility of the univariate polynomial addition. (Contributed by Stefan O'Rear, 27-Mar-2015)

Ref Expression
Assertion ply1plusgfvi ( +g ‘ ( Poly1𝑅 ) ) = ( +g ‘ ( Poly1 ‘ ( I ‘ 𝑅 ) ) )

Proof

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 ( ℕ0m 1o ) = { 𝑎 ∈ ( ℕ0m 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 ( ℕ0m 1o ) ) )
17 16 mptru ( Base ‘ ( 1o mPwSer ∅ ) ) = ( ∅ ↑m ( ℕ0m 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 } ) ∈ ( ℕ0m 1o ) ↔ ( 1o × { 0 } ) : 1o ⟶ ℕ0 )
23 19 22 mpbir ( 1o × { 0 } ) ∈ ( ℕ0m 1o )
24 ne0i ( ( 1o × { 0 } ) ∈ ( ℕ0m 1o ) → ( ℕ0m 1o ) ≠ ∅ )
25 map0b ( ( ℕ0m 1o ) ≠ ∅ → ( ∅ ↑m ( ℕ0m 1o ) ) = ∅ )
26 23 24 25 mp2b ( ∅ ↑m ( ℕ0m 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 df-plusg +g = Slot 2
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 ‘ 𝑅 ) ) )