Theorem isriscg

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

	Ref	Expression
Assertion	isriscg	⊢ ( ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐵 ) → ( 𝑅 ≃𝑟 𝑆 ↔ ( ( 𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ) ∧ ∃ 𝑓 𝑓 ∈ ( 𝑅 RngIso 𝑆 ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		eleq1	⊢ ( 𝑟 = 𝑅 → ( 𝑟 ∈ RingOps ↔ 𝑅 ∈ RingOps ) )
2	1	anbi1d	⊢ ( 𝑟 = 𝑅 → ( ( 𝑟 ∈ RingOps ∧ 𝑠 ∈ RingOps ) ↔ ( 𝑅 ∈ RingOps ∧ 𝑠 ∈ RingOps ) ) )
3		oveq1	⊢ ( 𝑟 = 𝑅 → ( 𝑟 RngIso 𝑠 ) = ( 𝑅 RngIso 𝑠 ) )
4	3	eleq2d	⊢ ( 𝑟 = 𝑅 → ( 𝑓 ∈ ( 𝑟 RngIso 𝑠 ) ↔ 𝑓 ∈ ( 𝑅 RngIso 𝑠 ) ) )
5	4	exbidv	⊢ ( 𝑟 = 𝑅 → ( ∃ 𝑓 𝑓 ∈ ( 𝑟 RngIso 𝑠 ) ↔ ∃ 𝑓 𝑓 ∈ ( 𝑅 RngIso 𝑠 ) ) )
6	2 5	anbi12d	⊢ ( 𝑟 = 𝑅 → ( ( ( 𝑟 ∈ RingOps ∧ 𝑠 ∈ RingOps ) ∧ ∃ 𝑓 𝑓 ∈ ( 𝑟 RngIso 𝑠 ) ) ↔ ( ( 𝑅 ∈ RingOps ∧ 𝑠 ∈ RingOps ) ∧ ∃ 𝑓 𝑓 ∈ ( 𝑅 RngIso 𝑠 ) ) ) )
7		eleq1	⊢ ( 𝑠 = 𝑆 → ( 𝑠 ∈ RingOps ↔ 𝑆 ∈ RingOps ) )
8	7	anbi2d	⊢ ( 𝑠 = 𝑆 → ( ( 𝑅 ∈ RingOps ∧ 𝑠 ∈ RingOps ) ↔ ( 𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ) ) )
9		oveq2	⊢ ( 𝑠 = 𝑆 → ( 𝑅 RngIso 𝑠 ) = ( 𝑅 RngIso 𝑆 ) )
10	9	eleq2d	⊢ ( 𝑠 = 𝑆 → ( 𝑓 ∈ ( 𝑅 RngIso 𝑠 ) ↔ 𝑓 ∈ ( 𝑅 RngIso 𝑆 ) ) )
11	10	exbidv	⊢ ( 𝑠 = 𝑆 → ( ∃ 𝑓 𝑓 ∈ ( 𝑅 RngIso 𝑠 ) ↔ ∃ 𝑓 𝑓 ∈ ( 𝑅 RngIso 𝑆 ) ) )
12	8 11	anbi12d	⊢ ( 𝑠 = 𝑆 → ( ( ( 𝑅 ∈ RingOps ∧ 𝑠 ∈ RingOps ) ∧ ∃ 𝑓 𝑓 ∈ ( 𝑅 RngIso 𝑠 ) ) ↔ ( ( 𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ) ∧ ∃ 𝑓 𝑓 ∈ ( 𝑅 RngIso 𝑆 ) ) ) )
13		df-risc	⊢ ≃𝑟 = { ⟨ 𝑟 , 𝑠 ⟩ ∣ ( ( 𝑟 ∈ RingOps ∧ 𝑠 ∈ RingOps ) ∧ ∃ 𝑓 𝑓 ∈ ( 𝑟 RngIso 𝑠 ) ) }
14	6 12 13	brabg	⊢ ( ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐵 ) → ( 𝑅 ≃𝑟 𝑆 ↔ ( ( 𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ) ∧ ∃ 𝑓 𝑓 ∈ ( 𝑅 RngIso 𝑆 ) ) ) )