Metamath Proof Explorer

Theorem isdrng4

Description: A division ring is a ring in which 1 =/= 0 and every nonzero element has a left and right inverse. (Contributed by Thierry Arnoux, 2-Mar-2025)

Ref Expression
Hypotheses isdrng4.b ⊢ 𝐵 = ( Base ‘ 𝑅 )
isdrng4.0 ⊢ 0 = ( 0g ‘ 𝑅 )
isdrng4.1 ⊢ 1 = ( 1r ‘ 𝑅 )
isdrng4.x ⊢ · = ( .r ‘ 𝑅 )
isdrng4.u ⊢ 𝑈 = ( Unit ‘ 𝑅 )
isdrng4.r ⊢ ( 𝜑 → 𝑅 ∈ Ring )
Assertion isdrng4 ( 𝜑 → ( 𝑅 ∈ DivRing ↔ ( 1 ≠ 0 ∧ ∀ 𝑥 ∈ ( 𝐵 ∖ { 0 } ) ∃ 𝑦 ∈ 𝐵 ( ( 𝑥 · 𝑦 ) = 1 ∧ ( 𝑦 · 𝑥 ) = 1 ) ) ) )

Proof

Step Hyp Ref Expression
1 isdrng4.b ⊢ 𝐵 = ( Base ‘ 𝑅 )
2 isdrng4.0 ⊢ 0 = ( 0g ‘ 𝑅 )
3 isdrng4.1 ⊢ 1 = ( 1r ‘ 𝑅 )
4 isdrng4.x ⊢ · = ( .r ‘ 𝑅 )
5 isdrng4.u ⊢ 𝑈 = ( Unit ‘ 𝑅 )
6 isdrng4.r ⊢ ( 𝜑 → 𝑅 ∈ Ring )
7 1 5 2 isdrng ⊢ ( 𝑅 ∈ DivRing ↔ ( 𝑅 ∈ Ring ∧ 𝑈 = ( 𝐵 ∖ { 0 } ) ) )
8 6 biantrurd ⊢ ( 𝜑 → ( 𝑈 = ( 𝐵 ∖ { 0 } ) ↔ ( 𝑅 ∈ Ring ∧ 𝑈 = ( 𝐵 ∖ { 0 } ) ) ) )
9 7 8 bitr4id ⊢ ( 𝜑 → ( 𝑅 ∈ DivRing ↔ 𝑈 = ( 𝐵 ∖ { 0 } ) ) )
10 5 3 1unit ⊢ ( 𝑅 ∈ Ring → 1 ∈ 𝑈 )
11 6 10 syl ⊢ ( 𝜑 → 1 ∈ 𝑈 )
12 11 adantr ⊢ ( ( 𝜑 ∧ 𝑈 = ( 𝐵 ∖ { 0 } ) ) → 1 ∈ 𝑈 )
13 simpr ⊢ ( ( 𝜑 ∧ 𝑈 = ( 𝐵 ∖ { 0 } ) ) → 𝑈 = ( 𝐵 ∖ { 0 } ) )
14 12 13 eleqtrd ⊢ ( ( 𝜑 ∧ 𝑈 = ( 𝐵 ∖ { 0 } ) ) → 1 ∈ ( 𝐵 ∖ { 0 } ) )
15 eldifsni ⊢ ( 1 ∈ ( 𝐵 ∖ { 0 } ) → 1 ≠ 0 )
16 14 15 syl ⊢ ( ( 𝜑 ∧ 𝑈 = ( 𝐵 ∖ { 0 } ) ) → 1 ≠ 0 )
17 simpll ⊢ ( ( ( 𝜑 ∧ 𝑈 = ( 𝐵 ∖ { 0 } ) ) ∧ 𝑥 ∈ ( 𝐵 ∖ { 0 } ) ) → 𝜑 )
18 13 eleq2d ⊢ ( ( 𝜑 ∧ 𝑈 = ( 𝐵 ∖ { 0 } ) ) → ( 𝑥 ∈ 𝑈 ↔ 𝑥 ∈ ( 𝐵 ∖ { 0 } ) ) )
19 18 biimpar ⊢ ( ( ( 𝜑 ∧ 𝑈 = ( 𝐵 ∖ { 0 } ) ) ∧ 𝑥 ∈ ( 𝐵 ∖ { 0 } ) ) → 𝑥 ∈ 𝑈 )
20 6 ad5antr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑈 ) ∧ 𝑦 ∈ 𝐵 ) ∧ ( 𝑦 · 𝑥 ) = 1 ) ∧ 𝑧 ∈ 𝐵 ) ∧ ( 𝑥 · 𝑧 ) = 1 ) → 𝑅 ∈ Ring )
21 1 5 unitcl ⊢ ( 𝑥 ∈ 𝑈 → 𝑥 ∈ 𝐵 )
22 21 ad5antlr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑈 ) ∧ 𝑦 ∈ 𝐵 ) ∧ ( 𝑦 · 𝑥 ) = 1 ) ∧ 𝑧 ∈ 𝐵 ) ∧ ( 𝑥 · 𝑧 ) = 1 ) → 𝑥 ∈ 𝐵 )
23 simp-4r ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑈 ) ∧ 𝑦 ∈ 𝐵 ) ∧ ( 𝑦 · 𝑥 ) = 1 ) ∧ 𝑧 ∈ 𝐵 ) ∧ ( 𝑥 · 𝑧 ) = 1 ) → 𝑦 ∈ 𝐵 )
24 simplr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑈 ) ∧ 𝑦 ∈ 𝐵 ) ∧ ( 𝑦 · 𝑥 ) = 1 ) ∧ 𝑧 ∈ 𝐵 ) ∧ ( 𝑥 · 𝑧 ) = 1 ) → 𝑧 ∈ 𝐵 )
25 simpllr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑈 ) ∧ 𝑦 ∈ 𝐵 ) ∧ ( 𝑦 · 𝑥 ) = 1 ) ∧ 𝑧 ∈ 𝐵 ) ∧ ( 𝑥 · 𝑧 ) = 1 ) → ( 𝑦 · 𝑥 ) = 1 )
26 simpr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑈 ) ∧ 𝑦 ∈ 𝐵 ) ∧ ( 𝑦 · 𝑥 ) = 1 ) ∧ 𝑧 ∈ 𝐵 ) ∧ ( 𝑥 · 𝑧 ) = 1 ) → ( 𝑥 · 𝑧 ) = 1 )
27 1 2 3 4 5 20 22 23 24 25 26 ringinveu ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑈 ) ∧ 𝑦 ∈ 𝐵 ) ∧ ( 𝑦 · 𝑥 ) = 1 ) ∧ 𝑧 ∈ 𝐵 ) ∧ ( 𝑥 · 𝑧 ) = 1 ) → 𝑧 = 𝑦 )
28 27 oveq2d ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑈 ) ∧ 𝑦 ∈ 𝐵 ) ∧ ( 𝑦 · 𝑥 ) = 1 ) ∧ 𝑧 ∈ 𝐵 ) ∧ ( 𝑥 · 𝑧 ) = 1 ) → ( 𝑥 · 𝑧 ) = ( 𝑥 · 𝑦 ) )
29 28 26 eqtr3d ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑈 ) ∧ 𝑦 ∈ 𝐵 ) ∧ ( 𝑦 · 𝑥 ) = 1 ) ∧ 𝑧 ∈ 𝐵 ) ∧ ( 𝑥 · 𝑧 ) = 1 ) → ( 𝑥 · 𝑦 ) = 1 )
30 21 ad3antlr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑈 ) ∧ 𝑦 ∈ 𝐵 ) ∧ ( 𝑦 · 𝑥 ) = 1 ) → 𝑥 ∈ 𝐵 )
31 eqid ⊢ ( ∥r ‘ 𝑅 ) = ( ∥r ‘ 𝑅 )
32 eqid ⊢ ( oppr ‘ 𝑅 ) = ( oppr ‘ 𝑅 )
33 eqid ⊢ ( ∥r ‘ ( oppr ‘ 𝑅 ) ) = ( ∥r ‘ ( oppr ‘ 𝑅 ) )
34 5 3 31 32 33 isunit ⊢ ( 𝑥 ∈ 𝑈 ↔ ( 𝑥 ( ∥r ‘ 𝑅 ) 1 ∧ 𝑥 ( ∥r ‘ ( oppr ‘ 𝑅 ) ) 1 ) )
35 34 simprbi ⊢ ( 𝑥 ∈ 𝑈 → 𝑥 ( ∥r ‘ ( oppr ‘ 𝑅 ) ) 1 )
36 35 ad3antlr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑈 ) ∧ 𝑦 ∈ 𝐵 ) ∧ ( 𝑦 · 𝑥 ) = 1 ) → 𝑥 ( ∥r ‘ ( oppr ‘ 𝑅 ) ) 1 )
37 32 1 opprbas ⊢ 𝐵 = ( Base ‘ ( oppr ‘ 𝑅 ) )
38 eqid ⊢ ( .r ‘ ( oppr ‘ 𝑅 ) ) = ( .r ‘ ( oppr ‘ 𝑅 ) )
39 37 33 38 dvdsr2 ⊢ ( 𝑥 ∈ 𝐵 → ( 𝑥 ( ∥r ‘ ( oppr ‘ 𝑅 ) ) 1 ↔ ∃ 𝑦 ∈ 𝐵 ( 𝑦 ( .r ‘ ( oppr ‘ 𝑅 ) ) 𝑥 ) = 1 ) )
40 39 biimpa ⊢ ( ( 𝑥 ∈ 𝐵 ∧ 𝑥 ( ∥r ‘ ( oppr ‘ 𝑅 ) ) 1 ) → ∃ 𝑦 ∈ 𝐵 ( 𝑦 ( .r ‘ ( oppr ‘ 𝑅 ) ) 𝑥 ) = 1 )
41 1 4 32 38 opprmul ⊢ ( 𝑦 ( .r ‘ ( oppr ‘ 𝑅 ) ) 𝑥 ) = ( 𝑥 · 𝑦 )
42 41 eqeq1i ⊢ ( ( 𝑦 ( .r ‘ ( oppr ‘ 𝑅 ) ) 𝑥 ) = 1 ↔ ( 𝑥 · 𝑦 ) = 1 )
43 42 rexbii ⊢ ( ∃ 𝑦 ∈ 𝐵 ( 𝑦 ( .r ‘ ( oppr ‘ 𝑅 ) ) 𝑥 ) = 1 ↔ ∃ 𝑦 ∈ 𝐵 ( 𝑥 · 𝑦 ) = 1 )
44 40 43 sylib ⊢ ( ( 𝑥 ∈ 𝐵 ∧ 𝑥 ( ∥r ‘ ( oppr ‘ 𝑅 ) ) 1 ) → ∃ 𝑦 ∈ 𝐵 ( 𝑥 · 𝑦 ) = 1 )
45 oveq2 ⊢ ( 𝑦 = 𝑧 → ( 𝑥 · 𝑦 ) = ( 𝑥 · 𝑧 ) )
46 45 eqeq1d ⊢ ( 𝑦 = 𝑧 → ( ( 𝑥 · 𝑦 ) = 1 ↔ ( 𝑥 · 𝑧 ) = 1 ) )
47 46 cbvrexvw ⊢ ( ∃ 𝑦 ∈ 𝐵 ( 𝑥 · 𝑦 ) = 1 ↔ ∃ 𝑧 ∈ 𝐵 ( 𝑥 · 𝑧 ) = 1 )
48 44 47 sylib ⊢ ( ( 𝑥 ∈ 𝐵 ∧ 𝑥 ( ∥r ‘ ( oppr ‘ 𝑅 ) ) 1 ) → ∃ 𝑧 ∈ 𝐵 ( 𝑥 · 𝑧 ) = 1 )
49 30 36 48 syl2anc ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑈 ) ∧ 𝑦 ∈ 𝐵 ) ∧ ( 𝑦 · 𝑥 ) = 1 ) → ∃ 𝑧 ∈ 𝐵 ( 𝑥 · 𝑧 ) = 1 )
50 29 49 r19.29a ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑈 ) ∧ 𝑦 ∈ 𝐵 ) ∧ ( 𝑦 · 𝑥 ) = 1 ) → ( 𝑥 · 𝑦 ) = 1 )
51 simpr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑈 ) ∧ 𝑦 ∈ 𝐵 ) ∧ ( 𝑦 · 𝑥 ) = 1 ) → ( 𝑦 · 𝑥 ) = 1 )
52 50 51 jca ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑈 ) ∧ 𝑦 ∈ 𝐵 ) ∧ ( 𝑦 · 𝑥 ) = 1 ) → ( ( 𝑥 · 𝑦 ) = 1 ∧ ( 𝑦 · 𝑥 ) = 1 ) )
53 52 anasss ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑈 ) ∧ ( 𝑦 ∈ 𝐵 ∧ ( 𝑦 · 𝑥 ) = 1 ) ) → ( ( 𝑥 · 𝑦 ) = 1 ∧ ( 𝑦 · 𝑥 ) = 1 ) )
54 21 adantl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑈 ) → 𝑥 ∈ 𝐵 )
55 34 simplbi ⊢ ( 𝑥 ∈ 𝑈 → 𝑥 ( ∥r ‘ 𝑅 ) 1 )
56 55 adantl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑈 ) → 𝑥 ( ∥r ‘ 𝑅 ) 1 )
57 1 31 4 dvdsr2 ⊢ ( 𝑥 ∈ 𝐵 → ( 𝑥 ( ∥r ‘ 𝑅 ) 1 ↔ ∃ 𝑦 ∈ 𝐵 ( 𝑦 · 𝑥 ) = 1 ) )
58 57 biimpa ⊢ ( ( 𝑥 ∈ 𝐵 ∧ 𝑥 ( ∥r ‘ 𝑅 ) 1 ) → ∃ 𝑦 ∈ 𝐵 ( 𝑦 · 𝑥 ) = 1 )
59 54 56 58 syl2anc ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑈 ) → ∃ 𝑦 ∈ 𝐵 ( 𝑦 · 𝑥 ) = 1 )
60 53 59 reximddv ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑈 ) → ∃ 𝑦 ∈ 𝐵 ( ( 𝑥 · 𝑦 ) = 1 ∧ ( 𝑦 · 𝑥 ) = 1 ) )
61 17 19 60 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑈 = ( 𝐵 ∖ { 0 } ) ) ∧ 𝑥 ∈ ( 𝐵 ∖ { 0 } ) ) → ∃ 𝑦 ∈ 𝐵 ( ( 𝑥 · 𝑦 ) = 1 ∧ ( 𝑦 · 𝑥 ) = 1 ) )
62 61 ralrimiva ⊢ ( ( 𝜑 ∧ 𝑈 = ( 𝐵 ∖ { 0 } ) ) → ∀ 𝑥 ∈ ( 𝐵 ∖ { 0 } ) ∃ 𝑦 ∈ 𝐵 ( ( 𝑥 · 𝑦 ) = 1 ∧ ( 𝑦 · 𝑥 ) = 1 ) )
63 16 62 jca ⊢ ( ( 𝜑 ∧ 𝑈 = ( 𝐵 ∖ { 0 } ) ) → ( 1 ≠ 0 ∧ ∀ 𝑥 ∈ ( 𝐵 ∖ { 0 } ) ∃ 𝑦 ∈ 𝐵 ( ( 𝑥 · 𝑦 ) = 1 ∧ ( 𝑦 · 𝑥 ) = 1 ) ) )
64 1 5 unitss ⊢ 𝑈 ⊆ 𝐵
65 64 a1i ⊢ ( ( 𝜑 ∧ ( 1 ≠ 0 ∧ ∀ 𝑥 ∈ ( 𝐵 ∖ { 0 } ) ∃ 𝑦 ∈ 𝐵 ( ( 𝑥 · 𝑦 ) = 1 ∧ ( 𝑦 · 𝑥 ) = 1 ) ) ) → 𝑈 ⊆ 𝐵 )
66 6 adantr ⊢ ( ( 𝜑 ∧ ( 1 ≠ 0 ∧ ∀ 𝑥 ∈ ( 𝐵 ∖ { 0 } ) ∃ 𝑦 ∈ 𝐵 ( ( 𝑥 · 𝑦 ) = 1 ∧ ( 𝑦 · 𝑥 ) = 1 ) ) ) → 𝑅 ∈ Ring )
67 simprl ⊢ ( ( 𝜑 ∧ ( 1 ≠ 0 ∧ ∀ 𝑥 ∈ ( 𝐵 ∖ { 0 } ) ∃ 𝑦 ∈ 𝐵 ( ( 𝑥 · 𝑦 ) = 1 ∧ ( 𝑦 · 𝑥 ) = 1 ) ) ) → 1 ≠ 0 )
68 5 2 3 0unit ⊢ ( 𝑅 ∈ Ring → ( 0 ∈ 𝑈 ↔ 1 = 0 ) )
69 68 necon3bbid ⊢ ( 𝑅 ∈ Ring → ( ¬ 0 ∈ 𝑈 ↔ 1 ≠ 0 ) )
70 69 biimpar ⊢ ( ( 𝑅 ∈ Ring ∧ 1 ≠ 0 ) → ¬ 0 ∈ 𝑈 )
71 66 67 70 syl2anc ⊢ ( ( 𝜑 ∧ ( 1 ≠ 0 ∧ ∀ 𝑥 ∈ ( 𝐵 ∖ { 0 } ) ∃ 𝑦 ∈ 𝐵 ( ( 𝑥 · 𝑦 ) = 1 ∧ ( 𝑦 · 𝑥 ) = 1 ) ) ) → ¬ 0 ∈ 𝑈 )
72 ssdifsn ⊢ ( 𝑈 ⊆ ( 𝐵 ∖ { 0 } ) ↔ ( 𝑈 ⊆ 𝐵 ∧ ¬ 0 ∈ 𝑈 ) )
73 65 71 72 sylanbrc ⊢ ( ( 𝜑 ∧ ( 1 ≠ 0 ∧ ∀ 𝑥 ∈ ( 𝐵 ∖ { 0 } ) ∃ 𝑦 ∈ 𝐵 ( ( 𝑥 · 𝑦 ) = 1 ∧ ( 𝑦 · 𝑥 ) = 1 ) ) ) → 𝑈 ⊆ ( 𝐵 ∖ { 0 } ) )
74 simplr ⊢ ( ( ( ( 𝜑 ∧ 1 ≠ 0 ) ∧ 𝑥 ∈ ( 𝐵 ∖ { 0 } ) ) ∧ ∃ 𝑦 ∈ 𝐵 ( ( 𝑥 · 𝑦 ) = 1 ∧ ( 𝑦 · 𝑥 ) = 1 ) ) → 𝑥 ∈ ( 𝐵 ∖ { 0 } ) )
75 74 eldifad ⊢ ( ( ( ( 𝜑 ∧ 1 ≠ 0 ) ∧ 𝑥 ∈ ( 𝐵 ∖ { 0 } ) ) ∧ ∃ 𝑦 ∈ 𝐵 ( ( 𝑥 · 𝑦 ) = 1 ∧ ( 𝑦 · 𝑥 ) = 1 ) ) → 𝑥 ∈ 𝐵 )
76 simpr ⊢ ( ( ( 𝑥 · 𝑦 ) = 1 ∧ ( 𝑦 · 𝑥 ) = 1 ) → ( 𝑦 · 𝑥 ) = 1 )
77 76 reximi ⊢ ( ∃ 𝑦 ∈ 𝐵 ( ( 𝑥 · 𝑦 ) = 1 ∧ ( 𝑦 · 𝑥 ) = 1 ) → ∃ 𝑦 ∈ 𝐵 ( 𝑦 · 𝑥 ) = 1 )
78 77 adantl ⊢ ( ( ( ( 𝜑 ∧ 1 ≠ 0 ) ∧ 𝑥 ∈ ( 𝐵 ∖ { 0 } ) ) ∧ ∃ 𝑦 ∈ 𝐵 ( ( 𝑥 · 𝑦 ) = 1 ∧ ( 𝑦 · 𝑥 ) = 1 ) ) → ∃ 𝑦 ∈ 𝐵 ( 𝑦 · 𝑥 ) = 1 )
79 57 biimpar ⊢ ( ( 𝑥 ∈ 𝐵 ∧ ∃ 𝑦 ∈ 𝐵 ( 𝑦 · 𝑥 ) = 1 ) → 𝑥 ( ∥r ‘ 𝑅 ) 1 )
80 75 78 79 syl2anc ⊢ ( ( ( ( 𝜑 ∧ 1 ≠ 0 ) ∧ 𝑥 ∈ ( 𝐵 ∖ { 0 } ) ) ∧ ∃ 𝑦 ∈ 𝐵 ( ( 𝑥 · 𝑦 ) = 1 ∧ ( 𝑦 · 𝑥 ) = 1 ) ) → 𝑥 ( ∥r ‘ 𝑅 ) 1 )
81 simpl ⊢ ( ( ( 𝑥 · 𝑦 ) = 1 ∧ ( 𝑦 · 𝑥 ) = 1 ) → ( 𝑥 · 𝑦 ) = 1 )
82 81 reximi ⊢ ( ∃ 𝑦 ∈ 𝐵 ( ( 𝑥 · 𝑦 ) = 1 ∧ ( 𝑦 · 𝑥 ) = 1 ) → ∃ 𝑦 ∈ 𝐵 ( 𝑥 · 𝑦 ) = 1 )
83 82 adantl ⊢ ( ( ( ( 𝜑 ∧ 1 ≠ 0 ) ∧ 𝑥 ∈ ( 𝐵 ∖ { 0 } ) ) ∧ ∃ 𝑦 ∈ 𝐵 ( ( 𝑥 · 𝑦 ) = 1 ∧ ( 𝑦 · 𝑥 ) = 1 ) ) → ∃ 𝑦 ∈ 𝐵 ( 𝑥 · 𝑦 ) = 1 )
84 83 43 sylibr ⊢ ( ( ( ( 𝜑 ∧ 1 ≠ 0 ) ∧ 𝑥 ∈ ( 𝐵 ∖ { 0 } ) ) ∧ ∃ 𝑦 ∈ 𝐵 ( ( 𝑥 · 𝑦 ) = 1 ∧ ( 𝑦 · 𝑥 ) = 1 ) ) → ∃ 𝑦 ∈ 𝐵 ( 𝑦 ( .r ‘ ( oppr ‘ 𝑅 ) ) 𝑥 ) = 1 )
85 39 biimpar ⊢ ( ( 𝑥 ∈ 𝐵 ∧ ∃ 𝑦 ∈ 𝐵 ( 𝑦 ( .r ‘ ( oppr ‘ 𝑅 ) ) 𝑥 ) = 1 ) → 𝑥 ( ∥r ‘ ( oppr ‘ 𝑅 ) ) 1 )
86 75 84 85 syl2anc ⊢ ( ( ( ( 𝜑 ∧ 1 ≠ 0 ) ∧ 𝑥 ∈ ( 𝐵 ∖ { 0 } ) ) ∧ ∃ 𝑦 ∈ 𝐵 ( ( 𝑥 · 𝑦 ) = 1 ∧ ( 𝑦 · 𝑥 ) = 1 ) ) → 𝑥 ( ∥r ‘ ( oppr ‘ 𝑅 ) ) 1 )
87 80 86 34 sylanbrc ⊢ ( ( ( ( 𝜑 ∧ 1 ≠ 0 ) ∧ 𝑥 ∈ ( 𝐵 ∖ { 0 } ) ) ∧ ∃ 𝑦 ∈ 𝐵 ( ( 𝑥 · 𝑦 ) = 1 ∧ ( 𝑦 · 𝑥 ) = 1 ) ) → 𝑥 ∈ 𝑈 )
88 87 ex ⊢ ( ( ( 𝜑 ∧ 1 ≠ 0 ) ∧ 𝑥 ∈ ( 𝐵 ∖ { 0 } ) ) → ( ∃ 𝑦 ∈ 𝐵 ( ( 𝑥 · 𝑦 ) = 1 ∧ ( 𝑦 · 𝑥 ) = 1 ) → 𝑥 ∈ 𝑈 ) )
89 88 ralimdva ⊢ ( ( 𝜑 ∧ 1 ≠ 0 ) → ( ∀ 𝑥 ∈ ( 𝐵 ∖ { 0 } ) ∃ 𝑦 ∈ 𝐵 ( ( 𝑥 · 𝑦 ) = 1 ∧ ( 𝑦 · 𝑥 ) = 1 ) → ∀ 𝑥 ∈ ( 𝐵 ∖ { 0 } ) 𝑥 ∈ 𝑈 ) )
90 89 impr ⊢ ( ( 𝜑 ∧ ( 1 ≠ 0 ∧ ∀ 𝑥 ∈ ( 𝐵 ∖ { 0 } ) ∃ 𝑦 ∈ 𝐵 ( ( 𝑥 · 𝑦 ) = 1 ∧ ( 𝑦 · 𝑥 ) = 1 ) ) ) → ∀ 𝑥 ∈ ( 𝐵 ∖ { 0 } ) 𝑥 ∈ 𝑈 )
91 dfss3 ⊢ ( ( 𝐵 ∖ { 0 } ) ⊆ 𝑈 ↔ ∀ 𝑥 ∈ ( 𝐵 ∖ { 0 } ) 𝑥 ∈ 𝑈 )
92 90 91 sylibr ⊢ ( ( 𝜑 ∧ ( 1 ≠ 0 ∧ ∀ 𝑥 ∈ ( 𝐵 ∖ { 0 } ) ∃ 𝑦 ∈ 𝐵 ( ( 𝑥 · 𝑦 ) = 1 ∧ ( 𝑦 · 𝑥 ) = 1 ) ) ) → ( 𝐵 ∖ { 0 } ) ⊆ 𝑈 )
93 73 92 eqssd ⊢ ( ( 𝜑 ∧ ( 1 ≠ 0 ∧ ∀ 𝑥 ∈ ( 𝐵 ∖ { 0 } ) ∃ 𝑦 ∈ 𝐵 ( ( 𝑥 · 𝑦 ) = 1 ∧ ( 𝑦 · 𝑥 ) = 1 ) ) ) → 𝑈 = ( 𝐵 ∖ { 0 } ) )
94 63 93 impbida ⊢ ( 𝜑 → ( 𝑈 = ( 𝐵 ∖ { 0 } ) ↔ ( 1 ≠ 0 ∧ ∀ 𝑥 ∈ ( 𝐵 ∖ { 0 } ) ∃ 𝑦 ∈ 𝐵 ( ( 𝑥 · 𝑦 ) = 1 ∧ ( 𝑦 · 𝑥 ) = 1 ) ) ) )
95 9 94 bitrd ⊢ ( 𝜑 → ( 𝑅 ∈ DivRing ↔ ( 1 ≠ 0 ∧ ∀ 𝑥 ∈ ( 𝐵 ∖ { 0 } ) ∃ 𝑦 ∈ 𝐵 ( ( 𝑥 · 𝑦 ) = 1 ∧ ( 𝑦 · 𝑥 ) = 1 ) ) ) )