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 ∩ B = G ↾ A ∩ B → F ∪ G = F ↾ A ∩ B ∪ F ↾ A ∖ B ∪ 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 ∪ G ↾ B = F ∪ G
4 1 2 3 syl2an ⊢ F Fn A ∧ G Fn B → F ↾ A ∪ G ↾ B = F ∪ G
5 4 3adant3 ⊢ F Fn A ∧ G Fn B ∧ F ↾ A ∩ B = G ↾ A ∩ B → F ↾ A ∪ G ↾ B = F ∪ G
6 inundif ⊢ A ∩ B ∪ A ∖ B = A
7 6 reseq2i ⊢ F ↾ A ∩ B ∪ A ∖ B = F ↾ A
8 resundi ⊢ F ↾ A ∩ B ∪ A ∖ B = F ↾ A ∩ B ∪ F ↾ A ∖ B
9 7 8 eqtr3i ⊢ F ↾ A = F ↾ A ∩ B ∪ F ↾ A ∖ B
10 incom ⊢ A ∩ B = B ∩ A
11 10 uneq1i ⊢ A ∩ B ∪ B ∖ A = B ∩ A ∪ B ∖ A
12 inundif ⊢ B ∩ A ∪ B ∖ A = B
13 11 12 eqtri ⊢ A ∩ B ∪ B ∖ A = B
14 13 reseq2i ⊢ G ↾ A ∩ B ∪ B ∖ A = G ↾ B
15 resundi ⊢ G ↾ A ∩ B ∪ B ∖ A = G ↾ A ∩ B ∪ G ↾ B ∖ A
16 14 15 eqtr3i ⊢ G ↾ B = G ↾ A ∩ B ∪ G ↾ B ∖ A
17 9 16 uneq12i ⊢ F ↾ A ∪ G ↾ B = F ↾ A ∩ B ∪ F ↾ A ∖ B ∪ G ↾ A ∩ B ∪ G ↾ B ∖ A
18 simp3 ⊢ F Fn A ∧ G Fn B ∧ F ↾ A ∩ B = G ↾ A ∩ B → F ↾ A ∩ B = G ↾ A ∩ B
19 18 uneq1d ⊢ F Fn A ∧ G Fn B ∧ F ↾ A ∩ B = G ↾ A ∩ B → F ↾ A ∩ B ∪ G ↾ B ∖ A = G ↾ A ∩ B ∪ G ↾ B ∖ A
20 19 uneq2d ⊢ F Fn A ∧ G Fn B ∧ F ↾ A ∩ B = G ↾ A ∩ B → F ↾ A ∩ B ∪ F ↾ A ∖ B ∪ F ↾ A ∩ B ∪ G ↾ B ∖ A = F ↾ A ∩ B ∪ F ↾ A ∖ B ∪ G ↾ A ∩ B ∪ G ↾ B ∖ A
21 17 20 eqtr4id ⊢ F Fn A ∧ G Fn B ∧ F ↾ A ∩ B = G ↾ A ∩ B → F ↾ A ∪ G ↾ B = F ↾ A ∩ B ∪ F ↾ A ∖ B ∪ F ↾ A ∩ B ∪ G ↾ B ∖ A
22 un4 ⊢ F ↾ A ∩ B ∪ F ↾ A ∖ B ∪ F ↾ A ∩ B ∪ G ↾ B ∖ A = F ↾ A ∩ B ∪ F ↾ A ∩ B ∪ F ↾ A ∖ B ∪ G ↾ B ∖ A
23 21 22 eqtrdi ⊢ F Fn A ∧ G Fn B ∧ F ↾ A ∩ B = G ↾ A ∩ B → F ↾ A ∪ G ↾ B = F ↾ A ∩ B ∪ F ↾ A ∩ B ∪ F ↾ A ∖ B ∪ G ↾ B ∖ A
24 unidm ⊢ F ↾ A ∩ B ∪ F ↾ A ∩ B = F ↾ A ∩ B
25 24 uneq1i ⊢ F ↾ A ∩ B ∪ F ↾ A ∩ B ∪ F ↾ A ∖ B ∪ G ↾ B ∖ A = F ↾ A ∩ B ∪ F ↾ A ∖ B ∪ G ↾ B ∖ A
26 23 25 eqtrdi ⊢ F Fn A ∧ G Fn B ∧ F ↾ A ∩ B = G ↾ A ∩ B → F ↾ A ∪ G ↾ B = F ↾ A ∩ B ∪ F ↾ A ∖ B ∪ G ↾ B ∖ A
27 5 26 eqtr3d ⊢ F Fn A ∧ G Fn B ∧ F ↾ A ∩ B = G ↾ A ∩ B → F ∪ G = F ↾ A ∩ B ∪ F ↾ A ∖ B ∪ G ↾ B ∖ A