Metamath Proof Explorer

Theorem mzpcl1

Description: Defining property 1 of a polynomially closed function set P : it contains all constant functions. (Contributed by Stefan O'Rear, 4-Oct-2014)

		Ref	Expression
	Assertion	mzpcl1	$⊢ (P \in mzPolyCld (V) \land F \in ℤ) \to (ℤ^{V}) \times \{F\} \in P$

Proof

Step	Hyp	Ref	Expression
1		simpr	$⊢ (P \in mzPolyCld (V) \land F \in ℤ) \to F \in ℤ$
2		simpl	$⊢ (P \in mzPolyCld (V) \land F \in ℤ) \to P \in mzPolyCld (V)$
3		elfvex	$⊢ P \in mzPolyCld (V) \to V \in V$
4	3	adantr	$⊢ (P \in mzPolyCld (V) \land F \in ℤ) \to V \in V$
5		elmzpcl	$⊢ V \in V \to (P \in mzPolyCld (V) \leftrightarrow (P \subseteq ℤ^{(ℤ^{V})} \land ((\forall f \in ℤ (ℤ^{V}) \times \{f\} \in P \land \forall f \in V (g \in (ℤ^{V}) ⟼ g (f)) \in P) \land \forall f \in P \forall g \in P (f +_{f} g \in P \land f \times_{f} g \in P))))$
6	4 5	syl	$⊢ (P \in mzPolyCld (V) \land F \in ℤ) \to (P \in mzPolyCld (V) \leftrightarrow (P \subseteq ℤ^{(ℤ^{V})} \land ((\forall f \in ℤ (ℤ^{V}) \times \{f\} \in P \land \forall f \in V (g \in (ℤ^{V}) ⟼ g (f)) \in P) \land \forall f \in P \forall g \in P (f +_{f} g \in P \land f \times_{f} g \in P))))$
7	2 6	mpbid	$⊢ (P \in mzPolyCld (V) \land F \in ℤ) \to (P \subseteq ℤ^{(ℤ^{V})} \land ((\forall f \in ℤ (ℤ^{V}) \times \{f\} \in P \land \forall f \in V (g \in (ℤ^{V}) ⟼ g (f)) \in P) \land \forall f \in P \forall g \in P (f +_{f} g \in P \land f \times_{f} g \in P)))$
8		simprll	$⊢ (P \subseteq ℤ^{(ℤ^{V})} \land ((\forall f \in ℤ (ℤ^{V}) \times \{f\} \in P \land \forall f \in V (g \in (ℤ^{V}) ⟼ g (f)) \in P) \land \forall f \in P \forall g \in P (f +_{f} g \in P \land f \times_{f} g \in P))) \to \forall f \in ℤ (ℤ^{V}) \times \{f\} \in P$
9	7 8	syl	$⊢ (P \in mzPolyCld (V) \land F \in ℤ) \to \forall f \in ℤ (ℤ^{V}) \times \{f\} \in P$
10		sneq	$⊢ f = F \to \{f\} = \{F\}$
11	10	xpeq2d	$⊢ f = F \to (ℤ^{V}) \times \{f\} = (ℤ^{V}) \times \{F\}$
12	11	eleq1d	$⊢ f = F \to ((ℤ^{V}) \times \{f\} \in P \leftrightarrow (ℤ^{V}) \times \{F\} \in P)$
13	12	rspcva	$⊢ (F \in ℤ \land \forall f \in ℤ (ℤ^{V}) \times \{f\} \in P) \to (ℤ^{V}) \times \{F\} \in P$
14	1 9 13	syl2anc	$⊢ (P \in mzPolyCld (V) \land F \in ℤ) \to (ℤ^{V}) \times \{F\} \in P$