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 ⊢ + ˙ = + P
selvadd.u ⊢ U = I ∖ J mPoly R
selvadd.t ⊢ T = J mPoly U
selvadd.2 ⊢ ✚ ˙ = + T
selvadd.i ⊢ φ → I ∈ V
selvadd.r ⊢ φ → R ∈ CRing
selvadd.j ⊢ φ → J ⊆ I
selvadd.f ⊢ φ → F ∈ B
selvadd.g ⊢ φ → G ∈ B
Assertion selvadd ⊢ φ → I selectVars R ⁡ J ⁡ F + ˙ G = I selectVars R ⁡ J ⁡ F ✚ ˙ 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 ⊢ + ˙ = + P
4 selvadd.u ⊢ U = I ∖ J mPoly R
5 selvadd.t ⊢ T = J mPoly U
6 selvadd.2 ⊢ ✚ ˙ = + T
7 selvadd.i ⊢ φ → I ∈ V
8 selvadd.r ⊢ φ → R ∈ CRing
9 selvadd.j ⊢ φ → J ⊆ I
10 selvadd.f ⊢ φ → F ∈ B
11 selvadd.g ⊢ φ → G ∈ B
12 eqid ⊢ I mPoly T = I mPoly T
13 eqid ⊢ Base I mPoly T = Base I mPoly T
14 eqid ⊢ + I mPoly T = + I mPoly T
15 eqid ⊢ algSc ⁡ T = algSc ⁡ T
16 eqid ⊢ algSc ⁡ T ∘ algSc ⁡ U = algSc ⁡ T ∘ algSc ⁡ U
17 7 difexd ⊢ φ → I ∖ J ∈ V
18 7 9 ssexd ⊢ φ → J ∈ V
19 4 5 15 16 17 18 8 selvcllem2 ⊢ φ → algSc ⁡ T ∘ algSc ⁡ U ∈ R RingHom T
20 rhmghm ⊢ algSc ⁡ T ∘ algSc ⁡ U ∈ R RingHom T → algSc ⁡ T ∘ algSc ⁡ U ∈ R GrpHom T
21 ghmmhm ⊢ algSc ⁡ T ∘ algSc ⁡ U ∈ R GrpHom T → algSc ⁡ T ∘ algSc ⁡ U ∈ R MndHom T
22 19 20 21 3syl ⊢ φ → algSc ⁡ T ∘ algSc ⁡ U ∈ R MndHom T
23 1 12 2 13 3 14 22 10 11 mhmcoaddmpl ⊢ φ → algSc ⁡ T ∘ algSc ⁡ U ∘ F + ˙ G = algSc ⁡ T ∘ algSc ⁡ U ∘ F + I mPoly T algSc ⁡ T ∘ algSc ⁡ U ∘ G
24 23 fveq2d ⊢ φ → I eval T ⁡ algSc ⁡ T ∘ algSc ⁡ U ∘ F + ˙ G = I eval T ⁡ algSc ⁡ T ∘ algSc ⁡ U ∘ F + I mPoly T algSc ⁡ T ∘ algSc ⁡ U ∘ G
25 24 fveq1d ⊢ φ → I eval T ⁡ algSc ⁡ T ∘ algSc ⁡ U ∘ F + ˙ G ⁡ x ∈ I ⟼ if x ∈ J J mVar U ⁡ x algSc ⁡ T ⁡ I ∖ J mVar R ⁡ x = I eval T ⁡ algSc ⁡ T ∘ algSc ⁡ U ∘ F + I mPoly T algSc ⁡ T ∘ algSc ⁡ U ∘ G ⁡ x ∈ I ⟼ if x ∈ 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 ⊢ φ → U ∈ CRing
29 5 18 28 mplcrngd ⊢ φ → T ∈ CRing
30 eqid ⊢ x ∈ I ⟼ if x ∈ J J mVar U ⁡ x algSc ⁡ T ⁡ I ∖ J mVar R ⁡ x = x ∈ I ⟼ if x ∈ J J mVar U ⁡ x algSc ⁡ T ⁡ I ∖ J mVar R ⁡ x
31 4 5 15 27 30 7 8 9 selvcllem5 ⊢ φ → x ∈ I ⟼ if x ∈ J J mVar U ⁡ x algSc ⁡ T ⁡ I ∖ J mVar R ⁡ x ∈ Base T I
32 1 12 2 13 22 10 mhmcompl ⊢ φ → algSc ⁡ T ∘ algSc ⁡ U ∘ F ∈ Base I mPoly T
33 eqidd ⊢ φ → I eval T ⁡ algSc ⁡ T ∘ algSc ⁡ U ∘ F ⁡ x ∈ I ⟼ if x ∈ J J mVar U ⁡ x algSc ⁡ T ⁡ I ∖ J mVar R ⁡ x = I eval T ⁡ algSc ⁡ T ∘ algSc ⁡ U ∘ F ⁡ x ∈ I ⟼ if x ∈ J J mVar U ⁡ x algSc ⁡ T ⁡ I ∖ J mVar R ⁡ x
34 32 33 jca ⊢ φ → algSc ⁡ T ∘ algSc ⁡ U ∘ F ∈ Base I mPoly T ∧ I eval T ⁡ algSc ⁡ T ∘ algSc ⁡ U ∘ F ⁡ x ∈ I ⟼ if x ∈ J J mVar U ⁡ x algSc ⁡ T ⁡ I ∖ J mVar R ⁡ x = I eval T ⁡ algSc ⁡ T ∘ algSc ⁡ U ∘ F ⁡ x ∈ I ⟼ if x ∈ J J mVar U ⁡ x algSc ⁡ T ⁡ I ∖ J mVar R ⁡ x
35 1 12 2 13 22 11 mhmcompl ⊢ φ → algSc ⁡ T ∘ algSc ⁡ U ∘ G ∈ Base I mPoly T
36 eqidd ⊢ φ → I eval T ⁡ algSc ⁡ T ∘ algSc ⁡ U ∘ G ⁡ x ∈ I ⟼ if x ∈ J J mVar U ⁡ x algSc ⁡ T ⁡ I ∖ J mVar R ⁡ x = I eval T ⁡ algSc ⁡ T ∘ algSc ⁡ U ∘ G ⁡ x ∈ I ⟼ if x ∈ J J mVar U ⁡ x algSc ⁡ T ⁡ I ∖ J mVar R ⁡ x
37 35 36 jca ⊢ φ → algSc ⁡ T ∘ algSc ⁡ U ∘ G ∈ Base I mPoly T ∧ I eval T ⁡ algSc ⁡ T ∘ algSc ⁡ U ∘ G ⁡ x ∈ I ⟼ if x ∈ J J mVar U ⁡ x algSc ⁡ T ⁡ I ∖ J mVar R ⁡ x = I eval T ⁡ algSc ⁡ T ∘ algSc ⁡ U ∘ G ⁡ x ∈ I ⟼ if x ∈ 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 ⊢ φ → algSc ⁡ T ∘ algSc ⁡ U ∘ F + I mPoly T algSc ⁡ T ∘ algSc ⁡ U ∘ G ∈ Base I mPoly T ∧ I eval T ⁡ algSc ⁡ T ∘ algSc ⁡ U ∘ F + I mPoly T algSc ⁡ T ∘ algSc ⁡ U ∘ G ⁡ x ∈ I ⟼ if x ∈ J J mVar U ⁡ x algSc ⁡ T ⁡ I ∖ J mVar R ⁡ x = I eval T ⁡ algSc ⁡ T ∘ algSc ⁡ U ∘ F ⁡ x ∈ I ⟼ if x ∈ J J mVar U ⁡ x algSc ⁡ T ⁡ I ∖ J mVar R ⁡ x ✚ ˙ I eval T ⁡ algSc ⁡ T ∘ algSc ⁡ U ∘ G ⁡ x ∈ I ⟼ if x ∈ J J mVar U ⁡ x algSc ⁡ T ⁡ I ∖ J mVar R ⁡ x
39 38 simprd ⊢ φ → I eval T ⁡ algSc ⁡ T ∘ algSc ⁡ U ∘ F + I mPoly T algSc ⁡ T ∘ algSc ⁡ U ∘ G ⁡ x ∈ I ⟼ if x ∈ J J mVar U ⁡ x algSc ⁡ T ⁡ I ∖ J mVar R ⁡ x = I eval T ⁡ algSc ⁡ T ∘ algSc ⁡ U ∘ F ⁡ x ∈ I ⟼ if x ∈ J J mVar U ⁡ x algSc ⁡ T ⁡ I ∖ J mVar R ⁡ x ✚ ˙ I eval T ⁡ algSc ⁡ T ∘ algSc ⁡ U ∘ G ⁡ x ∈ I ⟼ if x ∈ J J mVar U ⁡ x algSc ⁡ T ⁡ I ∖ J mVar R ⁡ x
40 25 39 eqtrd ⊢ φ → I eval T ⁡ algSc ⁡ T ∘ algSc ⁡ U ∘ F + ˙ G ⁡ x ∈ I ⟼ if x ∈ J J mVar U ⁡ x algSc ⁡ T ⁡ I ∖ J mVar R ⁡ x = I eval T ⁡ algSc ⁡ T ∘ algSc ⁡ U ∘ F ⁡ x ∈ I ⟼ if x ∈ J J mVar U ⁡ x algSc ⁡ T ⁡ I ∖ J mVar R ⁡ x ✚ ˙ I eval T ⁡ algSc ⁡ T ∘ algSc ⁡ U ∘ G ⁡ x ∈ I ⟼ if x ∈ J J mVar U ⁡ x algSc ⁡ T ⁡ I ∖ J mVar R ⁡ x
41 1 7 8 mplcrngd ⊢ φ → P ∈ CRing
42 41 crnggrpd ⊢ φ → P ∈ Grp
43 2 3 42 10 11 grpcld ⊢ φ → F + ˙ G ∈ B
44 1 2 4 5 15 16 8 9 43 selvval2 ⊢ φ → I selectVars R ⁡ J ⁡ F + ˙ G = I eval T ⁡ algSc ⁡ T ∘ algSc ⁡ U ∘ F + ˙ G ⁡ x ∈ I ⟼ if x ∈ J J mVar U ⁡ x algSc ⁡ T ⁡ I ∖ J mVar R ⁡ x
45 1 2 4 5 15 16 8 9 10 selvval2 ⊢ φ → I selectVars R ⁡ J ⁡ F = I eval T ⁡ algSc ⁡ T ∘ algSc ⁡ U ∘ F ⁡ x ∈ I ⟼ if x ∈ J J mVar U ⁡ x algSc ⁡ T ⁡ I ∖ J mVar R ⁡ x
46 1 2 4 5 15 16 8 9 11 selvval2 ⊢ φ → I selectVars R ⁡ J ⁡ G = I eval T ⁡ algSc ⁡ T ∘ algSc ⁡ U ∘ G ⁡ x ∈ I ⟼ if x ∈ J J mVar U ⁡ x algSc ⁡ T ⁡ I ∖ J mVar R ⁡ x
47 45 46 oveq12d ⊢ φ → I selectVars R ⁡ J ⁡ F ✚ ˙ I selectVars R ⁡ J ⁡ G = I eval T ⁡ algSc ⁡ T ∘ algSc ⁡ U ∘ F ⁡ x ∈ I ⟼ if x ∈ J J mVar U ⁡ x algSc ⁡ T ⁡ I ∖ J mVar R ⁡ x ✚ ˙ I eval T ⁡ algSc ⁡ T ∘ algSc ⁡ U ∘ G ⁡ x ∈ I ⟼ if x ∈ J J mVar U ⁡ x algSc ⁡ T ⁡ I ∖ J mVar R ⁡ x
48 40 44 47 3eqtr4d ⊢ φ → I selectVars R ⁡ J ⁡ F + ˙ G = I selectVars R ⁡ J ⁡ F ✚ ˙ I selectVars R ⁡ J ⁡ G