Metamath Proof Explorer


Theorem isunit

Description: Property of being a unit of a ring. A unit is an element that left- and right-divides one. (Contributed by Mario Carneiro, 1-Dec-2014) (Revised by Mario Carneiro, 8-Dec-2015)

Ref Expression
Hypotheses unit.1 𝑈 = ( Unit ‘ 𝑅 )
unit.2 1 = ( 1r𝑅 )
unit.3 = ( ∥r𝑅 )
unit.4 𝑆 = ( oppr𝑅 )
unit.5 𝐸 = ( ∥r𝑆 )
Assertion isunit ( 𝑋𝑈 ↔ ( 𝑋 1𝑋 𝐸 1 ) )

Proof

Step Hyp Ref Expression
1 unit.1 𝑈 = ( Unit ‘ 𝑅 )
2 unit.2 1 = ( 1r𝑅 )
3 unit.3 = ( ∥r𝑅 )
4 unit.4 𝑆 = ( oppr𝑅 )
5 unit.5 𝐸 = ( ∥r𝑆 )
6 elfvdm ( 𝑋 ∈ ( Unit ‘ 𝑅 ) → 𝑅 ∈ dom Unit )
7 6 1 eleq2s ( 𝑋𝑈𝑅 ∈ dom Unit )
8 7 elexd ( 𝑋𝑈𝑅 ∈ V )
9 df-br ( 𝑋 1 ↔ ⟨ 𝑋 , 1 ⟩ ∈ )
10 elfvdm ( ⟨ 𝑋 , 1 ⟩ ∈ ( ∥r𝑅 ) → 𝑅 ∈ dom ∥r )
11 10 3 eleq2s ( ⟨ 𝑋 , 1 ⟩ ∈ 𝑅 ∈ dom ∥r )
12 11 elexd ( ⟨ 𝑋 , 1 ⟩ ∈ 𝑅 ∈ V )
13 9 12 sylbi ( 𝑋 1𝑅 ∈ V )
14 13 adantr ( ( 𝑋 1𝑋 𝐸 1 ) → 𝑅 ∈ V )
15 fveq2 ( 𝑟 = 𝑅 → ( ∥r𝑟 ) = ( ∥r𝑅 ) )
16 15 3 eqtr4di ( 𝑟 = 𝑅 → ( ∥r𝑟 ) = )
17 fveq2 ( 𝑟 = 𝑅 → ( oppr𝑟 ) = ( oppr𝑅 ) )
18 17 4 eqtr4di ( 𝑟 = 𝑅 → ( oppr𝑟 ) = 𝑆 )
19 18 fveq2d ( 𝑟 = 𝑅 → ( ∥r ‘ ( oppr𝑟 ) ) = ( ∥r𝑆 ) )
20 19 5 eqtr4di ( 𝑟 = 𝑅 → ( ∥r ‘ ( oppr𝑟 ) ) = 𝐸 )
21 16 20 ineq12d ( 𝑟 = 𝑅 → ( ( ∥r𝑟 ) ∩ ( ∥r ‘ ( oppr𝑟 ) ) ) = ( 𝐸 ) )
22 21 cnveqd ( 𝑟 = 𝑅 ( ( ∥r𝑟 ) ∩ ( ∥r ‘ ( oppr𝑟 ) ) ) = ( 𝐸 ) )
23 fveq2 ( 𝑟 = 𝑅 → ( 1r𝑟 ) = ( 1r𝑅 ) )
24 23 2 eqtr4di ( 𝑟 = 𝑅 → ( 1r𝑟 ) = 1 )
25 24 sneqd ( 𝑟 = 𝑅 → { ( 1r𝑟 ) } = { 1 } )
26 22 25 imaeq12d ( 𝑟 = 𝑅 → ( ( ( ∥r𝑟 ) ∩ ( ∥r ‘ ( oppr𝑟 ) ) ) “ { ( 1r𝑟 ) } ) = ( ( 𝐸 ) “ { 1 } ) )
27 df-unit Unit = ( 𝑟 ∈ V ↦ ( ( ( ∥r𝑟 ) ∩ ( ∥r ‘ ( oppr𝑟 ) ) ) “ { ( 1r𝑟 ) } ) )
28 3 fvexi ∈ V
29 28 inex1 ( 𝐸 ) ∈ V
30 29 cnvex ( 𝐸 ) ∈ V
31 30 imaex ( ( 𝐸 ) “ { 1 } ) ∈ V
32 26 27 31 fvmpt ( 𝑅 ∈ V → ( Unit ‘ 𝑅 ) = ( ( 𝐸 ) “ { 1 } ) )
33 1 32 eqtrid ( 𝑅 ∈ V → 𝑈 = ( ( 𝐸 ) “ { 1 } ) )
34 33 eleq2d ( 𝑅 ∈ V → ( 𝑋𝑈𝑋 ∈ ( ( 𝐸 ) “ { 1 } ) ) )
35 inss1 ( 𝐸 ) ⊆
36 3 reldvdsr Rel
37 relss ( ( 𝐸 ) ⊆ → ( Rel → Rel ( 𝐸 ) ) )
38 35 36 37 mp2 Rel ( 𝐸 )
39 eliniseg2 ( Rel ( 𝐸 ) → ( 𝑋 ∈ ( ( 𝐸 ) “ { 1 } ) ↔ 𝑋 ( 𝐸 ) 1 ) )
40 38 39 ax-mp ( 𝑋 ∈ ( ( 𝐸 ) “ { 1 } ) ↔ 𝑋 ( 𝐸 ) 1 )
41 brin ( 𝑋 ( 𝐸 ) 1 ↔ ( 𝑋 1𝑋 𝐸 1 ) )
42 40 41 bitri ( 𝑋 ∈ ( ( 𝐸 ) “ { 1 } ) ↔ ( 𝑋 1𝑋 𝐸 1 ) )
43 34 42 bitrdi ( 𝑅 ∈ V → ( 𝑋𝑈 ↔ ( 𝑋 1𝑋 𝐸 1 ) ) )
44 8 14 43 pm5.21nii ( 𝑋𝑈 ↔ ( 𝑋 1𝑋 𝐸 1 ) )