Metamath Proof Explorer


Theorem drnginvrr

Description: Property of the multiplicative inverse in a division ring. ( recid analog). (Contributed by NM, 19-Apr-2014)

Ref Expression
Hypotheses drnginvrl.b โŠข ๐ต = ( Base โ€˜ ๐‘… )
drnginvrl.z โŠข 0 = ( 0g โ€˜ ๐‘… )
drnginvrl.t โŠข ยท = ( .r โ€˜ ๐‘… )
drnginvrl.u โŠข 1 = ( 1r โ€˜ ๐‘… )
drnginvrl.i โŠข ๐ผ = ( invr โ€˜ ๐‘… )
Assertion drnginvrr ( ( ๐‘… โˆˆ DivRing โˆง ๐‘‹ โˆˆ ๐ต โˆง ๐‘‹ โ‰  0 ) โ†’ ( ๐‘‹ ยท ( ๐ผ โ€˜ ๐‘‹ ) ) = 1 )

Proof

Step Hyp Ref Expression
1 drnginvrl.b โŠข ๐ต = ( Base โ€˜ ๐‘… )
2 drnginvrl.z โŠข 0 = ( 0g โ€˜ ๐‘… )
3 drnginvrl.t โŠข ยท = ( .r โ€˜ ๐‘… )
4 drnginvrl.u โŠข 1 = ( 1r โ€˜ ๐‘… )
5 drnginvrl.i โŠข ๐ผ = ( invr โ€˜ ๐‘… )
6 eqid โŠข ( Unit โ€˜ ๐‘… ) = ( Unit โ€˜ ๐‘… )
7 1 6 2 drngunit โŠข ( ๐‘… โˆˆ DivRing โ†’ ( ๐‘‹ โˆˆ ( Unit โ€˜ ๐‘… ) โ†” ( ๐‘‹ โˆˆ ๐ต โˆง ๐‘‹ โ‰  0 ) ) )
8 drngring โŠข ( ๐‘… โˆˆ DivRing โ†’ ๐‘… โˆˆ Ring )
9 6 5 3 4 unitrinv โŠข ( ( ๐‘… โˆˆ Ring โˆง ๐‘‹ โˆˆ ( Unit โ€˜ ๐‘… ) ) โ†’ ( ๐‘‹ ยท ( ๐ผ โ€˜ ๐‘‹ ) ) = 1 )
10 9 ex โŠข ( ๐‘… โˆˆ Ring โ†’ ( ๐‘‹ โˆˆ ( Unit โ€˜ ๐‘… ) โ†’ ( ๐‘‹ ยท ( ๐ผ โ€˜ ๐‘‹ ) ) = 1 ) )
11 8 10 syl โŠข ( ๐‘… โˆˆ DivRing โ†’ ( ๐‘‹ โˆˆ ( Unit โ€˜ ๐‘… ) โ†’ ( ๐‘‹ ยท ( ๐ผ โ€˜ ๐‘‹ ) ) = 1 ) )
12 7 11 sylbird โŠข ( ๐‘… โˆˆ DivRing โ†’ ( ( ๐‘‹ โˆˆ ๐ต โˆง ๐‘‹ โ‰  0 ) โ†’ ( ๐‘‹ ยท ( ๐ผ โ€˜ ๐‘‹ ) ) = 1 ) )
13 12 3impib โŠข ( ( ๐‘… โˆˆ DivRing โˆง ๐‘‹ โˆˆ ๐ต โˆง ๐‘‹ โ‰  0 ) โ†’ ( ๐‘‹ ยท ( ๐ผ โ€˜ ๐‘‹ ) ) = 1 )