rngoisoval

Description: The set of ring isomorphisms. (Contributed by Jeff Madsen, 16-Jun-2011)

	Ref	Expression
Hypotheses	rngisoval.1	⊢ 𝐺 = ( 1^st ‘ 𝑅 )
	rngisoval.2	⊢ 𝑋 = ran 𝐺
	rngisoval.3	⊢ 𝐽 = ( 1^st ‘ 𝑆 )
	rngisoval.4	⊢ 𝑌 = ran 𝐽
Assertion	rngoisoval	⊢ ( ( 𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ) → ( 𝑅 RingOpsIso 𝑆 ) = { 𝑓 ∈ ( 𝑅 RingOpsHom 𝑆 ) ∣ 𝑓 : 𝑋 –1-1-onto→ 𝑌 } )

Proof

Step	Hyp	Ref	Expression
1		rngisoval.1	⊢ 𝐺 = ( 1^st ‘ 𝑅 )
2		rngisoval.2	⊢ 𝑋 = ran 𝐺
3		rngisoval.3	⊢ 𝐽 = ( 1^st ‘ 𝑆 )
4		rngisoval.4	⊢ 𝑌 = ran 𝐽
5		oveq12	⊢ ( ( 𝑟 = 𝑅 ∧ 𝑠 = 𝑆 ) → ( 𝑟 RingOpsHom 𝑠 ) = ( 𝑅 RingOpsHom 𝑆 ) )
6		fveq2	⊢ ( 𝑟 = 𝑅 → ( 1^st ‘ 𝑟 ) = ( 1^st ‘ 𝑅 ) )
7	6 1	eqtr4di	⊢ ( 𝑟 = 𝑅 → ( 1^st ‘ 𝑟 ) = 𝐺 )
8	7	rneqd	⊢ ( 𝑟 = 𝑅 → ran ( 1^st ‘ 𝑟 ) = ran 𝐺 )
9	8 2	eqtr4di	⊢ ( 𝑟 = 𝑅 → ran ( 1^st ‘ 𝑟 ) = 𝑋 )
10	9	f1oeq2d	⊢ ( 𝑟 = 𝑅 → ( 𝑓 : ran ( 1^st ‘ 𝑟 ) –1-1-onto→ ran ( 1^st ‘ 𝑠 ) ↔ 𝑓 : 𝑋 –1-1-onto→ ran ( 1^st ‘ 𝑠 ) ) )
11		fveq2	⊢ ( 𝑠 = 𝑆 → ( 1^st ‘ 𝑠 ) = ( 1^st ‘ 𝑆 ) )
12	11 3	eqtr4di	⊢ ( 𝑠 = 𝑆 → ( 1^st ‘ 𝑠 ) = 𝐽 )
13	12	rneqd	⊢ ( 𝑠 = 𝑆 → ran ( 1^st ‘ 𝑠 ) = ran 𝐽 )
14	13 4	eqtr4di	⊢ ( 𝑠 = 𝑆 → ran ( 1^st ‘ 𝑠 ) = 𝑌 )
15	14	f1oeq3d	⊢ ( 𝑠 = 𝑆 → ( 𝑓 : 𝑋 –1-1-onto→ ran ( 1^st ‘ 𝑠 ) ↔ 𝑓 : 𝑋 –1-1-onto→ 𝑌 ) )
16	10 15	sylan9bb	⊢ ( ( 𝑟 = 𝑅 ∧ 𝑠 = 𝑆 ) → ( 𝑓 : ran ( 1^st ‘ 𝑟 ) –1-1-onto→ ran ( 1^st ‘ 𝑠 ) ↔ 𝑓 : 𝑋 –1-1-onto→ 𝑌 ) )
17	5 16	rabeqbidv	⊢ ( ( 𝑟 = 𝑅 ∧ 𝑠 = 𝑆 ) → { 𝑓 ∈ ( 𝑟 RingOpsHom 𝑠 ) ∣ 𝑓 : ran ( 1^st ‘ 𝑟 ) –1-1-onto→ ran ( 1^st ‘ 𝑠 ) } = { 𝑓 ∈ ( 𝑅 RingOpsHom 𝑆 ) ∣ 𝑓 : 𝑋 –1-1-onto→ 𝑌 } )
18		df-rngoiso	⊢ RingOpsIso = ( 𝑟 ∈ RingOps , 𝑠 ∈ RingOps ↦ { 𝑓 ∈ ( 𝑟 RingOpsHom 𝑠 ) ∣ 𝑓 : ran ( 1^st ‘ 𝑟 ) –1-1-onto→ ran ( 1^st ‘ 𝑠 ) } )
19		ovex	⊢ ( 𝑅 RingOpsHom 𝑆 ) ∈ V
20	19	rabex	⊢ { 𝑓 ∈ ( 𝑅 RingOpsHom 𝑆 ) ∣ 𝑓 : 𝑋 –1-1-onto→ 𝑌 } ∈ V
21	17 18 20	ovmpoa	⊢ ( ( 𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ) → ( 𝑅 RingOpsIso 𝑆 ) = { 𝑓 ∈ ( 𝑅 RingOpsHom 𝑆 ) ∣ 𝑓 : 𝑋 –1-1-onto→ 𝑌 } )

Metamath Proof Explorer

Theorem rngoisoval

Proof