itg1climres

Description: Restricting the simple function F to the increasing sequence A ( n ) of measurable sets whose union is RR yields a sequence of simple functions whose integrals approach the integral of F . (Contributed by Mario Carneiro, 15-Aug-2014)

	Ref	Expression
Hypotheses	itg1climres.1	$⊢ φ \to A : ℕ ⟶ dom vol$
	itg1climres.2	$⊢ (φ \land n \in ℕ) \to A (n) \subseteq A (n + 1)$
	itg1climres.3	$⊢ φ \to ⋃ ran A = ℝ$
	itg1climres.4	$⊢ φ \to F \in dom \int^{1}$
	itg1climres.5	$⊢ G = (x \in ℝ ⟼ if (x \in A (n), F (x), 0))$
Assertion	itg1climres	$⊢ φ \to (n \in ℕ ⟼ \int^{1} (G)) ⇝ \int^{1} (F)$

Proof

Step	Hyp	Ref	Expression
1		itg1climres.1	$⊢ φ \to A : ℕ ⟶ dom vol$
2		itg1climres.2	$⊢ (φ \land n \in ℕ) \to A (n) \subseteq A (n + 1)$
3		itg1climres.3	$⊢ φ \to ⋃ ran A = ℝ$
4		itg1climres.4	$⊢ φ \to F \in dom \int^{1}$
5		itg1climres.5	$⊢ G = (x \in ℝ ⟼ if (x \in A (n), F (x), 0))$
6		nnuz	$⊢ ℕ = ℤ_{\geq 1}$
7		1zzd	$⊢ φ \to 1 \in ℤ$
8		i1frn	$⊢ F \in dom \int^{1} \to ran F \in Fin$
9	4 8	syl	$⊢ φ \to ran F \in Fin$
10		difss	$⊢ ran F ∖ \{0\} \subseteq ran F$
11		ssfi	$⊢ (ran F \in Fin \land ran F ∖ \{0\} \subseteq ran F) \to ran F ∖ \{0\} \in Fin$
12	9 10 11	sylancl	$⊢ φ \to ran F ∖ \{0\} \in Fin$
13		1zzd	$⊢ (φ \land k \in (ran F ∖ \{0\})) \to 1 \in ℤ$
14		i1fima	$⊢ F \in dom \int^{1} \to F^{-1} [\{k\}] \in dom vol$
15	4 14	syl	$⊢ φ \to F^{-1} [\{k\}] \in dom vol$
16	15	ad2antrr	$⊢ ((φ \land k \in (ran F ∖ \{0\})) \land n \in ℕ) \to F^{-1} [\{k\}] \in dom vol$
17	1	ffvelrnda	$⊢ (φ \land n \in ℕ) \to A (n) \in dom vol$
18	17	adantlr	$⊢ ((φ \land k \in (ran F ∖ \{0\})) \land n \in ℕ) \to A (n) \in dom vol$
19		inmbl	$⊢ (F^{-1} [\{k\}] \in dom vol \land A (n) \in dom vol) \to F^{-1} [\{k\}] \cap A (n) \in dom vol$
20	16 18 19	syl2anc	$⊢ ((φ \land k \in (ran F ∖ \{0\})) \land n \in ℕ) \to F^{-1} [\{k\}] \cap A (n) \in dom vol$
21		mblvol	$⊢ F^{-1} [\{k\}] \cap A (n) \in dom vol \to vol (F^{-1} [\{k\}] \cap A (n)) = {vol}^{*} (F^{-1} [\{k\}] \cap A (n))$
22	20 21	syl	$⊢ ((φ \land k \in (ran F ∖ \{0\})) \land n \in ℕ) \to vol (F^{-1} [\{k\}] \cap A (n)) = {vol}^{*} (F^{-1} [\{k\}] \cap A (n))$
23		inss1	$⊢ F^{-1} [\{k\}] \cap A (n) \subseteq F^{-1} [\{k\}]$
24	23	a1i	$⊢ ((φ \land k \in (ran F ∖ \{0\})) \land n \in ℕ) \to F^{-1} [\{k\}] \cap A (n) \subseteq F^{-1} [\{k\}]$
25		mblss	$⊢ F^{-1} [\{k\}] \in dom vol \to F^{-1} [\{k\}] \subseteq ℝ$
26	16 25	syl	$⊢ ((φ \land k \in (ran F ∖ \{0\})) \land n \in ℕ) \to F^{-1} [\{k\}] \subseteq ℝ$
27		mblvol	$⊢ F^{-1} [\{k\}] \in dom vol \to vol (F^{-1} [\{k\}]) = {vol}^{*} (F^{-1} [\{k\}])$
28	16 27	syl	$⊢ ((φ \land k \in (ran F ∖ \{0\})) \land n \in ℕ) \to vol (F^{-1} [\{k\}]) = {vol}^{*} (F^{-1} [\{k\}])$
29		i1fima2sn	$⊢ (F \in dom \int^{1} \land k \in (ran F ∖ \{0\})) \to vol (F^{-1} [\{k\}]) \in ℝ$
30	4 29	sylan	$⊢ (φ \land k \in (ran F ∖ \{0\})) \to vol (F^{-1} [\{k\}]) \in ℝ$
31	30	adantr	$⊢ ((φ \land k \in (ran F ∖ \{0\})) \land n \in ℕ) \to vol (F^{-1} [\{k\}]) \in ℝ$
32	28 31	eqeltrrd	$⊢ ((φ \land k \in (ran F ∖ \{0\})) \land n \in ℕ) \to {vol}^{*} (F^{-1} [\{k\}]) \in ℝ$
33		ovolsscl	$⊢ (F^{-1} [\{k\}] \cap A (n) \subseteq F^{-1} [\{k\}] \land F^{-1} [\{k\}] \subseteq ℝ \land {vol}^{} (F^{-1} [\{k\}]) \in ℝ) \to {vol}^{} (F^{-1} [\{k\}] \cap A (n)) \in ℝ$
34	24 26 32 33	syl3anc	$⊢ ((φ \land k \in (ran F ∖ \{0\})) \land n \in ℕ) \to {vol}^{*} (F^{-1} [\{k\}] \cap A (n)) \in ℝ$
35	22 34	eqeltrd	$⊢ ((φ \land k \in (ran F ∖ \{0\})) \land n \in ℕ) \to vol (F^{-1} [\{k\}] \cap A (n)) \in ℝ$
36	35	fmpttd	$⊢ (φ \land k \in (ran F ∖ \{0\})) \to (n \in ℕ ⟼ vol (F^{-1} [\{k\}] \cap A (n))) : ℕ ⟶ ℝ$
37	2	adantlr	$⊢ ((φ \land k \in (ran F ∖ \{0\})) \land n \in ℕ) \to A (n) \subseteq A (n + 1)$
38		sslin	$⊢ A (n) \subseteq A (n + 1) \to F^{-1} [\{k\}] \cap A (n) \subseteq F^{-1} [\{k\}] \cap A (n + 1)$
39	37 38	syl	$⊢ ((φ \land k \in (ran F ∖ \{0\})) \land n \in ℕ) \to F^{-1} [\{k\}] \cap A (n) \subseteq F^{-1} [\{k\}] \cap A (n + 1)$
40	1	adantr	$⊢ (φ \land k \in (ran F ∖ \{0\})) \to A : ℕ ⟶ dom vol$
41		peano2nn	$⊢ n \in ℕ \to n + 1 \in ℕ$
42		ffvelrn	$⊢ (A : ℕ ⟶ dom vol \land n + 1 \in ℕ) \to A (n + 1) \in dom vol$
43	40 41 42	syl2an	$⊢ ((φ \land k \in (ran F ∖ \{0\})) \land n \in ℕ) \to A (n + 1) \in dom vol$
44		inmbl	$⊢ (F^{-1} [\{k\}] \in dom vol \land A (n + 1) \in dom vol) \to F^{-1} [\{k\}] \cap A (n + 1) \in dom vol$
45	16 43 44	syl2anc	$⊢ ((φ \land k \in (ran F ∖ \{0\})) \land n \in ℕ) \to F^{-1} [\{k\}] \cap A (n + 1) \in dom vol$
46		mblss	$⊢ F^{-1} [\{k\}] \cap A (n + 1) \in dom vol \to F^{-1} [\{k\}] \cap A (n + 1) \subseteq ℝ$
47	45 46	syl	$⊢ ((φ \land k \in (ran F ∖ \{0\})) \land n \in ℕ) \to F^{-1} [\{k\}] \cap A (n + 1) \subseteq ℝ$
48		ovolss	$⊢ (F^{-1} [\{k\}] \cap A (n) \subseteq F^{-1} [\{k\}] \cap A (n + 1) \land F^{-1} [\{k\}] \cap A (n + 1) \subseteq ℝ) \to {vol}^{} (F^{-1} [\{k\}] \cap A (n)) \leq {vol}^{} (F^{-1} [\{k\}] \cap A (n + 1))$
49	39 47 48	syl2anc	$⊢ ((φ \land k \in (ran F ∖ \{0\})) \land n \in ℕ) \to {vol}^{} (F^{-1} [\{k\}] \cap A (n)) \leq {vol}^{} (F^{-1} [\{k\}] \cap A (n + 1))$
50		mblvol	$⊢ F^{-1} [\{k\}] \cap A (n + 1) \in dom vol \to vol (F^{-1} [\{k\}] \cap A (n + 1)) = {vol}^{*} (F^{-1} [\{k\}] \cap A (n + 1))$
51	45 50	syl	$⊢ ((φ \land k \in (ran F ∖ \{0\})) \land n \in ℕ) \to vol (F^{-1} [\{k\}] \cap A (n + 1)) = {vol}^{*} (F^{-1} [\{k\}] \cap A (n + 1))$
52	49 22 51	3brtr4d	$⊢ ((φ \land k \in (ran F ∖ \{0\})) \land n \in ℕ) \to vol (F^{-1} [\{k\}] \cap A (n)) \leq vol (F^{-1} [\{k\}] \cap A (n + 1))$
53	52	ralrimiva	$⊢ (φ \land k \in (ran F ∖ \{0\})) \to \forall n \in ℕ vol (F^{-1} [\{k\}] \cap A (n)) \leq vol (F^{-1} [\{k\}] \cap A (n + 1))$
54		fveq2	$⊢ n = j \to A (n) = A (j)$
55	54	ineq2d	$⊢ n = j \to F^{-1} [\{k\}] \cap A (n) = F^{-1} [\{k\}] \cap A (j)$
56	55	fveq2d	$⊢ n = j \to vol (F^{-1} [\{k\}] \cap A (n)) = vol (F^{-1} [\{k\}] \cap A (j))$
57		eqid	$⊢ (n \in ℕ ⟼ vol (F^{-1} [\{k\}] \cap A (n))) = (n \in ℕ ⟼ vol (F^{-1} [\{k\}] \cap A (n)))$
58		fvex	$⊢ vol (F^{-1} [\{k\}] \cap A (j)) \in V$
59	56 57 58	fvmpt	$⊢ j \in ℕ \to (n \in ℕ ⟼ vol (F^{-1} [\{k\}] \cap A (n))) (j) = vol (F^{-1} [\{k\}] \cap A (j))$
60		peano2nn	$⊢ j \in ℕ \to j + 1 \in ℕ$
61		fveq2	$⊢ n = j + 1 \to A (n) = A (j + 1)$
62	61	ineq2d	$⊢ n = j + 1 \to F^{-1} [\{k\}] \cap A (n) = F^{-1} [\{k\}] \cap A (j + 1)$
63	62	fveq2d	$⊢ n = j + 1 \to vol (F^{-1} [\{k\}] \cap A (n)) = vol (F^{-1} [\{k\}] \cap A (j + 1))$
64		fvex	$⊢ vol (F^{-1} [\{k\}] \cap A (j + 1)) \in V$
65	63 57 64	fvmpt	$⊢ j + 1 \in ℕ \to (n \in ℕ ⟼ vol (F^{-1} [\{k\}] \cap A (n))) (j + 1) = vol (F^{-1} [\{k\}] \cap A (j + 1))$
66	60 65	syl	$⊢ j \in ℕ \to (n \in ℕ ⟼ vol (F^{-1} [\{k\}] \cap A (n))) (j + 1) = vol (F^{-1} [\{k\}] \cap A (j + 1))$
67	59 66	breq12d	$⊢ j \in ℕ \to ((n \in ℕ ⟼ vol (F^{-1} [\{k\}] \cap A (n))) (j) \leq (n \in ℕ ⟼ vol (F^{-1} [\{k\}] \cap A (n))) (j + 1) \leftrightarrow vol (F^{-1} [\{k\}] \cap A (j)) \leq vol (F^{-1} [\{k\}] \cap A (j + 1)))$
68	67	ralbiia	$⊢ \forall j \in ℕ (n \in ℕ ⟼ vol (F^{-1} [\{k\}] \cap A (n))) (j) \leq (n \in ℕ ⟼ vol (F^{-1} [\{k\}] \cap A (n))) (j + 1) \leftrightarrow \forall j \in ℕ vol (F^{-1} [\{k\}] \cap A (j)) \leq vol (F^{-1} [\{k\}] \cap A (j + 1))$
69		fvoveq1	$⊢ n = j \to A (n + 1) = A (j + 1)$
70	69	ineq2d	$⊢ n = j \to F^{-1} [\{k\}] \cap A (n + 1) = F^{-1} [\{k\}] \cap A (j + 1)$
71	70	fveq2d	$⊢ n = j \to vol (F^{-1} [\{k\}] \cap A (n + 1)) = vol (F^{-1} [\{k\}] \cap A (j + 1))$
72	56 71	breq12d	$⊢ n = j \to (vol (F^{-1} [\{k\}] \cap A (n)) \leq vol (F^{-1} [\{k\}] \cap A (n + 1)) \leftrightarrow vol (F^{-1} [\{k\}] \cap A (j)) \leq vol (F^{-1} [\{k\}] \cap A (j + 1)))$
73	72	cbvralvw	$⊢ \forall n \in ℕ vol (F^{-1} [\{k\}] \cap A (n)) \leq vol (F^{-1} [\{k\}] \cap A (n + 1)) \leftrightarrow \forall j \in ℕ vol (F^{-1} [\{k\}] \cap A (j)) \leq vol (F^{-1} [\{k\}] \cap A (j + 1))$
74	68 73	bitr4i	$⊢ \forall j \in ℕ (n \in ℕ ⟼ vol (F^{-1} [\{k\}] \cap A (n))) (j) \leq (n \in ℕ ⟼ vol (F^{-1} [\{k\}] \cap A (n))) (j + 1) \leftrightarrow \forall n \in ℕ vol (F^{-1} [\{k\}] \cap A (n)) \leq vol (F^{-1} [\{k\}] \cap A (n + 1))$
75	53 74	sylibr	$⊢ (φ \land k \in (ran F ∖ \{0\})) \to \forall j \in ℕ (n \in ℕ ⟼ vol (F^{-1} [\{k\}] \cap A (n))) (j) \leq (n \in ℕ ⟼ vol (F^{-1} [\{k\}] \cap A (n))) (j + 1)$
76	75	r19.21bi	$⊢ ((φ \land k \in (ran F ∖ \{0\})) \land j \in ℕ) \to (n \in ℕ ⟼ vol (F^{-1} [\{k\}] \cap A (n))) (j) \leq (n \in ℕ ⟼ vol (F^{-1} [\{k\}] \cap A (n))) (j + 1)$
77		ovolss	$⊢ (F^{-1} [\{k\}] \cap A (n) \subseteq F^{-1} [\{k\}] \land F^{-1} [\{k\}] \subseteq ℝ) \to {vol}^{} (F^{-1} [\{k\}] \cap A (n)) \leq {vol}^{} (F^{-1} [\{k\}])$
78	23 26 77	sylancr	$⊢ ((φ \land k \in (ran F ∖ \{0\})) \land n \in ℕ) \to {vol}^{} (F^{-1} [\{k\}] \cap A (n)) \leq {vol}^{} (F^{-1} [\{k\}])$
79	78 22 28	3brtr4d	$⊢ ((φ \land k \in (ran F ∖ \{0\})) \land n \in ℕ) \to vol (F^{-1} [\{k\}] \cap A (n)) \leq vol (F^{-1} [\{k\}])$
80	79	ralrimiva	$⊢ (φ \land k \in (ran F ∖ \{0\})) \to \forall n \in ℕ vol (F^{-1} [\{k\}] \cap A (n)) \leq vol (F^{-1} [\{k\}])$
81	59	breq1d	$⊢ j \in ℕ \to ((n \in ℕ ⟼ vol (F^{-1} [\{k\}] \cap A (n))) (j) \leq vol (F^{-1} [\{k\}]) \leftrightarrow vol (F^{-1} [\{k\}] \cap A (j)) \leq vol (F^{-1} [\{k\}]))$
82	81	ralbiia	$⊢ \forall j \in ℕ (n \in ℕ ⟼ vol (F^{-1} [\{k\}] \cap A (n))) (j) \leq vol (F^{-1} [\{k\}]) \leftrightarrow \forall j \in ℕ vol (F^{-1} [\{k\}] \cap A (j)) \leq vol (F^{-1} [\{k\}])$
83	56	breq1d	$⊢ n = j \to (vol (F^{-1} [\{k\}] \cap A (n)) \leq vol (F^{-1} [\{k\}]) \leftrightarrow vol (F^{-1} [\{k\}] \cap A (j)) \leq vol (F^{-1} [\{k\}]))$
84	83	cbvralvw	$⊢ \forall n \in ℕ vol (F^{-1} [\{k\}] \cap A (n)) \leq vol (F^{-1} [\{k\}]) \leftrightarrow \forall j \in ℕ vol (F^{-1} [\{k\}] \cap A (j)) \leq vol (F^{-1} [\{k\}])$
85	82 84	bitr4i	$⊢ \forall j \in ℕ (n \in ℕ ⟼ vol (F^{-1} [\{k\}] \cap A (n))) (j) \leq vol (F^{-1} [\{k\}]) \leftrightarrow \forall n \in ℕ vol (F^{-1} [\{k\}] \cap A (n)) \leq vol (F^{-1} [\{k\}])$
86	80 85	sylibr	$⊢ (φ \land k \in (ran F ∖ \{0\})) \to \forall j \in ℕ (n \in ℕ ⟼ vol (F^{-1} [\{k\}] \cap A (n))) (j) \leq vol (F^{-1} [\{k\}])$
87		brralrspcev	$⊢ (vol (F^{-1} [\{k\}]) \in ℝ \land \forall j \in ℕ (n \in ℕ ⟼ vol (F^{-1} [\{k\}] \cap A (n))) (j) \leq vol (F^{-1} [\{k\}])) \to \exists x \in ℝ \forall j \in ℕ (n \in ℕ ⟼ vol (F^{-1} [\{k\}] \cap A (n))) (j) \leq x$
88	30 86 87	syl2anc	$⊢ (φ \land k \in (ran F ∖ \{0\})) \to \exists x \in ℝ \forall j \in ℕ (n \in ℕ ⟼ vol (F^{-1} [\{k\}] \cap A (n))) (j) \leq x$
89	6 13 36 76 88	climsup	$⊢ (φ \land k \in (ran F ∖ \{0\})) \to (n \in ℕ ⟼ vol (F^{-1} [\{k\}] \cap A (n))) ⇝ sup (ran (n \in ℕ ⟼ vol (F^{-1} [\{k\}] \cap A (n))) ℝ <)$
90	20	fmpttd	$⊢ (φ \land k \in (ran F ∖ \{0\})) \to (n \in ℕ ⟼ F^{-1} [\{k\}] \cap A (n)) : ℕ ⟶ dom vol$
91	39	ralrimiva	$⊢ (φ \land k \in (ran F ∖ \{0\})) \to \forall n \in ℕ F^{-1} [\{k\}] \cap A (n) \subseteq F^{-1} [\{k\}] \cap A (n + 1)$
92		eqid	$⊢ (n \in ℕ ⟼ F^{-1} [\{k\}] \cap A (n)) = (n \in ℕ ⟼ F^{-1} [\{k\}] \cap A (n))$
93		fvex	$⊢ A (j) \in V$
94	93	inex2	$⊢ F^{-1} [\{k\}] \cap A (j) \in V$
95	55 92 94	fvmpt	$⊢ j \in ℕ \to (n \in ℕ ⟼ F^{-1} [\{k\}] \cap A (n)) (j) = F^{-1} [\{k\}] \cap A (j)$
96		fvex	$⊢ A (j + 1) \in V$
97	96	inex2	$⊢ F^{-1} [\{k\}] \cap A (j + 1) \in V$
98	62 92 97	fvmpt	$⊢ j + 1 \in ℕ \to (n \in ℕ ⟼ F^{-1} [\{k\}] \cap A (n)) (j + 1) = F^{-1} [\{k\}] \cap A (j + 1)$
99	60 98	syl	$⊢ j \in ℕ \to (n \in ℕ ⟼ F^{-1} [\{k\}] \cap A (n)) (j + 1) = F^{-1} [\{k\}] \cap A (j + 1)$
100	95 99	sseq12d	$⊢ j \in ℕ \to ((n \in ℕ ⟼ F^{-1} [\{k\}] \cap A (n)) (j) \subseteq (n \in ℕ ⟼ F^{-1} [\{k\}] \cap A (n)) (j + 1) \leftrightarrow F^{-1} [\{k\}] \cap A (j) \subseteq F^{-1} [\{k\}] \cap A (j + 1))$
101	100	ralbiia	$⊢ \forall j \in ℕ (n \in ℕ ⟼ F^{-1} [\{k\}] \cap A (n)) (j) \subseteq (n \in ℕ ⟼ F^{-1} [\{k\}] \cap A (n)) (j + 1) \leftrightarrow \forall j \in ℕ F^{-1} [\{k\}] \cap A (j) \subseteq F^{-1} [\{k\}] \cap A (j + 1)$
102	55 70	sseq12d	$⊢ n = j \to (F^{-1} [\{k\}] \cap A (n) \subseteq F^{-1} [\{k\}] \cap A (n + 1) \leftrightarrow F^{-1} [\{k\}] \cap A (j) \subseteq F^{-1} [\{k\}] \cap A (j + 1))$
103	102	cbvralvw	$⊢ \forall n \in ℕ F^{-1} [\{k\}] \cap A (n) \subseteq F^{-1} [\{k\}] \cap A (n + 1) \leftrightarrow \forall j \in ℕ F^{-1} [\{k\}] \cap A (j) \subseteq F^{-1} [\{k\}] \cap A (j + 1)$
104	101 103	bitr4i	$⊢ \forall j \in ℕ (n \in ℕ ⟼ F^{-1} [\{k\}] \cap A (n)) (j) \subseteq (n \in ℕ ⟼ F^{-1} [\{k\}] \cap A (n)) (j + 1) \leftrightarrow \forall n \in ℕ F^{-1} [\{k\}] \cap A (n) \subseteq F^{-1} [\{k\}] \cap A (n + 1)$
105	91 104	sylibr	$⊢ (φ \land k \in (ran F ∖ \{0\})) \to \forall j \in ℕ (n \in ℕ ⟼ F^{-1} [\{k\}] \cap A (n)) (j) \subseteq (n \in ℕ ⟼ F^{-1} [\{k\}] \cap A (n)) (j + 1)$
106		volsup	$⊢ ((n \in ℕ ⟼ F^{-1} [\{k\}] \cap A (n)) : ℕ ⟶ dom vol \land \forall j \in ℕ (n \in ℕ ⟼ F^{-1} [\{k\}] \cap A (n)) (j) \subseteq (n \in ℕ ⟼ F^{-1} [\{k\}] \cap A (n)) (j + 1)) \to vol (⋃ ran (n \in ℕ ⟼ F^{-1} [\{k\}] \cap A (n))) = sup (vol [ran (n \in ℕ ⟼ F^{-1} [\{k\}] \cap A (n))] ℝ^{*} <)$
107	90 105 106	syl2anc	$⊢ (φ \land k \in (ran F ∖ \{0\})) \to vol (⋃ ran (n \in ℕ ⟼ F^{-1} [\{k\}] \cap A (n))) = sup (vol [ran (n \in ℕ ⟼ F^{-1} [\{k\}] \cap A (n))] ℝ^{*} <)$
108	95	iuneq2i	$⊢ ⋃_{j \in ℕ} (n \in ℕ ⟼ F^{-1} [\{k\}] \cap A (n)) (j) = ⋃_{j \in ℕ} (F^{-1} [\{k\}] \cap A (j))$
109	55	cbviunv	$⊢ ⋃_{n \in ℕ} (F^{-1} [\{k\}] \cap A (n)) = ⋃_{j \in ℕ} (F^{-1} [\{k\}] \cap A (j))$
110		iunin2	$⊢ ⋃_{n \in ℕ} (F^{-1} [\{k\}] \cap A (n)) = F^{-1} [\{k\}] \cap ⋃_{n \in ℕ} A (n)$
111	108 109 110	3eqtr2i	$⊢ ⋃_{j \in ℕ} (n \in ℕ ⟼ F^{-1} [\{k\}] \cap A (n)) (j) = F^{-1} [\{k\}] \cap ⋃_{n \in ℕ} A (n)$
112		ffn	$⊢ A : ℕ ⟶ dom vol \to A Fn ℕ$
113		fniunfv	$⊢ A Fn ℕ \to ⋃_{n \in ℕ} A (n) = ⋃ ran A$
114	1 112 113	3syl	$⊢ φ \to ⋃_{n \in ℕ} A (n) = ⋃ ran A$
115	114 3	eqtrd	$⊢ φ \to ⋃_{n \in ℕ} A (n) = ℝ$
116	115	adantr	$⊢ (φ \land k \in (ran F ∖ \{0\})) \to ⋃_{n \in ℕ} A (n) = ℝ$
117	116	ineq2d	$⊢ (φ \land k \in (ran F ∖ \{0\})) \to F^{-1} [\{k\}] \cap ⋃_{n \in ℕ} A (n) = F^{-1} [\{k\}] \cap ℝ$
118	15	adantr	$⊢ (φ \land k \in (ran F ∖ \{0\})) \to F^{-1} [\{k\}] \in dom vol$
119	118 25	syl	$⊢ (φ \land k \in (ran F ∖ \{0\})) \to F^{-1} [\{k\}] \subseteq ℝ$
120		df-ss	$⊢ F^{-1} [\{k\}] \subseteq ℝ \leftrightarrow F^{-1} [\{k\}] \cap ℝ = F^{-1} [\{k\}]$
121	119 120	sylib	$⊢ (φ \land k \in (ran F ∖ \{0\})) \to F^{-1} [\{k\}] \cap ℝ = F^{-1} [\{k\}]$
122	117 121	eqtrd	$⊢ (φ \land k \in (ran F ∖ \{0\})) \to F^{-1} [\{k\}] \cap ⋃_{n \in ℕ} A (n) = F^{-1} [\{k\}]$
123	111 122	eqtrid	$⊢ (φ \land k \in (ran F ∖ \{0\})) \to ⋃_{j \in ℕ} (n \in ℕ ⟼ F^{-1} [\{k\}] \cap A (n)) (j) = F^{-1} [\{k\}]$
124		ffn	$⊢ (n \in ℕ ⟼ F^{-1} [\{k\}] \cap A (n)) : ℕ ⟶ dom vol \to (n \in ℕ ⟼ F^{-1} [\{k\}] \cap A (n)) Fn ℕ$
125		fniunfv	$⊢ (n \in ℕ ⟼ F^{-1} [\{k\}] \cap A (n)) Fn ℕ \to ⋃_{j \in ℕ} (n \in ℕ ⟼ F^{-1} [\{k\}] \cap A (n)) (j) = ⋃ ran (n \in ℕ ⟼ F^{-1} [\{k\}] \cap A (n))$
126	90 124 125	3syl	$⊢ (φ \land k \in (ran F ∖ \{0\})) \to ⋃_{j \in ℕ} (n \in ℕ ⟼ F^{-1} [\{k\}] \cap A (n)) (j) = ⋃ ran (n \in ℕ ⟼ F^{-1} [\{k\}] \cap A (n))$
127	123 126	eqtr3d	$⊢ (φ \land k \in (ran F ∖ \{0\})) \to F^{-1} [\{k\}] = ⋃ ran (n \in ℕ ⟼ F^{-1} [\{k\}] \cap A (n))$
128	127	fveq2d	$⊢ (φ \land k \in (ran F ∖ \{0\})) \to vol (F^{-1} [\{k\}]) = vol (⋃ ran (n \in ℕ ⟼ F^{-1} [\{k\}] \cap A (n)))$
129	36	frnd	$⊢ (φ \land k \in (ran F ∖ \{0\})) \to ran (n \in ℕ ⟼ vol (F^{-1} [\{k\}] \cap A (n))) \subseteq ℝ$
130	36	fdmd	$⊢ (φ \land k \in (ran F ∖ \{0\})) \to dom (n \in ℕ ⟼ vol (F^{-1} [\{k\}] \cap A (n))) = ℕ$
131		1nn	$⊢ 1 \in ℕ$
132		ne0i	$⊢ 1 \in ℕ \to ℕ \neq \emptyset$
133	131 132	mp1i	$⊢ (φ \land k \in (ran F ∖ \{0\})) \to ℕ \neq \emptyset$
134	130 133	eqnetrd	$⊢ (φ \land k \in (ran F ∖ \{0\})) \to dom (n \in ℕ ⟼ vol (F^{-1} [\{k\}] \cap A (n))) \neq \emptyset$
135		dm0rn0	$⊢ dom (n \in ℕ ⟼ vol (F^{-1} [\{k\}] \cap A (n))) = \emptyset \leftrightarrow ran (n \in ℕ ⟼ vol (F^{-1} [\{k\}] \cap A (n))) = \emptyset$
136	135	necon3bii	$⊢ dom (n \in ℕ ⟼ vol (F^{-1} [\{k\}] \cap A (n))) \neq \emptyset \leftrightarrow ran (n \in ℕ ⟼ vol (F^{-1} [\{k\}] \cap A (n))) \neq \emptyset$
137	134 136	sylib	$⊢ (φ \land k \in (ran F ∖ \{0\})) \to ran (n \in ℕ ⟼ vol (F^{-1} [\{k\}] \cap A (n))) \neq \emptyset$
138		ffn	$⊢ (n \in ℕ ⟼ vol (F^{-1} [\{k\}] \cap A (n))) : ℕ ⟶ ℝ \to (n \in ℕ ⟼ vol (F^{-1} [\{k\}] \cap A (n))) Fn ℕ$
139		breq1	$⊢ z = (n \in ℕ ⟼ vol (F^{-1} [\{k\}] \cap A (n))) (j) \to (z \leq x \leftrightarrow (n \in ℕ ⟼ vol (F^{-1} [\{k\}] \cap A (n))) (j) \leq x)$
140	139	ralrn	$⊢ (n \in ℕ ⟼ vol (F^{-1} [\{k\}] \cap A (n))) Fn ℕ \to (\forall z \in ran (n \in ℕ ⟼ vol (F^{-1} [\{k\}] \cap A (n))) z \leq x \leftrightarrow \forall j \in ℕ (n \in ℕ ⟼ vol (F^{-1} [\{k\}] \cap A (n))) (j) \leq x)$
141	36 138 140	3syl	$⊢ (φ \land k \in (ran F ∖ \{0\})) \to (\forall z \in ran (n \in ℕ ⟼ vol (F^{-1} [\{k\}] \cap A (n))) z \leq x \leftrightarrow \forall j \in ℕ (n \in ℕ ⟼ vol (F^{-1} [\{k\}] \cap A (n))) (j) \leq x)$
142	141	rexbidv	$⊢ (φ \land k \in (ran F ∖ \{0\})) \to (\exists x \in ℝ \forall z \in ran (n \in ℕ ⟼ vol (F^{-1} [\{k\}] \cap A (n))) z \leq x \leftrightarrow \exists x \in ℝ \forall j \in ℕ (n \in ℕ ⟼ vol (F^{-1} [\{k\}] \cap A (n))) (j) \leq x)$
143	88 142	mpbird	$⊢ (φ \land k \in (ran F ∖ \{0\})) \to \exists x \in ℝ \forall z \in ran (n \in ℕ ⟼ vol (F^{-1} [\{k\}] \cap A (n))) z \leq x$
144		supxrre	$⊢ (ran (n \in ℕ ⟼ vol (F^{-1} [\{k\}] \cap A (n))) \subseteq ℝ \land ran (n \in ℕ ⟼ vol (F^{-1} [\{k\}] \cap A (n))) \neq \emptyset \land \exists x \in ℝ \forall z \in ran (n \in ℕ ⟼ vol (F^{-1} [\{k\}] \cap A (n))) z \leq x) \to sup (ran (n \in ℕ ⟼ vol (F^{-1} [\{k\}] \cap A (n))) ℝ^{*} <) = sup (ran (n \in ℕ ⟼ vol (F^{-1} [\{k\}] \cap A (n))) ℝ <)$
145	129 137 143 144	syl3anc	$⊢ (φ \land k \in (ran F ∖ \{0\})) \to sup (ran (n \in ℕ ⟼ vol (F^{-1} [\{k\}] \cap A (n))) ℝ^{*} <) = sup (ran (n \in ℕ ⟼ vol (F^{-1} [\{k\}] \cap A (n))) ℝ <)$
146		volf	$⊢ vol : dom vol ⟶ [0, +∞]$
147	146	a1i	$⊢ (φ \land k \in (ran F ∖ \{0\})) \to vol : dom vol ⟶ [0, +∞]$
148	147 20	cofmpt	$⊢ (φ \land k \in (ran F ∖ \{0\})) \to vol \circ (n \in ℕ ⟼ F^{-1} [\{k\}] \cap A (n)) = (n \in ℕ ⟼ vol (F^{-1} [\{k\}] \cap A (n)))$
149	148	rneqd	$⊢ (φ \land k \in (ran F ∖ \{0\})) \to ran (vol \circ (n \in ℕ ⟼ F^{-1} [\{k\}] \cap A (n))) = ran (n \in ℕ ⟼ vol (F^{-1} [\{k\}] \cap A (n)))$
150		rnco2	$⊢ ran (vol \circ (n \in ℕ ⟼ F^{-1} [\{k\}] \cap A (n))) = vol [ran (n \in ℕ ⟼ F^{-1} [\{k\}] \cap A (n))]$
151	149 150	eqtr3di	$⊢ (φ \land k \in (ran F ∖ \{0\})) \to ran (n \in ℕ ⟼ vol (F^{-1} [\{k\}] \cap A (n))) = vol [ran (n \in ℕ ⟼ F^{-1} [\{k\}] \cap A (n))]$
152	151	supeq1d	$⊢ (φ \land k \in (ran F ∖ \{0\})) \to sup (ran (n \in ℕ ⟼ vol (F^{-1} [\{k\}] \cap A (n))) ℝ^{} <) = sup (vol [ran (n \in ℕ ⟼ F^{-1} [\{k\}] \cap A (n))] ℝ^{} <)$
153	145 152	eqtr3d	$⊢ (φ \land k \in (ran F ∖ \{0\})) \to sup (ran (n \in ℕ ⟼ vol (F^{-1} [\{k\}] \cap A (n))) ℝ <) = sup (vol [ran (n \in ℕ ⟼ F^{-1} [\{k\}] \cap A (n))] ℝ^{*} <)$
154	107 128 153	3eqtr4d	$⊢ (φ \land k \in (ran F ∖ \{0\})) \to vol (F^{-1} [\{k\}]) = sup (ran (n \in ℕ ⟼ vol (F^{-1} [\{k\}] \cap A (n))) ℝ <)$
155	89 154	breqtrrd	$⊢ (φ \land k \in (ran F ∖ \{0\})) \to (n \in ℕ ⟼ vol (F^{-1} [\{k\}] \cap A (n))) ⇝ vol (F^{-1} [\{k\}])$
156		i1ff	$⊢ F \in dom \int^{1} \to F : ℝ ⟶ ℝ$
157		frn	$⊢ F : ℝ ⟶ ℝ \to ran F \subseteq ℝ$
158	4 156 157	3syl	$⊢ φ \to ran F \subseteq ℝ$
159	158	ssdifssd	$⊢ φ \to ran F ∖ \{0\} \subseteq ℝ$
160	159	sselda	$⊢ (φ \land k \in (ran F ∖ \{0\})) \to k \in ℝ$
161	160	recnd	$⊢ (φ \land k \in (ran F ∖ \{0\})) \to k \in ℂ$
162		nnex	$⊢ ℕ \in V$
163	162	mptex	$⊢ (n \in ℕ ⟼ k vol (F^{-1} [\{k\}] \cap A (n))) \in V$
164	163	a1i	$⊢ (φ \land k \in (ran F ∖ \{0\})) \to (n \in ℕ ⟼ k vol (F^{-1} [\{k\}] \cap A (n))) \in V$
165	36	ffvelrnda	$⊢ ((φ \land k \in (ran F ∖ \{0\})) \land j \in ℕ) \to (n \in ℕ ⟼ vol (F^{-1} [\{k\}] \cap A (n))) (j) \in ℝ$
166	165	recnd	$⊢ ((φ \land k \in (ran F ∖ \{0\})) \land j \in ℕ) \to (n \in ℕ ⟼ vol (F^{-1} [\{k\}] \cap A (n))) (j) \in ℂ$
167	56	oveq2d	$⊢ n = j \to k vol (F^{-1} [\{k\}] \cap A (n)) = k vol (F^{-1} [\{k\}] \cap A (j))$
168		eqid	$⊢ (n \in ℕ ⟼ k vol (F^{-1} [\{k\}] \cap A (n))) = (n \in ℕ ⟼ k vol (F^{-1} [\{k\}] \cap A (n)))$
169		ovex	$⊢ k vol (F^{-1} [\{k\}] \cap A (j)) \in V$
170	167 168 169	fvmpt	$⊢ j \in ℕ \to (n \in ℕ ⟼ k vol (F^{-1} [\{k\}] \cap A (n))) (j) = k vol (F^{-1} [\{k\}] \cap A (j))$
171	59	oveq2d	$⊢ j \in ℕ \to k (n \in ℕ ⟼ vol (F^{-1} [\{k\}] \cap A (n))) (j) = k vol (F^{-1} [\{k\}] \cap A (j))$
172	170 171	eqtr4d	$⊢ j \in ℕ \to (n \in ℕ ⟼ k vol (F^{-1} [\{k\}] \cap A (n))) (j) = k (n \in ℕ ⟼ vol (F^{-1} [\{k\}] \cap A (n))) (j)$
173	172	adantl	$⊢ ((φ \land k \in (ran F ∖ \{0\})) \land j \in ℕ) \to (n \in ℕ ⟼ k vol (F^{-1} [\{k\}] \cap A (n))) (j) = k (n \in ℕ ⟼ vol (F^{-1} [\{k\}] \cap A (n))) (j)$
174	6 13 155 161 164 166 173	climmulc2	$⊢ (φ \land k \in (ran F ∖ \{0\})) \to (n \in ℕ ⟼ k vol (F^{-1} [\{k\}] \cap A (n))) ⇝ k vol (F^{-1} [\{k\}])$
175	162	mptex	$⊢ (n \in ℕ ⟼ \int^{1} (G)) \in V$
176	175	a1i	$⊢ φ \to (n \in ℕ ⟼ \int^{1} (G)) \in V$
177	160	adantr	$⊢ ((φ \land k \in (ran F ∖ \{0\})) \land n \in ℕ) \to k \in ℝ$
178	177 35	remulcld	$⊢ ((φ \land k \in (ran F ∖ \{0\})) \land n \in ℕ) \to k vol (F^{-1} [\{k\}] \cap A (n)) \in ℝ$
179	178	fmpttd	$⊢ (φ \land k \in (ran F ∖ \{0\})) \to (n \in ℕ ⟼ k vol (F^{-1} [\{k\}] \cap A (n))) : ℕ ⟶ ℝ$
180	179	ffvelrnda	$⊢ ((φ \land k \in (ran F ∖ \{0\})) \land j \in ℕ) \to (n \in ℕ ⟼ k vol (F^{-1} [\{k\}] \cap A (n))) (j) \in ℝ$
181	180	recnd	$⊢ ((φ \land k \in (ran F ∖ \{0\})) \land j \in ℕ) \to (n \in ℕ ⟼ k vol (F^{-1} [\{k\}] \cap A (n))) (j) \in ℂ$
182	181	anasss	$⊢ (φ \land (k \in (ran F ∖ \{0\}) \land j \in ℕ)) \to (n \in ℕ ⟼ k vol (F^{-1} [\{k\}] \cap A (n))) (j) \in ℂ$
183	4	adantr	$⊢ (φ \land n \in ℕ) \to F \in dom \int^{1}$
184	5	i1fres	$⊢ (F \in dom \int^{1} \land A (n) \in dom vol) \to G \in dom \int^{1}$
185	183 17 184	syl2anc	$⊢ (φ \land n \in ℕ) \to G \in dom \int^{1}$
186	12	adantr	$⊢ (φ \land n \in ℕ) \to ran F ∖ \{0\} \in Fin$
187		ffn	$⊢ F : ℝ ⟶ ℝ \to F Fn ℝ$
188	4 156 187	3syl	$⊢ φ \to F Fn ℝ$
189	188	adantr	$⊢ (φ \land n \in ℕ) \to F Fn ℝ$
190		fnfvelrn	$⊢ (F Fn ℝ \land x \in ℝ) \to F (x) \in ran F$
191	189 190	sylan	$⊢ ((φ \land n \in ℕ) \land x \in ℝ) \to F (x) \in ran F$
192		i1f0rn	$⊢ F \in dom \int^{1} \to 0 \in ran F$
193	4 192	syl	$⊢ φ \to 0 \in ran F$
194	193	ad2antrr	$⊢ ((φ \land n \in ℕ) \land x \in ℝ) \to 0 \in ran F$
195	191 194	ifcld	$⊢ ((φ \land n \in ℕ) \land x \in ℝ) \to if (x \in A (n), F (x), 0) \in ran F$
196	195 5	fmptd	$⊢ (φ \land n \in ℕ) \to G : ℝ ⟶ ran F$
197		frn	$⊢ G : ℝ ⟶ ran F \to ran G \subseteq ran F$
198		ssdif	$⊢ ran G \subseteq ran F \to ran G ∖ \{0\} \subseteq ran F ∖ \{0\}$
199	196 197 198	3syl	$⊢ (φ \land n \in ℕ) \to ran G ∖ \{0\} \subseteq ran F ∖ \{0\}$
200	158	adantr	$⊢ (φ \land n \in ℕ) \to ran F \subseteq ℝ$
201	200	ssdifd	$⊢ (φ \land n \in ℕ) \to ran F ∖ \{0\} \subseteq ℝ ∖ \{0\}$
202		itg1val2	$⊢ (G \in dom \int^{1} \land (ran F ∖ \{0\} \in Fin \land ran G ∖ \{0\} \subseteq ran F ∖ \{0\} \land ran F ∖ \{0\} \subseteq ℝ ∖ \{0\})) \to \int^{1} (G) = \sum_{k \in ran F ∖ \{0\}} k vol (G^{-1} [\{k\}])$
203	185 186 199 201 202	syl13anc	$⊢ (φ \land n \in ℕ) \to \int^{1} (G) = \sum_{k \in ran F ∖ \{0\}} k vol (G^{-1} [\{k\}])$
204		fvex	$⊢ F (x) \in V$
205		c0ex	$⊢ 0 \in V$
206	204 205	ifex	$⊢ if (x \in A (n), F (x), 0) \in V$
207	5	fvmpt2	$⊢ (x \in ℝ \land if (x \in A (n), F (x), 0) \in V) \to G (x) = if (x \in A (n), F (x), 0)$
208	206 207	mpan2	$⊢ x \in ℝ \to G (x) = if (x \in A (n), F (x), 0)$
209	208	adantl	$⊢ (((φ \land n \in ℕ) \land k \in (ran F ∖ \{0\})) \land x \in ℝ) \to G (x) = if (x \in A (n), F (x), 0)$
210	209	eqeq1d	$⊢ (((φ \land n \in ℕ) \land k \in (ran F ∖ \{0\})) \land x \in ℝ) \to (G (x) = k \leftrightarrow if (x \in A (n), F (x), 0) = k)$
211		eldifsni	$⊢ k \in (ran F ∖ \{0\}) \to k \neq 0$
212	211	ad2antlr	$⊢ (((φ \land n \in ℕ) \land k \in (ran F ∖ \{0\})) \land x \in ℝ) \to k \neq 0$
213		neeq1	$⊢ if (x \in A (n), F (x), 0) = k \to (if (x \in A (n), F (x), 0) \neq 0 \leftrightarrow k \neq 0)$
214	212 213	syl5ibrcom	$⊢ (((φ \land n \in ℕ) \land k \in (ran F ∖ \{0\})) \land x \in ℝ) \to (if (x \in A (n), F (x), 0) = k \to if (x \in A (n), F (x), 0) \neq 0)$
215		iffalse	$⊢ \neg x \in A (n) \to if (x \in A (n), F (x), 0) = 0$
216	215	necon1ai	$⊢ if (x \in A (n), F (x), 0) \neq 0 \to x \in A (n)$
217	214 216	syl6	$⊢ (((φ \land n \in ℕ) \land k \in (ran F ∖ \{0\})) \land x \in ℝ) \to (if (x \in A (n), F (x), 0) = k \to x \in A (n))$
218	217	pm4.71rd	$⊢ (((φ \land n \in ℕ) \land k \in (ran F ∖ \{0\})) \land x \in ℝ) \to (if (x \in A (n), F (x), 0) = k \leftrightarrow (x \in A (n) \land if (x \in A (n), F (x), 0) = k))$
219	210 218	bitrd	$⊢ (((φ \land n \in ℕ) \land k \in (ran F ∖ \{0\})) \land x \in ℝ) \to (G (x) = k \leftrightarrow (x \in A (n) \land if (x \in A (n), F (x), 0) = k))$
220		iftrue	$⊢ x \in A (n) \to if (x \in A (n), F (x), 0) = F (x)$
221	220	eqeq1d	$⊢ x \in A (n) \to (if (x \in A (n), F (x), 0) = k \leftrightarrow F (x) = k)$
222	221	pm5.32i	$⊢ (x \in A (n) \land if (x \in A (n), F (x), 0) = k) \leftrightarrow (x \in A (n) \land F (x) = k)$
223	222	biancomi	$⊢ (x \in A (n) \land if (x \in A (n), F (x), 0) = k) \leftrightarrow (F (x) = k \land x \in A (n))$
224	219 223	bitrdi	$⊢ (((φ \land n \in ℕ) \land k \in (ran F ∖ \{0\})) \land x \in ℝ) \to (G (x) = k \leftrightarrow (F (x) = k \land x \in A (n)))$
225	224	pm5.32da	$⊢ ((φ \land n \in ℕ) \land k \in (ran F ∖ \{0\})) \to ((x \in ℝ \land G (x) = k) \leftrightarrow (x \in ℝ \land (F (x) = k \land x \in A (n))))$
226		anass	$⊢ ((x \in ℝ \land F (x) = k) \land x \in A (n)) \leftrightarrow (x \in ℝ \land (F (x) = k \land x \in A (n)))$
227	225 226	bitr4di	$⊢ ((φ \land n \in ℕ) \land k \in (ran F ∖ \{0\})) \to ((x \in ℝ \land G (x) = k) \leftrightarrow ((x \in ℝ \land F (x) = k) \land x \in A (n)))$
228		i1ff	$⊢ G \in dom \int^{1} \to G : ℝ ⟶ ℝ$
229		ffn	$⊢ G : ℝ ⟶ ℝ \to G Fn ℝ$
230	185 228 229	3syl	$⊢ (φ \land n \in ℕ) \to G Fn ℝ$
231	230	adantr	$⊢ ((φ \land n \in ℕ) \land k \in (ran F ∖ \{0\})) \to G Fn ℝ$
232		fniniseg	$⊢ G Fn ℝ \to (x \in G^{-1} [\{k\}] \leftrightarrow (x \in ℝ \land G (x) = k))$
233	231 232	syl	$⊢ ((φ \land n \in ℕ) \land k \in (ran F ∖ \{0\})) \to (x \in G^{-1} [\{k\}] \leftrightarrow (x \in ℝ \land G (x) = k))$
234		elin	$⊢ x \in (F^{-1} [\{k\}] \cap A (n)) \leftrightarrow (x \in F^{-1} [\{k\}] \land x \in A (n))$
235	189	adantr	$⊢ ((φ \land n \in ℕ) \land k \in (ran F ∖ \{0\})) \to F Fn ℝ$
236		fniniseg	$⊢ F Fn ℝ \to (x \in F^{-1} [\{k\}] \leftrightarrow (x \in ℝ \land F (x) = k))$
237	235 236	syl	$⊢ ((φ \land n \in ℕ) \land k \in (ran F ∖ \{0\})) \to (x \in F^{-1} [\{k\}] \leftrightarrow (x \in ℝ \land F (x) = k))$
238	237	anbi1d	$⊢ ((φ \land n \in ℕ) \land k \in (ran F ∖ \{0\})) \to ((x \in F^{-1} [\{k\}] \land x \in A (n)) \leftrightarrow ((x \in ℝ \land F (x) = k) \land x \in A (n)))$
239	234 238	syl5bb	$⊢ ((φ \land n \in ℕ) \land k \in (ran F ∖ \{0\})) \to (x \in (F^{-1} [\{k\}] \cap A (n)) \leftrightarrow ((x \in ℝ \land F (x) = k) \land x \in A (n)))$
240	227 233 239	3bitr4d	$⊢ ((φ \land n \in ℕ) \land k \in (ran F ∖ \{0\})) \to (x \in G^{-1} [\{k\}] \leftrightarrow x \in (F^{-1} [\{k\}] \cap A (n)))$
241	240	alrimiv	$⊢ ((φ \land n \in ℕ) \land k \in (ran F ∖ \{0\})) \to \forall x (x \in G^{-1} [\{k\}] \leftrightarrow x \in (F^{-1} [\{k\}] \cap A (n)))$
242		nfmpt1	$⊢ \underline{Ⅎ} x (x \in ℝ ⟼ if (x \in A (n), F (x), 0))$
243	5 242	nfcxfr	$⊢ \underline{Ⅎ} x G$
244	243	nfcnv	$⊢ \underline{Ⅎ} x G^{-1}$
245		nfcv	$⊢ \underline{Ⅎ} x \{k\}$
246	244 245	nfima	$⊢ \underline{Ⅎ} x G^{-1} [\{k\}]$
247		nfcv	$⊢ \underline{Ⅎ} x (F^{-1} [\{k\}] \cap A (n))$
248	246 247	cleqf	$⊢ G^{-1} [\{k\}] = F^{-1} [\{k\}] \cap A (n) \leftrightarrow \forall x (x \in G^{-1} [\{k\}] \leftrightarrow x \in (F^{-1} [\{k\}] \cap A (n)))$
249	241 248	sylibr	$⊢ ((φ \land n \in ℕ) \land k \in (ran F ∖ \{0\})) \to G^{-1} [\{k\}] = F^{-1} [\{k\}] \cap A (n)$
250	249	fveq2d	$⊢ ((φ \land n \in ℕ) \land k \in (ran F ∖ \{0\})) \to vol (G^{-1} [\{k\}]) = vol (F^{-1} [\{k\}] \cap A (n))$
251	250	oveq2d	$⊢ ((φ \land n \in ℕ) \land k \in (ran F ∖ \{0\})) \to k vol (G^{-1} [\{k\}]) = k vol (F^{-1} [\{k\}] \cap A (n))$
252	251	sumeq2dv	$⊢ (φ \land n \in ℕ) \to \sum_{k \in ran F ∖ \{0\}} k vol (G^{-1} [\{k\}]) = \sum_{k \in ran F ∖ \{0\}} k vol (F^{-1} [\{k\}] \cap A (n))$
253	203 252	eqtrd	$⊢ (φ \land n \in ℕ) \to \int^{1} (G) = \sum_{k \in ran F ∖ \{0\}} k vol (F^{-1} [\{k\}] \cap A (n))$
254	253	mpteq2dva	$⊢ φ \to (n \in ℕ ⟼ \int^{1} (G)) = (n \in ℕ ⟼ \sum_{k \in ran F ∖ \{0\}} k vol (F^{-1} [\{k\}] \cap A (n)))$
255	254	fveq1d	$⊢ φ \to (n \in ℕ ⟼ \int^{1} (G)) (j) = (n \in ℕ ⟼ \sum_{k \in ran F ∖ \{0\}} k vol (F^{-1} [\{k\}] \cap A (n))) (j)$
256	167	sumeq2sdv	$⊢ n = j \to \sum_{k \in ran F ∖ \{0\}} k vol (F^{-1} [\{k\}] \cap A (n)) = \sum_{k \in ran F ∖ \{0\}} k vol (F^{-1} [\{k\}] \cap A (j))$
257		eqid	$⊢ (n \in ℕ ⟼ \sum_{k \in ran F ∖ \{0\}} k vol (F^{-1} [\{k\}] \cap A (n))) = (n \in ℕ ⟼ \sum_{k \in ran F ∖ \{0\}} k vol (F^{-1} [\{k\}] \cap A (n)))$
258		sumex	$⊢ \sum_{k \in ran F ∖ \{0\}} k vol (F^{-1} [\{k\}] \cap A (j)) \in V$
259	256 257 258	fvmpt	$⊢ j \in ℕ \to (n \in ℕ ⟼ \sum_{k \in ran F ∖ \{0\}} k vol (F^{-1} [\{k\}] \cap A (n))) (j) = \sum_{k \in ran F ∖ \{0\}} k vol (F^{-1} [\{k\}] \cap A (j))$
260	170	sumeq2sdv	$⊢ j \in ℕ \to \sum_{k \in ran F ∖ \{0\}} (n \in ℕ ⟼ k vol (F^{-1} [\{k\}] \cap A (n))) (j) = \sum_{k \in ran F ∖ \{0\}} k vol (F^{-1} [\{k\}] \cap A (j))$
261	259 260	eqtr4d	$⊢ j \in ℕ \to (n \in ℕ ⟼ \sum_{k \in ran F ∖ \{0\}} k vol (F^{-1} [\{k\}] \cap A (n))) (j) = \sum_{k \in ran F ∖ \{0\}} (n \in ℕ ⟼ k vol (F^{-1} [\{k\}] \cap A (n))) (j)$
262	255 261	sylan9eq	$⊢ (φ \land j \in ℕ) \to (n \in ℕ ⟼ \int^{1} (G)) (j) = \sum_{k \in ran F ∖ \{0\}} (n \in ℕ ⟼ k vol (F^{-1} [\{k\}] \cap A (n))) (j)$
263	6 7 12 174 176 182 262	climfsum	$⊢ φ \to (n \in ℕ ⟼ \int^{1} (G)) ⇝ \sum_{k \in ran F ∖ \{0\}} k vol (F^{-1} [\{k\}])$
264		itg1val	$⊢ F \in dom \int^{1} \to \int^{1} (F) = \sum_{k \in ran F ∖ \{0\}} k vol (F^{-1} [\{k\}])$
265	4 264	syl	$⊢ φ \to \int^{1} (F) = \sum_{k \in ran F ∖ \{0\}} k vol (F^{-1} [\{k\}])$
266	263 265	breqtrrd	$⊢ φ \to (n \in ℕ ⟼ \int^{1} (G)) ⇝ \int^{1} (F)$

Metamath Proof Explorer

Theorem itg1climres

Proof