This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem cnfld1OLD

Description: Obsolete version of cnfld1 as of 30-Apr-2025. (Contributed by Stefan O'Rear, 27-Nov-2014) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Assertion cnfld1OLD ⊢ 1 = 1 ℂ fld

Proof

Step Hyp Ref Expression
1 ax-1cn ⊢ 1 ∈ ℂ
2 mullid ⊢ x ∈ ℂ → 1 ⁢ x = x
3 mulrid ⊢ x ∈ ℂ → x ⋅ 1 = x
4 2 3 jca ⊢ x ∈ ℂ → 1 ⁢ x = x ∧ x ⋅ 1 = x
5 4 rgen ⊢ ∀ x ∈ ℂ 1 ⁢ x = x ∧ x ⋅ 1 = x
6 1 5 pm3.2i ⊢ 1 ∈ ℂ ∧ ∀ x ∈ ℂ 1 ⁢ x = x ∧ x ⋅ 1 = x
7 cnring ⊢ ℂ fld ∈ Ring
8 cnfldbas ⊢ ℂ = Base ℂ fld
9 cnfldmul ⊢ × = ⋅ ℂ fld
10 eqid ⊢ 1 ℂ fld = 1 ℂ fld
11 8 9 10 isringid ⊢ ℂ fld ∈ Ring → 1 ∈ ℂ ∧ ∀ x ∈ ℂ 1 ⁢ x = x ∧ x ⋅ 1 = x ↔ 1 ℂ fld = 1
12 7 11 ax-mp ⊢ 1 ∈ ℂ ∧ ∀ x ∈ ℂ 1 ⁢ x = x ∧ x ⋅ 1 = x ↔ 1 ℂ fld = 1
13 6 12 mpbi ⊢ 1 ℂ fld = 1
14 13 eqcomi ⊢ 1 = 1 ℂ fld