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	⊢ 𝐵 = ( Base ‘ 𝑊 )
	sitgval.j	⊢ 𝐽 = ( TopOpen ‘ 𝑊 )
	sitgval.s	⊢ 𝑆 = ( sigaGen ‘ 𝐽 )
	sitgval.0	⊢ 0 = ( 0_g ‘ 𝑊 )
	sitgval.x	⊢ · = ( ·_𝑠 ‘ 𝑊 )
	sitgval.h	⊢ 𝐻 = ( ℝHom ‘ ( Scalar ‘ 𝑊 ) )
	sitgval.1	⊢ ( 𝜑 → 𝑊 ∈ 𝑉 )
	sitgval.2	⊢ ( 𝜑 → 𝑀 ∈ ∪ ran measures )
	sibfmbl.1	⊢ ( 𝜑 → 𝐹 ∈ dom ( 𝑊 sitg 𝑀 ) )
	sibfinima.g	⊢ ( 𝜑 → 𝐺 ∈ dom ( 𝑊 sitg 𝑀 ) )
	sibfinima.w	⊢ ( 𝜑 → 𝑊 ∈ TopSp )
	sibfinima.j	⊢ ( 𝜑 → 𝐽 ∈ Fre )
Assertion	sibfinima	⊢ ( ( ( 𝜑 ∧ 𝑋 ∈ ran 𝐹 ∧ 𝑌 ∈ ran 𝐺 ) ∧ ( 𝑋 ≠ 0 ∨ 𝑌 ≠ 0 ) ) → ( 𝑀 ‘ ( ( ^◡ 𝐹 “ { 𝑋 } ) ∩ ( ^◡ 𝐺 “ { 𝑌 } ) ) ) ∈ ( 0 [,) +∞ ) )

Proof

Step	Hyp	Ref	Expression
1		sitgval.b	⊢ 𝐵 = ( Base ‘ 𝑊 )
2		sitgval.j	⊢ 𝐽 = ( TopOpen ‘ 𝑊 )
3		sitgval.s	⊢ 𝑆 = ( sigaGen ‘ 𝐽 )
4		sitgval.0	⊢ 0 = ( 0_g ‘ 𝑊 )
5		sitgval.x	⊢ · = ( ·_𝑠 ‘ 𝑊 )
6		sitgval.h	⊢ 𝐻 = ( ℝHom ‘ ( Scalar ‘ 𝑊 ) )
7		sitgval.1	⊢ ( 𝜑 → 𝑊 ∈ 𝑉 )
8		sitgval.2	⊢ ( 𝜑 → 𝑀 ∈ ∪ ran measures )
9		sibfmbl.1	⊢ ( 𝜑 → 𝐹 ∈ dom ( 𝑊 sitg 𝑀 ) )
10		sibfinima.g	⊢ ( 𝜑 → 𝐺 ∈ dom ( 𝑊 sitg 𝑀 ) )
11		sibfinima.w	⊢ ( 𝜑 → 𝑊 ∈ TopSp )
12		sibfinima.j	⊢ ( 𝜑 → 𝐽 ∈ Fre )
13		measbasedom	⊢ ( 𝑀 ∈ ∪ ran measures ↔ 𝑀 ∈ ( measures ‘ dom 𝑀 ) )
14	8 13	sylib	⊢ ( 𝜑 → 𝑀 ∈ ( measures ‘ dom 𝑀 ) )
15	14	3ad2ant1	⊢ ( ( 𝜑 ∧ 𝑋 ∈ ran 𝐹 ∧ 𝑌 ∈ ran 𝐺 ) → 𝑀 ∈ ( measures ‘ dom 𝑀 ) )
16		dmmeas	⊢ ( 𝑀 ∈ ∪ ran measures → dom 𝑀 ∈ ∪ ran sigAlgebra )
17	8 16	syl	⊢ ( 𝜑 → dom 𝑀 ∈ ∪ ran sigAlgebra )
18	17	3ad2ant1	⊢ ( ( 𝜑 ∧ 𝑋 ∈ ran 𝐹 ∧ 𝑌 ∈ ran 𝐺 ) → dom 𝑀 ∈ ∪ ran sigAlgebra )
19	12	sgsiga	⊢ ( 𝜑 → ( sigaGen ‘ 𝐽 ) ∈ ∪ ran sigAlgebra )
20	3 19	eqeltrid	⊢ ( 𝜑 → 𝑆 ∈ ∪ ran sigAlgebra )
21	20	3ad2ant1	⊢ ( ( 𝜑 ∧ 𝑋 ∈ ran 𝐹 ∧ 𝑌 ∈ ran 𝐺 ) → 𝑆 ∈ ∪ ran sigAlgebra )
22	1 2 3 4 5 6 7 8 9	sibfmbl	⊢ ( 𝜑 → 𝐹 ∈ ( dom 𝑀 MblFnM 𝑆 ) )
23	22	3ad2ant1	⊢ ( ( 𝜑 ∧ 𝑋 ∈ ran 𝐹 ∧ 𝑌 ∈ ran 𝐺 ) → 𝐹 ∈ ( dom 𝑀 MblFnM 𝑆 ) )
24	2	tpstop	⊢ ( 𝑊 ∈ TopSp → 𝐽 ∈ Top )
25		cldssbrsiga	⊢ ( 𝐽 ∈ Top → ( Clsd ‘ 𝐽 ) ⊆ ( sigaGen ‘ 𝐽 ) )
26	11 24 25	3syl	⊢ ( 𝜑 → ( Clsd ‘ 𝐽 ) ⊆ ( sigaGen ‘ 𝐽 ) )
27	26 3	sseqtrrdi	⊢ ( 𝜑 → ( Clsd ‘ 𝐽 ) ⊆ 𝑆 )
28	27	3ad2ant1	⊢ ( ( 𝜑 ∧ 𝑋 ∈ ran 𝐹 ∧ 𝑌 ∈ ran 𝐺 ) → ( Clsd ‘ 𝐽 ) ⊆ 𝑆 )
29	12	3ad2ant1	⊢ ( ( 𝜑 ∧ 𝑋 ∈ ran 𝐹 ∧ 𝑌 ∈ ran 𝐺 ) → 𝐽 ∈ Fre )
30	1 2 3 4 5 6 7 8 9	sibff	⊢ ( 𝜑 → 𝐹 : ∪ dom 𝑀 ⟶ ∪ 𝐽 )
31	30	frnd	⊢ ( 𝜑 → ran 𝐹 ⊆ ∪ 𝐽 )
32	31	3ad2ant1	⊢ ( ( 𝜑 ∧ 𝑋 ∈ ran 𝐹 ∧ 𝑌 ∈ ran 𝐺 ) → ran 𝐹 ⊆ ∪ 𝐽 )
33		simp2	⊢ ( ( 𝜑 ∧ 𝑋 ∈ ran 𝐹 ∧ 𝑌 ∈ ran 𝐺 ) → 𝑋 ∈ ran 𝐹 )
34	32 33	sseldd	⊢ ( ( 𝜑 ∧ 𝑋 ∈ ran 𝐹 ∧ 𝑌 ∈ ran 𝐺 ) → 𝑋 ∈ ∪ 𝐽 )
35		eqid	⊢ ∪ 𝐽 = ∪ 𝐽
36	35	t1sncld	⊢ ( ( 𝐽 ∈ Fre ∧ 𝑋 ∈ ∪ 𝐽 ) → { 𝑋 } ∈ ( Clsd ‘ 𝐽 ) )
37	29 34 36	syl2anc	⊢ ( ( 𝜑 ∧ 𝑋 ∈ ran 𝐹 ∧ 𝑌 ∈ ran 𝐺 ) → { 𝑋 } ∈ ( Clsd ‘ 𝐽 ) )
38	28 37	sseldd	⊢ ( ( 𝜑 ∧ 𝑋 ∈ ran 𝐹 ∧ 𝑌 ∈ ran 𝐺 ) → { 𝑋 } ∈ 𝑆 )
39	18 21 23 38	mbfmcnvima	⊢ ( ( 𝜑 ∧ 𝑋 ∈ ran 𝐹 ∧ 𝑌 ∈ ran 𝐺 ) → ( ^◡ 𝐹 “ { 𝑋 } ) ∈ dom 𝑀 )
40	1 2 3 4 5 6 7 8 10	sibfmbl	⊢ ( 𝜑 → 𝐺 ∈ ( dom 𝑀 MblFnM 𝑆 ) )
41	40	3ad2ant1	⊢ ( ( 𝜑 ∧ 𝑋 ∈ ran 𝐹 ∧ 𝑌 ∈ ran 𝐺 ) → 𝐺 ∈ ( dom 𝑀 MblFnM 𝑆 ) )
42	1 2 3 4 5 6 7 8 10	sibff	⊢ ( 𝜑 → 𝐺 : ∪ dom 𝑀 ⟶ ∪ 𝐽 )
43	42	frnd	⊢ ( 𝜑 → ran 𝐺 ⊆ ∪ 𝐽 )
44	43	3ad2ant1	⊢ ( ( 𝜑 ∧ 𝑋 ∈ ran 𝐹 ∧ 𝑌 ∈ ran 𝐺 ) → ran 𝐺 ⊆ ∪ 𝐽 )
45		simp3	⊢ ( ( 𝜑 ∧ 𝑋 ∈ ran 𝐹 ∧ 𝑌 ∈ ran 𝐺 ) → 𝑌 ∈ ran 𝐺 )
46	44 45	sseldd	⊢ ( ( 𝜑 ∧ 𝑋 ∈ ran 𝐹 ∧ 𝑌 ∈ ran 𝐺 ) → 𝑌 ∈ ∪ 𝐽 )
47	35	t1sncld	⊢ ( ( 𝐽 ∈ Fre ∧ 𝑌 ∈ ∪ 𝐽 ) → { 𝑌 } ∈ ( Clsd ‘ 𝐽 ) )
48	29 46 47	syl2anc	⊢ ( ( 𝜑 ∧ 𝑋 ∈ ran 𝐹 ∧ 𝑌 ∈ ran 𝐺 ) → { 𝑌 } ∈ ( Clsd ‘ 𝐽 ) )
49	28 48	sseldd	⊢ ( ( 𝜑 ∧ 𝑋 ∈ ran 𝐹 ∧ 𝑌 ∈ ran 𝐺 ) → { 𝑌 } ∈ 𝑆 )
50	18 21 41 49	mbfmcnvima	⊢ ( ( 𝜑 ∧ 𝑋 ∈ ran 𝐹 ∧ 𝑌 ∈ ran 𝐺 ) → ( ^◡ 𝐺 “ { 𝑌 } ) ∈ dom 𝑀 )
51		inelsiga	⊢ ( ( dom 𝑀 ∈ ∪ ran sigAlgebra ∧ ( ^◡ 𝐹 “ { 𝑋 } ) ∈ dom 𝑀 ∧ ( ^◡ 𝐺 “ { 𝑌 } ) ∈ dom 𝑀 ) → ( ( ^◡ 𝐹 “ { 𝑋 } ) ∩ ( ^◡ 𝐺 “ { 𝑌 } ) ) ∈ dom 𝑀 )
52	18 39 50 51	syl3anc	⊢ ( ( 𝜑 ∧ 𝑋 ∈ ran 𝐹 ∧ 𝑌 ∈ ran 𝐺 ) → ( ( ^◡ 𝐹 “ { 𝑋 } ) ∩ ( ^◡ 𝐺 “ { 𝑌 } ) ) ∈ dom 𝑀 )
53		measvxrge0	⊢ ( ( 𝑀 ∈ ( measures ‘ dom 𝑀 ) ∧ ( ( ^◡ 𝐹 “ { 𝑋 } ) ∩ ( ^◡ 𝐺 “ { 𝑌 } ) ) ∈ dom 𝑀 ) → ( 𝑀 ‘ ( ( ^◡ 𝐹 “ { 𝑋 } ) ∩ ( ^◡ 𝐺 “ { 𝑌 } ) ) ) ∈ ( 0 [,] +∞ ) )
54	15 52 53	syl2anc	⊢ ( ( 𝜑 ∧ 𝑋 ∈ ran 𝐹 ∧ 𝑌 ∈ ran 𝐺 ) → ( 𝑀 ‘ ( ( ^◡ 𝐹 “ { 𝑋 } ) ∩ ( ^◡ 𝐺 “ { 𝑌 } ) ) ) ∈ ( 0 [,] +∞ ) )
55		elxrge0	⊢ ( ( 𝑀 ‘ ( ( ^◡ 𝐹 “ { 𝑋 } ) ∩ ( ^◡ 𝐺 “ { 𝑌 } ) ) ) ∈ ( 0 [,] +∞ ) ↔ ( ( 𝑀 ‘ ( ( ^◡ 𝐹 “ { 𝑋 } ) ∩ ( ^◡ 𝐺 “ { 𝑌 } ) ) ) ∈ ℝ^* ∧ 0 ≤ ( 𝑀 ‘ ( ( ^◡ 𝐹 “ { 𝑋 } ) ∩ ( ^◡ 𝐺 “ { 𝑌 } ) ) ) ) )
56	55	simplbi	⊢ ( ( 𝑀 ‘ ( ( ^◡ 𝐹 “ { 𝑋 } ) ∩ ( ^◡ 𝐺 “ { 𝑌 } ) ) ) ∈ ( 0 [,] +∞ ) → ( 𝑀 ‘ ( ( ^◡ 𝐹 “ { 𝑋 } ) ∩ ( ^◡ 𝐺 “ { 𝑌 } ) ) ) ∈ ℝ^* )
57	54 56	syl	⊢ ( ( 𝜑 ∧ 𝑋 ∈ ran 𝐹 ∧ 𝑌 ∈ ran 𝐺 ) → ( 𝑀 ‘ ( ( ^◡ 𝐹 “ { 𝑋 } ) ∩ ( ^◡ 𝐺 “ { 𝑌 } ) ) ) ∈ ℝ^* )
58	57	adantr	⊢ ( ( ( 𝜑 ∧ 𝑋 ∈ ran 𝐹 ∧ 𝑌 ∈ ran 𝐺 ) ∧ ( 𝑋 ≠ 0 ∨ 𝑌 ≠ 0 ) ) → ( 𝑀 ‘ ( ( ^◡ 𝐹 “ { 𝑋 } ) ∩ ( ^◡ 𝐺 “ { 𝑌 } ) ) ) ∈ ℝ^* )
59		0re	⊢ 0 ∈ ℝ
60	59	a1i	⊢ ( ( ( 𝜑 ∧ 𝑋 ∈ ran 𝐹 ∧ 𝑌 ∈ ran 𝐺 ) ∧ ( 𝑋 ≠ 0 ∨ 𝑌 ≠ 0 ) ) → 0 ∈ ℝ )
61	55	simprbi	⊢ ( ( 𝑀 ‘ ( ( ^◡ 𝐹 “ { 𝑋 } ) ∩ ( ^◡ 𝐺 “ { 𝑌 } ) ) ) ∈ ( 0 [,] +∞ ) → 0 ≤ ( 𝑀 ‘ ( ( ^◡ 𝐹 “ { 𝑋 } ) ∩ ( ^◡ 𝐺 “ { 𝑌 } ) ) ) )
62	54 61	syl	⊢ ( ( 𝜑 ∧ 𝑋 ∈ ran 𝐹 ∧ 𝑌 ∈ ran 𝐺 ) → 0 ≤ ( 𝑀 ‘ ( ( ^◡ 𝐹 “ { 𝑋 } ) ∩ ( ^◡ 𝐺 “ { 𝑌 } ) ) ) )
63	62	adantr	⊢ ( ( ( 𝜑 ∧ 𝑋 ∈ ran 𝐹 ∧ 𝑌 ∈ ran 𝐺 ) ∧ ( 𝑋 ≠ 0 ∨ 𝑌 ≠ 0 ) ) → 0 ≤ ( 𝑀 ‘ ( ( ^◡ 𝐹 “ { 𝑋 } ) ∩ ( ^◡ 𝐺 “ { 𝑌 } ) ) ) )
64	57	adantr	⊢ ( ( ( 𝜑 ∧ 𝑋 ∈ ran 𝐹 ∧ 𝑌 ∈ ran 𝐺 ) ∧ 𝑋 ≠ 0 ) → ( 𝑀 ‘ ( ( ^◡ 𝐹 “ { 𝑋 } ) ∩ ( ^◡ 𝐺 “ { 𝑌 } ) ) ) ∈ ℝ^* )
65	15	adantr	⊢ ( ( ( 𝜑 ∧ 𝑋 ∈ ran 𝐹 ∧ 𝑌 ∈ ran 𝐺 ) ∧ 𝑋 ≠ 0 ) → 𝑀 ∈ ( measures ‘ dom 𝑀 ) )
66	39	adantr	⊢ ( ( ( 𝜑 ∧ 𝑋 ∈ ran 𝐹 ∧ 𝑌 ∈ ran 𝐺 ) ∧ 𝑋 ≠ 0 ) → ( ^◡ 𝐹 “ { 𝑋 } ) ∈ dom 𝑀 )
67		measvxrge0	⊢ ( ( 𝑀 ∈ ( measures ‘ dom 𝑀 ) ∧ ( ^◡ 𝐹 “ { 𝑋 } ) ∈ dom 𝑀 ) → ( 𝑀 ‘ ( ^◡ 𝐹 “ { 𝑋 } ) ) ∈ ( 0 [,] +∞ ) )
68	65 66 67	syl2anc	⊢ ( ( ( 𝜑 ∧ 𝑋 ∈ ran 𝐹 ∧ 𝑌 ∈ ran 𝐺 ) ∧ 𝑋 ≠ 0 ) → ( 𝑀 ‘ ( ^◡ 𝐹 “ { 𝑋 } ) ) ∈ ( 0 [,] +∞ ) )
69		elxrge0	⊢ ( ( 𝑀 ‘ ( ^◡ 𝐹 “ { 𝑋 } ) ) ∈ ( 0 [,] +∞ ) ↔ ( ( 𝑀 ‘ ( ^◡ 𝐹 “ { 𝑋 } ) ) ∈ ℝ^* ∧ 0 ≤ ( 𝑀 ‘ ( ^◡ 𝐹 “ { 𝑋 } ) ) ) )
70	69	simplbi	⊢ ( ( 𝑀 ‘ ( ^◡ 𝐹 “ { 𝑋 } ) ) ∈ ( 0 [,] +∞ ) → ( 𝑀 ‘ ( ^◡ 𝐹 “ { 𝑋 } ) ) ∈ ℝ^* )
71	68 70	syl	⊢ ( ( ( 𝜑 ∧ 𝑋 ∈ ran 𝐹 ∧ 𝑌 ∈ ran 𝐺 ) ∧ 𝑋 ≠ 0 ) → ( 𝑀 ‘ ( ^◡ 𝐹 “ { 𝑋 } ) ) ∈ ℝ^* )
72		pnfxr	⊢ +∞ ∈ ℝ^*
73	72	a1i	⊢ ( ( ( 𝜑 ∧ 𝑋 ∈ ran 𝐹 ∧ 𝑌 ∈ ran 𝐺 ) ∧ 𝑋 ≠ 0 ) → +∞ ∈ ℝ^* )
74	52	adantr	⊢ ( ( ( 𝜑 ∧ 𝑋 ∈ ran 𝐹 ∧ 𝑌 ∈ ran 𝐺 ) ∧ 𝑋 ≠ 0 ) → ( ( ^◡ 𝐹 “ { 𝑋 } ) ∩ ( ^◡ 𝐺 “ { 𝑌 } ) ) ∈ dom 𝑀 )
75		inss1	⊢ ( ( ^◡ 𝐹 “ { 𝑋 } ) ∩ ( ^◡ 𝐺 “ { 𝑌 } ) ) ⊆ ( ^◡ 𝐹 “ { 𝑋 } )
76	75	a1i	⊢ ( ( ( 𝜑 ∧ 𝑋 ∈ ran 𝐹 ∧ 𝑌 ∈ ran 𝐺 ) ∧ 𝑋 ≠ 0 ) → ( ( ^◡ 𝐹 “ { 𝑋 } ) ∩ ( ^◡ 𝐺 “ { 𝑌 } ) ) ⊆ ( ^◡ 𝐹 “ { 𝑋 } ) )
77	65 74 66 76	measssd	⊢ ( ( ( 𝜑 ∧ 𝑋 ∈ ran 𝐹 ∧ 𝑌 ∈ ran 𝐺 ) ∧ 𝑋 ≠ 0 ) → ( 𝑀 ‘ ( ( ^◡ 𝐹 “ { 𝑋 } ) ∩ ( ^◡ 𝐺 “ { 𝑌 } ) ) ) ≤ ( 𝑀 ‘ ( ^◡ 𝐹 “ { 𝑋 } ) ) )
78		simpl1	⊢ ( ( ( 𝜑 ∧ 𝑋 ∈ ran 𝐹 ∧ 𝑌 ∈ ran 𝐺 ) ∧ 𝑋 ≠ 0 ) → 𝜑 )
79	33	anim1i	⊢ ( ( ( 𝜑 ∧ 𝑋 ∈ ran 𝐹 ∧ 𝑌 ∈ ran 𝐺 ) ∧ 𝑋 ≠ 0 ) → ( 𝑋 ∈ ran 𝐹 ∧ 𝑋 ≠ 0 ) )
80		eldifsn	⊢ ( 𝑋 ∈ ( ran 𝐹 ∖ { 0 } ) ↔ ( 𝑋 ∈ ran 𝐹 ∧ 𝑋 ≠ 0 ) )
81	79 80	sylibr	⊢ ( ( ( 𝜑 ∧ 𝑋 ∈ ran 𝐹 ∧ 𝑌 ∈ ran 𝐺 ) ∧ 𝑋 ≠ 0 ) → 𝑋 ∈ ( ran 𝐹 ∖ { 0 } ) )
82	1 2 3 4 5 6 7 8 9	sibfima	⊢ ( ( 𝜑 ∧ 𝑋 ∈ ( ran 𝐹 ∖ { 0 } ) ) → ( 𝑀 ‘ ( ^◡ 𝐹 “ { 𝑋 } ) ) ∈ ( 0 [,) +∞ ) )
83	78 81 82	syl2anc	⊢ ( ( ( 𝜑 ∧ 𝑋 ∈ ran 𝐹 ∧ 𝑌 ∈ ran 𝐺 ) ∧ 𝑋 ≠ 0 ) → ( 𝑀 ‘ ( ^◡ 𝐹 “ { 𝑋 } ) ) ∈ ( 0 [,) +∞ ) )
84		elico2	⊢ ( ( 0 ∈ ℝ ∧ +∞ ∈ ℝ^* ) → ( ( 𝑀 ‘ ( ^◡ 𝐹 “ { 𝑋 } ) ) ∈ ( 0 [,) +∞ ) ↔ ( ( 𝑀 ‘ ( ^◡ 𝐹 “ { 𝑋 } ) ) ∈ ℝ ∧ 0 ≤ ( 𝑀 ‘ ( ^◡ 𝐹 “ { 𝑋 } ) ) ∧ ( 𝑀 ‘ ( ^◡ 𝐹 “ { 𝑋 } ) ) < +∞ ) ) )
85	59 72 84	mp2an	⊢ ( ( 𝑀 ‘ ( ^◡ 𝐹 “ { 𝑋 } ) ) ∈ ( 0 [,) +∞ ) ↔ ( ( 𝑀 ‘ ( ^◡ 𝐹 “ { 𝑋 } ) ) ∈ ℝ ∧ 0 ≤ ( 𝑀 ‘ ( ^◡ 𝐹 “ { 𝑋 } ) ) ∧ ( 𝑀 ‘ ( ^◡ 𝐹 “ { 𝑋 } ) ) < +∞ ) )
86	85	simp3bi	⊢ ( ( 𝑀 ‘ ( ^◡ 𝐹 “ { 𝑋 } ) ) ∈ ( 0 [,) +∞ ) → ( 𝑀 ‘ ( ^◡ 𝐹 “ { 𝑋 } ) ) < +∞ )
87	83 86	syl	⊢ ( ( ( 𝜑 ∧ 𝑋 ∈ ran 𝐹 ∧ 𝑌 ∈ ran 𝐺 ) ∧ 𝑋 ≠ 0 ) → ( 𝑀 ‘ ( ^◡ 𝐹 “ { 𝑋 } ) ) < +∞ )
88	64 71 73 77 87	xrlelttrd	⊢ ( ( ( 𝜑 ∧ 𝑋 ∈ ran 𝐹 ∧ 𝑌 ∈ ran 𝐺 ) ∧ 𝑋 ≠ 0 ) → ( 𝑀 ‘ ( ( ^◡ 𝐹 “ { 𝑋 } ) ∩ ( ^◡ 𝐺 “ { 𝑌 } ) ) ) < +∞ )
89	57	adantr	⊢ ( ( ( 𝜑 ∧ 𝑋 ∈ ran 𝐹 ∧ 𝑌 ∈ ran 𝐺 ) ∧ 𝑌 ≠ 0 ) → ( 𝑀 ‘ ( ( ^◡ 𝐹 “ { 𝑋 } ) ∩ ( ^◡ 𝐺 “ { 𝑌 } ) ) ) ∈ ℝ^* )
90	15	adantr	⊢ ( ( ( 𝜑 ∧ 𝑋 ∈ ran 𝐹 ∧ 𝑌 ∈ ran 𝐺 ) ∧ 𝑌 ≠ 0 ) → 𝑀 ∈ ( measures ‘ dom 𝑀 ) )
91	50	adantr	⊢ ( ( ( 𝜑 ∧ 𝑋 ∈ ran 𝐹 ∧ 𝑌 ∈ ran 𝐺 ) ∧ 𝑌 ≠ 0 ) → ( ^◡ 𝐺 “ { 𝑌 } ) ∈ dom 𝑀 )
92		measvxrge0	⊢ ( ( 𝑀 ∈ ( measures ‘ dom 𝑀 ) ∧ ( ^◡ 𝐺 “ { 𝑌 } ) ∈ dom 𝑀 ) → ( 𝑀 ‘ ( ^◡ 𝐺 “ { 𝑌 } ) ) ∈ ( 0 [,] +∞ ) )
93	90 91 92	syl2anc	⊢ ( ( ( 𝜑 ∧ 𝑋 ∈ ran 𝐹 ∧ 𝑌 ∈ ran 𝐺 ) ∧ 𝑌 ≠ 0 ) → ( 𝑀 ‘ ( ^◡ 𝐺 “ { 𝑌 } ) ) ∈ ( 0 [,] +∞ ) )
94		elxrge0	⊢ ( ( 𝑀 ‘ ( ^◡ 𝐺 “ { 𝑌 } ) ) ∈ ( 0 [,] +∞ ) ↔ ( ( 𝑀 ‘ ( ^◡ 𝐺 “ { 𝑌 } ) ) ∈ ℝ^* ∧ 0 ≤ ( 𝑀 ‘ ( ^◡ 𝐺 “ { 𝑌 } ) ) ) )
95	94	simplbi	⊢ ( ( 𝑀 ‘ ( ^◡ 𝐺 “ { 𝑌 } ) ) ∈ ( 0 [,] +∞ ) → ( 𝑀 ‘ ( ^◡ 𝐺 “ { 𝑌 } ) ) ∈ ℝ^* )
96	93 95	syl	⊢ ( ( ( 𝜑 ∧ 𝑋 ∈ ran 𝐹 ∧ 𝑌 ∈ ran 𝐺 ) ∧ 𝑌 ≠ 0 ) → ( 𝑀 ‘ ( ^◡ 𝐺 “ { 𝑌 } ) ) ∈ ℝ^* )
97	72	a1i	⊢ ( ( ( 𝜑 ∧ 𝑋 ∈ ran 𝐹 ∧ 𝑌 ∈ ran 𝐺 ) ∧ 𝑌 ≠ 0 ) → +∞ ∈ ℝ^* )
98	52	adantr	⊢ ( ( ( 𝜑 ∧ 𝑋 ∈ ran 𝐹 ∧ 𝑌 ∈ ran 𝐺 ) ∧ 𝑌 ≠ 0 ) → ( ( ^◡ 𝐹 “ { 𝑋 } ) ∩ ( ^◡ 𝐺 “ { 𝑌 } ) ) ∈ dom 𝑀 )
99		inss2	⊢ ( ( ^◡ 𝐹 “ { 𝑋 } ) ∩ ( ^◡ 𝐺 “ { 𝑌 } ) ) ⊆ ( ^◡ 𝐺 “ { 𝑌 } )
100	99	a1i	⊢ ( ( ( 𝜑 ∧ 𝑋 ∈ ran 𝐹 ∧ 𝑌 ∈ ran 𝐺 ) ∧ 𝑌 ≠ 0 ) → ( ( ^◡ 𝐹 “ { 𝑋 } ) ∩ ( ^◡ 𝐺 “ { 𝑌 } ) ) ⊆ ( ^◡ 𝐺 “ { 𝑌 } ) )
101	90 98 91 100	measssd	⊢ ( ( ( 𝜑 ∧ 𝑋 ∈ ran 𝐹 ∧ 𝑌 ∈ ran 𝐺 ) ∧ 𝑌 ≠ 0 ) → ( 𝑀 ‘ ( ( ^◡ 𝐹 “ { 𝑋 } ) ∩ ( ^◡ 𝐺 “ { 𝑌 } ) ) ) ≤ ( 𝑀 ‘ ( ^◡ 𝐺 “ { 𝑌 } ) ) )
102		simpl1	⊢ ( ( ( 𝜑 ∧ 𝑋 ∈ ran 𝐹 ∧ 𝑌 ∈ ran 𝐺 ) ∧ 𝑌 ≠ 0 ) → 𝜑 )
103	45	anim1i	⊢ ( ( ( 𝜑 ∧ 𝑋 ∈ ran 𝐹 ∧ 𝑌 ∈ ran 𝐺 ) ∧ 𝑌 ≠ 0 ) → ( 𝑌 ∈ ran 𝐺 ∧ 𝑌 ≠ 0 ) )
104		eldifsn	⊢ ( 𝑌 ∈ ( ran 𝐺 ∖ { 0 } ) ↔ ( 𝑌 ∈ ran 𝐺 ∧ 𝑌 ≠ 0 ) )
105	103 104	sylibr	⊢ ( ( ( 𝜑 ∧ 𝑋 ∈ ran 𝐹 ∧ 𝑌 ∈ ran 𝐺 ) ∧ 𝑌 ≠ 0 ) → 𝑌 ∈ ( ran 𝐺 ∖ { 0 } ) )
106	1 2 3 4 5 6 7 8 10	sibfima	⊢ ( ( 𝜑 ∧ 𝑌 ∈ ( ran 𝐺 ∖ { 0 } ) ) → ( 𝑀 ‘ ( ^◡ 𝐺 “ { 𝑌 } ) ) ∈ ( 0 [,) +∞ ) )
107	102 105 106	syl2anc	⊢ ( ( ( 𝜑 ∧ 𝑋 ∈ ran 𝐹 ∧ 𝑌 ∈ ran 𝐺 ) ∧ 𝑌 ≠ 0 ) → ( 𝑀 ‘ ( ^◡ 𝐺 “ { 𝑌 } ) ) ∈ ( 0 [,) +∞ ) )
108		elico2	⊢ ( ( 0 ∈ ℝ ∧ +∞ ∈ ℝ^* ) → ( ( 𝑀 ‘ ( ^◡ 𝐺 “ { 𝑌 } ) ) ∈ ( 0 [,) +∞ ) ↔ ( ( 𝑀 ‘ ( ^◡ 𝐺 “ { 𝑌 } ) ) ∈ ℝ ∧ 0 ≤ ( 𝑀 ‘ ( ^◡ 𝐺 “ { 𝑌 } ) ) ∧ ( 𝑀 ‘ ( ^◡ 𝐺 “ { 𝑌 } ) ) < +∞ ) ) )
109	59 72 108	mp2an	⊢ ( ( 𝑀 ‘ ( ^◡ 𝐺 “ { 𝑌 } ) ) ∈ ( 0 [,) +∞ ) ↔ ( ( 𝑀 ‘ ( ^◡ 𝐺 “ { 𝑌 } ) ) ∈ ℝ ∧ 0 ≤ ( 𝑀 ‘ ( ^◡ 𝐺 “ { 𝑌 } ) ) ∧ ( 𝑀 ‘ ( ^◡ 𝐺 “ { 𝑌 } ) ) < +∞ ) )
110	109	simp3bi	⊢ ( ( 𝑀 ‘ ( ^◡ 𝐺 “ { 𝑌 } ) ) ∈ ( 0 [,) +∞ ) → ( 𝑀 ‘ ( ^◡ 𝐺 “ { 𝑌 } ) ) < +∞ )
111	107 110	syl	⊢ ( ( ( 𝜑 ∧ 𝑋 ∈ ran 𝐹 ∧ 𝑌 ∈ ran 𝐺 ) ∧ 𝑌 ≠ 0 ) → ( 𝑀 ‘ ( ^◡ 𝐺 “ { 𝑌 } ) ) < +∞ )
112	89 96 97 101 111	xrlelttrd	⊢ ( ( ( 𝜑 ∧ 𝑋 ∈ ran 𝐹 ∧ 𝑌 ∈ ran 𝐺 ) ∧ 𝑌 ≠ 0 ) → ( 𝑀 ‘ ( ( ^◡ 𝐹 “ { 𝑋 } ) ∩ ( ^◡ 𝐺 “ { 𝑌 } ) ) ) < +∞ )
113	88 112	jaodan	⊢ ( ( ( 𝜑 ∧ 𝑋 ∈ ran 𝐹 ∧ 𝑌 ∈ ran 𝐺 ) ∧ ( 𝑋 ≠ 0 ∨ 𝑌 ≠ 0 ) ) → ( 𝑀 ‘ ( ( ^◡ 𝐹 “ { 𝑋 } ) ∩ ( ^◡ 𝐺 “ { 𝑌 } ) ) ) < +∞ )
114		xrre3	⊢ ( ( ( ( 𝑀 ‘ ( ( ^◡ 𝐹 “ { 𝑋 } ) ∩ ( ^◡ 𝐺 “ { 𝑌 } ) ) ) ∈ ℝ^* ∧ 0 ∈ ℝ ) ∧ ( 0 ≤ ( 𝑀 ‘ ( ( ^◡ 𝐹 “ { 𝑋 } ) ∩ ( ^◡ 𝐺 “ { 𝑌 } ) ) ) ∧ ( 𝑀 ‘ ( ( ^◡ 𝐹 “ { 𝑋 } ) ∩ ( ^◡ 𝐺 “ { 𝑌 } ) ) ) < +∞ ) ) → ( 𝑀 ‘ ( ( ^◡ 𝐹 “ { 𝑋 } ) ∩ ( ^◡ 𝐺 “ { 𝑌 } ) ) ) ∈ ℝ )
115	58 60 63 113 114	syl22anc	⊢ ( ( ( 𝜑 ∧ 𝑋 ∈ ran 𝐹 ∧ 𝑌 ∈ ran 𝐺 ) ∧ ( 𝑋 ≠ 0 ∨ 𝑌 ≠ 0 ) ) → ( 𝑀 ‘ ( ( ^◡ 𝐹 “ { 𝑋 } ) ∩ ( ^◡ 𝐺 “ { 𝑌 } ) ) ) ∈ ℝ )
116		elico2	⊢ ( ( 0 ∈ ℝ ∧ +∞ ∈ ℝ^* ) → ( ( 𝑀 ‘ ( ( ^◡ 𝐹 “ { 𝑋 } ) ∩ ( ^◡ 𝐺 “ { 𝑌 } ) ) ) ∈ ( 0 [,) +∞ ) ↔ ( ( 𝑀 ‘ ( ( ^◡ 𝐹 “ { 𝑋 } ) ∩ ( ^◡ 𝐺 “ { 𝑌 } ) ) ) ∈ ℝ ∧ 0 ≤ ( 𝑀 ‘ ( ( ^◡ 𝐹 “ { 𝑋 } ) ∩ ( ^◡ 𝐺 “ { 𝑌 } ) ) ) ∧ ( 𝑀 ‘ ( ( ^◡ 𝐹 “ { 𝑋 } ) ∩ ( ^◡ 𝐺 “ { 𝑌 } ) ) ) < +∞ ) ) )
117	59 72 116	mp2an	⊢ ( ( 𝑀 ‘ ( ( ^◡ 𝐹 “ { 𝑋 } ) ∩ ( ^◡ 𝐺 “ { 𝑌 } ) ) ) ∈ ( 0 [,) +∞ ) ↔ ( ( 𝑀 ‘ ( ( ^◡ 𝐹 “ { 𝑋 } ) ∩ ( ^◡ 𝐺 “ { 𝑌 } ) ) ) ∈ ℝ ∧ 0 ≤ ( 𝑀 ‘ ( ( ^◡ 𝐹 “ { 𝑋 } ) ∩ ( ^◡ 𝐺 “ { 𝑌 } ) ) ) ∧ ( 𝑀 ‘ ( ( ^◡ 𝐹 “ { 𝑋 } ) ∩ ( ^◡ 𝐺 “ { 𝑌 } ) ) ) < +∞ ) )
118	115 63 113 117	syl3anbrc	⊢ ( ( ( 𝜑 ∧ 𝑋 ∈ ran 𝐹 ∧ 𝑌 ∈ ran 𝐺 ) ∧ ( 𝑋 ≠ 0 ∨ 𝑌 ≠ 0 ) ) → ( 𝑀 ‘ ( ( ^◡ 𝐹 “ { 𝑋 } ) ∩ ( ^◡ 𝐺 “ { 𝑌 } ) ) ) ∈ ( 0 [,) +∞ ) )

Metamath Proof Explorer

Theorem sibfinima

Proof