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

Metamath Proof Explorer

Theorem rnghmfn

Description: The mapping of two non-unital rings to the non-unital ring homomorphisms between them is a function. (Contributed by AV, 1-Mar-2020)

Ref Expression
Assertion rnghmfn ⊢ RngHom Fn Rng × Rng

Proof

Step Hyp Ref Expression
1 df-rnghm ⊢ RngHom = r ∈ Rng , s ∈ Rng ⟼ ⦋ Base r / v⦌ ⦋ Base s / w⦌ f ∈ w v | ∀ x ∈ v ∀ y ∈ v f ⁡ x + r y = f ⁡ x + s f ⁡ y ∧ f ⁡ x ⋅ r y = f ⁡ x ⋅ s f ⁡ y
2 ovex ⊢ w v ∈ V
3 2 rabex ⊢ f ∈ w v | ∀ x ∈ v ∀ y ∈ v f ⁡ x + r y = f ⁡ x + s f ⁡ y ∧ f ⁡ x ⋅ r y = f ⁡ x ⋅ s f ⁡ y ∈ V
4 3 csbex ⊢ ⦋ Base s / w⦌ f ∈ w v | ∀ x ∈ v ∀ y ∈ v f ⁡ x + r y = f ⁡ x + s f ⁡ y ∧ f ⁡ x ⋅ r y = f ⁡ x ⋅ s f ⁡ y ∈ V
5 4 csbex ⊢ ⦋ Base r / v⦌ ⦋ Base s / w⦌ f ∈ w v | ∀ x ∈ v ∀ y ∈ v f ⁡ x + r y = f ⁡ x + s f ⁡ y ∧ f ⁡ x ⋅ r y = f ⁡ x ⋅ s f ⁡ y ∈ V
6 1 5 fnmpoi ⊢ RngHom Fn Rng × Rng