Theorem mpocnfldadd

Description: The addition operation of the field of complex numbers. Version of cnfldadd using maps-to notation, which does not require ax-addf . (Contributed by GG, 31-Mar-2025)

	Ref	Expression
Assertion	mpocnfldadd	⊢ ( 𝑥 ∈ ℂ , 𝑦 ∈ ℂ ↦ ( 𝑥 + 𝑦 ) ) = ( +g ‘ ℂfld )

Proof

Step	Hyp	Ref	Expression
1		mpoaddex	⊢ ( 𝑥 ∈ ℂ , 𝑦 ∈ ℂ ↦ ( 𝑥 + 𝑦 ) ) ∈ V
2		cnfldstr	⊢ ℂfld Struct ⟨ 1 , ; 1 3 ⟩
3		plusgid	⊢ +g = Slot ( +g ‘ ndx )
4		snsstp2	⊢ { ⟨ ( +g ‘ ndx ) , ( 𝑥 ∈ ℂ , 𝑦 ∈ ℂ ↦ ( 𝑥 + 𝑦 ) ) ⟩ } ⊆ { ⟨ ( Base ‘ ndx ) , ℂ ⟩ , ⟨ ( +g ‘ ndx ) , ( 𝑥 ∈ ℂ , 𝑦 ∈ ℂ ↦ ( 𝑥 + 𝑦 ) ) ⟩ , ⟨ ( .r ‘ ndx ) , ( 𝑥 ∈ ℂ , 𝑦 ∈ ℂ ↦ ( 𝑥 · 𝑦 ) ) ⟩ }
5		ssun1	⊢ { ⟨ ( Base ‘ ndx ) , ℂ ⟩ , ⟨ ( +g ‘ ndx ) , ( 𝑥 ∈ ℂ , 𝑦 ∈ ℂ ↦ ( 𝑥 + 𝑦 ) ) ⟩ , ⟨ ( .r ‘ ndx ) , ( 𝑥 ∈ ℂ , 𝑦 ∈ ℂ ↦ ( 𝑥 · 𝑦 ) ) ⟩ } ⊆ ( { ⟨ ( Base ‘ ndx ) , ℂ ⟩ , ⟨ ( +g ‘ ndx ) , ( 𝑥 ∈ ℂ , 𝑦 ∈ ℂ ↦ ( 𝑥 + 𝑦 ) ) ⟩ , ⟨ ( .r ‘ ndx ) , ( 𝑥 ∈ ℂ , 𝑦 ∈ ℂ ↦ ( 𝑥 · 𝑦 ) ) ⟩ } ∪ { ⟨ ( *𝑟 ‘ ndx ) , ∗ ⟩ } )
6		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 ∘ − ) ) ⟩ } ) )
7		df-cnfld	⊢ ℂfld = ( ( { ⟨ ( Base ‘ ndx ) , ℂ ⟩ , ⟨ ( +g ‘ ndx ) , ( 𝑥 ∈ ℂ , 𝑦 ∈ ℂ ↦ ( 𝑥 + 𝑦 ) ) ⟩ , ⟨ ( .r ‘ ndx ) , ( 𝑥 ∈ ℂ , 𝑦 ∈ ℂ ↦ ( 𝑥 · 𝑦 ) ) ⟩ } ∪ { ⟨ ( *𝑟 ‘ ndx ) , ∗ ⟩ } ) ∪ ( { ⟨ ( TopSet ‘ ndx ) , ( MetOpen ‘ ( abs ∘ − ) ) ⟩ , ⟨ ( le ‘ ndx ) , ≤ ⟩ , ⟨ ( dist ‘ ndx ) , ( abs ∘ − ) ⟩ } ∪ { ⟨ ( UnifSet ‘ ndx ) , ( metUnif ‘ ( abs ∘ − ) ) ⟩ } ) )
8	6 7	sseqtrri	⊢ ( { ⟨ ( Base ‘ ndx ) , ℂ ⟩ , ⟨ ( +g ‘ ndx ) , ( 𝑥 ∈ ℂ , 𝑦 ∈ ℂ ↦ ( 𝑥 + 𝑦 ) ) ⟩ , ⟨ ( .r ‘ ndx ) , ( 𝑥 ∈ ℂ , 𝑦 ∈ ℂ ↦ ( 𝑥 · 𝑦 ) ) ⟩ } ∪ { ⟨ ( *𝑟 ‘ ndx ) , ∗ ⟩ } ) ⊆ ℂfld
9	5 8	sstri	⊢ { ⟨ ( Base ‘ ndx ) , ℂ ⟩ , ⟨ ( +g ‘ ndx ) , ( 𝑥 ∈ ℂ , 𝑦 ∈ ℂ ↦ ( 𝑥 + 𝑦 ) ) ⟩ , ⟨ ( .r ‘ ndx ) , ( 𝑥 ∈ ℂ , 𝑦 ∈ ℂ ↦ ( 𝑥 · 𝑦 ) ) ⟩ } ⊆ ℂfld
10	4 9	sstri	⊢ { ⟨ ( +g ‘ ndx ) , ( 𝑥 ∈ ℂ , 𝑦 ∈ ℂ ↦ ( 𝑥 + 𝑦 ) ) ⟩ } ⊆ ℂfld
11	2 3 10	strfv	⊢ ( ( 𝑥 ∈ ℂ , 𝑦 ∈ ℂ ↦ ( 𝑥 + 𝑦 ) ) ∈ V → ( 𝑥 ∈ ℂ , 𝑦 ∈ ℂ ↦ ( 𝑥 + 𝑦 ) ) = ( +g ‘ ℂfld ) )
12	1 11	ax-mp	⊢ ( 𝑥 ∈ ℂ , 𝑦 ∈ ℂ ↦ ( 𝑥 + 𝑦 ) ) = ( +g ‘ ℂfld )