Theorem ply1basfvi

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

	Ref	Expression
Assertion	ply1basfvi	⊢ ( Base ‘ ( Poly1 ‘ 𝑅 ) ) = ( Base ‘ ( Poly1 ‘ ( I ‘ 𝑅 ) ) )

Proof

Step	Hyp	Ref	Expression
1		fvi	⊢ ( 𝑅 ∈ V → ( I ‘ 𝑅 ) = 𝑅 )
2	1	eqcomd	⊢ ( 𝑅 ∈ V → 𝑅 = ( I ‘ 𝑅 ) )
3	2	fveq2d	⊢ ( 𝑅 ∈ V → ( Poly1 ‘ 𝑅 ) = ( Poly1 ‘ ( I ‘ 𝑅 ) ) )
4	3	fveq2d	⊢ ( 𝑅 ∈ V → ( Base ‘ ( Poly1 ‘ 𝑅 ) ) = ( Base ‘ ( Poly1 ‘ ( I ‘ 𝑅 ) ) ) )
5		base0	⊢ ∅ = ( Base ‘ ∅ )
6		00ply1bas	⊢ ∅ = ( Base ‘ ( Poly1 ‘ ∅ ) )
7	5 6	eqtr3i	⊢ ( Base ‘ ∅ ) = ( Base ‘ ( Poly1 ‘ ∅ ) )
8		fvprc	⊢ ( ¬ 𝑅 ∈ V → ( Poly1 ‘ 𝑅 ) = ∅ )
9	8	fveq2d	⊢ ( ¬ 𝑅 ∈ V → ( Base ‘ ( Poly1 ‘ 𝑅 ) ) = ( Base ‘ ∅ ) )
10		fvprc	⊢ ( ¬ 𝑅 ∈ V → ( I ‘ 𝑅 ) = ∅ )
11	10	fveq2d	⊢ ( ¬ 𝑅 ∈ V → ( Poly1 ‘ ( I ‘ 𝑅 ) ) = ( Poly1 ‘ ∅ ) )
12	11	fveq2d	⊢ ( ¬ 𝑅 ∈ V → ( Base ‘ ( Poly1 ‘ ( I ‘ 𝑅 ) ) ) = ( Base ‘ ( Poly1 ‘ ∅ ) ) )
13	7 9 12	3eqtr4a	⊢ ( ¬ 𝑅 ∈ V → ( Base ‘ ( Poly1 ‘ 𝑅 ) ) = ( Base ‘ ( Poly1 ‘ ( I ‘ 𝑅 ) ) ) )
14	4 13	pm2.61i	⊢ ( Base ‘ ( Poly1 ‘ 𝑅 ) ) = ( Base ‘ ( Poly1 ‘ ( I ‘ 𝑅 ) ) )