Users' Mathboxes Mathbox for Thierry Arnoux < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  sibfof Structured version   Visualization version   GIF version

Theorem sibfof 33327
Description: Applying function operations on simple functions results in simple functions with regard to the destination space, provided the operation fulfills a simple condition. (Contributed by Thierry Arnoux, 12-Mar-2018.)
Hypotheses
Ref Expression
sitgval.b 𝐡 = (Baseβ€˜π‘Š)
sitgval.j 𝐽 = (TopOpenβ€˜π‘Š)
sitgval.s 𝑆 = (sigaGenβ€˜π½)
sitgval.0 0 = (0gβ€˜π‘Š)
sitgval.x Β· = ( ·𝑠 β€˜π‘Š)
sitgval.h 𝐻 = (ℝHomβ€˜(Scalarβ€˜π‘Š))
sitgval.1 (πœ‘ β†’ π‘Š ∈ 𝑉)
sitgval.2 (πœ‘ β†’ 𝑀 ∈ βˆͺ ran measures)
sibfmbl.1 (πœ‘ β†’ 𝐹 ∈ dom (π‘Šsitg𝑀))
sibfof.c 𝐢 = (Baseβ€˜πΎ)
sibfof.0 (πœ‘ β†’ π‘Š ∈ TopSp)
sibfof.1 (πœ‘ β†’ + :(𝐡 Γ— 𝐡)⟢𝐢)
sibfof.2 (πœ‘ β†’ 𝐺 ∈ dom (π‘Šsitg𝑀))
sibfof.3 (πœ‘ β†’ 𝐾 ∈ TopSp)
sibfof.4 (πœ‘ β†’ 𝐽 ∈ Fre)
sibfof.5 (πœ‘ β†’ ( 0 + 0 ) = (0gβ€˜πΎ))
Assertion
Ref Expression
sibfof (πœ‘ β†’ (𝐹 ∘f + 𝐺) ∈ dom (𝐾sitg𝑀))

Proof of Theorem sibfof
Dummy variables π‘₯ 𝑦 𝑧 𝑝 𝑏 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 sibfof.1 . . . . . . . 8 (πœ‘ β†’ + :(𝐡 Γ— 𝐡)⟢𝐢)
2 sibfof.0 . . . . . . . . . . 11 (πœ‘ β†’ π‘Š ∈ TopSp)
3 sitgval.b . . . . . . . . . . . 12 𝐡 = (Baseβ€˜π‘Š)
4 sitgval.j . . . . . . . . . . . 12 𝐽 = (TopOpenβ€˜π‘Š)
53, 4tpsuni 22429 . . . . . . . . . . 11 (π‘Š ∈ TopSp β†’ 𝐡 = βˆͺ 𝐽)
62, 5syl 17 . . . . . . . . . 10 (πœ‘ β†’ 𝐡 = βˆͺ 𝐽)
76sqxpeqd 5707 . . . . . . . . 9 (πœ‘ β†’ (𝐡 Γ— 𝐡) = (βˆͺ 𝐽 Γ— βˆͺ 𝐽))
87feq2d 6700 . . . . . . . 8 (πœ‘ β†’ ( + :(𝐡 Γ— 𝐡)⟢𝐢 ↔ + :(βˆͺ 𝐽 Γ— βˆͺ 𝐽)⟢𝐢))
91, 8mpbid 231 . . . . . . 7 (πœ‘ β†’ + :(βˆͺ 𝐽 Γ— βˆͺ 𝐽)⟢𝐢)
109fovcdmda 7574 . . . . . 6 ((πœ‘ ∧ (𝑧 ∈ βˆͺ 𝐽 ∧ π‘₯ ∈ βˆͺ 𝐽)) β†’ (𝑧 + π‘₯) ∈ 𝐢)
11 sitgval.s . . . . . . 7 𝑆 = (sigaGenβ€˜π½)
12 sitgval.0 . . . . . . 7 0 = (0gβ€˜π‘Š)
13 sitgval.x . . . . . . 7 Β· = ( ·𝑠 β€˜π‘Š)
14 sitgval.h . . . . . . 7 𝐻 = (ℝHomβ€˜(Scalarβ€˜π‘Š))
15 sitgval.1 . . . . . . 7 (πœ‘ β†’ π‘Š ∈ 𝑉)
16 sitgval.2 . . . . . . 7 (πœ‘ β†’ 𝑀 ∈ βˆͺ ran measures)
17 sibfmbl.1 . . . . . . 7 (πœ‘ β†’ 𝐹 ∈ dom (π‘Šsitg𝑀))
183, 4, 11, 12, 13, 14, 15, 16, 17sibff 33323 . . . . . 6 (πœ‘ β†’ 𝐹:βˆͺ dom π‘€βŸΆβˆͺ 𝐽)
19 sibfof.2 . . . . . . 7 (πœ‘ β†’ 𝐺 ∈ dom (π‘Šsitg𝑀))
203, 4, 11, 12, 13, 14, 15, 16, 19sibff 33323 . . . . . 6 (πœ‘ β†’ 𝐺:βˆͺ dom π‘€βŸΆβˆͺ 𝐽)
21 dmexg 7890 . . . . . . 7 (𝑀 ∈ βˆͺ ran measures β†’ dom 𝑀 ∈ V)
22 uniexg 7726 . . . . . . 7 (dom 𝑀 ∈ V β†’ βˆͺ dom 𝑀 ∈ V)
2316, 21, 223syl 18 . . . . . 6 (πœ‘ β†’ βˆͺ dom 𝑀 ∈ V)
24 inidm 4217 . . . . . 6 (βˆͺ dom 𝑀 ∩ βˆͺ dom 𝑀) = βˆͺ dom 𝑀
2510, 18, 20, 23, 23, 24off 7684 . . . . 5 (πœ‘ β†’ (𝐹 ∘f + 𝐺):βˆͺ dom π‘€βŸΆπΆ)
26 sibfof.3 . . . . . . . 8 (πœ‘ β†’ 𝐾 ∈ TopSp)
27 sibfof.c . . . . . . . . 9 𝐢 = (Baseβ€˜πΎ)
28 eqid 2732 . . . . . . . . 9 (TopOpenβ€˜πΎ) = (TopOpenβ€˜πΎ)
2927, 28tpsuni 22429 . . . . . . . 8 (𝐾 ∈ TopSp β†’ 𝐢 = βˆͺ (TopOpenβ€˜πΎ))
3026, 29syl 17 . . . . . . 7 (πœ‘ β†’ 𝐢 = βˆͺ (TopOpenβ€˜πΎ))
31 fvex 6901 . . . . . . . 8 (TopOpenβ€˜πΎ) ∈ V
32 unisg 33129 . . . . . . . 8 ((TopOpenβ€˜πΎ) ∈ V β†’ βˆͺ (sigaGenβ€˜(TopOpenβ€˜πΎ)) = βˆͺ (TopOpenβ€˜πΎ))
3331, 32ax-mp 5 . . . . . . 7 βˆͺ (sigaGenβ€˜(TopOpenβ€˜πΎ)) = βˆͺ (TopOpenβ€˜πΎ)
3430, 33eqtr4di 2790 . . . . . 6 (πœ‘ β†’ 𝐢 = βˆͺ (sigaGenβ€˜(TopOpenβ€˜πΎ)))
3534feq3d 6701 . . . . 5 (πœ‘ β†’ ((𝐹 ∘f + 𝐺):βˆͺ dom π‘€βŸΆπΆ ↔ (𝐹 ∘f + 𝐺):βˆͺ dom π‘€βŸΆβˆͺ (sigaGenβ€˜(TopOpenβ€˜πΎ))))
3625, 35mpbid 231 . . . 4 (πœ‘ β†’ (𝐹 ∘f + 𝐺):βˆͺ dom π‘€βŸΆβˆͺ (sigaGenβ€˜(TopOpenβ€˜πΎ)))
3731a1i 11 . . . . . . 7 (πœ‘ β†’ (TopOpenβ€˜πΎ) ∈ V)
3837sgsiga 33128 . . . . . 6 (πœ‘ β†’ (sigaGenβ€˜(TopOpenβ€˜πΎ)) ∈ βˆͺ ran sigAlgebra)
3938uniexd 7728 . . . . 5 (πœ‘ β†’ βˆͺ (sigaGenβ€˜(TopOpenβ€˜πΎ)) ∈ V)
4039, 23elmapd 8830 . . . 4 (πœ‘ β†’ ((𝐹 ∘f + 𝐺) ∈ (βˆͺ (sigaGenβ€˜(TopOpenβ€˜πΎ)) ↑m βˆͺ dom 𝑀) ↔ (𝐹 ∘f + 𝐺):βˆͺ dom π‘€βŸΆβˆͺ (sigaGenβ€˜(TopOpenβ€˜πΎ))))
4136, 40mpbird 256 . . 3 (πœ‘ β†’ (𝐹 ∘f + 𝐺) ∈ (βˆͺ (sigaGenβ€˜(TopOpenβ€˜πΎ)) ↑m βˆͺ dom 𝑀))
42 inundif 4477 . . . . . . 7 ((𝑏 ∩ ran (𝐹 ∘f + 𝐺)) βˆͺ (𝑏 βˆ– ran (𝐹 ∘f + 𝐺))) = 𝑏
4342imaeq2i 6055 . . . . . 6 (β—‘(𝐹 ∘f + 𝐺) β€œ ((𝑏 ∩ ran (𝐹 ∘f + 𝐺)) βˆͺ (𝑏 βˆ– ran (𝐹 ∘f + 𝐺)))) = (β—‘(𝐹 ∘f + 𝐺) β€œ 𝑏)
44 ffun 6717 . . . . . . . 8 ((𝐹 ∘f + 𝐺):βˆͺ dom π‘€βŸΆπΆ β†’ Fun (𝐹 ∘f + 𝐺))
45 unpreima 7061 . . . . . . . 8 (Fun (𝐹 ∘f + 𝐺) β†’ (β—‘(𝐹 ∘f + 𝐺) β€œ ((𝑏 ∩ ran (𝐹 ∘f + 𝐺)) βˆͺ (𝑏 βˆ– ran (𝐹 ∘f + 𝐺)))) = ((β—‘(𝐹 ∘f + 𝐺) β€œ (𝑏 ∩ ran (𝐹 ∘f + 𝐺))) βˆͺ (β—‘(𝐹 ∘f + 𝐺) β€œ (𝑏 βˆ– ran (𝐹 ∘f + 𝐺)))))
4625, 44, 453syl 18 . . . . . . 7 (πœ‘ β†’ (β—‘(𝐹 ∘f + 𝐺) β€œ ((𝑏 ∩ ran (𝐹 ∘f + 𝐺)) βˆͺ (𝑏 βˆ– ran (𝐹 ∘f + 𝐺)))) = ((β—‘(𝐹 ∘f + 𝐺) β€œ (𝑏 ∩ ran (𝐹 ∘f + 𝐺))) βˆͺ (β—‘(𝐹 ∘f + 𝐺) β€œ (𝑏 βˆ– ran (𝐹 ∘f + 𝐺)))))
4746adantr 481 . . . . . 6 ((πœ‘ ∧ 𝑏 ∈ (sigaGenβ€˜(TopOpenβ€˜πΎ))) β†’ (β—‘(𝐹 ∘f + 𝐺) β€œ ((𝑏 ∩ ran (𝐹 ∘f + 𝐺)) βˆͺ (𝑏 βˆ– ran (𝐹 ∘f + 𝐺)))) = ((β—‘(𝐹 ∘f + 𝐺) β€œ (𝑏 ∩ ran (𝐹 ∘f + 𝐺))) βˆͺ (β—‘(𝐹 ∘f + 𝐺) β€œ (𝑏 βˆ– ran (𝐹 ∘f + 𝐺)))))
4843, 47eqtr3id 2786 . . . . 5 ((πœ‘ ∧ 𝑏 ∈ (sigaGenβ€˜(TopOpenβ€˜πΎ))) β†’ (β—‘(𝐹 ∘f + 𝐺) β€œ 𝑏) = ((β—‘(𝐹 ∘f + 𝐺) β€œ (𝑏 ∩ ran (𝐹 ∘f + 𝐺))) βˆͺ (β—‘(𝐹 ∘f + 𝐺) β€œ (𝑏 βˆ– ran (𝐹 ∘f + 𝐺)))))
49 dmmeas 33187 . . . . . . . 8 (𝑀 ∈ βˆͺ ran measures β†’ dom 𝑀 ∈ βˆͺ ran sigAlgebra)
5016, 49syl 17 . . . . . . 7 (πœ‘ β†’ dom 𝑀 ∈ βˆͺ ran sigAlgebra)
5150adantr 481 . . . . . 6 ((πœ‘ ∧ 𝑏 ∈ (sigaGenβ€˜(TopOpenβ€˜πΎ))) β†’ dom 𝑀 ∈ βˆͺ ran sigAlgebra)
52 imaiun 7240 . . . . . . . 8 (β—‘(𝐹 ∘f + 𝐺) β€œ βˆͺ 𝑧 ∈ (𝑏 ∩ ran (𝐹 ∘f + 𝐺)){𝑧}) = βˆͺ 𝑧 ∈ (𝑏 ∩ ran (𝐹 ∘f + 𝐺))(β—‘(𝐹 ∘f + 𝐺) β€œ {𝑧})
53 iunid 5062 . . . . . . . . 9 βˆͺ 𝑧 ∈ (𝑏 ∩ ran (𝐹 ∘f + 𝐺)){𝑧} = (𝑏 ∩ ran (𝐹 ∘f + 𝐺))
5453imaeq2i 6055 . . . . . . . 8 (β—‘(𝐹 ∘f + 𝐺) β€œ βˆͺ 𝑧 ∈ (𝑏 ∩ ran (𝐹 ∘f + 𝐺)){𝑧}) = (β—‘(𝐹 ∘f + 𝐺) β€œ (𝑏 ∩ ran (𝐹 ∘f + 𝐺)))
5552, 54eqtr3i 2762 . . . . . . 7 βˆͺ 𝑧 ∈ (𝑏 ∩ ran (𝐹 ∘f + 𝐺))(β—‘(𝐹 ∘f + 𝐺) β€œ {𝑧}) = (β—‘(𝐹 ∘f + 𝐺) β€œ (𝑏 ∩ ran (𝐹 ∘f + 𝐺)))
56 inss2 4228 . . . . . . . . . 10 (𝑏 ∩ ran (𝐹 ∘f + 𝐺)) βŠ† ran (𝐹 ∘f + 𝐺)
576feq3d 6701 . . . . . . . . . . . . . . 15 (πœ‘ β†’ (𝐹:βˆͺ dom π‘€βŸΆπ΅ ↔ 𝐹:βˆͺ dom π‘€βŸΆβˆͺ 𝐽))
5818, 57mpbird 256 . . . . . . . . . . . . . 14 (πœ‘ β†’ 𝐹:βˆͺ dom π‘€βŸΆπ΅)
596feq3d 6701 . . . . . . . . . . . . . . 15 (πœ‘ β†’ (𝐺:βˆͺ dom π‘€βŸΆπ΅ ↔ 𝐺:βˆͺ dom π‘€βŸΆβˆͺ 𝐽))
6020, 59mpbird 256 . . . . . . . . . . . . . 14 (πœ‘ β†’ 𝐺:βˆͺ dom π‘€βŸΆπ΅)
611ffnd 6715 . . . . . . . . . . . . . 14 (πœ‘ β†’ + Fn (𝐡 Γ— 𝐡))
6258, 60, 23, 61ofpreima2 31878 . . . . . . . . . . . . 13 (πœ‘ β†’ (β—‘(𝐹 ∘f + 𝐺) β€œ {𝑧}) = βˆͺ 𝑝 ∈ ((β—‘ + β€œ {𝑧}) ∩ (ran 𝐹 Γ— ran 𝐺))((◑𝐹 β€œ {(1st β€˜π‘)}) ∩ (◑𝐺 β€œ {(2nd β€˜π‘)})))
6362adantr 481 . . . . . . . . . . . 12 ((πœ‘ ∧ 𝑧 ∈ ran (𝐹 ∘f + 𝐺)) β†’ (β—‘(𝐹 ∘f + 𝐺) β€œ {𝑧}) = βˆͺ 𝑝 ∈ ((β—‘ + β€œ {𝑧}) ∩ (ran 𝐹 Γ— ran 𝐺))((◑𝐹 β€œ {(1st β€˜π‘)}) ∩ (◑𝐺 β€œ {(2nd β€˜π‘)})))
6450adantr 481 . . . . . . . . . . . . 13 ((πœ‘ ∧ 𝑧 ∈ ran (𝐹 ∘f + 𝐺)) β†’ dom 𝑀 ∈ βˆͺ ran sigAlgebra)
6550ad2antrr 724 . . . . . . . . . . . . . . 15 (((πœ‘ ∧ 𝑧 ∈ ran (𝐹 ∘f + 𝐺)) ∧ 𝑝 ∈ ((β—‘ + β€œ {𝑧}) ∩ (ran 𝐹 Γ— ran 𝐺))) β†’ dom 𝑀 ∈ βˆͺ ran sigAlgebra)
66 simpll 765 . . . . . . . . . . . . . . . 16 (((πœ‘ ∧ 𝑧 ∈ ran (𝐹 ∘f + 𝐺)) ∧ 𝑝 ∈ ((β—‘ + β€œ {𝑧}) ∩ (ran 𝐹 Γ— ran 𝐺))) β†’ πœ‘)
67 inss1 4227 . . . . . . . . . . . . . . . . . 18 ((β—‘ + β€œ {𝑧}) ∩ (ran 𝐹 Γ— ran 𝐺)) βŠ† (β—‘ + β€œ {𝑧})
68 cnvimass 6077 . . . . . . . . . . . . . . . . . . . 20 (β—‘ + β€œ {𝑧}) βŠ† dom +
6968, 1fssdm 6734 . . . . . . . . . . . . . . . . . . 19 (πœ‘ β†’ (β—‘ + β€œ {𝑧}) βŠ† (𝐡 Γ— 𝐡))
7069adantr 481 . . . . . . . . . . . . . . . . . 18 ((πœ‘ ∧ 𝑧 ∈ ran (𝐹 ∘f + 𝐺)) β†’ (β—‘ + β€œ {𝑧}) βŠ† (𝐡 Γ— 𝐡))
7167, 70sstrid 3992 . . . . . . . . . . . . . . . . 17 ((πœ‘ ∧ 𝑧 ∈ ran (𝐹 ∘f + 𝐺)) β†’ ((β—‘ + β€œ {𝑧}) ∩ (ran 𝐹 Γ— ran 𝐺)) βŠ† (𝐡 Γ— 𝐡))
7271sselda 3981 . . . . . . . . . . . . . . . 16 (((πœ‘ ∧ 𝑧 ∈ ran (𝐹 ∘f + 𝐺)) ∧ 𝑝 ∈ ((β—‘ + β€œ {𝑧}) ∩ (ran 𝐹 Γ— ran 𝐺))) β†’ 𝑝 ∈ (𝐡 Γ— 𝐡))
7350adantr 481 . . . . . . . . . . . . . . . . 17 ((πœ‘ ∧ 𝑝 ∈ (𝐡 Γ— 𝐡)) β†’ dom 𝑀 ∈ βˆͺ ran sigAlgebra)
74 sibfof.4 . . . . . . . . . . . . . . . . . . . 20 (πœ‘ β†’ 𝐽 ∈ Fre)
7574sgsiga 33128 . . . . . . . . . . . . . . . . . . 19 (πœ‘ β†’ (sigaGenβ€˜π½) ∈ βˆͺ ran sigAlgebra)
7611, 75eqeltrid 2837 . . . . . . . . . . . . . . . . . 18 (πœ‘ β†’ 𝑆 ∈ βˆͺ ran sigAlgebra)
7776adantr 481 . . . . . . . . . . . . . . . . 17 ((πœ‘ ∧ 𝑝 ∈ (𝐡 Γ— 𝐡)) β†’ 𝑆 ∈ βˆͺ ran sigAlgebra)
783, 4, 11, 12, 13, 14, 15, 16, 17sibfmbl 33322 . . . . . . . . . . . . . . . . . 18 (πœ‘ β†’ 𝐹 ∈ (dom 𝑀MblFnM𝑆))
7978adantr 481 . . . . . . . . . . . . . . . . 17 ((πœ‘ ∧ 𝑝 ∈ (𝐡 Γ— 𝐡)) β†’ 𝐹 ∈ (dom 𝑀MblFnM𝑆))
804tpstop 22430 . . . . . . . . . . . . . . . . . . . . 21 (π‘Š ∈ TopSp β†’ 𝐽 ∈ Top)
81 cldssbrsiga 33173 . . . . . . . . . . . . . . . . . . . . 21 (𝐽 ∈ Top β†’ (Clsdβ€˜π½) βŠ† (sigaGenβ€˜π½))
822, 80, 813syl 18 . . . . . . . . . . . . . . . . . . . 20 (πœ‘ β†’ (Clsdβ€˜π½) βŠ† (sigaGenβ€˜π½))
8382adantr 481 . . . . . . . . . . . . . . . . . . 19 ((πœ‘ ∧ 𝑝 ∈ (𝐡 Γ— 𝐡)) β†’ (Clsdβ€˜π½) βŠ† (sigaGenβ€˜π½))
8474adantr 481 . . . . . . . . . . . . . . . . . . . 20 ((πœ‘ ∧ 𝑝 ∈ (𝐡 Γ— 𝐡)) β†’ 𝐽 ∈ Fre)
85 xp1st 8003 . . . . . . . . . . . . . . . . . . . . . 22 (𝑝 ∈ (𝐡 Γ— 𝐡) β†’ (1st β€˜π‘) ∈ 𝐡)
8685adantl 482 . . . . . . . . . . . . . . . . . . . . 21 ((πœ‘ ∧ 𝑝 ∈ (𝐡 Γ— 𝐡)) β†’ (1st β€˜π‘) ∈ 𝐡)
876adantr 481 . . . . . . . . . . . . . . . . . . . . 21 ((πœ‘ ∧ 𝑝 ∈ (𝐡 Γ— 𝐡)) β†’ 𝐡 = βˆͺ 𝐽)
8886, 87eleqtrd 2835 . . . . . . . . . . . . . . . . . . . 20 ((πœ‘ ∧ 𝑝 ∈ (𝐡 Γ— 𝐡)) β†’ (1st β€˜π‘) ∈ βˆͺ 𝐽)
89 eqid 2732 . . . . . . . . . . . . . . . . . . . . 21 βˆͺ 𝐽 = βˆͺ 𝐽
9089t1sncld 22821 . . . . . . . . . . . . . . . . . . . 20 ((𝐽 ∈ Fre ∧ (1st β€˜π‘) ∈ βˆͺ 𝐽) β†’ {(1st β€˜π‘)} ∈ (Clsdβ€˜π½))
9184, 88, 90syl2anc 584 . . . . . . . . . . . . . . . . . . 19 ((πœ‘ ∧ 𝑝 ∈ (𝐡 Γ— 𝐡)) β†’ {(1st β€˜π‘)} ∈ (Clsdβ€˜π½))
9283, 91sseldd 3982 . . . . . . . . . . . . . . . . . 18 ((πœ‘ ∧ 𝑝 ∈ (𝐡 Γ— 𝐡)) β†’ {(1st β€˜π‘)} ∈ (sigaGenβ€˜π½))
9392, 11eleqtrrdi 2844 . . . . . . . . . . . . . . . . 17 ((πœ‘ ∧ 𝑝 ∈ (𝐡 Γ— 𝐡)) β†’ {(1st β€˜π‘)} ∈ 𝑆)
9473, 77, 79, 93mbfmcnvima 33242 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ 𝑝 ∈ (𝐡 Γ— 𝐡)) β†’ (◑𝐹 β€œ {(1st β€˜π‘)}) ∈ dom 𝑀)
9566, 72, 94syl2anc 584 . . . . . . . . . . . . . . 15 (((πœ‘ ∧ 𝑧 ∈ ran (𝐹 ∘f + 𝐺)) ∧ 𝑝 ∈ ((β—‘ + β€œ {𝑧}) ∩ (ran 𝐹 Γ— ran 𝐺))) β†’ (◑𝐹 β€œ {(1st β€˜π‘)}) ∈ dom 𝑀)
963, 4, 11, 12, 13, 14, 15, 16, 19sibfmbl 33322 . . . . . . . . . . . . . . . . . 18 (πœ‘ β†’ 𝐺 ∈ (dom 𝑀MblFnM𝑆))
9796adantr 481 . . . . . . . . . . . . . . . . 17 ((πœ‘ ∧ 𝑝 ∈ (𝐡 Γ— 𝐡)) β†’ 𝐺 ∈ (dom 𝑀MblFnM𝑆))
98 xp2nd 8004 . . . . . . . . . . . . . . . . . . . . . 22 (𝑝 ∈ (𝐡 Γ— 𝐡) β†’ (2nd β€˜π‘) ∈ 𝐡)
9998adantl 482 . . . . . . . . . . . . . . . . . . . . 21 ((πœ‘ ∧ 𝑝 ∈ (𝐡 Γ— 𝐡)) β†’ (2nd β€˜π‘) ∈ 𝐡)
10099, 87eleqtrd 2835 . . . . . . . . . . . . . . . . . . . 20 ((πœ‘ ∧ 𝑝 ∈ (𝐡 Γ— 𝐡)) β†’ (2nd β€˜π‘) ∈ βˆͺ 𝐽)
10189t1sncld 22821 . . . . . . . . . . . . . . . . . . . 20 ((𝐽 ∈ Fre ∧ (2nd β€˜π‘) ∈ βˆͺ 𝐽) β†’ {(2nd β€˜π‘)} ∈ (Clsdβ€˜π½))
10284, 100, 101syl2anc 584 . . . . . . . . . . . . . . . . . . 19 ((πœ‘ ∧ 𝑝 ∈ (𝐡 Γ— 𝐡)) β†’ {(2nd β€˜π‘)} ∈ (Clsdβ€˜π½))
10383, 102sseldd 3982 . . . . . . . . . . . . . . . . . 18 ((πœ‘ ∧ 𝑝 ∈ (𝐡 Γ— 𝐡)) β†’ {(2nd β€˜π‘)} ∈ (sigaGenβ€˜π½))
104103, 11eleqtrrdi 2844 . . . . . . . . . . . . . . . . 17 ((πœ‘ ∧ 𝑝 ∈ (𝐡 Γ— 𝐡)) β†’ {(2nd β€˜π‘)} ∈ 𝑆)
10573, 77, 97, 104mbfmcnvima 33242 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ 𝑝 ∈ (𝐡 Γ— 𝐡)) β†’ (◑𝐺 β€œ {(2nd β€˜π‘)}) ∈ dom 𝑀)
10666, 72, 105syl2anc 584 . . . . . . . . . . . . . . 15 (((πœ‘ ∧ 𝑧 ∈ ran (𝐹 ∘f + 𝐺)) ∧ 𝑝 ∈ ((β—‘ + β€œ {𝑧}) ∩ (ran 𝐹 Γ— ran 𝐺))) β†’ (◑𝐺 β€œ {(2nd β€˜π‘)}) ∈ dom 𝑀)
107 inelsiga 33121 . . . . . . . . . . . . . . 15 ((dom 𝑀 ∈ βˆͺ ran sigAlgebra ∧ (◑𝐹 β€œ {(1st β€˜π‘)}) ∈ dom 𝑀 ∧ (◑𝐺 β€œ {(2nd β€˜π‘)}) ∈ dom 𝑀) β†’ ((◑𝐹 β€œ {(1st β€˜π‘)}) ∩ (◑𝐺 β€œ {(2nd β€˜π‘)})) ∈ dom 𝑀)
10865, 95, 106, 107syl3anc 1371 . . . . . . . . . . . . . 14 (((πœ‘ ∧ 𝑧 ∈ ran (𝐹 ∘f + 𝐺)) ∧ 𝑝 ∈ ((β—‘ + β€œ {𝑧}) ∩ (ran 𝐹 Γ— ran 𝐺))) β†’ ((◑𝐹 β€œ {(1st β€˜π‘)}) ∩ (◑𝐺 β€œ {(2nd β€˜π‘)})) ∈ dom 𝑀)
109108ralrimiva 3146 . . . . . . . . . . . . 13 ((πœ‘ ∧ 𝑧 ∈ ran (𝐹 ∘f + 𝐺)) β†’ βˆ€π‘ ∈ ((β—‘ + β€œ {𝑧}) ∩ (ran 𝐹 Γ— ran 𝐺))((◑𝐹 β€œ {(1st β€˜π‘)}) ∩ (◑𝐺 β€œ {(2nd β€˜π‘)})) ∈ dom 𝑀)
1103, 4, 11, 12, 13, 14, 15, 16, 17sibfrn 33324 . . . . . . . . . . . . . . . . 17 (πœ‘ β†’ ran 𝐹 ∈ Fin)
1113, 4, 11, 12, 13, 14, 15, 16, 19sibfrn 33324 . . . . . . . . . . . . . . . . 17 (πœ‘ β†’ ran 𝐺 ∈ Fin)
112 xpfi 9313 . . . . . . . . . . . . . . . . 17 ((ran 𝐹 ∈ Fin ∧ ran 𝐺 ∈ Fin) β†’ (ran 𝐹 Γ— ran 𝐺) ∈ Fin)
113110, 111, 112syl2anc 584 . . . . . . . . . . . . . . . 16 (πœ‘ β†’ (ran 𝐹 Γ— ran 𝐺) ∈ Fin)
114 inss2 4228 . . . . . . . . . . . . . . . 16 ((β—‘ + β€œ {𝑧}) ∩ (ran 𝐹 Γ— ran 𝐺)) βŠ† (ran 𝐹 Γ— ran 𝐺)
115 ssdomg 8992 . . . . . . . . . . . . . . . 16 ((ran 𝐹 Γ— ran 𝐺) ∈ Fin β†’ (((β—‘ + β€œ {𝑧}) ∩ (ran 𝐹 Γ— ran 𝐺)) βŠ† (ran 𝐹 Γ— ran 𝐺) β†’ ((β—‘ + β€œ {𝑧}) ∩ (ran 𝐹 Γ— ran 𝐺)) β‰Ό (ran 𝐹 Γ— ran 𝐺)))
116113, 114, 115mpisyl 21 . . . . . . . . . . . . . . 15 (πœ‘ β†’ ((β—‘ + β€œ {𝑧}) ∩ (ran 𝐹 Γ— ran 𝐺)) β‰Ό (ran 𝐹 Γ— ran 𝐺))
117 isfinite 9643 . . . . . . . . . . . . . . . . 17 ((ran 𝐹 Γ— ran 𝐺) ∈ Fin ↔ (ran 𝐹 Γ— ran 𝐺) β‰Ί Ο‰)
118117biimpi 215 . . . . . . . . . . . . . . . 16 ((ran 𝐹 Γ— ran 𝐺) ∈ Fin β†’ (ran 𝐹 Γ— ran 𝐺) β‰Ί Ο‰)
119 sdomdom 8972 . . . . . . . . . . . . . . . 16 ((ran 𝐹 Γ— ran 𝐺) β‰Ί Ο‰ β†’ (ran 𝐹 Γ— ran 𝐺) β‰Ό Ο‰)
120113, 118, 1193syl 18 . . . . . . . . . . . . . . 15 (πœ‘ β†’ (ran 𝐹 Γ— ran 𝐺) β‰Ό Ο‰)
121 domtr 8999 . . . . . . . . . . . . . . 15 ((((β—‘ + β€œ {𝑧}) ∩ (ran 𝐹 Γ— ran 𝐺)) β‰Ό (ran 𝐹 Γ— ran 𝐺) ∧ (ran 𝐹 Γ— ran 𝐺) β‰Ό Ο‰) β†’ ((β—‘ + β€œ {𝑧}) ∩ (ran 𝐹 Γ— ran 𝐺)) β‰Ό Ο‰)
122116, 120, 121syl2anc 584 . . . . . . . . . . . . . 14 (πœ‘ β†’ ((β—‘ + β€œ {𝑧}) ∩ (ran 𝐹 Γ— ran 𝐺)) β‰Ό Ο‰)
123122adantr 481 . . . . . . . . . . . . 13 ((πœ‘ ∧ 𝑧 ∈ ran (𝐹 ∘f + 𝐺)) β†’ ((β—‘ + β€œ {𝑧}) ∩ (ran 𝐹 Γ— ran 𝐺)) β‰Ό Ο‰)
124 nfcv 2903 . . . . . . . . . . . . . 14 Ⅎ𝑝((β—‘ + β€œ {𝑧}) ∩ (ran 𝐹 Γ— ran 𝐺))
125124sigaclcuni 33104 . . . . . . . . . . . . 13 ((dom 𝑀 ∈ βˆͺ ran sigAlgebra ∧ βˆ€π‘ ∈ ((β—‘ + β€œ {𝑧}) ∩ (ran 𝐹 Γ— ran 𝐺))((◑𝐹 β€œ {(1st β€˜π‘)}) ∩ (◑𝐺 β€œ {(2nd β€˜π‘)})) ∈ dom 𝑀 ∧ ((β—‘ + β€œ {𝑧}) ∩ (ran 𝐹 Γ— ran 𝐺)) β‰Ό Ο‰) β†’ βˆͺ 𝑝 ∈ ((β—‘ + β€œ {𝑧}) ∩ (ran 𝐹 Γ— ran 𝐺))((◑𝐹 β€œ {(1st β€˜π‘)}) ∩ (◑𝐺 β€œ {(2nd β€˜π‘)})) ∈ dom 𝑀)
12664, 109, 123, 125syl3anc 1371 . . . . . . . . . . . 12 ((πœ‘ ∧ 𝑧 ∈ ran (𝐹 ∘f + 𝐺)) β†’ βˆͺ 𝑝 ∈ ((β—‘ + β€œ {𝑧}) ∩ (ran 𝐹 Γ— ran 𝐺))((◑𝐹 β€œ {(1st β€˜π‘)}) ∩ (◑𝐺 β€œ {(2nd β€˜π‘)})) ∈ dom 𝑀)
12763, 126eqeltrd 2833 . . . . . . . . . . 11 ((πœ‘ ∧ 𝑧 ∈ ran (𝐹 ∘f + 𝐺)) β†’ (β—‘(𝐹 ∘f + 𝐺) β€œ {𝑧}) ∈ dom 𝑀)
128127ralrimiva 3146 . . . . . . . . . 10 (πœ‘ β†’ βˆ€π‘§ ∈ ran (𝐹 ∘f + 𝐺)(β—‘(𝐹 ∘f + 𝐺) β€œ {𝑧}) ∈ dom 𝑀)
129 ssralv 4049 . . . . . . . . . 10 ((𝑏 ∩ ran (𝐹 ∘f + 𝐺)) βŠ† ran (𝐹 ∘f + 𝐺) β†’ (βˆ€π‘§ ∈ ran (𝐹 ∘f + 𝐺)(β—‘(𝐹 ∘f + 𝐺) β€œ {𝑧}) ∈ dom 𝑀 β†’ βˆ€π‘§ ∈ (𝑏 ∩ ran (𝐹 ∘f + 𝐺))(β—‘(𝐹 ∘f + 𝐺) β€œ {𝑧}) ∈ dom 𝑀))
13056, 128, 129mpsyl 68 . . . . . . . . 9 (πœ‘ β†’ βˆ€π‘§ ∈ (𝑏 ∩ ran (𝐹 ∘f + 𝐺))(β—‘(𝐹 ∘f + 𝐺) β€œ {𝑧}) ∈ dom 𝑀)
131130adantr 481 . . . . . . . 8 ((πœ‘ ∧ 𝑏 ∈ (sigaGenβ€˜(TopOpenβ€˜πΎ))) β†’ βˆ€π‘§ ∈ (𝑏 ∩ ran (𝐹 ∘f + 𝐺))(β—‘(𝐹 ∘f + 𝐺) β€œ {𝑧}) ∈ dom 𝑀)
1321ffund 6718 . . . . . . . . . . . . 13 (πœ‘ β†’ Fun + )
133 imafi 9171 . . . . . . . . . . . . 13 ((Fun + ∧ (ran 𝐹 Γ— ran 𝐺) ∈ Fin) β†’ ( + β€œ (ran 𝐹 Γ— ran 𝐺)) ∈ Fin)
134132, 113, 133syl2anc 584 . . . . . . . . . . . 12 (πœ‘ β†’ ( + β€œ (ran 𝐹 Γ— ran 𝐺)) ∈ Fin)
13518, 20, 9, 23ofrn2 31852 . . . . . . . . . . . 12 (πœ‘ β†’ ran (𝐹 ∘f + 𝐺) βŠ† ( + β€œ (ran 𝐹 Γ— ran 𝐺)))
136 ssfi 9169 . . . . . . . . . . . 12 ((( + β€œ (ran 𝐹 Γ— ran 𝐺)) ∈ Fin ∧ ran (𝐹 ∘f + 𝐺) βŠ† ( + β€œ (ran 𝐹 Γ— ran 𝐺))) β†’ ran (𝐹 ∘f + 𝐺) ∈ Fin)
137134, 135, 136syl2anc 584 . . . . . . . . . . 11 (πœ‘ β†’ ran (𝐹 ∘f + 𝐺) ∈ Fin)
138 ssdomg 8992 . . . . . . . . . . 11 (ran (𝐹 ∘f + 𝐺) ∈ Fin β†’ ((𝑏 ∩ ran (𝐹 ∘f + 𝐺)) βŠ† ran (𝐹 ∘f + 𝐺) β†’ (𝑏 ∩ ran (𝐹 ∘f + 𝐺)) β‰Ό ran (𝐹 ∘f + 𝐺)))
139137, 56, 138mpisyl 21 . . . . . . . . . 10 (πœ‘ β†’ (𝑏 ∩ ran (𝐹 ∘f + 𝐺)) β‰Ό ran (𝐹 ∘f + 𝐺))
140 isfinite 9643 . . . . . . . . . . . 12 (ran (𝐹 ∘f + 𝐺) ∈ Fin ↔ ran (𝐹 ∘f + 𝐺) β‰Ί Ο‰)
141137, 140sylib 217 . . . . . . . . . . 11 (πœ‘ β†’ ran (𝐹 ∘f + 𝐺) β‰Ί Ο‰)
142 sdomdom 8972 . . . . . . . . . . 11 (ran (𝐹 ∘f + 𝐺) β‰Ί Ο‰ β†’ ran (𝐹 ∘f + 𝐺) β‰Ό Ο‰)
143141, 142syl 17 . . . . . . . . . 10 (πœ‘ β†’ ran (𝐹 ∘f + 𝐺) β‰Ό Ο‰)
144 domtr 8999 . . . . . . . . . 10 (((𝑏 ∩ ran (𝐹 ∘f + 𝐺)) β‰Ό ran (𝐹 ∘f + 𝐺) ∧ ran (𝐹 ∘f + 𝐺) β‰Ό Ο‰) β†’ (𝑏 ∩ ran (𝐹 ∘f + 𝐺)) β‰Ό Ο‰)
145139, 143, 144syl2anc 584 . . . . . . . . 9 (πœ‘ β†’ (𝑏 ∩ ran (𝐹 ∘f + 𝐺)) β‰Ό Ο‰)
146145adantr 481 . . . . . . . 8 ((πœ‘ ∧ 𝑏 ∈ (sigaGenβ€˜(TopOpenβ€˜πΎ))) β†’ (𝑏 ∩ ran (𝐹 ∘f + 𝐺)) β‰Ό Ο‰)
147 nfcv 2903 . . . . . . . . 9 Ⅎ𝑧(𝑏 ∩ ran (𝐹 ∘f + 𝐺))
148147sigaclcuni 33104 . . . . . . . 8 ((dom 𝑀 ∈ βˆͺ ran sigAlgebra ∧ βˆ€π‘§ ∈ (𝑏 ∩ ran (𝐹 ∘f + 𝐺))(β—‘(𝐹 ∘f + 𝐺) β€œ {𝑧}) ∈ dom 𝑀 ∧ (𝑏 ∩ ran (𝐹 ∘f + 𝐺)) β‰Ό Ο‰) β†’ βˆͺ 𝑧 ∈ (𝑏 ∩ ran (𝐹 ∘f + 𝐺))(β—‘(𝐹 ∘f + 𝐺) β€œ {𝑧}) ∈ dom 𝑀)
14951, 131, 146, 148syl3anc 1371 . . . . . . 7 ((πœ‘ ∧ 𝑏 ∈ (sigaGenβ€˜(TopOpenβ€˜πΎ))) β†’ βˆͺ 𝑧 ∈ (𝑏 ∩ ran (𝐹 ∘f + 𝐺))(β—‘(𝐹 ∘f + 𝐺) β€œ {𝑧}) ∈ dom 𝑀)
15055, 149eqeltrrid 2838 . . . . . 6 ((πœ‘ ∧ 𝑏 ∈ (sigaGenβ€˜(TopOpenβ€˜πΎ))) β†’ (β—‘(𝐹 ∘f + 𝐺) β€œ (𝑏 ∩ ran (𝐹 ∘f + 𝐺))) ∈ dom 𝑀)
151 difpreima 7063 . . . . . . . . . 10 (Fun (𝐹 ∘f + 𝐺) β†’ (β—‘(𝐹 ∘f + 𝐺) β€œ (𝑏 βˆ– ran (𝐹 ∘f + 𝐺))) = ((β—‘(𝐹 ∘f + 𝐺) β€œ 𝑏) βˆ– (β—‘(𝐹 ∘f + 𝐺) β€œ ran (𝐹 ∘f + 𝐺))))
15225, 44, 1513syl 18 . . . . . . . . 9 (πœ‘ β†’ (β—‘(𝐹 ∘f + 𝐺) β€œ (𝑏 βˆ– ran (𝐹 ∘f + 𝐺))) = ((β—‘(𝐹 ∘f + 𝐺) β€œ 𝑏) βˆ– (β—‘(𝐹 ∘f + 𝐺) β€œ ran (𝐹 ∘f + 𝐺))))
153 cnvimarndm 6078 . . . . . . . . . . 11 (β—‘(𝐹 ∘f + 𝐺) β€œ ran (𝐹 ∘f + 𝐺)) = dom (𝐹 ∘f + 𝐺)
154153difeq2i 4118 . . . . . . . . . 10 ((β—‘(𝐹 ∘f + 𝐺) β€œ 𝑏) βˆ– (β—‘(𝐹 ∘f + 𝐺) β€œ ran (𝐹 ∘f + 𝐺))) = ((β—‘(𝐹 ∘f + 𝐺) β€œ 𝑏) βˆ– dom (𝐹 ∘f + 𝐺))
155 cnvimass 6077 . . . . . . . . . . 11 (β—‘(𝐹 ∘f + 𝐺) β€œ 𝑏) βŠ† dom (𝐹 ∘f + 𝐺)
156 ssdif0 4362 . . . . . . . . . . 11 ((β—‘(𝐹 ∘f + 𝐺) β€œ 𝑏) βŠ† dom (𝐹 ∘f + 𝐺) ↔ ((β—‘(𝐹 ∘f + 𝐺) β€œ 𝑏) βˆ– dom (𝐹 ∘f + 𝐺)) = βˆ…)
157155, 156mpbi 229 . . . . . . . . . 10 ((β—‘(𝐹 ∘f + 𝐺) β€œ 𝑏) βˆ– dom (𝐹 ∘f + 𝐺)) = βˆ…
158154, 157eqtri 2760 . . . . . . . . 9 ((β—‘(𝐹 ∘f + 𝐺) β€œ 𝑏) βˆ– (β—‘(𝐹 ∘f + 𝐺) β€œ ran (𝐹 ∘f + 𝐺))) = βˆ…
159152, 158eqtrdi 2788 . . . . . . . 8 (πœ‘ β†’ (β—‘(𝐹 ∘f + 𝐺) β€œ (𝑏 βˆ– ran (𝐹 ∘f + 𝐺))) = βˆ…)
160 0elsiga 33100 . . . . . . . . 9 (dom 𝑀 ∈ βˆͺ ran sigAlgebra β†’ βˆ… ∈ dom 𝑀)
16116, 49, 1603syl 18 . . . . . . . 8 (πœ‘ β†’ βˆ… ∈ dom 𝑀)
162159, 161eqeltrd 2833 . . . . . . 7 (πœ‘ β†’ (β—‘(𝐹 ∘f + 𝐺) β€œ (𝑏 βˆ– ran (𝐹 ∘f + 𝐺))) ∈ dom 𝑀)
163162adantr 481 . . . . . 6 ((πœ‘ ∧ 𝑏 ∈ (sigaGenβ€˜(TopOpenβ€˜πΎ))) β†’ (β—‘(𝐹 ∘f + 𝐺) β€œ (𝑏 βˆ– ran (𝐹 ∘f + 𝐺))) ∈ dom 𝑀)
164 unelsiga 33120 . . . . . 6 ((dom 𝑀 ∈ βˆͺ ran sigAlgebra ∧ (β—‘(𝐹 ∘f + 𝐺) β€œ (𝑏 ∩ ran (𝐹 ∘f + 𝐺))) ∈ dom 𝑀 ∧ (β—‘(𝐹 ∘f + 𝐺) β€œ (𝑏 βˆ– ran (𝐹 ∘f + 𝐺))) ∈ dom 𝑀) β†’ ((β—‘(𝐹 ∘f + 𝐺) β€œ (𝑏 ∩ ran (𝐹 ∘f + 𝐺))) βˆͺ (β—‘(𝐹 ∘f + 𝐺) β€œ (𝑏 βˆ– ran (𝐹 ∘f + 𝐺)))) ∈ dom 𝑀)
16551, 150, 163, 164syl3anc 1371 . . . . 5 ((πœ‘ ∧ 𝑏 ∈ (sigaGenβ€˜(TopOpenβ€˜πΎ))) β†’ ((β—‘(𝐹 ∘f + 𝐺) β€œ (𝑏 ∩ ran (𝐹 ∘f + 𝐺))) βˆͺ (β—‘(𝐹 ∘f + 𝐺) β€œ (𝑏 βˆ– ran (𝐹 ∘f + 𝐺)))) ∈ dom 𝑀)
16648, 165eqeltrd 2833 . . . 4 ((πœ‘ ∧ 𝑏 ∈ (sigaGenβ€˜(TopOpenβ€˜πΎ))) β†’ (β—‘(𝐹 ∘f + 𝐺) β€œ 𝑏) ∈ dom 𝑀)
167166ralrimiva 3146 . . 3 (πœ‘ β†’ βˆ€π‘ ∈ (sigaGenβ€˜(TopOpenβ€˜πΎ))(β—‘(𝐹 ∘f + 𝐺) β€œ 𝑏) ∈ dom 𝑀)
16850, 38ismbfm 33237 . . 3 (πœ‘ β†’ ((𝐹 ∘f + 𝐺) ∈ (dom 𝑀MblFnM(sigaGenβ€˜(TopOpenβ€˜πΎ))) ↔ ((𝐹 ∘f + 𝐺) ∈ (βˆͺ (sigaGenβ€˜(TopOpenβ€˜πΎ)) ↑m βˆͺ dom 𝑀) ∧ βˆ€π‘ ∈ (sigaGenβ€˜(TopOpenβ€˜πΎ))(β—‘(𝐹 ∘f + 𝐺) β€œ 𝑏) ∈ dom 𝑀)))
16941, 167, 168mpbir2and 711 . 2 (πœ‘ β†’ (𝐹 ∘f + 𝐺) ∈ (dom 𝑀MblFnM(sigaGenβ€˜(TopOpenβ€˜πΎ))))
17062adantr 481 . . . . . . 7 ((πœ‘ ∧ 𝑧 ∈ (ran (𝐹 ∘f + 𝐺) βˆ– {(0gβ€˜πΎ)})) β†’ (β—‘(𝐹 ∘f + 𝐺) β€œ {𝑧}) = βˆͺ 𝑝 ∈ ((β—‘ + β€œ {𝑧}) ∩ (ran 𝐹 Γ— ran 𝐺))((◑𝐹 β€œ {(1st β€˜π‘)}) ∩ (◑𝐺 β€œ {(2nd β€˜π‘)})))
171170fveq2d 6892 . . . . . 6 ((πœ‘ ∧ 𝑧 ∈ (ran (𝐹 ∘f + 𝐺) βˆ– {(0gβ€˜πΎ)})) β†’ (π‘€β€˜(β—‘(𝐹 ∘f + 𝐺) β€œ {𝑧})) = (π‘€β€˜βˆͺ 𝑝 ∈ ((β—‘ + β€œ {𝑧}) ∩ (ran 𝐹 Γ— ran 𝐺))((◑𝐹 β€œ {(1st β€˜π‘)}) ∩ (◑𝐺 β€œ {(2nd β€˜π‘)}))))
172 measbasedom 33188 . . . . . . . . 9 (𝑀 ∈ βˆͺ ran measures ↔ 𝑀 ∈ (measuresβ€˜dom 𝑀))
17316, 172sylib 217 . . . . . . . 8 (πœ‘ β†’ 𝑀 ∈ (measuresβ€˜dom 𝑀))
174173adantr 481 . . . . . . 7 ((πœ‘ ∧ 𝑧 ∈ (ran (𝐹 ∘f + 𝐺) βˆ– {(0gβ€˜πΎ)})) β†’ 𝑀 ∈ (measuresβ€˜dom 𝑀))
175 eldifi 4125 . . . . . . . 8 (𝑧 ∈ (ran (𝐹 ∘f + 𝐺) βˆ– {(0gβ€˜πΎ)}) β†’ 𝑧 ∈ ran (𝐹 ∘f + 𝐺))
176175, 109sylan2 593 . . . . . . 7 ((πœ‘ ∧ 𝑧 ∈ (ran (𝐹 ∘f + 𝐺) βˆ– {(0gβ€˜πΎ)})) β†’ βˆ€π‘ ∈ ((β—‘ + β€œ {𝑧}) ∩ (ran 𝐹 Γ— ran 𝐺))((◑𝐹 β€œ {(1st β€˜π‘)}) ∩ (◑𝐺 β€œ {(2nd β€˜π‘)})) ∈ dom 𝑀)
177122adantr 481 . . . . . . 7 ((πœ‘ ∧ 𝑧 ∈ (ran (𝐹 ∘f + 𝐺) βˆ– {(0gβ€˜πΎ)})) β†’ ((β—‘ + β€œ {𝑧}) ∩ (ran 𝐹 Γ— ran 𝐺)) β‰Ό Ο‰)
178 sneq 4637 . . . . . . . . . . 11 (π‘₯ = (1st β€˜π‘) β†’ {π‘₯} = {(1st β€˜π‘)})
179178imaeq2d 6057 . . . . . . . . . 10 (π‘₯ = (1st β€˜π‘) β†’ (◑𝐹 β€œ {π‘₯}) = (◑𝐹 β€œ {(1st β€˜π‘)}))
180 sneq 4637 . . . . . . . . . . 11 (𝑦 = (2nd β€˜π‘) β†’ {𝑦} = {(2nd β€˜π‘)})
181180imaeq2d 6057 . . . . . . . . . 10 (𝑦 = (2nd β€˜π‘) β†’ (◑𝐺 β€œ {𝑦}) = (◑𝐺 β€œ {(2nd β€˜π‘)}))
18218ffund 6718 . . . . . . . . . . 11 (πœ‘ β†’ Fun 𝐹)
183 sndisj 5138 . . . . . . . . . . 11 Disj π‘₯ ∈ ran 𝐹{π‘₯}
184 disjpreima 31802 . . . . . . . . . . 11 ((Fun 𝐹 ∧ Disj π‘₯ ∈ ran 𝐹{π‘₯}) β†’ Disj π‘₯ ∈ ran 𝐹(◑𝐹 β€œ {π‘₯}))
185182, 183, 184sylancl 586 . . . . . . . . . 10 (πœ‘ β†’ Disj π‘₯ ∈ ran 𝐹(◑𝐹 β€œ {π‘₯}))
18620ffund 6718 . . . . . . . . . . 11 (πœ‘ β†’ Fun 𝐺)
187 sndisj 5138 . . . . . . . . . . 11 Disj 𝑦 ∈ ran 𝐺{𝑦}
188 disjpreima 31802 . . . . . . . . . . 11 ((Fun 𝐺 ∧ Disj 𝑦 ∈ ran 𝐺{𝑦}) β†’ Disj 𝑦 ∈ ran 𝐺(◑𝐺 β€œ {𝑦}))
189186, 187, 188sylancl 586 . . . . . . . . . 10 (πœ‘ β†’ Disj 𝑦 ∈ ran 𝐺(◑𝐺 β€œ {𝑦}))
190179, 181, 185, 189disjxpin 31806 . . . . . . . . 9 (πœ‘ β†’ Disj 𝑝 ∈ (ran 𝐹 Γ— ran 𝐺)((◑𝐹 β€œ {(1st β€˜π‘)}) ∩ (◑𝐺 β€œ {(2nd β€˜π‘)})))
191 disjss1 5118 . . . . . . . . 9 (((β—‘ + β€œ {𝑧}) ∩ (ran 𝐹 Γ— ran 𝐺)) βŠ† (ran 𝐹 Γ— ran 𝐺) β†’ (Disj 𝑝 ∈ (ran 𝐹 Γ— ran 𝐺)((◑𝐹 β€œ {(1st β€˜π‘)}) ∩ (◑𝐺 β€œ {(2nd β€˜π‘)})) β†’ Disj 𝑝 ∈ ((β—‘ + β€œ {𝑧}) ∩ (ran 𝐹 Γ— ran 𝐺))((◑𝐹 β€œ {(1st β€˜π‘)}) ∩ (◑𝐺 β€œ {(2nd β€˜π‘)}))))
192114, 190, 191mpsyl 68 . . . . . . . 8 (πœ‘ β†’ Disj 𝑝 ∈ ((β—‘ + β€œ {𝑧}) ∩ (ran 𝐹 Γ— ran 𝐺))((◑𝐹 β€œ {(1st β€˜π‘)}) ∩ (◑𝐺 β€œ {(2nd β€˜π‘)})))
193192adantr 481 . . . . . . 7 ((πœ‘ ∧ 𝑧 ∈ (ran (𝐹 ∘f + 𝐺) βˆ– {(0gβ€˜πΎ)})) β†’ Disj 𝑝 ∈ ((β—‘ + β€œ {𝑧}) ∩ (ran 𝐹 Γ— ran 𝐺))((◑𝐹 β€œ {(1st β€˜π‘)}) ∩ (◑𝐺 β€œ {(2nd β€˜π‘)})))
194 measvuni 33200 . . . . . . 7 ((𝑀 ∈ (measuresβ€˜dom 𝑀) ∧ βˆ€π‘ ∈ ((β—‘ + β€œ {𝑧}) ∩ (ran 𝐹 Γ— ran 𝐺))((◑𝐹 β€œ {(1st β€˜π‘)}) ∩ (◑𝐺 β€œ {(2nd β€˜π‘)})) ∈ dom 𝑀 ∧ (((β—‘ + β€œ {𝑧}) ∩ (ran 𝐹 Γ— ran 𝐺)) β‰Ό Ο‰ ∧ Disj 𝑝 ∈ ((β—‘ + β€œ {𝑧}) ∩ (ran 𝐹 Γ— ran 𝐺))((◑𝐹 β€œ {(1st β€˜π‘)}) ∩ (◑𝐺 β€œ {(2nd β€˜π‘)})))) β†’ (π‘€β€˜βˆͺ 𝑝 ∈ ((β—‘ + β€œ {𝑧}) ∩ (ran 𝐹 Γ— ran 𝐺))((◑𝐹 β€œ {(1st β€˜π‘)}) ∩ (◑𝐺 β€œ {(2nd β€˜π‘)}))) = Ξ£*𝑝 ∈ ((β—‘ + β€œ {𝑧}) ∩ (ran 𝐹 Γ— ran 𝐺))(π‘€β€˜((◑𝐹 β€œ {(1st β€˜π‘)}) ∩ (◑𝐺 β€œ {(2nd β€˜π‘)}))))
195174, 176, 177, 193, 194syl112anc 1374 . . . . . 6 ((πœ‘ ∧ 𝑧 ∈ (ran (𝐹 ∘f + 𝐺) βˆ– {(0gβ€˜πΎ)})) β†’ (π‘€β€˜βˆͺ 𝑝 ∈ ((β—‘ + β€œ {𝑧}) ∩ (ran 𝐹 Γ— ran 𝐺))((◑𝐹 β€œ {(1st β€˜π‘)}) ∩ (◑𝐺 β€œ {(2nd β€˜π‘)}))) = Ξ£*𝑝 ∈ ((β—‘ + β€œ {𝑧}) ∩ (ran 𝐹 Γ— ran 𝐺))(π‘€β€˜((◑𝐹 β€œ {(1st β€˜π‘)}) ∩ (◑𝐺 β€œ {(2nd β€˜π‘)}))))
196 ssfi 9169 . . . . . . . . 9 (((ran 𝐹 Γ— ran 𝐺) ∈ Fin ∧ ((β—‘ + β€œ {𝑧}) ∩ (ran 𝐹 Γ— ran 𝐺)) βŠ† (ran 𝐹 Γ— ran 𝐺)) β†’ ((β—‘ + β€œ {𝑧}) ∩ (ran 𝐹 Γ— ran 𝐺)) ∈ Fin)
197113, 114, 196sylancl 586 . . . . . . . 8 (πœ‘ β†’ ((β—‘ + β€œ {𝑧}) ∩ (ran 𝐹 Γ— ran 𝐺)) ∈ Fin)
198197adantr 481 . . . . . . 7 ((πœ‘ ∧ 𝑧 ∈ (ran (𝐹 ∘f + 𝐺) βˆ– {(0gβ€˜πΎ)})) β†’ ((β—‘ + β€œ {𝑧}) ∩ (ran 𝐹 Γ— ran 𝐺)) ∈ Fin)
199 simpll 765 . . . . . . . 8 (((πœ‘ ∧ 𝑧 ∈ (ran (𝐹 ∘f + 𝐺) βˆ– {(0gβ€˜πΎ)})) ∧ 𝑝 ∈ ((β—‘ + β€œ {𝑧}) ∩ (ran 𝐹 Γ— ran 𝐺))) β†’ πœ‘)
200 simpr 485 . . . . . . . . . 10 (((πœ‘ ∧ 𝑧 ∈ (ran (𝐹 ∘f + 𝐺) βˆ– {(0gβ€˜πΎ)})) ∧ 𝑝 ∈ ((β—‘ + β€œ {𝑧}) ∩ (ran 𝐹 Γ— ran 𝐺))) β†’ 𝑝 ∈ ((β—‘ + β€œ {𝑧}) ∩ (ran 𝐹 Γ— ran 𝐺)))
201114, 200sselid 3979 . . . . . . . . 9 (((πœ‘ ∧ 𝑧 ∈ (ran (𝐹 ∘f + 𝐺) βˆ– {(0gβ€˜πΎ)})) ∧ 𝑝 ∈ ((β—‘ + β€œ {𝑧}) ∩ (ran 𝐹 Γ— ran 𝐺))) β†’ 𝑝 ∈ (ran 𝐹 Γ— ran 𝐺))
202 xp1st 8003 . . . . . . . . 9 (𝑝 ∈ (ran 𝐹 Γ— ran 𝐺) β†’ (1st β€˜π‘) ∈ ran 𝐹)
203201, 202syl 17 . . . . . . . 8 (((πœ‘ ∧ 𝑧 ∈ (ran (𝐹 ∘f + 𝐺) βˆ– {(0gβ€˜πΎ)})) ∧ 𝑝 ∈ ((β—‘ + β€œ {𝑧}) ∩ (ran 𝐹 Γ— ran 𝐺))) β†’ (1st β€˜π‘) ∈ ran 𝐹)
204 xp2nd 8004 . . . . . . . . 9 (𝑝 ∈ (ran 𝐹 Γ— ran 𝐺) β†’ (2nd β€˜π‘) ∈ ran 𝐺)
205201, 204syl 17 . . . . . . . 8 (((πœ‘ ∧ 𝑧 ∈ (ran (𝐹 ∘f + 𝐺) βˆ– {(0gβ€˜πΎ)})) ∧ 𝑝 ∈ ((β—‘ + β€œ {𝑧}) ∩ (ran 𝐹 Γ— ran 𝐺))) β†’ (2nd β€˜π‘) ∈ ran 𝐺)
206 oveq12 7414 . . . . . . . . . . . . . . . 16 ((π‘₯ = 0 ∧ 𝑦 = 0 ) β†’ (π‘₯ + 𝑦) = ( 0 + 0 ))
207 sibfof.5 . . . . . . . . . . . . . . . 16 (πœ‘ β†’ ( 0 + 0 ) = (0gβ€˜πΎ))
208206, 207sylan9eqr 2794 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ (π‘₯ = 0 ∧ 𝑦 = 0 )) β†’ (π‘₯ + 𝑦) = (0gβ€˜πΎ))
209208ex 413 . . . . . . . . . . . . . 14 (πœ‘ β†’ ((π‘₯ = 0 ∧ 𝑦 = 0 ) β†’ (π‘₯ + 𝑦) = (0gβ€˜πΎ)))
210209necon3ad 2953 . . . . . . . . . . . . 13 (πœ‘ β†’ ((π‘₯ + 𝑦) β‰  (0gβ€˜πΎ) β†’ Β¬ (π‘₯ = 0 ∧ 𝑦 = 0 )))
211 neorian 3037 . . . . . . . . . . . . 13 ((π‘₯ β‰  0 ∨ 𝑦 β‰  0 ) ↔ Β¬ (π‘₯ = 0 ∧ 𝑦 = 0 ))
212210, 211syl6ibr 251 . . . . . . . . . . . 12 (πœ‘ β†’ ((π‘₯ + 𝑦) β‰  (0gβ€˜πΎ) β†’ (π‘₯ β‰  0 ∨ 𝑦 β‰  0 )))
213212adantr 481 . . . . . . . . . . 11 ((πœ‘ ∧ (π‘₯ ∈ 𝐡 ∧ 𝑦 ∈ 𝐡)) β†’ ((π‘₯ + 𝑦) β‰  (0gβ€˜πΎ) β†’ (π‘₯ β‰  0 ∨ 𝑦 β‰  0 )))
214213ralrimivva 3200 . . . . . . . . . 10 (πœ‘ β†’ βˆ€π‘₯ ∈ 𝐡 βˆ€π‘¦ ∈ 𝐡 ((π‘₯ + 𝑦) β‰  (0gβ€˜πΎ) β†’ (π‘₯ β‰  0 ∨ 𝑦 β‰  0 )))
215199, 214syl 17 . . . . . . . . 9 (((πœ‘ ∧ 𝑧 ∈ (ran (𝐹 ∘f + 𝐺) βˆ– {(0gβ€˜πΎ)})) ∧ 𝑝 ∈ ((β—‘ + β€œ {𝑧}) ∩ (ran 𝐹 Γ— ran 𝐺))) β†’ βˆ€π‘₯ ∈ 𝐡 βˆ€π‘¦ ∈ 𝐡 ((π‘₯ + 𝑦) β‰  (0gβ€˜πΎ) β†’ (π‘₯ β‰  0 ∨ 𝑦 β‰  0 )))
21667a1i 11 . . . . . . . . . . . . 13 ((πœ‘ ∧ 𝑧 ∈ (ran (𝐹 ∘f + 𝐺) βˆ– {(0gβ€˜πΎ)})) β†’ ((β—‘ + β€œ {𝑧}) ∩ (ran 𝐹 Γ— ran 𝐺)) βŠ† (β—‘ + β€œ {𝑧}))
217216sselda 3981 . . . . . . . . . . . 12 (((πœ‘ ∧ 𝑧 ∈ (ran (𝐹 ∘f + 𝐺) βˆ– {(0gβ€˜πΎ)})) ∧ 𝑝 ∈ ((β—‘ + β€œ {𝑧}) ∩ (ran 𝐹 Γ— ran 𝐺))) β†’ 𝑝 ∈ (β—‘ + β€œ {𝑧}))
218 fniniseg 7058 . . . . . . . . . . . . 13 ( + Fn (𝐡 Γ— 𝐡) β†’ (𝑝 ∈ (β—‘ + β€œ {𝑧}) ↔ (𝑝 ∈ (𝐡 Γ— 𝐡) ∧ ( + β€˜π‘) = 𝑧)))
219199, 61, 2183syl 18 . . . . . . . . . . . 12 (((πœ‘ ∧ 𝑧 ∈ (ran (𝐹 ∘f + 𝐺) βˆ– {(0gβ€˜πΎ)})) ∧ 𝑝 ∈ ((β—‘ + β€œ {𝑧}) ∩ (ran 𝐹 Γ— ran 𝐺))) β†’ (𝑝 ∈ (β—‘ + β€œ {𝑧}) ↔ (𝑝 ∈ (𝐡 Γ— 𝐡) ∧ ( + β€˜π‘) = 𝑧)))
220217, 219mpbid 231 . . . . . . . . . . 11 (((πœ‘ ∧ 𝑧 ∈ (ran (𝐹 ∘f + 𝐺) βˆ– {(0gβ€˜πΎ)})) ∧ 𝑝 ∈ ((β—‘ + β€œ {𝑧}) ∩ (ran 𝐹 Γ— ran 𝐺))) β†’ (𝑝 ∈ (𝐡 Γ— 𝐡) ∧ ( + β€˜π‘) = 𝑧))
221 simpr 485 . . . . . . . . . . . 12 ((𝑝 ∈ (𝐡 Γ— 𝐡) ∧ ( + β€˜π‘) = 𝑧) β†’ ( + β€˜π‘) = 𝑧)
222 1st2nd2 8010 . . . . . . . . . . . . . . 15 (𝑝 ∈ (𝐡 Γ— 𝐡) β†’ 𝑝 = ⟨(1st β€˜π‘), (2nd β€˜π‘)⟩)
223222fveq2d 6892 . . . . . . . . . . . . . 14 (𝑝 ∈ (𝐡 Γ— 𝐡) β†’ ( + β€˜π‘) = ( + β€˜βŸ¨(1st β€˜π‘), (2nd β€˜π‘)⟩))
224 df-ov 7408 . . . . . . . . . . . . . 14 ((1st β€˜π‘) + (2nd β€˜π‘)) = ( + β€˜βŸ¨(1st β€˜π‘), (2nd β€˜π‘)⟩)
225223, 224eqtr4di 2790 . . . . . . . . . . . . 13 (𝑝 ∈ (𝐡 Γ— 𝐡) β†’ ( + β€˜π‘) = ((1st β€˜π‘) + (2nd β€˜π‘)))
226225adantr 481 . . . . . . . . . . . 12 ((𝑝 ∈ (𝐡 Γ— 𝐡) ∧ ( + β€˜π‘) = 𝑧) β†’ ( + β€˜π‘) = ((1st β€˜π‘) + (2nd β€˜π‘)))
227221, 226eqtr3d 2774 . . . . . . . . . . 11 ((𝑝 ∈ (𝐡 Γ— 𝐡) ∧ ( + β€˜π‘) = 𝑧) β†’ 𝑧 = ((1st β€˜π‘) + (2nd β€˜π‘)))
228220, 227syl 17 . . . . . . . . . 10 (((πœ‘ ∧ 𝑧 ∈ (ran (𝐹 ∘f + 𝐺) βˆ– {(0gβ€˜πΎ)})) ∧ 𝑝 ∈ ((β—‘ + β€œ {𝑧}) ∩ (ran 𝐹 Γ— ran 𝐺))) β†’ 𝑧 = ((1st β€˜π‘) + (2nd β€˜π‘)))
229 simplr 767 . . . . . . . . . . . 12 (((πœ‘ ∧ 𝑧 ∈ (ran (𝐹 ∘f + 𝐺) βˆ– {(0gβ€˜πΎ)})) ∧ 𝑝 ∈ ((β—‘ + β€œ {𝑧}) ∩ (ran 𝐹 Γ— ran 𝐺))) β†’ 𝑧 ∈ (ran (𝐹 ∘f + 𝐺) βˆ– {(0gβ€˜πΎ)}))
230229eldifbd 3960 . . . . . . . . . . 11 (((πœ‘ ∧ 𝑧 ∈ (ran (𝐹 ∘f + 𝐺) βˆ– {(0gβ€˜πΎ)})) ∧ 𝑝 ∈ ((β—‘ + β€œ {𝑧}) ∩ (ran 𝐹 Γ— ran 𝐺))) β†’ Β¬ 𝑧 ∈ {(0gβ€˜πΎ)})
231 velsn 4643 . . . . . . . . . . . 12 (𝑧 ∈ {(0gβ€˜πΎ)} ↔ 𝑧 = (0gβ€˜πΎ))
232231necon3bbii 2988 . . . . . . . . . . 11 (Β¬ 𝑧 ∈ {(0gβ€˜πΎ)} ↔ 𝑧 β‰  (0gβ€˜πΎ))
233230, 232sylib 217 . . . . . . . . . 10 (((πœ‘ ∧ 𝑧 ∈ (ran (𝐹 ∘f + 𝐺) βˆ– {(0gβ€˜πΎ)})) ∧ 𝑝 ∈ ((β—‘ + β€œ {𝑧}) ∩ (ran 𝐹 Γ— ran 𝐺))) β†’ 𝑧 β‰  (0gβ€˜πΎ))
234228, 233eqnetrrd 3009 . . . . . . . . 9 (((πœ‘ ∧ 𝑧 ∈ (ran (𝐹 ∘f + 𝐺) βˆ– {(0gβ€˜πΎ)})) ∧ 𝑝 ∈ ((β—‘ + β€œ {𝑧}) ∩ (ran 𝐹 Γ— ran 𝐺))) β†’ ((1st β€˜π‘) + (2nd β€˜π‘)) β‰  (0gβ€˜πΎ))
235175, 72sylanl2 679 . . . . . . . . . . 11 (((πœ‘ ∧ 𝑧 ∈ (ran (𝐹 ∘f + 𝐺) βˆ– {(0gβ€˜πΎ)})) ∧ 𝑝 ∈ ((β—‘ + β€œ {𝑧}) ∩ (ran 𝐹 Γ— ran 𝐺))) β†’ 𝑝 ∈ (𝐡 Γ— 𝐡))
236235, 85syl 17 . . . . . . . . . 10 (((πœ‘ ∧ 𝑧 ∈ (ran (𝐹 ∘f + 𝐺) βˆ– {(0gβ€˜πΎ)})) ∧ 𝑝 ∈ ((β—‘ + β€œ {𝑧}) ∩ (ran 𝐹 Γ— ran 𝐺))) β†’ (1st β€˜π‘) ∈ 𝐡)
237235, 98syl 17 . . . . . . . . . 10 (((πœ‘ ∧ 𝑧 ∈ (ran (𝐹 ∘f + 𝐺) βˆ– {(0gβ€˜πΎ)})) ∧ 𝑝 ∈ ((β—‘ + β€œ {𝑧}) ∩ (ran 𝐹 Γ— ran 𝐺))) β†’ (2nd β€˜π‘) ∈ 𝐡)
238 oveq1 7412 . . . . . . . . . . . . 13 (π‘₯ = (1st β€˜π‘) β†’ (π‘₯ + 𝑦) = ((1st β€˜π‘) + 𝑦))
239238neeq1d 3000 . . . . . . . . . . . 12 (π‘₯ = (1st β€˜π‘) β†’ ((π‘₯ + 𝑦) β‰  (0gβ€˜πΎ) ↔ ((1st β€˜π‘) + 𝑦) β‰  (0gβ€˜πΎ)))
240 neeq1 3003 . . . . . . . . . . . . 13 (π‘₯ = (1st β€˜π‘) β†’ (π‘₯ β‰  0 ↔ (1st β€˜π‘) β‰  0 ))
241240orbi1d 915 . . . . . . . . . . . 12 (π‘₯ = (1st β€˜π‘) β†’ ((π‘₯ β‰  0 ∨ 𝑦 β‰  0 ) ↔ ((1st β€˜π‘) β‰  0 ∨ 𝑦 β‰  0 )))
242239, 241imbi12d 344 . . . . . . . . . . 11 (π‘₯ = (1st β€˜π‘) β†’ (((π‘₯ + 𝑦) β‰  (0gβ€˜πΎ) β†’ (π‘₯ β‰  0 ∨ 𝑦 β‰  0 )) ↔ (((1st β€˜π‘) + 𝑦) β‰  (0gβ€˜πΎ) β†’ ((1st β€˜π‘) β‰  0 ∨ 𝑦 β‰  0 ))))
243 oveq2 7413 . . . . . . . . . . . . 13 (𝑦 = (2nd β€˜π‘) β†’ ((1st β€˜π‘) + 𝑦) = ((1st β€˜π‘) + (2nd β€˜π‘)))
244243neeq1d 3000 . . . . . . . . . . . 12 (𝑦 = (2nd β€˜π‘) β†’ (((1st β€˜π‘) + 𝑦) β‰  (0gβ€˜πΎ) ↔ ((1st β€˜π‘) + (2nd β€˜π‘)) β‰  (0gβ€˜πΎ)))
245 neeq1 3003 . . . . . . . . . . . . 13 (𝑦 = (2nd β€˜π‘) β†’ (𝑦 β‰  0 ↔ (2nd β€˜π‘) β‰  0 ))
246245orbi2d 914 . . . . . . . . . . . 12 (𝑦 = (2nd β€˜π‘) β†’ (((1st β€˜π‘) β‰  0 ∨ 𝑦 β‰  0 ) ↔ ((1st β€˜π‘) β‰  0 ∨ (2nd β€˜π‘) β‰  0 )))
247244, 246imbi12d 344 . . . . . . . . . . 11 (𝑦 = (2nd β€˜π‘) β†’ ((((1st β€˜π‘) + 𝑦) β‰  (0gβ€˜πΎ) β†’ ((1st β€˜π‘) β‰  0 ∨ 𝑦 β‰  0 )) ↔ (((1st β€˜π‘) + (2nd β€˜π‘)) β‰  (0gβ€˜πΎ) β†’ ((1st β€˜π‘) β‰  0 ∨ (2nd β€˜π‘) β‰  0 ))))
248242, 247rspc2v 3621 . . . . . . . . . 10 (((1st β€˜π‘) ∈ 𝐡 ∧ (2nd β€˜π‘) ∈ 𝐡) β†’ (βˆ€π‘₯ ∈ 𝐡 βˆ€π‘¦ ∈ 𝐡 ((π‘₯ + 𝑦) β‰  (0gβ€˜πΎ) β†’ (π‘₯ β‰  0 ∨ 𝑦 β‰  0 )) β†’ (((1st β€˜π‘) + (2nd β€˜π‘)) β‰  (0gβ€˜πΎ) β†’ ((1st β€˜π‘) β‰  0 ∨ (2nd β€˜π‘) β‰  0 ))))
249236, 237, 248syl2anc 584 . . . . . . . . 9 (((πœ‘ ∧ 𝑧 ∈ (ran (𝐹 ∘f + 𝐺) βˆ– {(0gβ€˜πΎ)})) ∧ 𝑝 ∈ ((β—‘ + β€œ {𝑧}) ∩ (ran 𝐹 Γ— ran 𝐺))) β†’ (βˆ€π‘₯ ∈ 𝐡 βˆ€π‘¦ ∈ 𝐡 ((π‘₯ + 𝑦) β‰  (0gβ€˜πΎ) β†’ (π‘₯ β‰  0 ∨ 𝑦 β‰  0 )) β†’ (((1st β€˜π‘) + (2nd β€˜π‘)) β‰  (0gβ€˜πΎ) β†’ ((1st β€˜π‘) β‰  0 ∨ (2nd β€˜π‘) β‰  0 ))))
250215, 234, 249mp2d 49 . . . . . . . 8 (((πœ‘ ∧ 𝑧 ∈ (ran (𝐹 ∘f + 𝐺) βˆ– {(0gβ€˜πΎ)})) ∧ 𝑝 ∈ ((β—‘ + β€œ {𝑧}) ∩ (ran 𝐹 Γ— ran 𝐺))) β†’ ((1st β€˜π‘) β‰  0 ∨ (2nd β€˜π‘) β‰  0 ))
2513, 4, 11, 12, 13, 14, 15, 16, 17, 19, 2, 74sibfinima 33326 . . . . . . . 8 (((πœ‘ ∧ (1st β€˜π‘) ∈ ran 𝐹 ∧ (2nd β€˜π‘) ∈ ran 𝐺) ∧ ((1st β€˜π‘) β‰  0 ∨ (2nd β€˜π‘) β‰  0 )) β†’ (π‘€β€˜((◑𝐹 β€œ {(1st β€˜π‘)}) ∩ (◑𝐺 β€œ {(2nd β€˜π‘)}))) ∈ (0[,)+∞))
252199, 203, 205, 250, 251syl31anc 1373 . . . . . . 7 (((πœ‘ ∧ 𝑧 ∈ (ran (𝐹 ∘f + 𝐺) βˆ– {(0gβ€˜πΎ)})) ∧ 𝑝 ∈ ((β—‘ + β€œ {𝑧}) ∩ (ran 𝐹 Γ— ran 𝐺))) β†’ (π‘€β€˜((◑𝐹 β€œ {(1st β€˜π‘)}) ∩ (◑𝐺 β€œ {(2nd β€˜π‘)}))) ∈ (0[,)+∞))
253198, 252esumpfinval 33061 . . . . . 6 ((πœ‘ ∧ 𝑧 ∈ (ran (𝐹 ∘f + 𝐺) βˆ– {(0gβ€˜πΎ)})) β†’ Ξ£*𝑝 ∈ ((β—‘ + β€œ {𝑧}) ∩ (ran 𝐹 Γ— ran 𝐺))(π‘€β€˜((◑𝐹 β€œ {(1st β€˜π‘)}) ∩ (◑𝐺 β€œ {(2nd β€˜π‘)}))) = Σ𝑝 ∈ ((β—‘ + β€œ {𝑧}) ∩ (ran 𝐹 Γ— ran 𝐺))(π‘€β€˜((◑𝐹 β€œ {(1st β€˜π‘)}) ∩ (◑𝐺 β€œ {(2nd β€˜π‘)}))))
254171, 195, 2533eqtrd 2776 . . . . 5 ((πœ‘ ∧ 𝑧 ∈ (ran (𝐹 ∘f + 𝐺) βˆ– {(0gβ€˜πΎ)})) β†’ (π‘€β€˜(β—‘(𝐹 ∘f + 𝐺) β€œ {𝑧})) = Σ𝑝 ∈ ((β—‘ + β€œ {𝑧}) ∩ (ran 𝐹 Γ— ran 𝐺))(π‘€β€˜((◑𝐹 β€œ {(1st β€˜π‘)}) ∩ (◑𝐺 β€œ {(2nd β€˜π‘)}))))
255 rge0ssre 13429 . . . . . . 7 (0[,)+∞) βŠ† ℝ
256255, 252sselid 3979 . . . . . 6 (((πœ‘ ∧ 𝑧 ∈ (ran (𝐹 ∘f + 𝐺) βˆ– {(0gβ€˜πΎ)})) ∧ 𝑝 ∈ ((β—‘ + β€œ {𝑧}) ∩ (ran 𝐹 Γ— ran 𝐺))) β†’ (π‘€β€˜((◑𝐹 β€œ {(1st β€˜π‘)}) ∩ (◑𝐺 β€œ {(2nd β€˜π‘)}))) ∈ ℝ)
257198, 256fsumrecl 15676 . . . . 5 ((πœ‘ ∧ 𝑧 ∈ (ran (𝐹 ∘f + 𝐺) βˆ– {(0gβ€˜πΎ)})) β†’ Σ𝑝 ∈ ((β—‘ + β€œ {𝑧}) ∩ (ran 𝐹 Γ— ran 𝐺))(π‘€β€˜((◑𝐹 β€œ {(1st β€˜π‘)}) ∩ (◑𝐺 β€œ {(2nd β€˜π‘)}))) ∈ ℝ)
258254, 257eqeltrd 2833 . . . 4 ((πœ‘ ∧ 𝑧 ∈ (ran (𝐹 ∘f + 𝐺) βˆ– {(0gβ€˜πΎ)})) β†’ (π‘€β€˜(β—‘(𝐹 ∘f + 𝐺) β€œ {𝑧})) ∈ ℝ)
259174adantr 481 . . . . . . 7 (((πœ‘ ∧ 𝑧 ∈ (ran (𝐹 ∘f + 𝐺) βˆ– {(0gβ€˜πΎ)})) ∧ 𝑝 ∈ ((β—‘ + β€œ {𝑧}) ∩ (ran 𝐹 Γ— ran 𝐺))) β†’ 𝑀 ∈ (measuresβ€˜dom 𝑀))
260175, 108sylanl2 679 . . . . . . 7 (((πœ‘ ∧ 𝑧 ∈ (ran (𝐹 ∘f + 𝐺) βˆ– {(0gβ€˜πΎ)})) ∧ 𝑝 ∈ ((β—‘ + β€œ {𝑧}) ∩ (ran 𝐹 Γ— ran 𝐺))) β†’ ((◑𝐹 β€œ {(1st β€˜π‘)}) ∩ (◑𝐺 β€œ {(2nd β€˜π‘)})) ∈ dom 𝑀)
261 measge0 33193 . . . . . . 7 ((𝑀 ∈ (measuresβ€˜dom 𝑀) ∧ ((◑𝐹 β€œ {(1st β€˜π‘)}) ∩ (◑𝐺 β€œ {(2nd β€˜π‘)})) ∈ dom 𝑀) β†’ 0 ≀ (π‘€β€˜((◑𝐹 β€œ {(1st β€˜π‘)}) ∩ (◑𝐺 β€œ {(2nd β€˜π‘)}))))
262259, 260, 261syl2anc 584 . . . . . 6 (((πœ‘ ∧ 𝑧 ∈ (ran (𝐹 ∘f + 𝐺) βˆ– {(0gβ€˜πΎ)})) ∧ 𝑝 ∈ ((β—‘ + β€œ {𝑧}) ∩ (ran 𝐹 Γ— ran 𝐺))) β†’ 0 ≀ (π‘€β€˜((◑𝐹 β€œ {(1st β€˜π‘)}) ∩ (◑𝐺 β€œ {(2nd β€˜π‘)}))))
263198, 256, 262fsumge0 15737 . . . . 5 ((πœ‘ ∧ 𝑧 ∈ (ran (𝐹 ∘f + 𝐺) βˆ– {(0gβ€˜πΎ)})) β†’ 0 ≀ Σ𝑝 ∈ ((β—‘ + β€œ {𝑧}) ∩ (ran 𝐹 Γ— ran 𝐺))(π‘€β€˜((◑𝐹 β€œ {(1st β€˜π‘)}) ∩ (◑𝐺 β€œ {(2nd β€˜π‘)}))))
264263, 254breqtrrd 5175 . . . 4 ((πœ‘ ∧ 𝑧 ∈ (ran (𝐹 ∘f + 𝐺) βˆ– {(0gβ€˜πΎ)})) β†’ 0 ≀ (π‘€β€˜(β—‘(𝐹 ∘f + 𝐺) β€œ {𝑧})))
265 elrege0 13427 . . . 4 ((π‘€β€˜(β—‘(𝐹 ∘f + 𝐺) β€œ {𝑧})) ∈ (0[,)+∞) ↔ ((π‘€β€˜(β—‘(𝐹 ∘f + 𝐺) β€œ {𝑧})) ∈ ℝ ∧ 0 ≀ (π‘€β€˜(β—‘(𝐹 ∘f + 𝐺) β€œ {𝑧}))))
266258, 264, 265sylanbrc 583 . . 3 ((πœ‘ ∧ 𝑧 ∈ (ran (𝐹 ∘f + 𝐺) βˆ– {(0gβ€˜πΎ)})) β†’ (π‘€β€˜(β—‘(𝐹 ∘f + 𝐺) β€œ {𝑧})) ∈ (0[,)+∞))
267266ralrimiva 3146 . 2 (πœ‘ β†’ βˆ€π‘§ ∈ (ran (𝐹 ∘f + 𝐺) βˆ– {(0gβ€˜πΎ)})(π‘€β€˜(β—‘(𝐹 ∘f + 𝐺) β€œ {𝑧})) ∈ (0[,)+∞))
268 eqid 2732 . . 3 (sigaGenβ€˜(TopOpenβ€˜πΎ)) = (sigaGenβ€˜(TopOpenβ€˜πΎ))
269 eqid 2732 . . 3 (0gβ€˜πΎ) = (0gβ€˜πΎ)
270 eqid 2732 . . 3 ( ·𝑠 β€˜πΎ) = ( ·𝑠 β€˜πΎ)
271 eqid 2732 . . 3 (ℝHomβ€˜(Scalarβ€˜πΎ)) = (ℝHomβ€˜(Scalarβ€˜πΎ))
27227, 28, 268, 269, 270, 271, 26, 16issibf 33320 . 2 (πœ‘ β†’ ((𝐹 ∘f + 𝐺) ∈ dom (𝐾sitg𝑀) ↔ ((𝐹 ∘f + 𝐺) ∈ (dom 𝑀MblFnM(sigaGenβ€˜(TopOpenβ€˜πΎ))) ∧ ran (𝐹 ∘f + 𝐺) ∈ Fin ∧ βˆ€π‘§ ∈ (ran (𝐹 ∘f + 𝐺) βˆ– {(0gβ€˜πΎ)})(π‘€β€˜(β—‘(𝐹 ∘f + 𝐺) β€œ {𝑧})) ∈ (0[,)+∞))))
273169, 137, 267, 272mpbir3and 1342 1 (πœ‘ β†’ (𝐹 ∘f + 𝐺) ∈ dom (𝐾sitg𝑀))
Colors of variables: wff setvar class
Syntax hints:  Β¬ wn 3   β†’ wi 4   ↔ wb 205   ∧ wa 396   ∨ wo 845   = wceq 1541   ∈ wcel 2106   β‰  wne 2940  βˆ€wral 3061  Vcvv 3474   βˆ– cdif 3944   βˆͺ cun 3945   ∩ cin 3946   βŠ† wss 3947  βˆ…c0 4321  {csn 4627  βŸ¨cop 4633  βˆͺ cuni 4907  βˆͺ ciun 4996  Disj wdisj 5112   class class class wbr 5147   Γ— cxp 5673  β—‘ccnv 5674  dom cdm 5675  ran crn 5676   β€œ cima 5678  Fun wfun 6534   Fn wfn 6535  βŸΆwf 6536  β€˜cfv 6540  (class class class)co 7405   ∘f cof 7664  Ο‰com 7851  1st c1st 7969  2nd c2nd 7970   ↑m cmap 8816   β‰Ό cdom 8933   β‰Ί csdm 8934  Fincfn 8935  β„cr 11105  0cc0 11106  +∞cpnf 11241   ≀ cle 11245  [,)cico 13322  Ξ£csu 15628  Basecbs 17140  Scalarcsca 17196   ·𝑠 cvsca 17197  TopOpenctopn 17363  0gc0g 17381  Topctop 22386  TopSpctps 22425  Clsdccld 22511  Frect1 22802  β„Homcrrh 32961  Ξ£*cesum 33013  sigAlgebracsiga 33094  sigaGencsigagen 33124  measurescmeas 33181  MblFnMcmbfm 33235  sitgcsitg 33316
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2703  ax-rep 5284  ax-sep 5298  ax-nul 5305  ax-pow 5362  ax-pr 5426  ax-un 7721  ax-inf2 9632  ax-ac2 10454  ax-cnex 11162  ax-resscn 11163  ax-1cn 11164  ax-icn 11165  ax-addcl 11166  ax-addrcl 11167  ax-mulcl 11168  ax-mulrcl 11169  ax-mulcom 11170  ax-addass 11171  ax-mulass 11172  ax-distr 11173  ax-i2m1 11174  ax-1ne0 11175  ax-1rid 11176  ax-rnegex 11177  ax-rrecex 11178  ax-cnre 11179  ax-pre-lttri 11180  ax-pre-lttrn 11181  ax-pre-ltadd 11182  ax-pre-mulgt0 11183  ax-pre-sup 11184  ax-addf 11185  ax-mulf 11186
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3or 1088  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2534  df-eu 2563  df-clab 2710  df-cleq 2724  df-clel 2810  df-nfc 2885  df-ne 2941  df-nel 3047  df-ral 3062  df-rex 3071  df-rmo 3376  df-reu 3377  df-rab 3433  df-v 3476  df-sbc 3777  df-csb 3893  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-pss 3966  df-nul 4322  df-if 4528  df-pw 4603  df-sn 4628  df-pr 4630  df-tp 4632  df-op 4634  df-uni 4908  df-int 4950  df-iun 4998  df-iin 4999  df-disj 5113  df-br 5148  df-opab 5210  df-mpt 5231  df-tr 5265  df-id 5573  df-eprel 5579  df-po 5587  df-so 5588  df-fr 5630  df-se 5631  df-we 5632  df-xp 5681  df-rel 5682  df-cnv 5683  df-co 5684  df-dm 5685  df-rn 5686  df-res 5687  df-ima 5688  df-pred 6297  df-ord 6364  df-on 6365  df-lim 6366  df-suc 6367  df-iota 6492  df-fun 6542  df-fn 6543  df-f 6544  df-f1 6545  df-fo 6546  df-f1o 6547  df-fv 6548  df-isom 6549  df-riota 7361  df-ov 7408  df-oprab 7409  df-mpo 7410  df-of 7666  df-om 7852  df-1st 7971  df-2nd 7972  df-supp 8143  df-frecs 8262  df-wrecs 8293  df-recs 8367  df-rdg 8406  df-1o 8462  df-2o 8463  df-er 8699  df-map 8818  df-pm 8819  df-ixp 8888  df-en 8936  df-dom 8937  df-sdom 8938  df-fin 8939  df-fsupp 9358  df-fi 9402  df-sup 9433  df-inf 9434  df-oi 9501  df-dju 9892  df-card 9930  df-acn 9933  df-ac 10107  df-pnf 11246  df-mnf 11247  df-xr 11248  df-ltxr 11249  df-le 11250  df-sub 11442  df-neg 11443  df-div 11868  df-nn 12209  df-2 12271  df-3 12272  df-4 12273  df-5 12274  df-6 12275  df-7 12276  df-8 12277  df-9 12278  df-n0 12469  df-z 12555  df-dec 12674  df-uz 12819  df-q 12929  df-rp 12971  df-xneg 13088  df-xadd 13089  df-xmul 13090  df-ioo 13324  df-ioc 13325  df-ico 13326  df-icc 13327  df-fz 13481  df-fzo 13624  df-fl 13753  df-mod 13831  df-seq 13963  df-exp 14024  df-fac 14230  df-bc 14259  df-hash 14287  df-shft 15010  df-cj 15042  df-re 15043  df-im 15044  df-sqrt 15178  df-abs 15179  df-limsup 15411  df-clim 15428  df-rlim 15429  df-sum 15629  df-ef 16007  df-sin 16009  df-cos 16010  df-pi 16012  df-struct 17076  df-sets 17093  df-slot 17111  df-ndx 17123  df-base 17141  df-ress 17170  df-plusg 17206  df-mulr 17207  df-starv 17208  df-sca 17209  df-vsca 17210  df-ip 17211  df-tset 17212  df-ple 17213  df-ds 17215  df-unif 17216  df-hom 17217  df-cco 17218  df-rest 17364  df-topn 17365  df-0g 17383  df-gsum 17384  df-topgen 17385  df-pt 17386  df-prds 17389  df-ordt 17443  df-xrs 17444  df-qtop 17449  df-imas 17450  df-xps 17452  df-mre 17526  df-mrc 17527  df-acs 17529  df-ps 18515  df-tsr 18516  df-plusf 18556  df-mgm 18557  df-sgrp 18606  df-mnd 18622  df-mhm 18667  df-submnd 18668  df-grp 18818  df-minusg 18819  df-sbg 18820  df-mulg 18945  df-subg 18997  df-cntz 19175  df-cmn 19644  df-abl 19645  df-mgp 19982  df-ur 19999  df-ring 20051  df-cring 20052  df-subrg 20353  df-abv 20417  df-lmod 20465  df-scaf 20466  df-sra 20777  df-rgmod 20778  df-psmet 20928  df-xmet 20929  df-met 20930  df-bl 20931  df-mopn 20932  df-fbas 20933  df-fg 20934  df-cnfld 20937  df-top 22387  df-topon 22404  df-topsp 22426  df-bases 22440  df-cld 22514  df-ntr 22515  df-cls 22516  df-nei 22593  df-lp 22631  df-perf 22632  df-cn 22722  df-cnp 22723  df-t1 22809  df-haus 22810  df-tx 23057  df-hmeo 23250  df-fil 23341  df-fm 23433  df-flim 23434  df-flf 23435  df-tmd 23567  df-tgp 23568  df-tsms 23622  df-trg 23655  df-xms 23817  df-ms 23818  df-tms 23819  df-nm 24082  df-ngp 24083  df-nrg 24085  df-nlm 24086  df-ii 24384  df-cncf 24385  df-limc 25374  df-dv 25375  df-log 26056  df-esum 33014  df-siga 33095  df-sigagen 33125  df-meas 33182  df-mbfm 33236  df-sitg 33317
This theorem is referenced by:  sitmcl  33338
  Copyright terms: Public domain W3C validator