Theorem sibfof 31240

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	⊢ (𝜑 → (𝐹 ∘𝑓 + 𝐺) ∈ dom (𝐾sitg𝑀))

Proof of Theorem sibfof

Dummy variables 𝑥 𝑦 𝑧 𝑝 𝑏 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		sibfof.1	. . . . . . . 8 ⊢ (𝜑 → + :(𝐵 × 𝐵)⟶𝐶)
2		sibfof.0	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑊 ∈ TopSp)
3		sitgval.b	. . . . . . . . . . . 12 ⊢ 𝐵 = (Base‘𝑊)
4		sitgval.j	. . . . . . . . . . . 12 ⊢ 𝐽 = (TopOpen‘𝑊)
5	3, 4	tpsuni 21248	. . . . . . . . . . 11 ⊢ (𝑊 ∈ TopSp → 𝐵 = ∪ 𝐽)
6	2, 5	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → 𝐵 = ∪ 𝐽)
7	6	sqxpeqd 5439	. . . . . . . . 9 ⊢ (𝜑 → (𝐵 × 𝐵) = (∪ 𝐽 × ∪ 𝐽))
8	7	feq2d 6330	. . . . . . . 8 ⊢ (𝜑 → ( + :(𝐵 × 𝐵)⟶𝐶 ↔ + :(∪ 𝐽 × ∪ 𝐽)⟶𝐶))
9	1, 8	mpbid 224	. . . . . . 7 ⊢ (𝜑 → + :(∪ 𝐽 × ∪ 𝐽)⟶𝐶)
10	9	fovrnda 7135	. . . . . 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𝑀))
18	3, 4, 11, 12, 13, 14, 15, 16, 17	sibff 31236	. . . . . 6 ⊢ (𝜑 → 𝐹:∪ dom 𝑀⟶∪ 𝐽)
19		sibfof.2	. . . . . . 7 ⊢ (𝜑 → 𝐺 ∈ dom (𝑊sitg𝑀))
20	3, 4, 11, 12, 13, 14, 15, 16, 19	sibff 31236	. . . . . 6 ⊢ (𝜑 → 𝐺:∪ dom 𝑀⟶∪ 𝐽)
21		dmexg 7428	. . . . . . 7 ⊢ (𝑀 ∈ ∪ ran measures → dom 𝑀 ∈ V)
22		uniexg 7285	. . . . . . 7 ⊢ (dom 𝑀 ∈ V → ∪ dom 𝑀 ∈ V)
23	16, 21, 22	3syl 18	. . . . . 6 ⊢ (𝜑 → ∪ dom 𝑀 ∈ V)
24		inidm 4083	. . . . . 6 ⊢ (∪ dom 𝑀 ∩ ∪ dom 𝑀) = ∪ dom 𝑀
25	10, 18, 20, 23, 23, 24	off 7242	. . . . 5 ⊢ (𝜑 → (𝐹 ∘𝑓 + 𝐺):∪ dom 𝑀⟶𝐶)
26		sibfof.3	. . . . . . . 8 ⊢ (𝜑 → 𝐾 ∈ TopSp)
27		sibfof.c	. . . . . . . . 9 ⊢ 𝐶 = (Base‘𝐾)
28		eqid 2779	. . . . . . . . 9 ⊢ (TopOpen‘𝐾) = (TopOpen‘𝐾)
29	27, 28	tpsuni 21248	. . . . . . . 8 ⊢ (𝐾 ∈ TopSp → 𝐶 = ∪ (TopOpen‘𝐾))
30	26, 29	syl 17	. . . . . . 7 ⊢ (𝜑 → 𝐶 = ∪ (TopOpen‘𝐾))
31		fvex 6512	. . . . . . . 8 ⊢ (TopOpen‘𝐾) ∈ V
32		unisg 31044	. . . . . . . 8 ⊢ ((TopOpen‘𝐾) ∈ V → ∪ (sigaGen‘(TopOpen‘𝐾)) = ∪ (TopOpen‘𝐾))
33	31, 32	ax-mp 5	. . . . . . 7 ⊢ ∪ (sigaGen‘(TopOpen‘𝐾)) = ∪ (TopOpen‘𝐾)
34	30, 33	syl6eqr 2833	. . . . . 6 ⊢ (𝜑 → 𝐶 = ∪ (sigaGen‘(TopOpen‘𝐾)))
35	34	feq3d 6331	. . . . 5 ⊢ (𝜑 → ((𝐹 ∘𝑓 + 𝐺):∪ dom 𝑀⟶𝐶 ↔ (𝐹 ∘𝑓 + 𝐺):∪ dom 𝑀⟶∪ (sigaGen‘(TopOpen‘𝐾))))
36	25, 35	mpbid 224	. . . 4 ⊢ (𝜑 → (𝐹 ∘𝑓 + 𝐺):∪ dom 𝑀⟶∪ (sigaGen‘(TopOpen‘𝐾)))
37	31	a1i 11	. . . . . . 7 ⊢ (𝜑 → (TopOpen‘𝐾) ∈ V)
38	37	sgsiga 31043	. . . . . 6 ⊢ (𝜑 → (sigaGen‘(TopOpen‘𝐾)) ∈ ∪ ran sigAlgebra)
39		uniexg 7285	. . . . . 6 ⊢ ((sigaGen‘(TopOpen‘𝐾)) ∈ ∪ ran sigAlgebra → ∪ (sigaGen‘(TopOpen‘𝐾)) ∈ V)
40	38, 39	syl 17	. . . . 5 ⊢ (𝜑 → ∪ (sigaGen‘(TopOpen‘𝐾)) ∈ V)
41	40, 23	elmapd 8220	. . . 4 ⊢ (𝜑 → ((𝐹 ∘𝑓 + 𝐺) ∈ (∪ (sigaGen‘(TopOpen‘𝐾)) ↑𝑚 ∪ dom 𝑀) ↔ (𝐹 ∘𝑓 + 𝐺):∪ dom 𝑀⟶∪ (sigaGen‘(TopOpen‘𝐾))))
42	36, 41	mpbird 249	. . 3 ⊢ (𝜑 → (𝐹 ∘𝑓 + 𝐺) ∈ (∪ (sigaGen‘(TopOpen‘𝐾)) ↑𝑚 ∪ dom 𝑀))
43		inundif 4310	. . . . . . 7 ⊢ ((𝑏 ∩ ran (𝐹 ∘𝑓 + 𝐺)) ∪ (𝑏 ∖ ran (𝐹 ∘𝑓 + 𝐺))) = 𝑏
44	43	imaeq2i 5768	. . . . . 6 ⊢ (◡(𝐹 ∘𝑓 + 𝐺) “ ((𝑏 ∩ ran (𝐹 ∘𝑓 + 𝐺)) ∪ (𝑏 ∖ ran (𝐹 ∘𝑓 + 𝐺)))) = (◡(𝐹 ∘𝑓 + 𝐺) “ 𝑏)
45		ffun 6347	. . . . . . . 8 ⊢ ((𝐹 ∘𝑓 + 𝐺):∪ dom 𝑀⟶𝐶 → Fun (𝐹 ∘𝑓 + 𝐺))
46		unpreima 6658	. . . . . . . 8 ⊢ (Fun (𝐹 ∘𝑓 + 𝐺) → (◡(𝐹 ∘𝑓 + 𝐺) “ ((𝑏 ∩ ran (𝐹 ∘𝑓 + 𝐺)) ∪ (𝑏 ∖ ran (𝐹 ∘𝑓 + 𝐺)))) = ((◡(𝐹 ∘𝑓 + 𝐺) “ (𝑏 ∩ ran (𝐹 ∘𝑓 + 𝐺))) ∪ (◡(𝐹 ∘𝑓 + 𝐺) “ (𝑏 ∖ ran (𝐹 ∘𝑓 + 𝐺)))))
47	25, 45, 46	3syl 18	. . . . . . 7 ⊢ (𝜑 → (◡(𝐹 ∘𝑓 + 𝐺) “ ((𝑏 ∩ ran (𝐹 ∘𝑓 + 𝐺)) ∪ (𝑏 ∖ ran (𝐹 ∘𝑓 + 𝐺)))) = ((◡(𝐹 ∘𝑓 + 𝐺) “ (𝑏 ∩ ran (𝐹 ∘𝑓 + 𝐺))) ∪ (◡(𝐹 ∘𝑓 + 𝐺) “ (𝑏 ∖ ran (𝐹 ∘𝑓 + 𝐺)))))
48	47	adantr 473	. . . . . 6 ⊢ ((𝜑 ∧ 𝑏 ∈ (sigaGen‘(TopOpen‘𝐾))) → (◡(𝐹 ∘𝑓 + 𝐺) “ ((𝑏 ∩ ran (𝐹 ∘𝑓 + 𝐺)) ∪ (𝑏 ∖ ran (𝐹 ∘𝑓 + 𝐺)))) = ((◡(𝐹 ∘𝑓 + 𝐺) “ (𝑏 ∩ ran (𝐹 ∘𝑓 + 𝐺))) ∪ (◡(𝐹 ∘𝑓 + 𝐺) “ (𝑏 ∖ ran (𝐹 ∘𝑓 + 𝐺)))))
49	44, 48	syl5eqr 2829	. . . . 5 ⊢ ((𝜑 ∧ 𝑏 ∈ (sigaGen‘(TopOpen‘𝐾))) → (◡(𝐹 ∘𝑓 + 𝐺) “ 𝑏) = ((◡(𝐹 ∘𝑓 + 𝐺) “ (𝑏 ∩ ran (𝐹 ∘𝑓 + 𝐺))) ∪ (◡(𝐹 ∘𝑓 + 𝐺) “ (𝑏 ∖ ran (𝐹 ∘𝑓 + 𝐺)))))
50		dmmeas 31102	. . . . . . . 8 ⊢ (𝑀 ∈ ∪ ran measures → dom 𝑀 ∈ ∪ ran sigAlgebra)
51	16, 50	syl 17	. . . . . . 7 ⊢ (𝜑 → dom 𝑀 ∈ ∪ ran sigAlgebra)
52	51	adantr 473	. . . . . 6 ⊢ ((𝜑 ∧ 𝑏 ∈ (sigaGen‘(TopOpen‘𝐾))) → dom 𝑀 ∈ ∪ ran sigAlgebra)
53		imaiun 6829	. . . . . . . 8 ⊢ (◡(𝐹 ∘𝑓 + 𝐺) “ ∪ 𝑧 ∈ (𝑏 ∩ ran (𝐹 ∘𝑓 + 𝐺)){𝑧}) = ∪ 𝑧 ∈ (𝑏 ∩ ran (𝐹 ∘𝑓 + 𝐺))(◡(𝐹 ∘𝑓 + 𝐺) “ {𝑧})
54		iunid 4850	. . . . . . . . 9 ⊢ ∪ 𝑧 ∈ (𝑏 ∩ ran (𝐹 ∘𝑓 + 𝐺)){𝑧} = (𝑏 ∩ ran (𝐹 ∘𝑓 + 𝐺))
55	54	imaeq2i 5768	. . . . . . . 8 ⊢ (◡(𝐹 ∘𝑓 + 𝐺) “ ∪ 𝑧 ∈ (𝑏 ∩ ran (𝐹 ∘𝑓 + 𝐺)){𝑧}) = (◡(𝐹 ∘𝑓 + 𝐺) “ (𝑏 ∩ ran (𝐹 ∘𝑓 + 𝐺)))
56	53, 55	eqtr3i 2805	. . . . . . 7 ⊢ ∪ 𝑧 ∈ (𝑏 ∩ ran (𝐹 ∘𝑓 + 𝐺))(◡(𝐹 ∘𝑓 + 𝐺) “ {𝑧}) = (◡(𝐹 ∘𝑓 + 𝐺) “ (𝑏 ∩ ran (𝐹 ∘𝑓 + 𝐺)))
57		inss2 4094	. . . . . . . . . 10 ⊢ (𝑏 ∩ ran (𝐹 ∘𝑓 + 𝐺)) ⊆ ran (𝐹 ∘𝑓 + 𝐺)
58	6	feq3d 6331	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝐹:∪ dom 𝑀⟶𝐵 ↔ 𝐹:∪ dom 𝑀⟶∪ 𝐽))
59	18, 58	mpbird 249	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝐹:∪ dom 𝑀⟶𝐵)
60	6	feq3d 6331	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝐺:∪ dom 𝑀⟶𝐵 ↔ 𝐺:∪ dom 𝑀⟶∪ 𝐽))
61	20, 60	mpbird 249	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝐺:∪ dom 𝑀⟶𝐵)
62	1	ffnd 6345	. . . . . . . . . . . . . 14 ⊢ (𝜑 → + Fn (𝐵 × 𝐵))
63	59, 61, 23, 62	ofpreima2 30173	. . . . . . . . . . . . 13 ⊢ (𝜑 → (◡(𝐹 ∘𝑓 + 𝐺) “ {𝑧}) = ∪ 𝑝 ∈ ((◡ + “ {𝑧}) ∩ (ran 𝐹 × ran 𝐺))((◡𝐹 “ {(1st ‘𝑝)}) ∩ (◡𝐺 “ {(2nd ‘𝑝)})))
64	63	adantr 473	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑧 ∈ ran (𝐹 ∘𝑓 + 𝐺)) → (◡(𝐹 ∘𝑓 + 𝐺) “ {𝑧}) = ∪ 𝑝 ∈ ((◡ + “ {𝑧}) ∩ (ran 𝐹 × ran 𝐺))((◡𝐹 “ {(1st ‘𝑝)}) ∩ (◡𝐺 “ {(2nd ‘𝑝)})))
65	51	adantr 473	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑧 ∈ ran (𝐹 ∘𝑓 + 𝐺)) → dom 𝑀 ∈ ∪ ran sigAlgebra)
66	51	ad2antrr 713	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑧 ∈ ran (𝐹 ∘𝑓 + 𝐺)) ∧ 𝑝 ∈ ((◡ + “ {𝑧}) ∩ (ran 𝐹 × ran 𝐺))) → dom 𝑀 ∈ ∪ ran sigAlgebra)
67		simpll 754	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑧 ∈ ran (𝐹 ∘𝑓 + 𝐺)) ∧ 𝑝 ∈ ((◡ + “ {𝑧}) ∩ (ran 𝐹 × ran 𝐺))) → 𝜑)
68		inss1 4093	. . . . . . . . . . . . . . . . . 18 ⊢ ((◡ + “ {𝑧}) ∩ (ran 𝐹 × ran 𝐺)) ⊆ (◡ + “ {𝑧})
69		cnvimass 5789	. . . . . . . . . . . . . . . . . . . 20 ⊢ (◡ + “ {𝑧}) ⊆ dom +
70	69, 1	fssdm 6360	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (◡ + “ {𝑧}) ⊆ (𝐵 × 𝐵))
71	70	adantr 473	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑧 ∈ ran (𝐹 ∘𝑓 + 𝐺)) → (◡ + “ {𝑧}) ⊆ (𝐵 × 𝐵))
72	68, 71	syl5ss 3870	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑧 ∈ ran (𝐹 ∘𝑓 + 𝐺)) → ((◡ + “ {𝑧}) ∩ (ran 𝐹 × ran 𝐺)) ⊆ (𝐵 × 𝐵))
73	72	sselda 3859	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑧 ∈ ran (𝐹 ∘𝑓 + 𝐺)) ∧ 𝑝 ∈ ((◡ + “ {𝑧}) ∩ (ran 𝐹 × ran 𝐺))) → 𝑝 ∈ (𝐵 × 𝐵))
74	51	adantr 473	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑝 ∈ (𝐵 × 𝐵)) → dom 𝑀 ∈ ∪ ran sigAlgebra)
75		sibfof.4	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → 𝐽 ∈ Fre)
76	75	sgsiga 31043	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (sigaGen‘𝐽) ∈ ∪ ran sigAlgebra)
77	11, 76	syl5eqel 2871	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝑆 ∈ ∪ ran sigAlgebra)
78	77	adantr 473	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑝 ∈ (𝐵 × 𝐵)) → 𝑆 ∈ ∪ ran sigAlgebra)
79	3, 4, 11, 12, 13, 14, 15, 16, 17	sibfmbl 31235	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝐹 ∈ (dom 𝑀MblFnM𝑆))
80	79	adantr 473	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑝 ∈ (𝐵 × 𝐵)) → 𝐹 ∈ (dom 𝑀MblFnM𝑆))
81	4	tpstop 21249	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑊 ∈ TopSp → 𝐽 ∈ Top)
82		cldssbrsiga 31088	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝐽 ∈ Top → (Clsd‘𝐽) ⊆ (sigaGen‘𝐽))
83	2, 81, 82	3syl 18	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (Clsd‘𝐽) ⊆ (sigaGen‘𝐽))
84	83	adantr 473	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑝 ∈ (𝐵 × 𝐵)) → (Clsd‘𝐽) ⊆ (sigaGen‘𝐽))
85	75	adantr 473	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑝 ∈ (𝐵 × 𝐵)) → 𝐽 ∈ Fre)
86		xp1st 7533	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑝 ∈ (𝐵 × 𝐵) → (1st ‘𝑝) ∈ 𝐵)
87	86	adantl 474	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑝 ∈ (𝐵 × 𝐵)) → (1st ‘𝑝) ∈ 𝐵)
88	6	adantr 473	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑝 ∈ (𝐵 × 𝐵)) → 𝐵 = ∪ 𝐽)
89	87, 88	eleqtrd 2869	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑝 ∈ (𝐵 × 𝐵)) → (1st ‘𝑝) ∈ ∪ 𝐽)
90		eqid 2779	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ∪ 𝐽 = ∪ 𝐽
91	90	t1sncld 21638	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐽 ∈ Fre ∧ (1st ‘𝑝) ∈ ∪ 𝐽) → {(1st ‘𝑝)} ∈ (Clsd‘𝐽))
92	85, 89, 91	syl2anc 576	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑝 ∈ (𝐵 × 𝐵)) → {(1st ‘𝑝)} ∈ (Clsd‘𝐽))
93	84, 92	sseldd 3860	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑝 ∈ (𝐵 × 𝐵)) → {(1st ‘𝑝)} ∈ (sigaGen‘𝐽))
94	93, 11	syl6eleqr 2878	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑝 ∈ (𝐵 × 𝐵)) → {(1st ‘𝑝)} ∈ 𝑆)
95	74, 78, 80, 94	mbfmcnvima 31157	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑝 ∈ (𝐵 × 𝐵)) → (◡𝐹 “ {(1st ‘𝑝)}) ∈ dom 𝑀)
96	67, 73, 95	syl2anc 576	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑧 ∈ ran (𝐹 ∘𝑓 + 𝐺)) ∧ 𝑝 ∈ ((◡ + “ {𝑧}) ∩ (ran 𝐹 × ran 𝐺))) → (◡𝐹 “ {(1st ‘𝑝)}) ∈ dom 𝑀)
97	3, 4, 11, 12, 13, 14, 15, 16, 19	sibfmbl 31235	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝐺 ∈ (dom 𝑀MblFnM𝑆))
98	97	adantr 473	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑝 ∈ (𝐵 × 𝐵)) → 𝐺 ∈ (dom 𝑀MblFnM𝑆))
99		xp2nd 7534	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑝 ∈ (𝐵 × 𝐵) → (2nd ‘𝑝) ∈ 𝐵)
100	99	adantl 474	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑝 ∈ (𝐵 × 𝐵)) → (2nd ‘𝑝) ∈ 𝐵)
101	100, 88	eleqtrd 2869	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑝 ∈ (𝐵 × 𝐵)) → (2nd ‘𝑝) ∈ ∪ 𝐽)
102	90	t1sncld 21638	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐽 ∈ Fre ∧ (2nd ‘𝑝) ∈ ∪ 𝐽) → {(2nd ‘𝑝)} ∈ (Clsd‘𝐽))
103	85, 101, 102	syl2anc 576	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑝 ∈ (𝐵 × 𝐵)) → {(2nd ‘𝑝)} ∈ (Clsd‘𝐽))
104	84, 103	sseldd 3860	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑝 ∈ (𝐵 × 𝐵)) → {(2nd ‘𝑝)} ∈ (sigaGen‘𝐽))
105	104, 11	syl6eleqr 2878	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑝 ∈ (𝐵 × 𝐵)) → {(2nd ‘𝑝)} ∈ 𝑆)
106	74, 78, 98, 105	mbfmcnvima 31157	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑝 ∈ (𝐵 × 𝐵)) → (◡𝐺 “ {(2nd ‘𝑝)}) ∈ dom 𝑀)
107	67, 73, 106	syl2anc 576	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑧 ∈ ran (𝐹 ∘𝑓 + 𝐺)) ∧ 𝑝 ∈ ((◡ + “ {𝑧}) ∩ (ran 𝐹 × ran 𝐺))) → (◡𝐺 “ {(2nd ‘𝑝)}) ∈ dom 𝑀)
108		inelsiga 31036	. . . . . . . . . . . . . . 15 ⊢ ((dom 𝑀 ∈ ∪ ran sigAlgebra ∧ (◡𝐹 “ {(1st ‘𝑝)}) ∈ dom 𝑀 ∧ (◡𝐺 “ {(2nd ‘𝑝)}) ∈ dom 𝑀) → ((◡𝐹 “ {(1st ‘𝑝)}) ∩ (◡𝐺 “ {(2nd ‘𝑝)})) ∈ dom 𝑀)
109	66, 96, 107, 108	syl3anc 1351	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑧 ∈ ran (𝐹 ∘𝑓 + 𝐺)) ∧ 𝑝 ∈ ((◡ + “ {𝑧}) ∩ (ran 𝐹 × ran 𝐺))) → ((◡𝐹 “ {(1st ‘𝑝)}) ∩ (◡𝐺 “ {(2nd ‘𝑝)})) ∈ dom 𝑀)
110	109	ralrimiva 3133	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑧 ∈ ran (𝐹 ∘𝑓 + 𝐺)) → ∀𝑝 ∈ ((◡ + “ {𝑧}) ∩ (ran 𝐹 × ran 𝐺))((◡𝐹 “ {(1st ‘𝑝)}) ∩ (◡𝐺 “ {(2nd ‘𝑝)})) ∈ dom 𝑀)
111	3, 4, 11, 12, 13, 14, 15, 16, 17	sibfrn 31237	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ran 𝐹 ∈ Fin)
112	3, 4, 11, 12, 13, 14, 15, 16, 19	sibfrn 31237	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ran 𝐺 ∈ Fin)
113		xpfi 8584	. . . . . . . . . . . . . . . . 17 ⊢ ((ran 𝐹 ∈ Fin ∧ ran 𝐺 ∈ Fin) → (ran 𝐹 × ran 𝐺) ∈ Fin)
114	111, 112, 113	syl2anc 576	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (ran 𝐹 × ran 𝐺) ∈ Fin)
115		inss2 4094	. . . . . . . . . . . . . . . 16 ⊢ ((◡ + “ {𝑧}) ∩ (ran 𝐹 × ran 𝐺)) ⊆ (ran 𝐹 × ran 𝐺)
116		ssdomg 8352	. . . . . . . . . . . . . . . 16 ⊢ ((ran 𝐹 × ran 𝐺) ∈ Fin → (((◡ + “ {𝑧}) ∩ (ran 𝐹 × ran 𝐺)) ⊆ (ran 𝐹 × ran 𝐺) → ((◡ + “ {𝑧}) ∩ (ran 𝐹 × ran 𝐺)) ≼ (ran 𝐹 × ran 𝐺)))
117	114, 115, 116	mpisyl 21	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((◡ + “ {𝑧}) ∩ (ran 𝐹 × ran 𝐺)) ≼ (ran 𝐹 × ran 𝐺))
118		isfinite 8909	. . . . . . . . . . . . . . . . 17 ⊢ ((ran 𝐹 × ran 𝐺) ∈ Fin ↔ (ran 𝐹 × ran 𝐺) ≺ ω)
119	118	biimpi 208	. . . . . . . . . . . . . . . 16 ⊢ ((ran 𝐹 × ran 𝐺) ∈ Fin → (ran 𝐹 × ran 𝐺) ≺ ω)
120		sdomdom 8334	. . . . . . . . . . . . . . . 16 ⊢ ((ran 𝐹 × ran 𝐺) ≺ ω → (ran 𝐹 × ran 𝐺) ≼ ω)
121	114, 119, 120	3syl 18	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (ran 𝐹 × ran 𝐺) ≼ ω)
122		domtr 8359	. . . . . . . . . . . . . . 15 ⊢ ((((◡ + “ {𝑧}) ∩ (ran 𝐹 × ran 𝐺)) ≼ (ran 𝐹 × ran 𝐺) ∧ (ran 𝐹 × ran 𝐺) ≼ ω) → ((◡ + “ {𝑧}) ∩ (ran 𝐹 × ran 𝐺)) ≼ ω)
123	117, 121, 122	syl2anc 576	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((◡ + “ {𝑧}) ∩ (ran 𝐹 × ran 𝐺)) ≼ ω)
124	123	adantr 473	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑧 ∈ ran (𝐹 ∘𝑓 + 𝐺)) → ((◡ + “ {𝑧}) ∩ (ran 𝐹 × ran 𝐺)) ≼ ω)
125		nfcv 2933	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑝((◡ + “ {𝑧}) ∩ (ran 𝐹 × ran 𝐺))
126	125	sigaclcuni 31019	. . . . . . . . . . . . 13 ⊢ ((dom 𝑀 ∈ ∪ ran sigAlgebra ∧ ∀𝑝 ∈ ((◡ + “ {𝑧}) ∩ (ran 𝐹 × ran 𝐺))((◡𝐹 “ {(1st ‘𝑝)}) ∩ (◡𝐺 “ {(2nd ‘𝑝)})) ∈ dom 𝑀 ∧ ((◡ + “ {𝑧}) ∩ (ran 𝐹 × ran 𝐺)) ≼ ω) → ∪ 𝑝 ∈ ((◡ + “ {𝑧}) ∩ (ran 𝐹 × ran 𝐺))((◡𝐹 “ {(1st ‘𝑝)}) ∩ (◡𝐺 “ {(2nd ‘𝑝)})) ∈ dom 𝑀)
127	65, 110, 124, 126	syl3anc 1351	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑧 ∈ ran (𝐹 ∘𝑓 + 𝐺)) → ∪ 𝑝 ∈ ((◡ + “ {𝑧}) ∩ (ran 𝐹 × ran 𝐺))((◡𝐹 “ {(1st ‘𝑝)}) ∩ (◡𝐺 “ {(2nd ‘𝑝)})) ∈ dom 𝑀)
128	64, 127	eqeltrd 2867	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑧 ∈ ran (𝐹 ∘𝑓 + 𝐺)) → (◡(𝐹 ∘𝑓 + 𝐺) “ {𝑧}) ∈ dom 𝑀)
129	128	ralrimiva 3133	. . . . . . . . . 10 ⊢ (𝜑 → ∀𝑧 ∈ ran (𝐹 ∘𝑓 + 𝐺)(◡(𝐹 ∘𝑓 + 𝐺) “ {𝑧}) ∈ dom 𝑀)
130		ssralv 3924	. . . . . . . . . 10 ⊢ ((𝑏 ∩ ran (𝐹 ∘𝑓 + 𝐺)) ⊆ ran (𝐹 ∘𝑓 + 𝐺) → (∀𝑧 ∈ ran (𝐹 ∘𝑓 + 𝐺)(◡(𝐹 ∘𝑓 + 𝐺) “ {𝑧}) ∈ dom 𝑀 → ∀𝑧 ∈ (𝑏 ∩ ran (𝐹 ∘𝑓 + 𝐺))(◡(𝐹 ∘𝑓 + 𝐺) “ {𝑧}) ∈ dom 𝑀))
131	57, 129, 130	mpsyl 68	. . . . . . . . 9 ⊢ (𝜑 → ∀𝑧 ∈ (𝑏 ∩ ran (𝐹 ∘𝑓 + 𝐺))(◡(𝐹 ∘𝑓 + 𝐺) “ {𝑧}) ∈ dom 𝑀)
132	131	adantr 473	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑏 ∈ (sigaGen‘(TopOpen‘𝐾))) → ∀𝑧 ∈ (𝑏 ∩ ran (𝐹 ∘𝑓 + 𝐺))(◡(𝐹 ∘𝑓 + 𝐺) “ {𝑧}) ∈ dom 𝑀)
133	1	ffund 6348	. . . . . . . . . . . . 13 ⊢ (𝜑 → Fun + )
134		imafi 8612	. . . . . . . . . . . . 13 ⊢ ((Fun + ∧ (ran 𝐹 × ran 𝐺) ∈ Fin) → ( + “ (ran 𝐹 × ran 𝐺)) ∈ Fin)
135	133, 114, 134	syl2anc 576	. . . . . . . . . . . 12 ⊢ (𝜑 → ( + “ (ran 𝐹 × ran 𝐺)) ∈ Fin)
136	18, 20, 9, 23	ofrn2 30149	. . . . . . . . . . . 12 ⊢ (𝜑 → ran (𝐹 ∘𝑓 + 𝐺) ⊆ ( + “ (ran 𝐹 × ran 𝐺)))
137		ssfi 8533	. . . . . . . . . . . 12 ⊢ ((( + “ (ran 𝐹 × ran 𝐺)) ∈ Fin ∧ ran (𝐹 ∘𝑓 + 𝐺) ⊆ ( + “ (ran 𝐹 × ran 𝐺))) → ran (𝐹 ∘𝑓 + 𝐺) ∈ Fin)
138	135, 136, 137	syl2anc 576	. . . . . . . . . . 11 ⊢ (𝜑 → ran (𝐹 ∘𝑓 + 𝐺) ∈ Fin)
139		ssdomg 8352	. . . . . . . . . . 11 ⊢ (ran (𝐹 ∘𝑓 + 𝐺) ∈ Fin → ((𝑏 ∩ ran (𝐹 ∘𝑓 + 𝐺)) ⊆ ran (𝐹 ∘𝑓 + 𝐺) → (𝑏 ∩ ran (𝐹 ∘𝑓 + 𝐺)) ≼ ran (𝐹 ∘𝑓 + 𝐺)))
140	138, 57, 139	mpisyl 21	. . . . . . . . . 10 ⊢ (𝜑 → (𝑏 ∩ ran (𝐹 ∘𝑓 + 𝐺)) ≼ ran (𝐹 ∘𝑓 + 𝐺))
141		isfinite 8909	. . . . . . . . . . . 12 ⊢ (ran (𝐹 ∘𝑓 + 𝐺) ∈ Fin ↔ ran (𝐹 ∘𝑓 + 𝐺) ≺ ω)
142	138, 141	sylib 210	. . . . . . . . . . 11 ⊢ (𝜑 → ran (𝐹 ∘𝑓 + 𝐺) ≺ ω)
143		sdomdom 8334	. . . . . . . . . . 11 ⊢ (ran (𝐹 ∘𝑓 + 𝐺) ≺ ω → ran (𝐹 ∘𝑓 + 𝐺) ≼ ω)
144	142, 143	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → ran (𝐹 ∘𝑓 + 𝐺) ≼ ω)
145		domtr 8359	. . . . . . . . . 10 ⊢ (((𝑏 ∩ ran (𝐹 ∘𝑓 + 𝐺)) ≼ ran (𝐹 ∘𝑓 + 𝐺) ∧ ran (𝐹 ∘𝑓 + 𝐺) ≼ ω) → (𝑏 ∩ ran (𝐹 ∘𝑓 + 𝐺)) ≼ ω)
146	140, 144, 145	syl2anc 576	. . . . . . . . 9 ⊢ (𝜑 → (𝑏 ∩ ran (𝐹 ∘𝑓 + 𝐺)) ≼ ω)
147	146	adantr 473	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑏 ∈ (sigaGen‘(TopOpen‘𝐾))) → (𝑏 ∩ ran (𝐹 ∘𝑓 + 𝐺)) ≼ ω)
148		nfcv 2933	. . . . . . . . 9 ⊢ Ⅎ𝑧(𝑏 ∩ ran (𝐹 ∘𝑓 + 𝐺))
149	148	sigaclcuni 31019	. . . . . . . 8 ⊢ ((dom 𝑀 ∈ ∪ ran sigAlgebra ∧ ∀𝑧 ∈ (𝑏 ∩ ran (𝐹 ∘𝑓 + 𝐺))(◡(𝐹 ∘𝑓 + 𝐺) “ {𝑧}) ∈ dom 𝑀 ∧ (𝑏 ∩ ran (𝐹 ∘𝑓 + 𝐺)) ≼ ω) → ∪ 𝑧 ∈ (𝑏 ∩ ran (𝐹 ∘𝑓 + 𝐺))(◡(𝐹 ∘𝑓 + 𝐺) “ {𝑧}) ∈ dom 𝑀)
150	52, 132, 147, 149	syl3anc 1351	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑏 ∈ (sigaGen‘(TopOpen‘𝐾))) → ∪ 𝑧 ∈ (𝑏 ∩ ran (𝐹 ∘𝑓 + 𝐺))(◡(𝐹 ∘𝑓 + 𝐺) “ {𝑧}) ∈ dom 𝑀)
151	56, 150	syl5eqelr 2872	. . . . . 6 ⊢ ((𝜑 ∧ 𝑏 ∈ (sigaGen‘(TopOpen‘𝐾))) → (◡(𝐹 ∘𝑓 + 𝐺) “ (𝑏 ∩ ran (𝐹 ∘𝑓 + 𝐺))) ∈ dom 𝑀)
152		difpreima 6660	. . . . . . . . . 10 ⊢ (Fun (𝐹 ∘𝑓 + 𝐺) → (◡(𝐹 ∘𝑓 + 𝐺) “ (𝑏 ∖ ran (𝐹 ∘𝑓 + 𝐺))) = ((◡(𝐹 ∘𝑓 + 𝐺) “ 𝑏) ∖ (◡(𝐹 ∘𝑓 + 𝐺) “ ran (𝐹 ∘𝑓 + 𝐺))))
153	25, 45, 152	3syl 18	. . . . . . . . 9 ⊢ (𝜑 → (◡(𝐹 ∘𝑓 + 𝐺) “ (𝑏 ∖ ran (𝐹 ∘𝑓 + 𝐺))) = ((◡(𝐹 ∘𝑓 + 𝐺) “ 𝑏) ∖ (◡(𝐹 ∘𝑓 + 𝐺) “ ran (𝐹 ∘𝑓 + 𝐺))))
154		cnvimarndm 5790	. . . . . . . . . . 11 ⊢ (◡(𝐹 ∘𝑓 + 𝐺) “ ran (𝐹 ∘𝑓 + 𝐺)) = dom (𝐹 ∘𝑓 + 𝐺)
155	154	difeq2i 3987	. . . . . . . . . 10 ⊢ ((◡(𝐹 ∘𝑓 + 𝐺) “ 𝑏) ∖ (◡(𝐹 ∘𝑓 + 𝐺) “ ran (𝐹 ∘𝑓 + 𝐺))) = ((◡(𝐹 ∘𝑓 + 𝐺) “ 𝑏) ∖ dom (𝐹 ∘𝑓 + 𝐺))
156		cnvimass 5789	. . . . . . . . . . 11 ⊢ (◡(𝐹 ∘𝑓 + 𝐺) “ 𝑏) ⊆ dom (𝐹 ∘𝑓 + 𝐺)
157		ssdif0 4210	. . . . . . . . . . 11 ⊢ ((◡(𝐹 ∘𝑓 + 𝐺) “ 𝑏) ⊆ dom (𝐹 ∘𝑓 + 𝐺) ↔ ((◡(𝐹 ∘𝑓 + 𝐺) “ 𝑏) ∖ dom (𝐹 ∘𝑓 + 𝐺)) = ∅)
158	156, 157	mpbi 222	. . . . . . . . . 10 ⊢ ((◡(𝐹 ∘𝑓 + 𝐺) “ 𝑏) ∖ dom (𝐹 ∘𝑓 + 𝐺)) = ∅
159	155, 158	eqtri 2803	. . . . . . . . 9 ⊢ ((◡(𝐹 ∘𝑓 + 𝐺) “ 𝑏) ∖ (◡(𝐹 ∘𝑓 + 𝐺) “ ran (𝐹 ∘𝑓 + 𝐺))) = ∅
160	153, 159	syl6eq 2831	. . . . . . . 8 ⊢ (𝜑 → (◡(𝐹 ∘𝑓 + 𝐺) “ (𝑏 ∖ ran (𝐹 ∘𝑓 + 𝐺))) = ∅)
161		0elsiga 31015	. . . . . . . . 9 ⊢ (dom 𝑀 ∈ ∪ ran sigAlgebra → ∅ ∈ dom 𝑀)
162	16, 50, 161	3syl 18	. . . . . . . 8 ⊢ (𝜑 → ∅ ∈ dom 𝑀)
163	160, 162	eqeltrd 2867	. . . . . . 7 ⊢ (𝜑 → (◡(𝐹 ∘𝑓 + 𝐺) “ (𝑏 ∖ ran (𝐹 ∘𝑓 + 𝐺))) ∈ dom 𝑀)
164	163	adantr 473	. . . . . 6 ⊢ ((𝜑 ∧ 𝑏 ∈ (sigaGen‘(TopOpen‘𝐾))) → (◡(𝐹 ∘𝑓 + 𝐺) “ (𝑏 ∖ ran (𝐹 ∘𝑓 + 𝐺))) ∈ dom 𝑀)
165		unelsiga 31035	. . . . . 6 ⊢ ((dom 𝑀 ∈ ∪ ran sigAlgebra ∧ (◡(𝐹 ∘𝑓 + 𝐺) “ (𝑏 ∩ ran (𝐹 ∘𝑓 + 𝐺))) ∈ dom 𝑀 ∧ (◡(𝐹 ∘𝑓 + 𝐺) “ (𝑏 ∖ ran (𝐹 ∘𝑓 + 𝐺))) ∈ dom 𝑀) → ((◡(𝐹 ∘𝑓 + 𝐺) “ (𝑏 ∩ ran (𝐹 ∘𝑓 + 𝐺))) ∪ (◡(𝐹 ∘𝑓 + 𝐺) “ (𝑏 ∖ ran (𝐹 ∘𝑓 + 𝐺)))) ∈ dom 𝑀)
166	52, 151, 164, 165	syl3anc 1351	. . . . 5 ⊢ ((𝜑 ∧ 𝑏 ∈ (sigaGen‘(TopOpen‘𝐾))) → ((◡(𝐹 ∘𝑓 + 𝐺) “ (𝑏 ∩ ran (𝐹 ∘𝑓 + 𝐺))) ∪ (◡(𝐹 ∘𝑓 + 𝐺) “ (𝑏 ∖ ran (𝐹 ∘𝑓 + 𝐺)))) ∈ dom 𝑀)
167	49, 166	eqeltrd 2867	. . . 4 ⊢ ((𝜑 ∧ 𝑏 ∈ (sigaGen‘(TopOpen‘𝐾))) → (◡(𝐹 ∘𝑓 + 𝐺) “ 𝑏) ∈ dom 𝑀)
168	167	ralrimiva 3133	. . 3 ⊢ (𝜑 → ∀𝑏 ∈ (sigaGen‘(TopOpen‘𝐾))(◡(𝐹 ∘𝑓 + 𝐺) “ 𝑏) ∈ dom 𝑀)
169	51, 38	ismbfm 31152	. . 3 ⊢ (𝜑 → ((𝐹 ∘𝑓 + 𝐺) ∈ (dom 𝑀MblFnM(sigaGen‘(TopOpen‘𝐾))) ↔ ((𝐹 ∘𝑓 + 𝐺) ∈ (∪ (sigaGen‘(TopOpen‘𝐾)) ↑𝑚 ∪ dom 𝑀) ∧ ∀𝑏 ∈ (sigaGen‘(TopOpen‘𝐾))(◡(𝐹 ∘𝑓 + 𝐺) “ 𝑏) ∈ dom 𝑀)))
170	42, 168, 169	mpbir2and 700	. 2 ⊢ (𝜑 → (𝐹 ∘𝑓 + 𝐺) ∈ (dom 𝑀MblFnM(sigaGen‘(TopOpen‘𝐾))))
171	63	adantr 473	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑧 ∈ (ran (𝐹 ∘𝑓 + 𝐺) ∖ {(0g‘𝐾)})) → (◡(𝐹 ∘𝑓 + 𝐺) “ {𝑧}) = ∪ 𝑝 ∈ ((◡ + “ {𝑧}) ∩ (ran 𝐹 × ran 𝐺))((◡𝐹 “ {(1st ‘𝑝)}) ∩ (◡𝐺 “ {(2nd ‘𝑝)})))
172	171	fveq2d 6503	. . . . . 6 ⊢ ((𝜑 ∧ 𝑧 ∈ (ran (𝐹 ∘𝑓 + 𝐺) ∖ {(0g‘𝐾)})) → (𝑀‘(◡(𝐹 ∘𝑓 + 𝐺) “ {𝑧})) = (𝑀‘∪ 𝑝 ∈ ((◡ + “ {𝑧}) ∩ (ran 𝐹 × ran 𝐺))((◡𝐹 “ {(1st ‘𝑝)}) ∩ (◡𝐺 “ {(2nd ‘𝑝)}))))
173		measbasedom 31103	. . . . . . . . 9 ⊢ (𝑀 ∈ ∪ ran measures ↔ 𝑀 ∈ (measures‘dom 𝑀))
174	16, 173	sylib 210	. . . . . . . 8 ⊢ (𝜑 → 𝑀 ∈ (measures‘dom 𝑀))
175	174	adantr 473	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑧 ∈ (ran (𝐹 ∘𝑓 + 𝐺) ∖ {(0g‘𝐾)})) → 𝑀 ∈ (measures‘dom 𝑀))
176		eldifi 3994	. . . . . . . 8 ⊢ (𝑧 ∈ (ran (𝐹 ∘𝑓 + 𝐺) ∖ {(0g‘𝐾)}) → 𝑧 ∈ ran (𝐹 ∘𝑓 + 𝐺))
177	176, 110	sylan2 583	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑧 ∈ (ran (𝐹 ∘𝑓 + 𝐺) ∖ {(0g‘𝐾)})) → ∀𝑝 ∈ ((◡ + “ {𝑧}) ∩ (ran 𝐹 × ran 𝐺))((◡𝐹 “ {(1st ‘𝑝)}) ∩ (◡𝐺 “ {(2nd ‘𝑝)})) ∈ dom 𝑀)
178	123	adantr 473	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑧 ∈ (ran (𝐹 ∘𝑓 + 𝐺) ∖ {(0g‘𝐾)})) → ((◡ + “ {𝑧}) ∩ (ran 𝐹 × ran 𝐺)) ≼ ω)
179		sneq 4451	. . . . . . . . . . 11 ⊢ (𝑥 = (1st ‘𝑝) → {𝑥} = {(1st ‘𝑝)})
180	179	imaeq2d 5770	. . . . . . . . . 10 ⊢ (𝑥 = (1st ‘𝑝) → (◡𝐹 “ {𝑥}) = (◡𝐹 “ {(1st ‘𝑝)}))
181		sneq 4451	. . . . . . . . . . 11 ⊢ (𝑦 = (2nd ‘𝑝) → {𝑦} = {(2nd ‘𝑝)})
182	181	imaeq2d 5770	. . . . . . . . . 10 ⊢ (𝑦 = (2nd ‘𝑝) → (◡𝐺 “ {𝑦}) = (◡𝐺 “ {(2nd ‘𝑝)}))
183	18	ffund 6348	. . . . . . . . . . 11 ⊢ (𝜑 → Fun 𝐹)
184		sndisj 4921	. . . . . . . . . . 11 ⊢ Disj 𝑥 ∈ ran 𝐹{𝑥}
185		disjpreima 30100	. . . . . . . . . . 11 ⊢ ((Fun 𝐹 ∧ Disj 𝑥 ∈ ran 𝐹{𝑥}) → Disj 𝑥 ∈ ran 𝐹(◡𝐹 “ {𝑥}))
186	183, 184, 185	sylancl 577	. . . . . . . . . 10 ⊢ (𝜑 → Disj 𝑥 ∈ ran 𝐹(◡𝐹 “ {𝑥}))
187	20	ffund 6348	. . . . . . . . . . 11 ⊢ (𝜑 → Fun 𝐺)
188		sndisj 4921	. . . . . . . . . . 11 ⊢ Disj 𝑦 ∈ ran 𝐺{𝑦}
189		disjpreima 30100	. . . . . . . . . . 11 ⊢ ((Fun 𝐺 ∧ Disj 𝑦 ∈ ran 𝐺{𝑦}) → Disj 𝑦 ∈ ran 𝐺(◡𝐺 “ {𝑦}))
190	187, 188, 189	sylancl 577	. . . . . . . . . 10 ⊢ (𝜑 → Disj 𝑦 ∈ ran 𝐺(◡𝐺 “ {𝑦}))
191	180, 182, 186, 190	disjxpin 30104	. . . . . . . . 9 ⊢ (𝜑 → Disj 𝑝 ∈ (ran 𝐹 × ran 𝐺)((◡𝐹 “ {(1st ‘𝑝)}) ∩ (◡𝐺 “ {(2nd ‘𝑝)})))
192		disjss1 4903	. . . . . . . . 9 ⊢ (((◡ + “ {𝑧}) ∩ (ran 𝐹 × ran 𝐺)) ⊆ (ran 𝐹 × ran 𝐺) → (Disj 𝑝 ∈ (ran 𝐹 × ran 𝐺)((◡𝐹 “ {(1st ‘𝑝)}) ∩ (◡𝐺 “ {(2nd ‘𝑝)})) → Disj 𝑝 ∈ ((◡ + “ {𝑧}) ∩ (ran 𝐹 × ran 𝐺))((◡𝐹 “ {(1st ‘𝑝)}) ∩ (◡𝐺 “ {(2nd ‘𝑝)}))))
193	115, 191, 192	mpsyl 68	. . . . . . . 8 ⊢ (𝜑 → Disj 𝑝 ∈ ((◡ + “ {𝑧}) ∩ (ran 𝐹 × ran 𝐺))((◡𝐹 “ {(1st ‘𝑝)}) ∩ (◡𝐺 “ {(2nd ‘𝑝)})))
194	193	adantr 473	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑧 ∈ (ran (𝐹 ∘𝑓 + 𝐺) ∖ {(0g‘𝐾)})) → Disj 𝑝 ∈ ((◡ + “ {𝑧}) ∩ (ran 𝐹 × ran 𝐺))((◡𝐹 “ {(1st ‘𝑝)}) ∩ (◡𝐺 “ {(2nd ‘𝑝)})))
195		measvuni 31115	. . . . . . 7 ⊢ ((𝑀 ∈ (measures‘dom 𝑀) ∧ ∀𝑝 ∈ ((◡ + “ {𝑧}) ∩ (ran 𝐹 × ran 𝐺))((◡𝐹 “ {(1st ‘𝑝)}) ∩ (◡𝐺 “ {(2nd ‘𝑝)})) ∈ dom 𝑀 ∧ (((◡ + “ {𝑧}) ∩ (ran 𝐹 × ran 𝐺)) ≼ ω ∧ Disj 𝑝 ∈ ((◡ + “ {𝑧}) ∩ (ran 𝐹 × ran 𝐺))((◡𝐹 “ {(1st ‘𝑝)}) ∩ (◡𝐺 “ {(2nd ‘𝑝)})))) → (𝑀‘∪ 𝑝 ∈ ((◡ + “ {𝑧}) ∩ (ran 𝐹 × ran 𝐺))((◡𝐹 “ {(1st ‘𝑝)}) ∩ (◡𝐺 “ {(2nd ‘𝑝)}))) = Σ*𝑝 ∈ ((◡ + “ {𝑧}) ∩ (ran 𝐹 × ran 𝐺))(𝑀‘((◡𝐹 “ {(1st ‘𝑝)}) ∩ (◡𝐺 “ {(2nd ‘𝑝)}))))
196	175, 177, 178, 194, 195	syl112anc 1354	. . . . . 6 ⊢ ((𝜑 ∧ 𝑧 ∈ (ran (𝐹 ∘𝑓 + 𝐺) ∖ {(0g‘𝐾)})) → (𝑀‘∪ 𝑝 ∈ ((◡ + “ {𝑧}) ∩ (ran 𝐹 × ran 𝐺))((◡𝐹 “ {(1st ‘𝑝)}) ∩ (◡𝐺 “ {(2nd ‘𝑝)}))) = Σ*𝑝 ∈ ((◡ + “ {𝑧}) ∩ (ran 𝐹 × ran 𝐺))(𝑀‘((◡𝐹 “ {(1st ‘𝑝)}) ∩ (◡𝐺 “ {(2nd ‘𝑝)}))))
197		ssfi 8533	. . . . . . . . 9 ⊢ (((ran 𝐹 × ran 𝐺) ∈ Fin ∧ ((◡ + “ {𝑧}) ∩ (ran 𝐹 × ran 𝐺)) ⊆ (ran 𝐹 × ran 𝐺)) → ((◡ + “ {𝑧}) ∩ (ran 𝐹 × ran 𝐺)) ∈ Fin)
198	114, 115, 197	sylancl 577	. . . . . . . 8 ⊢ (𝜑 → ((◡ + “ {𝑧}) ∩ (ran 𝐹 × ran 𝐺)) ∈ Fin)
199	198	adantr 473	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑧 ∈ (ran (𝐹 ∘𝑓 + 𝐺) ∖ {(0g‘𝐾)})) → ((◡ + “ {𝑧}) ∩ (ran 𝐹 × ran 𝐺)) ∈ Fin)
200		simpll 754	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑧 ∈ (ran (𝐹 ∘𝑓 + 𝐺) ∖ {(0g‘𝐾)})) ∧ 𝑝 ∈ ((◡ + “ {𝑧}) ∩ (ran 𝐹 × ran 𝐺))) → 𝜑)
201		simpr 477	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑧 ∈ (ran (𝐹 ∘𝑓 + 𝐺) ∖ {(0g‘𝐾)})) ∧ 𝑝 ∈ ((◡ + “ {𝑧}) ∩ (ran 𝐹 × ran 𝐺))) → 𝑝 ∈ ((◡ + “ {𝑧}) ∩ (ran 𝐹 × ran 𝐺)))
202	115, 201	sseldi 3857	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑧 ∈ (ran (𝐹 ∘𝑓 + 𝐺) ∖ {(0g‘𝐾)})) ∧ 𝑝 ∈ ((◡ + “ {𝑧}) ∩ (ran 𝐹 × ran 𝐺))) → 𝑝 ∈ (ran 𝐹 × ran 𝐺))
203		xp1st 7533	. . . . . . . . 9 ⊢ (𝑝 ∈ (ran 𝐹 × ran 𝐺) → (1st ‘𝑝) ∈ ran 𝐹)
204	202, 203	syl 17	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑧 ∈ (ran (𝐹 ∘𝑓 + 𝐺) ∖ {(0g‘𝐾)})) ∧ 𝑝 ∈ ((◡ + “ {𝑧}) ∩ (ran 𝐹 × ran 𝐺))) → (1st ‘𝑝) ∈ ran 𝐹)
205		xp2nd 7534	. . . . . . . . 9 ⊢ (𝑝 ∈ (ran 𝐹 × ran 𝐺) → (2nd ‘𝑝) ∈ ran 𝐺)
206	202, 205	syl 17	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑧 ∈ (ran (𝐹 ∘𝑓 + 𝐺) ∖ {(0g‘𝐾)})) ∧ 𝑝 ∈ ((◡ + “ {𝑧}) ∩ (ran 𝐹 × ran 𝐺))) → (2nd ‘𝑝) ∈ ran 𝐺)
207		oveq12 6985	. . . . . . . . . . . . . . . 16 ⊢ ((𝑥 = 0 ∧ 𝑦 = 0 ) → (𝑥 + 𝑦) = ( 0 + 0 ))
208		sibfof.5	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ( 0 + 0 ) = (0g‘𝐾))
209	207, 208	sylan9eqr 2837	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑥 = 0 ∧ 𝑦 = 0 )) → (𝑥 + 𝑦) = (0g‘𝐾))
210	209	ex 405	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((𝑥 = 0 ∧ 𝑦 = 0 ) → (𝑥 + 𝑦) = (0g‘𝐾)))
211	210	necon3ad 2981	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝑥 + 𝑦) ≠ (0g‘𝐾) → ¬ (𝑥 = 0 ∧ 𝑦 = 0 )))
212		neorian 3063	. . . . . . . . . . . . 13 ⊢ ((𝑥 ≠ 0 ∨ 𝑦 ≠ 0 ) ↔ ¬ (𝑥 = 0 ∧ 𝑦 = 0 ))
213	211, 212	syl6ibr 244	. . . . . . . . . . . 12 ⊢ (𝜑 → ((𝑥 + 𝑦) ≠ (0g‘𝐾) → (𝑥 ≠ 0 ∨ 𝑦 ≠ 0 )))
214	213	adantr 473	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → ((𝑥 + 𝑦) ≠ (0g‘𝐾) → (𝑥 ≠ 0 ∨ 𝑦 ≠ 0 )))
215	214	ralrimivva 3142	. . . . . . . . . 10 ⊢ (𝜑 → ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ((𝑥 + 𝑦) ≠ (0g‘𝐾) → (𝑥 ≠ 0 ∨ 𝑦 ≠ 0 )))
216	200, 215	syl 17	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑧 ∈ (ran (𝐹 ∘𝑓 + 𝐺) ∖ {(0g‘𝐾)})) ∧ 𝑝 ∈ ((◡ + “ {𝑧}) ∩ (ran 𝐹 × ran 𝐺))) → ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ((𝑥 + 𝑦) ≠ (0g‘𝐾) → (𝑥 ≠ 0 ∨ 𝑦 ≠ 0 )))
217	68	a1i 11	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑧 ∈ (ran (𝐹 ∘𝑓 + 𝐺) ∖ {(0g‘𝐾)})) → ((◡ + “ {𝑧}) ∩ (ran 𝐹 × ran 𝐺)) ⊆ (◡ + “ {𝑧}))
218	217	sselda 3859	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑧 ∈ (ran (𝐹 ∘𝑓 + 𝐺) ∖ {(0g‘𝐾)})) ∧ 𝑝 ∈ ((◡ + “ {𝑧}) ∩ (ran 𝐹 × ran 𝐺))) → 𝑝 ∈ (◡ + “ {𝑧}))
219		fniniseg 6655	. . . . . . . . . . . . 13 ⊢ ( + Fn (𝐵 × 𝐵) → (𝑝 ∈ (◡ + “ {𝑧}) ↔ (𝑝 ∈ (𝐵 × 𝐵) ∧ ( + ‘𝑝) = 𝑧)))
220	200, 62, 219	3syl 18	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑧 ∈ (ran (𝐹 ∘𝑓 + 𝐺) ∖ {(0g‘𝐾)})) ∧ 𝑝 ∈ ((◡ + “ {𝑧}) ∩ (ran 𝐹 × ran 𝐺))) → (𝑝 ∈ (◡ + “ {𝑧}) ↔ (𝑝 ∈ (𝐵 × 𝐵) ∧ ( + ‘𝑝) = 𝑧)))
221	218, 220	mpbid 224	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑧 ∈ (ran (𝐹 ∘𝑓 + 𝐺) ∖ {(0g‘𝐾)})) ∧ 𝑝 ∈ ((◡ + “ {𝑧}) ∩ (ran 𝐹 × ran 𝐺))) → (𝑝 ∈ (𝐵 × 𝐵) ∧ ( + ‘𝑝) = 𝑧))
222		simpr 477	. . . . . . . . . . . 12 ⊢ ((𝑝 ∈ (𝐵 × 𝐵) ∧ ( + ‘𝑝) = 𝑧) → ( + ‘𝑝) = 𝑧)
223		1st2nd2 7540	. . . . . . . . . . . . . . 15 ⊢ (𝑝 ∈ (𝐵 × 𝐵) → 𝑝 = ⟨(1st ‘𝑝), (2nd ‘𝑝)⟩)
224	223	fveq2d 6503	. . . . . . . . . . . . . 14 ⊢ (𝑝 ∈ (𝐵 × 𝐵) → ( + ‘𝑝) = ( + ‘⟨(1st ‘𝑝), (2nd ‘𝑝)⟩))
225		df-ov 6979	. . . . . . . . . . . . . 14 ⊢ ((1st ‘𝑝) + (2nd ‘𝑝)) = ( + ‘⟨(1st ‘𝑝), (2nd ‘𝑝)⟩)
226	224, 225	syl6eqr 2833	. . . . . . . . . . . . 13 ⊢ (𝑝 ∈ (𝐵 × 𝐵) → ( + ‘𝑝) = ((1st ‘𝑝) + (2nd ‘𝑝)))
227	226	adantr 473	. . . . . . . . . . . 12 ⊢ ((𝑝 ∈ (𝐵 × 𝐵) ∧ ( + ‘𝑝) = 𝑧) → ( + ‘𝑝) = ((1st ‘𝑝) + (2nd ‘𝑝)))
228	222, 227	eqtr3d 2817	. . . . . . . . . . 11 ⊢ ((𝑝 ∈ (𝐵 × 𝐵) ∧ ( + ‘𝑝) = 𝑧) → 𝑧 = ((1st ‘𝑝) + (2nd ‘𝑝)))
229	221, 228	syl 17	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑧 ∈ (ran (𝐹 ∘𝑓 + 𝐺) ∖ {(0g‘𝐾)})) ∧ 𝑝 ∈ ((◡ + “ {𝑧}) ∩ (ran 𝐹 × ran 𝐺))) → 𝑧 = ((1st ‘𝑝) + (2nd ‘𝑝)))
230		simplr 756	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑧 ∈ (ran (𝐹 ∘𝑓 + 𝐺) ∖ {(0g‘𝐾)})) ∧ 𝑝 ∈ ((◡ + “ {𝑧}) ∩ (ran 𝐹 × ran 𝐺))) → 𝑧 ∈ (ran (𝐹 ∘𝑓 + 𝐺) ∖ {(0g‘𝐾)}))
231	230	eldifbd 3843	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑧 ∈ (ran (𝐹 ∘𝑓 + 𝐺) ∖ {(0g‘𝐾)})) ∧ 𝑝 ∈ ((◡ + “ {𝑧}) ∩ (ran 𝐹 × ran 𝐺))) → ¬ 𝑧 ∈ {(0g‘𝐾)})
232		velsn 4457	. . . . . . . . . . . 12 ⊢ (𝑧 ∈ {(0g‘𝐾)} ↔ 𝑧 = (0g‘𝐾))
233	232	necon3bbii 3015	. . . . . . . . . . 11 ⊢ (¬ 𝑧 ∈ {(0g‘𝐾)} ↔ 𝑧 ≠ (0g‘𝐾))
234	231, 233	sylib 210	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑧 ∈ (ran (𝐹 ∘𝑓 + 𝐺) ∖ {(0g‘𝐾)})) ∧ 𝑝 ∈ ((◡ + “ {𝑧}) ∩ (ran 𝐹 × ran 𝐺))) → 𝑧 ≠ (0g‘𝐾))
235	229, 234	eqnetrrd 3036	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑧 ∈ (ran (𝐹 ∘𝑓 + 𝐺) ∖ {(0g‘𝐾)})) ∧ 𝑝 ∈ ((◡ + “ {𝑧}) ∩ (ran 𝐹 × ran 𝐺))) → ((1st ‘𝑝) + (2nd ‘𝑝)) ≠ (0g‘𝐾))
236	176, 73	sylanl2 668	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑧 ∈ (ran (𝐹 ∘𝑓 + 𝐺) ∖ {(0g‘𝐾)})) ∧ 𝑝 ∈ ((◡ + “ {𝑧}) ∩ (ran 𝐹 × ran 𝐺))) → 𝑝 ∈ (𝐵 × 𝐵))
237	236, 86	syl 17	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑧 ∈ (ran (𝐹 ∘𝑓 + 𝐺) ∖ {(0g‘𝐾)})) ∧ 𝑝 ∈ ((◡ + “ {𝑧}) ∩ (ran 𝐹 × ran 𝐺))) → (1st ‘𝑝) ∈ 𝐵)
238	236, 99	syl 17	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑧 ∈ (ran (𝐹 ∘𝑓 + 𝐺) ∖ {(0g‘𝐾)})) ∧ 𝑝 ∈ ((◡ + “ {𝑧}) ∩ (ran 𝐹 × ran 𝐺))) → (2nd ‘𝑝) ∈ 𝐵)
239		oveq1 6983	. . . . . . . . . . . . 13 ⊢ (𝑥 = (1st ‘𝑝) → (𝑥 + 𝑦) = ((1st ‘𝑝) + 𝑦))
240	239	neeq1d 3027	. . . . . . . . . . . 12 ⊢ (𝑥 = (1st ‘𝑝) → ((𝑥 + 𝑦) ≠ (0g‘𝐾) ↔ ((1st ‘𝑝) + 𝑦) ≠ (0g‘𝐾)))
241		neeq1 3030	. . . . . . . . . . . . 13 ⊢ (𝑥 = (1st ‘𝑝) → (𝑥 ≠ 0 ↔ (1st ‘𝑝) ≠ 0 ))
242	241	orbi1d 900	. . . . . . . . . . . 12 ⊢ (𝑥 = (1st ‘𝑝) → ((𝑥 ≠ 0 ∨ 𝑦 ≠ 0 ) ↔ ((1st ‘𝑝) ≠ 0 ∨ 𝑦 ≠ 0 )))
243	240, 242	imbi12d 337	. . . . . . . . . . 11 ⊢ (𝑥 = (1st ‘𝑝) → (((𝑥 + 𝑦) ≠ (0g‘𝐾) → (𝑥 ≠ 0 ∨ 𝑦 ≠ 0 )) ↔ (((1st ‘𝑝) + 𝑦) ≠ (0g‘𝐾) → ((1st ‘𝑝) ≠ 0 ∨ 𝑦 ≠ 0 ))))
244		oveq2 6984	. . . . . . . . . . . . 13 ⊢ (𝑦 = (2nd ‘𝑝) → ((1st ‘𝑝) + 𝑦) = ((1st ‘𝑝) + (2nd ‘𝑝)))
245	244	neeq1d 3027	. . . . . . . . . . . 12 ⊢ (𝑦 = (2nd ‘𝑝) → (((1st ‘𝑝) + 𝑦) ≠ (0g‘𝐾) ↔ ((1st ‘𝑝) + (2nd ‘𝑝)) ≠ (0g‘𝐾)))
246		neeq1 3030	. . . . . . . . . . . . 13 ⊢ (𝑦 = (2nd ‘𝑝) → (𝑦 ≠ 0 ↔ (2nd ‘𝑝) ≠ 0 ))
247	246	orbi2d 899	. . . . . . . . . . . 12 ⊢ (𝑦 = (2nd ‘𝑝) → (((1st ‘𝑝) ≠ 0 ∨ 𝑦 ≠ 0 ) ↔ ((1st ‘𝑝) ≠ 0 ∨ (2nd ‘𝑝) ≠ 0 )))
248	245, 247	imbi12d 337	. . . . . . . . . . 11 ⊢ (𝑦 = (2nd ‘𝑝) → ((((1st ‘𝑝) + 𝑦) ≠ (0g‘𝐾) → ((1st ‘𝑝) ≠ 0 ∨ 𝑦 ≠ 0 )) ↔ (((1st ‘𝑝) + (2nd ‘𝑝)) ≠ (0g‘𝐾) → ((1st ‘𝑝) ≠ 0 ∨ (2nd ‘𝑝) ≠ 0 ))))
249	243, 248	rspc2v 3549	. . . . . . . . . 10 ⊢ (((1st ‘𝑝) ∈ 𝐵 ∧ (2nd ‘𝑝) ∈ 𝐵) → (∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ((𝑥 + 𝑦) ≠ (0g‘𝐾) → (𝑥 ≠ 0 ∨ 𝑦 ≠ 0 )) → (((1st ‘𝑝) + (2nd ‘𝑝)) ≠ (0g‘𝐾) → ((1st ‘𝑝) ≠ 0 ∨ (2nd ‘𝑝) ≠ 0 ))))
250	237, 238, 249	syl2anc 576	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑧 ∈ (ran (𝐹 ∘𝑓 + 𝐺) ∖ {(0g‘𝐾)})) ∧ 𝑝 ∈ ((◡ + “ {𝑧}) ∩ (ran 𝐹 × ran 𝐺))) → (∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ((𝑥 + 𝑦) ≠ (0g‘𝐾) → (𝑥 ≠ 0 ∨ 𝑦 ≠ 0 )) → (((1st ‘𝑝) + (2nd ‘𝑝)) ≠ (0g‘𝐾) → ((1st ‘𝑝) ≠ 0 ∨ (2nd ‘𝑝) ≠ 0 ))))
251	216, 235, 250	mp2d 49	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑧 ∈ (ran (𝐹 ∘𝑓 + 𝐺) ∖ {(0g‘𝐾)})) ∧ 𝑝 ∈ ((◡ + “ {𝑧}) ∩ (ran 𝐹 × ran 𝐺))) → ((1st ‘𝑝) ≠ 0 ∨ (2nd ‘𝑝) ≠ 0 ))
252	3, 4, 11, 12, 13, 14, 15, 16, 17, 19, 2, 75	sibfinima 31239	. . . . . . . 8 ⊢ (((𝜑 ∧ (1st ‘𝑝) ∈ ran 𝐹 ∧ (2nd ‘𝑝) ∈ ran 𝐺) ∧ ((1st ‘𝑝) ≠ 0 ∨ (2nd ‘𝑝) ≠ 0 )) → (𝑀‘((◡𝐹 “ {(1st ‘𝑝)}) ∩ (◡𝐺 “ {(2nd ‘𝑝)}))) ∈ (0[,)+∞))
253	200, 204, 206, 251, 252	syl31anc 1353	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑧 ∈ (ran (𝐹 ∘𝑓 + 𝐺) ∖ {(0g‘𝐾)})) ∧ 𝑝 ∈ ((◡ + “ {𝑧}) ∩ (ran 𝐹 × ran 𝐺))) → (𝑀‘((◡𝐹 “ {(1st ‘𝑝)}) ∩ (◡𝐺 “ {(2nd ‘𝑝)}))) ∈ (0[,)+∞))
254	199, 253	esumpfinval 30975	. . . . . 6 ⊢ ((𝜑 ∧ 𝑧 ∈ (ran (𝐹 ∘𝑓 + 𝐺) ∖ {(0g‘𝐾)})) → Σ*𝑝 ∈ ((◡ + “ {𝑧}) ∩ (ran 𝐹 × ran 𝐺))(𝑀‘((◡𝐹 “ {(1st ‘𝑝)}) ∩ (◡𝐺 “ {(2nd ‘𝑝)}))) = Σ𝑝 ∈ ((◡ + “ {𝑧}) ∩ (ran 𝐹 × ran 𝐺))(𝑀‘((◡𝐹 “ {(1st ‘𝑝)}) ∩ (◡𝐺 “ {(2nd ‘𝑝)}))))
255	172, 196, 254	3eqtrd 2819	. . . . 5 ⊢ ((𝜑 ∧ 𝑧 ∈ (ran (𝐹 ∘𝑓 + 𝐺) ∖ {(0g‘𝐾)})) → (𝑀‘(◡(𝐹 ∘𝑓 + 𝐺) “ {𝑧})) = Σ𝑝 ∈ ((◡ + “ {𝑧}) ∩ (ran 𝐹 × ran 𝐺))(𝑀‘((◡𝐹 “ {(1st ‘𝑝)}) ∩ (◡𝐺 “ {(2nd ‘𝑝)}))))
256		rge0ssre 12660	. . . . . . 7 ⊢ (0[,)+∞) ⊆ ℝ
257	256, 253	sseldi 3857	. . . . . 6 ⊢ (((𝜑 ∧ 𝑧 ∈ (ran (𝐹 ∘𝑓 + 𝐺) ∖ {(0g‘𝐾)})) ∧ 𝑝 ∈ ((◡ + “ {𝑧}) ∩ (ran 𝐹 × ran 𝐺))) → (𝑀‘((◡𝐹 “ {(1st ‘𝑝)}) ∩ (◡𝐺 “ {(2nd ‘𝑝)}))) ∈ ℝ)
258	199, 257	fsumrecl 14951	. . . . 5 ⊢ ((𝜑 ∧ 𝑧 ∈ (ran (𝐹 ∘𝑓 + 𝐺) ∖ {(0g‘𝐾)})) → Σ𝑝 ∈ ((◡ + “ {𝑧}) ∩ (ran 𝐹 × ran 𝐺))(𝑀‘((◡𝐹 “ {(1st ‘𝑝)}) ∩ (◡𝐺 “ {(2nd ‘𝑝)}))) ∈ ℝ)
259	255, 258	eqeltrd 2867	. . . 4 ⊢ ((𝜑 ∧ 𝑧 ∈ (ran (𝐹 ∘𝑓 + 𝐺) ∖ {(0g‘𝐾)})) → (𝑀‘(◡(𝐹 ∘𝑓 + 𝐺) “ {𝑧})) ∈ ℝ)
260	175	adantr 473	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑧 ∈ (ran (𝐹 ∘𝑓 + 𝐺) ∖ {(0g‘𝐾)})) ∧ 𝑝 ∈ ((◡ + “ {𝑧}) ∩ (ran 𝐹 × ran 𝐺))) → 𝑀 ∈ (measures‘dom 𝑀))
261	176, 109	sylanl2 668	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑧 ∈ (ran (𝐹 ∘𝑓 + 𝐺) ∖ {(0g‘𝐾)})) ∧ 𝑝 ∈ ((◡ + “ {𝑧}) ∩ (ran 𝐹 × ran 𝐺))) → ((◡𝐹 “ {(1st ‘𝑝)}) ∩ (◡𝐺 “ {(2nd ‘𝑝)})) ∈ dom 𝑀)
262		measge0 31108	. . . . . . 7 ⊢ ((𝑀 ∈ (measures‘dom 𝑀) ∧ ((◡𝐹 “ {(1st ‘𝑝)}) ∩ (◡𝐺 “ {(2nd ‘𝑝)})) ∈ dom 𝑀) → 0 ≤ (𝑀‘((◡𝐹 “ {(1st ‘𝑝)}) ∩ (◡𝐺 “ {(2nd ‘𝑝)}))))
263	260, 261, 262	syl2anc 576	. . . . . 6 ⊢ (((𝜑 ∧ 𝑧 ∈ (ran (𝐹 ∘𝑓 + 𝐺) ∖ {(0g‘𝐾)})) ∧ 𝑝 ∈ ((◡ + “ {𝑧}) ∩ (ran 𝐹 × ran 𝐺))) → 0 ≤ (𝑀‘((◡𝐹 “ {(1st ‘𝑝)}) ∩ (◡𝐺 “ {(2nd ‘𝑝)}))))
264	199, 257, 263	fsumge0 15010	. . . . 5 ⊢ ((𝜑 ∧ 𝑧 ∈ (ran (𝐹 ∘𝑓 + 𝐺) ∖ {(0g‘𝐾)})) → 0 ≤ Σ𝑝 ∈ ((◡ + “ {𝑧}) ∩ (ran 𝐹 × ran 𝐺))(𝑀‘((◡𝐹 “ {(1st ‘𝑝)}) ∩ (◡𝐺 “ {(2nd ‘𝑝)}))))
265	264, 255	breqtrrd 4957	. . . 4 ⊢ ((𝜑 ∧ 𝑧 ∈ (ran (𝐹 ∘𝑓 + 𝐺) ∖ {(0g‘𝐾)})) → 0 ≤ (𝑀‘(◡(𝐹 ∘𝑓 + 𝐺) “ {𝑧})))
266		elrege0 12658	. . . 4 ⊢ ((𝑀‘(◡(𝐹 ∘𝑓 + 𝐺) “ {𝑧})) ∈ (0[,)+∞) ↔ ((𝑀‘(◡(𝐹 ∘𝑓 + 𝐺) “ {𝑧})) ∈ ℝ ∧ 0 ≤ (𝑀‘(◡(𝐹 ∘𝑓 + 𝐺) “ {𝑧}))))
267	259, 265, 266	sylanbrc 575	. . 3 ⊢ ((𝜑 ∧ 𝑧 ∈ (ran (𝐹 ∘𝑓 + 𝐺) ∖ {(0g‘𝐾)})) → (𝑀‘(◡(𝐹 ∘𝑓 + 𝐺) “ {𝑧})) ∈ (0[,)+∞))
268	267	ralrimiva 3133	. 2 ⊢ (𝜑 → ∀𝑧 ∈ (ran (𝐹 ∘𝑓 + 𝐺) ∖ {(0g‘𝐾)})(𝑀‘(◡(𝐹 ∘𝑓 + 𝐺) “ {𝑧})) ∈ (0[,)+∞))
269		eqid 2779	. . 3 ⊢ (sigaGen‘(TopOpen‘𝐾)) = (sigaGen‘(TopOpen‘𝐾))
270		eqid 2779	. . 3 ⊢ (0g‘𝐾) = (0g‘𝐾)
271		eqid 2779	. . 3 ⊢ ( ·𝑠 ‘𝐾) = ( ·𝑠 ‘𝐾)
272		eqid 2779	. . 3 ⊢ (ℝHom‘(Scalar‘𝐾)) = (ℝHom‘(Scalar‘𝐾))
273	27, 28, 269, 270, 271, 272, 26, 16	issibf 31233	. 2 ⊢ (𝜑 → ((𝐹 ∘𝑓 + 𝐺) ∈ dom (𝐾sitg𝑀) ↔ ((𝐹 ∘𝑓 + 𝐺) ∈ (dom 𝑀MblFnM(sigaGen‘(TopOpen‘𝐾))) ∧ ran (𝐹 ∘𝑓 + 𝐺) ∈ Fin ∧ ∀𝑧 ∈ (ran (𝐹 ∘𝑓 + 𝐺) ∖ {(0g‘𝐾)})(𝑀‘(◡(𝐹 ∘𝑓 + 𝐺) “ {𝑧})) ∈ (0[,)+∞))))
274	170, 138, 268, 273	mpbir3and 1322	1 ⊢ (𝜑 → (𝐹 ∘𝑓 + 𝐺) ∈ dom (𝐾sitg𝑀))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 198   ∧ wa 387   ∨ wo 833   = wceq 1507   ∈ wcel 2050   ≠ wne 2968  ∀wral 3089  Vcvv 3416   ∖ cdif 3827   ∪ cun 3828   ∩ cin 3829   ⊆ wss 3830  ∅c0 4179  {csn 4441  ⟨cop 4447  ∪ cuni 4712  ∪ ciun 4792  Disj wdisj 4897   class class class wbr 4929   × cxp 5405  ^◡ccnv 5406  dom cdm 5407  ran crn 5408   “ cima 5410  Fun wfun 6182   Fn wfn 6183  ⟶wf 6184  ‘cfv 6188  (class class class)co 6976   ∘_𝑓 cof 7225  ωcom 7396  1^st c1st 7499  2^nd c2nd 7500   ↑_𝑚 cmap 8206   ≼ cdom 8304   ≺ csdm 8305  Fincfn 8306  ℝcr 10334  0cc0 10335  +∞cpnf 10471   ≤ cle 10475  [,)cico 12556  Σcsu 14903  Basecbs 16339  Scalarcsca 16424   ·_𝑠 cvsca 16425  TopOpenctopn 16551  0_gc0g 16569  Topctop 21205  TopSpctps 21244  Clsdccld 21328  Frect1 21619  ℝHomcrrh 30875  Σ^*cesum 30927  sigAlgebracsiga 31008  sigaGencsigagen 31039  measurescmeas 31096  MblFnMcmbfm 31150  sitgcsitg 31229

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1758  ax-4 1772  ax-5 1869  ax-6 1928  ax-7 1965  ax-8 2052  ax-9 2059  ax-10 2079  ax-11 2093  ax-12 2106  ax-13 2301  ax-ext 2751  ax-rep 5049  ax-sep 5060  ax-nul 5067  ax-pow 5119  ax-pr 5186  ax-un 7279  ax-inf2 8898  ax-ac2 9683  ax-cnex 10391  ax-resscn 10392  ax-1cn 10393  ax-icn 10394  ax-addcl 10395  ax-addrcl 10396  ax-mulcl 10397  ax-mulrcl 10398  ax-mulcom 10399  ax-addass 10400  ax-mulass 10401  ax-distr 10402  ax-i2m1 10403  ax-1ne0 10404  ax-1rid 10405  ax-rnegex 10406  ax-rrecex 10407  ax-cnre 10408  ax-pre-lttri 10409  ax-pre-lttrn 10410  ax-pre-ltadd 10411  ax-pre-mulgt0 10412  ax-pre-sup 10413  ax-addf 10414  ax-mulf 10415

This theorem depends on definitions:  df-bi 199  df-an 388  df-or 834  df-3or 1069  df-3an 1070  df-tru 1510  df-fal 1520  df-ex 1743  df-nf 1747  df-sb 2016  df-mo 2547  df-eu 2584  df-clab 2760  df-cleq 2772  df-clel 2847  df-nfc 2919  df-ne 2969  df-nel 3075  df-ral 3094  df-rex 3095  df-reu 3096  df-rmo 3097  df-rab 3098  df-v 3418  df-sbc 3683  df-csb 3788  df-dif 3833  df-un 3835  df-in 3837  df-ss 3844  df-pss 3846  df-nul 4180  df-if 4351  df-pw 4424  df-sn 4442  df-pr 4444  df-tp 4446  df-op 4448  df-uni 4713  df-int 4750  df-iun 4794  df-iin 4795  df-disj 4898  df-br 4930  df-opab 4992  df-mpt 5009  df-tr 5031  df-id 5312  df-eprel 5317  df-po 5326  df-so 5327  df-fr 5366  df-se 5367  df-we 5368  df-xp 5413  df-rel 5414  df-cnv 5415  df-co 5416  df-dm 5417  df-rn 5418  df-res 5419  df-ima 5420  df-pred 5986  df-ord 6032  df-on 6033  df-lim 6034  df-suc 6035  df-iota 6152  df-fun 6190  df-fn 6191  df-f 6192  df-f1 6193  df-fo 6194  df-f1o 6195  df-fv 6196  df-isom 6197  df-riota 6937  df-ov 6979  df-oprab 6980  df-mpo 6981  df-of 7227  df-om 7397  df-1st 7501  df-2nd 7502  df-supp 7634  df-wrecs 7750  df-recs 7812  df-rdg 7850  df-1o 7905  df-2o 7906  df-oadd 7909  df-er 8089  df-map 8208  df-pm 8209  df-ixp 8260  df-en 8307  df-dom 8308  df-sdom 8309  df-fin 8310  df-fsupp 8629  df-fi 8670  df-sup 8701  df-inf 8702  df-oi 8769  df-dju 9124  df-card 9162  df-acn 9165  df-ac 9336  df-cda 9388  df-pnf 10476  df-mnf 10477  df-xr 10478  df-ltxr 10479  df-le 10480  df-sub 10672  df-neg 10673  df-div 11099  df-nn 11440  df-2 11503  df-3 11504  df-4 11505  df-5 11506  df-6 11507  df-7 11508  df-8 11509  df-9 11510  df-n0 11708  df-z 11794  df-dec 11912  df-uz 12059  df-q 12163  df-rp 12205  df-xneg 12324  df-xadd 12325  df-xmul 12326  df-ioo 12558  df-ioc 12559  df-ico 12560  df-icc 12561  df-fz 12709  df-fzo 12850  df-fl 12977  df-mod 13053  df-seq 13185  df-exp 13245  df-fac 13449  df-bc 13478  df-hash 13506  df-shft 14287  df-cj 14319  df-re 14320  df-im 14321  df-sqrt 14455  df-abs 14456  df-limsup 14689  df-clim 14706  df-rlim 14707  df-sum 14904  df-ef 15281  df-sin 15283  df-cos 15284  df-pi 15286  df-struct 16341  df-ndx 16342  df-slot 16343  df-base 16345  df-sets 16346  df-ress 16347  df-plusg 16434  df-mulr 16435  df-starv 16436  df-sca 16437  df-vsca 16438  df-ip 16439  df-tset 16440  df-ple 16441  df-ds 16443  df-unif 16444  df-hom 16445  df-cco 16446  df-rest 16552  df-topn 16553  df-0g 16571  df-gsum 16572  df-topgen 16573  df-pt 16574  df-prds 16577  df-ordt 16630  df-xrs 16631  df-qtop 16636  df-imas 16637  df-xps 16639  df-mre 16715  df-mrc 16716  df-acs 16718  df-ps 17668  df-tsr 17669  df-plusf 17709  df-mgm 17710  df-sgrp 17752  df-mnd 17763  df-mhm 17803  df-submnd 17804  df-grp 17894  df-minusg 17895  df-sbg 17896  df-mulg 18012  df-subg 18060  df-cntz 18218  df-cmn 18668  df-abl 18669  df-mgp 18963  df-ur 18975  df-ring 19022  df-cring 19023  df-subrg 19256  df-abv 19310  df-lmod 19358  df-scaf 19359  df-sra 19666  df-rgmod 19667  df-psmet 20239  df-xmet 20240  df-met 20241  df-bl 20242  df-mopn 20243  df-fbas 20244  df-fg 20245  df-cnfld 20248  df-top 21206  df-topon 21223  df-topsp 21245  df-bases 21258  df-cld 21331  df-ntr 21332  df-cls 21333  df-nei 21410  df-lp 21448  df-perf 21449  df-cn 21539  df-cnp 21540  df-t1 21626  df-haus 21627  df-tx 21874  df-hmeo 22067  df-fil 22158  df-fm 22250  df-flim 22251  df-flf 22252  df-tmd 22384  df-tgp 22385  df-tsms 22438  df-trg 22471  df-xms 22633  df-ms 22634  df-tms 22635  df-nm 22895  df-ngp 22896  df-nrg 22898  df-nlm 22899  df-ii 23188  df-cncf 23189  df-limc 24167  df-dv 24168  df-log 24841  df-esum 30928  df-siga 31009  df-sigagen 31040  df-meas 31097  df-mbfm 31151  df-sitg 31230

This theorem is referenced by:  sitmcl  31251