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