Theorem cnfldcj

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

	Ref	Expression
Assertion	cnfldcj	⊢ ∗ = ( *𝑟 ‘ ℂfld )

Proof

Step	Hyp	Ref	Expression
1		cjf	⊢ ∗ : ℂ ⟶ ℂ
2		cnex	⊢ ℂ ∈ V
3		fex2	⊢ ( ( ∗ : ℂ ⟶ ℂ ∧ ℂ ∈ V ∧ ℂ ∈ V ) → ∗ ∈ V )
4	1 2 2 3	mp3an	⊢ ∗ ∈ V
5		cnfldstr	⊢ ℂfld Struct ⟨ 1 , ; 1 3 ⟩
6		starvid	⊢ *𝑟 = Slot ( *𝑟 ‘ ndx )
7		ssun2	⊢ { ⟨ ( *𝑟 ‘ ndx ) , ∗ ⟩ } ⊆ ( { ⟨ ( Base ‘ ndx ) , ℂ ⟩ , ⟨ ( +g ‘ ndx ) , + ⟩ , ⟨ ( .r ‘ ndx ) , · ⟩ } ∪ { ⟨ ( *𝑟 ‘ ndx ) , ∗ ⟩ } )
8		ssun1	⊢ ( { ⟨ ( Base ‘ ndx ) , ℂ ⟩ , ⟨ ( +g ‘ ndx ) , + ⟩ , ⟨ ( .r ‘ ndx ) , · ⟩ } ∪ { ⟨ ( *𝑟 ‘ ndx ) , ∗ ⟩ } ) ⊆ ( ( { ⟨ ( Base ‘ ndx ) , ℂ ⟩ , ⟨ ( +g ‘ ndx ) , + ⟩ , ⟨ ( .r ‘ ndx ) , · ⟩ } ∪ { ⟨ ( *𝑟 ‘ ndx ) , ∗ ⟩ } ) ∪ ( { ⟨ ( TopSet ‘ ndx ) , ( MetOpen ‘ ( abs ∘ − ) ) ⟩ , ⟨ ( le ‘ ndx ) , ≤ ⟩ , ⟨ ( dist ‘ ndx ) , ( abs ∘ − ) ⟩ } ∪ { ⟨ ( UnifSet ‘ ndx ) , ( metUnif ‘ ( abs ∘ − ) ) ⟩ } ) )
9		df-cnfld	⊢ ℂfld = ( ( { ⟨ ( Base ‘ ndx ) , ℂ ⟩ , ⟨ ( +g ‘ ndx ) , + ⟩ , ⟨ ( .r ‘ ndx ) , · ⟩ } ∪ { ⟨ ( *𝑟 ‘ ndx ) , ∗ ⟩ } ) ∪ ( { ⟨ ( TopSet ‘ ndx ) , ( MetOpen ‘ ( abs ∘ − ) ) ⟩ , ⟨ ( le ‘ ndx ) , ≤ ⟩ , ⟨ ( dist ‘ ndx ) , ( abs ∘ − ) ⟩ } ∪ { ⟨ ( UnifSet ‘ ndx ) , ( metUnif ‘ ( abs ∘ − ) ) ⟩ } ) )
10	8 9	sseqtrri	⊢ ( { ⟨ ( Base ‘ ndx ) , ℂ ⟩ , ⟨ ( +g ‘ ndx ) , + ⟩ , ⟨ ( .r ‘ ndx ) , · ⟩ } ∪ { ⟨ ( *𝑟 ‘ ndx ) , ∗ ⟩ } ) ⊆ ℂfld
11	7 10	sstri	⊢ { ⟨ ( *𝑟 ‘ ndx ) , ∗ ⟩ } ⊆ ℂfld
12	5 6 11	strfv	⊢ ( ∗ ∈ V → ∗ = ( *𝑟 ‘ ℂfld ) )
13	4 12	ax-mp	⊢ ∗ = ( *𝑟 ‘ ℂfld )