Metamath Proof Explorer

Theorem selvply1rhmlem2

Description: Lemma for selvply1rhm : Image of the ring unit by the mapping H (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 )
Assertion selvply1rhmlem2 
|- ( ph -> ( H ` ( 1r ` P ) ) = ( 1r ` Q ) )

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 fveq2 
 |-  ( f = ( 1r ` P ) -> ( ( ( I selectVars R ) ` { X } ) ` f ) = ( ( ( I selectVars R ) ` { X } ) ` ( 1r ` P ) ) )
10 9 fveq1d 
 |-  ( f = ( 1r ` P ) -> ( ( ( ( I selectVars R ) ` { X } ) ` f ) ` { <. X , ( n ` (/) ) >. } ) = ( ( ( ( I selectVars R ) ` { X } ) ` ( 1r ` P ) ) ` { <. X , ( n ` (/) ) >. } ) )
11 10 mpteq2dv 
 |-  ( f = ( 1r ` P ) -> ( n e. ( NN0 ^m 1o ) |-> ( ( ( ( I selectVars R ) ` { X } ) ` f ) ` { <. X , ( n ` (/) ) >. } ) ) = ( n e. ( NN0 ^m 1o ) |-> ( ( ( ( I selectVars R ) ` { X } ) ` ( 1r ` P ) ) ` { <. X , ( n ` (/) ) >. } ) ) )
12 eqid 
 |-  ( algSc ` P ) = ( algSc ` P )
13 eqid 
 |-  ( 1r ` R ) = ( 1r ` R )
14 eqid 
 |-  ( 1r ` P ) = ( 1r ` P )
15 8 crngringd 
 |-  ( ph -> R e. Ring )
16 2 12 13 14 6 15 mplascl1 
 |-  ( ph -> ( ( algSc ` P ) ` ( 1r ` R ) ) = ( 1r ` P ) )
17 16 fveq2d 
 |-  ( ph -> ( ( ( I selectVars R ) ` { X } ) ` ( ( algSc ` P ) ` ( 1r ` R ) ) ) = ( ( ( I selectVars R ) ` { X } ) ` ( 1r ` P ) ) )
18 eqid 
 |-  ( Base ` R ) = ( Base ` R )
19 eqid 
 |-  ( algSc ` ( { X } mPoly U ) ) = ( algSc ` ( { X } mPoly U ) )
20 18 13 15 ringidcld 
 |-  ( ph -> ( 1r ` R ) e. ( Base ` R ) )
21 eqid 
 |-  ( { X } mPoly U ) = ( { X } mPoly U )
22 eqid 
 |-  ( ( algSc ` ( { X } mPoly U ) ) o. ( algSc ` U ) ) = ( ( algSc ` ( { X } mPoly U ) ) o. ( algSc ` U ) )
23 7 snssd 
 |-  ( ph -> { X } C_ I )
24 18 2 12 19 6 20 3 21 22 8 23 selvascl 
 |-  ( ph -> ( ( ( I selectVars R ) ` { X } ) ` ( ( algSc ` P ) ` ( 1r ` R ) ) ) = ( ( ( algSc ` ( { X } mPoly U ) ) o. ( algSc ` U ) ) ` ( 1r ` R ) ) )
25 17 24 eqtr3d 
 |-  ( ph -> ( ( ( I selectVars R ) ` { X } ) ` ( 1r ` P ) ) = ( ( ( algSc ` ( { X } mPoly U ) ) o. ( algSc ` U ) ) ` ( 1r ` R ) ) )
26 25 fveq1d 
 |-  ( ph -> ( ( ( ( I selectVars R ) ` { X } ) ` ( 1r ` P ) ) ` { <. X , ( n ` (/) ) >. } ) = ( ( ( ( algSc ` ( { X } mPoly U ) ) o. ( algSc ` U ) ) ` ( 1r ` R ) ) ` { <. X , ( n ` (/) ) >. } ) )
27 26 adantr 
 |-  ( ( ph /\ n e. ( NN0 ^m 1o ) ) -> ( ( ( ( I selectVars R ) ` { X } ) ` ( 1r ` P ) ) ` { <. X , ( n ` (/) ) >. } ) = ( ( ( ( algSc ` ( { X } mPoly U ) ) o. ( algSc ` U ) ) ` ( 1r ` R ) ) ` { <. X , ( n ` (/) ) >. } ) )
28 eqid 
 |-  ( Base ` U ) = ( Base ` U )
29 eqid 
 |-  ( algSc ` U ) = ( algSc ` U )
30 6 difexd 
 |-  ( ph -> ( I \ { X } ) e. _V )
31 3 28 18 29 30 15 mplasclf 
 |-  ( ph -> ( algSc ` U ) : ( Base ` R ) --> ( Base ` U ) )
32 31 20 fvco3d 
 |-  ( ph -> ( ( ( algSc ` ( { X } mPoly U ) ) o. ( algSc ` U ) ) ` ( 1r ` R ) ) = ( ( algSc ` ( { X } mPoly U ) ) ` ( ( algSc ` U ) ` ( 1r ` R ) ) ) )
33 eqid 
 |-  { h e. ( NN0 ^m { X } ) | ( `' h " NN ) e. Fin } = { h e. ( NN0 ^m { X } ) | ( `' h " NN ) e. Fin }
34 eqid 
 |-  ( 0g ` U ) = ( 0g ` U )
35 snex 
 |-  { X } e. _V
36 35 a1i 
 |-  ( ph -> { X } e. _V )
37 3 30 15 mplringd 
 |-  ( ph -> U e. Ring )
38 31 20 ffvelcdmd 
 |-  ( ph -> ( ( algSc ` U ) ` ( 1r ` R ) ) e. ( Base ` U ) )
39 21 33 34 28 19 36 37 38 mplascl 
 |-  ( ph -> ( ( algSc ` ( { X } mPoly U ) ) ` ( ( algSc ` U ) ` ( 1r ` R ) ) ) = ( p e. { h e. ( NN0 ^m { X } ) | ( `' h " NN ) e. Fin } |-> if ( p = ( { X } X. { 0 } ) , ( ( algSc ` U ) ` ( 1r ` R ) ) , ( 0g ` U ) ) ) )
40 32 39 eqtrd 
 |-  ( ph -> ( ( ( algSc ` ( { X } mPoly U ) ) o. ( algSc ` U ) ) ` ( 1r ` R ) ) = ( p e. { h e. ( NN0 ^m { X } ) | ( `' h " NN ) e. Fin } |-> if ( p = ( { X } X. { 0 } ) , ( ( algSc ` U ) ` ( 1r ` R ) ) , ( 0g ` U ) ) ) )
41 40 adantr 
 |-  ( ( ph /\ n e. ( NN0 ^m 1o ) ) -> ( ( ( algSc ` ( { X } mPoly U ) ) o. ( algSc ` U ) ) ` ( 1r ` R ) ) = ( p e. { h e. ( NN0 ^m { X } ) | ( `' h " NN ) e. Fin } |-> if ( p = ( { X } X. { 0 } ) , ( ( algSc ` U ) ` ( 1r ` R ) ) , ( 0g ` U ) ) ) )
42 eqeq1 
 |-  ( p = { <. X , ( n ` (/) ) >. } -> ( p = ( { X } X. { 0 } ) <-> { <. X , ( n ` (/) ) >. } = ( { X } X. { 0 } ) ) )
43 42 adantl 
 |-  ( ( ( ph /\ n e. ( NN0 ^m 1o ) ) /\ p = { <. X , ( n ` (/) ) >. } ) -> ( p = ( { X } X. { 0 } ) <-> { <. X , ( n ` (/) ) >. } = ( { X } X. { 0 } ) ) )
44 c0ex 
 |-  0 e. _V
45 44 a1i 
 |-  ( ph -> 0 e. _V )
46 xpsng 
 |-  ( ( X e. I /\ 0 e. _V ) -> ( { X } X. { 0 } ) = { <. X , 0 >. } )
47 7 45 46 syl2anc 
 |-  ( ph -> ( { X } X. { 0 } ) = { <. X , 0 >. } )
48 47 eqeq2d 
 |-  ( ph -> ( { <. X , ( n ` (/) ) >. } = ( { X } X. { 0 } ) <-> { <. X , ( n ` (/) ) >. } = { <. X , 0 >. } ) )
49 48 ad2antrr 
 |-  ( ( ( ph /\ n e. ( NN0 ^m 1o ) ) /\ p = { <. X , ( n ` (/) ) >. } ) -> ( { <. X , ( n ` (/) ) >. } = ( { X } X. { 0 } ) <-> { <. X , ( n ` (/) ) >. } = { <. X , 0 >. } ) )
50 opex 
 |-  <. X , ( n ` (/) ) >. e. _V
51 sneqbg 
 |-  ( <. X , ( n ` (/) ) >. e. _V -> ( { <. X , ( n ` (/) ) >. } = { <. X , 0 >. } <-> <. X , ( n ` (/) ) >. = <. X , 0 >. ) )
52 50 51 mp1i 
 |-  ( ( ph /\ n e. ( NN0 ^m 1o ) ) -> ( { <. X , ( n ` (/) ) >. } = { <. X , 0 >. } <-> <. X , ( n ` (/) ) >. = <. X , 0 >. ) )
53 eqidd 
 |-  ( ph -> X = X )
54 fvexd 
 |-  ( ph -> ( n ` (/) ) e. _V )
55 opthg 
 |-  ( ( X e. I /\ ( n ` (/) ) e. _V ) -> ( <. X , ( n ` (/) ) >. = <. X , 0 >. <-> ( X = X /\ ( n ` (/) ) = 0 ) ) )
56 7 54 55 syl2anc 
 |-  ( ph -> ( <. X , ( n ` (/) ) >. = <. X , 0 >. <-> ( X = X /\ ( n ` (/) ) = 0 ) ) )
57 53 56 mpbirand 
 |-  ( ph -> ( <. X , ( n ` (/) ) >. = <. X , 0 >. <-> ( n ` (/) ) = 0 ) )
58 57 adantr 
 |-  ( ( ph /\ n e. ( NN0 ^m 1o ) ) -> ( <. X , ( n ` (/) ) >. = <. X , 0 >. <-> ( n ` (/) ) = 0 ) )
59 1oex 
 |-  1o e. _V
60 59 a1i 
 |-  ( ( ph /\ n e. ( NN0 ^m 1o ) ) -> 1o e. _V )
61 nn0ex 
 |-  NN0 e. _V
62 61 a1i 
 |-  ( ( ph /\ n e. ( NN0 ^m 1o ) ) -> NN0 e. _V )
63 simpr 
 |-  ( ( ph /\ n e. ( NN0 ^m 1o ) ) -> n e. ( NN0 ^m 1o ) )
64 60 62 63 elmaprd 
 |-  ( ( ph /\ n e. ( NN0 ^m 1o ) ) -> n : 1o --> NN0 )
65 64 adantr 
 |-  ( ( ( ph /\ n e. ( NN0 ^m 1o ) ) /\ ( n ` (/) ) = 0 ) -> n : 1o --> NN0 )
66 65 feqmptd 
 |-  ( ( ( ph /\ n e. ( NN0 ^m 1o ) ) /\ ( n ` (/) ) = 0 ) -> n = ( u e. 1o |-> ( n ` u ) ) )
67 el1o 
 |-  ( u e. 1o <-> u = (/) )
68 67 biimpi 
 |-  ( u e. 1o -> u = (/) )
69 68 adantl 
 |-  ( ( ( ( ph /\ n e. ( NN0 ^m 1o ) ) /\ ( n ` (/) ) = 0 ) /\ u e. 1o ) -> u = (/) )
70 69 fveq2d 
 |-  ( ( ( ( ph /\ n e. ( NN0 ^m 1o ) ) /\ ( n ` (/) ) = 0 ) /\ u e. 1o ) -> ( n ` u ) = ( n ` (/) ) )
71 simplr 
 |-  ( ( ( ( ph /\ n e. ( NN0 ^m 1o ) ) /\ ( n ` (/) ) = 0 ) /\ u e. 1o ) -> ( n ` (/) ) = 0 )
72 70 71 eqtrd 
 |-  ( ( ( ( ph /\ n e. ( NN0 ^m 1o ) ) /\ ( n ` (/) ) = 0 ) /\ u e. 1o ) -> ( n ` u ) = 0 )
73 72 mpteq2dva 
 |-  ( ( ( ph /\ n e. ( NN0 ^m 1o ) ) /\ ( n ` (/) ) = 0 ) -> ( u e. 1o |-> ( n ` u ) ) = ( u e. 1o |-> 0 ) )
74 66 73 eqtrd 
 |-  ( ( ( ph /\ n e. ( NN0 ^m 1o ) ) /\ ( n ` (/) ) = 0 ) -> n = ( u e. 1o |-> 0 ) )
75 fconstmpt 
 |-  ( 1o X. { 0 } ) = ( u e. 1o |-> 0 )
76 75 eqeq2i 
 |-  ( n = ( 1o X. { 0 } ) <-> n = ( u e. 1o |-> 0 ) )
77 74 76 sylibr 
 |-  ( ( ( ph /\ n e. ( NN0 ^m 1o ) ) /\ ( n ` (/) ) = 0 ) -> n = ( 1o X. { 0 } ) )
78 76 biimpi 
 |-  ( n = ( 1o X. { 0 } ) -> n = ( u e. 1o |-> 0 ) )
79 78 adantl 
 |-  ( ( ( ph /\ n e. ( NN0 ^m 1o ) ) /\ n = ( 1o X. { 0 } ) ) -> n = ( u e. 1o |-> 0 ) )
80 eqidd 
 |-  ( ( ( ( ph /\ n e. ( NN0 ^m 1o ) ) /\ n = ( 1o X. { 0 } ) ) /\ u = (/) ) -> 0 = 0 )
81 0lt1o 
 |-  (/) e. 1o
82 81 a1i 
 |-  ( ( ( ph /\ n e. ( NN0 ^m 1o ) ) /\ n = ( 1o X. { 0 } ) ) -> (/) e. 1o )
83 44 a1i 
 |-  ( ( ( ph /\ n e. ( NN0 ^m 1o ) ) /\ n = ( 1o X. { 0 } ) ) -> 0 e. _V )
84 79 80 82 83 fvmptd 
 |-  ( ( ( ph /\ n e. ( NN0 ^m 1o ) ) /\ n = ( 1o X. { 0 } ) ) -> ( n ` (/) ) = 0 )
85 77 84 impbida 
 |-  ( ( ph /\ n e. ( NN0 ^m 1o ) ) -> ( ( n ` (/) ) = 0 <-> n = ( 1o X. { 0 } ) ) )
86 52 58 85 3bitrd 
 |-  ( ( ph /\ n e. ( NN0 ^m 1o ) ) -> ( { <. X , ( n ` (/) ) >. } = { <. X , 0 >. } <-> n = ( 1o X. { 0 } ) ) )
87 86 adantr 
 |-  ( ( ( ph /\ n e. ( NN0 ^m 1o ) ) /\ p = { <. X , ( n ` (/) ) >. } ) -> ( { <. X , ( n ` (/) ) >. } = { <. X , 0 >. } <-> n = ( 1o X. { 0 } ) ) )
88 43 49 87 3bitrd 
 |-  ( ( ( ph /\ n e. ( NN0 ^m 1o ) ) /\ p = { <. X , ( n ` (/) ) >. } ) -> ( p = ( { X } X. { 0 } ) <-> n = ( 1o X. { 0 } ) ) )
89 eqid 
 |-  ( 1r ` U ) = ( 1r ` U )
90 3 29 13 89 30 15 mplascl1 
 |-  ( ph -> ( ( algSc ` U ) ` ( 1r ` R ) ) = ( 1r ` U ) )
91 90 ad2antrr 
 |-  ( ( ( ph /\ n e. ( NN0 ^m 1o ) ) /\ p = { <. X , ( n ` (/) ) >. } ) -> ( ( algSc ` U ) ` ( 1r ` R ) ) = ( 1r ` U ) )
92 88 91 ifbieq1d 
 |-  ( ( ( ph /\ n e. ( NN0 ^m 1o ) ) /\ p = { <. X , ( n ` (/) ) >. } ) -> if ( p = ( { X } X. { 0 } ) , ( ( algSc ` U ) ` ( 1r ` R ) ) , ( 0g ` U ) ) = if ( n = ( 1o X. { 0 } ) , ( 1r ` U ) , ( 0g ` U ) ) )
93 breq1 
 |-  ( h = { <. X , ( n ` (/) ) >. } -> ( h finSupp 0 <-> { <. X , ( n ` (/) ) >. } finSupp 0 ) )
94 35 a1i 
 |-  ( ( ph /\ n e. ( NN0 ^m 1o ) ) -> { X } e. _V )
95 7 adantr 
 |-  ( ( ph /\ n e. ( NN0 ^m 1o ) ) -> X e. I )
96 81 a1i 
 |-  ( ( ph /\ n e. ( NN0 ^m 1o ) ) -> (/) e. 1o )
97 64 96 ffvelcdmd 
 |-  ( ( ph /\ n e. ( NN0 ^m 1o ) ) -> ( n ` (/) ) e. NN0 )
98 95 97 fsnd 
 |-  ( ( ph /\ n e. ( NN0 ^m 1o ) ) -> { <. X , ( n ` (/) ) >. } : { X } --> NN0 )
99 62 94 98 elmapdd 
 |-  ( ( ph /\ n e. ( NN0 ^m 1o ) ) -> { <. X , ( n ` (/) ) >. } e. ( NN0 ^m { X } ) )
100 snopfsupp 
 |-  ( ( X e. I /\ ( n ` (/) ) e. _V /\ 0 e. _V ) -> { <. X , ( n ` (/) ) >. } finSupp 0 )
101 7 54 45 100 syl3anc 
 |-  ( ph -> { <. X , ( n ` (/) ) >. } finSupp 0 )
102 101 adantr 
 |-  ( ( ph /\ n e. ( NN0 ^m 1o ) ) -> { <. X , ( n ` (/) ) >. } finSupp 0 )
103 93 99 102 elrabd 
 |-  ( ( ph /\ n e. ( NN0 ^m 1o ) ) -> { <. X , ( n ` (/) ) >. } e. { h e. ( NN0 ^m { X } ) | h finSupp 0 } )
104 eqid 
 |-  { h e. ( NN0 ^m { X } ) | h finSupp 0 } = { h e. ( NN0 ^m { X } ) | h finSupp 0 }
105 104 psrbasfsupp 
 |-  { h e. ( NN0 ^m { X } ) | h finSupp 0 } = { h e. ( NN0 ^m { X } ) | ( `' h " NN ) e. Fin }
106 103 105 eleqtrdi 
 |-  ( ( ph /\ n e. ( NN0 ^m 1o ) ) -> { <. X , ( n ` (/) ) >. } e. { h e. ( NN0 ^m { X } ) | ( `' h " NN ) e. Fin } )
107 28 89 37 ringidcld 
 |-  ( ph -> ( 1r ` U ) e. ( Base ` U ) )
108 37 ringgrpd 
 |-  ( ph -> U e. Grp )
109 28 34 108 grpidcld 
 |-  ( ph -> ( 0g ` U ) e. ( Base ` U ) )
110 107 109 ifcld 
 |-  ( ph -> if ( n = ( 1o X. { 0 } ) , ( 1r ` U ) , ( 0g ` U ) ) e. ( Base ` U ) )
111 110 adantr 
 |-  ( ( ph /\ n e. ( NN0 ^m 1o ) ) -> if ( n = ( 1o X. { 0 } ) , ( 1r ` U ) , ( 0g ` U ) ) e. ( Base ` U ) )
112 41 92 106 111 fvmptd 
 |-  ( ( ph /\ n e. ( NN0 ^m 1o ) ) -> ( ( ( ( algSc ` ( { X } mPoly U ) ) o. ( algSc ` U ) ) ` ( 1r ` R ) ) ` { <. X , ( n ` (/) ) >. } ) = if ( n = ( 1o X. { 0 } ) , ( 1r ` U ) , ( 0g ` U ) ) )
113 27 112 eqtrd 
 |-  ( ( ph /\ n e. ( NN0 ^m 1o ) ) -> ( ( ( ( I selectVars R ) ` { X } ) ` ( 1r ` P ) ) ` { <. X , ( n ` (/) ) >. } ) = if ( n = ( 1o X. { 0 } ) , ( 1r ` U ) , ( 0g ` U ) ) )
114 113 mpteq2dva 
 |-  ( ph -> ( n e. ( NN0 ^m 1o ) |-> ( ( ( ( I selectVars R ) ` { X } ) ` ( 1r ` P ) ) ` { <. X , ( n ` (/) ) >. } ) ) = ( n e. ( NN0 ^m 1o ) |-> if ( n = ( 1o X. { 0 } ) , ( 1r ` U ) , ( 0g ` U ) ) ) )
115 eqid 
 |-  ( 1o mPoly U ) = ( 1o mPoly U )
116 psr1baslem 
 |-  ( NN0 ^m 1o ) = { h e. ( NN0 ^m 1o ) | ( `' h " NN ) e. Fin }
117 eqid 
 |-  ( algSc ` Q ) = ( algSc ` Q )
118 4 117 ply1ascl 
 |-  ( algSc ` Q ) = ( algSc ` ( 1o mPoly U ) )
119 59 a1i 
 |-  ( ph -> 1o e. _V )
120 115 116 34 28 118 119 37 107 mplascl 
 |-  ( ph -> ( ( algSc ` Q ) ` ( 1r ` U ) ) = ( n e. ( NN0 ^m 1o ) |-> if ( n = ( 1o X. { 0 } ) , ( 1r ` U ) , ( 0g ` U ) ) ) )
121 eqid 
 |-  ( 1r ` Q ) = ( 1r ` Q )
122 4 117 89 121 37 ply1ascl1 
 |-  ( ph -> ( ( algSc ` Q ) ` ( 1r ` U ) ) = ( 1r ` Q ) )
123 114 120 122 3eqtr2d 
 |-  ( ph -> ( n e. ( NN0 ^m 1o ) |-> ( ( ( ( I selectVars R ) ` { X } ) ` ( 1r ` P ) ) ` { <. X , ( n ` (/) ) >. } ) ) = ( 1r ` Q ) )
124 11 123 sylan9eqr 
 |-  ( ( ph /\ f = ( 1r ` P ) ) -> ( n e. ( NN0 ^m 1o ) |-> ( ( ( ( I selectVars R ) ` { X } ) ` f ) ` { <. X , ( n ` (/) ) >. } ) ) = ( 1r ` Q ) )
125 2 6 15 mplringd 
 |-  ( ph -> P e. Ring )
126 1 14 125 ringidcld 
 |-  ( ph -> ( 1r ` P ) e. B )
127 fvexd 
 |-  ( ph -> ( 1r ` Q ) e. _V )
128 5 124 126 127 fvmptd2 
 |-  ( ph -> ( H ` ( 1r ` P ) ) = ( 1r ` Q ) )