Metamath Proof Explorer

Theorem selvadd

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

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

Proof

Step Hyp Ref Expression
1 selvadd.p 
 |-  P = ( I mPoly R )
2 selvadd.b 
 |-  B = ( Base ` P )
3 selvadd.1 
 |-  .+ = ( +g ` P )
4 selvadd.u 
 |-  U = ( ( I \ J ) mPoly R )
5 selvadd.t 
 |-  T = ( J mPoly U )
6 selvadd.2 
 |-  .+b = ( +g ` T )
7 selvadd.i 
 |-  ( ph -> I e. V )
8 selvadd.r 
 |-  ( ph -> R e. CRing )
9 selvadd.j 
 |-  ( ph -> J C_ I )
10 selvadd.f 
 |-  ( ph -> F e. B )
11 selvadd.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 
 |-  ( +g ` ( I mPoly T ) ) = ( +g ` ( 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 rhmghm 
 |-  ( ( ( algSc ` T ) o. ( algSc ` U ) ) e. ( R RingHom T ) -> ( ( algSc ` T ) o. ( algSc ` U ) ) e. ( R GrpHom T ) )
21 ghmmhm 
 |-  ( ( ( algSc ` T ) o. ( algSc ` U ) ) e. ( R GrpHom T ) -> ( ( algSc ` T ) o. ( algSc ` U ) ) e. ( R MndHom T ) )
22 19 20 21 3syl 
 |-  ( ph -> ( ( algSc ` T ) o. ( algSc ` U ) ) e. ( R MndHom T ) )
23 1 12 2 13 3 14 22 10 11 mhmcoaddmpl 
 |-  ( ph -> ( ( ( algSc ` T ) o. ( algSc ` U ) ) o. ( F .+ G ) ) = ( ( ( ( algSc ` T ) o. ( algSc ` U ) ) o. F ) ( +g ` ( I mPoly T ) ) ( ( ( algSc ` T ) o. ( algSc ` U ) ) o. G ) ) )
24 23 fveq2d 
 |-  ( ph -> ( ( I eval T ) ` ( ( ( algSc ` T ) o. ( algSc ` U ) ) o. ( F .+ G ) ) ) = ( ( I eval T ) ` ( ( ( ( algSc ` T ) o. ( algSc ` U ) ) o. F ) ( +g ` ( I mPoly T ) ) ( ( ( algSc ` T ) o. ( algSc ` U ) ) o. G ) ) ) )
25 24 fveq1d 
 |-  ( ph -> ( ( ( I eval T ) ` ( ( ( algSc ` T ) o. ( algSc ` U ) ) o. ( F .+ 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 ) ( +g ` ( 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 ) ) ) ) ) )
26 eqid 
 |-  ( I eval T ) = ( I eval T )
27 eqid 
 |-  ( Base ` T ) = ( Base ` T )
28 4 17 8 mplcrngd 
 |-  ( ph -> U e. CRing )
29 5 18 28 mplcrngd 
 |-  ( ph -> T e. CRing )
30 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 ) ) ) )
31 4 5 15 27 30 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 ) )
32 1 12 2 13 22 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 22 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 26 12 27 13 14 6 7 29 31 34 37 evladdval 
 |-  ( ph -> ( ( ( ( ( algSc ` T ) o. ( algSc ` U ) ) o. F ) ( +g ` ( 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 ) ( +g ` ( 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 ) ) ) ) ) .+b ( ( ( 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 ) ( +g ` ( 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 ) ) ) ) ) .+b ( ( ( 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 25 39 eqtrd 
 |-  ( ph -> ( ( ( I eval T ) ` ( ( ( algSc ` T ) o. ( algSc ` U ) ) o. ( F .+ 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 ) ) ) ) ) .+b ( ( ( 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 crnggrpd 
 |-  ( ph -> P e. Grp )
43 2 3 42 10 11 grpcld 
 |-  ( ph -> ( F .+ G ) e. B )
44 1 2 4 5 15 16 8 9 43 selvval2 
 |-  ( ph -> ( ( ( I selectVars R ) ` J ) ` ( F .+ G ) ) = ( ( ( I eval T ) ` ( ( ( algSc ` T ) o. ( algSc ` U ) ) o. ( F .+ 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 ) .+b ( ( ( 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 ) ) ) ) ) .+b ( ( ( 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 .+ G ) ) = ( ( ( ( I selectVars R ) ` J ) ` F ) .+b ( ( ( I selectVars R ) ` J ) ` G ) ) )