selvply1rhmlem3

	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 ` (/) ) >. } ) )

Metamath Proof Explorer

Theorem selvply1rhmlem3

Proof