Theorem selvply1rhmlem3

Description: Lemma for selvply1rhm . (Contributed by Thierry Arnoux, 4-May-2026)

	Ref	Expression
Hypotheses	selvply1rhm.1	⊢ 𝐵 = ( Base ‘ 𝑃 )
	selvply1rhm.2	⊢ 𝑃 = ( 𝐼 mPoly 𝑅 )
	selvply1rhm.3	⊢ 𝑈 = ( ( 𝐼 ∖ { 𝑋 } ) mPoly 𝑅 )
	selvply1rhm.4	⊢ 𝑄 = ( Poly1 ‘ 𝑈 )
	selvply1rhm.5	⊢ 𝐻 = ( 𝑓 ∈ 𝐵 ↦ ( 𝑛 ∈ ( ℕ0 ↑m 1o ) ↦ ( ( ( ( 𝐼 selectVars 𝑅 ) ‘ { 𝑋 } ) ‘ 𝑓 ) ‘ { ⟨ 𝑋 , ( 𝑛 ‘ ∅ ) ⟩ } ) ) )
	selvply1rhm.6	⊢ ( 𝜑 → 𝐼 ∈ 𝑉 )
	selvply1rhm.7	⊢ ( 𝜑 → 𝑋 ∈ 𝐼 )
	selvply1rhm.8	⊢ ( 𝜑 → 𝑅 ∈ CRing )
	selvply1rhmlem3.f	⊢ ( 𝜑 → 𝐹 ∈ 𝐵 )
	selvply1rhmlem3.n	⊢ ( 𝜑 → 𝑁 ∈ ( ℕ0 ↑m 1o ) )
Assertion	selvply1rhmlem3	⊢ ( 𝜑 → ( ( 𝐻 ‘ 𝐹 ) ‘ 𝑁 ) = ( ( ( ( 𝐼 selectVars 𝑅 ) ‘ { 𝑋 } ) ‘ 𝐹 ) ‘ { ⟨ 𝑋 , ( 𝑁 ‘ ∅ ) ⟩ } ) )

Proof

Step	Hyp	Ref	Expression
1		selvply1rhm.1	⊢ 𝐵 = ( Base ‘ 𝑃 )
2		selvply1rhm.2	⊢ 𝑃 = ( 𝐼 mPoly 𝑅 )
3		selvply1rhm.3	⊢ 𝑈 = ( ( 𝐼 ∖ { 𝑋 } ) mPoly 𝑅 )
4		selvply1rhm.4	⊢ 𝑄 = ( Poly1 ‘ 𝑈 )
5		selvply1rhm.5	⊢ 𝐻 = ( 𝑓 ∈ 𝐵 ↦ ( 𝑛 ∈ ( ℕ0 ↑m 1o ) ↦ ( ( ( ( 𝐼 selectVars 𝑅 ) ‘ { 𝑋 } ) ‘ 𝑓 ) ‘ { ⟨ 𝑋 , ( 𝑛 ‘ ∅ ) ⟩ } ) ) )
6		selvply1rhm.6	⊢ ( 𝜑 → 𝐼 ∈ 𝑉 )
7		selvply1rhm.7	⊢ ( 𝜑 → 𝑋 ∈ 𝐼 )
8		selvply1rhm.8	⊢ ( 𝜑 → 𝑅 ∈ CRing )
9		selvply1rhmlem3.f	⊢ ( 𝜑 → 𝐹 ∈ 𝐵 )
10		selvply1rhmlem3.n	⊢ ( 𝜑 → 𝑁 ∈ ( ℕ0 ↑m 1o ) )
11		fveq1	⊢ ( 𝑚 = 𝑁 → ( 𝑚 ‘ ∅ ) = ( 𝑁 ‘ ∅ ) )
12	11	opeq2d	⊢ ( 𝑚 = 𝑁 → ⟨ 𝑋 , ( 𝑚 ‘ ∅ ) ⟩ = ⟨ 𝑋 , ( 𝑁 ‘ ∅ ) ⟩ )
13	12	sneqd	⊢ ( 𝑚 = 𝑁 → { ⟨ 𝑋 , ( 𝑚 ‘ ∅ ) ⟩ } = { ⟨ 𝑋 , ( 𝑁 ‘ ∅ ) ⟩ } )
14	13	fveq2d	⊢ ( 𝑚 = 𝑁 → ( ( ( ( 𝐼 selectVars 𝑅 ) ‘ { 𝑋 } ) ‘ 𝐹 ) ‘ { ⟨ 𝑋 , ( 𝑚 ‘ ∅ ) ⟩ } ) = ( ( ( ( 𝐼 selectVars 𝑅 ) ‘ { 𝑋 } ) ‘ 𝐹 ) ‘ { ⟨ 𝑋 , ( 𝑁 ‘ ∅ ) ⟩ } ) )
15		fveq2	⊢ ( 𝑓 = 𝐹 → ( ( ( 𝐼 selectVars 𝑅 ) ‘ { 𝑋 } ) ‘ 𝑓 ) = ( ( ( 𝐼 selectVars 𝑅 ) ‘ { 𝑋 } ) ‘ 𝐹 ) )
16	15	fveq1d	⊢ ( 𝑓 = 𝐹 → ( ( ( ( 𝐼 selectVars 𝑅 ) ‘ { 𝑋 } ) ‘ 𝑓 ) ‘ { ⟨ 𝑋 , ( 𝑛 ‘ ∅ ) ⟩ } ) = ( ( ( ( 𝐼 selectVars 𝑅 ) ‘ { 𝑋 } ) ‘ 𝐹 ) ‘ { ⟨ 𝑋 , ( 𝑛 ‘ ∅ ) ⟩ } ) )
17	16	mpteq2dv	⊢ ( 𝑓 = 𝐹 → ( 𝑛 ∈ ( ℕ0 ↑m 1o ) ↦ ( ( ( ( 𝐼 selectVars 𝑅 ) ‘ { 𝑋 } ) ‘ 𝑓 ) ‘ { ⟨ 𝑋 , ( 𝑛 ‘ ∅ ) ⟩ } ) ) = ( 𝑛 ∈ ( ℕ0 ↑m 1o ) ↦ ( ( ( ( 𝐼 selectVars 𝑅 ) ‘ { 𝑋 } ) ‘ 𝐹 ) ‘ { ⟨ 𝑋 , ( 𝑛 ‘ ∅ ) ⟩ } ) ) )
18		ovexd	⊢ ( 𝜑 → ( ℕ0 ↑m 1o ) ∈ V )
19	18	mptexd	⊢ ( 𝜑 → ( 𝑛 ∈ ( ℕ0 ↑m 1o ) ↦ ( ( ( ( 𝐼 selectVars 𝑅 ) ‘ { 𝑋 } ) ‘ 𝐹 ) ‘ { ⟨ 𝑋 , ( 𝑛 ‘ ∅ ) ⟩ } ) ) ∈ V )
20	5 17 9 19	fvmptd3	⊢ ( 𝜑 → ( 𝐻 ‘ 𝐹 ) = ( 𝑛 ∈ ( ℕ0 ↑m 1o ) ↦ ( ( ( ( 𝐼 selectVars 𝑅 ) ‘ { 𝑋 } ) ‘ 𝐹 ) ‘ { ⟨ 𝑋 , ( 𝑛 ‘ ∅ ) ⟩ } ) ) )
21		fveq1	⊢ ( 𝑛 = 𝑚 → ( 𝑛 ‘ ∅ ) = ( 𝑚 ‘ ∅ ) )
22	21	opeq2d	⊢ ( 𝑛 = 𝑚 → ⟨ 𝑋 , ( 𝑛 ‘ ∅ ) ⟩ = ⟨ 𝑋 , ( 𝑚 ‘ ∅ ) ⟩ )
23	22	sneqd	⊢ ( 𝑛 = 𝑚 → { ⟨ 𝑋 , ( 𝑛 ‘ ∅ ) ⟩ } = { ⟨ 𝑋 , ( 𝑚 ‘ ∅ ) ⟩ } )
24	23	fveq2d	⊢ ( 𝑛 = 𝑚 → ( ( ( ( 𝐼 selectVars 𝑅 ) ‘ { 𝑋 } ) ‘ 𝐹 ) ‘ { ⟨ 𝑋 , ( 𝑛 ‘ ∅ ) ⟩ } ) = ( ( ( ( 𝐼 selectVars 𝑅 ) ‘ { 𝑋 } ) ‘ 𝐹 ) ‘ { ⟨ 𝑋 , ( 𝑚 ‘ ∅ ) ⟩ } ) )
25	24	cbvmptv	⊢ ( 𝑛 ∈ ( ℕ0 ↑m 1o ) ↦ ( ( ( ( 𝐼 selectVars 𝑅 ) ‘ { 𝑋 } ) ‘ 𝐹 ) ‘ { ⟨ 𝑋 , ( 𝑛 ‘ ∅ ) ⟩ } ) ) = ( 𝑚 ∈ ( ℕ0 ↑m 1o ) ↦ ( ( ( ( 𝐼 selectVars 𝑅 ) ‘ { 𝑋 } ) ‘ 𝐹 ) ‘ { ⟨ 𝑋 , ( 𝑚 ‘ ∅ ) ⟩ } ) )
26	20 25	eqtrdi	⊢ ( 𝜑 → ( 𝐻 ‘ 𝐹 ) = ( 𝑚 ∈ ( ℕ0 ↑m 1o ) ↦ ( ( ( ( 𝐼 selectVars 𝑅 ) ‘ { 𝑋 } ) ‘ 𝐹 ) ‘ { ⟨ 𝑋 , ( 𝑚 ‘ ∅ ) ⟩ } ) ) )
27		fvexd	⊢ ( 𝜑 → ( ( ( ( 𝐼 selectVars 𝑅 ) ‘ { 𝑋 } ) ‘ 𝐹 ) ‘ { ⟨ 𝑋 , ( 𝑁 ‘ ∅ ) ⟩ } ) ∈ V )
28	14 26 10 27	fvmptd4	⊢ ( 𝜑 → ( ( 𝐻 ‘ 𝐹 ) ‘ 𝑁 ) = ( ( ( ( 𝐼 selectVars 𝑅 ) ‘ { 𝑋 } ) ‘ 𝐹 ) ‘ { ⟨ 𝑋 , ( 𝑁 ‘ ∅ ) ⟩ } ) )