Metamath Proof Explorer

Theorem isrisc

Description: Obsolete theorem, use isbrric2 instead. The ring isomorphism relation. (Contributed by Jeff Madsen, 16-Jun-2011) (Proof modification is discouraged.) (New usage is discouraged.)

	Ref	Expression
Hypotheses	isrisc.1	$⊢ R \in V$
	isrisc.2	$⊢ S \in V$
Assertion	isrisc	$⊢ R ≃_{𝑟} S \leftrightarrow ((R \in RingOps \land S \in RingOps) \land \exists f f \in (R RingOpsIso S))$

Proof

Step	Hyp	Ref	Expression
1		isrisc.1	$⊢ R \in V$
2		isrisc.2	$⊢ S \in V$
3		isriscg	$⊢ (R \in V \land S \in V) \to (R ≃_{𝑟} S \leftrightarrow ((R \in RingOps \land S \in RingOps) \land \exists f f \in (R RingOpsIso S)))$
4	1 2 3	mp2an	$⊢ R ≃_{𝑟} S \leftrightarrow ((R \in RingOps \land S \in RingOps) \land \exists f f \in (R RingOpsIso S))$