Step | Hyp | Ref
| Expression |
1 | | imasbas.u |
. . 3
⊢ (𝜑 → 𝑈 = (𝐹 “s 𝑅)) |
2 | | imasbas.v |
. . 3
⊢ (𝜑 → 𝑉 = (Base‘𝑅)) |
3 | | eqid 2740 |
. . 3
⊢
(+g‘𝑅) = (+g‘𝑅) |
4 | | imasmulr.p |
. . 3
⊢ · =
(.r‘𝑅) |
5 | | eqid 2740 |
. . 3
⊢
(Scalar‘𝑅) =
(Scalar‘𝑅) |
6 | | eqid 2740 |
. . 3
⊢
(Base‘(Scalar‘𝑅)) = (Base‘(Scalar‘𝑅)) |
7 | | eqid 2740 |
. . 3
⊢ (
·𝑠 ‘𝑅) = ( ·𝑠
‘𝑅) |
8 | | eqid 2740 |
. . 3
⊢
(·𝑖‘𝑅) =
(·𝑖‘𝑅) |
9 | | eqid 2740 |
. . 3
⊢
(TopOpen‘𝑅) =
(TopOpen‘𝑅) |
10 | | eqid 2740 |
. . 3
⊢
(dist‘𝑅) =
(dist‘𝑅) |
11 | | eqid 2740 |
. . 3
⊢
(le‘𝑅) =
(le‘𝑅) |
12 | | imasbas.f |
. . . 4
⊢ (𝜑 → 𝐹:𝑉–onto→𝐵) |
13 | | imasbas.r |
. . . 4
⊢ (𝜑 → 𝑅 ∈ 𝑍) |
14 | | eqid 2740 |
. . . 4
⊢
(+g‘𝑈) = (+g‘𝑈) |
15 | 1, 2, 12, 13, 3, 14 | imasplusg 17226 |
. . 3
⊢ (𝜑 → (+g‘𝑈) = ∪ 𝑝 ∈ 𝑉 ∪ 𝑞 ∈ 𝑉 {〈〈(𝐹‘𝑝), (𝐹‘𝑞)〉, (𝐹‘(𝑝(+g‘𝑅)𝑞))〉}) |
16 | | eqidd 2741 |
. . 3
⊢ (𝜑 → ∪ 𝑝 ∈ 𝑉 ∪ 𝑞 ∈ 𝑉 {〈〈(𝐹‘𝑝), (𝐹‘𝑞)〉, (𝐹‘(𝑝 · 𝑞))〉} = ∪ 𝑝 ∈ 𝑉 ∪ 𝑞 ∈ 𝑉 {〈〈(𝐹‘𝑝), (𝐹‘𝑞)〉, (𝐹‘(𝑝 · 𝑞))〉}) |
17 | | eqidd 2741 |
. . 3
⊢ (𝜑 → ∪ 𝑞 ∈ 𝑉 (𝑝 ∈ (Base‘(Scalar‘𝑅)), 𝑥 ∈ {(𝐹‘𝑞)} ↦ (𝐹‘(𝑝( ·𝑠
‘𝑅)𝑞))) = ∪
𝑞 ∈ 𝑉 (𝑝 ∈ (Base‘(Scalar‘𝑅)), 𝑥 ∈ {(𝐹‘𝑞)} ↦ (𝐹‘(𝑝( ·𝑠
‘𝑅)𝑞)))) |
18 | | eqidd 2741 |
. . 3
⊢ (𝜑 → ∪ 𝑝 ∈ 𝑉 ∪ 𝑞 ∈ 𝑉 {〈〈(𝐹‘𝑝), (𝐹‘𝑞)〉, (𝑝(·𝑖‘𝑅)𝑞)〉} = ∪
𝑝 ∈ 𝑉 ∪ 𝑞 ∈ 𝑉 {〈〈(𝐹‘𝑝), (𝐹‘𝑞)〉, (𝑝(·𝑖‘𝑅)𝑞)〉}) |
19 | | eqidd 2741 |
. . 3
⊢ (𝜑 → ((TopOpen‘𝑅) qTop 𝐹) = ((TopOpen‘𝑅) qTop 𝐹)) |
20 | | eqid 2740 |
. . . 4
⊢
(dist‘𝑈) =
(dist‘𝑈) |
21 | 1, 2, 12, 13, 10, 20 | imasds 17222 |
. . 3
⊢ (𝜑 → (dist‘𝑈) = (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ inf(∪ 𝑛 ∈ ℕ ran (𝑔 ∈ {ℎ ∈ ((𝑉 × 𝑉) ↑m (1...𝑛)) ∣ ((𝐹‘(1st ‘(ℎ‘1))) = 𝑥 ∧ (𝐹‘(2nd ‘(ℎ‘𝑛))) = 𝑦 ∧ ∀𝑖 ∈ (1...(𝑛 − 1))(𝐹‘(2nd ‘(ℎ‘𝑖))) = (𝐹‘(1st ‘(ℎ‘(𝑖 + 1)))))} ↦
(ℝ*𝑠 Σg
((dist‘𝑅) ∘
𝑔))), ℝ*,
< ))) |
22 | | eqidd 2741 |
. . 3
⊢ (𝜑 → ((𝐹 ∘ (le‘𝑅)) ∘ ◡𝐹) = ((𝐹 ∘ (le‘𝑅)) ∘ ◡𝐹)) |
23 | 1, 2, 3, 4, 5, 6, 7, 8, 9, 10,
11, 15, 16, 17, 18, 19, 21, 22, 12, 13 | imasval 17220 |
. 2
⊢ (𝜑 → 𝑈 = (({〈(Base‘ndx), 𝐵〉,
〈(+g‘ndx), (+g‘𝑈)〉, 〈(.r‘ndx),
∪ 𝑝 ∈ 𝑉 ∪ 𝑞 ∈ 𝑉 {〈〈(𝐹‘𝑝), (𝐹‘𝑞)〉, (𝐹‘(𝑝 · 𝑞))〉}〉} ∪
{〈(Scalar‘ndx), (Scalar‘𝑅)〉, 〈(
·𝑠 ‘ndx), ∪ 𝑞 ∈ 𝑉 (𝑝 ∈ (Base‘(Scalar‘𝑅)), 𝑥 ∈ {(𝐹‘𝑞)} ↦ (𝐹‘(𝑝( ·𝑠
‘𝑅)𝑞)))〉,
〈(·𝑖‘ndx), ∪ 𝑝 ∈ 𝑉 ∪ 𝑞 ∈ 𝑉 {〈〈(𝐹‘𝑝), (𝐹‘𝑞)〉, (𝑝(·𝑖‘𝑅)𝑞)〉}〉}) ∪
{〈(TopSet‘ndx), ((TopOpen‘𝑅) qTop 𝐹)〉, 〈(le‘ndx), ((𝐹 ∘ (le‘𝑅)) ∘ ◡𝐹)〉, 〈(dist‘ndx),
(dist‘𝑈)〉})) |
24 | | eqid 2740 |
. . 3
⊢
(({〈(Base‘ndx), 𝐵〉, 〈(+g‘ndx),
(+g‘𝑈)〉, 〈(.r‘ndx),
∪ 𝑝 ∈ 𝑉 ∪ 𝑞 ∈ 𝑉 {〈〈(𝐹‘𝑝), (𝐹‘𝑞)〉, (𝐹‘(𝑝 · 𝑞))〉}〉} ∪
{〈(Scalar‘ndx), (Scalar‘𝑅)〉, 〈(
·𝑠 ‘ndx), ∪ 𝑞 ∈ 𝑉 (𝑝 ∈ (Base‘(Scalar‘𝑅)), 𝑥 ∈ {(𝐹‘𝑞)} ↦ (𝐹‘(𝑝( ·𝑠
‘𝑅)𝑞)))〉,
〈(·𝑖‘ndx), ∪ 𝑝 ∈ 𝑉 ∪ 𝑞 ∈ 𝑉 {〈〈(𝐹‘𝑝), (𝐹‘𝑞)〉, (𝑝(·𝑖‘𝑅)𝑞)〉}〉}) ∪
{〈(TopSet‘ndx), ((TopOpen‘𝑅) qTop 𝐹)〉, 〈(le‘ndx), ((𝐹 ∘ (le‘𝑅)) ∘ ◡𝐹)〉, 〈(dist‘ndx),
(dist‘𝑈)〉}) =
(({〈(Base‘ndx), 𝐵〉, 〈(+g‘ndx),
(+g‘𝑈)〉,
〈(.r‘ndx), ∪ 𝑝 ∈ 𝑉 ∪ 𝑞 ∈ 𝑉 {〈〈(𝐹‘𝑝), (𝐹‘𝑞)〉, (𝐹‘(𝑝 · 𝑞))〉}〉} ∪
{〈(Scalar‘ndx), (Scalar‘𝑅)〉, 〈(
·𝑠 ‘ndx), ∪ 𝑞
∈ 𝑉 (𝑝 ∈ (Base‘(Scalar‘𝑅)), 𝑥 ∈ {(𝐹‘𝑞)} ↦ (𝐹‘(𝑝( ·𝑠
‘𝑅)𝑞)))〉,
〈(·𝑖‘ndx), ∪ 𝑝
∈ 𝑉 ∪ 𝑞
∈ 𝑉 {〈〈(𝐹‘𝑝), (𝐹‘𝑞)〉, (𝑝(·𝑖‘𝑅)𝑞)〉}〉}) ∪
{〈(TopSet‘ndx), ((TopOpen‘𝑅) qTop 𝐹)〉, 〈(le‘ndx), ((𝐹 ∘ (le‘𝑅)) ∘ ◡𝐹)〉, 〈(dist‘ndx),
(dist‘𝑈)〉}) |
25 | 24 | imasvalstr 17160 |
. 2
⊢
(({〈(Base‘ndx), 𝐵〉, 〈(+g‘ndx),
(+g‘𝑈)〉, 〈(.r‘ndx),
∪ 𝑝 ∈ 𝑉 ∪ 𝑞 ∈ 𝑉 {〈〈(𝐹‘𝑝), (𝐹‘𝑞)〉, (𝐹‘(𝑝 · 𝑞))〉}〉} ∪
{〈(Scalar‘ndx), (Scalar‘𝑅)〉, 〈(
·𝑠 ‘ndx), ∪ 𝑞 ∈ 𝑉 (𝑝 ∈ (Base‘(Scalar‘𝑅)), 𝑥 ∈ {(𝐹‘𝑞)} ↦ (𝐹‘(𝑝( ·𝑠
‘𝑅)𝑞)))〉,
〈(·𝑖‘ndx), ∪ 𝑝 ∈ 𝑉 ∪ 𝑞 ∈ 𝑉 {〈〈(𝐹‘𝑝), (𝐹‘𝑞)〉, (𝑝(·𝑖‘𝑅)𝑞)〉}〉}) ∪
{〈(TopSet‘ndx), ((TopOpen‘𝑅) qTop 𝐹)〉, 〈(le‘ndx), ((𝐹 ∘ (le‘𝑅)) ∘ ◡𝐹)〉, 〈(dist‘ndx),
(dist‘𝑈)〉}) Struct
〈1, ;12〉 |
26 | | mulrid 17002 |
. 2
⊢
.r = Slot (.r‘ndx) |
27 | | snsstp3 4757 |
. . . 4
⊢
{〈(.r‘ndx), ∪
𝑝 ∈ 𝑉 ∪ 𝑞 ∈ 𝑉 {〈〈(𝐹‘𝑝), (𝐹‘𝑞)〉, (𝐹‘(𝑝 · 𝑞))〉}〉} ⊆
{〈(Base‘ndx), 𝐵〉, 〈(+g‘ndx),
(+g‘𝑈)〉, 〈(.r‘ndx),
∪ 𝑝 ∈ 𝑉 ∪ 𝑞 ∈ 𝑉 {〈〈(𝐹‘𝑝), (𝐹‘𝑞)〉, (𝐹‘(𝑝 · 𝑞))〉}〉} |
28 | | ssun1 4111 |
. . . 4
⊢
{〈(Base‘ndx), 𝐵〉, 〈(+g‘ndx),
(+g‘𝑈)〉, 〈(.r‘ndx),
∪ 𝑝 ∈ 𝑉 ∪ 𝑞 ∈ 𝑉 {〈〈(𝐹‘𝑝), (𝐹‘𝑞)〉, (𝐹‘(𝑝 · 𝑞))〉}〉} ⊆
({〈(Base‘ndx), 𝐵〉, 〈(+g‘ndx),
(+g‘𝑈)〉, 〈(.r‘ndx),
∪ 𝑝 ∈ 𝑉 ∪ 𝑞 ∈ 𝑉 {〈〈(𝐹‘𝑝), (𝐹‘𝑞)〉, (𝐹‘(𝑝 · 𝑞))〉}〉} ∪
{〈(Scalar‘ndx), (Scalar‘𝑅)〉, 〈(
·𝑠 ‘ndx), ∪ 𝑞 ∈ 𝑉 (𝑝 ∈ (Base‘(Scalar‘𝑅)), 𝑥 ∈ {(𝐹‘𝑞)} ↦ (𝐹‘(𝑝( ·𝑠
‘𝑅)𝑞)))〉,
〈(·𝑖‘ndx), ∪ 𝑝 ∈ 𝑉 ∪ 𝑞 ∈ 𝑉 {〈〈(𝐹‘𝑝), (𝐹‘𝑞)〉, (𝑝(·𝑖‘𝑅)𝑞)〉}〉}) |
29 | 27, 28 | sstri 3935 |
. . 3
⊢
{〈(.r‘ndx), ∪
𝑝 ∈ 𝑉 ∪ 𝑞 ∈ 𝑉 {〈〈(𝐹‘𝑝), (𝐹‘𝑞)〉, (𝐹‘(𝑝 · 𝑞))〉}〉} ⊆
({〈(Base‘ndx), 𝐵〉, 〈(+g‘ndx),
(+g‘𝑈)〉, 〈(.r‘ndx),
∪ 𝑝 ∈ 𝑉 ∪ 𝑞 ∈ 𝑉 {〈〈(𝐹‘𝑝), (𝐹‘𝑞)〉, (𝐹‘(𝑝 · 𝑞))〉}〉} ∪
{〈(Scalar‘ndx), (Scalar‘𝑅)〉, 〈(
·𝑠 ‘ndx), ∪ 𝑞 ∈ 𝑉 (𝑝 ∈ (Base‘(Scalar‘𝑅)), 𝑥 ∈ {(𝐹‘𝑞)} ↦ (𝐹‘(𝑝( ·𝑠
‘𝑅)𝑞)))〉,
〈(·𝑖‘ndx), ∪ 𝑝 ∈ 𝑉 ∪ 𝑞 ∈ 𝑉 {〈〈(𝐹‘𝑝), (𝐹‘𝑞)〉, (𝑝(·𝑖‘𝑅)𝑞)〉}〉}) |
30 | | ssun1 4111 |
. . 3
⊢
({〈(Base‘ndx), 𝐵〉, 〈(+g‘ndx),
(+g‘𝑈)〉, 〈(.r‘ndx),
∪ 𝑝 ∈ 𝑉 ∪ 𝑞 ∈ 𝑉 {〈〈(𝐹‘𝑝), (𝐹‘𝑞)〉, (𝐹‘(𝑝 · 𝑞))〉}〉} ∪
{〈(Scalar‘ndx), (Scalar‘𝑅)〉, 〈(
·𝑠 ‘ndx), ∪ 𝑞 ∈ 𝑉 (𝑝 ∈ (Base‘(Scalar‘𝑅)), 𝑥 ∈ {(𝐹‘𝑞)} ↦ (𝐹‘(𝑝( ·𝑠
‘𝑅)𝑞)))〉,
〈(·𝑖‘ndx), ∪ 𝑝 ∈ 𝑉 ∪ 𝑞 ∈ 𝑉 {〈〈(𝐹‘𝑝), (𝐹‘𝑞)〉, (𝑝(·𝑖‘𝑅)𝑞)〉}〉}) ⊆
(({〈(Base‘ndx), 𝐵〉, 〈(+g‘ndx),
(+g‘𝑈)〉,
〈(.r‘ndx), ∪ 𝑝 ∈ 𝑉 ∪ 𝑞 ∈ 𝑉 {〈〈(𝐹‘𝑝), (𝐹‘𝑞)〉, (𝐹‘(𝑝 · 𝑞))〉}〉} ∪
{〈(Scalar‘ndx), (Scalar‘𝑅)〉, 〈(
·𝑠 ‘ndx), ∪ 𝑞
∈ 𝑉 (𝑝 ∈ (Base‘(Scalar‘𝑅)), 𝑥 ∈ {(𝐹‘𝑞)} ↦ (𝐹‘(𝑝( ·𝑠
‘𝑅)𝑞)))〉,
〈(·𝑖‘ndx), ∪ 𝑝
∈ 𝑉 ∪ 𝑞
∈ 𝑉 {〈〈(𝐹‘𝑝), (𝐹‘𝑞)〉, (𝑝(·𝑖‘𝑅)𝑞)〉}〉}) ∪
{〈(TopSet‘ndx), ((TopOpen‘𝑅) qTop 𝐹)〉, 〈(le‘ndx), ((𝐹 ∘ (le‘𝑅)) ∘ ◡𝐹)〉, 〈(dist‘ndx),
(dist‘𝑈)〉}) |
31 | 29, 30 | sstri 3935 |
. 2
⊢
{〈(.r‘ndx), ∪
𝑝 ∈ 𝑉 ∪ 𝑞 ∈ 𝑉 {〈〈(𝐹‘𝑝), (𝐹‘𝑞)〉, (𝐹‘(𝑝 · 𝑞))〉}〉} ⊆
(({〈(Base‘ndx), 𝐵〉, 〈(+g‘ndx),
(+g‘𝑈)〉, 〈(.r‘ndx),
∪ 𝑝 ∈ 𝑉 ∪ 𝑞 ∈ 𝑉 {〈〈(𝐹‘𝑝), (𝐹‘𝑞)〉, (𝐹‘(𝑝 · 𝑞))〉}〉} ∪
{〈(Scalar‘ndx), (Scalar‘𝑅)〉, 〈(
·𝑠 ‘ndx), ∪ 𝑞 ∈ 𝑉 (𝑝 ∈ (Base‘(Scalar‘𝑅)), 𝑥 ∈ {(𝐹‘𝑞)} ↦ (𝐹‘(𝑝( ·𝑠
‘𝑅)𝑞)))〉,
〈(·𝑖‘ndx), ∪ 𝑝 ∈ 𝑉 ∪ 𝑞 ∈ 𝑉 {〈〈(𝐹‘𝑝), (𝐹‘𝑞)〉, (𝑝(·𝑖‘𝑅)𝑞)〉}〉}) ∪
{〈(TopSet‘ndx), ((TopOpen‘𝑅) qTop 𝐹)〉, 〈(le‘ndx), ((𝐹 ∘ (le‘𝑅)) ∘ ◡𝐹)〉, 〈(dist‘ndx),
(dist‘𝑈)〉}) |
32 | | fvex 6784 |
. . . 4
⊢
(Base‘𝑅)
∈ V |
33 | 2, 32 | eqeltrdi 2849 |
. . 3
⊢ (𝜑 → 𝑉 ∈ V) |
34 | | snex 5358 |
. . . . . 6
⊢
{〈〈(𝐹‘𝑝), (𝐹‘𝑞)〉, (𝐹‘(𝑝 · 𝑞))〉} ∈ V |
35 | 34 | rgenw 3078 |
. . . . 5
⊢
∀𝑞 ∈
𝑉 {〈〈(𝐹‘𝑝), (𝐹‘𝑞)〉, (𝐹‘(𝑝 · 𝑞))〉} ∈ V |
36 | | iunexg 7799 |
. . . . 5
⊢ ((𝑉 ∈ V ∧ ∀𝑞 ∈ 𝑉 {〈〈(𝐹‘𝑝), (𝐹‘𝑞)〉, (𝐹‘(𝑝 · 𝑞))〉} ∈ V) → ∪ 𝑞 ∈ 𝑉 {〈〈(𝐹‘𝑝), (𝐹‘𝑞)〉, (𝐹‘(𝑝 · 𝑞))〉} ∈ V) |
37 | 33, 35, 36 | sylancl 586 |
. . . 4
⊢ (𝜑 → ∪ 𝑞 ∈ 𝑉 {〈〈(𝐹‘𝑝), (𝐹‘𝑞)〉, (𝐹‘(𝑝 · 𝑞))〉} ∈ V) |
38 | 37 | ralrimivw 3111 |
. . 3
⊢ (𝜑 → ∀𝑝 ∈ 𝑉 ∪ 𝑞 ∈ 𝑉 {〈〈(𝐹‘𝑝), (𝐹‘𝑞)〉, (𝐹‘(𝑝 · 𝑞))〉} ∈ V) |
39 | | iunexg 7799 |
. . 3
⊢ ((𝑉 ∈ V ∧ ∀𝑝 ∈ 𝑉 ∪ 𝑞 ∈ 𝑉 {〈〈(𝐹‘𝑝), (𝐹‘𝑞)〉, (𝐹‘(𝑝 · 𝑞))〉} ∈ V) → ∪ 𝑝 ∈ 𝑉 ∪ 𝑞 ∈ 𝑉 {〈〈(𝐹‘𝑝), (𝐹‘𝑞)〉, (𝐹‘(𝑝 · 𝑞))〉} ∈ V) |
40 | 33, 38, 39 | syl2anc 584 |
. 2
⊢ (𝜑 → ∪ 𝑝 ∈ 𝑉 ∪ 𝑞 ∈ 𝑉 {〈〈(𝐹‘𝑝), (𝐹‘𝑞)〉, (𝐹‘(𝑝 · 𝑞))〉} ∈ V) |
41 | | imasmulr.t |
. 2
⊢ ∙ =
(.r‘𝑈) |
42 | 23, 25, 26, 31, 40, 41 | strfv3 16904 |
1
⊢ (𝜑 → ∙ = ∪ 𝑝 ∈ 𝑉 ∪ 𝑞 ∈ 𝑉 {〈〈(𝐹‘𝑝), (𝐹‘𝑞)〉, (𝐹‘(𝑝 · 𝑞))〉}) |