Mathbox for Alexander van der Vekens < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  invginvrid Structured version   Unicode version

Theorem invginvrid 38471
 Description: Identity for a multiplication with additive and multiplicative inverses in a ring. (Contributed by AV, 18-May-2018.)
Hypotheses
Ref Expression
invginvrid.b
invginvrid.u Unit
invginvrid.n
invginvrid.i
invginvrid.t
Assertion
Ref Expression
invginvrid

Proof of Theorem invginvrid
StepHypRef Expression
1 eqid 2402 . . . . 5 mulGrp mulGrp
21ringmgp 17524 . . . 4 mulGrp
323ad2ant1 1018 . . 3 mulGrp
4 ringgrp 17523 . . . . 5
5 invginvrid.b . . . . . 6
6 invginvrid.u . . . . . 6 Unit
75, 6unitcl 17628 . . . . 5
8 invginvrid.n . . . . . 6
95, 8grpinvcl 16419 . . . . 5
104, 7, 9syl2an 475 . . . 4
126, 8unitnegcl 17650 . . . . 5
13 invginvrid.i . . . . . 6
146, 13, 5ringinvcl 17645 . . . . 5
1512, 14syldan 468 . . . 4
17 simp2 998 . . 3
181, 5mgpbas 17467 . . . . 5 mulGrp
19 invginvrid.t . . . . . 6
201, 19mgpplusg 17465 . . . . 5 mulGrp
2118, 20mndass 16254 . . . 4 mulGrp
2221eqcomd 2410 . . 3 mulGrp
233, 11, 16, 17, 22syl13anc 1232 . 2
24 simp1 997 . . . 4
25123adant2 1016 . . . 4
26 eqid 2402 . . . . 5
276, 13, 19, 26unitrinv 17647 . . . 4
2824, 25, 27syl2anc 659 . . 3
2928oveq1d 6293 . 2
305, 19, 26ringlidm 17542 . . 3