Metamath Proof Explorer


Theorem isdrngrd

Description: Properties that characterize a division ring among rings: it should be nonzero, have no nonzero zero-divisors, and every nonzero element x should have a right-inverse I ( x ) . See isdrngd for the characterization using left-inverses. (Contributed by NM, 10-Aug-2013) Remove hypothesis. (Revised by SN, 19-Feb-2025)

Ref Expression
Hypotheses isdrngd.b ( 𝜑𝐵 = ( Base ‘ 𝑅 ) )
isdrngd.t ( 𝜑· = ( .r𝑅 ) )
isdrngd.z ( 𝜑0 = ( 0g𝑅 ) )
isdrngd.u ( 𝜑1 = ( 1r𝑅 ) )
isdrngd.r ( 𝜑𝑅 ∈ Ring )
isdrngd.n ( ( 𝜑 ∧ ( 𝑥𝐵𝑥0 ) ∧ ( 𝑦𝐵𝑦0 ) ) → ( 𝑥 · 𝑦 ) ≠ 0 )
isdrngd.o ( 𝜑10 )
isdrngd.i ( ( 𝜑 ∧ ( 𝑥𝐵𝑥0 ) ) → 𝐼𝐵 )
isdrngrd.k ( ( 𝜑 ∧ ( 𝑥𝐵𝑥0 ) ) → ( 𝑥 · 𝐼 ) = 1 )
Assertion isdrngrd ( 𝜑𝑅 ∈ DivRing )

Proof

Step Hyp Ref Expression
1 isdrngd.b ( 𝜑𝐵 = ( Base ‘ 𝑅 ) )
2 isdrngd.t ( 𝜑· = ( .r𝑅 ) )
3 isdrngd.z ( 𝜑0 = ( 0g𝑅 ) )
4 isdrngd.u ( 𝜑1 = ( 1r𝑅 ) )
5 isdrngd.r ( 𝜑𝑅 ∈ Ring )
6 isdrngd.n ( ( 𝜑 ∧ ( 𝑥𝐵𝑥0 ) ∧ ( 𝑦𝐵𝑦0 ) ) → ( 𝑥 · 𝑦 ) ≠ 0 )
7 isdrngd.o ( 𝜑10 )
8 isdrngd.i ( ( 𝜑 ∧ ( 𝑥𝐵𝑥0 ) ) → 𝐼𝐵 )
9 isdrngrd.k ( ( 𝜑 ∧ ( 𝑥𝐵𝑥0 ) ) → ( 𝑥 · 𝐼 ) = 1 )
10 eqid ( oppr𝑅 ) = ( oppr𝑅 )
11 eqid ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
12 10 11 opprbas ( Base ‘ 𝑅 ) = ( Base ‘ ( oppr𝑅 ) )
13 1 12 eqtrdi ( 𝜑𝐵 = ( Base ‘ ( oppr𝑅 ) ) )
14 eqidd ( 𝜑 → ( .r ‘ ( oppr𝑅 ) ) = ( .r ‘ ( oppr𝑅 ) ) )
15 eqid ( 0g𝑅 ) = ( 0g𝑅 )
16 10 15 oppr0 ( 0g𝑅 ) = ( 0g ‘ ( oppr𝑅 ) )
17 3 16 eqtrdi ( 𝜑0 = ( 0g ‘ ( oppr𝑅 ) ) )
18 eqid ( 1r𝑅 ) = ( 1r𝑅 )
19 10 18 oppr1 ( 1r𝑅 ) = ( 1r ‘ ( oppr𝑅 ) )
20 4 19 eqtrdi ( 𝜑1 = ( 1r ‘ ( oppr𝑅 ) ) )
21 10 opprring ( 𝑅 ∈ Ring → ( oppr𝑅 ) ∈ Ring )
22 5 21 syl ( 𝜑 → ( oppr𝑅 ) ∈ Ring )
23 eleq1w ( 𝑦 = 𝑥 → ( 𝑦𝐵𝑥𝐵 ) )
24 neeq1 ( 𝑦 = 𝑥 → ( 𝑦0𝑥0 ) )
25 23 24 anbi12d ( 𝑦 = 𝑥 → ( ( 𝑦𝐵𝑦0 ) ↔ ( 𝑥𝐵𝑥0 ) ) )
26 25 3anbi2d ( 𝑦 = 𝑥 → ( ( 𝜑 ∧ ( 𝑦𝐵𝑦0 ) ∧ ( 𝑧𝐵𝑧0 ) ) ↔ ( 𝜑 ∧ ( 𝑥𝐵𝑥0 ) ∧ ( 𝑧𝐵𝑧0 ) ) ) )
27 oveq1 ( 𝑦 = 𝑥 → ( 𝑦 ( .r ‘ ( oppr𝑅 ) ) 𝑧 ) = ( 𝑥 ( .r ‘ ( oppr𝑅 ) ) 𝑧 ) )
28 27 neeq1d ( 𝑦 = 𝑥 → ( ( 𝑦 ( .r ‘ ( oppr𝑅 ) ) 𝑧 ) ≠ 0 ↔ ( 𝑥 ( .r ‘ ( oppr𝑅 ) ) 𝑧 ) ≠ 0 ) )
29 26 28 imbi12d ( 𝑦 = 𝑥 → ( ( ( 𝜑 ∧ ( 𝑦𝐵𝑦0 ) ∧ ( 𝑧𝐵𝑧0 ) ) → ( 𝑦 ( .r ‘ ( oppr𝑅 ) ) 𝑧 ) ≠ 0 ) ↔ ( ( 𝜑 ∧ ( 𝑥𝐵𝑥0 ) ∧ ( 𝑧𝐵𝑧0 ) ) → ( 𝑥 ( .r ‘ ( oppr𝑅 ) ) 𝑧 ) ≠ 0 ) ) )
30 eleq1w ( 𝑥 = 𝑧 → ( 𝑥𝐵𝑧𝐵 ) )
31 neeq1 ( 𝑥 = 𝑧 → ( 𝑥0𝑧0 ) )
32 30 31 anbi12d ( 𝑥 = 𝑧 → ( ( 𝑥𝐵𝑥0 ) ↔ ( 𝑧𝐵𝑧0 ) ) )
33 32 3anbi3d ( 𝑥 = 𝑧 → ( ( 𝜑 ∧ ( 𝑦𝐵𝑦0 ) ∧ ( 𝑥𝐵𝑥0 ) ) ↔ ( 𝜑 ∧ ( 𝑦𝐵𝑦0 ) ∧ ( 𝑧𝐵𝑧0 ) ) ) )
34 oveq2 ( 𝑥 = 𝑧 → ( 𝑦 ( .r ‘ ( oppr𝑅 ) ) 𝑥 ) = ( 𝑦 ( .r ‘ ( oppr𝑅 ) ) 𝑧 ) )
35 34 neeq1d ( 𝑥 = 𝑧 → ( ( 𝑦 ( .r ‘ ( oppr𝑅 ) ) 𝑥 ) ≠ 0 ↔ ( 𝑦 ( .r ‘ ( oppr𝑅 ) ) 𝑧 ) ≠ 0 ) )
36 33 35 imbi12d ( 𝑥 = 𝑧 → ( ( ( 𝜑 ∧ ( 𝑦𝐵𝑦0 ) ∧ ( 𝑥𝐵𝑥0 ) ) → ( 𝑦 ( .r ‘ ( oppr𝑅 ) ) 𝑥 ) ≠ 0 ) ↔ ( ( 𝜑 ∧ ( 𝑦𝐵𝑦0 ) ∧ ( 𝑧𝐵𝑧0 ) ) → ( 𝑦 ( .r ‘ ( oppr𝑅 ) ) 𝑧 ) ≠ 0 ) ) )
37 2 3ad2ant1 ( ( 𝜑 ∧ ( 𝑥𝐵𝑥0 ) ∧ ( 𝑦𝐵𝑦0 ) ) → · = ( .r𝑅 ) )
38 37 oveqd ( ( 𝜑 ∧ ( 𝑥𝐵𝑥0 ) ∧ ( 𝑦𝐵𝑦0 ) ) → ( 𝑥 · 𝑦 ) = ( 𝑥 ( .r𝑅 ) 𝑦 ) )
39 eqid ( .r𝑅 ) = ( .r𝑅 )
40 eqid ( .r ‘ ( oppr𝑅 ) ) = ( .r ‘ ( oppr𝑅 ) )
41 11 39 10 40 opprmul ( 𝑦 ( .r ‘ ( oppr𝑅 ) ) 𝑥 ) = ( 𝑥 ( .r𝑅 ) 𝑦 )
42 38 41 eqtr4di ( ( 𝜑 ∧ ( 𝑥𝐵𝑥0 ) ∧ ( 𝑦𝐵𝑦0 ) ) → ( 𝑥 · 𝑦 ) = ( 𝑦 ( .r ‘ ( oppr𝑅 ) ) 𝑥 ) )
43 42 6 eqnetrrd ( ( 𝜑 ∧ ( 𝑥𝐵𝑥0 ) ∧ ( 𝑦𝐵𝑦0 ) ) → ( 𝑦 ( .r ‘ ( oppr𝑅 ) ) 𝑥 ) ≠ 0 )
44 43 3com23 ( ( 𝜑 ∧ ( 𝑦𝐵𝑦0 ) ∧ ( 𝑥𝐵𝑥0 ) ) → ( 𝑦 ( .r ‘ ( oppr𝑅 ) ) 𝑥 ) ≠ 0 )
45 36 44 chvarvv ( ( 𝜑 ∧ ( 𝑦𝐵𝑦0 ) ∧ ( 𝑧𝐵𝑧0 ) ) → ( 𝑦 ( .r ‘ ( oppr𝑅 ) ) 𝑧 ) ≠ 0 )
46 29 45 chvarvv ( ( 𝜑 ∧ ( 𝑥𝐵𝑥0 ) ∧ ( 𝑧𝐵𝑧0 ) ) → ( 𝑥 ( .r ‘ ( oppr𝑅 ) ) 𝑧 ) ≠ 0 )
47 11 39 10 40 opprmul ( 𝐼 ( .r ‘ ( oppr𝑅 ) ) 𝑥 ) = ( 𝑥 ( .r𝑅 ) 𝐼 )
48 2 adantr ( ( 𝜑 ∧ ( 𝑥𝐵𝑥0 ) ) → · = ( .r𝑅 ) )
49 48 oveqd ( ( 𝜑 ∧ ( 𝑥𝐵𝑥0 ) ) → ( 𝑥 · 𝐼 ) = ( 𝑥 ( .r𝑅 ) 𝐼 ) )
50 49 9 eqtr3d ( ( 𝜑 ∧ ( 𝑥𝐵𝑥0 ) ) → ( 𝑥 ( .r𝑅 ) 𝐼 ) = 1 )
51 47 50 eqtrid ( ( 𝜑 ∧ ( 𝑥𝐵𝑥0 ) ) → ( 𝐼 ( .r ‘ ( oppr𝑅 ) ) 𝑥 ) = 1 )
52 13 14 17 20 22 46 7 8 51 isdrngd ( 𝜑 → ( oppr𝑅 ) ∈ DivRing )
53 10 opprdrng ( 𝑅 ∈ DivRing ↔ ( oppr𝑅 ) ∈ DivRing )
54 52 53 sylibr ( 𝜑𝑅 ∈ DivRing )