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

Theorem unitrinv 17645
 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
unitrinv

Proof of Theorem unitrinv
StepHypRef Expression
1 unitinvcl.1 . . . 4 Unit
2 eqid 2402 . . . 4 mulGrps mulGrps
31, 2unitgrp 17634 . . 3 mulGrps
41, 2unitgrpbas 17633 . . . 4 mulGrps
5 fvex 5858 . . . . . 6 Unit
61, 5eqeltri 2486 . . . . 5
7 eqid 2402 . . . . . . 7 mulGrp mulGrp
8 unitinvcl.3 . . . . . . 7
97, 8mgpplusg 17463 . . . . . 6 mulGrp
102, 9ressplusg 14953 . . . . 5 mulGrps
116, 10ax-mp 5 . . . 4 mulGrps
12 eqid 2402 . . . 4 mulGrps mulGrps
13 unitinvcl.2 . . . . 5
141, 2, 13invrfval 17640 . . . 4 mulGrps
154, 11, 12, 14grprinv 16419 . . 3 mulGrps mulGrps
163, 15sylan 469 . 2 mulGrps
17 unitinvcl.4 . . . 4
181, 2, 17unitgrpid 17636 . . 3 mulGrps