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 simpr 
 |-  ( ( ph /\ n e. ( NN0 ^m 1o ) ) -> n e. ( NN0 ^m 1o ) )
57 56 elmaprd 
 |-  ( ( ph /\ n e. ( NN0 ^m 1o ) ) -> n : 1o --> NN0 )
58 0lt1o 
 |-  (/) e. 1o
59 58 a1i 
 |-  ( ( ph /\ n e. ( NN0 ^m 1o ) ) -> (/) e. 1o )
60 57 59 ffvelcdmd 
 |-  ( ( ph /\ n e. ( NN0 ^m 1o ) ) -> ( n ` (/) ) e. NN0 )
61 55 60 fsnd 
 |-  ( ( ph /\ n e. ( NN0 ^m 1o ) ) -> { <. X , ( n ` (/) ) >. } : { X } --> NN0 )
62 52 54 61 elmapdd 
 |-  ( ( ph /\ n e. ( NN0 ^m 1o ) ) -> { <. X , ( n ` (/) ) >. } e. ( NN0 ^m { X } ) )
63 c0ex 
 |-  0 e. _V
64 63 a1i 
 |-  ( ( ph /\ n e. ( NN0 ^m 1o ) ) -> 0 e. _V )
65 snopfsupp 
 |-  ( ( X e. I /\ ( n ` (/) ) e. NN0 /\ 0 e. _V ) -> { <. X , ( n ` (/) ) >. } finSupp 0 )
66 55 60 64 65 syl3anc 
 |-  ( ( ph /\ n e. ( NN0 ^m 1o ) ) -> { <. X , ( n ` (/) ) >. } finSupp 0 )
67 50 62 66 elrabd 
 |-  ( ( ph /\ n e. ( NN0 ^m 1o ) ) -> { <. X , ( n ` (/) ) >. } e. { h e. ( NN0 ^m { X } ) | h finSupp 0 } )
68 eqid 
 |-  { h e. ( NN0 ^m { X } ) | h finSupp 0 } = { h e. ( NN0 ^m { X } ) | h finSupp 0 }
69 68 psrbasfsupp 
 |-  { h e. ( NN0 ^m { X } ) | h finSupp 0 } = { h e. ( NN0 ^m { X } ) | ( `' h " NN ) e. Fin }
70 67 69 eleqtrdi 
 |-  ( ( ph /\ n e. ( NN0 ^m 1o ) ) -> { <. X , ( n ` (/) ) >. } e. { h e. ( NN0 ^m { X } ) | ( `' h " NN ) e. Fin } )
71 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 ` (/) ) >. } ) ) )
72 42 46 49 70 71 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 ` (/) ) >. } ) ) )
73 eqid 
 |-  ( +g ` ( { X } mPoly U ) ) = ( +g ` ( { X } mPoly U ) )
74 35 36 29 73 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 ) ) )
75 74 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 ` (/) ) >. } ) )
76 75 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 ` (/) ) >. } ) )
77 6 adantr 
 |-  ( ( ph /\ n e. ( NN0 ^m 1o ) ) -> I e. V )
78 8 adantr 
 |-  ( ( ph /\ n e. ( NN0 ^m 1o ) ) -> R e. CRing )
79 9 adantr 
 |-  ( ( ph /\ n e. ( NN0 ^m 1o ) ) -> F e. B )
80 1 2 3 4 5 77 55 78 79 56 selvply1rhmlem3 
 |-  ( ( ph /\ n e. ( NN0 ^m 1o ) ) -> ( ( H ` F ) ` n ) = ( ( ( ( I selectVars R ) ` { X } ) ` F ) ` { <. X , ( n ` (/) ) >. } ) )
81 10 adantr 
 |-  ( ( ph /\ n e. ( NN0 ^m 1o ) ) -> G e. B )
82 1 2 3 4 5 77 55 78 81 56 selvply1rhmlem3 
 |-  ( ( ph /\ n e. ( NN0 ^m 1o ) ) -> ( ( H ` G ) ` n ) = ( ( ( ( I selectVars R ) ` { X } ) ` G ) ` { <. X , ( n ` (/) ) >. } ) )
83 80 82 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 ` (/) ) >. } ) ) )
84 72 76 83 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 ) ) )
85 26 34 84 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 ) )
86 85 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 ) ) )
87 fveq2 
 |-  ( f = ( F ( +g ` P ) G ) -> ( ( ( I selectVars R ) ` { X } ) ` f ) = ( ( ( I selectVars R ) ` { X } ) ` ( F ( +g ` P ) G ) ) )
88 eqid 
 |-  ( +g ` P ) = ( +g ` P )
89 2 1 88 3 35 73 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 ) ) )
90 87 89 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 ) ) )
91 90 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 ` (/) ) >. } ) )
92 91 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 ` (/) ) >. } ) ) )
93 8 crngringd 
 |-  ( ph -> R e. Ring )
94 2 6 93 mplringd 
 |-  ( ph -> P e. Ring )
95 94 ringgrpd 
 |-  ( ph -> P e. Grp )
96 1 88 95 9 10 grpcld 
 |-  ( ph -> ( F ( +g ` P ) G ) e. B )
97 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 )
98 5 92 96 97 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 ` (/) ) >. } ) ) )
99 6 difexd 
 |-  ( ph -> ( I \ { X } ) e. _V )
100 3 99 93 mplringd 
 |-  ( ph -> U e. Ring )
101 4 ply1ring 
 |-  ( U e. Ring -> Q e. Ring )
102 100 101 syl 
 |-  ( ph -> Q e. Ring )
103 102 ringgrpd 
 |-  ( ph -> Q e. Grp )
104 13 30 103 12 18 grpcld 
 |-  ( ph -> ( ( H ` F ) ( +g ` Q ) ( H ` G ) ) e. ( Base ` Q ) )
105 4 13 14 ply1basf 
 |-  ( ( ( H ` F ) ( +g ` Q ) ( H ` G ) ) e. ( Base ` Q ) -> ( ( H ` F ) ( +g ` Q ) ( H ` G ) ) : ( NN0 ^m 1o ) --> ( Base ` U ) )
106 104 105 syl 
 |-  ( ph -> ( ( H ` F ) ( +g ` Q ) ( H ` G ) ) : ( NN0 ^m 1o ) --> ( Base ` U ) )
107 106 feqmptd 
 |-  ( ph -> ( ( H ` F ) ( +g ` Q ) ( H ` G ) ) = ( n e. ( NN0 ^m 1o ) |-> ( ( ( H ` F ) ( +g ` Q ) ( H ` G ) ) ` n ) ) )
108 86 98 107 3eqtr4d 
 |-  ( ph -> ( H ` ( F ( +g ` P ) G ) ) = ( ( H ` F ) ( +g ` Q ) ( H ` G ) ) )