measdivcst

Description: Division of a measure by a positive constant is a measure. (Contributed by Thierry Arnoux, 25-Dec-2016) (Revised by Thierry Arnoux, 30-Jan-2017)

		Ref	Expression
	Assertion	measdivcst	$⊢ (M \in measures (S) \land A \in ℝ^{+}) \to M \circ_{fc} \div_{𝑒} A \in measures (S)$

Proof

Step	Hyp	Ref	Expression
1		ofcfval3	$⊢ (M \in measures (S) \land A \in ℝ^{+}) \to M \circ_{fc} \div_{𝑒} A = (x \in dom M ⟼ M (x) \div_{𝑒} A)$
2		measfrge0	$⊢ M \in measures (S) \to M : S ⟶ [0, +∞]$
3	2	fdmd	$⊢ M \in measures (S) \to dom M = S$
4	3	adantr	$⊢ (M \in measures (S) \land A \in ℝ^{+}) \to dom M = S$
5	4	mpteq1d	$⊢ (M \in measures (S) \land A \in ℝ^{+}) \to (x \in dom M ⟼ M (x) \div_{𝑒} A) = (x \in S ⟼ M (x) \div_{𝑒} A)$
6	1 5	eqtrd	$⊢ (M \in measures (S) \land A \in ℝ^{+}) \to M \circ_{fc} \div_{𝑒} A = (x \in S ⟼ M (x) \div_{𝑒} A)$
7		measvxrge0	$⊢ (M \in measures (S) \land x \in S) \to M (x) \in [0, +∞]$
8	7	adantlr	$⊢ ((M \in measures (S) \land A \in ℝ^{+}) \land x \in S) \to M (x) \in [0, +∞]$
9		simplr	$⊢ ((M \in measures (S) \land A \in ℝ^{+}) \land x \in S) \to A \in ℝ^{+}$
10	8 9	xrpxdivcld	$⊢ ((M \in measures (S) \land A \in ℝ^{+}) \land x \in S) \to M (x) \div_{𝑒} A \in [0, +∞]$
11	10	fmpttd	$⊢ (M \in measures (S) \land A \in ℝ^{+}) \to (x \in S ⟼ M (x) \div_{𝑒} A) : S ⟶ [0, +∞]$
12		measbase	$⊢ M \in measures (S) \to S \in ⋃ ran sigAlgebra$
13		0elsiga	$⊢ S \in ⋃ ran sigAlgebra \to \emptyset \in S$
14	12 13	syl	$⊢ M \in measures (S) \to \emptyset \in S$
15	14	adantr	$⊢ (M \in measures (S) \land A \in ℝ^{+}) \to \emptyset \in S$
16		ovex	$⊢ M (\emptyset) \div_{𝑒} A \in V$
17		fveq2	$⊢ x = \emptyset \to M (x) = M (\emptyset)$
18	17	oveq1d	$⊢ x = \emptyset \to M (x) \div_{𝑒} A = M (\emptyset) \div_{𝑒} A$
19		eqid	$⊢ (x \in S ⟼ M (x) \div_{𝑒} A) = (x \in S ⟼ M (x) \div_{𝑒} A)$
20	18 19	fvmptg	$⊢ (\emptyset \in S \land M (\emptyset) \div_{𝑒} A \in V) \to (x \in S ⟼ M (x) \div_{𝑒} A) (\emptyset) = M (\emptyset) \div_{𝑒} A$
21	15 16 20	sylancl	$⊢ (M \in measures (S) \land A \in ℝ^{+}) \to (x \in S ⟼ M (x) \div_{𝑒} A) (\emptyset) = M (\emptyset) \div_{𝑒} A$
22		measvnul	$⊢ M \in measures (S) \to M (\emptyset) = 0$
23	22	oveq1d	$⊢ M \in measures (S) \to M (\emptyset) \div_{𝑒} A = 0 \div_{𝑒} A$
24		xdiv0rp	$⊢ A \in ℝ^{+} \to 0 \div_{𝑒} A = 0$
25	23 24	sylan9eq	$⊢ (M \in measures (S) \land A \in ℝ^{+}) \to M (\emptyset) \div_{𝑒} A = 0$
26	21 25	eqtrd	$⊢ (M \in measures (S) \land A \in ℝ^{+}) \to (x \in S ⟼ M (x) \div_{𝑒} A) (\emptyset) = 0$
27		simpll	$⊢ (((M \in measures (S) \land A \in ℝ^{+}) \land y \in 𝒫 S) \land (y ≼ ω \land \underset{z \in y}{Disj} z)) \to (M \in measures (S) \land A \in ℝ^{+})$
28		simplr	$⊢ (((M \in measures (S) \land A \in ℝ^{+}) \land y \in 𝒫 S) \land (y ≼ ω \land \underset{z \in y}{Disj} z)) \to y \in 𝒫 S$
29		simprl	$⊢ (((M \in measures (S) \land A \in ℝ^{+}) \land y \in 𝒫 S) \land (y ≼ ω \land \underset{z \in y}{Disj} z)) \to y ≼ ω$
30		simprr	$⊢ (((M \in measures (S) \land A \in ℝ^{+}) \land y \in 𝒫 S) \land (y ≼ ω \land \underset{z \in y}{Disj} z)) \to \underset{z \in y}{Disj} z$
31		vex	$⊢ y \in V$
32	31	a1i	$⊢ ((M \in measures (S) \land A \in ℝ^{+}) \land y \in 𝒫 S) \to y \in V$
33		simplll	$⊢ (((M \in measures (S) \land A \in ℝ^{+}) \land y \in 𝒫 S) \land z \in y) \to M \in measures (S)$
34		velpw	$⊢ y \in 𝒫 S \leftrightarrow y \subseteq S$
35		ssel2	$⊢ (y \subseteq S \land z \in y) \to z \in S$
36	34 35	sylanb	$⊢ (y \in 𝒫 S \land z \in y) \to z \in S$
37	36	adantll	$⊢ (((M \in measures (S) \land A \in ℝ^{+}) \land y \in 𝒫 S) \land z \in y) \to z \in S$
38		measvxrge0	$⊢ (M \in measures (S) \land z \in S) \to M (z) \in [0, +∞]$
39	33 37 38	syl2anc	$⊢ (((M \in measures (S) \land A \in ℝ^{+}) \land y \in 𝒫 S) \land z \in y) \to M (z) \in [0, +∞]$
40		simplr	$⊢ ((M \in measures (S) \land A \in ℝ^{+}) \land y \in 𝒫 S) \to A \in ℝ^{+}$
41	32 39 40	esumdivc	$⊢ ((M \in measures (S) \land A \in ℝ^{+}) \land y \in 𝒫 S) \to \underset{z \in y}{\sum^{}} M (z) \div_{𝑒} A = \underset{z \in y}{\sum^{}} (M (z) \div_{𝑒} A)$
42	41	3ad2antr1	$⊢ ((M \in measures (S) \land A \in ℝ^{+}) \land (y \in 𝒫 S \land y ≼ ω \land \underset{z \in y}{Disj} z)) \to \underset{z \in y}{\sum^{}} M (z) \div_{𝑒} A = \underset{z \in y}{\sum^{}} (M (z) \div_{𝑒} A)$
43	12	ad2antrr	$⊢ ((M \in measures (S) \land A \in ℝ^{+}) \land (y \in 𝒫 S \land y ≼ ω \land \underset{z \in y}{Disj} z)) \to S \in ⋃ ran sigAlgebra$
44		simpr1	$⊢ ((M \in measures (S) \land A \in ℝ^{+}) \land (y \in 𝒫 S \land y ≼ ω \land \underset{z \in y}{Disj} z)) \to y \in 𝒫 S$
45		simpr2	$⊢ ((M \in measures (S) \land A \in ℝ^{+}) \land (y \in 𝒫 S \land y ≼ ω \land \underset{z \in y}{Disj} z)) \to y ≼ ω$
46		sigaclcu	$⊢ (S \in ⋃ ran sigAlgebra \land y \in 𝒫 S \land y ≼ ω) \to ⋃ y \in S$
47	43 44 45 46	syl3anc	$⊢ ((M \in measures (S) \land A \in ℝ^{+}) \land (y \in 𝒫 S \land y ≼ ω \land \underset{z \in y}{Disj} z)) \to ⋃ y \in S$
48		fveq2	$⊢ x = ⋃ y \to M (x) = M (⋃ y)$
49	48	oveq1d	$⊢ x = ⋃ y \to M (x) \div_{𝑒} A = M (⋃ y) \div_{𝑒} A$
50		ovex	$⊢ M (x) \div_{𝑒} A \in V$
51	49 19 50	fvmpt3i	$⊢ ⋃ y \in S \to (x \in S ⟼ M (x) \div_{𝑒} A) (⋃ y) = M (⋃ y) \div_{𝑒} A$
52	47 51	syl	$⊢ ((M \in measures (S) \land A \in ℝ^{+}) \land (y \in 𝒫 S \land y ≼ ω \land \underset{z \in y}{Disj} z)) \to (x \in S ⟼ M (x) \div_{𝑒} A) (⋃ y) = M (⋃ y) \div_{𝑒} A$
53		simpll	$⊢ ((M \in measures (S) \land A \in ℝ^{+}) \land (y \in 𝒫 S \land y ≼ ω \land \underset{z \in y}{Disj} z)) \to M \in measures (S)$
54		simpr3	$⊢ ((M \in measures (S) \land A \in ℝ^{+}) \land (y \in 𝒫 S \land y ≼ ω \land \underset{z \in y}{Disj} z)) \to \underset{z \in y}{Disj} z$
55		measvun	$⊢ (M \in measures (S) \land y \in 𝒫 S \land (y ≼ ω \land \underset{z \in y}{Disj} z)) \to M (⋃ y) = \underset{z \in y}{\sum^{*}} M (z)$
56	53 44 45 54 55	syl112anc	$⊢ ((M \in measures (S) \land A \in ℝ^{+}) \land (y \in 𝒫 S \land y ≼ ω \land \underset{z \in y}{Disj} z)) \to M (⋃ y) = \underset{z \in y}{\sum^{*}} M (z)$
57	56	oveq1d	$⊢ ((M \in measures (S) \land A \in ℝ^{+}) \land (y \in 𝒫 S \land y ≼ ω \land \underset{z \in y}{Disj} z)) \to M (⋃ y) \div_{𝑒} A = \underset{z \in y}{\sum^{*}} M (z) \div_{𝑒} A$
58	52 57	eqtrd	$⊢ ((M \in measures (S) \land A \in ℝ^{+}) \land (y \in 𝒫 S \land y ≼ ω \land \underset{z \in y}{Disj} z)) \to (x \in S ⟼ M (x) \div_{𝑒} A) (⋃ y) = \underset{z \in y}{\sum^{*}} M (z) \div_{𝑒} A$
59		fveq2	$⊢ x = z \to M (x) = M (z)$
60	59	oveq1d	$⊢ x = z \to M (x) \div_{𝑒} A = M (z) \div_{𝑒} A$
61	60 19 50	fvmpt3i	$⊢ z \in S \to (x \in S ⟼ M (x) \div_{𝑒} A) (z) = M (z) \div_{𝑒} A$
62	36 61	syl	$⊢ (y \in 𝒫 S \land z \in y) \to (x \in S ⟼ M (x) \div_{𝑒} A) (z) = M (z) \div_{𝑒} A$
63	62	esumeq2dv	$⊢ y \in 𝒫 S \to \underset{z \in y}{\sum^{}} (x \in S ⟼ M (x) \div_{𝑒} A) (z) = \underset{z \in y}{\sum^{}} (M (z) \div_{𝑒} A)$
64	44 63	syl	$⊢ ((M \in measures (S) \land A \in ℝ^{+}) \land (y \in 𝒫 S \land y ≼ ω \land \underset{z \in y}{Disj} z)) \to \underset{z \in y}{\sum^{}} (x \in S ⟼ M (x) \div_{𝑒} A) (z) = \underset{z \in y}{\sum^{}} (M (z) \div_{𝑒} A)$
65	42 58 64	3eqtr4d	$⊢ ((M \in measures (S) \land A \in ℝ^{+}) \land (y \in 𝒫 S \land y ≼ ω \land \underset{z \in y}{Disj} z)) \to (x \in S ⟼ M (x) \div_{𝑒} A) (⋃ y) = \underset{z \in y}{\sum^{*}} (x \in S ⟼ M (x) \div_{𝑒} A) (z)$
66	27 28 29 30 65	syl13anc	$⊢ (((M \in measures (S) \land A \in ℝ^{+}) \land y \in 𝒫 S) \land (y ≼ ω \land \underset{z \in y}{Disj} z)) \to (x \in S ⟼ M (x) \div_{𝑒} A) (⋃ y) = \underset{z \in y}{\sum^{*}} (x \in S ⟼ M (x) \div_{𝑒} A) (z)$
67	66	ex	$⊢ ((M \in measures (S) \land A \in ℝ^{+}) \land y \in 𝒫 S) \to ((y ≼ ω \land \underset{z \in y}{Disj} z) \to (x \in S ⟼ M (x) \div_{𝑒} A) (⋃ y) = \underset{z \in y}{\sum^{*}} (x \in S ⟼ M (x) \div_{𝑒} A) (z))$
68	67	ralrimiva	$⊢ (M \in measures (S) \land A \in ℝ^{+}) \to \forall y \in 𝒫 S ((y ≼ ω \land \underset{z \in y}{Disj} z) \to (x \in S ⟼ M (x) \div_{𝑒} A) (⋃ y) = \underset{z \in y}{\sum^{*}} (x \in S ⟼ M (x) \div_{𝑒} A) (z))$
69		ismeas	$⊢ S \in ⋃ ran sigAlgebra \to ((x \in S ⟼ M (x) \div_{𝑒} A) \in measures (S) \leftrightarrow ((x \in S ⟼ M (x) \div_{𝑒} A) : S ⟶ [0, +∞] \land (x \in S ⟼ M (x) \div_{𝑒} A) (\emptyset) = 0 \land \forall y \in 𝒫 S ((y ≼ ω \land \underset{z \in y}{Disj} z) \to (x \in S ⟼ M (x) \div_{𝑒} A) (⋃ y) = \underset{z \in y}{\sum^{*}} (x \in S ⟼ M (x) \div_{𝑒} A) (z))))$
70	12 69	syl	$⊢ M \in measures (S) \to ((x \in S ⟼ M (x) \div_{𝑒} A) \in measures (S) \leftrightarrow ((x \in S ⟼ M (x) \div_{𝑒} A) : S ⟶ [0, +∞] \land (x \in S ⟼ M (x) \div_{𝑒} A) (\emptyset) = 0 \land \forall y \in 𝒫 S ((y ≼ ω \land \underset{z \in y}{Disj} z) \to (x \in S ⟼ M (x) \div_{𝑒} A) (⋃ y) = \underset{z \in y}{\sum^{*}} (x \in S ⟼ M (x) \div_{𝑒} A) (z))))$
71	70	biimprd	$⊢ M \in measures (S) \to (((x \in S ⟼ M (x) \div_{𝑒} A) : S ⟶ [0, +∞] \land (x \in S ⟼ M (x) \div_{𝑒} A) (\emptyset) = 0 \land \forall y \in 𝒫 S ((y ≼ ω \land \underset{z \in y}{Disj} z) \to (x \in S ⟼ M (x) \div_{𝑒} A) (⋃ y) = \underset{z \in y}{\sum^{*}} (x \in S ⟼ M (x) \div_{𝑒} A) (z))) \to (x \in S ⟼ M (x) \div_{𝑒} A) \in measures (S))$
72	71	adantr	$⊢ (M \in measures (S) \land A \in ℝ^{+}) \to (((x \in S ⟼ M (x) \div_{𝑒} A) : S ⟶ [0, +∞] \land (x \in S ⟼ M (x) \div_{𝑒} A) (\emptyset) = 0 \land \forall y \in 𝒫 S ((y ≼ ω \land \underset{z \in y}{Disj} z) \to (x \in S ⟼ M (x) \div_{𝑒} A) (⋃ y) = \underset{z \in y}{\sum^{*}} (x \in S ⟼ M (x) \div_{𝑒} A) (z))) \to (x \in S ⟼ M (x) \div_{𝑒} A) \in measures (S))$
73	11 26 68 72	mp3and	$⊢ (M \in measures (S) \land A \in ℝ^{+}) \to (x \in S ⟼ M (x) \div_{𝑒} A) \in measures (S)$
74	6 73	eqeltrd	$⊢ (M \in measures (S) \land A \in ℝ^{+}) \to M \circ_{fc} \div_{𝑒} A \in measures (S)$

Metamath Proof Explorer

Theorem measdivcst

Proof