measdivcstALTV

Description: Alternate version of measdivcst . (Contributed by Thierry Arnoux, 25-Dec-2016) (New usage is discouraged.)

		Ref	Expression
	Assertion	measdivcstALTV	$⊢ (M \in measures (S) \land A \in ℝ^{+}) \to (x \in S ⟼ M (x) \div_{𝑒} A) \in measures (S)$

Proof

Step	Hyp	Ref	Expression
1		funmpt	$⊢ Fun (x \in S ⟼ M (x) \div_{𝑒} A)$
2		ovex	$⊢ M (x) \div_{𝑒} A \in V$
3	2	rgenw	$⊢ \forall x \in S M (x) \div_{𝑒} A \in V$
4		dmmptg	$⊢ \forall x \in S M (x) \div_{𝑒} A \in V \to dom (x \in S ⟼ M (x) \div_{𝑒} A) = S$
5	3 4	ax-mp	$⊢ dom (x \in S ⟼ M (x) \div_{𝑒} A) = S$
6		df-fn	$⊢ (x \in S ⟼ M (x) \div_{𝑒} A) Fn S \leftrightarrow (Fun (x \in S ⟼ M (x) \div_{𝑒} A) \land dom (x \in S ⟼ M (x) \div_{𝑒} A) = S)$
7	1 5 6	mpbir2an	$⊢ (x \in S ⟼ M (x) \div_{𝑒} A) Fn S$
8	7	a1i	$⊢ (M \in measures (S) \land A \in ℝ^{+}) \to (x \in S ⟼ M (x) \div_{𝑒} A) Fn S$
9		vex	$⊢ y \in V$
10		eqid	$⊢ (x \in S ⟼ M (x) \div_{𝑒} A) = (x \in S ⟼ M (x) \div_{𝑒} A)$
11	10	elrnmpt	$⊢ y \in V \to (y \in ran (x \in S ⟼ M (x) \div_{𝑒} A) \leftrightarrow \exists x \in S y = M (x) \div_{𝑒} A)$
12	9 11	ax-mp	$⊢ y \in ran (x \in S ⟼ M (x) \div_{𝑒} A) \leftrightarrow \exists x \in S y = M (x) \div_{𝑒} A$
13		measfrge0	$⊢ M \in measures (S) \to M : S ⟶ [0, +∞]$
14		ffvelrn	$⊢ (M : S ⟶ [0, +∞] \land x \in S) \to M (x) \in [0, +∞]$
15	13 14	sylan	$⊢ (M \in measures (S) \land x \in S) \to M (x) \in [0, +∞]$
16	15	adantlr	$⊢ ((M \in measures (S) \land A \in ℝ^{+}) \land x \in S) \to M (x) \in [0, +∞]$
17		simplr	$⊢ ((M \in measures (S) \land A \in ℝ^{+}) \land x \in S) \to A \in ℝ^{+}$
18	16 17	xrpxdivcld	$⊢ ((M \in measures (S) \land A \in ℝ^{+}) \land x \in S) \to M (x) \div_{𝑒} A \in [0, +∞]$
19		eleq1a	$⊢ M (x) \div_{𝑒} A \in [0, +∞] \to (y = M (x) \div_{𝑒} A \to y \in [0, +∞])$
20	18 19	syl	$⊢ ((M \in measures (S) \land A \in ℝ^{+}) \land x \in S) \to (y = M (x) \div_{𝑒} A \to y \in [0, +∞])$
21	20	rexlimdva	$⊢ (M \in measures (S) \land A \in ℝ^{+}) \to (\exists x \in S y = M (x) \div_{𝑒} A \to y \in [0, +∞])$
22	12 21	syl5bi	$⊢ (M \in measures (S) \land A \in ℝ^{+}) \to (y \in ran (x \in S ⟼ M (x) \div_{𝑒} A) \to y \in [0, +∞])$
23	22	ssrdv	$⊢ (M \in measures (S) \land A \in ℝ^{+}) \to ran (x \in S ⟼ M (x) \div_{𝑒} A) \subseteq [0, +∞]$
24		df-f	$⊢ (x \in S ⟼ M (x) \div_{𝑒} A) : S ⟶ [0, +∞] \leftrightarrow ((x \in S ⟼ M (x) \div_{𝑒} A) Fn S \land ran (x \in S ⟼ M (x) \div_{𝑒} A) \subseteq [0, +∞])$
25	8 23 24	sylanbrc	$⊢ (M \in measures (S) \land A \in ℝ^{+}) \to (x \in S ⟼ M (x) \div_{𝑒} A) : S ⟶ [0, +∞]$
26		measbase	$⊢ M \in measures (S) \to S \in ⋃ ran sigAlgebra$
27		0elsiga	$⊢ S \in ⋃ ran sigAlgebra \to \emptyset \in S$
28	26 27	syl	$⊢ M \in measures (S) \to \emptyset \in S$
29	28	adantr	$⊢ (M \in measures (S) \land A \in ℝ^{+}) \to \emptyset \in S$
30		ovex	$⊢ M (\emptyset) \div_{𝑒} A \in V$
31	29 30	jctir	$⊢ (M \in measures (S) \land A \in ℝ^{+}) \to (\emptyset \in S \land M (\emptyset) \div_{𝑒} A \in V)$
32		fveq2	$⊢ x = \emptyset \to M (x) = M (\emptyset)$
33	32	oveq1d	$⊢ x = \emptyset \to M (x) \div_{𝑒} A = M (\emptyset) \div_{𝑒} A$
34	33 10	fvmptg	$⊢ (\emptyset \in S \land M (\emptyset) \div_{𝑒} A \in V) \to (x \in S ⟼ M (x) \div_{𝑒} A) (\emptyset) = M (\emptyset) \div_{𝑒} A$
35	31 34	syl	$⊢ (M \in measures (S) \land A \in ℝ^{+}) \to (x \in S ⟼ M (x) \div_{𝑒} A) (\emptyset) = M (\emptyset) \div_{𝑒} A$
36		measvnul	$⊢ M \in measures (S) \to M (\emptyset) = 0$
37	36	oveq1d	$⊢ M \in measures (S) \to M (\emptyset) \div_{𝑒} A = 0 \div_{𝑒} A$
38		xdiv0rp	$⊢ A \in ℝ^{+} \to 0 \div_{𝑒} A = 0$
39	37 38	sylan9eq	$⊢ (M \in measures (S) \land A \in ℝ^{+}) \to M (\emptyset) \div_{𝑒} A = 0$
40	35 39	eqtrd	$⊢ (M \in measures (S) \land A \in ℝ^{+}) \to (x \in S ⟼ M (x) \div_{𝑒} A) (\emptyset) = 0$
41		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 ℝ^{+})$
42		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$
43		simprl	$⊢ (((M \in measures (S) \land A \in ℝ^{+}) \land y \in 𝒫 S) \land (y ≼ ω \land \underset{z \in y}{Disj} z)) \to y ≼ ω$
44		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$
45	42 43 44	3jca	$⊢ (((M \in measures (S) \land A \in ℝ^{+}) \land y \in 𝒫 S) \land (y ≼ ω \land \underset{z \in y}{Disj} z)) \to (y \in 𝒫 S \land y ≼ ω \land \underset{z \in y}{Disj} z)$
46	9	a1i	$⊢ ((M \in measures (S) \land A \in ℝ^{+}) \land y \in 𝒫 S) \to y \in V$
47		simplll	$⊢ (((M \in measures (S) \land A \in ℝ^{+}) \land y \in 𝒫 S) \land z \in y) \to M \in measures (S)$
48		simplr	$⊢ (((M \in measures (S) \land A \in ℝ^{+}) \land y \in 𝒫 S) \land z \in y) \to y \in 𝒫 S$
49		simpr	$⊢ (((M \in measures (S) \land A \in ℝ^{+}) \land y \in 𝒫 S) \land z \in y) \to z \in y$
50		elpwg	$⊢ y \in V \to (y \in 𝒫 S \leftrightarrow y \subseteq S)$
51	9 50	ax-mp	$⊢ y \in 𝒫 S \leftrightarrow y \subseteq S$
52		ssel2	$⊢ (y \subseteq S \land z \in y) \to z \in S$
53	51 52	sylanb	$⊢ (y \in 𝒫 S \land z \in y) \to z \in S$
54	48 49 53	syl2anc	$⊢ (((M \in measures (S) \land A \in ℝ^{+}) \land y \in 𝒫 S) \land z \in y) \to z \in S$
55		measvxrge0	$⊢ (M \in measures (S) \land z \in S) \to M (z) \in [0, +∞]$
56	47 54 55	syl2anc	$⊢ (((M \in measures (S) \land A \in ℝ^{+}) \land y \in 𝒫 S) \land z \in y) \to M (z) \in [0, +∞]$
57		simplr	$⊢ ((M \in measures (S) \land A \in ℝ^{+}) \land y \in 𝒫 S) \to A \in ℝ^{+}$
58	46 56 57	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)$
59	58	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)$
60	26	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$
61		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$
62		simpr2	$⊢ ((M \in measures (S) \land A \in ℝ^{+}) \land (y \in 𝒫 S \land y ≼ ω \land \underset{z \in y}{Disj} z)) \to y ≼ ω$
63		sigaclcu	$⊢ (S \in ⋃ ran sigAlgebra \land y \in 𝒫 S \land y ≼ ω) \to ⋃ y \in S$
64	60 61 62 63	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$
65		fveq2	$⊢ x = ⋃ y \to M (x) = M (⋃ y)$
66	65	oveq1d	$⊢ x = ⋃ y \to M (x) \div_{𝑒} A = M (⋃ y) \div_{𝑒} A$
67	66 10 2	fvmpt3i	$⊢ ⋃ y \in S \to (x \in S ⟼ M (x) \div_{𝑒} A) (⋃ y) = M (⋃ y) \div_{𝑒} A$
68	64 67	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$
69		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)$
70	69 61	jca	$⊢ ((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 y \in 𝒫 S)$
71		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$
72	62 71	jca	$⊢ ((M \in measures (S) \land A \in ℝ^{+}) \land (y \in 𝒫 S \land y ≼ ω \land \underset{z \in y}{Disj} z)) \to (y ≼ ω \land \underset{z \in y}{Disj} z)$
73		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)$
74	73	3expia	$⊢ (M \in measures (S) \land y \in 𝒫 S) \to ((y ≼ ω \land \underset{z \in y}{Disj} z) \to M (⋃ y) = \underset{z \in y}{\sum^{*}} M (z))$
75	74	ralrimiva	$⊢ M \in measures (S) \to \forall y \in 𝒫 S ((y ≼ ω \land \underset{z \in y}{Disj} z) \to M (⋃ y) = \underset{z \in y}{\sum^{*}} M (z))$
76	75	r19.21bi	$⊢ (M \in measures (S) \land y \in 𝒫 S) \to ((y ≼ ω \land \underset{z \in y}{Disj} z) \to M (⋃ y) = \underset{z \in y}{\sum^{*}} M (z))$
77	70 72 76	sylc	$⊢ ((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)$
78	77	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$
79	68 78	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$
80		fveq2	$⊢ x = z \to M (x) = M (z)$
81	80	oveq1d	$⊢ x = z \to M (x) \div_{𝑒} A = M (z) \div_{𝑒} A$
82	81 10 2	fvmpt3i	$⊢ z \in S \to (x \in S ⟼ M (x) \div_{𝑒} A) (z) = M (z) \div_{𝑒} A$
83	53 82	syl	$⊢ (y \in 𝒫 S \land z \in y) \to (x \in S ⟼ M (x) \div_{𝑒} A) (z) = M (z) \div_{𝑒} A$
84	83	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)$
85	61 84	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)$
86	59 79 85	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)$
87	41 45 86	syl2anc	$⊢ (((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)$
88	87	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))$
89	88	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))$
90	25 40 89	3jca	$⊢ (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)))$
91		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))))$
92	26 91	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))))$
93	92	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))$
94	93	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))$
95	90 94	mpd	$⊢ (M \in measures (S) \land A \in ℝ^{+}) \to (x \in S ⟼ M (x) \div_{𝑒} A) \in measures (S)$

Metamath Proof Explorer

Theorem measdivcstALTV

Proof