Metamath Proof Explorer


Theorem grpinvnzcl

Description: The inverse of a nonzero group element is a nonzero group element. (Contributed by Stefan O'Rear, 27-Feb-2015)

Ref Expression
Hypotheses grpinvnzcl.b B=BaseG
grpinvnzcl.z 0˙=0G
grpinvnzcl.n N=invgG
Assertion grpinvnzcl GGrpXB0˙NXB0˙

Proof

Step Hyp Ref Expression
1 grpinvnzcl.b B=BaseG
2 grpinvnzcl.z 0˙=0G
3 grpinvnzcl.n N=invgG
4 eldifi XB0˙XB
5 1 3 grpinvcl GGrpXBNXB
6 4 5 sylan2 GGrpXB0˙NXB
7 eldifsn XB0˙XBX0˙
8 1 2 3 grpinvnz GGrpXBX0˙NX0˙
9 8 3expb GGrpXBX0˙NX0˙
10 7 9 sylan2b GGrpXB0˙NX0˙
11 eldifsn NXB0˙NXBNX0˙
12 6 10 11 sylanbrc GGrpXB0˙NXB0˙