selvply1rhm0

Description: The ring homomorphism H built in selvply1rhm is injective. (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 )
	selvply1rhm0.1	\|- .0. = ( 0g ` Q )
	selvply1rhm0.2	\|- Z = ( 0g ` P )
	selvply1rhm0.3	\|- ( ph -> F e. B )
	selvply1rhm0.4	\|- ( ph -> ( H ` F ) = .0. )
Assertion	selvply1rhm0	\|- ( ph -> F = Z )

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		selvply1rhm0.1	\|- .0. = ( 0g ` Q )
10		selvply1rhm0.2	\|- Z = ( 0g ` P )
11		selvply1rhm0.3	\|- ( ph -> F e. B )
12		selvply1rhm0.4	\|- ( ph -> ( H ` F ) = .0. )
13		eqid	\|- ( Base ` R ) = ( Base ` R )
14		eqid	\|- { h e. ( NN0 ^m I ) \| h finSupp 0 } = { h e. ( NN0 ^m I ) \| h finSupp 0 }
15	14	psrbasfsupp	\|- { h e. ( NN0 ^m I ) \| h finSupp 0 } = { h e. ( NN0 ^m I ) \| ( `' h " NN ) e. Fin }
16	2 13 1 15 11	mplelf	\|- ( ph -> F : { h e. ( NN0 ^m I ) \| h finSupp 0 } --> ( Base ` R ) )
17	16	feqmptd	\|- ( ph -> F = ( p e. { h e. ( NN0 ^m I ) \| h finSupp 0 } \|-> ( F ` p ) ) )
18		nn0ex	\|- NN0 e. _V
19	18	a1i	\|- ( ( ph /\ p e. { h e. ( NN0 ^m I ) \| h finSupp 0 } ) -> NN0 e. _V )
20		1oex	\|- 1o e. _V
21	20	a1i	\|- ( ( ph /\ p e. { h e. ( NN0 ^m I ) \| h finSupp 0 } ) -> 1o e. _V )
22		df1o2	\|- 1o = { (/) }
23	22	eqcomi	\|- { (/) } = 1o
24	23	a1i	\|- ( ( ph /\ p e. { h e. ( NN0 ^m I ) \| h finSupp 0 } ) -> { (/) } = 1o )
25		0ex	\|- (/) e. _V
26	25	a1i	\|- ( ( ph /\ p e. { h e. ( NN0 ^m I ) \| h finSupp 0 } ) -> (/) e. _V )
27	6	adantr	\|- ( ( ph /\ p e. { h e. ( NN0 ^m I ) \| h finSupp 0 } ) -> I e. V )
28		ssrab2	\|- { h e. ( NN0 ^m I ) \| h finSupp 0 } C_ ( NN0 ^m I )
29	28	a1i	\|- ( ph -> { h e. ( NN0 ^m I ) \| h finSupp 0 } C_ ( NN0 ^m I ) )
30	29	sselda	\|- ( ( ph /\ p e. { h e. ( NN0 ^m I ) \| h finSupp 0 } ) -> p e. ( NN0 ^m I ) )
31	27 19 30	elmaprd	\|- ( ( ph /\ p e. { h e. ( NN0 ^m I ) \| h finSupp 0 } ) -> p : I --> NN0 )
32	7	adantr	\|- ( ( ph /\ p e. { h e. ( NN0 ^m I ) \| h finSupp 0 } ) -> X e. I )
33	31 32	ffvelcdmd	\|- ( ( ph /\ p e. { h e. ( NN0 ^m I ) \| h finSupp 0 } ) -> ( p ` X ) e. NN0 )
34	26 33	fsnd	\|- ( ( ph /\ p e. { h e. ( NN0 ^m I ) \| h finSupp 0 } ) -> { <. (/) , ( p ` X ) >. } : { (/) } --> NN0 )
35	24 34	feq2dd	\|- ( ( ph /\ p e. { h e. ( NN0 ^m I ) \| h finSupp 0 } ) -> { <. (/) , ( p ` X ) >. } : 1o --> NN0 )
36	19 21 35	elmapdd	\|- ( ( ph /\ p e. { h e. ( NN0 ^m I ) \| h finSupp 0 } ) -> { <. (/) , ( p ` X ) >. } e. ( NN0 ^m 1o ) )
37		psr1baslem	\|- ( NN0 ^m 1o ) = { h e. ( NN0 ^m 1o ) \| ( `' h " NN ) e. Fin }
38		eqid	\|- { h e. ( NN0 ^m 1o ) \| h finSupp 0 } = { h e. ( NN0 ^m 1o ) \| h finSupp 0 }
39	38	psrbasfsupp	\|- { h e. ( NN0 ^m 1o ) \| h finSupp 0 } = { h e. ( NN0 ^m 1o ) \| ( `' h " NN ) e. Fin }
40	37 39	eqtr4i	\|- ( NN0 ^m 1o ) = { h e. ( NN0 ^m 1o ) \| h finSupp 0 }
41	36 40	eleqtrdi	\|- ( ( ph /\ p e. { h e. ( NN0 ^m I ) \| h finSupp 0 } ) -> { <. (/) , ( p ` X ) >. } e. { h e. ( NN0 ^m 1o ) \| h finSupp 0 } )
42		fvex	\|- ( 0g ` U ) e. _V
43	42	fvconst2	\|- ( { <. (/) , ( p ` X ) >. } e. { h e. ( NN0 ^m 1o ) \| h finSupp 0 } -> ( ( { h e. ( NN0 ^m 1o ) \| h finSupp 0 } X. { ( 0g ` U ) } ) ` { <. (/) , ( p ` X ) >. } ) = ( 0g ` U ) )
44	41 43	syl	\|- ( ( ph /\ p e. { h e. ( NN0 ^m I ) \| h finSupp 0 } ) -> ( ( { h e. ( NN0 ^m 1o ) \| h finSupp 0 } X. { ( 0g ` U ) } ) ` { <. (/) , ( p ` X ) >. } ) = ( 0g ` U ) )
45	31	ffnd	\|- ( ( ph /\ p e. { h e. ( NN0 ^m I ) \| h finSupp 0 } ) -> p Fn I )
46		fnressn	\|- ( ( p Fn I /\ X e. I ) -> ( p \|` { X } ) = { <. X , ( p ` X ) >. } )
47	45 32 46	syl2anc	\|- ( ( ph /\ p e. { h e. ( NN0 ^m I ) \| h finSupp 0 } ) -> ( p \|` { X } ) = { <. X , ( p ` X ) >. } )
48		fvex	\|- ( p ` X ) e. _V
49	25 48	fvsn	\|- ( { <. (/) , ( p ` X ) >. } ` (/) ) = ( p ` X )
50	49	opeq2i	\|- <. X , ( { <. (/) , ( p ` X ) >. } ` (/) ) >. = <. X , ( p ` X ) >.
51	50	sneqi	\|- { <. X , ( { <. (/) , ( p ` X ) >. } ` (/) ) >. } = { <. X , ( p ` X ) >. }
52	47 51	eqtr4di	\|- ( ( ph /\ p e. { h e. ( NN0 ^m I ) \| h finSupp 0 } ) -> ( p \|` { X } ) = { <. X , ( { <. (/) , ( p ` X ) >. } ` (/) ) >. } )
53	52	fveq2d	\|- ( ( ph /\ p e. { h e. ( NN0 ^m I ) \| h finSupp 0 } ) -> ( ( ( ( I selectVars R ) ` { X } ) ` F ) ` ( p \|` { X } ) ) = ( ( ( ( I selectVars R ) ` { X } ) ` F ) ` { <. X , ( { <. (/) , ( p ` X ) >. } ` (/) ) >. } ) )
54	8	adantr	\|- ( ( ph /\ p e. { h e. ( NN0 ^m I ) \| h finSupp 0 } ) -> R e. CRing )
55	11	adantr	\|- ( ( ph /\ p e. { h e. ( NN0 ^m I ) \| h finSupp 0 } ) -> F e. B )
56	1 2 3 4 5 27 32 54 55 36	selvply1rhmlem3	\|- ( ( ph /\ p e. { h e. ( NN0 ^m I ) \| h finSupp 0 } ) -> ( ( H ` F ) ` { <. (/) , ( p ` X ) >. } ) = ( ( ( ( I selectVars R ) ` { X } ) ` F ) ` { <. X , ( { <. (/) , ( p ` X ) >. } ` (/) ) >. } ) )
57		eqid	\|- ( 1o mPoly U ) = ( 1o mPoly U )
58		eqid	\|- ( 0g ` U ) = ( 0g ` U )
59	57 4 9	ply1mpl0	\|- .0. = ( 0g ` ( 1o mPoly U ) )
60	20	a1i	\|- ( ph -> 1o e. _V )
61	6	difexd	\|- ( ph -> ( I \ { X } ) e. _V )
62	8	crngringd	\|- ( ph -> R e. Ring )
63	3 61 62	mplringd	\|- ( ph -> U e. Ring )
64	63	ringgrpd	\|- ( ph -> U e. Grp )
65	57 39 58 59 60 64	mpl0	\|- ( ph -> .0. = ( { h e. ( NN0 ^m 1o ) \| h finSupp 0 } X. { ( 0g ` U ) } ) )
66	12 65	eqtrd	\|- ( ph -> ( H ` F ) = ( { h e. ( NN0 ^m 1o ) \| h finSupp 0 } X. { ( 0g ` U ) } ) )
67	66	fveq1d	\|- ( ph -> ( ( H ` F ) ` { <. (/) , ( p ` X ) >. } ) = ( ( { h e. ( NN0 ^m 1o ) \| h finSupp 0 } X. { ( 0g ` U ) } ) ` { <. (/) , ( p ` X ) >. } ) )
68	67	adantr	\|- ( ( ph /\ p e. { h e. ( NN0 ^m I ) \| h finSupp 0 } ) -> ( ( H ` F ) ` { <. (/) , ( p ` X ) >. } ) = ( ( { h e. ( NN0 ^m 1o ) \| h finSupp 0 } X. { ( 0g ` U ) } ) ` { <. (/) , ( p ` X ) >. } ) )
69	53 56 68	3eqtr2rd	\|- ( ( ph /\ p e. { h e. ( NN0 ^m I ) \| h finSupp 0 } ) -> ( ( { h e. ( NN0 ^m 1o ) \| h finSupp 0 } X. { ( 0g ` U ) } ) ` { <. (/) , ( p ` X ) >. } ) = ( ( ( ( I selectVars R ) ` { X } ) ` F ) ` ( p \|` { X } ) ) )
70		eqid	\|- { h e. ( NN0 ^m ( I \ { X } ) ) \| h finSupp 0 } = { h e. ( NN0 ^m ( I \ { X } ) ) \| h finSupp 0 }
71	70	psrbasfsupp	\|- { h e. ( NN0 ^m ( I \ { X } ) ) \| h finSupp 0 } = { h e. ( NN0 ^m ( I \ { X } ) ) \| ( `' h " NN ) e. Fin }
72		eqid	\|- ( 0g ` R ) = ( 0g ` R )
73	61	adantr	\|- ( ( ph /\ p e. { h e. ( NN0 ^m I ) \| h finSupp 0 } ) -> ( I \ { X } ) e. _V )
74	62	ringgrpd	\|- ( ph -> R e. Grp )
75	74	adantr	\|- ( ( ph /\ p e. { h e. ( NN0 ^m I ) \| h finSupp 0 } ) -> R e. Grp )
76	3 71 72 58 73 75	mpl0	\|- ( ( ph /\ p e. { h e. ( NN0 ^m I ) \| h finSupp 0 } ) -> ( 0g ` U ) = ( { h e. ( NN0 ^m ( I \ { X } ) ) \| h finSupp 0 } X. { ( 0g ` R ) } ) )
77	44 69 76	3eqtr3d	\|- ( ( ph /\ p e. { h e. ( NN0 ^m I ) \| h finSupp 0 } ) -> ( ( ( ( I selectVars R ) ` { X } ) ` F ) ` ( p \|` { X } ) ) = ( { h e. ( NN0 ^m ( I \ { X } ) ) \| h finSupp 0 } X. { ( 0g ` R ) } ) )
78	77	fveq1d	\|- ( ( ph /\ p e. { h e. ( NN0 ^m I ) \| h finSupp 0 } ) -> ( ( ( ( ( I selectVars R ) ` { X } ) ` F ) ` ( p \|` { X } ) ) ` ( p \|` ( I \ { X } ) ) ) = ( ( { h e. ( NN0 ^m ( I \ { X } ) ) \| h finSupp 0 } X. { ( 0g ` R ) } ) ` ( p \|` ( I \ { X } ) ) ) )
79	7	snssd	\|- ( ph -> { X } C_ I )
80	79	adantr	\|- ( ( ph /\ p e. { h e. ( NN0 ^m I ) \| h finSupp 0 } ) -> { X } C_ I )
81		simpr	\|- ( ( ph /\ p e. { h e. ( NN0 ^m I ) \| h finSupp 0 } ) -> p e. { h e. ( NN0 ^m I ) \| h finSupp 0 } )
82	15 2 1 54 80 55 81	selvvvval	\|- ( ( ph /\ p e. { h e. ( NN0 ^m I ) \| h finSupp 0 } ) -> ( ( ( ( ( I selectVars R ) ` { X } ) ` F ) ` ( p \|` { X } ) ) ` ( p \|` ( I \ { X } ) ) ) = ( F ` p ) )
83		breq1	\|- ( h = ( p \|` ( I \ { X } ) ) -> ( h finSupp 0 <-> ( p \|` ( I \ { X } ) ) finSupp 0 ) )
84		difssd	\|- ( ( ph /\ p e. { h e. ( NN0 ^m I ) \| h finSupp 0 } ) -> ( I \ { X } ) C_ I )
85	30 84	elmapssresd	\|- ( ( ph /\ p e. { h e. ( NN0 ^m I ) \| h finSupp 0 } ) -> ( p \|` ( I \ { X } ) ) e. ( NN0 ^m ( I \ { X } ) ) )
86		breq1	\|- ( h = p -> ( h finSupp 0 <-> p finSupp 0 ) )
87	86 81	elrabrd	\|- ( ( ph /\ p e. { h e. ( NN0 ^m I ) \| h finSupp 0 } ) -> p finSupp 0 )
88		c0ex	\|- 0 e. _V
89	88	a1i	\|- ( ( ph /\ p e. { h e. ( NN0 ^m I ) \| h finSupp 0 } ) -> 0 e. _V )
90	87 89	fsuppres	\|- ( ( ph /\ p e. { h e. ( NN0 ^m I ) \| h finSupp 0 } ) -> ( p \|` ( I \ { X } ) ) finSupp 0 )
91	83 85 90	elrabd	\|- ( ( ph /\ p e. { h e. ( NN0 ^m I ) \| h finSupp 0 } ) -> ( p \|` ( I \ { X } ) ) e. { h e. ( NN0 ^m ( I \ { X } ) ) \| h finSupp 0 } )
92		fvex	\|- ( 0g ` R ) e. _V
93	92	fvconst2	\|- ( ( p \|` ( I \ { X } ) ) e. { h e. ( NN0 ^m ( I \ { X } ) ) \| h finSupp 0 } -> ( ( { h e. ( NN0 ^m ( I \ { X } ) ) \| h finSupp 0 } X. { ( 0g ` R ) } ) ` ( p \|` ( I \ { X } ) ) ) = ( 0g ` R ) )
94	91 93	syl	\|- ( ( ph /\ p e. { h e. ( NN0 ^m I ) \| h finSupp 0 } ) -> ( ( { h e. ( NN0 ^m ( I \ { X } ) ) \| h finSupp 0 } X. { ( 0g ` R ) } ) ` ( p \|` ( I \ { X } ) ) ) = ( 0g ` R ) )
95	78 82 94	3eqtr3d	\|- ( ( ph /\ p e. { h e. ( NN0 ^m I ) \| h finSupp 0 } ) -> ( F ` p ) = ( 0g ` R ) )
96	95	mpteq2dva	\|- ( ph -> ( p e. { h e. ( NN0 ^m I ) \| h finSupp 0 } \|-> ( F ` p ) ) = ( p e. { h e. ( NN0 ^m I ) \| h finSupp 0 } \|-> ( 0g ` R ) ) )
97	2 15 72 10 6 74	mpl0	\|- ( ph -> Z = ( { h e. ( NN0 ^m I ) \| h finSupp 0 } X. { ( 0g ` R ) } ) )
98		fconstmpt	\|- ( { h e. ( NN0 ^m I ) \| h finSupp 0 } X. { ( 0g ` R ) } ) = ( p e. { h e. ( NN0 ^m I ) \| h finSupp 0 } \|-> ( 0g ` R ) )
99	97 98	eqtr2di	\|- ( ph -> ( p e. { h e. ( NN0 ^m I ) \| h finSupp 0 } \|-> ( 0g ` R ) ) = Z )
100	17 96 99	3eqtrd	\|- ( ph -> F = Z )

Metamath Proof Explorer

Theorem selvply1rhm0

Proof