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

Metamath Proof Explorer

Definition df-unit

Description: Define the set of units in a ring, that is, all elements with a left and right multiplicative inverse. (Contributed by Mario Carneiro, 1-Dec-2014)

Ref Expression
Assertion df-unit Unit = ( 𝑤 ∈ V ↦ ( ◡ ( ( ∥r ‘ 𝑤 ) ∩ ( ∥r ‘ ( oppr ‘ 𝑤 ) ) ) “ { ( 1r ‘ 𝑤 ) } ) )

Detailed syntax breakdown

Step Hyp Ref Expression
0 cui ⊢ Unit
1 vw ⊢ 𝑤
2 cvv ⊢ V
3 cdsr ⊢ ∥r
4 1 cv ⊢ 𝑤
5 4 3 cfv ⊢ ( ∥r ‘ 𝑤 )
6 coppr ⊢ oppr
7 4 6 cfv ⊢ ( oppr ‘ 𝑤 )
8 7 3 cfv ⊢ ( ∥r ‘ ( oppr ‘ 𝑤 ) )
9 5 8 cin ⊢ ( ( ∥r ‘ 𝑤 ) ∩ ( ∥r ‘ ( oppr ‘ 𝑤 ) ) )
10 9 ccnv ⊢ ◡ ( ( ∥r ‘ 𝑤 ) ∩ ( ∥r ‘ ( oppr ‘ 𝑤 ) ) )
11 cur ⊢ 1r
12 4 11 cfv ⊢ ( 1r ‘ 𝑤 )
13 12 csn ⊢ { ( 1r ‘ 𝑤 ) }
14 10 13 cima ⊢ ( ◡ ( ( ∥r ‘ 𝑤 ) ∩ ( ∥r ‘ ( oppr ‘ 𝑤 ) ) ) “ { ( 1r ‘ 𝑤 ) } )
15 1 2 14 cmpt ⊢ ( 𝑤 ∈ V ↦ ( ◡ ( ( ∥r ‘ 𝑤 ) ∩ ( ∥r ‘ ( oppr ‘ 𝑤 ) ) ) “ { ( 1r ‘ 𝑤 ) } ) )
16 0 15 wceq ⊢ Unit = ( 𝑤 ∈ V ↦ ( ◡ ( ( ∥r ‘ 𝑤 ) ∩ ( ∥r ‘ ( oppr ‘ 𝑤 ) ) ) “ { ( 1r ‘ 𝑤 ) } ) )