Database
BASIC ALGEBRAIC STRUCTURES
Rings
Ring homomorphisms
rimf1o
Next ⟩
rimrhmOLD
Metamath Proof Explorer
Ascii
Unicode
Theorem
rimf1o
Description:
An isomorphism of rings is a bijection.
(Contributed by
AV
, 22-Oct-2019)
Ref
Expression
Hypotheses
rhmf1o.b
⊢
B
=
Base
R
rhmf1o.c
⊢
C
=
Base
S
Assertion
rimf1o
⊢
F
∈
R
RingIso
S
→
F
:
B
⟶
1-1 onto
C
Proof
Step
Hyp
Ref
Expression
1
rhmf1o.b
⊢
B
=
Base
R
2
rhmf1o.c
⊢
C
=
Base
S
3
1
2
isrim
⊢
F
∈
R
RingIso
S
↔
F
∈
R
RingHom
S
∧
F
:
B
⟶
1-1 onto
C
4
3
simprbi
⊢
F
∈
R
RingIso
S
→
F
:
B
⟶
1-1 onto
C