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 𝑆 ) ∧ 𝑅 ∈ CRing ) → 𝑆 = ( 𝑆 ↾s ( 𝑓 “ ( Base ‘ 𝑅 ) ) ) ) |
16 |
|
eqid |
⊢ ( 𝑆 ↾s ( 𝑓 “ ( Base ‘ 𝑅 ) ) ) = ( 𝑆 ↾s ( 𝑓 “ ( Base ‘ 𝑅 ) ) ) |
17 |
|
rimrhm |
⊢ ( 𝑓 ∈ ( 𝑅 RingIso 𝑆 ) → 𝑓 ∈ ( 𝑅 RingHom 𝑆 ) ) |
18 |
17
|
adantr |
⊢ ( ( 𝑓 ∈ ( 𝑅 RingIso 𝑆 ) ∧ 𝑅 ∈ CRing ) → 𝑓 ∈ ( 𝑅 RingHom 𝑆 ) ) |
19 |
|
simpr |
⊢ ( ( 𝑓 ∈ ( 𝑅 RingIso 𝑆 ) ∧ 𝑅 ∈ CRing ) → 𝑅 ∈ CRing ) |
20 |
19
|
crngringd |
⊢ ( ( 𝑓 ∈ ( 𝑅 RingIso 𝑆 ) ∧ 𝑅 ∈ CRing ) → 𝑅 ∈ Ring ) |
21 |
4
|
subrgid |
⊢ ( 𝑅 ∈ Ring → ( Base ‘ 𝑅 ) ∈ ( SubRing ‘ 𝑅 ) ) |
22 |
20 21
|
syl |
⊢ ( ( 𝑓 ∈ ( 𝑅 RingIso 𝑆 ) ∧ 𝑅 ∈ CRing ) → ( Base ‘ 𝑅 ) ∈ ( SubRing ‘ 𝑅 ) ) |
23 |
16 18 19 22
|
imacrhmcl |
⊢ ( ( 𝑓 ∈ ( 𝑅 RingIso 𝑆 ) ∧ 𝑅 ∈ CRing ) → ( 𝑆 ↾s ( 𝑓 “ ( Base ‘ 𝑅 ) ) ) ∈ CRing ) |
24 |
15 23
|
eqeltrd |
⊢ ( ( 𝑓 ∈ ( 𝑅 RingIso 𝑆 ) ∧ 𝑅 ∈ CRing ) → 𝑆 ∈ CRing ) |
25 |
24
|
ex |
⊢ ( 𝑓 ∈ ( 𝑅 RingIso 𝑆 ) → ( 𝑅 ∈ CRing → 𝑆 ∈ CRing ) ) |
26 |
25
|
exlimiv |
⊢ ( ∃ 𝑓 𝑓 ∈ ( 𝑅 RingIso 𝑆 ) → ( 𝑅 ∈ CRing → 𝑆 ∈ CRing ) ) |
27 |
26
|
imp |
⊢ ( ( ∃ 𝑓 𝑓 ∈ ( 𝑅 RingIso 𝑆 ) ∧ 𝑅 ∈ CRing ) → 𝑆 ∈ CRing ) |
28 |
3 27
|
sylanb |
⊢ ( ( 𝑅 ≃𝑟 𝑆 ∧ 𝑅 ∈ CRing ) → 𝑆 ∈ CRing ) |