Theorem sibfof

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)

	Ref	Expression
Hypotheses	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	sibfof	⊢ ( 𝜑 → ( 𝐹 ∘f + 𝐺 ) ∈ dom ( 𝐾 sitg 𝑀 ) )

Proof

Step	Hyp	Ref	Expression
1		sitgval.b	⊢ 𝐵 = ( Base ‘ 𝑊 )
2		sitgval.j	⊢ 𝐽 = ( TopOpen ‘ 𝑊 )
3		sitgval.s	⊢ 𝑆 = ( sigaGen ‘ 𝐽 )
4		sitgval.0	⊢ 0 = ( 0g ‘ 𝑊 )
5		sitgval.x	⊢ · = ( ·𝑠 ‘ 𝑊 )
6		sitgval.h	⊢ 𝐻 = ( ℝHom ‘ ( Scalar ‘ 𝑊 ) )
7		sitgval.1	⊢ ( 𝜑 → 𝑊 ∈ 𝑉 )
8		sitgval.2	⊢ ( 𝜑 → 𝑀 ∈ ∪ ran measures )
9		sibfmbl.1	⊢ ( 𝜑 → 𝐹 ∈ dom ( 𝑊 sitg 𝑀 ) )
10		sibfof.c	⊢ 𝐶 = ( Base ‘ 𝐾 )
11		sibfof.0	⊢ ( 𝜑 → 𝑊 ∈ TopSp )
12		sibfof.1	⊢ ( 𝜑 → + : ( 𝐵 × 𝐵 ) ⟶ 𝐶 )
13		sibfof.2	⊢ ( 𝜑 → 𝐺 ∈ dom ( 𝑊 sitg 𝑀 ) )
14		sibfof.3	⊢ ( 𝜑 → 𝐾 ∈ TopSp )
15		sibfof.4	⊢ ( 𝜑 → 𝐽 ∈ Fre )
16		sibfof.5	⊢ ( 𝜑 → ( 0 + 0 ) = ( 0g ‘ 𝐾 ) )
17	1 2	tpsuni	⊢ ( 𝑊 ∈ TopSp → 𝐵 = ∪ 𝐽 )
18	11 17	syl	⊢ ( 𝜑 → 𝐵 = ∪ 𝐽 )
19	18	sqxpeqd	⊢ ( 𝜑 → ( 𝐵 × 𝐵 ) = ( ∪ 𝐽 × ∪ 𝐽 ) )
20	19	feq2d	⊢ ( 𝜑 → ( + : ( 𝐵 × 𝐵 ) ⟶ 𝐶 ↔ + : ( ∪ 𝐽 × ∪ 𝐽 ) ⟶ 𝐶 ) )
21	12 20	mpbid	⊢ ( 𝜑 → + : ( ∪ 𝐽 × ∪ 𝐽 ) ⟶ 𝐶 )
22	21	fovrnda	⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ ∪ 𝐽 ∧ 𝑥 ∈ ∪ 𝐽 ) ) → ( 𝑧 + 𝑥 ) ∈ 𝐶 )
23	1 2 3 4 5 6 7 8 9	sibff	⊢ ( 𝜑 → 𝐹 : ∪ dom 𝑀 ⟶ ∪ 𝐽 )
24	1 2 3 4 5 6 7 8 13	sibff	⊢ ( 𝜑 → 𝐺 : ∪ dom 𝑀 ⟶ ∪ 𝐽 )
25		dmexg	⊢ ( 𝑀 ∈ ∪ ran measures → dom 𝑀 ∈ V )
26		uniexg	⊢ ( dom 𝑀 ∈ V → ∪ dom 𝑀 ∈ V )
27	8 25 26	3syl	⊢ ( 𝜑 → ∪ dom 𝑀 ∈ V )
28		inidm	⊢ ( ∪ dom 𝑀 ∩ ∪ dom 𝑀 ) = ∪ dom 𝑀
29	22 23 24 27 27 28	off	⊢ ( 𝜑 → ( 𝐹 ∘f + 𝐺 ) : ∪ dom 𝑀 ⟶ 𝐶 )
30		eqid	⊢ ( TopOpen ‘ 𝐾 ) = ( TopOpen ‘ 𝐾 )
31	10 30	tpsuni	⊢ ( 𝐾 ∈ TopSp → 𝐶 = ∪ ( TopOpen ‘ 𝐾 ) )
32	14 31	syl	⊢ ( 𝜑 → 𝐶 = ∪ ( TopOpen ‘ 𝐾 ) )
33		fvex	⊢ ( TopOpen ‘ 𝐾 ) ∈ V
34		unisg	⊢ ( ( TopOpen ‘ 𝐾 ) ∈ V → ∪ ( sigaGen ‘ ( TopOpen ‘ 𝐾 ) ) = ∪ ( TopOpen ‘ 𝐾 ) )
35	33 34	ax-mp	⊢ ∪ ( sigaGen ‘ ( TopOpen ‘ 𝐾 ) ) = ∪ ( TopOpen ‘ 𝐾 )
36	32 35	eqtr4di	⊢ ( 𝜑 → 𝐶 = ∪ ( sigaGen ‘ ( TopOpen ‘ 𝐾 ) ) )
37	36	feq3d	⊢ ( 𝜑 → ( ( 𝐹 ∘f + 𝐺 ) : ∪ dom 𝑀 ⟶ 𝐶 ↔ ( 𝐹 ∘f + 𝐺 ) : ∪ dom 𝑀 ⟶ ∪ ( sigaGen ‘ ( TopOpen ‘ 𝐾 ) ) ) )
38	29 37	mpbid	⊢ ( 𝜑 → ( 𝐹 ∘f + 𝐺 ) : ∪ dom 𝑀 ⟶ ∪ ( sigaGen ‘ ( TopOpen ‘ 𝐾 ) ) )
39	33	a1i	⊢ ( 𝜑 → ( TopOpen ‘ 𝐾 ) ∈ V )
40	39	sgsiga	⊢ ( 𝜑 → ( sigaGen ‘ ( TopOpen ‘ 𝐾 ) ) ∈ ∪ ran sigAlgebra )
41	40	uniexd	⊢ ( 𝜑 → ∪ ( sigaGen ‘ ( TopOpen ‘ 𝐾 ) ) ∈ V )
42	41 27	elmapd	⊢ ( 𝜑 → ( ( 𝐹 ∘f + 𝐺 ) ∈ ( ∪ ( sigaGen ‘ ( TopOpen ‘ 𝐾 ) ) ↑m ∪ dom 𝑀 ) ↔ ( 𝐹 ∘f + 𝐺 ) : ∪ dom 𝑀 ⟶ ∪ ( sigaGen ‘ ( TopOpen ‘ 𝐾 ) ) ) )
43	38 42	mpbird	⊢ ( 𝜑 → ( 𝐹 ∘f + 𝐺 ) ∈ ( ∪ ( sigaGen ‘ ( TopOpen ‘ 𝐾 ) ) ↑m ∪ dom 𝑀 ) )
44		inundif	⊢ ( ( 𝑏 ∩ ran ( 𝐹 ∘f + 𝐺 ) ) ∪ ( 𝑏 ∖ ran ( 𝐹 ∘f + 𝐺 ) ) ) = 𝑏
45	44	imaeq2i	⊢ ( ◡ ( 𝐹 ∘f + 𝐺 ) “ ( ( 𝑏 ∩ ran ( 𝐹 ∘f + 𝐺 ) ) ∪ ( 𝑏 ∖ ran ( 𝐹 ∘f + 𝐺 ) ) ) ) = ( ◡ ( 𝐹 ∘f + 𝐺 ) “ 𝑏 )
46		ffun	⊢ ( ( 𝐹 ∘f + 𝐺 ) : ∪ dom 𝑀 ⟶ 𝐶 → Fun ( 𝐹 ∘f + 𝐺 ) )
47		unpreima	⊢ ( Fun ( 𝐹 ∘f + 𝐺 ) → ( ◡ ( 𝐹 ∘f + 𝐺 ) “ ( ( 𝑏 ∩ ran ( 𝐹 ∘f + 𝐺 ) ) ∪ ( 𝑏 ∖ ran ( 𝐹 ∘f + 𝐺 ) ) ) ) = ( ( ◡ ( 𝐹 ∘f + 𝐺 ) “ ( 𝑏 ∩ ran ( 𝐹 ∘f + 𝐺 ) ) ) ∪ ( ◡ ( 𝐹 ∘f + 𝐺 ) “ ( 𝑏 ∖ ran ( 𝐹 ∘f + 𝐺 ) ) ) ) )
48	29 46 47	3syl	⊢ ( 𝜑 → ( ◡ ( 𝐹 ∘f + 𝐺 ) “ ( ( 𝑏 ∩ ran ( 𝐹 ∘f + 𝐺 ) ) ∪ ( 𝑏 ∖ ran ( 𝐹 ∘f + 𝐺 ) ) ) ) = ( ( ◡ ( 𝐹 ∘f + 𝐺 ) “ ( 𝑏 ∩ ran ( 𝐹 ∘f + 𝐺 ) ) ) ∪ ( ◡ ( 𝐹 ∘f + 𝐺 ) “ ( 𝑏 ∖ ran ( 𝐹 ∘f + 𝐺 ) ) ) ) )
49	48	adantr	⊢ ( ( 𝜑 ∧ 𝑏 ∈ ( sigaGen ‘ ( TopOpen ‘ 𝐾 ) ) ) → ( ◡ ( 𝐹 ∘f + 𝐺 ) “ ( ( 𝑏 ∩ ran ( 𝐹 ∘f + 𝐺 ) ) ∪ ( 𝑏 ∖ ran ( 𝐹 ∘f + 𝐺 ) ) ) ) = ( ( ◡ ( 𝐹 ∘f + 𝐺 ) “ ( 𝑏 ∩ ran ( 𝐹 ∘f + 𝐺 ) ) ) ∪ ( ◡ ( 𝐹 ∘f + 𝐺 ) “ ( 𝑏 ∖ ran ( 𝐹 ∘f + 𝐺 ) ) ) ) )
50	45 49	eqtr3id	⊢ ( ( 𝜑 ∧ 𝑏 ∈ ( sigaGen ‘ ( TopOpen ‘ 𝐾 ) ) ) → ( ◡ ( 𝐹 ∘f + 𝐺 ) “ 𝑏 ) = ( ( ◡ ( 𝐹 ∘f + 𝐺 ) “ ( 𝑏 ∩ ran ( 𝐹 ∘f + 𝐺 ) ) ) ∪ ( ◡ ( 𝐹 ∘f + 𝐺 ) “ ( 𝑏 ∖ ran ( 𝐹 ∘f + 𝐺 ) ) ) ) )
51		dmmeas	⊢ ( 𝑀 ∈ ∪ ran measures → dom 𝑀 ∈ ∪ ran sigAlgebra )
52	8 51	syl	⊢ ( 𝜑 → dom 𝑀 ∈ ∪ ran sigAlgebra )
53	52	adantr	⊢ ( ( 𝜑 ∧ 𝑏 ∈ ( sigaGen ‘ ( TopOpen ‘ 𝐾 ) ) ) → dom 𝑀 ∈ ∪ ran sigAlgebra )
54		imaiun	⊢ ( ◡ ( 𝐹 ∘f + 𝐺 ) “ ∪ 𝑧 ∈ ( 𝑏 ∩ ran ( 𝐹 ∘f + 𝐺 ) ) { 𝑧 } ) = ∪ 𝑧 ∈ ( 𝑏 ∩ ran ( 𝐹 ∘f + 𝐺 ) ) ( ◡ ( 𝐹 ∘f + 𝐺 ) “ { 𝑧 } )
55		iunid	⊢ ∪ 𝑧 ∈ ( 𝑏 ∩ ran ( 𝐹 ∘f + 𝐺 ) ) { 𝑧 } = ( 𝑏 ∩ ran ( 𝐹 ∘f + 𝐺 ) )
56	55	imaeq2i	⊢ ( ◡ ( 𝐹 ∘f + 𝐺 ) “ ∪ 𝑧 ∈ ( 𝑏 ∩ ran ( 𝐹 ∘f + 𝐺 ) ) { 𝑧 } ) = ( ◡ ( 𝐹 ∘f + 𝐺 ) “ ( 𝑏 ∩ ran ( 𝐹 ∘f + 𝐺 ) ) )
57	54 56	eqtr3i	⊢ ∪ 𝑧 ∈ ( 𝑏 ∩ ran ( 𝐹 ∘f + 𝐺 ) ) ( ◡ ( 𝐹 ∘f + 𝐺 ) “ { 𝑧 } ) = ( ◡ ( 𝐹 ∘f + 𝐺 ) “ ( 𝑏 ∩ ran ( 𝐹 ∘f + 𝐺 ) ) )
58		inss2	⊢ ( 𝑏 ∩ ran ( 𝐹 ∘f + 𝐺 ) ) ⊆ ran ( 𝐹 ∘f + 𝐺 )
59	18	feq3d	⊢ ( 𝜑 → ( 𝐹 : ∪ dom 𝑀 ⟶ 𝐵 ↔ 𝐹 : ∪ dom 𝑀 ⟶ ∪ 𝐽 ) )
60	23 59	mpbird	⊢ ( 𝜑 → 𝐹 : ∪ dom 𝑀 ⟶ 𝐵 )
61	18	feq3d	⊢ ( 𝜑 → ( 𝐺 : ∪ dom 𝑀 ⟶ 𝐵 ↔ 𝐺 : ∪ dom 𝑀 ⟶ ∪ 𝐽 ) )
62	24 61	mpbird	⊢ ( 𝜑 → 𝐺 : ∪ dom 𝑀 ⟶ 𝐵 )
63	12	ffnd	⊢ ( 𝜑 → + Fn ( 𝐵 × 𝐵 ) )
64	60 62 27 63	ofpreima2	⊢ ( 𝜑 → ( ◡ ( 𝐹 ∘f + 𝐺 ) “ { 𝑧 } ) = ∪ 𝑝 ∈ ( ( ◡ + “ { 𝑧 } ) ∩ ( ran 𝐹 × ran 𝐺 ) ) ( ( ◡ 𝐹 “ { ( 1st ‘ 𝑝 ) } ) ∩ ( ◡ 𝐺 “ { ( 2nd ‘ 𝑝 ) } ) ) )
65	64	adantr	⊢ ( ( 𝜑 ∧ 𝑧 ∈ ran ( 𝐹 ∘f + 𝐺 ) ) → ( ◡ ( 𝐹 ∘f + 𝐺 ) “ { 𝑧 } ) = ∪ 𝑝 ∈ ( ( ◡ + “ { 𝑧 } ) ∩ ( ran 𝐹 × ran 𝐺 ) ) ( ( ◡ 𝐹 “ { ( 1st ‘ 𝑝 ) } ) ∩ ( ◡ 𝐺 “ { ( 2nd ‘ 𝑝 ) } ) ) )
66	52	adantr	⊢ ( ( 𝜑 ∧ 𝑧 ∈ ran ( 𝐹 ∘f + 𝐺 ) ) → dom 𝑀 ∈ ∪ ran sigAlgebra )
67	52	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ran ( 𝐹 ∘f + 𝐺 ) ) ∧ 𝑝 ∈ ( ( ◡ + “ { 𝑧 } ) ∩ ( ran 𝐹 × ran 𝐺 ) ) ) → dom 𝑀 ∈ ∪ ran sigAlgebra )
68		simpll	⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ran ( 𝐹 ∘f + 𝐺 ) ) ∧ 𝑝 ∈ ( ( ◡ + “ { 𝑧 } ) ∩ ( ran 𝐹 × ran 𝐺 ) ) ) → 𝜑 )
69		inss1	⊢ ( ( ◡ + “ { 𝑧 } ) ∩ ( ran 𝐹 × ran 𝐺 ) ) ⊆ ( ◡ + “ { 𝑧 } )
70		cnvimass	⊢ ( ◡ + “ { 𝑧 } ) ⊆ dom +
71	70 12	fssdm	⊢ ( 𝜑 → ( ◡ + “ { 𝑧 } ) ⊆ ( 𝐵 × 𝐵 ) )
72	71	adantr	⊢ ( ( 𝜑 ∧ 𝑧 ∈ ran ( 𝐹 ∘f + 𝐺 ) ) → ( ◡ + “ { 𝑧 } ) ⊆ ( 𝐵 × 𝐵 ) )
73	69 72	sstrid	⊢ ( ( 𝜑 ∧ 𝑧 ∈ ran ( 𝐹 ∘f + 𝐺 ) ) → ( ( ◡ + “ { 𝑧 } ) ∩ ( ran 𝐹 × ran 𝐺 ) ) ⊆ ( 𝐵 × 𝐵 ) )
74	73	sselda	⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ran ( 𝐹 ∘f + 𝐺 ) ) ∧ 𝑝 ∈ ( ( ◡ + “ { 𝑧 } ) ∩ ( ran 𝐹 × ran 𝐺 ) ) ) → 𝑝 ∈ ( 𝐵 × 𝐵 ) )
75	52	adantr	⊢ ( ( 𝜑 ∧ 𝑝 ∈ ( 𝐵 × 𝐵 ) ) → dom 𝑀 ∈ ∪ ran sigAlgebra )
76	15	sgsiga	⊢ ( 𝜑 → ( sigaGen ‘ 𝐽 ) ∈ ∪ ran sigAlgebra )
77	3 76	eqeltrid	⊢ ( 𝜑 → 𝑆 ∈ ∪ ran sigAlgebra )
78	77	adantr	⊢ ( ( 𝜑 ∧ 𝑝 ∈ ( 𝐵 × 𝐵 ) ) → 𝑆 ∈ ∪ ran sigAlgebra )
79	1 2 3 4 5 6 7 8 9	sibfmbl	⊢ ( 𝜑 → 𝐹 ∈ ( dom 𝑀 MblFnM 𝑆 ) )
80	79	adantr	⊢ ( ( 𝜑 ∧ 𝑝 ∈ ( 𝐵 × 𝐵 ) ) → 𝐹 ∈ ( dom 𝑀 MblFnM 𝑆 ) )
81	2	tpstop	⊢ ( 𝑊 ∈ TopSp → 𝐽 ∈ Top )
82		cldssbrsiga	⊢ ( 𝐽 ∈ Top → ( Clsd ‘ 𝐽 ) ⊆ ( sigaGen ‘ 𝐽 ) )
83	11 81 82	3syl	⊢ ( 𝜑 → ( Clsd ‘ 𝐽 ) ⊆ ( sigaGen ‘ 𝐽 ) )
84	83	adantr	⊢ ( ( 𝜑 ∧ 𝑝 ∈ ( 𝐵 × 𝐵 ) ) → ( Clsd ‘ 𝐽 ) ⊆ ( sigaGen ‘ 𝐽 ) )
85	15	adantr	⊢ ( ( 𝜑 ∧ 𝑝 ∈ ( 𝐵 × 𝐵 ) ) → 𝐽 ∈ Fre )
86		xp1st	⊢ ( 𝑝 ∈ ( 𝐵 × 𝐵 ) → ( 1st ‘ 𝑝 ) ∈ 𝐵 )
87	86	adantl	⊢ ( ( 𝜑 ∧ 𝑝 ∈ ( 𝐵 × 𝐵 ) ) → ( 1st ‘ 𝑝 ) ∈ 𝐵 )
88	18	adantr	⊢ ( ( 𝜑 ∧ 𝑝 ∈ ( 𝐵 × 𝐵 ) ) → 𝐵 = ∪ 𝐽 )
89	87 88	eleqtrd	⊢ ( ( 𝜑 ∧ 𝑝 ∈ ( 𝐵 × 𝐵 ) ) → ( 1st ‘ 𝑝 ) ∈ ∪ 𝐽 )
90		eqid	⊢ ∪ 𝐽 = ∪ 𝐽
91	90	t1sncld	⊢ ( ( 𝐽 ∈ Fre ∧ ( 1st ‘ 𝑝 ) ∈ ∪ 𝐽 ) → { ( 1st ‘ 𝑝 ) } ∈ ( Clsd ‘ 𝐽 ) )
92	85 89 91	syl2anc	⊢ ( ( 𝜑 ∧ 𝑝 ∈ ( 𝐵 × 𝐵 ) ) → { ( 1st ‘ 𝑝 ) } ∈ ( Clsd ‘ 𝐽 ) )
93	84 92	sseldd	⊢ ( ( 𝜑 ∧ 𝑝 ∈ ( 𝐵 × 𝐵 ) ) → { ( 1st ‘ 𝑝 ) } ∈ ( sigaGen ‘ 𝐽 ) )
94	93 3	eleqtrrdi	⊢ ( ( 𝜑 ∧ 𝑝 ∈ ( 𝐵 × 𝐵 ) ) → { ( 1st ‘ 𝑝 ) } ∈ 𝑆 )
95	75 78 80 94	mbfmcnvima	⊢ ( ( 𝜑 ∧ 𝑝 ∈ ( 𝐵 × 𝐵 ) ) → ( ◡ 𝐹 “ { ( 1st ‘ 𝑝 ) } ) ∈ dom 𝑀 )
96	68 74 95	syl2anc	⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ran ( 𝐹 ∘f + 𝐺 ) ) ∧ 𝑝 ∈ ( ( ◡ + “ { 𝑧 } ) ∩ ( ran 𝐹 × ran 𝐺 ) ) ) → ( ◡ 𝐹 “ { ( 1st ‘ 𝑝 ) } ) ∈ dom 𝑀 )
97	1 2 3 4 5 6 7 8 13	sibfmbl	⊢ ( 𝜑 → 𝐺 ∈ ( dom 𝑀 MblFnM 𝑆 ) )
98	97	adantr	⊢ ( ( 𝜑 ∧ 𝑝 ∈ ( 𝐵 × 𝐵 ) ) → 𝐺 ∈ ( dom 𝑀 MblFnM 𝑆 ) )
99		xp2nd	⊢ ( 𝑝 ∈ ( 𝐵 × 𝐵 ) → ( 2nd ‘ 𝑝 ) ∈ 𝐵 )
100	99	adantl	⊢ ( ( 𝜑 ∧ 𝑝 ∈ ( 𝐵 × 𝐵 ) ) → ( 2nd ‘ 𝑝 ) ∈ 𝐵 )
101	100 88	eleqtrd	⊢ ( ( 𝜑 ∧ 𝑝 ∈ ( 𝐵 × 𝐵 ) ) → ( 2nd ‘ 𝑝 ) ∈ ∪ 𝐽 )
102	90	t1sncld	⊢ ( ( 𝐽 ∈ Fre ∧ ( 2nd ‘ 𝑝 ) ∈ ∪ 𝐽 ) → { ( 2nd ‘ 𝑝 ) } ∈ ( Clsd ‘ 𝐽 ) )
103	85 101 102	syl2anc	⊢ ( ( 𝜑 ∧ 𝑝 ∈ ( 𝐵 × 𝐵 ) ) → { ( 2nd ‘ 𝑝 ) } ∈ ( Clsd ‘ 𝐽 ) )
104	84 103	sseldd	⊢ ( ( 𝜑 ∧ 𝑝 ∈ ( 𝐵 × 𝐵 ) ) → { ( 2nd ‘ 𝑝 ) } ∈ ( sigaGen ‘ 𝐽 ) )
105	104 3	eleqtrrdi	⊢ ( ( 𝜑 ∧ 𝑝 ∈ ( 𝐵 × 𝐵 ) ) → { ( 2nd ‘ 𝑝 ) } ∈ 𝑆 )
106	75 78 98 105	mbfmcnvima	⊢ ( ( 𝜑 ∧ 𝑝 ∈ ( 𝐵 × 𝐵 ) ) → ( ◡ 𝐺 “ { ( 2nd ‘ 𝑝 ) } ) ∈ dom 𝑀 )
107	68 74 106	syl2anc	⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ran ( 𝐹 ∘f + 𝐺 ) ) ∧ 𝑝 ∈ ( ( ◡ + “ { 𝑧 } ) ∩ ( ran 𝐹 × ran 𝐺 ) ) ) → ( ◡ 𝐺 “ { ( 2nd ‘ 𝑝 ) } ) ∈ dom 𝑀 )
108		inelsiga	⊢ ( ( dom 𝑀 ∈ ∪ ran sigAlgebra ∧ ( ◡ 𝐹 “ { ( 1st ‘ 𝑝 ) } ) ∈ dom 𝑀 ∧ ( ◡ 𝐺 “ { ( 2nd ‘ 𝑝 ) } ) ∈ dom 𝑀 ) → ( ( ◡ 𝐹 “ { ( 1st ‘ 𝑝 ) } ) ∩ ( ◡ 𝐺 “ { ( 2nd ‘ 𝑝 ) } ) ) ∈ dom 𝑀 )
109	67 96 107 108	syl3anc	⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ran ( 𝐹 ∘f + 𝐺 ) ) ∧ 𝑝 ∈ ( ( ◡ + “ { 𝑧 } ) ∩ ( ran 𝐹 × ran 𝐺 ) ) ) → ( ( ◡ 𝐹 “ { ( 1st ‘ 𝑝 ) } ) ∩ ( ◡ 𝐺 “ { ( 2nd ‘ 𝑝 ) } ) ) ∈ dom 𝑀 )
110	109	ralrimiva	⊢ ( ( 𝜑 ∧ 𝑧 ∈ ran ( 𝐹 ∘f + 𝐺 ) ) → ∀ 𝑝 ∈ ( ( ◡ + “ { 𝑧 } ) ∩ ( ran 𝐹 × ran 𝐺 ) ) ( ( ◡ 𝐹 “ { ( 1st ‘ 𝑝 ) } ) ∩ ( ◡ 𝐺 “ { ( 2nd ‘ 𝑝 ) } ) ) ∈ dom 𝑀 )
111	1 2 3 4 5 6 7 8 9	sibfrn	⊢ ( 𝜑 → ran 𝐹 ∈ Fin )
112	1 2 3 4 5 6 7 8 13	sibfrn	⊢ ( 𝜑 → ran 𝐺 ∈ Fin )
113		xpfi	⊢ ( ( ran 𝐹 ∈ Fin ∧ ran 𝐺 ∈ Fin ) → ( ran 𝐹 × ran 𝐺 ) ∈ Fin )
114	111 112 113	syl2anc	⊢ ( 𝜑 → ( ran 𝐹 × ran 𝐺 ) ∈ Fin )
115		inss2	⊢ ( ( ◡ + “ { 𝑧 } ) ∩ ( ran 𝐹 × ran 𝐺 ) ) ⊆ ( ran 𝐹 × ran 𝐺 )
116		ssdomg	⊢ ( ( ran 𝐹 × ran 𝐺 ) ∈ Fin → ( ( ( ◡ + “ { 𝑧 } ) ∩ ( ran 𝐹 × ran 𝐺 ) ) ⊆ ( ran 𝐹 × ran 𝐺 ) → ( ( ◡ + “ { 𝑧 } ) ∩ ( ran 𝐹 × ran 𝐺 ) ) ≼ ( ran 𝐹 × ran 𝐺 ) ) )
117	114 115 116	mpisyl	⊢ ( 𝜑 → ( ( ◡ + “ { 𝑧 } ) ∩ ( ran 𝐹 × ran 𝐺 ) ) ≼ ( ran 𝐹 × ran 𝐺 ) )
118		isfinite	⊢ ( ( ran 𝐹 × ran 𝐺 ) ∈ Fin ↔ ( ran 𝐹 × ran 𝐺 ) ≺ ω )
119	118	biimpi	⊢ ( ( ran 𝐹 × ran 𝐺 ) ∈ Fin → ( ran 𝐹 × ran 𝐺 ) ≺ ω )
120		sdomdom	⊢ ( ( ran 𝐹 × ran 𝐺 ) ≺ ω → ( ran 𝐹 × ran 𝐺 ) ≼ ω )
121	114 119 120	3syl	⊢ ( 𝜑 → ( ran 𝐹 × ran 𝐺 ) ≼ ω )
122		domtr	⊢ ( ( ( ( ◡ + “ { 𝑧 } ) ∩ ( ran 𝐹 × ran 𝐺 ) ) ≼ ( ran 𝐹 × ran 𝐺 ) ∧ ( ran 𝐹 × ran 𝐺 ) ≼ ω ) → ( ( ◡ + “ { 𝑧 } ) ∩ ( ran 𝐹 × ran 𝐺 ) ) ≼ ω )
123	117 121 122	syl2anc	⊢ ( 𝜑 → ( ( ◡ + “ { 𝑧 } ) ∩ ( ran 𝐹 × ran 𝐺 ) ) ≼ ω )
124	123	adantr	⊢ ( ( 𝜑 ∧ 𝑧 ∈ ran ( 𝐹 ∘f + 𝐺 ) ) → ( ( ◡ + “ { 𝑧 } ) ∩ ( ran 𝐹 × ran 𝐺 ) ) ≼ ω )
125		nfcv	⊢ Ⅎ 𝑝 ( ( ◡ + “ { 𝑧 } ) ∩ ( ran 𝐹 × ran 𝐺 ) )
126	125	sigaclcuni	⊢ ( ( dom 𝑀 ∈ ∪ ran sigAlgebra ∧ ∀ 𝑝 ∈ ( ( ◡ + “ { 𝑧 } ) ∩ ( ran 𝐹 × ran 𝐺 ) ) ( ( ◡ 𝐹 “ { ( 1st ‘ 𝑝 ) } ) ∩ ( ◡ 𝐺 “ { ( 2nd ‘ 𝑝 ) } ) ) ∈ dom 𝑀 ∧ ( ( ◡ + “ { 𝑧 } ) ∩ ( ran 𝐹 × ran 𝐺 ) ) ≼ ω ) → ∪ 𝑝 ∈ ( ( ◡ + “ { 𝑧 } ) ∩ ( ran 𝐹 × ran 𝐺 ) ) ( ( ◡ 𝐹 “ { ( 1st ‘ 𝑝 ) } ) ∩ ( ◡ 𝐺 “ { ( 2nd ‘ 𝑝 ) } ) ) ∈ dom 𝑀 )
127	66 110 124 126	syl3anc	⊢ ( ( 𝜑 ∧ 𝑧 ∈ ran ( 𝐹 ∘f + 𝐺 ) ) → ∪ 𝑝 ∈ ( ( ◡ + “ { 𝑧 } ) ∩ ( ran 𝐹 × ran 𝐺 ) ) ( ( ◡ 𝐹 “ { ( 1st ‘ 𝑝 ) } ) ∩ ( ◡ 𝐺 “ { ( 2nd ‘ 𝑝 ) } ) ) ∈ dom 𝑀 )
128	65 127	eqeltrd	⊢ ( ( 𝜑 ∧ 𝑧 ∈ ran ( 𝐹 ∘f + 𝐺 ) ) → ( ◡ ( 𝐹 ∘f + 𝐺 ) “ { 𝑧 } ) ∈ dom 𝑀 )
129	128	ralrimiva	⊢ ( 𝜑 → ∀ 𝑧 ∈ ran ( 𝐹 ∘f + 𝐺 ) ( ◡ ( 𝐹 ∘f + 𝐺 ) “ { 𝑧 } ) ∈ dom 𝑀 )
130		ssralv	⊢ ( ( 𝑏 ∩ ran ( 𝐹 ∘f + 𝐺 ) ) ⊆ ran ( 𝐹 ∘f + 𝐺 ) → ( ∀ 𝑧 ∈ ran ( 𝐹 ∘f + 𝐺 ) ( ◡ ( 𝐹 ∘f + 𝐺 ) “ { 𝑧 } ) ∈ dom 𝑀 → ∀ 𝑧 ∈ ( 𝑏 ∩ ran ( 𝐹 ∘f + 𝐺 ) ) ( ◡ ( 𝐹 ∘f + 𝐺 ) “ { 𝑧 } ) ∈ dom 𝑀 ) )
131	58 129 130	mpsyl	⊢ ( 𝜑 → ∀ 𝑧 ∈ ( 𝑏 ∩ ran ( 𝐹 ∘f + 𝐺 ) ) ( ◡ ( 𝐹 ∘f + 𝐺 ) “ { 𝑧 } ) ∈ dom 𝑀 )
132	131	adantr	⊢ ( ( 𝜑 ∧ 𝑏 ∈ ( sigaGen ‘ ( TopOpen ‘ 𝐾 ) ) ) → ∀ 𝑧 ∈ ( 𝑏 ∩ ran ( 𝐹 ∘f + 𝐺 ) ) ( ◡ ( 𝐹 ∘f + 𝐺 ) “ { 𝑧 } ) ∈ dom 𝑀 )
133	12	ffund	⊢ ( 𝜑 → Fun + )
134		imafi	⊢ ( ( Fun + ∧ ( ran 𝐹 × ran 𝐺 ) ∈ Fin ) → ( + “ ( ran 𝐹 × ran 𝐺 ) ) ∈ Fin )
135	133 114 134	syl2anc	⊢ ( 𝜑 → ( + “ ( ran 𝐹 × ran 𝐺 ) ) ∈ Fin )
136	23 24 21 27	ofrn2	⊢ ( 𝜑 → ran ( 𝐹 ∘f + 𝐺 ) ⊆ ( + “ ( ran 𝐹 × ran 𝐺 ) ) )
137		ssfi	⊢ ( ( ( + “ ( ran 𝐹 × ran 𝐺 ) ) ∈ Fin ∧ ran ( 𝐹 ∘f + 𝐺 ) ⊆ ( + “ ( ran 𝐹 × ran 𝐺 ) ) ) → ran ( 𝐹 ∘f + 𝐺 ) ∈ Fin )
138	135 136 137	syl2anc	⊢ ( 𝜑 → ran ( 𝐹 ∘f + 𝐺 ) ∈ Fin )
139		ssdomg	⊢ ( ran ( 𝐹 ∘f + 𝐺 ) ∈ Fin → ( ( 𝑏 ∩ ran ( 𝐹 ∘f + 𝐺 ) ) ⊆ ran ( 𝐹 ∘f + 𝐺 ) → ( 𝑏 ∩ ran ( 𝐹 ∘f + 𝐺 ) ) ≼ ran ( 𝐹 ∘f + 𝐺 ) ) )
140	138 58 139	mpisyl	⊢ ( 𝜑 → ( 𝑏 ∩ ran ( 𝐹 ∘f + 𝐺 ) ) ≼ ran ( 𝐹 ∘f + 𝐺 ) )
141		isfinite	⊢ ( ran ( 𝐹 ∘f + 𝐺 ) ∈ Fin ↔ ran ( 𝐹 ∘f + 𝐺 ) ≺ ω )
142	138 141	sylib	⊢ ( 𝜑 → ran ( 𝐹 ∘f + 𝐺 ) ≺ ω )
143		sdomdom	⊢ ( ran ( 𝐹 ∘f + 𝐺 ) ≺ ω → ran ( 𝐹 ∘f + 𝐺 ) ≼ ω )
144	142 143	syl	⊢ ( 𝜑 → ran ( 𝐹 ∘f + 𝐺 ) ≼ ω )
145		domtr	⊢ ( ( ( 𝑏 ∩ ran ( 𝐹 ∘f + 𝐺 ) ) ≼ ran ( 𝐹 ∘f + 𝐺 ) ∧ ran ( 𝐹 ∘f + 𝐺 ) ≼ ω ) → ( 𝑏 ∩ ran ( 𝐹 ∘f + 𝐺 ) ) ≼ ω )
146	140 144 145	syl2anc	⊢ ( 𝜑 → ( 𝑏 ∩ ran ( 𝐹 ∘f + 𝐺 ) ) ≼ ω )
147	146	adantr	⊢ ( ( 𝜑 ∧ 𝑏 ∈ ( sigaGen ‘ ( TopOpen ‘ 𝐾 ) ) ) → ( 𝑏 ∩ ran ( 𝐹 ∘f + 𝐺 ) ) ≼ ω )
148		nfcv	⊢ Ⅎ 𝑧 ( 𝑏 ∩ ran ( 𝐹 ∘f + 𝐺 ) )
149	148	sigaclcuni	⊢ ( ( dom 𝑀 ∈ ∪ ran sigAlgebra ∧ ∀ 𝑧 ∈ ( 𝑏 ∩ ran ( 𝐹 ∘f + 𝐺 ) ) ( ◡ ( 𝐹 ∘f + 𝐺 ) “ { 𝑧 } ) ∈ dom 𝑀 ∧ ( 𝑏 ∩ ran ( 𝐹 ∘f + 𝐺 ) ) ≼ ω ) → ∪ 𝑧 ∈ ( 𝑏 ∩ ran ( 𝐹 ∘f + 𝐺 ) ) ( ◡ ( 𝐹 ∘f + 𝐺 ) “ { 𝑧 } ) ∈ dom 𝑀 )
150	53 132 147 149	syl3anc	⊢ ( ( 𝜑 ∧ 𝑏 ∈ ( sigaGen ‘ ( TopOpen ‘ 𝐾 ) ) ) → ∪ 𝑧 ∈ ( 𝑏 ∩ ran ( 𝐹 ∘f + 𝐺 ) ) ( ◡ ( 𝐹 ∘f + 𝐺 ) “ { 𝑧 } ) ∈ dom 𝑀 )
151	57 150	eqeltrrid	⊢ ( ( 𝜑 ∧ 𝑏 ∈ ( sigaGen ‘ ( TopOpen ‘ 𝐾 ) ) ) → ( ◡ ( 𝐹 ∘f + 𝐺 ) “ ( 𝑏 ∩ ran ( 𝐹 ∘f + 𝐺 ) ) ) ∈ dom 𝑀 )
152		difpreima	⊢ ( Fun ( 𝐹 ∘f + 𝐺 ) → ( ◡ ( 𝐹 ∘f + 𝐺 ) “ ( 𝑏 ∖ ran ( 𝐹 ∘f + 𝐺 ) ) ) = ( ( ◡ ( 𝐹 ∘f + 𝐺 ) “ 𝑏 ) ∖ ( ◡ ( 𝐹 ∘f + 𝐺 ) “ ran ( 𝐹 ∘f + 𝐺 ) ) ) )
153	29 46 152	3syl	⊢ ( 𝜑 → ( ◡ ( 𝐹 ∘f + 𝐺 ) “ ( 𝑏 ∖ ran ( 𝐹 ∘f + 𝐺 ) ) ) = ( ( ◡ ( 𝐹 ∘f + 𝐺 ) “ 𝑏 ) ∖ ( ◡ ( 𝐹 ∘f + 𝐺 ) “ ran ( 𝐹 ∘f + 𝐺 ) ) ) )
154		cnvimarndm	⊢ ( ◡ ( 𝐹 ∘f + 𝐺 ) “ ran ( 𝐹 ∘f + 𝐺 ) ) = dom ( 𝐹 ∘f + 𝐺 )
155	154	difeq2i	⊢ ( ( ◡ ( 𝐹 ∘f + 𝐺 ) “ 𝑏 ) ∖ ( ◡ ( 𝐹 ∘f + 𝐺 ) “ ran ( 𝐹 ∘f + 𝐺 ) ) ) = ( ( ◡ ( 𝐹 ∘f + 𝐺 ) “ 𝑏 ) ∖ dom ( 𝐹 ∘f + 𝐺 ) )
156		cnvimass	⊢ ( ◡ ( 𝐹 ∘f + 𝐺 ) “ 𝑏 ) ⊆ dom ( 𝐹 ∘f + 𝐺 )
157		ssdif0	⊢ ( ( ◡ ( 𝐹 ∘f + 𝐺 ) “ 𝑏 ) ⊆ dom ( 𝐹 ∘f + 𝐺 ) ↔ ( ( ◡ ( 𝐹 ∘f + 𝐺 ) “ 𝑏 ) ∖ dom ( 𝐹 ∘f + 𝐺 ) ) = ∅ )
158	156 157	mpbi	⊢ ( ( ◡ ( 𝐹 ∘f + 𝐺 ) “ 𝑏 ) ∖ dom ( 𝐹 ∘f + 𝐺 ) ) = ∅
159	155 158	eqtri	⊢ ( ( ◡ ( 𝐹 ∘f + 𝐺 ) “ 𝑏 ) ∖ ( ◡ ( 𝐹 ∘f + 𝐺 ) “ ran ( 𝐹 ∘f + 𝐺 ) ) ) = ∅
160	153 159	eqtrdi	⊢ ( 𝜑 → ( ◡ ( 𝐹 ∘f + 𝐺 ) “ ( 𝑏 ∖ ran ( 𝐹 ∘f + 𝐺 ) ) ) = ∅ )
161		0elsiga	⊢ ( dom 𝑀 ∈ ∪ ran sigAlgebra → ∅ ∈ dom 𝑀 )
162	8 51 161	3syl	⊢ ( 𝜑 → ∅ ∈ dom 𝑀 )
163	160 162	eqeltrd	⊢ ( 𝜑 → ( ◡ ( 𝐹 ∘f + 𝐺 ) “ ( 𝑏 ∖ ran ( 𝐹 ∘f + 𝐺 ) ) ) ∈ dom 𝑀 )
164	163	adantr	⊢ ( ( 𝜑 ∧ 𝑏 ∈ ( sigaGen ‘ ( TopOpen ‘ 𝐾 ) ) ) → ( ◡ ( 𝐹 ∘f + 𝐺 ) “ ( 𝑏 ∖ ran ( 𝐹 ∘f + 𝐺 ) ) ) ∈ dom 𝑀 )
165		unelsiga	⊢ ( ( dom 𝑀 ∈ ∪ ran sigAlgebra ∧ ( ◡ ( 𝐹 ∘f + 𝐺 ) “ ( 𝑏 ∩ ran ( 𝐹 ∘f + 𝐺 ) ) ) ∈ dom 𝑀 ∧ ( ◡ ( 𝐹 ∘f + 𝐺 ) “ ( 𝑏 ∖ ran ( 𝐹 ∘f + 𝐺 ) ) ) ∈ dom 𝑀 ) → ( ( ◡ ( 𝐹 ∘f + 𝐺 ) “ ( 𝑏 ∩ ran ( 𝐹 ∘f + 𝐺 ) ) ) ∪ ( ◡ ( 𝐹 ∘f + 𝐺 ) “ ( 𝑏 ∖ ran ( 𝐹 ∘f + 𝐺 ) ) ) ) ∈ dom 𝑀 )
166	53 151 164 165	syl3anc	⊢ ( ( 𝜑 ∧ 𝑏 ∈ ( sigaGen ‘ ( TopOpen ‘ 𝐾 ) ) ) → ( ( ◡ ( 𝐹 ∘f + 𝐺 ) “ ( 𝑏 ∩ ran ( 𝐹 ∘f + 𝐺 ) ) ) ∪ ( ◡ ( 𝐹 ∘f + 𝐺 ) “ ( 𝑏 ∖ ran ( 𝐹 ∘f + 𝐺 ) ) ) ) ∈ dom 𝑀 )
167	50 166	eqeltrd	⊢ ( ( 𝜑 ∧ 𝑏 ∈ ( sigaGen ‘ ( TopOpen ‘ 𝐾 ) ) ) → ( ◡ ( 𝐹 ∘f + 𝐺 ) “ 𝑏 ) ∈ dom 𝑀 )
168	167	ralrimiva	⊢ ( 𝜑 → ∀ 𝑏 ∈ ( sigaGen ‘ ( TopOpen ‘ 𝐾 ) ) ( ◡ ( 𝐹 ∘f + 𝐺 ) “ 𝑏 ) ∈ dom 𝑀 )
169	52 40	ismbfm	⊢ ( 𝜑 → ( ( 𝐹 ∘f + 𝐺 ) ∈ ( dom 𝑀 MblFnM ( sigaGen ‘ ( TopOpen ‘ 𝐾 ) ) ) ↔ ( ( 𝐹 ∘f + 𝐺 ) ∈ ( ∪ ( sigaGen ‘ ( TopOpen ‘ 𝐾 ) ) ↑m ∪ dom 𝑀 ) ∧ ∀ 𝑏 ∈ ( sigaGen ‘ ( TopOpen ‘ 𝐾 ) ) ( ◡ ( 𝐹 ∘f + 𝐺 ) “ 𝑏 ) ∈ dom 𝑀 ) ) )
170	43 168 169	mpbir2and	⊢ ( 𝜑 → ( 𝐹 ∘f + 𝐺 ) ∈ ( dom 𝑀 MblFnM ( sigaGen ‘ ( TopOpen ‘ 𝐾 ) ) ) )
171	64	adantr	⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( ran ( 𝐹 ∘f + 𝐺 ) ∖ { ( 0g ‘ 𝐾 ) } ) ) → ( ◡ ( 𝐹 ∘f + 𝐺 ) “ { 𝑧 } ) = ∪ 𝑝 ∈ ( ( ◡ + “ { 𝑧 } ) ∩ ( ran 𝐹 × ran 𝐺 ) ) ( ( ◡ 𝐹 “ { ( 1st ‘ 𝑝 ) } ) ∩ ( ◡ 𝐺 “ { ( 2nd ‘ 𝑝 ) } ) ) )
172	171	fveq2d	⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( ran ( 𝐹 ∘f + 𝐺 ) ∖ { ( 0g ‘ 𝐾 ) } ) ) → ( 𝑀 ‘ ( ◡ ( 𝐹 ∘f + 𝐺 ) “ { 𝑧 } ) ) = ( 𝑀 ‘ ∪ 𝑝 ∈ ( ( ◡ + “ { 𝑧 } ) ∩ ( ran 𝐹 × ran 𝐺 ) ) ( ( ◡ 𝐹 “ { ( 1st ‘ 𝑝 ) } ) ∩ ( ◡ 𝐺 “ { ( 2nd ‘ 𝑝 ) } ) ) ) )
173		measbasedom	⊢ ( 𝑀 ∈ ∪ ran measures ↔ 𝑀 ∈ ( measures ‘ dom 𝑀 ) )
174	8 173	sylib	⊢ ( 𝜑 → 𝑀 ∈ ( measures ‘ dom 𝑀 ) )
175	174	adantr	⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( ran ( 𝐹 ∘f + 𝐺 ) ∖ { ( 0g ‘ 𝐾 ) } ) ) → 𝑀 ∈ ( measures ‘ dom 𝑀 ) )
176		eldifi	⊢ ( 𝑧 ∈ ( ran ( 𝐹 ∘f + 𝐺 ) ∖ { ( 0g ‘ 𝐾 ) } ) → 𝑧 ∈ ran ( 𝐹 ∘f + 𝐺 ) )
177	176 110	sylan2	⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( ran ( 𝐹 ∘f + 𝐺 ) ∖ { ( 0g ‘ 𝐾 ) } ) ) → ∀ 𝑝 ∈ ( ( ◡ + “ { 𝑧 } ) ∩ ( ran 𝐹 × ran 𝐺 ) ) ( ( ◡ 𝐹 “ { ( 1st ‘ 𝑝 ) } ) ∩ ( ◡ 𝐺 “ { ( 2nd ‘ 𝑝 ) } ) ) ∈ dom 𝑀 )
178	123	adantr	⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( ran ( 𝐹 ∘f + 𝐺 ) ∖ { ( 0g ‘ 𝐾 ) } ) ) → ( ( ◡ + “ { 𝑧 } ) ∩ ( ran 𝐹 × ran 𝐺 ) ) ≼ ω )
179		sneq	⊢ ( 𝑥 = ( 1st ‘ 𝑝 ) → { 𝑥 } = { ( 1st ‘ 𝑝 ) } )
180	179	imaeq2d	⊢ ( 𝑥 = ( 1st ‘ 𝑝 ) → ( ◡ 𝐹 “ { 𝑥 } ) = ( ◡ 𝐹 “ { ( 1st ‘ 𝑝 ) } ) )
181		sneq	⊢ ( 𝑦 = ( 2nd ‘ 𝑝 ) → { 𝑦 } = { ( 2nd ‘ 𝑝 ) } )
182	181	imaeq2d	⊢ ( 𝑦 = ( 2nd ‘ 𝑝 ) → ( ◡ 𝐺 “ { 𝑦 } ) = ( ◡ 𝐺 “ { ( 2nd ‘ 𝑝 ) } ) )
183	23	ffund	⊢ ( 𝜑 → Fun 𝐹 )
184		sndisj	⊢ Disj 𝑥 ∈ ran 𝐹 { 𝑥 }
185		disjpreima	⊢ ( ( Fun 𝐹 ∧ Disj 𝑥 ∈ ran 𝐹 { 𝑥 } ) → Disj 𝑥 ∈ ran 𝐹 ( ◡ 𝐹 “ { 𝑥 } ) )
186	183 184 185	sylancl	⊢ ( 𝜑 → Disj 𝑥 ∈ ran 𝐹 ( ◡ 𝐹 “ { 𝑥 } ) )
187	24	ffund	⊢ ( 𝜑 → Fun 𝐺 )
188		sndisj	⊢ Disj 𝑦 ∈ ran 𝐺 { 𝑦 }
189		disjpreima	⊢ ( ( Fun 𝐺 ∧ Disj 𝑦 ∈ ran 𝐺 { 𝑦 } ) → Disj 𝑦 ∈ ran 𝐺 ( ◡ 𝐺 “ { 𝑦 } ) )
190	187 188 189	sylancl	⊢ ( 𝜑 → Disj 𝑦 ∈ ran 𝐺 ( ◡ 𝐺 “ { 𝑦 } ) )
191	180 182 186 190	disjxpin	⊢ ( 𝜑 → Disj 𝑝 ∈ ( ran 𝐹 × ran 𝐺 ) ( ( ◡ 𝐹 “ { ( 1st ‘ 𝑝 ) } ) ∩ ( ◡ 𝐺 “ { ( 2nd ‘ 𝑝 ) } ) ) )
192		disjss1	⊢ ( ( ( ◡ + “ { 𝑧 } ) ∩ ( ran 𝐹 × ran 𝐺 ) ) ⊆ ( ran 𝐹 × ran 𝐺 ) → ( Disj 𝑝 ∈ ( ran 𝐹 × ran 𝐺 ) ( ( ◡ 𝐹 “ { ( 1st ‘ 𝑝 ) } ) ∩ ( ◡ 𝐺 “ { ( 2nd ‘ 𝑝 ) } ) ) → Disj 𝑝 ∈ ( ( ◡ + “ { 𝑧 } ) ∩ ( ran 𝐹 × ran 𝐺 ) ) ( ( ◡ 𝐹 “ { ( 1st ‘ 𝑝 ) } ) ∩ ( ◡ 𝐺 “ { ( 2nd ‘ 𝑝 ) } ) ) ) )
193	115 191 192	mpsyl	⊢ ( 𝜑 → Disj 𝑝 ∈ ( ( ◡ + “ { 𝑧 } ) ∩ ( ran 𝐹 × ran 𝐺 ) ) ( ( ◡ 𝐹 “ { ( 1st ‘ 𝑝 ) } ) ∩ ( ◡ 𝐺 “ { ( 2nd ‘ 𝑝 ) } ) ) )
194	193	adantr	⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( ran ( 𝐹 ∘f + 𝐺 ) ∖ { ( 0g ‘ 𝐾 ) } ) ) → Disj 𝑝 ∈ ( ( ◡ + “ { 𝑧 } ) ∩ ( ran 𝐹 × ran 𝐺 ) ) ( ( ◡ 𝐹 “ { ( 1st ‘ 𝑝 ) } ) ∩ ( ◡ 𝐺 “ { ( 2nd ‘ 𝑝 ) } ) ) )
195		measvuni	⊢ ( ( 𝑀 ∈ ( 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	⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( ran ( 𝐹 ∘f + 𝐺 ) ∖ { ( 0g ‘ 𝐾 ) } ) ) → ( 𝑀 ‘ ∪ 𝑝 ∈ ( ( ◡ + “ { 𝑧 } ) ∩ ( ran 𝐹 × ran 𝐺 ) ) ( ( ◡ 𝐹 “ { ( 1st ‘ 𝑝 ) } ) ∩ ( ◡ 𝐺 “ { ( 2nd ‘ 𝑝 ) } ) ) ) = Σ* 𝑝 ∈ ( ( ◡ + “ { 𝑧 } ) ∩ ( ran 𝐹 × ran 𝐺 ) ) ( 𝑀 ‘ ( ( ◡ 𝐹 “ { ( 1st ‘ 𝑝 ) } ) ∩ ( ◡ 𝐺 “ { ( 2nd ‘ 𝑝 ) } ) ) ) )
197		ssfi	⊢ ( ( ( ran 𝐹 × ran 𝐺 ) ∈ Fin ∧ ( ( ◡ + “ { 𝑧 } ) ∩ ( ran 𝐹 × ran 𝐺 ) ) ⊆ ( ran 𝐹 × ran 𝐺 ) ) → ( ( ◡ + “ { 𝑧 } ) ∩ ( ran 𝐹 × ran 𝐺 ) ) ∈ Fin )
198	114 115 197	sylancl	⊢ ( 𝜑 → ( ( ◡ + “ { 𝑧 } ) ∩ ( ran 𝐹 × ran 𝐺 ) ) ∈ Fin )
199	198	adantr	⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( ran ( 𝐹 ∘f + 𝐺 ) ∖ { ( 0g ‘ 𝐾 ) } ) ) → ( ( ◡ + “ { 𝑧 } ) ∩ ( ran 𝐹 × ran 𝐺 ) ) ∈ Fin )
200		simpll	⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ( ran ( 𝐹 ∘f + 𝐺 ) ∖ { ( 0g ‘ 𝐾 ) } ) ) ∧ 𝑝 ∈ ( ( ◡ + “ { 𝑧 } ) ∩ ( ran 𝐹 × ran 𝐺 ) ) ) → 𝜑 )
201		simpr	⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ( ran ( 𝐹 ∘f + 𝐺 ) ∖ { ( 0g ‘ 𝐾 ) } ) ) ∧ 𝑝 ∈ ( ( ◡ + “ { 𝑧 } ) ∩ ( ran 𝐹 × ran 𝐺 ) ) ) → 𝑝 ∈ ( ( ◡ + “ { 𝑧 } ) ∩ ( ran 𝐹 × ran 𝐺 ) ) )
202	115 201	sseldi	⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ( ran ( 𝐹 ∘f + 𝐺 ) ∖ { ( 0g ‘ 𝐾 ) } ) ) ∧ 𝑝 ∈ ( ( ◡ + “ { 𝑧 } ) ∩ ( ran 𝐹 × ran 𝐺 ) ) ) → 𝑝 ∈ ( ran 𝐹 × ran 𝐺 ) )
203		xp1st	⊢ ( 𝑝 ∈ ( ran 𝐹 × ran 𝐺 ) → ( 1st ‘ 𝑝 ) ∈ ran 𝐹 )
204	202 203	syl	⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ( ran ( 𝐹 ∘f + 𝐺 ) ∖ { ( 0g ‘ 𝐾 ) } ) ) ∧ 𝑝 ∈ ( ( ◡ + “ { 𝑧 } ) ∩ ( ran 𝐹 × ran 𝐺 ) ) ) → ( 1st ‘ 𝑝 ) ∈ ran 𝐹 )
205		xp2nd	⊢ ( 𝑝 ∈ ( ran 𝐹 × ran 𝐺 ) → ( 2nd ‘ 𝑝 ) ∈ ran 𝐺 )
206	202 205	syl	⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ( ran ( 𝐹 ∘f + 𝐺 ) ∖ { ( 0g ‘ 𝐾 ) } ) ) ∧ 𝑝 ∈ ( ( ◡ + “ { 𝑧 } ) ∩ ( ran 𝐹 × ran 𝐺 ) ) ) → ( 2nd ‘ 𝑝 ) ∈ ran 𝐺 )
207		oveq12	⊢ ( ( 𝑥 = 0 ∧ 𝑦 = 0 ) → ( 𝑥 + 𝑦 ) = ( 0 + 0 ) )
208	207 16	sylan9eqr	⊢ ( ( 𝜑 ∧ ( 𝑥 = 0 ∧ 𝑦 = 0 ) ) → ( 𝑥 + 𝑦 ) = ( 0g ‘ 𝐾 ) )
209	208	ex	⊢ ( 𝜑 → ( ( 𝑥 = 0 ∧ 𝑦 = 0 ) → ( 𝑥 + 𝑦 ) = ( 0g ‘ 𝐾 ) ) )
210	209	necon3ad	⊢ ( 𝜑 → ( ( 𝑥 + 𝑦 ) ≠ ( 0g ‘ 𝐾 ) → ¬ ( 𝑥 = 0 ∧ 𝑦 = 0 ) ) )
211		neorian	⊢ ( ( 𝑥 ≠ 0 ∨ 𝑦 ≠ 0 ) ↔ ¬ ( 𝑥 = 0 ∧ 𝑦 = 0 ) )
212	210 211	syl6ibr	⊢ ( 𝜑 → ( ( 𝑥 + 𝑦 ) ≠ ( 0g ‘ 𝐾 ) → ( 𝑥 ≠ 0 ∨ 𝑦 ≠ 0 ) ) )
213	212	adantr	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( ( 𝑥 + 𝑦 ) ≠ ( 0g ‘ 𝐾 ) → ( 𝑥 ≠ 0 ∨ 𝑦 ≠ 0 ) ) )
214	213	ralrimivva	⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( ( 𝑥 + 𝑦 ) ≠ ( 0g ‘ 𝐾 ) → ( 𝑥 ≠ 0 ∨ 𝑦 ≠ 0 ) ) )
215	200 214	syl	⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ( ran ( 𝐹 ∘f + 𝐺 ) ∖ { ( 0g ‘ 𝐾 ) } ) ) ∧ 𝑝 ∈ ( ( ◡ + “ { 𝑧 } ) ∩ ( ran 𝐹 × ran 𝐺 ) ) ) → ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( ( 𝑥 + 𝑦 ) ≠ ( 0g ‘ 𝐾 ) → ( 𝑥 ≠ 0 ∨ 𝑦 ≠ 0 ) ) )
216	69	a1i	⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( ran ( 𝐹 ∘f + 𝐺 ) ∖ { ( 0g ‘ 𝐾 ) } ) ) → ( ( ◡ + “ { 𝑧 } ) ∩ ( ran 𝐹 × ran 𝐺 ) ) ⊆ ( ◡ + “ { 𝑧 } ) )
217	216	sselda	⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ( ran ( 𝐹 ∘f + 𝐺 ) ∖ { ( 0g ‘ 𝐾 ) } ) ) ∧ 𝑝 ∈ ( ( ◡ + “ { 𝑧 } ) ∩ ( ran 𝐹 × ran 𝐺 ) ) ) → 𝑝 ∈ ( ◡ + “ { 𝑧 } ) )
218		fniniseg	⊢ ( + Fn ( 𝐵 × 𝐵 ) → ( 𝑝 ∈ ( ◡ + “ { 𝑧 } ) ↔ ( 𝑝 ∈ ( 𝐵 × 𝐵 ) ∧ ( + ‘ 𝑝 ) = 𝑧 ) ) )
219	200 63 218	3syl	⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ( ran ( 𝐹 ∘f + 𝐺 ) ∖ { ( 0g ‘ 𝐾 ) } ) ) ∧ 𝑝 ∈ ( ( ◡ + “ { 𝑧 } ) ∩ ( ran 𝐹 × ran 𝐺 ) ) ) → ( 𝑝 ∈ ( ◡ + “ { 𝑧 } ) ↔ ( 𝑝 ∈ ( 𝐵 × 𝐵 ) ∧ ( + ‘ 𝑝 ) = 𝑧 ) ) )
220	217 219	mpbid	⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ( ran ( 𝐹 ∘f + 𝐺 ) ∖ { ( 0g ‘ 𝐾 ) } ) ) ∧ 𝑝 ∈ ( ( ◡ + “ { 𝑧 } ) ∩ ( ran 𝐹 × ran 𝐺 ) ) ) → ( 𝑝 ∈ ( 𝐵 × 𝐵 ) ∧ ( + ‘ 𝑝 ) = 𝑧 ) )
221		simpr	⊢ ( ( 𝑝 ∈ ( 𝐵 × 𝐵 ) ∧ ( + ‘ 𝑝 ) = 𝑧 ) → ( + ‘ 𝑝 ) = 𝑧 )
222		1st2nd2	⊢ ( 𝑝 ∈ ( 𝐵 × 𝐵 ) → 𝑝 = ⟨ ( 1st ‘ 𝑝 ) , ( 2nd ‘ 𝑝 ) ⟩ )
223	222	fveq2d	⊢ ( 𝑝 ∈ ( 𝐵 × 𝐵 ) → ( + ‘ 𝑝 ) = ( + ‘ ⟨ ( 1st ‘ 𝑝 ) , ( 2nd ‘ 𝑝 ) ⟩ ) )
224		df-ov	⊢ ( ( 1st ‘ 𝑝 ) + ( 2nd ‘ 𝑝 ) ) = ( + ‘ ⟨ ( 1st ‘ 𝑝 ) , ( 2nd ‘ 𝑝 ) ⟩ )
225	223 224	eqtr4di	⊢ ( 𝑝 ∈ ( 𝐵 × 𝐵 ) → ( + ‘ 𝑝 ) = ( ( 1st ‘ 𝑝 ) + ( 2nd ‘ 𝑝 ) ) )
226	225	adantr	⊢ ( ( 𝑝 ∈ ( 𝐵 × 𝐵 ) ∧ ( + ‘ 𝑝 ) = 𝑧 ) → ( + ‘ 𝑝 ) = ( ( 1st ‘ 𝑝 ) + ( 2nd ‘ 𝑝 ) ) )
227	221 226	eqtr3d	⊢ ( ( 𝑝 ∈ ( 𝐵 × 𝐵 ) ∧ ( + ‘ 𝑝 ) = 𝑧 ) → 𝑧 = ( ( 1st ‘ 𝑝 ) + ( 2nd ‘ 𝑝 ) ) )
228	220 227	syl	⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ( ran ( 𝐹 ∘f + 𝐺 ) ∖ { ( 0g ‘ 𝐾 ) } ) ) ∧ 𝑝 ∈ ( ( ◡ + “ { 𝑧 } ) ∩ ( ran 𝐹 × ran 𝐺 ) ) ) → 𝑧 = ( ( 1st ‘ 𝑝 ) + ( 2nd ‘ 𝑝 ) ) )
229		simplr	⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ( ran ( 𝐹 ∘f + 𝐺 ) ∖ { ( 0g ‘ 𝐾 ) } ) ) ∧ 𝑝 ∈ ( ( ◡ + “ { 𝑧 } ) ∩ ( ran 𝐹 × ran 𝐺 ) ) ) → 𝑧 ∈ ( ran ( 𝐹 ∘f + 𝐺 ) ∖ { ( 0g ‘ 𝐾 ) } ) )
230	229	eldifbd	⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ( ran ( 𝐹 ∘f + 𝐺 ) ∖ { ( 0g ‘ 𝐾 ) } ) ) ∧ 𝑝 ∈ ( ( ◡ + “ { 𝑧 } ) ∩ ( ran 𝐹 × ran 𝐺 ) ) ) → ¬ 𝑧 ∈ { ( 0g ‘ 𝐾 ) } )
231		velsn	⊢ ( 𝑧 ∈ { ( 0g ‘ 𝐾 ) } ↔ 𝑧 = ( 0g ‘ 𝐾 ) )
232	231	necon3bbii	⊢ ( ¬ 𝑧 ∈ { ( 0g ‘ 𝐾 ) } ↔ 𝑧 ≠ ( 0g ‘ 𝐾 ) )
233	230 232	sylib	⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ( ran ( 𝐹 ∘f + 𝐺 ) ∖ { ( 0g ‘ 𝐾 ) } ) ) ∧ 𝑝 ∈ ( ( ◡ + “ { 𝑧 } ) ∩ ( ran 𝐹 × ran 𝐺 ) ) ) → 𝑧 ≠ ( 0g ‘ 𝐾 ) )
234	228 233	eqnetrrd	⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ( ran ( 𝐹 ∘f + 𝐺 ) ∖ { ( 0g ‘ 𝐾 ) } ) ) ∧ 𝑝 ∈ ( ( ◡ + “ { 𝑧 } ) ∩ ( ran 𝐹 × ran 𝐺 ) ) ) → ( ( 1st ‘ 𝑝 ) + ( 2nd ‘ 𝑝 ) ) ≠ ( 0g ‘ 𝐾 ) )
235	176 74	sylanl2	⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ( ran ( 𝐹 ∘f + 𝐺 ) ∖ { ( 0g ‘ 𝐾 ) } ) ) ∧ 𝑝 ∈ ( ( ◡ + “ { 𝑧 } ) ∩ ( ran 𝐹 × ran 𝐺 ) ) ) → 𝑝 ∈ ( 𝐵 × 𝐵 ) )
236	235 86	syl	⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ( ran ( 𝐹 ∘f + 𝐺 ) ∖ { ( 0g ‘ 𝐾 ) } ) ) ∧ 𝑝 ∈ ( ( ◡ + “ { 𝑧 } ) ∩ ( ran 𝐹 × ran 𝐺 ) ) ) → ( 1st ‘ 𝑝 ) ∈ 𝐵 )
237	235 99	syl	⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ( ran ( 𝐹 ∘f + 𝐺 ) ∖ { ( 0g ‘ 𝐾 ) } ) ) ∧ 𝑝 ∈ ( ( ◡ + “ { 𝑧 } ) ∩ ( ran 𝐹 × ran 𝐺 ) ) ) → ( 2nd ‘ 𝑝 ) ∈ 𝐵 )
238		oveq1	⊢ ( 𝑥 = ( 1st ‘ 𝑝 ) → ( 𝑥 + 𝑦 ) = ( ( 1st ‘ 𝑝 ) + 𝑦 ) )
239	238	neeq1d	⊢ ( 𝑥 = ( 1st ‘ 𝑝 ) → ( ( 𝑥 + 𝑦 ) ≠ ( 0g ‘ 𝐾 ) ↔ ( ( 1st ‘ 𝑝 ) + 𝑦 ) ≠ ( 0g ‘ 𝐾 ) ) )
240		neeq1	⊢ ( 𝑥 = ( 1st ‘ 𝑝 ) → ( 𝑥 ≠ 0 ↔ ( 1st ‘ 𝑝 ) ≠ 0 ) )
241	240	orbi1d	⊢ ( 𝑥 = ( 1st ‘ 𝑝 ) → ( ( 𝑥 ≠ 0 ∨ 𝑦 ≠ 0 ) ↔ ( ( 1st ‘ 𝑝 ) ≠ 0 ∨ 𝑦 ≠ 0 ) ) )
242	239 241	imbi12d	⊢ ( 𝑥 = ( 1st ‘ 𝑝 ) → ( ( ( 𝑥 + 𝑦 ) ≠ ( 0g ‘ 𝐾 ) → ( 𝑥 ≠ 0 ∨ 𝑦 ≠ 0 ) ) ↔ ( ( ( 1st ‘ 𝑝 ) + 𝑦 ) ≠ ( 0g ‘ 𝐾 ) → ( ( 1st ‘ 𝑝 ) ≠ 0 ∨ 𝑦 ≠ 0 ) ) ) )
243		oveq2	⊢ ( 𝑦 = ( 2nd ‘ 𝑝 ) → ( ( 1st ‘ 𝑝 ) + 𝑦 ) = ( ( 1st ‘ 𝑝 ) + ( 2nd ‘ 𝑝 ) ) )
244	243	neeq1d	⊢ ( 𝑦 = ( 2nd ‘ 𝑝 ) → ( ( ( 1st ‘ 𝑝 ) + 𝑦 ) ≠ ( 0g ‘ 𝐾 ) ↔ ( ( 1st ‘ 𝑝 ) + ( 2nd ‘ 𝑝 ) ) ≠ ( 0g ‘ 𝐾 ) ) )
245		neeq1	⊢ ( 𝑦 = ( 2nd ‘ 𝑝 ) → ( 𝑦 ≠ 0 ↔ ( 2nd ‘ 𝑝 ) ≠ 0 ) )
246	245	orbi2d	⊢ ( 𝑦 = ( 2nd ‘ 𝑝 ) → ( ( ( 1st ‘ 𝑝 ) ≠ 0 ∨ 𝑦 ≠ 0 ) ↔ ( ( 1st ‘ 𝑝 ) ≠ 0 ∨ ( 2nd ‘ 𝑝 ) ≠ 0 ) ) )
247	244 246	imbi12d	⊢ ( 𝑦 = ( 2nd ‘ 𝑝 ) → ( ( ( ( 1st ‘ 𝑝 ) + 𝑦 ) ≠ ( 0g ‘ 𝐾 ) → ( ( 1st ‘ 𝑝 ) ≠ 0 ∨ 𝑦 ≠ 0 ) ) ↔ ( ( ( 1st ‘ 𝑝 ) + ( 2nd ‘ 𝑝 ) ) ≠ ( 0g ‘ 𝐾 ) → ( ( 1st ‘ 𝑝 ) ≠ 0 ∨ ( 2nd ‘ 𝑝 ) ≠ 0 ) ) ) )
248	242 247	rspc2v	⊢ ( ( ( 1st ‘ 𝑝 ) ∈ 𝐵 ∧ ( 2nd ‘ 𝑝 ) ∈ 𝐵 ) → ( ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( ( 𝑥 + 𝑦 ) ≠ ( 0g ‘ 𝐾 ) → ( 𝑥 ≠ 0 ∨ 𝑦 ≠ 0 ) ) → ( ( ( 1st ‘ 𝑝 ) + ( 2nd ‘ 𝑝 ) ) ≠ ( 0g ‘ 𝐾 ) → ( ( 1st ‘ 𝑝 ) ≠ 0 ∨ ( 2nd ‘ 𝑝 ) ≠ 0 ) ) ) )
249	236 237 248	syl2anc	⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ( ran ( 𝐹 ∘f + 𝐺 ) ∖ { ( 0g ‘ 𝐾 ) } ) ) ∧ 𝑝 ∈ ( ( ◡ + “ { 𝑧 } ) ∩ ( ran 𝐹 × ran 𝐺 ) ) ) → ( ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( ( 𝑥 + 𝑦 ) ≠ ( 0g ‘ 𝐾 ) → ( 𝑥 ≠ 0 ∨ 𝑦 ≠ 0 ) ) → ( ( ( 1st ‘ 𝑝 ) + ( 2nd ‘ 𝑝 ) ) ≠ ( 0g ‘ 𝐾 ) → ( ( 1st ‘ 𝑝 ) ≠ 0 ∨ ( 2nd ‘ 𝑝 ) ≠ 0 ) ) ) )
250	215 234 249	mp2d	⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ( ran ( 𝐹 ∘f + 𝐺 ) ∖ { ( 0g ‘ 𝐾 ) } ) ) ∧ 𝑝 ∈ ( ( ◡ + “ { 𝑧 } ) ∩ ( ran 𝐹 × ran 𝐺 ) ) ) → ( ( 1st ‘ 𝑝 ) ≠ 0 ∨ ( 2nd ‘ 𝑝 ) ≠ 0 ) )
251	1 2 3 4 5 6 7 8 9 13 11 15	sibfinima	⊢ ( ( ( 𝜑 ∧ ( 1st ‘ 𝑝 ) ∈ ran 𝐹 ∧ ( 2nd ‘ 𝑝 ) ∈ ran 𝐺 ) ∧ ( ( 1st ‘ 𝑝 ) ≠ 0 ∨ ( 2nd ‘ 𝑝 ) ≠ 0 ) ) → ( 𝑀 ‘ ( ( ◡ 𝐹 “ { ( 1st ‘ 𝑝 ) } ) ∩ ( ◡ 𝐺 “ { ( 2nd ‘ 𝑝 ) } ) ) ) ∈ ( 0 [,) +∞ ) )
252	200 204 206 250 251	syl31anc	⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ( ran ( 𝐹 ∘f + 𝐺 ) ∖ { ( 0g ‘ 𝐾 ) } ) ) ∧ 𝑝 ∈ ( ( ◡ + “ { 𝑧 } ) ∩ ( ran 𝐹 × ran 𝐺 ) ) ) → ( 𝑀 ‘ ( ( ◡ 𝐹 “ { ( 1st ‘ 𝑝 ) } ) ∩ ( ◡ 𝐺 “ { ( 2nd ‘ 𝑝 ) } ) ) ) ∈ ( 0 [,) +∞ ) )
253	199 252	esumpfinval	⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( ran ( 𝐹 ∘f + 𝐺 ) ∖ { ( 0g ‘ 𝐾 ) } ) ) → Σ* 𝑝 ∈ ( ( ◡ + “ { 𝑧 } ) ∩ ( ran 𝐹 × ran 𝐺 ) ) ( 𝑀 ‘ ( ( ◡ 𝐹 “ { ( 1st ‘ 𝑝 ) } ) ∩ ( ◡ 𝐺 “ { ( 2nd ‘ 𝑝 ) } ) ) ) = Σ 𝑝 ∈ ( ( ◡ + “ { 𝑧 } ) ∩ ( ran 𝐹 × ran 𝐺 ) ) ( 𝑀 ‘ ( ( ◡ 𝐹 “ { ( 1st ‘ 𝑝 ) } ) ∩ ( ◡ 𝐺 “ { ( 2nd ‘ 𝑝 ) } ) ) ) )
254	172 196 253	3eqtrd	⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( ran ( 𝐹 ∘f + 𝐺 ) ∖ { ( 0g ‘ 𝐾 ) } ) ) → ( 𝑀 ‘ ( ◡ ( 𝐹 ∘f + 𝐺 ) “ { 𝑧 } ) ) = Σ 𝑝 ∈ ( ( ◡ + “ { 𝑧 } ) ∩ ( ran 𝐹 × ran 𝐺 ) ) ( 𝑀 ‘ ( ( ◡ 𝐹 “ { ( 1st ‘ 𝑝 ) } ) ∩ ( ◡ 𝐺 “ { ( 2nd ‘ 𝑝 ) } ) ) ) )
255		rge0ssre	⊢ ( 0 [,) +∞ ) ⊆ ℝ
256	255 252	sseldi	⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ( ran ( 𝐹 ∘f + 𝐺 ) ∖ { ( 0g ‘ 𝐾 ) } ) ) ∧ 𝑝 ∈ ( ( ◡ + “ { 𝑧 } ) ∩ ( ran 𝐹 × ran 𝐺 ) ) ) → ( 𝑀 ‘ ( ( ◡ 𝐹 “ { ( 1st ‘ 𝑝 ) } ) ∩ ( ◡ 𝐺 “ { ( 2nd ‘ 𝑝 ) } ) ) ) ∈ ℝ )
257	199 256	fsumrecl	⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( ran ( 𝐹 ∘f + 𝐺 ) ∖ { ( 0g ‘ 𝐾 ) } ) ) → Σ 𝑝 ∈ ( ( ◡ + “ { 𝑧 } ) ∩ ( ran 𝐹 × ran 𝐺 ) ) ( 𝑀 ‘ ( ( ◡ 𝐹 “ { ( 1st ‘ 𝑝 ) } ) ∩ ( ◡ 𝐺 “ { ( 2nd ‘ 𝑝 ) } ) ) ) ∈ ℝ )
258	254 257	eqeltrd	⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( ran ( 𝐹 ∘f + 𝐺 ) ∖ { ( 0g ‘ 𝐾 ) } ) ) → ( 𝑀 ‘ ( ◡ ( 𝐹 ∘f + 𝐺 ) “ { 𝑧 } ) ) ∈ ℝ )
259	175	adantr	⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ( ran ( 𝐹 ∘f + 𝐺 ) ∖ { ( 0g ‘ 𝐾 ) } ) ) ∧ 𝑝 ∈ ( ( ◡ + “ { 𝑧 } ) ∩ ( ran 𝐹 × ran 𝐺 ) ) ) → 𝑀 ∈ ( measures ‘ dom 𝑀 ) )
260	176 109	sylanl2	⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ( ran ( 𝐹 ∘f + 𝐺 ) ∖ { ( 0g ‘ 𝐾 ) } ) ) ∧ 𝑝 ∈ ( ( ◡ + “ { 𝑧 } ) ∩ ( ran 𝐹 × ran 𝐺 ) ) ) → ( ( ◡ 𝐹 “ { ( 1st ‘ 𝑝 ) } ) ∩ ( ◡ 𝐺 “ { ( 2nd ‘ 𝑝 ) } ) ) ∈ dom 𝑀 )
261		measge0	⊢ ( ( 𝑀 ∈ ( measures ‘ dom 𝑀 ) ∧ ( ( ◡ 𝐹 “ { ( 1st ‘ 𝑝 ) } ) ∩ ( ◡ 𝐺 “ { ( 2nd ‘ 𝑝 ) } ) ) ∈ dom 𝑀 ) → 0 ≤ ( 𝑀 ‘ ( ( ◡ 𝐹 “ { ( 1st ‘ 𝑝 ) } ) ∩ ( ◡ 𝐺 “ { ( 2nd ‘ 𝑝 ) } ) ) ) )
262	259 260 261	syl2anc	⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ( ran ( 𝐹 ∘f + 𝐺 ) ∖ { ( 0g ‘ 𝐾 ) } ) ) ∧ 𝑝 ∈ ( ( ◡ + “ { 𝑧 } ) ∩ ( ran 𝐹 × ran 𝐺 ) ) ) → 0 ≤ ( 𝑀 ‘ ( ( ◡ 𝐹 “ { ( 1st ‘ 𝑝 ) } ) ∩ ( ◡ 𝐺 “ { ( 2nd ‘ 𝑝 ) } ) ) ) )
263	199 256 262	fsumge0	⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( ran ( 𝐹 ∘f + 𝐺 ) ∖ { ( 0g ‘ 𝐾 ) } ) ) → 0 ≤ Σ 𝑝 ∈ ( ( ◡ + “ { 𝑧 } ) ∩ ( ran 𝐹 × ran 𝐺 ) ) ( 𝑀 ‘ ( ( ◡ 𝐹 “ { ( 1st ‘ 𝑝 ) } ) ∩ ( ◡ 𝐺 “ { ( 2nd ‘ 𝑝 ) } ) ) ) )
264	263 254	breqtrrd	⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( ran ( 𝐹 ∘f + 𝐺 ) ∖ { ( 0g ‘ 𝐾 ) } ) ) → 0 ≤ ( 𝑀 ‘ ( ◡ ( 𝐹 ∘f + 𝐺 ) “ { 𝑧 } ) ) )
265		elrege0	⊢ ( ( 𝑀 ‘ ( ◡ ( 𝐹 ∘f + 𝐺 ) “ { 𝑧 } ) ) ∈ ( 0 [,) +∞ ) ↔ ( ( 𝑀 ‘ ( ◡ ( 𝐹 ∘f + 𝐺 ) “ { 𝑧 } ) ) ∈ ℝ ∧ 0 ≤ ( 𝑀 ‘ ( ◡ ( 𝐹 ∘f + 𝐺 ) “ { 𝑧 } ) ) ) )
266	258 264 265	sylanbrc	⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( ran ( 𝐹 ∘f + 𝐺 ) ∖ { ( 0g ‘ 𝐾 ) } ) ) → ( 𝑀 ‘ ( ◡ ( 𝐹 ∘f + 𝐺 ) “ { 𝑧 } ) ) ∈ ( 0 [,) +∞ ) )
267	266	ralrimiva	⊢ ( 𝜑 → ∀ 𝑧 ∈ ( ran ( 𝐹 ∘f + 𝐺 ) ∖ { ( 0g ‘ 𝐾 ) } ) ( 𝑀 ‘ ( ◡ ( 𝐹 ∘f + 𝐺 ) “ { 𝑧 } ) ) ∈ ( 0 [,) +∞ ) )
268		eqid	⊢ ( sigaGen ‘ ( TopOpen ‘ 𝐾 ) ) = ( sigaGen ‘ ( TopOpen ‘ 𝐾 ) )
269		eqid	⊢ ( 0g ‘ 𝐾 ) = ( 0g ‘ 𝐾 )
270		eqid	⊢ ( ·𝑠 ‘ 𝐾 ) = ( ·𝑠 ‘ 𝐾 )
271		eqid	⊢ ( ℝHom ‘ ( Scalar ‘ 𝐾 ) ) = ( ℝHom ‘ ( Scalar ‘ 𝐾 ) )
272	10 30 268 269 270 271 14 8	issibf	⊢ ( 𝜑 → ( ( 𝐹 ∘f + 𝐺 ) ∈ dom ( 𝐾 sitg 𝑀 ) ↔ ( ( 𝐹 ∘f + 𝐺 ) ∈ ( dom 𝑀 MblFnM ( sigaGen ‘ ( TopOpen ‘ 𝐾 ) ) ) ∧ ran ( 𝐹 ∘f + 𝐺 ) ∈ Fin ∧ ∀ 𝑧 ∈ ( ran ( 𝐹 ∘f + 𝐺 ) ∖ { ( 0g ‘ 𝐾 ) } ) ( 𝑀 ‘ ( ◡ ( 𝐹 ∘f + 𝐺 ) “ { 𝑧 } ) ) ∈ ( 0 [,) +∞ ) ) ) )
273	170 138 267 272	mpbir3and	⊢ ( 𝜑 → ( 𝐹 ∘f + 𝐺 ) ∈ dom ( 𝐾 sitg 𝑀 ) )