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