Metamath Proof Explorer

Theorem selvmul

Description: The "variable selection" function is multiplicative. (Contributed by SN, 18-Feb-2025)

Ref Expression
Hypotheses selvmul.p 
|- P = ( I mPoly R )
selvmul.b 
|- B = ( Base ` P )
selvmul.1 
|- .x. = ( .r ` P )
selvmul.u 
|- U = ( ( I \ J ) mPoly R )
selvmul.t 
|- T = ( J mPoly U )
selvmul.2 
|- .xb = ( .r ` T )
selvmul.i 
|- ( ph -> I e. V )
selvmul.r 
|- ( ph -> R e. CRing )
selvmul.j 
|- ( ph -> J C_ I )
selvmul.f 
|- ( ph -> F e. B )
selvmul.g 
|- ( ph -> G e. B )
Assertion selvmul 
|- ( ph -> ( ( ( I selectVars R ) ` J ) ` ( F .x. G ) ) = ( ( ( ( I selectVars R ) ` J ) ` F ) .xb ( ( ( I selectVars R ) ` J ) ` G ) ) )

Proof

Step Hyp Ref Expression
1 selvmul.p 
 |-  P = ( I mPoly R )
2 selvmul.b 
 |-  B = ( Base ` P )
3 selvmul.1 
 |-  .x. = ( .r ` P )
4 selvmul.u 
 |-  U = ( ( I \ J ) mPoly R )
5 selvmul.t 
 |-  T = ( J mPoly U )
6 selvmul.2 
 |-  .xb = ( .r ` T )
7 selvmul.i 
 |-  ( ph -> I e. V )
8 selvmul.r 
 |-  ( ph -> R e. CRing )
9 selvmul.j 
 |-  ( ph -> J C_ I )
10 selvmul.f 
 |-  ( ph -> F e. B )
11 selvmul.g 
 |-  ( ph -> G e. B )
12 eqid 
 |-  ( I mPoly T ) = ( I mPoly T )
13 eqid 
 |-  ( Base ` ( I mPoly T ) ) = ( Base ` ( I mPoly T ) )
14 eqid 
 |-  ( .r ` ( I mPoly T ) ) = ( .r ` ( I mPoly T ) )
15 eqid 
 |-  ( algSc ` T ) = ( algSc ` T )
16 eqid 
 |-  ( ( algSc ` T ) o. ( algSc ` U ) ) = ( ( algSc ` T ) o. ( algSc ` U ) )
17 7 difexd 
 |-  ( ph -> ( I \ J ) e. _V )
18 7 9 ssexd 
 |-  ( ph -> J e. _V )
19 4 5 15 16 17 18 8 selvcllem2 
 |-  ( ph -> ( ( algSc ` T ) o. ( algSc ` U ) ) e. ( R RingHom T ) )
20 1 12 2 13 3 14 19 10 11 rhmcomulmpl 
 |-  ( ph -> ( ( ( algSc ` T ) o. ( algSc ` U ) ) o. ( F .x. G ) ) = ( ( ( ( algSc ` T ) o. ( algSc ` U ) ) o. F ) ( .r ` ( I mPoly T ) ) ( ( ( algSc ` T ) o. ( algSc ` U ) ) o. G ) ) )
21 20 fveq2d 
 |-  ( ph -> ( ( I eval T ) ` ( ( ( algSc ` T ) o. ( algSc ` U ) ) o. ( F .x. G ) ) ) = ( ( I eval T ) ` ( ( ( ( algSc ` T ) o. ( algSc ` U ) ) o. F ) ( .r ` ( I mPoly T ) ) ( ( ( algSc ` T ) o. ( algSc ` U ) ) o. G ) ) ) )
22 21 fveq1d 
 |-  ( ph -> ( ( ( I eval T ) ` ( ( ( algSc ` T ) o. ( algSc ` U ) ) o. ( F .x. G ) ) ) ` ( x e. I |-> if ( x e. J , ( ( J mVar U ) ` x ) , ( ( algSc ` T ) ` ( ( ( I \ J ) mVar R ) ` x ) ) ) ) ) = ( ( ( I eval T ) ` ( ( ( ( algSc ` T ) o. ( algSc ` U ) ) o. F ) ( .r ` ( I mPoly T ) ) ( ( ( algSc ` T ) o. ( algSc ` U ) ) o. G ) ) ) ` ( x e. I |-> if ( x e. J , ( ( J mVar U ) ` x ) , ( ( algSc ` T ) ` ( ( ( I \ J ) mVar R ) ` x ) ) ) ) ) )
23 eqid 
 |-  ( I eval T ) = ( I eval T )
24 eqid 
 |-  ( Base ` T ) = ( Base ` T )
25 4 17 8 mplcrngd 
 |-  ( ph -> U e. CRing )
26 5 18 25 mplcrngd 
 |-  ( ph -> T e. CRing )
27 eqid 
 |-  ( x e. I |-> if ( x e. J , ( ( J mVar U ) ` x ) , ( ( algSc ` T ) ` ( ( ( I \ J ) mVar R ) ` x ) ) ) ) = ( x e. I |-> if ( x e. J , ( ( J mVar U ) ` x ) , ( ( algSc ` T ) ` ( ( ( I \ J ) mVar R ) ` x ) ) ) )
28 4 5 15 24 27 7 8 9 selvcllem5 
 |-  ( ph -> ( x e. I |-> if ( x e. J , ( ( J mVar U ) ` x ) , ( ( algSc ` T ) ` ( ( ( I \ J ) mVar R ) ` x ) ) ) ) e. ( ( Base ` T ) ^m I ) )
29 rhmghm 
 |-  ( ( ( algSc ` T ) o. ( algSc ` U ) ) e. ( R RingHom T ) -> ( ( algSc ` T ) o. ( algSc ` U ) ) e. ( R GrpHom T ) )
30 ghmmhm 
 |-  ( ( ( algSc ` T ) o. ( algSc ` U ) ) e. ( R GrpHom T ) -> ( ( algSc ` T ) o. ( algSc ` U ) ) e. ( R MndHom T ) )
31 19 29 30 3syl 
 |-  ( ph -> ( ( algSc ` T ) o. ( algSc ` U ) ) e. ( R MndHom T ) )
32 1 12 2 13 31 10 mhmcompl 
 |-  ( ph -> ( ( ( algSc ` T ) o. ( algSc ` U ) ) o. F ) e. ( Base ` ( I mPoly T ) ) )
33 eqidd 
 |-  ( ph -> ( ( ( I eval T ) ` ( ( ( algSc ` T ) o. ( algSc ` U ) ) o. F ) ) ` ( x e. I |-> if ( x e. J , ( ( J mVar U ) ` x ) , ( ( algSc ` T ) ` ( ( ( I \ J ) mVar R ) ` x ) ) ) ) ) = ( ( ( I eval T ) ` ( ( ( algSc ` T ) o. ( algSc ` U ) ) o. F ) ) ` ( x e. I |-> if ( x e. J , ( ( J mVar U ) ` x ) , ( ( algSc ` T ) ` ( ( ( I \ J ) mVar R ) ` x ) ) ) ) ) )
34 32 33 jca 
 |-  ( ph -> ( ( ( ( algSc ` T ) o. ( algSc ` U ) ) o. F ) e. ( Base ` ( I mPoly T ) ) /\ ( ( ( I eval T ) ` ( ( ( algSc ` T ) o. ( algSc ` U ) ) o. F ) ) ` ( x e. I |-> if ( x e. J , ( ( J mVar U ) ` x ) , ( ( algSc ` T ) ` ( ( ( I \ J ) mVar R ) ` x ) ) ) ) ) = ( ( ( I eval T ) ` ( ( ( algSc ` T ) o. ( algSc ` U ) ) o. F ) ) ` ( x e. I |-> if ( x e. J , ( ( J mVar U ) ` x ) , ( ( algSc ` T ) ` ( ( ( I \ J ) mVar R ) ` x ) ) ) ) ) ) )
35 1 12 2 13 31 11 mhmcompl 
 |-  ( ph -> ( ( ( algSc ` T ) o. ( algSc ` U ) ) o. G ) e. ( Base ` ( I mPoly T ) ) )
36 eqidd 
 |-  ( ph -> ( ( ( I eval T ) ` ( ( ( algSc ` T ) o. ( algSc ` U ) ) o. G ) ) ` ( x e. I |-> if ( x e. J , ( ( J mVar U ) ` x ) , ( ( algSc ` T ) ` ( ( ( I \ J ) mVar R ) ` x ) ) ) ) ) = ( ( ( I eval T ) ` ( ( ( algSc ` T ) o. ( algSc ` U ) ) o. G ) ) ` ( x e. I |-> if ( x e. J , ( ( J mVar U ) ` x ) , ( ( algSc ` T ) ` ( ( ( I \ J ) mVar R ) ` x ) ) ) ) ) )
37 35 36 jca 
 |-  ( ph -> ( ( ( ( algSc ` T ) o. ( algSc ` U ) ) o. G ) e. ( Base ` ( I mPoly T ) ) /\ ( ( ( I eval T ) ` ( ( ( algSc ` T ) o. ( algSc ` U ) ) o. G ) ) ` ( x e. I |-> if ( x e. J , ( ( J mVar U ) ` x ) , ( ( algSc ` T ) ` ( ( ( I \ J ) mVar R ) ` x ) ) ) ) ) = ( ( ( I eval T ) ` ( ( ( algSc ` T ) o. ( algSc ` U ) ) o. G ) ) ` ( x e. I |-> if ( x e. J , ( ( J mVar U ) ` x ) , ( ( algSc ` T ) ` ( ( ( I \ J ) mVar R ) ` x ) ) ) ) ) ) )
38 23 12 24 13 14 6 7 26 28 34 37 evlmulval 
 |-  ( ph -> ( ( ( ( ( algSc ` T ) o. ( algSc ` U ) ) o. F ) ( .r ` ( I mPoly T ) ) ( ( ( algSc ` T ) o. ( algSc ` U ) ) o. G ) ) e. ( Base ` ( I mPoly T ) ) /\ ( ( ( I eval T ) ` ( ( ( ( algSc ` T ) o. ( algSc ` U ) ) o. F ) ( .r ` ( I mPoly T ) ) ( ( ( algSc ` T ) o. ( algSc ` U ) ) o. G ) ) ) ` ( x e. I |-> if ( x e. J , ( ( J mVar U ) ` x ) , ( ( algSc ` T ) ` ( ( ( I \ J ) mVar R ) ` x ) ) ) ) ) = ( ( ( ( I eval T ) ` ( ( ( algSc ` T ) o. ( algSc ` U ) ) o. F ) ) ` ( x e. I |-> if ( x e. J , ( ( J mVar U ) ` x ) , ( ( algSc ` T ) ` ( ( ( I \ J ) mVar R ) ` x ) ) ) ) ) .xb ( ( ( I eval T ) ` ( ( ( algSc ` T ) o. ( algSc ` U ) ) o. G ) ) ` ( x e. I |-> if ( x e. J , ( ( J mVar U ) ` x ) , ( ( algSc ` T ) ` ( ( ( I \ J ) mVar R ) ` x ) ) ) ) ) ) ) )
39 38 simprd 
 |-  ( ph -> ( ( ( I eval T ) ` ( ( ( ( algSc ` T ) o. ( algSc ` U ) ) o. F ) ( .r ` ( I mPoly T ) ) ( ( ( algSc ` T ) o. ( algSc ` U ) ) o. G ) ) ) ` ( x e. I |-> if ( x e. J , ( ( J mVar U ) ` x ) , ( ( algSc ` T ) ` ( ( ( I \ J ) mVar R ) ` x ) ) ) ) ) = ( ( ( ( I eval T ) ` ( ( ( algSc ` T ) o. ( algSc ` U ) ) o. F ) ) ` ( x e. I |-> if ( x e. J , ( ( J mVar U ) ` x ) , ( ( algSc ` T ) ` ( ( ( I \ J ) mVar R ) ` x ) ) ) ) ) .xb ( ( ( I eval T ) ` ( ( ( algSc ` T ) o. ( algSc ` U ) ) o. G ) ) ` ( x e. I |-> if ( x e. J , ( ( J mVar U ) ` x ) , ( ( algSc ` T ) ` ( ( ( I \ J ) mVar R ) ` x ) ) ) ) ) ) )
40 22 39 eqtrd 
 |-  ( ph -> ( ( ( I eval T ) ` ( ( ( algSc ` T ) o. ( algSc ` U ) ) o. ( F .x. G ) ) ) ` ( x e. I |-> if ( x e. J , ( ( J mVar U ) ` x ) , ( ( algSc ` T ) ` ( ( ( I \ J ) mVar R ) ` x ) ) ) ) ) = ( ( ( ( I eval T ) ` ( ( ( algSc ` T ) o. ( algSc ` U ) ) o. F ) ) ` ( x e. I |-> if ( x e. J , ( ( J mVar U ) ` x ) , ( ( algSc ` T ) ` ( ( ( I \ J ) mVar R ) ` x ) ) ) ) ) .xb ( ( ( I eval T ) ` ( ( ( algSc ` T ) o. ( algSc ` U ) ) o. G ) ) ` ( x e. I |-> if ( x e. J , ( ( J mVar U ) ` x ) , ( ( algSc ` T ) ` ( ( ( I \ J ) mVar R ) ` x ) ) ) ) ) ) )
41 1 7 8 mplcrngd 
 |-  ( ph -> P e. CRing )
42 41 crngringd 
 |-  ( ph -> P e. Ring )
43 2 3 42 10 11 ringcld 
 |-  ( ph -> ( F .x. G ) e. B )
44 1 2 4 5 15 16 8 9 43 selvval2 
 |-  ( ph -> ( ( ( I selectVars R ) ` J ) ` ( F .x. G ) ) = ( ( ( I eval T ) ` ( ( ( algSc ` T ) o. ( algSc ` U ) ) o. ( F .x. G ) ) ) ` ( x e. I |-> if ( x e. J , ( ( J mVar U ) ` x ) , ( ( algSc ` T ) ` ( ( ( I \ J ) mVar R ) ` x ) ) ) ) ) )
45 1 2 4 5 15 16 8 9 10 selvval2 
 |-  ( ph -> ( ( ( I selectVars R ) ` J ) ` F ) = ( ( ( I eval T ) ` ( ( ( algSc ` T ) o. ( algSc ` U ) ) o. F ) ) ` ( x e. I |-> if ( x e. J , ( ( J mVar U ) ` x ) , ( ( algSc ` T ) ` ( ( ( I \ J ) mVar R ) ` x ) ) ) ) ) )
46 1 2 4 5 15 16 8 9 11 selvval2 
 |-  ( ph -> ( ( ( I selectVars R ) ` J ) ` G ) = ( ( ( I eval T ) ` ( ( ( algSc ` T ) o. ( algSc ` U ) ) o. G ) ) ` ( x e. I |-> if ( x e. J , ( ( J mVar U ) ` x ) , ( ( algSc ` T ) ` ( ( ( I \ J ) mVar R ) ` x ) ) ) ) ) )
47 45 46 oveq12d 
 |-  ( ph -> ( ( ( ( I selectVars R ) ` J ) ` F ) .xb ( ( ( I selectVars R ) ` J ) ` G ) ) = ( ( ( ( I eval T ) ` ( ( ( algSc ` T ) o. ( algSc ` U ) ) o. F ) ) ` ( x e. I |-> if ( x e. J , ( ( J mVar U ) ` x ) , ( ( algSc ` T ) ` ( ( ( I \ J ) mVar R ) ` x ) ) ) ) ) .xb ( ( ( I eval T ) ` ( ( ( algSc ` T ) o. ( algSc ` U ) ) o. G ) ) ` ( x e. I |-> if ( x e. J , ( ( J mVar U ) ` x ) , ( ( algSc ` T ) ` ( ( ( I \ J ) mVar R ) ` x ) ) ) ) ) ) )
48 40 44 47 3eqtr4d 
 |-  ( ph -> ( ( ( I selectVars R ) ` J ) ` ( F .x. G ) ) = ( ( ( ( I selectVars R ) ` J ) ` F ) .xb ( ( ( I selectVars R ) ` J ) ` G ) ) )