Theorem cnfldds

Description: The metric of the field of complex numbers. (Contributed by Mario Carneiro, 14-Aug-2015) (Revised by Mario Carneiro, 6-Oct-2015) (Revised by Thierry Arnoux, 17-Dec-2017)

	Ref	Expression
Assertion	cnfldds	⊢ ( abs ∘ − ) = ( dist ‘ ℂfld )

Proof

Step	Hyp	Ref	Expression
1		absf	⊢ abs : ℂ ⟶ ℝ
2		subf	⊢ − : ( ℂ × ℂ ) ⟶ ℂ
3		fco	⊢ ( ( abs : ℂ ⟶ ℝ ∧ − : ( ℂ × ℂ ) ⟶ ℂ ) → ( abs ∘ − ) : ( ℂ × ℂ ) ⟶ ℝ )
4	1 2 3	mp2an	⊢ ( abs ∘ − ) : ( ℂ × ℂ ) ⟶ ℝ
5		cnex	⊢ ℂ ∈ V
6	5 5	xpex	⊢ ( ℂ × ℂ ) ∈ V
7		reex	⊢ ℝ ∈ V
8		fex2	⊢ ( ( ( abs ∘ − ) : ( ℂ × ℂ ) ⟶ ℝ ∧ ( ℂ × ℂ ) ∈ V ∧ ℝ ∈ V ) → ( abs ∘ − ) ∈ V )
9	4 6 7 8	mp3an	⊢ ( abs ∘ − ) ∈ V
10		cnfldstr	⊢ ℂfld Struct ⟨ 1 , ; 1 3 ⟩
11		dsid	⊢ dist = Slot ( dist ‘ ndx )
12		snsstp3	⊢ { ⟨ ( dist ‘ ndx ) , ( abs ∘ − ) ⟩ } ⊆ { ⟨ ( TopSet ‘ ndx ) , ( MetOpen ‘ ( abs ∘ − ) ) ⟩ , ⟨ ( le ‘ ndx ) , ≤ ⟩ , ⟨ ( dist ‘ ndx ) , ( abs ∘ − ) ⟩ }
13		ssun1	⊢ { ⟨ ( TopSet ‘ ndx ) , ( MetOpen ‘ ( abs ∘ − ) ) ⟩ , ⟨ ( le ‘ ndx ) , ≤ ⟩ , ⟨ ( dist ‘ ndx ) , ( abs ∘ − ) ⟩ } ⊆ ( { ⟨ ( TopSet ‘ ndx ) , ( MetOpen ‘ ( abs ∘ − ) ) ⟩ , ⟨ ( le ‘ ndx ) , ≤ ⟩ , ⟨ ( dist ‘ ndx ) , ( abs ∘ − ) ⟩ } ∪ { ⟨ ( UnifSet ‘ ndx ) , ( metUnif ‘ ( abs ∘ − ) ) ⟩ } )
14		ssun2	⊢ ( { ⟨ ( TopSet ‘ ndx ) , ( MetOpen ‘ ( abs ∘ − ) ) ⟩ , ⟨ ( le ‘ ndx ) , ≤ ⟩ , ⟨ ( dist ‘ ndx ) , ( abs ∘ − ) ⟩ } ∪ { ⟨ ( UnifSet ‘ ndx ) , ( metUnif ‘ ( abs ∘ − ) ) ⟩ } ) ⊆ ( ( { ⟨ ( Base ‘ ndx ) , ℂ ⟩ , ⟨ ( +g ‘ ndx ) , + ⟩ , ⟨ ( .r ‘ ndx ) , · ⟩ } ∪ { ⟨ ( *𝑟 ‘ ndx ) , ∗ ⟩ } ) ∪ ( { ⟨ ( TopSet ‘ ndx ) , ( MetOpen ‘ ( abs ∘ − ) ) ⟩ , ⟨ ( le ‘ ndx ) , ≤ ⟩ , ⟨ ( dist ‘ ndx ) , ( abs ∘ − ) ⟩ } ∪ { ⟨ ( UnifSet ‘ ndx ) , ( metUnif ‘ ( abs ∘ − ) ) ⟩ } ) )
15		df-cnfld	⊢ ℂfld = ( ( { ⟨ ( Base ‘ ndx ) , ℂ ⟩ , ⟨ ( +g ‘ ndx ) , + ⟩ , ⟨ ( .r ‘ ndx ) , · ⟩ } ∪ { ⟨ ( *𝑟 ‘ ndx ) , ∗ ⟩ } ) ∪ ( { ⟨ ( TopSet ‘ ndx ) , ( MetOpen ‘ ( abs ∘ − ) ) ⟩ , ⟨ ( le ‘ ndx ) , ≤ ⟩ , ⟨ ( dist ‘ ndx ) , ( abs ∘ − ) ⟩ } ∪ { ⟨ ( UnifSet ‘ ndx ) , ( metUnif ‘ ( abs ∘ − ) ) ⟩ } ) )
16	14 15	sseqtrri	⊢ ( { ⟨ ( TopSet ‘ ndx ) , ( MetOpen ‘ ( abs ∘ − ) ) ⟩ , ⟨ ( le ‘ ndx ) , ≤ ⟩ , ⟨ ( dist ‘ ndx ) , ( abs ∘ − ) ⟩ } ∪ { ⟨ ( UnifSet ‘ ndx ) , ( metUnif ‘ ( abs ∘ − ) ) ⟩ } ) ⊆ ℂfld
17	13 16	sstri	⊢ { ⟨ ( TopSet ‘ ndx ) , ( MetOpen ‘ ( abs ∘ − ) ) ⟩ , ⟨ ( le ‘ ndx ) , ≤ ⟩ , ⟨ ( dist ‘ ndx ) , ( abs ∘ − ) ⟩ } ⊆ ℂfld
18	12 17	sstri	⊢ { ⟨ ( dist ‘ ndx ) , ( abs ∘ − ) ⟩ } ⊆ ℂfld
19	10 11 18	strfv	⊢ ( ( abs ∘ − ) ∈ V → ( abs ∘ − ) = ( dist ‘ ℂfld ) )
20	9 19	ax-mp	⊢ ( abs ∘ − ) = ( dist ‘ ℂfld )