cnfldaddOLD

Description: Obsolete version of cnfldadd as of 27-Apr-2025. (Contributed by Stefan O'Rear, 27-Nov-2014) (Revised by Mario Carneiro, 6-Oct-2015) (Revised by Thierry Arnoux, 17-Dec-2017) (Proof modification is discouraged.) (New usage is discouraged.)

		Ref	Expression
	Assertion	cnfldaddOLD	$⊢ + = +_{ℂ_{fld}}$

Proof

Step	Hyp	Ref	Expression
1		addex	$⊢ + \in V$
2		cnfldstrOLD	$⊢ ℂ_{fld} Struct ⟨1, 13⟩$
3		plusgid	$⊢ +_{𝑔} = Slot +_{ndx}$
4		snsstp2	$⊢ \{⟨+_{ndx} +⟩\} \subseteq \{⟨{Base}_{ndx}, ℂ⟩, ⟨+_{ndx} +⟩, ⟨\cdot_{ndx} \times⟩\}$
5		ssun1	$⊢ \{⟨{Base}_{ndx}, ℂ⟩, ⟨+_{ndx} +⟩, ⟨\cdot_{ndx} \times⟩\} \subseteq \{⟨{Base}_{ndx}, ℂ⟩, ⟨+_{ndx} +⟩, ⟨\cdot_{ndx} \times⟩\} \cup \{⟨_{ndx} ⟩\}$
6		ssun1	$⊢ \{⟨{Base}_{ndx}, ℂ⟩, ⟨+_{ndx} +⟩, ⟨\cdot_{ndx} \times⟩\} \cup \{⟨_{ndx} ⟩\} \subseteq (\{⟨{Base}_{ndx}, ℂ⟩, ⟨+_{ndx} +⟩, ⟨\cdot_{ndx} \times⟩\} \cup \{⟨_{ndx} ⟩\}) \cup (\{⟨TopSet (ndx), MetOpen (abs \circ -)⟩, ⟨\leq_{ndx} \leq⟩, ⟨dist (ndx), abs \circ -⟩\} \cup \{⟨UnifSet (ndx), metUnif (abs \circ -)⟩\})$
7		dfcnfldOLD	$⊢ ℂ_{fld} = (\{⟨{Base}_{ndx}, ℂ⟩, ⟨+_{ndx} +⟩, ⟨\cdot_{ndx} \times⟩\} \cup \{⟨_{ndx} ⟩\}) \cup (\{⟨TopSet (ndx), MetOpen (abs \circ -)⟩, ⟨\leq_{ndx} \leq⟩, ⟨dist (ndx), abs \circ -⟩\} \cup \{⟨UnifSet (ndx), metUnif (abs \circ -)⟩\})$
8	6 7	sseqtrri	$⊢ \{⟨{Base}_{ndx}, ℂ⟩, ⟨+_{ndx} +⟩, ⟨\cdot_{ndx} \times⟩\} \cup \{⟨_{ndx} ⟩\} \subseteq ℂ_{fld}$
9	5 8	sstri	$⊢ \{⟨{Base}_{ndx}, ℂ⟩, ⟨+_{ndx} +⟩, ⟨\cdot_{ndx} \times⟩\} \subseteq ℂ_{fld}$
10	4 9	sstri	$⊢ \{⟨+_{ndx} +⟩\} \subseteq ℂ_{fld}$
11	2 3 10	strfv	$⊢ + \in V \to + = +_{ℂ_{fld}}$
12	1 11	ax-mp	$⊢ + = +_{ℂ_{fld}}$

Metamath Proof Explorer

Theorem cnfldaddOLD

Proof