This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ) ) ) ) )