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

Metamath Proof Explorer

Theorem cnaddid

Description: The group identity element of complex number addition is zero. See also cnfld0 . (Contributed by Steve Rodriguez, 3-Dec-2006) (Revised by AV, 26-Aug-2021) (New usage is discouraged.)

Ref Expression
Hypothesis cnaddabl.g ⊢ 𝐺 = { ⟨ ( Base ‘ ndx ) , ℂ ⟩ , ⟨ ( +g ‘ ndx ) , + ⟩ }
Assertion cnaddid ( 0g ‘ 𝐺 ) = 0

Proof

Step Hyp Ref Expression
1 cnaddabl.g ⊢ 𝐺 = { ⟨ ( Base ‘ ndx ) , ℂ ⟩ , ⟨ ( +g ‘ ndx ) , + ⟩ }
2 0cn ⊢ 0 ∈ ℂ
3 cnex ⊢ ℂ ∈ V
4 1 grpbase ⊢ ( ℂ ∈ V → ℂ = ( Base ‘ 𝐺 ) )
5 3 4 ax-mp ⊢ ℂ = ( Base ‘ 𝐺 )
6 eqid ⊢ ( 0g ‘ 𝐺 ) = ( 0g ‘ 𝐺 )
7 addex ⊢ + ∈ V
8 1 grpplusg ⊢ ( + ∈ V → + = ( +g ‘ 𝐺 ) )
9 7 8 ax-mp ⊢ + = ( +g ‘ 𝐺 )
10 id ⊢ ( 0 ∈ ℂ → 0 ∈ ℂ )
11 addlid ⊢ ( 𝑥 ∈ ℂ → ( 0 + 𝑥 ) = 𝑥 )
12 11 adantl ⊢ ( ( 0 ∈ ℂ ∧ 𝑥 ∈ ℂ ) → ( 0 + 𝑥 ) = 𝑥 )
13 addrid ⊢ ( 𝑥 ∈ ℂ → ( 𝑥 + 0 ) = 𝑥 )
14 13 adantl ⊢ ( ( 0 ∈ ℂ ∧ 𝑥 ∈ ℂ ) → ( 𝑥 + 0 ) = 𝑥 )
15 5 6 9 10 12 14 ismgmid2 ⊢ ( 0 ∈ ℂ → 0 = ( 0g ‘ 𝐺 ) )
16 2 15 ax-mp ⊢ 0 = ( 0g ‘ 𝐺 )
17 16 eqcomi ⊢ ( 0g ‘ 𝐺 ) = 0