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

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 ‘ + ) = ( ℩ 𝑦 ∈ ℂ ∀ 𝑥 ∈ ℂ ( 𝑦 + 𝑥 ) = 𝑥 ) )
9 3 8 ax-mp ⊢ ( GId ‘ + ) = ( ℩ 𝑦 ∈ ℂ ∀ 𝑥 ∈ ℂ ( 𝑦 + 𝑥 ) = 𝑥 )
10 addlid ⊢ ( 𝑥 ∈ ℂ → ( 0 + 𝑥 ) = 𝑥 )
11 10 rgen ⊢ ∀ 𝑥 ∈ ℂ ( 0 + 𝑥 ) = 𝑥
12 0cn ⊢ 0 ∈ ℂ
13 6 grpoideu ⊢ ( + ∈ GrpOp → ∃! 𝑦 ∈ ℂ ∀ 𝑥 ∈ ℂ ( 𝑦 + 𝑥 ) = 𝑥 )
14 3 13 ax-mp ⊢ ∃! 𝑦 ∈ ℂ ∀ 𝑥 ∈ ℂ ( 𝑦 + 𝑥 ) = 𝑥
15 oveq1 ⊢ ( 𝑦 = 0 → ( 𝑦 + 𝑥 ) = ( 0 + 𝑥 ) )
16 15 eqeq1d ⊢ ( 𝑦 = 0 → ( ( 𝑦 + 𝑥 ) = 𝑥 ↔ ( 0 + 𝑥 ) = 𝑥 ) )
17 16 ralbidv ⊢ ( 𝑦 = 0 → ( ∀ 𝑥 ∈ ℂ ( 𝑦 + 𝑥 ) = 𝑥 ↔ ∀ 𝑥 ∈ ℂ ( 0 + 𝑥 ) = 𝑥 ) )
18 17 riota2 ⊢ ( ( 0 ∈ ℂ ∧ ∃! 𝑦 ∈ ℂ ∀ 𝑥 ∈ ℂ ( 𝑦 + 𝑥 ) = 𝑥 ) → ( ∀ 𝑥 ∈ ℂ ( 0 + 𝑥 ) = 𝑥 ↔ ( ℩ 𝑦 ∈ ℂ ∀ 𝑥 ∈ ℂ ( 𝑦 + 𝑥 ) = 𝑥 ) = 0 ) )
19 12 14 18 mp2an ⊢ ( ∀ 𝑥 ∈ ℂ ( 0 + 𝑥 ) = 𝑥 ↔ ( ℩ 𝑦 ∈ ℂ ∀ 𝑥 ∈ ℂ ( 𝑦 + 𝑥 ) = 𝑥 ) = 0 )
20 11 19 mpbi ⊢ ( ℩ 𝑦 ∈ ℂ ∀ 𝑥 ∈ ℂ ( 𝑦 + 𝑥 ) = 𝑥 ) = 0
21 9 20 eqtr2i ⊢ 0 = ( GId ‘ + )