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)

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