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	$⊢ B = {Base}_{W}$
	sitgval.j	$⊢ J = TopOpen (W)$
	sitgval.s	$⊢ S = 𝛔 (J)$
	sitgval.0	$⊢ \underset{˙}{0} = 0_{W}$
	sitgval.x	$⊢ \underset{˙}{\cdot} = \cdot_{W}$
	sitgval.h	$⊢ H = ℝHom (Scalar (W))$
	sitgval.1	$⊢ φ \to W \in V$
	sitgval.2	$⊢ φ \to M \in ⋃ ran measures$
	sibfmbl.1	$⊢ φ \to F \in ℑ_{M}^{W}$
	sibfof.c	$⊢ C = {Base}_{K}$
	sibfof.0	$⊢ φ \to W \in TopSp$
	sibfof.1	$⊢ φ \to \underset{˙}{+} : B \times B ⟶ C$
	sibfof.2	$⊢ φ \to G \in ℑ_{M}^{W}$
	sibfof.3	$⊢ φ \to K \in TopSp$
	sibfof.4	$⊢ φ \to J \in Fre$
	sibfof.5	$⊢ φ \to \underset{˙}{0} \underset{˙}{+} \underset{˙}{0} = 0_{K}$
Assertion	sibfof	$⊢ φ \to F {\underset{˙}{+}}_{f} G \in ℑ_{M}^{K}$

Proof

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

Metamath Proof Explorer

Theorem sibfof

Proof