Database
SUPPLEMENTARY MATERIAL (USERS' MATHBOXES)
Mathbox for Jeff Madsen
Ring homomorphisms
risc
Next ⟩
risci
Metamath Proof Explorer
Ascii
Unicode
Theorem
risc
Description:
The ring isomorphism relation.
(Contributed by
Jeff Madsen
, 16-Jun-2011)
Ref
Expression
Assertion
risc
⊢
R
∈
RingOps
∧
S
∈
RingOps
→
R
≃
𝑟
S
↔
∃
f
f
∈
R
RngIso
S
Proof
Step
Hyp
Ref
Expression
1
isriscg
⊢
R
∈
RingOps
∧
S
∈
RingOps
→
R
≃
𝑟
S
↔
R
∈
RingOps
∧
S
∈
RingOps
∧
∃
f
f
∈
R
RngIso
S
2
1
bianabs
⊢
R
∈
RingOps
∧
S
∈
RingOps
→
R
≃
𝑟
S
↔
∃
f
f
∈
R
RngIso
S