fresaunres2

Description: From the union of two functions that agree on the domain overlap, either component can be recovered by restriction. (Contributed by Stefan O'Rear, 9-Oct-2014)

		Ref	Expression
	Assertion	fresaunres2	$⊢ (F : A ⟶ C \land G : B ⟶ C \land {F ↾}_{(A \cap B)} = {G ↾}_{(A \cap B)}) \to {(F \cup G) ↾}_{B} = G$

Proof

Step	Hyp	Ref	Expression
1		ffn	$⊢ F : A ⟶ C \to F Fn A$
2		ffn	$⊢ G : B ⟶ C \to G Fn B$
3		id	$⊢ {F ↾}_{(A \cap B)} = {G ↾}_{(A \cap B)} \to {F ↾}_{(A \cap B)} = {G ↾}_{(A \cap B)}$
4		resasplit	$⊢ (F Fn A \land G Fn B \land {F ↾}_{(A \cap B)} = {G ↾}_{(A \cap B)}) \to F \cup G = ({F ↾}_{(A \cap B)}) \cup (({F ↾}_{(A ∖ B)}) \cup ({G ↾}_{(B ∖ A)}))$
5	1 2 3 4	syl3an	$⊢ (F : A ⟶ C \land G : B ⟶ C \land {F ↾}_{(A \cap B)} = {G ↾}_{(A \cap B)}) \to F \cup G = ({F ↾}_{(A \cap B)}) \cup (({F ↾}_{(A ∖ B)}) \cup ({G ↾}_{(B ∖ A)}))$
6	5	reseq1d	$⊢ (F : A ⟶ C \land G : B ⟶ C \land {F ↾}_{(A \cap B)} = {G ↾}_{(A \cap B)}) \to {(F \cup G) ↾}_{B} = {(({F ↾}_{(A \cap B)}) \cup (({F ↾}_{(A ∖ B)}) \cup ({G ↾}_{(B ∖ A)}))) ↾}_{B}$
7		resundir	$⊢ {(({F ↾}_{(A \cap B)}) \cup (({F ↾}_{(A ∖ B)}) \cup ({G ↾}_{(B ∖ A)}))) ↾}_{B} = ({({F ↾}_{(A \cap B)}) ↾}_{B}) \cup ({(({F ↾}_{(A ∖ B)}) \cup ({G ↾}_{(B ∖ A)})) ↾}_{B})$
8		inss2	$⊢ A \cap B \subseteq B$
9		resabs2	$⊢ A \cap B \subseteq B \to {({F ↾}_{(A \cap B)}) ↾}_{B} = {F ↾}_{(A \cap B)}$
10	8 9	ax-mp	$⊢ {({F ↾}_{(A \cap B)}) ↾}_{B} = {F ↾}_{(A \cap B)}$
11		resundir	$⊢ {(({F ↾}_{(A ∖ B)}) \cup ({G ↾}_{(B ∖ A)})) ↾}_{B} = ({({F ↾}_{(A ∖ B)}) ↾}_{B}) \cup ({({G ↾}_{(B ∖ A)}) ↾}_{B})$
12	10 11	uneq12i	$⊢ ({({F ↾}_{(A \cap B)}) ↾}_{B}) \cup ({(({F ↾}_{(A ∖ B)}) \cup ({G ↾}_{(B ∖ A)})) ↾}_{B}) = ({F ↾}_{(A \cap B)}) \cup (({({F ↾}_{(A ∖ B)}) ↾}_{B}) \cup ({({G ↾}_{(B ∖ A)}) ↾}_{B}))$
13		dmres	$⊢ dom ({({F ↾}_{(A ∖ B)}) ↾}_{B}) = B \cap dom ({F ↾}_{(A ∖ B)})$
14		dmres	$⊢ dom ({F ↾}_{(A ∖ B)}) = (A ∖ B) \cap dom F$
15	14	ineq2i	$⊢ B \cap dom ({F ↾}_{(A ∖ B)}) = B \cap ((A ∖ B) \cap dom F)$
16		disjdif	$⊢ B \cap (A ∖ B) = \emptyset$
17	16	ineq1i	$⊢ (B \cap (A ∖ B)) \cap dom F = \emptyset \cap dom F$
18		inass	$⊢ (B \cap (A ∖ B)) \cap dom F = B \cap ((A ∖ B) \cap dom F)$
19		0in	$⊢ \emptyset \cap dom F = \emptyset$
20	17 18 19	3eqtr3i	$⊢ B \cap ((A ∖ B) \cap dom F) = \emptyset$
21	15 20	eqtri	$⊢ B \cap dom ({F ↾}_{(A ∖ B)}) = \emptyset$
22	13 21	eqtri	$⊢ dom ({({F ↾}_{(A ∖ B)}) ↾}_{B}) = \emptyset$
23		relres	$⊢ Rel ({({F ↾}_{(A ∖ B)}) ↾}_{B})$
24		reldm0	$⊢ Rel ({({F ↾}_{(A ∖ B)}) ↾}_{B}) \to ({({F ↾}_{(A ∖ B)}) ↾}_{B} = \emptyset \leftrightarrow dom ({({F ↾}_{(A ∖ B)}) ↾}_{B}) = \emptyset)$
25	23 24	ax-mp	$⊢ {({F ↾}_{(A ∖ B)}) ↾}_{B} = \emptyset \leftrightarrow dom ({({F ↾}_{(A ∖ B)}) ↾}_{B}) = \emptyset$
26	22 25	mpbir	$⊢ {({F ↾}_{(A ∖ B)}) ↾}_{B} = \emptyset$
27		difss	$⊢ B ∖ A \subseteq B$
28		resabs2	$⊢ B ∖ A \subseteq B \to {({G ↾}_{(B ∖ A)}) ↾}_{B} = {G ↾}_{(B ∖ A)}$
29	27 28	ax-mp	$⊢ {({G ↾}_{(B ∖ A)}) ↾}_{B} = {G ↾}_{(B ∖ A)}$
30	26 29	uneq12i	$⊢ ({({F ↾}_{(A ∖ B)}) ↾}_{B}) \cup ({({G ↾}_{(B ∖ A)}) ↾}_{B}) = \emptyset \cup ({G ↾}_{(B ∖ A)})$
31	30	uneq2i	$⊢ ({F ↾}_{(A \cap B)}) \cup (({({F ↾}_{(A ∖ B)}) ↾}_{B}) \cup ({({G ↾}_{(B ∖ A)}) ↾}_{B})) = ({F ↾}_{(A \cap B)}) \cup (\emptyset \cup ({G ↾}_{(B ∖ A)}))$
32		simp3	$⊢ (F : A ⟶ C \land G : B ⟶ C \land {F ↾}_{(A \cap B)} = {G ↾}_{(A \cap B)}) \to {F ↾}_{(A \cap B)} = {G ↾}_{(A \cap B)}$
33	32	uneq1d	$⊢ (F : A ⟶ C \land G : B ⟶ C \land {F ↾}_{(A \cap B)} = {G ↾}_{(A \cap B)}) \to ({F ↾}_{(A \cap B)}) \cup (\emptyset \cup ({G ↾}_{(B ∖ A)})) = ({G ↾}_{(A \cap B)}) \cup (\emptyset \cup ({G ↾}_{(B ∖ A)}))$
34		uncom	$⊢ \emptyset \cup ({G ↾}_{(B ∖ A)}) = ({G ↾}_{(B ∖ A)}) \cup \emptyset$
35		un0	$⊢ ({G ↾}_{(B ∖ A)}) \cup \emptyset = {G ↾}_{(B ∖ A)}$
36	34 35	eqtri	$⊢ \emptyset \cup ({G ↾}_{(B ∖ A)}) = {G ↾}_{(B ∖ A)}$
37	36	uneq2i	$⊢ ({G ↾}_{(A \cap B)}) \cup (\emptyset \cup ({G ↾}_{(B ∖ A)})) = ({G ↾}_{(A \cap B)}) \cup ({G ↾}_{(B ∖ A)})$
38		resundi	$⊢ {G ↾}_{((A \cap B) \cup (B ∖ A))} = ({G ↾}_{(A \cap B)}) \cup ({G ↾}_{(B ∖ A)})$
39		incom	$⊢ A \cap B = B \cap A$
40	39	uneq1i	$⊢ (A \cap B) \cup (B ∖ A) = (B \cap A) \cup (B ∖ A)$
41		inundif	$⊢ (B \cap A) \cup (B ∖ A) = B$
42	40 41	eqtri	$⊢ (A \cap B) \cup (B ∖ A) = B$
43	42	reseq2i	$⊢ {G ↾}_{((A \cap B) \cup (B ∖ A))} = {G ↾}_{B}$
44		fnresdm	$⊢ G Fn B \to {G ↾}_{B} = G$
45	2 44	syl	$⊢ G : B ⟶ C \to {G ↾}_{B} = G$
46	45	adantl	$⊢ (F : A ⟶ C \land G : B ⟶ C) \to {G ↾}_{B} = G$
47	43 46	eqtrid	$⊢ (F : A ⟶ C \land G : B ⟶ C) \to {G ↾}_{((A \cap B) \cup (B ∖ A))} = G$
48	38 47	eqtr3id	$⊢ (F : A ⟶ C \land G : B ⟶ C) \to ({G ↾}_{(A \cap B)}) \cup ({G ↾}_{(B ∖ A)}) = G$
49	37 48	eqtrid	$⊢ (F : A ⟶ C \land G : B ⟶ C) \to ({G ↾}_{(A \cap B)}) \cup (\emptyset \cup ({G ↾}_{(B ∖ A)})) = G$
50	49	3adant3	$⊢ (F : A ⟶ C \land G : B ⟶ C \land {F ↾}_{(A \cap B)} = {G ↾}_{(A \cap B)}) \to ({G ↾}_{(A \cap B)}) \cup (\emptyset \cup ({G ↾}_{(B ∖ A)})) = G$
51	33 50	eqtrd	$⊢ (F : A ⟶ C \land G : B ⟶ C \land {F ↾}_{(A \cap B)} = {G ↾}_{(A \cap B)}) \to ({F ↾}_{(A \cap B)}) \cup (\emptyset \cup ({G ↾}_{(B ∖ A)})) = G$
52	31 51	eqtrid	$⊢ (F : A ⟶ C \land G : B ⟶ C \land {F ↾}_{(A \cap B)} = {G ↾}_{(A \cap B)}) \to ({F ↾}_{(A \cap B)}) \cup (({({F ↾}_{(A ∖ B)}) ↾}_{B}) \cup ({({G ↾}_{(B ∖ A)}) ↾}_{B})) = G$
53	12 52	eqtrid	$⊢ (F : A ⟶ C \land G : B ⟶ C \land {F ↾}_{(A \cap B)} = {G ↾}_{(A \cap B)}) \to ({({F ↾}_{(A \cap B)}) ↾}_{B}) \cup ({(({F ↾}_{(A ∖ B)}) \cup ({G ↾}_{(B ∖ A)})) ↾}_{B}) = G$
54	7 53	eqtrid	$⊢ (F : A ⟶ C \land G : B ⟶ C \land {F ↾}_{(A \cap B)} = {G ↾}_{(A \cap B)}) \to {(({F ↾}_{(A \cap B)}) \cup (({F ↾}_{(A ∖ B)}) \cup ({G ↾}_{(B ∖ A)}))) ↾}_{B} = G$
55	6 54	eqtrd	$⊢ (F : A ⟶ C \land G : B ⟶ C \land {F ↾}_{(A \cap B)} = {G ↾}_{(A \cap B)}) \to {(F \cup G) ↾}_{B} = G$

Metamath Proof Explorer

Theorem fresaunres2

Proof