Step | Hyp | Ref
| Expression |
1 | | selvadd.p |
. . . . . 6
⊢ 𝑃 = (𝐼 mPoly 𝑅) |
2 | | eqid 2740 |
. . . . . 6
⊢ (𝐼 mPoly 𝑇) = (𝐼 mPoly 𝑇) |
3 | | selvadd.b |
. . . . . 6
⊢ 𝐵 = (Base‘𝑃) |
4 | | eqid 2740 |
. . . . . 6
⊢
(Base‘(𝐼 mPoly
𝑇)) = (Base‘(𝐼 mPoly 𝑇)) |
5 | | selvadd.1 |
. . . . . 6
⊢ + =
(+g‘𝑃) |
6 | | eqid 2740 |
. . . . . 6
⊢
(+g‘(𝐼 mPoly 𝑇)) = (+g‘(𝐼 mPoly 𝑇)) |
7 | | selvadd.u |
. . . . . . . 8
⊢ 𝑈 = ((𝐼 ∖ 𝐽) mPoly 𝑅) |
8 | | selvadd.t |
. . . . . . . 8
⊢ 𝑇 = (𝐽 mPoly 𝑈) |
9 | | eqid 2740 |
. . . . . . . 8
⊢
(algSc‘𝑇) =
(algSc‘𝑇) |
10 | | eqid 2740 |
. . . . . . . 8
⊢
((algSc‘𝑇)
∘ (algSc‘𝑈)) =
((algSc‘𝑇) ∘
(algSc‘𝑈)) |
11 | | selvadd.i |
. . . . . . . . 9
⊢ (𝜑 → 𝐼 ∈ 𝑉) |
12 | 11 | difexd 5349 |
. . . . . . . 8
⊢ (𝜑 → (𝐼 ∖ 𝐽) ∈ V) |
13 | | selvadd.j |
. . . . . . . . 9
⊢ (𝜑 → 𝐽 ⊆ 𝐼) |
14 | 11, 13 | ssexd 5342 |
. . . . . . . 8
⊢ (𝜑 → 𝐽 ∈ V) |
15 | | selvadd.r |
. . . . . . . 8
⊢ (𝜑 → 𝑅 ∈ CRing) |
16 | 7, 8, 9, 10, 12, 14, 15 | selvcllem2 42533 |
. . . . . . 7
⊢ (𝜑 → ((algSc‘𝑇) ∘ (algSc‘𝑈)) ∈ (𝑅 RingHom 𝑇)) |
17 | | rhmghm 20510 |
. . . . . . 7
⊢
(((algSc‘𝑇)
∘ (algSc‘𝑈))
∈ (𝑅 RingHom 𝑇) → ((algSc‘𝑇) ∘ (algSc‘𝑈)) ∈ (𝑅 GrpHom 𝑇)) |
18 | | ghmmhm 19266 |
. . . . . . 7
⊢
(((algSc‘𝑇)
∘ (algSc‘𝑈))
∈ (𝑅 GrpHom 𝑇) → ((algSc‘𝑇) ∘ (algSc‘𝑈)) ∈ (𝑅 MndHom 𝑇)) |
19 | 16, 17, 18 | 3syl 18 |
. . . . . 6
⊢ (𝜑 → ((algSc‘𝑇) ∘ (algSc‘𝑈)) ∈ (𝑅 MndHom 𝑇)) |
20 | | selvadd.f |
. . . . . 6
⊢ (𝜑 → 𝐹 ∈ 𝐵) |
21 | | selvadd.g |
. . . . . 6
⊢ (𝜑 → 𝐺 ∈ 𝐵) |
22 | 1, 2, 3, 4, 5, 6, 19, 20, 21 | mhmcoaddmpl 22406 |
. . . . 5
⊢ (𝜑 → (((algSc‘𝑇) ∘ (algSc‘𝑈)) ∘ (𝐹 + 𝐺)) = ((((algSc‘𝑇) ∘ (algSc‘𝑈)) ∘ 𝐹)(+g‘(𝐼 mPoly 𝑇))(((algSc‘𝑇) ∘ (algSc‘𝑈)) ∘ 𝐺))) |
23 | 22 | fveq2d 6924 |
. . . 4
⊢ (𝜑 → ((𝐼 eval 𝑇)‘(((algSc‘𝑇) ∘ (algSc‘𝑈)) ∘ (𝐹 + 𝐺))) = ((𝐼 eval 𝑇)‘((((algSc‘𝑇) ∘ (algSc‘𝑈)) ∘ 𝐹)(+g‘(𝐼 mPoly 𝑇))(((algSc‘𝑇) ∘ (algSc‘𝑈)) ∘ 𝐺)))) |
24 | 23 | fveq1d 6922 |
. . 3
⊢ (𝜑 → (((𝐼 eval 𝑇)‘(((algSc‘𝑇) ∘ (algSc‘𝑈)) ∘ (𝐹 + 𝐺)))‘(𝑥 ∈ 𝐼 ↦ if(𝑥 ∈ 𝐽, ((𝐽 mVar 𝑈)‘𝑥), ((algSc‘𝑇)‘(((𝐼 ∖ 𝐽) mVar 𝑅)‘𝑥))))) = (((𝐼 eval 𝑇)‘((((algSc‘𝑇) ∘ (algSc‘𝑈)) ∘ 𝐹)(+g‘(𝐼 mPoly 𝑇))(((algSc‘𝑇) ∘ (algSc‘𝑈)) ∘ 𝐺)))‘(𝑥 ∈ 𝐼 ↦ if(𝑥 ∈ 𝐽, ((𝐽 mVar 𝑈)‘𝑥), ((algSc‘𝑇)‘(((𝐼 ∖ 𝐽) mVar 𝑅)‘𝑥)))))) |
25 | | eqid 2740 |
. . . . 5
⊢ (𝐼 eval 𝑇) = (𝐼 eval 𝑇) |
26 | | eqid 2740 |
. . . . 5
⊢
(Base‘𝑇) =
(Base‘𝑇) |
27 | | selvadd.2 |
. . . . 5
⊢ ✚ =
(+g‘𝑇) |
28 | 7, 12, 15 | mplcrngd 42502 |
. . . . . 6
⊢ (𝜑 → 𝑈 ∈ CRing) |
29 | 8, 14, 28 | mplcrngd 42502 |
. . . . 5
⊢ (𝜑 → 𝑇 ∈ CRing) |
30 | | eqid 2740 |
. . . . . 6
⊢ (𝑥 ∈ 𝐼 ↦ if(𝑥 ∈ 𝐽, ((𝐽 mVar 𝑈)‘𝑥), ((algSc‘𝑇)‘(((𝐼 ∖ 𝐽) mVar 𝑅)‘𝑥)))) = (𝑥 ∈ 𝐼 ↦ if(𝑥 ∈ 𝐽, ((𝐽 mVar 𝑈)‘𝑥), ((algSc‘𝑇)‘(((𝐼 ∖ 𝐽) mVar 𝑅)‘𝑥)))) |
31 | 7, 8, 9, 26, 30, 11, 15, 13 | selvcllem5 42537 |
. . . . 5
⊢ (𝜑 → (𝑥 ∈ 𝐼 ↦ if(𝑥 ∈ 𝐽, ((𝐽 mVar 𝑈)‘𝑥), ((algSc‘𝑇)‘(((𝐼 ∖ 𝐽) mVar 𝑅)‘𝑥)))) ∈ ((Base‘𝑇) ↑m 𝐼)) |
32 | 1, 2, 3, 4, 19, 20 | mhmcompl 22405 |
. . . . . 6
⊢ (𝜑 → (((algSc‘𝑇) ∘ (algSc‘𝑈)) ∘ 𝐹) ∈ (Base‘(𝐼 mPoly 𝑇))) |
33 | | eqidd 2741 |
. . . . . 6
⊢ (𝜑 → (((𝐼 eval 𝑇)‘(((algSc‘𝑇) ∘ (algSc‘𝑈)) ∘ 𝐹))‘(𝑥 ∈ 𝐼 ↦ if(𝑥 ∈ 𝐽, ((𝐽 mVar 𝑈)‘𝑥), ((algSc‘𝑇)‘(((𝐼 ∖ 𝐽) mVar 𝑅)‘𝑥))))) = (((𝐼 eval 𝑇)‘(((algSc‘𝑇) ∘ (algSc‘𝑈)) ∘ 𝐹))‘(𝑥 ∈ 𝐼 ↦ if(𝑥 ∈ 𝐽, ((𝐽 mVar 𝑈)‘𝑥), ((algSc‘𝑇)‘(((𝐼 ∖ 𝐽) mVar 𝑅)‘𝑥)))))) |
34 | 32, 33 | jca 511 |
. . . . 5
⊢ (𝜑 → ((((algSc‘𝑇) ∘ (algSc‘𝑈)) ∘ 𝐹) ∈ (Base‘(𝐼 mPoly 𝑇)) ∧ (((𝐼 eval 𝑇)‘(((algSc‘𝑇) ∘ (algSc‘𝑈)) ∘ 𝐹))‘(𝑥 ∈ 𝐼 ↦ if(𝑥 ∈ 𝐽, ((𝐽 mVar 𝑈)‘𝑥), ((algSc‘𝑇)‘(((𝐼 ∖ 𝐽) mVar 𝑅)‘𝑥))))) = (((𝐼 eval 𝑇)‘(((algSc‘𝑇) ∘ (algSc‘𝑈)) ∘ 𝐹))‘(𝑥 ∈ 𝐼 ↦ if(𝑥 ∈ 𝐽, ((𝐽 mVar 𝑈)‘𝑥), ((algSc‘𝑇)‘(((𝐼 ∖ 𝐽) mVar 𝑅)‘𝑥))))))) |
35 | 1, 2, 3, 4, 19, 21 | mhmcompl 22405 |
. . . . . 6
⊢ (𝜑 → (((algSc‘𝑇) ∘ (algSc‘𝑈)) ∘ 𝐺) ∈ (Base‘(𝐼 mPoly 𝑇))) |
36 | | eqidd 2741 |
. . . . . 6
⊢ (𝜑 → (((𝐼 eval 𝑇)‘(((algSc‘𝑇) ∘ (algSc‘𝑈)) ∘ 𝐺))‘(𝑥 ∈ 𝐼 ↦ if(𝑥 ∈ 𝐽, ((𝐽 mVar 𝑈)‘𝑥), ((algSc‘𝑇)‘(((𝐼 ∖ 𝐽) mVar 𝑅)‘𝑥))))) = (((𝐼 eval 𝑇)‘(((algSc‘𝑇) ∘ (algSc‘𝑈)) ∘ 𝐺))‘(𝑥 ∈ 𝐼 ↦ if(𝑥 ∈ 𝐽, ((𝐽 mVar 𝑈)‘𝑥), ((algSc‘𝑇)‘(((𝐼 ∖ 𝐽) mVar 𝑅)‘𝑥)))))) |
37 | 35, 36 | jca 511 |
. . . . 5
⊢ (𝜑 → ((((algSc‘𝑇) ∘ (algSc‘𝑈)) ∘ 𝐺) ∈ (Base‘(𝐼 mPoly 𝑇)) ∧ (((𝐼 eval 𝑇)‘(((algSc‘𝑇) ∘ (algSc‘𝑈)) ∘ 𝐺))‘(𝑥 ∈ 𝐼 ↦ if(𝑥 ∈ 𝐽, ((𝐽 mVar 𝑈)‘𝑥), ((algSc‘𝑇)‘(((𝐼 ∖ 𝐽) mVar 𝑅)‘𝑥))))) = (((𝐼 eval 𝑇)‘(((algSc‘𝑇) ∘ (algSc‘𝑈)) ∘ 𝐺))‘(𝑥 ∈ 𝐼 ↦ if(𝑥 ∈ 𝐽, ((𝐽 mVar 𝑈)‘𝑥), ((algSc‘𝑇)‘(((𝐼 ∖ 𝐽) mVar 𝑅)‘𝑥))))))) |
38 | 25, 2, 26, 4, 6, 27, 11, 29, 31, 34, 37 | evladdval 42530 |
. . . 4
⊢ (𝜑 → (((((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 495 |
. . 3
⊢ (𝜑 → (((𝐼 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 | 24, 39 | eqtrd 2780 |
. 2
⊢ (𝜑 → (((𝐼 eval 𝑇)‘(((algSc‘𝑇) ∘ (algSc‘𝑈)) ∘ (𝐹 + 𝐺)))‘(𝑥 ∈ 𝐼 ↦ if(𝑥 ∈ 𝐽, ((𝐽 mVar 𝑈)‘𝑥), ((algSc‘𝑇)‘(((𝐼 ∖ 𝐽) mVar 𝑅)‘𝑥))))) = ((((𝐼 eval 𝑇)‘(((algSc‘𝑇) ∘ (algSc‘𝑈)) ∘ 𝐹))‘(𝑥 ∈ 𝐼 ↦ if(𝑥 ∈ 𝐽, ((𝐽 mVar 𝑈)‘𝑥), ((algSc‘𝑇)‘(((𝐼 ∖ 𝐽) mVar 𝑅)‘𝑥))))) ✚ (((𝐼 eval 𝑇)‘(((algSc‘𝑇) ∘ (algSc‘𝑈)) ∘ 𝐺))‘(𝑥 ∈ 𝐼 ↦ if(𝑥 ∈ 𝐽, ((𝐽 mVar 𝑈)‘𝑥), ((algSc‘𝑇)‘(((𝐼 ∖ 𝐽) mVar 𝑅)‘𝑥))))))) |
41 | 1, 11, 15 | mplcrngd 42502 |
. . . . 5
⊢ (𝜑 → 𝑃 ∈ CRing) |
42 | 41 | crnggrpd 20274 |
. . . 4
⊢ (𝜑 → 𝑃 ∈ Grp) |
43 | 3, 5, 42, 20, 21 | grpcld 18987 |
. . 3
⊢ (𝜑 → (𝐹 + 𝐺) ∈ 𝐵) |
44 | 1, 3, 7, 8, 9, 10,
15, 13, 43 | selvval2 42539 |
. 2
⊢ (𝜑 → (((𝐼 selectVars 𝑅)‘𝐽)‘(𝐹 + 𝐺)) = (((𝐼 eval 𝑇)‘(((algSc‘𝑇) ∘ (algSc‘𝑈)) ∘ (𝐹 + 𝐺)))‘(𝑥 ∈ 𝐼 ↦ if(𝑥 ∈ 𝐽, ((𝐽 mVar 𝑈)‘𝑥), ((algSc‘𝑇)‘(((𝐼 ∖ 𝐽) mVar 𝑅)‘𝑥)))))) |
45 | 1, 3, 7, 8, 9, 10,
15, 13, 20 | selvval2 42539 |
. . 3
⊢ (𝜑 → (((𝐼 selectVars 𝑅)‘𝐽)‘𝐹) = (((𝐼 eval 𝑇)‘(((algSc‘𝑇) ∘ (algSc‘𝑈)) ∘ 𝐹))‘(𝑥 ∈ 𝐼 ↦ if(𝑥 ∈ 𝐽, ((𝐽 mVar 𝑈)‘𝑥), ((algSc‘𝑇)‘(((𝐼 ∖ 𝐽) mVar 𝑅)‘𝑥)))))) |
46 | 1, 3, 7, 8, 9, 10,
15, 13, 21 | selvval2 42539 |
. . 3
⊢ (𝜑 → (((𝐼 selectVars 𝑅)‘𝐽)‘𝐺) = (((𝐼 eval 𝑇)‘(((algSc‘𝑇) ∘ (algSc‘𝑈)) ∘ 𝐺))‘(𝑥 ∈ 𝐼 ↦ if(𝑥 ∈ 𝐽, ((𝐽 mVar 𝑈)‘𝑥), ((algSc‘𝑇)‘(((𝐼 ∖ 𝐽) mVar 𝑅)‘𝑥)))))) |
47 | 45, 46 | oveq12d 7466 |
. 2
⊢ (𝜑 → ((((𝐼 selectVars 𝑅)‘𝐽)‘𝐹) ✚ (((𝐼 selectVars 𝑅)‘𝐽)‘𝐺)) = ((((𝐼 eval 𝑇)‘(((algSc‘𝑇) ∘ (algSc‘𝑈)) ∘ 𝐹))‘(𝑥 ∈ 𝐼 ↦ if(𝑥 ∈ 𝐽, ((𝐽 mVar 𝑈)‘𝑥), ((algSc‘𝑇)‘(((𝐼 ∖ 𝐽) mVar 𝑅)‘𝑥))))) ✚ (((𝐼 eval 𝑇)‘(((algSc‘𝑇) ∘ (algSc‘𝑈)) ∘ 𝐺))‘(𝑥 ∈ 𝐼 ↦ if(𝑥 ∈ 𝐽, ((𝐽 mVar 𝑈)‘𝑥), ((algSc‘𝑇)‘(((𝐼 ∖ 𝐽) mVar 𝑅)‘𝑥))))))) |
48 | 40, 44, 47 | 3eqtr4d 2790 |
1
⊢ (𝜑 → (((𝐼 selectVars 𝑅)‘𝐽)‘(𝐹 + 𝐺)) = ((((𝐼 selectVars 𝑅)‘𝐽)‘𝐹) ✚ (((𝐼 selectVars 𝑅)‘𝐽)‘𝐺))) |