Metamath Proof Explorer

Theorem selvply1rhmlem1

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 )
Assertion selvply1rhmlem1 
|- ( ph -> H : B --> ( Base ` 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 fvexd 
 |-  ( ( ph /\ f e. B ) -> ( Base ` U ) e. _V )
10 ovexd 
 |-  ( ( ph /\ f e. B ) -> ( NN0 ^m 1o ) e. _V )
11 eqid 
 |-  ( { X } mPoly U ) = ( { X } mPoly U )
12 eqid 
 |-  ( Base ` U ) = ( Base ` U )
13 eqid 
 |-  ( Base ` ( { X } mPoly U ) ) = ( Base ` ( { X } mPoly U ) )
14 eqid 
 |-  { h e. ( NN0 ^m { X } ) | h finSupp 0 } = { h e. ( NN0 ^m { X } ) | h finSupp 0 }
15 14 psrbasfsupp 
 |-  { h e. ( NN0 ^m { X } ) | h finSupp 0 } = { h e. ( NN0 ^m { X } ) | ( `' h " NN ) e. Fin }
16 8 adantr 
 |-  ( ( ph /\ f e. B ) -> R e. CRing )
17 7 snssd 
 |-  ( ph -> { X } C_ I )
18 17 adantr 
 |-  ( ( ph /\ f e. B ) -> { X } C_ I )
19 simpr 
 |-  ( ( ph /\ f e. B ) -> f e. B )
20 2 1 3 11 13 16 18 19 selvcl 
 |-  ( ( ph /\ f e. B ) -> ( ( ( I selectVars R ) ` { X } ) ` f ) e. ( Base ` ( { X } mPoly U ) ) )
21 11 12 13 15 20 mplelf 
 |-  ( ( ph /\ f e. B ) -> ( ( ( I selectVars R ) ` { X } ) ` f ) : { h e. ( NN0 ^m { X } ) | h finSupp 0 } --> ( Base ` U ) )
22 21 adantr 
 |-  ( ( ( ph /\ f e. B ) /\ n e. ( NN0 ^m 1o ) ) -> ( ( ( I selectVars R ) ` { X } ) ` f ) : { h e. ( NN0 ^m { X } ) | h finSupp 0 } --> ( Base ` U ) )
23 breq1 
 |-  ( h = { <. X , ( n ` (/) ) >. } -> ( h finSupp 0 <-> { <. X , ( n ` (/) ) >. } finSupp 0 ) )
24 nn0ex 
 |-  NN0 e. _V
25 24 a1i 
 |-  ( ( ( ph /\ f e. B ) /\ n e. ( NN0 ^m 1o ) ) -> NN0 e. _V )
26 snex 
 |-  { X } e. _V
27 26 a1i 
 |-  ( ( ( ph /\ f e. B ) /\ n e. ( NN0 ^m 1o ) ) -> { X } e. _V )
28 7 ad2antrr 
 |-  ( ( ( ph /\ f e. B ) /\ n e. ( NN0 ^m 1o ) ) -> X e. I )
29 simpr 
 |-  ( ( ( ph /\ f e. B ) /\ n e. ( NN0 ^m 1o ) ) -> n e. ( NN0 ^m 1o ) )
30 29 elmaprd 
 |-  ( ( ( ph /\ f e. B ) /\ n e. ( NN0 ^m 1o ) ) -> n : 1o --> NN0 )
31 0lt1o 
 |-  (/) e. 1o
32 31 a1i 
 |-  ( ( ( ph /\ f e. B ) /\ n e. ( NN0 ^m 1o ) ) -> (/) e. 1o )
33 30 32 ffvelcdmd 
 |-  ( ( ( ph /\ f e. B ) /\ n e. ( NN0 ^m 1o ) ) -> ( n ` (/) ) e. NN0 )
34 28 33 fsnd 
 |-  ( ( ( ph /\ f e. B ) /\ n e. ( NN0 ^m 1o ) ) -> { <. X , ( n ` (/) ) >. } : { X } --> NN0 )
35 25 27 34 elmapdd 
 |-  ( ( ( ph /\ f e. B ) /\ n e. ( NN0 ^m 1o ) ) -> { <. X , ( n ` (/) ) >. } e. ( NN0 ^m { X } ) )
36 c0ex 
 |-  0 e. _V
37 36 a1i 
 |-  ( ( ( ph /\ f e. B ) /\ n e. ( NN0 ^m 1o ) ) -> 0 e. _V )
38 snopfsupp 
 |-  ( ( X e. I /\ ( n ` (/) ) e. NN0 /\ 0 e. _V ) -> { <. X , ( n ` (/) ) >. } finSupp 0 )
39 28 33 37 38 syl3anc 
 |-  ( ( ( ph /\ f e. B ) /\ n e. ( NN0 ^m 1o ) ) -> { <. X , ( n ` (/) ) >. } finSupp 0 )
40 23 35 39 elrabd 
 |-  ( ( ( ph /\ f e. B ) /\ n e. ( NN0 ^m 1o ) ) -> { <. X , ( n ` (/) ) >. } e. { h e. ( NN0 ^m { X } ) | h finSupp 0 } )
41 22 40 ffvelcdmd 
 |-  ( ( ( ph /\ f e. B ) /\ n e. ( NN0 ^m 1o ) ) -> ( ( ( ( I selectVars R ) ` { X } ) ` f ) ` { <. X , ( n ` (/) ) >. } ) e. ( Base ` U ) )
42 41 fmpttd 
 |-  ( ( ph /\ f e. B ) -> ( n e. ( NN0 ^m 1o ) |-> ( ( ( ( I selectVars R ) ` { X } ) ` f ) ` { <. X , ( n ` (/) ) >. } ) ) : ( NN0 ^m 1o ) --> ( Base ` U ) )
43 9 10 42 elmapdd 
 |-  ( ( ph /\ f e. B ) -> ( n e. ( NN0 ^m 1o ) |-> ( ( ( ( I selectVars R ) ` { X } ) ` f ) ` { <. X , ( n ` (/) ) >. } ) ) e. ( ( Base ` U ) ^m ( NN0 ^m 1o ) ) )
44 eqid 
 |-  ( 1o mPwSer U ) = ( 1o mPwSer U )
45 psr1baslem 
 |-  ( NN0 ^m 1o ) = { h e. ( NN0 ^m 1o ) | ( `' h " NN ) e. Fin }
46 eqid 
 |-  ( Base ` ( 1o mPwSer U ) ) = ( Base ` ( 1o mPwSer U ) )
47 1oex 
 |-  1o e. _V
48 47 a1i 
 |-  ( ( ph /\ f e. B ) -> 1o e. _V )
49 44 12 45 46 48 psrbas 
 |-  ( ( ph /\ f e. B ) -> ( Base ` ( 1o mPwSer U ) ) = ( ( Base ` U ) ^m ( NN0 ^m 1o ) ) )
50 43 49 eleqtrrd 
 |-  ( ( ph /\ f e. B ) -> ( n e. ( NN0 ^m 1o ) |-> ( ( ( ( I selectVars R ) ` { X } ) ` f ) ` { <. X , ( n ` (/) ) >. } ) ) e. ( Base ` ( 1o mPwSer U ) ) )
51 21 40 cofmpt 
 |-  ( ( ph /\ f e. B ) -> ( ( ( ( I selectVars R ) ` { X } ) ` f ) o. ( n e. ( NN0 ^m 1o ) |-> { <. X , ( n ` (/) ) >. } ) ) = ( n e. ( NN0 ^m 1o ) |-> ( ( ( ( I selectVars R ) ` { X } ) ` f ) ` { <. X , ( n ` (/) ) >. } ) ) )
52 eqid 
 |-  ( 0g ` U ) = ( 0g ` U )
53 11 13 52 20 mplelsfi 
 |-  ( ( ph /\ f e. B ) -> ( ( ( I selectVars R ) ` { X } ) ` f ) finSupp ( 0g ` U ) )
54 35 ralrimiva 
 |-  ( ( ph /\ f e. B ) -> A. n e. ( NN0 ^m 1o ) { <. X , ( n ` (/) ) >. } e. ( NN0 ^m { X } ) )
55 28 ad2antrr 
 |-  ( ( ( ( ( ph /\ f e. B ) /\ n e. ( NN0 ^m 1o ) ) /\ m e. ( NN0 ^m 1o ) ) /\ { <. X , ( n ` (/) ) >. } = { <. X , ( m ` (/) ) >. } ) -> X e. I )
56 fvexd 
 |-  ( ( ( ( ( ph /\ f e. B ) /\ n e. ( NN0 ^m 1o ) ) /\ m e. ( NN0 ^m 1o ) ) /\ { <. X , ( n ` (/) ) >. } = { <. X , ( m ` (/) ) >. } ) -> ( n ` (/) ) e. _V )
57 opex 
 |-  <. X , ( n ` (/) ) >. e. _V
58 57 sneqr 
 |-  ( { <. X , ( n ` (/) ) >. } = { <. X , ( m ` (/) ) >. } -> <. X , ( n ` (/) ) >. = <. X , ( m ` (/) ) >. )
59 58 adantl 
 |-  ( ( ( ( ( ph /\ f e. B ) /\ n e. ( NN0 ^m 1o ) ) /\ m e. ( NN0 ^m 1o ) ) /\ { <. X , ( n ` (/) ) >. } = { <. X , ( m ` (/) ) >. } ) -> <. X , ( n ` (/) ) >. = <. X , ( m ` (/) ) >. )
60 opthg 
 |-  ( ( X e. I /\ ( n ` (/) ) e. _V ) -> ( <. X , ( n ` (/) ) >. = <. X , ( m ` (/) ) >. <-> ( X = X /\ ( n ` (/) ) = ( m ` (/) ) ) ) )
61 60 simplbda 
 |-  ( ( ( X e. I /\ ( n ` (/) ) e. _V ) /\ <. X , ( n ` (/) ) >. = <. X , ( m ` (/) ) >. ) -> ( n ` (/) ) = ( m ` (/) ) )
62 55 56 59 61 syl21anc 
 |-  ( ( ( ( ( ph /\ f e. B ) /\ n e. ( NN0 ^m 1o ) ) /\ m e. ( NN0 ^m 1o ) ) /\ { <. X , ( n ` (/) ) >. } = { <. X , ( m ` (/) ) >. } ) -> ( n ` (/) ) = ( m ` (/) ) )
63 0ex 
 |-  (/) e. _V
64 63 a1i 
 |-  ( ( ( ( ( ph /\ f e. B ) /\ n e. ( NN0 ^m 1o ) ) /\ m e. ( NN0 ^m 1o ) ) /\ { <. X , ( n ` (/) ) >. } = { <. X , ( m ` (/) ) >. } ) -> (/) e. _V )
65 df1o2 
 |-  1o = { (/) }
66 30 ad2antrr 
 |-  ( ( ( ( ( ph /\ f e. B ) /\ n e. ( NN0 ^m 1o ) ) /\ m e. ( NN0 ^m 1o ) ) /\ { <. X , ( n ` (/) ) >. } = { <. X , ( m ` (/) ) >. } ) -> n : 1o --> NN0 )
67 66 ffnd 
 |-  ( ( ( ( ( ph /\ f e. B ) /\ n e. ( NN0 ^m 1o ) ) /\ m e. ( NN0 ^m 1o ) ) /\ { <. X , ( n ` (/) ) >. } = { <. X , ( m ` (/) ) >. } ) -> n Fn 1o )
68 simplr 
 |-  ( ( ( ( ( ph /\ f e. B ) /\ n e. ( NN0 ^m 1o ) ) /\ m e. ( NN0 ^m 1o ) ) /\ { <. X , ( n ` (/) ) >. } = { <. X , ( m ` (/) ) >. } ) -> m e. ( NN0 ^m 1o ) )
69 68 elmaprd 
 |-  ( ( ( ( ( ph /\ f e. B ) /\ n e. ( NN0 ^m 1o ) ) /\ m e. ( NN0 ^m 1o ) ) /\ { <. X , ( n ` (/) ) >. } = { <. X , ( m ` (/) ) >. } ) -> m : 1o --> NN0 )
70 69 ffnd 
 |-  ( ( ( ( ( ph /\ f e. B ) /\ n e. ( NN0 ^m 1o ) ) /\ m e. ( NN0 ^m 1o ) ) /\ { <. X , ( n ` (/) ) >. } = { <. X , ( m ` (/) ) >. } ) -> m Fn 1o )
71 64 65 67 70 fsneq 
 |-  ( ( ( ( ( ph /\ f e. B ) /\ n e. ( NN0 ^m 1o ) ) /\ m e. ( NN0 ^m 1o ) ) /\ { <. X , ( n ` (/) ) >. } = { <. X , ( m ` (/) ) >. } ) -> ( n = m <-> ( n ` (/) ) = ( m ` (/) ) ) )
72 62 71 mpbird 
 |-  ( ( ( ( ( ph /\ f e. B ) /\ n e. ( NN0 ^m 1o ) ) /\ m e. ( NN0 ^m 1o ) ) /\ { <. X , ( n ` (/) ) >. } = { <. X , ( m ` (/) ) >. } ) -> n = m )
73 72 ex 
 |-  ( ( ( ( ph /\ f e. B ) /\ n e. ( NN0 ^m 1o ) ) /\ m e. ( NN0 ^m 1o ) ) -> ( { <. X , ( n ` (/) ) >. } = { <. X , ( m ` (/) ) >. } -> n = m ) )
74 73 anasss 
 |-  ( ( ( ph /\ f e. B ) /\ ( n e. ( NN0 ^m 1o ) /\ m e. ( NN0 ^m 1o ) ) ) -> ( { <. X , ( n ` (/) ) >. } = { <. X , ( m ` (/) ) >. } -> n = m ) )
75 74 ralrimivva 
 |-  ( ( ph /\ f e. B ) -> A. n e. ( NN0 ^m 1o ) A. m e. ( NN0 ^m 1o ) ( { <. X , ( n ` (/) ) >. } = { <. X , ( m ` (/) ) >. } -> n = m ) )
76 eqid 
 |-  ( n e. ( NN0 ^m 1o ) |-> { <. X , ( n ` (/) ) >. } ) = ( n e. ( NN0 ^m 1o ) |-> { <. X , ( n ` (/) ) >. } )
77 fveq1 
 |-  ( n = m -> ( n ` (/) ) = ( m ` (/) ) )
78 77 opeq2d 
 |-  ( n = m -> <. X , ( n ` (/) ) >. = <. X , ( m ` (/) ) >. )
79 78 sneqd 
 |-  ( n = m -> { <. X , ( n ` (/) ) >. } = { <. X , ( m ` (/) ) >. } )
80 76 79 f1mpt 
 |-  ( ( n e. ( NN0 ^m 1o ) |-> { <. X , ( n ` (/) ) >. } ) : ( NN0 ^m 1o ) -1-1-> ( NN0 ^m { X } ) <-> ( A. n e. ( NN0 ^m 1o ) { <. X , ( n ` (/) ) >. } e. ( NN0 ^m { X } ) /\ A. n e. ( NN0 ^m 1o ) A. m e. ( NN0 ^m 1o ) ( { <. X , ( n ` (/) ) >. } = { <. X , ( m ` (/) ) >. } -> n = m ) ) )
81 54 75 80 sylanbrc 
 |-  ( ( ph /\ f e. B ) -> ( n e. ( NN0 ^m 1o ) |-> { <. X , ( n ` (/) ) >. } ) : ( NN0 ^m 1o ) -1-1-> ( NN0 ^m { X } ) )
82 fvexd 
 |-  ( ( ph /\ f e. B ) -> ( 0g ` U ) e. _V )
83 53 81 82 20 fsuppco 
 |-  ( ( ph /\ f e. B ) -> ( ( ( ( I selectVars R ) ` { X } ) ` f ) o. ( n e. ( NN0 ^m 1o ) |-> { <. X , ( n ` (/) ) >. } ) ) finSupp ( 0g ` U ) )
84 51 83 eqbrtrrd 
 |-  ( ( ph /\ f e. B ) -> ( n e. ( NN0 ^m 1o ) |-> ( ( ( ( I selectVars R ) ` { X } ) ` f ) ` { <. X , ( n ` (/) ) >. } ) ) finSupp ( 0g ` U ) )
85 eqid 
 |-  ( 1o mPoly U ) = ( 1o mPoly U )
86 eqid 
 |-  ( Base ` Q ) = ( Base ` Q )
87 4 86 ply1bas 
 |-  ( Base ` Q ) = ( Base ` ( 1o mPoly U ) )
88 85 44 46 52 87 mplelbas 
 |-  ( ( n e. ( NN0 ^m 1o ) |-> ( ( ( ( I selectVars R ) ` { X } ) ` f ) ` { <. X , ( n ` (/) ) >. } ) ) e. ( Base ` Q ) <-> ( ( n e. ( NN0 ^m 1o ) |-> ( ( ( ( I selectVars R ) ` { X } ) ` f ) ` { <. X , ( n ` (/) ) >. } ) ) e. ( Base ` ( 1o mPwSer U ) ) /\ ( n e. ( NN0 ^m 1o ) |-> ( ( ( ( I selectVars R ) ` { X } ) ` f ) ` { <. X , ( n ` (/) ) >. } ) ) finSupp ( 0g ` U ) ) )
89 50 84 88 sylanbrc 
 |-  ( ( ph /\ f e. B ) -> ( n e. ( NN0 ^m 1o ) |-> ( ( ( ( I selectVars R ) ` { X } ) ` f ) ` { <. X , ( n ` (/) ) >. } ) ) e. ( Base ` Q ) )
90 89 5 fmptd 
 |-  ( ph -> H : B --> ( Base ` Q ) )