Theorem elmzpcl

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

	Ref	Expression
Assertion	elmzpcl	⊢ ( 𝑉 ∈ V → ( 𝑃 ∈ ( mzPolyCld ‘ 𝑉 ) ↔ ( 𝑃 ⊆ ( ℤ ↑m ( ℤ ↑m 𝑉 ) ) ∧ ( ( ∀ 𝑖 ∈ ℤ ( ( ℤ ↑m 𝑉 ) × { 𝑖 } ) ∈ 𝑃 ∧ ∀ 𝑗 ∈ 𝑉 ( 𝑥 ∈ ( ℤ ↑m 𝑉 ) ↦ ( 𝑥 ‘ 𝑗 ) ) ∈ 𝑃 ) ∧ ∀ 𝑓 ∈ 𝑃 ∀ 𝑔 ∈ 𝑃 ( ( 𝑓 ∘f + 𝑔 ) ∈ 𝑃 ∧ ( 𝑓 ∘f · 𝑔 ) ∈ 𝑃 ) ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		mzpclval	⊢ ( 𝑉 ∈ V → ( mzPolyCld ‘ 𝑉 ) = { 𝑝 ∈ 𝒫 ( ℤ ↑m ( ℤ ↑m 𝑉 ) ) ∣ ( ( ∀ 𝑖 ∈ ℤ ( ( ℤ ↑m 𝑉 ) × { 𝑖 } ) ∈ 𝑝 ∧ ∀ 𝑗 ∈ 𝑉 ( 𝑥 ∈ ( ℤ ↑m 𝑉 ) ↦ ( 𝑥 ‘ 𝑗 ) ) ∈ 𝑝 ) ∧ ∀ 𝑓 ∈ 𝑝 ∀ 𝑔 ∈ 𝑝 ( ( 𝑓 ∘f + 𝑔 ) ∈ 𝑝 ∧ ( 𝑓 ∘f · 𝑔 ) ∈ 𝑝 ) ) } )
2	1	eleq2d	⊢ ( 𝑉 ∈ V → ( 𝑃 ∈ ( mzPolyCld ‘ 𝑉 ) ↔ 𝑃 ∈ { 𝑝 ∈ 𝒫 ( ℤ ↑m ( ℤ ↑m 𝑉 ) ) ∣ ( ( ∀ 𝑖 ∈ ℤ ( ( ℤ ↑m 𝑉 ) × { 𝑖 } ) ∈ 𝑝 ∧ ∀ 𝑗 ∈ 𝑉 ( 𝑥 ∈ ( ℤ ↑m 𝑉 ) ↦ ( 𝑥 ‘ 𝑗 ) ) ∈ 𝑝 ) ∧ ∀ 𝑓 ∈ 𝑝 ∀ 𝑔 ∈ 𝑝 ( ( 𝑓 ∘f + 𝑔 ) ∈ 𝑝 ∧ ( 𝑓 ∘f · 𝑔 ) ∈ 𝑝 ) ) } ) )
3		eleq2	⊢ ( 𝑝 = 𝑃 → ( ( ( ℤ ↑m 𝑉 ) × { 𝑖 } ) ∈ 𝑝 ↔ ( ( ℤ ↑m 𝑉 ) × { 𝑖 } ) ∈ 𝑃 ) )
4	3	ralbidv	⊢ ( 𝑝 = 𝑃 → ( ∀ 𝑖 ∈ ℤ ( ( ℤ ↑m 𝑉 ) × { 𝑖 } ) ∈ 𝑝 ↔ ∀ 𝑖 ∈ ℤ ( ( ℤ ↑m 𝑉 ) × { 𝑖 } ) ∈ 𝑃 ) )
5		eleq2	⊢ ( 𝑝 = 𝑃 → ( ( 𝑥 ∈ ( ℤ ↑m 𝑉 ) ↦ ( 𝑥 ‘ 𝑗 ) ) ∈ 𝑝 ↔ ( 𝑥 ∈ ( ℤ ↑m 𝑉 ) ↦ ( 𝑥 ‘ 𝑗 ) ) ∈ 𝑃 ) )
6	5	ralbidv	⊢ ( 𝑝 = 𝑃 → ( ∀ 𝑗 ∈ 𝑉 ( 𝑥 ∈ ( ℤ ↑m 𝑉 ) ↦ ( 𝑥 ‘ 𝑗 ) ) ∈ 𝑝 ↔ ∀ 𝑗 ∈ 𝑉 ( 𝑥 ∈ ( ℤ ↑m 𝑉 ) ↦ ( 𝑥 ‘ 𝑗 ) ) ∈ 𝑃 ) )
7	4 6	anbi12d	⊢ ( 𝑝 = 𝑃 → ( ( ∀ 𝑖 ∈ ℤ ( ( ℤ ↑m 𝑉 ) × { 𝑖 } ) ∈ 𝑝 ∧ ∀ 𝑗 ∈ 𝑉 ( 𝑥 ∈ ( ℤ ↑m 𝑉 ) ↦ ( 𝑥 ‘ 𝑗 ) ) ∈ 𝑝 ) ↔ ( ∀ 𝑖 ∈ ℤ ( ( ℤ ↑m 𝑉 ) × { 𝑖 } ) ∈ 𝑃 ∧ ∀ 𝑗 ∈ 𝑉 ( 𝑥 ∈ ( ℤ ↑m 𝑉 ) ↦ ( 𝑥 ‘ 𝑗 ) ) ∈ 𝑃 ) ) )
8		eleq2	⊢ ( 𝑝 = 𝑃 → ( ( 𝑓 ∘f + 𝑔 ) ∈ 𝑝 ↔ ( 𝑓 ∘f + 𝑔 ) ∈ 𝑃 ) )
9		eleq2	⊢ ( 𝑝 = 𝑃 → ( ( 𝑓 ∘f · 𝑔 ) ∈ 𝑝 ↔ ( 𝑓 ∘f · 𝑔 ) ∈ 𝑃 ) )
10	8 9	anbi12d	⊢ ( 𝑝 = 𝑃 → ( ( ( 𝑓 ∘f + 𝑔 ) ∈ 𝑝 ∧ ( 𝑓 ∘f · 𝑔 ) ∈ 𝑝 ) ↔ ( ( 𝑓 ∘f + 𝑔 ) ∈ 𝑃 ∧ ( 𝑓 ∘f · 𝑔 ) ∈ 𝑃 ) ) )
11	10	raleqbi1dv	⊢ ( 𝑝 = 𝑃 → ( ∀ 𝑔 ∈ 𝑝 ( ( 𝑓 ∘f + 𝑔 ) ∈ 𝑝 ∧ ( 𝑓 ∘f · 𝑔 ) ∈ 𝑝 ) ↔ ∀ 𝑔 ∈ 𝑃 ( ( 𝑓 ∘f + 𝑔 ) ∈ 𝑃 ∧ ( 𝑓 ∘f · 𝑔 ) ∈ 𝑃 ) ) )
12	11	raleqbi1dv	⊢ ( 𝑝 = 𝑃 → ( ∀ 𝑓 ∈ 𝑝 ∀ 𝑔 ∈ 𝑝 ( ( 𝑓 ∘f + 𝑔 ) ∈ 𝑝 ∧ ( 𝑓 ∘f · 𝑔 ) ∈ 𝑝 ) ↔ ∀ 𝑓 ∈ 𝑃 ∀ 𝑔 ∈ 𝑃 ( ( 𝑓 ∘f + 𝑔 ) ∈ 𝑃 ∧ ( 𝑓 ∘f · 𝑔 ) ∈ 𝑃 ) ) )
13	7 12	anbi12d	⊢ ( 𝑝 = 𝑃 → ( ( ( ∀ 𝑖 ∈ ℤ ( ( ℤ ↑m 𝑉 ) × { 𝑖 } ) ∈ 𝑝 ∧ ∀ 𝑗 ∈ 𝑉 ( 𝑥 ∈ ( ℤ ↑m 𝑉 ) ↦ ( 𝑥 ‘ 𝑗 ) ) ∈ 𝑝 ) ∧ ∀ 𝑓 ∈ 𝑝 ∀ 𝑔 ∈ 𝑝 ( ( 𝑓 ∘f + 𝑔 ) ∈ 𝑝 ∧ ( 𝑓 ∘f · 𝑔 ) ∈ 𝑝 ) ) ↔ ( ( ∀ 𝑖 ∈ ℤ ( ( ℤ ↑m 𝑉 ) × { 𝑖 } ) ∈ 𝑃 ∧ ∀ 𝑗 ∈ 𝑉 ( 𝑥 ∈ ( ℤ ↑m 𝑉 ) ↦ ( 𝑥 ‘ 𝑗 ) ) ∈ 𝑃 ) ∧ ∀ 𝑓 ∈ 𝑃 ∀ 𝑔 ∈ 𝑃 ( ( 𝑓 ∘f + 𝑔 ) ∈ 𝑃 ∧ ( 𝑓 ∘f · 𝑔 ) ∈ 𝑃 ) ) ) )
14	13	elrab	⊢ ( 𝑃 ∈ { 𝑝 ∈ 𝒫 ( ℤ ↑m ( ℤ ↑m 𝑉 ) ) ∣ ( ( ∀ 𝑖 ∈ ℤ ( ( ℤ ↑m 𝑉 ) × { 𝑖 } ) ∈ 𝑝 ∧ ∀ 𝑗 ∈ 𝑉 ( 𝑥 ∈ ( ℤ ↑m 𝑉 ) ↦ ( 𝑥 ‘ 𝑗 ) ) ∈ 𝑝 ) ∧ ∀ 𝑓 ∈ 𝑝 ∀ 𝑔 ∈ 𝑝 ( ( 𝑓 ∘f + 𝑔 ) ∈ 𝑝 ∧ ( 𝑓 ∘f · 𝑔 ) ∈ 𝑝 ) ) } ↔ ( 𝑃 ∈ 𝒫 ( ℤ ↑m ( ℤ ↑m 𝑉 ) ) ∧ ( ( ∀ 𝑖 ∈ ℤ ( ( ℤ ↑m 𝑉 ) × { 𝑖 } ) ∈ 𝑃 ∧ ∀ 𝑗 ∈ 𝑉 ( 𝑥 ∈ ( ℤ ↑m 𝑉 ) ↦ ( 𝑥 ‘ 𝑗 ) ) ∈ 𝑃 ) ∧ ∀ 𝑓 ∈ 𝑃 ∀ 𝑔 ∈ 𝑃 ( ( 𝑓 ∘f + 𝑔 ) ∈ 𝑃 ∧ ( 𝑓 ∘f · 𝑔 ) ∈ 𝑃 ) ) ) )
15		ovex	⊢ ( ℤ ↑m ( ℤ ↑m 𝑉 ) ) ∈ V
16	15	elpw2	⊢ ( 𝑃 ∈ 𝒫 ( ℤ ↑m ( ℤ ↑m 𝑉 ) ) ↔ 𝑃 ⊆ ( ℤ ↑m ( ℤ ↑m 𝑉 ) ) )
17	16	anbi1i	⊢ ( ( 𝑃 ∈ 𝒫 ( ℤ ↑m ( ℤ ↑m 𝑉 ) ) ∧ ( ( ∀ 𝑖 ∈ ℤ ( ( ℤ ↑m 𝑉 ) × { 𝑖 } ) ∈ 𝑃 ∧ ∀ 𝑗 ∈ 𝑉 ( 𝑥 ∈ ( ℤ ↑m 𝑉 ) ↦ ( 𝑥 ‘ 𝑗 ) ) ∈ 𝑃 ) ∧ ∀ 𝑓 ∈ 𝑃 ∀ 𝑔 ∈ 𝑃 ( ( 𝑓 ∘f + 𝑔 ) ∈ 𝑃 ∧ ( 𝑓 ∘f · 𝑔 ) ∈ 𝑃 ) ) ) ↔ ( 𝑃 ⊆ ( ℤ ↑m ( ℤ ↑m 𝑉 ) ) ∧ ( ( ∀ 𝑖 ∈ ℤ ( ( ℤ ↑m 𝑉 ) × { 𝑖 } ) ∈ 𝑃 ∧ ∀ 𝑗 ∈ 𝑉 ( 𝑥 ∈ ( ℤ ↑m 𝑉 ) ↦ ( 𝑥 ‘ 𝑗 ) ) ∈ 𝑃 ) ∧ ∀ 𝑓 ∈ 𝑃 ∀ 𝑔 ∈ 𝑃 ( ( 𝑓 ∘f + 𝑔 ) ∈ 𝑃 ∧ ( 𝑓 ∘f · 𝑔 ) ∈ 𝑃 ) ) ) )
18	14 17	bitri	⊢ ( 𝑃 ∈ { 𝑝 ∈ 𝒫 ( ℤ ↑m ( ℤ ↑m 𝑉 ) ) ∣ ( ( ∀ 𝑖 ∈ ℤ ( ( ℤ ↑m 𝑉 ) × { 𝑖 } ) ∈ 𝑝 ∧ ∀ 𝑗 ∈ 𝑉 ( 𝑥 ∈ ( ℤ ↑m 𝑉 ) ↦ ( 𝑥 ‘ 𝑗 ) ) ∈ 𝑝 ) ∧ ∀ 𝑓 ∈ 𝑝 ∀ 𝑔 ∈ 𝑝 ( ( 𝑓 ∘f + 𝑔 ) ∈ 𝑝 ∧ ( 𝑓 ∘f · 𝑔 ) ∈ 𝑝 ) ) } ↔ ( 𝑃 ⊆ ( ℤ ↑m ( ℤ ↑m 𝑉 ) ) ∧ ( ( ∀ 𝑖 ∈ ℤ ( ( ℤ ↑m 𝑉 ) × { 𝑖 } ) ∈ 𝑃 ∧ ∀ 𝑗 ∈ 𝑉 ( 𝑥 ∈ ( ℤ ↑m 𝑉 ) ↦ ( 𝑥 ‘ 𝑗 ) ) ∈ 𝑃 ) ∧ ∀ 𝑓 ∈ 𝑃 ∀ 𝑔 ∈ 𝑃 ( ( 𝑓 ∘f + 𝑔 ) ∈ 𝑃 ∧ ( 𝑓 ∘f · 𝑔 ) ∈ 𝑃 ) ) ) )
19	2 18	bitrdi	⊢ ( 𝑉 ∈ V → ( 𝑃 ∈ ( mzPolyCld ‘ 𝑉 ) ↔ ( 𝑃 ⊆ ( ℤ ↑m ( ℤ ↑m 𝑉 ) ) ∧ ( ( ∀ 𝑖 ∈ ℤ ( ( ℤ ↑m 𝑉 ) × { 𝑖 } ) ∈ 𝑃 ∧ ∀ 𝑗 ∈ 𝑉 ( 𝑥 ∈ ( ℤ ↑m 𝑉 ) ↦ ( 𝑥 ‘ 𝑗 ) ) ∈ 𝑃 ) ∧ ∀ 𝑓 ∈ 𝑃 ∀ 𝑔 ∈ 𝑃 ( ( 𝑓 ∘f + 𝑔 ) ∈ 𝑃 ∧ ( 𝑓 ∘f · 𝑔 ) ∈ 𝑃 ) ) ) ) )