Metamath Proof Explorer

Theorem cnidOLD

Description: Obsolete version of cnaddid . The group identity element of complex number addition is zero. (Contributed by Steve Rodriguez, 3-Dec-2006) (Revised by Mario Carneiro, 21-Dec-2013) (New usage is discouraged.) (Proof modification is discouraged.)

Ref Expression
Assertion cnidOLD ⊢ 0 = GId ⁡ +

Proof

Step Hyp Ref Expression
1 cnaddabloOLD ⊢ + ∈ AbelOp
2 ablogrpo ⊢ + ∈ AbelOp → + ∈ GrpOp
3 1 2 ax-mp ⊢ + ∈ GrpOp
4 ax-addf ⊢ + : ℂ × ℂ ⟶ ℂ
5 4 fdmi ⊢ dom ⁡ + = ℂ × ℂ
6 3 5 grporn ⊢ ℂ = ran ⁡ +
7 eqid ⊢ GId ⁡ + = GId ⁡ +
8 6 7 grpoidval ⊢ + ∈ GrpOp → GId ⁡ + = ι y ∈ ℂ | ∀ x ∈ ℂ y + x = x
9 3 8 ax-mp ⊢ GId ⁡ + = ι y ∈ ℂ | ∀ x ∈ ℂ y + x = x
10 addlid ⊢ x ∈ ℂ → 0 + x = x
11 10 rgen ⊢ ∀ x ∈ ℂ 0 + x = x
12 0cn ⊢ 0 ∈ ℂ
13 6 grpoideu ⊢ + ∈ GrpOp → ∃! y ∈ ℂ ∀ x ∈ ℂ y + x = x
14 3 13 ax-mp ⊢ ∃! y ∈ ℂ ∀ x ∈ ℂ y + x = x
15 oveq1 ⊢ y = 0 → y + x = 0 + x
16 15 eqeq1d ⊢ y = 0 → y + x = x ↔ 0 + x = x
17 16 ralbidv ⊢ y = 0 → ∀ x ∈ ℂ y + x = x ↔ ∀ x ∈ ℂ 0 + x = x
18 17 riota2 ⊢ 0 ∈ ℂ ∧ ∃! y ∈ ℂ ∀ x ∈ ℂ y + x = x → ∀ x ∈ ℂ 0 + x = x ↔ ι y ∈ ℂ | ∀ x ∈ ℂ y + x = x = 0
19 12 14 18 mp2an ⊢ ∀ x ∈ ℂ 0 + x = x ↔ ι y ∈ ℂ | ∀ x ∈ ℂ y + x = x = 0
20 11 19 mpbi ⊢ ι y ∈ ℂ | ∀ x ∈ ℂ y + x = x = 0
21 9 20 eqtr2i ⊢ 0 = GId ⁡ +