Metamath Proof Explorer

Theorem cnfldfunALT

Description: The field of complex numbers is a function. Alternate proof of cnfldfun not requiring that the index set of the components is ordered, but using quadratically many inequalities for the indices. (Contributed by AV, 14-Nov-2021) (Proof shortened by AV, 11-Nov-2024) Revise df-cnfld . (Revised by GG, 31-Mar-2025) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Assertion cnfldfunALT Fun ℂfld

Proof

Step Hyp Ref Expression
1 basendxnplusgndx ⊢ ( Base ‘ ndx ) ≠ ( +g ‘ ndx )
2 basendxnmulrndx ⊢ ( Base ‘ ndx ) ≠ ( .r ‘ ndx )
3 plusgndxnmulrndx ⊢ ( +g ‘ ndx ) ≠ ( .r ‘ ndx )
4 fvex ⊢ ( Base ‘ ndx ) ∈ V
5 fvex ⊢ ( +g ‘ ndx ) ∈ V
6 fvex ⊢ ( .r ‘ ndx ) ∈ V
7 cnex ⊢ ℂ ∈ V
8 mpoaddex ⊢ ( 𝑢 ∈ ℂ , 𝑣 ∈ ℂ ↦ ( 𝑢 + 𝑣 ) ) ∈ V
9 mpomulex ⊢ ( 𝑢 ∈ ℂ , 𝑣 ∈ ℂ ↦ ( 𝑢 · 𝑣 ) ) ∈ V
10 4 5 6 7 8 9 funtp ⊢ ( ( ( 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 ⊢ Fun { ⟨ ( Base ‘ ndx ) , ℂ ⟩ , ⟨ ( +g ‘ ndx ) , ( 𝑢 ∈ ℂ , 𝑣 ∈ ℂ ↦ ( 𝑢 + 𝑣 ) ) ⟩ , ⟨ ( .r ‘ ndx ) , ( 𝑢 ∈ ℂ , 𝑣 ∈ ℂ ↦ ( 𝑢 · 𝑣 ) ) ⟩ }
12 fvex ⊢ ( *𝑟 ‘ ndx ) ∈ V
13 cjf ⊢ ∗ : ℂ ⟶ ℂ
14 fex ⊢ ( ( ∗ : ℂ ⟶ ℂ ∧ ℂ ∈ V ) → ∗ ∈ V )
15 13 7 14 mp2an ⊢ ∗ ∈ V
16 12 15 funsn ⊢ Fun { ⟨ ( *𝑟 ‘ ndx ) , ∗ ⟩ }
17 11 16 pm3.2i ⊢ ( Fun { ⟨ ( Base ‘ ndx ) , ℂ ⟩ , ⟨ ( +g ‘ ndx ) , ( 𝑢 ∈ ℂ , 𝑣 ∈ ℂ ↦ ( 𝑢 + 𝑣 ) ) ⟩ , ⟨ ( .r ‘ ndx ) , ( 𝑢 ∈ ℂ , 𝑣 ∈ ℂ ↦ ( 𝑢 · 𝑣 ) ) ⟩ } ∧ Fun { ⟨ ( *𝑟 ‘ ndx ) , ∗ ⟩ } )
18 7 8 9 dmtpop ⊢ dom { ⟨ ( Base ‘ ndx ) , ℂ ⟩ , ⟨ ( +g ‘ ndx ) , ( 𝑢 ∈ ℂ , 𝑣 ∈ ℂ ↦ ( 𝑢 + 𝑣 ) ) ⟩ , ⟨ ( .r ‘ ndx ) , ( 𝑢 ∈ ℂ , 𝑣 ∈ ℂ ↦ ( 𝑢 · 𝑣 ) ) ⟩ } = { ( Base ‘ ndx ) , ( +g ‘ ndx ) , ( .r ‘ ndx ) }
19 15 dmsnop ⊢ dom { ⟨ ( *𝑟 ‘ ndx ) , ∗ ⟩ } = { ( *𝑟 ‘ ndx ) }
20 18 19 ineq12i ⊢ ( dom { ⟨ ( Base ‘ ndx ) , ℂ ⟩ , ⟨ ( +g ‘ ndx ) , ( 𝑢 ∈ ℂ , 𝑣 ∈ ℂ ↦ ( 𝑢 + 𝑣 ) ) ⟩ , ⟨ ( .r ‘ ndx ) , ( 𝑢 ∈ ℂ , 𝑣 ∈ ℂ ↦ ( 𝑢 · 𝑣 ) ) ⟩ } ∩ dom { ⟨ ( *𝑟 ‘ ndx ) , ∗ ⟩ } ) = ( { ( Base ‘ ndx ) , ( +g ‘ ndx ) , ( .r ‘ ndx ) } ∩ { ( *𝑟 ‘ ndx ) } )
21 starvndxnbasendx ⊢ ( *𝑟 ‘ ndx ) ≠ ( Base ‘ ndx )
22 21 necomi ⊢ ( Base ‘ ndx ) ≠ ( *𝑟 ‘ ndx )
23 starvndxnplusgndx ⊢ ( *𝑟 ‘ ndx ) ≠ ( +g ‘ ndx )
24 23 necomi ⊢ ( +g ‘ ndx ) ≠ ( *𝑟 ‘ ndx )
25 starvndxnmulrndx ⊢ ( *𝑟 ‘ ndx ) ≠ ( .r ‘ ndx )
26 25 necomi ⊢ ( .r ‘ ndx ) ≠ ( *𝑟 ‘ ndx )
27 disjtpsn ⊢ ( ( ( Base ‘ ndx ) ≠ ( *𝑟 ‘ ndx ) ∧ ( +g ‘ ndx ) ≠ ( *𝑟 ‘ ndx ) ∧ ( .r ‘ ndx ) ≠ ( *𝑟 ‘ ndx ) ) → ( { ( Base ‘ ndx ) , ( +g ‘ ndx ) , ( .r ‘ ndx ) } ∩ { ( *𝑟 ‘ ndx ) } ) = ∅ )
28 22 24 26 27 mp3an ⊢ ( { ( Base ‘ ndx ) , ( +g ‘ ndx ) , ( .r ‘ ndx ) } ∩ { ( *𝑟 ‘ ndx ) } ) = ∅
29 20 28 eqtri ⊢ ( dom { ⟨ ( Base ‘ ndx ) , ℂ ⟩ , ⟨ ( +g ‘ ndx ) , ( 𝑢 ∈ ℂ , 𝑣 ∈ ℂ ↦ ( 𝑢 + 𝑣 ) ) ⟩ , ⟨ ( .r ‘ ndx ) , ( 𝑢 ∈ ℂ , 𝑣 ∈ ℂ ↦ ( 𝑢 · 𝑣 ) ) ⟩ } ∩ dom { ⟨ ( *𝑟 ‘ ndx ) , ∗ ⟩ } ) = ∅
30 funun ⊢ ( ( ( 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 ⊢ Fun ( { ⟨ ( Base ‘ ndx ) , ℂ ⟩ , ⟨ ( +g ‘ ndx ) , ( 𝑢 ∈ ℂ , 𝑣 ∈ ℂ ↦ ( 𝑢 + 𝑣 ) ) ⟩ , ⟨ ( .r ‘ ndx ) , ( 𝑢 ∈ ℂ , 𝑣 ∈ ℂ ↦ ( 𝑢 · 𝑣 ) ) ⟩ } ∪ { ⟨ ( *𝑟 ‘ ndx ) , ∗ ⟩ } )
32 slotsdifplendx ⊢ ( ( *𝑟 ‘ ndx ) ≠ ( le ‘ ndx ) ∧ ( TopSet ‘ ndx ) ≠ ( le ‘ ndx ) )
33 32 simpri ⊢ ( TopSet ‘ ndx ) ≠ ( le ‘ ndx )
34 dsndxntsetndx ⊢ ( dist ‘ ndx ) ≠ ( TopSet ‘ ndx )
35 34 necomi ⊢ ( TopSet ‘ ndx ) ≠ ( dist ‘ ndx )
36 slotsdifdsndx ⊢ ( ( *𝑟 ‘ ndx ) ≠ ( dist ‘ ndx ) ∧ ( le ‘ ndx ) ≠ ( dist ‘ ndx ) )
37 36 simpri ⊢ ( le ‘ ndx ) ≠ ( dist ‘ ndx )
38 fvex ⊢ ( TopSet ‘ ndx ) ∈ V
39 fvex ⊢ ( le ‘ ndx ) ∈ V
40 fvex ⊢ ( dist ‘ ndx ) ∈ V
41 fvex ⊢ ( MetOpen ‘ ( abs ∘ − ) ) ∈ V
42 letsr ⊢ ≤ ∈ TosetRel
43 42 elexi ⊢ ≤ ∈ V
44 absf ⊢ abs : ℂ ⟶ ℝ
45 fex ⊢ ( ( abs : ℂ ⟶ ℝ ∧ ℂ ∈ V ) → abs ∈ V )
46 44 7 45 mp2an ⊢ abs ∈ V
47 subf ⊢ − : ( ℂ × ℂ ) ⟶ ℂ
48 7 7 xpex ⊢ ( ℂ × ℂ ) ∈ V
49 fex ⊢ ( ( − : ( ℂ × ℂ ) ⟶ ℂ ∧ ( ℂ × ℂ ) ∈ V ) → − ∈ V )
50 47 48 49 mp2an ⊢ − ∈ V
51 46 50 coex ⊢ ( abs ∘ − ) ∈ V
52 38 39 40 41 43 51 funtp ⊢ ( ( ( 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 ⊢ Fun { ⟨ ( TopSet ‘ ndx ) , ( MetOpen ‘ ( abs ∘ − ) ) ⟩ , ⟨ ( le ‘ ndx ) , ≤ ⟩ , ⟨ ( dist ‘ ndx ) , ( abs ∘ − ) ⟩ }
54 fvex ⊢ ( UnifSet ‘ ndx ) ∈ V
55 fvex ⊢ ( metUnif ‘ ( abs ∘ − ) ) ∈ V
56 54 55 funsn ⊢ Fun { ⟨ ( UnifSet ‘ ndx ) , ( metUnif ‘ ( abs ∘ − ) ) ⟩ }
57 53 56 pm3.2i ⊢ ( Fun { ⟨ ( TopSet ‘ ndx ) , ( MetOpen ‘ ( abs ∘ − ) ) ⟩ , ⟨ ( le ‘ ndx ) , ≤ ⟩ , ⟨ ( dist ‘ ndx ) , ( abs ∘ − ) ⟩ } ∧ Fun { ⟨ ( UnifSet ‘ ndx ) , ( metUnif ‘ ( abs ∘ − ) ) ⟩ } )
58 41 43 51 dmtpop ⊢ dom { ⟨ ( TopSet ‘ ndx ) , ( MetOpen ‘ ( abs ∘ − ) ) ⟩ , ⟨ ( le ‘ ndx ) , ≤ ⟩ , ⟨ ( dist ‘ ndx ) , ( abs ∘ − ) ⟩ } = { ( TopSet ‘ ndx ) , ( le ‘ ndx ) , ( dist ‘ ndx ) }
59 55 dmsnop ⊢ dom { ⟨ ( UnifSet ‘ ndx ) , ( metUnif ‘ ( abs ∘ − ) ) ⟩ } = { ( UnifSet ‘ ndx ) }
60 58 59 ineq12i ⊢ ( 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 ⊢ ( ( ( +g ‘ ndx ) ≠ ( UnifSet ‘ ndx ) ∧ ( .r ‘ ndx ) ≠ ( UnifSet ‘ ndx ) ∧ ( *𝑟 ‘ ndx ) ≠ ( UnifSet ‘ ndx ) ) ∧ ( ( le ‘ ndx ) ≠ ( UnifSet ‘ ndx ) ∧ ( dist ‘ ndx ) ≠ ( UnifSet ‘ ndx ) ) )
62 unifndxntsetndx ⊢ ( UnifSet ‘ ndx ) ≠ ( TopSet ‘ ndx )
63 62 necomi ⊢ ( TopSet ‘ ndx ) ≠ ( UnifSet ‘ ndx )
64 63 a1i ⊢ ( ( ( +g ‘ ndx ) ≠ ( UnifSet ‘ ndx ) ∧ ( .r ‘ ndx ) ≠ ( UnifSet ‘ ndx ) ∧ ( *𝑟 ‘ ndx ) ≠ ( UnifSet ‘ ndx ) ) → ( TopSet ‘ ndx ) ≠ ( UnifSet ‘ ndx ) )
65 64 anim1i ⊢ ( ( ( ( +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 ⊢ ( ( ( 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 ⊢ ( ( ( ( +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 ⊢ ( ( TopSet ‘ ndx ) ≠ ( UnifSet ‘ ndx ) ∧ ( le ‘ ndx ) ≠ ( UnifSet ‘ ndx ) ∧ ( dist ‘ ndx ) ≠ ( UnifSet ‘ ndx ) )
69 disjtpsn ⊢ ( ( ( 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 ⊢ ( { ( TopSet ‘ ndx ) , ( le ‘ ndx ) , ( dist ‘ ndx ) } ∩ { ( UnifSet ‘ ndx ) } ) = ∅
71 60 70 eqtri ⊢ ( dom { ⟨ ( TopSet ‘ ndx ) , ( MetOpen ‘ ( abs ∘ − ) ) ⟩ , ⟨ ( le ‘ ndx ) , ≤ ⟩ , ⟨ ( dist ‘ ndx ) , ( abs ∘ − ) ⟩ } ∩ dom { ⟨ ( UnifSet ‘ ndx ) , ( metUnif ‘ ( abs ∘ − ) ) ⟩ } ) = ∅
72 funun ⊢ ( ( ( 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 ⊢ Fun ( { ⟨ ( TopSet ‘ ndx ) , ( MetOpen ‘ ( abs ∘ − ) ) ⟩ , ⟨ ( le ‘ ndx ) , ≤ ⟩ , ⟨ ( dist ‘ ndx ) , ( abs ∘ − ) ⟩ } ∪ { ⟨ ( UnifSet ‘ ndx ) , ( metUnif ‘ ( abs ∘ − ) ) ⟩ } )
74 31 73 pm3.2i ⊢ ( Fun ( { ⟨ ( Base ‘ ndx ) , ℂ ⟩ , ⟨ ( +g ‘ ndx ) , ( 𝑢 ∈ ℂ , 𝑣 ∈ ℂ ↦ ( 𝑢 + 𝑣 ) ) ⟩ , ⟨ ( .r ‘ ndx ) , ( 𝑢 ∈ ℂ , 𝑣 ∈ ℂ ↦ ( 𝑢 · 𝑣 ) ) ⟩ } ∪ { ⟨ ( *𝑟 ‘ ndx ) , ∗ ⟩ } ) ∧ Fun ( { ⟨ ( TopSet ‘ ndx ) , ( MetOpen ‘ ( abs ∘ − ) ) ⟩ , ⟨ ( le ‘ ndx ) , ≤ ⟩ , ⟨ ( dist ‘ ndx ) , ( abs ∘ − ) ⟩ } ∪ { ⟨ ( UnifSet ‘ ndx ) , ( metUnif ‘ ( abs ∘ − ) ) ⟩ } ) )
75 dmun ⊢ dom ( { ⟨ ( Base ‘ ndx ) , ℂ ⟩ , ⟨ ( +g ‘ ndx ) , ( 𝑢 ∈ ℂ , 𝑣 ∈ ℂ ↦ ( 𝑢 + 𝑣 ) ) ⟩ , ⟨ ( .r ‘ ndx ) , ( 𝑢 ∈ ℂ , 𝑣 ∈ ℂ ↦ ( 𝑢 · 𝑣 ) ) ⟩ } ∪ { ⟨ ( *𝑟 ‘ ndx ) , ∗ ⟩ } ) = ( dom { ⟨ ( Base ‘ ndx ) , ℂ ⟩ , ⟨ ( +g ‘ ndx ) , ( 𝑢 ∈ ℂ , 𝑣 ∈ ℂ ↦ ( 𝑢 + 𝑣 ) ) ⟩ , ⟨ ( .r ‘ ndx ) , ( 𝑢 ∈ ℂ , 𝑣 ∈ ℂ ↦ ( 𝑢 · 𝑣 ) ) ⟩ } ∪ dom { ⟨ ( *𝑟 ‘ ndx ) , ∗ ⟩ } )
76 dmun ⊢ 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 ⊢ ( 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 ⊢ ( 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 ⊢ ( TopSet ‘ ndx ) ≠ ( Base ‘ ndx )
80 79 necomi ⊢ ( Base ‘ ndx ) ≠ ( TopSet ‘ ndx )
81 tsetndxnplusgndx ⊢ ( TopSet ‘ ndx ) ≠ ( +g ‘ ndx )
82 81 necomi ⊢ ( +g ‘ ndx ) ≠ ( TopSet ‘ ndx )
83 tsetndxnmulrndx ⊢ ( TopSet ‘ ndx ) ≠ ( .r ‘ ndx )
84 83 necomi ⊢ ( .r ‘ ndx ) ≠ ( TopSet ‘ ndx )
85 80 82 84 3pm3.2i ⊢ ( ( Base ‘ ndx ) ≠ ( TopSet ‘ ndx ) ∧ ( +g ‘ ndx ) ≠ ( TopSet ‘ ndx ) ∧ ( .r ‘ ndx ) ≠ ( TopSet ‘ ndx ) )
86 plendxnbasendx ⊢ ( le ‘ ndx ) ≠ ( Base ‘ ndx )
87 86 necomi ⊢ ( Base ‘ ndx ) ≠ ( le ‘ ndx )
88 plendxnplusgndx ⊢ ( le ‘ ndx ) ≠ ( +g ‘ ndx )
89 88 necomi ⊢ ( +g ‘ ndx ) ≠ ( le ‘ ndx )
90 plendxnmulrndx ⊢ ( le ‘ ndx ) ≠ ( .r ‘ ndx )
91 90 necomi ⊢ ( .r ‘ ndx ) ≠ ( le ‘ ndx )
92 87 89 91 3pm3.2i ⊢ ( ( Base ‘ ndx ) ≠ ( le ‘ ndx ) ∧ ( +g ‘ ndx ) ≠ ( le ‘ ndx ) ∧ ( .r ‘ ndx ) ≠ ( le ‘ ndx ) )
93 dsndxnbasendx ⊢ ( dist ‘ ndx ) ≠ ( Base ‘ ndx )
94 93 necomi ⊢ ( Base ‘ ndx ) ≠ ( dist ‘ ndx )
95 dsndxnplusgndx ⊢ ( dist ‘ ndx ) ≠ ( +g ‘ ndx )
96 95 necomi ⊢ ( +g ‘ ndx ) ≠ ( dist ‘ ndx )
97 dsndxnmulrndx ⊢ ( dist ‘ ndx ) ≠ ( .r ‘ ndx )
98 97 necomi ⊢ ( .r ‘ ndx ) ≠ ( dist ‘ ndx )
99 94 96 98 3pm3.2i ⊢ ( ( Base ‘ ndx ) ≠ ( dist ‘ ndx ) ∧ ( +g ‘ ndx ) ≠ ( dist ‘ ndx ) ∧ ( .r ‘ ndx ) ≠ ( dist ‘ ndx ) )
100 disjtp2 ⊢ ( ( ( ( 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 ⊢ ( { ( Base ‘ ndx ) , ( +g ‘ ndx ) , ( .r ‘ ndx ) } ∩ { ( TopSet ‘ ndx ) , ( le ‘ ndx ) , ( dist ‘ ndx ) } ) = ∅
102 78 101 eqtri ⊢ ( dom { ⟨ ( Base ‘ ndx ) , ℂ ⟩ , ⟨ ( +g ‘ ndx ) , ( 𝑢 ∈ ℂ , 𝑣 ∈ ℂ ↦ ( 𝑢 + 𝑣 ) ) ⟩ , ⟨ ( .r ‘ ndx ) , ( 𝑢 ∈ ℂ , 𝑣 ∈ ℂ ↦ ( 𝑢 · 𝑣 ) ) ⟩ } ∩ dom { ⟨ ( TopSet ‘ ndx ) , ( MetOpen ‘ ( abs ∘ − ) ) ⟩ , ⟨ ( le ‘ ndx ) , ≤ ⟩ , ⟨ ( dist ‘ ndx ) , ( abs ∘ − ) ⟩ } ) = ∅
103 18 59 ineq12i ⊢ ( dom { ⟨ ( Base ‘ ndx ) , ℂ ⟩ , ⟨ ( +g ‘ ndx ) , ( 𝑢 ∈ ℂ , 𝑣 ∈ ℂ ↦ ( 𝑢 + 𝑣 ) ) ⟩ , ⟨ ( .r ‘ ndx ) , ( 𝑢 ∈ ℂ , 𝑣 ∈ ℂ ↦ ( 𝑢 · 𝑣 ) ) ⟩ } ∩ dom { ⟨ ( UnifSet ‘ ndx ) , ( metUnif ‘ ( abs ∘ − ) ) ⟩ } ) = ( { ( Base ‘ ndx ) , ( +g ‘ ndx ) , ( .r ‘ ndx ) } ∩ { ( UnifSet ‘ ndx ) } )
104 unifndxnbasendx ⊢ ( UnifSet ‘ ndx ) ≠ ( Base ‘ ndx )
105 104 necomi ⊢ ( Base ‘ ndx ) ≠ ( UnifSet ‘ ndx )
106 105 a1i ⊢ ( ( ( +g ‘ ndx ) ≠ ( UnifSet ‘ ndx ) ∧ ( .r ‘ ndx ) ≠ ( UnifSet ‘ ndx ) ∧ ( *𝑟 ‘ ndx ) ≠ ( UnifSet ‘ ndx ) ) → ( Base ‘ ndx ) ≠ ( UnifSet ‘ ndx ) )
107 3simpa ⊢ ( ( ( +g ‘ ndx ) ≠ ( UnifSet ‘ ndx ) ∧ ( .r ‘ ndx ) ≠ ( UnifSet ‘ ndx ) ∧ ( *𝑟 ‘ ndx ) ≠ ( UnifSet ‘ ndx ) ) → ( ( +g ‘ ndx ) ≠ ( UnifSet ‘ ndx ) ∧ ( .r ‘ ndx ) ≠ ( UnifSet ‘ ndx ) ) )
108 3anass ⊢ ( ( ( 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 ⊢ ( ( ( +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 ⊢ ( ( ( ( +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 ⊢ ( ( Base ‘ ndx ) ≠ ( UnifSet ‘ ndx ) ∧ ( +g ‘ ndx ) ≠ ( UnifSet ‘ ndx ) ∧ ( .r ‘ ndx ) ≠ ( UnifSet ‘ ndx ) )
112 disjtpsn ⊢ ( ( ( 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 ⊢ ( { ( Base ‘ ndx ) , ( +g ‘ ndx ) , ( .r ‘ ndx ) } ∩ { ( UnifSet ‘ ndx ) } ) = ∅
114 103 113 eqtri ⊢ ( dom { ⟨ ( Base ‘ ndx ) , ℂ ⟩ , ⟨ ( +g ‘ ndx ) , ( 𝑢 ∈ ℂ , 𝑣 ∈ ℂ ↦ ( 𝑢 + 𝑣 ) ) ⟩ , ⟨ ( .r ‘ ndx ) , ( 𝑢 ∈ ℂ , 𝑣 ∈ ℂ ↦ ( 𝑢 · 𝑣 ) ) ⟩ } ∩ dom { ⟨ ( UnifSet ‘ ndx ) , ( metUnif ‘ ( abs ∘ − ) ) ⟩ } ) = ∅
115 102 114 pm3.2i ⊢ ( ( 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 ⊢ ( ( ( 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 ⊢ ( 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 ⊢ ( dom { ⟨ ( *𝑟 ‘ ndx ) , ∗ ⟩ } ∩ dom { ⟨ ( TopSet ‘ ndx ) , ( MetOpen ‘ ( abs ∘ − ) ) ⟩ , ⟨ ( le ‘ ndx ) , ≤ ⟩ , ⟨ ( dist ‘ ndx ) , ( abs ∘ − ) ⟩ } ) = ( { ( *𝑟 ‘ ndx ) } ∩ { ( TopSet ‘ ndx ) , ( le ‘ ndx ) , ( dist ‘ ndx ) } )
119 tsetndxnstarvndx ⊢ ( TopSet ‘ ndx ) ≠ ( *𝑟 ‘ ndx )
120 necom ⊢ ( ( *𝑟 ‘ ndx ) ≠ ( le ‘ ndx ) ↔ ( le ‘ ndx ) ≠ ( *𝑟 ‘ ndx ) )
121 120 biimpi ⊢ ( ( *𝑟 ‘ ndx ) ≠ ( le ‘ ndx ) → ( le ‘ ndx ) ≠ ( *𝑟 ‘ ndx ) )
122 121 adantr ⊢ ( ( ( *𝑟 ‘ ndx ) ≠ ( le ‘ ndx ) ∧ ( TopSet ‘ ndx ) ≠ ( le ‘ ndx ) ) → ( le ‘ ndx ) ≠ ( *𝑟 ‘ ndx ) )
123 32 122 ax-mp ⊢ ( le ‘ ndx ) ≠ ( *𝑟 ‘ ndx )
124 necom ⊢ ( ( *𝑟 ‘ ndx ) ≠ ( dist ‘ ndx ) ↔ ( dist ‘ ndx ) ≠ ( *𝑟 ‘ ndx ) )
125 124 biimpi ⊢ ( ( *𝑟 ‘ ndx ) ≠ ( dist ‘ ndx ) → ( dist ‘ ndx ) ≠ ( *𝑟 ‘ ndx ) )
126 125 adantr ⊢ ( ( ( *𝑟 ‘ ndx ) ≠ ( dist ‘ ndx ) ∧ ( le ‘ ndx ) ≠ ( dist ‘ ndx ) ) → ( dist ‘ ndx ) ≠ ( *𝑟 ‘ ndx ) )
127 36 126 ax-mp ⊢ ( dist ‘ ndx ) ≠ ( *𝑟 ‘ ndx )
128 disjtpsn ⊢ ( ( ( TopSet ‘ ndx ) ≠ ( *𝑟 ‘ ndx ) ∧ ( le ‘ ndx ) ≠ ( *𝑟 ‘ ndx ) ∧ ( dist ‘ ndx ) ≠ ( *𝑟 ‘ ndx ) ) → ( { ( TopSet ‘ ndx ) , ( le ‘ ndx ) , ( dist ‘ ndx ) } ∩ { ( *𝑟 ‘ ndx ) } ) = ∅ )
129 119 123 127 128 mp3an ⊢ ( { ( TopSet ‘ ndx ) , ( le ‘ ndx ) , ( dist ‘ ndx ) } ∩ { ( *𝑟 ‘ ndx ) } ) = ∅
130 129 ineqcomi ⊢ ( { ( *𝑟 ‘ ndx ) } ∩ { ( TopSet ‘ ndx ) , ( le ‘ ndx ) , ( dist ‘ ndx ) } ) = ∅
131 118 130 eqtri ⊢ ( dom { ⟨ ( *𝑟 ‘ ndx ) , ∗ ⟩ } ∩ dom { ⟨ ( TopSet ‘ ndx ) , ( MetOpen ‘ ( abs ∘ − ) ) ⟩ , ⟨ ( le ‘ ndx ) , ≤ ⟩ , ⟨ ( dist ‘ ndx ) , ( abs ∘ − ) ⟩ } ) = ∅
132 19 59 ineq12i ⊢ ( dom { ⟨ ( *𝑟 ‘ ndx ) , ∗ ⟩ } ∩ dom { ⟨ ( UnifSet ‘ ndx ) , ( metUnif ‘ ( abs ∘ − ) ) ⟩ } ) = ( { ( *𝑟 ‘ ndx ) } ∩ { ( UnifSet ‘ ndx ) } )
133 simpl3 ⊢ ( ( ( ( +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 ⊢ ( *𝑟 ‘ ndx ) ≠ ( UnifSet ‘ ndx )
135 disjsn2 ⊢ ( ( *𝑟 ‘ ndx ) ≠ ( UnifSet ‘ ndx ) → ( { ( *𝑟 ‘ ndx ) } ∩ { ( UnifSet ‘ ndx ) } ) = ∅ )
136 134 135 ax-mp ⊢ ( { ( *𝑟 ‘ ndx ) } ∩ { ( UnifSet ‘ ndx ) } ) = ∅
137 132 136 eqtri ⊢ ( dom { ⟨ ( *𝑟 ‘ ndx ) , ∗ ⟩ } ∩ dom { ⟨ ( UnifSet ‘ ndx ) , ( metUnif ‘ ( abs ∘ − ) ) ⟩ } ) = ∅
138 131 137 pm3.2i ⊢ ( ( dom { ⟨ ( *𝑟 ‘ ndx ) , ∗ ⟩ } ∩ dom { ⟨ ( TopSet ‘ ndx ) , ( MetOpen ‘ ( abs ∘ − ) ) ⟩ , ⟨ ( le ‘ ndx ) , ≤ ⟩ , ⟨ ( dist ‘ ndx ) , ( abs ∘ − ) ⟩ } ) = ∅ ∧ ( dom { ⟨ ( *𝑟 ‘ ndx ) , ∗ ⟩ } ∩ dom { ⟨ ( UnifSet ‘ ndx ) , ( metUnif ‘ ( abs ∘ − ) ) ⟩ } ) = ∅ )
139 undisj2 ⊢ ( ( ( 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 ⊢ ( dom { ⟨ ( *𝑟 ‘ ndx ) , ∗ ⟩ } ∩ ( dom { ⟨ ( TopSet ‘ ndx ) , ( MetOpen ‘ ( abs ∘ − ) ) ⟩ , ⟨ ( le ‘ ndx ) , ≤ ⟩ , ⟨ ( dist ‘ ndx ) , ( abs ∘ − ) ⟩ } ∪ dom { ⟨ ( UnifSet ‘ ndx ) , ( metUnif ‘ ( abs ∘ − ) ) ⟩ } ) ) = ∅
141 117 140 pm3.2i ⊢ ( ( 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 ⊢ ( ( ( 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 ⊢ ( ( 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 ⊢ ( dom ( { ⟨ ( Base ‘ ndx ) , ℂ ⟩ , ⟨ ( +g ‘ ndx ) , ( 𝑢 ∈ ℂ , 𝑣 ∈ ℂ ↦ ( 𝑢 + 𝑣 ) ) ⟩ , ⟨ ( .r ‘ ndx ) , ( 𝑢 ∈ ℂ , 𝑣 ∈ ℂ ↦ ( 𝑢 · 𝑣 ) ) ⟩ } ∪ { ⟨ ( *𝑟 ‘ ndx ) , ∗ ⟩ } ) ∩ dom ( { ⟨ ( TopSet ‘ ndx ) , ( MetOpen ‘ ( abs ∘ − ) ) ⟩ , ⟨ ( le ‘ ndx ) , ≤ ⟩ , ⟨ ( dist ‘ ndx ) , ( abs ∘ − ) ⟩ } ∪ { ⟨ ( UnifSet ‘ ndx ) , ( metUnif ‘ ( abs ∘ − ) ) ⟩ } ) ) = ∅
145 funun ⊢ ( ( ( 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 ⊢ Fun ( ( { ⟨ ( Base ‘ ndx ) , ℂ ⟩ , ⟨ ( +g ‘ ndx ) , ( 𝑢 ∈ ℂ , 𝑣 ∈ ℂ ↦ ( 𝑢 + 𝑣 ) ) ⟩ , ⟨ ( .r ‘ ndx ) , ( 𝑢 ∈ ℂ , 𝑣 ∈ ℂ ↦ ( 𝑢 · 𝑣 ) ) ⟩ } ∪ { ⟨ ( *𝑟 ‘ ndx ) , ∗ ⟩ } ) ∪ ( { ⟨ ( TopSet ‘ ndx ) , ( MetOpen ‘ ( abs ∘ − ) ) ⟩ , ⟨ ( le ‘ ndx ) , ≤ ⟩ , ⟨ ( dist ‘ ndx ) , ( abs ∘ − ) ⟩ } ∪ { ⟨ ( UnifSet ‘ ndx ) , ( metUnif ‘ ( abs ∘ − ) ) ⟩ } ) )
147 df-cnfld ⊢ ℂfld = ( ( { ⟨ ( Base ‘ ndx ) , ℂ ⟩ , ⟨ ( +g ‘ ndx ) , ( 𝑢 ∈ ℂ , 𝑣 ∈ ℂ ↦ ( 𝑢 + 𝑣 ) ) ⟩ , ⟨ ( .r ‘ ndx ) , ( 𝑢 ∈ ℂ , 𝑣 ∈ ℂ ↦ ( 𝑢 · 𝑣 ) ) ⟩ } ∪ { ⟨ ( *𝑟 ‘ ndx ) , ∗ ⟩ } ) ∪ ( { ⟨ ( TopSet ‘ ndx ) , ( MetOpen ‘ ( abs ∘ − ) ) ⟩ , ⟨ ( le ‘ ndx ) , ≤ ⟩ , ⟨ ( dist ‘ ndx ) , ( abs ∘ − ) ⟩ } ∪ { ⟨ ( UnifSet ‘ ndx ) , ( metUnif ‘ ( abs ∘ − ) ) ⟩ } ) )
148 147 funeqi ⊢ ( 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 ⊢ Fun ℂfld