Metamath Proof Explorer

Theorem unitlinv

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

Ref Expression
Hypotheses unitinvcl.1 โŠข ๐‘ˆ = ( Unit โ€˜ ๐‘… )
unitinvcl.2 โŠข ๐ผ = ( invr โ€˜ ๐‘… )
unitinvcl.3 โŠข ยท = ( .r โ€˜ ๐‘… )
unitinvcl.4 โŠข 1 = ( 1r โ€˜ ๐‘… )
Assertion unitlinv ( ( ๐‘… โˆˆ Ring โˆง ๐‘‹ โˆˆ ๐‘ˆ ) โ†’ ( ( ๐ผ โ€˜ ๐‘‹ ) ยท ๐‘‹ ) = 1 )

Proof

Step Hyp Ref Expression
1 unitinvcl.1 โŠข ๐‘ˆ = ( Unit โ€˜ ๐‘… )
2 unitinvcl.2 โŠข ๐ผ = ( invr โ€˜ ๐‘… )
3 unitinvcl.3 โŠข ยท = ( .r โ€˜ ๐‘… )
4 unitinvcl.4 โŠข 1 = ( 1r โ€˜ ๐‘… )
5 eqid โŠข ( ( mulGrp โ€˜ ๐‘… ) โ†พs ๐‘ˆ ) = ( ( mulGrp โ€˜ ๐‘… ) โ†พs ๐‘ˆ )
6 1 5 unitgrp โŠข ( ๐‘… โˆˆ Ring โ†’ ( ( mulGrp โ€˜ ๐‘… ) โ†พs ๐‘ˆ ) โˆˆ Grp )
7 1 5 unitgrpbas โŠข ๐‘ˆ = ( Base โ€˜ ( ( mulGrp โ€˜ ๐‘… ) โ†พs ๐‘ˆ ) )
8 1 fvexi โŠข ๐‘ˆ โˆˆ V
9 eqid โŠข ( mulGrp โ€˜ ๐‘… ) = ( mulGrp โ€˜ ๐‘… )
10 9 3 mgpplusg โŠข ยท = ( +g โ€˜ ( mulGrp โ€˜ ๐‘… ) )
11 5 10 ressplusg โŠข ( ๐‘ˆ โˆˆ V โ†’ ยท = ( +g โ€˜ ( ( mulGrp โ€˜ ๐‘… ) โ†พs ๐‘ˆ ) ) )
12 8 11 ax-mp โŠข ยท = ( +g โ€˜ ( ( mulGrp โ€˜ ๐‘… ) โ†พs ๐‘ˆ ) )
13 eqid โŠข ( 0g โ€˜ ( ( mulGrp โ€˜ ๐‘… ) โ†พs ๐‘ˆ ) ) = ( 0g โ€˜ ( ( mulGrp โ€˜ ๐‘… ) โ†พs ๐‘ˆ ) )
14 1 5 2 invrfval โŠข ๐ผ = ( invg โ€˜ ( ( mulGrp โ€˜ ๐‘… ) โ†พs ๐‘ˆ ) )
15 7 12 13 14 grplinv โŠข ( ( ( ( mulGrp โ€˜ ๐‘… ) โ†พs ๐‘ˆ ) โˆˆ Grp โˆง ๐‘‹ โˆˆ ๐‘ˆ ) โ†’ ( ( ๐ผ โ€˜ ๐‘‹ ) ยท ๐‘‹ ) = ( 0g โ€˜ ( ( mulGrp โ€˜ ๐‘… ) โ†พs ๐‘ˆ ) ) )
16 6 15 sylan โŠข ( ( ๐‘… โˆˆ Ring โˆง ๐‘‹ โˆˆ ๐‘ˆ ) โ†’ ( ( ๐ผ โ€˜ ๐‘‹ ) ยท ๐‘‹ ) = ( 0g โ€˜ ( ( mulGrp โ€˜ ๐‘… ) โ†พs ๐‘ˆ ) ) )
17 1 5 4 unitgrpid โŠข ( ๐‘… โˆˆ Ring โ†’ 1 = ( 0g โ€˜ ( ( mulGrp โ€˜ ๐‘… ) โ†พs ๐‘ˆ ) ) )
18 17 adantr โŠข ( ( ๐‘… โˆˆ Ring โˆง ๐‘‹ โˆˆ ๐‘ˆ ) โ†’ 1 = ( 0g โ€˜ ( ( mulGrp โ€˜ ๐‘… ) โ†พs ๐‘ˆ ) ) )
19 16 18 eqtr4d โŠข ( ( ๐‘… โˆˆ Ring โˆง ๐‘‹ โˆˆ ๐‘ˆ ) โ†’ ( ( ๐ผ โ€˜ ๐‘‹ ) ยท ๐‘‹ ) = 1 )