sibfinima

Description: The measure of the intersection of any two preimages by simple functions is a real number. (Contributed by Thierry Arnoux, 21-Mar-2018)

	Ref	Expression
Hypotheses	sitgval.b	$⊢ B = {Base}_{W}$
	sitgval.j	$⊢ J = TopOpen (W)$
	sitgval.s	$⊢ S = 𝛔 (J)$
	sitgval.0	$⊢ \underset{˙}{0} = 0_{W}$
	sitgval.x	$⊢ \underset{˙}{\cdot} = \cdot_{W}$
	sitgval.h	$⊢ H = ℝHom (Scalar (W))$
	sitgval.1	$⊢ φ \to W \in V$
	sitgval.2	$⊢ φ \to M \in ⋃ ran measures$
	sibfmbl.1	$⊢ φ \to F \in ℑ_{M}^{W}$
	sibfinima.g	$⊢ φ \to G \in ℑ_{M}^{W}$
	sibfinima.w	$⊢ φ \to W \in TopSp$
	sibfinima.j	$⊢ φ \to J \in Fre$
Assertion	sibfinima	$⊢ ((φ \land X \in ran F \land Y \in ran G) \land (X \neq \underset{˙}{0} \lor Y \neq \underset{˙}{0})) \to M (F^{-1} [\{X\}] \cap G^{-1} [\{Y\}]) \in [0, +∞)$

Proof

Step	Hyp	Ref	Expression
1		sitgval.b	$⊢ B = {Base}_{W}$
2		sitgval.j	$⊢ J = TopOpen (W)$
3		sitgval.s	$⊢ S = 𝛔 (J)$
4		sitgval.0	$⊢ \underset{˙}{0} = 0_{W}$
5		sitgval.x	$⊢ \underset{˙}{\cdot} = \cdot_{W}$
6		sitgval.h	$⊢ H = ℝHom (Scalar (W))$
7		sitgval.1	$⊢ φ \to W \in V$
8		sitgval.2	$⊢ φ \to M \in ⋃ ran measures$
9		sibfmbl.1	$⊢ φ \to F \in ℑ_{M}^{W}$
10		sibfinima.g	$⊢ φ \to G \in ℑ_{M}^{W}$
11		sibfinima.w	$⊢ φ \to W \in TopSp$
12		sibfinima.j	$⊢ φ \to J \in Fre$
13		measbasedom	$⊢ M \in ⋃ ran measures \leftrightarrow M \in measures (dom M)$
14	8 13	sylib	$⊢ φ \to M \in measures (dom M)$
15	14	3ad2ant1	$⊢ (φ \land X \in ran F \land Y \in ran G) \to M \in measures (dom M)$
16		dmmeas	$⊢ M \in ⋃ ran measures \to dom M \in ⋃ ran sigAlgebra$
17	8 16	syl	$⊢ φ \to dom M \in ⋃ ran sigAlgebra$
18	17	3ad2ant1	$⊢ (φ \land X \in ran F \land Y \in ran G) \to dom M \in ⋃ ran sigAlgebra$
19	12	sgsiga	$⊢ φ \to 𝛔 (J) \in ⋃ ran sigAlgebra$
20	3 19	eqeltrid	$⊢ φ \to S \in ⋃ ran sigAlgebra$
21	20	3ad2ant1	$⊢ (φ \land X \in ran F \land Y \in ran G) \to S \in ⋃ ran sigAlgebra$
22	1 2 3 4 5 6 7 8 9	sibfmbl	$⊢ φ \to F \in (dom M {MblFn}_{μ} S)$
23	22	3ad2ant1	$⊢ (φ \land X \in ran F \land Y \in ran G) \to F \in (dom M {MblFn}_{μ} S)$
24	2	tpstop	$⊢ W \in TopSp \to J \in Top$
25		cldssbrsiga	$⊢ J \in Top \to Clsd (J) \subseteq 𝛔 (J)$
26	11 24 25	3syl	$⊢ φ \to Clsd (J) \subseteq 𝛔 (J)$
27	26 3	sseqtrrdi	$⊢ φ \to Clsd (J) \subseteq S$
28	27	3ad2ant1	$⊢ (φ \land X \in ran F \land Y \in ran G) \to Clsd (J) \subseteq S$
29	12	3ad2ant1	$⊢ (φ \land X \in ran F \land Y \in ran G) \to J \in Fre$
30	1 2 3 4 5 6 7 8 9	sibff	$⊢ φ \to F : ⋃ dom M ⟶ ⋃ J$
31	30	frnd	$⊢ φ \to ran F \subseteq ⋃ J$
32	31	3ad2ant1	$⊢ (φ \land X \in ran F \land Y \in ran G) \to ran F \subseteq ⋃ J$
33		simp2	$⊢ (φ \land X \in ran F \land Y \in ran G) \to X \in ran F$
34	32 33	sseldd	$⊢ (φ \land X \in ran F \land Y \in ran G) \to X \in ⋃ J$
35		eqid	$⊢ ⋃ J = ⋃ J$
36	35	t1sncld	$⊢ (J \in Fre \land X \in ⋃ J) \to \{X\} \in Clsd (J)$
37	29 34 36	syl2anc	$⊢ (φ \land X \in ran F \land Y \in ran G) \to \{X\} \in Clsd (J)$
38	28 37	sseldd	$⊢ (φ \land X \in ran F \land Y \in ran G) \to \{X\} \in S$
39	18 21 23 38	mbfmcnvima	$⊢ (φ \land X \in ran F \land Y \in ran G) \to F^{-1} [\{X\}] \in dom M$
40	1 2 3 4 5 6 7 8 10	sibfmbl	$⊢ φ \to G \in (dom M {MblFn}_{μ} S)$
41	40	3ad2ant1	$⊢ (φ \land X \in ran F \land Y \in ran G) \to G \in (dom M {MblFn}_{μ} S)$
42	1 2 3 4 5 6 7 8 10	sibff	$⊢ φ \to G : ⋃ dom M ⟶ ⋃ J$
43	42	frnd	$⊢ φ \to ran G \subseteq ⋃ J$
44	43	3ad2ant1	$⊢ (φ \land X \in ran F \land Y \in ran G) \to ran G \subseteq ⋃ J$
45		simp3	$⊢ (φ \land X \in ran F \land Y \in ran G) \to Y \in ran G$
46	44 45	sseldd	$⊢ (φ \land X \in ran F \land Y \in ran G) \to Y \in ⋃ J$
47	35	t1sncld	$⊢ (J \in Fre \land Y \in ⋃ J) \to \{Y\} \in Clsd (J)$
48	29 46 47	syl2anc	$⊢ (φ \land X \in ran F \land Y \in ran G) \to \{Y\} \in Clsd (J)$
49	28 48	sseldd	$⊢ (φ \land X \in ran F \land Y \in ran G) \to \{Y\} \in S$
50	18 21 41 49	mbfmcnvima	$⊢ (φ \land X \in ran F \land Y \in ran G) \to G^{-1} [\{Y\}] \in dom M$
51		inelsiga	$⊢ (dom M \in ⋃ ran sigAlgebra \land F^{-1} [\{X\}] \in dom M \land G^{-1} [\{Y\}] \in dom M) \to F^{-1} [\{X\}] \cap G^{-1} [\{Y\}] \in dom M$
52	18 39 50 51	syl3anc	$⊢ (φ \land X \in ran F \land Y \in ran G) \to F^{-1} [\{X\}] \cap G^{-1} [\{Y\}] \in dom M$
53		measvxrge0	$⊢ (M \in measures (dom M) \land F^{-1} [\{X\}] \cap G^{-1} [\{Y\}] \in dom M) \to M (F^{-1} [\{X\}] \cap G^{-1} [\{Y\}]) \in [0, +∞]$
54	15 52 53	syl2anc	$⊢ (φ \land X \in ran F \land Y \in ran G) \to M (F^{-1} [\{X\}] \cap G^{-1} [\{Y\}]) \in [0, +∞]$
55		elxrge0	$⊢ M (F^{-1} [\{X\}] \cap G^{-1} [\{Y\}]) \in [0, +∞] \leftrightarrow (M (F^{-1} [\{X\}] \cap G^{-1} [\{Y\}]) \in ℝ^{*} \land 0 \leq M (F^{-1} [\{X\}] \cap G^{-1} [\{Y\}]))$
56	55	simplbi	$⊢ M (F^{-1} [\{X\}] \cap G^{-1} [\{Y\}]) \in [0, +∞] \to M (F^{-1} [\{X\}] \cap G^{-1} [\{Y\}]) \in ℝ^{*}$
57	54 56	syl	$⊢ (φ \land X \in ran F \land Y \in ran G) \to M (F^{-1} [\{X\}] \cap G^{-1} [\{Y\}]) \in ℝ^{*}$
58	57	adantr	$⊢ ((φ \land X \in ran F \land Y \in ran G) \land (X \neq \underset{˙}{0} \lor Y \neq \underset{˙}{0})) \to M (F^{-1} [\{X\}] \cap G^{-1} [\{Y\}]) \in ℝ^{*}$
59		0re	$⊢ 0 \in ℝ$
60	59	a1i	$⊢ ((φ \land X \in ran F \land Y \in ran G) \land (X \neq \underset{˙}{0} \lor Y \neq \underset{˙}{0})) \to 0 \in ℝ$
61	55	simprbi	$⊢ M (F^{-1} [\{X\}] \cap G^{-1} [\{Y\}]) \in [0, +∞] \to 0 \leq M (F^{-1} [\{X\}] \cap G^{-1} [\{Y\}])$
62	54 61	syl	$⊢ (φ \land X \in ran F \land Y \in ran G) \to 0 \leq M (F^{-1} [\{X\}] \cap G^{-1} [\{Y\}])$
63	62	adantr	$⊢ ((φ \land X \in ran F \land Y \in ran G) \land (X \neq \underset{˙}{0} \lor Y \neq \underset{˙}{0})) \to 0 \leq M (F^{-1} [\{X\}] \cap G^{-1} [\{Y\}])$
64	57	adantr	$⊢ ((φ \land X \in ran F \land Y \in ran G) \land X \neq \underset{˙}{0}) \to M (F^{-1} [\{X\}] \cap G^{-1} [\{Y\}]) \in ℝ^{*}$
65	15	adantr	$⊢ ((φ \land X \in ran F \land Y \in ran G) \land X \neq \underset{˙}{0}) \to M \in measures (dom M)$
66	39	adantr	$⊢ ((φ \land X \in ran F \land Y \in ran G) \land X \neq \underset{˙}{0}) \to F^{-1} [\{X\}] \in dom M$
67		measvxrge0	$⊢ (M \in measures (dom M) \land F^{-1} [\{X\}] \in dom M) \to M (F^{-1} [\{X\}]) \in [0, +∞]$
68	65 66 67	syl2anc	$⊢ ((φ \land X \in ran F \land Y \in ran G) \land X \neq \underset{˙}{0}) \to M (F^{-1} [\{X\}]) \in [0, +∞]$
69		elxrge0	$⊢ M (F^{-1} [\{X\}]) \in [0, +∞] \leftrightarrow (M (F^{-1} [\{X\}]) \in ℝ^{*} \land 0 \leq M (F^{-1} [\{X\}]))$
70	69	simplbi	$⊢ M (F^{-1} [\{X\}]) \in [0, +∞] \to M (F^{-1} [\{X\}]) \in ℝ^{*}$
71	68 70	syl	$⊢ ((φ \land X \in ran F \land Y \in ran G) \land X \neq \underset{˙}{0}) \to M (F^{-1} [\{X\}]) \in ℝ^{*}$
72		pnfxr	$⊢ +∞ \in ℝ^{*}$
73	72	a1i	$⊢ ((φ \land X \in ran F \land Y \in ran G) \land X \neq \underset{˙}{0}) \to +∞ \in ℝ^{*}$
74	52	adantr	$⊢ ((φ \land X \in ran F \land Y \in ran G) \land X \neq \underset{˙}{0}) \to F^{-1} [\{X\}] \cap G^{-1} [\{Y\}] \in dom M$
75		inss1	$⊢ F^{-1} [\{X\}] \cap G^{-1} [\{Y\}] \subseteq F^{-1} [\{X\}]$
76	75	a1i	$⊢ ((φ \land X \in ran F \land Y \in ran G) \land X \neq \underset{˙}{0}) \to F^{-1} [\{X\}] \cap G^{-1} [\{Y\}] \subseteq F^{-1} [\{X\}]$
77	65 74 66 76	measssd	$⊢ ((φ \land X \in ran F \land Y \in ran G) \land X \neq \underset{˙}{0}) \to M (F^{-1} [\{X\}] \cap G^{-1} [\{Y\}]) \leq M (F^{-1} [\{X\}])$
78		simpl1	$⊢ ((φ \land X \in ran F \land Y \in ran G) \land X \neq \underset{˙}{0}) \to φ$
79	33	anim1i	$⊢ ((φ \land X \in ran F \land Y \in ran G) \land X \neq \underset{˙}{0}) \to (X \in ran F \land X \neq \underset{˙}{0})$
80		eldifsn	$⊢ X \in (ran F ∖ \{\underset{˙}{0}\}) \leftrightarrow (X \in ran F \land X \neq \underset{˙}{0})$
81	79 80	sylibr	$⊢ ((φ \land X \in ran F \land Y \in ran G) \land X \neq \underset{˙}{0}) \to X \in (ran F ∖ \{\underset{˙}{0}\})$
82	1 2 3 4 5 6 7 8 9	sibfima	$⊢ (φ \land X \in (ran F ∖ \{\underset{˙}{0}\})) \to M (F^{-1} [\{X\}]) \in [0, +∞)$
83	78 81 82	syl2anc	$⊢ ((φ \land X \in ran F \land Y \in ran G) \land X \neq \underset{˙}{0}) \to M (F^{-1} [\{X\}]) \in [0, +∞)$
84		elico2	$⊢ (0 \in ℝ \land +∞ \in ℝ^{*}) \to (M (F^{-1} [\{X\}]) \in [0, +∞) \leftrightarrow (M (F^{-1} [\{X\}]) \in ℝ \land 0 \leq M (F^{-1} [\{X\}]) \land M (F^{-1} [\{X\}]) < +∞))$
85	59 72 84	mp2an	$⊢ M (F^{-1} [\{X\}]) \in [0, +∞) \leftrightarrow (M (F^{-1} [\{X\}]) \in ℝ \land 0 \leq M (F^{-1} [\{X\}]) \land M (F^{-1} [\{X\}]) < +∞)$
86	85	simp3bi	$⊢ M (F^{-1} [\{X\}]) \in [0, +∞) \to M (F^{-1} [\{X\}]) < +∞$
87	83 86	syl	$⊢ ((φ \land X \in ran F \land Y \in ran G) \land X \neq \underset{˙}{0}) \to M (F^{-1} [\{X\}]) < +∞$
88	64 71 73 77 87	xrlelttrd	$⊢ ((φ \land X \in ran F \land Y \in ran G) \land X \neq \underset{˙}{0}) \to M (F^{-1} [\{X\}] \cap G^{-1} [\{Y\}]) < +∞$
89	57	adantr	$⊢ ((φ \land X \in ran F \land Y \in ran G) \land Y \neq \underset{˙}{0}) \to M (F^{-1} [\{X\}] \cap G^{-1} [\{Y\}]) \in ℝ^{*}$
90	15	adantr	$⊢ ((φ \land X \in ran F \land Y \in ran G) \land Y \neq \underset{˙}{0}) \to M \in measures (dom M)$
91	50	adantr	$⊢ ((φ \land X \in ran F \land Y \in ran G) \land Y \neq \underset{˙}{0}) \to G^{-1} [\{Y\}] \in dom M$
92		measvxrge0	$⊢ (M \in measures (dom M) \land G^{-1} [\{Y\}] \in dom M) \to M (G^{-1} [\{Y\}]) \in [0, +∞]$
93	90 91 92	syl2anc	$⊢ ((φ \land X \in ran F \land Y \in ran G) \land Y \neq \underset{˙}{0}) \to M (G^{-1} [\{Y\}]) \in [0, +∞]$
94		elxrge0	$⊢ M (G^{-1} [\{Y\}]) \in [0, +∞] \leftrightarrow (M (G^{-1} [\{Y\}]) \in ℝ^{*} \land 0 \leq M (G^{-1} [\{Y\}]))$
95	94	simplbi	$⊢ M (G^{-1} [\{Y\}]) \in [0, +∞] \to M (G^{-1} [\{Y\}]) \in ℝ^{*}$
96	93 95	syl	$⊢ ((φ \land X \in ran F \land Y \in ran G) \land Y \neq \underset{˙}{0}) \to M (G^{-1} [\{Y\}]) \in ℝ^{*}$
97	72	a1i	$⊢ ((φ \land X \in ran F \land Y \in ran G) \land Y \neq \underset{˙}{0}) \to +∞ \in ℝ^{*}$
98	52	adantr	$⊢ ((φ \land X \in ran F \land Y \in ran G) \land Y \neq \underset{˙}{0}) \to F^{-1} [\{X\}] \cap G^{-1} [\{Y\}] \in dom M$
99		inss2	$⊢ F^{-1} [\{X\}] \cap G^{-1} [\{Y\}] \subseteq G^{-1} [\{Y\}]$
100	99	a1i	$⊢ ((φ \land X \in ran F \land Y \in ran G) \land Y \neq \underset{˙}{0}) \to F^{-1} [\{X\}] \cap G^{-1} [\{Y\}] \subseteq G^{-1} [\{Y\}]$
101	90 98 91 100	measssd	$⊢ ((φ \land X \in ran F \land Y \in ran G) \land Y \neq \underset{˙}{0}) \to M (F^{-1} [\{X\}] \cap G^{-1} [\{Y\}]) \leq M (G^{-1} [\{Y\}])$
102		simpl1	$⊢ ((φ \land X \in ran F \land Y \in ran G) \land Y \neq \underset{˙}{0}) \to φ$
103	45	anim1i	$⊢ ((φ \land X \in ran F \land Y \in ran G) \land Y \neq \underset{˙}{0}) \to (Y \in ran G \land Y \neq \underset{˙}{0})$
104		eldifsn	$⊢ Y \in (ran G ∖ \{\underset{˙}{0}\}) \leftrightarrow (Y \in ran G \land Y \neq \underset{˙}{0})$
105	103 104	sylibr	$⊢ ((φ \land X \in ran F \land Y \in ran G) \land Y \neq \underset{˙}{0}) \to Y \in (ran G ∖ \{\underset{˙}{0}\})$
106	1 2 3 4 5 6 7 8 10	sibfima	$⊢ (φ \land Y \in (ran G ∖ \{\underset{˙}{0}\})) \to M (G^{-1} [\{Y\}]) \in [0, +∞)$
107	102 105 106	syl2anc	$⊢ ((φ \land X \in ran F \land Y \in ran G) \land Y \neq \underset{˙}{0}) \to M (G^{-1} [\{Y\}]) \in [0, +∞)$
108		elico2	$⊢ (0 \in ℝ \land +∞ \in ℝ^{*}) \to (M (G^{-1} [\{Y\}]) \in [0, +∞) \leftrightarrow (M (G^{-1} [\{Y\}]) \in ℝ \land 0 \leq M (G^{-1} [\{Y\}]) \land M (G^{-1} [\{Y\}]) < +∞))$
109	59 72 108	mp2an	$⊢ M (G^{-1} [\{Y\}]) \in [0, +∞) \leftrightarrow (M (G^{-1} [\{Y\}]) \in ℝ \land 0 \leq M (G^{-1} [\{Y\}]) \land M (G^{-1} [\{Y\}]) < +∞)$
110	109	simp3bi	$⊢ M (G^{-1} [\{Y\}]) \in [0, +∞) \to M (G^{-1} [\{Y\}]) < +∞$
111	107 110	syl	$⊢ ((φ \land X \in ran F \land Y \in ran G) \land Y \neq \underset{˙}{0}) \to M (G^{-1} [\{Y\}]) < +∞$
112	89 96 97 101 111	xrlelttrd	$⊢ ((φ \land X \in ran F \land Y \in ran G) \land Y \neq \underset{˙}{0}) \to M (F^{-1} [\{X\}] \cap G^{-1} [\{Y\}]) < +∞$
113	88 112	jaodan	$⊢ ((φ \land X \in ran F \land Y \in ran G) \land (X \neq \underset{˙}{0} \lor Y \neq \underset{˙}{0})) \to M (F^{-1} [\{X\}] \cap G^{-1} [\{Y\}]) < +∞$
114		xrre3	$⊢ ((M (F^{-1} [\{X\}] \cap G^{-1} [\{Y\}]) \in ℝ^{*} \land 0 \in ℝ) \land (0 \leq M (F^{-1} [\{X\}] \cap G^{-1} [\{Y\}]) \land M (F^{-1} [\{X\}] \cap G^{-1} [\{Y\}]) < +∞)) \to M (F^{-1} [\{X\}] \cap G^{-1} [\{Y\}]) \in ℝ$
115	58 60 63 113 114	syl22anc	$⊢ ((φ \land X \in ran F \land Y \in ran G) \land (X \neq \underset{˙}{0} \lor Y \neq \underset{˙}{0})) \to M (F^{-1} [\{X\}] \cap G^{-1} [\{Y\}]) \in ℝ$
116		elico2	$⊢ (0 \in ℝ \land +∞ \in ℝ^{*}) \to (M (F^{-1} [\{X\}] \cap G^{-1} [\{Y\}]) \in [0, +∞) \leftrightarrow (M (F^{-1} [\{X\}] \cap G^{-1} [\{Y\}]) \in ℝ \land 0 \leq M (F^{-1} [\{X\}] \cap G^{-1} [\{Y\}]) \land M (F^{-1} [\{X\}] \cap G^{-1} [\{Y\}]) < +∞))$
117	59 72 116	mp2an	$⊢ M (F^{-1} [\{X\}] \cap G^{-1} [\{Y\}]) \in [0, +∞) \leftrightarrow (M (F^{-1} [\{X\}] \cap G^{-1} [\{Y\}]) \in ℝ \land 0 \leq M (F^{-1} [\{X\}] \cap G^{-1} [\{Y\}]) \land M (F^{-1} [\{X\}] \cap G^{-1} [\{Y\}]) < +∞)$
118	115 63 113 117	syl3anbrc	$⊢ ((φ \land X \in ran F \land Y \in ran G) \land (X \neq \underset{˙}{0} \lor Y \neq \underset{˙}{0})) \to M (F^{-1} [\{X\}] \cap G^{-1} [\{Y\}]) \in [0, +∞)$

Metamath Proof Explorer

Theorem sibfinima

Proof