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 · 𝐹 ) “ { 𝐵 } ) = ( ◡ 𝐹 “ { ( 𝐵 / 𝐴 ) } ) )