Step | Hyp | Ref
| Expression |
1 | | basendxnplusgndx 17170 |
. . . . . . 7
⊢
(Base‘ndx) ≠ (+g‘ndx) |
2 | | basendxnmulrndx 17183 |
. . . . . . 7
⊢
(Base‘ndx) ≠ (.r‘ndx) |
3 | | plusgndxnmulrndx 17185 |
. . . . . . 7
⊢
(+g‘ndx) ≠
(.r‘ndx) |
4 | | fvex 6860 |
. . . . . . . 8
⊢
(Base‘ndx) ∈ V |
5 | | fvex 6860 |
. . . . . . . 8
⊢
(+g‘ndx) ∈ V |
6 | | fvex 6860 |
. . . . . . . 8
⊢
(.r‘ndx) ∈ V |
7 | | cnex 11139 |
. . . . . . . 8
⊢ ℂ
∈ V |
8 | | addex 12920 |
. . . . . . . 8
⊢ + ∈
V |
9 | | mulex 12921 |
. . . . . . . 8
⊢ ·
∈ V |
10 | 4, 5, 6, 7, 8, 9 | funtp 6563 |
. . . . . . 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 6860 |
. . . . . . 7
⊢
(*𝑟‘ndx) ∈ V |
13 | | cjf 14996 |
. . . . . . . 8
⊢
∗:ℂ⟶ℂ |
14 | | fex 7181 |
. . . . . . . 8
⊢
((∗:ℂ⟶ℂ ∧ ℂ ∈ V) →
∗ ∈ V) |
15 | 13, 7, 14 | mp2an 691 |
. . . . . . 7
⊢ ∗
∈ V |
16 | 12, 15 | funsn 6559 |
. . . . . 6
⊢ Fun
{⟨(*𝑟‘ndx), ∗⟩} |
17 | 11, 16 | pm3.2i 472 |
. . . . 5
⊢ (Fun
{⟨(Base‘ndx), ℂ⟩, ⟨(+g‘ndx), +
⟩, ⟨(.r‘ndx), · ⟩} ∧ Fun
{⟨(*𝑟‘ndx), ∗⟩}) |
18 | 7, 8, 9 | dmtpop 6175 |
. . . . . . 7
⊢ dom
{⟨(Base‘ndx), ℂ⟩, ⟨(+g‘ndx), +
⟩, ⟨(.r‘ndx), · ⟩} = {(Base‘ndx),
(+g‘ndx), (.r‘ndx)} |
19 | 15 | dmsnop 6173 |
. . . . . . 7
⊢ dom
{⟨(*𝑟‘ndx), ∗⟩} =
{(*𝑟‘ndx)} |
20 | 18, 19 | ineq12i 4175 |
. . . . . 6
⊢ (dom
{⟨(Base‘ndx), ℂ⟩, ⟨(+g‘ndx), +
⟩, ⟨(.r‘ndx), · ⟩} ∩ dom
{⟨(*𝑟‘ndx), ∗⟩}) =
({(Base‘ndx), (+g‘ndx), (.r‘ndx)} ∩
{(*𝑟‘ndx)}) |
21 | | basendx 17099 |
. . . . . . . 8
⊢
(Base‘ndx) = 1 |
22 | | 1re 11162 |
. . . . . . . . . 10
⊢ 1 ∈
ℝ |
23 | | 1lt4 12336 |
. . . . . . . . . 10
⊢ 1 <
4 |
24 | 22, 23 | ltneii 11275 |
. . . . . . . . 9
⊢ 1 ≠
4 |
25 | | starvndx 17190 |
. . . . . . . . 9
⊢
(*𝑟‘ndx) = 4 |
26 | 24, 25 | neeqtrri 3018 |
. . . . . . . 8
⊢ 1 ≠
(*𝑟‘ndx) |
27 | 21, 26 | eqnetri 3015 |
. . . . . . 7
⊢
(Base‘ndx) ≠ (*𝑟‘ndx) |
28 | | plusgndx 17166 |
. . . . . . . 8
⊢
(+g‘ndx) = 2 |
29 | | 2re 12234 |
. . . . . . . . . 10
⊢ 2 ∈
ℝ |
30 | | 2lt4 12335 |
. . . . . . . . . 10
⊢ 2 <
4 |
31 | 29, 30 | ltneii 11275 |
. . . . . . . . 9
⊢ 2 ≠
4 |
32 | 31, 25 | neeqtrri 3018 |
. . . . . . . 8
⊢ 2 ≠
(*𝑟‘ndx) |
33 | 28, 32 | eqnetri 3015 |
. . . . . . 7
⊢
(+g‘ndx) ≠
(*𝑟‘ndx) |
34 | | mulrndx 17181 |
. . . . . . . 8
⊢
(.r‘ndx) = 3 |
35 | | 3re 12240 |
. . . . . . . . . 10
⊢ 3 ∈
ℝ |
36 | | 3lt4 12334 |
. . . . . . . . . 10
⊢ 3 <
4 |
37 | 35, 36 | ltneii 11275 |
. . . . . . . . 9
⊢ 3 ≠
4 |
38 | 37, 25 | neeqtrri 3018 |
. . . . . . . 8
⊢ 3 ≠
(*𝑟‘ndx) |
39 | 34, 38 | eqnetri 3015 |
. . . . . . 7
⊢
(.r‘ndx) ≠
(*𝑟‘ndx) |
40 | | disjtpsn 4681 |
. . . . . . 7
⊢
(((Base‘ndx) ≠ (*𝑟‘ndx) ∧
(+g‘ndx) ≠ (*𝑟‘ndx) ∧
(.r‘ndx) ≠ (*𝑟‘ndx)) →
({(Base‘ndx), (+g‘ndx), (.r‘ndx)} ∩
{(*𝑟‘ndx)}) = ∅) |
41 | 27, 33, 39, 40 | mp3an 1462 |
. . . . . 6
⊢
({(Base‘ndx), (+g‘ndx),
(.r‘ndx)} ∩ {(*𝑟‘ndx)}) =
∅ |
42 | 20, 41 | eqtri 2765 |
. . . . 5
⊢ (dom
{⟨(Base‘ndx), ℂ⟩, ⟨(+g‘ndx), +
⟩, ⟨(.r‘ndx), · ⟩} ∩ dom
{⟨(*𝑟‘ndx), ∗⟩}) =
∅ |
43 | | funun 6552 |
. . . . 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), ∗⟩})) |
44 | 17, 42, 43 | mp2an 691 |
. . . 4
⊢ Fun
({⟨(Base‘ndx), ℂ⟩, ⟨(+g‘ndx), +
⟩, ⟨(.r‘ndx), · ⟩} ∪
{⟨(*𝑟‘ndx), ∗⟩}) |
45 | | tsetndx 17240 |
. . . . . . . 8
⊢
(TopSet‘ndx) = 9 |
46 | | 9re 12259 |
. . . . . . . . . 10
⊢ 9 ∈
ℝ |
47 | | 9lt10 12756 |
. . . . . . . . . 10
⊢ 9 <
;10 |
48 | 46, 47 | ltneii 11275 |
. . . . . . . . 9
⊢ 9 ≠
;10 |
49 | | plendx 17254 |
. . . . . . . . 9
⊢
(le‘ndx) = ;10 |
50 | 48, 49 | neeqtrri 3018 |
. . . . . . . 8
⊢ 9 ≠
(le‘ndx) |
51 | 45, 50 | eqnetri 3015 |
. . . . . . 7
⊢
(TopSet‘ndx) ≠ (le‘ndx) |
52 | | 1nn 12171 |
. . . . . . . . . . 11
⊢ 1 ∈
ℕ |
53 | | 2nn0 12437 |
. . . . . . . . . . 11
⊢ 2 ∈
ℕ0 |
54 | | 9nn0 12444 |
. . . . . . . . . . 11
⊢ 9 ∈
ℕ0 |
55 | 46 | leidi 11696 |
. . . . . . . . . . 11
⊢ 9 ≤
9 |
56 | 52, 53, 54, 55 | decltdi 12664 |
. . . . . . . . . 10
⊢ 9 <
;12 |
57 | 46, 56 | ltneii 11275 |
. . . . . . . . 9
⊢ 9 ≠
;12 |
58 | | dsndx 17273 |
. . . . . . . . 9
⊢
(dist‘ndx) = ;12 |
59 | 57, 58 | neeqtrri 3018 |
. . . . . . . 8
⊢ 9 ≠
(dist‘ndx) |
60 | 45, 59 | eqnetri 3015 |
. . . . . . 7
⊢
(TopSet‘ndx) ≠ (dist‘ndx) |
61 | | 10re 12644 |
. . . . . . . . . 10
⊢ ;10 ∈ ℝ |
62 | | 1nn0 12436 |
. . . . . . . . . . 11
⊢ 1 ∈
ℕ0 |
63 | | 0nn0 12435 |
. . . . . . . . . . 11
⊢ 0 ∈
ℕ0 |
64 | | 2nn 12233 |
. . . . . . . . . . 11
⊢ 2 ∈
ℕ |
65 | | 2pos 12263 |
. . . . . . . . . . 11
⊢ 0 <
2 |
66 | 62, 63, 64, 65 | declt 12653 |
. . . . . . . . . 10
⊢ ;10 < ;12 |
67 | 61, 66 | ltneii 11275 |
. . . . . . . . 9
⊢ ;10 ≠ ;12 |
68 | 67, 58 | neeqtrri 3018 |
. . . . . . . 8
⊢ ;10 ≠
(dist‘ndx) |
69 | 49, 68 | eqnetri 3015 |
. . . . . . 7
⊢
(le‘ndx) ≠ (dist‘ndx) |
70 | | fvex 6860 |
. . . . . . . 8
⊢
(TopSet‘ndx) ∈ V |
71 | | fvex 6860 |
. . . . . . . 8
⊢
(le‘ndx) ∈ V |
72 | | fvex 6860 |
. . . . . . . 8
⊢
(dist‘ndx) ∈ V |
73 | | fvex 6860 |
. . . . . . . 8
⊢
(MetOpen‘(abs ∘ − )) ∈ V |
74 | | letsr 18489 |
. . . . . . . . 9
⊢ ≤
∈ TosetRel |
75 | 74 | elexi 3467 |
. . . . . . . 8
⊢ ≤
∈ V |
76 | | absf 15229 |
. . . . . . . . . 10
⊢
abs:ℂ⟶ℝ |
77 | | fex 7181 |
. . . . . . . . . 10
⊢
((abs:ℂ⟶ℝ ∧ ℂ ∈ V) → abs ∈
V) |
78 | 76, 7, 77 | mp2an 691 |
. . . . . . . . 9
⊢ abs
∈ V |
79 | | subf 11410 |
. . . . . . . . . 10
⊢ −
:(ℂ × ℂ)⟶ℂ |
80 | 7, 7 | xpex 7692 |
. . . . . . . . . 10
⊢ (ℂ
× ℂ) ∈ V |
81 | | fex 7181 |
. . . . . . . . . 10
⊢ ((
− :(ℂ × ℂ)⟶ℂ ∧ (ℂ ×
ℂ) ∈ V) → − ∈ V) |
82 | 79, 80, 81 | mp2an 691 |
. . . . . . . . 9
⊢ −
∈ V |
83 | 78, 82 | coex 7872 |
. . . . . . . 8
⊢ (abs
∘ − ) ∈ V |
84 | 70, 71, 72, 73, 75, 83 | funtp 6563 |
. . . . . . 7
⊢
(((TopSet‘ndx) ≠ (le‘ndx) ∧ (TopSet‘ndx) ≠
(dist‘ndx) ∧ (le‘ndx) ≠ (dist‘ndx)) → Fun
{⟨(TopSet‘ndx), (MetOpen‘(abs ∘ − ))⟩,
⟨(le‘ndx), ≤ ⟩, ⟨(dist‘ndx), (abs ∘ −
)⟩}) |
85 | 51, 60, 69, 84 | mp3an 1462 |
. . . . . 6
⊢ Fun
{⟨(TopSet‘ndx), (MetOpen‘(abs ∘ − ))⟩,
⟨(le‘ndx), ≤ ⟩, ⟨(dist‘ndx), (abs ∘ −
)⟩} |
86 | | fvex 6860 |
. . . . . . 7
⊢
(UnifSet‘ndx) ∈ V |
87 | | fvex 6860 |
. . . . . . 7
⊢
(metUnif‘(abs ∘ − )) ∈ V |
88 | 86, 87 | funsn 6559 |
. . . . . 6
⊢ Fun
{⟨(UnifSet‘ndx), (metUnif‘(abs ∘ −
))⟩} |
89 | 85, 88 | pm3.2i 472 |
. . . . 5
⊢ (Fun
{⟨(TopSet‘ndx), (MetOpen‘(abs ∘ − ))⟩,
⟨(le‘ndx), ≤ ⟩, ⟨(dist‘ndx), (abs ∘ −
)⟩} ∧ Fun {⟨(UnifSet‘ndx), (metUnif‘(abs ∘
− ))⟩}) |
90 | 73, 75, 83 | dmtpop 6175 |
. . . . . . 7
⊢ dom
{⟨(TopSet‘ndx), (MetOpen‘(abs ∘ − ))⟩,
⟨(le‘ndx), ≤ ⟩, ⟨(dist‘ndx), (abs ∘ −
)⟩} = {(TopSet‘ndx), (le‘ndx),
(dist‘ndx)} |
91 | 87 | dmsnop 6173 |
. . . . . . 7
⊢ dom
{⟨(UnifSet‘ndx), (metUnif‘(abs ∘ − ))⟩} =
{(UnifSet‘ndx)} |
92 | 90, 91 | ineq12i 4175 |
. . . . . 6
⊢ (dom
{⟨(TopSet‘ndx), (MetOpen‘(abs ∘ − ))⟩,
⟨(le‘ndx), ≤ ⟩, ⟨(dist‘ndx), (abs ∘ −
)⟩} ∩ dom {⟨(UnifSet‘ndx), (metUnif‘(abs ∘
− ))⟩}) = ({(TopSet‘ndx), (le‘ndx), (dist‘ndx)}
∩ {(UnifSet‘ndx)}) |
93 | | 3nn0 12438 |
. . . . . . . . . . 11
⊢ 3 ∈
ℕ0 |
94 | 52, 93, 54, 55 | decltdi 12664 |
. . . . . . . . . 10
⊢ 9 <
;13 |
95 | 46, 94 | ltneii 11275 |
. . . . . . . . 9
⊢ 9 ≠
;13 |
96 | | unifndx 17283 |
. . . . . . . . 9
⊢
(UnifSet‘ndx) = ;13 |
97 | 95, 96 | neeqtrri 3018 |
. . . . . . . 8
⊢ 9 ≠
(UnifSet‘ndx) |
98 | 45, 97 | eqnetri 3015 |
. . . . . . 7
⊢
(TopSet‘ndx) ≠ (UnifSet‘ndx) |
99 | | 3nn 12239 |
. . . . . . . . . . 11
⊢ 3 ∈
ℕ |
100 | | 3pos 12265 |
. . . . . . . . . . 11
⊢ 0 <
3 |
101 | 62, 63, 99, 100 | declt 12653 |
. . . . . . . . . 10
⊢ ;10 < ;13 |
102 | 61, 101 | ltneii 11275 |
. . . . . . . . 9
⊢ ;10 ≠ ;13 |
103 | 102, 96 | neeqtrri 3018 |
. . . . . . . 8
⊢ ;10 ≠
(UnifSet‘ndx) |
104 | 49, 103 | eqnetri 3015 |
. . . . . . 7
⊢
(le‘ndx) ≠ (UnifSet‘ndx) |
105 | 62, 53 | deccl 12640 |
. . . . . . . . . . 11
⊢ ;12 ∈
ℕ0 |
106 | 105 | nn0rei 12431 |
. . . . . . . . . 10
⊢ ;12 ∈ ℝ |
107 | | 2lt3 12332 |
. . . . . . . . . . 11
⊢ 2 <
3 |
108 | 62, 53, 99, 107 | declt 12653 |
. . . . . . . . . 10
⊢ ;12 < ;13 |
109 | 106, 108 | ltneii 11275 |
. . . . . . . . 9
⊢ ;12 ≠ ;13 |
110 | 109, 96 | neeqtrri 3018 |
. . . . . . . 8
⊢ ;12 ≠
(UnifSet‘ndx) |
111 | 58, 110 | eqnetri 3015 |
. . . . . . 7
⊢
(dist‘ndx) ≠ (UnifSet‘ndx) |
112 | | disjtpsn 4681 |
. . . . . . 7
⊢
(((TopSet‘ndx) ≠ (UnifSet‘ndx) ∧ (le‘ndx) ≠
(UnifSet‘ndx) ∧ (dist‘ndx) ≠ (UnifSet‘ndx)) →
({(TopSet‘ndx), (le‘ndx), (dist‘ndx)} ∩
{(UnifSet‘ndx)}) = ∅) |
113 | 98, 104, 111, 112 | mp3an 1462 |
. . . . . 6
⊢
({(TopSet‘ndx), (le‘ndx), (dist‘ndx)} ∩
{(UnifSet‘ndx)}) = ∅ |
114 | 92, 113 | eqtri 2765 |
. . . . 5
⊢ (dom
{⟨(TopSet‘ndx), (MetOpen‘(abs ∘ − ))⟩,
⟨(le‘ndx), ≤ ⟩, ⟨(dist‘ndx), (abs ∘ −
)⟩} ∩ dom {⟨(UnifSet‘ndx), (metUnif‘(abs ∘
− ))⟩}) = ∅ |
115 | | funun 6552 |
. . . . 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 ∘ − ))⟩})) |
116 | 89, 114, 115 | mp2an 691 |
. . . 4
⊢ Fun
({⟨(TopSet‘ndx), (MetOpen‘(abs ∘ − ))⟩,
⟨(le‘ndx), ≤ ⟩, ⟨(dist‘ndx), (abs ∘ −
)⟩} ∪ {⟨(UnifSet‘ndx), (metUnif‘(abs ∘ −
))⟩}) |
117 | 44, 116 | 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 ∘ −
))⟩})) |
118 | | dmun 5871 |
. . . . 5
⊢ dom
({⟨(Base‘ndx), ℂ⟩, ⟨(+g‘ndx), +
⟩, ⟨(.r‘ndx), · ⟩} ∪
{⟨(*𝑟‘ndx), ∗⟩}) = (dom
{⟨(Base‘ndx), ℂ⟩, ⟨(+g‘ndx), +
⟩, ⟨(.r‘ndx), · ⟩} ∪ dom
{⟨(*𝑟‘ndx), ∗⟩}) |
119 | | dmun 5871 |
. . . . 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 ∘ − ))⟩}) |
120 | 118, 119 | ineq12i 4175 |
. . . 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 ∘ −
))⟩})) |
121 | 18, 90 | ineq12i 4175 |
. . . . . . . . 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)}) |
122 | | 1lt9 12366 |
. . . . . . . . . . . . . 14
⊢ 1 <
9 |
123 | 22, 122 | ltneii 11275 |
. . . . . . . . . . . . 13
⊢ 1 ≠
9 |
124 | 123, 45 | neeqtrri 3018 |
. . . . . . . . . . . 12
⊢ 1 ≠
(TopSet‘ndx) |
125 | 21, 124 | eqnetri 3015 |
. . . . . . . . . . 11
⊢
(Base‘ndx) ≠ (TopSet‘ndx) |
126 | | 2lt9 12365 |
. . . . . . . . . . . . . 14
⊢ 2 <
9 |
127 | 29, 126 | ltneii 11275 |
. . . . . . . . . . . . 13
⊢ 2 ≠
9 |
128 | 127, 45 | neeqtrri 3018 |
. . . . . . . . . . . 12
⊢ 2 ≠
(TopSet‘ndx) |
129 | 28, 128 | eqnetri 3015 |
. . . . . . . . . . 11
⊢
(+g‘ndx) ≠ (TopSet‘ndx) |
130 | | 3lt9 12364 |
. . . . . . . . . . . . . 14
⊢ 3 <
9 |
131 | 35, 130 | ltneii 11275 |
. . . . . . . . . . . . 13
⊢ 3 ≠
9 |
132 | 131, 45 | neeqtrri 3018 |
. . . . . . . . . . . 12
⊢ 3 ≠
(TopSet‘ndx) |
133 | 34, 132 | eqnetri 3015 |
. . . . . . . . . . 11
⊢
(.r‘ndx) ≠ (TopSet‘ndx) |
134 | 125, 129,
133 | 3pm3.2i 1340 |
. . . . . . . . . 10
⊢
((Base‘ndx) ≠ (TopSet‘ndx) ∧
(+g‘ndx) ≠ (TopSet‘ndx) ∧
(.r‘ndx) ≠ (TopSet‘ndx)) |
135 | | 1lt10 12764 |
. . . . . . . . . . . . . 14
⊢ 1 <
;10 |
136 | 22, 135 | ltneii 11275 |
. . . . . . . . . . . . 13
⊢ 1 ≠
;10 |
137 | 136, 49 | neeqtrri 3018 |
. . . . . . . . . . . 12
⊢ 1 ≠
(le‘ndx) |
138 | 21, 137 | eqnetri 3015 |
. . . . . . . . . . 11
⊢
(Base‘ndx) ≠ (le‘ndx) |
139 | | 2lt10 12763 |
. . . . . . . . . . . . . 14
⊢ 2 <
;10 |
140 | 29, 139 | ltneii 11275 |
. . . . . . . . . . . . 13
⊢ 2 ≠
;10 |
141 | 140, 49 | neeqtrri 3018 |
. . . . . . . . . . . 12
⊢ 2 ≠
(le‘ndx) |
142 | 28, 141 | eqnetri 3015 |
. . . . . . . . . . 11
⊢
(+g‘ndx) ≠ (le‘ndx) |
143 | | 3lt10 12762 |
. . . . . . . . . . . . . 14
⊢ 3 <
;10 |
144 | 35, 143 | ltneii 11275 |
. . . . . . . . . . . . 13
⊢ 3 ≠
;10 |
145 | 144, 49 | neeqtrri 3018 |
. . . . . . . . . . . 12
⊢ 3 ≠
(le‘ndx) |
146 | 34, 145 | eqnetri 3015 |
. . . . . . . . . . 11
⊢
(.r‘ndx) ≠ (le‘ndx) |
147 | 138, 142,
146 | 3pm3.2i 1340 |
. . . . . . . . . 10
⊢
((Base‘ndx) ≠ (le‘ndx) ∧ (+g‘ndx)
≠ (le‘ndx) ∧ (.r‘ndx) ≠
(le‘ndx)) |
148 | 22, 46, 122 | ltleii 11285 |
. . . . . . . . . . . . . . 15
⊢ 1 ≤
9 |
149 | 52, 53, 62, 148 | decltdi 12664 |
. . . . . . . . . . . . . 14
⊢ 1 <
;12 |
150 | 22, 149 | ltneii 11275 |
. . . . . . . . . . . . 13
⊢ 1 ≠
;12 |
151 | 150, 58 | neeqtrri 3018 |
. . . . . . . . . . . 12
⊢ 1 ≠
(dist‘ndx) |
152 | 21, 151 | eqnetri 3015 |
. . . . . . . . . . 11
⊢
(Base‘ndx) ≠ (dist‘ndx) |
153 | 29, 46, 126 | ltleii 11285 |
. . . . . . . . . . . . . . 15
⊢ 2 ≤
9 |
154 | 52, 53, 53, 153 | decltdi 12664 |
. . . . . . . . . . . . . 14
⊢ 2 <
;12 |
155 | 29, 154 | ltneii 11275 |
. . . . . . . . . . . . 13
⊢ 2 ≠
;12 |
156 | 155, 58 | neeqtrri 3018 |
. . . . . . . . . . . 12
⊢ 2 ≠
(dist‘ndx) |
157 | 28, 156 | eqnetri 3015 |
. . . . . . . . . . 11
⊢
(+g‘ndx) ≠ (dist‘ndx) |
158 | 35, 46, 130 | ltleii 11285 |
. . . . . . . . . . . . . . 15
⊢ 3 ≤
9 |
159 | 52, 53, 93, 158 | decltdi 12664 |
. . . . . . . . . . . . . 14
⊢ 3 <
;12 |
160 | 35, 159 | ltneii 11275 |
. . . . . . . . . . . . 13
⊢ 3 ≠
;12 |
161 | 160, 58 | neeqtrri 3018 |
. . . . . . . . . . . 12
⊢ 3 ≠
(dist‘ndx) |
162 | 34, 161 | eqnetri 3015 |
. . . . . . . . . . 11
⊢
(.r‘ndx) ≠ (dist‘ndx) |
163 | 152, 157,
162 | 3pm3.2i 1340 |
. . . . . . . . . 10
⊢
((Base‘ndx) ≠ (dist‘ndx) ∧ (+g‘ndx)
≠ (dist‘ndx) ∧ (.r‘ndx) ≠
(dist‘ndx)) |
164 | | disjtp2 4682 |
. . . . . . . . . 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)}) =
∅) |
165 | 134, 147,
163, 164 | mp3an 1462 |
. . . . . . . . 9
⊢
({(Base‘ndx), (+g‘ndx),
(.r‘ndx)} ∩ {(TopSet‘ndx), (le‘ndx),
(dist‘ndx)}) = ∅ |
166 | 121, 165 | eqtri 2765 |
. . . . . . . 8
⊢ (dom
{⟨(Base‘ndx), ℂ⟩, ⟨(+g‘ndx), +
⟩, ⟨(.r‘ndx), · ⟩} ∩ dom
{⟨(TopSet‘ndx), (MetOpen‘(abs ∘ − ))⟩,
⟨(le‘ndx), ≤ ⟩, ⟨(dist‘ndx), (abs ∘ −
)⟩}) = ∅ |
167 | 18, 91 | ineq12i 4175 |
. . . . . . . . 9
⊢ (dom
{⟨(Base‘ndx), ℂ⟩, ⟨(+g‘ndx), +
⟩, ⟨(.r‘ndx), · ⟩} ∩ dom
{⟨(UnifSet‘ndx), (metUnif‘(abs ∘ − ))⟩}) =
({(Base‘ndx), (+g‘ndx), (.r‘ndx)} ∩
{(UnifSet‘ndx)}) |
168 | 52, 93, 62, 148 | decltdi 12664 |
. . . . . . . . . . . . 13
⊢ 1 <
;13 |
169 | 22, 168 | ltneii 11275 |
. . . . . . . . . . . 12
⊢ 1 ≠
;13 |
170 | 169, 96 | neeqtrri 3018 |
. . . . . . . . . . 11
⊢ 1 ≠
(UnifSet‘ndx) |
171 | 21, 170 | eqnetri 3015 |
. . . . . . . . . 10
⊢
(Base‘ndx) ≠ (UnifSet‘ndx) |
172 | 52, 93, 53, 153 | decltdi 12664 |
. . . . . . . . . . . . 13
⊢ 2 <
;13 |
173 | 29, 172 | ltneii 11275 |
. . . . . . . . . . . 12
⊢ 2 ≠
;13 |
174 | 173, 96 | neeqtrri 3018 |
. . . . . . . . . . 11
⊢ 2 ≠
(UnifSet‘ndx) |
175 | 28, 174 | eqnetri 3015 |
. . . . . . . . . 10
⊢
(+g‘ndx) ≠ (UnifSet‘ndx) |
176 | 52, 93, 93, 158 | decltdi 12664 |
. . . . . . . . . . . . 13
⊢ 3 <
;13 |
177 | 35, 176 | ltneii 11275 |
. . . . . . . . . . . 12
⊢ 3 ≠
;13 |
178 | 177, 96 | neeqtrri 3018 |
. . . . . . . . . . 11
⊢ 3 ≠
(UnifSet‘ndx) |
179 | 34, 178 | eqnetri 3015 |
. . . . . . . . . 10
⊢
(.r‘ndx) ≠ (UnifSet‘ndx) |
180 | | disjtpsn 4681 |
. . . . . . . . . 10
⊢
(((Base‘ndx) ≠ (UnifSet‘ndx) ∧
(+g‘ndx) ≠ (UnifSet‘ndx) ∧
(.r‘ndx) ≠ (UnifSet‘ndx)) → ({(Base‘ndx),
(+g‘ndx), (.r‘ndx)} ∩
{(UnifSet‘ndx)}) = ∅) |
181 | 171, 175,
179, 180 | mp3an 1462 |
. . . . . . . . 9
⊢
({(Base‘ndx), (+g‘ndx),
(.r‘ndx)} ∩ {(UnifSet‘ndx)}) =
∅ |
182 | 167, 181 | eqtri 2765 |
. . . . . . . 8
⊢ (dom
{⟨(Base‘ndx), ℂ⟩, ⟨(+g‘ndx), +
⟩, ⟨(.r‘ndx), · ⟩} ∩ dom
{⟨(UnifSet‘ndx), (metUnif‘(abs ∘ − ))⟩}) =
∅ |
183 | 166, 182 | 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
∘ − ))⟩}) = ∅) |
184 | | undisj2 4427 |
. . . . . . 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 ∘
− ))⟩})) = ∅) |
185 | 183, 184 | 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 ∘
− ))⟩})) = ∅ |
186 | 19, 90 | ineq12i 4175 |
. . . . . . . . 9
⊢ (dom
{⟨(*𝑟‘ndx), ∗⟩} ∩ dom
{⟨(TopSet‘ndx), (MetOpen‘(abs ∘ − ))⟩,
⟨(le‘ndx), ≤ ⟩, ⟨(dist‘ndx), (abs ∘ −
)⟩}) = ({(*𝑟‘ndx)} ∩ {(TopSet‘ndx),
(le‘ndx), (dist‘ndx)}) |
187 | | incom 4166 |
. . . . . . . . . 10
⊢
({(*𝑟‘ndx)} ∩ {(TopSet‘ndx),
(le‘ndx), (dist‘ndx)}) = ({(TopSet‘ndx), (le‘ndx),
(dist‘ndx)} ∩ {(*𝑟‘ndx)}) |
188 | | 4re 12244 |
. . . . . . . . . . . . . 14
⊢ 4 ∈
ℝ |
189 | | 4lt9 12363 |
. . . . . . . . . . . . . 14
⊢ 4 <
9 |
190 | 188, 189 | gtneii 11274 |
. . . . . . . . . . . . 13
⊢ 9 ≠
4 |
191 | 190, 25 | neeqtrri 3018 |
. . . . . . . . . . . 12
⊢ 9 ≠
(*𝑟‘ndx) |
192 | 45, 191 | eqnetri 3015 |
. . . . . . . . . . 11
⊢
(TopSet‘ndx) ≠
(*𝑟‘ndx) |
193 | | 4lt10 12761 |
. . . . . . . . . . . . . 14
⊢ 4 <
;10 |
194 | 188, 193 | gtneii 11274 |
. . . . . . . . . . . . 13
⊢ ;10 ≠ 4 |
195 | 194, 25 | neeqtrri 3018 |
. . . . . . . . . . . 12
⊢ ;10 ≠
(*𝑟‘ndx) |
196 | 49, 195 | eqnetri 3015 |
. . . . . . . . . . 11
⊢
(le‘ndx) ≠ (*𝑟‘ndx) |
197 | | 4nn0 12439 |
. . . . . . . . . . . . . . 15
⊢ 4 ∈
ℕ0 |
198 | 188, 46, 189 | ltleii 11285 |
. . . . . . . . . . . . . . 15
⊢ 4 ≤
9 |
199 | 52, 53, 197, 198 | decltdi 12664 |
. . . . . . . . . . . . . 14
⊢ 4 <
;12 |
200 | 188, 199 | gtneii 11274 |
. . . . . . . . . . . . 13
⊢ ;12 ≠ 4 |
201 | 200, 25 | neeqtrri 3018 |
. . . . . . . . . . . 12
⊢ ;12 ≠
(*𝑟‘ndx) |
202 | 58, 201 | eqnetri 3015 |
. . . . . . . . . . 11
⊢
(dist‘ndx) ≠ (*𝑟‘ndx) |
203 | | disjtpsn 4681 |
. . . . . . . . . . 11
⊢
(((TopSet‘ndx) ≠ (*𝑟‘ndx) ∧
(le‘ndx) ≠ (*𝑟‘ndx) ∧ (dist‘ndx)
≠ (*𝑟‘ndx)) → ({(TopSet‘ndx),
(le‘ndx), (dist‘ndx)} ∩ {(*𝑟‘ndx)}) =
∅) |
204 | 192, 196,
202, 203 | mp3an 1462 |
. . . . . . . . . 10
⊢
({(TopSet‘ndx), (le‘ndx), (dist‘ndx)} ∩
{(*𝑟‘ndx)}) = ∅ |
205 | 187, 204 | eqtri 2765 |
. . . . . . . . 9
⊢
({(*𝑟‘ndx)} ∩ {(TopSet‘ndx),
(le‘ndx), (dist‘ndx)}) = ∅ |
206 | 186, 205 | eqtri 2765 |
. . . . . . . 8
⊢ (dom
{⟨(*𝑟‘ndx), ∗⟩} ∩ dom
{⟨(TopSet‘ndx), (MetOpen‘(abs ∘ − ))⟩,
⟨(le‘ndx), ≤ ⟩, ⟨(dist‘ndx), (abs ∘ −
)⟩}) = ∅ |
207 | 19, 91 | ineq12i 4175 |
. . . . . . . . 9
⊢ (dom
{⟨(*𝑟‘ndx), ∗⟩} ∩ dom
{⟨(UnifSet‘ndx), (metUnif‘(abs ∘ − ))⟩}) =
({(*𝑟‘ndx)} ∩
{(UnifSet‘ndx)}) |
208 | 52, 93, 197, 198 | decltdi 12664 |
. . . . . . . . . . . . 13
⊢ 4 <
;13 |
209 | 188, 208 | ltneii 11275 |
. . . . . . . . . . . 12
⊢ 4 ≠
;13 |
210 | 209, 96 | neeqtrri 3018 |
. . . . . . . . . . 11
⊢ 4 ≠
(UnifSet‘ndx) |
211 | 25, 210 | eqnetri 3015 |
. . . . . . . . . 10
⊢
(*𝑟‘ndx) ≠
(UnifSet‘ndx) |
212 | | disjsn2 4678 |
. . . . . . . . . 10
⊢
((*𝑟‘ndx) ≠ (UnifSet‘ndx) →
({(*𝑟‘ndx)} ∩ {(UnifSet‘ndx)}) =
∅) |
213 | 211, 212 | ax-mp 5 |
. . . . . . . . 9
⊢
({(*𝑟‘ndx)} ∩ {(UnifSet‘ndx)}) =
∅ |
214 | 207, 213 | eqtri 2765 |
. . . . . . . 8
⊢ (dom
{⟨(*𝑟‘ndx), ∗⟩} ∩ dom
{⟨(UnifSet‘ndx), (metUnif‘(abs ∘ − ))⟩}) =
∅ |
215 | 206, 214 | pm3.2i 472 |
. . . . . . 7
⊢ ((dom
{⟨(*𝑟‘ndx), ∗⟩} ∩ dom
{⟨(TopSet‘ndx), (MetOpen‘(abs ∘ − ))⟩,
⟨(le‘ndx), ≤ ⟩, ⟨(dist‘ndx), (abs ∘ −
)⟩}) = ∅ ∧ (dom {⟨(*𝑟‘ndx),
∗⟩} ∩ dom {⟨(UnifSet‘ndx), (metUnif‘(abs
∘ − ))⟩}) = ∅) |
216 | | undisj2 4427 |
. . . . . . 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 ∘
− ))⟩})) = ∅) |
217 | 215, 216 | mpbi 229 |
. . . . . 6
⊢ (dom
{⟨(*𝑟‘ndx), ∗⟩} ∩ (dom
{⟨(TopSet‘ndx), (MetOpen‘(abs ∘ − ))⟩,
⟨(le‘ndx), ≤ ⟩, ⟨(dist‘ndx), (abs ∘ −
)⟩} ∪ dom {⟨(UnifSet‘ndx), (metUnif‘(abs ∘
− ))⟩})) = ∅ |
218 | 185, 217 | 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 ∘
− ))⟩})) = ∅) |
219 | | undisj1 4426 |
. . . . 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 ∘
− ))⟩})) = ∅) |
220 | 218, 219 | 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 ∘
− ))⟩})) = ∅ |
221 | 120, 220 | 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 ∘ −
))⟩})) = ∅ |
222 | | funun 6552 |
. . 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 ∘ − ))⟩}))) |
223 | 117, 221,
222 | mp2an 691 |
. 2
⊢ Fun
(({⟨(Base‘ndx), ℂ⟩, ⟨(+g‘ndx), +
⟩, ⟨(.r‘ndx), · ⟩} ∪
{⟨(*𝑟‘ndx), ∗⟩}) ∪
({⟨(TopSet‘ndx), (MetOpen‘(abs ∘ − ))⟩,
⟨(le‘ndx), ≤ ⟩, ⟨(dist‘ndx), (abs ∘ −
)⟩} ∪ {⟨(UnifSet‘ndx), (metUnif‘(abs ∘ −
))⟩})) |
224 | | df-cnfld 20813 |
. . 3
⊢
ℂfld = (({⟨(Base‘ndx), ℂ⟩,
⟨(+g‘ndx), + ⟩, ⟨(.r‘ndx),
· ⟩} ∪ {⟨(*𝑟‘ndx),
∗⟩}) ∪ ({⟨(TopSet‘ndx), (MetOpen‘(abs ∘
− ))⟩, ⟨(le‘ndx), ≤ ⟩, ⟨(dist‘ndx),
(abs ∘ − )⟩} ∪ {⟨(UnifSet‘ndx),
(metUnif‘(abs ∘ − ))⟩})) |
225 | 224 | funeqi 6527 |
. 2
⊢ (Fun
ℂfld ↔ Fun (({⟨(Base‘ndx), ℂ⟩,
⟨(+g‘ndx), + ⟩, ⟨(.r‘ndx),
· ⟩} ∪ {⟨(*𝑟‘ndx),
∗⟩}) ∪ ({⟨(TopSet‘ndx), (MetOpen‘(abs ∘
− ))⟩, ⟨(le‘ndx), ≤ ⟩, ⟨(dist‘ndx),
(abs ∘ − )⟩} ∪ {⟨(UnifSet‘ndx),
(metUnif‘(abs ∘ − ))⟩}))) |
226 | 223, 225 | mpbir 230 |
1
⊢ Fun
ℂfld |