Database
SUPPLEMENTARY MATERIAL (USERS' MATHBOXES)
Mathbox for Jeff Madsen
Ring homomorphisms
risci
Next ⟩
riscer
Metamath Proof Explorer
Ascii
Unicode
Theorem
risci
Description:
Determine that two rings are isomorphic.
(Contributed by
Jeff Madsen
, 16-Jun-2011)
Ref
Expression
Assertion
risci
⊢
R
∈
RingOps
∧
S
∈
RingOps
∧
F
∈
R
RngIso
S
→
R
≃
𝑟
S
Proof
Step
Hyp
Ref
Expression
1
elex2
⊢
F
∈
R
RngIso
S
→
∃
f
f
∈
R
RngIso
S
2
risc
⊢
R
∈
RingOps
∧
S
∈
RingOps
→
R
≃
𝑟
S
↔
∃
f
f
∈
R
RngIso
S
3
1
2
syl5ibr
⊢
R
∈
RingOps
∧
S
∈
RingOps
→
F
∈
R
RngIso
S
→
R
≃
𝑟
S
4
3
3impia
⊢
R
∈
RingOps
∧
S
∈
RingOps
∧
F
∈
R
RngIso
S
→
R
≃
𝑟
S