Metamath Proof Explorer

Theorem rngohomf

Description: A ring homomorphism is a function. (Contributed by Jeff Madsen, 19-Jun-2010)

		Ref	Expression
	Hypotheses	rnghomf.1	⊢ 𝐺 = ( 1^st ‘ 𝑅 )
		rnghomf.2	⊢ 𝑋 = ran 𝐺
		rnghomf.3	⊢ 𝐽 = ( 1^st ‘ 𝑆 )
		rnghomf.4	⊢ 𝑌 = ran 𝐽
	Assertion	rngohomf	⊢ ( ( 𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ ( 𝑅 RngHom 𝑆 ) ) → 𝐹 : 𝑋 ⟶ 𝑌 )

Proof

Step	Hyp	Ref	Expression
1		rnghomf.1	⊢ 𝐺 = ( 1^st ‘ 𝑅 )
2		rnghomf.2	⊢ 𝑋 = ran 𝐺
3		rnghomf.3	⊢ 𝐽 = ( 1^st ‘ 𝑆 )
4		rnghomf.4	⊢ 𝑌 = ran 𝐽
5		eqid	⊢ ( 2^nd ‘ 𝑅 ) = ( 2^nd ‘ 𝑅 )
6		eqid	⊢ ( GId ‘ ( 2^nd ‘ 𝑅 ) ) = ( GId ‘ ( 2^nd ‘ 𝑅 ) )
7		eqid	⊢ ( 2^nd ‘ 𝑆 ) = ( 2^nd ‘ 𝑆 )
8		eqid	⊢ ( GId ‘ ( 2^nd ‘ 𝑆 ) ) = ( GId ‘ ( 2^nd ‘ 𝑆 ) )
9	1 5 2 6 3 7 4 8	isrngohom	⊢ ( ( 𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ) → ( 𝐹 ∈ ( 𝑅 RngHom 𝑆 ) ↔ ( 𝐹 : 𝑋 ⟶ 𝑌 ∧ ( 𝐹 ‘ ( GId ‘ ( 2^nd ‘ 𝑅 ) ) ) = ( GId ‘ ( 2^nd ‘ 𝑆 ) ) ∧ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( ( 𝐹 ‘ ( 𝑥 𝐺 𝑦 ) ) = ( ( 𝐹 ‘ 𝑥 ) 𝐽 ( 𝐹 ‘ 𝑦 ) ) ∧ ( 𝐹 ‘ ( 𝑥 ( 2^nd ‘ 𝑅 ) 𝑦 ) ) = ( ( 𝐹 ‘ 𝑥 ) ( 2^nd ‘ 𝑆 ) ( 𝐹 ‘ 𝑦 ) ) ) ) ) )
10	9	biimpa	⊢ ( ( ( 𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ) ∧ 𝐹 ∈ ( 𝑅 RngHom 𝑆 ) ) → ( 𝐹 : 𝑋 ⟶ 𝑌 ∧ ( 𝐹 ‘ ( GId ‘ ( 2^nd ‘ 𝑅 ) ) ) = ( GId ‘ ( 2^nd ‘ 𝑆 ) ) ∧ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( ( 𝐹 ‘ ( 𝑥 𝐺 𝑦 ) ) = ( ( 𝐹 ‘ 𝑥 ) 𝐽 ( 𝐹 ‘ 𝑦 ) ) ∧ ( 𝐹 ‘ ( 𝑥 ( 2^nd ‘ 𝑅 ) 𝑦 ) ) = ( ( 𝐹 ‘ 𝑥 ) ( 2^nd ‘ 𝑆 ) ( 𝐹 ‘ 𝑦 ) ) ) ) )
11	10	simp1d	⊢ ( ( ( 𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ) ∧ 𝐹 ∈ ( 𝑅 RngHom 𝑆 ) ) → 𝐹 : 𝑋 ⟶ 𝑌 )
12	11	3impa	⊢ ( ( 𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ ( 𝑅 RngHom 𝑆 ) ) → 𝐹 : 𝑋 ⟶ 𝑌 )