Theorem selvply1rhmlem5

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 )
	selvply1rhmlem5.f	⊢ ( 𝜑 → 𝐹 ∈ 𝐵 )
	selvply1rhmlem5.m	⊢ 𝑀 = ( 𝑞 ∈ ( Base ‘ ( { 𝑋 } mPoly 𝑈 ) ) ↦ ( 𝑠 ∈ ( ℕ0 ↑m 1o ) ↦ ( 𝑞 ‘ { ⟨ 𝑋 , ( 𝑠 ‘ ∅ ) ⟩ } ) ) )
Assertion	selvply1rhmlem5	⊢ ( 𝜑 → ( 𝐻 ‘ 𝐹 ) = ( 𝑀 ‘ ( ( ( 𝐼 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		selvply1rhmlem5.f	⊢ ( 𝜑 → 𝐹 ∈ 𝐵 )
10		selvply1rhmlem5.m	⊢ 𝑀 = ( 𝑞 ∈ ( Base ‘ ( { 𝑋 } mPoly 𝑈 ) ) ↦ ( 𝑠 ∈ ( ℕ0 ↑m 1o ) ↦ ( 𝑞 ‘ { ⟨ 𝑋 , ( 𝑠 ‘ ∅ ) ⟩ } ) ) )
11		fveq2	⊢ ( 𝑓 = 𝐹 → ( ( ( 𝐼 selectVars 𝑅 ) ‘ { 𝑋 } ) ‘ 𝑓 ) = ( ( ( 𝐼 selectVars 𝑅 ) ‘ { 𝑋 } ) ‘ 𝐹 ) )
12	11	fveq1d	⊢ ( 𝑓 = 𝐹 → ( ( ( ( 𝐼 selectVars 𝑅 ) ‘ { 𝑋 } ) ‘ 𝑓 ) ‘ { ⟨ 𝑋 , ( 𝑛 ‘ ∅ ) ⟩ } ) = ( ( ( ( 𝐼 selectVars 𝑅 ) ‘ { 𝑋 } ) ‘ 𝐹 ) ‘ { ⟨ 𝑋 , ( 𝑛 ‘ ∅ ) ⟩ } ) )
13	12	mpteq2dv	⊢ ( 𝑓 = 𝐹 → ( 𝑛 ∈ ( ℕ0 ↑m 1o ) ↦ ( ( ( ( 𝐼 selectVars 𝑅 ) ‘ { 𝑋 } ) ‘ 𝑓 ) ‘ { ⟨ 𝑋 , ( 𝑛 ‘ ∅ ) ⟩ } ) ) = ( 𝑛 ∈ ( ℕ0 ↑m 1o ) ↦ ( ( ( ( 𝐼 selectVars 𝑅 ) ‘ { 𝑋 } ) ‘ 𝐹 ) ‘ { ⟨ 𝑋 , ( 𝑛 ‘ ∅ ) ⟩ } ) ) )
14		ovexd	⊢ ( 𝜑 → ( ℕ0 ↑m 1o ) ∈ V )
15	14	mptexd	⊢ ( 𝜑 → ( 𝑛 ∈ ( ℕ0 ↑m 1o ) ↦ ( ( ( ( 𝐼 selectVars 𝑅 ) ‘ { 𝑋 } ) ‘ 𝐹 ) ‘ { ⟨ 𝑋 , ( 𝑛 ‘ ∅ ) ⟩ } ) ) ∈ V )
16	5 13 9 15	fvmptd3	⊢ ( 𝜑 → ( 𝐻 ‘ 𝐹 ) = ( 𝑛 ∈ ( ℕ0 ↑m 1o ) ↦ ( ( ( ( 𝐼 selectVars 𝑅 ) ‘ { 𝑋 } ) ‘ 𝐹 ) ‘ { ⟨ 𝑋 , ( 𝑛 ‘ ∅ ) ⟩ } ) ) )
17		fveq1	⊢ ( 𝑠 = 𝑛 → ( 𝑠 ‘ ∅ ) = ( 𝑛 ‘ ∅ ) )
18	17	opeq2d	⊢ ( 𝑠 = 𝑛 → ⟨ 𝑋 , ( 𝑠 ‘ ∅ ) ⟩ = ⟨ 𝑋 , ( 𝑛 ‘ ∅ ) ⟩ )
19	18	sneqd	⊢ ( 𝑠 = 𝑛 → { ⟨ 𝑋 , ( 𝑠 ‘ ∅ ) ⟩ } = { ⟨ 𝑋 , ( 𝑛 ‘ ∅ ) ⟩ } )
20	19	fveq2d	⊢ ( 𝑠 = 𝑛 → ( 𝑞 ‘ { ⟨ 𝑋 , ( 𝑠 ‘ ∅ ) ⟩ } ) = ( 𝑞 ‘ { ⟨ 𝑋 , ( 𝑛 ‘ ∅ ) ⟩ } ) )
21	20	cbvmptv	⊢ ( 𝑠 ∈ ( ℕ0 ↑m 1o ) ↦ ( 𝑞 ‘ { ⟨ 𝑋 , ( 𝑠 ‘ ∅ ) ⟩ } ) ) = ( 𝑛 ∈ ( ℕ0 ↑m 1o ) ↦ ( 𝑞 ‘ { ⟨ 𝑋 , ( 𝑛 ‘ ∅ ) ⟩ } ) )
22	21	mpteq2i	⊢ ( 𝑞 ∈ ( Base ‘ ( { 𝑋 } mPoly 𝑈 ) ) ↦ ( 𝑠 ∈ ( ℕ0 ↑m 1o ) ↦ ( 𝑞 ‘ { ⟨ 𝑋 , ( 𝑠 ‘ ∅ ) ⟩ } ) ) ) = ( 𝑞 ∈ ( Base ‘ ( { 𝑋 } mPoly 𝑈 ) ) ↦ ( 𝑛 ∈ ( ℕ0 ↑m 1o ) ↦ ( 𝑞 ‘ { ⟨ 𝑋 , ( 𝑛 ‘ ∅ ) ⟩ } ) ) )
23	10 22	eqtri	⊢ 𝑀 = ( 𝑞 ∈ ( Base ‘ ( { 𝑋 } mPoly 𝑈 ) ) ↦ ( 𝑛 ∈ ( ℕ0 ↑m 1o ) ↦ ( 𝑞 ‘ { ⟨ 𝑋 , ( 𝑛 ‘ ∅ ) ⟩ } ) ) )
24		fveq1	⊢ ( 𝑞 = ( ( ( 𝐼 selectVars 𝑅 ) ‘ { 𝑋 } ) ‘ 𝐹 ) → ( 𝑞 ‘ { ⟨ 𝑋 , ( 𝑛 ‘ ∅ ) ⟩ } ) = ( ( ( ( 𝐼 selectVars 𝑅 ) ‘ { 𝑋 } ) ‘ 𝐹 ) ‘ { ⟨ 𝑋 , ( 𝑛 ‘ ∅ ) ⟩ } ) )
25	24	mpteq2dv	⊢ ( 𝑞 = ( ( ( 𝐼 selectVars 𝑅 ) ‘ { 𝑋 } ) ‘ 𝐹 ) → ( 𝑛 ∈ ( ℕ0 ↑m 1o ) ↦ ( 𝑞 ‘ { ⟨ 𝑋 , ( 𝑛 ‘ ∅ ) ⟩ } ) ) = ( 𝑛 ∈ ( ℕ0 ↑m 1o ) ↦ ( ( ( ( 𝐼 selectVars 𝑅 ) ‘ { 𝑋 } ) ‘ 𝐹 ) ‘ { ⟨ 𝑋 , ( 𝑛 ‘ ∅ ) ⟩ } ) ) )
26		eqid	⊢ ( { 𝑋 } mPoly 𝑈 ) = ( { 𝑋 } mPoly 𝑈 )
27		eqid	⊢ ( Base ‘ ( { 𝑋 } mPoly 𝑈 ) ) = ( Base ‘ ( { 𝑋 } mPoly 𝑈 ) )
28	7	snssd	⊢ ( 𝜑 → { 𝑋 } ⊆ 𝐼 )
29	2 1 3 26 27 8 28 9	selvcl	⊢ ( 𝜑 → ( ( ( 𝐼 selectVars 𝑅 ) ‘ { 𝑋 } ) ‘ 𝐹 ) ∈ ( Base ‘ ( { 𝑋 } mPoly 𝑈 ) ) )
30	23 25 29 15	fvmptd3	⊢ ( 𝜑 → ( 𝑀 ‘ ( ( ( 𝐼 selectVars 𝑅 ) ‘ { 𝑋 } ) ‘ 𝐹 ) ) = ( 𝑛 ∈ ( ℕ0 ↑m 1o ) ↦ ( ( ( ( 𝐼 selectVars 𝑅 ) ‘ { 𝑋 } ) ‘ 𝐹 ) ‘ { ⟨ 𝑋 , ( 𝑛 ‘ ∅ ) ⟩ } ) ) )
31	16 30	eqtr4d	⊢ ( 𝜑 → ( 𝐻 ‘ 𝐹 ) = ( 𝑀 ‘ ( ( ( 𝐼 selectVars 𝑅 ) ‘ { 𝑋 } ) ‘ 𝐹 ) ) )