Metamath Proof Explorer

Theorem addlid

Description: 0 is a left identity for addition. This used to be one of our complex number axioms, until it was discovered that it was dependent on the others. Based on ideas by Eric Schmidt. (Contributed by Scott Fenton, 3-Jan-2013)

Ref Expression
Assertion addlid ( 𝐴 ∈ ℂ → ( 0 + 𝐴 ) = 𝐴 )

Proof

Step Hyp Ref Expression
1 cnegex ⊢ ( 𝐴 ∈ ℂ → ∃ 𝑥 ∈ ℂ ( 𝐴 + 𝑥 ) = 0 )
2 cnegex ⊢ ( 𝑥 ∈ ℂ → ∃ 𝑦 ∈ ℂ ( 𝑥 + 𝑦 ) = 0 )
3 2 ad2antrl ⊢ ( ( 𝐴 ∈ ℂ ∧ ( 𝑥 ∈ ℂ ∧ ( 𝐴 + 𝑥 ) = 0 ) ) → ∃ 𝑦 ∈ ℂ ( 𝑥 + 𝑦 ) = 0 )
4 0cn ⊢ 0 ∈ ℂ
5 addass ⊢ ( ( 0 ∈ ℂ ∧ 0 ∈ ℂ ∧ 𝑦 ∈ ℂ ) → ( ( 0 + 0 ) + 𝑦 ) = ( 0 + ( 0 + 𝑦 ) ) )
6 4 4 5 mp3an12 ⊢ ( 𝑦 ∈ ℂ → ( ( 0 + 0 ) + 𝑦 ) = ( 0 + ( 0 + 𝑦 ) ) )
7 6 adantr ⊢ ( ( 𝑦 ∈ ℂ ∧ ( 𝑥 + 𝑦 ) = 0 ) → ( ( 0 + 0 ) + 𝑦 ) = ( 0 + ( 0 + 𝑦 ) ) )
8 7 3ad2ant3 ⊢ ( ( 𝐴 ∈ ℂ ∧ ( 𝑥 ∈ ℂ ∧ ( 𝐴 + 𝑥 ) = 0 ) ∧ ( 𝑦 ∈ ℂ ∧ ( 𝑥 + 𝑦 ) = 0 ) ) → ( ( 0 + 0 ) + 𝑦 ) = ( 0 + ( 0 + 𝑦 ) ) )
9 00id ⊢ ( 0 + 0 ) = 0
10 9 oveq1i ⊢ ( ( 0 + 0 ) + 𝑦 ) = ( 0 + 𝑦 )
11 simp1 ⊢ ( ( 𝐴 ∈ ℂ ∧ ( 𝑥 ∈ ℂ ∧ ( 𝐴 + 𝑥 ) = 0 ) ∧ ( 𝑦 ∈ ℂ ∧ ( 𝑥 + 𝑦 ) = 0 ) ) → 𝐴 ∈ ℂ )
12 simp2l ⊢ ( ( 𝐴 ∈ ℂ ∧ ( 𝑥 ∈ ℂ ∧ ( 𝐴 + 𝑥 ) = 0 ) ∧ ( 𝑦 ∈ ℂ ∧ ( 𝑥 + 𝑦 ) = 0 ) ) → 𝑥 ∈ ℂ )
13 simp3l ⊢ ( ( 𝐴 ∈ ℂ ∧ ( 𝑥 ∈ ℂ ∧ ( 𝐴 + 𝑥 ) = 0 ) ∧ ( 𝑦 ∈ ℂ ∧ ( 𝑥 + 𝑦 ) = 0 ) ) → 𝑦 ∈ ℂ )
14 11 12 13 addassd ⊢ ( ( 𝐴 ∈ ℂ ∧ ( 𝑥 ∈ ℂ ∧ ( 𝐴 + 𝑥 ) = 0 ) ∧ ( 𝑦 ∈ ℂ ∧ ( 𝑥 + 𝑦 ) = 0 ) ) → ( ( 𝐴 + 𝑥 ) + 𝑦 ) = ( 𝐴 + ( 𝑥 + 𝑦 ) ) )
15 simp2r ⊢ ( ( 𝐴 ∈ ℂ ∧ ( 𝑥 ∈ ℂ ∧ ( 𝐴 + 𝑥 ) = 0 ) ∧ ( 𝑦 ∈ ℂ ∧ ( 𝑥 + 𝑦 ) = 0 ) ) → ( 𝐴 + 𝑥 ) = 0 )
16 15 oveq1d ⊢ ( ( 𝐴 ∈ ℂ ∧ ( 𝑥 ∈ ℂ ∧ ( 𝐴 + 𝑥 ) = 0 ) ∧ ( 𝑦 ∈ ℂ ∧ ( 𝑥 + 𝑦 ) = 0 ) ) → ( ( 𝐴 + 𝑥 ) + 𝑦 ) = ( 0 + 𝑦 ) )
17 simp3r ⊢ ( ( 𝐴 ∈ ℂ ∧ ( 𝑥 ∈ ℂ ∧ ( 𝐴 + 𝑥 ) = 0 ) ∧ ( 𝑦 ∈ ℂ ∧ ( 𝑥 + 𝑦 ) = 0 ) ) → ( 𝑥 + 𝑦 ) = 0 )
18 17 oveq2d ⊢ ( ( 𝐴 ∈ ℂ ∧ ( 𝑥 ∈ ℂ ∧ ( 𝐴 + 𝑥 ) = 0 ) ∧ ( 𝑦 ∈ ℂ ∧ ( 𝑥 + 𝑦 ) = 0 ) ) → ( 𝐴 + ( 𝑥 + 𝑦 ) ) = ( 𝐴 + 0 ) )
19 14 16 18 3eqtr3rd ⊢ ( ( 𝐴 ∈ ℂ ∧ ( 𝑥 ∈ ℂ ∧ ( 𝐴 + 𝑥 ) = 0 ) ∧ ( 𝑦 ∈ ℂ ∧ ( 𝑥 + 𝑦 ) = 0 ) ) → ( 𝐴 + 0 ) = ( 0 + 𝑦 ) )
20 addrid ⊢ ( 𝐴 ∈ ℂ → ( 𝐴 + 0 ) = 𝐴 )
21 20 3ad2ant1 ⊢ ( ( 𝐴 ∈ ℂ ∧ ( 𝑥 ∈ ℂ ∧ ( 𝐴 + 𝑥 ) = 0 ) ∧ ( 𝑦 ∈ ℂ ∧ ( 𝑥 + 𝑦 ) = 0 ) ) → ( 𝐴 + 0 ) = 𝐴 )
22 19 21 eqtr3d ⊢ ( ( 𝐴 ∈ ℂ ∧ ( 𝑥 ∈ ℂ ∧ ( 𝐴 + 𝑥 ) = 0 ) ∧ ( 𝑦 ∈ ℂ ∧ ( 𝑥 + 𝑦 ) = 0 ) ) → ( 0 + 𝑦 ) = 𝐴 )
23 10 22 eqtrid ⊢ ( ( 𝐴 ∈ ℂ ∧ ( 𝑥 ∈ ℂ ∧ ( 𝐴 + 𝑥 ) = 0 ) ∧ ( 𝑦 ∈ ℂ ∧ ( 𝑥 + 𝑦 ) = 0 ) ) → ( ( 0 + 0 ) + 𝑦 ) = 𝐴 )
24 22 oveq2d ⊢ ( ( 𝐴 ∈ ℂ ∧ ( 𝑥 ∈ ℂ ∧ ( 𝐴 + 𝑥 ) = 0 ) ∧ ( 𝑦 ∈ ℂ ∧ ( 𝑥 + 𝑦 ) = 0 ) ) → ( 0 + ( 0 + 𝑦 ) ) = ( 0 + 𝐴 ) )
25 8 23 24 3eqtr3rd ⊢ ( ( 𝐴 ∈ ℂ ∧ ( 𝑥 ∈ ℂ ∧ ( 𝐴 + 𝑥 ) = 0 ) ∧ ( 𝑦 ∈ ℂ ∧ ( 𝑥 + 𝑦 ) = 0 ) ) → ( 0 + 𝐴 ) = 𝐴 )
26 25 3expia ⊢ ( ( 𝐴 ∈ ℂ ∧ ( 𝑥 ∈ ℂ ∧ ( 𝐴 + 𝑥 ) = 0 ) ) → ( ( 𝑦 ∈ ℂ ∧ ( 𝑥 + 𝑦 ) = 0 ) → ( 0 + 𝐴 ) = 𝐴 ) )
27 26 expd ⊢ ( ( 𝐴 ∈ ℂ ∧ ( 𝑥 ∈ ℂ ∧ ( 𝐴 + 𝑥 ) = 0 ) ) → ( 𝑦 ∈ ℂ → ( ( 𝑥 + 𝑦 ) = 0 → ( 0 + 𝐴 ) = 𝐴 ) ) )
28 27 rexlimdv ⊢ ( ( 𝐴 ∈ ℂ ∧ ( 𝑥 ∈ ℂ ∧ ( 𝐴 + 𝑥 ) = 0 ) ) → ( ∃ 𝑦 ∈ ℂ ( 𝑥 + 𝑦 ) = 0 → ( 0 + 𝐴 ) = 𝐴 ) )
29 3 28 mpd ⊢ ( ( 𝐴 ∈ ℂ ∧ ( 𝑥 ∈ ℂ ∧ ( 𝐴 + 𝑥 ) = 0 ) ) → ( 0 + 𝐴 ) = 𝐴 )
30 1 29 rexlimddv ⊢ ( 𝐴 ∈ ℂ → ( 0 + 𝐴 ) = 𝐴 )