Step | Hyp | Ref
| Expression |
1 | | basendxnplusgndx 17164 |
. . . . . . 7
⊢
(Base‘ndx) ≠ (+g‘ndx) |
2 | | basendxnmulrndx 17177 |
. . . . . . 7
⊢
(Base‘ndx) ≠ (.r‘ndx) |
3 | | plusgndxnmulrndx 17179 |
. . . . . . 7
⊢
(+g‘ndx) ≠
(.r‘ndx) |
4 | | fvex 6856 |
. . . . . . . 8
⊢
(Base‘ndx) ∈ V |
5 | | fvex 6856 |
. . . . . . . 8
⊢
(+g‘ndx) ∈ V |
6 | | fvex 6856 |
. . . . . . . 8
⊢
(.r‘ndx) ∈ V |
7 | | cnex 11133 |
. . . . . . . 8
⊢ ℂ
∈ V |
8 | | addex 12914 |
. . . . . . . 8
⊢ + ∈
V |
9 | | mulex 12915 |
. . . . . . . 8
⊢ ·
∈ V |
10 | 4, 5, 6, 7, 8, 9 | funtp 6559 |
. . . . . . 7
⊢
(((Base‘ndx) ≠ (+g‘ndx) ∧ (Base‘ndx)
≠ (.r‘ndx) ∧ (+g‘ndx) ≠
(.r‘ndx)) → Fun {⟨(Base‘ndx), ℂ⟩,
⟨(+g‘ndx), + ⟩, ⟨(.r‘ndx),
· ⟩}) |
11 | 1, 2, 3, 10 | mp3an 1462 |
. . . . . 6
⊢ Fun
{⟨(Base‘ndx), ℂ⟩, ⟨(+g‘ndx), +
⟩, ⟨(.r‘ndx), · ⟩} |
12 | | fvex 6856 |
. . . . . . 7
⊢
(*𝑟‘ndx) ∈ V |
13 | | cjf 14990 |
. . . . . . . 8
⊢
∗:ℂ⟶ℂ |
14 | | fex 7177 |
. . . . . . . 8
⊢
((∗:ℂ⟶ℂ ∧ ℂ ∈ V) →
∗ ∈ V) |
15 | 13, 7, 14 | mp2an 691 |
. . . . . . 7
⊢ ∗
∈ V |
16 | 12, 15 | funsn 6555 |
. . . . . 6
⊢ Fun
{⟨(*𝑟‘ndx), ∗⟩} |
17 | 11, 16 | pm3.2i 472 |
. . . . 5
⊢ (Fun
{⟨(Base‘ndx), ℂ⟩, ⟨(+g‘ndx), +
⟩, ⟨(.r‘ndx), · ⟩} ∧ Fun
{⟨(*𝑟‘ndx), ∗⟩}) |
18 | 7, 8, 9 | dmtpop 6171 |
. . . . . . 7
⊢ dom
{⟨(Base‘ndx), ℂ⟩, ⟨(+g‘ndx), +
⟩, ⟨(.r‘ndx), · ⟩} = {(Base‘ndx),
(+g‘ndx), (.r‘ndx)} |
19 | 15 | dmsnop 6169 |
. . . . . . 7
⊢ dom
{⟨(*𝑟‘ndx), ∗⟩} =
{(*𝑟‘ndx)} |
20 | 18, 19 | ineq12i 4171 |
. . . . . 6
⊢ (dom
{⟨(Base‘ndx), ℂ⟩, ⟨(+g‘ndx), +
⟩, ⟨(.r‘ndx), · ⟩} ∩ dom
{⟨(*𝑟‘ndx), ∗⟩}) =
({(Base‘ndx), (+g‘ndx), (.r‘ndx)} ∩
{(*𝑟‘ndx)}) |
21 | | starvndxnbasendx 17186 |
. . . . . . . 8
⊢
(*𝑟‘ndx) ≠ (Base‘ndx) |
22 | 21 | necomi 2999 |
. . . . . . 7
⊢
(Base‘ndx) ≠ (*𝑟‘ndx) |
23 | | starvndxnplusgndx 17187 |
. . . . . . . 8
⊢
(*𝑟‘ndx) ≠
(+g‘ndx) |
24 | 23 | necomi 2999 |
. . . . . . 7
⊢
(+g‘ndx) ≠
(*𝑟‘ndx) |
25 | | starvndxnmulrndx 17188 |
. . . . . . . 8
⊢
(*𝑟‘ndx) ≠
(.r‘ndx) |
26 | 25 | necomi 2999 |
. . . . . . 7
⊢
(.r‘ndx) ≠
(*𝑟‘ndx) |
27 | | disjtpsn 4677 |
. . . . . . 7
⊢
(((Base‘ndx) ≠ (*𝑟‘ndx) ∧
(+g‘ndx) ≠ (*𝑟‘ndx) ∧
(.r‘ndx) ≠ (*𝑟‘ndx)) →
({(Base‘ndx), (+g‘ndx), (.r‘ndx)} ∩
{(*𝑟‘ndx)}) = ∅) |
28 | 22, 24, 26, 27 | mp3an 1462 |
. . . . . 6
⊢
({(Base‘ndx), (+g‘ndx),
(.r‘ndx)} ∩ {(*𝑟‘ndx)}) =
∅ |
29 | 20, 28 | eqtri 2765 |
. . . . 5
⊢ (dom
{⟨(Base‘ndx), ℂ⟩, ⟨(+g‘ndx), +
⟩, ⟨(.r‘ndx), · ⟩} ∩ dom
{⟨(*𝑟‘ndx), ∗⟩}) =
∅ |
30 | | funun 6548 |
. . . . 5
⊢ (((Fun
{⟨(Base‘ndx), ℂ⟩, ⟨(+g‘ndx), +
⟩, ⟨(.r‘ndx), · ⟩} ∧ Fun
{⟨(*𝑟‘ndx), ∗⟩}) ∧ (dom
{⟨(Base‘ndx), ℂ⟩, ⟨(+g‘ndx), +
⟩, ⟨(.r‘ndx), · ⟩} ∩ dom
{⟨(*𝑟‘ndx), ∗⟩}) = ∅) →
Fun ({⟨(Base‘ndx), ℂ⟩, ⟨(+g‘ndx), +
⟩, ⟨(.r‘ndx), · ⟩} ∪
{⟨(*𝑟‘ndx), ∗⟩})) |
31 | 17, 29, 30 | mp2an 691 |
. . . 4
⊢ Fun
({⟨(Base‘ndx), ℂ⟩, ⟨(+g‘ndx), +
⟩, ⟨(.r‘ndx), · ⟩} ∪
{⟨(*𝑟‘ndx), ∗⟩}) |
32 | | slotsdifplendx 17257 |
. . . . . . . 8
⊢
((*𝑟‘ndx) ≠ (le‘ndx) ∧
(TopSet‘ndx) ≠ (le‘ndx)) |
33 | 32 | simpri 487 |
. . . . . . 7
⊢
(TopSet‘ndx) ≠ (le‘ndx) |
34 | | dsndxntsetndx 17275 |
. . . . . . . 8
⊢
(dist‘ndx) ≠ (TopSet‘ndx) |
35 | 34 | necomi 2999 |
. . . . . . 7
⊢
(TopSet‘ndx) ≠ (dist‘ndx) |
36 | | slotsdifdsndx 17276 |
. . . . . . . 8
⊢
((*𝑟‘ndx) ≠ (dist‘ndx) ∧
(le‘ndx) ≠ (dist‘ndx)) |
37 | 36 | simpri 487 |
. . . . . . 7
⊢
(le‘ndx) ≠ (dist‘ndx) |
38 | | fvex 6856 |
. . . . . . . 8
⊢
(TopSet‘ndx) ∈ V |
39 | | fvex 6856 |
. . . . . . . 8
⊢
(le‘ndx) ∈ V |
40 | | fvex 6856 |
. . . . . . . 8
⊢
(dist‘ndx) ∈ V |
41 | | fvex 6856 |
. . . . . . . 8
⊢
(MetOpen‘(abs ∘ − )) ∈ V |
42 | | letsr 18483 |
. . . . . . . . 9
⊢ ≤
∈ TosetRel |
43 | 42 | elexi 3465 |
. . . . . . . 8
⊢ ≤
∈ V |
44 | | absf 15223 |
. . . . . . . . . 10
⊢
abs:ℂ⟶ℝ |
45 | | fex 7177 |
. . . . . . . . . 10
⊢
((abs:ℂ⟶ℝ ∧ ℂ ∈ V) → abs ∈
V) |
46 | 44, 7, 45 | mp2an 691 |
. . . . . . . . 9
⊢ abs
∈ V |
47 | | subf 11404 |
. . . . . . . . . 10
⊢ −
:(ℂ × ℂ)⟶ℂ |
48 | 7, 7 | xpex 7688 |
. . . . . . . . . 10
⊢ (ℂ
× ℂ) ∈ V |
49 | | fex 7177 |
. . . . . . . . . 10
⊢ ((
− :(ℂ × ℂ)⟶ℂ ∧ (ℂ ×
ℂ) ∈ V) → − ∈ V) |
50 | 47, 48, 49 | mp2an 691 |
. . . . . . . . 9
⊢ −
∈ V |
51 | 46, 50 | coex 7868 |
. . . . . . . 8
⊢ (abs
∘ − ) ∈ V |
52 | 38, 39, 40, 41, 43, 51 | funtp 6559 |
. . . . . . 7
⊢
(((TopSet‘ndx) ≠ (le‘ndx) ∧ (TopSet‘ndx) ≠
(dist‘ndx) ∧ (le‘ndx) ≠ (dist‘ndx)) → Fun
{⟨(TopSet‘ndx), (MetOpen‘(abs ∘ − ))⟩,
⟨(le‘ndx), ≤ ⟩, ⟨(dist‘ndx), (abs ∘ −
)⟩}) |
53 | 33, 35, 37, 52 | mp3an 1462 |
. . . . . 6
⊢ Fun
{⟨(TopSet‘ndx), (MetOpen‘(abs ∘ − ))⟩,
⟨(le‘ndx), ≤ ⟩, ⟨(dist‘ndx), (abs ∘ −
)⟩} |
54 | | fvex 6856 |
. . . . . . 7
⊢
(UnifSet‘ndx) ∈ V |
55 | | fvex 6856 |
. . . . . . 7
⊢
(metUnif‘(abs ∘ − )) ∈ V |
56 | 54, 55 | funsn 6555 |
. . . . . 6
⊢ Fun
{⟨(UnifSet‘ndx), (metUnif‘(abs ∘ −
))⟩} |
57 | 53, 56 | pm3.2i 472 |
. . . . 5
⊢ (Fun
{⟨(TopSet‘ndx), (MetOpen‘(abs ∘ − ))⟩,
⟨(le‘ndx), ≤ ⟩, ⟨(dist‘ndx), (abs ∘ −
)⟩} ∧ Fun {⟨(UnifSet‘ndx), (metUnif‘(abs ∘
− ))⟩}) |
58 | 41, 43, 51 | dmtpop 6171 |
. . . . . . 7
⊢ dom
{⟨(TopSet‘ndx), (MetOpen‘(abs ∘ − ))⟩,
⟨(le‘ndx), ≤ ⟩, ⟨(dist‘ndx), (abs ∘ −
)⟩} = {(TopSet‘ndx), (le‘ndx),
(dist‘ndx)} |
59 | 55 | dmsnop 6169 |
. . . . . . 7
⊢ dom
{⟨(UnifSet‘ndx), (metUnif‘(abs ∘ − ))⟩} =
{(UnifSet‘ndx)} |
60 | 58, 59 | ineq12i 4171 |
. . . . . 6
⊢ (dom
{⟨(TopSet‘ndx), (MetOpen‘(abs ∘ − ))⟩,
⟨(le‘ndx), ≤ ⟩, ⟨(dist‘ndx), (abs ∘ −
)⟩} ∩ dom {⟨(UnifSet‘ndx), (metUnif‘(abs ∘
− ))⟩}) = ({(TopSet‘ndx), (le‘ndx), (dist‘ndx)}
∩ {(UnifSet‘ndx)}) |
61 | | slotsdifunifndx 17283 |
. . . . . . . 8
⊢
(((+g‘ndx) ≠ (UnifSet‘ndx) ∧
(.r‘ndx) ≠ (UnifSet‘ndx) ∧
(*𝑟‘ndx) ≠ (UnifSet‘ndx)) ∧
((le‘ndx) ≠ (UnifSet‘ndx) ∧ (dist‘ndx) ≠
(UnifSet‘ndx))) |
62 | | unifndxntsetndx 17282 |
. . . . . . . . . . . 12
⊢
(UnifSet‘ndx) ≠ (TopSet‘ndx) |
63 | 62 | necomi 2999 |
. . . . . . . . . . 11
⊢
(TopSet‘ndx) ≠ (UnifSet‘ndx) |
64 | 63 | a1i 11 |
. . . . . . . . . 10
⊢
(((+g‘ndx) ≠ (UnifSet‘ndx) ∧
(.r‘ndx) ≠ (UnifSet‘ndx) ∧
(*𝑟‘ndx) ≠ (UnifSet‘ndx)) →
(TopSet‘ndx) ≠ (UnifSet‘ndx)) |
65 | 64 | anim1i 616 |
. . . . . . . . 9
⊢
((((+g‘ndx) ≠ (UnifSet‘ndx) ∧
(.r‘ndx) ≠ (UnifSet‘ndx) ∧
(*𝑟‘ndx) ≠ (UnifSet‘ndx)) ∧
((le‘ndx) ≠ (UnifSet‘ndx) ∧ (dist‘ndx) ≠
(UnifSet‘ndx))) → ((TopSet‘ndx) ≠ (UnifSet‘ndx) ∧
((le‘ndx) ≠ (UnifSet‘ndx) ∧ (dist‘ndx) ≠
(UnifSet‘ndx)))) |
66 | | 3anass 1096 |
. . . . . . . . 9
⊢
(((TopSet‘ndx) ≠ (UnifSet‘ndx) ∧ (le‘ndx) ≠
(UnifSet‘ndx) ∧ (dist‘ndx) ≠ (UnifSet‘ndx)) ↔
((TopSet‘ndx) ≠ (UnifSet‘ndx) ∧ ((le‘ndx) ≠
(UnifSet‘ndx) ∧ (dist‘ndx) ≠
(UnifSet‘ndx)))) |
67 | 65, 66 | sylibr 233 |
. . . . . . . 8
⊢
((((+g‘ndx) ≠ (UnifSet‘ndx) ∧
(.r‘ndx) ≠ (UnifSet‘ndx) ∧
(*𝑟‘ndx) ≠ (UnifSet‘ndx)) ∧
((le‘ndx) ≠ (UnifSet‘ndx) ∧ (dist‘ndx) ≠
(UnifSet‘ndx))) → ((TopSet‘ndx) ≠ (UnifSet‘ndx) ∧
(le‘ndx) ≠ (UnifSet‘ndx) ∧ (dist‘ndx) ≠
(UnifSet‘ndx))) |
68 | 61, 67 | ax-mp 5 |
. . . . . . 7
⊢
((TopSet‘ndx) ≠ (UnifSet‘ndx) ∧ (le‘ndx) ≠
(UnifSet‘ndx) ∧ (dist‘ndx) ≠
(UnifSet‘ndx)) |
69 | | disjtpsn 4677 |
. . . . . . 7
⊢
(((TopSet‘ndx) ≠ (UnifSet‘ndx) ∧ (le‘ndx) ≠
(UnifSet‘ndx) ∧ (dist‘ndx) ≠ (UnifSet‘ndx)) →
({(TopSet‘ndx), (le‘ndx), (dist‘ndx)} ∩
{(UnifSet‘ndx)}) = ∅) |
70 | 68, 69 | ax-mp 5 |
. . . . . 6
⊢
({(TopSet‘ndx), (le‘ndx), (dist‘ndx)} ∩
{(UnifSet‘ndx)}) = ∅ |
71 | 60, 70 | eqtri 2765 |
. . . . 5
⊢ (dom
{⟨(TopSet‘ndx), (MetOpen‘(abs ∘ − ))⟩,
⟨(le‘ndx), ≤ ⟩, ⟨(dist‘ndx), (abs ∘ −
)⟩} ∩ dom {⟨(UnifSet‘ndx), (metUnif‘(abs ∘
− ))⟩}) = ∅ |
72 | | funun 6548 |
. . . . 5
⊢ (((Fun
{⟨(TopSet‘ndx), (MetOpen‘(abs ∘ − ))⟩,
⟨(le‘ndx), ≤ ⟩, ⟨(dist‘ndx), (abs ∘ −
)⟩} ∧ Fun {⟨(UnifSet‘ndx), (metUnif‘(abs ∘
− ))⟩}) ∧ (dom {⟨(TopSet‘ndx), (MetOpen‘(abs
∘ − ))⟩, ⟨(le‘ndx), ≤ ⟩,
⟨(dist‘ndx), (abs ∘ − )⟩} ∩ dom
{⟨(UnifSet‘ndx), (metUnif‘(abs ∘ − ))⟩}) =
∅) → Fun ({⟨(TopSet‘ndx), (MetOpen‘(abs ∘
− ))⟩, ⟨(le‘ndx), ≤ ⟩, ⟨(dist‘ndx),
(abs ∘ − )⟩} ∪ {⟨(UnifSet‘ndx),
(metUnif‘(abs ∘ − ))⟩})) |
73 | 57, 71, 72 | mp2an 691 |
. . . 4
⊢ Fun
({⟨(TopSet‘ndx), (MetOpen‘(abs ∘ − ))⟩,
⟨(le‘ndx), ≤ ⟩, ⟨(dist‘ndx), (abs ∘ −
)⟩} ∪ {⟨(UnifSet‘ndx), (metUnif‘(abs ∘ −
))⟩}) |
74 | 31, 73 | pm3.2i 472 |
. . 3
⊢ (Fun
({⟨(Base‘ndx), ℂ⟩, ⟨(+g‘ndx), +
⟩, ⟨(.r‘ndx), · ⟩} ∪
{⟨(*𝑟‘ndx), ∗⟩}) ∧ Fun
({⟨(TopSet‘ndx), (MetOpen‘(abs ∘ − ))⟩,
⟨(le‘ndx), ≤ ⟩, ⟨(dist‘ndx), (abs ∘ −
)⟩} ∪ {⟨(UnifSet‘ndx), (metUnif‘(abs ∘ −
))⟩})) |
75 | | dmun 5867 |
. . . . 5
⊢ dom
({⟨(Base‘ndx), ℂ⟩, ⟨(+g‘ndx), +
⟩, ⟨(.r‘ndx), · ⟩} ∪
{⟨(*𝑟‘ndx), ∗⟩}) = (dom
{⟨(Base‘ndx), ℂ⟩, ⟨(+g‘ndx), +
⟩, ⟨(.r‘ndx), · ⟩} ∪ dom
{⟨(*𝑟‘ndx), ∗⟩}) |
76 | | dmun 5867 |
. . . . 5
⊢ dom
({⟨(TopSet‘ndx), (MetOpen‘(abs ∘ − ))⟩,
⟨(le‘ndx), ≤ ⟩, ⟨(dist‘ndx), (abs ∘ −
)⟩} ∪ {⟨(UnifSet‘ndx), (metUnif‘(abs ∘ −
))⟩}) = (dom {⟨(TopSet‘ndx), (MetOpen‘(abs ∘
− ))⟩, ⟨(le‘ndx), ≤ ⟩, ⟨(dist‘ndx),
(abs ∘ − )⟩} ∪ dom {⟨(UnifSet‘ndx),
(metUnif‘(abs ∘ − ))⟩}) |
77 | 75, 76 | ineq12i 4171 |
. . . 4
⊢ (dom
({⟨(Base‘ndx), ℂ⟩, ⟨(+g‘ndx), +
⟩, ⟨(.r‘ndx), · ⟩} ∪
{⟨(*𝑟‘ndx), ∗⟩}) ∩ dom
({⟨(TopSet‘ndx), (MetOpen‘(abs ∘ − ))⟩,
⟨(le‘ndx), ≤ ⟩, ⟨(dist‘ndx), (abs ∘ −
)⟩} ∪ {⟨(UnifSet‘ndx), (metUnif‘(abs ∘ −
))⟩})) = ((dom {⟨(Base‘ndx), ℂ⟩,
⟨(+g‘ndx), + ⟩, ⟨(.r‘ndx),
· ⟩} ∪ dom {⟨(*𝑟‘ndx),
∗⟩}) ∩ (dom {⟨(TopSet‘ndx), (MetOpen‘(abs
∘ − ))⟩, ⟨(le‘ndx), ≤ ⟩,
⟨(dist‘ndx), (abs ∘ − )⟩} ∪ dom
{⟨(UnifSet‘ndx), (metUnif‘(abs ∘ −
))⟩})) |
78 | 18, 58 | ineq12i 4171 |
. . . . . . . . 9
⊢ (dom
{⟨(Base‘ndx), ℂ⟩, ⟨(+g‘ndx), +
⟩, ⟨(.r‘ndx), · ⟩} ∩ dom
{⟨(TopSet‘ndx), (MetOpen‘(abs ∘ − ))⟩,
⟨(le‘ndx), ≤ ⟩, ⟨(dist‘ndx), (abs ∘ −
)⟩}) = ({(Base‘ndx), (+g‘ndx),
(.r‘ndx)} ∩ {(TopSet‘ndx), (le‘ndx),
(dist‘ndx)}) |
79 | | tsetndxnbasendx 17238 |
. . . . . . . . . . . 12
⊢
(TopSet‘ndx) ≠ (Base‘ndx) |
80 | 79 | necomi 2999 |
. . . . . . . . . . 11
⊢
(Base‘ndx) ≠ (TopSet‘ndx) |
81 | | tsetndxnplusgndx 17239 |
. . . . . . . . . . . 12
⊢
(TopSet‘ndx) ≠ (+g‘ndx) |
82 | 81 | necomi 2999 |
. . . . . . . . . . 11
⊢
(+g‘ndx) ≠ (TopSet‘ndx) |
83 | | tsetndxnmulrndx 17240 |
. . . . . . . . . . . 12
⊢
(TopSet‘ndx) ≠ (.r‘ndx) |
84 | 83 | necomi 2999 |
. . . . . . . . . . 11
⊢
(.r‘ndx) ≠ (TopSet‘ndx) |
85 | 80, 82, 84 | 3pm3.2i 1340 |
. . . . . . . . . 10
⊢
((Base‘ndx) ≠ (TopSet‘ndx) ∧
(+g‘ndx) ≠ (TopSet‘ndx) ∧
(.r‘ndx) ≠ (TopSet‘ndx)) |
86 | | plendxnbasendx 17252 |
. . . . . . . . . . . 12
⊢
(le‘ndx) ≠ (Base‘ndx) |
87 | 86 | necomi 2999 |
. . . . . . . . . . 11
⊢
(Base‘ndx) ≠ (le‘ndx) |
88 | | plendxnplusgndx 17253 |
. . . . . . . . . . . 12
⊢
(le‘ndx) ≠ (+g‘ndx) |
89 | 88 | necomi 2999 |
. . . . . . . . . . 11
⊢
(+g‘ndx) ≠ (le‘ndx) |
90 | | plendxnmulrndx 17254 |
. . . . . . . . . . . 12
⊢
(le‘ndx) ≠ (.r‘ndx) |
91 | 90 | necomi 2999 |
. . . . . . . . . . 11
⊢
(.r‘ndx) ≠ (le‘ndx) |
92 | 87, 89, 91 | 3pm3.2i 1340 |
. . . . . . . . . 10
⊢
((Base‘ndx) ≠ (le‘ndx) ∧ (+g‘ndx)
≠ (le‘ndx) ∧ (.r‘ndx) ≠
(le‘ndx)) |
93 | | dsndxnbasendx 17271 |
. . . . . . . . . . . 12
⊢
(dist‘ndx) ≠ (Base‘ndx) |
94 | 93 | necomi 2999 |
. . . . . . . . . . 11
⊢
(Base‘ndx) ≠ (dist‘ndx) |
95 | | dsndxnplusgndx 17272 |
. . . . . . . . . . . 12
⊢
(dist‘ndx) ≠ (+g‘ndx) |
96 | 95 | necomi 2999 |
. . . . . . . . . . 11
⊢
(+g‘ndx) ≠ (dist‘ndx) |
97 | | dsndxnmulrndx 17273 |
. . . . . . . . . . . 12
⊢
(dist‘ndx) ≠ (.r‘ndx) |
98 | 97 | necomi 2999 |
. . . . . . . . . . 11
⊢
(.r‘ndx) ≠ (dist‘ndx) |
99 | 94, 96, 98 | 3pm3.2i 1340 |
. . . . . . . . . 10
⊢
((Base‘ndx) ≠ (dist‘ndx) ∧ (+g‘ndx)
≠ (dist‘ndx) ∧ (.r‘ndx) ≠
(dist‘ndx)) |
100 | | disjtp2 4678 |
. . . . . . . . . 10
⊢
((((Base‘ndx) ≠ (TopSet‘ndx) ∧
(+g‘ndx) ≠ (TopSet‘ndx) ∧
(.r‘ndx) ≠ (TopSet‘ndx)) ∧ ((Base‘ndx) ≠
(le‘ndx) ∧ (+g‘ndx) ≠ (le‘ndx) ∧
(.r‘ndx) ≠ (le‘ndx)) ∧ ((Base‘ndx) ≠
(dist‘ndx) ∧ (+g‘ndx) ≠ (dist‘ndx) ∧
(.r‘ndx) ≠ (dist‘ndx))) → ({(Base‘ndx),
(+g‘ndx), (.r‘ndx)} ∩
{(TopSet‘ndx), (le‘ndx), (dist‘ndx)}) =
∅) |
101 | 85, 92, 99, 100 | mp3an 1462 |
. . . . . . . . 9
⊢
({(Base‘ndx), (+g‘ndx),
(.r‘ndx)} ∩ {(TopSet‘ndx), (le‘ndx),
(dist‘ndx)}) = ∅ |
102 | 78, 101 | eqtri 2765 |
. . . . . . . 8
⊢ (dom
{⟨(Base‘ndx), ℂ⟩, ⟨(+g‘ndx), +
⟩, ⟨(.r‘ndx), · ⟩} ∩ dom
{⟨(TopSet‘ndx), (MetOpen‘(abs ∘ − ))⟩,
⟨(le‘ndx), ≤ ⟩, ⟨(dist‘ndx), (abs ∘ −
)⟩}) = ∅ |
103 | 18, 59 | ineq12i 4171 |
. . . . . . . . 9
⊢ (dom
{⟨(Base‘ndx), ℂ⟩, ⟨(+g‘ndx), +
⟩, ⟨(.r‘ndx), · ⟩} ∩ dom
{⟨(UnifSet‘ndx), (metUnif‘(abs ∘ − ))⟩}) =
({(Base‘ndx), (+g‘ndx), (.r‘ndx)} ∩
{(UnifSet‘ndx)}) |
104 | | unifndxnbasendx 17281 |
. . . . . . . . . . . . . . 15
⊢
(UnifSet‘ndx) ≠ (Base‘ndx) |
105 | 104 | necomi 2999 |
. . . . . . . . . . . . . 14
⊢
(Base‘ndx) ≠ (UnifSet‘ndx) |
106 | 105 | a1i 11 |
. . . . . . . . . . . . 13
⊢
(((+g‘ndx) ≠ (UnifSet‘ndx) ∧
(.r‘ndx) ≠ (UnifSet‘ndx) ∧
(*𝑟‘ndx) ≠ (UnifSet‘ndx)) →
(Base‘ndx) ≠ (UnifSet‘ndx)) |
107 | | 3simpa 1149 |
. . . . . . . . . . . . 13
⊢
(((+g‘ndx) ≠ (UnifSet‘ndx) ∧
(.r‘ndx) ≠ (UnifSet‘ndx) ∧
(*𝑟‘ndx) ≠ (UnifSet‘ndx)) →
((+g‘ndx) ≠ (UnifSet‘ndx) ∧
(.r‘ndx) ≠ (UnifSet‘ndx))) |
108 | | 3anass 1096 |
. . . . . . . . . . . . 13
⊢
(((Base‘ndx) ≠ (UnifSet‘ndx) ∧
(+g‘ndx) ≠ (UnifSet‘ndx) ∧
(.r‘ndx) ≠ (UnifSet‘ndx)) ↔ ((Base‘ndx)
≠ (UnifSet‘ndx) ∧ ((+g‘ndx) ≠
(UnifSet‘ndx) ∧ (.r‘ndx) ≠
(UnifSet‘ndx)))) |
109 | 106, 107,
108 | sylanbrc 584 |
. . . . . . . . . . . 12
⊢
(((+g‘ndx) ≠ (UnifSet‘ndx) ∧
(.r‘ndx) ≠ (UnifSet‘ndx) ∧
(*𝑟‘ndx) ≠ (UnifSet‘ndx)) →
((Base‘ndx) ≠ (UnifSet‘ndx) ∧ (+g‘ndx) ≠
(UnifSet‘ndx) ∧ (.r‘ndx) ≠
(UnifSet‘ndx))) |
110 | 109 | adantr 482 |
. . . . . . . . . . 11
⊢
((((+g‘ndx) ≠ (UnifSet‘ndx) ∧
(.r‘ndx) ≠ (UnifSet‘ndx) ∧
(*𝑟‘ndx) ≠ (UnifSet‘ndx)) ∧
((le‘ndx) ≠ (UnifSet‘ndx) ∧ (dist‘ndx) ≠
(UnifSet‘ndx))) → ((Base‘ndx) ≠ (UnifSet‘ndx) ∧
(+g‘ndx) ≠ (UnifSet‘ndx) ∧
(.r‘ndx) ≠ (UnifSet‘ndx))) |
111 | 61, 110 | ax-mp 5 |
. . . . . . . . . 10
⊢
((Base‘ndx) ≠ (UnifSet‘ndx) ∧
(+g‘ndx) ≠ (UnifSet‘ndx) ∧
(.r‘ndx) ≠ (UnifSet‘ndx)) |
112 | | disjtpsn 4677 |
. . . . . . . . . 10
⊢
(((Base‘ndx) ≠ (UnifSet‘ndx) ∧
(+g‘ndx) ≠ (UnifSet‘ndx) ∧
(.r‘ndx) ≠ (UnifSet‘ndx)) → ({(Base‘ndx),
(+g‘ndx), (.r‘ndx)} ∩
{(UnifSet‘ndx)}) = ∅) |
113 | 111, 112 | ax-mp 5 |
. . . . . . . . 9
⊢
({(Base‘ndx), (+g‘ndx),
(.r‘ndx)} ∩ {(UnifSet‘ndx)}) =
∅ |
114 | 103, 113 | eqtri 2765 |
. . . . . . . 8
⊢ (dom
{⟨(Base‘ndx), ℂ⟩, ⟨(+g‘ndx), +
⟩, ⟨(.r‘ndx), · ⟩} ∩ dom
{⟨(UnifSet‘ndx), (metUnif‘(abs ∘ − ))⟩}) =
∅ |
115 | 102, 114 | pm3.2i 472 |
. . . . . . 7
⊢ ((dom
{⟨(Base‘ndx), ℂ⟩, ⟨(+g‘ndx), +
⟩, ⟨(.r‘ndx), · ⟩} ∩ dom
{⟨(TopSet‘ndx), (MetOpen‘(abs ∘ − ))⟩,
⟨(le‘ndx), ≤ ⟩, ⟨(dist‘ndx), (abs ∘ −
)⟩}) = ∅ ∧ (dom {⟨(Base‘ndx), ℂ⟩,
⟨(+g‘ndx), + ⟩, ⟨(.r‘ndx),
· ⟩} ∩ dom {⟨(UnifSet‘ndx), (metUnif‘(abs
∘ − ))⟩}) = ∅) |
116 | | undisj2 4423 |
. . . . . . 7
⊢ (((dom
{⟨(Base‘ndx), ℂ⟩, ⟨(+g‘ndx), +
⟩, ⟨(.r‘ndx), · ⟩} ∩ dom
{⟨(TopSet‘ndx), (MetOpen‘(abs ∘ − ))⟩,
⟨(le‘ndx), ≤ ⟩, ⟨(dist‘ndx), (abs ∘ −
)⟩}) = ∅ ∧ (dom {⟨(Base‘ndx), ℂ⟩,
⟨(+g‘ndx), + ⟩, ⟨(.r‘ndx),
· ⟩} ∩ dom {⟨(UnifSet‘ndx), (metUnif‘(abs
∘ − ))⟩}) = ∅) ↔ (dom {⟨(Base‘ndx),
ℂ⟩, ⟨(+g‘ndx), + ⟩,
⟨(.r‘ndx), · ⟩} ∩ (dom
{⟨(TopSet‘ndx), (MetOpen‘(abs ∘ − ))⟩,
⟨(le‘ndx), ≤ ⟩, ⟨(dist‘ndx), (abs ∘ −
)⟩} ∪ dom {⟨(UnifSet‘ndx), (metUnif‘(abs ∘
− ))⟩})) = ∅) |
117 | 115, 116 | mpbi 229 |
. . . . . 6
⊢ (dom
{⟨(Base‘ndx), ℂ⟩, ⟨(+g‘ndx), +
⟩, ⟨(.r‘ndx), · ⟩} ∩ (dom
{⟨(TopSet‘ndx), (MetOpen‘(abs ∘ − ))⟩,
⟨(le‘ndx), ≤ ⟩, ⟨(dist‘ndx), (abs ∘ −
)⟩} ∪ dom {⟨(UnifSet‘ndx), (metUnif‘(abs ∘
− ))⟩})) = ∅ |
118 | 19, 58 | ineq12i 4171 |
. . . . . . . . 9
⊢ (dom
{⟨(*𝑟‘ndx), ∗⟩} ∩ dom
{⟨(TopSet‘ndx), (MetOpen‘(abs ∘ − ))⟩,
⟨(le‘ndx), ≤ ⟩, ⟨(dist‘ndx), (abs ∘ −
)⟩}) = ({(*𝑟‘ndx)} ∩ {(TopSet‘ndx),
(le‘ndx), (dist‘ndx)}) |
119 | | tsetndxnstarvndx 17241 |
. . . . . . . . . . 11
⊢
(TopSet‘ndx) ≠
(*𝑟‘ndx) |
120 | | necom 2998 |
. . . . . . . . . . . . . 14
⊢
((*𝑟‘ndx) ≠ (le‘ndx) ↔
(le‘ndx) ≠ (*𝑟‘ndx)) |
121 | 120 | biimpi 215 |
. . . . . . . . . . . . 13
⊢
((*𝑟‘ndx) ≠ (le‘ndx) →
(le‘ndx) ≠ (*𝑟‘ndx)) |
122 | 121 | adantr 482 |
. . . . . . . . . . . 12
⊢
(((*𝑟‘ndx) ≠ (le‘ndx) ∧
(TopSet‘ndx) ≠ (le‘ndx)) → (le‘ndx) ≠
(*𝑟‘ndx)) |
123 | 32, 122 | ax-mp 5 |
. . . . . . . . . . 11
⊢
(le‘ndx) ≠ (*𝑟‘ndx) |
124 | | necom 2998 |
. . . . . . . . . . . . . 14
⊢
((*𝑟‘ndx) ≠ (dist‘ndx) ↔
(dist‘ndx) ≠ (*𝑟‘ndx)) |
125 | 124 | biimpi 215 |
. . . . . . . . . . . . 13
⊢
((*𝑟‘ndx) ≠ (dist‘ndx) →
(dist‘ndx) ≠ (*𝑟‘ndx)) |
126 | 125 | adantr 482 |
. . . . . . . . . . . 12
⊢
(((*𝑟‘ndx) ≠ (dist‘ndx) ∧
(le‘ndx) ≠ (dist‘ndx)) → (dist‘ndx) ≠
(*𝑟‘ndx)) |
127 | 36, 126 | ax-mp 5 |
. . . . . . . . . . 11
⊢
(dist‘ndx) ≠ (*𝑟‘ndx) |
128 | | disjtpsn 4677 |
. . . . . . . . . . 11
⊢
(((TopSet‘ndx) ≠ (*𝑟‘ndx) ∧
(le‘ndx) ≠ (*𝑟‘ndx) ∧ (dist‘ndx)
≠ (*𝑟‘ndx)) → ({(TopSet‘ndx),
(le‘ndx), (dist‘ndx)} ∩ {(*𝑟‘ndx)}) =
∅) |
129 | 119, 123,
127, 128 | mp3an 1462 |
. . . . . . . . . 10
⊢
({(TopSet‘ndx), (le‘ndx), (dist‘ndx)} ∩
{(*𝑟‘ndx)}) = ∅ |
130 | 129 | ineqcomi 4164 |
. . . . . . . . 9
⊢
({(*𝑟‘ndx)} ∩ {(TopSet‘ndx),
(le‘ndx), (dist‘ndx)}) = ∅ |
131 | 118, 130 | eqtri 2765 |
. . . . . . . 8
⊢ (dom
{⟨(*𝑟‘ndx), ∗⟩} ∩ dom
{⟨(TopSet‘ndx), (MetOpen‘(abs ∘ − ))⟩,
⟨(le‘ndx), ≤ ⟩, ⟨(dist‘ndx), (abs ∘ −
)⟩}) = ∅ |
132 | 19, 59 | ineq12i 4171 |
. . . . . . . . 9
⊢ (dom
{⟨(*𝑟‘ndx), ∗⟩} ∩ dom
{⟨(UnifSet‘ndx), (metUnif‘(abs ∘ − ))⟩}) =
({(*𝑟‘ndx)} ∩
{(UnifSet‘ndx)}) |
133 | | simpl3 1194 |
. . . . . . . . . . 11
⊢
((((+g‘ndx) ≠ (UnifSet‘ndx) ∧
(.r‘ndx) ≠ (UnifSet‘ndx) ∧
(*𝑟‘ndx) ≠ (UnifSet‘ndx)) ∧
((le‘ndx) ≠ (UnifSet‘ndx) ∧ (dist‘ndx) ≠
(UnifSet‘ndx))) → (*𝑟‘ndx) ≠
(UnifSet‘ndx)) |
134 | 61, 133 | ax-mp 5 |
. . . . . . . . . 10
⊢
(*𝑟‘ndx) ≠
(UnifSet‘ndx) |
135 | | disjsn2 4674 |
. . . . . . . . . 10
⊢
((*𝑟‘ndx) ≠ (UnifSet‘ndx) →
({(*𝑟‘ndx)} ∩ {(UnifSet‘ndx)}) =
∅) |
136 | 134, 135 | ax-mp 5 |
. . . . . . . . 9
⊢
({(*𝑟‘ndx)} ∩ {(UnifSet‘ndx)}) =
∅ |
137 | 132, 136 | eqtri 2765 |
. . . . . . . 8
⊢ (dom
{⟨(*𝑟‘ndx), ∗⟩} ∩ dom
{⟨(UnifSet‘ndx), (metUnif‘(abs ∘ − ))⟩}) =
∅ |
138 | 131, 137 | pm3.2i 472 |
. . . . . . 7
⊢ ((dom
{⟨(*𝑟‘ndx), ∗⟩} ∩ dom
{⟨(TopSet‘ndx), (MetOpen‘(abs ∘ − ))⟩,
⟨(le‘ndx), ≤ ⟩, ⟨(dist‘ndx), (abs ∘ −
)⟩}) = ∅ ∧ (dom {⟨(*𝑟‘ndx),
∗⟩} ∩ dom {⟨(UnifSet‘ndx), (metUnif‘(abs
∘ − ))⟩}) = ∅) |
139 | | undisj2 4423 |
. . . . . . 7
⊢ (((dom
{⟨(*𝑟‘ndx), ∗⟩} ∩ dom
{⟨(TopSet‘ndx), (MetOpen‘(abs ∘ − ))⟩,
⟨(le‘ndx), ≤ ⟩, ⟨(dist‘ndx), (abs ∘ −
)⟩}) = ∅ ∧ (dom {⟨(*𝑟‘ndx),
∗⟩} ∩ dom {⟨(UnifSet‘ndx), (metUnif‘(abs
∘ − ))⟩}) = ∅) ↔ (dom
{⟨(*𝑟‘ndx), ∗⟩} ∩ (dom
{⟨(TopSet‘ndx), (MetOpen‘(abs ∘ − ))⟩,
⟨(le‘ndx), ≤ ⟩, ⟨(dist‘ndx), (abs ∘ −
)⟩} ∪ dom {⟨(UnifSet‘ndx), (metUnif‘(abs ∘
− ))⟩})) = ∅) |
140 | 138, 139 | mpbi 229 |
. . . . . 6
⊢ (dom
{⟨(*𝑟‘ndx), ∗⟩} ∩ (dom
{⟨(TopSet‘ndx), (MetOpen‘(abs ∘ − ))⟩,
⟨(le‘ndx), ≤ ⟩, ⟨(dist‘ndx), (abs ∘ −
)⟩} ∪ dom {⟨(UnifSet‘ndx), (metUnif‘(abs ∘
− ))⟩})) = ∅ |
141 | 117, 140 | pm3.2i 472 |
. . . . 5
⊢ ((dom
{⟨(Base‘ndx), ℂ⟩, ⟨(+g‘ndx), +
⟩, ⟨(.r‘ndx), · ⟩} ∩ (dom
{⟨(TopSet‘ndx), (MetOpen‘(abs ∘ − ))⟩,
⟨(le‘ndx), ≤ ⟩, ⟨(dist‘ndx), (abs ∘ −
)⟩} ∪ dom {⟨(UnifSet‘ndx), (metUnif‘(abs ∘
− ))⟩})) = ∅ ∧ (dom
{⟨(*𝑟‘ndx), ∗⟩} ∩ (dom
{⟨(TopSet‘ndx), (MetOpen‘(abs ∘ − ))⟩,
⟨(le‘ndx), ≤ ⟩, ⟨(dist‘ndx), (abs ∘ −
)⟩} ∪ dom {⟨(UnifSet‘ndx), (metUnif‘(abs ∘
− ))⟩})) = ∅) |
142 | | undisj1 4422 |
. . . . 5
⊢ (((dom
{⟨(Base‘ndx), ℂ⟩, ⟨(+g‘ndx), +
⟩, ⟨(.r‘ndx), · ⟩} ∩ (dom
{⟨(TopSet‘ndx), (MetOpen‘(abs ∘ − ))⟩,
⟨(le‘ndx), ≤ ⟩, ⟨(dist‘ndx), (abs ∘ −
)⟩} ∪ dom {⟨(UnifSet‘ndx), (metUnif‘(abs ∘
− ))⟩})) = ∅ ∧ (dom
{⟨(*𝑟‘ndx), ∗⟩} ∩ (dom
{⟨(TopSet‘ndx), (MetOpen‘(abs ∘ − ))⟩,
⟨(le‘ndx), ≤ ⟩, ⟨(dist‘ndx), (abs ∘ −
)⟩} ∪ dom {⟨(UnifSet‘ndx), (metUnif‘(abs ∘
− ))⟩})) = ∅) ↔ ((dom {⟨(Base‘ndx),
ℂ⟩, ⟨(+g‘ndx), + ⟩,
⟨(.r‘ndx), · ⟩} ∪ dom
{⟨(*𝑟‘ndx), ∗⟩}) ∩ (dom
{⟨(TopSet‘ndx), (MetOpen‘(abs ∘ − ))⟩,
⟨(le‘ndx), ≤ ⟩, ⟨(dist‘ndx), (abs ∘ −
)⟩} ∪ dom {⟨(UnifSet‘ndx), (metUnif‘(abs ∘
− ))⟩})) = ∅) |
143 | 141, 142 | mpbi 229 |
. . . 4
⊢ ((dom
{⟨(Base‘ndx), ℂ⟩, ⟨(+g‘ndx), +
⟩, ⟨(.r‘ndx), · ⟩} ∪ dom
{⟨(*𝑟‘ndx), ∗⟩}) ∩ (dom
{⟨(TopSet‘ndx), (MetOpen‘(abs ∘ − ))⟩,
⟨(le‘ndx), ≤ ⟩, ⟨(dist‘ndx), (abs ∘ −
)⟩} ∪ dom {⟨(UnifSet‘ndx), (metUnif‘(abs ∘
− ))⟩})) = ∅ |
144 | 77, 143 | eqtri 2765 |
. . 3
⊢ (dom
({⟨(Base‘ndx), ℂ⟩, ⟨(+g‘ndx), +
⟩, ⟨(.r‘ndx), · ⟩} ∪
{⟨(*𝑟‘ndx), ∗⟩}) ∩ dom
({⟨(TopSet‘ndx), (MetOpen‘(abs ∘ − ))⟩,
⟨(le‘ndx), ≤ ⟩, ⟨(dist‘ndx), (abs ∘ −
)⟩} ∪ {⟨(UnifSet‘ndx), (metUnif‘(abs ∘ −
))⟩})) = ∅ |
145 | | funun 6548 |
. . 3
⊢ (((Fun
({⟨(Base‘ndx), ℂ⟩, ⟨(+g‘ndx), +
⟩, ⟨(.r‘ndx), · ⟩} ∪
{⟨(*𝑟‘ndx), ∗⟩}) ∧ Fun
({⟨(TopSet‘ndx), (MetOpen‘(abs ∘ − ))⟩,
⟨(le‘ndx), ≤ ⟩, ⟨(dist‘ndx), (abs ∘ −
)⟩} ∪ {⟨(UnifSet‘ndx), (metUnif‘(abs ∘ −
))⟩})) ∧ (dom ({⟨(Base‘ndx), ℂ⟩,
⟨(+g‘ndx), + ⟩, ⟨(.r‘ndx),
· ⟩} ∪ {⟨(*𝑟‘ndx),
∗⟩}) ∩ dom ({⟨(TopSet‘ndx), (MetOpen‘(abs
∘ − ))⟩, ⟨(le‘ndx), ≤ ⟩,
⟨(dist‘ndx), (abs ∘ − )⟩} ∪
{⟨(UnifSet‘ndx), (metUnif‘(abs ∘ − ))⟩})) =
∅) → Fun (({⟨(Base‘ndx), ℂ⟩,
⟨(+g‘ndx), + ⟩, ⟨(.r‘ndx),
· ⟩} ∪ {⟨(*𝑟‘ndx),
∗⟩}) ∪ ({⟨(TopSet‘ndx), (MetOpen‘(abs ∘
− ))⟩, ⟨(le‘ndx), ≤ ⟩, ⟨(dist‘ndx),
(abs ∘ − )⟩} ∪ {⟨(UnifSet‘ndx),
(metUnif‘(abs ∘ − ))⟩}))) |
146 | 74, 144, 145 | mp2an 691 |
. 2
⊢ Fun
(({⟨(Base‘ndx), ℂ⟩, ⟨(+g‘ndx), +
⟩, ⟨(.r‘ndx), · ⟩} ∪
{⟨(*𝑟‘ndx), ∗⟩}) ∪
({⟨(TopSet‘ndx), (MetOpen‘(abs ∘ − ))⟩,
⟨(le‘ndx), ≤ ⟩, ⟨(dist‘ndx), (abs ∘ −
)⟩} ∪ {⟨(UnifSet‘ndx), (metUnif‘(abs ∘ −
))⟩})) |
147 | | df-cnfld 20800 |
. . 3
⊢
ℂfld = (({⟨(Base‘ndx), ℂ⟩,
⟨(+g‘ndx), + ⟩, ⟨(.r‘ndx),
· ⟩} ∪ {⟨(*𝑟‘ndx),
∗⟩}) ∪ ({⟨(TopSet‘ndx), (MetOpen‘(abs ∘
− ))⟩, ⟨(le‘ndx), ≤ ⟩, ⟨(dist‘ndx),
(abs ∘ − )⟩} ∪ {⟨(UnifSet‘ndx),
(metUnif‘(abs ∘ − ))⟩})) |
148 | 147 | funeqi 6523 |
. 2
⊢ (Fun
ℂfld ↔ Fun (({⟨(Base‘ndx), ℂ⟩,
⟨(+g‘ndx), + ⟩, ⟨(.r‘ndx),
· ⟩} ∪ {⟨(*𝑟‘ndx),
∗⟩}) ∪ ({⟨(TopSet‘ndx), (MetOpen‘(abs ∘
− ))⟩, ⟨(le‘ndx), ≤ ⟩, ⟨(dist‘ndx),
(abs ∘ − )⟩} ∪ {⟨(UnifSet‘ndx),
(metUnif‘(abs ∘ − ))⟩}))) |
149 | 146, 148 | mpbir 230 |
1
⊢ Fun
ℂfld |