Metamath Proof Explorer

Theorem isdrngd

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 left-inverse I ( x ) . See isdrngd for the characterization using right-inverses. (Contributed by NM, 2-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 )
isdrngd.k ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑥 ≠ 0 ) ) → ( 𝐼 · 𝑥 ) = 1 )
Assertion isdrngd ( 𝜑 → 𝑅 ∈ 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 isdrngd.k ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑥 ≠ 0 ) ) → ( 𝐼 · 𝑥 ) = 1 )
11 difss ⊢ ( 𝐵 ∖ { 0 } ) ⊆ 𝐵
12 11 1 sseqtrid ⊢ ( 𝜑 → ( 𝐵 ∖ { 0 } ) ⊆ ( Base ‘ 𝑅 ) )
13 eqid ⊢ ( ( mulGrp ‘ 𝑅 ) ↾s ( 𝐵 ∖ { 0 } ) ) = ( ( mulGrp ‘ 𝑅 ) ↾s ( 𝐵 ∖ { 0 } ) )
14 eqid ⊢ ( mulGrp ‘ 𝑅 ) = ( mulGrp ‘ 𝑅 )
15 eqid ⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
16 14 15 mgpbas ⊢ ( Base ‘ 𝑅 ) = ( Base ‘ ( mulGrp ‘ 𝑅 ) )
17 13 16 ressbas2 ⊢ ( ( 𝐵 ∖ { 0 } ) ⊆ ( Base ‘ 𝑅 ) → ( 𝐵 ∖ { 0 } ) = ( Base ‘ ( ( mulGrp ‘ 𝑅 ) ↾s ( 𝐵 ∖ { 0 } ) ) ) )
18 12 17 syl ⊢ ( 𝜑 → ( 𝐵 ∖ { 0 } ) = ( Base ‘ ( ( mulGrp ‘ 𝑅 ) ↾s ( 𝐵 ∖ { 0 } ) ) ) )
19 fvex ⊢ ( Base ‘ 𝑅 ) ∈ V
20 1 19 eqeltrdi ⊢ ( 𝜑 → 𝐵 ∈ V )
21 difexg ⊢ ( 𝐵 ∈ V → ( 𝐵 ∖ { 0 } ) ∈ V )
22 eqid ⊢ ( .r ‘ 𝑅 ) = ( .r ‘ 𝑅 )
23 14 22 mgpplusg ⊢ ( .r ‘ 𝑅 ) = ( +g ‘ ( mulGrp ‘ 𝑅 ) )
24 13 23 ressplusg ⊢ ( ( 𝐵 ∖ { 0 } ) ∈ V → ( .r ‘ 𝑅 ) = ( +g ‘ ( ( mulGrp ‘ 𝑅 ) ↾s ( 𝐵 ∖ { 0 } ) ) ) )
25 20 21 24 3syl ⊢ ( 𝜑 → ( .r ‘ 𝑅 ) = ( +g ‘ ( ( mulGrp ‘ 𝑅 ) ↾s ( 𝐵 ∖ { 0 } ) ) ) )
26 2 25 eqtrd ⊢ ( 𝜑 → · = ( +g ‘ ( ( mulGrp ‘ 𝑅 ) ↾s ( 𝐵 ∖ { 0 } ) ) ) )
27 eldifsn ⊢ ( 𝑥 ∈ ( 𝐵 ∖ { 0 } ) ↔ ( 𝑥 ∈ 𝐵 ∧ 𝑥 ≠ 0 ) )
28 eldifsn ⊢ ( 𝑦 ∈ ( 𝐵 ∖ { 0 } ) ↔ ( 𝑦 ∈ 𝐵 ∧ 𝑦 ≠ 0 ) )
29 15 22 ringcl ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ∧ 𝑦 ∈ ( Base ‘ 𝑅 ) ) → ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) ∈ ( Base ‘ 𝑅 ) )
30 5 29 syl3an1 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ∧ 𝑦 ∈ ( Base ‘ 𝑅 ) ) → ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) ∈ ( Base ‘ 𝑅 ) )
31 30 3expib ⊢ ( 𝜑 → ( ( 𝑥 ∈ ( Base ‘ 𝑅 ) ∧ 𝑦 ∈ ( Base ‘ 𝑅 ) ) → ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) ∈ ( Base ‘ 𝑅 ) ) )
32 1 eleq2d ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐵 ↔ 𝑥 ∈ ( Base ‘ 𝑅 ) ) )
33 1 eleq2d ⊢ ( 𝜑 → ( 𝑦 ∈ 𝐵 ↔ 𝑦 ∈ ( Base ‘ 𝑅 ) ) )
34 32 33 anbi12d ⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ↔ ( 𝑥 ∈ ( Base ‘ 𝑅 ) ∧ 𝑦 ∈ ( Base ‘ 𝑅 ) ) ) )
35 2 oveqd ⊢ ( 𝜑 → ( 𝑥 · 𝑦 ) = ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) )
36 35 1 eleq12d ⊢ ( 𝜑 → ( ( 𝑥 · 𝑦 ) ∈ 𝐵 ↔ ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) ∈ ( Base ‘ 𝑅 ) ) )
37 31 34 36 3imtr4d ⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) → ( 𝑥 · 𝑦 ) ∈ 𝐵 ) )
38 37 3impib ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) → ( 𝑥 · 𝑦 ) ∈ 𝐵 )
39 38 3adant2r ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑥 ≠ 0 ) ∧ 𝑦 ∈ 𝐵 ) → ( 𝑥 · 𝑦 ) ∈ 𝐵 )
40 39 3adant3r ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑥 ≠ 0 ) ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑦 ≠ 0 ) ) → ( 𝑥 · 𝑦 ) ∈ 𝐵 )
41 eldifsn ⊢ ( ( 𝑥 · 𝑦 ) ∈ ( 𝐵 ∖ { 0 } ) ↔ ( ( 𝑥 · 𝑦 ) ∈ 𝐵 ∧ ( 𝑥 · 𝑦 ) ≠ 0 ) )
42 40 6 41 sylanbrc ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑥 ≠ 0 ) ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑦 ≠ 0 ) ) → ( 𝑥 · 𝑦 ) ∈ ( 𝐵 ∖ { 0 } ) )
43 28 42 syl3an3b ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑥 ≠ 0 ) ∧ 𝑦 ∈ ( 𝐵 ∖ { 0 } ) ) → ( 𝑥 · 𝑦 ) ∈ ( 𝐵 ∖ { 0 } ) )
44 27 43 syl3an2b ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐵 ∖ { 0 } ) ∧ 𝑦 ∈ ( 𝐵 ∖ { 0 } ) ) → ( 𝑥 · 𝑦 ) ∈ ( 𝐵 ∖ { 0 } ) )
45 15 22 ringass ⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝑥 ∈ ( Base ‘ 𝑅 ) ∧ 𝑦 ∈ ( Base ‘ 𝑅 ) ∧ 𝑧 ∈ ( Base ‘ 𝑅 ) ) ) → ( ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) ( .r ‘ 𝑅 ) 𝑧 ) = ( 𝑥 ( .r ‘ 𝑅 ) ( 𝑦 ( .r ‘ 𝑅 ) 𝑧 ) ) )
46 45 ex ⊢ ( 𝑅 ∈ Ring → ( ( 𝑥 ∈ ( Base ‘ 𝑅 ) ∧ 𝑦 ∈ ( Base ‘ 𝑅 ) ∧ 𝑧 ∈ ( Base ‘ 𝑅 ) ) → ( ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) ( .r ‘ 𝑅 ) 𝑧 ) = ( 𝑥 ( .r ‘ 𝑅 ) ( 𝑦 ( .r ‘ 𝑅 ) 𝑧 ) ) ) )
47 5 46 syl ⊢ ( 𝜑 → ( ( 𝑥 ∈ ( Base ‘ 𝑅 ) ∧ 𝑦 ∈ ( Base ‘ 𝑅 ) ∧ 𝑧 ∈ ( Base ‘ 𝑅 ) ) → ( ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) ( .r ‘ 𝑅 ) 𝑧 ) = ( 𝑥 ( .r ‘ 𝑅 ) ( 𝑦 ( .r ‘ 𝑅 ) 𝑧 ) ) ) )
48 1 eleq2d ⊢ ( 𝜑 → ( 𝑧 ∈ 𝐵 ↔ 𝑧 ∈ ( Base ‘ 𝑅 ) ) )
49 32 33 48 3anbi123d ⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) ↔ ( 𝑥 ∈ ( Base ‘ 𝑅 ) ∧ 𝑦 ∈ ( Base ‘ 𝑅 ) ∧ 𝑧 ∈ ( Base ‘ 𝑅 ) ) ) )
50 eqidd ⊢ ( 𝜑 → 𝑧 = 𝑧 )
51 2 35 50 oveq123d ⊢ ( 𝜑 → ( ( 𝑥 · 𝑦 ) · 𝑧 ) = ( ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) ( .r ‘ 𝑅 ) 𝑧 ) )
52 eqidd ⊢ ( 𝜑 → 𝑥 = 𝑥 )
53 2 oveqd ⊢ ( 𝜑 → ( 𝑦 · 𝑧 ) = ( 𝑦 ( .r ‘ 𝑅 ) 𝑧 ) )
54 2 52 53 oveq123d ⊢ ( 𝜑 → ( 𝑥 · ( 𝑦 · 𝑧 ) ) = ( 𝑥 ( .r ‘ 𝑅 ) ( 𝑦 ( .r ‘ 𝑅 ) 𝑧 ) ) )
55 51 54 eqeq12d ⊢ ( 𝜑 → ( ( ( 𝑥 · 𝑦 ) · 𝑧 ) = ( 𝑥 · ( 𝑦 · 𝑧 ) ) ↔ ( ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) ( .r ‘ 𝑅 ) 𝑧 ) = ( 𝑥 ( .r ‘ 𝑅 ) ( 𝑦 ( .r ‘ 𝑅 ) 𝑧 ) ) ) )
56 47 49 55 3imtr4d ⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) → ( ( 𝑥 · 𝑦 ) · 𝑧 ) = ( 𝑥 · ( 𝑦 · 𝑧 ) ) ) )
57 eldifi ⊢ ( 𝑥 ∈ ( 𝐵 ∖ { 0 } ) → 𝑥 ∈ 𝐵 )
58 eldifi ⊢ ( 𝑦 ∈ ( 𝐵 ∖ { 0 } ) → 𝑦 ∈ 𝐵 )
59 eldifi ⊢ ( 𝑧 ∈ ( 𝐵 ∖ { 0 } ) → 𝑧 ∈ 𝐵 )
60 57 58 59 3anim123i ⊢ ( ( 𝑥 ∈ ( 𝐵 ∖ { 0 } ) ∧ 𝑦 ∈ ( 𝐵 ∖ { 0 } ) ∧ 𝑧 ∈ ( 𝐵 ∖ { 0 } ) ) → ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) )
61 56 60 impel ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( 𝐵 ∖ { 0 } ) ∧ 𝑦 ∈ ( 𝐵 ∖ { 0 } ) ∧ 𝑧 ∈ ( 𝐵 ∖ { 0 } ) ) ) → ( ( 𝑥 · 𝑦 ) · 𝑧 ) = ( 𝑥 · ( 𝑦 · 𝑧 ) ) )
62 eqid ⊢ ( 1r ‘ 𝑅 ) = ( 1r ‘ 𝑅 )
63 15 62 ringidcl ⊢ ( 𝑅 ∈ Ring → ( 1r ‘ 𝑅 ) ∈ ( Base ‘ 𝑅 ) )
64 5 63 syl ⊢ ( 𝜑 → ( 1r ‘ 𝑅 ) ∈ ( Base ‘ 𝑅 ) )
65 64 4 1 3eltr4d ⊢ ( 𝜑 → 1 ∈ 𝐵 )
66 eldifsn ⊢ ( 1 ∈ ( 𝐵 ∖ { 0 } ) ↔ ( 1 ∈ 𝐵 ∧ 1 ≠ 0 ) )
67 65 7 66 sylanbrc ⊢ ( 𝜑 → 1 ∈ ( 𝐵 ∖ { 0 } ) )
68 15 22 62 ringlidm ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ) → ( ( 1r ‘ 𝑅 ) ( .r ‘ 𝑅 ) 𝑥 ) = 𝑥 )
69 68 ex ⊢ ( 𝑅 ∈ Ring → ( 𝑥 ∈ ( Base ‘ 𝑅 ) → ( ( 1r ‘ 𝑅 ) ( .r ‘ 𝑅 ) 𝑥 ) = 𝑥 ) )
70 5 69 syl ⊢ ( 𝜑 → ( 𝑥 ∈ ( Base ‘ 𝑅 ) → ( ( 1r ‘ 𝑅 ) ( .r ‘ 𝑅 ) 𝑥 ) = 𝑥 ) )
71 2 4 52 oveq123d ⊢ ( 𝜑 → ( 1 · 𝑥 ) = ( ( 1r ‘ 𝑅 ) ( .r ‘ 𝑅 ) 𝑥 ) )
72 71 eqeq1d ⊢ ( 𝜑 → ( ( 1 · 𝑥 ) = 𝑥 ↔ ( ( 1r ‘ 𝑅 ) ( .r ‘ 𝑅 ) 𝑥 ) = 𝑥 ) )
73 70 32 72 3imtr4d ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐵 → ( 1 · 𝑥 ) = 𝑥 ) )
74 73 imp ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → ( 1 · 𝑥 ) = 𝑥 )
75 74 adantrr ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑥 ≠ 0 ) ) → ( 1 · 𝑥 ) = 𝑥 )
76 27 75 sylan2b ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐵 ∖ { 0 } ) ) → ( 1 · 𝑥 ) = 𝑥 )
77 eldifsn ⊢ ( 𝐼 ∈ ( 𝐵 ∖ { 0 } ) ↔ ( 𝐼 ∈ 𝐵 ∧ 𝐼 ≠ 0 ) )
78 8 9 77 sylanbrc ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑥 ≠ 0 ) ) → 𝐼 ∈ ( 𝐵 ∖ { 0 } ) )
79 27 78 sylan2b ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐵 ∖ { 0 } ) ) → 𝐼 ∈ ( 𝐵 ∖ { 0 } ) )
80 27 10 sylan2b ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐵 ∖ { 0 } ) ) → ( 𝐼 · 𝑥 ) = 1 )
81 18 26 44 61 67 76 79 80 isgrpd ⊢ ( 𝜑 → ( ( mulGrp ‘ 𝑅 ) ↾s ( 𝐵 ∖ { 0 } ) ) ∈ Grp )
82 3 sneqd ⊢ ( 𝜑 → { 0 } = { ( 0g ‘ 𝑅 ) } )
83 1 82 difeq12d ⊢ ( 𝜑 → ( 𝐵 ∖ { 0 } ) = ( ( Base ‘ 𝑅 ) ∖ { ( 0g ‘ 𝑅 ) } ) )
84 83 oveq2d ⊢ ( 𝜑 → ( ( mulGrp ‘ 𝑅 ) ↾s ( 𝐵 ∖ { 0 } ) ) = ( ( mulGrp ‘ 𝑅 ) ↾s ( ( Base ‘ 𝑅 ) ∖ { ( 0g ‘ 𝑅 ) } ) ) )
85 84 eleq1d ⊢ ( 𝜑 → ( ( ( mulGrp ‘ 𝑅 ) ↾s ( 𝐵 ∖ { 0 } ) ) ∈ Grp ↔ ( ( mulGrp ‘ 𝑅 ) ↾s ( ( Base ‘ 𝑅 ) ∖ { ( 0g ‘ 𝑅 ) } ) ) ∈ Grp ) )
86 85 anbi2d ⊢ ( 𝜑 → ( ( 𝑅 ∈ Ring ∧ ( ( mulGrp ‘ 𝑅 ) ↾s ( 𝐵 ∖ { 0 } ) ) ∈ Grp ) ↔ ( 𝑅 ∈ Ring ∧ ( ( mulGrp ‘ 𝑅 ) ↾s ( ( Base ‘ 𝑅 ) ∖ { ( 0g ‘ 𝑅 ) } ) ) ∈ Grp ) ) )
87 5 81 86 mpbi2and ⊢ ( 𝜑 → ( 𝑅 ∈ Ring ∧ ( ( mulGrp ‘ 𝑅 ) ↾s ( ( Base ‘ 𝑅 ) ∖ { ( 0g ‘ 𝑅 ) } ) ) ∈ Grp ) )
88 eqid ⊢ ( 0g ‘ 𝑅 ) = ( 0g ‘ 𝑅 )
89 eqid ⊢ ( ( mulGrp ‘ 𝑅 ) ↾s ( ( Base ‘ 𝑅 ) ∖ { ( 0g ‘ 𝑅 ) } ) ) = ( ( mulGrp ‘ 𝑅 ) ↾s ( ( Base ‘ 𝑅 ) ∖ { ( 0g ‘ 𝑅 ) } ) )
90 15 88 89 isdrng2 ⊢ ( 𝑅 ∈ DivRing ↔ ( 𝑅 ∈ Ring ∧ ( ( mulGrp ‘ 𝑅 ) ↾s ( ( Base ‘ 𝑅 ) ∖ { ( 0g ‘ 𝑅 ) } ) ) ∈ Grp ) )
91 87 90 sylibr ⊢ ( 𝜑 → 𝑅 ∈ DivRing )