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 32980
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 22301 . . . . . . . . . . 11 (π‘Š ∈ TopSp β†’ 𝐡 = βˆͺ 𝐽)
62, 5syl 17 . . . . . . . . . 10 (πœ‘ β†’ 𝐡 = βˆͺ 𝐽)
76sqxpeqd 5670 . . . . . . . . 9 (πœ‘ β†’ (𝐡 Γ— 𝐡) = (βˆͺ 𝐽 Γ— βˆͺ 𝐽))
87feq2d 6659 . . . . . . . 8 (πœ‘ β†’ ( + :(𝐡 Γ— 𝐡)⟢𝐢 ↔ + :(βˆͺ 𝐽 Γ— βˆͺ 𝐽)⟢𝐢))
91, 8mpbid 231 . . . . . . 7 (πœ‘ β†’ + :(βˆͺ 𝐽 Γ— βˆͺ 𝐽)⟢𝐢)
109fovcdmda 7530 . . . . . 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 32976 . . . . . 6 (πœ‘ β†’ 𝐹:βˆͺ dom π‘€βŸΆβˆͺ 𝐽)
19 sibfof.2 . . . . . . 7 (πœ‘ β†’ 𝐺 ∈ dom (π‘Šsitg𝑀))
203, 4, 11, 12, 13, 14, 15, 16, 19sibff 32976 . . . . . 6 (πœ‘ β†’ 𝐺:βˆͺ dom π‘€βŸΆβˆͺ 𝐽)
21 dmexg 7845 . . . . . . 7 (𝑀 ∈ βˆͺ ran measures β†’ dom 𝑀 ∈ V)
22 uniexg 7682 . . . . . . 7 (dom 𝑀 ∈ V β†’ βˆͺ dom 𝑀 ∈ V)
2316, 21, 223syl 18 . . . . . 6 (πœ‘ β†’ βˆͺ dom 𝑀 ∈ V)
24 inidm 4183 . . . . . 6 (βˆͺ dom 𝑀 ∩ βˆͺ dom 𝑀) = βˆͺ dom 𝑀
2510, 18, 20, 23, 23, 24off 7640 . . . . 5 (πœ‘ β†’ (𝐹 ∘f + 𝐺):βˆͺ dom π‘€βŸΆπΆ)
26 sibfof.3 . . . . . . . 8 (πœ‘ β†’ 𝐾 ∈ TopSp)
27 sibfof.c . . . . . . . . 9 𝐢 = (Baseβ€˜πΎ)
28 eqid 2737 . . . . . . . . 9 (TopOpenβ€˜πΎ) = (TopOpenβ€˜πΎ)
2927, 28tpsuni 22301 . . . . . . . 8 (𝐾 ∈ TopSp β†’ 𝐢 = βˆͺ (TopOpenβ€˜πΎ))
3026, 29syl 17 . . . . . . 7 (πœ‘ β†’ 𝐢 = βˆͺ (TopOpenβ€˜πΎ))
31 fvex 6860 . . . . . . . 8 (TopOpenβ€˜πΎ) ∈ V
32 unisg 32782 . . . . . . . 8 ((TopOpenβ€˜πΎ) ∈ V β†’ βˆͺ (sigaGenβ€˜(TopOpenβ€˜πΎ)) = βˆͺ (TopOpenβ€˜πΎ))
3331, 32ax-mp 5 . . . . . . 7 βˆͺ (sigaGenβ€˜(TopOpenβ€˜πΎ)) = βˆͺ (TopOpenβ€˜πΎ)
3430, 33eqtr4di 2795 . . . . . 6 (πœ‘ β†’ 𝐢 = βˆͺ (sigaGenβ€˜(TopOpenβ€˜πΎ)))
3534feq3d 6660 . . . . 5 (πœ‘ β†’ ((𝐹 ∘f + 𝐺):βˆͺ dom π‘€βŸΆπΆ ↔ (𝐹 ∘f + 𝐺):βˆͺ dom π‘€βŸΆβˆͺ (sigaGenβ€˜(TopOpenβ€˜πΎ))))
3625, 35mpbid 231 . . . 4 (πœ‘ β†’ (𝐹 ∘f + 𝐺):βˆͺ dom π‘€βŸΆβˆͺ (sigaGenβ€˜(TopOpenβ€˜πΎ)))
3731a1i 11 . . . . . . 7 (πœ‘ β†’ (TopOpenβ€˜πΎ) ∈ V)
3837sgsiga 32781 . . . . . 6 (πœ‘ β†’ (sigaGenβ€˜(TopOpenβ€˜πΎ)) ∈ βˆͺ ran sigAlgebra)
3938uniexd 7684 . . . . 5 (πœ‘ β†’ βˆͺ (sigaGenβ€˜(TopOpenβ€˜πΎ)) ∈ V)
4039, 23elmapd 8786 . . . 4 (πœ‘ β†’ ((𝐹 ∘f + 𝐺) ∈ (βˆͺ (sigaGenβ€˜(TopOpenβ€˜πΎ)) ↑m βˆͺ dom 𝑀) ↔ (𝐹 ∘f + 𝐺):βˆͺ dom π‘€βŸΆβˆͺ (sigaGenβ€˜(TopOpenβ€˜πΎ))))
4136, 40mpbird 257 . . 3 (πœ‘ β†’ (𝐹 ∘f + 𝐺) ∈ (βˆͺ (sigaGenβ€˜(TopOpenβ€˜πΎ)) ↑m βˆͺ dom 𝑀))
42 inundif 4443 . . . . . . 7 ((𝑏 ∩ ran (𝐹 ∘f + 𝐺)) βˆͺ (𝑏 βˆ– ran (𝐹 ∘f + 𝐺))) = 𝑏
4342imaeq2i 6016 . . . . . 6 (β—‘(𝐹 ∘f + 𝐺) β€œ ((𝑏 ∩ ran (𝐹 ∘f + 𝐺)) βˆͺ (𝑏 βˆ– ran (𝐹 ∘f + 𝐺)))) = (β—‘(𝐹 ∘f + 𝐺) β€œ 𝑏)
44 ffun 6676 . . . . . . . 8 ((𝐹 ∘f + 𝐺):βˆͺ dom π‘€βŸΆπΆ β†’ Fun (𝐹 ∘f + 𝐺))
45 unpreima 7018 . . . . . . . 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 482 . . . . . 6 ((πœ‘ ∧ 𝑏 ∈ (sigaGenβ€˜(TopOpenβ€˜πΎ))) β†’ (β—‘(𝐹 ∘f + 𝐺) β€œ ((𝑏 ∩ ran (𝐹 ∘f + 𝐺)) βˆͺ (𝑏 βˆ– ran (𝐹 ∘f + 𝐺)))) = ((β—‘(𝐹 ∘f + 𝐺) β€œ (𝑏 ∩ ran (𝐹 ∘f + 𝐺))) βˆͺ (β—‘(𝐹 ∘f + 𝐺) β€œ (𝑏 βˆ– ran (𝐹 ∘f + 𝐺)))))
4843, 47eqtr3id 2791 . . . . 5 ((πœ‘ ∧ 𝑏 ∈ (sigaGenβ€˜(TopOpenβ€˜πΎ))) β†’ (β—‘(𝐹 ∘f + 𝐺) β€œ 𝑏) = ((β—‘(𝐹 ∘f + 𝐺) β€œ (𝑏 ∩ ran (𝐹 ∘f + 𝐺))) βˆͺ (β—‘(𝐹 ∘f + 𝐺) β€œ (𝑏 βˆ– ran (𝐹 ∘f + 𝐺)))))
49 dmmeas 32840 . . . . . . . 8 (𝑀 ∈ βˆͺ ran measures β†’ dom 𝑀 ∈ βˆͺ ran sigAlgebra)
5016, 49syl 17 . . . . . . 7 (πœ‘ β†’ dom 𝑀 ∈ βˆͺ ran sigAlgebra)
5150adantr 482 . . . . . 6 ((πœ‘ ∧ 𝑏 ∈ (sigaGenβ€˜(TopOpenβ€˜πΎ))) β†’ dom 𝑀 ∈ βˆͺ ran sigAlgebra)
52 imaiun 7197 . . . . . . . 8 (β—‘(𝐹 ∘f + 𝐺) β€œ βˆͺ 𝑧 ∈ (𝑏 ∩ ran (𝐹 ∘f + 𝐺)){𝑧}) = βˆͺ 𝑧 ∈ (𝑏 ∩ ran (𝐹 ∘f + 𝐺))(β—‘(𝐹 ∘f + 𝐺) β€œ {𝑧})
53 iunid 5025 . . . . . . . . 9 βˆͺ 𝑧 ∈ (𝑏 ∩ ran (𝐹 ∘f + 𝐺)){𝑧} = (𝑏 ∩ ran (𝐹 ∘f + 𝐺))
5453imaeq2i 6016 . . . . . . . 8 (β—‘(𝐹 ∘f + 𝐺) β€œ βˆͺ 𝑧 ∈ (𝑏 ∩ ran (𝐹 ∘f + 𝐺)){𝑧}) = (β—‘(𝐹 ∘f + 𝐺) β€œ (𝑏 ∩ ran (𝐹 ∘f + 𝐺)))
5552, 54eqtr3i 2767 . . . . . . 7 βˆͺ 𝑧 ∈ (𝑏 ∩ ran (𝐹 ∘f + 𝐺))(β—‘(𝐹 ∘f + 𝐺) β€œ {𝑧}) = (β—‘(𝐹 ∘f + 𝐺) β€œ (𝑏 ∩ ran (𝐹 ∘f + 𝐺)))
56 inss2 4194 . . . . . . . . . 10 (𝑏 ∩ ran (𝐹 ∘f + 𝐺)) βŠ† ran (𝐹 ∘f + 𝐺)
576feq3d 6660 . . . . . . . . . . . . . . 15 (πœ‘ β†’ (𝐹:βˆͺ dom π‘€βŸΆπ΅ ↔ 𝐹:βˆͺ dom π‘€βŸΆβˆͺ 𝐽))
5818, 57mpbird 257 . . . . . . . . . . . . . 14 (πœ‘ β†’ 𝐹:βˆͺ dom π‘€βŸΆπ΅)
596feq3d 6660 . . . . . . . . . . . . . . 15 (πœ‘ β†’ (𝐺:βˆͺ dom π‘€βŸΆπ΅ ↔ 𝐺:βˆͺ dom π‘€βŸΆβˆͺ 𝐽))
6020, 59mpbird 257 . . . . . . . . . . . . . 14 (πœ‘ β†’ 𝐺:βˆͺ dom π‘€βŸΆπ΅)
611ffnd 6674 . . . . . . . . . . . . . 14 (πœ‘ β†’ + Fn (𝐡 Γ— 𝐡))
6258, 60, 23, 61ofpreima2 31624 . . . . . . . . . . . . 13 (πœ‘ β†’ (β—‘(𝐹 ∘f + 𝐺) β€œ {𝑧}) = βˆͺ 𝑝 ∈ ((β—‘ + β€œ {𝑧}) ∩ (ran 𝐹 Γ— ran 𝐺))((◑𝐹 β€œ {(1st β€˜π‘)}) ∩ (◑𝐺 β€œ {(2nd β€˜π‘)})))
6362adantr 482 . . . . . . . . . . . 12 ((πœ‘ ∧ 𝑧 ∈ ran (𝐹 ∘f + 𝐺)) β†’ (β—‘(𝐹 ∘f + 𝐺) β€œ {𝑧}) = βˆͺ 𝑝 ∈ ((β—‘ + β€œ {𝑧}) ∩ (ran 𝐹 Γ— ran 𝐺))((◑𝐹 β€œ {(1st β€˜π‘)}) ∩ (◑𝐺 β€œ {(2nd β€˜π‘)})))
6450adantr 482 . . . . . . . . . . . . 13 ((πœ‘ ∧ 𝑧 ∈ ran (𝐹 ∘f + 𝐺)) β†’ dom 𝑀 ∈ βˆͺ ran sigAlgebra)
6550ad2antrr 725 . . . . . . . . . . . . . . 15 (((πœ‘ ∧ 𝑧 ∈ ran (𝐹 ∘f + 𝐺)) ∧ 𝑝 ∈ ((β—‘ + β€œ {𝑧}) ∩ (ran 𝐹 Γ— ran 𝐺))) β†’ dom 𝑀 ∈ βˆͺ ran sigAlgebra)
66 simpll 766 . . . . . . . . . . . . . . . 16 (((πœ‘ ∧ 𝑧 ∈ ran (𝐹 ∘f + 𝐺)) ∧ 𝑝 ∈ ((β—‘ + β€œ {𝑧}) ∩ (ran 𝐹 Γ— ran 𝐺))) β†’ πœ‘)
67 inss1 4193 . . . . . . . . . . . . . . . . . 18 ((β—‘ + β€œ {𝑧}) ∩ (ran 𝐹 Γ— ran 𝐺)) βŠ† (β—‘ + β€œ {𝑧})
68 cnvimass 6038 . . . . . . . . . . . . . . . . . . . 20 (β—‘ + β€œ {𝑧}) βŠ† dom +
6968, 1fssdm 6693 . . . . . . . . . . . . . . . . . . 19 (πœ‘ β†’ (β—‘ + β€œ {𝑧}) βŠ† (𝐡 Γ— 𝐡))
7069adantr 482 . . . . . . . . . . . . . . . . . 18 ((πœ‘ ∧ 𝑧 ∈ ran (𝐹 ∘f + 𝐺)) β†’ (β—‘ + β€œ {𝑧}) βŠ† (𝐡 Γ— 𝐡))
7167, 70sstrid 3960 . . . . . . . . . . . . . . . . 17 ((πœ‘ ∧ 𝑧 ∈ ran (𝐹 ∘f + 𝐺)) β†’ ((β—‘ + β€œ {𝑧}) ∩ (ran 𝐹 Γ— ran 𝐺)) βŠ† (𝐡 Γ— 𝐡))
7271sselda 3949 . . . . . . . . . . . . . . . 16 (((πœ‘ ∧ 𝑧 ∈ ran (𝐹 ∘f + 𝐺)) ∧ 𝑝 ∈ ((β—‘ + β€œ {𝑧}) ∩ (ran 𝐹 Γ— ran 𝐺))) β†’ 𝑝 ∈ (𝐡 Γ— 𝐡))
7350adantr 482 . . . . . . . . . . . . . . . . 17 ((πœ‘ ∧ 𝑝 ∈ (𝐡 Γ— 𝐡)) β†’ dom 𝑀 ∈ βˆͺ ran sigAlgebra)
74 sibfof.4 . . . . . . . . . . . . . . . . . . . 20 (πœ‘ β†’ 𝐽 ∈ Fre)
7574sgsiga 32781 . . . . . . . . . . . . . . . . . . 19 (πœ‘ β†’ (sigaGenβ€˜π½) ∈ βˆͺ ran sigAlgebra)
7611, 75eqeltrid 2842 . . . . . . . . . . . . . . . . . 18 (πœ‘ β†’ 𝑆 ∈ βˆͺ ran sigAlgebra)
7776adantr 482 . . . . . . . . . . . . . . . . 17 ((πœ‘ ∧ 𝑝 ∈ (𝐡 Γ— 𝐡)) β†’ 𝑆 ∈ βˆͺ ran sigAlgebra)
783, 4, 11, 12, 13, 14, 15, 16, 17sibfmbl 32975 . . . . . . . . . . . . . . . . . 18 (πœ‘ β†’ 𝐹 ∈ (dom 𝑀MblFnM𝑆))
7978adantr 482 . . . . . . . . . . . . . . . . 17 ((πœ‘ ∧ 𝑝 ∈ (𝐡 Γ— 𝐡)) β†’ 𝐹 ∈ (dom 𝑀MblFnM𝑆))
804tpstop 22302 . . . . . . . . . . . . . . . . . . . . 21 (π‘Š ∈ TopSp β†’ 𝐽 ∈ Top)
81 cldssbrsiga 32826 . . . . . . . . . . . . . . . . . . . . 21 (𝐽 ∈ Top β†’ (Clsdβ€˜π½) βŠ† (sigaGenβ€˜π½))
822, 80, 813syl 18 . . . . . . . . . . . . . . . . . . . 20 (πœ‘ β†’ (Clsdβ€˜π½) βŠ† (sigaGenβ€˜π½))
8382adantr 482 . . . . . . . . . . . . . . . . . . 19 ((πœ‘ ∧ 𝑝 ∈ (𝐡 Γ— 𝐡)) β†’ (Clsdβ€˜π½) βŠ† (sigaGenβ€˜π½))
8474adantr 482 . . . . . . . . . . . . . . . . . . . 20 ((πœ‘ ∧ 𝑝 ∈ (𝐡 Γ— 𝐡)) β†’ 𝐽 ∈ Fre)
85 xp1st 7958 . . . . . . . . . . . . . . . . . . . . . 22 (𝑝 ∈ (𝐡 Γ— 𝐡) β†’ (1st β€˜π‘) ∈ 𝐡)
8685adantl 483 . . . . . . . . . . . . . . . . . . . . 21 ((πœ‘ ∧ 𝑝 ∈ (𝐡 Γ— 𝐡)) β†’ (1st β€˜π‘) ∈ 𝐡)
876adantr 482 . . . . . . . . . . . . . . . . . . . . 21 ((πœ‘ ∧ 𝑝 ∈ (𝐡 Γ— 𝐡)) β†’ 𝐡 = βˆͺ 𝐽)
8886, 87eleqtrd 2840 . . . . . . . . . . . . . . . . . . . 20 ((πœ‘ ∧ 𝑝 ∈ (𝐡 Γ— 𝐡)) β†’ (1st β€˜π‘) ∈ βˆͺ 𝐽)
89 eqid 2737 . . . . . . . . . . . . . . . . . . . . 21 βˆͺ 𝐽 = βˆͺ 𝐽
9089t1sncld 22693 . . . . . . . . . . . . . . . . . . . 20 ((𝐽 ∈ Fre ∧ (1st β€˜π‘) ∈ βˆͺ 𝐽) β†’ {(1st β€˜π‘)} ∈ (Clsdβ€˜π½))
9184, 88, 90syl2anc 585 . . . . . . . . . . . . . . . . . . 19 ((πœ‘ ∧ 𝑝 ∈ (𝐡 Γ— 𝐡)) β†’ {(1st β€˜π‘)} ∈ (Clsdβ€˜π½))
9283, 91sseldd 3950 . . . . . . . . . . . . . . . . . 18 ((πœ‘ ∧ 𝑝 ∈ (𝐡 Γ— 𝐡)) β†’ {(1st β€˜π‘)} ∈ (sigaGenβ€˜π½))
9392, 11eleqtrrdi 2849 . . . . . . . . . . . . . . . . 17 ((πœ‘ ∧ 𝑝 ∈ (𝐡 Γ— 𝐡)) β†’ {(1st β€˜π‘)} ∈ 𝑆)
9473, 77, 79, 93mbfmcnvima 32895 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ 𝑝 ∈ (𝐡 Γ— 𝐡)) β†’ (◑𝐹 β€œ {(1st β€˜π‘)}) ∈ dom 𝑀)
9566, 72, 94syl2anc 585 . . . . . . . . . . . . . . 15 (((πœ‘ ∧ 𝑧 ∈ ran (𝐹 ∘f + 𝐺)) ∧ 𝑝 ∈ ((β—‘ + β€œ {𝑧}) ∩ (ran 𝐹 Γ— ran 𝐺))) β†’ (◑𝐹 β€œ {(1st β€˜π‘)}) ∈ dom 𝑀)
963, 4, 11, 12, 13, 14, 15, 16, 19sibfmbl 32975 . . . . . . . . . . . . . . . . . 18 (πœ‘ β†’ 𝐺 ∈ (dom 𝑀MblFnM𝑆))
9796adantr 482 . . . . . . . . . . . . . . . . 17 ((πœ‘ ∧ 𝑝 ∈ (𝐡 Γ— 𝐡)) β†’ 𝐺 ∈ (dom 𝑀MblFnM𝑆))
98 xp2nd 7959 . . . . . . . . . . . . . . . . . . . . . 22 (𝑝 ∈ (𝐡 Γ— 𝐡) β†’ (2nd β€˜π‘) ∈ 𝐡)
9998adantl 483 . . . . . . . . . . . . . . . . . . . . 21 ((πœ‘ ∧ 𝑝 ∈ (𝐡 Γ— 𝐡)) β†’ (2nd β€˜π‘) ∈ 𝐡)
10099, 87eleqtrd 2840 . . . . . . . . . . . . . . . . . . . 20 ((πœ‘ ∧ 𝑝 ∈ (𝐡 Γ— 𝐡)) β†’ (2nd β€˜π‘) ∈ βˆͺ 𝐽)
10189t1sncld 22693 . . . . . . . . . . . . . . . . . . . 20 ((𝐽 ∈ Fre ∧ (2nd β€˜π‘) ∈ βˆͺ 𝐽) β†’ {(2nd β€˜π‘)} ∈ (Clsdβ€˜π½))
10284, 100, 101syl2anc 585 . . . . . . . . . . . . . . . . . . 19 ((πœ‘ ∧ 𝑝 ∈ (𝐡 Γ— 𝐡)) β†’ {(2nd β€˜π‘)} ∈ (Clsdβ€˜π½))
10383, 102sseldd 3950 . . . . . . . . . . . . . . . . . 18 ((πœ‘ ∧ 𝑝 ∈ (𝐡 Γ— 𝐡)) β†’ {(2nd β€˜π‘)} ∈ (sigaGenβ€˜π½))
104103, 11eleqtrrdi 2849 . . . . . . . . . . . . . . . . 17 ((πœ‘ ∧ 𝑝 ∈ (𝐡 Γ— 𝐡)) β†’ {(2nd β€˜π‘)} ∈ 𝑆)
10573, 77, 97, 104mbfmcnvima 32895 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ 𝑝 ∈ (𝐡 Γ— 𝐡)) β†’ (◑𝐺 β€œ {(2nd β€˜π‘)}) ∈ dom 𝑀)
10666, 72, 105syl2anc 585 . . . . . . . . . . . . . . 15 (((πœ‘ ∧ 𝑧 ∈ ran (𝐹 ∘f + 𝐺)) ∧ 𝑝 ∈ ((β—‘ + β€œ {𝑧}) ∩ (ran 𝐹 Γ— ran 𝐺))) β†’ (◑𝐺 β€œ {(2nd β€˜π‘)}) ∈ dom 𝑀)
107 inelsiga 32774 . . . . . . . . . . . . . . 15 ((dom 𝑀 ∈ βˆͺ ran sigAlgebra ∧ (◑𝐹 β€œ {(1st β€˜π‘)}) ∈ dom 𝑀 ∧ (◑𝐺 β€œ {(2nd β€˜π‘)}) ∈ dom 𝑀) β†’ ((◑𝐹 β€œ {(1st β€˜π‘)}) ∩ (◑𝐺 β€œ {(2nd β€˜π‘)})) ∈ dom 𝑀)
10865, 95, 106, 107syl3anc 1372 . . . . . . . . . . . . . 14 (((πœ‘ ∧ 𝑧 ∈ ran (𝐹 ∘f + 𝐺)) ∧ 𝑝 ∈ ((β—‘ + β€œ {𝑧}) ∩ (ran 𝐹 Γ— ran 𝐺))) β†’ ((◑𝐹 β€œ {(1st β€˜π‘)}) ∩ (◑𝐺 β€œ {(2nd β€˜π‘)})) ∈ dom 𝑀)
109108ralrimiva 3144 . . . . . . . . . . . . 13 ((πœ‘ ∧ 𝑧 ∈ ran (𝐹 ∘f + 𝐺)) β†’ βˆ€π‘ ∈ ((β—‘ + β€œ {𝑧}) ∩ (ran 𝐹 Γ— ran 𝐺))((◑𝐹 β€œ {(1st β€˜π‘)}) ∩ (◑𝐺 β€œ {(2nd β€˜π‘)})) ∈ dom 𝑀)
1103, 4, 11, 12, 13, 14, 15, 16, 17sibfrn 32977 . . . . . . . . . . . . . . . . 17 (πœ‘ β†’ ran 𝐹 ∈ Fin)
1113, 4, 11, 12, 13, 14, 15, 16, 19sibfrn 32977 . . . . . . . . . . . . . . . . 17 (πœ‘ β†’ ran 𝐺 ∈ Fin)
112 xpfi 9268 . . . . . . . . . . . . . . . . 17 ((ran 𝐹 ∈ Fin ∧ ran 𝐺 ∈ Fin) β†’ (ran 𝐹 Γ— ran 𝐺) ∈ Fin)
113110, 111, 112syl2anc 585 . . . . . . . . . . . . . . . 16 (πœ‘ β†’ (ran 𝐹 Γ— ran 𝐺) ∈ Fin)
114 inss2 4194 . . . . . . . . . . . . . . . 16 ((β—‘ + β€œ {𝑧}) ∩ (ran 𝐹 Γ— ran 𝐺)) βŠ† (ran 𝐹 Γ— ran 𝐺)
115 ssdomg 8947 . . . . . . . . . . . . . . . 16 ((ran 𝐹 Γ— ran 𝐺) ∈ Fin β†’ (((β—‘ + β€œ {𝑧}) ∩ (ran 𝐹 Γ— ran 𝐺)) βŠ† (ran 𝐹 Γ— ran 𝐺) β†’ ((β—‘ + β€œ {𝑧}) ∩ (ran 𝐹 Γ— ran 𝐺)) β‰Ό (ran 𝐹 Γ— ran 𝐺)))
116113, 114, 115mpisyl 21 . . . . . . . . . . . . . . 15 (πœ‘ β†’ ((β—‘ + β€œ {𝑧}) ∩ (ran 𝐹 Γ— ran 𝐺)) β‰Ό (ran 𝐹 Γ— ran 𝐺))
117 isfinite 9595 . . . . . . . . . . . . . . . . 17 ((ran 𝐹 Γ— ran 𝐺) ∈ Fin ↔ (ran 𝐹 Γ— ran 𝐺) β‰Ί Ο‰)
118117biimpi 215 . . . . . . . . . . . . . . . 16 ((ran 𝐹 Γ— ran 𝐺) ∈ Fin β†’ (ran 𝐹 Γ— ran 𝐺) β‰Ί Ο‰)
119 sdomdom 8927 . . . . . . . . . . . . . . . 16 ((ran 𝐹 Γ— ran 𝐺) β‰Ί Ο‰ β†’ (ran 𝐹 Γ— ran 𝐺) β‰Ό Ο‰)
120113, 118, 1193syl 18 . . . . . . . . . . . . . . 15 (πœ‘ β†’ (ran 𝐹 Γ— ran 𝐺) β‰Ό Ο‰)
121 domtr 8954 . . . . . . . . . . . . . . 15 ((((β—‘ + β€œ {𝑧}) ∩ (ran 𝐹 Γ— ran 𝐺)) β‰Ό (ran 𝐹 Γ— ran 𝐺) ∧ (ran 𝐹 Γ— ran 𝐺) β‰Ό Ο‰) β†’ ((β—‘ + β€œ {𝑧}) ∩ (ran 𝐹 Γ— ran 𝐺)) β‰Ό Ο‰)
122116, 120, 121syl2anc 585 . . . . . . . . . . . . . 14 (πœ‘ β†’ ((β—‘ + β€œ {𝑧}) ∩ (ran 𝐹 Γ— ran 𝐺)) β‰Ό Ο‰)
123122adantr 482 . . . . . . . . . . . . 13 ((πœ‘ ∧ 𝑧 ∈ ran (𝐹 ∘f + 𝐺)) β†’ ((β—‘ + β€œ {𝑧}) ∩ (ran 𝐹 Γ— ran 𝐺)) β‰Ό Ο‰)
124 nfcv 2908 . . . . . . . . . . . . . 14 Ⅎ𝑝((β—‘ + β€œ {𝑧}) ∩ (ran 𝐹 Γ— ran 𝐺))
125124sigaclcuni 32757 . . . . . . . . . . . . 13 ((dom 𝑀 ∈ βˆͺ ran sigAlgebra ∧ βˆ€π‘ ∈ ((β—‘ + β€œ {𝑧}) ∩ (ran 𝐹 Γ— ran 𝐺))((◑𝐹 β€œ {(1st β€˜π‘)}) ∩ (◑𝐺 β€œ {(2nd β€˜π‘)})) ∈ dom 𝑀 ∧ ((β—‘ + β€œ {𝑧}) ∩ (ran 𝐹 Γ— ran 𝐺)) β‰Ό Ο‰) β†’ βˆͺ 𝑝 ∈ ((β—‘ + β€œ {𝑧}) ∩ (ran 𝐹 Γ— ran 𝐺))((◑𝐹 β€œ {(1st β€˜π‘)}) ∩ (◑𝐺 β€œ {(2nd β€˜π‘)})) ∈ dom 𝑀)
12664, 109, 123, 125syl3anc 1372 . . . . . . . . . . . 12 ((πœ‘ ∧ 𝑧 ∈ ran (𝐹 ∘f + 𝐺)) β†’ βˆͺ 𝑝 ∈ ((β—‘ + β€œ {𝑧}) ∩ (ran 𝐹 Γ— ran 𝐺))((◑𝐹 β€œ {(1st β€˜π‘)}) ∩ (◑𝐺 β€œ {(2nd β€˜π‘)})) ∈ dom 𝑀)
12763, 126eqeltrd 2838 . . . . . . . . . . 11 ((πœ‘ ∧ 𝑧 ∈ ran (𝐹 ∘f + 𝐺)) β†’ (β—‘(𝐹 ∘f + 𝐺) β€œ {𝑧}) ∈ dom 𝑀)
128127ralrimiva 3144 . . . . . . . . . 10 (πœ‘ β†’ βˆ€π‘§ ∈ ran (𝐹 ∘f + 𝐺)(β—‘(𝐹 ∘f + 𝐺) β€œ {𝑧}) ∈ dom 𝑀)
129 ssralv 4015 . . . . . . . . . 10 ((𝑏 ∩ ran (𝐹 ∘f + 𝐺)) βŠ† ran (𝐹 ∘f + 𝐺) β†’ (βˆ€π‘§ ∈ ran (𝐹 ∘f + 𝐺)(β—‘(𝐹 ∘f + 𝐺) β€œ {𝑧}) ∈ dom 𝑀 β†’ βˆ€π‘§ ∈ (𝑏 ∩ ran (𝐹 ∘f + 𝐺))(β—‘(𝐹 ∘f + 𝐺) β€œ {𝑧}) ∈ dom 𝑀))
13056, 128, 129mpsyl 68 . . . . . . . . 9 (πœ‘ β†’ βˆ€π‘§ ∈ (𝑏 ∩ ran (𝐹 ∘f + 𝐺))(β—‘(𝐹 ∘f + 𝐺) β€œ {𝑧}) ∈ dom 𝑀)
131130adantr 482 . . . . . . . 8 ((πœ‘ ∧ 𝑏 ∈ (sigaGenβ€˜(TopOpenβ€˜πΎ))) β†’ βˆ€π‘§ ∈ (𝑏 ∩ ran (𝐹 ∘f + 𝐺))(β—‘(𝐹 ∘f + 𝐺) β€œ {𝑧}) ∈ dom 𝑀)
1321ffund 6677 . . . . . . . . . . . . 13 (πœ‘ β†’ Fun + )
133 imafi 9126 . . . . . . . . . . . . 13 ((Fun + ∧ (ran 𝐹 Γ— ran 𝐺) ∈ Fin) β†’ ( + β€œ (ran 𝐹 Γ— ran 𝐺)) ∈ Fin)
134132, 113, 133syl2anc 585 . . . . . . . . . . . 12 (πœ‘ β†’ ( + β€œ (ran 𝐹 Γ— ran 𝐺)) ∈ Fin)
13518, 20, 9, 23ofrn2 31598 . . . . . . . . . . . 12 (πœ‘ β†’ ran (𝐹 ∘f + 𝐺) βŠ† ( + β€œ (ran 𝐹 Γ— ran 𝐺)))
136 ssfi 9124 . . . . . . . . . . . 12 ((( + β€œ (ran 𝐹 Γ— ran 𝐺)) ∈ Fin ∧ ran (𝐹 ∘f + 𝐺) βŠ† ( + β€œ (ran 𝐹 Γ— ran 𝐺))) β†’ ran (𝐹 ∘f + 𝐺) ∈ Fin)
137134, 135, 136syl2anc 585 . . . . . . . . . . 11 (πœ‘ β†’ ran (𝐹 ∘f + 𝐺) ∈ Fin)
138 ssdomg 8947 . . . . . . . . . . 11 (ran (𝐹 ∘f + 𝐺) ∈ Fin β†’ ((𝑏 ∩ ran (𝐹 ∘f + 𝐺)) βŠ† ran (𝐹 ∘f + 𝐺) β†’ (𝑏 ∩ ran (𝐹 ∘f + 𝐺)) β‰Ό ran (𝐹 ∘f + 𝐺)))
139137, 56, 138mpisyl 21 . . . . . . . . . 10 (πœ‘ β†’ (𝑏 ∩ ran (𝐹 ∘f + 𝐺)) β‰Ό ran (𝐹 ∘f + 𝐺))
140 isfinite 9595 . . . . . . . . . . . 12 (ran (𝐹 ∘f + 𝐺) ∈ Fin ↔ ran (𝐹 ∘f + 𝐺) β‰Ί Ο‰)
141137, 140sylib 217 . . . . . . . . . . 11 (πœ‘ β†’ ran (𝐹 ∘f + 𝐺) β‰Ί Ο‰)
142 sdomdom 8927 . . . . . . . . . . 11 (ran (𝐹 ∘f + 𝐺) β‰Ί Ο‰ β†’ ran (𝐹 ∘f + 𝐺) β‰Ό Ο‰)
143141, 142syl 17 . . . . . . . . . 10 (πœ‘ β†’ ran (𝐹 ∘f + 𝐺) β‰Ό Ο‰)
144 domtr 8954 . . . . . . . . . 10 (((𝑏 ∩ ran (𝐹 ∘f + 𝐺)) β‰Ό ran (𝐹 ∘f + 𝐺) ∧ ran (𝐹 ∘f + 𝐺) β‰Ό Ο‰) β†’ (𝑏 ∩ ran (𝐹 ∘f + 𝐺)) β‰Ό Ο‰)
145139, 143, 144syl2anc 585 . . . . . . . . 9 (πœ‘ β†’ (𝑏 ∩ ran (𝐹 ∘f + 𝐺)) β‰Ό Ο‰)
146145adantr 482 . . . . . . . 8 ((πœ‘ ∧ 𝑏 ∈ (sigaGenβ€˜(TopOpenβ€˜πΎ))) β†’ (𝑏 ∩ ran (𝐹 ∘f + 𝐺)) β‰Ό Ο‰)
147 nfcv 2908 . . . . . . . . 9 Ⅎ𝑧(𝑏 ∩ ran (𝐹 ∘f + 𝐺))
148147sigaclcuni 32757 . . . . . . . 8 ((dom 𝑀 ∈ βˆͺ ran sigAlgebra ∧ βˆ€π‘§ ∈ (𝑏 ∩ ran (𝐹 ∘f + 𝐺))(β—‘(𝐹 ∘f + 𝐺) β€œ {𝑧}) ∈ dom 𝑀 ∧ (𝑏 ∩ ran (𝐹 ∘f + 𝐺)) β‰Ό Ο‰) β†’ βˆͺ 𝑧 ∈ (𝑏 ∩ ran (𝐹 ∘f + 𝐺))(β—‘(𝐹 ∘f + 𝐺) β€œ {𝑧}) ∈ dom 𝑀)
14951, 131, 146, 148syl3anc 1372 . . . . . . 7 ((πœ‘ ∧ 𝑏 ∈ (sigaGenβ€˜(TopOpenβ€˜πΎ))) β†’ βˆͺ 𝑧 ∈ (𝑏 ∩ ran (𝐹 ∘f + 𝐺))(β—‘(𝐹 ∘f + 𝐺) β€œ {𝑧}) ∈ dom 𝑀)
15055, 149eqeltrrid 2843 . . . . . 6 ((πœ‘ ∧ 𝑏 ∈ (sigaGenβ€˜(TopOpenβ€˜πΎ))) β†’ (β—‘(𝐹 ∘f + 𝐺) β€œ (𝑏 ∩ ran (𝐹 ∘f + 𝐺))) ∈ dom 𝑀)
151 difpreima 7020 . . . . . . . . . 10 (Fun (𝐹 ∘f + 𝐺) β†’ (β—‘(𝐹 ∘f + 𝐺) β€œ (𝑏 βˆ– ran (𝐹 ∘f + 𝐺))) = ((β—‘(𝐹 ∘f + 𝐺) β€œ 𝑏) βˆ– (β—‘(𝐹 ∘f + 𝐺) β€œ ran (𝐹 ∘f + 𝐺))))
15225, 44, 1513syl 18 . . . . . . . . 9 (πœ‘ β†’ (β—‘(𝐹 ∘f + 𝐺) β€œ (𝑏 βˆ– ran (𝐹 ∘f + 𝐺))) = ((β—‘(𝐹 ∘f + 𝐺) β€œ 𝑏) βˆ– (β—‘(𝐹 ∘f + 𝐺) β€œ ran (𝐹 ∘f + 𝐺))))
153 cnvimarndm 6039 . . . . . . . . . . 11 (β—‘(𝐹 ∘f + 𝐺) β€œ ran (𝐹 ∘f + 𝐺)) = dom (𝐹 ∘f + 𝐺)
154153difeq2i 4084 . . . . . . . . . 10 ((β—‘(𝐹 ∘f + 𝐺) β€œ 𝑏) βˆ– (β—‘(𝐹 ∘f + 𝐺) β€œ ran (𝐹 ∘f + 𝐺))) = ((β—‘(𝐹 ∘f + 𝐺) β€œ 𝑏) βˆ– dom (𝐹 ∘f + 𝐺))
155 cnvimass 6038 . . . . . . . . . . 11 (β—‘(𝐹 ∘f + 𝐺) β€œ 𝑏) βŠ† dom (𝐹 ∘f + 𝐺)
156 ssdif0 4328 . . . . . . . . . . 11 ((β—‘(𝐹 ∘f + 𝐺) β€œ 𝑏) βŠ† dom (𝐹 ∘f + 𝐺) ↔ ((β—‘(𝐹 ∘f + 𝐺) β€œ 𝑏) βˆ– dom (𝐹 ∘f + 𝐺)) = βˆ…)
157155, 156mpbi 229 . . . . . . . . . 10 ((β—‘(𝐹 ∘f + 𝐺) β€œ 𝑏) βˆ– dom (𝐹 ∘f + 𝐺)) = βˆ…
158154, 157eqtri 2765 . . . . . . . . 9 ((β—‘(𝐹 ∘f + 𝐺) β€œ 𝑏) βˆ– (β—‘(𝐹 ∘f + 𝐺) β€œ ran (𝐹 ∘f + 𝐺))) = βˆ…
159152, 158eqtrdi 2793 . . . . . . . 8 (πœ‘ β†’ (β—‘(𝐹 ∘f + 𝐺) β€œ (𝑏 βˆ– ran (𝐹 ∘f + 𝐺))) = βˆ…)
160 0elsiga 32753 . . . . . . . . 9 (dom 𝑀 ∈ βˆͺ ran sigAlgebra β†’ βˆ… ∈ dom 𝑀)
16116, 49, 1603syl 18 . . . . . . . 8 (πœ‘ β†’ βˆ… ∈ dom 𝑀)
162159, 161eqeltrd 2838 . . . . . . 7 (πœ‘ β†’ (β—‘(𝐹 ∘f + 𝐺) β€œ (𝑏 βˆ– ran (𝐹 ∘f + 𝐺))) ∈ dom 𝑀)
163162adantr 482 . . . . . 6 ((πœ‘ ∧ 𝑏 ∈ (sigaGenβ€˜(TopOpenβ€˜πΎ))) β†’ (β—‘(𝐹 ∘f + 𝐺) β€œ (𝑏 βˆ– ran (𝐹 ∘f + 𝐺))) ∈ dom 𝑀)
164 unelsiga 32773 . . . . . 6 ((dom 𝑀 ∈ βˆͺ ran sigAlgebra ∧ (β—‘(𝐹 ∘f + 𝐺) β€œ (𝑏 ∩ ran (𝐹 ∘f + 𝐺))) ∈ dom 𝑀 ∧ (β—‘(𝐹 ∘f + 𝐺) β€œ (𝑏 βˆ– ran (𝐹 ∘f + 𝐺))) ∈ dom 𝑀) β†’ ((β—‘(𝐹 ∘f + 𝐺) β€œ (𝑏 ∩ ran (𝐹 ∘f + 𝐺))) βˆͺ (β—‘(𝐹 ∘f + 𝐺) β€œ (𝑏 βˆ– ran (𝐹 ∘f + 𝐺)))) ∈ dom 𝑀)
16551, 150, 163, 164syl3anc 1372 . . . . 5 ((πœ‘ ∧ 𝑏 ∈ (sigaGenβ€˜(TopOpenβ€˜πΎ))) β†’ ((β—‘(𝐹 ∘f + 𝐺) β€œ (𝑏 ∩ ran (𝐹 ∘f + 𝐺))) βˆͺ (β—‘(𝐹 ∘f + 𝐺) β€œ (𝑏 βˆ– ran (𝐹 ∘f + 𝐺)))) ∈ dom 𝑀)
16648, 165eqeltrd 2838 . . . 4 ((πœ‘ ∧ 𝑏 ∈ (sigaGenβ€˜(TopOpenβ€˜πΎ))) β†’ (β—‘(𝐹 ∘f + 𝐺) β€œ 𝑏) ∈ dom 𝑀)
167166ralrimiva 3144 . . 3 (πœ‘ β†’ βˆ€π‘ ∈ (sigaGenβ€˜(TopOpenβ€˜πΎ))(β—‘(𝐹 ∘f + 𝐺) β€œ 𝑏) ∈ dom 𝑀)
16850, 38ismbfm 32890 . . 3 (πœ‘ β†’ ((𝐹 ∘f + 𝐺) ∈ (dom 𝑀MblFnM(sigaGenβ€˜(TopOpenβ€˜πΎ))) ↔ ((𝐹 ∘f + 𝐺) ∈ (βˆͺ (sigaGenβ€˜(TopOpenβ€˜πΎ)) ↑m βˆͺ dom 𝑀) ∧ βˆ€π‘ ∈ (sigaGenβ€˜(TopOpenβ€˜πΎ))(β—‘(𝐹 ∘f + 𝐺) β€œ 𝑏) ∈ dom 𝑀)))
16941, 167, 168mpbir2and 712 . 2 (πœ‘ β†’ (𝐹 ∘f + 𝐺) ∈ (dom 𝑀MblFnM(sigaGenβ€˜(TopOpenβ€˜πΎ))))
17062adantr 482 . . . . . . 7 ((πœ‘ ∧ 𝑧 ∈ (ran (𝐹 ∘f + 𝐺) βˆ– {(0gβ€˜πΎ)})) β†’ (β—‘(𝐹 ∘f + 𝐺) β€œ {𝑧}) = βˆͺ 𝑝 ∈ ((β—‘ + β€œ {𝑧}) ∩ (ran 𝐹 Γ— ran 𝐺))((◑𝐹 β€œ {(1st β€˜π‘)}) ∩ (◑𝐺 β€œ {(2nd β€˜π‘)})))
171170fveq2d 6851 . . . . . 6 ((πœ‘ ∧ 𝑧 ∈ (ran (𝐹 ∘f + 𝐺) βˆ– {(0gβ€˜πΎ)})) β†’ (π‘€β€˜(β—‘(𝐹 ∘f + 𝐺) β€œ {𝑧})) = (π‘€β€˜βˆͺ 𝑝 ∈ ((β—‘ + β€œ {𝑧}) ∩ (ran 𝐹 Γ— ran 𝐺))((◑𝐹 β€œ {(1st β€˜π‘)}) ∩ (◑𝐺 β€œ {(2nd β€˜π‘)}))))
172 measbasedom 32841 . . . . . . . . 9 (𝑀 ∈ βˆͺ ran measures ↔ 𝑀 ∈ (measuresβ€˜dom 𝑀))
17316, 172sylib 217 . . . . . . . 8 (πœ‘ β†’ 𝑀 ∈ (measuresβ€˜dom 𝑀))
174173adantr 482 . . . . . . 7 ((πœ‘ ∧ 𝑧 ∈ (ran (𝐹 ∘f + 𝐺) βˆ– {(0gβ€˜πΎ)})) β†’ 𝑀 ∈ (measuresβ€˜dom 𝑀))
175 eldifi 4091 . . . . . . . 8 (𝑧 ∈ (ran (𝐹 ∘f + 𝐺) βˆ– {(0gβ€˜πΎ)}) β†’ 𝑧 ∈ ran (𝐹 ∘f + 𝐺))
176175, 109sylan2 594 . . . . . . 7 ((πœ‘ ∧ 𝑧 ∈ (ran (𝐹 ∘f + 𝐺) βˆ– {(0gβ€˜πΎ)})) β†’ βˆ€π‘ ∈ ((β—‘ + β€œ {𝑧}) ∩ (ran 𝐹 Γ— ran 𝐺))((◑𝐹 β€œ {(1st β€˜π‘)}) ∩ (◑𝐺 β€œ {(2nd β€˜π‘)})) ∈ dom 𝑀)
177122adantr 482 . . . . . . 7 ((πœ‘ ∧ 𝑧 ∈ (ran (𝐹 ∘f + 𝐺) βˆ– {(0gβ€˜πΎ)})) β†’ ((β—‘ + β€œ {𝑧}) ∩ (ran 𝐹 Γ— ran 𝐺)) β‰Ό Ο‰)
178 sneq 4601 . . . . . . . . . . 11 (π‘₯ = (1st β€˜π‘) β†’ {π‘₯} = {(1st β€˜π‘)})
179178imaeq2d 6018 . . . . . . . . . 10 (π‘₯ = (1st β€˜π‘) β†’ (◑𝐹 β€œ {π‘₯}) = (◑𝐹 β€œ {(1st β€˜π‘)}))
180 sneq 4601 . . . . . . . . . . 11 (𝑦 = (2nd β€˜π‘) β†’ {𝑦} = {(2nd β€˜π‘)})
181180imaeq2d 6018 . . . . . . . . . 10 (𝑦 = (2nd β€˜π‘) β†’ (◑𝐺 β€œ {𝑦}) = (◑𝐺 β€œ {(2nd β€˜π‘)}))
18218ffund 6677 . . . . . . . . . . 11 (πœ‘ β†’ Fun 𝐹)
183 sndisj 5101 . . . . . . . . . . 11 Disj π‘₯ ∈ ran 𝐹{π‘₯}
184 disjpreima 31544 . . . . . . . . . . 11 ((Fun 𝐹 ∧ Disj π‘₯ ∈ ran 𝐹{π‘₯}) β†’ Disj π‘₯ ∈ ran 𝐹(◑𝐹 β€œ {π‘₯}))
185182, 183, 184sylancl 587 . . . . . . . . . 10 (πœ‘ β†’ Disj π‘₯ ∈ ran 𝐹(◑𝐹 β€œ {π‘₯}))
18620ffund 6677 . . . . . . . . . . 11 (πœ‘ β†’ Fun 𝐺)
187 sndisj 5101 . . . . . . . . . . 11 Disj 𝑦 ∈ ran 𝐺{𝑦}
188 disjpreima 31544 . . . . . . . . . . 11 ((Fun 𝐺 ∧ Disj 𝑦 ∈ ran 𝐺{𝑦}) β†’ Disj 𝑦 ∈ ran 𝐺(◑𝐺 β€œ {𝑦}))
189186, 187, 188sylancl 587 . . . . . . . . . 10 (πœ‘ β†’ Disj 𝑦 ∈ ran 𝐺(◑𝐺 β€œ {𝑦}))
190179, 181, 185, 189disjxpin 31548 . . . . . . . . 9 (πœ‘ β†’ Disj 𝑝 ∈ (ran 𝐹 Γ— ran 𝐺)((◑𝐹 β€œ {(1st β€˜π‘)}) ∩ (◑𝐺 β€œ {(2nd β€˜π‘)})))
191 disjss1 5081 . . . . . . . . 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 482 . . . . . . 7 ((πœ‘ ∧ 𝑧 ∈ (ran (𝐹 ∘f + 𝐺) βˆ– {(0gβ€˜πΎ)})) β†’ Disj 𝑝 ∈ ((β—‘ + β€œ {𝑧}) ∩ (ran 𝐹 Γ— ran 𝐺))((◑𝐹 β€œ {(1st β€˜π‘)}) ∩ (◑𝐺 β€œ {(2nd β€˜π‘)})))
194 measvuni 32853 . . . . . . 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 1375 . . . . . 6 ((πœ‘ ∧ 𝑧 ∈ (ran (𝐹 ∘f + 𝐺) βˆ– {(0gβ€˜πΎ)})) β†’ (π‘€β€˜βˆͺ 𝑝 ∈ ((β—‘ + β€œ {𝑧}) ∩ (ran 𝐹 Γ— ran 𝐺))((◑𝐹 β€œ {(1st β€˜π‘)}) ∩ (◑𝐺 β€œ {(2nd β€˜π‘)}))) = Ξ£*𝑝 ∈ ((β—‘ + β€œ {𝑧}) ∩ (ran 𝐹 Γ— ran 𝐺))(π‘€β€˜((◑𝐹 β€œ {(1st β€˜π‘)}) ∩ (◑𝐺 β€œ {(2nd β€˜π‘)}))))
196 ssfi 9124 . . . . . . . . 9 (((ran 𝐹 Γ— ran 𝐺) ∈ Fin ∧ ((β—‘ + β€œ {𝑧}) ∩ (ran 𝐹 Γ— ran 𝐺)) βŠ† (ran 𝐹 Γ— ran 𝐺)) β†’ ((β—‘ + β€œ {𝑧}) ∩ (ran 𝐹 Γ— ran 𝐺)) ∈ Fin)
197113, 114, 196sylancl 587 . . . . . . . 8 (πœ‘ β†’ ((β—‘ + β€œ {𝑧}) ∩ (ran 𝐹 Γ— ran 𝐺)) ∈ Fin)
198197adantr 482 . . . . . . 7 ((πœ‘ ∧ 𝑧 ∈ (ran (𝐹 ∘f + 𝐺) βˆ– {(0gβ€˜πΎ)})) β†’ ((β—‘ + β€œ {𝑧}) ∩ (ran 𝐹 Γ— ran 𝐺)) ∈ Fin)
199 simpll 766 . . . . . . . 8 (((πœ‘ ∧ 𝑧 ∈ (ran (𝐹 ∘f + 𝐺) βˆ– {(0gβ€˜πΎ)})) ∧ 𝑝 ∈ ((β—‘ + β€œ {𝑧}) ∩ (ran 𝐹 Γ— ran 𝐺))) β†’ πœ‘)
200 simpr 486 . . . . . . . . . 10 (((πœ‘ ∧ 𝑧 ∈ (ran (𝐹 ∘f + 𝐺) βˆ– {(0gβ€˜πΎ)})) ∧ 𝑝 ∈ ((β—‘ + β€œ {𝑧}) ∩ (ran 𝐹 Γ— ran 𝐺))) β†’ 𝑝 ∈ ((β—‘ + β€œ {𝑧}) ∩ (ran 𝐹 Γ— ran 𝐺)))
201114, 200sselid 3947 . . . . . . . . 9 (((πœ‘ ∧ 𝑧 ∈ (ran (𝐹 ∘f + 𝐺) βˆ– {(0gβ€˜πΎ)})) ∧ 𝑝 ∈ ((β—‘ + β€œ {𝑧}) ∩ (ran 𝐹 Γ— ran 𝐺))) β†’ 𝑝 ∈ (ran 𝐹 Γ— ran 𝐺))
202 xp1st 7958 . . . . . . . . 9 (𝑝 ∈ (ran 𝐹 Γ— ran 𝐺) β†’ (1st β€˜π‘) ∈ ran 𝐹)
203201, 202syl 17 . . . . . . . 8 (((πœ‘ ∧ 𝑧 ∈ (ran (𝐹 ∘f + 𝐺) βˆ– {(0gβ€˜πΎ)})) ∧ 𝑝 ∈ ((β—‘ + β€œ {𝑧}) ∩ (ran 𝐹 Γ— ran 𝐺))) β†’ (1st β€˜π‘) ∈ ran 𝐹)
204 xp2nd 7959 . . . . . . . . 9 (𝑝 ∈ (ran 𝐹 Γ— ran 𝐺) β†’ (2nd β€˜π‘) ∈ ran 𝐺)
205201, 204syl 17 . . . . . . . 8 (((πœ‘ ∧ 𝑧 ∈ (ran (𝐹 ∘f + 𝐺) βˆ– {(0gβ€˜πΎ)})) ∧ 𝑝 ∈ ((β—‘ + β€œ {𝑧}) ∩ (ran 𝐹 Γ— ran 𝐺))) β†’ (2nd β€˜π‘) ∈ ran 𝐺)
206 oveq12 7371 . . . . . . . . . . . . . . . 16 ((π‘₯ = 0 ∧ 𝑦 = 0 ) β†’ (π‘₯ + 𝑦) = ( 0 + 0 ))
207 sibfof.5 . . . . . . . . . . . . . . . 16 (πœ‘ β†’ ( 0 + 0 ) = (0gβ€˜πΎ))
208206, 207sylan9eqr 2799 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ (π‘₯ = 0 ∧ 𝑦 = 0 )) β†’ (π‘₯ + 𝑦) = (0gβ€˜πΎ))
209208ex 414 . . . . . . . . . . . . . 14 (πœ‘ β†’ ((π‘₯ = 0 ∧ 𝑦 = 0 ) β†’ (π‘₯ + 𝑦) = (0gβ€˜πΎ)))
210209necon3ad 2957 . . . . . . . . . . . . 13 (πœ‘ β†’ ((π‘₯ + 𝑦) β‰  (0gβ€˜πΎ) β†’ Β¬ (π‘₯ = 0 ∧ 𝑦 = 0 )))
211 neorian 3040 . . . . . . . . . . . . 13 ((π‘₯ β‰  0 ∨ 𝑦 β‰  0 ) ↔ Β¬ (π‘₯ = 0 ∧ 𝑦 = 0 ))
212210, 211syl6ibr 252 . . . . . . . . . . . 12 (πœ‘ β†’ ((π‘₯ + 𝑦) β‰  (0gβ€˜πΎ) β†’ (π‘₯ β‰  0 ∨ 𝑦 β‰  0 )))
213212adantr 482 . . . . . . . . . . 11 ((πœ‘ ∧ (π‘₯ ∈ 𝐡 ∧ 𝑦 ∈ 𝐡)) β†’ ((π‘₯ + 𝑦) β‰  (0gβ€˜πΎ) β†’ (π‘₯ β‰  0 ∨ 𝑦 β‰  0 )))
214213ralrimivva 3198 . . . . . . . . . 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 3949 . . . . . . . . . . . 12 (((πœ‘ ∧ 𝑧 ∈ (ran (𝐹 ∘f + 𝐺) βˆ– {(0gβ€˜πΎ)})) ∧ 𝑝 ∈ ((β—‘ + β€œ {𝑧}) ∩ (ran 𝐹 Γ— ran 𝐺))) β†’ 𝑝 ∈ (β—‘ + β€œ {𝑧}))
218 fniniseg 7015 . . . . . . . . . . . . 13 ( + Fn (𝐡 Γ— 𝐡) β†’ (𝑝 ∈ (β—‘ + β€œ {𝑧}) ↔ (𝑝 ∈ (𝐡 Γ— 𝐡) ∧ ( + β€˜π‘) = 𝑧)))
219199, 61, 2183syl 18 . . . . . . . . . . . 12 (((πœ‘ ∧ 𝑧 ∈ (ran (𝐹 ∘f + 𝐺) βˆ– {(0gβ€˜πΎ)})) ∧ 𝑝 ∈ ((β—‘ + β€œ {𝑧}) ∩ (ran 𝐹 Γ— ran 𝐺))) β†’ (𝑝 ∈ (β—‘ + β€œ {𝑧}) ↔ (𝑝 ∈ (𝐡 Γ— 𝐡) ∧ ( + β€˜π‘) = 𝑧)))
220217, 219mpbid 231 . . . . . . . . . . 11 (((πœ‘ ∧ 𝑧 ∈ (ran (𝐹 ∘f + 𝐺) βˆ– {(0gβ€˜πΎ)})) ∧ 𝑝 ∈ ((β—‘ + β€œ {𝑧}) ∩ (ran 𝐹 Γ— ran 𝐺))) β†’ (𝑝 ∈ (𝐡 Γ— 𝐡) ∧ ( + β€˜π‘) = 𝑧))
221 simpr 486 . . . . . . . . . . . 12 ((𝑝 ∈ (𝐡 Γ— 𝐡) ∧ ( + β€˜π‘) = 𝑧) β†’ ( + β€˜π‘) = 𝑧)
222 1st2nd2 7965 . . . . . . . . . . . . . . 15 (𝑝 ∈ (𝐡 Γ— 𝐡) β†’ 𝑝 = ⟨(1st β€˜π‘), (2nd β€˜π‘)⟩)
223222fveq2d 6851 . . . . . . . . . . . . . 14 (𝑝 ∈ (𝐡 Γ— 𝐡) β†’ ( + β€˜π‘) = ( + β€˜βŸ¨(1st β€˜π‘), (2nd β€˜π‘)⟩))
224 df-ov 7365 . . . . . . . . . . . . . 14 ((1st β€˜π‘) + (2nd β€˜π‘)) = ( + β€˜βŸ¨(1st β€˜π‘), (2nd β€˜π‘)⟩)
225223, 224eqtr4di 2795 . . . . . . . . . . . . 13 (𝑝 ∈ (𝐡 Γ— 𝐡) β†’ ( + β€˜π‘) = ((1st β€˜π‘) + (2nd β€˜π‘)))
226225adantr 482 . . . . . . . . . . . 12 ((𝑝 ∈ (𝐡 Γ— 𝐡) ∧ ( + β€˜π‘) = 𝑧) β†’ ( + β€˜π‘) = ((1st β€˜π‘) + (2nd β€˜π‘)))
227221, 226eqtr3d 2779 . . . . . . . . . . 11 ((𝑝 ∈ (𝐡 Γ— 𝐡) ∧ ( + β€˜π‘) = 𝑧) β†’ 𝑧 = ((1st β€˜π‘) + (2nd β€˜π‘)))
228220, 227syl 17 . . . . . . . . . 10 (((πœ‘ ∧ 𝑧 ∈ (ran (𝐹 ∘f + 𝐺) βˆ– {(0gβ€˜πΎ)})) ∧ 𝑝 ∈ ((β—‘ + β€œ {𝑧}) ∩ (ran 𝐹 Γ— ran 𝐺))) β†’ 𝑧 = ((1st β€˜π‘) + (2nd β€˜π‘)))
229 simplr 768 . . . . . . . . . . . 12 (((πœ‘ ∧ 𝑧 ∈ (ran (𝐹 ∘f + 𝐺) βˆ– {(0gβ€˜πΎ)})) ∧ 𝑝 ∈ ((β—‘ + β€œ {𝑧}) ∩ (ran 𝐹 Γ— ran 𝐺))) β†’ 𝑧 ∈ (ran (𝐹 ∘f + 𝐺) βˆ– {(0gβ€˜πΎ)}))
230229eldifbd 3928 . . . . . . . . . . 11 (((πœ‘ ∧ 𝑧 ∈ (ran (𝐹 ∘f + 𝐺) βˆ– {(0gβ€˜πΎ)})) ∧ 𝑝 ∈ ((β—‘ + β€œ {𝑧}) ∩ (ran 𝐹 Γ— ran 𝐺))) β†’ Β¬ 𝑧 ∈ {(0gβ€˜πΎ)})
231 velsn 4607 . . . . . . . . . . . 12 (𝑧 ∈ {(0gβ€˜πΎ)} ↔ 𝑧 = (0gβ€˜πΎ))
232231necon3bbii 2992 . . . . . . . . . . 11 (Β¬ 𝑧 ∈ {(0gβ€˜πΎ)} ↔ 𝑧 β‰  (0gβ€˜πΎ))
233230, 232sylib 217 . . . . . . . . . 10 (((πœ‘ ∧ 𝑧 ∈ (ran (𝐹 ∘f + 𝐺) βˆ– {(0gβ€˜πΎ)})) ∧ 𝑝 ∈ ((β—‘ + β€œ {𝑧}) ∩ (ran 𝐹 Γ— ran 𝐺))) β†’ 𝑧 β‰  (0gβ€˜πΎ))
234228, 233eqnetrrd 3013 . . . . . . . . 9 (((πœ‘ ∧ 𝑧 ∈ (ran (𝐹 ∘f + 𝐺) βˆ– {(0gβ€˜πΎ)})) ∧ 𝑝 ∈ ((β—‘ + β€œ {𝑧}) ∩ (ran 𝐹 Γ— ran 𝐺))) β†’ ((1st β€˜π‘) + (2nd β€˜π‘)) β‰  (0gβ€˜πΎ))
235175, 72sylanl2 680 . . . . . . . . . . 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 7369 . . . . . . . . . . . . 13 (π‘₯ = (1st β€˜π‘) β†’ (π‘₯ + 𝑦) = ((1st β€˜π‘) + 𝑦))
239238neeq1d 3004 . . . . . . . . . . . 12 (π‘₯ = (1st β€˜π‘) β†’ ((π‘₯ + 𝑦) β‰  (0gβ€˜πΎ) ↔ ((1st β€˜π‘) + 𝑦) β‰  (0gβ€˜πΎ)))
240 neeq1 3007 . . . . . . . . . . . . 13 (π‘₯ = (1st β€˜π‘) β†’ (π‘₯ β‰  0 ↔ (1st β€˜π‘) β‰  0 ))
241240orbi1d 916 . . . . . . . . . . . 12 (π‘₯ = (1st β€˜π‘) β†’ ((π‘₯ β‰  0 ∨ 𝑦 β‰  0 ) ↔ ((1st β€˜π‘) β‰  0 ∨ 𝑦 β‰  0 )))
242239, 241imbi12d 345 . . . . . . . . . . 11 (π‘₯ = (1st β€˜π‘) β†’ (((π‘₯ + 𝑦) β‰  (0gβ€˜πΎ) β†’ (π‘₯ β‰  0 ∨ 𝑦 β‰  0 )) ↔ (((1st β€˜π‘) + 𝑦) β‰  (0gβ€˜πΎ) β†’ ((1st β€˜π‘) β‰  0 ∨ 𝑦 β‰  0 ))))
243 oveq2 7370 . . . . . . . . . . . . 13 (𝑦 = (2nd β€˜π‘) β†’ ((1st β€˜π‘) + 𝑦) = ((1st β€˜π‘) + (2nd β€˜π‘)))
244243neeq1d 3004 . . . . . . . . . . . 12 (𝑦 = (2nd β€˜π‘) β†’ (((1st β€˜π‘) + 𝑦) β‰  (0gβ€˜πΎ) ↔ ((1st β€˜π‘) + (2nd β€˜π‘)) β‰  (0gβ€˜πΎ)))
245 neeq1 3007 . . . . . . . . . . . . 13 (𝑦 = (2nd β€˜π‘) β†’ (𝑦 β‰  0 ↔ (2nd β€˜π‘) β‰  0 ))
246245orbi2d 915 . . . . . . . . . . . 12 (𝑦 = (2nd β€˜π‘) β†’ (((1st β€˜π‘) β‰  0 ∨ 𝑦 β‰  0 ) ↔ ((1st β€˜π‘) β‰  0 ∨ (2nd β€˜π‘) β‰  0 )))
247244, 246imbi12d 345 . . . . . . . . . . 11 (𝑦 = (2nd β€˜π‘) β†’ ((((1st β€˜π‘) + 𝑦) β‰  (0gβ€˜πΎ) β†’ ((1st β€˜π‘) β‰  0 ∨ 𝑦 β‰  0 )) ↔ (((1st β€˜π‘) + (2nd β€˜π‘)) β‰  (0gβ€˜πΎ) β†’ ((1st β€˜π‘) β‰  0 ∨ (2nd β€˜π‘) β‰  0 ))))
248242, 247rspc2v 3593 . . . . . . . . . 10 (((1st β€˜π‘) ∈ 𝐡 ∧ (2nd β€˜π‘) ∈ 𝐡) β†’ (βˆ€π‘₯ ∈ 𝐡 βˆ€π‘¦ ∈ 𝐡 ((π‘₯ + 𝑦) β‰  (0gβ€˜πΎ) β†’ (π‘₯ β‰  0 ∨ 𝑦 β‰  0 )) β†’ (((1st β€˜π‘) + (2nd β€˜π‘)) β‰  (0gβ€˜πΎ) β†’ ((1st β€˜π‘) β‰  0 ∨ (2nd β€˜π‘) β‰  0 ))))
249236, 237, 248syl2anc 585 . . . . . . . . 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 32979 . . . . . . . 8 (((πœ‘ ∧ (1st β€˜π‘) ∈ ran 𝐹 ∧ (2nd β€˜π‘) ∈ ran 𝐺) ∧ ((1st β€˜π‘) β‰  0 ∨ (2nd β€˜π‘) β‰  0 )) β†’ (π‘€β€˜((◑𝐹 β€œ {(1st β€˜π‘)}) ∩ (◑𝐺 β€œ {(2nd β€˜π‘)}))) ∈ (0[,)+∞))
252199, 203, 205, 250, 251syl31anc 1374 . . . . . . 7 (((πœ‘ ∧ 𝑧 ∈ (ran (𝐹 ∘f + 𝐺) βˆ– {(0gβ€˜πΎ)})) ∧ 𝑝 ∈ ((β—‘ + β€œ {𝑧}) ∩ (ran 𝐹 Γ— ran 𝐺))) β†’ (π‘€β€˜((◑𝐹 β€œ {(1st β€˜π‘)}) ∩ (◑𝐺 β€œ {(2nd β€˜π‘)}))) ∈ (0[,)+∞))
253198, 252esumpfinval 32714 . . . . . 6 ((πœ‘ ∧ 𝑧 ∈ (ran (𝐹 ∘f + 𝐺) βˆ– {(0gβ€˜πΎ)})) β†’ Ξ£*𝑝 ∈ ((β—‘ + β€œ {𝑧}) ∩ (ran 𝐹 Γ— ran 𝐺))(π‘€β€˜((◑𝐹 β€œ {(1st β€˜π‘)}) ∩ (◑𝐺 β€œ {(2nd β€˜π‘)}))) = Σ𝑝 ∈ ((β—‘ + β€œ {𝑧}) ∩ (ran 𝐹 Γ— ran 𝐺))(π‘€β€˜((◑𝐹 β€œ {(1st β€˜π‘)}) ∩ (◑𝐺 β€œ {(2nd β€˜π‘)}))))
254171, 195, 2533eqtrd 2781 . . . . 5 ((πœ‘ ∧ 𝑧 ∈ (ran (𝐹 ∘f + 𝐺) βˆ– {(0gβ€˜πΎ)})) β†’ (π‘€β€˜(β—‘(𝐹 ∘f + 𝐺) β€œ {𝑧})) = Σ𝑝 ∈ ((β—‘ + β€œ {𝑧}) ∩ (ran 𝐹 Γ— ran 𝐺))(π‘€β€˜((◑𝐹 β€œ {(1st β€˜π‘)}) ∩ (◑𝐺 β€œ {(2nd β€˜π‘)}))))
255 rge0ssre 13380 . . . . . . 7 (0[,)+∞) βŠ† ℝ
256255, 252sselid 3947 . . . . . 6 (((πœ‘ ∧ 𝑧 ∈ (ran (𝐹 ∘f + 𝐺) βˆ– {(0gβ€˜πΎ)})) ∧ 𝑝 ∈ ((β—‘ + β€œ {𝑧}) ∩ (ran 𝐹 Γ— ran 𝐺))) β†’ (π‘€β€˜((◑𝐹 β€œ {(1st β€˜π‘)}) ∩ (◑𝐺 β€œ {(2nd β€˜π‘)}))) ∈ ℝ)
257198, 256fsumrecl 15626 . . . . 5 ((πœ‘ ∧ 𝑧 ∈ (ran (𝐹 ∘f + 𝐺) βˆ– {(0gβ€˜πΎ)})) β†’ Σ𝑝 ∈ ((β—‘ + β€œ {𝑧}) ∩ (ran 𝐹 Γ— ran 𝐺))(π‘€β€˜((◑𝐹 β€œ {(1st β€˜π‘)}) ∩ (◑𝐺 β€œ {(2nd β€˜π‘)}))) ∈ ℝ)
258254, 257eqeltrd 2838 . . . 4 ((πœ‘ ∧ 𝑧 ∈ (ran (𝐹 ∘f + 𝐺) βˆ– {(0gβ€˜πΎ)})) β†’ (π‘€β€˜(β—‘(𝐹 ∘f + 𝐺) β€œ {𝑧})) ∈ ℝ)
259174adantr 482 . . . . . . 7 (((πœ‘ ∧ 𝑧 ∈ (ran (𝐹 ∘f + 𝐺) βˆ– {(0gβ€˜πΎ)})) ∧ 𝑝 ∈ ((β—‘ + β€œ {𝑧}) ∩ (ran 𝐹 Γ— ran 𝐺))) β†’ 𝑀 ∈ (measuresβ€˜dom 𝑀))
260175, 108sylanl2 680 . . . . . . 7 (((πœ‘ ∧ 𝑧 ∈ (ran (𝐹 ∘f + 𝐺) βˆ– {(0gβ€˜πΎ)})) ∧ 𝑝 ∈ ((β—‘ + β€œ {𝑧}) ∩ (ran 𝐹 Γ— ran 𝐺))) β†’ ((◑𝐹 β€œ {(1st β€˜π‘)}) ∩ (◑𝐺 β€œ {(2nd β€˜π‘)})) ∈ dom 𝑀)
261 measge0 32846 . . . . . . 7 ((𝑀 ∈ (measuresβ€˜dom 𝑀) ∧ ((◑𝐹 β€œ {(1st β€˜π‘)}) ∩ (◑𝐺 β€œ {(2nd β€˜π‘)})) ∈ dom 𝑀) β†’ 0 ≀ (π‘€β€˜((◑𝐹 β€œ {(1st β€˜π‘)}) ∩ (◑𝐺 β€œ {(2nd β€˜π‘)}))))
262259, 260, 261syl2anc 585 . . . . . 6 (((πœ‘ ∧ 𝑧 ∈ (ran (𝐹 ∘f + 𝐺) βˆ– {(0gβ€˜πΎ)})) ∧ 𝑝 ∈ ((β—‘ + β€œ {𝑧}) ∩ (ran 𝐹 Γ— ran 𝐺))) β†’ 0 ≀ (π‘€β€˜((◑𝐹 β€œ {(1st β€˜π‘)}) ∩ (◑𝐺 β€œ {(2nd β€˜π‘)}))))
263198, 256, 262fsumge0 15687 . . . . 5 ((πœ‘ ∧ 𝑧 ∈ (ran (𝐹 ∘f + 𝐺) βˆ– {(0gβ€˜πΎ)})) β†’ 0 ≀ Σ𝑝 ∈ ((β—‘ + β€œ {𝑧}) ∩ (ran 𝐹 Γ— ran 𝐺))(π‘€β€˜((◑𝐹 β€œ {(1st β€˜π‘)}) ∩ (◑𝐺 β€œ {(2nd β€˜π‘)}))))
264263, 254breqtrrd 5138 . . . 4 ((πœ‘ ∧ 𝑧 ∈ (ran (𝐹 ∘f + 𝐺) βˆ– {(0gβ€˜πΎ)})) β†’ 0 ≀ (π‘€β€˜(β—‘(𝐹 ∘f + 𝐺) β€œ {𝑧})))
265 elrege0 13378 . . . 4 ((π‘€β€˜(β—‘(𝐹 ∘f + 𝐺) β€œ {𝑧})) ∈ (0[,)+∞) ↔ ((π‘€β€˜(β—‘(𝐹 ∘f + 𝐺) β€œ {𝑧})) ∈ ℝ ∧ 0 ≀ (π‘€β€˜(β—‘(𝐹 ∘f + 𝐺) β€œ {𝑧}))))
266258, 264, 265sylanbrc 584 . . 3 ((πœ‘ ∧ 𝑧 ∈ (ran (𝐹 ∘f + 𝐺) βˆ– {(0gβ€˜πΎ)})) β†’ (π‘€β€˜(β—‘(𝐹 ∘f + 𝐺) β€œ {𝑧})) ∈ (0[,)+∞))
267266ralrimiva 3144 . 2 (πœ‘ β†’ βˆ€π‘§ ∈ (ran (𝐹 ∘f + 𝐺) βˆ– {(0gβ€˜πΎ)})(π‘€β€˜(β—‘(𝐹 ∘f + 𝐺) β€œ {𝑧})) ∈ (0[,)+∞))
268 eqid 2737 . . 3 (sigaGenβ€˜(TopOpenβ€˜πΎ)) = (sigaGenβ€˜(TopOpenβ€˜πΎ))
269 eqid 2737 . . 3 (0gβ€˜πΎ) = (0gβ€˜πΎ)
270 eqid 2737 . . 3 ( ·𝑠 β€˜πΎ) = ( ·𝑠 β€˜πΎ)
271 eqid 2737 . . 3 (ℝHomβ€˜(Scalarβ€˜πΎ)) = (ℝHomβ€˜(Scalarβ€˜πΎ))
27227, 28, 268, 269, 270, 271, 26, 16issibf 32973 . 2 (πœ‘ β†’ ((𝐹 ∘f + 𝐺) ∈ dom (𝐾sitg𝑀) ↔ ((𝐹 ∘f + 𝐺) ∈ (dom 𝑀MblFnM(sigaGenβ€˜(TopOpenβ€˜πΎ))) ∧ ran (𝐹 ∘f + 𝐺) ∈ Fin ∧ βˆ€π‘§ ∈ (ran (𝐹 ∘f + 𝐺) βˆ– {(0gβ€˜πΎ)})(π‘€β€˜(β—‘(𝐹 ∘f + 𝐺) β€œ {𝑧})) ∈ (0[,)+∞))))
273169, 137, 267, 272mpbir3and 1343 1 (πœ‘ β†’ (𝐹 ∘f + 𝐺) ∈ dom (𝐾sitg𝑀))
Colors of variables: wff setvar class
Syntax hints:  Β¬ wn 3   β†’ wi 4   ↔ wb 205   ∧ wa 397   ∨ wo 846   = wceq 1542   ∈ wcel 2107   β‰  wne 2944  βˆ€wral 3065  Vcvv 3448   βˆ– cdif 3912   βˆͺ cun 3913   ∩ cin 3914   βŠ† wss 3915  βˆ…c0 4287  {csn 4591  βŸ¨cop 4597  βˆͺ cuni 4870  βˆͺ ciun 4959  Disj wdisj 5075   class class class wbr 5110   Γ— cxp 5636  β—‘ccnv 5637  dom cdm 5638  ran crn 5639   β€œ cima 5641  Fun wfun 6495   Fn wfn 6496  βŸΆwf 6497  β€˜cfv 6501  (class class class)co 7362   ∘f cof 7620  Ο‰com 7807  1st c1st 7924  2nd c2nd 7925   ↑m cmap 8772   β‰Ό cdom 8888   β‰Ί csdm 8889  Fincfn 8890  β„cr 11057  0cc0 11058  +∞cpnf 11193   ≀ cle 11197  [,)cico 13273  Ξ£csu 15577  Basecbs 17090  Scalarcsca 17143   ·𝑠 cvsca 17144  TopOpenctopn 17310  0gc0g 17328  Topctop 22258  TopSpctps 22297  Clsdccld 22383  Frect1 22674  β„Homcrrh 32614  Ξ£*cesum 32666  sigAlgebracsiga 32747  sigaGencsigagen 32777  measurescmeas 32834  MblFnMcmbfm 32888  sitgcsitg 32969
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2708  ax-rep 5247  ax-sep 5261  ax-nul 5268  ax-pow 5325  ax-pr 5389  ax-un 7677  ax-inf2 9584  ax-ac2 10406  ax-cnex 11114  ax-resscn 11115  ax-1cn 11116  ax-icn 11117  ax-addcl 11118  ax-addrcl 11119  ax-mulcl 11120  ax-mulrcl 11121  ax-mulcom 11122  ax-addass 11123  ax-mulass 11124  ax-distr 11125  ax-i2m1 11126  ax-1ne0 11127  ax-1rid 11128  ax-rnegex 11129  ax-rrecex 11130  ax-cnre 11131  ax-pre-lttri 11132  ax-pre-lttrn 11133  ax-pre-ltadd 11134  ax-pre-mulgt0 11135  ax-pre-sup 11136  ax-addf 11137  ax-mulf 11138
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3or 1089  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2539  df-eu 2568  df-clab 2715  df-cleq 2729  df-clel 2815  df-nfc 2890  df-ne 2945  df-nel 3051  df-ral 3066  df-rex 3075  df-rmo 3356  df-reu 3357  df-rab 3411  df-v 3450  df-sbc 3745  df-csb 3861  df-dif 3918  df-un 3920  df-in 3922  df-ss 3932  df-pss 3934  df-nul 4288  df-if 4492  df-pw 4567  df-sn 4592  df-pr 4594  df-tp 4596  df-op 4598  df-uni 4871  df-int 4913  df-iun 4961  df-iin 4962  df-disj 5076  df-br 5111  df-opab 5173  df-mpt 5194  df-tr 5228  df-id 5536  df-eprel 5542  df-po 5550  df-so 5551  df-fr 5593  df-se 5594  df-we 5595  df-xp 5644  df-rel 5645  df-cnv 5646  df-co 5647  df-dm 5648  df-rn 5649  df-res 5650  df-ima 5651  df-pred 6258  df-ord 6325  df-on 6326  df-lim 6327  df-suc 6328  df-iota 6453  df-fun 6503  df-fn 6504  df-f 6505  df-f1 6506  df-fo 6507  df-f1o 6508  df-fv 6509  df-isom 6510  df-riota 7318  df-ov 7365  df-oprab 7366  df-mpo 7367  df-of 7622  df-om 7808  df-1st 7926  df-2nd 7927  df-supp 8098  df-frecs 8217  df-wrecs 8248  df-recs 8322  df-rdg 8361  df-1o 8417  df-2o 8418  df-er 8655  df-map 8774  df-pm 8775  df-ixp 8843  df-en 8891  df-dom 8892  df-sdom 8893  df-fin 8894  df-fsupp 9313  df-fi 9354  df-sup 9385  df-inf 9386  df-oi 9453  df-dju 9844  df-card 9882  df-acn 9885  df-ac 10059  df-pnf 11198  df-mnf 11199  df-xr 11200  df-ltxr 11201  df-le 11202  df-sub 11394  df-neg 11395  df-div 11820  df-nn 12161  df-2 12223  df-3 12224  df-4 12225  df-5 12226  df-6 12227  df-7 12228  df-8 12229  df-9 12230  df-n0 12421  df-z 12507  df-dec 12626  df-uz 12771  df-q 12881  df-rp 12923  df-xneg 13040  df-xadd 13041  df-xmul 13042  df-ioo 13275  df-ioc 13276  df-ico 13277  df-icc 13278  df-fz 13432  df-fzo 13575  df-fl 13704  df-mod 13782  df-seq 13914  df-exp 13975  df-fac 14181  df-bc 14210  df-hash 14238  df-shft 14959  df-cj 14991  df-re 14992  df-im 14993  df-sqrt 15127  df-abs 15128  df-limsup 15360  df-clim 15377  df-rlim 15378  df-sum 15578  df-ef 15957  df-sin 15959  df-cos 15960  df-pi 15962  df-struct 17026  df-sets 17043  df-slot 17061  df-ndx 17073  df-base 17091  df-ress 17120  df-plusg 17153  df-mulr 17154  df-starv 17155  df-sca 17156  df-vsca 17157  df-ip 17158  df-tset 17159  df-ple 17160  df-ds 17162  df-unif 17163  df-hom 17164  df-cco 17165  df-rest 17311  df-topn 17312  df-0g 17330  df-gsum 17331  df-topgen 17332  df-pt 17333  df-prds 17336  df-ordt 17390  df-xrs 17391  df-qtop 17396  df-imas 17397  df-xps 17399  df-mre 17473  df-mrc 17474  df-acs 17476  df-ps 18462  df-tsr 18463  df-plusf 18503  df-mgm 18504  df-sgrp 18553  df-mnd 18564  df-mhm 18608  df-submnd 18609  df-grp 18758  df-minusg 18759  df-sbg 18760  df-mulg 18880  df-subg 18932  df-cntz 19104  df-cmn 19571  df-abl 19572  df-mgp 19904  df-ur 19921  df-ring 19973  df-cring 19974  df-subrg 20236  df-abv 20292  df-lmod 20340  df-scaf 20341  df-sra 20649  df-rgmod 20650  df-psmet 20804  df-xmet 20805  df-met 20806  df-bl 20807  df-mopn 20808  df-fbas 20809  df-fg 20810  df-cnfld 20813  df-top 22259  df-topon 22276  df-topsp 22298  df-bases 22312  df-cld 22386  df-ntr 22387  df-cls 22388  df-nei 22465  df-lp 22503  df-perf 22504  df-cn 22594  df-cnp 22595  df-t1 22681  df-haus 22682  df-tx 22929  df-hmeo 23122  df-fil 23213  df-fm 23305  df-flim 23306  df-flf 23307  df-tmd 23439  df-tgp 23440  df-tsms 23494  df-trg 23527  df-xms 23689  df-ms 23690  df-tms 23691  df-nm 23954  df-ngp 23955  df-nrg 23957  df-nlm 23958  df-ii 24256  df-cncf 24257  df-limc 25246  df-dv 25247  df-log 25928  df-esum 32667  df-siga 32748  df-sigagen 32778  df-meas 32835  df-mbfm 32889  df-sitg 32970
This theorem is referenced by:  sitmcl  32991
  Copyright terms: Public domain W3C validator