mzpsubst

Description: Substituting polynomials for the variables of a polynomial results in a polynomial. G is expected to depend on y and provide the polynomials which are being substituted. (Contributed by Stefan O'Rear, 5-Oct-2014)

		Ref	Expression
	Assertion	mzpsubst	$⊢ (W \in V \land F \in mzPoly (V) \land \forall y \in V G \in mzPoly (W)) \to (x \in (ℤ^{W}) ⟼ F ((y \in V ⟼ G (x)))) \in mzPoly (W)$

Proof

Step	Hyp	Ref	Expression
1		simp1	$⊢ (W \in V \land F \in mzPoly (V) \land \forall y \in V G \in mzPoly (W)) \to W \in V$
2		elfvex	$⊢ F \in mzPoly (V) \to V \in V$
3	2	3ad2ant2	$⊢ (W \in V \land F \in mzPoly (V) \land \forall y \in V G \in mzPoly (W)) \to V \in V$
4		simp3	$⊢ (W \in V \land F \in mzPoly (V) \land \forall y \in V G \in mzPoly (W)) \to \forall y \in V G \in mzPoly (W)$
5		simp2	$⊢ (W \in V \land F \in mzPoly (V) \land \forall y \in V G \in mzPoly (W)) \to F \in mzPoly (V)$
6		simpr	$⊢ (((W \in V \land V \in V \land \forall y \in V G \in mzPoly (W)) \land b \in ℤ) \land x \in (ℤ^{W})) \to x \in (ℤ^{W})$
7		simpll3	$⊢ (((W \in V \land V \in V \land \forall y \in V G \in mzPoly (W)) \land b \in ℤ) \land x \in (ℤ^{W})) \to \forall y \in V G \in mzPoly (W)$
8		simpll2	$⊢ (((W \in V \land V \in V \land \forall y \in V G \in mzPoly (W)) \land b \in ℤ) \land x \in (ℤ^{W})) \to V \in V$
9		mzpf	$⊢ G \in mzPoly (W) \to G : ℤ^{W} ⟶ ℤ$
10	9	ffvelcdmda	$⊢ (G \in mzPoly (W) \land x \in (ℤ^{W})) \to G (x) \in ℤ$
11	10	expcom	$⊢ x \in (ℤ^{W}) \to (G \in mzPoly (W) \to G (x) \in ℤ)$
12	11	ralimdv	$⊢ x \in (ℤ^{W}) \to (\forall y \in V G \in mzPoly (W) \to \forall y \in V G (x) \in ℤ)$
13	12	imp	$⊢ (x \in (ℤ^{W}) \land \forall y \in V G \in mzPoly (W)) \to \forall y \in V G (x) \in ℤ$
14		eqid	$⊢ (y \in V ⟼ G (x)) = (y \in V ⟼ G (x))$
15	14	fmpt	$⊢ \forall y \in V G (x) \in ℤ \leftrightarrow (y \in V ⟼ G (x)) : V ⟶ ℤ$
16	13 15	sylib	$⊢ (x \in (ℤ^{W}) \land \forall y \in V G \in mzPoly (W)) \to (y \in V ⟼ G (x)) : V ⟶ ℤ$
17	16	adantr	$⊢ ((x \in (ℤ^{W}) \land \forall y \in V G \in mzPoly (W)) \land V \in V) \to (y \in V ⟼ G (x)) : V ⟶ ℤ$
18		zex	$⊢ ℤ \in V$
19		simpr	$⊢ ((x \in (ℤ^{W}) \land \forall y \in V G \in mzPoly (W)) \land V \in V) \to V \in V$
20		elmapg	$⊢ (ℤ \in V \land V \in V) \to ((y \in V ⟼ G (x)) \in (ℤ^{V}) \leftrightarrow (y \in V ⟼ G (x)) : V ⟶ ℤ)$
21	18 19 20	sylancr	$⊢ ((x \in (ℤ^{W}) \land \forall y \in V G \in mzPoly (W)) \land V \in V) \to ((y \in V ⟼ G (x)) \in (ℤ^{V}) \leftrightarrow (y \in V ⟼ G (x)) : V ⟶ ℤ)$
22	17 21	mpbird	$⊢ ((x \in (ℤ^{W}) \land \forall y \in V G \in mzPoly (W)) \land V \in V) \to (y \in V ⟼ G (x)) \in (ℤ^{V})$
23	6 7 8 22	syl21anc	$⊢ (((W \in V \land V \in V \land \forall y \in V G \in mzPoly (W)) \land b \in ℤ) \land x \in (ℤ^{W})) \to (y \in V ⟼ G (x)) \in (ℤ^{V})$
24		vex	$⊢ b \in V$
25	24	fvconst2	$⊢ (y \in V ⟼ G (x)) \in (ℤ^{V}) \to ((ℤ^{V}) \times \{b\}) ((y \in V ⟼ G (x))) = b$
26	23 25	syl	$⊢ (((W \in V \land V \in V \land \forall y \in V G \in mzPoly (W)) \land b \in ℤ) \land x \in (ℤ^{W})) \to ((ℤ^{V}) \times \{b\}) ((y \in V ⟼ G (x))) = b$
27	26	mpteq2dva	$⊢ ((W \in V \land V \in V \land \forall y \in V G \in mzPoly (W)) \land b \in ℤ) \to (x \in (ℤ^{W}) ⟼ ((ℤ^{V}) \times \{b\}) ((y \in V ⟼ G (x)))) = (x \in (ℤ^{W}) ⟼ b)$
28		mzpconstmpt	$⊢ (W \in V \land b \in ℤ) \to (x \in (ℤ^{W}) ⟼ b) \in mzPoly (W)$
29	28	3ad2antl1	$⊢ ((W \in V \land V \in V \land \forall y \in V G \in mzPoly (W)) \land b \in ℤ) \to (x \in (ℤ^{W}) ⟼ b) \in mzPoly (W)$
30	27 29	eqeltrd	$⊢ ((W \in V \land V \in V \land \forall y \in V G \in mzPoly (W)) \land b \in ℤ) \to (x \in (ℤ^{W}) ⟼ ((ℤ^{V}) \times \{b\}) ((y \in V ⟼ G (x)))) \in mzPoly (W)$
31		simpr	$⊢ (((W \in V \land V \in V \land \forall y \in V G \in mzPoly (W)) \land b \in V) \land x \in (ℤ^{W})) \to x \in (ℤ^{W})$
32		simpll3	$⊢ (((W \in V \land V \in V \land \forall y \in V G \in mzPoly (W)) \land b \in V) \land x \in (ℤ^{W})) \to \forall y \in V G \in mzPoly (W)$
33		simpll2	$⊢ (((W \in V \land V \in V \land \forall y \in V G \in mzPoly (W)) \land b \in V) \land x \in (ℤ^{W})) \to V \in V$
34	31 32 33 22	syl21anc	$⊢ (((W \in V \land V \in V \land \forall y \in V G \in mzPoly (W)) \land b \in V) \land x \in (ℤ^{W})) \to (y \in V ⟼ G (x)) \in (ℤ^{V})$
35		fveq1	$⊢ c = (y \in V ⟼ G (x)) \to c (b) = (y \in V ⟼ G (x)) (b)$
36		eqid	$⊢ (c \in (ℤ^{V}) ⟼ c (b)) = (c \in (ℤ^{V}) ⟼ c (b))$
37		fvex	$⊢ (y \in V ⟼ G (x)) (b) \in V$
38	35 36 37	fvmpt	$⊢ (y \in V ⟼ G (x)) \in (ℤ^{V}) \to (c \in (ℤ^{V}) ⟼ c (b)) ((y \in V ⟼ G (x))) = (y \in V ⟼ G (x)) (b)$
39	34 38	syl	$⊢ (((W \in V \land V \in V \land \forall y \in V G \in mzPoly (W)) \land b \in V) \land x \in (ℤ^{W})) \to (c \in (ℤ^{V}) ⟼ c (b)) ((y \in V ⟼ G (x))) = (y \in V ⟼ G (x)) (b)$
40		simplr	$⊢ (((W \in V \land V \in V \land \forall y \in V G \in mzPoly (W)) \land b \in V) \land x \in (ℤ^{W})) \to b \in V$
41		fvex	$⊢ ⦋ b / y ⦌ G (x) \in V$
42		csbeq1	$⊢ a = b \to ⦋ a / y ⦌ G = ⦋ b / y ⦌ G$
43	42	fveq1d	$⊢ a = b \to ⦋ a / y ⦌ G (x) = ⦋ b / y ⦌ G (x)$
44		nfcv	$⊢ \underline{Ⅎ} a G (x)$
45		nfcsb1v	$⊢ \underline{Ⅎ} y ⦋ a / y ⦌ G$
46		nfcv	$⊢ \underline{Ⅎ} y x$
47	45 46	nffv	$⊢ \underline{Ⅎ} y ⦋ a / y ⦌ G (x)$
48		csbeq1a	$⊢ y = a \to G = ⦋ a / y ⦌ G$
49	48	fveq1d	$⊢ y = a \to G (x) = ⦋ a / y ⦌ G (x)$
50	44 47 49	cbvmpt	$⊢ (y \in V ⟼ G (x)) = (a \in V ⟼ ⦋ a / y ⦌ G (x))$
51	43 50	fvmptg	$⊢ (b \in V \land ⦋ b / y ⦌ G (x) \in V) \to (y \in V ⟼ G (x)) (b) = ⦋ b / y ⦌ G (x)$
52	40 41 51	sylancl	$⊢ (((W \in V \land V \in V \land \forall y \in V G \in mzPoly (W)) \land b \in V) \land x \in (ℤ^{W})) \to (y \in V ⟼ G (x)) (b) = ⦋ b / y ⦌ G (x)$
53	39 52	eqtrd	$⊢ (((W \in V \land V \in V \land \forall y \in V G \in mzPoly (W)) \land b \in V) \land x \in (ℤ^{W})) \to (c \in (ℤ^{V}) ⟼ c (b)) ((y \in V ⟼ G (x))) = ⦋ b / y ⦌ G (x)$
54	53	mpteq2dva	$⊢ ((W \in V \land V \in V \land \forall y \in V G \in mzPoly (W)) \land b \in V) \to (x \in (ℤ^{W}) ⟼ (c \in (ℤ^{V}) ⟼ c (b)) ((y \in V ⟼ G (x)))) = (x \in (ℤ^{W}) ⟼ ⦋ b / y ⦌ G (x))$
55		simpr	$⊢ ((W \in V \land V \in V \land \forall y \in V G \in mzPoly (W)) \land b \in V) \to b \in V$
56		simpl3	$⊢ ((W \in V \land V \in V \land \forall y \in V G \in mzPoly (W)) \land b \in V) \to \forall y \in V G \in mzPoly (W)$
57		nfcsb1v	$⊢ \underline{Ⅎ} y ⦋ b / y ⦌ G$
58	57	nfel1	$⊢ Ⅎ y ⦋ b / y ⦌ G \in mzPoly (W)$
59		csbeq1a	$⊢ y = b \to G = ⦋ b / y ⦌ G$
60	59	eleq1d	$⊢ y = b \to (G \in mzPoly (W) \leftrightarrow ⦋ b / y ⦌ G \in mzPoly (W))$
61	58 60	rspc	$⊢ b \in V \to (\forall y \in V G \in mzPoly (W) \to ⦋ b / y ⦌ G \in mzPoly (W))$
62	55 56 61	sylc	$⊢ ((W \in V \land V \in V \land \forall y \in V G \in mzPoly (W)) \land b \in V) \to ⦋ b / y ⦌ G \in mzPoly (W)$
63		mzpf	$⊢ ⦋ b / y ⦌ G \in mzPoly (W) \to ⦋ b / y ⦌ G : ℤ^{W} ⟶ ℤ$
64	62 63	syl	$⊢ ((W \in V \land V \in V \land \forall y \in V G \in mzPoly (W)) \land b \in V) \to ⦋ b / y ⦌ G : ℤ^{W} ⟶ ℤ$
65	64	feqmptd	$⊢ ((W \in V \land V \in V \land \forall y \in V G \in mzPoly (W)) \land b \in V) \to ⦋ b / y ⦌ G = (x \in (ℤ^{W}) ⟼ ⦋ b / y ⦌ G (x))$
66	54 65	eqtr4d	$⊢ ((W \in V \land V \in V \land \forall y \in V G \in mzPoly (W)) \land b \in V) \to (x \in (ℤ^{W}) ⟼ (c \in (ℤ^{V}) ⟼ c (b)) ((y \in V ⟼ G (x)))) = ⦋ b / y ⦌ G$
67	66 62	eqeltrd	$⊢ ((W \in V \land V \in V \land \forall y \in V G \in mzPoly (W)) \land b \in V) \to (x \in (ℤ^{W}) ⟼ (c \in (ℤ^{V}) ⟼ c (b)) ((y \in V ⟼ G (x)))) \in mzPoly (W)$
68		simp2l	$⊢ ((W \in V \land V \in V \land \forall y \in V G \in mzPoly (W)) \land (b : ℤ^{V} ⟶ ℤ \land (x \in (ℤ^{W}) ⟼ b ((y \in V ⟼ G (x)))) \in mzPoly (W)) \land (c : ℤ^{V} ⟶ ℤ \land (x \in (ℤ^{W}) ⟼ c ((y \in V ⟼ G (x)))) \in mzPoly (W))) \to b : ℤ^{V} ⟶ ℤ$
69	68	ffnd	$⊢ ((W \in V \land V \in V \land \forall y \in V G \in mzPoly (W)) \land (b : ℤ^{V} ⟶ ℤ \land (x \in (ℤ^{W}) ⟼ b ((y \in V ⟼ G (x)))) \in mzPoly (W)) \land (c : ℤ^{V} ⟶ ℤ \land (x \in (ℤ^{W}) ⟼ c ((y \in V ⟼ G (x)))) \in mzPoly (W))) \to b Fn (ℤ^{V})$
70		simp3l	$⊢ ((W \in V \land V \in V \land \forall y \in V G \in mzPoly (W)) \land (b : ℤ^{V} ⟶ ℤ \land (x \in (ℤ^{W}) ⟼ b ((y \in V ⟼ G (x)))) \in mzPoly (W)) \land (c : ℤ^{V} ⟶ ℤ \land (x \in (ℤ^{W}) ⟼ c ((y \in V ⟼ G (x)))) \in mzPoly (W))) \to c : ℤ^{V} ⟶ ℤ$
71	70	ffnd	$⊢ ((W \in V \land V \in V \land \forall y \in V G \in mzPoly (W)) \land (b : ℤ^{V} ⟶ ℤ \land (x \in (ℤ^{W}) ⟼ b ((y \in V ⟼ G (x)))) \in mzPoly (W)) \land (c : ℤ^{V} ⟶ ℤ \land (x \in (ℤ^{W}) ⟼ c ((y \in V ⟼ G (x)))) \in mzPoly (W))) \to c Fn (ℤ^{V})$
72		simp13	$⊢ ((W \in V \land V \in V \land \forall y \in V G \in mzPoly (W)) \land (b : ℤ^{V} ⟶ ℤ \land (x \in (ℤ^{W}) ⟼ b ((y \in V ⟼ G (x)))) \in mzPoly (W)) \land (c : ℤ^{V} ⟶ ℤ \land (x \in (ℤ^{W}) ⟼ c ((y \in V ⟼ G (x)))) \in mzPoly (W))) \to \forall y \in V G \in mzPoly (W)$
73		simp12	$⊢ ((W \in V \land V \in V \land \forall y \in V G \in mzPoly (W)) \land (b : ℤ^{V} ⟶ ℤ \land (x \in (ℤ^{W}) ⟼ b ((y \in V ⟼ G (x)))) \in mzPoly (W)) \land (c : ℤ^{V} ⟶ ℤ \land (x \in (ℤ^{W}) ⟼ c ((y \in V ⟼ G (x)))) \in mzPoly (W))) \to V \in V$
74		simplll	$⊢ (((b Fn (ℤ^{V}) \land c Fn (ℤ^{V})) \land (\forall y \in V G \in mzPoly (W) \land V \in V)) \land x \in (ℤ^{W})) \to b Fn (ℤ^{V})$
75		simpllr	$⊢ (((b Fn (ℤ^{V}) \land c Fn (ℤ^{V})) \land (\forall y \in V G \in mzPoly (W) \land V \in V)) \land x \in (ℤ^{W})) \to c Fn (ℤ^{V})$
76		ovexd	$⊢ (((b Fn (ℤ^{V}) \land c Fn (ℤ^{V})) \land (\forall y \in V G \in mzPoly (W) \land V \in V)) \land x \in (ℤ^{W})) \to ℤ^{V} \in V$
77		simpr	$⊢ (((b Fn (ℤ^{V}) \land c Fn (ℤ^{V})) \land (\forall y \in V G \in mzPoly (W) \land V \in V)) \land x \in (ℤ^{W})) \to x \in (ℤ^{W})$
78		simplrl	$⊢ (((b Fn (ℤ^{V}) \land c Fn (ℤ^{V})) \land (\forall y \in V G \in mzPoly (W) \land V \in V)) \land x \in (ℤ^{W})) \to \forall y \in V G \in mzPoly (W)$
79	77 78 12	sylc	$⊢ (((b Fn (ℤ^{V}) \land c Fn (ℤ^{V})) \land (\forall y \in V G \in mzPoly (W) \land V \in V)) \land x \in (ℤ^{W})) \to \forall y \in V G (x) \in ℤ$
80	79 15	sylib	$⊢ (((b Fn (ℤ^{V}) \land c Fn (ℤ^{V})) \land (\forall y \in V G \in mzPoly (W) \land V \in V)) \land x \in (ℤ^{W})) \to (y \in V ⟼ G (x)) : V ⟶ ℤ$
81		simplrr	$⊢ (((b Fn (ℤ^{V}) \land c Fn (ℤ^{V})) \land (\forall y \in V G \in mzPoly (W) \land V \in V)) \land x \in (ℤ^{W})) \to V \in V$
82	18 81 20	sylancr	$⊢ (((b Fn (ℤ^{V}) \land c Fn (ℤ^{V})) \land (\forall y \in V G \in mzPoly (W) \land V \in V)) \land x \in (ℤ^{W})) \to ((y \in V ⟼ G (x)) \in (ℤ^{V}) \leftrightarrow (y \in V ⟼ G (x)) : V ⟶ ℤ)$
83	80 82	mpbird	$⊢ (((b Fn (ℤ^{V}) \land c Fn (ℤ^{V})) \land (\forall y \in V G \in mzPoly (W) \land V \in V)) \land x \in (ℤ^{W})) \to (y \in V ⟼ G (x)) \in (ℤ^{V})$
84		fnfvof	$⊢ ((b Fn (ℤ^{V}) \land c Fn (ℤ^{V})) \land (ℤ^{V} \in V \land (y \in V ⟼ G (x)) \in (ℤ^{V}))) \to (b +_{f} c) ((y \in V ⟼ G (x))) = b ((y \in V ⟼ G (x))) + c ((y \in V ⟼ G (x)))$
85	74 75 76 83 84	syl22anc	$⊢ (((b Fn (ℤ^{V}) \land c Fn (ℤ^{V})) \land (\forall y \in V G \in mzPoly (W) \land V \in V)) \land x \in (ℤ^{W})) \to (b +_{f} c) ((y \in V ⟼ G (x))) = b ((y \in V ⟼ G (x))) + c ((y \in V ⟼ G (x)))$
86	85	mpteq2dva	$⊢ ((b Fn (ℤ^{V}) \land c Fn (ℤ^{V})) \land (\forall y \in V G \in mzPoly (W) \land V \in V)) \to (x \in (ℤ^{W}) ⟼ (b +_{f} c) ((y \in V ⟼ G (x)))) = (x \in (ℤ^{W}) ⟼ b ((y \in V ⟼ G (x))) + c ((y \in V ⟼ G (x))))$
87	69 71 72 73 86	syl22anc	$⊢ ((W \in V \land V \in V \land \forall y \in V G \in mzPoly (W)) \land (b : ℤ^{V} ⟶ ℤ \land (x \in (ℤ^{W}) ⟼ b ((y \in V ⟼ G (x)))) \in mzPoly (W)) \land (c : ℤ^{V} ⟶ ℤ \land (x \in (ℤ^{W}) ⟼ c ((y \in V ⟼ G (x)))) \in mzPoly (W))) \to (x \in (ℤ^{W}) ⟼ (b +_{f} c) ((y \in V ⟼ G (x)))) = (x \in (ℤ^{W}) ⟼ b ((y \in V ⟼ G (x))) + c ((y \in V ⟼ G (x))))$
88		simp2r	$⊢ ((W \in V \land V \in V \land \forall y \in V G \in mzPoly (W)) \land (b : ℤ^{V} ⟶ ℤ \land (x \in (ℤ^{W}) ⟼ b ((y \in V ⟼ G (x)))) \in mzPoly (W)) \land (c : ℤ^{V} ⟶ ℤ \land (x \in (ℤ^{W}) ⟼ c ((y \in V ⟼ G (x)))) \in mzPoly (W))) \to (x \in (ℤ^{W}) ⟼ b ((y \in V ⟼ G (x)))) \in mzPoly (W)$
89		simp3r	$⊢ ((W \in V \land V \in V \land \forall y \in V G \in mzPoly (W)) \land (b : ℤ^{V} ⟶ ℤ \land (x \in (ℤ^{W}) ⟼ b ((y \in V ⟼ G (x)))) \in mzPoly (W)) \land (c : ℤ^{V} ⟶ ℤ \land (x \in (ℤ^{W}) ⟼ c ((y \in V ⟼ G (x)))) \in mzPoly (W))) \to (x \in (ℤ^{W}) ⟼ c ((y \in V ⟼ G (x)))) \in mzPoly (W)$
90		mzpaddmpt	$⊢ ((x \in (ℤ^{W}) ⟼ b ((y \in V ⟼ G (x)))) \in mzPoly (W) \land (x \in (ℤ^{W}) ⟼ c ((y \in V ⟼ G (x)))) \in mzPoly (W)) \to (x \in (ℤ^{W}) ⟼ b ((y \in V ⟼ G (x))) + c ((y \in V ⟼ G (x)))) \in mzPoly (W)$
91	88 89 90	syl2anc	$⊢ ((W \in V \land V \in V \land \forall y \in V G \in mzPoly (W)) \land (b : ℤ^{V} ⟶ ℤ \land (x \in (ℤ^{W}) ⟼ b ((y \in V ⟼ G (x)))) \in mzPoly (W)) \land (c : ℤ^{V} ⟶ ℤ \land (x \in (ℤ^{W}) ⟼ c ((y \in V ⟼ G (x)))) \in mzPoly (W))) \to (x \in (ℤ^{W}) ⟼ b ((y \in V ⟼ G (x))) + c ((y \in V ⟼ G (x)))) \in mzPoly (W)$
92	87 91	eqeltrd	$⊢ ((W \in V \land V \in V \land \forall y \in V G \in mzPoly (W)) \land (b : ℤ^{V} ⟶ ℤ \land (x \in (ℤ^{W}) ⟼ b ((y \in V ⟼ G (x)))) \in mzPoly (W)) \land (c : ℤ^{V} ⟶ ℤ \land (x \in (ℤ^{W}) ⟼ c ((y \in V ⟼ G (x)))) \in mzPoly (W))) \to (x \in (ℤ^{W}) ⟼ (b +_{f} c) ((y \in V ⟼ G (x)))) \in mzPoly (W)$
93		fnfvof	$⊢ ((b Fn (ℤ^{V}) \land c Fn (ℤ^{V})) \land (ℤ^{V} \in V \land (y \in V ⟼ G (x)) \in (ℤ^{V}))) \to (b \times_{f} c) ((y \in V ⟼ G (x))) = b ((y \in V ⟼ G (x))) c ((y \in V ⟼ G (x)))$
94	74 75 76 83 93	syl22anc	$⊢ (((b Fn (ℤ^{V}) \land c Fn (ℤ^{V})) \land (\forall y \in V G \in mzPoly (W) \land V \in V)) \land x \in (ℤ^{W})) \to (b \times_{f} c) ((y \in V ⟼ G (x))) = b ((y \in V ⟼ G (x))) c ((y \in V ⟼ G (x)))$
95	94	mpteq2dva	$⊢ ((b Fn (ℤ^{V}) \land c Fn (ℤ^{V})) \land (\forall y \in V G \in mzPoly (W) \land V \in V)) \to (x \in (ℤ^{W}) ⟼ (b \times_{f} c) ((y \in V ⟼ G (x)))) = (x \in (ℤ^{W}) ⟼ b ((y \in V ⟼ G (x))) c ((y \in V ⟼ G (x))))$
96	69 71 72 73 95	syl22anc	$⊢ ((W \in V \land V \in V \land \forall y \in V G \in mzPoly (W)) \land (b : ℤ^{V} ⟶ ℤ \land (x \in (ℤ^{W}) ⟼ b ((y \in V ⟼ G (x)))) \in mzPoly (W)) \land (c : ℤ^{V} ⟶ ℤ \land (x \in (ℤ^{W}) ⟼ c ((y \in V ⟼ G (x)))) \in mzPoly (W))) \to (x \in (ℤ^{W}) ⟼ (b \times_{f} c) ((y \in V ⟼ G (x)))) = (x \in (ℤ^{W}) ⟼ b ((y \in V ⟼ G (x))) c ((y \in V ⟼ G (x))))$
97		mzpmulmpt	$⊢ ((x \in (ℤ^{W}) ⟼ b ((y \in V ⟼ G (x)))) \in mzPoly (W) \land (x \in (ℤ^{W}) ⟼ c ((y \in V ⟼ G (x)))) \in mzPoly (W)) \to (x \in (ℤ^{W}) ⟼ b ((y \in V ⟼ G (x))) c ((y \in V ⟼ G (x)))) \in mzPoly (W)$
98	88 89 97	syl2anc	$⊢ ((W \in V \land V \in V \land \forall y \in V G \in mzPoly (W)) \land (b : ℤ^{V} ⟶ ℤ \land (x \in (ℤ^{W}) ⟼ b ((y \in V ⟼ G (x)))) \in mzPoly (W)) \land (c : ℤ^{V} ⟶ ℤ \land (x \in (ℤ^{W}) ⟼ c ((y \in V ⟼ G (x)))) \in mzPoly (W))) \to (x \in (ℤ^{W}) ⟼ b ((y \in V ⟼ G (x))) c ((y \in V ⟼ G (x)))) \in mzPoly (W)$
99	96 98	eqeltrd	$⊢ ((W \in V \land V \in V \land \forall y \in V G \in mzPoly (W)) \land (b : ℤ^{V} ⟶ ℤ \land (x \in (ℤ^{W}) ⟼ b ((y \in V ⟼ G (x)))) \in mzPoly (W)) \land (c : ℤ^{V} ⟶ ℤ \land (x \in (ℤ^{W}) ⟼ c ((y \in V ⟼ G (x)))) \in mzPoly (W))) \to (x \in (ℤ^{W}) ⟼ (b \times_{f} c) ((y \in V ⟼ G (x)))) \in mzPoly (W)$
100		fveq1	$⊢ a = (ℤ^{V}) \times \{b\} \to a ((y \in V ⟼ G (x))) = ((ℤ^{V}) \times \{b\}) ((y \in V ⟼ G (x)))$
101	100	mpteq2dv	$⊢ a = (ℤ^{V}) \times \{b\} \to (x \in (ℤ^{W}) ⟼ a ((y \in V ⟼ G (x)))) = (x \in (ℤ^{W}) ⟼ ((ℤ^{V}) \times \{b\}) ((y \in V ⟼ G (x))))$
102	101	eleq1d	$⊢ a = (ℤ^{V}) \times \{b\} \to ((x \in (ℤ^{W}) ⟼ a ((y \in V ⟼ G (x)))) \in mzPoly (W) \leftrightarrow (x \in (ℤ^{W}) ⟼ ((ℤ^{V}) \times \{b\}) ((y \in V ⟼ G (x)))) \in mzPoly (W))$
103		fveq1	$⊢ a = (c \in (ℤ^{V}) ⟼ c (b)) \to a ((y \in V ⟼ G (x))) = (c \in (ℤ^{V}) ⟼ c (b)) ((y \in V ⟼ G (x)))$
104	103	mpteq2dv	$⊢ a = (c \in (ℤ^{V}) ⟼ c (b)) \to (x \in (ℤ^{W}) ⟼ a ((y \in V ⟼ G (x)))) = (x \in (ℤ^{W}) ⟼ (c \in (ℤ^{V}) ⟼ c (b)) ((y \in V ⟼ G (x))))$
105	104	eleq1d	$⊢ a = (c \in (ℤ^{V}) ⟼ c (b)) \to ((x \in (ℤ^{W}) ⟼ a ((y \in V ⟼ G (x)))) \in mzPoly (W) \leftrightarrow (x \in (ℤ^{W}) ⟼ (c \in (ℤ^{V}) ⟼ c (b)) ((y \in V ⟼ G (x)))) \in mzPoly (W))$
106		fveq1	$⊢ a = b \to a ((y \in V ⟼ G (x))) = b ((y \in V ⟼ G (x)))$
107	106	mpteq2dv	$⊢ a = b \to (x \in (ℤ^{W}) ⟼ a ((y \in V ⟼ G (x)))) = (x \in (ℤ^{W}) ⟼ b ((y \in V ⟼ G (x))))$
108	107	eleq1d	$⊢ a = b \to ((x \in (ℤ^{W}) ⟼ a ((y \in V ⟼ G (x)))) \in mzPoly (W) \leftrightarrow (x \in (ℤ^{W}) ⟼ b ((y \in V ⟼ G (x)))) \in mzPoly (W))$
109		fveq1	$⊢ a = c \to a ((y \in V ⟼ G (x))) = c ((y \in V ⟼ G (x)))$
110	109	mpteq2dv	$⊢ a = c \to (x \in (ℤ^{W}) ⟼ a ((y \in V ⟼ G (x)))) = (x \in (ℤ^{W}) ⟼ c ((y \in V ⟼ G (x))))$
111	110	eleq1d	$⊢ a = c \to ((x \in (ℤ^{W}) ⟼ a ((y \in V ⟼ G (x)))) \in mzPoly (W) \leftrightarrow (x \in (ℤ^{W}) ⟼ c ((y \in V ⟼ G (x)))) \in mzPoly (W))$
112		fveq1	$⊢ a = b +_{f} c \to a ((y \in V ⟼ G (x))) = (b +_{f} c) ((y \in V ⟼ G (x)))$
113	112	mpteq2dv	$⊢ a = b +_{f} c \to (x \in (ℤ^{W}) ⟼ a ((y \in V ⟼ G (x)))) = (x \in (ℤ^{W}) ⟼ (b +_{f} c) ((y \in V ⟼ G (x))))$
114	113	eleq1d	$⊢ a = b +_{f} c \to ((x \in (ℤ^{W}) ⟼ a ((y \in V ⟼ G (x)))) \in mzPoly (W) \leftrightarrow (x \in (ℤ^{W}) ⟼ (b +_{f} c) ((y \in V ⟼ G (x)))) \in mzPoly (W))$
115		fveq1	$⊢ a = b \times_{f} c \to a ((y \in V ⟼ G (x))) = (b \times_{f} c) ((y \in V ⟼ G (x)))$
116	115	mpteq2dv	$⊢ a = b \times_{f} c \to (x \in (ℤ^{W}) ⟼ a ((y \in V ⟼ G (x)))) = (x \in (ℤ^{W}) ⟼ (b \times_{f} c) ((y \in V ⟼ G (x))))$
117	116	eleq1d	$⊢ a = b \times_{f} c \to ((x \in (ℤ^{W}) ⟼ a ((y \in V ⟼ G (x)))) \in mzPoly (W) \leftrightarrow (x \in (ℤ^{W}) ⟼ (b \times_{f} c) ((y \in V ⟼ G (x)))) \in mzPoly (W))$
118		fveq1	$⊢ a = F \to a ((y \in V ⟼ G (x))) = F ((y \in V ⟼ G (x)))$
119	118	mpteq2dv	$⊢ a = F \to (x \in (ℤ^{W}) ⟼ a ((y \in V ⟼ G (x)))) = (x \in (ℤ^{W}) ⟼ F ((y \in V ⟼ G (x))))$
120	119	eleq1d	$⊢ a = F \to ((x \in (ℤ^{W}) ⟼ a ((y \in V ⟼ G (x)))) \in mzPoly (W) \leftrightarrow (x \in (ℤ^{W}) ⟼ F ((y \in V ⟼ G (x)))) \in mzPoly (W))$
121	30 67 92 99 102 105 108 111 114 117 120	mzpindd	$⊢ ((W \in V \land V \in V \land \forall y \in V G \in mzPoly (W)) \land F \in mzPoly (V)) \to (x \in (ℤ^{W}) ⟼ F ((y \in V ⟼ G (x)))) \in mzPoly (W)$
122	1 3 4 5 121	syl31anc	$⊢ (W \in V \land F \in mzPoly (V) \land \forall y \in V G \in mzPoly (W)) \to (x \in (ℤ^{W}) ⟼ F ((y \in V ⟼ G (x)))) \in mzPoly (W)$

Metamath Proof Explorer

Theorem mzpsubst

Proof