This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ( ( 𝑅 ≃𝑟 𝑆 ∧ 𝑅 ∈ 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 )