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