Metamath Proof Explorer

Theorem isriscg

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

Ref Expression
Assertion isriscg ⊢ R ∈ A ∧ S ∈ B → R ≃ 𝑟 S ↔ R ∈ RingOps ∧ S ∈ RingOps ∧ ∃ f f ∈ R RngIso S

Proof

Step Hyp Ref Expression
1 eleq1 ⊢ r = R → r ∈ RingOps ↔ R ∈ RingOps
2 1 anbi1d ⊢ r = R → r ∈ RingOps ∧ s ∈ RingOps ↔ R ∈ RingOps ∧ s ∈ RingOps
3 oveq1 ⊢ r = R → r RngIso s = R RngIso s
4 3 eleq2d ⊢ r = R → f ∈ r RngIso s ↔ f ∈ R RngIso s
5 4 exbidv ⊢ r = R → ∃ f f ∈ r RngIso s ↔ ∃ f f ∈ R RngIso s
6 2 5 anbi12d ⊢ r = R → r ∈ RingOps ∧ s ∈ RingOps ∧ ∃ f f ∈ r RngIso s ↔ R ∈ RingOps ∧ s ∈ RingOps ∧ ∃ f f ∈ R RngIso s
7 eleq1 ⊢ s = S → s ∈ RingOps ↔ S ∈ RingOps
8 7 anbi2d ⊢ s = S → R ∈ RingOps ∧ s ∈ RingOps ↔ R ∈ RingOps ∧ S ∈ RingOps
9 oveq2 ⊢ s = S → R RngIso s = R RngIso S
10 9 eleq2d ⊢ s = S → f ∈ R RngIso s ↔ f ∈ R RngIso S
11 10 exbidv ⊢ s = S → ∃ f f ∈ R RngIso s ↔ ∃ f f ∈ R RngIso S
12 8 11 anbi12d ⊢ s = S → R ∈ RingOps ∧ s ∈ RingOps ∧ ∃ f f ∈ R RngIso s ↔ R ∈ RingOps ∧ S ∈ RingOps ∧ ∃ f f ∈ R RngIso S
13 df-risc ⊢ ≃ 𝑟 = r s | r ∈ RingOps ∧ s ∈ RingOps ∧ ∃ f f ∈ r RngIso s
14 6 12 13 brabg ⊢ R ∈ A ∧ S ∈ B → R ≃ 𝑟 S ↔ R ∈ RingOps ∧ S ∈ RingOps ∧ ∃ f f ∈ R RngIso S