Proof of Theorem sitgaddlemb
Step | Hyp | Ref
| Expression |
1 | | sitgadd.2 |
. . 3
⊢ (𝜑 → (𝑊 ↾v (𝐻 “ (0[,)+∞))) ∈
SLMod) |
2 | 1 | adantr 481 |
. 2
⊢ ((𝜑 ∧ 𝑝 ∈ ((ran 𝐹 × ran 𝐺) ∖ {〈 0 , 0 〉})) → (𝑊 ↾v (𝐻 “ (0[,)+∞))) ∈
SLMod) |
3 | | simpl 483 |
. . . . 5
⊢ ((𝜑 ∧ 𝑝 ∈ ((ran 𝐹 × ran 𝐺) ∖ {〈 0 , 0 〉})) → 𝜑) |
4 | | sitgadd.6 |
. . . . . . . 8
⊢ (𝜑 → (Scalar‘𝑊) ∈ ℝExt
) |
5 | | eqid 2738 |
. . . . . . . . 9
⊢
(Base‘(Scalar‘𝑊)) = (Base‘(Scalar‘𝑊)) |
6 | 5 | rrhfe 31962 |
. . . . . . . 8
⊢
((Scalar‘𝑊)
∈ ℝExt → (ℝHom‘(Scalar‘𝑊)):ℝ⟶(Base‘(Scalar‘𝑊))) |
7 | 4, 6 | syl 17 |
. . . . . . 7
⊢ (𝜑 →
(ℝHom‘(Scalar‘𝑊)):ℝ⟶(Base‘(Scalar‘𝑊))) |
8 | | sitgval.h |
. . . . . . . 8
⊢ 𝐻 =
(ℝHom‘(Scalar‘𝑊)) |
9 | 8 | feq1i 6591 |
. . . . . . 7
⊢ (𝐻:ℝ⟶(Base‘(Scalar‘𝑊)) ↔
(ℝHom‘(Scalar‘𝑊)):ℝ⟶(Base‘(Scalar‘𝑊))) |
10 | 7, 9 | sylibr 233 |
. . . . . 6
⊢ (𝜑 → 𝐻:ℝ⟶(Base‘(Scalar‘𝑊))) |
11 | 10 | ffnd 6601 |
. . . . 5
⊢ (𝜑 → 𝐻 Fn ℝ) |
12 | 3, 11 | syl 17 |
. . . 4
⊢ ((𝜑 ∧ 𝑝 ∈ ((ran 𝐹 × ran 𝐺) ∖ {〈 0 , 0 〉})) → 𝐻 Fn ℝ) |
13 | | rge0ssre 13188 |
. . . . 5
⊢
(0[,)+∞) ⊆ ℝ |
14 | 13 | a1i 11 |
. . . 4
⊢ ((𝜑 ∧ 𝑝 ∈ ((ran 𝐹 × ran 𝐺) ∖ {〈 0 , 0 〉})) →
(0[,)+∞) ⊆ ℝ) |
15 | | simpr 485 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑝 ∈ ((ran 𝐹 × ran 𝐺) ∖ {〈 0 , 0 〉})) → 𝑝 ∈ ((ran 𝐹 × ran 𝐺) ∖ {〈 0 , 0 〉})) |
16 | 15 | eldifad 3899 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑝 ∈ ((ran 𝐹 × ran 𝐺) ∖ {〈 0 , 0 〉})) → 𝑝 ∈ (ran 𝐹 × ran 𝐺)) |
17 | | xp1st 7863 |
. . . . . 6
⊢ (𝑝 ∈ (ran 𝐹 × ran 𝐺) → (1st ‘𝑝) ∈ ran 𝐹) |
18 | 16, 17 | syl 17 |
. . . . 5
⊢ ((𝜑 ∧ 𝑝 ∈ ((ran 𝐹 × ran 𝐺) ∖ {〈 0 , 0 〉})) →
(1st ‘𝑝)
∈ ran 𝐹) |
19 | | xp2nd 7864 |
. . . . . 6
⊢ (𝑝 ∈ (ran 𝐹 × ran 𝐺) → (2nd ‘𝑝) ∈ ran 𝐺) |
20 | 16, 19 | syl 17 |
. . . . 5
⊢ ((𝜑 ∧ 𝑝 ∈ ((ran 𝐹 × ran 𝐺) ∖ {〈 0 , 0 〉})) →
(2nd ‘𝑝)
∈ ran 𝐺) |
21 | 15 | eldifbd 3900 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑝 ∈ ((ran 𝐹 × ran 𝐺) ∖ {〈 0 , 0 〉})) → ¬
𝑝 ∈ {〈 0 , 0
〉}) |
22 | | velsn 4577 |
. . . . . . . . 9
⊢ (𝑝 ∈ {〈 0 , 0 〉}
↔ 𝑝 = 〈 0 , 0
〉) |
23 | 22 | notbii 320 |
. . . . . . . 8
⊢ (¬
𝑝 ∈ {〈 0 , 0 〉}
↔ ¬ 𝑝 = 〈
0 , 0
〉) |
24 | 21, 23 | sylib 217 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑝 ∈ ((ran 𝐹 × ran 𝐺) ∖ {〈 0 , 0 〉})) → ¬
𝑝 = 〈 0 , 0
〉) |
25 | | eqopi 7867 |
. . . . . . . . . 10
⊢ ((𝑝 ∈ (ran 𝐹 × ran 𝐺) ∧ ((1st ‘𝑝) = 0 ∧ (2nd
‘𝑝) = 0 )) →
𝑝 = 〈 0 , 0
〉) |
26 | 25 | ex 413 |
. . . . . . . . 9
⊢ (𝑝 ∈ (ran 𝐹 × ran 𝐺) → (((1st ‘𝑝) = 0 ∧ (2nd
‘𝑝) = 0 ) →
𝑝 = 〈 0 , 0
〉)) |
27 | 26 | con3d 152 |
. . . . . . . 8
⊢ (𝑝 ∈ (ran 𝐹 × ran 𝐺) → (¬ 𝑝 = 〈 0 , 0 〉 → ¬
((1st ‘𝑝)
= 0 ∧
(2nd ‘𝑝) =
0
))) |
28 | 27 | imp 407 |
. . . . . . 7
⊢ ((𝑝 ∈ (ran 𝐹 × ran 𝐺) ∧ ¬ 𝑝 = 〈 0 , 0 〉) → ¬
((1st ‘𝑝)
= 0 ∧
(2nd ‘𝑝) =
0
)) |
29 | 16, 24, 28 | syl2anc 584 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑝 ∈ ((ran 𝐹 × ran 𝐺) ∖ {〈 0 , 0 〉})) → ¬
((1st ‘𝑝)
= 0 ∧
(2nd ‘𝑝) =
0
)) |
30 | | ianor 979 |
. . . . . . 7
⊢ (¬
((1st ‘𝑝)
= 0 ∧
(2nd ‘𝑝) =
0 )
↔ (¬ (1st ‘𝑝) = 0 ∨ ¬ (2nd
‘𝑝) = 0
)) |
31 | | df-ne 2944 |
. . . . . . . 8
⊢
((1st ‘𝑝) ≠ 0 ↔ ¬
(1st ‘𝑝) =
0
) |
32 | | df-ne 2944 |
. . . . . . . 8
⊢
((2nd ‘𝑝) ≠ 0 ↔ ¬
(2nd ‘𝑝) =
0
) |
33 | 31, 32 | orbi12i 912 |
. . . . . . 7
⊢
(((1st ‘𝑝) ≠ 0 ∨ (2nd
‘𝑝) ≠ 0 ) ↔
(¬ (1st ‘𝑝) = 0 ∨ ¬ (2nd
‘𝑝) = 0
)) |
34 | 30, 33 | bitr4i 277 |
. . . . . 6
⊢ (¬
((1st ‘𝑝)
= 0 ∧
(2nd ‘𝑝) =
0 )
↔ ((1st ‘𝑝) ≠ 0 ∨ (2nd
‘𝑝) ≠ 0
)) |
35 | 29, 34 | sylib 217 |
. . . . 5
⊢ ((𝜑 ∧ 𝑝 ∈ ((ran 𝐹 × ran 𝐺) ∖ {〈 0 , 0 〉})) →
((1st ‘𝑝)
≠ 0
∨ (2nd ‘𝑝) ≠ 0 )) |
36 | | sitgval.b |
. . . . . 6
⊢ 𝐵 = (Base‘𝑊) |
37 | | sitgval.j |
. . . . . 6
⊢ 𝐽 = (TopOpen‘𝑊) |
38 | | sitgval.s |
. . . . . 6
⊢ 𝑆 = (sigaGen‘𝐽) |
39 | | sitgval.0 |
. . . . . 6
⊢ 0 =
(0g‘𝑊) |
40 | | sitgval.x |
. . . . . 6
⊢ · = (
·𝑠 ‘𝑊) |
41 | | sitgval.1 |
. . . . . 6
⊢ (𝜑 → 𝑊 ∈ 𝑉) |
42 | | sitgval.2 |
. . . . . 6
⊢ (𝜑 → 𝑀 ∈ ∪ ran
measures) |
43 | | sitgadd.4 |
. . . . . 6
⊢ (𝜑 → 𝐹 ∈ dom (𝑊sitg𝑀)) |
44 | | sitgadd.5 |
. . . . . 6
⊢ (𝜑 → 𝐺 ∈ dom (𝑊sitg𝑀)) |
45 | | sitgadd.1 |
. . . . . 6
⊢ (𝜑 → 𝑊 ∈ TopSp) |
46 | | sitgadd.3 |
. . . . . 6
⊢ (𝜑 → 𝐽 ∈ Fre) |
47 | 36, 37, 38, 39, 40, 8, 41, 42, 43, 44, 45, 46 | sibfinima 32306 |
. . . . 5
⊢ (((𝜑 ∧ (1st
‘𝑝) ∈ ran 𝐹 ∧ (2nd
‘𝑝) ∈ ran 𝐺) ∧ ((1st
‘𝑝) ≠ 0 ∨
(2nd ‘𝑝)
≠ 0 ))
→ (𝑀‘((◡𝐹 “ {(1st ‘𝑝)}) ∩ (◡𝐺 “ {(2nd ‘𝑝)}))) ∈
(0[,)+∞)) |
48 | 3, 18, 20, 35, 47 | syl31anc 1372 |
. . . 4
⊢ ((𝜑 ∧ 𝑝 ∈ ((ran 𝐹 × ran 𝐺) ∖ {〈 0 , 0 〉})) → (𝑀‘((◡𝐹 “ {(1st ‘𝑝)}) ∩ (◡𝐺 “ {(2nd ‘𝑝)}))) ∈
(0[,)+∞)) |
49 | | fnfvima 7109 |
. . . 4
⊢ ((𝐻 Fn ℝ ∧ (0[,)+∞)
⊆ ℝ ∧ (𝑀‘((◡𝐹 “ {(1st ‘𝑝)}) ∩ (◡𝐺 “ {(2nd ‘𝑝)}))) ∈ (0[,)+∞))
→ (𝐻‘(𝑀‘((◡𝐹 “ {(1st ‘𝑝)}) ∩ (◡𝐺 “ {(2nd ‘𝑝)})))) ∈ (𝐻 “ (0[,)+∞))) |
50 | 12, 14, 48, 49 | syl3anc 1370 |
. . 3
⊢ ((𝜑 ∧ 𝑝 ∈ ((ran 𝐹 × ran 𝐺) ∖ {〈 0 , 0 〉})) → (𝐻‘(𝑀‘((◡𝐹 “ {(1st ‘𝑝)}) ∩ (◡𝐺 “ {(2nd ‘𝑝)})))) ∈ (𝐻 “ (0[,)+∞))) |
51 | | imassrn 5980 |
. . . . . 6
⊢ (𝐻 “ (0[,)+∞)) ⊆
ran 𝐻 |
52 | 10 | frnd 6608 |
. . . . . 6
⊢ (𝜑 → ran 𝐻 ⊆ (Base‘(Scalar‘𝑊))) |
53 | 51, 52 | sstrid 3932 |
. . . . 5
⊢ (𝜑 → (𝐻 “ (0[,)+∞)) ⊆
(Base‘(Scalar‘𝑊))) |
54 | | eqid 2738 |
. . . . . 6
⊢
((Scalar‘𝑊)
↾s (𝐻
“ (0[,)+∞))) = ((Scalar‘𝑊) ↾s (𝐻 “ (0[,)+∞))) |
55 | 54, 5 | ressbas2 16949 |
. . . . 5
⊢ ((𝐻 “ (0[,)+∞)) ⊆
(Base‘(Scalar‘𝑊)) → (𝐻 “ (0[,)+∞)) =
(Base‘((Scalar‘𝑊) ↾s (𝐻 “ (0[,)+∞))))) |
56 | 53, 55 | syl 17 |
. . . 4
⊢ (𝜑 → (𝐻 “ (0[,)+∞)) =
(Base‘((Scalar‘𝑊) ↾s (𝐻 “ (0[,)+∞))))) |
57 | 3, 56 | syl 17 |
. . 3
⊢ ((𝜑 ∧ 𝑝 ∈ ((ran 𝐹 × ran 𝐺) ∖ {〈 0 , 0 〉})) → (𝐻 “ (0[,)+∞)) =
(Base‘((Scalar‘𝑊) ↾s (𝐻 “ (0[,)+∞))))) |
58 | 50, 57 | eleqtrd 2841 |
. 2
⊢ ((𝜑 ∧ 𝑝 ∈ ((ran 𝐹 × ran 𝐺) ∖ {〈 0 , 0 〉})) → (𝐻‘(𝑀‘((◡𝐹 “ {(1st ‘𝑝)}) ∩ (◡𝐺 “ {(2nd ‘𝑝)})))) ∈
(Base‘((Scalar‘𝑊) ↾s (𝐻 “ (0[,)+∞))))) |
59 | 36, 37, 38, 39, 40, 8, 41, 42, 44 | sibff 32303 |
. . . . . 6
⊢ (𝜑 → 𝐺:∪ dom 𝑀⟶∪ 𝐽) |
60 | 36, 37 | tpsuni 22085 |
. . . . . . 7
⊢ (𝑊 ∈ TopSp → 𝐵 = ∪
𝐽) |
61 | | feq3 6583 |
. . . . . . 7
⊢ (𝐵 = ∪
𝐽 → (𝐺:∪ dom 𝑀⟶𝐵 ↔ 𝐺:∪ dom 𝑀⟶∪ 𝐽)) |
62 | 45, 60, 61 | 3syl 18 |
. . . . . 6
⊢ (𝜑 → (𝐺:∪ dom 𝑀⟶𝐵 ↔ 𝐺:∪ dom 𝑀⟶∪ 𝐽)) |
63 | 59, 62 | mpbird 256 |
. . . . 5
⊢ (𝜑 → 𝐺:∪ dom 𝑀⟶𝐵) |
64 | 63 | frnd 6608 |
. . . 4
⊢ (𝜑 → ran 𝐺 ⊆ 𝐵) |
65 | 64 | adantr 481 |
. . 3
⊢ ((𝜑 ∧ 𝑝 ∈ ((ran 𝐹 × ran 𝐺) ∖ {〈 0 , 0 〉})) → ran 𝐺 ⊆ 𝐵) |
66 | 65, 20 | sseldd 3922 |
. 2
⊢ ((𝜑 ∧ 𝑝 ∈ ((ran 𝐹 × ran 𝐺) ∖ {〈 0 , 0 〉})) →
(2nd ‘𝑝)
∈ 𝐵) |
67 | 8 | fvexi 6788 |
. . . 4
⊢ 𝐻 ∈ V |
68 | | imaexg 7762 |
. . . 4
⊢ (𝐻 ∈ V → (𝐻 “ (0[,)+∞)) ∈
V) |
69 | | eqid 2738 |
. . . . 5
⊢ (𝑊 ↾v (𝐻 “ (0[,)+∞))) =
(𝑊 ↾v
(𝐻 “
(0[,)+∞))) |
70 | 69, 36 | resvbas 31532 |
. . . 4
⊢ ((𝐻 “ (0[,)+∞)) ∈
V → 𝐵 =
(Base‘(𝑊
↾v (𝐻
“ (0[,)+∞))))) |
71 | 67, 68, 70 | mp2b 10 |
. . 3
⊢ 𝐵 = (Base‘(𝑊 ↾v (𝐻 “
(0[,)+∞)))) |
72 | | eqid 2738 |
. . . . 5
⊢
(Scalar‘𝑊) =
(Scalar‘𝑊) |
73 | 69, 72, 5 | resvsca 31529 |
. . . 4
⊢ ((𝐻 “ (0[,)+∞)) ∈
V → ((Scalar‘𝑊)
↾s (𝐻
“ (0[,)+∞))) = (Scalar‘(𝑊 ↾v (𝐻 “ (0[,)+∞))))) |
74 | 67, 68, 73 | mp2b 10 |
. . 3
⊢
((Scalar‘𝑊)
↾s (𝐻
“ (0[,)+∞))) = (Scalar‘(𝑊 ↾v (𝐻 “ (0[,)+∞)))) |
75 | 69, 40 | resvvsca 31536 |
. . . 4
⊢ ((𝐻 “ (0[,)+∞)) ∈
V → · = (
·𝑠 ‘(𝑊 ↾v (𝐻 “ (0[,)+∞))))) |
76 | 67, 68, 75 | mp2b 10 |
. . 3
⊢ · = (
·𝑠 ‘(𝑊 ↾v (𝐻 “ (0[,)+∞)))) |
77 | | eqid 2738 |
. . 3
⊢
(Base‘((Scalar‘𝑊) ↾s (𝐻 “ (0[,)+∞)))) =
(Base‘((Scalar‘𝑊) ↾s (𝐻 “ (0[,)+∞)))) |
78 | 71, 74, 76, 77 | slmdvscl 31467 |
. 2
⊢ (((𝑊 ↾v (𝐻 “ (0[,)+∞))) ∈
SLMod ∧ (𝐻‘(𝑀‘((◡𝐹 “ {(1st ‘𝑝)}) ∩ (◡𝐺 “ {(2nd ‘𝑝)})))) ∈
(Base‘((Scalar‘𝑊) ↾s (𝐻 “ (0[,)+∞)))) ∧
(2nd ‘𝑝)
∈ 𝐵) → ((𝐻‘(𝑀‘((◡𝐹 “ {(1st ‘𝑝)}) ∩ (◡𝐺 “ {(2nd ‘𝑝)})))) · (2nd
‘𝑝)) ∈ 𝐵) |
79 | 2, 58, 66, 78 | syl3anc 1370 |
1
⊢ ((𝜑 ∧ 𝑝 ∈ ((ran 𝐹 × ran 𝐺) ∖ {〈 0 , 0 〉})) → ((𝐻‘(𝑀‘((◡𝐹 “ {(1st ‘𝑝)}) ∩ (◡𝐺 “ {(2nd ‘𝑝)})))) · (2nd
‘𝑝)) ∈ 𝐵) |