Proof of Theorem sitgaddlemb
Step | Hyp | Ref
| Expression |
1 | | sitgadd.2 |
. . 3
⊢ (𝜑 → (𝑊 ↾v (𝐻 “ (0[,)+∞))) ∈
SLMod) |
2 | 1 | adantr 480 |
. 2
⊢ ((𝜑 ∧ 𝑝 ∈ ((ran 𝐹 × ran 𝐺) ∖ {〈 0 , 0 〉})) → (𝑊 ↾v (𝐻 “ (0[,)+∞))) ∈
SLMod) |
3 | | simpl 472 |
. . . . 5
⊢ ((𝜑 ∧ 𝑝 ∈ ((ran 𝐹 × ran 𝐺) ∖ {〈 0 , 0 〉})) → 𝜑) |
4 | | sitgadd.6 |
. . . . . . . 8
⊢ (𝜑 → (Scalar‘𝑊) ∈ ℝExt
) |
5 | | eqid 2610 |
. . . . . . . . 9
⊢
(Base‘(Scalar‘𝑊)) = (Base‘(Scalar‘𝑊)) |
6 | 5 | rrhfe 29384 |
. . . . . . . 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 5949 |
. . . . . . 7
⊢ (𝐻:ℝ⟶(Base‘(Scalar‘𝑊)) ↔
(ℝHom‘(Scalar‘𝑊)):ℝ⟶(Base‘(Scalar‘𝑊))) |
10 | 7, 9 | sylibr 223 |
. . . . . 6
⊢ (𝜑 → 𝐻:ℝ⟶(Base‘(Scalar‘𝑊))) |
11 | | ffn 5958 |
. . . . . 6
⊢ (𝐻:ℝ⟶(Base‘(Scalar‘𝑊)) → 𝐻 Fn ℝ) |
12 | 10, 11 | syl 17 |
. . . . 5
⊢ (𝜑 → 𝐻 Fn ℝ) |
13 | 3, 12 | syl 17 |
. . . 4
⊢ ((𝜑 ∧ 𝑝 ∈ ((ran 𝐹 × ran 𝐺) ∖ {〈 0 , 0 〉})) → 𝐻 Fn ℝ) |
14 | | rge0ssre 12151 |
. . . . 5
⊢
(0[,)+∞) ⊆ ℝ |
15 | 14 | a1i 11 |
. . . 4
⊢ ((𝜑 ∧ 𝑝 ∈ ((ran 𝐹 × ran 𝐺) ∖ {〈 0 , 0 〉})) →
(0[,)+∞) ⊆ ℝ) |
16 | | simpr 476 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑝 ∈ ((ran 𝐹 × ran 𝐺) ∖ {〈 0 , 0 〉})) → 𝑝 ∈ ((ran 𝐹 × ran 𝐺) ∖ {〈 0 , 0 〉})) |
17 | 16 | eldifad 3552 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑝 ∈ ((ran 𝐹 × ran 𝐺) ∖ {〈 0 , 0 〉})) → 𝑝 ∈ (ran 𝐹 × ran 𝐺)) |
18 | | xp1st 7089 |
. . . . . 6
⊢ (𝑝 ∈ (ran 𝐹 × ran 𝐺) → (1st ‘𝑝) ∈ ran 𝐹) |
19 | 17, 18 | syl 17 |
. . . . 5
⊢ ((𝜑 ∧ 𝑝 ∈ ((ran 𝐹 × ran 𝐺) ∖ {〈 0 , 0 〉})) →
(1st ‘𝑝)
∈ ran 𝐹) |
20 | | xp2nd 7090 |
. . . . . 6
⊢ (𝑝 ∈ (ran 𝐹 × ran 𝐺) → (2nd ‘𝑝) ∈ ran 𝐺) |
21 | 17, 20 | syl 17 |
. . . . 5
⊢ ((𝜑 ∧ 𝑝 ∈ ((ran 𝐹 × ran 𝐺) ∖ {〈 0 , 0 〉})) →
(2nd ‘𝑝)
∈ ran 𝐺) |
22 | 16 | eldifbd 3553 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑝 ∈ ((ran 𝐹 × ran 𝐺) ∖ {〈 0 , 0 〉})) → ¬
𝑝 ∈ {〈 0 , 0
〉}) |
23 | | velsn 4141 |
. . . . . . . . 9
⊢ (𝑝 ∈ {〈 0 , 0 〉}
↔ 𝑝 = 〈 0 , 0
〉) |
24 | 23 | notbii 309 |
. . . . . . . 8
⊢ (¬
𝑝 ∈ {〈 0 , 0 〉}
↔ ¬ 𝑝 = 〈
0 , 0
〉) |
25 | 22, 24 | sylib 207 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑝 ∈ ((ran 𝐹 × ran 𝐺) ∖ {〈 0 , 0 〉})) → ¬
𝑝 = 〈 0 , 0
〉) |
26 | | eqopi 7093 |
. . . . . . . . . 10
⊢ ((𝑝 ∈ (ran 𝐹 × ran 𝐺) ∧ ((1st ‘𝑝) = 0 ∧ (2nd
‘𝑝) = 0 )) →
𝑝 = 〈 0 , 0
〉) |
27 | 26 | ex 449 |
. . . . . . . . 9
⊢ (𝑝 ∈ (ran 𝐹 × ran 𝐺) → (((1st ‘𝑝) = 0 ∧ (2nd
‘𝑝) = 0 ) →
𝑝 = 〈 0 , 0
〉)) |
28 | 27 | con3d 147 |
. . . . . . . 8
⊢ (𝑝 ∈ (ran 𝐹 × ran 𝐺) → (¬ 𝑝 = 〈 0 , 0 〉 → ¬
((1st ‘𝑝)
= 0 ∧
(2nd ‘𝑝) =
0
))) |
29 | 28 | imp 444 |
. . . . . . 7
⊢ ((𝑝 ∈ (ran 𝐹 × ran 𝐺) ∧ ¬ 𝑝 = 〈 0 , 0 〉) → ¬
((1st ‘𝑝)
= 0 ∧
(2nd ‘𝑝) =
0
)) |
30 | 17, 25, 29 | syl2anc 691 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑝 ∈ ((ran 𝐹 × ran 𝐺) ∖ {〈 0 , 0 〉})) → ¬
((1st ‘𝑝)
= 0 ∧
(2nd ‘𝑝) =
0
)) |
31 | | ianor 508 |
. . . . . . 7
⊢ (¬
((1st ‘𝑝)
= 0 ∧
(2nd ‘𝑝) =
0 )
↔ (¬ (1st ‘𝑝) = 0 ∨ ¬ (2nd
‘𝑝) = 0
)) |
32 | | df-ne 2782 |
. . . . . . . 8
⊢
((1st ‘𝑝) ≠ 0 ↔ ¬
(1st ‘𝑝) =
0
) |
33 | | df-ne 2782 |
. . . . . . . 8
⊢
((2nd ‘𝑝) ≠ 0 ↔ ¬
(2nd ‘𝑝) =
0
) |
34 | 32, 33 | orbi12i 542 |
. . . . . . 7
⊢
(((1st ‘𝑝) ≠ 0 ∨ (2nd
‘𝑝) ≠ 0 ) ↔
(¬ (1st ‘𝑝) = 0 ∨ ¬ (2nd
‘𝑝) = 0
)) |
35 | 31, 34 | bitr4i 266 |
. . . . . 6
⊢ (¬
((1st ‘𝑝)
= 0 ∧
(2nd ‘𝑝) =
0 )
↔ ((1st ‘𝑝) ≠ 0 ∨ (2nd
‘𝑝) ≠ 0
)) |
36 | 30, 35 | sylib 207 |
. . . . 5
⊢ ((𝜑 ∧ 𝑝 ∈ ((ran 𝐹 × ran 𝐺) ∖ {〈 0 , 0 〉})) →
((1st ‘𝑝)
≠ 0
∨ (2nd ‘𝑝) ≠ 0 )) |
37 | | sitgval.b |
. . . . . 6
⊢ 𝐵 = (Base‘𝑊) |
38 | | sitgval.j |
. . . . . 6
⊢ 𝐽 = (TopOpen‘𝑊) |
39 | | sitgval.s |
. . . . . 6
⊢ 𝑆 = (sigaGen‘𝐽) |
40 | | sitgval.0 |
. . . . . 6
⊢ 0 =
(0g‘𝑊) |
41 | | sitgval.x |
. . . . . 6
⊢ · = (
·𝑠 ‘𝑊) |
42 | | sitgval.1 |
. . . . . 6
⊢ (𝜑 → 𝑊 ∈ 𝑉) |
43 | | sitgval.2 |
. . . . . 6
⊢ (𝜑 → 𝑀 ∈ ∪ ran
measures) |
44 | | sitgadd.4 |
. . . . . 6
⊢ (𝜑 → 𝐹 ∈ dom (𝑊sitg𝑀)) |
45 | | sitgadd.5 |
. . . . . 6
⊢ (𝜑 → 𝐺 ∈ dom (𝑊sitg𝑀)) |
46 | | sitgadd.1 |
. . . . . 6
⊢ (𝜑 → 𝑊 ∈ TopSp) |
47 | | sitgadd.3 |
. . . . . 6
⊢ (𝜑 → 𝐽 ∈ Fre) |
48 | 37, 38, 39, 40, 41, 8, 42, 43, 44, 45, 46, 47 | sibfinima 29728 |
. . . . 5
⊢ (((𝜑 ∧ (1st
‘𝑝) ∈ ran 𝐹 ∧ (2nd
‘𝑝) ∈ ran 𝐺) ∧ ((1st
‘𝑝) ≠ 0 ∨
(2nd ‘𝑝)
≠ 0 ))
→ (𝑀‘((◡𝐹 “ {(1st ‘𝑝)}) ∩ (◡𝐺 “ {(2nd ‘𝑝)}))) ∈
(0[,)+∞)) |
49 | 3, 19, 21, 36, 48 | syl31anc 1321 |
. . . 4
⊢ ((𝜑 ∧ 𝑝 ∈ ((ran 𝐹 × ran 𝐺) ∖ {〈 0 , 0 〉})) → (𝑀‘((◡𝐹 “ {(1st ‘𝑝)}) ∩ (◡𝐺 “ {(2nd ‘𝑝)}))) ∈
(0[,)+∞)) |
50 | | fnfvima 6400 |
. . . 4
⊢ ((𝐻 Fn ℝ ∧ (0[,)+∞)
⊆ ℝ ∧ (𝑀‘((◡𝐹 “ {(1st ‘𝑝)}) ∩ (◡𝐺 “ {(2nd ‘𝑝)}))) ∈ (0[,)+∞))
→ (𝐻‘(𝑀‘((◡𝐹 “ {(1st ‘𝑝)}) ∩ (◡𝐺 “ {(2nd ‘𝑝)})))) ∈ (𝐻 “ (0[,)+∞))) |
51 | 13, 15, 49, 50 | syl3anc 1318 |
. . 3
⊢ ((𝜑 ∧ 𝑝 ∈ ((ran 𝐹 × ran 𝐺) ∖ {〈 0 , 0 〉})) → (𝐻‘(𝑀‘((◡𝐹 “ {(1st ‘𝑝)}) ∩ (◡𝐺 “ {(2nd ‘𝑝)})))) ∈ (𝐻 “ (0[,)+∞))) |
52 | | imassrn 5396 |
. . . . . 6
⊢ (𝐻 “ (0[,)+∞)) ⊆
ran 𝐻 |
53 | | frn 5966 |
. . . . . . 7
⊢ (𝐻:ℝ⟶(Base‘(Scalar‘𝑊)) → ran 𝐻 ⊆ (Base‘(Scalar‘𝑊))) |
54 | 10, 53 | syl 17 |
. . . . . 6
⊢ (𝜑 → ran 𝐻 ⊆ (Base‘(Scalar‘𝑊))) |
55 | 52, 54 | syl5ss 3579 |
. . . . 5
⊢ (𝜑 → (𝐻 “ (0[,)+∞)) ⊆
(Base‘(Scalar‘𝑊))) |
56 | | eqid 2610 |
. . . . . 6
⊢
((Scalar‘𝑊)
↾s (𝐻
“ (0[,)+∞))) = ((Scalar‘𝑊) ↾s (𝐻 “ (0[,)+∞))) |
57 | 56, 5 | ressbas2 15758 |
. . . . 5
⊢ ((𝐻 “ (0[,)+∞)) ⊆
(Base‘(Scalar‘𝑊)) → (𝐻 “ (0[,)+∞)) =
(Base‘((Scalar‘𝑊) ↾s (𝐻 “ (0[,)+∞))))) |
58 | 55, 57 | syl 17 |
. . . 4
⊢ (𝜑 → (𝐻 “ (0[,)+∞)) =
(Base‘((Scalar‘𝑊) ↾s (𝐻 “ (0[,)+∞))))) |
59 | 3, 58 | syl 17 |
. . 3
⊢ ((𝜑 ∧ 𝑝 ∈ ((ran 𝐹 × ran 𝐺) ∖ {〈 0 , 0 〉})) → (𝐻 “ (0[,)+∞)) =
(Base‘((Scalar‘𝑊) ↾s (𝐻 “ (0[,)+∞))))) |
60 | 51, 59 | eleqtrd 2690 |
. 2
⊢ ((𝜑 ∧ 𝑝 ∈ ((ran 𝐹 × ran 𝐺) ∖ {〈 0 , 0 〉})) → (𝐻‘(𝑀‘((◡𝐹 “ {(1st ‘𝑝)}) ∩ (◡𝐺 “ {(2nd ‘𝑝)})))) ∈
(Base‘((Scalar‘𝑊) ↾s (𝐻 “ (0[,)+∞))))) |
61 | 37, 38, 39, 40, 41, 8, 42, 43, 45 | sibff 29725 |
. . . . . 6
⊢ (𝜑 → 𝐺:∪ dom 𝑀⟶∪ 𝐽) |
62 | 37, 38 | tpsuni 20553 |
. . . . . . 7
⊢ (𝑊 ∈ TopSp → 𝐵 = ∪
𝐽) |
63 | | feq3 5941 |
. . . . . . 7
⊢ (𝐵 = ∪
𝐽 → (𝐺:∪ dom 𝑀⟶𝐵 ↔ 𝐺:∪ dom 𝑀⟶∪ 𝐽)) |
64 | 46, 62, 63 | 3syl 18 |
. . . . . 6
⊢ (𝜑 → (𝐺:∪ dom 𝑀⟶𝐵 ↔ 𝐺:∪ dom 𝑀⟶∪ 𝐽)) |
65 | 61, 64 | mpbird 246 |
. . . . 5
⊢ (𝜑 → 𝐺:∪ dom 𝑀⟶𝐵) |
66 | | frn 5966 |
. . . . 5
⊢ (𝐺:∪
dom 𝑀⟶𝐵 → ran 𝐺 ⊆ 𝐵) |
67 | 65, 66 | syl 17 |
. . . 4
⊢ (𝜑 → ran 𝐺 ⊆ 𝐵) |
68 | 67 | adantr 480 |
. . 3
⊢ ((𝜑 ∧ 𝑝 ∈ ((ran 𝐹 × ran 𝐺) ∖ {〈 0 , 0 〉})) → ran 𝐺 ⊆ 𝐵) |
69 | 68, 21 | sseldd 3569 |
. 2
⊢ ((𝜑 ∧ 𝑝 ∈ ((ran 𝐹 × ran 𝐺) ∖ {〈 0 , 0 〉})) →
(2nd ‘𝑝)
∈ 𝐵) |
70 | | fvex 6113 |
. . . . 5
⊢
(ℝHom‘(Scalar‘𝑊)) ∈ V |
71 | 8, 70 | eqeltri 2684 |
. . . 4
⊢ 𝐻 ∈ V |
72 | | imaexg 6995 |
. . . 4
⊢ (𝐻 ∈ V → (𝐻 “ (0[,)+∞)) ∈
V) |
73 | | eqid 2610 |
. . . . 5
⊢ (𝑊 ↾v (𝐻 “ (0[,)+∞))) =
(𝑊 ↾v
(𝐻 “
(0[,)+∞))) |
74 | 73, 37 | resvbas 29163 |
. . . 4
⊢ ((𝐻 “ (0[,)+∞)) ∈
V → 𝐵 =
(Base‘(𝑊
↾v (𝐻
“ (0[,)+∞))))) |
75 | 71, 72, 74 | mp2b 10 |
. . 3
⊢ 𝐵 = (Base‘(𝑊 ↾v (𝐻 “
(0[,)+∞)))) |
76 | | eqid 2610 |
. . . . 5
⊢
(Scalar‘𝑊) =
(Scalar‘𝑊) |
77 | 73, 76, 5 | resvsca 29161 |
. . . 4
⊢ ((𝐻 “ (0[,)+∞)) ∈
V → ((Scalar‘𝑊)
↾s (𝐻
“ (0[,)+∞))) = (Scalar‘(𝑊 ↾v (𝐻 “ (0[,)+∞))))) |
78 | 71, 72, 77 | mp2b 10 |
. . 3
⊢
((Scalar‘𝑊)
↾s (𝐻
“ (0[,)+∞))) = (Scalar‘(𝑊 ↾v (𝐻 “ (0[,)+∞)))) |
79 | 73, 41 | resvvsca 29165 |
. . . 4
⊢ ((𝐻 “ (0[,)+∞)) ∈
V → · = (
·𝑠 ‘(𝑊 ↾v (𝐻 “ (0[,)+∞))))) |
80 | 71, 72, 79 | mp2b 10 |
. . 3
⊢ · = (
·𝑠 ‘(𝑊 ↾v (𝐻 “ (0[,)+∞)))) |
81 | | eqid 2610 |
. . 3
⊢
(Base‘((Scalar‘𝑊) ↾s (𝐻 “ (0[,)+∞)))) =
(Base‘((Scalar‘𝑊) ↾s (𝐻 “ (0[,)+∞)))) |
82 | 75, 78, 80, 81 | slmdvscl 29098 |
. 2
⊢ (((𝑊 ↾v (𝐻 “ (0[,)+∞))) ∈
SLMod ∧ (𝐻‘(𝑀‘((◡𝐹 “ {(1st ‘𝑝)}) ∩ (◡𝐺 “ {(2nd ‘𝑝)})))) ∈
(Base‘((Scalar‘𝑊) ↾s (𝐻 “ (0[,)+∞)))) ∧
(2nd ‘𝑝)
∈ 𝐵) → ((𝐻‘(𝑀‘((◡𝐹 “ {(1st ‘𝑝)}) ∩ (◡𝐺 “ {(2nd ‘𝑝)})))) · (2nd
‘𝑝)) ∈ 𝐵) |
83 | 2, 60, 69, 82 | syl3anc 1318 |
1
⊢ ((𝜑 ∧ 𝑝 ∈ ((ran 𝐹 × ran 𝐺) ∖ {〈 0 , 0 〉})) → ((𝐻‘(𝑀‘((◡𝐹 “ {(1st ‘𝑝)}) ∩ (◡𝐺 “ {(2nd ‘𝑝)})))) · (2nd
‘𝑝)) ∈ 𝐵) |