Metamath Proof Explorer

Theorem selvply1rhmlem3

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

Ref Expression
Hypotheses selvply1rhm.1 
|- B = ( Base ` P )
selvply1rhm.2 
|- P = ( I mPoly R )
selvply1rhm.3 
|- U = ( ( I \ { X } ) mPoly R )
selvply1rhm.4 
|- Q = ( Poly1 ` U )
selvply1rhm.5 
|- H = ( f e. B |-> ( n e. ( NN0 ^m 1o ) |-> ( ( ( ( I selectVars R ) ` { X } ) ` f ) ` { <. X , ( n ` (/) ) >. } ) ) )
selvply1rhm.6 
|- ( ph -> I e. V )
selvply1rhm.7 
|- ( ph -> X e. I )
selvply1rhm.8 
|- ( ph -> R e. CRing )
selvply1rhmlem3.f 
|- ( ph -> F e. B )
selvply1rhmlem3.n 
|- ( ph -> N e. ( NN0 ^m 1o ) )
Assertion selvply1rhmlem3 
|- ( ph -> ( ( H ` F ) ` N ) = ( ( ( ( I selectVars R ) ` { X } ) ` F ) ` { <. X , ( N ` (/) ) >. } ) )

Proof

Step Hyp Ref Expression
1 selvply1rhm.1 
 |-  B = ( Base ` P )
2 selvply1rhm.2 
 |-  P = ( I mPoly R )
3 selvply1rhm.3 
 |-  U = ( ( I \ { X } ) mPoly R )
4 selvply1rhm.4 
 |-  Q = ( Poly1 ` U )
5 selvply1rhm.5 
 |-  H = ( f e. B |-> ( n e. ( NN0 ^m 1o ) |-> ( ( ( ( I selectVars R ) ` { X } ) ` f ) ` { <. X , ( n ` (/) ) >. } ) ) )
6 selvply1rhm.6 
 |-  ( ph -> I e. V )
7 selvply1rhm.7 
 |-  ( ph -> X e. I )
8 selvply1rhm.8 
 |-  ( ph -> R e. CRing )
9 selvply1rhmlem3.f 
 |-  ( ph -> F e. B )
10 selvply1rhmlem3.n 
 |-  ( ph -> N e. ( NN0 ^m 1o ) )
11 fveq1 
 |-  ( m = N -> ( m ` (/) ) = ( N ` (/) ) )
12 11 opeq2d 
 |-  ( m = N -> <. X , ( m ` (/) ) >. = <. X , ( N ` (/) ) >. )
13 12 sneqd 
 |-  ( m = N -> { <. X , ( m ` (/) ) >. } = { <. X , ( N ` (/) ) >. } )
14 13 fveq2d 
 |-  ( m = N -> ( ( ( ( I selectVars R ) ` { X } ) ` F ) ` { <. X , ( m ` (/) ) >. } ) = ( ( ( ( I selectVars R ) ` { X } ) ` F ) ` { <. X , ( N ` (/) ) >. } ) )
15 fveq2 
 |-  ( f = F -> ( ( ( I selectVars R ) ` { X } ) ` f ) = ( ( ( I selectVars R ) ` { X } ) ` F ) )
16 15 fveq1d 
 |-  ( f = F -> ( ( ( ( I selectVars R ) ` { X } ) ` f ) ` { <. X , ( n ` (/) ) >. } ) = ( ( ( ( I selectVars R ) ` { X } ) ` F ) ` { <. X , ( n ` (/) ) >. } ) )
17 16 mpteq2dv 
 |-  ( f = F -> ( n e. ( NN0 ^m 1o ) |-> ( ( ( ( I selectVars R ) ` { X } ) ` f ) ` { <. X , ( n ` (/) ) >. } ) ) = ( n e. ( NN0 ^m 1o ) |-> ( ( ( ( I selectVars R ) ` { X } ) ` F ) ` { <. X , ( n ` (/) ) >. } ) ) )
18 ovexd 
 |-  ( ph -> ( NN0 ^m 1o ) e. _V )
19 18 mptexd 
 |-  ( ph -> ( n e. ( NN0 ^m 1o ) |-> ( ( ( ( I selectVars R ) ` { X } ) ` F ) ` { <. X , ( n ` (/) ) >. } ) ) e. _V )
20 5 17 9 19 fvmptd3 
 |-  ( ph -> ( H ` F ) = ( n e. ( NN0 ^m 1o ) |-> ( ( ( ( I selectVars R ) ` { X } ) ` F ) ` { <. X , ( n ` (/) ) >. } ) ) )
21 fveq1 
 |-  ( n = m -> ( n ` (/) ) = ( m ` (/) ) )
22 21 opeq2d 
 |-  ( n = m -> <. X , ( n ` (/) ) >. = <. X , ( m ` (/) ) >. )
23 22 sneqd 
 |-  ( n = m -> { <. X , ( n ` (/) ) >. } = { <. X , ( m ` (/) ) >. } )
24 23 fveq2d 
 |-  ( n = m -> ( ( ( ( I selectVars R ) ` { X } ) ` F ) ` { <. X , ( n ` (/) ) >. } ) = ( ( ( ( I selectVars R ) ` { X } ) ` F ) ` { <. X , ( m ` (/) ) >. } ) )
25 24 cbvmptv 
 |-  ( n e. ( NN0 ^m 1o ) |-> ( ( ( ( I selectVars R ) ` { X } ) ` F ) ` { <. X , ( n ` (/) ) >. } ) ) = ( m e. ( NN0 ^m 1o ) |-> ( ( ( ( I selectVars R ) ` { X } ) ` F ) ` { <. X , ( m ` (/) ) >. } ) )
26 20 25 eqtrdi 
 |-  ( ph -> ( H ` F ) = ( m e. ( NN0 ^m 1o ) |-> ( ( ( ( I selectVars R ) ` { X } ) ` F ) ` { <. X , ( m ` (/) ) >. } ) ) )
27 fvexd 
 |-  ( ph -> ( ( ( ( I selectVars R ) ` { X } ) ` F ) ` { <. X , ( N ` (/) ) >. } ) e. _V )
28 14 26 10 27 fvmptd4 
 |-  ( ph -> ( ( H ` F ) ` N ) = ( ( ( ( I selectVars R ) ` { X } ) ` F ) ` { <. X , ( N ` (/) ) >. } ) )