Metamath Proof Explorer


Theorem i1fmulc

Description: A nonnegative constant times a simple function gives another simple function. (Contributed by Mario Carneiro, 25-Jun-2014)

Ref Expression
Hypotheses i1fmulc.2 ( 𝜑𝐹 ∈ dom ∫1 )
i1fmulc.3 ( 𝜑𝐴 ∈ ℝ )
Assertion i1fmulc ( 𝜑 → ( ( ℝ × { 𝐴 } ) ∘f · 𝐹 ) ∈ dom ∫1 )

Proof

Step Hyp Ref Expression
1 i1fmulc.2 ( 𝜑𝐹 ∈ dom ∫1 )
2 i1fmulc.3 ( 𝜑𝐴 ∈ ℝ )
3 reex ℝ ∈ V
4 3 a1i ( ( 𝜑𝐴 = 0 ) → ℝ ∈ V )
5 i1ff ( 𝐹 ∈ dom ∫1𝐹 : ℝ ⟶ ℝ )
6 1 5 syl ( 𝜑𝐹 : ℝ ⟶ ℝ )
7 6 adantr ( ( 𝜑𝐴 = 0 ) → 𝐹 : ℝ ⟶ ℝ )
8 2 adantr ( ( 𝜑𝐴 = 0 ) → 𝐴 ∈ ℝ )
9 0red ( ( 𝜑𝐴 = 0 ) → 0 ∈ ℝ )
10 simplr ( ( ( 𝜑𝐴 = 0 ) ∧ 𝑥 ∈ ℝ ) → 𝐴 = 0 )
11 10 oveq1d ( ( ( 𝜑𝐴 = 0 ) ∧ 𝑥 ∈ ℝ ) → ( 𝐴 · 𝑥 ) = ( 0 · 𝑥 ) )
12 mul02lem2 ( 𝑥 ∈ ℝ → ( 0 · 𝑥 ) = 0 )
13 12 adantl ( ( ( 𝜑𝐴 = 0 ) ∧ 𝑥 ∈ ℝ ) → ( 0 · 𝑥 ) = 0 )
14 11 13 eqtrd ( ( ( 𝜑𝐴 = 0 ) ∧ 𝑥 ∈ ℝ ) → ( 𝐴 · 𝑥 ) = 0 )
15 4 7 8 9 14 caofid2 ( ( 𝜑𝐴 = 0 ) → ( ( ℝ × { 𝐴 } ) ∘f · 𝐹 ) = ( ℝ × { 0 } ) )
16 i1f0 ( ℝ × { 0 } ) ∈ dom ∫1
17 15 16 eqeltrdi ( ( 𝜑𝐴 = 0 ) → ( ( ℝ × { 𝐴 } ) ∘f · 𝐹 ) ∈ dom ∫1 )
18 remulcl ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) → ( 𝑥 · 𝑦 ) ∈ ℝ )
19 18 adantl ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) ) → ( 𝑥 · 𝑦 ) ∈ ℝ )
20 fconst6g ( 𝐴 ∈ ℝ → ( ℝ × { 𝐴 } ) : ℝ ⟶ ℝ )
21 2 20 syl ( 𝜑 → ( ℝ × { 𝐴 } ) : ℝ ⟶ ℝ )
22 3 a1i ( 𝜑 → ℝ ∈ V )
23 inidm ( ℝ ∩ ℝ ) = ℝ
24 19 21 6 22 22 23 off ( 𝜑 → ( ( ℝ × { 𝐴 } ) ∘f · 𝐹 ) : ℝ ⟶ ℝ )
25 24 adantr ( ( 𝜑𝐴 ≠ 0 ) → ( ( ℝ × { 𝐴 } ) ∘f · 𝐹 ) : ℝ ⟶ ℝ )
26 i1frn ( 𝐹 ∈ dom ∫1 → ran 𝐹 ∈ Fin )
27 1 26 syl ( 𝜑 → ran 𝐹 ∈ Fin )
28 ovex ( 𝐴 · 𝑦 ) ∈ V
29 eqid ( 𝑦 ∈ ran 𝐹 ↦ ( 𝐴 · 𝑦 ) ) = ( 𝑦 ∈ ran 𝐹 ↦ ( 𝐴 · 𝑦 ) )
30 28 29 fnmpti ( 𝑦 ∈ ran 𝐹 ↦ ( 𝐴 · 𝑦 ) ) Fn ran 𝐹
31 dffn4 ( ( 𝑦 ∈ ran 𝐹 ↦ ( 𝐴 · 𝑦 ) ) Fn ran 𝐹 ↔ ( 𝑦 ∈ ran 𝐹 ↦ ( 𝐴 · 𝑦 ) ) : ran 𝐹onto→ ran ( 𝑦 ∈ ran 𝐹 ↦ ( 𝐴 · 𝑦 ) ) )
32 30 31 mpbi ( 𝑦 ∈ ran 𝐹 ↦ ( 𝐴 · 𝑦 ) ) : ran 𝐹onto→ ran ( 𝑦 ∈ ran 𝐹 ↦ ( 𝐴 · 𝑦 ) )
33 fofi ( ( ran 𝐹 ∈ Fin ∧ ( 𝑦 ∈ ran 𝐹 ↦ ( 𝐴 · 𝑦 ) ) : ran 𝐹onto→ ran ( 𝑦 ∈ ran 𝐹 ↦ ( 𝐴 · 𝑦 ) ) ) → ran ( 𝑦 ∈ ran 𝐹 ↦ ( 𝐴 · 𝑦 ) ) ∈ Fin )
34 27 32 33 sylancl ( 𝜑 → ran ( 𝑦 ∈ ran 𝐹 ↦ ( 𝐴 · 𝑦 ) ) ∈ Fin )
35 id ( 𝑤 ∈ ran 𝐹𝑤 ∈ ran 𝐹 )
36 elsni ( 𝑥 ∈ { 𝐴 } → 𝑥 = 𝐴 )
37 36 oveq1d ( 𝑥 ∈ { 𝐴 } → ( 𝑥 · 𝑤 ) = ( 𝐴 · 𝑤 ) )
38 oveq2 ( 𝑦 = 𝑤 → ( 𝐴 · 𝑦 ) = ( 𝐴 · 𝑤 ) )
39 38 rspceeqv ( ( 𝑤 ∈ ran 𝐹 ∧ ( 𝑥 · 𝑤 ) = ( 𝐴 · 𝑤 ) ) → ∃ 𝑦 ∈ ran 𝐹 ( 𝑥 · 𝑤 ) = ( 𝐴 · 𝑦 ) )
40 35 37 39 syl2anr ( ( 𝑥 ∈ { 𝐴 } ∧ 𝑤 ∈ ran 𝐹 ) → ∃ 𝑦 ∈ ran 𝐹 ( 𝑥 · 𝑤 ) = ( 𝐴 · 𝑦 ) )
41 ovex ( 𝑥 · 𝑤 ) ∈ V
42 eqeq1 ( 𝑧 = ( 𝑥 · 𝑤 ) → ( 𝑧 = ( 𝐴 · 𝑦 ) ↔ ( 𝑥 · 𝑤 ) = ( 𝐴 · 𝑦 ) ) )
43 42 rexbidv ( 𝑧 = ( 𝑥 · 𝑤 ) → ( ∃ 𝑦 ∈ ran 𝐹 𝑧 = ( 𝐴 · 𝑦 ) ↔ ∃ 𝑦 ∈ ran 𝐹 ( 𝑥 · 𝑤 ) = ( 𝐴 · 𝑦 ) ) )
44 41 43 elab ( ( 𝑥 · 𝑤 ) ∈ { 𝑧 ∣ ∃ 𝑦 ∈ ran 𝐹 𝑧 = ( 𝐴 · 𝑦 ) } ↔ ∃ 𝑦 ∈ ran 𝐹 ( 𝑥 · 𝑤 ) = ( 𝐴 · 𝑦 ) )
45 40 44 sylibr ( ( 𝑥 ∈ { 𝐴 } ∧ 𝑤 ∈ ran 𝐹 ) → ( 𝑥 · 𝑤 ) ∈ { 𝑧 ∣ ∃ 𝑦 ∈ ran 𝐹 𝑧 = ( 𝐴 · 𝑦 ) } )
46 45 adantl ( ( 𝜑 ∧ ( 𝑥 ∈ { 𝐴 } ∧ 𝑤 ∈ ran 𝐹 ) ) → ( 𝑥 · 𝑤 ) ∈ { 𝑧 ∣ ∃ 𝑦 ∈ ran 𝐹 𝑧 = ( 𝐴 · 𝑦 ) } )
47 fconstg ( 𝐴 ∈ ℝ → ( ℝ × { 𝐴 } ) : ℝ ⟶ { 𝐴 } )
48 2 47 syl ( 𝜑 → ( ℝ × { 𝐴 } ) : ℝ ⟶ { 𝐴 } )
49 6 ffnd ( 𝜑𝐹 Fn ℝ )
50 dffn3 ( 𝐹 Fn ℝ ↔ 𝐹 : ℝ ⟶ ran 𝐹 )
51 49 50 sylib ( 𝜑𝐹 : ℝ ⟶ ran 𝐹 )
52 46 48 51 22 22 23 off ( 𝜑 → ( ( ℝ × { 𝐴 } ) ∘f · 𝐹 ) : ℝ ⟶ { 𝑧 ∣ ∃ 𝑦 ∈ ran 𝐹 𝑧 = ( 𝐴 · 𝑦 ) } )
53 52 frnd ( 𝜑 → ran ( ( ℝ × { 𝐴 } ) ∘f · 𝐹 ) ⊆ { 𝑧 ∣ ∃ 𝑦 ∈ ran 𝐹 𝑧 = ( 𝐴 · 𝑦 ) } )
54 29 rnmpt ran ( 𝑦 ∈ ran 𝐹 ↦ ( 𝐴 · 𝑦 ) ) = { 𝑧 ∣ ∃ 𝑦 ∈ ran 𝐹 𝑧 = ( 𝐴 · 𝑦 ) }
55 53 54 sseqtrrdi ( 𝜑 → ran ( ( ℝ × { 𝐴 } ) ∘f · 𝐹 ) ⊆ ran ( 𝑦 ∈ ran 𝐹 ↦ ( 𝐴 · 𝑦 ) ) )
56 34 55 ssfid ( 𝜑 → ran ( ( ℝ × { 𝐴 } ) ∘f · 𝐹 ) ∈ Fin )
57 56 adantr ( ( 𝜑𝐴 ≠ 0 ) → ran ( ( ℝ × { 𝐴 } ) ∘f · 𝐹 ) ∈ Fin )
58 24 frnd ( 𝜑 → ran ( ( ℝ × { 𝐴 } ) ∘f · 𝐹 ) ⊆ ℝ )
59 58 ssdifssd ( 𝜑 → ( ran ( ( ℝ × { 𝐴 } ) ∘f · 𝐹 ) ∖ { 0 } ) ⊆ ℝ )
60 59 adantr ( ( 𝜑𝐴 ≠ 0 ) → ( ran ( ( ℝ × { 𝐴 } ) ∘f · 𝐹 ) ∖ { 0 } ) ⊆ ℝ )
61 60 sselda ( ( ( 𝜑𝐴 ≠ 0 ) ∧ 𝑦 ∈ ( ran ( ( ℝ × { 𝐴 } ) ∘f · 𝐹 ) ∖ { 0 } ) ) → 𝑦 ∈ ℝ )
62 1 2 i1fmulclem ( ( ( 𝜑𝐴 ≠ 0 ) ∧ 𝑦 ∈ ℝ ) → ( ( ( ℝ × { 𝐴 } ) ∘f · 𝐹 ) “ { 𝑦 } ) = ( 𝐹 “ { ( 𝑦 / 𝐴 ) } ) )
63 61 62 syldan ( ( ( 𝜑𝐴 ≠ 0 ) ∧ 𝑦 ∈ ( ran ( ( ℝ × { 𝐴 } ) ∘f · 𝐹 ) ∖ { 0 } ) ) → ( ( ( ℝ × { 𝐴 } ) ∘f · 𝐹 ) “ { 𝑦 } ) = ( 𝐹 “ { ( 𝑦 / 𝐴 ) } ) )
64 i1fima ( 𝐹 ∈ dom ∫1 → ( 𝐹 “ { ( 𝑦 / 𝐴 ) } ) ∈ dom vol )
65 1 64 syl ( 𝜑 → ( 𝐹 “ { ( 𝑦 / 𝐴 ) } ) ∈ dom vol )
66 65 ad2antrr ( ( ( 𝜑𝐴 ≠ 0 ) ∧ 𝑦 ∈ ( ran ( ( ℝ × { 𝐴 } ) ∘f · 𝐹 ) ∖ { 0 } ) ) → ( 𝐹 “ { ( 𝑦 / 𝐴 ) } ) ∈ dom vol )
67 63 66 eqeltrd ( ( ( 𝜑𝐴 ≠ 0 ) ∧ 𝑦 ∈ ( ran ( ( ℝ × { 𝐴 } ) ∘f · 𝐹 ) ∖ { 0 } ) ) → ( ( ( ℝ × { 𝐴 } ) ∘f · 𝐹 ) “ { 𝑦 } ) ∈ dom vol )
68 63 fveq2d ( ( ( 𝜑𝐴 ≠ 0 ) ∧ 𝑦 ∈ ( ran ( ( ℝ × { 𝐴 } ) ∘f · 𝐹 ) ∖ { 0 } ) ) → ( vol ‘ ( ( ( ℝ × { 𝐴 } ) ∘f · 𝐹 ) “ { 𝑦 } ) ) = ( vol ‘ ( 𝐹 “ { ( 𝑦 / 𝐴 ) } ) ) )
69 1 ad2antrr ( ( ( 𝜑𝐴 ≠ 0 ) ∧ 𝑦 ∈ ( ran ( ( ℝ × { 𝐴 } ) ∘f · 𝐹 ) ∖ { 0 } ) ) → 𝐹 ∈ dom ∫1 )
70 2 ad2antrr ( ( ( 𝜑𝐴 ≠ 0 ) ∧ 𝑦 ∈ ( ran ( ( ℝ × { 𝐴 } ) ∘f · 𝐹 ) ∖ { 0 } ) ) → 𝐴 ∈ ℝ )
71 simplr ( ( ( 𝜑𝐴 ≠ 0 ) ∧ 𝑦 ∈ ( ran ( ( ℝ × { 𝐴 } ) ∘f · 𝐹 ) ∖ { 0 } ) ) → 𝐴 ≠ 0 )
72 61 70 71 redivcld ( ( ( 𝜑𝐴 ≠ 0 ) ∧ 𝑦 ∈ ( ran ( ( ℝ × { 𝐴 } ) ∘f · 𝐹 ) ∖ { 0 } ) ) → ( 𝑦 / 𝐴 ) ∈ ℝ )
73 61 recnd ( ( ( 𝜑𝐴 ≠ 0 ) ∧ 𝑦 ∈ ( ran ( ( ℝ × { 𝐴 } ) ∘f · 𝐹 ) ∖ { 0 } ) ) → 𝑦 ∈ ℂ )
74 70 recnd ( ( ( 𝜑𝐴 ≠ 0 ) ∧ 𝑦 ∈ ( ran ( ( ℝ × { 𝐴 } ) ∘f · 𝐹 ) ∖ { 0 } ) ) → 𝐴 ∈ ℂ )
75 eldifsni ( 𝑦 ∈ ( ran ( ( ℝ × { 𝐴 } ) ∘f · 𝐹 ) ∖ { 0 } ) → 𝑦 ≠ 0 )
76 75 adantl ( ( ( 𝜑𝐴 ≠ 0 ) ∧ 𝑦 ∈ ( ran ( ( ℝ × { 𝐴 } ) ∘f · 𝐹 ) ∖ { 0 } ) ) → 𝑦 ≠ 0 )
77 73 74 76 71 divne0d ( ( ( 𝜑𝐴 ≠ 0 ) ∧ 𝑦 ∈ ( ran ( ( ℝ × { 𝐴 } ) ∘f · 𝐹 ) ∖ { 0 } ) ) → ( 𝑦 / 𝐴 ) ≠ 0 )
78 eldifsn ( ( 𝑦 / 𝐴 ) ∈ ( ℝ ∖ { 0 } ) ↔ ( ( 𝑦 / 𝐴 ) ∈ ℝ ∧ ( 𝑦 / 𝐴 ) ≠ 0 ) )
79 72 77 78 sylanbrc ( ( ( 𝜑𝐴 ≠ 0 ) ∧ 𝑦 ∈ ( ran ( ( ℝ × { 𝐴 } ) ∘f · 𝐹 ) ∖ { 0 } ) ) → ( 𝑦 / 𝐴 ) ∈ ( ℝ ∖ { 0 } ) )
80 i1fima2sn ( ( 𝐹 ∈ dom ∫1 ∧ ( 𝑦 / 𝐴 ) ∈ ( ℝ ∖ { 0 } ) ) → ( vol ‘ ( 𝐹 “ { ( 𝑦 / 𝐴 ) } ) ) ∈ ℝ )
81 69 79 80 syl2anc ( ( ( 𝜑𝐴 ≠ 0 ) ∧ 𝑦 ∈ ( ran ( ( ℝ × { 𝐴 } ) ∘f · 𝐹 ) ∖ { 0 } ) ) → ( vol ‘ ( 𝐹 “ { ( 𝑦 / 𝐴 ) } ) ) ∈ ℝ )
82 68 81 eqeltrd ( ( ( 𝜑𝐴 ≠ 0 ) ∧ 𝑦 ∈ ( ran ( ( ℝ × { 𝐴 } ) ∘f · 𝐹 ) ∖ { 0 } ) ) → ( vol ‘ ( ( ( ℝ × { 𝐴 } ) ∘f · 𝐹 ) “ { 𝑦 } ) ) ∈ ℝ )
83 25 57 67 82 i1fd ( ( 𝜑𝐴 ≠ 0 ) → ( ( ℝ × { 𝐴 } ) ∘f · 𝐹 ) ∈ dom ∫1 )
84 17 83 pm2.61dane ( 𝜑 → ( ( ℝ × { 𝐴 } ) ∘f · 𝐹 ) ∈ dom ∫1 )