Metamath Proof Explorer

Theorem isriscg

Description: The ring isomorphism relation. (Contributed by Jeff Madsen, 16-Jun-2011)

		Ref	Expression
	Assertion	isriscg	$⊢ (R \in A \land S \in B) \to (R ≃_{𝑟} S \leftrightarrow ((R \in RingOps \land S \in RingOps) \land \exists f f \in (R RingOpsIso S)))$

Proof

Step	Hyp	Ref	Expression
1		eleq1	$⊢ r = R \to (r \in RingOps \leftrightarrow R \in RingOps)$
2	1	anbi1d	$⊢ r = R \to ((r \in RingOps \land s \in RingOps) \leftrightarrow (R \in RingOps \land s \in RingOps))$
3		oveq1	$⊢ r = R \to r RingOpsIso s = R RingOpsIso s$
4	3	eleq2d	$⊢ r = R \to (f \in (r RingOpsIso s) \leftrightarrow f \in (R RingOpsIso s))$
5	4	exbidv	$⊢ r = R \to (\exists f f \in (r RingOpsIso s) \leftrightarrow \exists f f \in (R RingOpsIso s))$
6	2 5	anbi12d	$⊢ r = R \to (((r \in RingOps \land s \in RingOps) \land \exists f f \in (r RingOpsIso s)) \leftrightarrow ((R \in RingOps \land s \in RingOps) \land \exists f f \in (R RingOpsIso s)))$
7		eleq1	$⊢ s = S \to (s \in RingOps \leftrightarrow S \in RingOps)$
8	7	anbi2d	$⊢ s = S \to ((R \in RingOps \land s \in RingOps) \leftrightarrow (R \in RingOps \land S \in RingOps))$
9		oveq2	$⊢ s = S \to R RingOpsIso s = R RingOpsIso S$
10	9	eleq2d	$⊢ s = S \to (f \in (R RingOpsIso s) \leftrightarrow f \in (R RingOpsIso S))$
11	10	exbidv	$⊢ s = S \to (\exists f f \in (R RingOpsIso s) \leftrightarrow \exists f f \in (R RingOpsIso S))$
12	8 11	anbi12d	$⊢ s = S \to (((R \in RingOps \land s \in RingOps) \land \exists f f \in (R RingOpsIso s)) \leftrightarrow ((R \in RingOps \land S \in RingOps) \land \exists f f \in (R RingOpsIso S)))$
13		df-risc	$⊢ ≃_{𝑟} = \{⟨r, s⟩ \| ((r \in RingOps \land s \in RingOps) \land \exists f f \in (r RingOpsIso s))\}$
14	6 12 13	brabg	$⊢ (R \in A \land S \in B) \to (R ≃_{𝑟} S \leftrightarrow ((R \in RingOps \land S \in RingOps) \land \exists f f \in (R RingOpsIso S)))$