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 ∈ V x ∈ ℤ V ⟼ x ⁡ j ∈ p ∧ ∀ f ∈ p ∀ g ∈ p f + f g ∈ p ∧ f × f g ∈ 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 ∈ v c ∈ ℤ v ⟼ c ⁡ b ∈ p ↔ ∀ b ∈ V c ∈ ℤ 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 ∈ V c ∈ ℤ V ⟼ c ⁡ b ∈ p ↔ ∀ j ∈ V x ∈ ℤ V ⟼ x ⁡ j ∈ p
23 14 22 bitrdi ⊢ v = V → ∀ b ∈ v c ∈ ℤ v ⟼ c ⁡ b ∈ p ↔ ∀ j ∈ V x ∈ ℤ V ⟼ x ⁡ j ∈ p
24 11 23 anbi12d ⊢ v = V → ∀ a ∈ ℤ ℤ v × a ∈ p ∧ ∀ b ∈ v c ∈ ℤ v ⟼ c ⁡ b ∈ p ↔ ∀ i ∈ ℤ ℤ V × i ∈ p ∧ ∀ j ∈ V x ∈ ℤ V ⟼ x ⁡ j ∈ p
25 24 anbi1d ⊢ v = V → ∀ a ∈ ℤ ℤ v × a ∈ p ∧ ∀ b ∈ v c ∈ ℤ v ⟼ c ⁡ b ∈ p ∧ ∀ f ∈ p ∀ g ∈ p f + f g ∈ p ∧ f × f g ∈ p ↔ ∀ i ∈ ℤ ℤ V × i ∈ p ∧ ∀ j ∈ V x ∈ ℤ V ⟼ x ⁡ j ∈ p ∧ ∀ f ∈ p ∀ g ∈ p f + f g ∈ p ∧ f × f g ∈ p
26 3 25 rabeqbidv ⊢ v = V → p ∈ 𝒫 ℤ ℤ v | ∀ a ∈ ℤ ℤ v × a ∈ p ∧ ∀ b ∈ v c ∈ ℤ v ⟼ c ⁡ b ∈ p ∧ ∀ f ∈ p ∀ g ∈ p f + f g ∈ p ∧ f × f g ∈ p = p ∈ 𝒫 ℤ ℤ V | ∀ i ∈ ℤ ℤ V × i ∈ p ∧ ∀ j ∈ V x ∈ ℤ V ⟼ x ⁡ j ∈ p ∧ ∀ f ∈ p ∀ g ∈ p f + f g ∈ p ∧ f × f g ∈ p
27 df-mzpcl ⊢ mzPolyCld = v ∈ V ⟼ p ∈ 𝒫 ℤ ℤ v | ∀ a ∈ ℤ ℤ v × a ∈ p ∧ ∀ b ∈ v c ∈ ℤ v ⟼ c ⁡ b ∈ p ∧ ∀ f ∈ p ∀ g ∈ p f + f g ∈ p ∧ f × f g ∈ p
28 ovex ⊢ ℤ ℤ V ∈ V
29 28 pwex ⊢ 𝒫 ℤ ℤ V ∈ V
30 29 rabex ⊢ p ∈ 𝒫 ℤ ℤ V | ∀ i ∈ ℤ ℤ V × i ∈ p ∧ ∀ j ∈ V x ∈ ℤ V ⟼ x ⁡ j ∈ p ∧ ∀ f ∈ p ∀ g ∈ p f + f g ∈ p ∧ f × f g ∈ p ∈ V
31 26 27 30 fvmpt ⊢ V ∈ V → mzPolyCld ⁡ V = p ∈ 𝒫 ℤ ℤ V | ∀ i ∈ ℤ ℤ V × i ∈ p ∧ ∀ j ∈ V x ∈ ℤ V ⟼ x ⁡ j ∈ p ∧ ∀ f ∈ p ∀ g ∈ p f + f g ∈ p ∧ f × f g ∈ p