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

Metamath Proof Explorer

Theorem ringinveu

Description: If a ring unit element X admits both a left inverse Y and a right inverse Z , they are equal. (Contributed by Thierry Arnoux, 9-Mar-2025)

Ref Expression
Hypotheses isdrng4.b ⊢ 𝐵 = ( Base ‘ 𝑅 )
isdrng4.0 ⊢ 0 = ( 0g ‘ 𝑅 )
isdrng4.1 ⊢ 1 = ( 1r ‘ 𝑅 )
isdrng4.x ⊢ · = ( .r ‘ 𝑅 )
isdrng4.u ⊢ 𝑈 = ( Unit ‘ 𝑅 )
isdrng4.r ⊢ ( 𝜑 → 𝑅 ∈ Ring )
ringinveu.1 ⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
ringinveu.2 ⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
ringinveu.3 ⊢ ( 𝜑 → 𝑍 ∈ 𝐵 )
ringinveu.4 ⊢ ( 𝜑 → ( 𝑌 · 𝑋 ) = 1 )
ringinveu.5 ⊢ ( 𝜑 → ( 𝑋 · 𝑍 ) = 1 )
Assertion ringinveu ( 𝜑 → 𝑍 = 𝑌 )

Proof

Step Hyp Ref Expression
1 isdrng4.b ⊢ 𝐵 = ( Base ‘ 𝑅 )
2 isdrng4.0 ⊢ 0 = ( 0g ‘ 𝑅 )
3 isdrng4.1 ⊢ 1 = ( 1r ‘ 𝑅 )
4 isdrng4.x ⊢ · = ( .r ‘ 𝑅 )
5 isdrng4.u ⊢ 𝑈 = ( Unit ‘ 𝑅 )
6 isdrng4.r ⊢ ( 𝜑 → 𝑅 ∈ Ring )
7 ringinveu.1 ⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
8 ringinveu.2 ⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
9 ringinveu.3 ⊢ ( 𝜑 → 𝑍 ∈ 𝐵 )
10 ringinveu.4 ⊢ ( 𝜑 → ( 𝑌 · 𝑋 ) = 1 )
11 ringinveu.5 ⊢ ( 𝜑 → ( 𝑋 · 𝑍 ) = 1 )
12 11 oveq2d ⊢ ( 𝜑 → ( 𝑌 · ( 𝑋 · 𝑍 ) ) = ( 𝑌 · 1 ) )
13 10 oveq1d ⊢ ( 𝜑 → ( ( 𝑌 · 𝑋 ) · 𝑍 ) = ( 1 · 𝑍 ) )
14 1 4 6 8 7 9 ringassd ⊢ ( 𝜑 → ( ( 𝑌 · 𝑋 ) · 𝑍 ) = ( 𝑌 · ( 𝑋 · 𝑍 ) ) )
15 1 4 3 6 9 ringlidmd ⊢ ( 𝜑 → ( 1 · 𝑍 ) = 𝑍 )
16 13 14 15 3eqtr3d ⊢ ( 𝜑 → ( 𝑌 · ( 𝑋 · 𝑍 ) ) = 𝑍 )
17 1 4 3 6 8 ringridmd ⊢ ( 𝜑 → ( 𝑌 · 1 ) = 𝑌 )
18 12 16 17 3eqtr3d ⊢ ( 𝜑 → 𝑍 = 𝑌 )