Metamath Proof Explorer

Theorem selvply1rhmlem4

Description: Lemma for selvply1rhm : The mapping H is linear. (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 )
selvply1rhmlem4.f 
|- ( ph -> F e. B )
selvply1rhmlem4.g 
|- ( ph -> G e. B )
Assertion selvply1rhmlem4 
|- ( ph -> ( H ` ( F ( +g ` P ) G ) ) = ( ( H ` F ) ( +g ` Q ) ( H ` G ) ) )

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 selvply1rhmlem4.f 
 |-  ( ph -> F e. B )
10 selvply1rhmlem4.g 
 |-  ( ph -> G e. B )
11 1 2 3 4 5 6 7 8 selvply1rhmlem1 
 |-  ( ph -> H : B --> ( Base ` Q ) )
12 11 9 ffvelcdmd 
 |-  ( ph -> ( H ` F ) e. ( Base ` Q ) )
13 eqid 
 |-  ( Base ` Q ) = ( Base ` Q )
14 eqid 
 |-  ( Base ` U ) = ( Base ` U )
15 4 13 14 ply1basf 
 |-  ( ( H ` F ) e. ( Base ` Q ) -> ( H ` F ) : ( NN0 ^m 1o ) --> ( Base ` U ) )
16 12 15 syl 
 |-  ( ph -> ( H ` F ) : ( NN0 ^m 1o ) --> ( Base ` U ) )
17 16 ffnd 
 |-  ( ph -> ( H ` F ) Fn ( NN0 ^m 1o ) )
18 11 10 ffvelcdmd 
 |-  ( ph -> ( H ` G ) e. ( Base ` Q ) )
19 4 13 14 ply1basf 
 |-  ( ( H ` G ) e. ( Base ` Q ) -> ( H ` G ) : ( NN0 ^m 1o ) --> ( Base ` U ) )
20 18 19 syl 
 |-  ( ph -> ( H ` G ) : ( NN0 ^m 1o ) --> ( Base ` U ) )
21 20 ffnd 
 |-  ( ph -> ( H ` G ) Fn ( NN0 ^m 1o ) )
22 ovexd 
 |-  ( ph -> ( NN0 ^m 1o ) e. _V )
23 inidm 
 |-  ( ( NN0 ^m 1o ) i^i ( NN0 ^m 1o ) ) = ( NN0 ^m 1o )
24 eqidd 
 |-  ( ( ph /\ n e. ( NN0 ^m 1o ) ) -> ( ( H ` F ) ` n ) = ( ( H ` F ) ` n ) )
25 eqidd 
 |-  ( ( ph /\ n e. ( NN0 ^m 1o ) ) -> ( ( H ` G ) ` n ) = ( ( H ` G ) ` n ) )
26 17 21 22 22 23 24 25 ofval 
 |-  ( ( ph /\ n e. ( NN0 ^m 1o ) ) -> ( ( ( H ` F ) oF ( +g ` U ) ( H ` G ) ) ` n ) = ( ( ( H ` F ) ` n ) ( +g ` U ) ( ( H ` G ) ` n ) ) )
27 eqid 
 |-  ( 1o mPoly U ) = ( 1o mPoly U )
28 4 13 ply1bas 
 |-  ( Base ` Q ) = ( Base ` ( 1o mPoly U ) )
29 eqid 
 |-  ( +g ` U ) = ( +g ` U )
30 eqid 
 |-  ( +g ` Q ) = ( +g ` Q )
31 4 27 30 ply1plusg 
 |-  ( +g ` Q ) = ( +g ` ( 1o mPoly U ) )
32 27 28 29 31 12 18 mpladd 
 |-  ( ph -> ( ( H ` F ) ( +g ` Q ) ( H ` G ) ) = ( ( H ` F ) oF ( +g ` U ) ( H ` G ) ) )
33 32 fveq1d 
 |-  ( ph -> ( ( ( H ` F ) ( +g ` Q ) ( H ` G ) ) ` n ) = ( ( ( H ` F ) oF ( +g ` U ) ( H ` G ) ) ` n ) )
34 33 adantr 
 |-  ( ( ph /\ n e. ( NN0 ^m 1o ) ) -> ( ( ( H ` F ) ( +g ` Q ) ( H ` G ) ) ` n ) = ( ( ( H ` F ) oF ( +g ` U ) ( H ` G ) ) ` n ) )
35 eqid 
 |-  ( { X } mPoly U ) = ( { X } mPoly U )
36 eqid 
 |-  ( Base ` ( { X } mPoly U ) ) = ( Base ` ( { X } mPoly U ) )
37 eqid 
 |-  { h e. ( NN0 ^m { X } ) | ( `' h " NN ) e. Fin } = { h e. ( NN0 ^m { X } ) | ( `' h " NN ) e. Fin }
38 7 snssd 
 |-  ( ph -> { X } C_ I )
39 2 1 3 35 36 8 38 9 selvcl 
 |-  ( ph -> ( ( ( I selectVars R ) ` { X } ) ` F ) e. ( Base ` ( { X } mPoly U ) ) )
40 35 14 36 37 39 mplelf 
 |-  ( ph -> ( ( ( I selectVars R ) ` { X } ) ` F ) : { h e. ( NN0 ^m { X } ) | ( `' h " NN ) e. Fin } --> ( Base ` U ) )
41 40 ffnd 
 |-  ( ph -> ( ( ( I selectVars R ) ` { X } ) ` F ) Fn { h e. ( NN0 ^m { X } ) | ( `' h " NN ) e. Fin } )
42 41 adantr 
 |-  ( ( ph /\ n e. ( NN0 ^m 1o ) ) -> ( ( ( I selectVars R ) ` { X } ) ` F ) Fn { h e. ( NN0 ^m { X } ) | ( `' h " NN ) e. Fin } )
43 2 1 3 35 36 8 38 10 selvcl 
 |-  ( ph -> ( ( ( I selectVars R ) ` { X } ) ` G ) e. ( Base ` ( { X } mPoly U ) ) )
44 35 14 36 37 43 mplelf 
 |-  ( ph -> ( ( ( I selectVars R ) ` { X } ) ` G ) : { h e. ( NN0 ^m { X } ) | ( `' h " NN ) e. Fin } --> ( Base ` U ) )
45 44 ffnd 
 |-  ( ph -> ( ( ( I selectVars R ) ` { X } ) ` G ) Fn { h e. ( NN0 ^m { X } ) | ( `' h " NN ) e. Fin } )
46 45 adantr 
 |-  ( ( ph /\ n e. ( NN0 ^m 1o ) ) -> ( ( ( I selectVars R ) ` { X } ) ` G ) Fn { h e. ( NN0 ^m { X } ) | ( `' h " NN ) e. Fin } )
47 ovex 
 |-  ( NN0 ^m { X } ) e. _V
48 47 rabex 
 |-  { h e. ( NN0 ^m { X } ) | ( `' h " NN ) e. Fin } e. _V
49 48 a1i 
 |-  ( ( ph /\ n e. ( NN0 ^m 1o ) ) -> { h e. ( NN0 ^m { X } ) | ( `' h " NN ) e. Fin } e. _V )
50 breq1 
 |-  ( h = { <. X , ( n ` (/) ) >. } -> ( h finSupp 0 <-> { <. X , ( n ` (/) ) >. } finSupp 0 ) )
51 nn0ex 
 |-  NN0 e. _V
52 51 a1i 
 |-  ( ( ph /\ n e. ( NN0 ^m 1o ) ) -> NN0 e. _V )
53 snex 
 |-  { X } e. _V
54 53 a1i 
 |-  ( ( ph /\ n e. ( NN0 ^m 1o ) ) -> { X } e. _V )
55 7 adantr 
 |-  ( ( ph /\ n e. ( NN0 ^m 1o ) ) -> X e. I )
56 1oex 
 |-  1o e. _V
57 56 a1i 
 |-  ( ( ph /\ n e. ( NN0 ^m 1o ) ) -> 1o e. _V )
58 simpr 
 |-  ( ( ph /\ n e. ( NN0 ^m 1o ) ) -> n e. ( NN0 ^m 1o ) )
59 57 52 58 elmaprd 
 |-  ( ( ph /\ n e. ( NN0 ^m 1o ) ) -> n : 1o --> NN0 )
60 0lt1o 
 |-  (/) e. 1o
61 60 a1i 
 |-  ( ( ph /\ n e. ( NN0 ^m 1o ) ) -> (/) e. 1o )
62 59 61 ffvelcdmd 
 |-  ( ( ph /\ n e. ( NN0 ^m 1o ) ) -> ( n ` (/) ) e. NN0 )
63 55 62 fsnd 
 |-  ( ( ph /\ n e. ( NN0 ^m 1o ) ) -> { <. X , ( n ` (/) ) >. } : { X } --> NN0 )
64 52 54 63 elmapdd 
 |-  ( ( ph /\ n e. ( NN0 ^m 1o ) ) -> { <. X , ( n ` (/) ) >. } e. ( NN0 ^m { X } ) )
65 c0ex 
 |-  0 e. _V
66 65 a1i 
 |-  ( ( ph /\ n e. ( NN0 ^m 1o ) ) -> 0 e. _V )
67 snopfsupp 
 |-  ( ( X e. I /\ ( n ` (/) ) e. NN0 /\ 0 e. _V ) -> { <. X , ( n ` (/) ) >. } finSupp 0 )
68 55 62 66 67 syl3anc 
 |-  ( ( ph /\ n e. ( NN0 ^m 1o ) ) -> { <. X , ( n ` (/) ) >. } finSupp 0 )
69 50 64 68 elrabd 
 |-  ( ( ph /\ n e. ( NN0 ^m 1o ) ) -> { <. X , ( n ` (/) ) >. } e. { h e. ( NN0 ^m { X } ) | h finSupp 0 } )
70 eqid 
 |-  { h e. ( NN0 ^m { X } ) | h finSupp 0 } = { h e. ( NN0 ^m { X } ) | h finSupp 0 }
71 70 psrbasfsupp 
 |-  { h e. ( NN0 ^m { X } ) | h finSupp 0 } = { h e. ( NN0 ^m { X } ) | ( `' h " NN ) e. Fin }
72 69 71 eleqtrdi 
 |-  ( ( ph /\ n e. ( NN0 ^m 1o ) ) -> { <. X , ( n ` (/) ) >. } e. { h e. ( NN0 ^m { X } ) | ( `' h " NN ) e. Fin } )
73 fnfvof 
 |-  ( ( ( ( ( ( I selectVars R ) ` { X } ) ` F ) Fn { h e. ( NN0 ^m { X } ) | ( `' h " NN ) e. Fin } /\ ( ( ( I selectVars R ) ` { X } ) ` G ) Fn { h e. ( NN0 ^m { X } ) | ( `' h " NN ) e. Fin } ) /\ ( { h e. ( NN0 ^m { X } ) | ( `' h " NN ) e. Fin } e. _V /\ { <. X , ( n ` (/) ) >. } e. { h e. ( NN0 ^m { X } ) | ( `' h " NN ) e. Fin } ) ) -> ( ( ( ( ( I selectVars R ) ` { X } ) ` F ) oF ( +g ` U ) ( ( ( I selectVars R ) ` { X } ) ` G ) ) ` { <. X , ( n ` (/) ) >. } ) = ( ( ( ( ( I selectVars R ) ` { X } ) ` F ) ` { <. X , ( n ` (/) ) >. } ) ( +g ` U ) ( ( ( ( I selectVars R ) ` { X } ) ` G ) ` { <. X , ( n ` (/) ) >. } ) ) )
74 42 46 49 72 73 syl22anc 
 |-  ( ( ph /\ n e. ( NN0 ^m 1o ) ) -> ( ( ( ( ( I selectVars R ) ` { X } ) ` F ) oF ( +g ` U ) ( ( ( I selectVars R ) ` { X } ) ` G ) ) ` { <. X , ( n ` (/) ) >. } ) = ( ( ( ( ( I selectVars R ) ` { X } ) ` F ) ` { <. X , ( n ` (/) ) >. } ) ( +g ` U ) ( ( ( ( I selectVars R ) ` { X } ) ` G ) ` { <. X , ( n ` (/) ) >. } ) ) )
75 eqid 
 |-  ( +g ` ( { X } mPoly U ) ) = ( +g ` ( { X } mPoly U ) )
76 35 36 29 75 39 43 mpladd 
 |-  ( ph -> ( ( ( ( I selectVars R ) ` { X } ) ` F ) ( +g ` ( { X } mPoly U ) ) ( ( ( I selectVars R ) ` { X } ) ` G ) ) = ( ( ( ( I selectVars R ) ` { X } ) ` F ) oF ( +g ` U ) ( ( ( I selectVars R ) ` { X } ) ` G ) ) )
77 76 fveq1d 
 |-  ( ph -> ( ( ( ( ( I selectVars R ) ` { X } ) ` F ) ( +g ` ( { X } mPoly U ) ) ( ( ( I selectVars R ) ` { X } ) ` G ) ) ` { <. X , ( n ` (/) ) >. } ) = ( ( ( ( ( I selectVars R ) ` { X } ) ` F ) oF ( +g ` U ) ( ( ( I selectVars R ) ` { X } ) ` G ) ) ` { <. X , ( n ` (/) ) >. } ) )
78 77 adantr 
 |-  ( ( ph /\ n e. ( NN0 ^m 1o ) ) -> ( ( ( ( ( I selectVars R ) ` { X } ) ` F ) ( +g ` ( { X } mPoly U ) ) ( ( ( I selectVars R ) ` { X } ) ` G ) ) ` { <. X , ( n ` (/) ) >. } ) = ( ( ( ( ( I selectVars R ) ` { X } ) ` F ) oF ( +g ` U ) ( ( ( I selectVars R ) ` { X } ) ` G ) ) ` { <. X , ( n ` (/) ) >. } ) )
79 6 adantr 
 |-  ( ( ph /\ n e. ( NN0 ^m 1o ) ) -> I e. V )
80 8 adantr 
 |-  ( ( ph /\ n e. ( NN0 ^m 1o ) ) -> R e. CRing )
81 9 adantr 
 |-  ( ( ph /\ n e. ( NN0 ^m 1o ) ) -> F e. B )
82 1 2 3 4 5 79 55 80 81 58 selvply1rhmlem3 
 |-  ( ( ph /\ n e. ( NN0 ^m 1o ) ) -> ( ( H ` F ) ` n ) = ( ( ( ( I selectVars R ) ` { X } ) ` F ) ` { <. X , ( n ` (/) ) >. } ) )
83 10 adantr 
 |-  ( ( ph /\ n e. ( NN0 ^m 1o ) ) -> G e. B )
84 1 2 3 4 5 79 55 80 83 58 selvply1rhmlem3 
 |-  ( ( ph /\ n e. ( NN0 ^m 1o ) ) -> ( ( H ` G ) ` n ) = ( ( ( ( I selectVars R ) ` { X } ) ` G ) ` { <. X , ( n ` (/) ) >. } ) )
85 82 84 oveq12d 
 |-  ( ( ph /\ n e. ( NN0 ^m 1o ) ) -> ( ( ( H ` F ) ` n ) ( +g ` U ) ( ( H ` G ) ` n ) ) = ( ( ( ( ( I selectVars R ) ` { X } ) ` F ) ` { <. X , ( n ` (/) ) >. } ) ( +g ` U ) ( ( ( ( I selectVars R ) ` { X } ) ` G ) ` { <. X , ( n ` (/) ) >. } ) ) )
86 74 78 85 3eqtr4d 
 |-  ( ( ph /\ n e. ( NN0 ^m 1o ) ) -> ( ( ( ( ( I selectVars R ) ` { X } ) ` F ) ( +g ` ( { X } mPoly U ) ) ( ( ( I selectVars R ) ` { X } ) ` G ) ) ` { <. X , ( n ` (/) ) >. } ) = ( ( ( H ` F ) ` n ) ( +g ` U ) ( ( H ` G ) ` n ) ) )
87 26 34 86 3eqtr4rd 
 |-  ( ( ph /\ n e. ( NN0 ^m 1o ) ) -> ( ( ( ( ( I selectVars R ) ` { X } ) ` F ) ( +g ` ( { X } mPoly U ) ) ( ( ( I selectVars R ) ` { X } ) ` G ) ) ` { <. X , ( n ` (/) ) >. } ) = ( ( ( H ` F ) ( +g ` Q ) ( H ` G ) ) ` n ) )
88 87 mpteq2dva 
 |-  ( ph -> ( n e. ( NN0 ^m 1o ) |-> ( ( ( ( ( I selectVars R ) ` { X } ) ` F ) ( +g ` ( { X } mPoly U ) ) ( ( ( I selectVars R ) ` { X } ) ` G ) ) ` { <. X , ( n ` (/) ) >. } ) ) = ( n e. ( NN0 ^m 1o ) |-> ( ( ( H ` F ) ( +g ` Q ) ( H ` G ) ) ` n ) ) )
89 fveq2 
 |-  ( f = ( F ( +g ` P ) G ) -> ( ( ( I selectVars R ) ` { X } ) ` f ) = ( ( ( I selectVars R ) ` { X } ) ` ( F ( +g ` P ) G ) ) )
90 eqid 
 |-  ( +g ` P ) = ( +g ` P )
91 2 1 90 3 35 75 6 8 38 9 10 selvadd 
 |-  ( ph -> ( ( ( I selectVars R ) ` { X } ) ` ( F ( +g ` P ) G ) ) = ( ( ( ( I selectVars R ) ` { X } ) ` F ) ( +g ` ( { X } mPoly U ) ) ( ( ( I selectVars R ) ` { X } ) ` G ) ) )
92 89 91 sylan9eqr 
 |-  ( ( ph /\ f = ( F ( +g ` P ) G ) ) -> ( ( ( I selectVars R ) ` { X } ) ` f ) = ( ( ( ( I selectVars R ) ` { X } ) ` F ) ( +g ` ( { X } mPoly U ) ) ( ( ( I selectVars R ) ` { X } ) ` G ) ) )
93 92 fveq1d 
 |-  ( ( ph /\ f = ( F ( +g ` P ) G ) ) -> ( ( ( ( I selectVars R ) ` { X } ) ` f ) ` { <. X , ( n ` (/) ) >. } ) = ( ( ( ( ( I selectVars R ) ` { X } ) ` F ) ( +g ` ( { X } mPoly U ) ) ( ( ( I selectVars R ) ` { X } ) ` G ) ) ` { <. X , ( n ` (/) ) >. } ) )
94 93 mpteq2dv 
 |-  ( ( ph /\ f = ( F ( +g ` P ) G ) ) -> ( n e. ( NN0 ^m 1o ) |-> ( ( ( ( I selectVars R ) ` { X } ) ` f ) ` { <. X , ( n ` (/) ) >. } ) ) = ( n e. ( NN0 ^m 1o ) |-> ( ( ( ( ( I selectVars R ) ` { X } ) ` F ) ( +g ` ( { X } mPoly U ) ) ( ( ( I selectVars R ) ` { X } ) ` G ) ) ` { <. X , ( n ` (/) ) >. } ) ) )
95 8 crngringd 
 |-  ( ph -> R e. Ring )
96 2 6 95 mplringd 
 |-  ( ph -> P e. Ring )
97 96 ringgrpd 
 |-  ( ph -> P e. Grp )
98 1 90 97 9 10 grpcld 
 |-  ( ph -> ( F ( +g ` P ) G ) e. B )
99 22 mptexd 
 |-  ( ph -> ( n e. ( NN0 ^m 1o ) |-> ( ( ( ( ( I selectVars R ) ` { X } ) ` F ) ( +g ` ( { X } mPoly U ) ) ( ( ( I selectVars R ) ` { X } ) ` G ) ) ` { <. X , ( n ` (/) ) >. } ) ) e. _V )
100 5 94 98 99 fvmptd2 
 |-  ( ph -> ( H ` ( F ( +g ` P ) G ) ) = ( n e. ( NN0 ^m 1o ) |-> ( ( ( ( ( I selectVars R ) ` { X } ) ` F ) ( +g ` ( { X } mPoly U ) ) ( ( ( I selectVars R ) ` { X } ) ` G ) ) ` { <. X , ( n ` (/) ) >. } ) ) )
101 6 difexd 
 |-  ( ph -> ( I \ { X } ) e. _V )
102 3 101 95 mplringd 
 |-  ( ph -> U e. Ring )
103 4 ply1ring 
 |-  ( U e. Ring -> Q e. Ring )
104 102 103 syl 
 |-  ( ph -> Q e. Ring )
105 104 ringgrpd 
 |-  ( ph -> Q e. Grp )
106 13 30 105 12 18 grpcld 
 |-  ( ph -> ( ( H ` F ) ( +g ` Q ) ( H ` G ) ) e. ( Base ` Q ) )
107 4 13 14 ply1basf 
 |-  ( ( ( H ` F ) ( +g ` Q ) ( H ` G ) ) e. ( Base ` Q ) -> ( ( H ` F ) ( +g ` Q ) ( H ` G ) ) : ( NN0 ^m 1o ) --> ( Base ` U ) )
108 106 107 syl 
 |-  ( ph -> ( ( H ` F ) ( +g ` Q ) ( H ` G ) ) : ( NN0 ^m 1o ) --> ( Base ` U ) )
109 108 feqmptd 
 |-  ( ph -> ( ( H ` F ) ( +g ` Q ) ( H ` G ) ) = ( n e. ( NN0 ^m 1o ) |-> ( ( ( H ` F ) ( +g ` Q ) ( H ` G ) ) ` n ) ) )
110 88 100 109 3eqtr4d 
 |-  ( ph -> ( H ` ( F ( +g ` P ) G ) ) = ( ( H ` F ) ( +g ` Q ) ( H ` G ) ) )