Database
BASIC ALGEBRAIC STRUCTURES
Rings
Ring homomorphisms
brrici
Next ⟩
brric2
Metamath Proof Explorer
Ascii
Unicode
Theorem
brrici
Description:
Prove isomorphic by an explicit isomorphism.
(Contributed by
SN
, 10-Jan-2025)
Ref
Expression
Assertion
brrici
⊢
F
∈
R
RingIso
S
→
R
≃
𝑟
S
Proof
Step
Hyp
Ref
Expression
1
ne0i
⊢
F
∈
R
RingIso
S
→
R
RingIso
S
≠
∅
2
brric
⊢
R
≃
𝑟
S
↔
R
RingIso
S
≠
∅
3
1
2
sylibr
⊢
F
∈
R
RingIso
S
→
R
≃
𝑟
S