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