Metamath Proof Explorer

Theorem isdrng5

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, 23-Jul-2026)

Ref Expression
Hypotheses isdrng3.b ⊢ 𝐵 = ( Base ‘ 𝑅 )
isdrng3.0 ⊢ 0 = ( 0g ‘ 𝑅 )
isdrng3.1 ⊢ 1 = ( 1r ‘ 𝑅 )
isdrng3.t ⊢ · = ( .r ‘ 𝑅 )
Assertion isdrng5 ( 𝑅 ∈ DivRing ↔ ( 𝑅 ∈ Ring ∧ 1 ≠ 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 1 2 3 4 isdrng3 ⊢ ( 𝑅 ∈ DivRing ↔ ( 𝑅 ∈ Ring ∧ 1 ≠ 0 ∧ ∀ 𝑥 ∈ ( 𝐵 ∖ { 0 } ) ∃ 𝑦 ∈ ( 𝐵 ∖ { 0 } ) ( 𝑦 · 𝑥 ) = 1 ) )
6 eldifi ⊢ ( 𝑥 ∈ ( 𝐵 ∖ { 0 } ) → 𝑥 ∈ 𝐵 )
7 difss ⊢ ( 𝐵 ∖ { 0 } ) ⊆ 𝐵
8 ssrexv ⊢ ( ( 𝐵 ∖ { 0 } ) ⊆ 𝐵 → ( ∃ 𝑦 ∈ ( 𝐵 ∖ { 0 } ) ( 𝑦 · 𝑥 ) = 1 → ∃ 𝑦 ∈ 𝐵 ( 𝑦 · 𝑥 ) = 1 ) )
9 7 8 ax-mp ⊢ ( ∃ 𝑦 ∈ ( 𝐵 ∖ { 0 } ) ( 𝑦 · 𝑥 ) = 1 → ∃ 𝑦 ∈ 𝐵 ( 𝑦 · 𝑥 ) = 1 )
10 1 4 2 ringlz ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑥 ∈ 𝐵 ) → ( 0 · 𝑥 ) = 0 )
11 oveq1 ⊢ ( 𝑦 = 0 → ( 𝑦 · 𝑥 ) = ( 0 · 𝑥 ) )
12 11 eqeq1d ⊢ ( 𝑦 = 0 → ( ( 𝑦 · 𝑥 ) = 0 ↔ ( 0 · 𝑥 ) = 0 ) )
13 10 12 syl5ibrcom ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑥 ∈ 𝐵 ) → ( 𝑦 = 0 → ( 𝑦 · 𝑥 ) = 0 ) )
14 13 necon3d ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑥 ∈ 𝐵 ) → ( ( 𝑦 · 𝑥 ) ≠ 0 → 𝑦 ≠ 0 ) )
15 neeq1 ⊢ ( ( 𝑦 · 𝑥 ) = 1 → ( ( 𝑦 · 𝑥 ) ≠ 0 ↔ 1 ≠ 0 ) )
16 15 biimparc ⊢ ( ( 1 ≠ 0 ∧ ( 𝑦 · 𝑥 ) = 1 ) → ( 𝑦 · 𝑥 ) ≠ 0 )
17 14 16 impel ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝑥 ∈ 𝐵 ) ∧ ( 1 ≠ 0 ∧ ( 𝑦 · 𝑥 ) = 1 ) ) → 𝑦 ≠ 0 )
18 17 an4s ⊢ ( ( ( 𝑅 ∈ Ring ∧ 1 ≠ 0 ) ∧ ( 𝑥 ∈ 𝐵 ∧ ( 𝑦 · 𝑥 ) = 1 ) ) → 𝑦 ≠ 0 )
19 18 anassrs ⊢ ( ( ( ( 𝑅 ∈ Ring ∧ 1 ≠ 0 ) ∧ 𝑥 ∈ 𝐵 ) ∧ ( 𝑦 · 𝑥 ) = 1 ) → 𝑦 ≠ 0 )
20 pm3.2 ⊢ ( 𝑦 ∈ 𝐵 → ( 𝑦 ≠ 0 → ( 𝑦 ∈ 𝐵 ∧ 𝑦 ≠ 0 ) ) )
21 19 20 syl5com ⊢ ( ( ( ( 𝑅 ∈ Ring ∧ 1 ≠ 0 ) ∧ 𝑥 ∈ 𝐵 ) ∧ ( 𝑦 · 𝑥 ) = 1 ) → ( 𝑦 ∈ 𝐵 → ( 𝑦 ∈ 𝐵 ∧ 𝑦 ≠ 0 ) ) )
22 eldifsn ⊢ ( 𝑦 ∈ ( 𝐵 ∖ { 0 } ) ↔ ( 𝑦 ∈ 𝐵 ∧ 𝑦 ≠ 0 ) )
23 21 22 imbitrrdi ⊢ ( ( ( ( 𝑅 ∈ Ring ∧ 1 ≠ 0 ) ∧ 𝑥 ∈ 𝐵 ) ∧ ( 𝑦 · 𝑥 ) = 1 ) → ( 𝑦 ∈ 𝐵 → 𝑦 ∈ ( 𝐵 ∖ { 0 } ) ) )
24 23 imdistanda ⊢ ( ( ( 𝑅 ∈ Ring ∧ 1 ≠ 0 ) ∧ 𝑥 ∈ 𝐵 ) → ( ( ( 𝑦 · 𝑥 ) = 1 ∧ 𝑦 ∈ 𝐵 ) → ( ( 𝑦 · 𝑥 ) = 1 ∧ 𝑦 ∈ ( 𝐵 ∖ { 0 } ) ) ) )
25 ancom ⊢ ( ( 𝑦 ∈ 𝐵 ∧ ( 𝑦 · 𝑥 ) = 1 ) ↔ ( ( 𝑦 · 𝑥 ) = 1 ∧ 𝑦 ∈ 𝐵 ) )
26 ancom ⊢ ( ( 𝑦 ∈ ( 𝐵 ∖ { 0 } ) ∧ ( 𝑦 · 𝑥 ) = 1 ) ↔ ( ( 𝑦 · 𝑥 ) = 1 ∧ 𝑦 ∈ ( 𝐵 ∖ { 0 } ) ) )
27 24 25 26 3imtr4g ⊢ ( ( ( 𝑅 ∈ Ring ∧ 1 ≠ 0 ) ∧ 𝑥 ∈ 𝐵 ) → ( ( 𝑦 ∈ 𝐵 ∧ ( 𝑦 · 𝑥 ) = 1 ) → ( 𝑦 ∈ ( 𝐵 ∖ { 0 } ) ∧ ( 𝑦 · 𝑥 ) = 1 ) ) )
28 27 reximdv2 ⊢ ( ( ( 𝑅 ∈ Ring ∧ 1 ≠ 0 ) ∧ 𝑥 ∈ 𝐵 ) → ( ∃ 𝑦 ∈ 𝐵 ( 𝑦 · 𝑥 ) = 1 → ∃ 𝑦 ∈ ( 𝐵 ∖ { 0 } ) ( 𝑦 · 𝑥 ) = 1 ) )
29 9 28 impbid2 ⊢ ( ( ( 𝑅 ∈ Ring ∧ 1 ≠ 0 ) ∧ 𝑥 ∈ 𝐵 ) → ( ∃ 𝑦 ∈ ( 𝐵 ∖ { 0 } ) ( 𝑦 · 𝑥 ) = 1 ↔ ∃ 𝑦 ∈ 𝐵 ( 𝑦 · 𝑥 ) = 1 ) )
30 6 29 sylan2 ⊢ ( ( ( 𝑅 ∈ Ring ∧ 1 ≠ 0 ) ∧ 𝑥 ∈ ( 𝐵 ∖ { 0 } ) ) → ( ∃ 𝑦 ∈ ( 𝐵 ∖ { 0 } ) ( 𝑦 · 𝑥 ) = 1 ↔ ∃ 𝑦 ∈ 𝐵 ( 𝑦 · 𝑥 ) = 1 ) )
31 30 ralbidva ⊢ ( ( 𝑅 ∈ Ring ∧ 1 ≠ 0 ) → ( ∀ 𝑥 ∈ ( 𝐵 ∖ { 0 } ) ∃ 𝑦 ∈ ( 𝐵 ∖ { 0 } ) ( 𝑦 · 𝑥 ) = 1 ↔ ∀ 𝑥 ∈ ( 𝐵 ∖ { 0 } ) ∃ 𝑦 ∈ 𝐵 ( 𝑦 · 𝑥 ) = 1 ) )
32 31 pm5.32i ⊢ ( ( ( 𝑅 ∈ Ring ∧ 1 ≠ 0 ) ∧ ∀ 𝑥 ∈ ( 𝐵 ∖ { 0 } ) ∃ 𝑦 ∈ ( 𝐵 ∖ { 0 } ) ( 𝑦 · 𝑥 ) = 1 ) ↔ ( ( 𝑅 ∈ Ring ∧ 1 ≠ 0 ) ∧ ∀ 𝑥 ∈ ( 𝐵 ∖ { 0 } ) ∃ 𝑦 ∈ 𝐵 ( 𝑦 · 𝑥 ) = 1 ) )
33 df-3an ⊢ ( ( 𝑅 ∈ Ring ∧ 1 ≠ 0 ∧ ∀ 𝑥 ∈ ( 𝐵 ∖ { 0 } ) ∃ 𝑦 ∈ ( 𝐵 ∖ { 0 } ) ( 𝑦 · 𝑥 ) = 1 ) ↔ ( ( 𝑅 ∈ Ring ∧ 1 ≠ 0 ) ∧ ∀ 𝑥 ∈ ( 𝐵 ∖ { 0 } ) ∃ 𝑦 ∈ ( 𝐵 ∖ { 0 } ) ( 𝑦 · 𝑥 ) = 1 ) )
34 df-3an ⊢ ( ( 𝑅 ∈ Ring ∧ 1 ≠ 0 ∧ ∀ 𝑥 ∈ ( 𝐵 ∖ { 0 } ) ∃ 𝑦 ∈ 𝐵 ( 𝑦 · 𝑥 ) = 1 ) ↔ ( ( 𝑅 ∈ Ring ∧ 1 ≠ 0 ) ∧ ∀ 𝑥 ∈ ( 𝐵 ∖ { 0 } ) ∃ 𝑦 ∈ 𝐵 ( 𝑦 · 𝑥 ) = 1 ) )
35 32 33 34 3bitr4i ⊢ ( ( 𝑅 ∈ Ring ∧ 1 ≠ 0 ∧ ∀ 𝑥 ∈ ( 𝐵 ∖ { 0 } ) ∃ 𝑦 ∈ ( 𝐵 ∖ { 0 } ) ( 𝑦 · 𝑥 ) = 1 ) ↔ ( 𝑅 ∈ Ring ∧ 1 ≠ 0 ∧ ∀ 𝑥 ∈ ( 𝐵 ∖ { 0 } ) ∃ 𝑦 ∈ 𝐵 ( 𝑦 · 𝑥 ) = 1 ) )
36 5 35 bitri ⊢ ( 𝑅 ∈ DivRing ↔ ( 𝑅 ∈ Ring ∧ 1 ≠ 0 ∧ ∀ 𝑥 ∈ ( 𝐵 ∖ { 0 } ) ∃ 𝑦 ∈ 𝐵 ( 𝑦 · 𝑥 ) = 1 ) )