This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊢ ( ℕ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 ‘ 𝑅 ) ) )