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	⊢ ( 𝑅 ≃𝑟 𝑆 → 𝑅 ≃𝑔 𝑆 )

Proof

Step	Hyp	Ref	Expression
1		isbrric2	⊢ ( 𝑅 ≃𝑟 𝑆 ↔ ( ( 𝑅 ∈ Ring ∧ 𝑆 ∈ Ring ) ∧ ∃ 𝑓 𝑓 ∈ ( 𝑅 RingIso 𝑆 ) ) )
2		rimgim	⊢ ( 𝑓 ∈ ( 𝑅 RingIso 𝑆 ) → 𝑓 ∈ ( 𝑅 GrpIso 𝑆 ) )
3		brgici	⊢ ( 𝑓 ∈ ( 𝑅 GrpIso 𝑆 ) → 𝑅 ≃𝑔 𝑆 )
4	2 3	syl	⊢ ( 𝑓 ∈ ( 𝑅 RingIso 𝑆 ) → 𝑅 ≃𝑔 𝑆 )
5	4	exlimiv	⊢ ( ∃ 𝑓 𝑓 ∈ ( 𝑅 RingIso 𝑆 ) → 𝑅 ≃𝑔 𝑆 )
6	1 5	simplbiim	⊢ ( 𝑅 ≃𝑟 𝑆 → 𝑅 ≃𝑔 𝑆 )