Metamath Proof Explorer

Theorem 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 )