Theorem resasplit

Description: If two functions agree on their common domain, express their union as a union of three functions with pairwise disjoint domains. (Contributed by Stefan O'Rear, 9-Oct-2014)

	Ref	Expression
Assertion	resasplit	|- ( ( F Fn A /\ G Fn B /\ ( F |` ( A i^i B ) ) = ( G |` ( A i^i B ) ) ) -> ( F u. G ) = ( ( F |` ( A i^i B ) ) u. ( ( F |` ( A \ B ) ) u. ( G |` ( B \ A ) ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		fnresdm	|- ( F Fn A -> ( F |` A ) = F )
2		fnresdm	|- ( G Fn B -> ( G |` B ) = G )
3		uneq12	|- ( ( ( F |` A ) = F /\ ( G |` B ) = G ) -> ( ( F |` A ) u. ( G |` B ) ) = ( F u. G ) )
4	1 2 3	syl2an	|- ( ( F Fn A /\ G Fn B ) -> ( ( F |` A ) u. ( G |` B ) ) = ( F u. G ) )
5	4	3adant3	|- ( ( F Fn A /\ G Fn B /\ ( F |` ( A i^i B ) ) = ( G |` ( A i^i B ) ) ) -> ( ( F |` A ) u. ( G |` B ) ) = ( F u. G ) )
6		inundif	|- ( ( A i^i B ) u. ( A \ B ) ) = A
7	6	reseq2i	|- ( F |` ( ( A i^i B ) u. ( A \ B ) ) ) = ( F |` A )
8		resundi	|- ( F |` ( ( A i^i B ) u. ( A \ B ) ) ) = ( ( F |` ( A i^i B ) ) u. ( F |` ( A \ B ) ) )
9	7 8	eqtr3i	|- ( F |` A ) = ( ( F |` ( A i^i B ) ) u. ( F |` ( A \ B ) ) )
10		incom	|- ( A i^i B ) = ( B i^i A )
11	10	uneq1i	|- ( ( A i^i B ) u. ( B \ A ) ) = ( ( B i^i A ) u. ( B \ A ) )
12		inundif	|- ( ( B i^i A ) u. ( B \ A ) ) = B
13	11 12	eqtri	|- ( ( A i^i B ) u. ( B \ A ) ) = B
14	13	reseq2i	|- ( G |` ( ( A i^i B ) u. ( B \ A ) ) ) = ( G |` B )
15		resundi	|- ( G |` ( ( A i^i B ) u. ( B \ A ) ) ) = ( ( G |` ( A i^i B ) ) u. ( G |` ( B \ A ) ) )
16	14 15	eqtr3i	|- ( G |` B ) = ( ( G |` ( A i^i B ) ) u. ( G |` ( B \ A ) ) )
17	9 16	uneq12i	|- ( ( F |` A ) u. ( G |` B ) ) = ( ( ( F |` ( A i^i B ) ) u. ( F |` ( A \ B ) ) ) u. ( ( G |` ( A i^i B ) ) u. ( G |` ( B \ A ) ) ) )
18		simp3	|- ( ( F Fn A /\ G Fn B /\ ( F |` ( A i^i B ) ) = ( G |` ( A i^i B ) ) ) -> ( F |` ( A i^i B ) ) = ( G |` ( A i^i B ) ) )
19	18	uneq1d	|- ( ( F Fn A /\ G Fn B /\ ( F |` ( A i^i B ) ) = ( G |` ( A i^i B ) ) ) -> ( ( F |` ( A i^i B ) ) u. ( G |` ( B \ A ) ) ) = ( ( G |` ( A i^i B ) ) u. ( G |` ( B \ A ) ) ) )
20	19	uneq2d	|- ( ( F Fn A /\ G Fn B /\ ( F |` ( A i^i B ) ) = ( G |` ( A i^i B ) ) ) -> ( ( ( F |` ( A i^i B ) ) u. ( F |` ( A \ B ) ) ) u. ( ( F |` ( A i^i B ) ) u. ( G |` ( B \ A ) ) ) ) = ( ( ( F |` ( A i^i B ) ) u. ( F |` ( A \ B ) ) ) u. ( ( G |` ( A i^i B ) ) u. ( G |` ( B \ A ) ) ) ) )
21	17 20	eqtr4id	|- ( ( F Fn A /\ G Fn B /\ ( F |` ( A i^i B ) ) = ( G |` ( A i^i B ) ) ) -> ( ( F |` A ) u. ( G |` B ) ) = ( ( ( F |` ( A i^i B ) ) u. ( F |` ( A \ B ) ) ) u. ( ( F |` ( A i^i B ) ) u. ( G |` ( B \ A ) ) ) ) )
22		un4	|- ( ( ( F |` ( A i^i B ) ) u. ( F |` ( A \ B ) ) ) u. ( ( F |` ( A i^i B ) ) u. ( G |` ( B \ A ) ) ) ) = ( ( ( F |` ( A i^i B ) ) u. ( F |` ( A i^i B ) ) ) u. ( ( F |` ( A \ B ) ) u. ( G |` ( B \ A ) ) ) )
23	21 22	eqtrdi	|- ( ( F Fn A /\ G Fn B /\ ( F |` ( A i^i B ) ) = ( G |` ( A i^i B ) ) ) -> ( ( F |` A ) u. ( G |` B ) ) = ( ( ( F |` ( A i^i B ) ) u. ( F |` ( A i^i B ) ) ) u. ( ( F |` ( A \ B ) ) u. ( G |` ( B \ A ) ) ) ) )
24		unidm	|- ( ( F |` ( A i^i B ) ) u. ( F |` ( A i^i B ) ) ) = ( F |` ( A i^i B ) )
25	24	uneq1i	|- ( ( ( F |` ( A i^i B ) ) u. ( F |` ( A i^i B ) ) ) u. ( ( F |` ( A \ B ) ) u. ( G |` ( B \ A ) ) ) ) = ( ( F |` ( A i^i B ) ) u. ( ( F |` ( A \ B ) ) u. ( G |` ( B \ A ) ) ) )
26	23 25	eqtrdi	|- ( ( F Fn A /\ G Fn B /\ ( F |` ( A i^i B ) ) = ( G |` ( A i^i B ) ) ) -> ( ( F |` A ) u. ( G |` B ) ) = ( ( F |` ( A i^i B ) ) u. ( ( F |` ( A \ B ) ) u. ( G |` ( B \ A ) ) ) ) )
27	5 26	eqtr3d	|- ( ( F Fn A /\ G Fn B /\ ( F |` ( A i^i B ) ) = ( G |` ( A i^i B ) ) ) -> ( F u. G ) = ( ( F |` ( A i^i B ) ) u. ( ( F |` ( A \ B ) ) u. ( G |` ( B \ A ) ) ) ) )