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 A0+A=A

Proof

Step Hyp Ref Expression
1 cnegex AxA+x=0
2 cnegex xyx+y=0
3 2 ad2antrl AxA+x=0yx+y=0
4 0cn 0
5 addass 00y0+0+y=0+0+y
6 4 4 5 mp3an12 y0+0+y=0+0+y
7 6 adantr yx+y=00+0+y=0+0+y
8 7 3ad2ant3 AxA+x=0yx+y=00+0+y=0+0+y
9 00id 0+0=0
10 9 oveq1i 0+0+y=0+y
11 simp1 AxA+x=0yx+y=0A
12 simp2l AxA+x=0yx+y=0x
13 simp3l AxA+x=0yx+y=0y
14 11 12 13 addassd AxA+x=0yx+y=0A+x+y=A+x+y
15 simp2r AxA+x=0yx+y=0A+x=0
16 15 oveq1d AxA+x=0yx+y=0A+x+y=0+y
17 simp3r AxA+x=0yx+y=0x+y=0
18 17 oveq2d AxA+x=0yx+y=0A+x+y=A+0
19 14 16 18 3eqtr3rd AxA+x=0yx+y=0A+0=0+y
20 addrid AA+0=A
21 20 3ad2ant1 AxA+x=0yx+y=0A+0=A
22 19 21 eqtr3d AxA+x=0yx+y=00+y=A
23 10 22 eqtrid AxA+x=0yx+y=00+0+y=A
24 22 oveq2d AxA+x=0yx+y=00+0+y=0+A
25 8 23 24 3eqtr3rd AxA+x=0yx+y=00+A=A
26 25 3expia AxA+x=0yx+y=00+A=A
27 26 expd AxA+x=0yx+y=00+A=A
28 27 rexlimdv AxA+x=0yx+y=00+A=A
29 3 28 mpd AxA+x=00+A=A
30 1 29 rexlimddv A0+A=A