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{˙}{\cdot} = \cdot_{R}$
	esplyindfv.i	$⊢ φ \to I \in Fin$
	esplyindfv.r	$⊢ φ \to R \in CRing$
	esplyindfv.y	$⊢ φ \to Y \in I$
	esplyindfv.j	$⊢ J = I ∖ \{Y\}$
	esplyindfv.e	No typesetting found for \|- E = ( J eSymPoly R ) with typecode \|-
	esplyindfv.k	$⊢ φ \to K \in (0 \dots \|J\|)$
	esplyindfv.c	$⊢ C = \{h \in ({ℕ_{0}}^{J}) \| {finSupp}_{0} (h)\}$
	esplyindfv.f	No typesetting found for \|- F = ( ( I eSymPoly R ) ` ( K + 1 ) ) with typecode \|-
	esplyindfv.b	$⊢ B = {Base}_{R}$
	esplyindfv.q	$⊢ Q = I eval R$
	esplyindfv.o	$⊢ O = J eval R$
	esplyindfv.p	$⊢ \underset{˙}{+} = +_{R}$
	esplyindfv.z	$⊢ φ \to Z : I ⟶ B$
Assertion	esplyindfv	$⊢ φ \to Q (F) (Z) = (Z (Y) \underset{˙}{\cdot} O (E (K)) ({Z ↾}_{J})) \underset{˙}{+} O (E (K + 1)) ({Z ↾}_{J})$

Proof

Step	Hyp	Ref	Expression
1		esplyindfv.m	$⊢ \underset{˙}{\cdot} = \cdot_{R}$
2		esplyindfv.i	$⊢ φ \to I \in Fin$
3		esplyindfv.r	$⊢ φ \to R \in CRing$
4		esplyindfv.y	$⊢ φ \to Y \in I$
5		esplyindfv.j	$⊢ J = I ∖ \{Y\}$
6		esplyindfv.e	Could not format E = ( J eSymPoly R ) : No typesetting found for \|- E = ( J eSymPoly R ) with typecode \|-
7		esplyindfv.k	$⊢ φ \to K \in (0 \dots \|J\|)$
8		esplyindfv.c	$⊢ C = \{h \in ({ℕ_{0}}^{J}) \| {finSupp}_{0} (h)\}$
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 = {Base}_{R}$
11		esplyindfv.q	$⊢ Q = I eval R$
12		esplyindfv.o	$⊢ O = J eval R$
13		esplyindfv.p	$⊢ \underset{˙}{+} = +_{R}$
14		esplyindfv.z	$⊢ φ \to Z : I ⟶ B$
15		eqid	$⊢ I mPoly R = I mPoly R$
16		eqid	$⊢ I mVar R = I mVar R$
17		eqid	$⊢ +_{(I mPoly R)} = +_{(I mPoly R)}$
18		eqid	$⊢ \cdot_{(I mPoly R)} = \cdot_{(I mPoly R)}$
19		eqid	$⊢ \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\} = \{h \in ({ℕ_{0}}^{I}) \| {finSupp}_{0} (h)\}$
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	$⊢ φ \to R \in Ring$
22	7	elfzelzd	$⊢ φ \to K \in ℤ$
23		hashcl	$⊢ I \in Fin \to \|I\| \in ℕ_{0}$
24	2 23	syl	$⊢ φ \to \|I\| \in ℕ_{0}$
25	24	nn0zd	$⊢ φ \to \|I\| \in ℤ$
26	5	uneq1i	$⊢ J \cup \{Y\} = (I ∖ \{Y\}) \cup \{Y\}$
27	4	snssd	$⊢ φ \to \{Y\} \subseteq I$
28		undifr	$⊢ \{Y\} \subseteq I \leftrightarrow (I ∖ \{Y\}) \cup \{Y\} = I$
29	27 28	sylib	$⊢ φ \to (I ∖ \{Y\}) \cup \{Y\} = I$
30	26 29	eqtrid	$⊢ φ \to J \cup \{Y\} = I$
31	30	fveq2d	$⊢ φ \to \|J \cup \{Y\}\| = \|I\|$
32		difssd	$⊢ φ \to I ∖ \{Y\} \subseteq I$
33	5 32	eqsstrid	$⊢ φ \to J \subseteq I$
34	2 33	ssfid	$⊢ φ \to J \in Fin$
35		neldifsnd	$⊢ φ \to \neg Y \in (I ∖ \{Y\})$
36	5	eleq2i	$⊢ Y \in J \leftrightarrow Y \in (I ∖ \{Y\})$
37	35 36	sylnibr	$⊢ φ \to \neg Y \in J$
38		hashunsng	$⊢ Y \in I \to ((J \in Fin \land \neg Y \in J) \to \|J \cup \{Y\}\| = \|J\| + 1)$
39	38	imp	$⊢ (Y \in I \land (J \in Fin \land \neg Y \in J)) \to \|J \cup \{Y\}\| = \|J\| + 1$
40	4 34 37 39	syl12anc	$⊢ φ \to \|J \cup \{Y\}\| = \|J\| + 1$
41	31 40	eqtr3d	$⊢ φ \to \|I\| = \|J\| + 1$
42	41	oveq1d	$⊢ φ \to \|I\| - 1 = \|J\| + 1 - 1$
43		hashcl	$⊢ J \in Fin \to \|J\| \in ℕ_{0}$
44	34 43	syl	$⊢ φ \to \|J\| \in ℕ_{0}$
45	44	nn0cnd	$⊢ φ \to \|J\| \in ℂ$
46		1cnd	$⊢ φ \to 1 \in ℂ$
47	45 46	pncand	$⊢ φ \to \|J\| + 1 - 1 = \|J\|$
48	42 47	eqtr2d	$⊢ φ \to \|J\| = \|I\| - 1$
49	48	oveq2d	$⊢ φ \to (0 \dots \|J\|) = (0 \dots \|I\| - 1)$
50	7 49	eleqtrd	$⊢ φ \to K \in (0 \dots \|I\| - 1)$
51		elfzp1b	$⊢ (K \in ℤ \land \|I\| \in ℤ) \to (K \in (0 \dots \|I\| - 1) \leftrightarrow K + 1 \in (1 \dots \|I\|))$
52	51	biimpa	$⊢ ((K \in ℤ \land \|I\| \in ℤ) \land K \in (0 \dots \|I\| - 1)) \to K + 1 \in (1 \dots \|I\|)$
53	22 25 50 52	syl21anc	$⊢ φ \to K + 1 \in (1 \dots \|I\|)$
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	$⊢ {Base}_{(I mPoly R)} = {Base}_{(I mPoly R)}$
59	10	fvexi	$⊢ B \in V$
60	59	a1i	$⊢ φ \to B \in V$
61	60 2 14	elmapdd	$⊢ φ \to Z \in (B^{I})$
62	11 15 10 58 18 1 2 3 61 16 4	evlvarval	$⊢ φ \to ((I mVar R) (Y) \in {Base}_{(I mPoly R)} \land Q ((I mVar R) (Y)) (Z) = Z (Y))$
63		eqid	$⊢ 0_{R} = 0_{R}$
64		eqid	$⊢ {Base}_{(J mPoly R)} = {Base}_{(J mPoly R)}$
65	22	zcnd	$⊢ φ \to K \in ℂ$
66	65 46	pncand	$⊢ φ \to K + 1 - 1 = K$
67	66	fveq2d	$⊢ φ \to E (K + 1 - 1) = E (K)$
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	$⊢ (0 \dots \|J\|) \subseteq ℕ_{0}$
70	69 7	sselid	$⊢ φ \to K \in ℕ_{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	$⊢ φ \to E (K) \in {Base}_{(J mPoly R)}$
73	67 72	eqeltrd	$⊢ φ \to E (K + 1 - 1) \in {Base}_{(J mPoly R)}$
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 ℕ_{0} \to K + 1 \in ℕ_{0}$
85	70 84	syl	$⊢ φ \to K + 1 \in ℕ_{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	$⊢ φ \to E (K + 1) \in {Base}_{(J mPoly R)}$
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	$⊢ φ \to Q (F) (Z) = (Z (Y) \underset{˙}{\cdot} O (E (K)) ({Z ↾}_{J})) \underset{˙}{+} O (E (K + 1)) ({Z ↾}_{J})$

Metamath Proof Explorer

Theorem esplyindfv

Proof