This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem cnfldstr

Description: The field of complex numbers is a structure. (Contributed by Mario Carneiro, 14-Aug-2015) (Revised by Thierry Arnoux, 17-Dec-2017) Revise df-cnfld . (Revised by GG, 31-Mar-2025)

Ref Expression
Assertion cnfldstr ℂfld Struct ⟨ 1 , 1 3 ⟩

Proof

Step Hyp Ref Expression
1 df-cnfld ⊢ ℂfld = ( ( { ⟨ ( Base ‘ ndx ) , ℂ ⟩ , ⟨ ( +g ‘ ndx ) , ( 𝑢 ∈ ℂ , 𝑣 ∈ ℂ ↦ ( 𝑢 + 𝑣 ) ) ⟩ , ⟨ ( .r ‘ ndx ) , ( 𝑢 ∈ ℂ , 𝑣 ∈ ℂ ↦ ( 𝑢 · 𝑣 ) ) ⟩ } ∪ { ⟨ ( *𝑟 ‘ ndx ) , ∗ ⟩ } ) ∪ ( { ⟨ ( TopSet ‘ ndx ) , ( MetOpen ‘ ( abs ∘ − ) ) ⟩ , ⟨ ( le ‘ ndx ) , ≤ ⟩ , ⟨ ( dist ‘ ndx ) , ( abs ∘ − ) ⟩ } ∪ { ⟨ ( UnifSet ‘ ndx ) , ( metUnif ‘ ( abs ∘ − ) ) ⟩ } ) )
2 eqid ⊢ ( { ⟨ ( Base ‘ ndx ) , ℂ ⟩ , ⟨ ( +g ‘ ndx ) , ( 𝑢 ∈ ℂ , 𝑣 ∈ ℂ ↦ ( 𝑢 + 𝑣 ) ) ⟩ , ⟨ ( .r ‘ ndx ) , ( 𝑢 ∈ ℂ , 𝑣 ∈ ℂ ↦ ( 𝑢 · 𝑣 ) ) ⟩ } ∪ { ⟨ ( *𝑟 ‘ ndx ) , ∗ ⟩ } ) = ( { ⟨ ( Base ‘ ndx ) , ℂ ⟩ , ⟨ ( +g ‘ ndx ) , ( 𝑢 ∈ ℂ , 𝑣 ∈ ℂ ↦ ( 𝑢 + 𝑣 ) ) ⟩ , ⟨ ( .r ‘ ndx ) , ( 𝑢 ∈ ℂ , 𝑣 ∈ ℂ ↦ ( 𝑢 · 𝑣 ) ) ⟩ } ∪ { ⟨ ( *𝑟 ‘ ndx ) , ∗ ⟩ } )
3 2 srngstr ⊢ ( { ⟨ ( Base ‘ ndx ) , ℂ ⟩ , ⟨ ( +g ‘ ndx ) , ( 𝑢 ∈ ℂ , 𝑣 ∈ ℂ ↦ ( 𝑢 + 𝑣 ) ) ⟩ , ⟨ ( .r ‘ ndx ) , ( 𝑢 ∈ ℂ , 𝑣 ∈ ℂ ↦ ( 𝑢 · 𝑣 ) ) ⟩ } ∪ { ⟨ ( *𝑟 ‘ ndx ) , ∗ ⟩ } ) Struct ⟨ 1 , 4 ⟩
4 9nn ⊢ 9 ∈ ℕ
5 tsetndx ⊢ ( TopSet ‘ ndx ) = 9
6 9lt10 ⊢ 9 < 1 0
7 10nn ⊢ 1 0 ∈ ℕ
8 plendx ⊢ ( le ‘ ndx ) = 1 0
9 1nn0 ⊢ 1 ∈ ℕ0
10 0nn0 ⊢ 0 ∈ ℕ0
11 2nn ⊢ 2 ∈ ℕ
12 2pos ⊢ 0 < 2
13 9 10 11 12 declt ⊢ 1 0 < 1 2
14 9 11 decnncl ⊢ 1 2 ∈ ℕ
15 dsndx ⊢ ( dist ‘ ndx ) = 1 2
16 4 5 6 7 8 13 14 15 strle3 ⊢ { ⟨ ( TopSet ‘ ndx ) , ( MetOpen ‘ ( abs ∘ − ) ) ⟩ , ⟨ ( le ‘ ndx ) , ≤ ⟩ , ⟨ ( dist ‘ ndx ) , ( abs ∘ − ) ⟩ } Struct ⟨ 9 , 1 2 ⟩
17 3nn ⊢ 3 ∈ ℕ
18 9 17 decnncl ⊢ 1 3 ∈ ℕ
19 unifndx ⊢ ( UnifSet ‘ ndx ) = 1 3
20 18 19 strle1 ⊢ { ⟨ ( UnifSet ‘ ndx ) , ( metUnif ‘ ( abs ∘ − ) ) ⟩ } Struct ⟨ 1 3 , 1 3 ⟩
21 2nn0 ⊢ 2 ∈ ℕ0
22 2lt3 ⊢ 2 < 3
23 9 21 17 22 declt ⊢ 1 2 < 1 3
24 16 20 23 strleun ⊢ ( { ⟨ ( TopSet ‘ ndx ) , ( MetOpen ‘ ( abs ∘ − ) ) ⟩ , ⟨ ( le ‘ ndx ) , ≤ ⟩ , ⟨ ( dist ‘ ndx ) , ( abs ∘ − ) ⟩ } ∪ { ⟨ ( UnifSet ‘ ndx ) , ( metUnif ‘ ( abs ∘ − ) ) ⟩ } ) Struct ⟨ 9 , 1 3 ⟩
25 4lt9 ⊢ 4 < 9
26 3 24 25 strleun ⊢ ( ( { ⟨ ( Base ‘ ndx ) , ℂ ⟩ , ⟨ ( +g ‘ ndx ) , ( 𝑢 ∈ ℂ , 𝑣 ∈ ℂ ↦ ( 𝑢 + 𝑣 ) ) ⟩ , ⟨ ( .r ‘ ndx ) , ( 𝑢 ∈ ℂ , 𝑣 ∈ ℂ ↦ ( 𝑢 · 𝑣 ) ) ⟩ } ∪ { ⟨ ( *𝑟 ‘ ndx ) , ∗ ⟩ } ) ∪ ( { ⟨ ( TopSet ‘ ndx ) , ( MetOpen ‘ ( abs ∘ − ) ) ⟩ , ⟨ ( le ‘ ndx ) , ≤ ⟩ , ⟨ ( dist ‘ ndx ) , ( abs ∘ − ) ⟩ } ∪ { ⟨ ( UnifSet ‘ ndx ) , ( metUnif ‘ ( abs ∘ − ) ) ⟩ } ) ) Struct ⟨ 1 , 1 3 ⟩
27 1 26 eqbrtri ⊢ ℂfld Struct ⟨ 1 , 1 3 ⟩