This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem i1fmulclem

Description: Decompose the preimage of a constant times a function. (Contributed by Mario Carneiro, 25-Jun-2014)

Ref Expression
Hypotheses i1fmulc.2 ⊢ ( 𝜑 → 𝐹 ∈ dom ∫1 )
i1fmulc.3 ⊢ ( 𝜑 → 𝐴 ∈ ℝ )
Assertion i1fmulclem ( ( ( 𝜑 ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ) → ( ◡ ( ( ℝ × { 𝐴 } ) ∘f · 𝐹 ) “ { 𝐵 } ) = ( ◡ 𝐹 “ { ( 𝐵 / 𝐴 ) } ) )

Proof

Step Hyp Ref Expression
1 i1fmulc.2 ⊢ ( 𝜑 → 𝐹 ∈ dom ∫1 )
2 i1fmulc.3 ⊢ ( 𝜑 → 𝐴 ∈ ℝ )
3 reex ⊢ ℝ ∈ V
4 3 a1i ⊢ ( 𝜑 → ℝ ∈ V )
5 i1ff ⊢ ( 𝐹 ∈ dom ∫1 → 𝐹 : ℝ ⟶ ℝ )
6 1 5 syl ⊢ ( 𝜑 → 𝐹 : ℝ ⟶ ℝ )
7 6 ffnd ⊢ ( 𝜑 → 𝐹 Fn ℝ )
8 eqidd ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ℝ ) → ( 𝐹 ‘ 𝑧 ) = ( 𝐹 ‘ 𝑧 ) )
9 4 2 7 8 ofc1 ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ℝ ) → ( ( ( ℝ × { 𝐴 } ) ∘f · 𝐹 ) ‘ 𝑧 ) = ( 𝐴 · ( 𝐹 ‘ 𝑧 ) ) )
10 9 ad4ant14 ⊢ ( ( ( ( 𝜑 ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ) ∧ 𝑧 ∈ ℝ ) → ( ( ( ℝ × { 𝐴 } ) ∘f · 𝐹 ) ‘ 𝑧 ) = ( 𝐴 · ( 𝐹 ‘ 𝑧 ) ) )
11 10 eqeq1d ⊢ ( ( ( ( 𝜑 ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ) ∧ 𝑧 ∈ ℝ ) → ( ( ( ( ℝ × { 𝐴 } ) ∘f · 𝐹 ) ‘ 𝑧 ) = 𝐵 ↔ ( 𝐴 · ( 𝐹 ‘ 𝑧 ) ) = 𝐵 ) )
12 eqcom ⊢ ( ( 𝐹 ‘ 𝑧 ) = ( 𝐵 / 𝐴 ) ↔ ( 𝐵 / 𝐴 ) = ( 𝐹 ‘ 𝑧 ) )
13 simplr ⊢ ( ( ( ( 𝜑 ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ) ∧ 𝑧 ∈ ℝ ) → 𝐵 ∈ ℝ )
14 13 recnd ⊢ ( ( ( ( 𝜑 ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ) ∧ 𝑧 ∈ ℝ ) → 𝐵 ∈ ℂ )
15 2 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ) ∧ 𝑧 ∈ ℝ ) → 𝐴 ∈ ℝ )
16 15 recnd ⊢ ( ( ( ( 𝜑 ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ) ∧ 𝑧 ∈ ℝ ) → 𝐴 ∈ ℂ )
17 6 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ) → 𝐹 : ℝ ⟶ ℝ )
18 17 ffvelcdmda ⊢ ( ( ( ( 𝜑 ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ) ∧ 𝑧 ∈ ℝ ) → ( 𝐹 ‘ 𝑧 ) ∈ ℝ )
19 18 recnd ⊢ ( ( ( ( 𝜑 ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ) ∧ 𝑧 ∈ ℝ ) → ( 𝐹 ‘ 𝑧 ) ∈ ℂ )
20 simpllr ⊢ ( ( ( ( 𝜑 ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ) ∧ 𝑧 ∈ ℝ ) → 𝐴 ≠ 0 )
21 14 16 19 20 divmuld ⊢ ( ( ( ( 𝜑 ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ) ∧ 𝑧 ∈ ℝ ) → ( ( 𝐵 / 𝐴 ) = ( 𝐹 ‘ 𝑧 ) ↔ ( 𝐴 · ( 𝐹 ‘ 𝑧 ) ) = 𝐵 ) )
22 12 21 bitrid ⊢ ( ( ( ( 𝜑 ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ) ∧ 𝑧 ∈ ℝ ) → ( ( 𝐹 ‘ 𝑧 ) = ( 𝐵 / 𝐴 ) ↔ ( 𝐴 · ( 𝐹 ‘ 𝑧 ) ) = 𝐵 ) )
23 11 22 bitr4d ⊢ ( ( ( ( 𝜑 ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ) ∧ 𝑧 ∈ ℝ ) → ( ( ( ( ℝ × { 𝐴 } ) ∘f · 𝐹 ) ‘ 𝑧 ) = 𝐵 ↔ ( 𝐹 ‘ 𝑧 ) = ( 𝐵 / 𝐴 ) ) )
24 23 pm5.32da ⊢ ( ( ( 𝜑 ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ) → ( ( 𝑧 ∈ ℝ ∧ ( ( ( ℝ × { 𝐴 } ) ∘f · 𝐹 ) ‘ 𝑧 ) = 𝐵 ) ↔ ( 𝑧 ∈ ℝ ∧ ( 𝐹 ‘ 𝑧 ) = ( 𝐵 / 𝐴 ) ) ) )
25 remulcl ⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) → ( 𝑥 · 𝑦 ) ∈ ℝ )
26 25 adantl ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) ) → ( 𝑥 · 𝑦 ) ∈ ℝ )
27 fconstg ⊢ ( 𝐴 ∈ ℝ → ( ℝ × { 𝐴 } ) : ℝ ⟶ { 𝐴 } )
28 2 27 syl ⊢ ( 𝜑 → ( ℝ × { 𝐴 } ) : ℝ ⟶ { 𝐴 } )
29 2 snssd ⊢ ( 𝜑 → { 𝐴 } ⊆ ℝ )
30 28 29 fssd ⊢ ( 𝜑 → ( ℝ × { 𝐴 } ) : ℝ ⟶ ℝ )
31 inidm ⊢ ( ℝ ∩ ℝ ) = ℝ
32 26 30 6 4 4 31 off ⊢ ( 𝜑 → ( ( ℝ × { 𝐴 } ) ∘f · 𝐹 ) : ℝ ⟶ ℝ )
33 32 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ) → ( ( ℝ × { 𝐴 } ) ∘f · 𝐹 ) : ℝ ⟶ ℝ )
34 33 ffnd ⊢ ( ( ( 𝜑 ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ) → ( ( ℝ × { 𝐴 } ) ∘f · 𝐹 ) Fn ℝ )
35 fniniseg ⊢ ( ( ( ℝ × { 𝐴 } ) ∘f · 𝐹 ) Fn ℝ → ( 𝑧 ∈ ( ◡ ( ( ℝ × { 𝐴 } ) ∘f · 𝐹 ) “ { 𝐵 } ) ↔ ( 𝑧 ∈ ℝ ∧ ( ( ( ℝ × { 𝐴 } ) ∘f · 𝐹 ) ‘ 𝑧 ) = 𝐵 ) ) )
36 34 35 syl ⊢ ( ( ( 𝜑 ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ) → ( 𝑧 ∈ ( ◡ ( ( ℝ × { 𝐴 } ) ∘f · 𝐹 ) “ { 𝐵 } ) ↔ ( 𝑧 ∈ ℝ ∧ ( ( ( ℝ × { 𝐴 } ) ∘f · 𝐹 ) ‘ 𝑧 ) = 𝐵 ) ) )
37 17 ffnd ⊢ ( ( ( 𝜑 ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ) → 𝐹 Fn ℝ )
38 fniniseg ⊢ ( 𝐹 Fn ℝ → ( 𝑧 ∈ ( ◡ 𝐹 “ { ( 𝐵 / 𝐴 ) } ) ↔ ( 𝑧 ∈ ℝ ∧ ( 𝐹 ‘ 𝑧 ) = ( 𝐵 / 𝐴 ) ) ) )
39 37 38 syl ⊢ ( ( ( 𝜑 ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ) → ( 𝑧 ∈ ( ◡ 𝐹 “ { ( 𝐵 / 𝐴 ) } ) ↔ ( 𝑧 ∈ ℝ ∧ ( 𝐹 ‘ 𝑧 ) = ( 𝐵 / 𝐴 ) ) ) )
40 24 36 39 3bitr4d ⊢ ( ( ( 𝜑 ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ) → ( 𝑧 ∈ ( ◡ ( ( ℝ × { 𝐴 } ) ∘f · 𝐹 ) “ { 𝐵 } ) ↔ 𝑧 ∈ ( ◡ 𝐹 “ { ( 𝐵 / 𝐴 ) } ) ) )
41 40 eqrdv ⊢ ( ( ( 𝜑 ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ) → ( ◡ ( ( ℝ × { 𝐴 } ) ∘f · 𝐹 ) “ { 𝐵 } ) = ( ◡ 𝐹 “ { ( 𝐵 / 𝐴 ) } ) )