Theorem ricdrng1

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

	Ref	Expression
Assertion	ricdrng1	⊢ ( ( 𝑅 ≃𝑟 𝑆 ∧ 𝑅 ∈ DivRing ) → 𝑆 ∈ DivRing )

Proof

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