This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem unitrinv

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 unitrinv ( ( 𝑅 ∈ 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 grprinv ⊢ ( ( ( ( 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 )