ismeas

Description: The property of being a measure. (Contributed by Thierry Arnoux, 10-Sep-2016) (Revised by Thierry Arnoux, 19-Oct-2016)

		Ref	Expression
	Assertion	ismeas	$⊢ S \in ⋃ ran sigAlgebra \to (M \in measures (S) \leftrightarrow (M : S ⟶ [0, +∞] \land M (\emptyset) = 0 \land \forall x \in 𝒫 S ((x ≼ ω \land \underset{y \in x}{Disj} y) \to M (⋃ x) = \underset{y \in x}{\sum^{*}} M (y))))$

Proof

Step	Hyp	Ref	Expression
1		elex	$⊢ M \in measures (S) \to M \in V$
2	1	a1i	$⊢ S \in ⋃ ran sigAlgebra \to (M \in measures (S) \to M \in V)$
3		simp1	$⊢ (M : S ⟶ [0, +∞] \land M (\emptyset) = 0 \land \forall x \in 𝒫 S ((x ≼ ω \land \underset{y \in x}{Disj} y) \to M (⋃ x) = \underset{y \in x}{\sum^{*}} M (y))) \to M : S ⟶ [0, +∞]$
4		ovex	$⊢ [0, +∞] \in V$
5		fex2	$⊢ (M : S ⟶ [0, +∞] \land S \in ⋃ ran sigAlgebra \land [0, +∞] \in V) \to M \in V$
6	5	3expb	$⊢ (M : S ⟶ [0, +∞] \land (S \in ⋃ ran sigAlgebra \land [0, +∞] \in V)) \to M \in V$
7	6	expcom	$⊢ (S \in ⋃ ran sigAlgebra \land [0, +∞] \in V) \to (M : S ⟶ [0, +∞] \to M \in V)$
8	4 7	mpan2	$⊢ S \in ⋃ ran sigAlgebra \to (M : S ⟶ [0, +∞] \to M \in V)$
9	3 8	syl5	$⊢ S \in ⋃ ran sigAlgebra \to ((M : S ⟶ [0, +∞] \land M (\emptyset) = 0 \land \forall x \in 𝒫 S ((x ≼ ω \land \underset{y \in x}{Disj} y) \to M (⋃ x) = \underset{y \in x}{\sum^{*}} M (y))) \to M \in V)$
10		df-meas	$⊢ measures = (s \in ⋃ ran sigAlgebra ⟼ \{m \| (m : s ⟶ [0, +∞] \land m (\emptyset) = 0 \land \forall x \in 𝒫 s ((x ≼ ω \land \underset{y \in x}{Disj} y) \to m (⋃ x) = \underset{y \in x}{\sum^{*}} m (y)))\})$
11		vex	$⊢ s \in V$
12		mapex	$⊢ (s \in V \land [0, +∞] \in V) \to \{m \| m : s ⟶ [0, +∞]\} \in V$
13	11 4 12	mp2an	$⊢ \{m \| m : s ⟶ [0, +∞]\} \in V$
14		simp1	$⊢ (m : s ⟶ [0, +∞] \land m (\emptyset) = 0 \land \forall x \in 𝒫 s ((x ≼ ω \land \underset{y \in x}{Disj} y) \to m (⋃ x) = \underset{y \in x}{\sum^{*}} m (y))) \to m : s ⟶ [0, +∞]$
15	14	ss2abi	$⊢ \{m \| (m : s ⟶ [0, +∞] \land m (\emptyset) = 0 \land \forall x \in 𝒫 s ((x ≼ ω \land \underset{y \in x}{Disj} y) \to m (⋃ x) = \underset{y \in x}{\sum^{*}} m (y)))\} \subseteq \{m \| m : s ⟶ [0, +∞]\}$
16	13 15	ssexi	$⊢ \{m \| (m : s ⟶ [0, +∞] \land m (\emptyset) = 0 \land \forall x \in 𝒫 s ((x ≼ ω \land \underset{y \in x}{Disj} y) \to m (⋃ x) = \underset{y \in x}{\sum^{*}} m (y)))\} \in V$
17		simpr	$⊢ (s = S \land m = M) \to m = M$
18		simpl	$⊢ (s = S \land m = M) \to s = S$
19	17 18	feq12d	$⊢ (s = S \land m = M) \to (m : s ⟶ [0, +∞] \leftrightarrow M : S ⟶ [0, +∞])$
20		fveq1	$⊢ m = M \to m (\emptyset) = M (\emptyset)$
21	20	eqeq1d	$⊢ m = M \to (m (\emptyset) = 0 \leftrightarrow M (\emptyset) = 0)$
22	21	adantl	$⊢ (s = S \land m = M) \to (m (\emptyset) = 0 \leftrightarrow M (\emptyset) = 0)$
23	18	pweqd	$⊢ (s = S \land m = M) \to 𝒫 s = 𝒫 S$
24		fveq1	$⊢ m = M \to m (⋃ x) = M (⋃ x)$
25		fveq1	$⊢ m = M \to m (y) = M (y)$
26	25	esumeq2sdv	$⊢ m = M \to \underset{y \in x}{\sum^{}} m (y) = \underset{y \in x}{\sum^{}} M (y)$
27	24 26	eqeq12d	$⊢ m = M \to (m (⋃ x) = \underset{y \in x}{\sum^{}} m (y) \leftrightarrow M (⋃ x) = \underset{y \in x}{\sum^{}} M (y))$
28	27	imbi2d	$⊢ m = M \to (((x ≼ ω \land \underset{y \in x}{Disj} y) \to m (⋃ x) = \underset{y \in x}{\sum^{}} m (y)) \leftrightarrow ((x ≼ ω \land \underset{y \in x}{Disj} y) \to M (⋃ x) = \underset{y \in x}{\sum^{}} M (y)))$
29	28	adantl	$⊢ (s = S \land m = M) \to (((x ≼ ω \land \underset{y \in x}{Disj} y) \to m (⋃ x) = \underset{y \in x}{\sum^{}} m (y)) \leftrightarrow ((x ≼ ω \land \underset{y \in x}{Disj} y) \to M (⋃ x) = \underset{y \in x}{\sum^{}} M (y)))$
30	23 29	raleqbidv	$⊢ (s = S \land m = M) \to (\forall x \in 𝒫 s ((x ≼ ω \land \underset{y \in x}{Disj} y) \to m (⋃ x) = \underset{y \in x}{\sum^{}} m (y)) \leftrightarrow \forall x \in 𝒫 S ((x ≼ ω \land \underset{y \in x}{Disj} y) \to M (⋃ x) = \underset{y \in x}{\sum^{}} M (y)))$
31	19 22 30	3anbi123d	$⊢ (s = S \land m = M) \to ((m : s ⟶ [0, +∞] \land m (\emptyset) = 0 \land \forall x \in 𝒫 s ((x ≼ ω \land \underset{y \in x}{Disj} y) \to m (⋃ x) = \underset{y \in x}{\sum^{}} m (y))) \leftrightarrow (M : S ⟶ [0, +∞] \land M (\emptyset) = 0 \land \forall x \in 𝒫 S ((x ≼ ω \land \underset{y \in x}{Disj} y) \to M (⋃ x) = \underset{y \in x}{\sum^{}} M (y))))$
32	10 16 31	abfmpel	$⊢ (S \in ⋃ ran sigAlgebra \land M \in V) \to (M \in measures (S) \leftrightarrow (M : S ⟶ [0, +∞] \land M (\emptyset) = 0 \land \forall x \in 𝒫 S ((x ≼ ω \land \underset{y \in x}{Disj} y) \to M (⋃ x) = \underset{y \in x}{\sum^{*}} M (y))))$
33	32	ex	$⊢ S \in ⋃ ran sigAlgebra \to (M \in V \to (M \in measures (S) \leftrightarrow (M : S ⟶ [0, +∞] \land M (\emptyset) = 0 \land \forall x \in 𝒫 S ((x ≼ ω \land \underset{y \in x}{Disj} y) \to M (⋃ x) = \underset{y \in x}{\sum^{*}} M (y)))))$
34	2 9 33	pm5.21ndd	$⊢ S \in ⋃ ran sigAlgebra \to (M \in measures (S) \leftrightarrow (M : S ⟶ [0, +∞] \land M (\emptyset) = 0 \land \forall x \in 𝒫 S ((x ≼ ω \land \underset{y \in x}{Disj} y) \to M (⋃ x) = \underset{y \in x}{\sum^{*}} M (y))))$

Metamath Proof Explorer

Theorem ismeas

Proof