Metamath Proof Explorer

Theorem selvadd

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

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

Proof

Step Hyp Ref Expression
1 selvadd.p ⊢ 𝑃 = ( 𝐼 mPoly 𝑅 )
2 selvadd.b ⊢ 𝐵 = ( Base ‘ 𝑃 )
3 selvadd.1 ⊢ + = ( +g ‘ 𝑃 )
4 selvadd.u ⊢ 𝑈 = ( ( 𝐼 ∖ 𝐽 ) mPoly 𝑅 )
5 selvadd.t ⊢ 𝑇 = ( 𝐽 mPoly 𝑈 )
6 selvadd.2 ⊢ ✚ = ( +g ‘ 𝑇 )
7 selvadd.i ⊢ ( 𝜑 → 𝐼 ∈ 𝑉 )
8 selvadd.r ⊢ ( 𝜑 → 𝑅 ∈ CRing )
9 selvadd.j ⊢ ( 𝜑 → 𝐽 ⊆ 𝐼 )
10 selvadd.f ⊢ ( 𝜑 → 𝐹 ∈ 𝐵 )
11 selvadd.g ⊢ ( 𝜑 → 𝐺 ∈ 𝐵 )
12 eqid ⊢ ( 𝐼 mPoly 𝑇 ) = ( 𝐼 mPoly 𝑇 )
13 eqid ⊢ ( Base ‘ ( 𝐼 mPoly 𝑇 ) ) = ( Base ‘ ( 𝐼 mPoly 𝑇 ) )
14 eqid ⊢ ( +g ‘ ( 𝐼 mPoly 𝑇 ) ) = ( +g ‘ ( 𝐼 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 rhmghm ⊢ ( ( ( algSc ‘ 𝑇 ) ∘ ( algSc ‘ 𝑈 ) ) ∈ ( 𝑅 RingHom 𝑇 ) → ( ( algSc ‘ 𝑇 ) ∘ ( algSc ‘ 𝑈 ) ) ∈ ( 𝑅 GrpHom 𝑇 ) )
21 ghmmhm ⊢ ( ( ( algSc ‘ 𝑇 ) ∘ ( algSc ‘ 𝑈 ) ) ∈ ( 𝑅 GrpHom 𝑇 ) → ( ( algSc ‘ 𝑇 ) ∘ ( algSc ‘ 𝑈 ) ) ∈ ( 𝑅 MndHom 𝑇 ) )
22 19 20 21 3syl ⊢ ( 𝜑 → ( ( algSc ‘ 𝑇 ) ∘ ( algSc ‘ 𝑈 ) ) ∈ ( 𝑅 MndHom 𝑇 ) )
23 1 12 2 13 3 14 22 10 11 mhmcoaddmpl ⊢ ( 𝜑 → ( ( ( algSc ‘ 𝑇 ) ∘ ( algSc ‘ 𝑈 ) ) ∘ ( 𝐹 + 𝐺 ) ) = ( ( ( ( algSc ‘ 𝑇 ) ∘ ( algSc ‘ 𝑈 ) ) ∘ 𝐹 ) ( +g ‘ ( 𝐼 mPoly 𝑇 ) ) ( ( ( algSc ‘ 𝑇 ) ∘ ( algSc ‘ 𝑈 ) ) ∘ 𝐺 ) ) )
24 23 fveq2d ⊢ ( 𝜑 → ( ( 𝐼 eval 𝑇 ) ‘ ( ( ( algSc ‘ 𝑇 ) ∘ ( algSc ‘ 𝑈 ) ) ∘ ( 𝐹 + 𝐺 ) ) ) = ( ( 𝐼 eval 𝑇 ) ‘ ( ( ( ( algSc ‘ 𝑇 ) ∘ ( algSc ‘ 𝑈 ) ) ∘ 𝐹 ) ( +g ‘ ( 𝐼 mPoly 𝑇 ) ) ( ( ( algSc ‘ 𝑇 ) ∘ ( algSc ‘ 𝑈 ) ) ∘ 𝐺 ) ) ) )
25 24 fveq1d ⊢ ( 𝜑 → ( ( ( 𝐼 eval 𝑇 ) ‘ ( ( ( algSc ‘ 𝑇 ) ∘ ( algSc ‘ 𝑈 ) ) ∘ ( 𝐹 + 𝐺 ) ) ) ‘ ( 𝑥 ∈ 𝐼 ↦ if ( 𝑥 ∈ 𝐽 , ( ( 𝐽 mVar 𝑈 ) ‘ 𝑥 ) , ( ( algSc ‘ 𝑇 ) ‘ ( ( ( 𝐼 ∖ 𝐽 ) mVar 𝑅 ) ‘ 𝑥 ) ) ) ) ) = ( ( ( 𝐼 eval 𝑇 ) ‘ ( ( ( ( algSc ‘ 𝑇 ) ∘ ( algSc ‘ 𝑈 ) ) ∘ 𝐹 ) ( +g ‘ ( 𝐼 mPoly 𝑇 ) ) ( ( ( algSc ‘ 𝑇 ) ∘ ( algSc ‘ 𝑈 ) ) ∘ 𝐺 ) ) ) ‘ ( 𝑥 ∈ 𝐼 ↦ if ( 𝑥 ∈ 𝐽 , ( ( 𝐽 mVar 𝑈 ) ‘ 𝑥 ) , ( ( algSc ‘ 𝑇 ) ‘ ( ( ( 𝐼 ∖ 𝐽 ) mVar 𝑅 ) ‘ 𝑥 ) ) ) ) ) )
26 eqid ⊢ ( 𝐼 eval 𝑇 ) = ( 𝐼 eval 𝑇 )
27 eqid ⊢ ( Base ‘ 𝑇 ) = ( Base ‘ 𝑇 )
28 4 17 8 mplcrngd ⊢ ( 𝜑 → 𝑈 ∈ CRing )
29 5 18 28 mplcrngd ⊢ ( 𝜑 → 𝑇 ∈ CRing )
30 eqid ⊢ ( 𝑥 ∈ 𝐼 ↦ if ( 𝑥 ∈ 𝐽 , ( ( 𝐽 mVar 𝑈 ) ‘ 𝑥 ) , ( ( algSc ‘ 𝑇 ) ‘ ( ( ( 𝐼 ∖ 𝐽 ) mVar 𝑅 ) ‘ 𝑥 ) ) ) ) = ( 𝑥 ∈ 𝐼 ↦ if ( 𝑥 ∈ 𝐽 , ( ( 𝐽 mVar 𝑈 ) ‘ 𝑥 ) , ( ( algSc ‘ 𝑇 ) ‘ ( ( ( 𝐼 ∖ 𝐽 ) mVar 𝑅 ) ‘ 𝑥 ) ) ) )
31 4 5 15 27 30 7 8 9 selvcllem5 ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐼 ↦ if ( 𝑥 ∈ 𝐽 , ( ( 𝐽 mVar 𝑈 ) ‘ 𝑥 ) , ( ( algSc ‘ 𝑇 ) ‘ ( ( ( 𝐼 ∖ 𝐽 ) mVar 𝑅 ) ‘ 𝑥 ) ) ) ) ∈ ( ( Base ‘ 𝑇 ) ↑m 𝐼 ) )
32 1 12 2 13 22 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 22 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 26 12 27 13 14 6 7 29 31 34 37 evladdval ⊢ ( 𝜑 → ( ( ( ( ( algSc ‘ 𝑇 ) ∘ ( algSc ‘ 𝑈 ) ) ∘ 𝐹 ) ( +g ‘ ( 𝐼 mPoly 𝑇 ) ) ( ( ( algSc ‘ 𝑇 ) ∘ ( algSc ‘ 𝑈 ) ) ∘ 𝐺 ) ) ∈ ( Base ‘ ( 𝐼 mPoly 𝑇 ) ) ∧ ( ( ( 𝐼 eval 𝑇 ) ‘ ( ( ( ( algSc ‘ 𝑇 ) ∘ ( algSc ‘ 𝑈 ) ) ∘ 𝐹 ) ( +g ‘ ( 𝐼 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 ‘ 𝑈 ) ) ∘ 𝐹 ) ( +g ‘ ( 𝐼 mPoly 𝑇 ) ) ( ( ( algSc ‘ 𝑇 ) ∘ ( algSc ‘ 𝑈 ) ) ∘ 𝐺 ) ) ) ‘ ( 𝑥 ∈ 𝐼 ↦ if ( 𝑥 ∈ 𝐽 , ( ( 𝐽 mVar 𝑈 ) ‘ 𝑥 ) , ( ( algSc ‘ 𝑇 ) ‘ ( ( ( 𝐼 ∖ 𝐽 ) mVar 𝑅 ) ‘ 𝑥 ) ) ) ) ) = ( ( ( ( 𝐼 eval 𝑇 ) ‘ ( ( ( algSc ‘ 𝑇 ) ∘ ( algSc ‘ 𝑈 ) ) ∘ 𝐹 ) ) ‘ ( 𝑥 ∈ 𝐼 ↦ if ( 𝑥 ∈ 𝐽 , ( ( 𝐽 mVar 𝑈 ) ‘ 𝑥 ) , ( ( algSc ‘ 𝑇 ) ‘ ( ( ( 𝐼 ∖ 𝐽 ) mVar 𝑅 ) ‘ 𝑥 ) ) ) ) ) ✚ ( ( ( 𝐼 eval 𝑇 ) ‘ ( ( ( algSc ‘ 𝑇 ) ∘ ( algSc ‘ 𝑈 ) ) ∘ 𝐺 ) ) ‘ ( 𝑥 ∈ 𝐼 ↦ if ( 𝑥 ∈ 𝐽 , ( ( 𝐽 mVar 𝑈 ) ‘ 𝑥 ) , ( ( algSc ‘ 𝑇 ) ‘ ( ( ( 𝐼 ∖ 𝐽 ) mVar 𝑅 ) ‘ 𝑥 ) ) ) ) ) ) )
40 25 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 crnggrpd ⊢ ( 𝜑 → 𝑃 ∈ Grp )
43 2 3 42 10 11 grpcld ⊢ ( 𝜑 → ( 𝐹 + 𝐺 ) ∈ 𝐵 )
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 𝑅 ) ‘ 𝐽 ) ‘ 𝐺 ) ) )