Metamath Proof Explorer

Theorem rngohomf

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

Ref Expression
Hypotheses rnghomf.1 ⊢ G = 1 st ⁡ R
rnghomf.2 ⊢ X = ran ⁡ G
rnghomf.3 ⊢ J = 1 st ⁡ S
rnghomf.4 ⊢ Y = ran ⁡ J
Assertion rngohomf ⊢ R ∈ RingOps ∧ S ∈ RingOps ∧ F ∈ R RngHom S → F : X ⟶ Y

Proof

Step Hyp Ref Expression
1 rnghomf.1 ⊢ G = 1 st ⁡ R
2 rnghomf.2 ⊢ X = ran ⁡ G
3 rnghomf.3 ⊢ J = 1 st ⁡ S
4 rnghomf.4 ⊢ Y = ran ⁡ J
5 eqid ⊢ 2 nd ⁡ R = 2 nd ⁡ R
6 eqid ⊢ GId ⁡ 2 nd ⁡ R = GId ⁡ 2 nd ⁡ R
7 eqid ⊢ 2 nd ⁡ S = 2 nd ⁡ S
8 eqid ⊢ GId ⁡ 2 nd ⁡ S = GId ⁡ 2 nd ⁡ S
9 1 5 2 6 3 7 4 8 isrngohom ⊢ R ∈ RingOps ∧ S ∈ RingOps → F ∈ R RngHom S ↔ F : X ⟶ Y ∧ F ⁡ GId ⁡ 2 nd ⁡ R = GId ⁡ 2 nd ⁡ S ∧ ∀ x ∈ X ∀ y ∈ X F ⁡ x G y = F ⁡ x J F ⁡ y ∧ F ⁡ x 2 nd ⁡ R y = F ⁡ x 2 nd ⁡ S F ⁡ y
10 9 biimpa ⊢ R ∈ RingOps ∧ S ∈ RingOps ∧ F ∈ R RngHom S → F : X ⟶ Y ∧ F ⁡ GId ⁡ 2 nd ⁡ R = GId ⁡ 2 nd ⁡ S ∧ ∀ x ∈ X ∀ y ∈ X F ⁡ x G y = F ⁡ x J F ⁡ y ∧ F ⁡ x 2 nd ⁡ R y = F ⁡ x 2 nd ⁡ S F ⁡ y
11 10 simp1d ⊢ R ∈ RingOps ∧ S ∈ RingOps ∧ F ∈ R RngHom S → F : X ⟶ Y
12 11 3impa ⊢ R ∈ RingOps ∧ S ∈ RingOps ∧ F ∈ R RngHom S → F : X ⟶ Y