Step | Hyp | Ref
| Expression |
1 | | imassca.g |
. . . 4
⊢ 𝐺 = (Scalar‘𝑅) |
2 | 1 | fvexi 6749 |
. . 3
⊢ 𝐺 ∈ V |
3 | | eqid 2738 |
. . . . 5
⊢
(({〈(Base‘ndx), 𝐵〉, 〈(+g‘ndx),
(+g‘𝑈)〉, 〈(.r‘ndx),
(.r‘𝑈)〉} ∪ {〈(Scalar‘ndx),
𝐺〉, 〈(
·𝑠 ‘ndx), ∪ 𝑞 ∈ 𝑉 (𝑝 ∈ (Base‘𝐺), 𝑥 ∈ {(𝐹‘𝑞)} ↦ (𝐹‘(𝑝( ·𝑠
‘𝑅)𝑞)))〉,
〈(·𝑖‘ndx), ∪ 𝑝 ∈ 𝑉 ∪ 𝑞 ∈ 𝑉 {〈〈(𝐹‘𝑝), (𝐹‘𝑞)〉, (𝑝(·𝑖‘𝑅)𝑞)〉}〉}) ∪
{〈(TopSet‘ndx), ((TopOpen‘𝑅) qTop 𝐹)〉, 〈(le‘ndx), ((𝐹 ∘ (le‘𝑅)) ∘ ◡𝐹)〉, 〈(dist‘ndx),
(dist‘𝑈)〉}) =
(({〈(Base‘ndx), 𝐵〉, 〈(+g‘ndx),
(+g‘𝑈)〉,
〈(.r‘ndx), (.r‘𝑈)〉} ∪ {〈(Scalar‘ndx), 𝐺〉, 〈(
·𝑠 ‘ndx), ∪ 𝑞
∈ 𝑉 (𝑝 ∈ (Base‘𝐺), 𝑥 ∈ {(𝐹‘𝑞)} ↦ (𝐹‘(𝑝( ·𝑠
‘𝑅)𝑞)))〉,
〈(·𝑖‘ndx), ∪ 𝑝
∈ 𝑉 ∪ 𝑞
∈ 𝑉 {〈〈(𝐹‘𝑝), (𝐹‘𝑞)〉, (𝑝(·𝑖‘𝑅)𝑞)〉}〉}) ∪
{〈(TopSet‘ndx), ((TopOpen‘𝑅) qTop 𝐹)〉, 〈(le‘ndx), ((𝐹 ∘ (le‘𝑅)) ∘ ◡𝐹)〉, 〈(dist‘ndx),
(dist‘𝑈)〉}) |
4 | 3 | imasvalstr 16980 |
. . . 4
⊢
(({〈(Base‘ndx), 𝐵〉, 〈(+g‘ndx),
(+g‘𝑈)〉, 〈(.r‘ndx),
(.r‘𝑈)〉} ∪ {〈(Scalar‘ndx),
𝐺〉, 〈(
·𝑠 ‘ndx), ∪ 𝑞 ∈ 𝑉 (𝑝 ∈ (Base‘𝐺), 𝑥 ∈ {(𝐹‘𝑞)} ↦ (𝐹‘(𝑝( ·𝑠
‘𝑅)𝑞)))〉,
〈(·𝑖‘ndx), ∪ 𝑝 ∈ 𝑉 ∪ 𝑞 ∈ 𝑉 {〈〈(𝐹‘𝑝), (𝐹‘𝑞)〉, (𝑝(·𝑖‘𝑅)𝑞)〉}〉}) ∪
{〈(TopSet‘ndx), ((TopOpen‘𝑅) qTop 𝐹)〉, 〈(le‘ndx), ((𝐹 ∘ (le‘𝑅)) ∘ ◡𝐹)〉, 〈(dist‘ndx),
(dist‘𝑈)〉}) Struct
〈1, ;12〉 |
5 | | scaid 16880 |
. . . 4
⊢ Scalar =
Slot (Scalar‘ndx) |
6 | | snsstp1 4743 |
. . . . . 6
⊢
{〈(Scalar‘ndx), 𝐺〉} ⊆ {〈(Scalar‘ndx),
𝐺〉, 〈(
·𝑠 ‘ndx), ∪ 𝑞 ∈ 𝑉 (𝑝 ∈ (Base‘𝐺), 𝑥 ∈ {(𝐹‘𝑞)} ↦ (𝐹‘(𝑝( ·𝑠
‘𝑅)𝑞)))〉,
〈(·𝑖‘ndx), ∪ 𝑝 ∈ 𝑉 ∪ 𝑞 ∈ 𝑉 {〈〈(𝐹‘𝑝), (𝐹‘𝑞)〉, (𝑝(·𝑖‘𝑅)𝑞)〉}〉} |
7 | | ssun2 4101 |
. . . . . 6
⊢
{〈(Scalar‘ndx), 𝐺〉, 〈(
·𝑠 ‘ndx), ∪ 𝑞 ∈ 𝑉 (𝑝 ∈ (Base‘𝐺), 𝑥 ∈ {(𝐹‘𝑞)} ↦ (𝐹‘(𝑝( ·𝑠
‘𝑅)𝑞)))〉,
〈(·𝑖‘ndx), ∪ 𝑝 ∈ 𝑉 ∪ 𝑞 ∈ 𝑉 {〈〈(𝐹‘𝑝), (𝐹‘𝑞)〉, (𝑝(·𝑖‘𝑅)𝑞)〉}〉} ⊆
({〈(Base‘ndx), 𝐵〉, 〈(+g‘ndx),
(+g‘𝑈)〉,
〈(.r‘ndx), (.r‘𝑈)〉} ∪ {〈(Scalar‘ndx), 𝐺〉, 〈(
·𝑠 ‘ndx), ∪ 𝑞
∈ 𝑉 (𝑝 ∈ (Base‘𝐺), 𝑥 ∈ {(𝐹‘𝑞)} ↦ (𝐹‘(𝑝( ·𝑠
‘𝑅)𝑞)))〉,
〈(·𝑖‘ndx), ∪ 𝑝
∈ 𝑉 ∪ 𝑞
∈ 𝑉 {〈〈(𝐹‘𝑝), (𝐹‘𝑞)〉, (𝑝(·𝑖‘𝑅)𝑞)〉}〉}) |
8 | 6, 7 | sstri 3924 |
. . . . 5
⊢
{〈(Scalar‘ndx), 𝐺〉} ⊆ ({〈(Base‘ndx),
𝐵〉,
〈(+g‘ndx), (+g‘𝑈)〉, 〈(.r‘ndx),
(.r‘𝑈)〉} ∪ {〈(Scalar‘ndx),
𝐺〉, 〈(
·𝑠 ‘ndx), ∪ 𝑞 ∈ 𝑉 (𝑝 ∈ (Base‘𝐺), 𝑥 ∈ {(𝐹‘𝑞)} ↦ (𝐹‘(𝑝( ·𝑠
‘𝑅)𝑞)))〉,
〈(·𝑖‘ndx), ∪ 𝑝 ∈ 𝑉 ∪ 𝑞 ∈ 𝑉 {〈〈(𝐹‘𝑝), (𝐹‘𝑞)〉, (𝑝(·𝑖‘𝑅)𝑞)〉}〉}) |
9 | | ssun1 4100 |
. . . . 5
⊢
({〈(Base‘ndx), 𝐵〉, 〈(+g‘ndx),
(+g‘𝑈)〉, 〈(.r‘ndx),
(.r‘𝑈)〉} ∪ {〈(Scalar‘ndx),
𝐺〉, 〈(
·𝑠 ‘ndx), ∪ 𝑞 ∈ 𝑉 (𝑝 ∈ (Base‘𝐺), 𝑥 ∈ {(𝐹‘𝑞)} ↦ (𝐹‘(𝑝( ·𝑠
‘𝑅)𝑞)))〉,
〈(·𝑖‘ndx), ∪ 𝑝 ∈ 𝑉 ∪ 𝑞 ∈ 𝑉 {〈〈(𝐹‘𝑝), (𝐹‘𝑞)〉, (𝑝(·𝑖‘𝑅)𝑞)〉}〉}) ⊆
(({〈(Base‘ndx), 𝐵〉, 〈(+g‘ndx),
(+g‘𝑈)〉,
〈(.r‘ndx), (.r‘𝑈)〉} ∪ {〈(Scalar‘ndx), 𝐺〉, 〈(
·𝑠 ‘ndx), ∪ 𝑞
∈ 𝑉 (𝑝 ∈ (Base‘𝐺), 𝑥 ∈ {(𝐹‘𝑞)} ↦ (𝐹‘(𝑝( ·𝑠
‘𝑅)𝑞)))〉,
〈(·𝑖‘ndx), ∪ 𝑝
∈ 𝑉 ∪ 𝑞
∈ 𝑉 {〈〈(𝐹‘𝑝), (𝐹‘𝑞)〉, (𝑝(·𝑖‘𝑅)𝑞)〉}〉}) ∪
{〈(TopSet‘ndx), ((TopOpen‘𝑅) qTop 𝐹)〉, 〈(le‘ndx), ((𝐹 ∘ (le‘𝑅)) ∘ ◡𝐹)〉, 〈(dist‘ndx),
(dist‘𝑈)〉}) |
10 | 8, 9 | sstri 3924 |
. . . 4
⊢
{〈(Scalar‘ndx), 𝐺〉} ⊆ (({〈(Base‘ndx),
𝐵〉,
〈(+g‘ndx), (+g‘𝑈)〉, 〈(.r‘ndx),
(.r‘𝑈)〉} ∪ {〈(Scalar‘ndx),
𝐺〉, 〈(
·𝑠 ‘ndx), ∪ 𝑞 ∈ 𝑉 (𝑝 ∈ (Base‘𝐺), 𝑥 ∈ {(𝐹‘𝑞)} ↦ (𝐹‘(𝑝( ·𝑠
‘𝑅)𝑞)))〉,
〈(·𝑖‘ndx), ∪ 𝑝 ∈ 𝑉 ∪ 𝑞 ∈ 𝑉 {〈〈(𝐹‘𝑝), (𝐹‘𝑞)〉, (𝑝(·𝑖‘𝑅)𝑞)〉}〉}) ∪
{〈(TopSet‘ndx), ((TopOpen‘𝑅) qTop 𝐹)〉, 〈(le‘ndx), ((𝐹 ∘ (le‘𝑅)) ∘ ◡𝐹)〉, 〈(dist‘ndx),
(dist‘𝑈)〉}) |
11 | 4, 5, 10 | strfv 16778 |
. . 3
⊢ (𝐺 ∈ V → 𝐺 =
(Scalar‘(({〈(Base‘ndx), 𝐵〉, 〈(+g‘ndx),
(+g‘𝑈)〉, 〈(.r‘ndx),
(.r‘𝑈)〉} ∪ {〈(Scalar‘ndx),
𝐺〉, 〈(
·𝑠 ‘ndx), ∪ 𝑞 ∈ 𝑉 (𝑝 ∈ (Base‘𝐺), 𝑥 ∈ {(𝐹‘𝑞)} ↦ (𝐹‘(𝑝( ·𝑠
‘𝑅)𝑞)))〉,
〈(·𝑖‘ndx), ∪ 𝑝 ∈ 𝑉 ∪ 𝑞 ∈ 𝑉 {〈〈(𝐹‘𝑝), (𝐹‘𝑞)〉, (𝑝(·𝑖‘𝑅)𝑞)〉}〉}) ∪
{〈(TopSet‘ndx), ((TopOpen‘𝑅) qTop 𝐹)〉, 〈(le‘ndx), ((𝐹 ∘ (le‘𝑅)) ∘ ◡𝐹)〉, 〈(dist‘ndx),
(dist‘𝑈)〉}))) |
12 | 2, 11 | ax-mp 5 |
. 2
⊢ 𝐺 =
(Scalar‘(({〈(Base‘ndx), 𝐵〉, 〈(+g‘ndx),
(+g‘𝑈)〉, 〈(.r‘ndx),
(.r‘𝑈)〉} ∪ {〈(Scalar‘ndx),
𝐺〉, 〈(
·𝑠 ‘ndx), ∪ 𝑞 ∈ 𝑉 (𝑝 ∈ (Base‘𝐺), 𝑥 ∈ {(𝐹‘𝑞)} ↦ (𝐹‘(𝑝( ·𝑠
‘𝑅)𝑞)))〉,
〈(·𝑖‘ndx), ∪ 𝑝 ∈ 𝑉 ∪ 𝑞 ∈ 𝑉 {〈〈(𝐹‘𝑝), (𝐹‘𝑞)〉, (𝑝(·𝑖‘𝑅)𝑞)〉}〉}) ∪
{〈(TopSet‘ndx), ((TopOpen‘𝑅) qTop 𝐹)〉, 〈(le‘ndx), ((𝐹 ∘ (le‘𝑅)) ∘ ◡𝐹)〉, 〈(dist‘ndx),
(dist‘𝑈)〉})) |
13 | | imasbas.u |
. . . 4
⊢ (𝜑 → 𝑈 = (𝐹 “s 𝑅)) |
14 | | imasbas.v |
. . . 4
⊢ (𝜑 → 𝑉 = (Base‘𝑅)) |
15 | | eqid 2738 |
. . . 4
⊢
(+g‘𝑅) = (+g‘𝑅) |
16 | | eqid 2738 |
. . . 4
⊢
(.r‘𝑅) = (.r‘𝑅) |
17 | | eqid 2738 |
. . . 4
⊢
(Base‘𝐺) =
(Base‘𝐺) |
18 | | eqid 2738 |
. . . 4
⊢ (
·𝑠 ‘𝑅) = ( ·𝑠
‘𝑅) |
19 | | eqid 2738 |
. . . 4
⊢
(·𝑖‘𝑅) =
(·𝑖‘𝑅) |
20 | | eqid 2738 |
. . . 4
⊢
(TopOpen‘𝑅) =
(TopOpen‘𝑅) |
21 | | eqid 2738 |
. . . 4
⊢
(dist‘𝑅) =
(dist‘𝑅) |
22 | | eqid 2738 |
. . . 4
⊢
(le‘𝑅) =
(le‘𝑅) |
23 | | imasbas.f |
. . . . 5
⊢ (𝜑 → 𝐹:𝑉–onto→𝐵) |
24 | | imasbas.r |
. . . . 5
⊢ (𝜑 → 𝑅 ∈ 𝑍) |
25 | | eqid 2738 |
. . . . 5
⊢
(+g‘𝑈) = (+g‘𝑈) |
26 | 13, 14, 23, 24, 15, 25 | imasplusg 17046 |
. . . 4
⊢ (𝜑 → (+g‘𝑈) = ∪ 𝑝 ∈ 𝑉 ∪ 𝑞 ∈ 𝑉 {〈〈(𝐹‘𝑝), (𝐹‘𝑞)〉, (𝐹‘(𝑝(+g‘𝑅)𝑞))〉}) |
27 | | eqid 2738 |
. . . . 5
⊢
(.r‘𝑈) = (.r‘𝑈) |
28 | 13, 14, 23, 24, 16, 27 | imasmulr 17047 |
. . . 4
⊢ (𝜑 → (.r‘𝑈) = ∪ 𝑝 ∈ 𝑉 ∪ 𝑞 ∈ 𝑉 {〈〈(𝐹‘𝑝), (𝐹‘𝑞)〉, (𝐹‘(𝑝(.r‘𝑅)𝑞))〉}) |
29 | | eqidd 2739 |
. . . 4
⊢ (𝜑 → ∪ 𝑞 ∈ 𝑉 (𝑝 ∈ (Base‘𝐺), 𝑥 ∈ {(𝐹‘𝑞)} ↦ (𝐹‘(𝑝( ·𝑠
‘𝑅)𝑞))) = ∪
𝑞 ∈ 𝑉 (𝑝 ∈ (Base‘𝐺), 𝑥 ∈ {(𝐹‘𝑞)} ↦ (𝐹‘(𝑝( ·𝑠
‘𝑅)𝑞)))) |
30 | | eqidd 2739 |
. . . 4
⊢ (𝜑 → ∪ 𝑝 ∈ 𝑉 ∪ 𝑞 ∈ 𝑉 {〈〈(𝐹‘𝑝), (𝐹‘𝑞)〉, (𝑝(·𝑖‘𝑅)𝑞)〉} = ∪
𝑝 ∈ 𝑉 ∪ 𝑞 ∈ 𝑉 {〈〈(𝐹‘𝑝), (𝐹‘𝑞)〉, (𝑝(·𝑖‘𝑅)𝑞)〉}) |
31 | | eqidd 2739 |
. . . 4
⊢ (𝜑 → ((TopOpen‘𝑅) qTop 𝐹) = ((TopOpen‘𝑅) qTop 𝐹)) |
32 | | eqid 2738 |
. . . . 5
⊢
(dist‘𝑈) =
(dist‘𝑈) |
33 | 13, 14, 23, 24, 21, 32 | imasds 17042 |
. . . 4
⊢ (𝜑 → (dist‘𝑈) = (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ inf(∪ 𝑛 ∈ ℕ ran (𝑔 ∈ {ℎ ∈ ((𝑉 × 𝑉) ↑m (1...𝑛)) ∣ ((𝐹‘(1st ‘(ℎ‘1))) = 𝑥 ∧ (𝐹‘(2nd ‘(ℎ‘𝑛))) = 𝑦 ∧ ∀𝑖 ∈ (1...(𝑛 − 1))(𝐹‘(2nd ‘(ℎ‘𝑖))) = (𝐹‘(1st ‘(ℎ‘(𝑖 + 1)))))} ↦
(ℝ*𝑠 Σg
((dist‘𝑅) ∘
𝑔))), ℝ*,
< ))) |
34 | | eqidd 2739 |
. . . 4
⊢ (𝜑 → ((𝐹 ∘ (le‘𝑅)) ∘ ◡𝐹) = ((𝐹 ∘ (le‘𝑅)) ∘ ◡𝐹)) |
35 | 13, 14, 15, 16, 1, 17, 18, 19, 20, 21, 22, 26, 28, 29, 30, 31, 33, 34, 23, 24 | imasval 17040 |
. . 3
⊢ (𝜑 → 𝑈 = (({〈(Base‘ndx), 𝐵〉,
〈(+g‘ndx), (+g‘𝑈)〉, 〈(.r‘ndx),
(.r‘𝑈)〉} ∪ {〈(Scalar‘ndx),
𝐺〉, 〈(
·𝑠 ‘ndx), ∪ 𝑞 ∈ 𝑉 (𝑝 ∈ (Base‘𝐺), 𝑥 ∈ {(𝐹‘𝑞)} ↦ (𝐹‘(𝑝( ·𝑠
‘𝑅)𝑞)))〉,
〈(·𝑖‘ndx), ∪ 𝑝 ∈ 𝑉 ∪ 𝑞 ∈ 𝑉 {〈〈(𝐹‘𝑝), (𝐹‘𝑞)〉, (𝑝(·𝑖‘𝑅)𝑞)〉}〉}) ∪
{〈(TopSet‘ndx), ((TopOpen‘𝑅) qTop 𝐹)〉, 〈(le‘ndx), ((𝐹 ∘ (le‘𝑅)) ∘ ◡𝐹)〉, 〈(dist‘ndx),
(dist‘𝑈)〉})) |
36 | 35 | fveq2d 6739 |
. 2
⊢ (𝜑 → (Scalar‘𝑈) =
(Scalar‘(({〈(Base‘ndx), 𝐵〉, 〈(+g‘ndx),
(+g‘𝑈)〉, 〈(.r‘ndx),
(.r‘𝑈)〉} ∪ {〈(Scalar‘ndx),
𝐺〉, 〈(
·𝑠 ‘ndx), ∪ 𝑞 ∈ 𝑉 (𝑝 ∈ (Base‘𝐺), 𝑥 ∈ {(𝐹‘𝑞)} ↦ (𝐹‘(𝑝( ·𝑠
‘𝑅)𝑞)))〉,
〈(·𝑖‘ndx), ∪ 𝑝 ∈ 𝑉 ∪ 𝑞 ∈ 𝑉 {〈〈(𝐹‘𝑝), (𝐹‘𝑞)〉, (𝑝(·𝑖‘𝑅)𝑞)〉}〉}) ∪
{〈(TopSet‘ndx), ((TopOpen‘𝑅) qTop 𝐹)〉, 〈(le‘ndx), ((𝐹 ∘ (le‘𝑅)) ∘ ◡𝐹)〉, 〈(dist‘ndx),
(dist‘𝑈)〉}))) |
37 | 12, 36 | eqtr4id 2798 |
1
⊢ (𝜑 → 𝐺 = (Scalar‘𝑈)) |