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 isdrngrd for the characterization using right-inverses. (Contributed by NM, 2-Aug-2013) Remove hypothesis. (Revised by SN, 19-Feb-2025)

Ref Expression
Hypotheses isdrngd.b φ B = Base R
isdrngd.t φ · ˙ = R
isdrngd.z φ 0 ˙ = 0 R
isdrngd.u φ 1 ˙ = 1 R
isdrngd.r φ R Ring
isdrngd.n φ x B x 0 ˙ y B y 0 ˙ x · ˙ y 0 ˙
isdrngd.o φ 1 ˙ 0 ˙
isdrngd.i φ x B x 0 ˙ I B
isdrngd.k φ x B x 0 ˙ I · ˙ x = 1 ˙
Assertion isdrngd φ R DivRing

Proof

Step Hyp Ref Expression
1 isdrngd.b φ B = Base R
2 isdrngd.t φ · ˙ = R
3 isdrngd.z φ 0 ˙ = 0 R
4 isdrngd.u φ 1 ˙ = 1 R
5 isdrngd.r φ R Ring
6 isdrngd.n φ x B x 0 ˙ y B y 0 ˙ x · ˙ y 0 ˙
7 isdrngd.o φ 1 ˙ 0 ˙
8 isdrngd.i φ x B x 0 ˙ I B
9 isdrngd.k φ x B x 0 ˙ I · ˙ x = 1 ˙
10 difss B 0 ˙ B
11 10 1 sseqtrid φ B 0 ˙ Base R
12 eqid mulGrp R 𝑠 B 0 ˙ = mulGrp R 𝑠 B 0 ˙
13 eqid mulGrp R = mulGrp R
14 eqid Base R = Base R
15 13 14 mgpbas Base R = Base mulGrp R
16 12 15 ressbas2 B 0 ˙ Base R B 0 ˙ = Base mulGrp R 𝑠 B 0 ˙
17 11 16 syl φ B 0 ˙ = Base mulGrp R 𝑠 B 0 ˙
18 fvex Base R V
19 1 18 eqeltrdi φ B V
20 difexg B V B 0 ˙ V
21 eqid R = R
22 13 21 mgpplusg R = + mulGrp R
23 12 22 ressplusg B 0 ˙ V R = + mulGrp R 𝑠 B 0 ˙
24 19 20 23 3syl φ R = + mulGrp R 𝑠 B 0 ˙
25 2 24 eqtrd φ · ˙ = + mulGrp R 𝑠 B 0 ˙
26 eldifsn x B 0 ˙ x B x 0 ˙
27 eldifsn y B 0 ˙ y B y 0 ˙
28 14 21 ringcl R Ring x Base R y Base R x R y Base R
29 5 28 syl3an1 φ x Base R y Base R x R y Base R
30 29 3expib φ x Base R y Base R x R y Base R
31 1 eleq2d φ x B x Base R
32 1 eleq2d φ y B y Base R
33 31 32 anbi12d φ x B y B x Base R y Base R
34 2 oveqd φ x · ˙ y = x R y
35 34 1 eleq12d φ x · ˙ y B x R y Base R
36 30 33 35 3imtr4d φ x B y B x · ˙ y B
37 36 3impib φ x B y B x · ˙ y B
38 37 3adant2r φ x B x 0 ˙ y B x · ˙ y B
39 38 3adant3r φ x B x 0 ˙ y B y 0 ˙ x · ˙ y B
40 eldifsn x · ˙ y B 0 ˙ x · ˙ y B x · ˙ y 0 ˙
41 39 6 40 sylanbrc φ x B x 0 ˙ y B y 0 ˙ x · ˙ y B 0 ˙
42 27 41 syl3an3b φ x B x 0 ˙ y B 0 ˙ x · ˙ y B 0 ˙
43 26 42 syl3an2b φ x B 0 ˙ y B 0 ˙ x · ˙ y B 0 ˙
44 14 21 ringass R Ring x Base R y Base R z Base R x R y R z = x R y R z
45 44 ex R Ring x Base R y Base R z Base R x R y R z = x R y R z
46 5 45 syl φ x Base R y Base R z Base R x R y R z = x R y R z
47 1 eleq2d φ z B z Base R
48 31 32 47 3anbi123d φ x B y B z B x Base R y Base R z Base R
49 eqidd φ z = z
50 2 34 49 oveq123d φ x · ˙ y · ˙ z = x R y R z
51 eqidd φ x = x
52 2 oveqd φ y · ˙ z = y R z
53 2 51 52 oveq123d φ x · ˙ y · ˙ z = x R y R z
54 50 53 eqeq12d φ x · ˙ y · ˙ z = x · ˙ y · ˙ z x R y R z = x R y R z
55 46 48 54 3imtr4d φ x B y B z B x · ˙ y · ˙ z = x · ˙ y · ˙ z
56 eldifi x B 0 ˙ x B
57 eldifi y B 0 ˙ y B
58 eldifi z B 0 ˙ z B
59 56 57 58 3anim123i x B 0 ˙ y B 0 ˙ z B 0 ˙ x B y B z B
60 55 59 impel φ x B 0 ˙ y B 0 ˙ z B 0 ˙ x · ˙ y · ˙ z = x · ˙ y · ˙ z
61 eqid 1 R = 1 R
62 14 61 ringidcl R Ring 1 R Base R
63 5 62 syl φ 1 R Base R
64 63 4 1 3eltr4d φ 1 ˙ B
65 eldifsn 1 ˙ B 0 ˙ 1 ˙ B 1 ˙ 0 ˙
66 64 7 65 sylanbrc φ 1 ˙ B 0 ˙
67 14 21 61 ringlidm R Ring x Base R 1 R R x = x
68 67 ex R Ring x Base R 1 R R x = x
69 5 68 syl φ x Base R 1 R R x = x
70 2 4 51 oveq123d φ 1 ˙ · ˙ x = 1 R R x
71 70 eqeq1d φ 1 ˙ · ˙ x = x 1 R R x = x
72 69 31 71 3imtr4d φ x B 1 ˙ · ˙ x = x
73 72 imp φ x B 1 ˙ · ˙ x = x
74 73 adantrr φ x B x 0 ˙ 1 ˙ · ˙ x = x
75 26 74 sylan2b φ x B 0 ˙ 1 ˙ · ˙ x = x
76 7 adantr φ x B x 0 ˙ 1 ˙ 0 ˙
77 simpr φ x B x 0 ˙ I = 0 ˙ I = 0 ˙
78 77 oveq1d φ x B x 0 ˙ I = 0 ˙ I · ˙ x = 0 ˙ · ˙ x
79 9 adantr φ x B x 0 ˙ I = 0 ˙ I · ˙ x = 1 ˙
80 31 biimpa φ x B x Base R
81 80 adantrr φ x B x 0 ˙ x Base R
82 eqid 0 R = 0 R
83 14 21 82 ringlz R Ring x Base R 0 R R x = 0 R
84 5 81 83 syl2an2r φ x B x 0 ˙ 0 R R x = 0 R
85 2 3 51 oveq123d φ 0 ˙ · ˙ x = 0 R R x
86 85 adantr φ x B x 0 ˙ 0 ˙ · ˙ x = 0 R R x
87 3 adantr φ x B x 0 ˙ 0 ˙ = 0 R
88 84 86 87 3eqtr4d φ x B x 0 ˙ 0 ˙ · ˙ x = 0 ˙
89 88 adantr φ x B x 0 ˙ I = 0 ˙ 0 ˙ · ˙ x = 0 ˙
90 78 79 89 3eqtr3d φ x B x 0 ˙ I = 0 ˙ 1 ˙ = 0 ˙
91 76 90 mteqand φ x B x 0 ˙ I 0 ˙
92 eldifsn I B 0 ˙ I B I 0 ˙
93 8 91 92 sylanbrc φ x B x 0 ˙ I B 0 ˙
94 26 93 sylan2b φ x B 0 ˙ I B 0 ˙
95 26 9 sylan2b φ x B 0 ˙ I · ˙ x = 1 ˙
96 17 25 43 60 66 75 94 95 isgrpd φ mulGrp R 𝑠 B 0 ˙ Grp
97 3 sneqd φ 0 ˙ = 0 R
98 1 97 difeq12d φ B 0 ˙ = Base R 0 R
99 98 oveq2d φ mulGrp R 𝑠 B 0 ˙ = mulGrp R 𝑠 Base R 0 R
100 99 eleq1d φ mulGrp R 𝑠 B 0 ˙ Grp mulGrp R 𝑠 Base R 0 R Grp
101 100 anbi2d φ R Ring mulGrp R 𝑠 B 0 ˙ Grp R Ring mulGrp R 𝑠 Base R 0 R Grp
102 5 96 101 mpbi2and φ R Ring mulGrp R 𝑠 Base R 0 R Grp
103 eqid mulGrp R 𝑠 Base R 0 R = mulGrp R 𝑠 Base R 0 R
104 14 82 103 isdrng2 R DivRing R Ring mulGrp R 𝑠 Base R 0 R Grp
105 102 104 sylibr φ R DivRing