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 ⊢ ( 𝜑 → 1 ≠ 0 )
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 ⊢ ( 𝜑 → 1 ≠ 0 )
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 syl5eq ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑥 ≠ 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 )