i1fres

Description: The "restriction" of a simple function to a measurable subset is simple. (It's not actually a restriction because it is zero instead of undefined outside A .) (Contributed by Mario Carneiro, 29-Jun-2014)

		Ref	Expression
	Hypothesis	i1fres.1	⊢ 𝐺 = ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ 𝐴 , ( 𝐹 ‘ 𝑥 ) , 0 ) )
	Assertion	i1fres	⊢ ( ( 𝐹 ∈ dom ∫₁ ∧ 𝐴 ∈ dom vol ) → 𝐺 ∈ dom ∫₁ )

Proof

Step	Hyp	Ref	Expression
1		i1fres.1	⊢ 𝐺 = ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ 𝐴 , ( 𝐹 ‘ 𝑥 ) , 0 ) )
2		i1ff	⊢ ( 𝐹 ∈ dom ∫₁ → 𝐹 : ℝ ⟶ ℝ )
3	2	adantr	⊢ ( ( 𝐹 ∈ dom ∫₁ ∧ 𝐴 ∈ dom vol ) → 𝐹 : ℝ ⟶ ℝ )
4	3	ffnd	⊢ ( ( 𝐹 ∈ dom ∫₁ ∧ 𝐴 ∈ dom vol ) → 𝐹 Fn ℝ )
5		fnfvelrn	⊢ ( ( 𝐹 Fn ℝ ∧ 𝑥 ∈ ℝ ) → ( 𝐹 ‘ 𝑥 ) ∈ ran 𝐹 )
6	4 5	sylan	⊢ ( ( ( 𝐹 ∈ dom ∫₁ ∧ 𝐴 ∈ dom vol ) ∧ 𝑥 ∈ ℝ ) → ( 𝐹 ‘ 𝑥 ) ∈ ran 𝐹 )
7		i1f0rn	⊢ ( 𝐹 ∈ dom ∫₁ → 0 ∈ ran 𝐹 )
8	7	ad2antrr	⊢ ( ( ( 𝐹 ∈ dom ∫₁ ∧ 𝐴 ∈ dom vol ) ∧ 𝑥 ∈ ℝ ) → 0 ∈ ran 𝐹 )
9	6 8	ifcld	⊢ ( ( ( 𝐹 ∈ dom ∫₁ ∧ 𝐴 ∈ dom vol ) ∧ 𝑥 ∈ ℝ ) → if ( 𝑥 ∈ 𝐴 , ( 𝐹 ‘ 𝑥 ) , 0 ) ∈ ran 𝐹 )
10	9 1	fmptd	⊢ ( ( 𝐹 ∈ dom ∫₁ ∧ 𝐴 ∈ dom vol ) → 𝐺 : ℝ ⟶ ran 𝐹 )
11	3	frnd	⊢ ( ( 𝐹 ∈ dom ∫₁ ∧ 𝐴 ∈ dom vol ) → ran 𝐹 ⊆ ℝ )
12	10 11	fssd	⊢ ( ( 𝐹 ∈ dom ∫₁ ∧ 𝐴 ∈ dom vol ) → 𝐺 : ℝ ⟶ ℝ )
13		i1frn	⊢ ( 𝐹 ∈ dom ∫₁ → ran 𝐹 ∈ Fin )
14	13	adantr	⊢ ( ( 𝐹 ∈ dom ∫₁ ∧ 𝐴 ∈ dom vol ) → ran 𝐹 ∈ Fin )
15	10	frnd	⊢ ( ( 𝐹 ∈ dom ∫₁ ∧ 𝐴 ∈ dom vol ) → ran 𝐺 ⊆ ran 𝐹 )
16	14 15	ssfid	⊢ ( ( 𝐹 ∈ dom ∫₁ ∧ 𝐴 ∈ dom vol ) → ran 𝐺 ∈ Fin )
17		eleq1w	⊢ ( 𝑥 = 𝑧 → ( 𝑥 ∈ 𝐴 ↔ 𝑧 ∈ 𝐴 ) )
18		fveq2	⊢ ( 𝑥 = 𝑧 → ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑧 ) )
19	17 18	ifbieq1d	⊢ ( 𝑥 = 𝑧 → if ( 𝑥 ∈ 𝐴 , ( 𝐹 ‘ 𝑥 ) , 0 ) = if ( 𝑧 ∈ 𝐴 , ( 𝐹 ‘ 𝑧 ) , 0 ) )
20		fvex	⊢ ( 𝐹 ‘ 𝑧 ) ∈ V
21		c0ex	⊢ 0 ∈ V
22	20 21	ifex	⊢ if ( 𝑧 ∈ 𝐴 , ( 𝐹 ‘ 𝑧 ) , 0 ) ∈ V
23	19 1 22	fvmpt	⊢ ( 𝑧 ∈ ℝ → ( 𝐺 ‘ 𝑧 ) = if ( 𝑧 ∈ 𝐴 , ( 𝐹 ‘ 𝑧 ) , 0 ) )
24	23	adantl	⊢ ( ( ( ( 𝐹 ∈ dom ∫₁ ∧ 𝐴 ∈ dom vol ) ∧ 𝑦 ∈ ( ran 𝐺 ∖ { 0 } ) ) ∧ 𝑧 ∈ ℝ ) → ( 𝐺 ‘ 𝑧 ) = if ( 𝑧 ∈ 𝐴 , ( 𝐹 ‘ 𝑧 ) , 0 ) )
25	24	eqeq1d	⊢ ( ( ( ( 𝐹 ∈ dom ∫₁ ∧ 𝐴 ∈ dom vol ) ∧ 𝑦 ∈ ( ran 𝐺 ∖ { 0 } ) ) ∧ 𝑧 ∈ ℝ ) → ( ( 𝐺 ‘ 𝑧 ) = 𝑦 ↔ if ( 𝑧 ∈ 𝐴 , ( 𝐹 ‘ 𝑧 ) , 0 ) = 𝑦 ) )
26		eldifsni	⊢ ( 𝑦 ∈ ( ran 𝐺 ∖ { 0 } ) → 𝑦 ≠ 0 )
27	26	ad2antlr	⊢ ( ( ( ( 𝐹 ∈ dom ∫₁ ∧ 𝐴 ∈ dom vol ) ∧ 𝑦 ∈ ( ran 𝐺 ∖ { 0 } ) ) ∧ 𝑧 ∈ ℝ ) → 𝑦 ≠ 0 )
28	27	necomd	⊢ ( ( ( ( 𝐹 ∈ dom ∫₁ ∧ 𝐴 ∈ dom vol ) ∧ 𝑦 ∈ ( ran 𝐺 ∖ { 0 } ) ) ∧ 𝑧 ∈ ℝ ) → 0 ≠ 𝑦 )
29		iffalse	⊢ ( ¬ 𝑧 ∈ 𝐴 → if ( 𝑧 ∈ 𝐴 , ( 𝐹 ‘ 𝑧 ) , 0 ) = 0 )
30	29	neeq1d	⊢ ( ¬ 𝑧 ∈ 𝐴 → ( if ( 𝑧 ∈ 𝐴 , ( 𝐹 ‘ 𝑧 ) , 0 ) ≠ 𝑦 ↔ 0 ≠ 𝑦 ) )
31	28 30	syl5ibrcom	⊢ ( ( ( ( 𝐹 ∈ dom ∫₁ ∧ 𝐴 ∈ dom vol ) ∧ 𝑦 ∈ ( ran 𝐺 ∖ { 0 } ) ) ∧ 𝑧 ∈ ℝ ) → ( ¬ 𝑧 ∈ 𝐴 → if ( 𝑧 ∈ 𝐴 , ( 𝐹 ‘ 𝑧 ) , 0 ) ≠ 𝑦 ) )
32	31	necon4bd	⊢ ( ( ( ( 𝐹 ∈ dom ∫₁ ∧ 𝐴 ∈ dom vol ) ∧ 𝑦 ∈ ( ran 𝐺 ∖ { 0 } ) ) ∧ 𝑧 ∈ ℝ ) → ( if ( 𝑧 ∈ 𝐴 , ( 𝐹 ‘ 𝑧 ) , 0 ) = 𝑦 → 𝑧 ∈ 𝐴 ) )
33	32	pm4.71rd	⊢ ( ( ( ( 𝐹 ∈ dom ∫₁ ∧ 𝐴 ∈ dom vol ) ∧ 𝑦 ∈ ( ran 𝐺 ∖ { 0 } ) ) ∧ 𝑧 ∈ ℝ ) → ( if ( 𝑧 ∈ 𝐴 , ( 𝐹 ‘ 𝑧 ) , 0 ) = 𝑦 ↔ ( 𝑧 ∈ 𝐴 ∧ if ( 𝑧 ∈ 𝐴 , ( 𝐹 ‘ 𝑧 ) , 0 ) = 𝑦 ) ) )
34	25 33	bitrd	⊢ ( ( ( ( 𝐹 ∈ dom ∫₁ ∧ 𝐴 ∈ dom vol ) ∧ 𝑦 ∈ ( ran 𝐺 ∖ { 0 } ) ) ∧ 𝑧 ∈ ℝ ) → ( ( 𝐺 ‘ 𝑧 ) = 𝑦 ↔ ( 𝑧 ∈ 𝐴 ∧ if ( 𝑧 ∈ 𝐴 , ( 𝐹 ‘ 𝑧 ) , 0 ) = 𝑦 ) ) )
35		iftrue	⊢ ( 𝑧 ∈ 𝐴 → if ( 𝑧 ∈ 𝐴 , ( 𝐹 ‘ 𝑧 ) , 0 ) = ( 𝐹 ‘ 𝑧 ) )
36	35	eqeq1d	⊢ ( 𝑧 ∈ 𝐴 → ( if ( 𝑧 ∈ 𝐴 , ( 𝐹 ‘ 𝑧 ) , 0 ) = 𝑦 ↔ ( 𝐹 ‘ 𝑧 ) = 𝑦 ) )
37	36	pm5.32i	⊢ ( ( 𝑧 ∈ 𝐴 ∧ if ( 𝑧 ∈ 𝐴 , ( 𝐹 ‘ 𝑧 ) , 0 ) = 𝑦 ) ↔ ( 𝑧 ∈ 𝐴 ∧ ( 𝐹 ‘ 𝑧 ) = 𝑦 ) )
38	34 37	bitrdi	⊢ ( ( ( ( 𝐹 ∈ dom ∫₁ ∧ 𝐴 ∈ dom vol ) ∧ 𝑦 ∈ ( ran 𝐺 ∖ { 0 } ) ) ∧ 𝑧 ∈ ℝ ) → ( ( 𝐺 ‘ 𝑧 ) = 𝑦 ↔ ( 𝑧 ∈ 𝐴 ∧ ( 𝐹 ‘ 𝑧 ) = 𝑦 ) ) )
39	38	pm5.32da	⊢ ( ( ( 𝐹 ∈ dom ∫₁ ∧ 𝐴 ∈ dom vol ) ∧ 𝑦 ∈ ( ran 𝐺 ∖ { 0 } ) ) → ( ( 𝑧 ∈ ℝ ∧ ( 𝐺 ‘ 𝑧 ) = 𝑦 ) ↔ ( 𝑧 ∈ ℝ ∧ ( 𝑧 ∈ 𝐴 ∧ ( 𝐹 ‘ 𝑧 ) = 𝑦 ) ) ) )
40		an12	⊢ ( ( 𝑧 ∈ ℝ ∧ ( 𝑧 ∈ 𝐴 ∧ ( 𝐹 ‘ 𝑧 ) = 𝑦 ) ) ↔ ( 𝑧 ∈ 𝐴 ∧ ( 𝑧 ∈ ℝ ∧ ( 𝐹 ‘ 𝑧 ) = 𝑦 ) ) )
41	39 40	bitrdi	⊢ ( ( ( 𝐹 ∈ dom ∫₁ ∧ 𝐴 ∈ dom vol ) ∧ 𝑦 ∈ ( ran 𝐺 ∖ { 0 } ) ) → ( ( 𝑧 ∈ ℝ ∧ ( 𝐺 ‘ 𝑧 ) = 𝑦 ) ↔ ( 𝑧 ∈ 𝐴 ∧ ( 𝑧 ∈ ℝ ∧ ( 𝐹 ‘ 𝑧 ) = 𝑦 ) ) ) )
42	10	ffnd	⊢ ( ( 𝐹 ∈ dom ∫₁ ∧ 𝐴 ∈ dom vol ) → 𝐺 Fn ℝ )
43	42	adantr	⊢ ( ( ( 𝐹 ∈ dom ∫₁ ∧ 𝐴 ∈ dom vol ) ∧ 𝑦 ∈ ( ran 𝐺 ∖ { 0 } ) ) → 𝐺 Fn ℝ )
44		fniniseg	⊢ ( 𝐺 Fn ℝ → ( 𝑧 ∈ ( ^◡ 𝐺 “ { 𝑦 } ) ↔ ( 𝑧 ∈ ℝ ∧ ( 𝐺 ‘ 𝑧 ) = 𝑦 ) ) )
45	43 44	syl	⊢ ( ( ( 𝐹 ∈ dom ∫₁ ∧ 𝐴 ∈ dom vol ) ∧ 𝑦 ∈ ( ran 𝐺 ∖ { 0 } ) ) → ( 𝑧 ∈ ( ^◡ 𝐺 “ { 𝑦 } ) ↔ ( 𝑧 ∈ ℝ ∧ ( 𝐺 ‘ 𝑧 ) = 𝑦 ) ) )
46	4	adantr	⊢ ( ( ( 𝐹 ∈ dom ∫₁ ∧ 𝐴 ∈ dom vol ) ∧ 𝑦 ∈ ( ran 𝐺 ∖ { 0 } ) ) → 𝐹 Fn ℝ )
47		fniniseg	⊢ ( 𝐹 Fn ℝ → ( 𝑧 ∈ ( ^◡ 𝐹 “ { 𝑦 } ) ↔ ( 𝑧 ∈ ℝ ∧ ( 𝐹 ‘ 𝑧 ) = 𝑦 ) ) )
48	46 47	syl	⊢ ( ( ( 𝐹 ∈ dom ∫₁ ∧ 𝐴 ∈ dom vol ) ∧ 𝑦 ∈ ( ran 𝐺 ∖ { 0 } ) ) → ( 𝑧 ∈ ( ^◡ 𝐹 “ { 𝑦 } ) ↔ ( 𝑧 ∈ ℝ ∧ ( 𝐹 ‘ 𝑧 ) = 𝑦 ) ) )
49	48	anbi2d	⊢ ( ( ( 𝐹 ∈ dom ∫₁ ∧ 𝐴 ∈ dom vol ) ∧ 𝑦 ∈ ( ran 𝐺 ∖ { 0 } ) ) → ( ( 𝑧 ∈ 𝐴 ∧ 𝑧 ∈ ( ^◡ 𝐹 “ { 𝑦 } ) ) ↔ ( 𝑧 ∈ 𝐴 ∧ ( 𝑧 ∈ ℝ ∧ ( 𝐹 ‘ 𝑧 ) = 𝑦 ) ) ) )
50	41 45 49	3bitr4d	⊢ ( ( ( 𝐹 ∈ dom ∫₁ ∧ 𝐴 ∈ dom vol ) ∧ 𝑦 ∈ ( ran 𝐺 ∖ { 0 } ) ) → ( 𝑧 ∈ ( ^◡ 𝐺 “ { 𝑦 } ) ↔ ( 𝑧 ∈ 𝐴 ∧ 𝑧 ∈ ( ^◡ 𝐹 “ { 𝑦 } ) ) ) )
51		elin	⊢ ( 𝑧 ∈ ( 𝐴 ∩ ( ^◡ 𝐹 “ { 𝑦 } ) ) ↔ ( 𝑧 ∈ 𝐴 ∧ 𝑧 ∈ ( ^◡ 𝐹 “ { 𝑦 } ) ) )
52	50 51	bitr4di	⊢ ( ( ( 𝐹 ∈ dom ∫₁ ∧ 𝐴 ∈ dom vol ) ∧ 𝑦 ∈ ( ran 𝐺 ∖ { 0 } ) ) → ( 𝑧 ∈ ( ^◡ 𝐺 “ { 𝑦 } ) ↔ 𝑧 ∈ ( 𝐴 ∩ ( ^◡ 𝐹 “ { 𝑦 } ) ) ) )
53	52	eqrdv	⊢ ( ( ( 𝐹 ∈ dom ∫₁ ∧ 𝐴 ∈ dom vol ) ∧ 𝑦 ∈ ( ran 𝐺 ∖ { 0 } ) ) → ( ^◡ 𝐺 “ { 𝑦 } ) = ( 𝐴 ∩ ( ^◡ 𝐹 “ { 𝑦 } ) ) )
54		simplr	⊢ ( ( ( 𝐹 ∈ dom ∫₁ ∧ 𝐴 ∈ dom vol ) ∧ 𝑦 ∈ ( ran 𝐺 ∖ { 0 } ) ) → 𝐴 ∈ dom vol )
55		i1fima	⊢ ( 𝐹 ∈ dom ∫₁ → ( ^◡ 𝐹 “ { 𝑦 } ) ∈ dom vol )
56	55	ad2antrr	⊢ ( ( ( 𝐹 ∈ dom ∫₁ ∧ 𝐴 ∈ dom vol ) ∧ 𝑦 ∈ ( ran 𝐺 ∖ { 0 } ) ) → ( ^◡ 𝐹 “ { 𝑦 } ) ∈ dom vol )
57		inmbl	⊢ ( ( 𝐴 ∈ dom vol ∧ ( ^◡ 𝐹 “ { 𝑦 } ) ∈ dom vol ) → ( 𝐴 ∩ ( ^◡ 𝐹 “ { 𝑦 } ) ) ∈ dom vol )
58	54 56 57	syl2anc	⊢ ( ( ( 𝐹 ∈ dom ∫₁ ∧ 𝐴 ∈ dom vol ) ∧ 𝑦 ∈ ( ran 𝐺 ∖ { 0 } ) ) → ( 𝐴 ∩ ( ^◡ 𝐹 “ { 𝑦 } ) ) ∈ dom vol )
59	53 58	eqeltrd	⊢ ( ( ( 𝐹 ∈ dom ∫₁ ∧ 𝐴 ∈ dom vol ) ∧ 𝑦 ∈ ( ran 𝐺 ∖ { 0 } ) ) → ( ^◡ 𝐺 “ { 𝑦 } ) ∈ dom vol )
60	53	fveq2d	⊢ ( ( ( 𝐹 ∈ dom ∫₁ ∧ 𝐴 ∈ dom vol ) ∧ 𝑦 ∈ ( ran 𝐺 ∖ { 0 } ) ) → ( vol ‘ ( ^◡ 𝐺 “ { 𝑦 } ) ) = ( vol ‘ ( 𝐴 ∩ ( ^◡ 𝐹 “ { 𝑦 } ) ) ) )
61		mblvol	⊢ ( ( 𝐴 ∩ ( ^◡ 𝐹 “ { 𝑦 } ) ) ∈ dom vol → ( vol ‘ ( 𝐴 ∩ ( ^◡ 𝐹 “ { 𝑦 } ) ) ) = ( vol* ‘ ( 𝐴 ∩ ( ^◡ 𝐹 “ { 𝑦 } ) ) ) )
62	58 61	syl	⊢ ( ( ( 𝐹 ∈ dom ∫₁ ∧ 𝐴 ∈ dom vol ) ∧ 𝑦 ∈ ( ran 𝐺 ∖ { 0 } ) ) → ( vol ‘ ( 𝐴 ∩ ( ^◡ 𝐹 “ { 𝑦 } ) ) ) = ( vol* ‘ ( 𝐴 ∩ ( ^◡ 𝐹 “ { 𝑦 } ) ) ) )
63	60 62	eqtrd	⊢ ( ( ( 𝐹 ∈ dom ∫₁ ∧ 𝐴 ∈ dom vol ) ∧ 𝑦 ∈ ( ran 𝐺 ∖ { 0 } ) ) → ( vol ‘ ( ^◡ 𝐺 “ { 𝑦 } ) ) = ( vol* ‘ ( 𝐴 ∩ ( ^◡ 𝐹 “ { 𝑦 } ) ) ) )
64		inss2	⊢ ( 𝐴 ∩ ( ^◡ 𝐹 “ { 𝑦 } ) ) ⊆ ( ^◡ 𝐹 “ { 𝑦 } )
65		mblss	⊢ ( ( ^◡ 𝐹 “ { 𝑦 } ) ∈ dom vol → ( ^◡ 𝐹 “ { 𝑦 } ) ⊆ ℝ )
66	56 65	syl	⊢ ( ( ( 𝐹 ∈ dom ∫₁ ∧ 𝐴 ∈ dom vol ) ∧ 𝑦 ∈ ( ran 𝐺 ∖ { 0 } ) ) → ( ^◡ 𝐹 “ { 𝑦 } ) ⊆ ℝ )
67		mblvol	⊢ ( ( ^◡ 𝐹 “ { 𝑦 } ) ∈ dom vol → ( vol ‘ ( ^◡ 𝐹 “ { 𝑦 } ) ) = ( vol* ‘ ( ^◡ 𝐹 “ { 𝑦 } ) ) )
68	56 67	syl	⊢ ( ( ( 𝐹 ∈ dom ∫₁ ∧ 𝐴 ∈ dom vol ) ∧ 𝑦 ∈ ( ran 𝐺 ∖ { 0 } ) ) → ( vol ‘ ( ^◡ 𝐹 “ { 𝑦 } ) ) = ( vol* ‘ ( ^◡ 𝐹 “ { 𝑦 } ) ) )
69		i1fima2sn	⊢ ( ( 𝐹 ∈ dom ∫₁ ∧ 𝑦 ∈ ( ran 𝐺 ∖ { 0 } ) ) → ( vol ‘ ( ^◡ 𝐹 “ { 𝑦 } ) ) ∈ ℝ )
70	69	adantlr	⊢ ( ( ( 𝐹 ∈ dom ∫₁ ∧ 𝐴 ∈ dom vol ) ∧ 𝑦 ∈ ( ran 𝐺 ∖ { 0 } ) ) → ( vol ‘ ( ^◡ 𝐹 “ { 𝑦 } ) ) ∈ ℝ )
71	68 70	eqeltrrd	⊢ ( ( ( 𝐹 ∈ dom ∫₁ ∧ 𝐴 ∈ dom vol ) ∧ 𝑦 ∈ ( ran 𝐺 ∖ { 0 } ) ) → ( vol* ‘ ( ^◡ 𝐹 “ { 𝑦 } ) ) ∈ ℝ )
72		ovolsscl	⊢ ( ( ( 𝐴 ∩ ( ^◡ 𝐹 “ { 𝑦 } ) ) ⊆ ( ^◡ 𝐹 “ { 𝑦 } ) ∧ ( ^◡ 𝐹 “ { 𝑦 } ) ⊆ ℝ ∧ ( vol* ‘ ( ^◡ 𝐹 “ { 𝑦 } ) ) ∈ ℝ ) → ( vol* ‘ ( 𝐴 ∩ ( ^◡ 𝐹 “ { 𝑦 } ) ) ) ∈ ℝ )
73	64 66 71 72	mp3an2i	⊢ ( ( ( 𝐹 ∈ dom ∫₁ ∧ 𝐴 ∈ dom vol ) ∧ 𝑦 ∈ ( ran 𝐺 ∖ { 0 } ) ) → ( vol* ‘ ( 𝐴 ∩ ( ^◡ 𝐹 “ { 𝑦 } ) ) ) ∈ ℝ )
74	63 73	eqeltrd	⊢ ( ( ( 𝐹 ∈ dom ∫₁ ∧ 𝐴 ∈ dom vol ) ∧ 𝑦 ∈ ( ran 𝐺 ∖ { 0 } ) ) → ( vol ‘ ( ^◡ 𝐺 “ { 𝑦 } ) ) ∈ ℝ )
75	12 16 59 74	i1fd	⊢ ( ( 𝐹 ∈ dom ∫₁ ∧ 𝐴 ∈ dom vol ) → 𝐺 ∈ dom ∫₁ )

Metamath Proof Explorer

Theorem i1fres

Proof