Metamath Proof Explorer

Theorem selvmul

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

Ref Expression
Hypotheses selvmul.p ⊢ 𝑃 = ( 𝐼 mPoly 𝑅 )
selvmul.b ⊢ 𝐵 = ( Base ‘ 𝑃 )
selvmul.1 ⊢ · = ( .r ‘ 𝑃 )
selvmul.u ⊢ 𝑈 = ( ( 𝐼 ∖ 𝐽 ) mPoly 𝑅 )
selvmul.t ⊢ 𝑇 = ( 𝐽 mPoly 𝑈 )
selvmul.2 ⊢ ∙ = ( .r ‘ 𝑇 )
selvmul.i ⊢ ( 𝜑 → 𝐼 ∈ 𝑉 )
selvmul.r ⊢ ( 𝜑 → 𝑅 ∈ CRing )
selvmul.j ⊢ ( 𝜑 → 𝐽 ⊆ 𝐼 )
selvmul.f ⊢ ( 𝜑 → 𝐹 ∈ 𝐵 )
selvmul.g ⊢ ( 𝜑 → 𝐺 ∈ 𝐵 )
Assertion selvmul ( 𝜑 → ( ( ( 𝐼 selectVars 𝑅 ) ‘ 𝐽 ) ‘ ( 𝐹 · 𝐺 ) ) = ( ( ( ( 𝐼 selectVars 𝑅 ) ‘ 𝐽 ) ‘ 𝐹 ) ∙ ( ( ( 𝐼 selectVars 𝑅 ) ‘ 𝐽 ) ‘ 𝐺 ) ) )

Proof

Step Hyp Ref Expression
1 selvmul.p ⊢ 𝑃 = ( 𝐼 mPoly 𝑅 )
2 selvmul.b ⊢ 𝐵 = ( Base ‘ 𝑃 )
3 selvmul.1 ⊢ · = ( .r ‘ 𝑃 )
4 selvmul.u ⊢ 𝑈 = ( ( 𝐼 ∖ 𝐽 ) mPoly 𝑅 )
5 selvmul.t ⊢ 𝑇 = ( 𝐽 mPoly 𝑈 )
6 selvmul.2 ⊢ ∙ = ( .r ‘ 𝑇 )
7 selvmul.i ⊢ ( 𝜑 → 𝐼 ∈ 𝑉 )
8 selvmul.r ⊢ ( 𝜑 → 𝑅 ∈ CRing )
9 selvmul.j ⊢ ( 𝜑 → 𝐽 ⊆ 𝐼 )
10 selvmul.f ⊢ ( 𝜑 → 𝐹 ∈ 𝐵 )
11 selvmul.g ⊢ ( 𝜑 → 𝐺 ∈ 𝐵 )
12 eqid ⊢ ( 𝐼 mPoly 𝑇 ) = ( 𝐼 mPoly 𝑇 )
13 eqid ⊢ ( Base ‘ ( 𝐼 mPoly 𝑇 ) ) = ( Base ‘ ( 𝐼 mPoly 𝑇 ) )
14 eqid ⊢ ( .r ‘ ( 𝐼 mPoly 𝑇 ) ) = ( .r ‘ ( 𝐼 mPoly 𝑇 ) )
15 eqid ⊢ ( algSc ‘ 𝑇 ) = ( algSc ‘ 𝑇 )
16 eqid ⊢ ( ( algSc ‘ 𝑇 ) ∘ ( algSc ‘ 𝑈 ) ) = ( ( algSc ‘ 𝑇 ) ∘ ( algSc ‘ 𝑈 ) )
17 7 difexd ⊢ ( 𝜑 → ( 𝐼 ∖ 𝐽 ) ∈ V )
18 7 9 ssexd ⊢ ( 𝜑 → 𝐽 ∈ V )
19 4 5 15 16 17 18 8 selvcllem2 ⊢ ( 𝜑 → ( ( algSc ‘ 𝑇 ) ∘ ( algSc ‘ 𝑈 ) ) ∈ ( 𝑅 RingHom 𝑇 ) )
20 1 12 2 13 3 14 19 10 11 rhmcomulmpl ⊢ ( 𝜑 → ( ( ( algSc ‘ 𝑇 ) ∘ ( algSc ‘ 𝑈 ) ) ∘ ( 𝐹 · 𝐺 ) ) = ( ( ( ( algSc ‘ 𝑇 ) ∘ ( algSc ‘ 𝑈 ) ) ∘ 𝐹 ) ( .r ‘ ( 𝐼 mPoly 𝑇 ) ) ( ( ( algSc ‘ 𝑇 ) ∘ ( algSc ‘ 𝑈 ) ) ∘ 𝐺 ) ) )
21 20 fveq2d ⊢ ( 𝜑 → ( ( 𝐼 eval 𝑇 ) ‘ ( ( ( algSc ‘ 𝑇 ) ∘ ( algSc ‘ 𝑈 ) ) ∘ ( 𝐹 · 𝐺 ) ) ) = ( ( 𝐼 eval 𝑇 ) ‘ ( ( ( ( algSc ‘ 𝑇 ) ∘ ( algSc ‘ 𝑈 ) ) ∘ 𝐹 ) ( .r ‘ ( 𝐼 mPoly 𝑇 ) ) ( ( ( algSc ‘ 𝑇 ) ∘ ( algSc ‘ 𝑈 ) ) ∘ 𝐺 ) ) ) )
22 21 fveq1d ⊢ ( 𝜑 → ( ( ( 𝐼 eval 𝑇 ) ‘ ( ( ( algSc ‘ 𝑇 ) ∘ ( algSc ‘ 𝑈 ) ) ∘ ( 𝐹 · 𝐺 ) ) ) ‘ ( 𝑥 ∈ 𝐼 ↦ if ( 𝑥 ∈ 𝐽 , ( ( 𝐽 mVar 𝑈 ) ‘ 𝑥 ) , ( ( algSc ‘ 𝑇 ) ‘ ( ( ( 𝐼 ∖ 𝐽 ) mVar 𝑅 ) ‘ 𝑥 ) ) ) ) ) = ( ( ( 𝐼 eval 𝑇 ) ‘ ( ( ( ( algSc ‘ 𝑇 ) ∘ ( algSc ‘ 𝑈 ) ) ∘ 𝐹 ) ( .r ‘ ( 𝐼 mPoly 𝑇 ) ) ( ( ( algSc ‘ 𝑇 ) ∘ ( algSc ‘ 𝑈 ) ) ∘ 𝐺 ) ) ) ‘ ( 𝑥 ∈ 𝐼 ↦ if ( 𝑥 ∈ 𝐽 , ( ( 𝐽 mVar 𝑈 ) ‘ 𝑥 ) , ( ( algSc ‘ 𝑇 ) ‘ ( ( ( 𝐼 ∖ 𝐽 ) mVar 𝑅 ) ‘ 𝑥 ) ) ) ) ) )
23 eqid ⊢ ( 𝐼 eval 𝑇 ) = ( 𝐼 eval 𝑇 )
24 eqid ⊢ ( Base ‘ 𝑇 ) = ( Base ‘ 𝑇 )
25 4 17 8 mplcrngd ⊢ ( 𝜑 → 𝑈 ∈ CRing )
26 5 18 25 mplcrngd ⊢ ( 𝜑 → 𝑇 ∈ CRing )
27 eqid ⊢ ( 𝑥 ∈ 𝐼 ↦ if ( 𝑥 ∈ 𝐽 , ( ( 𝐽 mVar 𝑈 ) ‘ 𝑥 ) , ( ( algSc ‘ 𝑇 ) ‘ ( ( ( 𝐼 ∖ 𝐽 ) mVar 𝑅 ) ‘ 𝑥 ) ) ) ) = ( 𝑥 ∈ 𝐼 ↦ if ( 𝑥 ∈ 𝐽 , ( ( 𝐽 mVar 𝑈 ) ‘ 𝑥 ) , ( ( algSc ‘ 𝑇 ) ‘ ( ( ( 𝐼 ∖ 𝐽 ) mVar 𝑅 ) ‘ 𝑥 ) ) ) )
28 4 5 15 24 27 7 8 9 selvcllem5 ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐼 ↦ if ( 𝑥 ∈ 𝐽 , ( ( 𝐽 mVar 𝑈 ) ‘ 𝑥 ) , ( ( algSc ‘ 𝑇 ) ‘ ( ( ( 𝐼 ∖ 𝐽 ) mVar 𝑅 ) ‘ 𝑥 ) ) ) ) ∈ ( ( Base ‘ 𝑇 ) ↑m 𝐼 ) )
29 rhmghm ⊢ ( ( ( algSc ‘ 𝑇 ) ∘ ( algSc ‘ 𝑈 ) ) ∈ ( 𝑅 RingHom 𝑇 ) → ( ( algSc ‘ 𝑇 ) ∘ ( algSc ‘ 𝑈 ) ) ∈ ( 𝑅 GrpHom 𝑇 ) )
30 ghmmhm ⊢ ( ( ( algSc ‘ 𝑇 ) ∘ ( algSc ‘ 𝑈 ) ) ∈ ( 𝑅 GrpHom 𝑇 ) → ( ( algSc ‘ 𝑇 ) ∘ ( algSc ‘ 𝑈 ) ) ∈ ( 𝑅 MndHom 𝑇 ) )
31 19 29 30 3syl ⊢ ( 𝜑 → ( ( algSc ‘ 𝑇 ) ∘ ( algSc ‘ 𝑈 ) ) ∈ ( 𝑅 MndHom 𝑇 ) )
32 1 12 2 13 31 10 mhmcompl ⊢ ( 𝜑 → ( ( ( algSc ‘ 𝑇 ) ∘ ( algSc ‘ 𝑈 ) ) ∘ 𝐹 ) ∈ ( Base ‘ ( 𝐼 mPoly 𝑇 ) ) )
33 eqidd ⊢ ( 𝜑 → ( ( ( 𝐼 eval 𝑇 ) ‘ ( ( ( algSc ‘ 𝑇 ) ∘ ( algSc ‘ 𝑈 ) ) ∘ 𝐹 ) ) ‘ ( 𝑥 ∈ 𝐼 ↦ if ( 𝑥 ∈ 𝐽 , ( ( 𝐽 mVar 𝑈 ) ‘ 𝑥 ) , ( ( algSc ‘ 𝑇 ) ‘ ( ( ( 𝐼 ∖ 𝐽 ) mVar 𝑅 ) ‘ 𝑥 ) ) ) ) ) = ( ( ( 𝐼 eval 𝑇 ) ‘ ( ( ( algSc ‘ 𝑇 ) ∘ ( algSc ‘ 𝑈 ) ) ∘ 𝐹 ) ) ‘ ( 𝑥 ∈ 𝐼 ↦ if ( 𝑥 ∈ 𝐽 , ( ( 𝐽 mVar 𝑈 ) ‘ 𝑥 ) , ( ( algSc ‘ 𝑇 ) ‘ ( ( ( 𝐼 ∖ 𝐽 ) mVar 𝑅 ) ‘ 𝑥 ) ) ) ) ) )
34 32 33 jca ⊢ ( 𝜑 → ( ( ( ( algSc ‘ 𝑇 ) ∘ ( algSc ‘ 𝑈 ) ) ∘ 𝐹 ) ∈ ( Base ‘ ( 𝐼 mPoly 𝑇 ) ) ∧ ( ( ( 𝐼 eval 𝑇 ) ‘ ( ( ( algSc ‘ 𝑇 ) ∘ ( algSc ‘ 𝑈 ) ) ∘ 𝐹 ) ) ‘ ( 𝑥 ∈ 𝐼 ↦ if ( 𝑥 ∈ 𝐽 , ( ( 𝐽 mVar 𝑈 ) ‘ 𝑥 ) , ( ( algSc ‘ 𝑇 ) ‘ ( ( ( 𝐼 ∖ 𝐽 ) mVar 𝑅 ) ‘ 𝑥 ) ) ) ) ) = ( ( ( 𝐼 eval 𝑇 ) ‘ ( ( ( algSc ‘ 𝑇 ) ∘ ( algSc ‘ 𝑈 ) ) ∘ 𝐹 ) ) ‘ ( 𝑥 ∈ 𝐼 ↦ if ( 𝑥 ∈ 𝐽 , ( ( 𝐽 mVar 𝑈 ) ‘ 𝑥 ) , ( ( algSc ‘ 𝑇 ) ‘ ( ( ( 𝐼 ∖ 𝐽 ) mVar 𝑅 ) ‘ 𝑥 ) ) ) ) ) ) )
35 1 12 2 13 31 11 mhmcompl ⊢ ( 𝜑 → ( ( ( algSc ‘ 𝑇 ) ∘ ( algSc ‘ 𝑈 ) ) ∘ 𝐺 ) ∈ ( Base ‘ ( 𝐼 mPoly 𝑇 ) ) )
36 eqidd ⊢ ( 𝜑 → ( ( ( 𝐼 eval 𝑇 ) ‘ ( ( ( algSc ‘ 𝑇 ) ∘ ( algSc ‘ 𝑈 ) ) ∘ 𝐺 ) ) ‘ ( 𝑥 ∈ 𝐼 ↦ if ( 𝑥 ∈ 𝐽 , ( ( 𝐽 mVar 𝑈 ) ‘ 𝑥 ) , ( ( algSc ‘ 𝑇 ) ‘ ( ( ( 𝐼 ∖ 𝐽 ) mVar 𝑅 ) ‘ 𝑥 ) ) ) ) ) = ( ( ( 𝐼 eval 𝑇 ) ‘ ( ( ( algSc ‘ 𝑇 ) ∘ ( algSc ‘ 𝑈 ) ) ∘ 𝐺 ) ) ‘ ( 𝑥 ∈ 𝐼 ↦ if ( 𝑥 ∈ 𝐽 , ( ( 𝐽 mVar 𝑈 ) ‘ 𝑥 ) , ( ( algSc ‘ 𝑇 ) ‘ ( ( ( 𝐼 ∖ 𝐽 ) mVar 𝑅 ) ‘ 𝑥 ) ) ) ) ) )
37 35 36 jca ⊢ ( 𝜑 → ( ( ( ( algSc ‘ 𝑇 ) ∘ ( algSc ‘ 𝑈 ) ) ∘ 𝐺 ) ∈ ( Base ‘ ( 𝐼 mPoly 𝑇 ) ) ∧ ( ( ( 𝐼 eval 𝑇 ) ‘ ( ( ( algSc ‘ 𝑇 ) ∘ ( algSc ‘ 𝑈 ) ) ∘ 𝐺 ) ) ‘ ( 𝑥 ∈ 𝐼 ↦ if ( 𝑥 ∈ 𝐽 , ( ( 𝐽 mVar 𝑈 ) ‘ 𝑥 ) , ( ( algSc ‘ 𝑇 ) ‘ ( ( ( 𝐼 ∖ 𝐽 ) mVar 𝑅 ) ‘ 𝑥 ) ) ) ) ) = ( ( ( 𝐼 eval 𝑇 ) ‘ ( ( ( algSc ‘ 𝑇 ) ∘ ( algSc ‘ 𝑈 ) ) ∘ 𝐺 ) ) ‘ ( 𝑥 ∈ 𝐼 ↦ if ( 𝑥 ∈ 𝐽 , ( ( 𝐽 mVar 𝑈 ) ‘ 𝑥 ) , ( ( algSc ‘ 𝑇 ) ‘ ( ( ( 𝐼 ∖ 𝐽 ) mVar 𝑅 ) ‘ 𝑥 ) ) ) ) ) ) )
38 23 12 24 13 14 6 7 26 28 34 37 evlmulval ⊢ ( 𝜑 → ( ( ( ( ( algSc ‘ 𝑇 ) ∘ ( algSc ‘ 𝑈 ) ) ∘ 𝐹 ) ( .r ‘ ( 𝐼 mPoly 𝑇 ) ) ( ( ( algSc ‘ 𝑇 ) ∘ ( algSc ‘ 𝑈 ) ) ∘ 𝐺 ) ) ∈ ( Base ‘ ( 𝐼 mPoly 𝑇 ) ) ∧ ( ( ( 𝐼 eval 𝑇 ) ‘ ( ( ( ( algSc ‘ 𝑇 ) ∘ ( algSc ‘ 𝑈 ) ) ∘ 𝐹 ) ( .r ‘ ( 𝐼 mPoly 𝑇 ) ) ( ( ( algSc ‘ 𝑇 ) ∘ ( algSc ‘ 𝑈 ) ) ∘ 𝐺 ) ) ) ‘ ( 𝑥 ∈ 𝐼 ↦ if ( 𝑥 ∈ 𝐽 , ( ( 𝐽 mVar 𝑈 ) ‘ 𝑥 ) , ( ( algSc ‘ 𝑇 ) ‘ ( ( ( 𝐼 ∖ 𝐽 ) mVar 𝑅 ) ‘ 𝑥 ) ) ) ) ) = ( ( ( ( 𝐼 eval 𝑇 ) ‘ ( ( ( algSc ‘ 𝑇 ) ∘ ( algSc ‘ 𝑈 ) ) ∘ 𝐹 ) ) ‘ ( 𝑥 ∈ 𝐼 ↦ if ( 𝑥 ∈ 𝐽 , ( ( 𝐽 mVar 𝑈 ) ‘ 𝑥 ) , ( ( algSc ‘ 𝑇 ) ‘ ( ( ( 𝐼 ∖ 𝐽 ) mVar 𝑅 ) ‘ 𝑥 ) ) ) ) ) ∙ ( ( ( 𝐼 eval 𝑇 ) ‘ ( ( ( algSc ‘ 𝑇 ) ∘ ( algSc ‘ 𝑈 ) ) ∘ 𝐺 ) ) ‘ ( 𝑥 ∈ 𝐼 ↦ if ( 𝑥 ∈ 𝐽 , ( ( 𝐽 mVar 𝑈 ) ‘ 𝑥 ) , ( ( algSc ‘ 𝑇 ) ‘ ( ( ( 𝐼 ∖ 𝐽 ) mVar 𝑅 ) ‘ 𝑥 ) ) ) ) ) ) ) )
39 38 simprd ⊢ ( 𝜑 → ( ( ( 𝐼 eval 𝑇 ) ‘ ( ( ( ( algSc ‘ 𝑇 ) ∘ ( algSc ‘ 𝑈 ) ) ∘ 𝐹 ) ( .r ‘ ( 𝐼 mPoly 𝑇 ) ) ( ( ( algSc ‘ 𝑇 ) ∘ ( algSc ‘ 𝑈 ) ) ∘ 𝐺 ) ) ) ‘ ( 𝑥 ∈ 𝐼 ↦ if ( 𝑥 ∈ 𝐽 , ( ( 𝐽 mVar 𝑈 ) ‘ 𝑥 ) , ( ( algSc ‘ 𝑇 ) ‘ ( ( ( 𝐼 ∖ 𝐽 ) mVar 𝑅 ) ‘ 𝑥 ) ) ) ) ) = ( ( ( ( 𝐼 eval 𝑇 ) ‘ ( ( ( algSc ‘ 𝑇 ) ∘ ( algSc ‘ 𝑈 ) ) ∘ 𝐹 ) ) ‘ ( 𝑥 ∈ 𝐼 ↦ if ( 𝑥 ∈ 𝐽 , ( ( 𝐽 mVar 𝑈 ) ‘ 𝑥 ) , ( ( algSc ‘ 𝑇 ) ‘ ( ( ( 𝐼 ∖ 𝐽 ) mVar 𝑅 ) ‘ 𝑥 ) ) ) ) ) ∙ ( ( ( 𝐼 eval 𝑇 ) ‘ ( ( ( algSc ‘ 𝑇 ) ∘ ( algSc ‘ 𝑈 ) ) ∘ 𝐺 ) ) ‘ ( 𝑥 ∈ 𝐼 ↦ if ( 𝑥 ∈ 𝐽 , ( ( 𝐽 mVar 𝑈 ) ‘ 𝑥 ) , ( ( algSc ‘ 𝑇 ) ‘ ( ( ( 𝐼 ∖ 𝐽 ) mVar 𝑅 ) ‘ 𝑥 ) ) ) ) ) ) )
40 22 39 eqtrd ⊢ ( 𝜑 → ( ( ( 𝐼 eval 𝑇 ) ‘ ( ( ( algSc ‘ 𝑇 ) ∘ ( algSc ‘ 𝑈 ) ) ∘ ( 𝐹 · 𝐺 ) ) ) ‘ ( 𝑥 ∈ 𝐼 ↦ if ( 𝑥 ∈ 𝐽 , ( ( 𝐽 mVar 𝑈 ) ‘ 𝑥 ) , ( ( algSc ‘ 𝑇 ) ‘ ( ( ( 𝐼 ∖ 𝐽 ) mVar 𝑅 ) ‘ 𝑥 ) ) ) ) ) = ( ( ( ( 𝐼 eval 𝑇 ) ‘ ( ( ( algSc ‘ 𝑇 ) ∘ ( algSc ‘ 𝑈 ) ) ∘ 𝐹 ) ) ‘ ( 𝑥 ∈ 𝐼 ↦ if ( 𝑥 ∈ 𝐽 , ( ( 𝐽 mVar 𝑈 ) ‘ 𝑥 ) , ( ( algSc ‘ 𝑇 ) ‘ ( ( ( 𝐼 ∖ 𝐽 ) mVar 𝑅 ) ‘ 𝑥 ) ) ) ) ) ∙ ( ( ( 𝐼 eval 𝑇 ) ‘ ( ( ( algSc ‘ 𝑇 ) ∘ ( algSc ‘ 𝑈 ) ) ∘ 𝐺 ) ) ‘ ( 𝑥 ∈ 𝐼 ↦ if ( 𝑥 ∈ 𝐽 , ( ( 𝐽 mVar 𝑈 ) ‘ 𝑥 ) , ( ( algSc ‘ 𝑇 ) ‘ ( ( ( 𝐼 ∖ 𝐽 ) mVar 𝑅 ) ‘ 𝑥 ) ) ) ) ) ) )
41 1 7 8 mplcrngd ⊢ ( 𝜑 → 𝑃 ∈ CRing )
42 41 crngringd ⊢ ( 𝜑 → 𝑃 ∈ Ring )
43 2 3 42 10 11 ringcld ⊢ ( 𝜑 → ( 𝐹 · 𝐺 ) ∈ 𝐵 )
44 1 2 4 5 15 16 8 9 43 selvval2 ⊢ ( 𝜑 → ( ( ( 𝐼 selectVars 𝑅 ) ‘ 𝐽 ) ‘ ( 𝐹 · 𝐺 ) ) = ( ( ( 𝐼 eval 𝑇 ) ‘ ( ( ( algSc ‘ 𝑇 ) ∘ ( algSc ‘ 𝑈 ) ) ∘ ( 𝐹 · 𝐺 ) ) ) ‘ ( 𝑥 ∈ 𝐼 ↦ if ( 𝑥 ∈ 𝐽 , ( ( 𝐽 mVar 𝑈 ) ‘ 𝑥 ) , ( ( algSc ‘ 𝑇 ) ‘ ( ( ( 𝐼 ∖ 𝐽 ) mVar 𝑅 ) ‘ 𝑥 ) ) ) ) ) )
45 1 2 4 5 15 16 8 9 10 selvval2 ⊢ ( 𝜑 → ( ( ( 𝐼 selectVars 𝑅 ) ‘ 𝐽 ) ‘ 𝐹 ) = ( ( ( 𝐼 eval 𝑇 ) ‘ ( ( ( algSc ‘ 𝑇 ) ∘ ( algSc ‘ 𝑈 ) ) ∘ 𝐹 ) ) ‘ ( 𝑥 ∈ 𝐼 ↦ if ( 𝑥 ∈ 𝐽 , ( ( 𝐽 mVar 𝑈 ) ‘ 𝑥 ) , ( ( algSc ‘ 𝑇 ) ‘ ( ( ( 𝐼 ∖ 𝐽 ) mVar 𝑅 ) ‘ 𝑥 ) ) ) ) ) )
46 1 2 4 5 15 16 8 9 11 selvval2 ⊢ ( 𝜑 → ( ( ( 𝐼 selectVars 𝑅 ) ‘ 𝐽 ) ‘ 𝐺 ) = ( ( ( 𝐼 eval 𝑇 ) ‘ ( ( ( algSc ‘ 𝑇 ) ∘ ( algSc ‘ 𝑈 ) ) ∘ 𝐺 ) ) ‘ ( 𝑥 ∈ 𝐼 ↦ if ( 𝑥 ∈ 𝐽 , ( ( 𝐽 mVar 𝑈 ) ‘ 𝑥 ) , ( ( algSc ‘ 𝑇 ) ‘ ( ( ( 𝐼 ∖ 𝐽 ) mVar 𝑅 ) ‘ 𝑥 ) ) ) ) ) )
47 45 46 oveq12d ⊢ ( 𝜑 → ( ( ( ( 𝐼 selectVars 𝑅 ) ‘ 𝐽 ) ‘ 𝐹 ) ∙ ( ( ( 𝐼 selectVars 𝑅 ) ‘ 𝐽 ) ‘ 𝐺 ) ) = ( ( ( ( 𝐼 eval 𝑇 ) ‘ ( ( ( algSc ‘ 𝑇 ) ∘ ( algSc ‘ 𝑈 ) ) ∘ 𝐹 ) ) ‘ ( 𝑥 ∈ 𝐼 ↦ if ( 𝑥 ∈ 𝐽 , ( ( 𝐽 mVar 𝑈 ) ‘ 𝑥 ) , ( ( algSc ‘ 𝑇 ) ‘ ( ( ( 𝐼 ∖ 𝐽 ) mVar 𝑅 ) ‘ 𝑥 ) ) ) ) ) ∙ ( ( ( 𝐼 eval 𝑇 ) ‘ ( ( ( algSc ‘ 𝑇 ) ∘ ( algSc ‘ 𝑈 ) ) ∘ 𝐺 ) ) ‘ ( 𝑥 ∈ 𝐼 ↦ if ( 𝑥 ∈ 𝐽 , ( ( 𝐽 mVar 𝑈 ) ‘ 𝑥 ) , ( ( algSc ‘ 𝑇 ) ‘ ( ( ( 𝐼 ∖ 𝐽 ) mVar 𝑅 ) ‘ 𝑥 ) ) ) ) ) ) )
48 40 44 47 3eqtr4d ⊢ ( 𝜑 → ( ( ( 𝐼 selectVars 𝑅 ) ‘ 𝐽 ) ‘ ( 𝐹 · 𝐺 ) ) = ( ( ( ( 𝐼 selectVars 𝑅 ) ‘ 𝐽 ) ‘ 𝐹 ) ∙ ( ( ( 𝐼 selectVars 𝑅 ) ‘ 𝐽 ) ‘ 𝐺 ) ) )