Theorem esplyindfv

Description: A recursive formula for the elementary symmetric polynomials, evaluated at a given set of points Z . (Contributed by Thierry Arnoux, 15-Feb-2026)

	Ref	Expression
Hypotheses	esplyindfv.m	$$⊢\underset{\dot{}}{·}={\cdot }_R$$
	esplyindfv.i	$$⊢\phi \to I\in \mathrm{Fin}$$
	esplyindfv.r	$$⊢\phi \to R\in \mathrm{CRing}$$
	esplyindfv.y	$$⊢\phi \to Y\in I$$
	esplyindfv.j	$$⊢J=I\setminus \left\{Y\right\}$$
	esplyindfv.e	No typesetting found for |- E = ( J eSymPoly R ) with typecode |-
	esplyindfv.k	$$⊢\phi \to K\in \left(0\dots \left|J\right|\right)$$
	esplyindfv.c	$$⊢C=\left\{h\in \left({{\mathbb{N}}_0}^J\right)|{finSupp}_0\left(h\right)\right\}$$
	esplyindfv.f	No typesetting found for |- F = ( ( I eSymPoly R ) ` ( K + 1 ) ) with typecode |-
	esplyindfv.b	$$⊢B={\mathrm{Base}}_R$$
	esplyindfv.q	$$⊢Q=I\mathrm{eval}R$$
	esplyindfv.o	$$⊢O=J\mathrm{eval}R$$
	esplyindfv.p	$$⊢\underset{\dot{}}{+}={+}_R$$
	esplyindfv.z	$$⊢\phi \to Z:I⟶B$$
Assertion	esplyindfv	$$⊢\phi \to Q\left(F\right)\left(Z\right)=\left(Z\left(Y\right)\underset{\dot{}}{·}O\left(E\left(K\right)\right)\left({Z\upharpoonright }_J\right)\right)\underset{\dot{}}{+}O\left(E\left(K+1\right)\right)\left({Z\upharpoonright }_J\right)$$

Proof

Step	Hyp	Ref	Expression
1		esplyindfv.m	$$⊢\underset{\dot{}}{·}={\cdot }_R$$
2		esplyindfv.i	$$⊢\phi \to I\in \mathrm{Fin}$$
3		esplyindfv.r	$$⊢\phi \to R\in \mathrm{CRing}$$
4		esplyindfv.y	$$⊢\phi \to Y\in I$$
5		esplyindfv.j	$$⊢J=I\setminus \left\{Y\right\}$$
6		esplyindfv.e	Could not format E = ( J eSymPoly R ) : No typesetting found for |- E = ( J eSymPoly R ) with typecode |-
7		esplyindfv.k	$$⊢\phi \to K\in \left(0\dots \left|J\right|\right)$$
8		esplyindfv.c	$$⊢C=\left\{h\in \left({{\mathbb{N}}_0}^J\right)|{finSupp}_0\left(h\right)\right\}$$
9		esplyindfv.f	Could not format F = ( ( I eSymPoly R ) ` ( K + 1 ) ) : No typesetting found for |- F = ( ( I eSymPoly R ) ` ( K + 1 ) ) with typecode |-
10		esplyindfv.b	$$⊢B={\mathrm{Base}}_R$$
11		esplyindfv.q	$$⊢Q=I\mathrm{eval}R$$
12		esplyindfv.o	$$⊢O=J\mathrm{eval}R$$
13		esplyindfv.p	$$⊢\underset{\dot{}}{+}={+}_R$$
14		esplyindfv.z	$$⊢\phi \to Z:I⟶B$$
15		eqid	$$⊢I\mathrm{mPoly}R=I\mathrm{mPoly}R$$
16		eqid	$$⊢I\mathrm{mVar}R=I\mathrm{mVar}R$$
17		eqid	$$⊢{+}_{\left(I\mathrm{mPoly}R\right)}={+}_{\left(I\mathrm{mPoly}R\right)}$$
18		eqid	$$⊢{\cdot }_{\left(I\mathrm{mPoly}R\right)}={\cdot }_{\left(I\mathrm{mPoly}R\right)}$$
19		eqid	$$⊢\left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}=\left\{h\in \left({{\mathbb{N}}_0}^I\right)|{finSupp}_0\left(h\right)\right\}$$
20		eqid	Could not format ( ( I extendVars R ) ` Y ) = ( ( I extendVars R ) ` Y ) : No typesetting found for |- ( ( I extendVars R ) ` Y ) = ( ( I extendVars R ) ` Y ) with typecode |-
21	3	crngringd	$$⊢\phi \to R\in \mathrm{Ring}$$
22	7	elfzelzd	$$⊢\phi \to K\in \mathbb{Z}$$
23		hashcl	$$⊢I\in \mathrm{Fin}\to \left|I\right|\in {\mathbb{N}}_0$$
24	2 23	syl	$$⊢\phi \to \left|I\right|\in {\mathbb{N}}_0$$
25	24	nn0zd	$$⊢\phi \to \left|I\right|\in \mathbb{Z}$$
26	5	uneq1i	$$⊢J\cup \left\{Y\right\}=\left(I\setminus \left\{Y\right\}\right)\cup \left\{Y\right\}$$
27	4	snssd	$$⊢\phi \to \left\{Y\right\}\subseteq I$$
28		undifr	$$⊢\left\{Y\right\}\subseteq I\leftrightarrow \left(I\setminus \left\{Y\right\}\right)\cup \left\{Y\right\}=I$$
29	27 28	sylib	$$⊢\phi \to \left(I\setminus \left\{Y\right\}\right)\cup \left\{Y\right\}=I$$
30	26 29	eqtrid	$$⊢\phi \to J\cup \left\{Y\right\}=I$$
31	30	fveq2d	$$⊢\phi \to \left|J\cup \left\{Y\right\}\right|=\left|I\right|$$
32		difssd	$$⊢\phi \to I\setminus \left\{Y\right\}\subseteq I$$
33	5 32	eqsstrid	$$⊢\phi \to J\subseteq I$$
34	2 33	ssfid	$$⊢\phi \to J\in \mathrm{Fin}$$
35		neldifsnd	$$⊢\phi \to \neg Y\in \left(I\setminus \left\{Y\right\}\right)$$
36	5	eleq2i	$$⊢Y\in J\leftrightarrow Y\in \left(I\setminus \left\{Y\right\}\right)$$
37	35 36	sylnibr	$$⊢\phi \to \neg Y\in J$$
38		hashunsng	$$⊢Y\in I\to \left(\left(J\in \mathrm{Fin}\wedge \neg Y\in J\right)\to \left|J\cup \left\{Y\right\}\right|=\left|J\right|+1\right)$$
39	38	imp	$$⊢\left(Y\in I\wedge \left(J\in \mathrm{Fin}\wedge \neg Y\in J\right)\right)\to \left|J\cup \left\{Y\right\}\right|=\left|J\right|+1$$
40	4 34 37 39	syl12anc	$$⊢\phi \to \left|J\cup \left\{Y\right\}\right|=\left|J\right|+1$$
41	31 40	eqtr3d	$$⊢\phi \to \left|I\right|=\left|J\right|+1$$
42	41	oveq1d	$$⊢\phi \to \left|I\right|-1=\left|J\right|+1-1$$
43		hashcl	$$⊢J\in \mathrm{Fin}\to \left|J\right|\in {\mathbb{N}}_0$$
44	34 43	syl	$$⊢\phi \to \left|J\right|\in {\mathbb{N}}_0$$
45	44	nn0cnd	$$⊢\phi \to \left|J\right|\in ℂ$$
46		1cnd	$$⊢\phi \to 1\in ℂ$$
47	45 46	pncand	$$⊢\phi \to \left|J\right|+1-1=\left|J\right|$$
48	42 47	eqtr2d	$$⊢\phi \to \left|J\right|=\left|I\right|-1$$
49	48	oveq2d	$$⊢\phi \to \left(0\dots \left|J\right|\right)=\left(0\dots \left|I\right|-1\right)$$
50	7 49	eleqtrd	$$⊢\phi \to K\in \left(0\dots \left|I\right|-1\right)$$
51		elfzp1b	$$⊢\left(K\in \mathbb{Z}\wedge \left|I\right|\in \mathbb{Z}\right)\to \left(K\in \left(0\dots \left|I\right|-1\right)\leftrightarrow K+1\in \left(1\dots \left|I\right|\right)\right)$$
52	51	biimpa	$$⊢\left(\left(K\in \mathbb{Z}\wedge \left|I\right|\in \mathbb{Z}\right)\wedge K\in \left(0\dots \left|I\right|-1\right)\right)\to K+1\in \left(1\dots \left|I\right|\right)$$
53	22 25 50 52	syl21anc	$$⊢\phi \to K+1\in \left(1\dots \left|I\right|\right)$$
54	15 16 17 18 19 20 2 21 4 5 6 53 8	esplyind	Could not format ( ph -> ( ( I eSymPoly R ) ` ( K + 1 ) ) = ( ( ( ( I mVar R ) ` Y ) ( .r ` ( I mPoly R ) ) ( ( ( I extendVars R ) ` Y ) ` ( E ` ( ( K + 1 ) - 1 ) ) ) ) ( +g ` ( I mPoly R ) ) ( ( ( I extendVars R ) ` Y ) ` ( E ` ( K + 1 ) ) ) ) ) : No typesetting found for |- ( ph -> ( ( I eSymPoly R ) ` ( K + 1 ) ) = ( ( ( ( I mVar R ) ` Y ) ( .r ` ( I mPoly R ) ) ( ( ( I extendVars R ) ` Y ) ` ( E ` ( ( K + 1 ) - 1 ) ) ) ) ( +g ` ( I mPoly R ) ) ( ( ( I extendVars R ) ` Y ) ` ( E ` ( K + 1 ) ) ) ) ) with typecode |-
55	9 54	eqtrid	Could not format ( ph -> F = ( ( ( ( I mVar R ) ` Y ) ( .r ` ( I mPoly R ) ) ( ( ( I extendVars R ) ` Y ) ` ( E ` ( ( K + 1 ) - 1 ) ) ) ) ( +g ` ( I mPoly R ) ) ( ( ( I extendVars R ) ` Y ) ` ( E ` ( K + 1 ) ) ) ) ) : No typesetting found for |- ( ph -> F = ( ( ( ( I mVar R ) ` Y ) ( .r ` ( I mPoly R ) ) ( ( ( I extendVars R ) ` Y ) ` ( E ` ( ( K + 1 ) - 1 ) ) ) ) ( +g ` ( I mPoly R ) ) ( ( ( I extendVars R ) ` Y ) ` ( E ` ( K + 1 ) ) ) ) ) with typecode |-
56	55	fveq2d	Could not format ( ph -> ( Q ` F ) = ( Q ` ( ( ( ( I mVar R ) ` Y ) ( .r ` ( I mPoly R ) ) ( ( ( I extendVars R ) ` Y ) ` ( E ` ( ( K + 1 ) - 1 ) ) ) ) ( +g ` ( I mPoly R ) ) ( ( ( I extendVars R ) ` Y ) ` ( E ` ( K + 1 ) ) ) ) ) ) : No typesetting found for |- ( ph -> ( Q ` F ) = ( Q ` ( ( ( ( I mVar R ) ` Y ) ( .r ` ( I mPoly R ) ) ( ( ( I extendVars R ) ` Y ) ` ( E ` ( ( K + 1 ) - 1 ) ) ) ) ( +g ` ( I mPoly R ) ) ( ( ( I extendVars R ) ` Y ) ` ( E ` ( K + 1 ) ) ) ) ) ) with typecode |-
57	56	fveq1d	Could not format ( ph -> ( ( Q ` F ) ` Z ) = ( ( Q ` ( ( ( ( I mVar R ) ` Y ) ( .r ` ( I mPoly R ) ) ( ( ( I extendVars R ) ` Y ) ` ( E ` ( ( K + 1 ) - 1 ) ) ) ) ( +g ` ( I mPoly R ) ) ( ( ( I extendVars R ) ` Y ) ` ( E ` ( K + 1 ) ) ) ) ) ` Z ) ) : No typesetting found for |- ( ph -> ( ( Q ` F ) ` Z ) = ( ( Q ` ( ( ( ( I mVar R ) ` Y ) ( .r ` ( I mPoly R ) ) ( ( ( I extendVars R ) ` Y ) ` ( E ` ( ( K + 1 ) - 1 ) ) ) ) ( +g ` ( I mPoly R ) ) ( ( ( I extendVars R ) ` Y ) ` ( E ` ( K + 1 ) ) ) ) ) ` Z ) ) with typecode |-
58		eqid	$$⊢{\mathrm{Base}}_{\left(I\mathrm{mPoly}R\right)}={\mathrm{Base}}_{\left(I\mathrm{mPoly}R\right)}$$
59	10	fvexi	$$⊢B\in \mathrm{V}$$
60	59	a1i	$$⊢\phi \to B\in \mathrm{V}$$
61	60 2 14	elmapdd	$$⊢\phi \to Z\in \left(B^I\right)$$
62	11 15 10 58 18 1 2 3 61 16 4	evlvarval	$$⊢\phi \to \left(\left(I\mathrm{mVar}R\right)\left(Y\right)\in {\mathrm{Base}}_{\left(I\mathrm{mPoly}R\right)}\wedge Q\left(\left(I\mathrm{mVar}R\right)\left(Y\right)\right)\left(Z\right)=Z\left(Y\right)\right)$$
63		eqid	$$⊢0_R=0_R$$
64		eqid	$$⊢{\mathrm{Base}}_{\left(J\mathrm{mPoly}R\right)}={\mathrm{Base}}_{\left(J\mathrm{mPoly}R\right)}$$
65	22	zcnd	$$⊢\phi \to K\in ℂ$$
66	65 46	pncand	$$⊢\phi \to K+1-1=K$$
67	66	fveq2d	$$⊢\phi \to E\left(K+1-1\right)=E\left(K\right)$$
68	6	fveq1i	Could not format ( E ` K ) = ( ( J eSymPoly R ) ` K ) : No typesetting found for |- ( E ` K ) = ( ( J eSymPoly R ) ` K ) with typecode |-
69		fz0ssnn0	$$⊢\left(0\dots \left|J\right|\right)\subseteq {\mathbb{N}}_0$$
70	69 7	sselid	$$⊢\phi \to K\in {\mathbb{N}}_0$$
71	8 34 21 70 64	esplympl	Could not format ( ph -> ( ( J eSymPoly R ) ` K ) e. ( Base ` ( J mPoly R ) ) ) : No typesetting found for |- ( ph -> ( ( J eSymPoly R ) ` K ) e. ( Base ` ( J mPoly R ) ) ) with typecode |-
72	68 71	eqeltrid	$$⊢\phi \to E\left(K\right)\in {\mathrm{Base}}_{\left(J\mathrm{mPoly}R\right)}$$
73	67 72	eqeltrd	$$⊢\phi \to E\left(K+1-1\right)\in {\mathrm{Base}}_{\left(J\mathrm{mPoly}R\right)}$$
74	19 63 2 21 10 5 64 4 73 58	extvfvcl	Could not format ( ph -> ( ( ( I extendVars R ) ` Y ) ` ( E ` ( ( K + 1 ) - 1 ) ) ) e. ( Base ` ( I mPoly R ) ) ) : No typesetting found for |- ( ph -> ( ( ( I extendVars R ) ` Y ) ` ( E ` ( ( K + 1 ) - 1 ) ) ) e. ( Base ` ( I mPoly R ) ) ) with typecode |-
75	67	fveq2d	Could not format ( ph -> ( ( ( I extendVars R ) ` Y ) ` ( E ` ( ( K + 1 ) - 1 ) ) ) = ( ( ( I extendVars R ) ` Y ) ` ( E ` K ) ) ) : No typesetting found for |- ( ph -> ( ( ( I extendVars R ) ` Y ) ` ( E ` ( ( K + 1 ) - 1 ) ) ) = ( ( ( I extendVars R ) ` Y ) ` ( E ` K ) ) ) with typecode |-
76	75	fveq2d	Could not format ( ph -> ( Q ` ( ( ( I extendVars R ) ` Y ) ` ( E ` ( ( K + 1 ) - 1 ) ) ) ) = ( Q ` ( ( ( I extendVars R ) ` Y ) ` ( E ` K ) ) ) ) : No typesetting found for |- ( ph -> ( Q ` ( ( ( I extendVars R ) ` Y ) ` ( E ` ( ( K + 1 ) - 1 ) ) ) ) = ( Q ` ( ( ( I extendVars R ) ` Y ) ` ( E ` K ) ) ) ) with typecode |-
77	76	fveq1d	Could not format ( ph -> ( ( Q ` ( ( ( I extendVars R ) ` Y ) ` ( E ` ( ( K + 1 ) - 1 ) ) ) ) ` Z ) = ( ( Q ` ( ( ( I extendVars R ) ` Y ) ` ( E ` K ) ) ) ` Z ) ) : No typesetting found for |- ( ph -> ( ( Q ` ( ( ( I extendVars R ) ` Y ) ` ( E ` ( ( K + 1 ) - 1 ) ) ) ) ` Z ) = ( ( Q ` ( ( ( I extendVars R ) ` Y ) ` ( E ` K ) ) ) ` Z ) ) with typecode |-
78		eqid	Could not format ( I extendVars R ) = ( I extendVars R ) : No typesetting found for |- ( I extendVars R ) = ( I extendVars R ) with typecode |-
79	11 12 5 64 10 78 3 2 4 72 14	evlextv	Could not format ( ph -> ( ( Q ` ( ( ( I extendVars R ) ` Y ) ` ( E ` K ) ) ) ` Z ) = ( ( O ` ( E ` K ) ) ` ( Z |` J ) ) ) : No typesetting found for |- ( ph -> ( ( Q ` ( ( ( I extendVars R ) ` Y ) ` ( E ` K ) ) ) ` Z ) = ( ( O ` ( E ` K ) ) ` ( Z |` J ) ) ) with typecode |-
80	77 79	eqtrd	Could not format ( ph -> ( ( Q ` ( ( ( I extendVars R ) ` Y ) ` ( E ` ( ( K + 1 ) - 1 ) ) ) ) ` Z ) = ( ( O ` ( E ` K ) ) ` ( Z |` J ) ) ) : No typesetting found for |- ( ph -> ( ( Q ` ( ( ( I extendVars R ) ` Y ) ` ( E ` ( ( K + 1 ) - 1 ) ) ) ) ` Z ) = ( ( O ` ( E ` K ) ) ` ( Z |` J ) ) ) with typecode |-
81	74 80	jca	Could not format ( ph -> ( ( ( ( I extendVars R ) ` Y ) ` ( E ` ( ( K + 1 ) - 1 ) ) ) e. ( Base ` ( I mPoly R ) ) /\ ( ( Q ` ( ( ( I extendVars R ) ` Y ) ` ( E ` ( ( K + 1 ) - 1 ) ) ) ) ` Z ) = ( ( O ` ( E ` K ) ) ` ( Z |` J ) ) ) ) : No typesetting found for |- ( ph -> ( ( ( ( I extendVars R ) ` Y ) ` ( E ` ( ( K + 1 ) - 1 ) ) ) e. ( Base ` ( I mPoly R ) ) /\ ( ( Q ` ( ( ( I extendVars R ) ` Y ) ` ( E ` ( ( K + 1 ) - 1 ) ) ) ) ` Z ) = ( ( O ` ( E ` K ) ) ` ( Z |` J ) ) ) ) with typecode |-
82	11 15 10 58 18 1 2 3 61 62 81	evlmulval	Could not format ( ph -> ( ( ( ( I mVar R ) ` Y ) ( .r ` ( I mPoly R ) ) ( ( ( I extendVars R ) ` Y ) ` ( E ` ( ( K + 1 ) - 1 ) ) ) ) e. ( Base ` ( I mPoly R ) ) /\ ( ( Q ` ( ( ( I mVar R ) ` Y ) ( .r ` ( I mPoly R ) ) ( ( ( I extendVars R ) ` Y ) ` ( E ` ( ( K + 1 ) - 1 ) ) ) ) ) ` Z ) = ( ( Z ` Y ) .x. ( ( O ` ( E ` K ) ) ` ( Z |` J ) ) ) ) ) : No typesetting found for |- ( ph -> ( ( ( ( I mVar R ) ` Y ) ( .r ` ( I mPoly R ) ) ( ( ( I extendVars R ) ` Y ) ` ( E ` ( ( K + 1 ) - 1 ) ) ) ) e. ( Base ` ( I mPoly R ) ) /\ ( ( Q ` ( ( ( I mVar R ) ` Y ) ( .r ` ( I mPoly R ) ) ( ( ( I extendVars R ) ` Y ) ` ( E ` ( ( K + 1 ) - 1 ) ) ) ) ) ` Z ) = ( ( Z ` Y ) .x. ( ( O ` ( E ` K ) ) ` ( Z |` J ) ) ) ) ) with typecode |-
83	6	fveq1i	Could not format ( E ` ( K + 1 ) ) = ( ( J eSymPoly R ) ` ( K + 1 ) ) : No typesetting found for |- ( E ` ( K + 1 ) ) = ( ( J eSymPoly R ) ` ( K + 1 ) ) with typecode |-
84		peano2nn0	$$⊢K\in {\mathbb{N}}_0\to K+1\in {\mathbb{N}}_0$$
85	70 84	syl	$$⊢\phi \to K+1\in {\mathbb{N}}_0$$
86	8 34 21 85 64	esplympl	Could not format ( ph -> ( ( J eSymPoly R ) ` ( K + 1 ) ) e. ( Base ` ( J mPoly R ) ) ) : No typesetting found for |- ( ph -> ( ( J eSymPoly R ) ` ( K + 1 ) ) e. ( Base ` ( J mPoly R ) ) ) with typecode |-
87	83 86	eqeltrid	$$⊢\phi \to E\left(K+1\right)\in {\mathrm{Base}}_{\left(J\mathrm{mPoly}R\right)}$$
88	19 63 2 21 10 5 64 4 87 58	extvfvcl	Could not format ( ph -> ( ( ( I extendVars R ) ` Y ) ` ( E ` ( K + 1 ) ) ) e. ( Base ` ( I mPoly R ) ) ) : No typesetting found for |- ( ph -> ( ( ( I extendVars R ) ` Y ) ` ( E ` ( K + 1 ) ) ) e. ( Base ` ( I mPoly R ) ) ) with typecode |-
89	11 12 5 64 10 78 3 2 4 87 14	evlextv	Could not format ( ph -> ( ( Q ` ( ( ( I extendVars R ) ` Y ) ` ( E ` ( K + 1 ) ) ) ) ` Z ) = ( ( O ` ( E ` ( K + 1 ) ) ) ` ( Z |` J ) ) ) : No typesetting found for |- ( ph -> ( ( Q ` ( ( ( I extendVars R ) ` Y ) ` ( E ` ( K + 1 ) ) ) ) ` Z ) = ( ( O ` ( E ` ( K + 1 ) ) ) ` ( Z |` J ) ) ) with typecode |-
90	88 89	jca	Could not format ( ph -> ( ( ( ( I extendVars R ) ` Y ) ` ( E ` ( K + 1 ) ) ) e. ( Base ` ( I mPoly R ) ) /\ ( ( Q ` ( ( ( I extendVars R ) ` Y ) ` ( E ` ( K + 1 ) ) ) ) ` Z ) = ( ( O ` ( E ` ( K + 1 ) ) ) ` ( Z |` J ) ) ) ) : No typesetting found for |- ( ph -> ( ( ( ( I extendVars R ) ` Y ) ` ( E ` ( K + 1 ) ) ) e. ( Base ` ( I mPoly R ) ) /\ ( ( Q ` ( ( ( I extendVars R ) ` Y ) ` ( E ` ( K + 1 ) ) ) ) ` Z ) = ( ( O ` ( E ` ( K + 1 ) ) ) ` ( Z |` J ) ) ) ) with typecode |-
91	11 15 10 58 17 13 2 3 61 82 90	evladdval	Could not format ( ph -> ( ( ( ( ( I mVar R ) ` Y ) ( .r ` ( I mPoly R ) ) ( ( ( I extendVars R ) ` Y ) ` ( E ` ( ( K + 1 ) - 1 ) ) ) ) ( +g ` ( I mPoly R ) ) ( ( ( I extendVars R ) ` Y ) ` ( E ` ( K + 1 ) ) ) ) e. ( Base ` ( I mPoly R ) ) /\ ( ( Q ` ( ( ( ( I mVar R ) ` Y ) ( .r ` ( I mPoly R ) ) ( ( ( I extendVars R ) ` Y ) ` ( E ` ( ( K + 1 ) - 1 ) ) ) ) ( +g ` ( I mPoly R ) ) ( ( ( I extendVars R ) ` Y ) ` ( E ` ( K + 1 ) ) ) ) ) ` Z ) = ( ( ( Z ` Y ) .x. ( ( O ` ( E ` K ) ) ` ( Z |` J ) ) ) .+ ( ( O ` ( E ` ( K + 1 ) ) ) ` ( Z |` J ) ) ) ) ) : No typesetting found for |- ( ph -> ( ( ( ( ( I mVar R ) ` Y ) ( .r ` ( I mPoly R ) ) ( ( ( I extendVars R ) ` Y ) ` ( E ` ( ( K + 1 ) - 1 ) ) ) ) ( +g ` ( I mPoly R ) ) ( ( ( I extendVars R ) ` Y ) ` ( E ` ( K + 1 ) ) ) ) e. ( Base ` ( I mPoly R ) ) /\ ( ( Q ` ( ( ( ( I mVar R ) ` Y ) ( .r ` ( I mPoly R ) ) ( ( ( I extendVars R ) ` Y ) ` ( E ` ( ( K + 1 ) - 1 ) ) ) ) ( +g ` ( I mPoly R ) ) ( ( ( I extendVars R ) ` Y ) ` ( E ` ( K + 1 ) ) ) ) ) ` Z ) = ( ( ( Z ` Y ) .x. ( ( O ` ( E ` K ) ) ` ( Z |` J ) ) ) .+ ( ( O ` ( E ` ( K + 1 ) ) ) ` ( Z |` J ) ) ) ) ) with typecode |-
92	91	simprd	Could not format ( ph -> ( ( Q ` ( ( ( ( I mVar R ) ` Y ) ( .r ` ( I mPoly R ) ) ( ( ( I extendVars R ) ` Y ) ` ( E ` ( ( K + 1 ) - 1 ) ) ) ) ( +g ` ( I mPoly R ) ) ( ( ( I extendVars R ) ` Y ) ` ( E ` ( K + 1 ) ) ) ) ) ` Z ) = ( ( ( Z ` Y ) .x. ( ( O ` ( E ` K ) ) ` ( Z |` J ) ) ) .+ ( ( O ` ( E ` ( K + 1 ) ) ) ` ( Z |` J ) ) ) ) : No typesetting found for |- ( ph -> ( ( Q ` ( ( ( ( I mVar R ) ` Y ) ( .r ` ( I mPoly R ) ) ( ( ( I extendVars R ) ` Y ) ` ( E ` ( ( K + 1 ) - 1 ) ) ) ) ( +g ` ( I mPoly R ) ) ( ( ( I extendVars R ) ` Y ) ` ( E ` ( K + 1 ) ) ) ) ) ` Z ) = ( ( ( Z ` Y ) .x. ( ( O ` ( E ` K ) ) ` ( Z |` J ) ) ) .+ ( ( O ` ( E ` ( K + 1 ) ) ) ` ( Z |` J ) ) ) ) with typecode |-
93	57 92	eqtrd	$$⊢\phi \to Q\left(F\right)\left(Z\right)=\left(Z\left(Y\right)\underset{\dot{}}{·}O\left(E\left(K\right)\right)\left({Z\upharpoonright }_J\right)\right)\underset{\dot{}}{+}O\left(E\left(K+1\right)\right)\left({Z\upharpoonright }_J\right)$$