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 φ 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.j φ x B x 0 ˙ I 0 ˙
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.j φ x B x 0 ˙ I 0 ˙
10 isdrngd.k φ x B x 0 ˙ I · ˙ x = 1 ˙
11 difss B 0 ˙ B
12 11 1 sseqtrid φ B 0 ˙ Base R
13 eqid mulGrp R 𝑠 B 0 ˙ = mulGrp R 𝑠 B 0 ˙
14 eqid mulGrp R = mulGrp R
15 eqid Base R = Base R
16 14 15 mgpbas Base R = Base mulGrp R
17 13 16 ressbas2 B 0 ˙ Base R B 0 ˙ = Base mulGrp R 𝑠 B 0 ˙
18 12 17 syl φ B 0 ˙ = Base mulGrp R 𝑠 B 0 ˙
19 fvex Base R V
20 1 19 eqeltrdi φ B V
21 difexg B V B 0 ˙ V
22 eqid R = R
23 14 22 mgpplusg R = + mulGrp R
24 13 23 ressplusg B 0 ˙ V R = + mulGrp R 𝑠 B 0 ˙
25 20 21 24 3syl φ R = + mulGrp R 𝑠 B 0 ˙
26 2 25 eqtrd φ · ˙ = + mulGrp R 𝑠 B 0 ˙
27 eldifsn x B 0 ˙ x B x 0 ˙
28 eldifsn y B 0 ˙ y B y 0 ˙
29 15 22 ringcl R Ring x Base R y Base R x R y Base R
30 5 29 syl3an1 φ x Base R y Base R x R y Base R
31 30 3expib φ x Base R y Base R x R y Base R
32 1 eleq2d φ x B x Base R
33 1 eleq2d φ y B y Base R
34 32 33 anbi12d φ x B y B x Base R y Base R
35 2 oveqd φ x · ˙ y = x R y
36 35 1 eleq12d φ x · ˙ y B x R y Base R
37 31 34 36 3imtr4d φ x B y B x · ˙ y B
38 37 3impib φ x B y B x · ˙ y B
39 38 3adant2r φ x B x 0 ˙ y B x · ˙ y B
40 39 3adant3r φ x B x 0 ˙ y B y 0 ˙ x · ˙ y B
41 eldifsn x · ˙ y B 0 ˙ x · ˙ y B x · ˙ y 0 ˙
42 40 6 41 sylanbrc φ x B x 0 ˙ y B y 0 ˙ x · ˙ y B 0 ˙
43 28 42 syl3an3b φ x B x 0 ˙ y B 0 ˙ x · ˙ y B 0 ˙
44 27 43 syl3an2b φ x B 0 ˙ y B 0 ˙ x · ˙ y B 0 ˙
45 15 22 ringass R Ring x Base R y Base R z Base R x R y R z = x R y R z
46 45 ex R Ring x Base R y Base R z Base R x R y R z = x R y R z
47 5 46 syl φ x Base R y Base R z Base R x R y R z = x R y R z
48 1 eleq2d φ z B z Base R
49 32 33 48 3anbi123d φ x B y B z B x Base R y Base R z Base R
50 eqidd φ z = z
51 2 35 50 oveq123d φ x · ˙ y · ˙ z = x R y R z
52 eqidd φ x = x
53 2 oveqd φ y · ˙ z = y R z
54 2 52 53 oveq123d φ x · ˙ y · ˙ z = x R y R z
55 51 54 eqeq12d φ x · ˙ y · ˙ z = x · ˙ y · ˙ z x R y R z = x R y R z
56 47 49 55 3imtr4d φ x B y B z B x · ˙ y · ˙ z = x · ˙ y · ˙ z
57 eldifi x B 0 ˙ x B
58 eldifi y B 0 ˙ y B
59 eldifi z B 0 ˙ z B
60 57 58 59 3anim123i x B 0 ˙ y B 0 ˙ z B 0 ˙ x B y B z B
61 56 60 impel φ x B 0 ˙ y B 0 ˙ z B 0 ˙ x · ˙ y · ˙ z = x · ˙ y · ˙ z
62 eqid 1 R = 1 R
63 15 62 ringidcl R Ring 1 R Base R
64 5 63 syl φ 1 R Base R
65 64 4 1 3eltr4d φ 1 ˙ B
66 eldifsn 1 ˙ B 0 ˙ 1 ˙ B 1 ˙ 0 ˙
67 65 7 66 sylanbrc φ 1 ˙ B 0 ˙
68 15 22 62 ringlidm R Ring x Base R 1 R R x = x
69 68 ex R Ring x Base R 1 R R x = x
70 5 69 syl φ x Base R 1 R R x = x
71 2 4 52 oveq123d φ 1 ˙ · ˙ x = 1 R R x
72 71 eqeq1d φ 1 ˙ · ˙ x = x 1 R R x = x
73 70 32 72 3imtr4d φ x B 1 ˙ · ˙ x = x
74 73 imp φ x B 1 ˙ · ˙ x = x
75 74 adantrr φ x B x 0 ˙ 1 ˙ · ˙ x = x
76 27 75 sylan2b φ x B 0 ˙ 1 ˙ · ˙ x = x
77 eldifsn I B 0 ˙ I B I 0 ˙
78 8 9 77 sylanbrc φ x B x 0 ˙ I B 0 ˙
79 27 78 sylan2b φ x B 0 ˙ I B 0 ˙
80 27 10 sylan2b φ x B 0 ˙ I · ˙ x = 1 ˙
81 18 26 44 61 67 76 79 80 isgrpd φ mulGrp R 𝑠 B 0 ˙ Grp
82 3 sneqd φ 0 ˙ = 0 R
83 1 82 difeq12d φ B 0 ˙ = Base R 0 R
84 83 oveq2d φ mulGrp R 𝑠 B 0 ˙ = mulGrp R 𝑠 Base R 0 R
85 84 eleq1d φ mulGrp R 𝑠 B 0 ˙ Grp mulGrp R 𝑠 Base R 0 R Grp
86 85 anbi2d φ R Ring mulGrp R 𝑠 B 0 ˙ Grp R Ring mulGrp R 𝑠 Base R 0 R Grp
87 5 81 86 mpbi2and φ R Ring mulGrp R 𝑠 Base R 0 R Grp
88 eqid 0 R = 0 R
89 eqid mulGrp R 𝑠 Base R 0 R = mulGrp R 𝑠 Base R 0 R
90 15 88 89 isdrng2 R DivRing R Ring mulGrp R 𝑠 Base R 0 R Grp
91 87 90 sylibr φ R DivRing