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

Metamath Proof Explorer

Theorem rhmsubclem1

Description: Lemma 1 for rhmsubc . (Contributed by AV, 2-Mar-2020)

Ref Expression
Hypotheses rngcrescrhm.u ⊢ ( 𝜑 → 𝑈 ∈ 𝑉 )
rngcrescrhm.c ⊢ 𝐶 = ( RngCat ‘ 𝑈 )
rngcrescrhm.r ⊢ ( 𝜑 → 𝑅 = ( Ring ∩ 𝑈 ) )
rngcrescrhm.h ⊢ 𝐻 = ( RingHom ↾ ( 𝑅 × 𝑅 ) )
Assertion rhmsubclem1 ( 𝜑 → 𝐻 Fn ( 𝑅 × 𝑅 ) )

Proof

Step Hyp Ref Expression
1 rngcrescrhm.u ⊢ ( 𝜑 → 𝑈 ∈ 𝑉 )
2 rngcrescrhm.c ⊢ 𝐶 = ( RngCat ‘ 𝑈 )
3 rngcrescrhm.r ⊢ ( 𝜑 → 𝑅 = ( Ring ∩ 𝑈 ) )
4 rngcrescrhm.h ⊢ 𝐻 = ( RingHom ↾ ( 𝑅 × 𝑅 ) )
5 eqid ⊢ ( 𝑥 ∈ 𝑅 , 𝑦 ∈ 𝑅 ↦ ( ( 𝑥 GrpHom 𝑦 ) ∩ ( ( mulGrp ‘ 𝑥 ) MndHom ( mulGrp ‘ 𝑦 ) ) ) ) = ( 𝑥 ∈ 𝑅 , 𝑦 ∈ 𝑅 ↦ ( ( 𝑥 GrpHom 𝑦 ) ∩ ( ( mulGrp ‘ 𝑥 ) MndHom ( mulGrp ‘ 𝑦 ) ) ) )
6 ovex ⊢ ( 𝑥 GrpHom 𝑦 ) ∈ V
7 6 inex1 ⊢ ( ( 𝑥 GrpHom 𝑦 ) ∩ ( ( mulGrp ‘ 𝑥 ) MndHom ( mulGrp ‘ 𝑦 ) ) ) ∈ V
8 5 7 fnmpoi ⊢ ( 𝑥 ∈ 𝑅 , 𝑦 ∈ 𝑅 ↦ ( ( 𝑥 GrpHom 𝑦 ) ∩ ( ( mulGrp ‘ 𝑥 ) MndHom ( mulGrp ‘ 𝑦 ) ) ) ) Fn ( 𝑅 × 𝑅 )
9 4 a1i ⊢ ( 𝜑 → 𝐻 = ( RingHom ↾ ( 𝑅 × 𝑅 ) ) )
10 dfrhm2 ⊢ RingHom = ( 𝑥 ∈ Ring , 𝑦 ∈ Ring ↦ ( ( 𝑥 GrpHom 𝑦 ) ∩ ( ( mulGrp ‘ 𝑥 ) MndHom ( mulGrp ‘ 𝑦 ) ) ) )
11 10 a1i ⊢ ( 𝜑 → RingHom = ( 𝑥 ∈ Ring , 𝑦 ∈ Ring ↦ ( ( 𝑥 GrpHom 𝑦 ) ∩ ( ( mulGrp ‘ 𝑥 ) MndHom ( mulGrp ‘ 𝑦 ) ) ) ) )
12 11 reseq1d ⊢ ( 𝜑 → ( RingHom ↾ ( 𝑅 × 𝑅 ) ) = ( ( 𝑥 ∈ Ring , 𝑦 ∈ Ring ↦ ( ( 𝑥 GrpHom 𝑦 ) ∩ ( ( mulGrp ‘ 𝑥 ) MndHom ( mulGrp ‘ 𝑦 ) ) ) ) ↾ ( 𝑅 × 𝑅 ) ) )
13 inss1 ⊢ ( Ring ∩ 𝑈 ) ⊆ Ring
14 3 13 eqsstrdi ⊢ ( 𝜑 → 𝑅 ⊆ Ring )
15 resmpo ⊢ ( ( 𝑅 ⊆ Ring ∧ 𝑅 ⊆ Ring ) → ( ( 𝑥 ∈ Ring , 𝑦 ∈ Ring ↦ ( ( 𝑥 GrpHom 𝑦 ) ∩ ( ( mulGrp ‘ 𝑥 ) MndHom ( mulGrp ‘ 𝑦 ) ) ) ) ↾ ( 𝑅 × 𝑅 ) ) = ( 𝑥 ∈ 𝑅 , 𝑦 ∈ 𝑅 ↦ ( ( 𝑥 GrpHom 𝑦 ) ∩ ( ( mulGrp ‘ 𝑥 ) MndHom ( mulGrp ‘ 𝑦 ) ) ) ) )
16 14 14 15 syl2anc ⊢ ( 𝜑 → ( ( 𝑥 ∈ Ring , 𝑦 ∈ Ring ↦ ( ( 𝑥 GrpHom 𝑦 ) ∩ ( ( mulGrp ‘ 𝑥 ) MndHom ( mulGrp ‘ 𝑦 ) ) ) ) ↾ ( 𝑅 × 𝑅 ) ) = ( 𝑥 ∈ 𝑅 , 𝑦 ∈ 𝑅 ↦ ( ( 𝑥 GrpHom 𝑦 ) ∩ ( ( mulGrp ‘ 𝑥 ) MndHom ( mulGrp ‘ 𝑦 ) ) ) ) )
17 9 12 16 3eqtrd ⊢ ( 𝜑 → 𝐻 = ( 𝑥 ∈ 𝑅 , 𝑦 ∈ 𝑅 ↦ ( ( 𝑥 GrpHom 𝑦 ) ∩ ( ( mulGrp ‘ 𝑥 ) MndHom ( mulGrp ‘ 𝑦 ) ) ) ) )
18 17 fneq1d ⊢ ( 𝜑 → ( 𝐻 Fn ( 𝑅 × 𝑅 ) ↔ ( 𝑥 ∈ 𝑅 , 𝑦 ∈ 𝑅 ↦ ( ( 𝑥 GrpHom 𝑦 ) ∩ ( ( mulGrp ‘ 𝑥 ) MndHom ( mulGrp ‘ 𝑦 ) ) ) ) Fn ( 𝑅 × 𝑅 ) ) )
19 8 18 mpbiri ⊢ ( 𝜑 → 𝐻 Fn ( 𝑅 × 𝑅 ) )