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

Metamath Proof Explorer

Theorem isrngoiso

Description: The predicate "is a ring isomorphism between R and S ". (Contributed by Jeff Madsen, 16-Jun-2011)

Ref Expression
Hypotheses rngisoval.1 ⊢ 𝐺 = ( 1st ‘ 𝑅 )
rngisoval.2 ⊢ 𝑋 = ran 𝐺
rngisoval.3 ⊢ 𝐽 = ( 1st ‘ 𝑆 )
rngisoval.4 ⊢ 𝑌 = ran 𝐽
Assertion isrngoiso ( ( 𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ) → ( 𝐹 ∈ ( 𝑅 RingOpsIso 𝑆 ) ↔ ( 𝐹 ∈ ( 𝑅 RingOpsHom 𝑆 ) ∧ 𝐹 : 𝑋 –1-1-onto→ 𝑌 ) ) )

Proof

Step Hyp Ref Expression
1 rngisoval.1 ⊢ 𝐺 = ( 1st ‘ 𝑅 )
2 rngisoval.2 ⊢ 𝑋 = ran 𝐺
3 rngisoval.3 ⊢ 𝐽 = ( 1st ‘ 𝑆 )
4 rngisoval.4 ⊢ 𝑌 = ran 𝐽
5 1 2 3 4 rngoisoval ⊢ ( ( 𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ) → ( 𝑅 RingOpsIso 𝑆 ) = { 𝑓 ∈ ( 𝑅 RingOpsHom 𝑆 ) ∣ 𝑓 : 𝑋 –1-1-onto→ 𝑌 } )
6 5 eleq2d ⊢ ( ( 𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ) → ( 𝐹 ∈ ( 𝑅 RingOpsIso 𝑆 ) ↔ 𝐹 ∈ { 𝑓 ∈ ( 𝑅 RingOpsHom 𝑆 ) ∣ 𝑓 : 𝑋 –1-1-onto→ 𝑌 } ) )
7 f1oeq1 ⊢ ( 𝑓 = 𝐹 → ( 𝑓 : 𝑋 –1-1-onto→ 𝑌 ↔ 𝐹 : 𝑋 –1-1-onto→ 𝑌 ) )
8 7 elrab ⊢ ( 𝐹 ∈ { 𝑓 ∈ ( 𝑅 RingOpsHom 𝑆 ) ∣ 𝑓 : 𝑋 –1-1-onto→ 𝑌 } ↔ ( 𝐹 ∈ ( 𝑅 RingOpsHom 𝑆 ) ∧ 𝐹 : 𝑋 –1-1-onto→ 𝑌 ) )
9 6 8 bitrdi ⊢ ( ( 𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ) → ( 𝐹 ∈ ( 𝑅 RingOpsIso 𝑆 ) ↔ ( 𝐹 ∈ ( 𝑅 RingOpsHom 𝑆 ) ∧ 𝐹 : 𝑋 –1-1-onto→ 𝑌 ) ) )