Metamath Proof Explorer

Theorem isdrng3

Description: A division ring is a ring in which 1 =/= 0 and every nonzero element is invertible. (Contributed by Jeff Madsen, 8-Jun-2010) (Revised by AV, 22-Jul-2026)

Ref Expression
Hypotheses isdrng3.b ⊢ 𝐵 = ( Base ‘ 𝑅 )
isdrng3.0 ⊢ 0 = ( 0g ‘ 𝑅 )
isdrng3.1 ⊢ 1 = ( 1r ‘ 𝑅 )
isdrng3.t ⊢ · = ( .r ‘ 𝑅 )
Assertion isdrng3 ( 𝑅 ∈ DivRing ↔ ( 𝑅 ∈ Ring ∧ 1 ≠ 0 ∧ ∀ 𝑥 ∈ ( 𝐵 ∖ { 0 } ) ∃ 𝑦 ∈ ( 𝐵 ∖ { 0 } ) ( 𝑦 · 𝑥 ) = 1 ) )

Proof

Step Hyp Ref Expression
1 isdrng3.b ⊢ 𝐵 = ( Base ‘ 𝑅 )
2 isdrng3.0 ⊢ 0 = ( 0g ‘ 𝑅 )
3 isdrng3.1 ⊢ 1 = ( 1r ‘ 𝑅 )
4 isdrng3.t ⊢ · = ( .r ‘ 𝑅 )
5 eqid ⊢ ( ( mulGrp ‘ 𝑅 ) ↾s ( 𝐵 ∖ { 0 } ) ) = ( ( mulGrp ‘ 𝑅 ) ↾s ( 𝐵 ∖ { 0 } ) )
6 1 2 5 isdrng2 ⊢ ( 𝑅 ∈ DivRing ↔ ( 𝑅 ∈ Ring ∧ ( ( mulGrp ‘ 𝑅 ) ↾s ( 𝐵 ∖ { 0 } ) ) ∈ Grp ) )
7 2 3 drngunz ⊢ ( 𝑅 ∈ DivRing → 1 ≠ 0 )
8 6 7 sylbir ⊢ ( ( 𝑅 ∈ Ring ∧ ( ( mulGrp ‘ 𝑅 ) ↾s ( 𝐵 ∖ { 0 } ) ) ∈ Grp ) → 1 ≠ 0 )
9 1 2 3 4 isdrng3lem1 ⊢ ( ( 𝑅 ∈ Ring ∧ ( ( mulGrp ‘ 𝑅 ) ↾s ( 𝐵 ∖ { 0 } ) ) ∈ Grp ) → ∀ 𝑥 ∈ ( 𝐵 ∖ { 0 } ) ∃ 𝑦 ∈ ( 𝐵 ∖ { 0 } ) ( 𝑦 · 𝑥 ) = 1 )
10 8 9 jca ⊢ ( ( 𝑅 ∈ Ring ∧ ( ( mulGrp ‘ 𝑅 ) ↾s ( 𝐵 ∖ { 0 } ) ) ∈ Grp ) → ( 1 ≠ 0 ∧ ∀ 𝑥 ∈ ( 𝐵 ∖ { 0 } ) ∃ 𝑦 ∈ ( 𝐵 ∖ { 0 } ) ( 𝑦 · 𝑥 ) = 1 ) )
11 3anass ⊢ ( ( 𝑅 ∈ Ring ∧ 1 ≠ 0 ∧ ∀ 𝑥 ∈ ( 𝐵 ∖ { 0 } ) ∃ 𝑦 ∈ ( 𝐵 ∖ { 0 } ) ( 𝑦 · 𝑥 ) = 1 ) ↔ ( 𝑅 ∈ Ring ∧ ( 1 ≠ 0 ∧ ∀ 𝑥 ∈ ( 𝐵 ∖ { 0 } ) ∃ 𝑦 ∈ ( 𝐵 ∖ { 0 } ) ( 𝑦 · 𝑥 ) = 1 ) ) )
12 1 2 3 4 isdrng3lem2 ⊢ ( ( 𝑅 ∈ Ring ∧ 1 ≠ 0 ∧ ∀ 𝑥 ∈ ( 𝐵 ∖ { 0 } ) ∃ 𝑦 ∈ ( 𝐵 ∖ { 0 } ) ( 𝑦 · 𝑥 ) = 1 ) → ( ( mulGrp ‘ 𝑅 ) ↾s ( 𝐵 ∖ { 0 } ) ) ∈ Grp )
13 11 12 sylbir ⊢ ( ( 𝑅 ∈ Ring ∧ ( 1 ≠ 0 ∧ ∀ 𝑥 ∈ ( 𝐵 ∖ { 0 } ) ∃ 𝑦 ∈ ( 𝐵 ∖ { 0 } ) ( 𝑦 · 𝑥 ) = 1 ) ) → ( ( mulGrp ‘ 𝑅 ) ↾s ( 𝐵 ∖ { 0 } ) ) ∈ Grp )
14 10 13 impbida ⊢ ( 𝑅 ∈ Ring → ( ( ( mulGrp ‘ 𝑅 ) ↾s ( 𝐵 ∖ { 0 } ) ) ∈ Grp ↔ ( 1 ≠ 0 ∧ ∀ 𝑥 ∈ ( 𝐵 ∖ { 0 } ) ∃ 𝑦 ∈ ( 𝐵 ∖ { 0 } ) ( 𝑦 · 𝑥 ) = 1 ) ) )
15 14 pm5.32i ⊢ ( ( 𝑅 ∈ Ring ∧ ( ( mulGrp ‘ 𝑅 ) ↾s ( 𝐵 ∖ { 0 } ) ) ∈ Grp ) ↔ ( 𝑅 ∈ Ring ∧ ( 1 ≠ 0 ∧ ∀ 𝑥 ∈ ( 𝐵 ∖ { 0 } ) ∃ 𝑦 ∈ ( 𝐵 ∖ { 0 } ) ( 𝑦 · 𝑥 ) = 1 ) ) )
16 15 6 11 3bitr4i ⊢ ( 𝑅 ∈ DivRing ↔ ( 𝑅 ∈ Ring ∧ 1 ≠ 0 ∧ ∀ 𝑥 ∈ ( 𝐵 ∖ { 0 } ) ∃ 𝑦 ∈ ( 𝐵 ∖ { 0 } ) ( 𝑦 · 𝑥 ) = 1 ) )