Metamath Proof Explorer

Theorem 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 ⊢ 0 ˙ = 0 W
sitgval.x ⊢ · ˙ = ⋅ W
sitgval.h ⊢ H = ℝHom ⁡ Scalar ⁡ W
sitgval.1 ⊢ φ → W ∈ V
sitgval.2 ⊢ φ → M ∈ ⋃ ran ⁡ measures
sitgadd.1 ⊢ φ → W ∈ TopSp
sitgadd.2 ⊢ φ → W ↾ 𝑣 H 0 +∞ ∈ SLMod
sitgadd.3 ⊢ φ → J ∈ Fre
sitgadd.4 ⊢ φ → F ∈ ℑ M W
sitgadd.5 ⊢ φ → G ∈ ℑ M W
sitgadd.6 ⊢ φ → Scalar ⁡ W ∈ ℝExt
sitgadd.7 ⊢ + ˙ = + W
Assertion sitgaddlemb ⊢ φ ∧ p ∈ ran ⁡ F × ran ⁡ G ∖ 0 ˙ 0 ˙ → H ⁡ M ⁡ F -1 1 st ⁡ p ∩ G -1 2 nd ⁡ p · ˙ 2 nd ⁡ p ∈ 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 ⊢ 0 ˙ = 0 W
5 sitgval.x ⊢ · ˙ = ⋅ W
6 sitgval.h ⊢ H = ℝHom ⁡ Scalar ⁡ W
7 sitgval.1 ⊢ φ → W ∈ V
8 sitgval.2 ⊢ φ → M ∈ ⋃ ran ⁡ measures
9 sitgadd.1 ⊢ φ → W ∈ TopSp
10 sitgadd.2 ⊢ φ → W ↾ 𝑣 H 0 +∞ ∈ SLMod
11 sitgadd.3 ⊢ φ → J ∈ Fre
12 sitgadd.4 ⊢ φ → F ∈ ℑ M W
13 sitgadd.5 ⊢ φ → G ∈ ℑ M W
14 sitgadd.6 ⊢ φ → Scalar ⁡ W ∈ ℝExt
15 sitgadd.7 ⊢ + ˙ = + W
16 10 adantr ⊢ φ ∧ p ∈ ran ⁡ F × ran ⁡ G ∖ 0 ˙ 0 ˙ → W ↾ 𝑣 H 0 +∞ ∈ SLMod
17 simpl ⊢ φ ∧ p ∈ ran ⁡ F × ran ⁡ G ∖ 0 ˙ 0 ˙ → φ
18 eqid ⊢ Base Scalar ⁡ W = Base Scalar ⁡ W
19 18 rrhfe ⊢ Scalar ⁡ W ∈ ℝExt → ℝHom ⁡ Scalar ⁡ W : ℝ ⟶ Base Scalar ⁡ W
20 14 19 syl ⊢ φ → ℝHom ⁡ Scalar ⁡ W : ℝ ⟶ Base Scalar ⁡ W
21 6 feq1i ⊢ H : ℝ ⟶ Base Scalar ⁡ W ↔ ℝHom ⁡ Scalar ⁡ W : ℝ ⟶ Base Scalar ⁡ W
22 20 21 sylibr ⊢ φ → H : ℝ ⟶ Base Scalar ⁡ W
23 22 ffnd ⊢ φ → H Fn ℝ
24 17 23 syl ⊢ φ ∧ p ∈ ran ⁡ F × ran ⁡ G ∖ 0 ˙ 0 ˙ → H Fn ℝ
25 rge0ssre ⊢ 0 +∞ ⊆ ℝ
26 25 a1i ⊢ φ ∧ p ∈ ran ⁡ F × ran ⁡ G ∖ 0 ˙ 0 ˙ → 0 +∞ ⊆ ℝ
27 simpr ⊢ φ ∧ p ∈ ran ⁡ F × ran ⁡ G ∖ 0 ˙ 0 ˙ → p ∈ ran ⁡ F × ran ⁡ G ∖ 0 ˙ 0 ˙
28 27 eldifad ⊢ φ ∧ p ∈ ran ⁡ F × ran ⁡ G ∖ 0 ˙ 0 ˙ → p ∈ ran ⁡ F × ran ⁡ G
29 xp1st ⊢ p ∈ ran ⁡ F × ran ⁡ G → 1 st ⁡ p ∈ ran ⁡ F
30 28 29 syl ⊢ φ ∧ p ∈ ran ⁡ F × ran ⁡ G ∖ 0 ˙ 0 ˙ → 1 st ⁡ p ∈ ran ⁡ F
31 xp2nd ⊢ p ∈ ran ⁡ F × ran ⁡ G → 2 nd ⁡ p ∈ ran ⁡ G
32 28 31 syl ⊢ φ ∧ p ∈ ran ⁡ F × ran ⁡ G ∖ 0 ˙ 0 ˙ → 2 nd ⁡ p ∈ ran ⁡ G
33 27 eldifbd ⊢ φ ∧ p ∈ ran ⁡ F × ran ⁡ G ∖ 0 ˙ 0 ˙ → ¬ p ∈ 0 ˙ 0 ˙
34 velsn ⊢ p ∈ 0 ˙ 0 ˙ ↔ p = 0 ˙ 0 ˙
35 34 notbii ⊢ ¬ p ∈ 0 ˙ 0 ˙ ↔ ¬ p = 0 ˙ 0 ˙
36 33 35 sylib ⊢ φ ∧ p ∈ ran ⁡ F × ran ⁡ G ∖ 0 ˙ 0 ˙ → ¬ p = 0 ˙ 0 ˙
37 eqopi ⊢ p ∈ ran ⁡ F × ran ⁡ G ∧ 1 st ⁡ p = 0 ˙ ∧ 2 nd ⁡ p = 0 ˙ → p = 0 ˙ 0 ˙
38 37 ex ⊢ p ∈ ran ⁡ F × ran ⁡ G → 1 st ⁡ p = 0 ˙ ∧ 2 nd ⁡ p = 0 ˙ → p = 0 ˙ 0 ˙
39 38 con3d ⊢ p ∈ ran ⁡ F × ran ⁡ G → ¬ p = 0 ˙ 0 ˙ → ¬ 1 st ⁡ p = 0 ˙ ∧ 2 nd ⁡ p = 0 ˙
40 39 imp ⊢ p ∈ ran ⁡ F × ran ⁡ G ∧ ¬ p = 0 ˙ 0 ˙ → ¬ 1 st ⁡ p = 0 ˙ ∧ 2 nd ⁡ p = 0 ˙
41 28 36 40 syl2anc ⊢ φ ∧ p ∈ ran ⁡ F × ran ⁡ G ∖ 0 ˙ 0 ˙ → ¬ 1 st ⁡ p = 0 ˙ ∧ 2 nd ⁡ p = 0 ˙
42 ianor ⊢ ¬ 1 st ⁡ p = 0 ˙ ∧ 2 nd ⁡ p = 0 ˙ ↔ ¬ 1 st ⁡ p = 0 ˙ ∨ ¬ 2 nd ⁡ p = 0 ˙
43 df-ne ⊢ 1 st ⁡ p ≠ 0 ˙ ↔ ¬ 1 st ⁡ p = 0 ˙
44 df-ne ⊢ 2 nd ⁡ p ≠ 0 ˙ ↔ ¬ 2 nd ⁡ p = 0 ˙
45 43 44 orbi12i ⊢ 1 st ⁡ p ≠ 0 ˙ ∨ 2 nd ⁡ p ≠ 0 ˙ ↔ ¬ 1 st ⁡ p = 0 ˙ ∨ ¬ 2 nd ⁡ p = 0 ˙
46 42 45 bitr4i ⊢ ¬ 1 st ⁡ p = 0 ˙ ∧ 2 nd ⁡ p = 0 ˙ ↔ 1 st ⁡ p ≠ 0 ˙ ∨ 2 nd ⁡ p ≠ 0 ˙
47 41 46 sylib ⊢ φ ∧ p ∈ ran ⁡ F × ran ⁡ G ∖ 0 ˙ 0 ˙ → 1 st ⁡ p ≠ 0 ˙ ∨ 2 nd ⁡ p ≠ 0 ˙
48 1 2 3 4 5 6 7 8 12 13 9 11 sibfinima ⊢ φ ∧ 1 st ⁡ p ∈ ran ⁡ F ∧ 2 nd ⁡ p ∈ ran ⁡ G ∧ 1 st ⁡ p ≠ 0 ˙ ∨ 2 nd ⁡ p ≠ 0 ˙ → M ⁡ F -1 1 st ⁡ p ∩ G -1 2 nd ⁡ p ∈ 0 +∞
49 17 30 32 47 48 syl31anc ⊢ φ ∧ p ∈ ran ⁡ F × ran ⁡ G ∖ 0 ˙ 0 ˙ → M ⁡ F -1 1 st ⁡ p ∩ G -1 2 nd ⁡ p ∈ 0 +∞
50 fnfvima ⊢ H Fn ℝ ∧ 0 +∞ ⊆ ℝ ∧ M ⁡ F -1 1 st ⁡ p ∩ G -1 2 nd ⁡ p ∈ 0 +∞ → H ⁡ M ⁡ F -1 1 st ⁡ p ∩ G -1 2 nd ⁡ p ∈ H 0 +∞
51 24 26 49 50 syl3anc ⊢ φ ∧ p ∈ ran ⁡ F × ran ⁡ G ∖ 0 ˙ 0 ˙ → H ⁡ M ⁡ F -1 1 st ⁡ p ∩ G -1 2 nd ⁡ p ∈ H 0 +∞
52 imassrn ⊢ H 0 +∞ ⊆ ran ⁡ H
53 22 frnd ⊢ φ → ran ⁡ H ⊆ Base Scalar ⁡ W
54 52 53 sstrid ⊢ φ → H 0 +∞ ⊆ Base Scalar ⁡ W
55 eqid ⊢ Scalar ⁡ W ↾ 𝑠 H 0 +∞ = Scalar ⁡ W ↾ 𝑠 H 0 +∞
56 55 18 ressbas2 ⊢ H 0 +∞ ⊆ Base Scalar ⁡ W → H 0 +∞ = Base Scalar ⁡ W ↾ 𝑠 H 0 +∞
57 54 56 syl ⊢ φ → H 0 +∞ = Base Scalar ⁡ W ↾ 𝑠 H 0 +∞
58 17 57 syl ⊢ φ ∧ p ∈ ran ⁡ F × ran ⁡ G ∖ 0 ˙ 0 ˙ → H 0 +∞ = Base Scalar ⁡ W ↾ 𝑠 H 0 +∞
59 51 58 eleqtrd ⊢ φ ∧ p ∈ ran ⁡ F × ran ⁡ G ∖ 0 ˙ 0 ˙ → H ⁡ M ⁡ F -1 1 st ⁡ p ∩ G -1 2 nd ⁡ p ∈ Base Scalar ⁡ W ↾ 𝑠 H 0 +∞
60 1 2 3 4 5 6 7 8 13 sibff ⊢ φ → G : ⋃ dom ⁡ M ⟶ ⋃ J
61 1 2 tpsuni ⊢ W ∈ TopSp → B = ⋃ J
62 feq3 ⊢ B = ⋃ J → G : ⋃ dom ⁡ M ⟶ B ↔ G : ⋃ dom ⁡ M ⟶ ⋃ J
63 9 61 62 3syl ⊢ φ → G : ⋃ dom ⁡ M ⟶ B ↔ G : ⋃ dom ⁡ M ⟶ ⋃ J
64 60 63 mpbird ⊢ φ → G : ⋃ dom ⁡ M ⟶ B
65 64 frnd ⊢ φ → ran ⁡ G ⊆ B
66 65 adantr ⊢ φ ∧ p ∈ ran ⁡ F × ran ⁡ G ∖ 0 ˙ 0 ˙ → ran ⁡ G ⊆ B
67 66 32 sseldd ⊢ φ ∧ p ∈ ran ⁡ F × ran ⁡ G ∖ 0 ˙ 0 ˙ → 2 nd ⁡ p ∈ B
68 6 fvexi ⊢ H ∈ V
69 imaexg ⊢ H ∈ V → H 0 +∞ ∈ V
70 eqid ⊢ W ↾ 𝑣 H 0 +∞ = W ↾ 𝑣 H 0 +∞
71 70 1 resvbas ⊢ H 0 +∞ ∈ V → 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 +∞ ∈ V → 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 +∞ ∈ V → · ˙ = ⋅ W ↾ 𝑣 H 0 +∞
77 68 69 76 mp2b ⊢ · ˙ = ⋅ W ↾ 𝑣 H 0 +∞
78 eqid ⊢ Base Scalar ⁡ W ↾ 𝑠 H 0 +∞ = Base Scalar ⁡ W ↾ 𝑠 H 0 +∞
79 72 75 77 78 slmdvscl ⊢ W ↾ 𝑣 H 0 +∞ ∈ SLMod ∧ H ⁡ M ⁡ F -1 1 st ⁡ p ∩ G -1 2 nd ⁡ p ∈ Base Scalar ⁡ W ↾ 𝑠 H 0 +∞ ∧ 2 nd ⁡ p ∈ B → H ⁡ M ⁡ F -1 1 st ⁡ p ∩ G -1 2 nd ⁡ p · ˙ 2 nd ⁡ p ∈ B
80 16 59 67 79 syl3anc ⊢ φ ∧ p ∈ ran ⁡ F × ran ⁡ G ∖ 0 ˙ 0 ˙ → H ⁡ M ⁡ F -1 1 st ⁡ p ∩ G -1 2 nd ⁡ p · ˙ 2 nd ⁡ p ∈ B