mzpincl

Description: Polynomial closedness is a universal first-order property and passes to intersections. This is where the closure properties of the polynomial ring itself are proved. (Contributed by Stefan O'Rear, 4-Oct-2014)

		Ref	Expression
	Assertion	mzpincl	$⊢ V \in V \to mzPoly (V) \in mzPolyCld (V)$

Proof

Step	Hyp	Ref	Expression
1		mzpval	$⊢ V \in V \to mzPoly (V) = ⋂ mzPolyCld (V)$
2		mzpclall	$⊢ V \in V \to ℤ^{(ℤ^{V})} \in mzPolyCld (V)$
3		intss1	$⊢ ℤ^{(ℤ^{V})} \in mzPolyCld (V) \to ⋂ mzPolyCld (V) \subseteq ℤ^{(ℤ^{V})}$
4	2 3	syl	$⊢ V \in V \to ⋂ mzPolyCld (V) \subseteq ℤ^{(ℤ^{V})}$
5		simpr	$⊢ ((V \in V \land f \in ℤ) \land a \in mzPolyCld (V)) \to a \in mzPolyCld (V)$
6		simplr	$⊢ ((V \in V \land f \in ℤ) \land a \in mzPolyCld (V)) \to f \in ℤ$
7		mzpcl1	$⊢ (a \in mzPolyCld (V) \land f \in ℤ) \to (ℤ^{V}) \times \{f\} \in a$
8	5 6 7	syl2anc	$⊢ ((V \in V \land f \in ℤ) \land a \in mzPolyCld (V)) \to (ℤ^{V}) \times \{f\} \in a$
9	8	ralrimiva	$⊢ (V \in V \land f \in ℤ) \to \forall a \in mzPolyCld (V) (ℤ^{V}) \times \{f\} \in a$
10		ovex	$⊢ ℤ^{V} \in V$
11		snex	$⊢ \{f\} \in V$
12	10 11	xpex	$⊢ (ℤ^{V}) \times \{f\} \in V$
13	12	elint2	$⊢ (ℤ^{V}) \times \{f\} \in ⋂ mzPolyCld (V) \leftrightarrow \forall a \in mzPolyCld (V) (ℤ^{V}) \times \{f\} \in a$
14	9 13	sylibr	$⊢ (V \in V \land f \in ℤ) \to (ℤ^{V}) \times \{f\} \in ⋂ mzPolyCld (V)$
15	14	ralrimiva	$⊢ V \in V \to \forall f \in ℤ (ℤ^{V}) \times \{f\} \in ⋂ mzPolyCld (V)$
16		simpr	$⊢ ((V \in V \land f \in V) \land a \in mzPolyCld (V)) \to a \in mzPolyCld (V)$
17		simplr	$⊢ ((V \in V \land f \in V) \land a \in mzPolyCld (V)) \to f \in V$
18		mzpcl2	$⊢ (a \in mzPolyCld (V) \land f \in V) \to (g \in (ℤ^{V}) ⟼ g (f)) \in a$
19	16 17 18	syl2anc	$⊢ ((V \in V \land f \in V) \land a \in mzPolyCld (V)) \to (g \in (ℤ^{V}) ⟼ g (f)) \in a$
20	19	ralrimiva	$⊢ (V \in V \land f \in V) \to \forall a \in mzPolyCld (V) (g \in (ℤ^{V}) ⟼ g (f)) \in a$
21	10	mptex	$⊢ (g \in (ℤ^{V}) ⟼ g (f)) \in V$
22	21	elint2	$⊢ (g \in (ℤ^{V}) ⟼ g (f)) \in ⋂ mzPolyCld (V) \leftrightarrow \forall a \in mzPolyCld (V) (g \in (ℤ^{V}) ⟼ g (f)) \in a$
23	20 22	sylibr	$⊢ (V \in V \land f \in V) \to (g \in (ℤ^{V}) ⟼ g (f)) \in ⋂ mzPolyCld (V)$
24	23	ralrimiva	$⊢ V \in V \to \forall f \in V (g \in (ℤ^{V}) ⟼ g (f)) \in ⋂ mzPolyCld (V)$
25	15 24	jca	$⊢ V \in V \to (\forall f \in ℤ (ℤ^{V}) \times \{f\} \in ⋂ mzPolyCld (V) \land \forall f \in V (g \in (ℤ^{V}) ⟼ g (f)) \in ⋂ mzPolyCld (V))$
26		vex	$⊢ f \in V$
27	26	elint2	$⊢ f \in ⋂ mzPolyCld (V) \leftrightarrow \forall a \in mzPolyCld (V) f \in a$
28		vex	$⊢ g \in V$
29	28	elint2	$⊢ g \in ⋂ mzPolyCld (V) \leftrightarrow \forall a \in mzPolyCld (V) g \in a$
30		mzpcl34	$⊢ (a \in mzPolyCld (V) \land f \in a \land g \in a) \to (f +_{f} g \in a \land f \times_{f} g \in a)$
31	30	3expib	$⊢ a \in mzPolyCld (V) \to ((f \in a \land g \in a) \to (f +_{f} g \in a \land f \times_{f} g \in a))$
32	31	ralimia	$⊢ \forall a \in mzPolyCld (V) (f \in a \land g \in a) \to \forall a \in mzPolyCld (V) (f +_{f} g \in a \land f \times_{f} g \in a)$
33		r19.26	$⊢ \forall a \in mzPolyCld (V) (f \in a \land g \in a) \leftrightarrow (\forall a \in mzPolyCld (V) f \in a \land \forall a \in mzPolyCld (V) g \in a)$
34		r19.26	$⊢ \forall a \in mzPolyCld (V) (f +_{f} g \in a \land f \times_{f} g \in a) \leftrightarrow (\forall a \in mzPolyCld (V) f +_{f} g \in a \land \forall a \in mzPolyCld (V) f \times_{f} g \in a)$
35	32 33 34	3imtr3i	$⊢ (\forall a \in mzPolyCld (V) f \in a \land \forall a \in mzPolyCld (V) g \in a) \to (\forall a \in mzPolyCld (V) f +_{f} g \in a \land \forall a \in mzPolyCld (V) f \times_{f} g \in a)$
36	27 29 35	syl2anb	$⊢ (f \in ⋂ mzPolyCld (V) \land g \in ⋂ mzPolyCld (V)) \to (\forall a \in mzPolyCld (V) f +_{f} g \in a \land \forall a \in mzPolyCld (V) f \times_{f} g \in a)$
37		ovex	$⊢ f +_{f} g \in V$
38	37	elint2	$⊢ f +_{f} g \in ⋂ mzPolyCld (V) \leftrightarrow \forall a \in mzPolyCld (V) f +_{f} g \in a$
39		ovex	$⊢ f \times_{f} g \in V$
40	39	elint2	$⊢ f \times_{f} g \in ⋂ mzPolyCld (V) \leftrightarrow \forall a \in mzPolyCld (V) f \times_{f} g \in a$
41	38 40	anbi12i	$⊢ (f +_{f} g \in ⋂ mzPolyCld (V) \land f \times_{f} g \in ⋂ mzPolyCld (V)) \leftrightarrow (\forall a \in mzPolyCld (V) f +_{f} g \in a \land \forall a \in mzPolyCld (V) f \times_{f} g \in a)$
42	36 41	sylibr	$⊢ (f \in ⋂ mzPolyCld (V) \land g \in ⋂ mzPolyCld (V)) \to (f +_{f} g \in ⋂ mzPolyCld (V) \land f \times_{f} g \in ⋂ mzPolyCld (V))$
43	42	a1i	$⊢ V \in V \to ((f \in ⋂ mzPolyCld (V) \land g \in ⋂ mzPolyCld (V)) \to (f +_{f} g \in ⋂ mzPolyCld (V) \land f \times_{f} g \in ⋂ mzPolyCld (V)))$
44	43	ralrimivv	$⊢ V \in V \to \forall f \in ⋂ mzPolyCld (V) \forall g \in ⋂ mzPolyCld (V) (f +_{f} g \in ⋂ mzPolyCld (V) \land f \times_{f} g \in ⋂ mzPolyCld (V))$
45	4 25 44	jca32	$⊢ V \in V \to (⋂ mzPolyCld (V) \subseteq ℤ^{(ℤ^{V})} \land ((\forall f \in ℤ (ℤ^{V}) \times \{f\} \in ⋂ mzPolyCld (V) \land \forall f \in V (g \in (ℤ^{V}) ⟼ g (f)) \in ⋂ mzPolyCld (V)) \land \forall f \in ⋂ mzPolyCld (V) \forall g \in ⋂ mzPolyCld (V) (f +_{f} g \in ⋂ mzPolyCld (V) \land f \times_{f} g \in ⋂ mzPolyCld (V))))$
46		elmzpcl	$⊢ V \in V \to (⋂ mzPolyCld (V) \in mzPolyCld (V) \leftrightarrow (⋂ mzPolyCld (V) \subseteq ℤ^{(ℤ^{V})} \land ((\forall f \in ℤ (ℤ^{V}) \times \{f\} \in ⋂ mzPolyCld (V) \land \forall f \in V (g \in (ℤ^{V}) ⟼ g (f)) \in ⋂ mzPolyCld (V)) \land \forall f \in ⋂ mzPolyCld (V) \forall g \in ⋂ mzPolyCld (V) (f +_{f} g \in ⋂ mzPolyCld (V) \land f \times_{f} g \in ⋂ mzPolyCld (V)))))$
47	45 46	mpbird	$⊢ V \in V \to ⋂ mzPolyCld (V) \in mzPolyCld (V)$
48	1 47	eqeltrd	$⊢ V \in V \to mzPoly (V) \in mzPolyCld (V)$

Metamath Proof Explorer

Theorem mzpincl

Proof