Metamath Proof Explorer


Theorem rhmsubcALTVlem1

Description: Lemma 1 for rhmsubcALTV . (Contributed by AV, 2-Mar-2020) (New usage is discouraged.)

Ref Expression
Hypotheses rngcrescrhmALTV.u ( 𝜑𝑈𝑉 )
rngcrescrhmALTV.c 𝐶 = ( RngCatALTV ‘ 𝑈 )
rngcrescrhmALTV.r ( 𝜑𝑅 = ( Ring ∩ 𝑈 ) )
rngcrescrhmALTV.h 𝐻 = ( RingHom ↾ ( 𝑅 × 𝑅 ) )
Assertion rhmsubcALTVlem1 ( 𝜑𝐻 Fn ( 𝑅 × 𝑅 ) )

Proof

Step Hyp Ref Expression
1 rngcrescrhmALTV.u ( 𝜑𝑈𝑉 )
2 rngcrescrhmALTV.c 𝐶 = ( RngCatALTV ‘ 𝑈 )
3 rngcrescrhmALTV.r ( 𝜑𝑅 = ( Ring ∩ 𝑈 ) )
4 rngcrescrhmALTV.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 ( 𝑅 × 𝑅 ) )