Metamath Proof Explorer


Theorem unitrinv

Description: A unit times its inverse is the identity. (Contributed by Mario Carneiro, 2-Dec-2014)

Ref Expression
Hypotheses unitinvcl.1 U = Unit R
unitinvcl.2 I = inv r R
unitinvcl.3 · ˙ = R
unitinvcl.4 1 ˙ = 1 R
Assertion unitrinv R Ring X U X · ˙ I X = 1 ˙

Proof

Step Hyp Ref Expression
1 unitinvcl.1 U = Unit R
2 unitinvcl.2 I = inv r R
3 unitinvcl.3 · ˙ = R
4 unitinvcl.4 1 ˙ = 1 R
5 eqid mulGrp R 𝑠 U = mulGrp R 𝑠 U
6 1 5 unitgrp R Ring mulGrp R 𝑠 U Grp
7 1 5 unitgrpbas U = Base mulGrp R 𝑠 U
8 1 fvexi U V
9 eqid mulGrp R = mulGrp R
10 9 3 mgpplusg · ˙ = + mulGrp R
11 5 10 ressplusg U V · ˙ = + mulGrp R 𝑠 U
12 8 11 ax-mp · ˙ = + mulGrp R 𝑠 U
13 eqid 0 mulGrp R 𝑠 U = 0 mulGrp R 𝑠 U
14 1 5 2 invrfval I = inv g mulGrp R 𝑠 U
15 7 12 13 14 grprinv mulGrp R 𝑠 U Grp X U X · ˙ I X = 0 mulGrp R 𝑠 U
16 6 15 sylan R Ring X U X · ˙ I X = 0 mulGrp R 𝑠 U
17 1 5 4 unitgrpid R Ring 1 ˙ = 0 mulGrp R 𝑠 U
18 17 adantr R Ring X U 1 ˙ = 0 mulGrp R 𝑠 U
19 16 18 eqtr4d R Ring X U X · ˙ I X = 1 ˙