Step |
Hyp |
Ref |
Expression |
1 |
|
brric |
⊢ ( 𝑅 ≃𝑟 𝑆 ↔ ( 𝑅 RingIso 𝑆 ) ≠ ∅ ) |
2 |
|
n0 |
⊢ ( ( 𝑅 RingIso 𝑆 ) ≠ ∅ ↔ ∃ 𝑓 𝑓 ∈ ( 𝑅 RingIso 𝑆 ) ) |
3 |
|
rimrhm |
⊢ ( 𝑓 ∈ ( 𝑅 RingIso 𝑆 ) → 𝑓 ∈ ( 𝑅 RingHom 𝑆 ) ) |
4 |
|
eqid |
⊢ ( mulGrp ‘ 𝑅 ) = ( mulGrp ‘ 𝑅 ) |
5 |
|
eqid |
⊢ ( mulGrp ‘ 𝑆 ) = ( mulGrp ‘ 𝑆 ) |
6 |
4 5
|
isrhm |
⊢ ( 𝑓 ∈ ( 𝑅 RingHom 𝑆 ) ↔ ( ( 𝑅 ∈ Ring ∧ 𝑆 ∈ Ring ) ∧ ( 𝑓 ∈ ( 𝑅 GrpHom 𝑆 ) ∧ 𝑓 ∈ ( ( mulGrp ‘ 𝑅 ) MndHom ( mulGrp ‘ 𝑆 ) ) ) ) ) |
7 |
6
|
simplbi |
⊢ ( 𝑓 ∈ ( 𝑅 RingHom 𝑆 ) → ( 𝑅 ∈ Ring ∧ 𝑆 ∈ Ring ) ) |
8 |
3 7
|
syl |
⊢ ( 𝑓 ∈ ( 𝑅 RingIso 𝑆 ) → ( 𝑅 ∈ Ring ∧ 𝑆 ∈ Ring ) ) |
9 |
8
|
exlimiv |
⊢ ( ∃ 𝑓 𝑓 ∈ ( 𝑅 RingIso 𝑆 ) → ( 𝑅 ∈ Ring ∧ 𝑆 ∈ Ring ) ) |
10 |
9
|
pm4.71ri |
⊢ ( ∃ 𝑓 𝑓 ∈ ( 𝑅 RingIso 𝑆 ) ↔ ( ( 𝑅 ∈ Ring ∧ 𝑆 ∈ Ring ) ∧ ∃ 𝑓 𝑓 ∈ ( 𝑅 RingIso 𝑆 ) ) ) |
11 |
1 2 10
|
3bitri |
⊢ ( 𝑅 ≃𝑟 𝑆 ↔ ( ( 𝑅 ∈ Ring ∧ 𝑆 ∈ Ring ) ∧ ∃ 𝑓 𝑓 ∈ ( 𝑅 RingIso 𝑆 ) ) ) |