mzpcl34

Description: Defining properties 3 and 4 of a polynomially closed function set P : it is closed under pointwise addition and multiplication. (Contributed by Stefan O'Rear, 4-Oct-2014)

		Ref	Expression
	Assertion	mzpcl34	$⊢ (P \in mzPolyCld (V) \land F \in P \land G \in P) \to (F +_{f} G \in P \land F \times_{f} G \in P)$

Proof

Step	Hyp	Ref	Expression
1		simp2	$⊢ (P \in mzPolyCld (V) \land F \in P \land G \in P) \to F \in P$
2		simp3	$⊢ (P \in mzPolyCld (V) \land F \in P \land G \in P) \to G \in P$
3		simp1	$⊢ (P \in mzPolyCld (V) \land F \in P \land G \in P) \to P \in mzPolyCld (V)$
4	3	elfvexd	$⊢ (P \in mzPolyCld (V) \land F \in P \land G \in P) \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 P \land G \in P) \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	3 6	mpbid	$⊢ (P \in mzPolyCld (V) \land F \in P \land G \in P) \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	7	simprrd	$⊢ (P \in mzPolyCld (V) \land F \in P \land G \in P) \to \forall f \in P \forall g \in P (f +_{f} g \in P \land f \times_{f} g \in P)$
9		oveq1	$⊢ f = F \to f +_{f} g = F +_{f} g$
10	9	eleq1d	$⊢ f = F \to (f +_{f} g \in P \leftrightarrow F +_{f} g \in P)$
11		oveq1	$⊢ f = F \to f \times_{f} g = F \times_{f} g$
12	11	eleq1d	$⊢ f = F \to (f \times_{f} g \in P \leftrightarrow F \times_{f} g \in P)$
13	10 12	anbi12d	$⊢ f = F \to ((f +_{f} g \in P \land f \times_{f} g \in P) \leftrightarrow (F +_{f} g \in P \land F \times_{f} g \in P))$
14		oveq2	$⊢ g = G \to F +_{f} g = F +_{f} G$
15	14	eleq1d	$⊢ g = G \to (F +_{f} g \in P \leftrightarrow F +_{f} G \in P)$
16		oveq2	$⊢ g = G \to F \times_{f} g = F \times_{f} G$
17	16	eleq1d	$⊢ g = G \to (F \times_{f} g \in P \leftrightarrow F \times_{f} G \in P)$
18	15 17	anbi12d	$⊢ g = G \to ((F +_{f} g \in P \land F \times_{f} g \in P) \leftrightarrow (F +_{f} G \in P \land F \times_{f} G \in P))$
19	13 18	rspc2va	$⊢ ((F \in P \land G \in P) \land \forall f \in P \forall g \in P (f +_{f} g \in P \land f \times_{f} g \in P)) \to (F +_{f} G \in P \land F \times_{f} G \in P)$
20	1 2 8 19	syl21anc	$⊢ (P \in mzPolyCld (V) \land F \in P \land G \in P) \to (F +_{f} G \in P \land F \times_{f} G \in P)$

Metamath Proof Explorer

Theorem mzpcl34

Proof