Metamath Proof Explorer

Theorem selvply1rhmlem5

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 )
selvply1rhmlem5.f 
|- ( ph -> F e. B )
selvply1rhmlem5.m 
|- M = ( q e. ( Base ` ( { X } mPoly U ) ) |-> ( s e. ( NN0 ^m 1o ) |-> ( q ` { <. X , ( s ` (/) ) >. } ) ) )
Assertion selvply1rhmlem5 
|- ( ph -> ( H ` F ) = ( M ` ( ( ( I selectVars R ) ` { X } ) ` F ) ) )

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 selvply1rhmlem5.f 
 |-  ( ph -> F e. B )
10 selvply1rhmlem5.m 
 |-  M = ( q e. ( Base ` ( { X } mPoly U ) ) |-> ( s e. ( NN0 ^m 1o ) |-> ( q ` { <. X , ( s ` (/) ) >. } ) ) )
11 fveq2 
 |-  ( f = F -> ( ( ( I selectVars R ) ` { X } ) ` f ) = ( ( ( I selectVars R ) ` { X } ) ` F ) )
12 11 fveq1d 
 |-  ( f = F -> ( ( ( ( I selectVars R ) ` { X } ) ` f ) ` { <. X , ( n ` (/) ) >. } ) = ( ( ( ( I selectVars R ) ` { X } ) ` F ) ` { <. X , ( n ` (/) ) >. } ) )
13 12 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 ` (/) ) >. } ) ) )
14 ovexd 
 |-  ( ph -> ( NN0 ^m 1o ) e. _V )
15 14 mptexd 
 |-  ( ph -> ( n e. ( NN0 ^m 1o ) |-> ( ( ( ( I selectVars R ) ` { X } ) ` F ) ` { <. X , ( n ` (/) ) >. } ) ) e. _V )
16 5 13 9 15 fvmptd3 
 |-  ( ph -> ( H ` F ) = ( n e. ( NN0 ^m 1o ) |-> ( ( ( ( I selectVars R ) ` { X } ) ` F ) ` { <. X , ( n ` (/) ) >. } ) ) )
17 fveq1 
 |-  ( s = n -> ( s ` (/) ) = ( n ` (/) ) )
18 17 opeq2d 
 |-  ( s = n -> <. X , ( s ` (/) ) >. = <. X , ( n ` (/) ) >. )
19 18 sneqd 
 |-  ( s = n -> { <. X , ( s ` (/) ) >. } = { <. X , ( n ` (/) ) >. } )
20 19 fveq2d 
 |-  ( s = n -> ( q ` { <. X , ( s ` (/) ) >. } ) = ( q ` { <. X , ( n ` (/) ) >. } ) )
21 20 cbvmptv 
 |-  ( s e. ( NN0 ^m 1o ) |-> ( q ` { <. X , ( s ` (/) ) >. } ) ) = ( n e. ( NN0 ^m 1o ) |-> ( q ` { <. X , ( n ` (/) ) >. } ) )
22 21 mpteq2i 
 |-  ( q e. ( Base ` ( { X } mPoly U ) ) |-> ( s e. ( NN0 ^m 1o ) |-> ( q ` { <. X , ( s ` (/) ) >. } ) ) ) = ( q e. ( Base ` ( { X } mPoly U ) ) |-> ( n e. ( NN0 ^m 1o ) |-> ( q ` { <. X , ( n ` (/) ) >. } ) ) )
23 10 22 eqtri 
 |-  M = ( q e. ( Base ` ( { X } mPoly U ) ) |-> ( n e. ( NN0 ^m 1o ) |-> ( q ` { <. X , ( n ` (/) ) >. } ) ) )
24 fveq1 
 |-  ( q = ( ( ( I selectVars R ) ` { X } ) ` F ) -> ( q ` { <. X , ( n ` (/) ) >. } ) = ( ( ( ( I selectVars R ) ` { X } ) ` F ) ` { <. X , ( n ` (/) ) >. } ) )
25 24 mpteq2dv 
 |-  ( q = ( ( ( I selectVars R ) ` { X } ) ` F ) -> ( n e. ( NN0 ^m 1o ) |-> ( q ` { <. X , ( n ` (/) ) >. } ) ) = ( n e. ( NN0 ^m 1o ) |-> ( ( ( ( I selectVars R ) ` { X } ) ` F ) ` { <. X , ( n ` (/) ) >. } ) ) )
26 eqid 
 |-  ( { X } mPoly U ) = ( { X } mPoly U )
27 eqid 
 |-  ( Base ` ( { X } mPoly U ) ) = ( Base ` ( { X } mPoly U ) )
28 7 snssd 
 |-  ( ph -> { X } C_ I )
29 2 1 3 26 27 8 28 9 selvcl 
 |-  ( ph -> ( ( ( I selectVars R ) ` { X } ) ` F ) e. ( Base ` ( { X } mPoly U ) ) )
30 23 25 29 15 fvmptd3 
 |-  ( ph -> ( M ` ( ( ( I selectVars R ) ` { X } ) ` F ) ) = ( n e. ( NN0 ^m 1o ) |-> ( ( ( ( I selectVars R ) ` { X } ) ` F ) ` { <. X , ( n ` (/) ) >. } ) ) )
31 16 30 eqtr4d 
 |-  ( ph -> ( H ` F ) = ( M ` ( ( ( I selectVars R ) ` { X } ) ` F ) ) )