Metamath Proof Explorer

Theorem crngunit

Description: Property of being a unit in a commutative ring. (Contributed by Mario Carneiro, 18-Apr-2016)

Ref Expression
Hypotheses crngunit.1 ⊢ 𝑈 = ( Unit ‘ 𝑅 )
crngunit.2 ⊢ 1 = ( 1r ‘ 𝑅 )
crngunit.3 ⊢ ∥ = ( ∥r ‘ 𝑅 )
Assertion crngunit ( 𝑅 ∈ CRing → ( 𝑋 ∈ 𝑈 ↔ 𝑋 ∥ 1 ) )

Proof

Step Hyp Ref Expression
1 crngunit.1 ⊢ 𝑈 = ( Unit ‘ 𝑅 )
2 crngunit.2 ⊢ 1 = ( 1r ‘ 𝑅 )
3 crngunit.3 ⊢ ∥ = ( ∥r ‘ 𝑅 )
4 eqid ⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
5 eqid ⊢ ( .r ‘ 𝑅 ) = ( .r ‘ 𝑅 )
6 eqid ⊢ ( oppr ‘ 𝑅 ) = ( oppr ‘ 𝑅 )
7 eqid ⊢ ( .r ‘ ( oppr ‘ 𝑅 ) ) = ( .r ‘ ( oppr ‘ 𝑅 ) )
8 4 5 6 7 crngoppr ⊢ ( ( 𝑅 ∈ CRing ∧ 𝑦 ∈ ( Base ‘ 𝑅 ) ∧ 𝑋 ∈ ( Base ‘ 𝑅 ) ) → ( 𝑦 ( .r ‘ 𝑅 ) 𝑋 ) = ( 𝑦 ( .r ‘ ( oppr ‘ 𝑅 ) ) 𝑋 ) )
9 8 3expa ⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝑦 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑋 ∈ ( Base ‘ 𝑅 ) ) → ( 𝑦 ( .r ‘ 𝑅 ) 𝑋 ) = ( 𝑦 ( .r ‘ ( oppr ‘ 𝑅 ) ) 𝑋 ) )
10 9 eqcomd ⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝑦 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑋 ∈ ( Base ‘ 𝑅 ) ) → ( 𝑦 ( .r ‘ ( oppr ‘ 𝑅 ) ) 𝑋 ) = ( 𝑦 ( .r ‘ 𝑅 ) 𝑋 ) )
11 10 an32s ⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝑋 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝑅 ) ) → ( 𝑦 ( .r ‘ ( oppr ‘ 𝑅 ) ) 𝑋 ) = ( 𝑦 ( .r ‘ 𝑅 ) 𝑋 ) )
12 11 eqeq1d ⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝑋 ∈ ( Base ‘ 𝑅 ) ) ∧ 𝑦 ∈ ( Base ‘ 𝑅 ) ) → ( ( 𝑦 ( .r ‘ ( oppr ‘ 𝑅 ) ) 𝑋 ) = 1 ↔ ( 𝑦 ( .r ‘ 𝑅 ) 𝑋 ) = 1 ) )
13 12 rexbidva ⊢ ( ( 𝑅 ∈ CRing ∧ 𝑋 ∈ ( Base ‘ 𝑅 ) ) → ( ∃ 𝑦 ∈ ( Base ‘ 𝑅 ) ( 𝑦 ( .r ‘ ( oppr ‘ 𝑅 ) ) 𝑋 ) = 1 ↔ ∃ 𝑦 ∈ ( Base ‘ 𝑅 ) ( 𝑦 ( .r ‘ 𝑅 ) 𝑋 ) = 1 ) )
14 13 pm5.32da ⊢ ( 𝑅 ∈ CRing → ( ( 𝑋 ∈ ( Base ‘ 𝑅 ) ∧ ∃ 𝑦 ∈ ( Base ‘ 𝑅 ) ( 𝑦 ( .r ‘ ( oppr ‘ 𝑅 ) ) 𝑋 ) = 1 ) ↔ ( 𝑋 ∈ ( Base ‘ 𝑅 ) ∧ ∃ 𝑦 ∈ ( Base ‘ 𝑅 ) ( 𝑦 ( .r ‘ 𝑅 ) 𝑋 ) = 1 ) ) )
15 6 4 opprbas ⊢ ( Base ‘ 𝑅 ) = ( Base ‘ ( oppr ‘ 𝑅 ) )
16 eqid ⊢ ( ∥r ‘ ( oppr ‘ 𝑅 ) ) = ( ∥r ‘ ( oppr ‘ 𝑅 ) )
17 15 16 7 dvdsr ⊢ ( 𝑋 ( ∥r ‘ ( oppr ‘ 𝑅 ) ) 1 ↔ ( 𝑋 ∈ ( Base ‘ 𝑅 ) ∧ ∃ 𝑦 ∈ ( Base ‘ 𝑅 ) ( 𝑦 ( .r ‘ ( oppr ‘ 𝑅 ) ) 𝑋 ) = 1 ) )
18 4 3 5 dvdsr ⊢ ( 𝑋 ∥ 1 ↔ ( 𝑋 ∈ ( Base ‘ 𝑅 ) ∧ ∃ 𝑦 ∈ ( Base ‘ 𝑅 ) ( 𝑦 ( .r ‘ 𝑅 ) 𝑋 ) = 1 ) )
19 14 17 18 3bitr4g ⊢ ( 𝑅 ∈ CRing → ( 𝑋 ( ∥r ‘ ( oppr ‘ 𝑅 ) ) 1 ↔ 𝑋 ∥ 1 ) )
20 19 anbi2d ⊢ ( 𝑅 ∈ CRing → ( ( 𝑋 ∥ 1 ∧ 𝑋 ( ∥r ‘ ( oppr ‘ 𝑅 ) ) 1 ) ↔ ( 𝑋 ∥ 1 ∧ 𝑋 ∥ 1 ) ) )
21 1 2 3 6 16 isunit ⊢ ( 𝑋 ∈ 𝑈 ↔ ( 𝑋 ∥ 1 ∧ 𝑋 ( ∥r ‘ ( oppr ‘ 𝑅 ) ) 1 ) )
22 pm4.24 ⊢ ( 𝑋 ∥ 1 ↔ ( 𝑋 ∥ 1 ∧ 𝑋 ∥ 1 ) )
23 20 21 22 3bitr4g ⊢ ( 𝑅 ∈ CRing → ( 𝑋 ∈ 𝑈 ↔ 𝑋 ∥ 1 ) )