Metamath Proof Explorer

Theorem mzpclval

Description: Substitution lemma for mzPolyCld . (Contributed by Stefan O'Rear, 4-Oct-2014)

Ref Expression
Assertion mzpclval ⊢V∈V→mzPolyCld⁡V=p∈𝒫ℤℤV|∀i∈ℤℤV×i∈p∧∀j∈Vx∈ℤV⟼x⁡j∈p∧∀f∈p∀g∈pf+fg∈p∧f×fg∈p

Proof

Step Hyp Ref Expression
1 oveq2 ⊢v=V→ℤv=ℤV
2 1 oveq2d ⊢v=V→ℤℤv=ℤℤV
3 2 pweqd ⊢v=V→𝒫ℤℤv=𝒫ℤℤV
4 1 xpeq1d ⊢v=V→ℤv×a=ℤV×a
5 4 eleq1d ⊢v=V→ℤv×a∈p↔ℤV×a∈p
6 5 ralbidv ⊢v=V→∀a∈ℤℤv×a∈p↔∀a∈ℤℤV×a∈p
7 sneq ⊢a=i→a=i
8 7 xpeq2d ⊢a=i→ℤV×a=ℤV×i
9 8 eleq1d ⊢a=i→ℤV×a∈p↔ℤV×i∈p
10 9 cbvralvw ⊢∀a∈ℤℤV×a∈p↔∀i∈ℤℤV×i∈p
11 6 10 bitrdi ⊢v=V→∀a∈ℤℤv×a∈p↔∀i∈ℤℤV×i∈p
12 1 mpteq1d ⊢v=V→c∈ℤv⟼c⁡b=c∈ℤV⟼c⁡b
13 12 eleq1d ⊢v=V→c∈ℤv⟼c⁡b∈p↔c∈ℤV⟼c⁡b∈p
14 13 raleqbi1dv ⊢v=V→∀b∈vc∈ℤv⟼c⁡b∈p↔∀b∈Vc∈ℤV⟼c⁡b∈p
15 fveq2 ⊢b=j→c⁡b=c⁡j
16 15 mpteq2dv ⊢b=j→c∈ℤV⟼c⁡b=c∈ℤV⟼c⁡j
17 16 eleq1d ⊢b=j→c∈ℤV⟼c⁡b∈p↔c∈ℤV⟼c⁡j∈p
18 fveq1 ⊢c=x→c⁡j=x⁡j
19 18 cbvmptv ⊢c∈ℤV⟼c⁡j=x∈ℤV⟼x⁡j
20 19 eleq1i ⊢c∈ℤV⟼c⁡j∈p↔x∈ℤV⟼x⁡j∈p
21 17 20 bitrdi ⊢b=j→c∈ℤV⟼c⁡b∈p↔x∈ℤV⟼x⁡j∈p
22 21 cbvralvw ⊢∀b∈Vc∈ℤV⟼c⁡b∈p↔∀j∈Vx∈ℤV⟼x⁡j∈p
23 14 22 bitrdi ⊢v=V→∀b∈vc∈ℤv⟼c⁡b∈p↔∀j∈Vx∈ℤV⟼x⁡j∈p
24 11 23 anbi12d ⊢v=V→∀a∈ℤℤv×a∈p∧∀b∈vc∈ℤv⟼c⁡b∈p↔∀i∈ℤℤV×i∈p∧∀j∈Vx∈ℤV⟼x⁡j∈p
25 24 anbi1d ⊢v=V→∀a∈ℤℤv×a∈p∧∀b∈vc∈ℤv⟼c⁡b∈p∧∀f∈p∀g∈pf+fg∈p∧f×fg∈p↔∀i∈ℤℤV×i∈p∧∀j∈Vx∈ℤV⟼x⁡j∈p∧∀f∈p∀g∈pf+fg∈p∧f×fg∈p
26 3 25 rabeqbidv ⊢v=V→p∈𝒫ℤℤv|∀a∈ℤℤv×a∈p∧∀b∈vc∈ℤv⟼c⁡b∈p∧∀f∈p∀g∈pf+fg∈p∧f×fg∈p=p∈𝒫ℤℤV|∀i∈ℤℤV×i∈p∧∀j∈Vx∈ℤV⟼x⁡j∈p∧∀f∈p∀g∈pf+fg∈p∧f×fg∈p
27 df-mzpcl ⊢mzPolyCld=v∈V⟼p∈𝒫ℤℤv|∀a∈ℤℤv×a∈p∧∀b∈vc∈ℤv⟼c⁡b∈p∧∀f∈p∀g∈pf+fg∈p∧f×fg∈p
28 ovex ⊢ℤℤV∈V
29 28 pwex ⊢𝒫ℤℤV∈V
30 29 rabex ⊢p∈𝒫ℤℤV|∀i∈ℤℤV×i∈p∧∀j∈Vx∈ℤV⟼x⁡j∈p∧∀f∈p∀g∈pf+fg∈p∧f×fg∈p∈V
31 26 27 30 fvmpt ⊢V∈V→mzPolyCld⁡V=p∈𝒫ℤℤV|∀i∈ℤℤV×i∈p∧∀j∈Vx∈ℤV⟼x⁡j∈p∧∀f∈p∀g∈pf+fg∈p∧f×fg∈p