Metamath Proof Explorer


Theorem abln0

Description: Abelian groups (and therefore also groups and monoids) exist. (Contributed by AV, 29-Apr-2019)

Ref Expression
Assertion abln0 Abel

Proof

Step Hyp Ref Expression
1 vex i V
2 eqid Base ndx i + ndx i i i = Base ndx i + ndx i i i
3 2 abl1 i V Base ndx i + ndx i i i Abel
4 ne0i Base ndx i + ndx i i i Abel Abel
5 1 3 4 mp2b Abel