This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem isriscg

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

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

Proof

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