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 RngIso S)))$

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 RngIso s = R RngIso s$
4	3	eleq2d	$⊢ r = R \to (f \in (r RngIso s) \leftrightarrow f \in (R RngIso s))$
5	4	exbidv	$⊢ r = R \to (\exists f f \in (r RngIso s) \leftrightarrow \exists f f \in (R RngIso s))$
6	2 5	anbi12d	$⊢ r = R \to (((r \in RingOps \land s \in RingOps) \land \exists f f \in (r RngIso s)) \leftrightarrow ((R \in RingOps \land s \in RingOps) \land \exists f f \in (R RngIso 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 RngIso s = R RngIso S$
10	9	eleq2d	$⊢ s = S \to (f \in (R RngIso s) \leftrightarrow f \in (R RngIso S))$
11	10	exbidv	$⊢ s = S \to (\exists f f \in (R RngIso s) \leftrightarrow \exists f f \in (R RngIso S))$
12	8 11	anbi12d	$⊢ s = S \to (((R \in RingOps \land s \in RingOps) \land \exists f f \in (R RngIso s)) \leftrightarrow ((R \in RingOps \land S \in RingOps) \land \exists f f \in (R RngIso S)))$
13		df-risc	$⊢ ≃_{𝑟} = \{⟨r, s⟩ \| ((r \in RingOps \land s \in RingOps) \land \exists f f \in (r RngIso 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 RngIso S)))$

Metamath Proof Explorer