Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  unitlinv Structured version   Unicode version

Theorem unitlinv 15774
 Description: A unit times its inverse is the identity. (Contributed by Mario Carneiro, 2-Dec-2014.)
Hypotheses
Ref Expression
unitinvcl.1 Unit
unitinvcl.2
unitinvcl.3
unitinvcl.4
Assertion
Ref Expression
unitlinv

Proof of Theorem unitlinv
StepHypRef Expression
1 unitinvcl.1 . . . 4 Unit
2 eqid 2435 . . . 4 mulGrps mulGrps
31, 2unitgrp 15764 . . 3 mulGrps
41, 2unitgrpbas 15763 . . . 4 mulGrps
5 fvex 5734 . . . . . 6 Unit
61, 5eqeltri 2505 . . . . 5
7 eqid 2435 . . . . . . 7 mulGrp mulGrp
8 unitinvcl.3 . . . . . . 7
97, 8mgpplusg 15644 . . . . . 6 mulGrp
102, 9ressplusg 13563 . . . . 5 mulGrps
116, 10ax-mp 8 . . . 4 mulGrps
12 eqid 2435 . . . 4 mulGrps mulGrps
13 unitinvcl.2 . . . . 5
141, 2, 13invrfval 15770 . . . 4 mulGrps
154, 11, 12, 14grplinv 14843 . . 3 mulGrps mulGrps
163, 15sylan 458 . 2 mulGrps
17 unitinvcl.4 . . . 4
181, 2, 17unitgrpid 15766 . . 3 mulGrps