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

Metamath Proof Explorer

Theorem ply1basfvi

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

Ref Expression
Assertion ply1basfvi ⊢ Base Poly 1 ⁡ R = Base Poly 1 ⁡ I ⁡ R

Proof

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