This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem ricgic

Description: If two rings are (ring) isomorphic, their additive groups are (group) isomorphic. (Contributed by AV, 24-Dec-2019)

		Ref	Expression
	Assertion	ricgic	$⊢ R ≃_{𝑟} S \to R ≃_{𝑔} S$

Step	Hyp	Ref	Expression
1		brric2	$⊢ R ≃_{𝑟} S \leftrightarrow ((R \in Ring \land S \in Ring) \land \exists f f \in (R RingIso S))$
2		rimgim	$⊢ f \in (R RingIso S) \to f \in (R GrpIso S)$
3		brgici	$⊢ f \in (R GrpIso S) \to R ≃_{𝑔} S$
4	2 3	syl	$⊢ f \in (R RingIso S) \to R ≃_{𝑔} S$
5	4	exlimiv	$⊢ \exists f f \in (R RingIso S) \to R ≃_{𝑔} S$
6	1 5	simplbiim	$⊢ R ≃_{𝑟} S \to R ≃_{𝑔} S$