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 \land R \in DivRing) \to S \in DivRing$

Proof

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

Metamath Proof Explorer

Theorem ricdrng1

Proof