sitgaddlemb

Description: Lemma for * sitgadd . (Contributed by Thierry Arnoux, 10-Mar-2019)

	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$
	sitgadd.1	$⊢ φ \to W \in TopSp$
	sitgadd.2	$⊢ φ \to W ↾_{𝑣} H [[0, +∞)] \in SLMod$
	sitgadd.3	$⊢ φ \to J \in Fre$
	sitgadd.4	$⊢ φ \to F \in ℑ_{M}^{W}$
	sitgadd.5	$⊢ φ \to G \in ℑ_{M}^{W}$
	sitgadd.6	$⊢ φ \to Scalar (W) \in ℝExt$
	sitgadd.7	$⊢ \underset{˙}{+} = +_{W}$
Assertion	sitgaddlemb	$⊢ (φ \land p \in ((ran F \times ran G) ∖ \{⟨\underset{˙}{0}, \underset{˙}{0}⟩\})) \to H (M (F^{-1} [\{1^{st} (p)\}] \cap G^{-1} [\{2^{nd} (p)\}])) \underset{˙}{\cdot} 2^{nd} (p) \in B$

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		sitgadd.1	$⊢ φ \to W \in TopSp$
10		sitgadd.2	$⊢ φ \to W ↾_{𝑣} H [[0, +∞)] \in SLMod$
11		sitgadd.3	$⊢ φ \to J \in Fre$
12		sitgadd.4	$⊢ φ \to F \in ℑ_{M}^{W}$
13		sitgadd.5	$⊢ φ \to G \in ℑ_{M}^{W}$
14		sitgadd.6	$⊢ φ \to Scalar (W) \in ℝExt$
15		sitgadd.7	$⊢ \underset{˙}{+} = +_{W}$
16	10	adantr	$⊢ (φ \land p \in ((ran F \times ran G) ∖ \{⟨\underset{˙}{0}, \underset{˙}{0}⟩\})) \to W ↾_{𝑣} H [[0, +∞)] \in SLMod$
17		simpl	$⊢ (φ \land p \in ((ran F \times ran G) ∖ \{⟨\underset{˙}{0}, \underset{˙}{0}⟩\})) \to φ$
18		eqid	$⊢ {Base}_{Scalar (W)} = {Base}_{Scalar (W)}$
19	18	rrhfe	$⊢ Scalar (W) \in ℝExt \to ℝHom (Scalar (W)) : ℝ ⟶ {Base}_{Scalar (W)}$
20	14 19	syl	$⊢ φ \to ℝHom (Scalar (W)) : ℝ ⟶ {Base}_{Scalar (W)}$
21	6	feq1i	$⊢ H : ℝ ⟶ {Base}_{Scalar (W)} \leftrightarrow ℝHom (Scalar (W)) : ℝ ⟶ {Base}_{Scalar (W)}$
22	20 21	sylibr	$⊢ φ \to H : ℝ ⟶ {Base}_{Scalar (W)}$
23	22	ffnd	$⊢ φ \to H Fn ℝ$
24	17 23	syl	$⊢ (φ \land p \in ((ran F \times ran G) ∖ \{⟨\underset{˙}{0}, \underset{˙}{0}⟩\})) \to H Fn ℝ$
25		rge0ssre	$⊢ [0, +∞) \subseteq ℝ$
26	25	a1i	$⊢ (φ \land p \in ((ran F \times ran G) ∖ \{⟨\underset{˙}{0}, \underset{˙}{0}⟩\})) \to [0, +∞) \subseteq ℝ$
27		simpr	$⊢ (φ \land p \in ((ran F \times ran G) ∖ \{⟨\underset{˙}{0}, \underset{˙}{0}⟩\})) \to p \in ((ran F \times ran G) ∖ \{⟨\underset{˙}{0}, \underset{˙}{0}⟩\})$
28	27	eldifad	$⊢ (φ \land p \in ((ran F \times ran G) ∖ \{⟨\underset{˙}{0}, \underset{˙}{0}⟩\})) \to p \in (ran F \times ran G)$
29		xp1st	$⊢ p \in (ran F \times ran G) \to 1^{st} (p) \in ran F$
30	28 29	syl	$⊢ (φ \land p \in ((ran F \times ran G) ∖ \{⟨\underset{˙}{0}, \underset{˙}{0}⟩\})) \to 1^{st} (p) \in ran F$
31		xp2nd	$⊢ p \in (ran F \times ran G) \to 2^{nd} (p) \in ran G$
32	28 31	syl	$⊢ (φ \land p \in ((ran F \times ran G) ∖ \{⟨\underset{˙}{0}, \underset{˙}{0}⟩\})) \to 2^{nd} (p) \in ran G$
33	27	eldifbd	$⊢ (φ \land p \in ((ran F \times ran G) ∖ \{⟨\underset{˙}{0}, \underset{˙}{0}⟩\})) \to \neg p \in \{⟨\underset{˙}{0}, \underset{˙}{0}⟩\}$
34		velsn	$⊢ p \in \{⟨\underset{˙}{0}, \underset{˙}{0}⟩\} \leftrightarrow p = ⟨\underset{˙}{0}, \underset{˙}{0}⟩$
35	34	notbii	$⊢ \neg p \in \{⟨\underset{˙}{0}, \underset{˙}{0}⟩\} \leftrightarrow \neg p = ⟨\underset{˙}{0}, \underset{˙}{0}⟩$
36	33 35	sylib	$⊢ (φ \land p \in ((ran F \times ran G) ∖ \{⟨\underset{˙}{0}, \underset{˙}{0}⟩\})) \to \neg p = ⟨\underset{˙}{0}, \underset{˙}{0}⟩$
37		eqopi	$⊢ (p \in (ran F \times ran G) \land (1^{st} (p) = \underset{˙}{0} \land 2^{nd} (p) = \underset{˙}{0})) \to p = ⟨\underset{˙}{0}, \underset{˙}{0}⟩$
38	37	ex	$⊢ p \in (ran F \times ran G) \to ((1^{st} (p) = \underset{˙}{0} \land 2^{nd} (p) = \underset{˙}{0}) \to p = ⟨\underset{˙}{0}, \underset{˙}{0}⟩)$
39	38	con3d	$⊢ p \in (ran F \times ran G) \to (\neg p = ⟨\underset{˙}{0}, \underset{˙}{0}⟩ \to \neg (1^{st} (p) = \underset{˙}{0} \land 2^{nd} (p) = \underset{˙}{0}))$
40	39	imp	$⊢ (p \in (ran F \times ran G) \land \neg p = ⟨\underset{˙}{0}, \underset{˙}{0}⟩) \to \neg (1^{st} (p) = \underset{˙}{0} \land 2^{nd} (p) = \underset{˙}{0})$
41	28 36 40	syl2anc	$⊢ (φ \land p \in ((ran F \times ran G) ∖ \{⟨\underset{˙}{0}, \underset{˙}{0}⟩\})) \to \neg (1^{st} (p) = \underset{˙}{0} \land 2^{nd} (p) = \underset{˙}{0})$
42		ianor	$⊢ \neg (1^{st} (p) = \underset{˙}{0} \land 2^{nd} (p) = \underset{˙}{0}) \leftrightarrow (\neg 1^{st} (p) = \underset{˙}{0} \lor \neg 2^{nd} (p) = \underset{˙}{0})$
43		df-ne	$⊢ 1^{st} (p) \neq \underset{˙}{0} \leftrightarrow \neg 1^{st} (p) = \underset{˙}{0}$
44		df-ne	$⊢ 2^{nd} (p) \neq \underset{˙}{0} \leftrightarrow \neg 2^{nd} (p) = \underset{˙}{0}$
45	43 44	orbi12i	$⊢ (1^{st} (p) \neq \underset{˙}{0} \lor 2^{nd} (p) \neq \underset{˙}{0}) \leftrightarrow (\neg 1^{st} (p) = \underset{˙}{0} \lor \neg 2^{nd} (p) = \underset{˙}{0})$
46	42 45	bitr4i	$⊢ \neg (1^{st} (p) = \underset{˙}{0} \land 2^{nd} (p) = \underset{˙}{0}) \leftrightarrow (1^{st} (p) \neq \underset{˙}{0} \lor 2^{nd} (p) \neq \underset{˙}{0})$
47	41 46	sylib	$⊢ (φ \land p \in ((ran F \times ran G) ∖ \{⟨\underset{˙}{0}, \underset{˙}{0}⟩\})) \to (1^{st} (p) \neq \underset{˙}{0} \lor 2^{nd} (p) \neq \underset{˙}{0})$
48	1 2 3 4 5 6 7 8 12 13 9 11	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, +∞)$
49	17 30 32 47 48	syl31anc	$⊢ (φ \land p \in ((ran F \times ran G) ∖ \{⟨\underset{˙}{0}, \underset{˙}{0}⟩\})) \to M (F^{-1} [\{1^{st} (p)\}] \cap G^{-1} [\{2^{nd} (p)\}]) \in [0, +∞)$
50		fnfvima	$⊢ (H Fn ℝ \land [0, +∞) \subseteq ℝ \land M (F^{-1} [\{1^{st} (p)\}] \cap G^{-1} [\{2^{nd} (p)\}]) \in [0, +∞)) \to H (M (F^{-1} [\{1^{st} (p)\}] \cap G^{-1} [\{2^{nd} (p)\}])) \in H [[0, +∞)]$
51	24 26 49 50	syl3anc	$⊢ (φ \land p \in ((ran F \times ran G) ∖ \{⟨\underset{˙}{0}, \underset{˙}{0}⟩\})) \to H (M (F^{-1} [\{1^{st} (p)\}] \cap G^{-1} [\{2^{nd} (p)\}])) \in H [[0, +∞)]$
52		imassrn	$⊢ H [[0, +∞)] \subseteq ran H$
53	22	frnd	$⊢ φ \to ran H \subseteq {Base}_{Scalar (W)}$
54	52 53	sstrid	$⊢ φ \to H [[0, +∞)] \subseteq {Base}_{Scalar (W)}$
55		eqid	$⊢ Scalar (W) ↾_{𝑠} H [[0, +∞)] = Scalar (W) ↾_{𝑠} H [[0, +∞)]$
56	55 18	ressbas2	$⊢ H [[0, +∞)] \subseteq {Base}_{Scalar (W)} \to H [[0, +∞)] = {Base}_{(Scalar (W) ↾_{𝑠} H [[0, +∞)])}$
57	54 56	syl	$⊢ φ \to H [[0, +∞)] = {Base}_{(Scalar (W) ↾_{𝑠} H [[0, +∞)])}$
58	17 57	syl	$⊢ (φ \land p \in ((ran F \times ran G) ∖ \{⟨\underset{˙}{0}, \underset{˙}{0}⟩\})) \to H [[0, +∞)] = {Base}_{(Scalar (W) ↾_{𝑠} H [[0, +∞)])}$
59	51 58	eleqtrd	$⊢ (φ \land p \in ((ran F \times ran G) ∖ \{⟨\underset{˙}{0}, \underset{˙}{0}⟩\})) \to H (M (F^{-1} [\{1^{st} (p)\}] \cap G^{-1} [\{2^{nd} (p)\}])) \in {Base}_{(Scalar (W) ↾_{𝑠} H [[0, +∞)])}$
60	1 2 3 4 5 6 7 8 13	sibff	$⊢ φ \to G : ⋃ dom M ⟶ ⋃ J$
61	1 2	tpsuni	$⊢ W \in TopSp \to B = ⋃ J$
62		feq3	$⊢ B = ⋃ J \to (G : ⋃ dom M ⟶ B \leftrightarrow G : ⋃ dom M ⟶ ⋃ J)$
63	9 61 62	3syl	$⊢ φ \to (G : ⋃ dom M ⟶ B \leftrightarrow G : ⋃ dom M ⟶ ⋃ J)$
64	60 63	mpbird	$⊢ φ \to G : ⋃ dom M ⟶ B$
65	64	frnd	$⊢ φ \to ran G \subseteq B$
66	65	adantr	$⊢ (φ \land p \in ((ran F \times ran G) ∖ \{⟨\underset{˙}{0}, \underset{˙}{0}⟩\})) \to ran G \subseteq B$
67	66 32	sseldd	$⊢ (φ \land p \in ((ran F \times ran G) ∖ \{⟨\underset{˙}{0}, \underset{˙}{0}⟩\})) \to 2^{nd} (p) \in B$
68	6	fvexi	$⊢ H \in V$
69		imaexg	$⊢ H \in V \to H [[0, +∞)] \in V$
70		eqid	$⊢ W ↾_{𝑣} H [[0, +∞)] = W ↾_{𝑣} H [[0, +∞)]$
71	70 1	resvbas	$⊢ H [[0, +∞)] \in V \to B = {Base}_{(W ↾_{𝑣} H [[0, +∞)])}$
72	68 69 71	mp2b	$⊢ B = {Base}_{(W ↾_{𝑣} H [[0, +∞)])}$
73		eqid	$⊢ Scalar (W) = Scalar (W)$
74	70 73 18	resvsca	$⊢ H [[0, +∞)] \in V \to Scalar (W) ↾_{𝑠} H [[0, +∞)] = Scalar (W ↾_{𝑣} H [[0, +∞)])$
75	68 69 74	mp2b	$⊢ Scalar (W) ↾_{𝑠} H [[0, +∞)] = Scalar (W ↾_{𝑣} H [[0, +∞)])$
76	70 5	resvvsca	$⊢ H [[0, +∞)] \in V \to \underset{˙}{\cdot} = \cdot_{(W ↾_{𝑣} H [[0, +∞)])}$
77	68 69 76	mp2b	$⊢ \underset{˙}{\cdot} = \cdot_{(W ↾_{𝑣} H [[0, +∞)])}$
78		eqid	$⊢ {Base}_{(Scalar (W) ↾_{𝑠} H [[0, +∞)])} = {Base}_{(Scalar (W) ↾_{𝑠} H [[0, +∞)])}$
79	72 75 77 78	slmdvscl	$⊢ (W ↾_{𝑣} H [[0, +∞)] \in SLMod \land H (M (F^{-1} [\{1^{st} (p)\}] \cap G^{-1} [\{2^{nd} (p)\}])) \in {Base}_{(Scalar (W) ↾_{𝑠} H [[0, +∞)])} \land 2^{nd} (p) \in B) \to H (M (F^{-1} [\{1^{st} (p)\}] \cap G^{-1} [\{2^{nd} (p)\}])) \underset{˙}{\cdot} 2^{nd} (p) \in B$
80	16 59 67 79	syl3anc	$⊢ (φ \land p \in ((ran F \times ran G) ∖ \{⟨\underset{˙}{0}, \underset{˙}{0}⟩\})) \to H (M (F^{-1} [\{1^{st} (p)\}] \cap G^{-1} [\{2^{nd} (p)\}])) \underset{˙}{\cdot} 2^{nd} (p) \in B$

Metamath Proof Explorer

Theorem sitgaddlemb

Proof