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) Revise df-cnfld . (Revised by Thierry Arnoux, 9-Nov-2026)

	Ref	Expression
Assertion	cnfldstr	⊢ ℂfld Struct ⟨ 1 , ; 2 1 ⟩

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 ∘ − ) ) ⟩ , ⟨ ( EuclF ‘ ndx ) , 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	11	nnnn0i	⊢ 2 ∈ ℕ0
21	17	nnnn0i	⊢ 3 ∈ ℕ0
22		3lt10	⊢ 3 < ; 1 0
23		1lt2	⊢ 1 < 2
24	9 20 21 9 22 23	decltc	⊢ ; 1 3 < ; 2 1
25		1nn	⊢ 1 ∈ ℕ
26	20 25	decnncl	⊢ ; 2 1 ∈ ℕ
27		eufndx	⊢ ( EuclF ‘ ndx ) = ; 2 1
28	18 19 24 26 27	strle2	⊢ { ⟨ ( UnifSet ‘ ndx ) , ( metUnif ‘ ( abs ∘ − ) ) ⟩ , ⟨ ( EuclF ‘ ndx ) , abs ⟩ } Struct ⟨ ; 1 3 , ; 2 1 ⟩
29		2lt3	⊢ 2 < 3
30	9 20 17 29	declt	⊢ ; 1 2 < ; 1 3
31	16 28 30	strleun	⊢ ( { ⟨ ( TopSet ‘ ndx ) , ( MetOpen ‘ ( abs ∘ − ) ) ⟩ , ⟨ ( le ‘ ndx ) , ≤ ⟩ , ⟨ ( dist ‘ ndx ) , ( abs ∘ − ) ⟩ } ∪ { ⟨ ( UnifSet ‘ ndx ) , ( metUnif ‘ ( abs ∘ − ) ) ⟩ , ⟨ ( EuclF ‘ ndx ) , abs ⟩ } ) Struct ⟨ 9 , ; 2 1 ⟩
32		4lt9	⊢ 4 < 9
33	3 31 32	strleun	⊢ ( ( { ⟨ ( Base ‘ ndx ) , ℂ ⟩ , ⟨ ( +g ‘ ndx ) , ( 𝑢 ∈ ℂ , 𝑣 ∈ ℂ ↦ ( 𝑢 + 𝑣 ) ) ⟩ , ⟨ ( .r ‘ ndx ) , ( 𝑢 ∈ ℂ , 𝑣 ∈ ℂ ↦ ( 𝑢 · 𝑣 ) ) ⟩ } ∪ { ⟨ ( *𝑟 ‘ ndx ) , ∗ ⟩ } ) ∪ ( { ⟨ ( TopSet ‘ ndx ) , ( MetOpen ‘ ( abs ∘ − ) ) ⟩ , ⟨ ( le ‘ ndx ) , ≤ ⟩ , ⟨ ( dist ‘ ndx ) , ( abs ∘ − ) ⟩ } ∪ { ⟨ ( UnifSet ‘ ndx ) , ( metUnif ‘ ( abs ∘ − ) ) ⟩ , ⟨ ( EuclF ‘ ndx ) , abs ⟩ } ) ) Struct ⟨ 1 , ; 2 1 ⟩
34	1 33	eqbrtri	⊢ ℂfld Struct ⟨ 1 , ; 2 1 ⟩