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 |`t S )
	dvun.k	|- K = ( TopOpen ` CCfld )
	dvun.s	|- ( ph -> S C_ CC )
	dvun.f	|- ( ph -> F : A --> CC )
	dvun.g	|- ( ph -> G : B --> CC )
	dvun.a	|- ( ph -> A C_ S )
	dvun.b	|- ( ph -> B C_ S )
	dvun.d	|- ( ph -> ( A i^i B ) = (/) )
	dvun.n	|- ( ph -> ( ( ( int ` J ) ` A ) u. ( ( int ` J ) ` B ) ) = ( ( int ` J ) ` ( A u. B ) ) )
Assertion	dvun	|- ( ph -> ( ( S _D F ) u. ( S _D G ) ) = ( S _D ( F u. G ) ) )

Proof

Step	Hyp	Ref	Expression
1		dvun.j	|- J = ( K |`t S )
2		dvun.k	|- K = ( TopOpen ` CCfld )
3		dvun.s	|- ( ph -> S C_ CC )
4		dvun.f	|- ( ph -> F : A --> CC )
5		dvun.g	|- ( ph -> G : B --> CC )
6		dvun.a	|- ( ph -> A C_ S )
7		dvun.b	|- ( ph -> B C_ S )
8		dvun.d	|- ( ph -> ( A i^i B ) = (/) )
9		dvun.n	|- ( ph -> ( ( ( int ` J ) ` A ) u. ( ( int ` J ) ` B ) ) = ( ( int ` J ) ` ( A u. B ) ) )
10		resundi	|- ( ( S _D ( F u. G ) ) |` ( ( ( int ` J ) ` A ) u. ( ( int ` J ) ` B ) ) ) = ( ( ( S _D ( F u. G ) ) |` ( ( int ` J ) ` A ) ) u. ( ( S _D ( F u. G ) ) |` ( ( int ` J ) ` B ) ) )
11	9	reseq2d	|- ( ph -> ( ( S _D ( F u. G ) ) |` ( ( ( int ` J ) ` A ) u. ( ( int ` J ) ` B ) ) ) = ( ( S _D ( F u. G ) ) |` ( ( int ` J ) ` ( A u. B ) ) ) )
12	10 11	eqtr3id	|- ( ph -> ( ( ( S _D ( F u. G ) ) |` ( ( int ` J ) ` A ) ) u. ( ( S _D ( F u. G ) ) |` ( ( int ` J ) ` B ) ) ) = ( ( S _D ( F u. G ) ) |` ( ( int ` J ) ` ( A u. B ) ) ) )
13	4 5 8	fun2d	|- ( ph -> ( F u. G ) : ( A u. B ) --> CC )
14	6 7	unssd	|- ( ph -> ( A u. B ) C_ S )
15	2 1	dvres	|- ( ( ( S C_ CC /\ ( F u. G ) : ( A u. B ) --> CC ) /\ ( ( A u. B ) C_ S /\ A C_ S ) ) -> ( S _D ( ( F u. G ) |` A ) ) = ( ( S _D ( F u. G ) ) |` ( ( int ` J ) ` A ) ) )
16	3 13 14 6 15	syl22anc	|- ( ph -> ( S _D ( ( F u. G ) |` A ) ) = ( ( S _D ( F u. G ) ) |` ( ( int ` J ) ` A ) ) )
17	4	ffnd	|- ( ph -> F Fn A )
18	5	ffnd	|- ( ph -> G Fn B )
19		fnunres1	|- ( ( F Fn A /\ G Fn B /\ ( A i^i B ) = (/) ) -> ( ( F u. G ) |` A ) = F )
20	17 18 8 19	syl3anc	|- ( ph -> ( ( F u. G ) |` A ) = F )
21	20	oveq2d	|- ( ph -> ( S _D ( ( F u. G ) |` A ) ) = ( S _D F ) )
22	16 21	eqtr3d	|- ( ph -> ( ( S _D ( F u. G ) ) |` ( ( int ` J ) ` A ) ) = ( S _D F ) )
23	2 1	dvres	|- ( ( ( S C_ CC /\ ( F u. G ) : ( A u. B ) --> CC ) /\ ( ( A u. B ) C_ S /\ B C_ S ) ) -> ( S _D ( ( F u. G ) |` B ) ) = ( ( S _D ( F u. G ) ) |` ( ( int ` J ) ` B ) ) )
24	3 13 14 7 23	syl22anc	|- ( ph -> ( S _D ( ( F u. G ) |` B ) ) = ( ( S _D ( F u. G ) ) |` ( ( int ` J ) ` B ) ) )
25		fnunres2	|- ( ( F Fn A /\ G Fn B /\ ( A i^i B ) = (/) ) -> ( ( F u. G ) |` B ) = G )
26	17 18 8 25	syl3anc	|- ( ph -> ( ( F u. G ) |` B ) = G )
27	26	oveq2d	|- ( ph -> ( S _D ( ( F u. G ) |` B ) ) = ( S _D G ) )
28	24 27	eqtr3d	|- ( ph -> ( ( S _D ( F u. G ) ) |` ( ( int ` J ) ` B ) ) = ( S _D G ) )
29	22 28	uneq12d	|- ( ph -> ( ( ( S _D ( F u. G ) ) |` ( ( int ` J ) ` A ) ) u. ( ( S _D ( F u. G ) ) |` ( ( int ` J ) ` B ) ) ) = ( ( S _D F ) u. ( S _D G ) ) )
30	2 1	dvres	|- ( ( ( S C_ CC /\ ( F u. G ) : ( A u. B ) --> CC ) /\ ( ( A u. B ) C_ S /\ ( A u. B ) C_ S ) ) -> ( S _D ( ( F u. G ) |` ( A u. B ) ) ) = ( ( S _D ( F u. G ) ) |` ( ( int ` J ) ` ( A u. B ) ) ) )
31	3 13 14 14 30	syl22anc	|- ( ph -> ( S _D ( ( F u. G ) |` ( A u. B ) ) ) = ( ( S _D ( F u. G ) ) |` ( ( int ` J ) ` ( A u. B ) ) ) )
32	13	ffnd	|- ( ph -> ( F u. G ) Fn ( A u. B ) )
33		fnresdm	|- ( ( F u. G ) Fn ( A u. B ) -> ( ( F u. G ) |` ( A u. B ) ) = ( F u. G ) )
34	32 33	syl	|- ( ph -> ( ( F u. G ) |` ( A u. B ) ) = ( F u. G ) )
35	34	oveq2d	|- ( ph -> ( S _D ( ( F u. G ) |` ( A u. B ) ) ) = ( S _D ( F u. G ) ) )
36	31 35	eqtr3d	|- ( ph -> ( ( S _D ( F u. G ) ) |` ( ( int ` J ) ` ( A u. B ) ) ) = ( S _D ( F u. G ) ) )
37	12 29 36	3eqtr3d	|- ( ph -> ( ( S _D F ) u. ( S _D G ) ) = ( S _D ( F u. G ) ) )