i1faddlem

Description: Decompose the preimage of a sum. (Contributed by Mario Carneiro, 19-Jun-2014)

	Ref	Expression
Hypotheses	i1fadd.1	$⊢ φ \to F \in dom \int^{1}$
	i1fadd.2	$⊢ φ \to G \in dom \int^{1}$
Assertion	i1faddlem	$⊢ (φ \land A \in ℂ) \to {(F +_{f} G)}^{-1} [\{A\}] = ⋃_{y \in ran G} (F^{-1} [\{A - y\}] \cap G^{-1} [\{y\}])$

Proof

Step	Hyp	Ref	Expression
1		i1fadd.1	$⊢ φ \to F \in dom \int^{1}$
2		i1fadd.2	$⊢ φ \to G \in dom \int^{1}$
3		i1ff	$⊢ F \in dom \int^{1} \to F : ℝ ⟶ ℝ$
4	1 3	syl	$⊢ φ \to F : ℝ ⟶ ℝ$
5	4	ffnd	$⊢ φ \to F Fn ℝ$
6		i1ff	$⊢ G \in dom \int^{1} \to G : ℝ ⟶ ℝ$
7	2 6	syl	$⊢ φ \to G : ℝ ⟶ ℝ$
8	7	ffnd	$⊢ φ \to G Fn ℝ$
9		reex	$⊢ ℝ \in V$
10	9	a1i	$⊢ φ \to ℝ \in V$
11		inidm	$⊢ ℝ \cap ℝ = ℝ$
12	5 8 10 10 11	offn	$⊢ φ \to (F +_{f} G) Fn ℝ$
13	12	adantr	$⊢ (φ \land A \in ℂ) \to (F +_{f} G) Fn ℝ$
14		fniniseg	$⊢ (F +_{f} G) Fn ℝ \to (z \in {(F +_{f} G)}^{-1} [\{A\}] \leftrightarrow (z \in ℝ \land (F +_{f} G) (z) = A))$
15	13 14	syl	$⊢ (φ \land A \in ℂ) \to (z \in {(F +_{f} G)}^{-1} [\{A\}] \leftrightarrow (z \in ℝ \land (F +_{f} G) (z) = A))$
16	8	ad2antrr	$⊢ ((φ \land A \in ℂ) \land (z \in ℝ \land (F +_{f} G) (z) = A)) \to G Fn ℝ$
17		simprl	$⊢ ((φ \land A \in ℂ) \land (z \in ℝ \land (F +_{f} G) (z) = A)) \to z \in ℝ$
18		fnfvelrn	$⊢ (G Fn ℝ \land z \in ℝ) \to G (z) \in ran G$
19	16 17 18	syl2anc	$⊢ ((φ \land A \in ℂ) \land (z \in ℝ \land (F +_{f} G) (z) = A)) \to G (z) \in ran G$
20		simprr	$⊢ ((φ \land A \in ℂ) \land (z \in ℝ \land (F +_{f} G) (z) = A)) \to (F +_{f} G) (z) = A$
21		eqidd	$⊢ (φ \land z \in ℝ) \to F (z) = F (z)$
22		eqidd	$⊢ (φ \land z \in ℝ) \to G (z) = G (z)$
23	5 8 10 10 11 21 22	ofval	$⊢ (φ \land z \in ℝ) \to (F +_{f} G) (z) = F (z) + G (z)$
24	23	ad2ant2r	$⊢ ((φ \land A \in ℂ) \land (z \in ℝ \land (F +_{f} G) (z) = A)) \to (F +_{f} G) (z) = F (z) + G (z)$
25	20 24	eqtr3d	$⊢ ((φ \land A \in ℂ) \land (z \in ℝ \land (F +_{f} G) (z) = A)) \to A = F (z) + G (z)$
26	25	oveq1d	$⊢ ((φ \land A \in ℂ) \land (z \in ℝ \land (F +_{f} G) (z) = A)) \to A - G (z) = F (z) + G (z) - G (z)$
27		ax-resscn	$⊢ ℝ \subseteq ℂ$
28		fss	$⊢ (F : ℝ ⟶ ℝ \land ℝ \subseteq ℂ) \to F : ℝ ⟶ ℂ$
29	4 27 28	sylancl	$⊢ φ \to F : ℝ ⟶ ℂ$
30	29	ad2antrr	$⊢ ((φ \land A \in ℂ) \land (z \in ℝ \land (F +_{f} G) (z) = A)) \to F : ℝ ⟶ ℂ$
31	30 17	ffvelrnd	$⊢ ((φ \land A \in ℂ) \land (z \in ℝ \land (F +_{f} G) (z) = A)) \to F (z) \in ℂ$
32		fss	$⊢ (G : ℝ ⟶ ℝ \land ℝ \subseteq ℂ) \to G : ℝ ⟶ ℂ$
33	7 27 32	sylancl	$⊢ φ \to G : ℝ ⟶ ℂ$
34	33	ad2antrr	$⊢ ((φ \land A \in ℂ) \land (z \in ℝ \land (F +_{f} G) (z) = A)) \to G : ℝ ⟶ ℂ$
35	34 17	ffvelrnd	$⊢ ((φ \land A \in ℂ) \land (z \in ℝ \land (F +_{f} G) (z) = A)) \to G (z) \in ℂ$
36	31 35	pncand	$⊢ ((φ \land A \in ℂ) \land (z \in ℝ \land (F +_{f} G) (z) = A)) \to F (z) + G (z) - G (z) = F (z)$
37	26 36	eqtr2d	$⊢ ((φ \land A \in ℂ) \land (z \in ℝ \land (F +_{f} G) (z) = A)) \to F (z) = A - G (z)$
38	5	ad2antrr	$⊢ ((φ \land A \in ℂ) \land (z \in ℝ \land (F +_{f} G) (z) = A)) \to F Fn ℝ$
39		fniniseg	$⊢ F Fn ℝ \to (z \in F^{-1} [\{A - G (z)\}] \leftrightarrow (z \in ℝ \land F (z) = A - G (z)))$
40	38 39	syl	$⊢ ((φ \land A \in ℂ) \land (z \in ℝ \land (F +_{f} G) (z) = A)) \to (z \in F^{-1} [\{A - G (z)\}] \leftrightarrow (z \in ℝ \land F (z) = A - G (z)))$
41	17 37 40	mpbir2and	$⊢ ((φ \land A \in ℂ) \land (z \in ℝ \land (F +_{f} G) (z) = A)) \to z \in F^{-1} [\{A - G (z)\}]$
42		eqidd	$⊢ ((φ \land A \in ℂ) \land (z \in ℝ \land (F +_{f} G) (z) = A)) \to G (z) = G (z)$
43		fniniseg	$⊢ G Fn ℝ \to (z \in G^{-1} [\{G (z)\}] \leftrightarrow (z \in ℝ \land G (z) = G (z)))$
44	16 43	syl	$⊢ ((φ \land A \in ℂ) \land (z \in ℝ \land (F +_{f} G) (z) = A)) \to (z \in G^{-1} [\{G (z)\}] \leftrightarrow (z \in ℝ \land G (z) = G (z)))$
45	17 42 44	mpbir2and	$⊢ ((φ \land A \in ℂ) \land (z \in ℝ \land (F +_{f} G) (z) = A)) \to z \in G^{-1} [\{G (z)\}]$
46	41 45	elind	$⊢ ((φ \land A \in ℂ) \land (z \in ℝ \land (F +_{f} G) (z) = A)) \to z \in (F^{-1} [\{A - G (z)\}] \cap G^{-1} [\{G (z)\}])$
47		oveq2	$⊢ y = G (z) \to A - y = A - G (z)$
48	47	sneqd	$⊢ y = G (z) \to \{A - y\} = \{A - G (z)\}$
49	48	imaeq2d	$⊢ y = G (z) \to F^{-1} [\{A - y\}] = F^{-1} [\{A - G (z)\}]$
50		sneq	$⊢ y = G (z) \to \{y\} = \{G (z)\}$
51	50	imaeq2d	$⊢ y = G (z) \to G^{-1} [\{y\}] = G^{-1} [\{G (z)\}]$
52	49 51	ineq12d	$⊢ y = G (z) \to F^{-1} [\{A - y\}] \cap G^{-1} [\{y\}] = F^{-1} [\{A - G (z)\}] \cap G^{-1} [\{G (z)\}]$
53	52	eleq2d	$⊢ y = G (z) \to (z \in (F^{-1} [\{A - y\}] \cap G^{-1} [\{y\}]) \leftrightarrow z \in (F^{-1} [\{A - G (z)\}] \cap G^{-1} [\{G (z)\}]))$
54	53	rspcev	$⊢ (G (z) \in ran G \land z \in (F^{-1} [\{A - G (z)\}] \cap G^{-1} [\{G (z)\}])) \to \exists y \in ran G z \in (F^{-1} [\{A - y\}] \cap G^{-1} [\{y\}])$
55	19 46 54	syl2anc	$⊢ ((φ \land A \in ℂ) \land (z \in ℝ \land (F +_{f} G) (z) = A)) \to \exists y \in ran G z \in (F^{-1} [\{A - y\}] \cap G^{-1} [\{y\}])$
56	55	ex	$⊢ (φ \land A \in ℂ) \to ((z \in ℝ \land (F +_{f} G) (z) = A) \to \exists y \in ran G z \in (F^{-1} [\{A - y\}] \cap G^{-1} [\{y\}]))$
57		elin	$⊢ z \in (F^{-1} [\{A - y\}] \cap G^{-1} [\{y\}]) \leftrightarrow (z \in F^{-1} [\{A - y\}] \land z \in G^{-1} [\{y\}])$
58	5	adantr	$⊢ (φ \land A \in ℂ) \to F Fn ℝ$
59		fniniseg	$⊢ F Fn ℝ \to (z \in F^{-1} [\{A - y\}] \leftrightarrow (z \in ℝ \land F (z) = A - y))$
60	58 59	syl	$⊢ (φ \land A \in ℂ) \to (z \in F^{-1} [\{A - y\}] \leftrightarrow (z \in ℝ \land F (z) = A - y))$
61	8	adantr	$⊢ (φ \land A \in ℂ) \to G Fn ℝ$
62		fniniseg	$⊢ G Fn ℝ \to (z \in G^{-1} [\{y\}] \leftrightarrow (z \in ℝ \land G (z) = y))$
63	61 62	syl	$⊢ (φ \land A \in ℂ) \to (z \in G^{-1} [\{y\}] \leftrightarrow (z \in ℝ \land G (z) = y))$
64	60 63	anbi12d	$⊢ (φ \land A \in ℂ) \to ((z \in F^{-1} [\{A - y\}] \land z \in G^{-1} [\{y\}]) \leftrightarrow ((z \in ℝ \land F (z) = A - y) \land (z \in ℝ \land G (z) = y)))$
65		anandi	$⊢ (z \in ℝ \land (F (z) = A - y \land G (z) = y)) \leftrightarrow ((z \in ℝ \land F (z) = A - y) \land (z \in ℝ \land G (z) = y))$
66		simprl	$⊢ ((φ \land A \in ℂ) \land (z \in ℝ \land (F (z) = A - y \land G (z) = y))) \to z \in ℝ$
67	23	ad2ant2r	$⊢ ((φ \land A \in ℂ) \land (z \in ℝ \land (F (z) = A - y \land G (z) = y))) \to (F +_{f} G) (z) = F (z) + G (z)$
68		simprrl	$⊢ ((φ \land A \in ℂ) \land (z \in ℝ \land (F (z) = A - y \land G (z) = y))) \to F (z) = A - y$
69		simprrr	$⊢ ((φ \land A \in ℂ) \land (z \in ℝ \land (F (z) = A - y \land G (z) = y))) \to G (z) = y$
70	68 69	oveq12d	$⊢ ((φ \land A \in ℂ) \land (z \in ℝ \land (F (z) = A - y \land G (z) = y))) \to F (z) + G (z) = A - y + y$
71		simplr	$⊢ ((φ \land A \in ℂ) \land (z \in ℝ \land (F (z) = A - y \land G (z) = y))) \to A \in ℂ$
72	33	ad2antrr	$⊢ ((φ \land A \in ℂ) \land (z \in ℝ \land (F (z) = A - y \land G (z) = y))) \to G : ℝ ⟶ ℂ$
73	72 66	ffvelrnd	$⊢ ((φ \land A \in ℂ) \land (z \in ℝ \land (F (z) = A - y \land G (z) = y))) \to G (z) \in ℂ$
74	69 73	eqeltrrd	$⊢ ((φ \land A \in ℂ) \land (z \in ℝ \land (F (z) = A - y \land G (z) = y))) \to y \in ℂ$
75	71 74	npcand	$⊢ ((φ \land A \in ℂ) \land (z \in ℝ \land (F (z) = A - y \land G (z) = y))) \to A - y + y = A$
76	67 70 75	3eqtrd	$⊢ ((φ \land A \in ℂ) \land (z \in ℝ \land (F (z) = A - y \land G (z) = y))) \to (F +_{f} G) (z) = A$
77	66 76	jca	$⊢ ((φ \land A \in ℂ) \land (z \in ℝ \land (F (z) = A - y \land G (z) = y))) \to (z \in ℝ \land (F +_{f} G) (z) = A)$
78	77	ex	$⊢ (φ \land A \in ℂ) \to ((z \in ℝ \land (F (z) = A - y \land G (z) = y)) \to (z \in ℝ \land (F +_{f} G) (z) = A))$
79	65 78	syl5bir	$⊢ (φ \land A \in ℂ) \to (((z \in ℝ \land F (z) = A - y) \land (z \in ℝ \land G (z) = y)) \to (z \in ℝ \land (F +_{f} G) (z) = A))$
80	64 79	sylbid	$⊢ (φ \land A \in ℂ) \to ((z \in F^{-1} [\{A - y\}] \land z \in G^{-1} [\{y\}]) \to (z \in ℝ \land (F +_{f} G) (z) = A))$
81	57 80	syl5bi	$⊢ (φ \land A \in ℂ) \to (z \in (F^{-1} [\{A - y\}] \cap G^{-1} [\{y\}]) \to (z \in ℝ \land (F +_{f} G) (z) = A))$
82	81	rexlimdvw	$⊢ (φ \land A \in ℂ) \to (\exists y \in ran G z \in (F^{-1} [\{A - y\}] \cap G^{-1} [\{y\}]) \to (z \in ℝ \land (F +_{f} G) (z) = A))$
83	56 82	impbid	$⊢ (φ \land A \in ℂ) \to ((z \in ℝ \land (F +_{f} G) (z) = A) \leftrightarrow \exists y \in ran G z \in (F^{-1} [\{A - y\}] \cap G^{-1} [\{y\}]))$
84	15 83	bitrd	$⊢ (φ \land A \in ℂ) \to (z \in {(F +_{f} G)}^{-1} [\{A\}] \leftrightarrow \exists y \in ran G z \in (F^{-1} [\{A - y\}] \cap G^{-1} [\{y\}]))$
85		eliun	$⊢ z \in ⋃_{y \in ran G} (F^{-1} [\{A - y\}] \cap G^{-1} [\{y\}]) \leftrightarrow \exists y \in ran G z \in (F^{-1} [\{A - y\}] \cap G^{-1} [\{y\}])$
86	84 85	bitr4di	$⊢ (φ \land A \in ℂ) \to (z \in {(F +_{f} G)}^{-1} [\{A\}] \leftrightarrow z \in ⋃_{y \in ran G} (F^{-1} [\{A - y\}] \cap G^{-1} [\{y\}]))$
87	86	eqrdv	$⊢ (φ \land A \in ℂ) \to {(F +_{f} G)}^{-1} [\{A\}] = ⋃_{y \in ran G} (F^{-1} [\{A - y\}] \cap G^{-1} [\{y\}])$

Metamath Proof Explorer

Theorem i1faddlem

Proof