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 ⊢ · ˙ = ⋅ P
selvmul.u ⊢ U = I ∖ J mPoly R
selvmul.t ⊢ T = J mPoly U
selvmul.2 ⊢ ∙ ˙ = ⋅ T
selvmul.i ⊢ φ → I ∈ V
selvmul.r ⊢ φ → R ∈ CRing
selvmul.j ⊢ φ → J ⊆ I
selvmul.f ⊢ φ → F ∈ B
selvmul.g ⊢ φ → G ∈ B
Assertion selvmul ⊢ φ → I selectVars R ⁡ J ⁡ F · ˙ G = I selectVars R ⁡ J ⁡ F ∙ ˙ 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 ⊢ · ˙ = ⋅ P
4 selvmul.u ⊢ U = I ∖ J mPoly R
5 selvmul.t ⊢ T = J mPoly U
6 selvmul.2 ⊢ ∙ ˙ = ⋅ T
7 selvmul.i ⊢ φ → I ∈ V
8 selvmul.r ⊢ φ → R ∈ CRing
9 selvmul.j ⊢ φ → J ⊆ I
10 selvmul.f ⊢ φ → F ∈ B
11 selvmul.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 1 12 2 13 3 14 19 10 11 rhmcomulmpl ⊢ φ → algSc ⁡ T ∘ algSc ⁡ U ∘ F · ˙ G = algSc ⁡ T ∘ algSc ⁡ U ∘ F ⋅ I mPoly T algSc ⁡ T ∘ algSc ⁡ U ∘ G
21 20 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
22 21 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
23 eqid ⊢ I eval T = I eval T
24 eqid ⊢ Base T = Base T
25 4 17 8 mplcrngd ⊢ φ → U ∈ CRing
26 5 18 25 mplcrngd ⊢ φ → T ∈ CRing
27 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
28 4 5 15 24 27 7 8 9 selvcllem5 ⊢ φ → x ∈ I ⟼ if x ∈ J J mVar U ⁡ x algSc ⁡ T ⁡ I ∖ J mVar R ⁡ x ∈ Base T I
29 rhmghm ⊢ algSc ⁡ T ∘ algSc ⁡ U ∈ R RingHom T → algSc ⁡ T ∘ algSc ⁡ U ∈ R GrpHom T
30 ghmmhm ⊢ algSc ⁡ T ∘ algSc ⁡ U ∈ R GrpHom T → algSc ⁡ T ∘ algSc ⁡ U ∈ R MndHom T
31 19 29 30 3syl ⊢ φ → algSc ⁡ T ∘ algSc ⁡ U ∈ R MndHom T
32 1 12 2 13 31 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 31 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 23 12 24 13 14 6 7 26 28 34 37 evlmulval ⊢ φ → 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 22 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 crngringd ⊢ φ → P ∈ Ring
43 2 3 42 10 11 ringcld ⊢ φ → 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