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 )