Metamath Proof Explorer


Theorem ricdrng1

Description: A ring isomorphism maps a division ring to a division ring. (Contributed by SN, 18-Feb-2025)

Ref Expression
Assertion ricdrng1 R 𝑟 S R DivRing S DivRing

Proof

Step Hyp Ref Expression
1 brric R 𝑟 S R RingIso S
2 n0 R RingIso S f f R RingIso S
3 1 2 bitri R 𝑟 S f f R RingIso S
4 eqid Base R = Base R
5 eqid Base S = Base S
6 4 5 rimf1o f R RingIso S f : Base R 1-1 onto Base S
7 f1ofo f : Base R 1-1 onto Base S f : Base R onto Base S
8 foima f : Base R onto Base S f Base R = Base S
9 6 7 8 3syl f R RingIso S f Base R = Base S
10 9 oveq2d f R RingIso S S 𝑠 f Base R = S 𝑠 Base S
11 rimrcl2 f R RingIso S S Ring
12 5 ressid S Ring S 𝑠 Base S = S
13 11 12 syl f R RingIso S S 𝑠 Base S = S
14 10 13 eqtr2d f R RingIso S S = S 𝑠 f Base R
15 14 adantr f R RingIso S R DivRing S = S 𝑠 f Base R
16 eqid S 𝑠 f Base R = S 𝑠 f Base R
17 eqid 0 S = 0 S
18 rimrhm f R RingIso S f R RingHom S
19 18 adantr f R RingIso S R DivRing f R RingHom S
20 4 sdrgid R DivRing Base R SubDRing R
21 20 adantl f R RingIso S R DivRing Base R SubDRing R
22 forn f : Base R onto Base S ran f = Base S
23 6 7 22 3syl f R RingIso S ran f = Base S
24 23 adantr f R RingIso S R DivRing ran f = Base S
25 rhmrcl2 f R RingHom S S Ring
26 eqid 1 S = 1 S
27 5 26 ringidcl S Ring 1 S Base S
28 18 25 27 3syl f R RingIso S 1 S Base S
29 eqid 0 R = 0 R
30 eqid 1 R = 1 R
31 29 30 drngunz R DivRing 1 R 0 R
32 31 adantl f R RingIso S R DivRing 1 R 0 R
33 f1of1 f : Base R 1-1 onto Base S f : Base R 1-1 Base S
34 6 33 syl f R RingIso S f : Base R 1-1 Base S
35 drngring R DivRing R Ring
36 4 30 ringidcl R Ring 1 R Base R
37 35 36 syl R DivRing 1 R Base R
38 4 29 ring0cl R Ring 0 R Base R
39 35 38 syl R DivRing 0 R Base R
40 37 39 jca R DivRing 1 R Base R 0 R Base R
41 f1veqaeq f : Base R 1-1 Base S 1 R Base R 0 R Base R f 1 R = f 0 R 1 R = 0 R
42 34 40 41 syl2an f R RingIso S R DivRing f 1 R = f 0 R 1 R = 0 R
43 42 imp f R RingIso S R DivRing f 1 R = f 0 R 1 R = 0 R
44 32 43 mteqand f R RingIso S R DivRing f 1 R f 0 R
45 30 26 rhm1 f R RingHom S f 1 R = 1 S
46 19 45 syl f R RingIso S R DivRing f 1 R = 1 S
47 rhmghm f R RingHom S f R GrpHom S
48 29 17 ghmid f R GrpHom S f 0 R = 0 S
49 19 47 48 3syl f R RingIso S R DivRing f 0 R = 0 S
50 44 46 49 3netr3d f R RingIso S R DivRing 1 S 0 S
51 nelsn 1 S 0 S ¬ 1 S 0 S
52 50 51 syl f R RingIso S R DivRing ¬ 1 S 0 S
53 nelne1 1 S Base S ¬ 1 S 0 S Base S 0 S
54 28 52 53 syl2an2r f R RingIso S R DivRing Base S 0 S
55 24 54 eqnetrd f R RingIso S R DivRing ran f 0 S
56 16 17 19 21 55 imadrhmcl f R RingIso S R DivRing S 𝑠 f Base R DivRing
57 15 56 eqeltrd f R RingIso S R DivRing S DivRing
58 57 ex f R RingIso S R DivRing S DivRing
59 58 exlimiv f f R RingIso S R DivRing S DivRing
60 59 imp f f R RingIso S R DivRing S DivRing
61 3 60 sylanb R 𝑟 S R DivRing S DivRing