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 )