Theorem dvun

Description: Condition for the union of the derivatives of two disjoint functions to be equal to the derivative of the union of the two functions. If A and B are open sets, this condition (dvun.n) is satisfied by isopn3i . (Contributed by SN, 30-Sep-2025)

	Ref	Expression
Hypotheses	dvun.j	$$⊢J=K{\upharpoonright }_{𝑡}S$$
	dvun.k	$$⊢K=\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)$$
	dvun.s	$$⊢\phi \to S\subseteq ℂ$$
	dvun.f	$$⊢\phi \to F:A⟶ℂ$$
	dvun.g	$$⊢\phi \to G:B⟶ℂ$$
	dvun.a	$$⊢\phi \to A\subseteq S$$
	dvun.b	$$⊢\phi \to B\subseteq S$$
	dvun.d	$$⊢\phi \to A\cap B=\varnothing$$
	dvun.n	$$⊢\phi \to \mathrm{int}\left(J\right)\left(A\right)\cup \mathrm{int}\left(J\right)\left(B\right)=\mathrm{int}\left(J\right)\left(A\cup B\right)$$
Assertion	dvun	$$⊢\phi \to F_S^{\prime }\cup G_S^{\prime }=S\mathrm{D}\left(F\cup G\right)$$

Proof

Step	Hyp	Ref	Expression
1		dvun.j	$$⊢J=K{\upharpoonright }_{𝑡}S$$
2		dvun.k	$$⊢K=\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)$$
3		dvun.s	$$⊢\phi \to S\subseteq ℂ$$
4		dvun.f	$$⊢\phi \to F:A⟶ℂ$$
5		dvun.g	$$⊢\phi \to G:B⟶ℂ$$
6		dvun.a	$$⊢\phi \to A\subseteq S$$
7		dvun.b	$$⊢\phi \to B\subseteq S$$
8		dvun.d	$$⊢\phi \to A\cap B=\varnothing$$
9		dvun.n	$$⊢\phi \to \mathrm{int}\left(J\right)\left(A\right)\cup \mathrm{int}\left(J\right)\left(B\right)=\mathrm{int}\left(J\right)\left(A\cup B\right)$$
10		resundi	$$⊢{{\left(F\cup G\right)}_S^{\prime }\upharpoonright }_{\left(\mathrm{int}\left(J\right)\left(A\right)\cup \mathrm{int}\left(J\right)\left(B\right)\right)}=\left({{\left(F\cup G\right)}_S^{\prime }\upharpoonright }_{\mathrm{int}\left(J\right)\left(A\right)}\right)\cup \left({{\left(F\cup G\right)}_S^{\prime }\upharpoonright }_{\mathrm{int}\left(J\right)\left(B\right)}\right)$$
11	9	reseq2d	$$⊢\phi \to {{\left(F\cup G\right)}_S^{\prime }\upharpoonright }_{\left(\mathrm{int}\left(J\right)\left(A\right)\cup \mathrm{int}\left(J\right)\left(B\right)\right)}={{\left(F\cup G\right)}_S^{\prime }\upharpoonright }_{\mathrm{int}\left(J\right)\left(A\cup B\right)}$$
12	10 11	eqtr3id	$$⊢\phi \to \left({{\left(F\cup G\right)}_S^{\prime }\upharpoonright }_{\mathrm{int}\left(J\right)\left(A\right)}\right)\cup \left({{\left(F\cup G\right)}_S^{\prime }\upharpoonright }_{\mathrm{int}\left(J\right)\left(B\right)}\right)={{\left(F\cup G\right)}_S^{\prime }\upharpoonright }_{\mathrm{int}\left(J\right)\left(A\cup B\right)}$$
13	4 5 8	fun2d	$$⊢\phi \to \left(F\cup G\right):A\cup B⟶ℂ$$
14	6 7	unssd	$$⊢\phi \to A\cup B\subseteq S$$
15	2 1	dvres	$$⊢\left(\left(S\subseteq ℂ\wedge \left(F\cup G\right):A\cup B⟶ℂ\right)\wedge \left(A\cup B\subseteq S\wedge A\subseteq S\right)\right)\to S\mathrm{D}\left({\left(F\cup G\right)\upharpoonright }_A\right)={{\left(F\cup G\right)}_S^{\prime }\upharpoonright }_{\mathrm{int}\left(J\right)\left(A\right)}$$
16	3 13 14 6 15	syl22anc	$$⊢\phi \to S\mathrm{D}\left({\left(F\cup G\right)\upharpoonright }_A\right)={{\left(F\cup G\right)}_S^{\prime }\upharpoonright }_{\mathrm{int}\left(J\right)\left(A\right)}$$
17	4	ffnd	$$⊢\phi \to FFnA$$
18	5	ffnd	$$⊢\phi \to GFnB$$
19		fnunres1	$$⊢\left(FFnA\wedge GFnB\wedge A\cap B=\varnothing \right)\to {\left(F\cup G\right)\upharpoonright }_A=F$$
20	17 18 8 19	syl3anc	$$⊢\phi \to {\left(F\cup G\right)\upharpoonright }_A=F$$
21	20	oveq2d	$$⊢\phi \to S\mathrm{D}\left({\left(F\cup G\right)\upharpoonright }_A\right)=S\mathrm{D}F$$
22	16 21	eqtr3d	$$⊢\phi \to {{\left(F\cup G\right)}_S^{\prime }\upharpoonright }_{\mathrm{int}\left(J\right)\left(A\right)}=S\mathrm{D}F$$
23	2 1	dvres	$$⊢\left(\left(S\subseteq ℂ\wedge \left(F\cup G\right):A\cup B⟶ℂ\right)\wedge \left(A\cup B\subseteq S\wedge B\subseteq S\right)\right)\to S\mathrm{D}\left({\left(F\cup G\right)\upharpoonright }_B\right)={{\left(F\cup G\right)}_S^{\prime }\upharpoonright }_{\mathrm{int}\left(J\right)\left(B\right)}$$
24	3 13 14 7 23	syl22anc	$$⊢\phi \to S\mathrm{D}\left({\left(F\cup G\right)\upharpoonright }_B\right)={{\left(F\cup G\right)}_S^{\prime }\upharpoonright }_{\mathrm{int}\left(J\right)\left(B\right)}$$
25		fnunres2	$$⊢\left(FFnA\wedge GFnB\wedge A\cap B=\varnothing \right)\to {\left(F\cup G\right)\upharpoonright }_B=G$$
26	17 18 8 25	syl3anc	$$⊢\phi \to {\left(F\cup G\right)\upharpoonright }_B=G$$
27	26	oveq2d	$$⊢\phi \to S\mathrm{D}\left({\left(F\cup G\right)\upharpoonright }_B\right)=S\mathrm{D}G$$
28	24 27	eqtr3d	$$⊢\phi \to {{\left(F\cup G\right)}_S^{\prime }\upharpoonright }_{\mathrm{int}\left(J\right)\left(B\right)}=S\mathrm{D}G$$
29	22 28	uneq12d	$$⊢\phi \to \left({{\left(F\cup G\right)}_S^{\prime }\upharpoonright }_{\mathrm{int}\left(J\right)\left(A\right)}\right)\cup \left({{\left(F\cup G\right)}_S^{\prime }\upharpoonright }_{\mathrm{int}\left(J\right)\left(B\right)}\right)=F_S^{\prime }\cup G_S^{\prime }$$
30	2 1	dvres	$$⊢\left(\left(S\subseteq ℂ\wedge \left(F\cup G\right):A\cup B⟶ℂ\right)\wedge \left(A\cup B\subseteq S\wedge A\cup B\subseteq S\right)\right)\to S\mathrm{D}\left({\left(F\cup G\right)\upharpoonright }_{\left(A\cup B\right)}\right)={{\left(F\cup G\right)}_S^{\prime }\upharpoonright }_{\mathrm{int}\left(J\right)\left(A\cup B\right)}$$
31	3 13 14 14 30	syl22anc	$$⊢\phi \to S\mathrm{D}\left({\left(F\cup G\right)\upharpoonright }_{\left(A\cup B\right)}\right)={{\left(F\cup G\right)}_S^{\prime }\upharpoonright }_{\mathrm{int}\left(J\right)\left(A\cup B\right)}$$
32	13	ffnd	$$⊢\phi \to \left(F\cup G\right)Fn\left(A\cup B\right)$$
33		fnresdm	$$⊢\left(F\cup G\right)Fn\left(A\cup B\right)\to {\left(F\cup G\right)\upharpoonright }_{\left(A\cup B\right)}=F\cup G$$
34	32 33	syl	$$⊢\phi \to {\left(F\cup G\right)\upharpoonright }_{\left(A\cup B\right)}=F\cup G$$
35	34	oveq2d	$$⊢\phi \to S\mathrm{D}\left({\left(F\cup G\right)\upharpoonright }_{\left(A\cup B\right)}\right)=S\mathrm{D}\left(F\cup G\right)$$
36	31 35	eqtr3d	$$⊢\phi \to {{\left(F\cup G\right)}_S^{\prime }\upharpoonright }_{\mathrm{int}\left(J\right)\left(A\cup B\right)}=S\mathrm{D}\left(F\cup G\right)$$
37	12 29 36	3eqtr3d	$$⊢\phi \to F_S^{\prime }\cup G_S^{\prime }=S\mathrm{D}\left(F\cup G\right)$$