Metamath Proof Explorer

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 ⊢ · = ( .r ‘ 𝑅 )
esplyindfv.i ⊢ ( 𝜑 → 𝐼 ∈ Fin )
esplyindfv.r ⊢ ( 𝜑 → 𝑅 ∈ CRing )
esplyindfv.y ⊢ ( 𝜑 → 𝑌 ∈ 𝐼 )
esplyindfv.j ⊢ 𝐽 = ( 𝐼 ∖ { 𝑌 } )
esplyindfv.e ⊢ 𝐸 = ( 𝐽 eSymPoly 𝑅 )
esplyindfv.k ⊢ ( 𝜑 → 𝐾 ∈ ( 0 ... ( ♯ ‘ 𝐽 ) ) )
esplyindfv.c ⊢ 𝐶 = { ℎ ∈ ( ℕ0 ↑m 𝐽 ) ∣ ℎ finSupp 0 }
esplyindfv.f ⊢ 𝐹 = ( ( 𝐼 eSymPoly 𝑅 ) ‘ ( 𝐾 + 1 ) )
esplyindfv.b ⊢ 𝐵 = ( Base ‘ 𝑅 )
esplyindfv.q ⊢ 𝑄 = ( 𝐼 eval 𝑅 )
esplyindfv.o ⊢ 𝑂 = ( 𝐽 eval 𝑅 )
esplyindfv.p ⊢ + = ( +g ‘ 𝑅 )
esplyindfv.z ⊢ ( 𝜑 → 𝑍 : 𝐼 ⟶ 𝐵 )
Assertion esplyindfv ( 𝜑 → ( ( 𝑄 ‘ 𝐹 ) ‘ 𝑍 ) = ( ( ( 𝑍 ‘ 𝑌 ) · ( ( 𝑂 ‘ ( 𝐸 ‘ 𝐾 ) ) ‘ ( 𝑍 ↾ 𝐽 ) ) ) + ( ( 𝑂 ‘ ( 𝐸 ‘ ( 𝐾 + 1 ) ) ) ‘ ( 𝑍 ↾ 𝐽 ) ) ) )

Proof

Step Hyp Ref Expression
1 esplyindfv.m ⊢ · = ( .r ‘ 𝑅 )
2 esplyindfv.i ⊢ ( 𝜑 → 𝐼 ∈ Fin )
3 esplyindfv.r ⊢ ( 𝜑 → 𝑅 ∈ CRing )
4 esplyindfv.y ⊢ ( 𝜑 → 𝑌 ∈ 𝐼 )
5 esplyindfv.j ⊢ 𝐽 = ( 𝐼 ∖ { 𝑌 } )
6 esplyindfv.e ⊢ 𝐸 = ( 𝐽 eSymPoly 𝑅 )
7 esplyindfv.k ⊢ ( 𝜑 → 𝐾 ∈ ( 0 ... ( ♯ ‘ 𝐽 ) ) )
8 esplyindfv.c ⊢ 𝐶 = { ℎ ∈ ( ℕ0 ↑m 𝐽 ) ∣ ℎ finSupp 0 }
9 esplyindfv.f ⊢ 𝐹 = ( ( 𝐼 eSymPoly 𝑅 ) ‘ ( 𝐾 + 1 ) )
10 esplyindfv.b ⊢ 𝐵 = ( Base ‘ 𝑅 )
11 esplyindfv.q ⊢ 𝑄 = ( 𝐼 eval 𝑅 )
12 esplyindfv.o ⊢ 𝑂 = ( 𝐽 eval 𝑅 )
13 esplyindfv.p ⊢ + = ( +g ‘ 𝑅 )
14 esplyindfv.z ⊢ ( 𝜑 → 𝑍 : 𝐼 ⟶ 𝐵 )
15 eqid ⊢ ( 𝐼 mPoly 𝑅 ) = ( 𝐼 mPoly 𝑅 )
16 eqid ⊢ ( 𝐼 mVar 𝑅 ) = ( 𝐼 mVar 𝑅 )
17 eqid ⊢ ( +g ‘ ( 𝐼 mPoly 𝑅 ) ) = ( +g ‘ ( 𝐼 mPoly 𝑅 ) )
18 eqid ⊢ ( .r ‘ ( 𝐼 mPoly 𝑅 ) ) = ( .r ‘ ( 𝐼 mPoly 𝑅 ) )
19 eqid ⊢ { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 } = { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 }
20 eqid ⊢ ( ( 𝐼 extendVars 𝑅 ) ‘ 𝑌 ) = ( ( 𝐼 extendVars 𝑅 ) ‘ 𝑌 )
21 3 crngringd ⊢ ( 𝜑 → 𝑅 ∈ Ring )
22 7 elfzelzd ⊢ ( 𝜑 → 𝐾 ∈ ℤ )
23 hashcl ⊢ ( 𝐼 ∈ Fin → ( ♯ ‘ 𝐼 ) ∈ ℕ0 )
24 2 23 syl ⊢ ( 𝜑 → ( ♯ ‘ 𝐼 ) ∈ ℕ0 )
25 24 nn0zd ⊢ ( 𝜑 → ( ♯ ‘ 𝐼 ) ∈ ℤ )
26 5 uneq1i ⊢ ( 𝐽 ∪ { 𝑌 } ) = ( ( 𝐼 ∖ { 𝑌 } ) ∪ { 𝑌 } )
27 4 snssd ⊢ ( 𝜑 → { 𝑌 } ⊆ 𝐼 )
28 undifr ⊢ ( { 𝑌 } ⊆ 𝐼 ↔ ( ( 𝐼 ∖ { 𝑌 } ) ∪ { 𝑌 } ) = 𝐼 )
29 27 28 sylib ⊢ ( 𝜑 → ( ( 𝐼 ∖ { 𝑌 } ) ∪ { 𝑌 } ) = 𝐼 )
30 26 29 eqtrid ⊢ ( 𝜑 → ( 𝐽 ∪ { 𝑌 } ) = 𝐼 )
31 30 fveq2d ⊢ ( 𝜑 → ( ♯ ‘ ( 𝐽 ∪ { 𝑌 } ) ) = ( ♯ ‘ 𝐼 ) )
32 difssd ⊢ ( 𝜑 → ( 𝐼 ∖ { 𝑌 } ) ⊆ 𝐼 )
33 5 32 eqsstrid ⊢ ( 𝜑 → 𝐽 ⊆ 𝐼 )
34 2 33 ssfid ⊢ ( 𝜑 → 𝐽 ∈ Fin )
35 neldifsnd ⊢ ( 𝜑 → ¬ 𝑌 ∈ ( 𝐼 ∖ { 𝑌 } ) )
36 5 eleq2i ⊢ ( 𝑌 ∈ 𝐽 ↔ 𝑌 ∈ ( 𝐼 ∖ { 𝑌 } ) )
37 35 36 sylnibr ⊢ ( 𝜑 → ¬ 𝑌 ∈ 𝐽 )
38 hashunsng ⊢ ( 𝑌 ∈ 𝐼 → ( ( 𝐽 ∈ Fin ∧ ¬ 𝑌 ∈ 𝐽 ) → ( ♯ ‘ ( 𝐽 ∪ { 𝑌 } ) ) = ( ( ♯ ‘ 𝐽 ) + 1 ) ) )
39 38 imp ⊢ ( ( 𝑌 ∈ 𝐼 ∧ ( 𝐽 ∈ Fin ∧ ¬ 𝑌 ∈ 𝐽 ) ) → ( ♯ ‘ ( 𝐽 ∪ { 𝑌 } ) ) = ( ( ♯ ‘ 𝐽 ) + 1 ) )
40 4 34 37 39 syl12anc ⊢ ( 𝜑 → ( ♯ ‘ ( 𝐽 ∪ { 𝑌 } ) ) = ( ( ♯ ‘ 𝐽 ) + 1 ) )
41 31 40 eqtr3d ⊢ ( 𝜑 → ( ♯ ‘ 𝐼 ) = ( ( ♯ ‘ 𝐽 ) + 1 ) )
42 41 oveq1d ⊢ ( 𝜑 → ( ( ♯ ‘ 𝐼 ) − 1 ) = ( ( ( ♯ ‘ 𝐽 ) + 1 ) − 1 ) )
43 hashcl ⊢ ( 𝐽 ∈ Fin → ( ♯ ‘ 𝐽 ) ∈ ℕ0 )
44 34 43 syl ⊢ ( 𝜑 → ( ♯ ‘ 𝐽 ) ∈ ℕ0 )
45 44 nn0cnd ⊢ ( 𝜑 → ( ♯ ‘ 𝐽 ) ∈ ℂ )
46 1cnd ⊢ ( 𝜑 → 1 ∈ ℂ )
47 45 46 pncand ⊢ ( 𝜑 → ( ( ( ♯ ‘ 𝐽 ) + 1 ) − 1 ) = ( ♯ ‘ 𝐽 ) )
48 42 47 eqtr2d ⊢ ( 𝜑 → ( ♯ ‘ 𝐽 ) = ( ( ♯ ‘ 𝐼 ) − 1 ) )
49 48 oveq2d ⊢ ( 𝜑 → ( 0 ... ( ♯ ‘ 𝐽 ) ) = ( 0 ... ( ( ♯ ‘ 𝐼 ) − 1 ) ) )
50 7 49 eleqtrd ⊢ ( 𝜑 → 𝐾 ∈ ( 0 ... ( ( ♯ ‘ 𝐼 ) − 1 ) ) )
51 elfzp1b ⊢ ( ( 𝐾 ∈ ℤ ∧ ( ♯ ‘ 𝐼 ) ∈ ℤ ) → ( 𝐾 ∈ ( 0 ... ( ( ♯ ‘ 𝐼 ) − 1 ) ) ↔ ( 𝐾 + 1 ) ∈ ( 1 ... ( ♯ ‘ 𝐼 ) ) ) )
52 51 biimpa ⊢ ( ( ( 𝐾 ∈ ℤ ∧ ( ♯ ‘ 𝐼 ) ∈ ℤ ) ∧ 𝐾 ∈ ( 0 ... ( ( ♯ ‘ 𝐼 ) − 1 ) ) ) → ( 𝐾 + 1 ) ∈ ( 1 ... ( ♯ ‘ 𝐼 ) ) )
53 22 25 50 52 syl21anc ⊢ ( 𝜑 → ( 𝐾 + 1 ) ∈ ( 1 ... ( ♯ ‘ 𝐼 ) ) )
54 15 16 17 18 19 20 2 21 4 5 6 53 8 esplyind ⊢ ( 𝜑 → ( ( 𝐼 eSymPoly 𝑅 ) ‘ ( 𝐾 + 1 ) ) = ( ( ( ( 𝐼 mVar 𝑅 ) ‘ 𝑌 ) ( .r ‘ ( 𝐼 mPoly 𝑅 ) ) ( ( ( 𝐼 extendVars 𝑅 ) ‘ 𝑌 ) ‘ ( 𝐸 ‘ ( ( 𝐾 + 1 ) − 1 ) ) ) ) ( +g ‘ ( 𝐼 mPoly 𝑅 ) ) ( ( ( 𝐼 extendVars 𝑅 ) ‘ 𝑌 ) ‘ ( 𝐸 ‘ ( 𝐾 + 1 ) ) ) ) )
55 9 54 eqtrid ⊢ ( 𝜑 → 𝐹 = ( ( ( ( 𝐼 mVar 𝑅 ) ‘ 𝑌 ) ( .r ‘ ( 𝐼 mPoly 𝑅 ) ) ( ( ( 𝐼 extendVars 𝑅 ) ‘ 𝑌 ) ‘ ( 𝐸 ‘ ( ( 𝐾 + 1 ) − 1 ) ) ) ) ( +g ‘ ( 𝐼 mPoly 𝑅 ) ) ( ( ( 𝐼 extendVars 𝑅 ) ‘ 𝑌 ) ‘ ( 𝐸 ‘ ( 𝐾 + 1 ) ) ) ) )
56 55 fveq2d ⊢ ( 𝜑 → ( 𝑄 ‘ 𝐹 ) = ( 𝑄 ‘ ( ( ( ( 𝐼 mVar 𝑅 ) ‘ 𝑌 ) ( .r ‘ ( 𝐼 mPoly 𝑅 ) ) ( ( ( 𝐼 extendVars 𝑅 ) ‘ 𝑌 ) ‘ ( 𝐸 ‘ ( ( 𝐾 + 1 ) − 1 ) ) ) ) ( +g ‘ ( 𝐼 mPoly 𝑅 ) ) ( ( ( 𝐼 extendVars 𝑅 ) ‘ 𝑌 ) ‘ ( 𝐸 ‘ ( 𝐾 + 1 ) ) ) ) ) )
57 56 fveq1d ⊢ ( 𝜑 → ( ( 𝑄 ‘ 𝐹 ) ‘ 𝑍 ) = ( ( 𝑄 ‘ ( ( ( ( 𝐼 mVar 𝑅 ) ‘ 𝑌 ) ( .r ‘ ( 𝐼 mPoly 𝑅 ) ) ( ( ( 𝐼 extendVars 𝑅 ) ‘ 𝑌 ) ‘ ( 𝐸 ‘ ( ( 𝐾 + 1 ) − 1 ) ) ) ) ( +g ‘ ( 𝐼 mPoly 𝑅 ) ) ( ( ( 𝐼 extendVars 𝑅 ) ‘ 𝑌 ) ‘ ( 𝐸 ‘ ( 𝐾 + 1 ) ) ) ) ) ‘ 𝑍 ) )
58 eqid ⊢ ( Base ‘ ( 𝐼 mPoly 𝑅 ) ) = ( Base ‘ ( 𝐼 mPoly 𝑅 ) )
59 10 fvexi ⊢ 𝐵 ∈ V
60 59 a1i ⊢ ( 𝜑 → 𝐵 ∈ V )
61 60 2 14 elmapdd ⊢ ( 𝜑 → 𝑍 ∈ ( 𝐵 ↑m 𝐼 ) )
62 11 15 10 58 18 1 2 3 61 16 4 evlvarval ⊢ ( 𝜑 → ( ( ( 𝐼 mVar 𝑅 ) ‘ 𝑌 ) ∈ ( Base ‘ ( 𝐼 mPoly 𝑅 ) ) ∧ ( ( 𝑄 ‘ ( ( 𝐼 mVar 𝑅 ) ‘ 𝑌 ) ) ‘ 𝑍 ) = ( 𝑍 ‘ 𝑌 ) ) )
63 eqid ⊢ ( 0g ‘ 𝑅 ) = ( 0g ‘ 𝑅 )
64 eqid ⊢ ( Base ‘ ( 𝐽 mPoly 𝑅 ) ) = ( Base ‘ ( 𝐽 mPoly 𝑅 ) )
65 22 zcnd ⊢ ( 𝜑 → 𝐾 ∈ ℂ )
66 65 46 pncand ⊢ ( 𝜑 → ( ( 𝐾 + 1 ) − 1 ) = 𝐾 )
67 66 fveq2d ⊢ ( 𝜑 → ( 𝐸 ‘ ( ( 𝐾 + 1 ) − 1 ) ) = ( 𝐸 ‘ 𝐾 ) )
68 6 fveq1i ⊢ ( 𝐸 ‘ 𝐾 ) = ( ( 𝐽 eSymPoly 𝑅 ) ‘ 𝐾 )
69 fz0ssnn0 ⊢ ( 0 ... ( ♯ ‘ 𝐽 ) ) ⊆ ℕ0
70 69 7 sselid ⊢ ( 𝜑 → 𝐾 ∈ ℕ0 )
71 8 34 21 70 64 esplympl ⊢ ( 𝜑 → ( ( 𝐽 eSymPoly 𝑅 ) ‘ 𝐾 ) ∈ ( Base ‘ ( 𝐽 mPoly 𝑅 ) ) )
72 68 71 eqeltrid ⊢ ( 𝜑 → ( 𝐸 ‘ 𝐾 ) ∈ ( Base ‘ ( 𝐽 mPoly 𝑅 ) ) )
73 67 72 eqeltrd ⊢ ( 𝜑 → ( 𝐸 ‘ ( ( 𝐾 + 1 ) − 1 ) ) ∈ ( Base ‘ ( 𝐽 mPoly 𝑅 ) ) )
74 19 63 2 21 10 5 64 4 73 58 extvfvcl ⊢ ( 𝜑 → ( ( ( 𝐼 extendVars 𝑅 ) ‘ 𝑌 ) ‘ ( 𝐸 ‘ ( ( 𝐾 + 1 ) − 1 ) ) ) ∈ ( Base ‘ ( 𝐼 mPoly 𝑅 ) ) )
75 67 fveq2d ⊢ ( 𝜑 → ( ( ( 𝐼 extendVars 𝑅 ) ‘ 𝑌 ) ‘ ( 𝐸 ‘ ( ( 𝐾 + 1 ) − 1 ) ) ) = ( ( ( 𝐼 extendVars 𝑅 ) ‘ 𝑌 ) ‘ ( 𝐸 ‘ 𝐾 ) ) )
76 75 fveq2d ⊢ ( 𝜑 → ( 𝑄 ‘ ( ( ( 𝐼 extendVars 𝑅 ) ‘ 𝑌 ) ‘ ( 𝐸 ‘ ( ( 𝐾 + 1 ) − 1 ) ) ) ) = ( 𝑄 ‘ ( ( ( 𝐼 extendVars 𝑅 ) ‘ 𝑌 ) ‘ ( 𝐸 ‘ 𝐾 ) ) ) )
77 76 fveq1d ⊢ ( 𝜑 → ( ( 𝑄 ‘ ( ( ( 𝐼 extendVars 𝑅 ) ‘ 𝑌 ) ‘ ( 𝐸 ‘ ( ( 𝐾 + 1 ) − 1 ) ) ) ) ‘ 𝑍 ) = ( ( 𝑄 ‘ ( ( ( 𝐼 extendVars 𝑅 ) ‘ 𝑌 ) ‘ ( 𝐸 ‘ 𝐾 ) ) ) ‘ 𝑍 ) )
78 eqid ⊢ ( 𝐼 extendVars 𝑅 ) = ( 𝐼 extendVars 𝑅 )
79 11 12 5 64 10 78 3 2 4 72 14 evlextv ⊢ ( 𝜑 → ( ( 𝑄 ‘ ( ( ( 𝐼 extendVars 𝑅 ) ‘ 𝑌 ) ‘ ( 𝐸 ‘ 𝐾 ) ) ) ‘ 𝑍 ) = ( ( 𝑂 ‘ ( 𝐸 ‘ 𝐾 ) ) ‘ ( 𝑍 ↾ 𝐽 ) ) )
80 77 79 eqtrd ⊢ ( 𝜑 → ( ( 𝑄 ‘ ( ( ( 𝐼 extendVars 𝑅 ) ‘ 𝑌 ) ‘ ( 𝐸 ‘ ( ( 𝐾 + 1 ) − 1 ) ) ) ) ‘ 𝑍 ) = ( ( 𝑂 ‘ ( 𝐸 ‘ 𝐾 ) ) ‘ ( 𝑍 ↾ 𝐽 ) ) )
81 74 80 jca ⊢ ( 𝜑 → ( ( ( ( 𝐼 extendVars 𝑅 ) ‘ 𝑌 ) ‘ ( 𝐸 ‘ ( ( 𝐾 + 1 ) − 1 ) ) ) ∈ ( Base ‘ ( 𝐼 mPoly 𝑅 ) ) ∧ ( ( 𝑄 ‘ ( ( ( 𝐼 extendVars 𝑅 ) ‘ 𝑌 ) ‘ ( 𝐸 ‘ ( ( 𝐾 + 1 ) − 1 ) ) ) ) ‘ 𝑍 ) = ( ( 𝑂 ‘ ( 𝐸 ‘ 𝐾 ) ) ‘ ( 𝑍 ↾ 𝐽 ) ) ) )
82 11 15 10 58 18 1 2 3 61 62 81 evlmulval ⊢ ( 𝜑 → ( ( ( ( 𝐼 mVar 𝑅 ) ‘ 𝑌 ) ( .r ‘ ( 𝐼 mPoly 𝑅 ) ) ( ( ( 𝐼 extendVars 𝑅 ) ‘ 𝑌 ) ‘ ( 𝐸 ‘ ( ( 𝐾 + 1 ) − 1 ) ) ) ) ∈ ( Base ‘ ( 𝐼 mPoly 𝑅 ) ) ∧ ( ( 𝑄 ‘ ( ( ( 𝐼 mVar 𝑅 ) ‘ 𝑌 ) ( .r ‘ ( 𝐼 mPoly 𝑅 ) ) ( ( ( 𝐼 extendVars 𝑅 ) ‘ 𝑌 ) ‘ ( 𝐸 ‘ ( ( 𝐾 + 1 ) − 1 ) ) ) ) ) ‘ 𝑍 ) = ( ( 𝑍 ‘ 𝑌 ) · ( ( 𝑂 ‘ ( 𝐸 ‘ 𝐾 ) ) ‘ ( 𝑍 ↾ 𝐽 ) ) ) ) )
83 6 fveq1i ⊢ ( 𝐸 ‘ ( 𝐾 + 1 ) ) = ( ( 𝐽 eSymPoly 𝑅 ) ‘ ( 𝐾 + 1 ) )
84 peano2nn0 ⊢ ( 𝐾 ∈ ℕ0 → ( 𝐾 + 1 ) ∈ ℕ0 )
85 70 84 syl ⊢ ( 𝜑 → ( 𝐾 + 1 ) ∈ ℕ0 )
86 8 34 21 85 64 esplympl ⊢ ( 𝜑 → ( ( 𝐽 eSymPoly 𝑅 ) ‘ ( 𝐾 + 1 ) ) ∈ ( Base ‘ ( 𝐽 mPoly 𝑅 ) ) )
87 83 86 eqeltrid ⊢ ( 𝜑 → ( 𝐸 ‘ ( 𝐾 + 1 ) ) ∈ ( Base ‘ ( 𝐽 mPoly 𝑅 ) ) )
88 19 63 2 21 10 5 64 4 87 58 extvfvcl ⊢ ( 𝜑 → ( ( ( 𝐼 extendVars 𝑅 ) ‘ 𝑌 ) ‘ ( 𝐸 ‘ ( 𝐾 + 1 ) ) ) ∈ ( Base ‘ ( 𝐼 mPoly 𝑅 ) ) )
89 11 12 5 64 10 78 3 2 4 87 14 evlextv ⊢ ( 𝜑 → ( ( 𝑄 ‘ ( ( ( 𝐼 extendVars 𝑅 ) ‘ 𝑌 ) ‘ ( 𝐸 ‘ ( 𝐾 + 1 ) ) ) ) ‘ 𝑍 ) = ( ( 𝑂 ‘ ( 𝐸 ‘ ( 𝐾 + 1 ) ) ) ‘ ( 𝑍 ↾ 𝐽 ) ) )
90 88 89 jca ⊢ ( 𝜑 → ( ( ( ( 𝐼 extendVars 𝑅 ) ‘ 𝑌 ) ‘ ( 𝐸 ‘ ( 𝐾 + 1 ) ) ) ∈ ( Base ‘ ( 𝐼 mPoly 𝑅 ) ) ∧ ( ( 𝑄 ‘ ( ( ( 𝐼 extendVars 𝑅 ) ‘ 𝑌 ) ‘ ( 𝐸 ‘ ( 𝐾 + 1 ) ) ) ) ‘ 𝑍 ) = ( ( 𝑂 ‘ ( 𝐸 ‘ ( 𝐾 + 1 ) ) ) ‘ ( 𝑍 ↾ 𝐽 ) ) ) )
91 11 15 10 58 17 13 2 3 61 82 90 evladdval ⊢ ( 𝜑 → ( ( ( ( ( 𝐼 mVar 𝑅 ) ‘ 𝑌 ) ( .r ‘ ( 𝐼 mPoly 𝑅 ) ) ( ( ( 𝐼 extendVars 𝑅 ) ‘ 𝑌 ) ‘ ( 𝐸 ‘ ( ( 𝐾 + 1 ) − 1 ) ) ) ) ( +g ‘ ( 𝐼 mPoly 𝑅 ) ) ( ( ( 𝐼 extendVars 𝑅 ) ‘ 𝑌 ) ‘ ( 𝐸 ‘ ( 𝐾 + 1 ) ) ) ) ∈ ( Base ‘ ( 𝐼 mPoly 𝑅 ) ) ∧ ( ( 𝑄 ‘ ( ( ( ( 𝐼 mVar 𝑅 ) ‘ 𝑌 ) ( .r ‘ ( 𝐼 mPoly 𝑅 ) ) ( ( ( 𝐼 extendVars 𝑅 ) ‘ 𝑌 ) ‘ ( 𝐸 ‘ ( ( 𝐾 + 1 ) − 1 ) ) ) ) ( +g ‘ ( 𝐼 mPoly 𝑅 ) ) ( ( ( 𝐼 extendVars 𝑅 ) ‘ 𝑌 ) ‘ ( 𝐸 ‘ ( 𝐾 + 1 ) ) ) ) ) ‘ 𝑍 ) = ( ( ( 𝑍 ‘ 𝑌 ) · ( ( 𝑂 ‘ ( 𝐸 ‘ 𝐾 ) ) ‘ ( 𝑍 ↾ 𝐽 ) ) ) + ( ( 𝑂 ‘ ( 𝐸 ‘ ( 𝐾 + 1 ) ) ) ‘ ( 𝑍 ↾ 𝐽 ) ) ) ) )
92 91 simprd ⊢ ( 𝜑 → ( ( 𝑄 ‘ ( ( ( ( 𝐼 mVar 𝑅 ) ‘ 𝑌 ) ( .r ‘ ( 𝐼 mPoly 𝑅 ) ) ( ( ( 𝐼 extendVars 𝑅 ) ‘ 𝑌 ) ‘ ( 𝐸 ‘ ( ( 𝐾 + 1 ) − 1 ) ) ) ) ( +g ‘ ( 𝐼 mPoly 𝑅 ) ) ( ( ( 𝐼 extendVars 𝑅 ) ‘ 𝑌 ) ‘ ( 𝐸 ‘ ( 𝐾 + 1 ) ) ) ) ) ‘ 𝑍 ) = ( ( ( 𝑍 ‘ 𝑌 ) · ( ( 𝑂 ‘ ( 𝐸 ‘ 𝐾 ) ) ‘ ( 𝑍 ↾ 𝐽 ) ) ) + ( ( 𝑂 ‘ ( 𝐸 ‘ ( 𝐾 + 1 ) ) ) ‘ ( 𝑍 ↾ 𝐽 ) ) ) )
93 57 92 eqtrd ⊢ ( 𝜑 → ( ( 𝑄 ‘ 𝐹 ) ‘ 𝑍 ) = ( ( ( 𝑍 ‘ 𝑌 ) · ( ( 𝑂 ‘ ( 𝐸 ‘ 𝐾 ) ) ‘ ( 𝑍 ↾ 𝐽 ) ) ) + ( ( 𝑂 ‘ ( 𝐸 ‘ ( 𝐾 + 1 ) ) ) ‘ ( 𝑍 ↾ 𝐽 ) ) ) )