Metamath Proof Explorer


Theorem cnaddabl

Description: The complex numbers are an Abelian group under addition. This version of cnaddablx hides the explicit structure indices i.e. is "scaffold-independent". Note that the proof also does not reference explicit structure indices. The actual structure is dependent on how Base and +g is defined. This theorem should not be referenced in any proof. For the group/ring properties of the complex numbers, see cnring . (Contributed by NM, 20-Oct-2012) (New usage is discouraged.)

Ref Expression
Hypothesis cnaddabl.g G = Base ndx + ndx +
Assertion cnaddabl G Abel

Proof

Step Hyp Ref Expression
1 cnaddabl.g G = Base ndx + ndx +
2 cnex V
3 1 grpbase V = Base G
4 2 3 ax-mp = Base G
5 addex + V
6 1 grpplusg + V + = + G
7 5 6 ax-mp + = + G
8 addcl x y x + y
9 addass x y z x + y + z = x + y + z
10 0cn 0
11 addid2 x 0 + x = x
12 negcl x x
13 addcom x x x + x = - x + x
14 12 13 mpdan x x + x = - x + x
15 negid x x + x = 0
16 14 15 eqtr3d x - x + x = 0
17 4 7 8 9 10 11 12 16 isgrpi G Grp
18 addcom x y x + y = y + x
19 17 4 7 18 isabli G Abel