mzpindd

Description: "Structural" induction to prove properties of all polynomial functions. (Contributed by Stefan O'Rear, 4-Oct-2014)

	Ref	Expression
Hypotheses	mzpindd.co	$⊢ (φ \land f \in ℤ) \to χ$
	mzpindd.pr	$⊢ (φ \land f \in V) \to θ$
	mzpindd.ad	$⊢ (φ \land (f : ℤ^{V} ⟶ ℤ \land τ) \land (g : ℤ^{V} ⟶ ℤ \land η)) \to ζ$
	mzpindd.mu	$⊢ (φ \land (f : ℤ^{V} ⟶ ℤ \land τ) \land (g : ℤ^{V} ⟶ ℤ \land η)) \to σ$
	mzpindd.1	$⊢ x = (ℤ^{V}) \times \{f\} \to (ψ \leftrightarrow χ)$
	mzpindd.2	$⊢ x = (g \in (ℤ^{V}) ⟼ g (f)) \to (ψ \leftrightarrow θ)$
	mzpindd.3	$⊢ x = f \to (ψ \leftrightarrow τ)$
	mzpindd.4	$⊢ x = g \to (ψ \leftrightarrow η)$
	mzpindd.5	$⊢ x = f +_{f} g \to (ψ \leftrightarrow ζ)$
	mzpindd.6	$⊢ x = f \times_{f} g \to (ψ \leftrightarrow σ)$
	mzpindd.7	$⊢ x = A \to (ψ \leftrightarrow ρ)$
Assertion	mzpindd	$⊢ (φ \land A \in mzPoly (V)) \to ρ$

Proof

Step	Hyp	Ref	Expression
1		mzpindd.co	$⊢ (φ \land f \in ℤ) \to χ$
2		mzpindd.pr	$⊢ (φ \land f \in V) \to θ$
3		mzpindd.ad	$⊢ (φ \land (f : ℤ^{V} ⟶ ℤ \land τ) \land (g : ℤ^{V} ⟶ ℤ \land η)) \to ζ$
4		mzpindd.mu	$⊢ (φ \land (f : ℤ^{V} ⟶ ℤ \land τ) \land (g : ℤ^{V} ⟶ ℤ \land η)) \to σ$
5		mzpindd.1	$⊢ x = (ℤ^{V}) \times \{f\} \to (ψ \leftrightarrow χ)$
6		mzpindd.2	$⊢ x = (g \in (ℤ^{V}) ⟼ g (f)) \to (ψ \leftrightarrow θ)$
7		mzpindd.3	$⊢ x = f \to (ψ \leftrightarrow τ)$
8		mzpindd.4	$⊢ x = g \to (ψ \leftrightarrow η)$
9		mzpindd.5	$⊢ x = f +_{f} g \to (ψ \leftrightarrow ζ)$
10		mzpindd.6	$⊢ x = f \times_{f} g \to (ψ \leftrightarrow σ)$
11		mzpindd.7	$⊢ x = A \to (ψ \leftrightarrow ρ)$
12		elfvex	$⊢ A \in mzPoly (V) \to V \in V$
13	12	adantl	$⊢ (φ \land A \in mzPoly (V)) \to V \in V$
14		mzpval	$⊢ V \in V \to mzPoly (V) = ⋂ mzPolyCld (V)$
15	14	adantl	$⊢ (φ \land V \in V) \to mzPoly (V) = ⋂ mzPolyCld (V)$
16		ssrab2	$⊢ \{x \in (ℤ^{(ℤ^{V})}) \| ψ\} \subseteq ℤ^{(ℤ^{V})}$
17	16	a1i	$⊢ (φ \land V \in V) \to \{x \in (ℤ^{(ℤ^{V})}) \| ψ\} \subseteq ℤ^{(ℤ^{V})}$
18		ovex	$⊢ ℤ^{V} \in V$
19		zex	$⊢ ℤ \in V$
20	18 19	constmap	$⊢ f \in ℤ \to (ℤ^{V}) \times \{f\} \in (ℤ^{(ℤ^{V})})$
21	20	adantl	$⊢ (φ \land f \in ℤ) \to (ℤ^{V}) \times \{f\} \in (ℤ^{(ℤ^{V})})$
22	5	elrab	$⊢ (ℤ^{V}) \times \{f\} \in \{x \in (ℤ^{(ℤ^{V})}) \| ψ\} \leftrightarrow ((ℤ^{V}) \times \{f\} \in (ℤ^{(ℤ^{V})}) \land χ)$
23	21 1 22	sylanbrc	$⊢ (φ \land f \in ℤ) \to (ℤ^{V}) \times \{f\} \in \{x \in (ℤ^{(ℤ^{V})}) \| ψ\}$
24	23	ralrimiva	$⊢ φ \to \forall f \in ℤ (ℤ^{V}) \times \{f\} \in \{x \in (ℤ^{(ℤ^{V})}) \| ψ\}$
25	24	adantr	$⊢ (φ \land V \in V) \to \forall f \in ℤ (ℤ^{V}) \times \{f\} \in \{x \in (ℤ^{(ℤ^{V})}) \| ψ\}$
26	19	a1i	$⊢ (((φ \land V \in V) \land f \in V) \land g \in (ℤ^{V})) \to ℤ \in V$
27		simpllr	$⊢ (((φ \land V \in V) \land f \in V) \land g \in (ℤ^{V})) \to V \in V$
28		simpr	$⊢ (((φ \land V \in V) \land f \in V) \land g \in (ℤ^{V})) \to g \in (ℤ^{V})$
29		elmapg	$⊢ (ℤ \in V \land V \in V) \to (g \in (ℤ^{V}) \leftrightarrow g : V ⟶ ℤ)$
30	29	biimpa	$⊢ ((ℤ \in V \land V \in V) \land g \in (ℤ^{V})) \to g : V ⟶ ℤ$
31	26 27 28 30	syl21anc	$⊢ (((φ \land V \in V) \land f \in V) \land g \in (ℤ^{V})) \to g : V ⟶ ℤ$
32		simplr	$⊢ (((φ \land V \in V) \land f \in V) \land g \in (ℤ^{V})) \to f \in V$
33	31 32	ffvelrnd	$⊢ (((φ \land V \in V) \land f \in V) \land g \in (ℤ^{V})) \to g (f) \in ℤ$
34	33	fmpttd	$⊢ ((φ \land V \in V) \land f \in V) \to (g \in (ℤ^{V}) ⟼ g (f)) : ℤ^{V} ⟶ ℤ$
35	19 18	elmap	$⊢ (g \in (ℤ^{V}) ⟼ g (f)) \in (ℤ^{(ℤ^{V})}) \leftrightarrow (g \in (ℤ^{V}) ⟼ g (f)) : ℤ^{V} ⟶ ℤ$
36	34 35	sylibr	$⊢ ((φ \land V \in V) \land f \in V) \to (g \in (ℤ^{V}) ⟼ g (f)) \in (ℤ^{(ℤ^{V})})$
37	2	adantlr	$⊢ ((φ \land V \in V) \land f \in V) \to θ$
38	6	elrab	$⊢ (g \in (ℤ^{V}) ⟼ g (f)) \in \{x \in (ℤ^{(ℤ^{V})}) \| ψ\} \leftrightarrow ((g \in (ℤ^{V}) ⟼ g (f)) \in (ℤ^{(ℤ^{V})}) \land θ)$
39	36 37 38	sylanbrc	$⊢ ((φ \land V \in V) \land f \in V) \to (g \in (ℤ^{V}) ⟼ g (f)) \in \{x \in (ℤ^{(ℤ^{V})}) \| ψ\}$
40	39	ralrimiva	$⊢ (φ \land V \in V) \to \forall f \in V (g \in (ℤ^{V}) ⟼ g (f)) \in \{x \in (ℤ^{(ℤ^{V})}) \| ψ\}$
41	25 40	jca	$⊢ (φ \land V \in V) \to (\forall f \in ℤ (ℤ^{V}) \times \{f\} \in \{x \in (ℤ^{(ℤ^{V})}) \| ψ\} \land \forall f \in V (g \in (ℤ^{V}) ⟼ g (f)) \in \{x \in (ℤ^{(ℤ^{V})}) \| ψ\})$
42		zaddcl	$⊢ (a \in ℤ \land b \in ℤ) \to a + b \in ℤ$
43	42	adantl	$⊢ ((f : ℤ^{V} ⟶ ℤ \land g : ℤ^{V} ⟶ ℤ) \land (a \in ℤ \land b \in ℤ)) \to a + b \in ℤ$
44		simpl	$⊢ (f : ℤ^{V} ⟶ ℤ \land g : ℤ^{V} ⟶ ℤ) \to f : ℤ^{V} ⟶ ℤ$
45		simpr	$⊢ (f : ℤ^{V} ⟶ ℤ \land g : ℤ^{V} ⟶ ℤ) \to g : ℤ^{V} ⟶ ℤ$
46	18	a1i	$⊢ (f : ℤ^{V} ⟶ ℤ \land g : ℤ^{V} ⟶ ℤ) \to ℤ^{V} \in V$
47		inidm	$⊢ (ℤ^{V}) \cap (ℤ^{V}) = ℤ^{V}$
48	43 44 45 46 46 47	off	$⊢ (f : ℤ^{V} ⟶ ℤ \land g : ℤ^{V} ⟶ ℤ) \to (f +_{f} g) : ℤ^{V} ⟶ ℤ$
49	48	ad2ant2r	$⊢ ((f : ℤ^{V} ⟶ ℤ \land τ) \land (g : ℤ^{V} ⟶ ℤ \land η)) \to (f +_{f} g) : ℤ^{V} ⟶ ℤ$
50	49	adantl	$⊢ (φ \land ((f : ℤ^{V} ⟶ ℤ \land τ) \land (g : ℤ^{V} ⟶ ℤ \land η))) \to (f +_{f} g) : ℤ^{V} ⟶ ℤ$
51	3	3expb	$⊢ (φ \land ((f : ℤ^{V} ⟶ ℤ \land τ) \land (g : ℤ^{V} ⟶ ℤ \land η))) \to ζ$
52	50 51	jca	$⊢ (φ \land ((f : ℤ^{V} ⟶ ℤ \land τ) \land (g : ℤ^{V} ⟶ ℤ \land η))) \to ((f +_{f} g) : ℤ^{V} ⟶ ℤ \land ζ)$
53		zmulcl	$⊢ (a \in ℤ \land b \in ℤ) \to a b \in ℤ$
54	53	adantl	$⊢ ((f : ℤ^{V} ⟶ ℤ \land g : ℤ^{V} ⟶ ℤ) \land (a \in ℤ \land b \in ℤ)) \to a b \in ℤ$
55	54 44 45 46 46 47	off	$⊢ (f : ℤ^{V} ⟶ ℤ \land g : ℤ^{V} ⟶ ℤ) \to (f \times_{f} g) : ℤ^{V} ⟶ ℤ$
56	55	ad2ant2r	$⊢ ((f : ℤ^{V} ⟶ ℤ \land τ) \land (g : ℤ^{V} ⟶ ℤ \land η)) \to (f \times_{f} g) : ℤ^{V} ⟶ ℤ$
57	56	adantl	$⊢ (φ \land ((f : ℤ^{V} ⟶ ℤ \land τ) \land (g : ℤ^{V} ⟶ ℤ \land η))) \to (f \times_{f} g) : ℤ^{V} ⟶ ℤ$
58	4	3expb	$⊢ (φ \land ((f : ℤ^{V} ⟶ ℤ \land τ) \land (g : ℤ^{V} ⟶ ℤ \land η))) \to σ$
59	52 57 58	jca32	$⊢ (φ \land ((f : ℤ^{V} ⟶ ℤ \land τ) \land (g : ℤ^{V} ⟶ ℤ \land η))) \to (((f +_{f} g) : ℤ^{V} ⟶ ℤ \land ζ) \land ((f \times_{f} g) : ℤ^{V} ⟶ ℤ \land σ))$
60	59	ex	$⊢ φ \to (((f : ℤ^{V} ⟶ ℤ \land τ) \land (g : ℤ^{V} ⟶ ℤ \land η)) \to (((f +_{f} g) : ℤ^{V} ⟶ ℤ \land ζ) \land ((f \times_{f} g) : ℤ^{V} ⟶ ℤ \land σ)))$
61	19 18	elmap	$⊢ f \in (ℤ^{(ℤ^{V})}) \leftrightarrow f : ℤ^{V} ⟶ ℤ$
62	61	anbi1i	$⊢ (f \in (ℤ^{(ℤ^{V})}) \land τ) \leftrightarrow (f : ℤ^{V} ⟶ ℤ \land τ)$
63	19 18	elmap	$⊢ g \in (ℤ^{(ℤ^{V})}) \leftrightarrow g : ℤ^{V} ⟶ ℤ$
64	63	anbi1i	$⊢ (g \in (ℤ^{(ℤ^{V})}) \land η) \leftrightarrow (g : ℤ^{V} ⟶ ℤ \land η)$
65	62 64	anbi12i	$⊢ ((f \in (ℤ^{(ℤ^{V})}) \land τ) \land (g \in (ℤ^{(ℤ^{V})}) \land η)) \leftrightarrow ((f : ℤ^{V} ⟶ ℤ \land τ) \land (g : ℤ^{V} ⟶ ℤ \land η))$
66	19 18	elmap	$⊢ f +_{f} g \in (ℤ^{(ℤ^{V})}) \leftrightarrow (f +_{f} g) : ℤ^{V} ⟶ ℤ$
67	66	anbi1i	$⊢ (f +_{f} g \in (ℤ^{(ℤ^{V})}) \land ζ) \leftrightarrow ((f +_{f} g) : ℤ^{V} ⟶ ℤ \land ζ)$
68	19 18	elmap	$⊢ f \times_{f} g \in (ℤ^{(ℤ^{V})}) \leftrightarrow (f \times_{f} g) : ℤ^{V} ⟶ ℤ$
69	68	anbi1i	$⊢ (f \times_{f} g \in (ℤ^{(ℤ^{V})}) \land σ) \leftrightarrow ((f \times_{f} g) : ℤ^{V} ⟶ ℤ \land σ)$
70	67 69	anbi12i	$⊢ ((f +_{f} g \in (ℤ^{(ℤ^{V})}) \land ζ) \land (f \times_{f} g \in (ℤ^{(ℤ^{V})}) \land σ)) \leftrightarrow (((f +_{f} g) : ℤ^{V} ⟶ ℤ \land ζ) \land ((f \times_{f} g) : ℤ^{V} ⟶ ℤ \land σ))$
71	60 65 70	3imtr4g	$⊢ φ \to (((f \in (ℤ^{(ℤ^{V})}) \land τ) \land (g \in (ℤ^{(ℤ^{V})}) \land η)) \to ((f +_{f} g \in (ℤ^{(ℤ^{V})}) \land ζ) \land (f \times_{f} g \in (ℤ^{(ℤ^{V})}) \land σ)))$
72	7	elrab	$⊢ f \in \{x \in (ℤ^{(ℤ^{V})}) \| ψ\} \leftrightarrow (f \in (ℤ^{(ℤ^{V})}) \land τ)$
73	8	elrab	$⊢ g \in \{x \in (ℤ^{(ℤ^{V})}) \| ψ\} \leftrightarrow (g \in (ℤ^{(ℤ^{V})}) \land η)$
74	72 73	anbi12i	$⊢ (f \in \{x \in (ℤ^{(ℤ^{V})}) \| ψ\} \land g \in \{x \in (ℤ^{(ℤ^{V})}) \| ψ\}) \leftrightarrow ((f \in (ℤ^{(ℤ^{V})}) \land τ) \land (g \in (ℤ^{(ℤ^{V})}) \land η))$
75	9	elrab	$⊢ f +_{f} g \in \{x \in (ℤ^{(ℤ^{V})}) \| ψ\} \leftrightarrow (f +_{f} g \in (ℤ^{(ℤ^{V})}) \land ζ)$
76	10	elrab	$⊢ f \times_{f} g \in \{x \in (ℤ^{(ℤ^{V})}) \| ψ\} \leftrightarrow (f \times_{f} g \in (ℤ^{(ℤ^{V})}) \land σ)$
77	75 76	anbi12i	$⊢ (f +_{f} g \in \{x \in (ℤ^{(ℤ^{V})}) \| ψ\} \land f \times_{f} g \in \{x \in (ℤ^{(ℤ^{V})}) \| ψ\}) \leftrightarrow ((f +_{f} g \in (ℤ^{(ℤ^{V})}) \land ζ) \land (f \times_{f} g \in (ℤ^{(ℤ^{V})}) \land σ))$
78	71 74 77	3imtr4g	$⊢ φ \to ((f \in \{x \in (ℤ^{(ℤ^{V})}) \| ψ\} \land g \in \{x \in (ℤ^{(ℤ^{V})}) \| ψ\}) \to (f +_{f} g \in \{x \in (ℤ^{(ℤ^{V})}) \| ψ\} \land f \times_{f} g \in \{x \in (ℤ^{(ℤ^{V})}) \| ψ\}))$
79	78	ralrimivv	$⊢ φ \to \forall f \in \{x \in (ℤ^{(ℤ^{V})}) \| ψ\} \forall g \in \{x \in (ℤ^{(ℤ^{V})}) \| ψ\} (f +_{f} g \in \{x \in (ℤ^{(ℤ^{V})}) \| ψ\} \land f \times_{f} g \in \{x \in (ℤ^{(ℤ^{V})}) \| ψ\})$
80	79	adantr	$⊢ (φ \land V \in V) \to \forall f \in \{x \in (ℤ^{(ℤ^{V})}) \| ψ\} \forall g \in \{x \in (ℤ^{(ℤ^{V})}) \| ψ\} (f +_{f} g \in \{x \in (ℤ^{(ℤ^{V})}) \| ψ\} \land f \times_{f} g \in \{x \in (ℤ^{(ℤ^{V})}) \| ψ\})$
81	17 41 80	jca32	$⊢ (φ \land V \in V) \to (\{x \in (ℤ^{(ℤ^{V})}) \| ψ\} \subseteq ℤ^{(ℤ^{V})} \land ((\forall f \in ℤ (ℤ^{V}) \times \{f\} \in \{x \in (ℤ^{(ℤ^{V})}) \| ψ\} \land \forall f \in V (g \in (ℤ^{V}) ⟼ g (f)) \in \{x \in (ℤ^{(ℤ^{V})}) \| ψ\}) \land \forall f \in \{x \in (ℤ^{(ℤ^{V})}) \| ψ\} \forall g \in \{x \in (ℤ^{(ℤ^{V})}) \| ψ\} (f +_{f} g \in \{x \in (ℤ^{(ℤ^{V})}) \| ψ\} \land f \times_{f} g \in \{x \in (ℤ^{(ℤ^{V})}) \| ψ\})))$
82		elmzpcl	$⊢ V \in V \to (\{x \in (ℤ^{(ℤ^{V})}) \| ψ\} \in mzPolyCld (V) \leftrightarrow (\{x \in (ℤ^{(ℤ^{V})}) \| ψ\} \subseteq ℤ^{(ℤ^{V})} \land ((\forall f \in ℤ (ℤ^{V}) \times \{f\} \in \{x \in (ℤ^{(ℤ^{V})}) \| ψ\} \land \forall f \in V (g \in (ℤ^{V}) ⟼ g (f)) \in \{x \in (ℤ^{(ℤ^{V})}) \| ψ\}) \land \forall f \in \{x \in (ℤ^{(ℤ^{V})}) \| ψ\} \forall g \in \{x \in (ℤ^{(ℤ^{V})}) \| ψ\} (f +_{f} g \in \{x \in (ℤ^{(ℤ^{V})}) \| ψ\} \land f \times_{f} g \in \{x \in (ℤ^{(ℤ^{V})}) \| ψ\}))))$
83	82	adantl	$⊢ (φ \land V \in V) \to (\{x \in (ℤ^{(ℤ^{V})}) \| ψ\} \in mzPolyCld (V) \leftrightarrow (\{x \in (ℤ^{(ℤ^{V})}) \| ψ\} \subseteq ℤ^{(ℤ^{V})} \land ((\forall f \in ℤ (ℤ^{V}) \times \{f\} \in \{x \in (ℤ^{(ℤ^{V})}) \| ψ\} \land \forall f \in V (g \in (ℤ^{V}) ⟼ g (f)) \in \{x \in (ℤ^{(ℤ^{V})}) \| ψ\}) \land \forall f \in \{x \in (ℤ^{(ℤ^{V})}) \| ψ\} \forall g \in \{x \in (ℤ^{(ℤ^{V})}) \| ψ\} (f +_{f} g \in \{x \in (ℤ^{(ℤ^{V})}) \| ψ\} \land f \times_{f} g \in \{x \in (ℤ^{(ℤ^{V})}) \| ψ\}))))$
84	81 83	mpbird	$⊢ (φ \land V \in V) \to \{x \in (ℤ^{(ℤ^{V})}) \| ψ\} \in mzPolyCld (V)$
85		intss1	$⊢ \{x \in (ℤ^{(ℤ^{V})}) \| ψ\} \in mzPolyCld (V) \to ⋂ mzPolyCld (V) \subseteq \{x \in (ℤ^{(ℤ^{V})}) \| ψ\}$
86	84 85	syl	$⊢ (φ \land V \in V) \to ⋂ mzPolyCld (V) \subseteq \{x \in (ℤ^{(ℤ^{V})}) \| ψ\}$
87	15 86	eqsstrd	$⊢ (φ \land V \in V) \to mzPoly (V) \subseteq \{x \in (ℤ^{(ℤ^{V})}) \| ψ\}$
88	87	sselda	$⊢ ((φ \land V \in V) \land A \in mzPoly (V)) \to A \in \{x \in (ℤ^{(ℤ^{V})}) \| ψ\}$
89	88	an32s	$⊢ ((φ \land A \in mzPoly (V)) \land V \in V) \to A \in \{x \in (ℤ^{(ℤ^{V})}) \| ψ\}$
90	13 89	mpdan	$⊢ (φ \land A \in mzPoly (V)) \to A \in \{x \in (ℤ^{(ℤ^{V})}) \| ψ\}$
91	11	elrab	$⊢ A \in \{x \in (ℤ^{(ℤ^{V})}) \| ψ\} \leftrightarrow (A \in (ℤ^{(ℤ^{V})}) \land ρ)$
92	91	simprbi	$⊢ A \in \{x \in (ℤ^{(ℤ^{V})}) \| ψ\} \to ρ$
93	90 92	syl	$⊢ (φ \land A \in mzPoly (V)) \to ρ$

Metamath Proof Explorer

Theorem mzpindd

Proof