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	⊢ 𝐽 = ( 𝐾 ↾_t 𝑆 )
	dvun.k	⊢ 𝐾 = ( TopOpen ‘ ℂ_fld )
	dvun.s	⊢ ( 𝜑 → 𝑆 ⊆ ℂ )
	dvun.f	⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ ℂ )
	dvun.g	⊢ ( 𝜑 → 𝐺 : 𝐵 ⟶ ℂ )
	dvun.a	⊢ ( 𝜑 → 𝐴 ⊆ 𝑆 )
	dvun.b	⊢ ( 𝜑 → 𝐵 ⊆ 𝑆 )
	dvun.d	⊢ ( 𝜑 → ( 𝐴 ∩ 𝐵 ) = ∅ )
	dvun.n	⊢ ( 𝜑 → ( ( ( int ‘ 𝐽 ) ‘ 𝐴 ) ∪ ( ( int ‘ 𝐽 ) ‘ 𝐵 ) ) = ( ( int ‘ 𝐽 ) ‘ ( 𝐴 ∪ 𝐵 ) ) )
Assertion	dvun	⊢ ( 𝜑 → ( ( 𝑆 D 𝐹 ) ∪ ( 𝑆 D 𝐺 ) ) = ( 𝑆 D ( 𝐹 ∪ 𝐺 ) ) )

Proof

Step	Hyp	Ref	Expression
1		dvun.j	⊢ 𝐽 = ( 𝐾 ↾_t 𝑆 )
2		dvun.k	⊢ 𝐾 = ( TopOpen ‘ ℂ_fld )
3		dvun.s	⊢ ( 𝜑 → 𝑆 ⊆ ℂ )
4		dvun.f	⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ ℂ )
5		dvun.g	⊢ ( 𝜑 → 𝐺 : 𝐵 ⟶ ℂ )
6		dvun.a	⊢ ( 𝜑 → 𝐴 ⊆ 𝑆 )
7		dvun.b	⊢ ( 𝜑 → 𝐵 ⊆ 𝑆 )
8		dvun.d	⊢ ( 𝜑 → ( 𝐴 ∩ 𝐵 ) = ∅ )
9		dvun.n	⊢ ( 𝜑 → ( ( ( int ‘ 𝐽 ) ‘ 𝐴 ) ∪ ( ( int ‘ 𝐽 ) ‘ 𝐵 ) ) = ( ( int ‘ 𝐽 ) ‘ ( 𝐴 ∪ 𝐵 ) ) )
10		resundi	⊢ ( ( 𝑆 D ( 𝐹 ∪ 𝐺 ) ) ↾ ( ( ( int ‘ 𝐽 ) ‘ 𝐴 ) ∪ ( ( int ‘ 𝐽 ) ‘ 𝐵 ) ) ) = ( ( ( 𝑆 D ( 𝐹 ∪ 𝐺 ) ) ↾ ( ( int ‘ 𝐽 ) ‘ 𝐴 ) ) ∪ ( ( 𝑆 D ( 𝐹 ∪ 𝐺 ) ) ↾ ( ( int ‘ 𝐽 ) ‘ 𝐵 ) ) )
11	9	reseq2d	⊢ ( 𝜑 → ( ( 𝑆 D ( 𝐹 ∪ 𝐺 ) ) ↾ ( ( ( int ‘ 𝐽 ) ‘ 𝐴 ) ∪ ( ( int ‘ 𝐽 ) ‘ 𝐵 ) ) ) = ( ( 𝑆 D ( 𝐹 ∪ 𝐺 ) ) ↾ ( ( int ‘ 𝐽 ) ‘ ( 𝐴 ∪ 𝐵 ) ) ) )
12	10 11	eqtr3id	⊢ ( 𝜑 → ( ( ( 𝑆 D ( 𝐹 ∪ 𝐺 ) ) ↾ ( ( int ‘ 𝐽 ) ‘ 𝐴 ) ) ∪ ( ( 𝑆 D ( 𝐹 ∪ 𝐺 ) ) ↾ ( ( int ‘ 𝐽 ) ‘ 𝐵 ) ) ) = ( ( 𝑆 D ( 𝐹 ∪ 𝐺 ) ) ↾ ( ( int ‘ 𝐽 ) ‘ ( 𝐴 ∪ 𝐵 ) ) ) )
13	4 5 8	fun2d	⊢ ( 𝜑 → ( 𝐹 ∪ 𝐺 ) : ( 𝐴 ∪ 𝐵 ) ⟶ ℂ )
14	6 7	unssd	⊢ ( 𝜑 → ( 𝐴 ∪ 𝐵 ) ⊆ 𝑆 )
15	2 1	dvres	⊢ ( ( ( 𝑆 ⊆ ℂ ∧ ( 𝐹 ∪ 𝐺 ) : ( 𝐴 ∪ 𝐵 ) ⟶ ℂ ) ∧ ( ( 𝐴 ∪ 𝐵 ) ⊆ 𝑆 ∧ 𝐴 ⊆ 𝑆 ) ) → ( 𝑆 D ( ( 𝐹 ∪ 𝐺 ) ↾ 𝐴 ) ) = ( ( 𝑆 D ( 𝐹 ∪ 𝐺 ) ) ↾ ( ( int ‘ 𝐽 ) ‘ 𝐴 ) ) )
16	3 13 14 6 15	syl22anc	⊢ ( 𝜑 → ( 𝑆 D ( ( 𝐹 ∪ 𝐺 ) ↾ 𝐴 ) ) = ( ( 𝑆 D ( 𝐹 ∪ 𝐺 ) ) ↾ ( ( int ‘ 𝐽 ) ‘ 𝐴 ) ) )
17	4	ffnd	⊢ ( 𝜑 → 𝐹 Fn 𝐴 )
18	5	ffnd	⊢ ( 𝜑 → 𝐺 Fn 𝐵 )
19		fnunres1	⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐵 ∧ ( 𝐴 ∩ 𝐵 ) = ∅ ) → ( ( 𝐹 ∪ 𝐺 ) ↾ 𝐴 ) = 𝐹 )
20	17 18 8 19	syl3anc	⊢ ( 𝜑 → ( ( 𝐹 ∪ 𝐺 ) ↾ 𝐴 ) = 𝐹 )
21	20	oveq2d	⊢ ( 𝜑 → ( 𝑆 D ( ( 𝐹 ∪ 𝐺 ) ↾ 𝐴 ) ) = ( 𝑆 D 𝐹 ) )
22	16 21	eqtr3d	⊢ ( 𝜑 → ( ( 𝑆 D ( 𝐹 ∪ 𝐺 ) ) ↾ ( ( int ‘ 𝐽 ) ‘ 𝐴 ) ) = ( 𝑆 D 𝐹 ) )
23	2 1	dvres	⊢ ( ( ( 𝑆 ⊆ ℂ ∧ ( 𝐹 ∪ 𝐺 ) : ( 𝐴 ∪ 𝐵 ) ⟶ ℂ ) ∧ ( ( 𝐴 ∪ 𝐵 ) ⊆ 𝑆 ∧ 𝐵 ⊆ 𝑆 ) ) → ( 𝑆 D ( ( 𝐹 ∪ 𝐺 ) ↾ 𝐵 ) ) = ( ( 𝑆 D ( 𝐹 ∪ 𝐺 ) ) ↾ ( ( int ‘ 𝐽 ) ‘ 𝐵 ) ) )
24	3 13 14 7 23	syl22anc	⊢ ( 𝜑 → ( 𝑆 D ( ( 𝐹 ∪ 𝐺 ) ↾ 𝐵 ) ) = ( ( 𝑆 D ( 𝐹 ∪ 𝐺 ) ) ↾ ( ( int ‘ 𝐽 ) ‘ 𝐵 ) ) )
25		fnunres2	⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐵 ∧ ( 𝐴 ∩ 𝐵 ) = ∅ ) → ( ( 𝐹 ∪ 𝐺 ) ↾ 𝐵 ) = 𝐺 )
26	17 18 8 25	syl3anc	⊢ ( 𝜑 → ( ( 𝐹 ∪ 𝐺 ) ↾ 𝐵 ) = 𝐺 )
27	26	oveq2d	⊢ ( 𝜑 → ( 𝑆 D ( ( 𝐹 ∪ 𝐺 ) ↾ 𝐵 ) ) = ( 𝑆 D 𝐺 ) )
28	24 27	eqtr3d	⊢ ( 𝜑 → ( ( 𝑆 D ( 𝐹 ∪ 𝐺 ) ) ↾ ( ( int ‘ 𝐽 ) ‘ 𝐵 ) ) = ( 𝑆 D 𝐺 ) )
29	22 28	uneq12d	⊢ ( 𝜑 → ( ( ( 𝑆 D ( 𝐹 ∪ 𝐺 ) ) ↾ ( ( int ‘ 𝐽 ) ‘ 𝐴 ) ) ∪ ( ( 𝑆 D ( 𝐹 ∪ 𝐺 ) ) ↾ ( ( int ‘ 𝐽 ) ‘ 𝐵 ) ) ) = ( ( 𝑆 D 𝐹 ) ∪ ( 𝑆 D 𝐺 ) ) )
30	2 1	dvres	⊢ ( ( ( 𝑆 ⊆ ℂ ∧ ( 𝐹 ∪ 𝐺 ) : ( 𝐴 ∪ 𝐵 ) ⟶ ℂ ) ∧ ( ( 𝐴 ∪ 𝐵 ) ⊆ 𝑆 ∧ ( 𝐴 ∪ 𝐵 ) ⊆ 𝑆 ) ) → ( 𝑆 D ( ( 𝐹 ∪ 𝐺 ) ↾ ( 𝐴 ∪ 𝐵 ) ) ) = ( ( 𝑆 D ( 𝐹 ∪ 𝐺 ) ) ↾ ( ( int ‘ 𝐽 ) ‘ ( 𝐴 ∪ 𝐵 ) ) ) )
31	3 13 14 14 30	syl22anc	⊢ ( 𝜑 → ( 𝑆 D ( ( 𝐹 ∪ 𝐺 ) ↾ ( 𝐴 ∪ 𝐵 ) ) ) = ( ( 𝑆 D ( 𝐹 ∪ 𝐺 ) ) ↾ ( ( int ‘ 𝐽 ) ‘ ( 𝐴 ∪ 𝐵 ) ) ) )
32	13	ffnd	⊢ ( 𝜑 → ( 𝐹 ∪ 𝐺 ) Fn ( 𝐴 ∪ 𝐵 ) )
33		fnresdm	⊢ ( ( 𝐹 ∪ 𝐺 ) Fn ( 𝐴 ∪ 𝐵 ) → ( ( 𝐹 ∪ 𝐺 ) ↾ ( 𝐴 ∪ 𝐵 ) ) = ( 𝐹 ∪ 𝐺 ) )
34	32 33	syl	⊢ ( 𝜑 → ( ( 𝐹 ∪ 𝐺 ) ↾ ( 𝐴 ∪ 𝐵 ) ) = ( 𝐹 ∪ 𝐺 ) )
35	34	oveq2d	⊢ ( 𝜑 → ( 𝑆 D ( ( 𝐹 ∪ 𝐺 ) ↾ ( 𝐴 ∪ 𝐵 ) ) ) = ( 𝑆 D ( 𝐹 ∪ 𝐺 ) ) )
36	31 35	eqtr3d	⊢ ( 𝜑 → ( ( 𝑆 D ( 𝐹 ∪ 𝐺 ) ) ↾ ( ( int ‘ 𝐽 ) ‘ ( 𝐴 ∪ 𝐵 ) ) ) = ( 𝑆 D ( 𝐹 ∪ 𝐺 ) ) )
37	12 29 36	3eqtr3d	⊢ ( 𝜑 → ( ( 𝑆 D 𝐹 ) ∪ ( 𝑆 D 𝐺 ) ) = ( 𝑆 D ( 𝐹 ∪ 𝐺 ) ) )

Metamath Proof Explorer

Theorem dvun

Proof