Metamath Proof Explorer

Theorem selvply1rhmlema

Description: Lemma for selvply1rhm . (Contributed by Thierry Arnoux, 4-May-2026)

Ref Expression
Hypotheses selvply1rhmlema.1 
|- B = ( Base ` P )
selvply1rhmlema.2 
|- P = ( { X } mPoly R )
selvply1rhmlema.3 
|- .x. = ( .r ` P )
selvply1rhmlema.4 
|- .X. = ( .r ` Q )
selvply1rhmlema.5 
|- Q = ( Poly1 ` R )
selvply1rhmlema.6 
|- M = ( f e. B |-> ( n e. ( NN0 ^m 1o ) |-> ( f ` { <. X , ( n ` (/) ) >. } ) ) )
selvply1rhmlema.7 
|- ( ph -> X e. V )
selvply1rhmlema.8 
|- ( ph -> R e. Ring )
selvply1rhmlema.9 
|- ( ph -> F e. B )
Assertion selvply1rhmlema 
|- ( ph -> ( M ` F ) e. ( Base ` Q ) )

Proof

Step Hyp Ref Expression
1 selvply1rhmlema.1 
 |-  B = ( Base ` P )
2 selvply1rhmlema.2 
 |-  P = ( { X } mPoly R )
3 selvply1rhmlema.3 
 |-  .x. = ( .r ` P )
4 selvply1rhmlema.4 
 |-  .X. = ( .r ` Q )
5 selvply1rhmlema.5 
 |-  Q = ( Poly1 ` R )
6 selvply1rhmlema.6 
 |-  M = ( f e. B |-> ( n e. ( NN0 ^m 1o ) |-> ( f ` { <. X , ( n ` (/) ) >. } ) ) )
7 selvply1rhmlema.7 
 |-  ( ph -> X e. V )
8 selvply1rhmlema.8 
 |-  ( ph -> R e. Ring )
9 selvply1rhmlema.9 
 |-  ( ph -> F e. B )
10 fvexd 
 |-  ( ph -> ( Base ` R ) e. _V )
11 ovexd 
 |-  ( ph -> ( NN0 ^m 1o ) e. _V )
12 fvexd 
 |-  ( ( ph /\ n e. ( NN0 ^m 1o ) ) -> ( F ` { <. X , ( n ` (/) ) >. } ) e. _V )
13 fveq1 
 |-  ( f = F -> ( f ` { <. X , ( n ` (/) ) >. } ) = ( F ` { <. X , ( n ` (/) ) >. } ) )
14 13 mpteq2dv 
 |-  ( f = F -> ( n e. ( NN0 ^m 1o ) |-> ( f ` { <. X , ( n ` (/) ) >. } ) ) = ( n e. ( NN0 ^m 1o ) |-> ( F ` { <. X , ( n ` (/) ) >. } ) ) )
15 11 mptexd 
 |-  ( ph -> ( n e. ( NN0 ^m 1o ) |-> ( F ` { <. X , ( n ` (/) ) >. } ) ) e. _V )
16 6 14 9 15 fvmptd3 
 |-  ( ph -> ( M ` F ) = ( n e. ( NN0 ^m 1o ) |-> ( F ` { <. X , ( n ` (/) ) >. } ) ) )
17 fveq1 
 |-  ( n = m -> ( n ` (/) ) = ( m ` (/) ) )
18 17 opeq2d 
 |-  ( n = m -> <. X , ( n ` (/) ) >. = <. X , ( m ` (/) ) >. )
19 18 sneqd 
 |-  ( n = m -> { <. X , ( n ` (/) ) >. } = { <. X , ( m ` (/) ) >. } )
20 19 fveq2d 
 |-  ( n = m -> ( F ` { <. X , ( n ` (/) ) >. } ) = ( F ` { <. X , ( m ` (/) ) >. } ) )
21 16 adantr 
 |-  ( ( ph /\ m e. ( NN0 ^m 1o ) ) -> ( M ` F ) = ( n e. ( NN0 ^m 1o ) |-> ( F ` { <. X , ( n ` (/) ) >. } ) ) )
22 simpr 
 |-  ( ( ph /\ m e. ( NN0 ^m 1o ) ) -> m e. ( NN0 ^m 1o ) )
23 eqid 
 |-  ( Base ` R ) = ( Base ` R )
24 eqid 
 |-  { h e. ( NN0 ^m { X } ) | h finSupp 0 } = { h e. ( NN0 ^m { X } ) | h finSupp 0 }
25 24 psrbasfsupp 
 |-  { h e. ( NN0 ^m { X } ) | h finSupp 0 } = { h e. ( NN0 ^m { X } ) | ( `' h " NN ) e. Fin }
26 9 adantr 
 |-  ( ( ph /\ m e. ( NN0 ^m 1o ) ) -> F e. B )
27 2 23 1 25 26 mplelf 
 |-  ( ( ph /\ m e. ( NN0 ^m 1o ) ) -> F : { h e. ( NN0 ^m { X } ) | h finSupp 0 } --> ( Base ` R ) )
28 breq1 
 |-  ( h = { <. X , ( m ` (/) ) >. } -> ( h finSupp 0 <-> { <. X , ( m ` (/) ) >. } finSupp 0 ) )
29 nn0ex 
 |-  NN0 e. _V
30 29 a1i 
 |-  ( ( ph /\ m e. ( NN0 ^m 1o ) ) -> NN0 e. _V )
31 snex 
 |-  { X } e. _V
32 31 a1i 
 |-  ( ( ph /\ m e. ( NN0 ^m 1o ) ) -> { X } e. _V )
33 7 adantr 
 |-  ( ( ph /\ m e. ( NN0 ^m 1o ) ) -> X e. V )
34 1oex 
 |-  1o e. _V
35 34 a1i 
 |-  ( ( ph /\ m e. ( NN0 ^m 1o ) ) -> 1o e. _V )
36 35 30 22 elmaprd 
 |-  ( ( ph /\ m e. ( NN0 ^m 1o ) ) -> m : 1o --> NN0 )
37 0lt1o 
 |-  (/) e. 1o
38 37 a1i 
 |-  ( ( ph /\ m e. ( NN0 ^m 1o ) ) -> (/) e. 1o )
39 36 38 ffvelcdmd 
 |-  ( ( ph /\ m e. ( NN0 ^m 1o ) ) -> ( m ` (/) ) e. NN0 )
40 33 39 fsnd 
 |-  ( ( ph /\ m e. ( NN0 ^m 1o ) ) -> { <. X , ( m ` (/) ) >. } : { X } --> NN0 )
41 30 32 40 elmapdd 
 |-  ( ( ph /\ m e. ( NN0 ^m 1o ) ) -> { <. X , ( m ` (/) ) >. } e. ( NN0 ^m { X } ) )
42 snfi 
 |-  { X } e. Fin
43 42 a1i 
 |-  ( ( ph /\ m e. ( NN0 ^m 1o ) ) -> { X } e. Fin )
44 c0ex 
 |-  0 e. _V
45 44 a1i 
 |-  ( ( ph /\ m e. ( NN0 ^m 1o ) ) -> 0 e. _V )
46 40 43 45 fdmfifsupp 
 |-  ( ( ph /\ m e. ( NN0 ^m 1o ) ) -> { <. X , ( m ` (/) ) >. } finSupp 0 )
47 28 41 46 elrabd 
 |-  ( ( ph /\ m e. ( NN0 ^m 1o ) ) -> { <. X , ( m ` (/) ) >. } e. { h e. ( NN0 ^m { X } ) | h finSupp 0 } )
48 27 47 ffvelcdmd 
 |-  ( ( ph /\ m e. ( NN0 ^m 1o ) ) -> ( F ` { <. X , ( m ` (/) ) >. } ) e. ( Base ` R ) )
49 20 21 22 48 fvmptd4 
 |-  ( ( ph /\ m e. ( NN0 ^m 1o ) ) -> ( ( M ` F ) ` m ) = ( F ` { <. X , ( m ` (/) ) >. } ) )
50 49 48 eqeltrd 
 |-  ( ( ph /\ m e. ( NN0 ^m 1o ) ) -> ( ( M ` F ) ` m ) e. ( Base ` R ) )
51 12 16 50 fmpt2d 
 |-  ( ph -> ( M ` F ) : ( NN0 ^m 1o ) --> ( Base ` R ) )
52 10 11 51 elmapdd 
 |-  ( ph -> ( M ` F ) e. ( ( Base ` R ) ^m ( NN0 ^m 1o ) ) )
53 eqid 
 |-  ( 1o mPwSer R ) = ( 1o mPwSer R )
54 psr1baslem 
 |-  ( NN0 ^m 1o ) = { h e. ( NN0 ^m 1o ) | ( `' h " NN ) e. Fin }
55 eqid 
 |-  ( Base ` ( 1o mPwSer R ) ) = ( Base ` ( 1o mPwSer R ) )
56 34 a1i 
 |-  ( ph -> 1o e. _V )
57 53 23 54 55 56 psrbas 
 |-  ( ph -> ( Base ` ( 1o mPwSer R ) ) = ( ( Base ` R ) ^m ( NN0 ^m 1o ) ) )
58 52 57 eleqtrrd 
 |-  ( ph -> ( M ` F ) e. ( Base ` ( 1o mPwSer R ) ) )
59 2 23 1 25 9 mplelf 
 |-  ( ph -> F : { h e. ( NN0 ^m { X } ) | h finSupp 0 } --> ( Base ` R ) )
60 breq1 
 |-  ( h = { <. X , ( n ` (/) ) >. } -> ( h finSupp 0 <-> { <. X , ( n ` (/) ) >. } finSupp 0 ) )
61 29 a1i 
 |-  ( ( ph /\ n e. ( NN0 ^m 1o ) ) -> NN0 e. _V )
62 31 a1i 
 |-  ( ( ph /\ n e. ( NN0 ^m 1o ) ) -> { X } e. _V )
63 7 adantr 
 |-  ( ( ph /\ n e. ( NN0 ^m 1o ) ) -> X e. V )
64 34 a1i 
 |-  ( ( ph /\ n e. ( NN0 ^m 1o ) ) -> 1o e. _V )
65 simpr 
 |-  ( ( ph /\ n e. ( NN0 ^m 1o ) ) -> n e. ( NN0 ^m 1o ) )
66 64 61 65 elmaprd 
 |-  ( ( ph /\ n e. ( NN0 ^m 1o ) ) -> n : 1o --> NN0 )
67 37 a1i 
 |-  ( ( ph /\ n e. ( NN0 ^m 1o ) ) -> (/) e. 1o )
68 66 67 ffvelcdmd 
 |-  ( ( ph /\ n e. ( NN0 ^m 1o ) ) -> ( n ` (/) ) e. NN0 )
69 63 68 fsnd 
 |-  ( ( ph /\ n e. ( NN0 ^m 1o ) ) -> { <. X , ( n ` (/) ) >. } : { X } --> NN0 )
70 61 62 69 elmapdd 
 |-  ( ( ph /\ n e. ( NN0 ^m 1o ) ) -> { <. X , ( n ` (/) ) >. } e. ( NN0 ^m { X } ) )
71 42 a1i 
 |-  ( ( ph /\ n e. ( NN0 ^m 1o ) ) -> { X } e. Fin )
72 44 a1i 
 |-  ( ( ph /\ n e. ( NN0 ^m 1o ) ) -> 0 e. _V )
73 69 71 72 fdmfifsupp 
 |-  ( ( ph /\ n e. ( NN0 ^m 1o ) ) -> { <. X , ( n ` (/) ) >. } finSupp 0 )
74 60 70 73 elrabd 
 |-  ( ( ph /\ n e. ( NN0 ^m 1o ) ) -> { <. X , ( n ` (/) ) >. } e. { h e. ( NN0 ^m { X } ) | h finSupp 0 } )
75 59 74 cofmpt 
 |-  ( ph -> ( F o. ( n e. ( NN0 ^m 1o ) |-> { <. X , ( n ` (/) ) >. } ) ) = ( n e. ( NN0 ^m 1o ) |-> ( F ` { <. X , ( n ` (/) ) >. } ) ) )
76 eqid 
 |-  ( 0g ` R ) = ( 0g ` R )
77 2 1 76 9 mplelsfi 
 |-  ( ph -> F finSupp ( 0g ` R ) )
78 70 ralrimiva 
 |-  ( ph -> A. n e. ( NN0 ^m 1o ) { <. X , ( n ` (/) ) >. } e. ( NN0 ^m { X } ) )
79 63 ad2antrr 
 |-  ( ( ( ( ph /\ n e. ( NN0 ^m 1o ) ) /\ m e. ( NN0 ^m 1o ) ) /\ { <. X , ( n ` (/) ) >. } = { <. X , ( m ` (/) ) >. } ) -> X e. V )
80 fvexd 
 |-  ( ( ( ( ph /\ n e. ( NN0 ^m 1o ) ) /\ m e. ( NN0 ^m 1o ) ) /\ { <. X , ( n ` (/) ) >. } = { <. X , ( m ` (/) ) >. } ) -> ( n ` (/) ) e. _V )
81 opex 
 |-  <. X , ( n ` (/) ) >. e. _V
82 81 sneqr 
 |-  ( { <. X , ( n ` (/) ) >. } = { <. X , ( m ` (/) ) >. } -> <. X , ( n ` (/) ) >. = <. X , ( m ` (/) ) >. )
83 82 adantl 
 |-  ( ( ( ( ph /\ n e. ( NN0 ^m 1o ) ) /\ m e. ( NN0 ^m 1o ) ) /\ { <. X , ( n ` (/) ) >. } = { <. X , ( m ` (/) ) >. } ) -> <. X , ( n ` (/) ) >. = <. X , ( m ` (/) ) >. )
84 opthg 
 |-  ( ( X e. V /\ ( n ` (/) ) e. _V ) -> ( <. X , ( n ` (/) ) >. = <. X , ( m ` (/) ) >. <-> ( X = X /\ ( n ` (/) ) = ( m ` (/) ) ) ) )
85 84 simplbda 
 |-  ( ( ( X e. V /\ ( n ` (/) ) e. _V ) /\ <. X , ( n ` (/) ) >. = <. X , ( m ` (/) ) >. ) -> ( n ` (/) ) = ( m ` (/) ) )
86 79 80 83 85 syl21anc 
 |-  ( ( ( ( ph /\ n e. ( NN0 ^m 1o ) ) /\ m e. ( NN0 ^m 1o ) ) /\ { <. X , ( n ` (/) ) >. } = { <. X , ( m ` (/) ) >. } ) -> ( n ` (/) ) = ( m ` (/) ) )
87 0ex 
 |-  (/) e. _V
88 87 a1i 
 |-  ( ( ( ( ph /\ n e. ( NN0 ^m 1o ) ) /\ m e. ( NN0 ^m 1o ) ) /\ { <. X , ( n ` (/) ) >. } = { <. X , ( m ` (/) ) >. } ) -> (/) e. _V )
89 df1o2 
 |-  1o = { (/) }
90 66 ad2antrr 
 |-  ( ( ( ( ph /\ n e. ( NN0 ^m 1o ) ) /\ m e. ( NN0 ^m 1o ) ) /\ { <. X , ( n ` (/) ) >. } = { <. X , ( m ` (/) ) >. } ) -> n : 1o --> NN0 )
91 90 ffnd 
 |-  ( ( ( ( ph /\ n e. ( NN0 ^m 1o ) ) /\ m e. ( NN0 ^m 1o ) ) /\ { <. X , ( n ` (/) ) >. } = { <. X , ( m ` (/) ) >. } ) -> n Fn 1o )
92 36 ad4ant13 
 |-  ( ( ( ( ph /\ n e. ( NN0 ^m 1o ) ) /\ m e. ( NN0 ^m 1o ) ) /\ { <. X , ( n ` (/) ) >. } = { <. X , ( m ` (/) ) >. } ) -> m : 1o --> NN0 )
93 92 ffnd 
 |-  ( ( ( ( ph /\ n e. ( NN0 ^m 1o ) ) /\ m e. ( NN0 ^m 1o ) ) /\ { <. X , ( n ` (/) ) >. } = { <. X , ( m ` (/) ) >. } ) -> m Fn 1o )
94 88 89 91 93 fsneq 
 |-  ( ( ( ( ph /\ n e. ( NN0 ^m 1o ) ) /\ m e. ( NN0 ^m 1o ) ) /\ { <. X , ( n ` (/) ) >. } = { <. X , ( m ` (/) ) >. } ) -> ( n = m <-> ( n ` (/) ) = ( m ` (/) ) ) )
95 86 94 mpbird 
 |-  ( ( ( ( ph /\ n e. ( NN0 ^m 1o ) ) /\ m e. ( NN0 ^m 1o ) ) /\ { <. X , ( n ` (/) ) >. } = { <. X , ( m ` (/) ) >. } ) -> n = m )
96 95 ex 
 |-  ( ( ( ph /\ n e. ( NN0 ^m 1o ) ) /\ m e. ( NN0 ^m 1o ) ) -> ( { <. X , ( n ` (/) ) >. } = { <. X , ( m ` (/) ) >. } -> n = m ) )
97 96 anasss 
 |-  ( ( ph /\ ( n e. ( NN0 ^m 1o ) /\ m e. ( NN0 ^m 1o ) ) ) -> ( { <. X , ( n ` (/) ) >. } = { <. X , ( m ` (/) ) >. } -> n = m ) )
98 97 ralrimivva 
 |-  ( ph -> A. n e. ( NN0 ^m 1o ) A. m e. ( NN0 ^m 1o ) ( { <. X , ( n ` (/) ) >. } = { <. X , ( m ` (/) ) >. } -> n = m ) )
99 eqid 
 |-  ( n e. ( NN0 ^m 1o ) |-> { <. X , ( n ` (/) ) >. } ) = ( n e. ( NN0 ^m 1o ) |-> { <. X , ( n ` (/) ) >. } )
100 99 19 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 ) ) )
101 78 98 100 sylanbrc 
 |-  ( ph -> ( n e. ( NN0 ^m 1o ) |-> { <. X , ( n ` (/) ) >. } ) : ( NN0 ^m 1o ) -1-1-> ( NN0 ^m { X } ) )
102 fvexd 
 |-  ( ph -> ( 0g ` R ) e. _V )
103 77 101 102 9 fsuppco 
 |-  ( ph -> ( F o. ( n e. ( NN0 ^m 1o ) |-> { <. X , ( n ` (/) ) >. } ) ) finSupp ( 0g ` R ) )
104 75 103 eqbrtrrd 
 |-  ( ph -> ( n e. ( NN0 ^m 1o ) |-> ( F ` { <. X , ( n ` (/) ) >. } ) ) finSupp ( 0g ` R ) )
105 16 104 eqbrtrd 
 |-  ( ph -> ( M ` F ) finSupp ( 0g ` R ) )
106 eqid 
 |-  ( 1o mPoly R ) = ( 1o mPoly R )
107 eqid 
 |-  ( Base ` Q ) = ( Base ` Q )
108 5 107 ply1bas 
 |-  ( Base ` Q ) = ( Base ` ( 1o mPoly R ) )
109 106 53 55 76 108 mplelbas 
 |-  ( ( M ` F ) e. ( Base ` Q ) <-> ( ( M ` F ) e. ( Base ` ( 1o mPwSer R ) ) /\ ( M ` F ) finSupp ( 0g ` R ) ) )
110 58 105 109 sylanbrc 
 |-  ( ph -> ( M ` F ) e. ( Base ` Q ) )