This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 𝑅 ) ‘ { 𝑋 } ) ‘ 𝐹 ) ‘ { ⟨ 𝑋 , ( 𝑁 ‘ ∅ ) ⟩ } ) )