# Metamath Proof Explorer

## Theorem dvcmulf

Description: The product rule when one argument is a constant. (Contributed by Mario Carneiro, 9-Aug-2014) (Revised by Mario Carneiro, 10-Feb-2015)

Ref Expression
Hypotheses dvcmul.s ${⊢}{\phi }\to {S}\in \left\{ℝ,ℂ\right\}$
dvcmul.f ${⊢}{\phi }\to {F}:{X}⟶ℂ$
dvcmul.a ${⊢}{\phi }\to {A}\in ℂ$
dvcmulf.df ${⊢}{\phi }\to \mathrm{dom}{{F}}_{{S}}^{\prime }={X}$
Assertion dvcmulf ${⊢}{\phi }\to {S}\mathrm{D}\left(\left({S}×\left\{{A}\right\}\right){×}_{f}{F}\right)=\left({S}×\left\{{A}\right\}\right){×}_{f}{{F}}_{{S}}^{\prime }$

### Proof

Step Hyp Ref Expression
1 dvcmul.s ${⊢}{\phi }\to {S}\in \left\{ℝ,ℂ\right\}$
2 dvcmul.f ${⊢}{\phi }\to {F}:{X}⟶ℂ$
3 dvcmul.a ${⊢}{\phi }\to {A}\in ℂ$
4 dvcmulf.df ${⊢}{\phi }\to \mathrm{dom}{{F}}_{{S}}^{\prime }={X}$
5 fconstg ${⊢}{A}\in ℂ\to \left({X}×\left\{{A}\right\}\right):{X}⟶\left\{{A}\right\}$
6 3 5 syl ${⊢}{\phi }\to \left({X}×\left\{{A}\right\}\right):{X}⟶\left\{{A}\right\}$
7 3 snssd ${⊢}{\phi }\to \left\{{A}\right\}\subseteq ℂ$
8 6 7 fssd ${⊢}{\phi }\to \left({X}×\left\{{A}\right\}\right):{X}⟶ℂ$
9 c0ex ${⊢}0\in \mathrm{V}$
10 9 fconst ${⊢}\left({X}×\left\{0\right\}\right):{X}⟶\left\{0\right\}$
11 recnprss ${⊢}{S}\in \left\{ℝ,ℂ\right\}\to {S}\subseteq ℂ$
12 1 11 syl ${⊢}{\phi }\to {S}\subseteq ℂ$
13 fconstg ${⊢}{A}\in ℂ\to \left({S}×\left\{{A}\right\}\right):{S}⟶\left\{{A}\right\}$
14 3 13 syl ${⊢}{\phi }\to \left({S}×\left\{{A}\right\}\right):{S}⟶\left\{{A}\right\}$
15 14 7 fssd ${⊢}{\phi }\to \left({S}×\left\{{A}\right\}\right):{S}⟶ℂ$
16 ssidd ${⊢}{\phi }\to {S}\subseteq {S}$
17 dvbsss ${⊢}\mathrm{dom}{{F}}_{{S}}^{\prime }\subseteq {S}$
18 17 a1i ${⊢}{\phi }\to \mathrm{dom}{{F}}_{{S}}^{\prime }\subseteq {S}$
19 4 18 eqsstrrd ${⊢}{\phi }\to {X}\subseteq {S}$
20 eqid ${⊢}\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)=\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)$
21 eqid ${⊢}\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right){↾}_{𝑡}{S}=\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right){↾}_{𝑡}{S}$
22 20 21 dvres ${⊢}\left(\left({S}\subseteq ℂ\wedge \left({S}×\left\{{A}\right\}\right):{S}⟶ℂ\right)\wedge \left({S}\subseteq {S}\wedge {X}\subseteq {S}\right)\right)\to {S}\mathrm{D}\left({\left({S}×\left\{{A}\right\}\right)↾}_{{X}}\right)={{\left({S}×\left\{{A}\right\}\right)}_{{S}}^{\prime }↾}_{\mathrm{int}\left(\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right){↾}_{𝑡}{S}\right)\left({X}\right)}$
23 12 15 16 19 22 syl22anc ${⊢}{\phi }\to {S}\mathrm{D}\left({\left({S}×\left\{{A}\right\}\right)↾}_{{X}}\right)={{\left({S}×\left\{{A}\right\}\right)}_{{S}}^{\prime }↾}_{\mathrm{int}\left(\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right){↾}_{𝑡}{S}\right)\left({X}\right)}$
24 19 resmptd ${⊢}{\phi }\to {\left({x}\in {S}⟼{A}\right)↾}_{{X}}=\left({x}\in {X}⟼{A}\right)$
25 fconstmpt ${⊢}{S}×\left\{{A}\right\}=\left({x}\in {S}⟼{A}\right)$
26 25 reseq1i ${⊢}{\left({S}×\left\{{A}\right\}\right)↾}_{{X}}={\left({x}\in {S}⟼{A}\right)↾}_{{X}}$
27 fconstmpt ${⊢}{X}×\left\{{A}\right\}=\left({x}\in {X}⟼{A}\right)$
28 24 26 27 3eqtr4g ${⊢}{\phi }\to {\left({S}×\left\{{A}\right\}\right)↾}_{{X}}={X}×\left\{{A}\right\}$
29 28 oveq2d ${⊢}{\phi }\to {S}\mathrm{D}\left({\left({S}×\left\{{A}\right\}\right)↾}_{{X}}\right)={S}\mathrm{D}\left({X}×\left\{{A}\right\}\right)$
30 19 resmptd ${⊢}{\phi }\to {\left({x}\in {S}⟼0\right)↾}_{{X}}=\left({x}\in {X}⟼0\right)$
31 fconstg ${⊢}{A}\in ℂ\to \left(ℂ×\left\{{A}\right\}\right):ℂ⟶\left\{{A}\right\}$
32 3 31 syl ${⊢}{\phi }\to \left(ℂ×\left\{{A}\right\}\right):ℂ⟶\left\{{A}\right\}$
33 32 7 fssd ${⊢}{\phi }\to \left(ℂ×\left\{{A}\right\}\right):ℂ⟶ℂ$
34 ssidd ${⊢}{\phi }\to ℂ\subseteq ℂ$
35 dvconst ${⊢}{A}\in ℂ\to ℂ\mathrm{D}\left(ℂ×\left\{{A}\right\}\right)=ℂ×\left\{0\right\}$
36 3 35 syl ${⊢}{\phi }\to ℂ\mathrm{D}\left(ℂ×\left\{{A}\right\}\right)=ℂ×\left\{0\right\}$
37 36 dmeqd ${⊢}{\phi }\to \mathrm{dom}{\left(ℂ×\left\{{A}\right\}\right)}_{ℂ}^{\prime }=\mathrm{dom}\left(ℂ×\left\{0\right\}\right)$
38 9 fconst ${⊢}\left(ℂ×\left\{0\right\}\right):ℂ⟶\left\{0\right\}$
39 38 fdmi ${⊢}\mathrm{dom}\left(ℂ×\left\{0\right\}\right)=ℂ$
40 37 39 syl6eq ${⊢}{\phi }\to \mathrm{dom}{\left(ℂ×\left\{{A}\right\}\right)}_{ℂ}^{\prime }=ℂ$
41 12 40 sseqtrrd ${⊢}{\phi }\to {S}\subseteq \mathrm{dom}{\left(ℂ×\left\{{A}\right\}\right)}_{ℂ}^{\prime }$
42 dvres3 ${⊢}\left(\left({S}\in \left\{ℝ,ℂ\right\}\wedge \left(ℂ×\left\{{A}\right\}\right):ℂ⟶ℂ\right)\wedge \left(ℂ\subseteq ℂ\wedge {S}\subseteq \mathrm{dom}{\left(ℂ×\left\{{A}\right\}\right)}_{ℂ}^{\prime }\right)\right)\to {S}\mathrm{D}\left({\left(ℂ×\left\{{A}\right\}\right)↾}_{{S}}\right)={{\left(ℂ×\left\{{A}\right\}\right)}_{ℂ}^{\prime }↾}_{{S}}$
43 1 33 34 41 42 syl22anc ${⊢}{\phi }\to {S}\mathrm{D}\left({\left(ℂ×\left\{{A}\right\}\right)↾}_{{S}}\right)={{\left(ℂ×\left\{{A}\right\}\right)}_{ℂ}^{\prime }↾}_{{S}}$
44 xpssres ${⊢}{S}\subseteq ℂ\to {\left(ℂ×\left\{{A}\right\}\right)↾}_{{S}}={S}×\left\{{A}\right\}$
45 12 44 syl ${⊢}{\phi }\to {\left(ℂ×\left\{{A}\right\}\right)↾}_{{S}}={S}×\left\{{A}\right\}$
46 45 oveq2d ${⊢}{\phi }\to {S}\mathrm{D}\left({\left(ℂ×\left\{{A}\right\}\right)↾}_{{S}}\right)={S}\mathrm{D}\left({S}×\left\{{A}\right\}\right)$
47 36 reseq1d ${⊢}{\phi }\to {{\left(ℂ×\left\{{A}\right\}\right)}_{ℂ}^{\prime }↾}_{{S}}={\left(ℂ×\left\{0\right\}\right)↾}_{{S}}$
48 xpssres ${⊢}{S}\subseteq ℂ\to {\left(ℂ×\left\{0\right\}\right)↾}_{{S}}={S}×\left\{0\right\}$
49 12 48 syl ${⊢}{\phi }\to {\left(ℂ×\left\{0\right\}\right)↾}_{{S}}={S}×\left\{0\right\}$
50 47 49 eqtrd ${⊢}{\phi }\to {{\left(ℂ×\left\{{A}\right\}\right)}_{ℂ}^{\prime }↾}_{{S}}={S}×\left\{0\right\}$
51 43 46 50 3eqtr3d ${⊢}{\phi }\to {S}\mathrm{D}\left({S}×\left\{{A}\right\}\right)={S}×\left\{0\right\}$
52 fconstmpt ${⊢}{S}×\left\{0\right\}=\left({x}\in {S}⟼0\right)$
53 51 52 syl6eq ${⊢}{\phi }\to {S}\mathrm{D}\left({S}×\left\{{A}\right\}\right)=\left({x}\in {S}⟼0\right)$
54 20 cnfldtopon ${⊢}\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)\in \mathrm{TopOn}\left(ℂ\right)$
55 resttopon ${⊢}\left(\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)\in \mathrm{TopOn}\left(ℂ\right)\wedge {S}\subseteq ℂ\right)\to \mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right){↾}_{𝑡}{S}\in \mathrm{TopOn}\left({S}\right)$
56 54 12 55 sylancr ${⊢}{\phi }\to \mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right){↾}_{𝑡}{S}\in \mathrm{TopOn}\left({S}\right)$
57 topontop ${⊢}\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right){↾}_{𝑡}{S}\in \mathrm{TopOn}\left({S}\right)\to \mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right){↾}_{𝑡}{S}\in \mathrm{Top}$
58 56 57 syl ${⊢}{\phi }\to \mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right){↾}_{𝑡}{S}\in \mathrm{Top}$
59 toponuni ${⊢}\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right){↾}_{𝑡}{S}\in \mathrm{TopOn}\left({S}\right)\to {S}=\bigcup \left(\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right){↾}_{𝑡}{S}\right)$
60 56 59 syl ${⊢}{\phi }\to {S}=\bigcup \left(\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right){↾}_{𝑡}{S}\right)$
61 19 60 sseqtrd ${⊢}{\phi }\to {X}\subseteq \bigcup \left(\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right){↾}_{𝑡}{S}\right)$
62 eqid ${⊢}\bigcup \left(\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right){↾}_{𝑡}{S}\right)=\bigcup \left(\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right){↾}_{𝑡}{S}\right)$
63 62 ntrss2 ${⊢}\left(\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right){↾}_{𝑡}{S}\in \mathrm{Top}\wedge {X}\subseteq \bigcup \left(\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right){↾}_{𝑡}{S}\right)\right)\to \mathrm{int}\left(\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right){↾}_{𝑡}{S}\right)\left({X}\right)\subseteq {X}$
64 58 61 63 syl2anc ${⊢}{\phi }\to \mathrm{int}\left(\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right){↾}_{𝑡}{S}\right)\left({X}\right)\subseteq {X}$
65 12 2 19 21 20 dvbssntr ${⊢}{\phi }\to \mathrm{dom}{{F}}_{{S}}^{\prime }\subseteq \mathrm{int}\left(\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right){↾}_{𝑡}{S}\right)\left({X}\right)$
66 4 65 eqsstrrd ${⊢}{\phi }\to {X}\subseteq \mathrm{int}\left(\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right){↾}_{𝑡}{S}\right)\left({X}\right)$
67 64 66 eqssd ${⊢}{\phi }\to \mathrm{int}\left(\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right){↾}_{𝑡}{S}\right)\left({X}\right)={X}$
68 53 67 reseq12d ${⊢}{\phi }\to {{\left({S}×\left\{{A}\right\}\right)}_{{S}}^{\prime }↾}_{\mathrm{int}\left(\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right){↾}_{𝑡}{S}\right)\left({X}\right)}={\left({x}\in {S}⟼0\right)↾}_{{X}}$
69 fconstmpt ${⊢}{X}×\left\{0\right\}=\left({x}\in {X}⟼0\right)$
70 69 a1i ${⊢}{\phi }\to {X}×\left\{0\right\}=\left({x}\in {X}⟼0\right)$
71 30 68 70 3eqtr4d ${⊢}{\phi }\to {{\left({S}×\left\{{A}\right\}\right)}_{{S}}^{\prime }↾}_{\mathrm{int}\left(\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right){↾}_{𝑡}{S}\right)\left({X}\right)}={X}×\left\{0\right\}$
72 23 29 71 3eqtr3d ${⊢}{\phi }\to {S}\mathrm{D}\left({X}×\left\{{A}\right\}\right)={X}×\left\{0\right\}$
73 72 feq1d ${⊢}{\phi }\to \left({\left({X}×\left\{{A}\right\}\right)}_{{S}}^{\prime }:{X}⟶\left\{0\right\}↔\left({X}×\left\{0\right\}\right):{X}⟶\left\{0\right\}\right)$
74 10 73 mpbiri ${⊢}{\phi }\to {\left({X}×\left\{{A}\right\}\right)}_{{S}}^{\prime }:{X}⟶\left\{0\right\}$
75 74 fdmd ${⊢}{\phi }\to \mathrm{dom}{\left({X}×\left\{{A}\right\}\right)}_{{S}}^{\prime }={X}$
76 1 8 2 75 4 dvmulf ${⊢}{\phi }\to {S}\mathrm{D}\left(\left({X}×\left\{{A}\right\}\right){×}_{f}{F}\right)=\left({\left({X}×\left\{{A}\right\}\right)}_{{S}}^{\prime }{×}_{f}{F}\right){+}_{f}\left({{F}}_{{S}}^{\prime }{×}_{f}\left({X}×\left\{{A}\right\}\right)\right)$
77 sseqin2 ${⊢}{X}\subseteq {S}↔{S}\cap {X}={X}$
78 19 77 sylib ${⊢}{\phi }\to {S}\cap {X}={X}$
79 78 mpteq1d ${⊢}{\phi }\to \left({x}\in \left({S}\cap {X}\right)⟼{A}{F}\left({x}\right)\right)=\left({x}\in {X}⟼{A}{F}\left({x}\right)\right)$
80 14 ffnd ${⊢}{\phi }\to \left({S}×\left\{{A}\right\}\right)Fn{S}$
81 2 ffnd ${⊢}{\phi }\to {F}Fn{X}$
82 1 19 ssexd ${⊢}{\phi }\to {X}\in \mathrm{V}$
83 eqid ${⊢}{S}\cap {X}={S}\cap {X}$
84 fvconst2g ${⊢}\left({A}\in ℂ\wedge {x}\in {S}\right)\to \left({S}×\left\{{A}\right\}\right)\left({x}\right)={A}$
85 3 84 sylan ${⊢}\left({\phi }\wedge {x}\in {S}\right)\to \left({S}×\left\{{A}\right\}\right)\left({x}\right)={A}$
86 eqidd ${⊢}\left({\phi }\wedge {x}\in {X}\right)\to {F}\left({x}\right)={F}\left({x}\right)$
87 80 81 1 82 83 85 86 offval ${⊢}{\phi }\to \left({S}×\left\{{A}\right\}\right){×}_{f}{F}=\left({x}\in \left({S}\cap {X}\right)⟼{A}{F}\left({x}\right)\right)$
88 6 ffnd ${⊢}{\phi }\to \left({X}×\left\{{A}\right\}\right)Fn{X}$
89 inidm ${⊢}{X}\cap {X}={X}$
90 fvconst2g ${⊢}\left({A}\in ℂ\wedge {x}\in {X}\right)\to \left({X}×\left\{{A}\right\}\right)\left({x}\right)={A}$
91 3 90 sylan ${⊢}\left({\phi }\wedge {x}\in {X}\right)\to \left({X}×\left\{{A}\right\}\right)\left({x}\right)={A}$
92 88 81 82 82 89 91 86 offval ${⊢}{\phi }\to \left({X}×\left\{{A}\right\}\right){×}_{f}{F}=\left({x}\in {X}⟼{A}{F}\left({x}\right)\right)$
93 79 87 92 3eqtr4d ${⊢}{\phi }\to \left({S}×\left\{{A}\right\}\right){×}_{f}{F}=\left({X}×\left\{{A}\right\}\right){×}_{f}{F}$
94 93 oveq2d ${⊢}{\phi }\to {S}\mathrm{D}\left(\left({S}×\left\{{A}\right\}\right){×}_{f}{F}\right)={S}\mathrm{D}\left(\left({X}×\left\{{A}\right\}\right){×}_{f}{F}\right)$
95 78 mpteq1d ${⊢}{\phi }\to \left({x}\in \left({S}\cap {X}\right)⟼{A}{{F}}_{{S}}^{\prime }\left({x}\right)\right)=\left({x}\in {X}⟼{A}{{F}}_{{S}}^{\prime }\left({x}\right)\right)$
96 dvfg ${⊢}{S}\in \left\{ℝ,ℂ\right\}\to {{F}}_{{S}}^{\prime }:\mathrm{dom}{{F}}_{{S}}^{\prime }⟶ℂ$
97 1 96 syl ${⊢}{\phi }\to {{F}}_{{S}}^{\prime }:\mathrm{dom}{{F}}_{{S}}^{\prime }⟶ℂ$
98 4 feq2d ${⊢}{\phi }\to \left({{F}}_{{S}}^{\prime }:\mathrm{dom}{{F}}_{{S}}^{\prime }⟶ℂ↔{{F}}_{{S}}^{\prime }:{X}⟶ℂ\right)$
99 97 98 mpbid ${⊢}{\phi }\to {{F}}_{{S}}^{\prime }:{X}⟶ℂ$
100 99 ffnd ${⊢}{\phi }\to {{F}}_{{S}}^{\prime }Fn{X}$
101 eqidd ${⊢}\left({\phi }\wedge {x}\in {X}\right)\to {{F}}_{{S}}^{\prime }\left({x}\right)={{F}}_{{S}}^{\prime }\left({x}\right)$
102 80 100 1 82 83 85 101 offval ${⊢}{\phi }\to \left({S}×\left\{{A}\right\}\right){×}_{f}{{F}}_{{S}}^{\prime }=\left({x}\in \left({S}\cap {X}\right)⟼{A}{{F}}_{{S}}^{\prime }\left({x}\right)\right)$
103 0cnd ${⊢}\left({\phi }\wedge {x}\in {X}\right)\to 0\in ℂ$
104 ovexd ${⊢}\left({\phi }\wedge {x}\in {X}\right)\to {{F}}_{{S}}^{\prime }\left({x}\right){A}\in \mathrm{V}$
105 72 oveq1d ${⊢}{\phi }\to {\left({X}×\left\{{A}\right\}\right)}_{{S}}^{\prime }{×}_{f}{F}=\left({X}×\left\{0\right\}\right){×}_{f}{F}$
106 0cnd ${⊢}{\phi }\to 0\in ℂ$
107 mul02 ${⊢}{x}\in ℂ\to 0\cdot {x}=0$
108 107 adantl ${⊢}\left({\phi }\wedge {x}\in ℂ\right)\to 0\cdot {x}=0$
109 82 2 106 106 108 caofid2 ${⊢}{\phi }\to \left({X}×\left\{0\right\}\right){×}_{f}{F}={X}×\left\{0\right\}$
110 105 109 eqtrd ${⊢}{\phi }\to {\left({X}×\left\{{A}\right\}\right)}_{{S}}^{\prime }{×}_{f}{F}={X}×\left\{0\right\}$
111 110 69 syl6eq ${⊢}{\phi }\to {\left({X}×\left\{{A}\right\}\right)}_{{S}}^{\prime }{×}_{f}{F}=\left({x}\in {X}⟼0\right)$
112 fvexd ${⊢}\left({\phi }\wedge {x}\in {X}\right)\to {{F}}_{{S}}^{\prime }\left({x}\right)\in \mathrm{V}$
113 3 adantr ${⊢}\left({\phi }\wedge {x}\in {X}\right)\to {A}\in ℂ$
114 99 feqmptd ${⊢}{\phi }\to {S}\mathrm{D}{F}=\left({x}\in {X}⟼{{F}}_{{S}}^{\prime }\left({x}\right)\right)$
115 27 a1i ${⊢}{\phi }\to {X}×\left\{{A}\right\}=\left({x}\in {X}⟼{A}\right)$
116 82 112 113 114 115 offval2 ${⊢}{\phi }\to {{F}}_{{S}}^{\prime }{×}_{f}\left({X}×\left\{{A}\right\}\right)=\left({x}\in {X}⟼{{F}}_{{S}}^{\prime }\left({x}\right){A}\right)$
117 82 103 104 111 116 offval2 ${⊢}{\phi }\to \left({\left({X}×\left\{{A}\right\}\right)}_{{S}}^{\prime }{×}_{f}{F}\right){+}_{f}\left({{F}}_{{S}}^{\prime }{×}_{f}\left({X}×\left\{{A}\right\}\right)\right)=\left({x}\in {X}⟼0+{{F}}_{{S}}^{\prime }\left({x}\right){A}\right)$
118 99 ffvelrnda ${⊢}\left({\phi }\wedge {x}\in {X}\right)\to {{F}}_{{S}}^{\prime }\left({x}\right)\in ℂ$
119 118 113 mulcld ${⊢}\left({\phi }\wedge {x}\in {X}\right)\to {{F}}_{{S}}^{\prime }\left({x}\right){A}\in ℂ$
120 119 addid2d ${⊢}\left({\phi }\wedge {x}\in {X}\right)\to 0+{{F}}_{{S}}^{\prime }\left({x}\right){A}={{F}}_{{S}}^{\prime }\left({x}\right){A}$
121 118 113 mulcomd ${⊢}\left({\phi }\wedge {x}\in {X}\right)\to {{F}}_{{S}}^{\prime }\left({x}\right){A}={A}{{F}}_{{S}}^{\prime }\left({x}\right)$
122 120 121 eqtrd ${⊢}\left({\phi }\wedge {x}\in {X}\right)\to 0+{{F}}_{{S}}^{\prime }\left({x}\right){A}={A}{{F}}_{{S}}^{\prime }\left({x}\right)$
123 122 mpteq2dva ${⊢}{\phi }\to \left({x}\in {X}⟼0+{{F}}_{{S}}^{\prime }\left({x}\right){A}\right)=\left({x}\in {X}⟼{A}{{F}}_{{S}}^{\prime }\left({x}\right)\right)$
124 117 123 eqtrd ${⊢}{\phi }\to \left({\left({X}×\left\{{A}\right\}\right)}_{{S}}^{\prime }{×}_{f}{F}\right){+}_{f}\left({{F}}_{{S}}^{\prime }{×}_{f}\left({X}×\left\{{A}\right\}\right)\right)=\left({x}\in {X}⟼{A}{{F}}_{{S}}^{\prime }\left({x}\right)\right)$
125 95 102 124 3eqtr4d ${⊢}{\phi }\to \left({S}×\left\{{A}\right\}\right){×}_{f}{{F}}_{{S}}^{\prime }=\left({\left({X}×\left\{{A}\right\}\right)}_{{S}}^{\prime }{×}_{f}{F}\right){+}_{f}\left({{F}}_{{S}}^{\prime }{×}_{f}\left({X}×\left\{{A}\right\}\right)\right)$
126 76 94 125 3eqtr4d ${⊢}{\phi }\to {S}\mathrm{D}\left(\left({S}×\left\{{A}\right\}\right){×}_{f}{F}\right)=\left({S}×\left\{{A}\right\}\right){×}_{f}{{F}}_{{S}}^{\prime }$