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 ( ( 𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐵 ∧ ( 𝐹 ↾ ( 𝐴 ∩ 𝐵 ) ) = ( 𝐺 ↾ ( 𝐴 ∩ 𝐵 ) ) ) → ( 𝐹 ∪ 𝐺 ) = ( ( 𝐹 ↾ ( 𝐴 ∩ 𝐵 ) ) ∪ ( ( 𝐹 ↾ ( 𝐴 ∖ 𝐵 ) ) ∪ ( 𝐺 ↾ ( 𝐵 ∖ 𝐴 ) ) ) ) )

Proof

Step Hyp Ref Expression
1 fnresdm ⊢ ( 𝐹 Fn 𝐴 → ( 𝐹 ↾ 𝐴 ) = 𝐹 )
2 fnresdm ⊢ ( 𝐺 Fn 𝐵 → ( 𝐺 ↾ 𝐵 ) = 𝐺 )
3 uneq12 ⊢ ( ( ( 𝐹 ↾ 𝐴 ) = 𝐹 ∧ ( 𝐺 ↾ 𝐵 ) = 𝐺 ) → ( ( 𝐹 ↾ 𝐴 ) ∪ ( 𝐺 ↾ 𝐵 ) ) = ( 𝐹 ∪ 𝐺 ) )
4 1 2 3 syl2an ⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐵 ) → ( ( 𝐹 ↾ 𝐴 ) ∪ ( 𝐺 ↾ 𝐵 ) ) = ( 𝐹 ∪ 𝐺 ) )
5 4 3adant3 ⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐵 ∧ ( 𝐹 ↾ ( 𝐴 ∩ 𝐵 ) ) = ( 𝐺 ↾ ( 𝐴 ∩ 𝐵 ) ) ) → ( ( 𝐹 ↾ 𝐴 ) ∪ ( 𝐺 ↾ 𝐵 ) ) = ( 𝐹 ∪ 𝐺 ) )
6 inundif ⊢ ( ( 𝐴 ∩ 𝐵 ) ∪ ( 𝐴 ∖ 𝐵 ) ) = 𝐴
7 6 reseq2i ⊢ ( 𝐹 ↾ ( ( 𝐴 ∩ 𝐵 ) ∪ ( 𝐴 ∖ 𝐵 ) ) ) = ( 𝐹 ↾ 𝐴 )
8 resundi ⊢ ( 𝐹 ↾ ( ( 𝐴 ∩ 𝐵 ) ∪ ( 𝐴 ∖ 𝐵 ) ) ) = ( ( 𝐹 ↾ ( 𝐴 ∩ 𝐵 ) ) ∪ ( 𝐹 ↾ ( 𝐴 ∖ 𝐵 ) ) )
9 7 8 eqtr3i ⊢ ( 𝐹 ↾ 𝐴 ) = ( ( 𝐹 ↾ ( 𝐴 ∩ 𝐵 ) ) ∪ ( 𝐹 ↾ ( 𝐴 ∖ 𝐵 ) ) )
10 incom ⊢ ( 𝐴 ∩ 𝐵 ) = ( 𝐵 ∩ 𝐴 )
11 10 uneq1i ⊢ ( ( 𝐴 ∩ 𝐵 ) ∪ ( 𝐵 ∖ 𝐴 ) ) = ( ( 𝐵 ∩ 𝐴 ) ∪ ( 𝐵 ∖ 𝐴 ) )
12 inundif ⊢ ( ( 𝐵 ∩ 𝐴 ) ∪ ( 𝐵 ∖ 𝐴 ) ) = 𝐵
13 11 12 eqtri ⊢ ( ( 𝐴 ∩ 𝐵 ) ∪ ( 𝐵 ∖ 𝐴 ) ) = 𝐵
14 13 reseq2i ⊢ ( 𝐺 ↾ ( ( 𝐴 ∩ 𝐵 ) ∪ ( 𝐵 ∖ 𝐴 ) ) ) = ( 𝐺 ↾ 𝐵 )
15 resundi ⊢ ( 𝐺 ↾ ( ( 𝐴 ∩ 𝐵 ) ∪ ( 𝐵 ∖ 𝐴 ) ) ) = ( ( 𝐺 ↾ ( 𝐴 ∩ 𝐵 ) ) ∪ ( 𝐺 ↾ ( 𝐵 ∖ 𝐴 ) ) )
16 14 15 eqtr3i ⊢ ( 𝐺 ↾ 𝐵 ) = ( ( 𝐺 ↾ ( 𝐴 ∩ 𝐵 ) ) ∪ ( 𝐺 ↾ ( 𝐵 ∖ 𝐴 ) ) )
17 9 16 uneq12i ⊢ ( ( 𝐹 ↾ 𝐴 ) ∪ ( 𝐺 ↾ 𝐵 ) ) = ( ( ( 𝐹 ↾ ( 𝐴 ∩ 𝐵 ) ) ∪ ( 𝐹 ↾ ( 𝐴 ∖ 𝐵 ) ) ) ∪ ( ( 𝐺 ↾ ( 𝐴 ∩ 𝐵 ) ) ∪ ( 𝐺 ↾ ( 𝐵 ∖ 𝐴 ) ) ) )
18 simp3 ⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐵 ∧ ( 𝐹 ↾ ( 𝐴 ∩ 𝐵 ) ) = ( 𝐺 ↾ ( 𝐴 ∩ 𝐵 ) ) ) → ( 𝐹 ↾ ( 𝐴 ∩ 𝐵 ) ) = ( 𝐺 ↾ ( 𝐴 ∩ 𝐵 ) ) )
19 18 uneq1d ⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐵 ∧ ( 𝐹 ↾ ( 𝐴 ∩ 𝐵 ) ) = ( 𝐺 ↾ ( 𝐴 ∩ 𝐵 ) ) ) → ( ( 𝐹 ↾ ( 𝐴 ∩ 𝐵 ) ) ∪ ( 𝐺 ↾ ( 𝐵 ∖ 𝐴 ) ) ) = ( ( 𝐺 ↾ ( 𝐴 ∩ 𝐵 ) ) ∪ ( 𝐺 ↾ ( 𝐵 ∖ 𝐴 ) ) ) )
20 19 uneq2d ⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐵 ∧ ( 𝐹 ↾ ( 𝐴 ∩ 𝐵 ) ) = ( 𝐺 ↾ ( 𝐴 ∩ 𝐵 ) ) ) → ( ( ( 𝐹 ↾ ( 𝐴 ∩ 𝐵 ) ) ∪ ( 𝐹 ↾ ( 𝐴 ∖ 𝐵 ) ) ) ∪ ( ( 𝐹 ↾ ( 𝐴 ∩ 𝐵 ) ) ∪ ( 𝐺 ↾ ( 𝐵 ∖ 𝐴 ) ) ) ) = ( ( ( 𝐹 ↾ ( 𝐴 ∩ 𝐵 ) ) ∪ ( 𝐹 ↾ ( 𝐴 ∖ 𝐵 ) ) ) ∪ ( ( 𝐺 ↾ ( 𝐴 ∩ 𝐵 ) ) ∪ ( 𝐺 ↾ ( 𝐵 ∖ 𝐴 ) ) ) ) )
21 17 20 eqtr4id ⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐵 ∧ ( 𝐹 ↾ ( 𝐴 ∩ 𝐵 ) ) = ( 𝐺 ↾ ( 𝐴 ∩ 𝐵 ) ) ) → ( ( 𝐹 ↾ 𝐴 ) ∪ ( 𝐺 ↾ 𝐵 ) ) = ( ( ( 𝐹 ↾ ( 𝐴 ∩ 𝐵 ) ) ∪ ( 𝐹 ↾ ( 𝐴 ∖ 𝐵 ) ) ) ∪ ( ( 𝐹 ↾ ( 𝐴 ∩ 𝐵 ) ) ∪ ( 𝐺 ↾ ( 𝐵 ∖ 𝐴 ) ) ) ) )
22 un4 ⊢ ( ( ( 𝐹 ↾ ( 𝐴 ∩ 𝐵 ) ) ∪ ( 𝐹 ↾ ( 𝐴 ∖ 𝐵 ) ) ) ∪ ( ( 𝐹 ↾ ( 𝐴 ∩ 𝐵 ) ) ∪ ( 𝐺 ↾ ( 𝐵 ∖ 𝐴 ) ) ) ) = ( ( ( 𝐹 ↾ ( 𝐴 ∩ 𝐵 ) ) ∪ ( 𝐹 ↾ ( 𝐴 ∩ 𝐵 ) ) ) ∪ ( ( 𝐹 ↾ ( 𝐴 ∖ 𝐵 ) ) ∪ ( 𝐺 ↾ ( 𝐵 ∖ 𝐴 ) ) ) )
23 21 22 eqtrdi ⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐵 ∧ ( 𝐹 ↾ ( 𝐴 ∩ 𝐵 ) ) = ( 𝐺 ↾ ( 𝐴 ∩ 𝐵 ) ) ) → ( ( 𝐹 ↾ 𝐴 ) ∪ ( 𝐺 ↾ 𝐵 ) ) = ( ( ( 𝐹 ↾ ( 𝐴 ∩ 𝐵 ) ) ∪ ( 𝐹 ↾ ( 𝐴 ∩ 𝐵 ) ) ) ∪ ( ( 𝐹 ↾ ( 𝐴 ∖ 𝐵 ) ) ∪ ( 𝐺 ↾ ( 𝐵 ∖ 𝐴 ) ) ) ) )
24 unidm ⊢ ( ( 𝐹 ↾ ( 𝐴 ∩ 𝐵 ) ) ∪ ( 𝐹 ↾ ( 𝐴 ∩ 𝐵 ) ) ) = ( 𝐹 ↾ ( 𝐴 ∩ 𝐵 ) )
25 24 uneq1i ⊢ ( ( ( 𝐹 ↾ ( 𝐴 ∩ 𝐵 ) ) ∪ ( 𝐹 ↾ ( 𝐴 ∩ 𝐵 ) ) ) ∪ ( ( 𝐹 ↾ ( 𝐴 ∖ 𝐵 ) ) ∪ ( 𝐺 ↾ ( 𝐵 ∖ 𝐴 ) ) ) ) = ( ( 𝐹 ↾ ( 𝐴 ∩ 𝐵 ) ) ∪ ( ( 𝐹 ↾ ( 𝐴 ∖ 𝐵 ) ) ∪ ( 𝐺 ↾ ( 𝐵 ∖ 𝐴 ) ) ) )
26 23 25 eqtrdi ⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐵 ∧ ( 𝐹 ↾ ( 𝐴 ∩ 𝐵 ) ) = ( 𝐺 ↾ ( 𝐴 ∩ 𝐵 ) ) ) → ( ( 𝐹 ↾ 𝐴 ) ∪ ( 𝐺 ↾ 𝐵 ) ) = ( ( 𝐹 ↾ ( 𝐴 ∩ 𝐵 ) ) ∪ ( ( 𝐹 ↾ ( 𝐴 ∖ 𝐵 ) ) ∪ ( 𝐺 ↾ ( 𝐵 ∖ 𝐴 ) ) ) ) )
27 5 26 eqtr3d ⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐵 ∧ ( 𝐹 ↾ ( 𝐴 ∩ 𝐵 ) ) = ( 𝐺 ↾ ( 𝐴 ∩ 𝐵 ) ) ) → ( 𝐹 ∪ 𝐺 ) = ( ( 𝐹 ↾ ( 𝐴 ∩ 𝐵 ) ) ∪ ( ( 𝐹 ↾ ( 𝐴 ∖ 𝐵 ) ) ∪ ( 𝐺 ↾ ( 𝐵 ∖ 𝐴 ) ) ) ) )