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

Metamath Proof Explorer

Theorem rhmresfn

Description: The class of unital ring homomorphisms restricted to subsets of unital rings is a function. (Contributed by AV, 10-Mar-2020)

Ref Expression
Hypotheses rhmresfn.b ⊢ ( 𝜑 → 𝐵 = ( 𝑈 ∩ Ring ) )
rhmresfn.h ⊢ ( 𝜑 → 𝐻 = ( RingHom ↾ ( 𝐵 × 𝐵 ) ) )
Assertion rhmresfn ( 𝜑 → 𝐻 Fn ( 𝐵 × 𝐵 ) )

Proof

Step Hyp Ref Expression
1 rhmresfn.b ⊢ ( 𝜑 → 𝐵 = ( 𝑈 ∩ Ring ) )
2 rhmresfn.h ⊢ ( 𝜑 → 𝐻 = ( RingHom ↾ ( 𝐵 × 𝐵 ) ) )
3 rhmfn ⊢ RingHom Fn ( Ring × Ring )
4 inss2 ⊢ ( 𝑈 ∩ Ring ) ⊆ Ring
5 1 4 eqsstrdi ⊢ ( 𝜑 → 𝐵 ⊆ Ring )
6 xpss12 ⊢ ( ( 𝐵 ⊆ Ring ∧ 𝐵 ⊆ Ring ) → ( 𝐵 × 𝐵 ) ⊆ ( Ring × Ring ) )
7 5 5 6 syl2anc ⊢ ( 𝜑 → ( 𝐵 × 𝐵 ) ⊆ ( Ring × Ring ) )
8 fnssres ⊢ ( ( RingHom Fn ( Ring × Ring ) ∧ ( 𝐵 × 𝐵 ) ⊆ ( Ring × Ring ) ) → ( RingHom ↾ ( 𝐵 × 𝐵 ) ) Fn ( 𝐵 × 𝐵 ) )
9 3 7 8 sylancr ⊢ ( 𝜑 → ( RingHom ↾ ( 𝐵 × 𝐵 ) ) Fn ( 𝐵 × 𝐵 ) )
10 2 fneq1d ⊢ ( 𝜑 → ( 𝐻 Fn ( 𝐵 × 𝐵 ) ↔ ( RingHom ↾ ( 𝐵 × 𝐵 ) ) Fn ( 𝐵 × 𝐵 ) ) )
11 9 10 mpbird ⊢ ( 𝜑 → 𝐻 Fn ( 𝐵 × 𝐵 ) )