This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊢ ( 𝜑 → 1 ≠ 0 )
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 ⊢ ( 𝜑 → 1 ≠ 0 )
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 )