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 482 | . . . . 5
⊢ ((𝜑 ∧ 𝑝 ∈ ((ran 𝐹 × ran 𝐺) ∖ {〈 0 , 0 〉})) → 𝜑) | 
| 4 |  | sitgadd.6 | . . . . . . . 8
⊢ (𝜑 → (Scalar‘𝑊) ∈ ℝExt
) | 
| 5 |  | eqid 2736 | . . . . . . . . 9
⊢
(Base‘(Scalar‘𝑊)) = (Base‘(Scalar‘𝑊)) | 
| 6 | 5 | rrhfe 34014 | . . . . . . . 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 6726 | . . . . . . 7
⊢ (𝐻:ℝ⟶(Base‘(Scalar‘𝑊)) ↔
(ℝHom‘(Scalar‘𝑊)):ℝ⟶(Base‘(Scalar‘𝑊))) | 
| 10 | 7, 9 | sylibr 234 | . . . . . 6
⊢ (𝜑 → 𝐻:ℝ⟶(Base‘(Scalar‘𝑊))) | 
| 11 | 10 | ffnd 6736 | . . . . 5
⊢ (𝜑 → 𝐻 Fn ℝ) | 
| 12 | 3, 11 | syl 17 | . . . 4
⊢ ((𝜑 ∧ 𝑝 ∈ ((ran 𝐹 × ran 𝐺) ∖ {〈 0 , 0 〉})) → 𝐻 Fn ℝ) | 
| 13 |  | rge0ssre 13497 | . . . . 5
⊢
(0[,)+∞) ⊆ ℝ | 
| 14 | 13 | a1i 11 | . . . 4
⊢ ((𝜑 ∧ 𝑝 ∈ ((ran 𝐹 × ran 𝐺) ∖ {〈 0 , 0 〉})) →
(0[,)+∞) ⊆ ℝ) | 
| 15 |  | simpr 484 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑝 ∈ ((ran 𝐹 × ran 𝐺) ∖ {〈 0 , 0 〉})) → 𝑝 ∈ ((ran 𝐹 × ran 𝐺) ∖ {〈 0 , 0 〉})) | 
| 16 | 15 | eldifad 3962 | . . . . . 6
⊢ ((𝜑 ∧ 𝑝 ∈ ((ran 𝐹 × ran 𝐺) ∖ {〈 0 , 0 〉})) → 𝑝 ∈ (ran 𝐹 × ran 𝐺)) | 
| 17 |  | xp1st 8047 | . . . . . 6
⊢ (𝑝 ∈ (ran 𝐹 × ran 𝐺) → (1st ‘𝑝) ∈ ran 𝐹) | 
| 18 | 16, 17 | syl 17 | . . . . 5
⊢ ((𝜑 ∧ 𝑝 ∈ ((ran 𝐹 × ran 𝐺) ∖ {〈 0 , 0 〉})) →
(1st ‘𝑝)
∈ ran 𝐹) | 
| 19 |  | xp2nd 8048 | . . . . . 6
⊢ (𝑝 ∈ (ran 𝐹 × ran 𝐺) → (2nd ‘𝑝) ∈ ran 𝐺) | 
| 20 | 16, 19 | syl 17 | . . . . 5
⊢ ((𝜑 ∧ 𝑝 ∈ ((ran 𝐹 × ran 𝐺) ∖ {〈 0 , 0 〉})) →
(2nd ‘𝑝)
∈ ran 𝐺) | 
| 21 | 15 | eldifbd 3963 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑝 ∈ ((ran 𝐹 × ran 𝐺) ∖ {〈 0 , 0 〉})) → ¬
𝑝 ∈ {〈 0 , 0
〉}) | 
| 22 |  | velsn 4641 | . . . . . . . . 9
⊢ (𝑝 ∈ {〈 0 , 0 〉}
↔ 𝑝 = 〈 0 , 0
〉) | 
| 23 | 22 | notbii 320 | . . . . . . . 8
⊢ (¬
𝑝 ∈ {〈 0 , 0 〉}
↔ ¬ 𝑝 = 〈
0 , 0
〉) | 
| 24 | 21, 23 | sylib 218 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑝 ∈ ((ran 𝐹 × ran 𝐺) ∖ {〈 0 , 0 〉})) → ¬
𝑝 = 〈 0 , 0
〉) | 
| 25 |  | eqopi 8051 | . . . . . . . . . 10
⊢ ((𝑝 ∈ (ran 𝐹 × ran 𝐺) ∧ ((1st ‘𝑝) = 0 ∧ (2nd
‘𝑝) = 0 )) →
𝑝 = 〈 0 , 0
〉) | 
| 26 | 25 | ex 412 | . . . . . . . . 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 406 | . . . . . . 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 983 | . . . . . . 7
⊢ (¬
((1st ‘𝑝)
= 0 ∧
(2nd ‘𝑝) =
0 )
↔ (¬ (1st ‘𝑝) = 0 ∨ ¬ (2nd
‘𝑝) = 0
)) | 
| 31 |  | df-ne 2940 | . . . . . . . 8
⊢
((1st ‘𝑝) ≠ 0 ↔ ¬
(1st ‘𝑝) =
0
) | 
| 32 |  | df-ne 2940 | . . . . . . . 8
⊢
((2nd ‘𝑝) ≠ 0 ↔ ¬
(2nd ‘𝑝) =
0
) | 
| 33 | 31, 32 | orbi12i 914 | . . . . . . 7
⊢
(((1st ‘𝑝) ≠ 0 ∨ (2nd
‘𝑝) ≠ 0 ) ↔
(¬ (1st ‘𝑝) = 0 ∨ ¬ (2nd
‘𝑝) = 0
)) | 
| 34 | 30, 33 | bitr4i 278 | . . . . . 6
⊢ (¬
((1st ‘𝑝)
= 0 ∧
(2nd ‘𝑝) =
0 )
↔ ((1st ‘𝑝) ≠ 0 ∨ (2nd
‘𝑝) ≠ 0
)) | 
| 35 | 29, 34 | sylib 218 | . . . . 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 34342 | . . . . 5
⊢ (((𝜑 ∧ (1st
‘𝑝) ∈ ran 𝐹 ∧ (2nd
‘𝑝) ∈ ran 𝐺) ∧ ((1st
‘𝑝) ≠ 0 ∨
(2nd ‘𝑝)
≠ 0 ))
→ (𝑀‘((◡𝐹 “ {(1st ‘𝑝)}) ∩ (◡𝐺 “ {(2nd ‘𝑝)}))) ∈
(0[,)+∞)) | 
| 48 | 3, 18, 20, 35, 47 | syl31anc 1374 | . . . 4
⊢ ((𝜑 ∧ 𝑝 ∈ ((ran 𝐹 × ran 𝐺) ∖ {〈 0 , 0 〉})) → (𝑀‘((◡𝐹 “ {(1st ‘𝑝)}) ∩ (◡𝐺 “ {(2nd ‘𝑝)}))) ∈
(0[,)+∞)) | 
| 49 |  | fnfvima 7254 | . . . 4
⊢ ((𝐻 Fn ℝ ∧ (0[,)+∞)
⊆ ℝ ∧ (𝑀‘((◡𝐹 “ {(1st ‘𝑝)}) ∩ (◡𝐺 “ {(2nd ‘𝑝)}))) ∈ (0[,)+∞))
→ (𝐻‘(𝑀‘((◡𝐹 “ {(1st ‘𝑝)}) ∩ (◡𝐺 “ {(2nd ‘𝑝)})))) ∈ (𝐻 “ (0[,)+∞))) | 
| 50 | 12, 14, 48, 49 | syl3anc 1372 | . . 3
⊢ ((𝜑 ∧ 𝑝 ∈ ((ran 𝐹 × ran 𝐺) ∖ {〈 0 , 0 〉})) → (𝐻‘(𝑀‘((◡𝐹 “ {(1st ‘𝑝)}) ∩ (◡𝐺 “ {(2nd ‘𝑝)})))) ∈ (𝐻 “ (0[,)+∞))) | 
| 51 |  | imassrn 6088 | . . . . . 6
⊢ (𝐻 “ (0[,)+∞)) ⊆
ran 𝐻 | 
| 52 | 10 | frnd 6743 | . . . . . 6
⊢ (𝜑 → ran 𝐻 ⊆ (Base‘(Scalar‘𝑊))) | 
| 53 | 51, 52 | sstrid 3994 | . . . . 5
⊢ (𝜑 → (𝐻 “ (0[,)+∞)) ⊆
(Base‘(Scalar‘𝑊))) | 
| 54 |  | eqid 2736 | . . . . . 6
⊢
((Scalar‘𝑊)
↾s (𝐻
“ (0[,)+∞))) = ((Scalar‘𝑊) ↾s (𝐻 “ (0[,)+∞))) | 
| 55 | 54, 5 | ressbas2 17284 | . . . . 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 2842 | . 2
⊢ ((𝜑 ∧ 𝑝 ∈ ((ran 𝐹 × ran 𝐺) ∖ {〈 0 , 0 〉})) → (𝐻‘(𝑀‘((◡𝐹 “ {(1st ‘𝑝)}) ∩ (◡𝐺 “ {(2nd ‘𝑝)})))) ∈
(Base‘((Scalar‘𝑊) ↾s (𝐻 “ (0[,)+∞))))) | 
| 59 | 36, 37, 38, 39, 40, 8, 41, 42, 44 | sibff 34339 | . . . . . 6
⊢ (𝜑 → 𝐺:∪ dom 𝑀⟶∪ 𝐽) | 
| 60 | 36, 37 | tpsuni 22943 | . . . . . . 7
⊢ (𝑊 ∈ TopSp → 𝐵 = ∪
𝐽) | 
| 61 |  | feq3 6717 | . . . . . . 7
⊢ (𝐵 = ∪
𝐽 → (𝐺:∪ dom 𝑀⟶𝐵 ↔ 𝐺:∪ dom 𝑀⟶∪ 𝐽)) | 
| 62 | 45, 60, 61 | 3syl 18 | . . . . . 6
⊢ (𝜑 → (𝐺:∪ dom 𝑀⟶𝐵 ↔ 𝐺:∪ dom 𝑀⟶∪ 𝐽)) | 
| 63 | 59, 62 | mpbird 257 | . . . . 5
⊢ (𝜑 → 𝐺:∪ dom 𝑀⟶𝐵) | 
| 64 | 63 | frnd 6743 | . . . 4
⊢ (𝜑 → ran 𝐺 ⊆ 𝐵) | 
| 65 | 64 | adantr 480 | . . 3
⊢ ((𝜑 ∧ 𝑝 ∈ ((ran 𝐹 × ran 𝐺) ∖ {〈 0 , 0 〉})) → ran 𝐺 ⊆ 𝐵) | 
| 66 | 65, 20 | sseldd 3983 | . 2
⊢ ((𝜑 ∧ 𝑝 ∈ ((ran 𝐹 × ran 𝐺) ∖ {〈 0 , 0 〉})) →
(2nd ‘𝑝)
∈ 𝐵) | 
| 67 | 8 | fvexi 6919 | . . . 4
⊢ 𝐻 ∈ V | 
| 68 |  | imaexg 7936 | . . . 4
⊢ (𝐻 ∈ V → (𝐻 “ (0[,)+∞)) ∈
V) | 
| 69 |  | eqid 2736 | . . . . 5
⊢ (𝑊 ↾v (𝐻 “ (0[,)+∞))) =
(𝑊 ↾v
(𝐻 “
(0[,)+∞))) | 
| 70 | 69, 36 | resvbas 33360 | . . . 4
⊢ ((𝐻 “ (0[,)+∞)) ∈
V → 𝐵 =
(Base‘(𝑊
↾v (𝐻
“ (0[,)+∞))))) | 
| 71 | 67, 68, 70 | mp2b 10 | . . 3
⊢ 𝐵 = (Base‘(𝑊 ↾v (𝐻 “
(0[,)+∞)))) | 
| 72 |  | eqid 2736 | . . . . 5
⊢
(Scalar‘𝑊) =
(Scalar‘𝑊) | 
| 73 | 69, 72, 5 | resvsca 33357 | . . . 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 33364 | . . . 4
⊢ ((𝐻 “ (0[,)+∞)) ∈
V → · = (
·𝑠 ‘(𝑊 ↾v (𝐻 “ (0[,)+∞))))) | 
| 76 | 67, 68, 75 | mp2b 10 | . . 3
⊢  · = (
·𝑠 ‘(𝑊 ↾v (𝐻 “ (0[,)+∞)))) | 
| 77 |  | eqid 2736 | . . 3
⊢
(Base‘((Scalar‘𝑊) ↾s (𝐻 “ (0[,)+∞)))) =
(Base‘((Scalar‘𝑊) ↾s (𝐻 “ (0[,)+∞)))) | 
| 78 | 71, 74, 76, 77 | slmdvscl 33221 | . 2
⊢ (((𝑊 ↾v (𝐻 “ (0[,)+∞))) ∈
SLMod ∧ (𝐻‘(𝑀‘((◡𝐹 “ {(1st ‘𝑝)}) ∩ (◡𝐺 “ {(2nd ‘𝑝)})))) ∈
(Base‘((Scalar‘𝑊) ↾s (𝐻 “ (0[,)+∞)))) ∧
(2nd ‘𝑝)
∈ 𝐵) → ((𝐻‘(𝑀‘((◡𝐹 “ {(1st ‘𝑝)}) ∩ (◡𝐺 “ {(2nd ‘𝑝)})))) · (2nd
‘𝑝)) ∈ 𝐵) | 
| 79 | 2, 58, 66, 78 | syl3anc 1372 | 1
⊢ ((𝜑 ∧ 𝑝 ∈ ((ran 𝐹 × ran 𝐺) ∖ {〈 0 , 0 〉})) → ((𝐻‘(𝑀‘((◡𝐹 “ {(1st ‘𝑝)}) ∩ (◡𝐺 “ {(2nd ‘𝑝)})))) · (2nd
‘𝑝)) ∈ 𝐵) |