Metamath Proof Explorer

Theorem i1fmullem

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

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

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 ⊢ ( ( 𝜑 ∧ 𝐴 ∈ ( ℂ ∖ { 0 } ) ) → ( 𝐹 ∘f · 𝐺 ) Fn ℝ )
14 fniniseg ⊢ ( ( 𝐹 ∘f · 𝐺 ) Fn ℝ → ( 𝑧 ∈ ( ◡ ( 𝐹 ∘f · 𝐺 ) “ { 𝐴 } ) ↔ ( 𝑧 ∈ ℝ ∧ ( ( 𝐹 ∘f · 𝐺 ) ‘ 𝑧 ) = 𝐴 ) ) )
15 13 14 syl ⊢ ( ( 𝜑 ∧ 𝐴 ∈ ( ℂ ∖ { 0 } ) ) → ( 𝑧 ∈ ( ◡ ( 𝐹 ∘f · 𝐺 ) “ { 𝐴 } ) ↔ ( 𝑧 ∈ ℝ ∧ ( ( 𝐹 ∘f · 𝐺 ) ‘ 𝑧 ) = 𝐴 ) ) )
16 5 adantr ⊢ ( ( 𝜑 ∧ 𝐴 ∈ ( ℂ ∖ { 0 } ) ) → 𝐹 Fn ℝ )
17 8 adantr ⊢ ( ( 𝜑 ∧ 𝐴 ∈ ( ℂ ∖ { 0 } ) ) → 𝐺 Fn ℝ )
18 9 a1i ⊢ ( ( 𝜑 ∧ 𝐴 ∈ ( ℂ ∖ { 0 } ) ) → ℝ ∈ V )
19 eqidd ⊢ ( ( ( 𝜑 ∧ 𝐴 ∈ ( ℂ ∖ { 0 } ) ) ∧ 𝑧 ∈ ℝ ) → ( 𝐹 ‘ 𝑧 ) = ( 𝐹 ‘ 𝑧 ) )
20 eqidd ⊢ ( ( ( 𝜑 ∧ 𝐴 ∈ ( ℂ ∖ { 0 } ) ) ∧ 𝑧 ∈ ℝ ) → ( 𝐺 ‘ 𝑧 ) = ( 𝐺 ‘ 𝑧 ) )
21 16 17 18 18 11 19 20 ofval ⊢ ( ( ( 𝜑 ∧ 𝐴 ∈ ( ℂ ∖ { 0 } ) ) ∧ 𝑧 ∈ ℝ ) → ( ( 𝐹 ∘f · 𝐺 ) ‘ 𝑧 ) = ( ( 𝐹 ‘ 𝑧 ) · ( 𝐺 ‘ 𝑧 ) ) )
22 21 eqeq1d ⊢ ( ( ( 𝜑 ∧ 𝐴 ∈ ( ℂ ∖ { 0 } ) ) ∧ 𝑧 ∈ ℝ ) → ( ( ( 𝐹 ∘f · 𝐺 ) ‘ 𝑧 ) = 𝐴 ↔ ( ( 𝐹 ‘ 𝑧 ) · ( 𝐺 ‘ 𝑧 ) ) = 𝐴 ) )
23 22 pm5.32da ⊢ ( ( 𝜑 ∧ 𝐴 ∈ ( ℂ ∖ { 0 } ) ) → ( ( 𝑧 ∈ ℝ ∧ ( ( 𝐹 ∘f · 𝐺 ) ‘ 𝑧 ) = 𝐴 ) ↔ ( 𝑧 ∈ ℝ ∧ ( ( 𝐹 ‘ 𝑧 ) · ( 𝐺 ‘ 𝑧 ) ) = 𝐴 ) ) )
24 8 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝐴 ∈ ( ℂ ∖ { 0 } ) ) ∧ ( 𝑧 ∈ ℝ ∧ ( ( 𝐹 ‘ 𝑧 ) · ( 𝐺 ‘ 𝑧 ) ) = 𝐴 ) ) → 𝐺 Fn ℝ )
25 simprl ⊢ ( ( ( 𝜑 ∧ 𝐴 ∈ ( ℂ ∖ { 0 } ) ) ∧ ( 𝑧 ∈ ℝ ∧ ( ( 𝐹 ‘ 𝑧 ) · ( 𝐺 ‘ 𝑧 ) ) = 𝐴 ) ) → 𝑧 ∈ ℝ )
26 fnfvelrn ⊢ ( ( 𝐺 Fn ℝ ∧ 𝑧 ∈ ℝ ) → ( 𝐺 ‘ 𝑧 ) ∈ ran 𝐺 )
27 24 25 26 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝐴 ∈ ( ℂ ∖ { 0 } ) ) ∧ ( 𝑧 ∈ ℝ ∧ ( ( 𝐹 ‘ 𝑧 ) · ( 𝐺 ‘ 𝑧 ) ) = 𝐴 ) ) → ( 𝐺 ‘ 𝑧 ) ∈ ran 𝐺 )
28 eldifsni ⊢ ( 𝐴 ∈ ( ℂ ∖ { 0 } ) → 𝐴 ≠ 0 )
29 28 ad2antlr ⊢ ( ( ( 𝜑 ∧ 𝐴 ∈ ( ℂ ∖ { 0 } ) ) ∧ ( 𝑧 ∈ ℝ ∧ ( ( 𝐹 ‘ 𝑧 ) · ( 𝐺 ‘ 𝑧 ) ) = 𝐴 ) ) → 𝐴 ≠ 0 )
30 simprr ⊢ ( ( ( 𝜑 ∧ 𝐴 ∈ ( ℂ ∖ { 0 } ) ) ∧ ( 𝑧 ∈ ℝ ∧ ( ( 𝐹 ‘ 𝑧 ) · ( 𝐺 ‘ 𝑧 ) ) = 𝐴 ) ) → ( ( 𝐹 ‘ 𝑧 ) · ( 𝐺 ‘ 𝑧 ) ) = 𝐴 )
31 4 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝐴 ∈ ( ℂ ∖ { 0 } ) ) ∧ ( 𝑧 ∈ ℝ ∧ ( ( 𝐹 ‘ 𝑧 ) · ( 𝐺 ‘ 𝑧 ) ) = 𝐴 ) ) → 𝐹 : ℝ ⟶ ℝ )
32 31 25 ffvelrnd ⊢ ( ( ( 𝜑 ∧ 𝐴 ∈ ( ℂ ∖ { 0 } ) ) ∧ ( 𝑧 ∈ ℝ ∧ ( ( 𝐹 ‘ 𝑧 ) · ( 𝐺 ‘ 𝑧 ) ) = 𝐴 ) ) → ( 𝐹 ‘ 𝑧 ) ∈ ℝ )
33 32 recnd ⊢ ( ( ( 𝜑 ∧ 𝐴 ∈ ( ℂ ∖ { 0 } ) ) ∧ ( 𝑧 ∈ ℝ ∧ ( ( 𝐹 ‘ 𝑧 ) · ( 𝐺 ‘ 𝑧 ) ) = 𝐴 ) ) → ( 𝐹 ‘ 𝑧 ) ∈ ℂ )
34 33 mul01d ⊢ ( ( ( 𝜑 ∧ 𝐴 ∈ ( ℂ ∖ { 0 } ) ) ∧ ( 𝑧 ∈ ℝ ∧ ( ( 𝐹 ‘ 𝑧 ) · ( 𝐺 ‘ 𝑧 ) ) = 𝐴 ) ) → ( ( 𝐹 ‘ 𝑧 ) · 0 ) = 0 )
35 29 30 34 3netr4d ⊢ ( ( ( 𝜑 ∧ 𝐴 ∈ ( ℂ ∖ { 0 } ) ) ∧ ( 𝑧 ∈ ℝ ∧ ( ( 𝐹 ‘ 𝑧 ) · ( 𝐺 ‘ 𝑧 ) ) = 𝐴 ) ) → ( ( 𝐹 ‘ 𝑧 ) · ( 𝐺 ‘ 𝑧 ) ) ≠ ( ( 𝐹 ‘ 𝑧 ) · 0 ) )
36 oveq2 ⊢ ( ( 𝐺 ‘ 𝑧 ) = 0 → ( ( 𝐹 ‘ 𝑧 ) · ( 𝐺 ‘ 𝑧 ) ) = ( ( 𝐹 ‘ 𝑧 ) · 0 ) )
37 36 necon3i ⊢ ( ( ( 𝐹 ‘ 𝑧 ) · ( 𝐺 ‘ 𝑧 ) ) ≠ ( ( 𝐹 ‘ 𝑧 ) · 0 ) → ( 𝐺 ‘ 𝑧 ) ≠ 0 )
38 35 37 syl ⊢ ( ( ( 𝜑 ∧ 𝐴 ∈ ( ℂ ∖ { 0 } ) ) ∧ ( 𝑧 ∈ ℝ ∧ ( ( 𝐹 ‘ 𝑧 ) · ( 𝐺 ‘ 𝑧 ) ) = 𝐴 ) ) → ( 𝐺 ‘ 𝑧 ) ≠ 0 )
39 eldifsn ⊢ ( ( 𝐺 ‘ 𝑧 ) ∈ ( ran 𝐺 ∖ { 0 } ) ↔ ( ( 𝐺 ‘ 𝑧 ) ∈ ran 𝐺 ∧ ( 𝐺 ‘ 𝑧 ) ≠ 0 ) )
40 27 38 39 sylanbrc ⊢ ( ( ( 𝜑 ∧ 𝐴 ∈ ( ℂ ∖ { 0 } ) ) ∧ ( 𝑧 ∈ ℝ ∧ ( ( 𝐹 ‘ 𝑧 ) · ( 𝐺 ‘ 𝑧 ) ) = 𝐴 ) ) → ( 𝐺 ‘ 𝑧 ) ∈ ( ran 𝐺 ∖ { 0 } ) )
41 7 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝐴 ∈ ( ℂ ∖ { 0 } ) ) ∧ ( 𝑧 ∈ ℝ ∧ ( ( 𝐹 ‘ 𝑧 ) · ( 𝐺 ‘ 𝑧 ) ) = 𝐴 ) ) → 𝐺 : ℝ ⟶ ℝ )
42 41 25 ffvelrnd ⊢ ( ( ( 𝜑 ∧ 𝐴 ∈ ( ℂ ∖ { 0 } ) ) ∧ ( 𝑧 ∈ ℝ ∧ ( ( 𝐹 ‘ 𝑧 ) · ( 𝐺 ‘ 𝑧 ) ) = 𝐴 ) ) → ( 𝐺 ‘ 𝑧 ) ∈ ℝ )
43 42 recnd ⊢ ( ( ( 𝜑 ∧ 𝐴 ∈ ( ℂ ∖ { 0 } ) ) ∧ ( 𝑧 ∈ ℝ ∧ ( ( 𝐹 ‘ 𝑧 ) · ( 𝐺 ‘ 𝑧 ) ) = 𝐴 ) ) → ( 𝐺 ‘ 𝑧 ) ∈ ℂ )
44 33 43 38 divcan4d ⊢ ( ( ( 𝜑 ∧ 𝐴 ∈ ( ℂ ∖ { 0 } ) ) ∧ ( 𝑧 ∈ ℝ ∧ ( ( 𝐹 ‘ 𝑧 ) · ( 𝐺 ‘ 𝑧 ) ) = 𝐴 ) ) → ( ( ( 𝐹 ‘ 𝑧 ) · ( 𝐺 ‘ 𝑧 ) ) / ( 𝐺 ‘ 𝑧 ) ) = ( 𝐹 ‘ 𝑧 ) )
45 30 oveq1d ⊢ ( ( ( 𝜑 ∧ 𝐴 ∈ ( ℂ ∖ { 0 } ) ) ∧ ( 𝑧 ∈ ℝ ∧ ( ( 𝐹 ‘ 𝑧 ) · ( 𝐺 ‘ 𝑧 ) ) = 𝐴 ) ) → ( ( ( 𝐹 ‘ 𝑧 ) · ( 𝐺 ‘ 𝑧 ) ) / ( 𝐺 ‘ 𝑧 ) ) = ( 𝐴 / ( 𝐺 ‘ 𝑧 ) ) )
46 44 45 eqtr3d ⊢ ( ( ( 𝜑 ∧ 𝐴 ∈ ( ℂ ∖ { 0 } ) ) ∧ ( 𝑧 ∈ ℝ ∧ ( ( 𝐹 ‘ 𝑧 ) · ( 𝐺 ‘ 𝑧 ) ) = 𝐴 ) ) → ( 𝐹 ‘ 𝑧 ) = ( 𝐴 / ( 𝐺 ‘ 𝑧 ) ) )
47 31 ffnd ⊢ ( ( ( 𝜑 ∧ 𝐴 ∈ ( ℂ ∖ { 0 } ) ) ∧ ( 𝑧 ∈ ℝ ∧ ( ( 𝐹 ‘ 𝑧 ) · ( 𝐺 ‘ 𝑧 ) ) = 𝐴 ) ) → 𝐹 Fn ℝ )
48 fniniseg ⊢ ( 𝐹 Fn ℝ → ( 𝑧 ∈ ( ◡ 𝐹 “ { ( 𝐴 / ( 𝐺 ‘ 𝑧 ) ) } ) ↔ ( 𝑧 ∈ ℝ ∧ ( 𝐹 ‘ 𝑧 ) = ( 𝐴 / ( 𝐺 ‘ 𝑧 ) ) ) ) )
49 47 48 syl ⊢ ( ( ( 𝜑 ∧ 𝐴 ∈ ( ℂ ∖ { 0 } ) ) ∧ ( 𝑧 ∈ ℝ ∧ ( ( 𝐹 ‘ 𝑧 ) · ( 𝐺 ‘ 𝑧 ) ) = 𝐴 ) ) → ( 𝑧 ∈ ( ◡ 𝐹 “ { ( 𝐴 / ( 𝐺 ‘ 𝑧 ) ) } ) ↔ ( 𝑧 ∈ ℝ ∧ ( 𝐹 ‘ 𝑧 ) = ( 𝐴 / ( 𝐺 ‘ 𝑧 ) ) ) ) )
50 25 46 49 mpbir2and ⊢ ( ( ( 𝜑 ∧ 𝐴 ∈ ( ℂ ∖ { 0 } ) ) ∧ ( 𝑧 ∈ ℝ ∧ ( ( 𝐹 ‘ 𝑧 ) · ( 𝐺 ‘ 𝑧 ) ) = 𝐴 ) ) → 𝑧 ∈ ( ◡ 𝐹 “ { ( 𝐴 / ( 𝐺 ‘ 𝑧 ) ) } ) )
51 eqidd ⊢ ( ( ( 𝜑 ∧ 𝐴 ∈ ( ℂ ∖ { 0 } ) ) ∧ ( 𝑧 ∈ ℝ ∧ ( ( 𝐹 ‘ 𝑧 ) · ( 𝐺 ‘ 𝑧 ) ) = 𝐴 ) ) → ( 𝐺 ‘ 𝑧 ) = ( 𝐺 ‘ 𝑧 ) )
52 fniniseg ⊢ ( 𝐺 Fn ℝ → ( 𝑧 ∈ ( ◡ 𝐺 “ { ( 𝐺 ‘ 𝑧 ) } ) ↔ ( 𝑧 ∈ ℝ ∧ ( 𝐺 ‘ 𝑧 ) = ( 𝐺 ‘ 𝑧 ) ) ) )
53 24 52 syl ⊢ ( ( ( 𝜑 ∧ 𝐴 ∈ ( ℂ ∖ { 0 } ) ) ∧ ( 𝑧 ∈ ℝ ∧ ( ( 𝐹 ‘ 𝑧 ) · ( 𝐺 ‘ 𝑧 ) ) = 𝐴 ) ) → ( 𝑧 ∈ ( ◡ 𝐺 “ { ( 𝐺 ‘ 𝑧 ) } ) ↔ ( 𝑧 ∈ ℝ ∧ ( 𝐺 ‘ 𝑧 ) = ( 𝐺 ‘ 𝑧 ) ) ) )
54 25 51 53 mpbir2and ⊢ ( ( ( 𝜑 ∧ 𝐴 ∈ ( ℂ ∖ { 0 } ) ) ∧ ( 𝑧 ∈ ℝ ∧ ( ( 𝐹 ‘ 𝑧 ) · ( 𝐺 ‘ 𝑧 ) ) = 𝐴 ) ) → 𝑧 ∈ ( ◡ 𝐺 “ { ( 𝐺 ‘ 𝑧 ) } ) )
55 50 54 elind ⊢ ( ( ( 𝜑 ∧ 𝐴 ∈ ( ℂ ∖ { 0 } ) ) ∧ ( 𝑧 ∈ ℝ ∧ ( ( 𝐹 ‘ 𝑧 ) · ( 𝐺 ‘ 𝑧 ) ) = 𝐴 ) ) → 𝑧 ∈ ( ( ◡ 𝐹 “ { ( 𝐴 / ( 𝐺 ‘ 𝑧 ) ) } ) ∩ ( ◡ 𝐺 “ { ( 𝐺 ‘ 𝑧 ) } ) ) )
56 oveq2 ⊢ ( 𝑦 = ( 𝐺 ‘ 𝑧 ) → ( 𝐴 / 𝑦 ) = ( 𝐴 / ( 𝐺 ‘ 𝑧 ) ) )
57 56 sneqd ⊢ ( 𝑦 = ( 𝐺 ‘ 𝑧 ) → { ( 𝐴 / 𝑦 ) } = { ( 𝐴 / ( 𝐺 ‘ 𝑧 ) ) } )
58 57 imaeq2d ⊢ ( 𝑦 = ( 𝐺 ‘ 𝑧 ) → ( ◡ 𝐹 “ { ( 𝐴 / 𝑦 ) } ) = ( ◡ 𝐹 “ { ( 𝐴 / ( 𝐺 ‘ 𝑧 ) ) } ) )
59 sneq ⊢ ( 𝑦 = ( 𝐺 ‘ 𝑧 ) → { 𝑦 } = { ( 𝐺 ‘ 𝑧 ) } )
60 59 imaeq2d ⊢ ( 𝑦 = ( 𝐺 ‘ 𝑧 ) → ( ◡ 𝐺 “ { 𝑦 } ) = ( ◡ 𝐺 “ { ( 𝐺 ‘ 𝑧 ) } ) )
61 58 60 ineq12d ⊢ ( 𝑦 = ( 𝐺 ‘ 𝑧 ) → ( ( ◡ 𝐹 “ { ( 𝐴 / 𝑦 ) } ) ∩ ( ◡ 𝐺 “ { 𝑦 } ) ) = ( ( ◡ 𝐹 “ { ( 𝐴 / ( 𝐺 ‘ 𝑧 ) ) } ) ∩ ( ◡ 𝐺 “ { ( 𝐺 ‘ 𝑧 ) } ) ) )
62 61 eleq2d ⊢ ( 𝑦 = ( 𝐺 ‘ 𝑧 ) → ( 𝑧 ∈ ( ( ◡ 𝐹 “ { ( 𝐴 / 𝑦 ) } ) ∩ ( ◡ 𝐺 “ { 𝑦 } ) ) ↔ 𝑧 ∈ ( ( ◡ 𝐹 “ { ( 𝐴 / ( 𝐺 ‘ 𝑧 ) ) } ) ∩ ( ◡ 𝐺 “ { ( 𝐺 ‘ 𝑧 ) } ) ) ) )
63 62 rspcev ⊢ ( ( ( 𝐺 ‘ 𝑧 ) ∈ ( ran 𝐺 ∖ { 0 } ) ∧ 𝑧 ∈ ( ( ◡ 𝐹 “ { ( 𝐴 / ( 𝐺 ‘ 𝑧 ) ) } ) ∩ ( ◡ 𝐺 “ { ( 𝐺 ‘ 𝑧 ) } ) ) ) → ∃ 𝑦 ∈ ( ran 𝐺 ∖ { 0 } ) 𝑧 ∈ ( ( ◡ 𝐹 “ { ( 𝐴 / 𝑦 ) } ) ∩ ( ◡ 𝐺 “ { 𝑦 } ) ) )
64 40 55 63 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝐴 ∈ ( ℂ ∖ { 0 } ) ) ∧ ( 𝑧 ∈ ℝ ∧ ( ( 𝐹 ‘ 𝑧 ) · ( 𝐺 ‘ 𝑧 ) ) = 𝐴 ) ) → ∃ 𝑦 ∈ ( ran 𝐺 ∖ { 0 } ) 𝑧 ∈ ( ( ◡ 𝐹 “ { ( 𝐴 / 𝑦 ) } ) ∩ ( ◡ 𝐺 “ { 𝑦 } ) ) )
65 64 ex ⊢ ( ( 𝜑 ∧ 𝐴 ∈ ( ℂ ∖ { 0 } ) ) → ( ( 𝑧 ∈ ℝ ∧ ( ( 𝐹 ‘ 𝑧 ) · ( 𝐺 ‘ 𝑧 ) ) = 𝐴 ) → ∃ 𝑦 ∈ ( ran 𝐺 ∖ { 0 } ) 𝑧 ∈ ( ( ◡ 𝐹 “ { ( 𝐴 / 𝑦 ) } ) ∩ ( ◡ 𝐺 “ { 𝑦 } ) ) ) )
66 fniniseg ⊢ ( 𝐹 Fn ℝ → ( 𝑧 ∈ ( ◡ 𝐹 “ { ( 𝐴 / 𝑦 ) } ) ↔ ( 𝑧 ∈ ℝ ∧ ( 𝐹 ‘ 𝑧 ) = ( 𝐴 / 𝑦 ) ) ) )
67 16 66 syl ⊢ ( ( 𝜑 ∧ 𝐴 ∈ ( ℂ ∖ { 0 } ) ) → ( 𝑧 ∈ ( ◡ 𝐹 “ { ( 𝐴 / 𝑦 ) } ) ↔ ( 𝑧 ∈ ℝ ∧ ( 𝐹 ‘ 𝑧 ) = ( 𝐴 / 𝑦 ) ) ) )
68 fniniseg ⊢ ( 𝐺 Fn ℝ → ( 𝑧 ∈ ( ◡ 𝐺 “ { 𝑦 } ) ↔ ( 𝑧 ∈ ℝ ∧ ( 𝐺 ‘ 𝑧 ) = 𝑦 ) ) )
69 17 68 syl ⊢ ( ( 𝜑 ∧ 𝐴 ∈ ( ℂ ∖ { 0 } ) ) → ( 𝑧 ∈ ( ◡ 𝐺 “ { 𝑦 } ) ↔ ( 𝑧 ∈ ℝ ∧ ( 𝐺 ‘ 𝑧 ) = 𝑦 ) ) )
70 67 69 anbi12d ⊢ ( ( 𝜑 ∧ 𝐴 ∈ ( ℂ ∖ { 0 } ) ) → ( ( 𝑧 ∈ ( ◡ 𝐹 “ { ( 𝐴 / 𝑦 ) } ) ∧ 𝑧 ∈ ( ◡ 𝐺 “ { 𝑦 } ) ) ↔ ( ( 𝑧 ∈ ℝ ∧ ( 𝐹 ‘ 𝑧 ) = ( 𝐴 / 𝑦 ) ) ∧ ( 𝑧 ∈ ℝ ∧ ( 𝐺 ‘ 𝑧 ) = 𝑦 ) ) ) )
71 elin ⊢ ( 𝑧 ∈ ( ( ◡ 𝐹 “ { ( 𝐴 / 𝑦 ) } ) ∩ ( ◡ 𝐺 “ { 𝑦 } ) ) ↔ ( 𝑧 ∈ ( ◡ 𝐹 “ { ( 𝐴 / 𝑦 ) } ) ∧ 𝑧 ∈ ( ◡ 𝐺 “ { 𝑦 } ) ) )
72 anandi ⊢ ( ( 𝑧 ∈ ℝ ∧ ( ( 𝐹 ‘ 𝑧 ) = ( 𝐴 / 𝑦 ) ∧ ( 𝐺 ‘ 𝑧 ) = 𝑦 ) ) ↔ ( ( 𝑧 ∈ ℝ ∧ ( 𝐹 ‘ 𝑧 ) = ( 𝐴 / 𝑦 ) ) ∧ ( 𝑧 ∈ ℝ ∧ ( 𝐺 ‘ 𝑧 ) = 𝑦 ) ) )
73 70 71 72 3bitr4g ⊢ ( ( 𝜑 ∧ 𝐴 ∈ ( ℂ ∖ { 0 } ) ) → ( 𝑧 ∈ ( ( ◡ 𝐹 “ { ( 𝐴 / 𝑦 ) } ) ∩ ( ◡ 𝐺 “ { 𝑦 } ) ) ↔ ( 𝑧 ∈ ℝ ∧ ( ( 𝐹 ‘ 𝑧 ) = ( 𝐴 / 𝑦 ) ∧ ( 𝐺 ‘ 𝑧 ) = 𝑦 ) ) ) )
74 73 adantr ⊢ ( ( ( 𝜑 ∧ 𝐴 ∈ ( ℂ ∖ { 0 } ) ) ∧ 𝑦 ∈ ( ran 𝐺 ∖ { 0 } ) ) → ( 𝑧 ∈ ( ( ◡ 𝐹 “ { ( 𝐴 / 𝑦 ) } ) ∩ ( ◡ 𝐺 “ { 𝑦 } ) ) ↔ ( 𝑧 ∈ ℝ ∧ ( ( 𝐹 ‘ 𝑧 ) = ( 𝐴 / 𝑦 ) ∧ ( 𝐺 ‘ 𝑧 ) = 𝑦 ) ) ) )
75 eldifi ⊢ ( 𝐴 ∈ ( ℂ ∖ { 0 } ) → 𝐴 ∈ ℂ )
76 75 ad2antlr ⊢ ( ( ( 𝜑 ∧ 𝐴 ∈ ( ℂ ∖ { 0 } ) ) ∧ ( 𝑦 ∈ ( ran 𝐺 ∖ { 0 } ) ∧ 𝑧 ∈ ℝ ) ) → 𝐴 ∈ ℂ )
77 7 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝐴 ∈ ( ℂ ∖ { 0 } ) ) ∧ ( 𝑦 ∈ ( ran 𝐺 ∖ { 0 } ) ∧ 𝑧 ∈ ℝ ) ) → 𝐺 : ℝ ⟶ ℝ )
78 77 frnd ⊢ ( ( ( 𝜑 ∧ 𝐴 ∈ ( ℂ ∖ { 0 } ) ) ∧ ( 𝑦 ∈ ( ran 𝐺 ∖ { 0 } ) ∧ 𝑧 ∈ ℝ ) ) → ran 𝐺 ⊆ ℝ )
79 simprl ⊢ ( ( ( 𝜑 ∧ 𝐴 ∈ ( ℂ ∖ { 0 } ) ) ∧ ( 𝑦 ∈ ( ran 𝐺 ∖ { 0 } ) ∧ 𝑧 ∈ ℝ ) ) → 𝑦 ∈ ( ran 𝐺 ∖ { 0 } ) )
80 eldifsn ⊢ ( 𝑦 ∈ ( ran 𝐺 ∖ { 0 } ) ↔ ( 𝑦 ∈ ran 𝐺 ∧ 𝑦 ≠ 0 ) )
81 79 80 sylib ⊢ ( ( ( 𝜑 ∧ 𝐴 ∈ ( ℂ ∖ { 0 } ) ) ∧ ( 𝑦 ∈ ( ran 𝐺 ∖ { 0 } ) ∧ 𝑧 ∈ ℝ ) ) → ( 𝑦 ∈ ran 𝐺 ∧ 𝑦 ≠ 0 ) )
82 81 simpld ⊢ ( ( ( 𝜑 ∧ 𝐴 ∈ ( ℂ ∖ { 0 } ) ) ∧ ( 𝑦 ∈ ( ran 𝐺 ∖ { 0 } ) ∧ 𝑧 ∈ ℝ ) ) → 𝑦 ∈ ran 𝐺 )
83 78 82 sseldd ⊢ ( ( ( 𝜑 ∧ 𝐴 ∈ ( ℂ ∖ { 0 } ) ) ∧ ( 𝑦 ∈ ( ran 𝐺 ∖ { 0 } ) ∧ 𝑧 ∈ ℝ ) ) → 𝑦 ∈ ℝ )
84 83 recnd ⊢ ( ( ( 𝜑 ∧ 𝐴 ∈ ( ℂ ∖ { 0 } ) ) ∧ ( 𝑦 ∈ ( ran 𝐺 ∖ { 0 } ) ∧ 𝑧 ∈ ℝ ) ) → 𝑦 ∈ ℂ )
85 81 simprd ⊢ ( ( ( 𝜑 ∧ 𝐴 ∈ ( ℂ ∖ { 0 } ) ) ∧ ( 𝑦 ∈ ( ran 𝐺 ∖ { 0 } ) ∧ 𝑧 ∈ ℝ ) ) → 𝑦 ≠ 0 )
86 76 84 85 divcan1d ⊢ ( ( ( 𝜑 ∧ 𝐴 ∈ ( ℂ ∖ { 0 } ) ) ∧ ( 𝑦 ∈ ( ran 𝐺 ∖ { 0 } ) ∧ 𝑧 ∈ ℝ ) ) → ( ( 𝐴 / 𝑦 ) · 𝑦 ) = 𝐴 )
87 oveq12 ⊢ ( ( ( 𝐹 ‘ 𝑧 ) = ( 𝐴 / 𝑦 ) ∧ ( 𝐺 ‘ 𝑧 ) = 𝑦 ) → ( ( 𝐹 ‘ 𝑧 ) · ( 𝐺 ‘ 𝑧 ) ) = ( ( 𝐴 / 𝑦 ) · 𝑦 ) )
88 87 eqeq1d ⊢ ( ( ( 𝐹 ‘ 𝑧 ) = ( 𝐴 / 𝑦 ) ∧ ( 𝐺 ‘ 𝑧 ) = 𝑦 ) → ( ( ( 𝐹 ‘ 𝑧 ) · ( 𝐺 ‘ 𝑧 ) ) = 𝐴 ↔ ( ( 𝐴 / 𝑦 ) · 𝑦 ) = 𝐴 ) )
89 86 88 syl5ibrcom ⊢ ( ( ( 𝜑 ∧ 𝐴 ∈ ( ℂ ∖ { 0 } ) ) ∧ ( 𝑦 ∈ ( ran 𝐺 ∖ { 0 } ) ∧ 𝑧 ∈ ℝ ) ) → ( ( ( 𝐹 ‘ 𝑧 ) = ( 𝐴 / 𝑦 ) ∧ ( 𝐺 ‘ 𝑧 ) = 𝑦 ) → ( ( 𝐹 ‘ 𝑧 ) · ( 𝐺 ‘ 𝑧 ) ) = 𝐴 ) )
90 89 anassrs ⊢ ( ( ( ( 𝜑 ∧ 𝐴 ∈ ( ℂ ∖ { 0 } ) ) ∧ 𝑦 ∈ ( ran 𝐺 ∖ { 0 } ) ) ∧ 𝑧 ∈ ℝ ) → ( ( ( 𝐹 ‘ 𝑧 ) = ( 𝐴 / 𝑦 ) ∧ ( 𝐺 ‘ 𝑧 ) = 𝑦 ) → ( ( 𝐹 ‘ 𝑧 ) · ( 𝐺 ‘ 𝑧 ) ) = 𝐴 ) )
91 90 imdistanda ⊢ ( ( ( 𝜑 ∧ 𝐴 ∈ ( ℂ ∖ { 0 } ) ) ∧ 𝑦 ∈ ( ran 𝐺 ∖ { 0 } ) ) → ( ( 𝑧 ∈ ℝ ∧ ( ( 𝐹 ‘ 𝑧 ) = ( 𝐴 / 𝑦 ) ∧ ( 𝐺 ‘ 𝑧 ) = 𝑦 ) ) → ( 𝑧 ∈ ℝ ∧ ( ( 𝐹 ‘ 𝑧 ) · ( 𝐺 ‘ 𝑧 ) ) = 𝐴 ) ) )
92 74 91 sylbid ⊢ ( ( ( 𝜑 ∧ 𝐴 ∈ ( ℂ ∖ { 0 } ) ) ∧ 𝑦 ∈ ( ran 𝐺 ∖ { 0 } ) ) → ( 𝑧 ∈ ( ( ◡ 𝐹 “ { ( 𝐴 / 𝑦 ) } ) ∩ ( ◡ 𝐺 “ { 𝑦 } ) ) → ( 𝑧 ∈ ℝ ∧ ( ( 𝐹 ‘ 𝑧 ) · ( 𝐺 ‘ 𝑧 ) ) = 𝐴 ) ) )
93 92 rexlimdva ⊢ ( ( 𝜑 ∧ 𝐴 ∈ ( ℂ ∖ { 0 } ) ) → ( ∃ 𝑦 ∈ ( ran 𝐺 ∖ { 0 } ) 𝑧 ∈ ( ( ◡ 𝐹 “ { ( 𝐴 / 𝑦 ) } ) ∩ ( ◡ 𝐺 “ { 𝑦 } ) ) → ( 𝑧 ∈ ℝ ∧ ( ( 𝐹 ‘ 𝑧 ) · ( 𝐺 ‘ 𝑧 ) ) = 𝐴 ) ) )
94 65 93 impbid ⊢ ( ( 𝜑 ∧ 𝐴 ∈ ( ℂ ∖ { 0 } ) ) → ( ( 𝑧 ∈ ℝ ∧ ( ( 𝐹 ‘ 𝑧 ) · ( 𝐺 ‘ 𝑧 ) ) = 𝐴 ) ↔ ∃ 𝑦 ∈ ( ran 𝐺 ∖ { 0 } ) 𝑧 ∈ ( ( ◡ 𝐹 “ { ( 𝐴 / 𝑦 ) } ) ∩ ( ◡ 𝐺 “ { 𝑦 } ) ) ) )
95 15 23 94 3bitrd ⊢ ( ( 𝜑 ∧ 𝐴 ∈ ( ℂ ∖ { 0 } ) ) → ( 𝑧 ∈ ( ◡ ( 𝐹 ∘f · 𝐺 ) “ { 𝐴 } ) ↔ ∃ 𝑦 ∈ ( ran 𝐺 ∖ { 0 } ) 𝑧 ∈ ( ( ◡ 𝐹 “ { ( 𝐴 / 𝑦 ) } ) ∩ ( ◡ 𝐺 “ { 𝑦 } ) ) ) )
96 eliun ⊢ ( 𝑧 ∈ ∪ 𝑦 ∈ ( ran 𝐺 ∖ { 0 } ) ( ( ◡ 𝐹 “ { ( 𝐴 / 𝑦 ) } ) ∩ ( ◡ 𝐺 “ { 𝑦 } ) ) ↔ ∃ 𝑦 ∈ ( ran 𝐺 ∖ { 0 } ) 𝑧 ∈ ( ( ◡ 𝐹 “ { ( 𝐴 / 𝑦 ) } ) ∩ ( ◡ 𝐺 “ { 𝑦 } ) ) )
97 95 96 bitr4di ⊢ ( ( 𝜑 ∧ 𝐴 ∈ ( ℂ ∖ { 0 } ) ) → ( 𝑧 ∈ ( ◡ ( 𝐹 ∘f · 𝐺 ) “ { 𝐴 } ) ↔ 𝑧 ∈ ∪ 𝑦 ∈ ( ran 𝐺 ∖ { 0 } ) ( ( ◡ 𝐹 “ { ( 𝐴 / 𝑦 ) } ) ∩ ( ◡ 𝐺 “ { 𝑦 } ) ) ) )
98 97 eqrdv ⊢ ( ( 𝜑 ∧ 𝐴 ∈ ( ℂ ∖ { 0 } ) ) → ( ◡ ( 𝐹 ∘f · 𝐺 ) “ { 𝐴 } ) = ∪ 𝑦 ∈ ( ran 𝐺 ∖ { 0 } ) ( ( ◡ 𝐹 “ { ( 𝐴 / 𝑦 ) } ) ∩ ( ◡ 𝐺 “ { 𝑦 } ) ) )