Database
SUPPLEMENTARY MATERIAL (USERS' MATHBOXES)
Mathbox for Steven Nguyen
Structures
ricsym
Next ⟩
rictr
Metamath Proof Explorer
Ascii
Unicode
Theorem
ricsym
Description:
Ring isomorphism is symmetric.
(Contributed by
SN
, 10-Jan-2025)
Ref
Expression
Assertion
ricsym
⊢
R
≃
𝑟
S
→
S
≃
𝑟
R
Proof
Step
Hyp
Ref
Expression
1
brric
⊢
R
≃
𝑟
S
↔
R
RingIso
S
≠
∅
2
n0
⊢
R
RingIso
S
≠
∅
↔
∃
f
f
∈
R
RingIso
S
3
rimcnv
⊢
f
∈
R
RingIso
S
→
f
-1
∈
S
RingIso
R
4
brrici
⊢
f
-1
∈
S
RingIso
R
→
S
≃
𝑟
R
5
3
4
syl
⊢
f
∈
R
RingIso
S
→
S
≃
𝑟
R
6
5
exlimiv
⊢
∃
f
f
∈
R
RingIso
S
→
S
≃
𝑟
R
7
2
6
sylbi
⊢
R
RingIso
S
≠
∅
→
S
≃
𝑟
R
8
1
7
sylbi
⊢
R
≃
𝑟
S
→
S
≃
𝑟
R