Metamath Proof Explorer

Theorem i1faddlem

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

Ref Expression
Hypotheses i1fadd.1 ⊢ ( 𝜑 → 𝐹 ∈ dom ∫1 )
i1fadd.2 ⊢ ( 𝜑 → 𝐺 ∈ dom ∫1 )
Assertion i1faddlem ( ( 𝜑 ∧ 𝐴 ∈ ℂ ) → ( ◡ ( 𝐹 ∘f + 𝐺 ) “ { 𝐴 } ) = ∪ 𝑦 ∈ ran 𝐺 ( ( ◡ 𝐹 “ { ( 𝐴 − 𝑦 ) } ) ∩ ( ◡ 𝐺 “ { 𝑦 } ) ) )

Proof

Step Hyp Ref Expression
1 i1fadd.1 ⊢ ( 𝜑 → 𝐹 ∈ dom ∫1 )
2 i1fadd.2 ⊢ ( 𝜑 → 𝐺 ∈ dom ∫1 )
3 i1ff ⊢ ( 𝐹 ∈ dom ∫1 → 𝐹 : ℝ ⟶ ℝ )
4 1 3 syl ⊢ ( 𝜑 → 𝐹 : ℝ ⟶ ℝ )
5 4 ffnd ⊢ ( 𝜑 → 𝐹 Fn ℝ )
6 i1ff ⊢ ( 𝐺 ∈ dom ∫1 → 𝐺 : ℝ ⟶ ℝ )
7 2 6 syl ⊢ ( 𝜑 → 𝐺 : ℝ ⟶ ℝ )
8 7 ffnd ⊢ ( 𝜑 → 𝐺 Fn ℝ )
9 reex ⊢ ℝ ∈ V
10 9 a1i ⊢ ( 𝜑 → ℝ ∈ V )
11 inidm ⊢ ( ℝ ∩ ℝ ) = ℝ
12 5 8 10 10 11 offn ⊢ ( 𝜑 → ( 𝐹 ∘f + 𝐺 ) Fn ℝ )
13 12 adantr ⊢ ( ( 𝜑 ∧ 𝐴 ∈ ℂ ) → ( 𝐹 ∘f + 𝐺 ) Fn ℝ )
14 fniniseg ⊢ ( ( 𝐹 ∘f + 𝐺 ) Fn ℝ → ( 𝑧 ∈ ( ◡ ( 𝐹 ∘f + 𝐺 ) “ { 𝐴 } ) ↔ ( 𝑧 ∈ ℝ ∧ ( ( 𝐹 ∘f + 𝐺 ) ‘ 𝑧 ) = 𝐴 ) ) )
15 13 14 syl ⊢ ( ( 𝜑 ∧ 𝐴 ∈ ℂ ) → ( 𝑧 ∈ ( ◡ ( 𝐹 ∘f + 𝐺 ) “ { 𝐴 } ) ↔ ( 𝑧 ∈ ℝ ∧ ( ( 𝐹 ∘f + 𝐺 ) ‘ 𝑧 ) = 𝐴 ) ) )
16 8 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝐴 ∈ ℂ ) ∧ ( 𝑧 ∈ ℝ ∧ ( ( 𝐹 ∘f + 𝐺 ) ‘ 𝑧 ) = 𝐴 ) ) → 𝐺 Fn ℝ )
17 simprl ⊢ ( ( ( 𝜑 ∧ 𝐴 ∈ ℂ ) ∧ ( 𝑧 ∈ ℝ ∧ ( ( 𝐹 ∘f + 𝐺 ) ‘ 𝑧 ) = 𝐴 ) ) → 𝑧 ∈ ℝ )
18 fnfvelrn ⊢ ( ( 𝐺 Fn ℝ ∧ 𝑧 ∈ ℝ ) → ( 𝐺 ‘ 𝑧 ) ∈ ran 𝐺 )
19 16 17 18 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝐴 ∈ ℂ ) ∧ ( 𝑧 ∈ ℝ ∧ ( ( 𝐹 ∘f + 𝐺 ) ‘ 𝑧 ) = 𝐴 ) ) → ( 𝐺 ‘ 𝑧 ) ∈ ran 𝐺 )
20 simprr ⊢ ( ( ( 𝜑 ∧ 𝐴 ∈ ℂ ) ∧ ( 𝑧 ∈ ℝ ∧ ( ( 𝐹 ∘f + 𝐺 ) ‘ 𝑧 ) = 𝐴 ) ) → ( ( 𝐹 ∘f + 𝐺 ) ‘ 𝑧 ) = 𝐴 )
21 eqidd ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ℝ ) → ( 𝐹 ‘ 𝑧 ) = ( 𝐹 ‘ 𝑧 ) )
22 eqidd ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ℝ ) → ( 𝐺 ‘ 𝑧 ) = ( 𝐺 ‘ 𝑧 ) )
23 5 8 10 10 11 21 22 ofval ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ℝ ) → ( ( 𝐹 ∘f + 𝐺 ) ‘ 𝑧 ) = ( ( 𝐹 ‘ 𝑧 ) + ( 𝐺 ‘ 𝑧 ) ) )
24 23 ad2ant2r ⊢ ( ( ( 𝜑 ∧ 𝐴 ∈ ℂ ) ∧ ( 𝑧 ∈ ℝ ∧ ( ( 𝐹 ∘f + 𝐺 ) ‘ 𝑧 ) = 𝐴 ) ) → ( ( 𝐹 ∘f + 𝐺 ) ‘ 𝑧 ) = ( ( 𝐹 ‘ 𝑧 ) + ( 𝐺 ‘ 𝑧 ) ) )
25 20 24 eqtr3d ⊢ ( ( ( 𝜑 ∧ 𝐴 ∈ ℂ ) ∧ ( 𝑧 ∈ ℝ ∧ ( ( 𝐹 ∘f + 𝐺 ) ‘ 𝑧 ) = 𝐴 ) ) → 𝐴 = ( ( 𝐹 ‘ 𝑧 ) + ( 𝐺 ‘ 𝑧 ) ) )
26 25 oveq1d ⊢ ( ( ( 𝜑 ∧ 𝐴 ∈ ℂ ) ∧ ( 𝑧 ∈ ℝ ∧ ( ( 𝐹 ∘f + 𝐺 ) ‘ 𝑧 ) = 𝐴 ) ) → ( 𝐴 − ( 𝐺 ‘ 𝑧 ) ) = ( ( ( 𝐹 ‘ 𝑧 ) + ( 𝐺 ‘ 𝑧 ) ) − ( 𝐺 ‘ 𝑧 ) ) )
27 ax-resscn ⊢ ℝ ⊆ ℂ
28 fss ⊢ ( ( 𝐹 : ℝ ⟶ ℝ ∧ ℝ ⊆ ℂ ) → 𝐹 : ℝ ⟶ ℂ )
29 4 27 28 sylancl ⊢ ( 𝜑 → 𝐹 : ℝ ⟶ ℂ )
30 29 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝐴 ∈ ℂ ) ∧ ( 𝑧 ∈ ℝ ∧ ( ( 𝐹 ∘f + 𝐺 ) ‘ 𝑧 ) = 𝐴 ) ) → 𝐹 : ℝ ⟶ ℂ )
31 30 17 ffvelcdmd ⊢ ( ( ( 𝜑 ∧ 𝐴 ∈ ℂ ) ∧ ( 𝑧 ∈ ℝ ∧ ( ( 𝐹 ∘f + 𝐺 ) ‘ 𝑧 ) = 𝐴 ) ) → ( 𝐹 ‘ 𝑧 ) ∈ ℂ )
32 fss ⊢ ( ( 𝐺 : ℝ ⟶ ℝ ∧ ℝ ⊆ ℂ ) → 𝐺 : ℝ ⟶ ℂ )
33 7 27 32 sylancl ⊢ ( 𝜑 → 𝐺 : ℝ ⟶ ℂ )
34 33 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝐴 ∈ ℂ ) ∧ ( 𝑧 ∈ ℝ ∧ ( ( 𝐹 ∘f + 𝐺 ) ‘ 𝑧 ) = 𝐴 ) ) → 𝐺 : ℝ ⟶ ℂ )
35 34 17 ffvelcdmd ⊢ ( ( ( 𝜑 ∧ 𝐴 ∈ ℂ ) ∧ ( 𝑧 ∈ ℝ ∧ ( ( 𝐹 ∘f + 𝐺 ) ‘ 𝑧 ) = 𝐴 ) ) → ( 𝐺 ‘ 𝑧 ) ∈ ℂ )
36 31 35 pncand ⊢ ( ( ( 𝜑 ∧ 𝐴 ∈ ℂ ) ∧ ( 𝑧 ∈ ℝ ∧ ( ( 𝐹 ∘f + 𝐺 ) ‘ 𝑧 ) = 𝐴 ) ) → ( ( ( 𝐹 ‘ 𝑧 ) + ( 𝐺 ‘ 𝑧 ) ) − ( 𝐺 ‘ 𝑧 ) ) = ( 𝐹 ‘ 𝑧 ) )
37 26 36 eqtr2d ⊢ ( ( ( 𝜑 ∧ 𝐴 ∈ ℂ ) ∧ ( 𝑧 ∈ ℝ ∧ ( ( 𝐹 ∘f + 𝐺 ) ‘ 𝑧 ) = 𝐴 ) ) → ( 𝐹 ‘ 𝑧 ) = ( 𝐴 − ( 𝐺 ‘ 𝑧 ) ) )
38 5 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝐴 ∈ ℂ ) ∧ ( 𝑧 ∈ ℝ ∧ ( ( 𝐹 ∘f + 𝐺 ) ‘ 𝑧 ) = 𝐴 ) ) → 𝐹 Fn ℝ )
39 fniniseg ⊢ ( 𝐹 Fn ℝ → ( 𝑧 ∈ ( ◡ 𝐹 “ { ( 𝐴 − ( 𝐺 ‘ 𝑧 ) ) } ) ↔ ( 𝑧 ∈ ℝ ∧ ( 𝐹 ‘ 𝑧 ) = ( 𝐴 − ( 𝐺 ‘ 𝑧 ) ) ) ) )
40 38 39 syl ⊢ ( ( ( 𝜑 ∧ 𝐴 ∈ ℂ ) ∧ ( 𝑧 ∈ ℝ ∧ ( ( 𝐹 ∘f + 𝐺 ) ‘ 𝑧 ) = 𝐴 ) ) → ( 𝑧 ∈ ( ◡ 𝐹 “ { ( 𝐴 − ( 𝐺 ‘ 𝑧 ) ) } ) ↔ ( 𝑧 ∈ ℝ ∧ ( 𝐹 ‘ 𝑧 ) = ( 𝐴 − ( 𝐺 ‘ 𝑧 ) ) ) ) )
41 17 37 40 mpbir2and ⊢ ( ( ( 𝜑 ∧ 𝐴 ∈ ℂ ) ∧ ( 𝑧 ∈ ℝ ∧ ( ( 𝐹 ∘f + 𝐺 ) ‘ 𝑧 ) = 𝐴 ) ) → 𝑧 ∈ ( ◡ 𝐹 “ { ( 𝐴 − ( 𝐺 ‘ 𝑧 ) ) } ) )
42 eqidd ⊢ ( ( ( 𝜑 ∧ 𝐴 ∈ ℂ ) ∧ ( 𝑧 ∈ ℝ ∧ ( ( 𝐹 ∘f + 𝐺 ) ‘ 𝑧 ) = 𝐴 ) ) → ( 𝐺 ‘ 𝑧 ) = ( 𝐺 ‘ 𝑧 ) )
43 fniniseg ⊢ ( 𝐺 Fn ℝ → ( 𝑧 ∈ ( ◡ 𝐺 “ { ( 𝐺 ‘ 𝑧 ) } ) ↔ ( 𝑧 ∈ ℝ ∧ ( 𝐺 ‘ 𝑧 ) = ( 𝐺 ‘ 𝑧 ) ) ) )
44 16 43 syl ⊢ ( ( ( 𝜑 ∧ 𝐴 ∈ ℂ ) ∧ ( 𝑧 ∈ ℝ ∧ ( ( 𝐹 ∘f + 𝐺 ) ‘ 𝑧 ) = 𝐴 ) ) → ( 𝑧 ∈ ( ◡ 𝐺 “ { ( 𝐺 ‘ 𝑧 ) } ) ↔ ( 𝑧 ∈ ℝ ∧ ( 𝐺 ‘ 𝑧 ) = ( 𝐺 ‘ 𝑧 ) ) ) )
45 17 42 44 mpbir2and ⊢ ( ( ( 𝜑 ∧ 𝐴 ∈ ℂ ) ∧ ( 𝑧 ∈ ℝ ∧ ( ( 𝐹 ∘f + 𝐺 ) ‘ 𝑧 ) = 𝐴 ) ) → 𝑧 ∈ ( ◡ 𝐺 “ { ( 𝐺 ‘ 𝑧 ) } ) )
46 41 45 elind ⊢ ( ( ( 𝜑 ∧ 𝐴 ∈ ℂ ) ∧ ( 𝑧 ∈ ℝ ∧ ( ( 𝐹 ∘f + 𝐺 ) ‘ 𝑧 ) = 𝐴 ) ) → 𝑧 ∈ ( ( ◡ 𝐹 “ { ( 𝐴 − ( 𝐺 ‘ 𝑧 ) ) } ) ∩ ( ◡ 𝐺 “ { ( 𝐺 ‘ 𝑧 ) } ) ) )
47 oveq2 ⊢ ( 𝑦 = ( 𝐺 ‘ 𝑧 ) → ( 𝐴 − 𝑦 ) = ( 𝐴 − ( 𝐺 ‘ 𝑧 ) ) )
48 47 sneqd ⊢ ( 𝑦 = ( 𝐺 ‘ 𝑧 ) → { ( 𝐴 − 𝑦 ) } = { ( 𝐴 − ( 𝐺 ‘ 𝑧 ) ) } )
49 48 imaeq2d ⊢ ( 𝑦 = ( 𝐺 ‘ 𝑧 ) → ( ◡ 𝐹 “ { ( 𝐴 − 𝑦 ) } ) = ( ◡ 𝐹 “ { ( 𝐴 − ( 𝐺 ‘ 𝑧 ) ) } ) )
50 sneq ⊢ ( 𝑦 = ( 𝐺 ‘ 𝑧 ) → { 𝑦 } = { ( 𝐺 ‘ 𝑧 ) } )
51 50 imaeq2d ⊢ ( 𝑦 = ( 𝐺 ‘ 𝑧 ) → ( ◡ 𝐺 “ { 𝑦 } ) = ( ◡ 𝐺 “ { ( 𝐺 ‘ 𝑧 ) } ) )
52 49 51 ineq12d ⊢ ( 𝑦 = ( 𝐺 ‘ 𝑧 ) → ( ( ◡ 𝐹 “ { ( 𝐴 − 𝑦 ) } ) ∩ ( ◡ 𝐺 “ { 𝑦 } ) ) = ( ( ◡ 𝐹 “ { ( 𝐴 − ( 𝐺 ‘ 𝑧 ) ) } ) ∩ ( ◡ 𝐺 “ { ( 𝐺 ‘ 𝑧 ) } ) ) )
53 52 eleq2d ⊢ ( 𝑦 = ( 𝐺 ‘ 𝑧 ) → ( 𝑧 ∈ ( ( ◡ 𝐹 “ { ( 𝐴 − 𝑦 ) } ) ∩ ( ◡ 𝐺 “ { 𝑦 } ) ) ↔ 𝑧 ∈ ( ( ◡ 𝐹 “ { ( 𝐴 − ( 𝐺 ‘ 𝑧 ) ) } ) ∩ ( ◡ 𝐺 “ { ( 𝐺 ‘ 𝑧 ) } ) ) ) )
54 53 rspcev ⊢ ( ( ( 𝐺 ‘ 𝑧 ) ∈ ran 𝐺 ∧ 𝑧 ∈ ( ( ◡ 𝐹 “ { ( 𝐴 − ( 𝐺 ‘ 𝑧 ) ) } ) ∩ ( ◡ 𝐺 “ { ( 𝐺 ‘ 𝑧 ) } ) ) ) → ∃ 𝑦 ∈ ran 𝐺 𝑧 ∈ ( ( ◡ 𝐹 “ { ( 𝐴 − 𝑦 ) } ) ∩ ( ◡ 𝐺 “ { 𝑦 } ) ) )
55 19 46 54 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝐴 ∈ ℂ ) ∧ ( 𝑧 ∈ ℝ ∧ ( ( 𝐹 ∘f + 𝐺 ) ‘ 𝑧 ) = 𝐴 ) ) → ∃ 𝑦 ∈ ran 𝐺 𝑧 ∈ ( ( ◡ 𝐹 “ { ( 𝐴 − 𝑦 ) } ) ∩ ( ◡ 𝐺 “ { 𝑦 } ) ) )
56 55 ex ⊢ ( ( 𝜑 ∧ 𝐴 ∈ ℂ ) → ( ( 𝑧 ∈ ℝ ∧ ( ( 𝐹 ∘f + 𝐺 ) ‘ 𝑧 ) = 𝐴 ) → ∃ 𝑦 ∈ ran 𝐺 𝑧 ∈ ( ( ◡ 𝐹 “ { ( 𝐴 − 𝑦 ) } ) ∩ ( ◡ 𝐺 “ { 𝑦 } ) ) ) )
57 elin ⊢ ( 𝑧 ∈ ( ( ◡ 𝐹 “ { ( 𝐴 − 𝑦 ) } ) ∩ ( ◡ 𝐺 “ { 𝑦 } ) ) ↔ ( 𝑧 ∈ ( ◡ 𝐹 “ { ( 𝐴 − 𝑦 ) } ) ∧ 𝑧 ∈ ( ◡ 𝐺 “ { 𝑦 } ) ) )
58 5 adantr ⊢ ( ( 𝜑 ∧ 𝐴 ∈ ℂ ) → 𝐹 Fn ℝ )
59 fniniseg ⊢ ( 𝐹 Fn ℝ → ( 𝑧 ∈ ( ◡ 𝐹 “ { ( 𝐴 − 𝑦 ) } ) ↔ ( 𝑧 ∈ ℝ ∧ ( 𝐹 ‘ 𝑧 ) = ( 𝐴 − 𝑦 ) ) ) )
60 58 59 syl ⊢ ( ( 𝜑 ∧ 𝐴 ∈ ℂ ) → ( 𝑧 ∈ ( ◡ 𝐹 “ { ( 𝐴 − 𝑦 ) } ) ↔ ( 𝑧 ∈ ℝ ∧ ( 𝐹 ‘ 𝑧 ) = ( 𝐴 − 𝑦 ) ) ) )
61 8 adantr ⊢ ( ( 𝜑 ∧ 𝐴 ∈ ℂ ) → 𝐺 Fn ℝ )
62 fniniseg ⊢ ( 𝐺 Fn ℝ → ( 𝑧 ∈ ( ◡ 𝐺 “ { 𝑦 } ) ↔ ( 𝑧 ∈ ℝ ∧ ( 𝐺 ‘ 𝑧 ) = 𝑦 ) ) )
63 61 62 syl ⊢ ( ( 𝜑 ∧ 𝐴 ∈ ℂ ) → ( 𝑧 ∈ ( ◡ 𝐺 “ { 𝑦 } ) ↔ ( 𝑧 ∈ ℝ ∧ ( 𝐺 ‘ 𝑧 ) = 𝑦 ) ) )
64 60 63 anbi12d ⊢ ( ( 𝜑 ∧ 𝐴 ∈ ℂ ) → ( ( 𝑧 ∈ ( ◡ 𝐹 “ { ( 𝐴 − 𝑦 ) } ) ∧ 𝑧 ∈ ( ◡ 𝐺 “ { 𝑦 } ) ) ↔ ( ( 𝑧 ∈ ℝ ∧ ( 𝐹 ‘ 𝑧 ) = ( 𝐴 − 𝑦 ) ) ∧ ( 𝑧 ∈ ℝ ∧ ( 𝐺 ‘ 𝑧 ) = 𝑦 ) ) ) )
65 anandi ⊢ ( ( 𝑧 ∈ ℝ ∧ ( ( 𝐹 ‘ 𝑧 ) = ( 𝐴 − 𝑦 ) ∧ ( 𝐺 ‘ 𝑧 ) = 𝑦 ) ) ↔ ( ( 𝑧 ∈ ℝ ∧ ( 𝐹 ‘ 𝑧 ) = ( 𝐴 − 𝑦 ) ) ∧ ( 𝑧 ∈ ℝ ∧ ( 𝐺 ‘ 𝑧 ) = 𝑦 ) ) )
66 simprl ⊢ ( ( ( 𝜑 ∧ 𝐴 ∈ ℂ ) ∧ ( 𝑧 ∈ ℝ ∧ ( ( 𝐹 ‘ 𝑧 ) = ( 𝐴 − 𝑦 ) ∧ ( 𝐺 ‘ 𝑧 ) = 𝑦 ) ) ) → 𝑧 ∈ ℝ )
67 23 ad2ant2r ⊢ ( ( ( 𝜑 ∧ 𝐴 ∈ ℂ ) ∧ ( 𝑧 ∈ ℝ ∧ ( ( 𝐹 ‘ 𝑧 ) = ( 𝐴 − 𝑦 ) ∧ ( 𝐺 ‘ 𝑧 ) = 𝑦 ) ) ) → ( ( 𝐹 ∘f + 𝐺 ) ‘ 𝑧 ) = ( ( 𝐹 ‘ 𝑧 ) + ( 𝐺 ‘ 𝑧 ) ) )
68 simprrl ⊢ ( ( ( 𝜑 ∧ 𝐴 ∈ ℂ ) ∧ ( 𝑧 ∈ ℝ ∧ ( ( 𝐹 ‘ 𝑧 ) = ( 𝐴 − 𝑦 ) ∧ ( 𝐺 ‘ 𝑧 ) = 𝑦 ) ) ) → ( 𝐹 ‘ 𝑧 ) = ( 𝐴 − 𝑦 ) )
69 simprrr ⊢ ( ( ( 𝜑 ∧ 𝐴 ∈ ℂ ) ∧ ( 𝑧 ∈ ℝ ∧ ( ( 𝐹 ‘ 𝑧 ) = ( 𝐴 − 𝑦 ) ∧ ( 𝐺 ‘ 𝑧 ) = 𝑦 ) ) ) → ( 𝐺 ‘ 𝑧 ) = 𝑦 )
70 68 69 oveq12d ⊢ ( ( ( 𝜑 ∧ 𝐴 ∈ ℂ ) ∧ ( 𝑧 ∈ ℝ ∧ ( ( 𝐹 ‘ 𝑧 ) = ( 𝐴 − 𝑦 ) ∧ ( 𝐺 ‘ 𝑧 ) = 𝑦 ) ) ) → ( ( 𝐹 ‘ 𝑧 ) + ( 𝐺 ‘ 𝑧 ) ) = ( ( 𝐴 − 𝑦 ) + 𝑦 ) )
71 simplr ⊢ ( ( ( 𝜑 ∧ 𝐴 ∈ ℂ ) ∧ ( 𝑧 ∈ ℝ ∧ ( ( 𝐹 ‘ 𝑧 ) = ( 𝐴 − 𝑦 ) ∧ ( 𝐺 ‘ 𝑧 ) = 𝑦 ) ) ) → 𝐴 ∈ ℂ )
72 33 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝐴 ∈ ℂ ) ∧ ( 𝑧 ∈ ℝ ∧ ( ( 𝐹 ‘ 𝑧 ) = ( 𝐴 − 𝑦 ) ∧ ( 𝐺 ‘ 𝑧 ) = 𝑦 ) ) ) → 𝐺 : ℝ ⟶ ℂ )
73 72 66 ffvelcdmd ⊢ ( ( ( 𝜑 ∧ 𝐴 ∈ ℂ ) ∧ ( 𝑧 ∈ ℝ ∧ ( ( 𝐹 ‘ 𝑧 ) = ( 𝐴 − 𝑦 ) ∧ ( 𝐺 ‘ 𝑧 ) = 𝑦 ) ) ) → ( 𝐺 ‘ 𝑧 ) ∈ ℂ )
74 69 73 eqeltrrd ⊢ ( ( ( 𝜑 ∧ 𝐴 ∈ ℂ ) ∧ ( 𝑧 ∈ ℝ ∧ ( ( 𝐹 ‘ 𝑧 ) = ( 𝐴 − 𝑦 ) ∧ ( 𝐺 ‘ 𝑧 ) = 𝑦 ) ) ) → 𝑦 ∈ ℂ )
75 71 74 npcand ⊢ ( ( ( 𝜑 ∧ 𝐴 ∈ ℂ ) ∧ ( 𝑧 ∈ ℝ ∧ ( ( 𝐹 ‘ 𝑧 ) = ( 𝐴 − 𝑦 ) ∧ ( 𝐺 ‘ 𝑧 ) = 𝑦 ) ) ) → ( ( 𝐴 − 𝑦 ) + 𝑦 ) = 𝐴 )
76 67 70 75 3eqtrd ⊢ ( ( ( 𝜑 ∧ 𝐴 ∈ ℂ ) ∧ ( 𝑧 ∈ ℝ ∧ ( ( 𝐹 ‘ 𝑧 ) = ( 𝐴 − 𝑦 ) ∧ ( 𝐺 ‘ 𝑧 ) = 𝑦 ) ) ) → ( ( 𝐹 ∘f + 𝐺 ) ‘ 𝑧 ) = 𝐴 )
77 66 76 jca ⊢ ( ( ( 𝜑 ∧ 𝐴 ∈ ℂ ) ∧ ( 𝑧 ∈ ℝ ∧ ( ( 𝐹 ‘ 𝑧 ) = ( 𝐴 − 𝑦 ) ∧ ( 𝐺 ‘ 𝑧 ) = 𝑦 ) ) ) → ( 𝑧 ∈ ℝ ∧ ( ( 𝐹 ∘f + 𝐺 ) ‘ 𝑧 ) = 𝐴 ) )
78 77 ex ⊢ ( ( 𝜑 ∧ 𝐴 ∈ ℂ ) → ( ( 𝑧 ∈ ℝ ∧ ( ( 𝐹 ‘ 𝑧 ) = ( 𝐴 − 𝑦 ) ∧ ( 𝐺 ‘ 𝑧 ) = 𝑦 ) ) → ( 𝑧 ∈ ℝ ∧ ( ( 𝐹 ∘f + 𝐺 ) ‘ 𝑧 ) = 𝐴 ) ) )
79 65 78 biimtrrid ⊢ ( ( 𝜑 ∧ 𝐴 ∈ ℂ ) → ( ( ( 𝑧 ∈ ℝ ∧ ( 𝐹 ‘ 𝑧 ) = ( 𝐴 − 𝑦 ) ) ∧ ( 𝑧 ∈ ℝ ∧ ( 𝐺 ‘ 𝑧 ) = 𝑦 ) ) → ( 𝑧 ∈ ℝ ∧ ( ( 𝐹 ∘f + 𝐺 ) ‘ 𝑧 ) = 𝐴 ) ) )
80 64 79 sylbid ⊢ ( ( 𝜑 ∧ 𝐴 ∈ ℂ ) → ( ( 𝑧 ∈ ( ◡ 𝐹 “ { ( 𝐴 − 𝑦 ) } ) ∧ 𝑧 ∈ ( ◡ 𝐺 “ { 𝑦 } ) ) → ( 𝑧 ∈ ℝ ∧ ( ( 𝐹 ∘f + 𝐺 ) ‘ 𝑧 ) = 𝐴 ) ) )
81 57 80 biimtrid ⊢ ( ( 𝜑 ∧ 𝐴 ∈ ℂ ) → ( 𝑧 ∈ ( ( ◡ 𝐹 “ { ( 𝐴 − 𝑦 ) } ) ∩ ( ◡ 𝐺 “ { 𝑦 } ) ) → ( 𝑧 ∈ ℝ ∧ ( ( 𝐹 ∘f + 𝐺 ) ‘ 𝑧 ) = 𝐴 ) ) )
82 81 rexlimdvw ⊢ ( ( 𝜑 ∧ 𝐴 ∈ ℂ ) → ( ∃ 𝑦 ∈ ran 𝐺 𝑧 ∈ ( ( ◡ 𝐹 “ { ( 𝐴 − 𝑦 ) } ) ∩ ( ◡ 𝐺 “ { 𝑦 } ) ) → ( 𝑧 ∈ ℝ ∧ ( ( 𝐹 ∘f + 𝐺 ) ‘ 𝑧 ) = 𝐴 ) ) )
83 56 82 impbid ⊢ ( ( 𝜑 ∧ 𝐴 ∈ ℂ ) → ( ( 𝑧 ∈ ℝ ∧ ( ( 𝐹 ∘f + 𝐺 ) ‘ 𝑧 ) = 𝐴 ) ↔ ∃ 𝑦 ∈ ran 𝐺 𝑧 ∈ ( ( ◡ 𝐹 “ { ( 𝐴 − 𝑦 ) } ) ∩ ( ◡ 𝐺 “ { 𝑦 } ) ) ) )
84 15 83 bitrd ⊢ ( ( 𝜑 ∧ 𝐴 ∈ ℂ ) → ( 𝑧 ∈ ( ◡ ( 𝐹 ∘f + 𝐺 ) “ { 𝐴 } ) ↔ ∃ 𝑦 ∈ ran 𝐺 𝑧 ∈ ( ( ◡ 𝐹 “ { ( 𝐴 − 𝑦 ) } ) ∩ ( ◡ 𝐺 “ { 𝑦 } ) ) ) )
85 eliun ⊢ ( 𝑧 ∈ ∪ 𝑦 ∈ ran 𝐺 ( ( ◡ 𝐹 “ { ( 𝐴 − 𝑦 ) } ) ∩ ( ◡ 𝐺 “ { 𝑦 } ) ) ↔ ∃ 𝑦 ∈ ran 𝐺 𝑧 ∈ ( ( ◡ 𝐹 “ { ( 𝐴 − 𝑦 ) } ) ∩ ( ◡ 𝐺 “ { 𝑦 } ) ) )
86 84 85 bitr4di ⊢ ( ( 𝜑 ∧ 𝐴 ∈ ℂ ) → ( 𝑧 ∈ ( ◡ ( 𝐹 ∘f + 𝐺 ) “ { 𝐴 } ) ↔ 𝑧 ∈ ∪ 𝑦 ∈ ran 𝐺 ( ( ◡ 𝐹 “ { ( 𝐴 − 𝑦 ) } ) ∩ ( ◡ 𝐺 “ { 𝑦 } ) ) ) )
87 86 eqrdv ⊢ ( ( 𝜑 ∧ 𝐴 ∈ ℂ ) → ( ◡ ( 𝐹 ∘f + 𝐺 ) “ { 𝐴 } ) = ∪ 𝑦 ∈ ran 𝐺 ( ( ◡ 𝐹 “ { ( 𝐴 − 𝑦 ) } ) ∩ ( ◡ 𝐺 “ { 𝑦 } ) ) )