Metamath Proof Explorer

Theorem dfrhm2

Description: The property of a ring homomorphism can be decomposed into separate homomorphic conditions for addition and multiplication. (Contributed by Stefan O'Rear, 7-Mar-2015)

Ref Expression
Assertion dfrhm2 RingHom = ( 𝑟 ∈ Ring , 𝑠 ∈ Ring ↦ ( ( 𝑟 GrpHom 𝑠 ) ∩ ( ( mulGrp ‘ 𝑟 ) MndHom ( mulGrp ‘ 𝑠 ) ) ) )

Proof

Step Hyp Ref Expression
1 df-rnghom ⊢ RingHom = ( 𝑟 ∈ Ring , 𝑠 ∈ Ring ↦ ⦋ ( Base ‘ 𝑟 ) / 𝑣 ⦌ ⦋ ( Base ‘ 𝑠 ) / 𝑤 ⦌ { 𝑓 ∈ ( 𝑤 ↑m 𝑣 ) ∣ ( ( 𝑓 ‘ ( 1r ‘ 𝑟 ) ) = ( 1r ‘ 𝑠 ) ∧ ∀ 𝑥 ∈ 𝑣 ∀ 𝑦 ∈ 𝑣 ( ( 𝑓 ‘ ( 𝑥 ( +g ‘ 𝑟 ) 𝑦 ) ) = ( ( 𝑓 ‘ 𝑥 ) ( +g ‘ 𝑠 ) ( 𝑓 ‘ 𝑦 ) ) ∧ ( 𝑓 ‘ ( 𝑥 ( .r ‘ 𝑟 ) 𝑦 ) ) = ( ( 𝑓 ‘ 𝑥 ) ( .r ‘ 𝑠 ) ( 𝑓 ‘ 𝑦 ) ) ) ) } )
2 ancom ⊢ ( ( ( 𝑓 ‘ ( 1r ‘ 𝑟 ) ) = ( 1r ‘ 𝑠 ) ∧ ∀ 𝑥 ∈ ( Base ‘ 𝑟 ) ∀ 𝑦 ∈ ( Base ‘ 𝑟 ) ( ( 𝑓 ‘ ( 𝑥 ( +g ‘ 𝑟 ) 𝑦 ) ) = ( ( 𝑓 ‘ 𝑥 ) ( +g ‘ 𝑠 ) ( 𝑓 ‘ 𝑦 ) ) ∧ ( 𝑓 ‘ ( 𝑥 ( .r ‘ 𝑟 ) 𝑦 ) ) = ( ( 𝑓 ‘ 𝑥 ) ( .r ‘ 𝑠 ) ( 𝑓 ‘ 𝑦 ) ) ) ) ↔ ( ∀ 𝑥 ∈ ( Base ‘ 𝑟 ) ∀ 𝑦 ∈ ( Base ‘ 𝑟 ) ( ( 𝑓 ‘ ( 𝑥 ( +g ‘ 𝑟 ) 𝑦 ) ) = ( ( 𝑓 ‘ 𝑥 ) ( +g ‘ 𝑠 ) ( 𝑓 ‘ 𝑦 ) ) ∧ ( 𝑓 ‘ ( 𝑥 ( .r ‘ 𝑟 ) 𝑦 ) ) = ( ( 𝑓 ‘ 𝑥 ) ( .r ‘ 𝑠 ) ( 𝑓 ‘ 𝑦 ) ) ) ∧ ( 𝑓 ‘ ( 1r ‘ 𝑟 ) ) = ( 1r ‘ 𝑠 ) ) )
3 r19.26-2 ⊢ ( ∀ 𝑥 ∈ ( Base ‘ 𝑟 ) ∀ 𝑦 ∈ ( Base ‘ 𝑟 ) ( ( 𝑓 ‘ ( 𝑥 ( +g ‘ 𝑟 ) 𝑦 ) ) = ( ( 𝑓 ‘ 𝑥 ) ( +g ‘ 𝑠 ) ( 𝑓 ‘ 𝑦 ) ) ∧ ( 𝑓 ‘ ( 𝑥 ( .r ‘ 𝑟 ) 𝑦 ) ) = ( ( 𝑓 ‘ 𝑥 ) ( .r ‘ 𝑠 ) ( 𝑓 ‘ 𝑦 ) ) ) ↔ ( ∀ 𝑥 ∈ ( Base ‘ 𝑟 ) ∀ 𝑦 ∈ ( Base ‘ 𝑟 ) ( 𝑓 ‘ ( 𝑥 ( +g ‘ 𝑟 ) 𝑦 ) ) = ( ( 𝑓 ‘ 𝑥 ) ( +g ‘ 𝑠 ) ( 𝑓 ‘ 𝑦 ) ) ∧ ∀ 𝑥 ∈ ( Base ‘ 𝑟 ) ∀ 𝑦 ∈ ( Base ‘ 𝑟 ) ( 𝑓 ‘ ( 𝑥 ( .r ‘ 𝑟 ) 𝑦 ) ) = ( ( 𝑓 ‘ 𝑥 ) ( .r ‘ 𝑠 ) ( 𝑓 ‘ 𝑦 ) ) ) )
4 3 anbi1i ⊢ ( ( ∀ 𝑥 ∈ ( Base ‘ 𝑟 ) ∀ 𝑦 ∈ ( Base ‘ 𝑟 ) ( ( 𝑓 ‘ ( 𝑥 ( +g ‘ 𝑟 ) 𝑦 ) ) = ( ( 𝑓 ‘ 𝑥 ) ( +g ‘ 𝑠 ) ( 𝑓 ‘ 𝑦 ) ) ∧ ( 𝑓 ‘ ( 𝑥 ( .r ‘ 𝑟 ) 𝑦 ) ) = ( ( 𝑓 ‘ 𝑥 ) ( .r ‘ 𝑠 ) ( 𝑓 ‘ 𝑦 ) ) ) ∧ ( 𝑓 ‘ ( 1r ‘ 𝑟 ) ) = ( 1r ‘ 𝑠 ) ) ↔ ( ( ∀ 𝑥 ∈ ( Base ‘ 𝑟 ) ∀ 𝑦 ∈ ( Base ‘ 𝑟 ) ( 𝑓 ‘ ( 𝑥 ( +g ‘ 𝑟 ) 𝑦 ) ) = ( ( 𝑓 ‘ 𝑥 ) ( +g ‘ 𝑠 ) ( 𝑓 ‘ 𝑦 ) ) ∧ ∀ 𝑥 ∈ ( Base ‘ 𝑟 ) ∀ 𝑦 ∈ ( Base ‘ 𝑟 ) ( 𝑓 ‘ ( 𝑥 ( .r ‘ 𝑟 ) 𝑦 ) ) = ( ( 𝑓 ‘ 𝑥 ) ( .r ‘ 𝑠 ) ( 𝑓 ‘ 𝑦 ) ) ) ∧ ( 𝑓 ‘ ( 1r ‘ 𝑟 ) ) = ( 1r ‘ 𝑠 ) ) )
5 anass ⊢ ( ( ( ∀ 𝑥 ∈ ( Base ‘ 𝑟 ) ∀ 𝑦 ∈ ( Base ‘ 𝑟 ) ( 𝑓 ‘ ( 𝑥 ( +g ‘ 𝑟 ) 𝑦 ) ) = ( ( 𝑓 ‘ 𝑥 ) ( +g ‘ 𝑠 ) ( 𝑓 ‘ 𝑦 ) ) ∧ ∀ 𝑥 ∈ ( Base ‘ 𝑟 ) ∀ 𝑦 ∈ ( Base ‘ 𝑟 ) ( 𝑓 ‘ ( 𝑥 ( .r ‘ 𝑟 ) 𝑦 ) ) = ( ( 𝑓 ‘ 𝑥 ) ( .r ‘ 𝑠 ) ( 𝑓 ‘ 𝑦 ) ) ) ∧ ( 𝑓 ‘ ( 1r ‘ 𝑟 ) ) = ( 1r ‘ 𝑠 ) ) ↔ ( ∀ 𝑥 ∈ ( Base ‘ 𝑟 ) ∀ 𝑦 ∈ ( Base ‘ 𝑟 ) ( 𝑓 ‘ ( 𝑥 ( +g ‘ 𝑟 ) 𝑦 ) ) = ( ( 𝑓 ‘ 𝑥 ) ( +g ‘ 𝑠 ) ( 𝑓 ‘ 𝑦 ) ) ∧ ( ∀ 𝑥 ∈ ( Base ‘ 𝑟 ) ∀ 𝑦 ∈ ( Base ‘ 𝑟 ) ( 𝑓 ‘ ( 𝑥 ( .r ‘ 𝑟 ) 𝑦 ) ) = ( ( 𝑓 ‘ 𝑥 ) ( .r ‘ 𝑠 ) ( 𝑓 ‘ 𝑦 ) ) ∧ ( 𝑓 ‘ ( 1r ‘ 𝑟 ) ) = ( 1r ‘ 𝑠 ) ) ) )
6 2 4 5 3bitri ⊢ ( ( ( 𝑓 ‘ ( 1r ‘ 𝑟 ) ) = ( 1r ‘ 𝑠 ) ∧ ∀ 𝑥 ∈ ( Base ‘ 𝑟 ) ∀ 𝑦 ∈ ( Base ‘ 𝑟 ) ( ( 𝑓 ‘ ( 𝑥 ( +g ‘ 𝑟 ) 𝑦 ) ) = ( ( 𝑓 ‘ 𝑥 ) ( +g ‘ 𝑠 ) ( 𝑓 ‘ 𝑦 ) ) ∧ ( 𝑓 ‘ ( 𝑥 ( .r ‘ 𝑟 ) 𝑦 ) ) = ( ( 𝑓 ‘ 𝑥 ) ( .r ‘ 𝑠 ) ( 𝑓 ‘ 𝑦 ) ) ) ) ↔ ( ∀ 𝑥 ∈ ( Base ‘ 𝑟 ) ∀ 𝑦 ∈ ( Base ‘ 𝑟 ) ( 𝑓 ‘ ( 𝑥 ( +g ‘ 𝑟 ) 𝑦 ) ) = ( ( 𝑓 ‘ 𝑥 ) ( +g ‘ 𝑠 ) ( 𝑓 ‘ 𝑦 ) ) ∧ ( ∀ 𝑥 ∈ ( Base ‘ 𝑟 ) ∀ 𝑦 ∈ ( Base ‘ 𝑟 ) ( 𝑓 ‘ ( 𝑥 ( .r ‘ 𝑟 ) 𝑦 ) ) = ( ( 𝑓 ‘ 𝑥 ) ( .r ‘ 𝑠 ) ( 𝑓 ‘ 𝑦 ) ) ∧ ( 𝑓 ‘ ( 1r ‘ 𝑟 ) ) = ( 1r ‘ 𝑠 ) ) ) )
7 6 rabbii ⊢ { 𝑓 ∈ ( ( Base ‘ 𝑠 ) ↑m ( Base ‘ 𝑟 ) ) ∣ ( ( 𝑓 ‘ ( 1r ‘ 𝑟 ) ) = ( 1r ‘ 𝑠 ) ∧ ∀ 𝑥 ∈ ( Base ‘ 𝑟 ) ∀ 𝑦 ∈ ( Base ‘ 𝑟 ) ( ( 𝑓 ‘ ( 𝑥 ( +g ‘ 𝑟 ) 𝑦 ) ) = ( ( 𝑓 ‘ 𝑥 ) ( +g ‘ 𝑠 ) ( 𝑓 ‘ 𝑦 ) ) ∧ ( 𝑓 ‘ ( 𝑥 ( .r ‘ 𝑟 ) 𝑦 ) ) = ( ( 𝑓 ‘ 𝑥 ) ( .r ‘ 𝑠 ) ( 𝑓 ‘ 𝑦 ) ) ) ) } = { 𝑓 ∈ ( ( Base ‘ 𝑠 ) ↑m ( Base ‘ 𝑟 ) ) ∣ ( ∀ 𝑥 ∈ ( Base ‘ 𝑟 ) ∀ 𝑦 ∈ ( Base ‘ 𝑟 ) ( 𝑓 ‘ ( 𝑥 ( +g ‘ 𝑟 ) 𝑦 ) ) = ( ( 𝑓 ‘ 𝑥 ) ( +g ‘ 𝑠 ) ( 𝑓 ‘ 𝑦 ) ) ∧ ( ∀ 𝑥 ∈ ( Base ‘ 𝑟 ) ∀ 𝑦 ∈ ( Base ‘ 𝑟 ) ( 𝑓 ‘ ( 𝑥 ( .r ‘ 𝑟 ) 𝑦 ) ) = ( ( 𝑓 ‘ 𝑥 ) ( .r ‘ 𝑠 ) ( 𝑓 ‘ 𝑦 ) ) ∧ ( 𝑓 ‘ ( 1r ‘ 𝑟 ) ) = ( 1r ‘ 𝑠 ) ) ) }
8 fvex ⊢ ( Base ‘ 𝑟 ) ∈ V
9 fvex ⊢ ( Base ‘ 𝑠 ) ∈ V
10 oveq12 ⊢ ( ( 𝑤 = ( Base ‘ 𝑠 ) ∧ 𝑣 = ( Base ‘ 𝑟 ) ) → ( 𝑤 ↑m 𝑣 ) = ( ( Base ‘ 𝑠 ) ↑m ( Base ‘ 𝑟 ) ) )
11 10 ancoms ⊢ ( ( 𝑣 = ( Base ‘ 𝑟 ) ∧ 𝑤 = ( Base ‘ 𝑠 ) ) → ( 𝑤 ↑m 𝑣 ) = ( ( Base ‘ 𝑠 ) ↑m ( Base ‘ 𝑟 ) ) )
12 raleq ⊢ ( 𝑣 = ( Base ‘ 𝑟 ) → ( ∀ 𝑦 ∈ 𝑣 ( ( 𝑓 ‘ ( 𝑥 ( +g ‘ 𝑟 ) 𝑦 ) ) = ( ( 𝑓 ‘ 𝑥 ) ( +g ‘ 𝑠 ) ( 𝑓 ‘ 𝑦 ) ) ∧ ( 𝑓 ‘ ( 𝑥 ( .r ‘ 𝑟 ) 𝑦 ) ) = ( ( 𝑓 ‘ 𝑥 ) ( .r ‘ 𝑠 ) ( 𝑓 ‘ 𝑦 ) ) ) ↔ ∀ 𝑦 ∈ ( Base ‘ 𝑟 ) ( ( 𝑓 ‘ ( 𝑥 ( +g ‘ 𝑟 ) 𝑦 ) ) = ( ( 𝑓 ‘ 𝑥 ) ( +g ‘ 𝑠 ) ( 𝑓 ‘ 𝑦 ) ) ∧ ( 𝑓 ‘ ( 𝑥 ( .r ‘ 𝑟 ) 𝑦 ) ) = ( ( 𝑓 ‘ 𝑥 ) ( .r ‘ 𝑠 ) ( 𝑓 ‘ 𝑦 ) ) ) ) )
13 12 raleqbi1dv ⊢ ( 𝑣 = ( Base ‘ 𝑟 ) → ( ∀ 𝑥 ∈ 𝑣 ∀ 𝑦 ∈ 𝑣 ( ( 𝑓 ‘ ( 𝑥 ( +g ‘ 𝑟 ) 𝑦 ) ) = ( ( 𝑓 ‘ 𝑥 ) ( +g ‘ 𝑠 ) ( 𝑓 ‘ 𝑦 ) ) ∧ ( 𝑓 ‘ ( 𝑥 ( .r ‘ 𝑟 ) 𝑦 ) ) = ( ( 𝑓 ‘ 𝑥 ) ( .r ‘ 𝑠 ) ( 𝑓 ‘ 𝑦 ) ) ) ↔ ∀ 𝑥 ∈ ( Base ‘ 𝑟 ) ∀ 𝑦 ∈ ( Base ‘ 𝑟 ) ( ( 𝑓 ‘ ( 𝑥 ( +g ‘ 𝑟 ) 𝑦 ) ) = ( ( 𝑓 ‘ 𝑥 ) ( +g ‘ 𝑠 ) ( 𝑓 ‘ 𝑦 ) ) ∧ ( 𝑓 ‘ ( 𝑥 ( .r ‘ 𝑟 ) 𝑦 ) ) = ( ( 𝑓 ‘ 𝑥 ) ( .r ‘ 𝑠 ) ( 𝑓 ‘ 𝑦 ) ) ) ) )
14 13 adantr ⊢ ( ( 𝑣 = ( Base ‘ 𝑟 ) ∧ 𝑤 = ( Base ‘ 𝑠 ) ) → ( ∀ 𝑥 ∈ 𝑣 ∀ 𝑦 ∈ 𝑣 ( ( 𝑓 ‘ ( 𝑥 ( +g ‘ 𝑟 ) 𝑦 ) ) = ( ( 𝑓 ‘ 𝑥 ) ( +g ‘ 𝑠 ) ( 𝑓 ‘ 𝑦 ) ) ∧ ( 𝑓 ‘ ( 𝑥 ( .r ‘ 𝑟 ) 𝑦 ) ) = ( ( 𝑓 ‘ 𝑥 ) ( .r ‘ 𝑠 ) ( 𝑓 ‘ 𝑦 ) ) ) ↔ ∀ 𝑥 ∈ ( Base ‘ 𝑟 ) ∀ 𝑦 ∈ ( Base ‘ 𝑟 ) ( ( 𝑓 ‘ ( 𝑥 ( +g ‘ 𝑟 ) 𝑦 ) ) = ( ( 𝑓 ‘ 𝑥 ) ( +g ‘ 𝑠 ) ( 𝑓 ‘ 𝑦 ) ) ∧ ( 𝑓 ‘ ( 𝑥 ( .r ‘ 𝑟 ) 𝑦 ) ) = ( ( 𝑓 ‘ 𝑥 ) ( .r ‘ 𝑠 ) ( 𝑓 ‘ 𝑦 ) ) ) ) )
15 14 anbi2d ⊢ ( ( 𝑣 = ( Base ‘ 𝑟 ) ∧ 𝑤 = ( Base ‘ 𝑠 ) ) → ( ( ( 𝑓 ‘ ( 1r ‘ 𝑟 ) ) = ( 1r ‘ 𝑠 ) ∧ ∀ 𝑥 ∈ 𝑣 ∀ 𝑦 ∈ 𝑣 ( ( 𝑓 ‘ ( 𝑥 ( +g ‘ 𝑟 ) 𝑦 ) ) = ( ( 𝑓 ‘ 𝑥 ) ( +g ‘ 𝑠 ) ( 𝑓 ‘ 𝑦 ) ) ∧ ( 𝑓 ‘ ( 𝑥 ( .r ‘ 𝑟 ) 𝑦 ) ) = ( ( 𝑓 ‘ 𝑥 ) ( .r ‘ 𝑠 ) ( 𝑓 ‘ 𝑦 ) ) ) ) ↔ ( ( 𝑓 ‘ ( 1r ‘ 𝑟 ) ) = ( 1r ‘ 𝑠 ) ∧ ∀ 𝑥 ∈ ( Base ‘ 𝑟 ) ∀ 𝑦 ∈ ( Base ‘ 𝑟 ) ( ( 𝑓 ‘ ( 𝑥 ( +g ‘ 𝑟 ) 𝑦 ) ) = ( ( 𝑓 ‘ 𝑥 ) ( +g ‘ 𝑠 ) ( 𝑓 ‘ 𝑦 ) ) ∧ ( 𝑓 ‘ ( 𝑥 ( .r ‘ 𝑟 ) 𝑦 ) ) = ( ( 𝑓 ‘ 𝑥 ) ( .r ‘ 𝑠 ) ( 𝑓 ‘ 𝑦 ) ) ) ) ) )
16 11 15 rabeqbidv ⊢ ( ( 𝑣 = ( Base ‘ 𝑟 ) ∧ 𝑤 = ( Base ‘ 𝑠 ) ) → { 𝑓 ∈ ( 𝑤 ↑m 𝑣 ) ∣ ( ( 𝑓 ‘ ( 1r ‘ 𝑟 ) ) = ( 1r ‘ 𝑠 ) ∧ ∀ 𝑥 ∈ 𝑣 ∀ 𝑦 ∈ 𝑣 ( ( 𝑓 ‘ ( 𝑥 ( +g ‘ 𝑟 ) 𝑦 ) ) = ( ( 𝑓 ‘ 𝑥 ) ( +g ‘ 𝑠 ) ( 𝑓 ‘ 𝑦 ) ) ∧ ( 𝑓 ‘ ( 𝑥 ( .r ‘ 𝑟 ) 𝑦 ) ) = ( ( 𝑓 ‘ 𝑥 ) ( .r ‘ 𝑠 ) ( 𝑓 ‘ 𝑦 ) ) ) ) } = { 𝑓 ∈ ( ( Base ‘ 𝑠 ) ↑m ( Base ‘ 𝑟 ) ) ∣ ( ( 𝑓 ‘ ( 1r ‘ 𝑟 ) ) = ( 1r ‘ 𝑠 ) ∧ ∀ 𝑥 ∈ ( Base ‘ 𝑟 ) ∀ 𝑦 ∈ ( Base ‘ 𝑟 ) ( ( 𝑓 ‘ ( 𝑥 ( +g ‘ 𝑟 ) 𝑦 ) ) = ( ( 𝑓 ‘ 𝑥 ) ( +g ‘ 𝑠 ) ( 𝑓 ‘ 𝑦 ) ) ∧ ( 𝑓 ‘ ( 𝑥 ( .r ‘ 𝑟 ) 𝑦 ) ) = ( ( 𝑓 ‘ 𝑥 ) ( .r ‘ 𝑠 ) ( 𝑓 ‘ 𝑦 ) ) ) ) } )
17 8 9 16 csbie2 ⊢ ⦋ ( Base ‘ 𝑟 ) / 𝑣 ⦌ ⦋ ( Base ‘ 𝑠 ) / 𝑤 ⦌ { 𝑓 ∈ ( 𝑤 ↑m 𝑣 ) ∣ ( ( 𝑓 ‘ ( 1r ‘ 𝑟 ) ) = ( 1r ‘ 𝑠 ) ∧ ∀ 𝑥 ∈ 𝑣 ∀ 𝑦 ∈ 𝑣 ( ( 𝑓 ‘ ( 𝑥 ( +g ‘ 𝑟 ) 𝑦 ) ) = ( ( 𝑓 ‘ 𝑥 ) ( +g ‘ 𝑠 ) ( 𝑓 ‘ 𝑦 ) ) ∧ ( 𝑓 ‘ ( 𝑥 ( .r ‘ 𝑟 ) 𝑦 ) ) = ( ( 𝑓 ‘ 𝑥 ) ( .r ‘ 𝑠 ) ( 𝑓 ‘ 𝑦 ) ) ) ) } = { 𝑓 ∈ ( ( Base ‘ 𝑠 ) ↑m ( Base ‘ 𝑟 ) ) ∣ ( ( 𝑓 ‘ ( 1r ‘ 𝑟 ) ) = ( 1r ‘ 𝑠 ) ∧ ∀ 𝑥 ∈ ( Base ‘ 𝑟 ) ∀ 𝑦 ∈ ( Base ‘ 𝑟 ) ( ( 𝑓 ‘ ( 𝑥 ( +g ‘ 𝑟 ) 𝑦 ) ) = ( ( 𝑓 ‘ 𝑥 ) ( +g ‘ 𝑠 ) ( 𝑓 ‘ 𝑦 ) ) ∧ ( 𝑓 ‘ ( 𝑥 ( .r ‘ 𝑟 ) 𝑦 ) ) = ( ( 𝑓 ‘ 𝑥 ) ( .r ‘ 𝑠 ) ( 𝑓 ‘ 𝑦 ) ) ) ) }
18 inrab ⊢ ( { 𝑓 ∈ ( ( Base ‘ 𝑠 ) ↑m ( Base ‘ 𝑟 ) ) ∣ ∀ 𝑥 ∈ ( Base ‘ 𝑟 ) ∀ 𝑦 ∈ ( Base ‘ 𝑟 ) ( 𝑓 ‘ ( 𝑥 ( +g ‘ 𝑟 ) 𝑦 ) ) = ( ( 𝑓 ‘ 𝑥 ) ( +g ‘ 𝑠 ) ( 𝑓 ‘ 𝑦 ) ) } ∩ { 𝑓 ∈ ( ( Base ‘ 𝑠 ) ↑m ( Base ‘ 𝑟 ) ) ∣ ( ∀ 𝑥 ∈ ( Base ‘ 𝑟 ) ∀ 𝑦 ∈ ( Base ‘ 𝑟 ) ( 𝑓 ‘ ( 𝑥 ( .r ‘ 𝑟 ) 𝑦 ) ) = ( ( 𝑓 ‘ 𝑥 ) ( .r ‘ 𝑠 ) ( 𝑓 ‘ 𝑦 ) ) ∧ ( 𝑓 ‘ ( 1r ‘ 𝑟 ) ) = ( 1r ‘ 𝑠 ) ) } ) = { 𝑓 ∈ ( ( Base ‘ 𝑠 ) ↑m ( Base ‘ 𝑟 ) ) ∣ ( ∀ 𝑥 ∈ ( Base ‘ 𝑟 ) ∀ 𝑦 ∈ ( Base ‘ 𝑟 ) ( 𝑓 ‘ ( 𝑥 ( +g ‘ 𝑟 ) 𝑦 ) ) = ( ( 𝑓 ‘ 𝑥 ) ( +g ‘ 𝑠 ) ( 𝑓 ‘ 𝑦 ) ) ∧ ( ∀ 𝑥 ∈ ( Base ‘ 𝑟 ) ∀ 𝑦 ∈ ( Base ‘ 𝑟 ) ( 𝑓 ‘ ( 𝑥 ( .r ‘ 𝑟 ) 𝑦 ) ) = ( ( 𝑓 ‘ 𝑥 ) ( .r ‘ 𝑠 ) ( 𝑓 ‘ 𝑦 ) ) ∧ ( 𝑓 ‘ ( 1r ‘ 𝑟 ) ) = ( 1r ‘ 𝑠 ) ) ) }
19 7 17 18 3eqtr4i ⊢ ⦋ ( Base ‘ 𝑟 ) / 𝑣 ⦌ ⦋ ( Base ‘ 𝑠 ) / 𝑤 ⦌ { 𝑓 ∈ ( 𝑤 ↑m 𝑣 ) ∣ ( ( 𝑓 ‘ ( 1r ‘ 𝑟 ) ) = ( 1r ‘ 𝑠 ) ∧ ∀ 𝑥 ∈ 𝑣 ∀ 𝑦 ∈ 𝑣 ( ( 𝑓 ‘ ( 𝑥 ( +g ‘ 𝑟 ) 𝑦 ) ) = ( ( 𝑓 ‘ 𝑥 ) ( +g ‘ 𝑠 ) ( 𝑓 ‘ 𝑦 ) ) ∧ ( 𝑓 ‘ ( 𝑥 ( .r ‘ 𝑟 ) 𝑦 ) ) = ( ( 𝑓 ‘ 𝑥 ) ( .r ‘ 𝑠 ) ( 𝑓 ‘ 𝑦 ) ) ) ) } = ( { 𝑓 ∈ ( ( Base ‘ 𝑠 ) ↑m ( Base ‘ 𝑟 ) ) ∣ ∀ 𝑥 ∈ ( Base ‘ 𝑟 ) ∀ 𝑦 ∈ ( Base ‘ 𝑟 ) ( 𝑓 ‘ ( 𝑥 ( +g ‘ 𝑟 ) 𝑦 ) ) = ( ( 𝑓 ‘ 𝑥 ) ( +g ‘ 𝑠 ) ( 𝑓 ‘ 𝑦 ) ) } ∩ { 𝑓 ∈ ( ( Base ‘ 𝑠 ) ↑m ( Base ‘ 𝑟 ) ) ∣ ( ∀ 𝑥 ∈ ( Base ‘ 𝑟 ) ∀ 𝑦 ∈ ( Base ‘ 𝑟 ) ( 𝑓 ‘ ( 𝑥 ( .r ‘ 𝑟 ) 𝑦 ) ) = ( ( 𝑓 ‘ 𝑥 ) ( .r ‘ 𝑠 ) ( 𝑓 ‘ 𝑦 ) ) ∧ ( 𝑓 ‘ ( 1r ‘ 𝑟 ) ) = ( 1r ‘ 𝑠 ) ) } )
20 ringgrp ⊢ ( 𝑟 ∈ Ring → 𝑟 ∈ Grp )
21 ringgrp ⊢ ( 𝑠 ∈ Ring → 𝑠 ∈ Grp )
22 eqid ⊢ ( Base ‘ 𝑟 ) = ( Base ‘ 𝑟 )
23 eqid ⊢ ( Base ‘ 𝑠 ) = ( Base ‘ 𝑠 )
24 eqid ⊢ ( +g ‘ 𝑟 ) = ( +g ‘ 𝑟 )
25 eqid ⊢ ( +g ‘ 𝑠 ) = ( +g ‘ 𝑠 )
26 22 23 24 25 isghm3 ⊢ ( ( 𝑟 ∈ Grp ∧ 𝑠 ∈ Grp ) → ( 𝑓 ∈ ( 𝑟 GrpHom 𝑠 ) ↔ ( 𝑓 : ( Base ‘ 𝑟 ) ⟶ ( Base ‘ 𝑠 ) ∧ ∀ 𝑥 ∈ ( Base ‘ 𝑟 ) ∀ 𝑦 ∈ ( Base ‘ 𝑟 ) ( 𝑓 ‘ ( 𝑥 ( +g ‘ 𝑟 ) 𝑦 ) ) = ( ( 𝑓 ‘ 𝑥 ) ( +g ‘ 𝑠 ) ( 𝑓 ‘ 𝑦 ) ) ) ) )
27 20 21 26 syl2an ⊢ ( ( 𝑟 ∈ Ring ∧ 𝑠 ∈ Ring ) → ( 𝑓 ∈ ( 𝑟 GrpHom 𝑠 ) ↔ ( 𝑓 : ( Base ‘ 𝑟 ) ⟶ ( Base ‘ 𝑠 ) ∧ ∀ 𝑥 ∈ ( Base ‘ 𝑟 ) ∀ 𝑦 ∈ ( Base ‘ 𝑟 ) ( 𝑓 ‘ ( 𝑥 ( +g ‘ 𝑟 ) 𝑦 ) ) = ( ( 𝑓 ‘ 𝑥 ) ( +g ‘ 𝑠 ) ( 𝑓 ‘ 𝑦 ) ) ) ) )
28 27 abbi2dv ⊢ ( ( 𝑟 ∈ Ring ∧ 𝑠 ∈ Ring ) → ( 𝑟 GrpHom 𝑠 ) = { 𝑓 ∣ ( 𝑓 : ( Base ‘ 𝑟 ) ⟶ ( Base ‘ 𝑠 ) ∧ ∀ 𝑥 ∈ ( Base ‘ 𝑟 ) ∀ 𝑦 ∈ ( Base ‘ 𝑟 ) ( 𝑓 ‘ ( 𝑥 ( +g ‘ 𝑟 ) 𝑦 ) ) = ( ( 𝑓 ‘ 𝑥 ) ( +g ‘ 𝑠 ) ( 𝑓 ‘ 𝑦 ) ) ) } )
29 df-rab ⊢ { 𝑓 ∈ ( ( Base ‘ 𝑠 ) ↑m ( Base ‘ 𝑟 ) ) ∣ ∀ 𝑥 ∈ ( Base ‘ 𝑟 ) ∀ 𝑦 ∈ ( Base ‘ 𝑟 ) ( 𝑓 ‘ ( 𝑥 ( +g ‘ 𝑟 ) 𝑦 ) ) = ( ( 𝑓 ‘ 𝑥 ) ( +g ‘ 𝑠 ) ( 𝑓 ‘ 𝑦 ) ) } = { 𝑓 ∣ ( 𝑓 ∈ ( ( Base ‘ 𝑠 ) ↑m ( Base ‘ 𝑟 ) ) ∧ ∀ 𝑥 ∈ ( Base ‘ 𝑟 ) ∀ 𝑦 ∈ ( Base ‘ 𝑟 ) ( 𝑓 ‘ ( 𝑥 ( +g ‘ 𝑟 ) 𝑦 ) ) = ( ( 𝑓 ‘ 𝑥 ) ( +g ‘ 𝑠 ) ( 𝑓 ‘ 𝑦 ) ) ) }
30 9 8 elmap ⊢ ( 𝑓 ∈ ( ( Base ‘ 𝑠 ) ↑m ( Base ‘ 𝑟 ) ) ↔ 𝑓 : ( Base ‘ 𝑟 ) ⟶ ( Base ‘ 𝑠 ) )
31 30 anbi1i ⊢ ( ( 𝑓 ∈ ( ( Base ‘ 𝑠 ) ↑m ( Base ‘ 𝑟 ) ) ∧ ∀ 𝑥 ∈ ( Base ‘ 𝑟 ) ∀ 𝑦 ∈ ( Base ‘ 𝑟 ) ( 𝑓 ‘ ( 𝑥 ( +g ‘ 𝑟 ) 𝑦 ) ) = ( ( 𝑓 ‘ 𝑥 ) ( +g ‘ 𝑠 ) ( 𝑓 ‘ 𝑦 ) ) ) ↔ ( 𝑓 : ( Base ‘ 𝑟 ) ⟶ ( Base ‘ 𝑠 ) ∧ ∀ 𝑥 ∈ ( Base ‘ 𝑟 ) ∀ 𝑦 ∈ ( Base ‘ 𝑟 ) ( 𝑓 ‘ ( 𝑥 ( +g ‘ 𝑟 ) 𝑦 ) ) = ( ( 𝑓 ‘ 𝑥 ) ( +g ‘ 𝑠 ) ( 𝑓 ‘ 𝑦 ) ) ) )
32 31 abbii ⊢ { 𝑓 ∣ ( 𝑓 ∈ ( ( Base ‘ 𝑠 ) ↑m ( Base ‘ 𝑟 ) ) ∧ ∀ 𝑥 ∈ ( Base ‘ 𝑟 ) ∀ 𝑦 ∈ ( Base ‘ 𝑟 ) ( 𝑓 ‘ ( 𝑥 ( +g ‘ 𝑟 ) 𝑦 ) ) = ( ( 𝑓 ‘ 𝑥 ) ( +g ‘ 𝑠 ) ( 𝑓 ‘ 𝑦 ) ) ) } = { 𝑓 ∣ ( 𝑓 : ( Base ‘ 𝑟 ) ⟶ ( Base ‘ 𝑠 ) ∧ ∀ 𝑥 ∈ ( Base ‘ 𝑟 ) ∀ 𝑦 ∈ ( Base ‘ 𝑟 ) ( 𝑓 ‘ ( 𝑥 ( +g ‘ 𝑟 ) 𝑦 ) ) = ( ( 𝑓 ‘ 𝑥 ) ( +g ‘ 𝑠 ) ( 𝑓 ‘ 𝑦 ) ) ) }
33 29 32 eqtri ⊢ { 𝑓 ∈ ( ( Base ‘ 𝑠 ) ↑m ( Base ‘ 𝑟 ) ) ∣ ∀ 𝑥 ∈ ( Base ‘ 𝑟 ) ∀ 𝑦 ∈ ( Base ‘ 𝑟 ) ( 𝑓 ‘ ( 𝑥 ( +g ‘ 𝑟 ) 𝑦 ) ) = ( ( 𝑓 ‘ 𝑥 ) ( +g ‘ 𝑠 ) ( 𝑓 ‘ 𝑦 ) ) } = { 𝑓 ∣ ( 𝑓 : ( Base ‘ 𝑟 ) ⟶ ( Base ‘ 𝑠 ) ∧ ∀ 𝑥 ∈ ( Base ‘ 𝑟 ) ∀ 𝑦 ∈ ( Base ‘ 𝑟 ) ( 𝑓 ‘ ( 𝑥 ( +g ‘ 𝑟 ) 𝑦 ) ) = ( ( 𝑓 ‘ 𝑥 ) ( +g ‘ 𝑠 ) ( 𝑓 ‘ 𝑦 ) ) ) }
34 28 33 eqtr4di ⊢ ( ( 𝑟 ∈ Ring ∧ 𝑠 ∈ Ring ) → ( 𝑟 GrpHom 𝑠 ) = { 𝑓 ∈ ( ( Base ‘ 𝑠 ) ↑m ( Base ‘ 𝑟 ) ) ∣ ∀ 𝑥 ∈ ( Base ‘ 𝑟 ) ∀ 𝑦 ∈ ( Base ‘ 𝑟 ) ( 𝑓 ‘ ( 𝑥 ( +g ‘ 𝑟 ) 𝑦 ) ) = ( ( 𝑓 ‘ 𝑥 ) ( +g ‘ 𝑠 ) ( 𝑓 ‘ 𝑦 ) ) } )
35 eqid ⊢ ( mulGrp ‘ 𝑟 ) = ( mulGrp ‘ 𝑟 )
36 35 ringmgp ⊢ ( 𝑟 ∈ Ring → ( mulGrp ‘ 𝑟 ) ∈ Mnd )
37 eqid ⊢ ( mulGrp ‘ 𝑠 ) = ( mulGrp ‘ 𝑠 )
38 37 ringmgp ⊢ ( 𝑠 ∈ Ring → ( mulGrp ‘ 𝑠 ) ∈ Mnd )
39 35 22 mgpbas ⊢ ( Base ‘ 𝑟 ) = ( Base ‘ ( mulGrp ‘ 𝑟 ) )
40 37 23 mgpbas ⊢ ( Base ‘ 𝑠 ) = ( Base ‘ ( mulGrp ‘ 𝑠 ) )
41 eqid ⊢ ( .r ‘ 𝑟 ) = ( .r ‘ 𝑟 )
42 35 41 mgpplusg ⊢ ( .r ‘ 𝑟 ) = ( +g ‘ ( mulGrp ‘ 𝑟 ) )
43 eqid ⊢ ( .r ‘ 𝑠 ) = ( .r ‘ 𝑠 )
44 37 43 mgpplusg ⊢ ( .r ‘ 𝑠 ) = ( +g ‘ ( mulGrp ‘ 𝑠 ) )
45 eqid ⊢ ( 1r ‘ 𝑟 ) = ( 1r ‘ 𝑟 )
46 35 45 ringidval ⊢ ( 1r ‘ 𝑟 ) = ( 0g ‘ ( mulGrp ‘ 𝑟 ) )
47 eqid ⊢ ( 1r ‘ 𝑠 ) = ( 1r ‘ 𝑠 )
48 37 47 ringidval ⊢ ( 1r ‘ 𝑠 ) = ( 0g ‘ ( mulGrp ‘ 𝑠 ) )
49 39 40 42 44 46 48 ismhm ⊢ ( 𝑓 ∈ ( ( mulGrp ‘ 𝑟 ) MndHom ( mulGrp ‘ 𝑠 ) ) ↔ ( ( ( mulGrp ‘ 𝑟 ) ∈ Mnd ∧ ( mulGrp ‘ 𝑠 ) ∈ Mnd ) ∧ ( 𝑓 : ( Base ‘ 𝑟 ) ⟶ ( Base ‘ 𝑠 ) ∧ ∀ 𝑥 ∈ ( Base ‘ 𝑟 ) ∀ 𝑦 ∈ ( Base ‘ 𝑟 ) ( 𝑓 ‘ ( 𝑥 ( .r ‘ 𝑟 ) 𝑦 ) ) = ( ( 𝑓 ‘ 𝑥 ) ( .r ‘ 𝑠 ) ( 𝑓 ‘ 𝑦 ) ) ∧ ( 𝑓 ‘ ( 1r ‘ 𝑟 ) ) = ( 1r ‘ 𝑠 ) ) ) )
50 49 baib ⊢ ( ( ( mulGrp ‘ 𝑟 ) ∈ Mnd ∧ ( mulGrp ‘ 𝑠 ) ∈ Mnd ) → ( 𝑓 ∈ ( ( mulGrp ‘ 𝑟 ) MndHom ( mulGrp ‘ 𝑠 ) ) ↔ ( 𝑓 : ( Base ‘ 𝑟 ) ⟶ ( Base ‘ 𝑠 ) ∧ ∀ 𝑥 ∈ ( Base ‘ 𝑟 ) ∀ 𝑦 ∈ ( Base ‘ 𝑟 ) ( 𝑓 ‘ ( 𝑥 ( .r ‘ 𝑟 ) 𝑦 ) ) = ( ( 𝑓 ‘ 𝑥 ) ( .r ‘ 𝑠 ) ( 𝑓 ‘ 𝑦 ) ) ∧ ( 𝑓 ‘ ( 1r ‘ 𝑟 ) ) = ( 1r ‘ 𝑠 ) ) ) )
51 36 38 50 syl2an ⊢ ( ( 𝑟 ∈ Ring ∧ 𝑠 ∈ Ring ) → ( 𝑓 ∈ ( ( mulGrp ‘ 𝑟 ) MndHom ( mulGrp ‘ 𝑠 ) ) ↔ ( 𝑓 : ( Base ‘ 𝑟 ) ⟶ ( Base ‘ 𝑠 ) ∧ ∀ 𝑥 ∈ ( Base ‘ 𝑟 ) ∀ 𝑦 ∈ ( Base ‘ 𝑟 ) ( 𝑓 ‘ ( 𝑥 ( .r ‘ 𝑟 ) 𝑦 ) ) = ( ( 𝑓 ‘ 𝑥 ) ( .r ‘ 𝑠 ) ( 𝑓 ‘ 𝑦 ) ) ∧ ( 𝑓 ‘ ( 1r ‘ 𝑟 ) ) = ( 1r ‘ 𝑠 ) ) ) )
52 51 abbi2dv ⊢ ( ( 𝑟 ∈ Ring ∧ 𝑠 ∈ Ring ) → ( ( mulGrp ‘ 𝑟 ) MndHom ( mulGrp ‘ 𝑠 ) ) = { 𝑓 ∣ ( 𝑓 : ( Base ‘ 𝑟 ) ⟶ ( Base ‘ 𝑠 ) ∧ ∀ 𝑥 ∈ ( Base ‘ 𝑟 ) ∀ 𝑦 ∈ ( Base ‘ 𝑟 ) ( 𝑓 ‘ ( 𝑥 ( .r ‘ 𝑟 ) 𝑦 ) ) = ( ( 𝑓 ‘ 𝑥 ) ( .r ‘ 𝑠 ) ( 𝑓 ‘ 𝑦 ) ) ∧ ( 𝑓 ‘ ( 1r ‘ 𝑟 ) ) = ( 1r ‘ 𝑠 ) ) } )
53 df-rab ⊢ { 𝑓 ∈ ( ( Base ‘ 𝑠 ) ↑m ( Base ‘ 𝑟 ) ) ∣ ( ∀ 𝑥 ∈ ( Base ‘ 𝑟 ) ∀ 𝑦 ∈ ( Base ‘ 𝑟 ) ( 𝑓 ‘ ( 𝑥 ( .r ‘ 𝑟 ) 𝑦 ) ) = ( ( 𝑓 ‘ 𝑥 ) ( .r ‘ 𝑠 ) ( 𝑓 ‘ 𝑦 ) ) ∧ ( 𝑓 ‘ ( 1r ‘ 𝑟 ) ) = ( 1r ‘ 𝑠 ) ) } = { 𝑓 ∣ ( 𝑓 ∈ ( ( Base ‘ 𝑠 ) ↑m ( Base ‘ 𝑟 ) ) ∧ ( ∀ 𝑥 ∈ ( Base ‘ 𝑟 ) ∀ 𝑦 ∈ ( Base ‘ 𝑟 ) ( 𝑓 ‘ ( 𝑥 ( .r ‘ 𝑟 ) 𝑦 ) ) = ( ( 𝑓 ‘ 𝑥 ) ( .r ‘ 𝑠 ) ( 𝑓 ‘ 𝑦 ) ) ∧ ( 𝑓 ‘ ( 1r ‘ 𝑟 ) ) = ( 1r ‘ 𝑠 ) ) ) }
54 30 anbi1i ⊢ ( ( 𝑓 ∈ ( ( Base ‘ 𝑠 ) ↑m ( Base ‘ 𝑟 ) ) ∧ ( ∀ 𝑥 ∈ ( Base ‘ 𝑟 ) ∀ 𝑦 ∈ ( Base ‘ 𝑟 ) ( 𝑓 ‘ ( 𝑥 ( .r ‘ 𝑟 ) 𝑦 ) ) = ( ( 𝑓 ‘ 𝑥 ) ( .r ‘ 𝑠 ) ( 𝑓 ‘ 𝑦 ) ) ∧ ( 𝑓 ‘ ( 1r ‘ 𝑟 ) ) = ( 1r ‘ 𝑠 ) ) ) ↔ ( 𝑓 : ( Base ‘ 𝑟 ) ⟶ ( Base ‘ 𝑠 ) ∧ ( ∀ 𝑥 ∈ ( Base ‘ 𝑟 ) ∀ 𝑦 ∈ ( Base ‘ 𝑟 ) ( 𝑓 ‘ ( 𝑥 ( .r ‘ 𝑟 ) 𝑦 ) ) = ( ( 𝑓 ‘ 𝑥 ) ( .r ‘ 𝑠 ) ( 𝑓 ‘ 𝑦 ) ) ∧ ( 𝑓 ‘ ( 1r ‘ 𝑟 ) ) = ( 1r ‘ 𝑠 ) ) ) )
55 3anass ⊢ ( ( 𝑓 : ( Base ‘ 𝑟 ) ⟶ ( Base ‘ 𝑠 ) ∧ ∀ 𝑥 ∈ ( Base ‘ 𝑟 ) ∀ 𝑦 ∈ ( Base ‘ 𝑟 ) ( 𝑓 ‘ ( 𝑥 ( .r ‘ 𝑟 ) 𝑦 ) ) = ( ( 𝑓 ‘ 𝑥 ) ( .r ‘ 𝑠 ) ( 𝑓 ‘ 𝑦 ) ) ∧ ( 𝑓 ‘ ( 1r ‘ 𝑟 ) ) = ( 1r ‘ 𝑠 ) ) ↔ ( 𝑓 : ( Base ‘ 𝑟 ) ⟶ ( Base ‘ 𝑠 ) ∧ ( ∀ 𝑥 ∈ ( Base ‘ 𝑟 ) ∀ 𝑦 ∈ ( Base ‘ 𝑟 ) ( 𝑓 ‘ ( 𝑥 ( .r ‘ 𝑟 ) 𝑦 ) ) = ( ( 𝑓 ‘ 𝑥 ) ( .r ‘ 𝑠 ) ( 𝑓 ‘ 𝑦 ) ) ∧ ( 𝑓 ‘ ( 1r ‘ 𝑟 ) ) = ( 1r ‘ 𝑠 ) ) ) )
56 54 55 bitr4i ⊢ ( ( 𝑓 ∈ ( ( Base ‘ 𝑠 ) ↑m ( Base ‘ 𝑟 ) ) ∧ ( ∀ 𝑥 ∈ ( Base ‘ 𝑟 ) ∀ 𝑦 ∈ ( Base ‘ 𝑟 ) ( 𝑓 ‘ ( 𝑥 ( .r ‘ 𝑟 ) 𝑦 ) ) = ( ( 𝑓 ‘ 𝑥 ) ( .r ‘ 𝑠 ) ( 𝑓 ‘ 𝑦 ) ) ∧ ( 𝑓 ‘ ( 1r ‘ 𝑟 ) ) = ( 1r ‘ 𝑠 ) ) ) ↔ ( 𝑓 : ( Base ‘ 𝑟 ) ⟶ ( Base ‘ 𝑠 ) ∧ ∀ 𝑥 ∈ ( Base ‘ 𝑟 ) ∀ 𝑦 ∈ ( Base ‘ 𝑟 ) ( 𝑓 ‘ ( 𝑥 ( .r ‘ 𝑟 ) 𝑦 ) ) = ( ( 𝑓 ‘ 𝑥 ) ( .r ‘ 𝑠 ) ( 𝑓 ‘ 𝑦 ) ) ∧ ( 𝑓 ‘ ( 1r ‘ 𝑟 ) ) = ( 1r ‘ 𝑠 ) ) )
57 56 abbii ⊢ { 𝑓 ∣ ( 𝑓 ∈ ( ( Base ‘ 𝑠 ) ↑m ( Base ‘ 𝑟 ) ) ∧ ( ∀ 𝑥 ∈ ( Base ‘ 𝑟 ) ∀ 𝑦 ∈ ( Base ‘ 𝑟 ) ( 𝑓 ‘ ( 𝑥 ( .r ‘ 𝑟 ) 𝑦 ) ) = ( ( 𝑓 ‘ 𝑥 ) ( .r ‘ 𝑠 ) ( 𝑓 ‘ 𝑦 ) ) ∧ ( 𝑓 ‘ ( 1r ‘ 𝑟 ) ) = ( 1r ‘ 𝑠 ) ) ) } = { 𝑓 ∣ ( 𝑓 : ( Base ‘ 𝑟 ) ⟶ ( Base ‘ 𝑠 ) ∧ ∀ 𝑥 ∈ ( Base ‘ 𝑟 ) ∀ 𝑦 ∈ ( Base ‘ 𝑟 ) ( 𝑓 ‘ ( 𝑥 ( .r ‘ 𝑟 ) 𝑦 ) ) = ( ( 𝑓 ‘ 𝑥 ) ( .r ‘ 𝑠 ) ( 𝑓 ‘ 𝑦 ) ) ∧ ( 𝑓 ‘ ( 1r ‘ 𝑟 ) ) = ( 1r ‘ 𝑠 ) ) }
58 53 57 eqtri ⊢ { 𝑓 ∈ ( ( Base ‘ 𝑠 ) ↑m ( Base ‘ 𝑟 ) ) ∣ ( ∀ 𝑥 ∈ ( Base ‘ 𝑟 ) ∀ 𝑦 ∈ ( Base ‘ 𝑟 ) ( 𝑓 ‘ ( 𝑥 ( .r ‘ 𝑟 ) 𝑦 ) ) = ( ( 𝑓 ‘ 𝑥 ) ( .r ‘ 𝑠 ) ( 𝑓 ‘ 𝑦 ) ) ∧ ( 𝑓 ‘ ( 1r ‘ 𝑟 ) ) = ( 1r ‘ 𝑠 ) ) } = { 𝑓 ∣ ( 𝑓 : ( Base ‘ 𝑟 ) ⟶ ( Base ‘ 𝑠 ) ∧ ∀ 𝑥 ∈ ( Base ‘ 𝑟 ) ∀ 𝑦 ∈ ( Base ‘ 𝑟 ) ( 𝑓 ‘ ( 𝑥 ( .r ‘ 𝑟 ) 𝑦 ) ) = ( ( 𝑓 ‘ 𝑥 ) ( .r ‘ 𝑠 ) ( 𝑓 ‘ 𝑦 ) ) ∧ ( 𝑓 ‘ ( 1r ‘ 𝑟 ) ) = ( 1r ‘ 𝑠 ) ) }
59 52 58 eqtr4di ⊢ ( ( 𝑟 ∈ Ring ∧ 𝑠 ∈ Ring ) → ( ( mulGrp ‘ 𝑟 ) MndHom ( mulGrp ‘ 𝑠 ) ) = { 𝑓 ∈ ( ( Base ‘ 𝑠 ) ↑m ( Base ‘ 𝑟 ) ) ∣ ( ∀ 𝑥 ∈ ( Base ‘ 𝑟 ) ∀ 𝑦 ∈ ( Base ‘ 𝑟 ) ( 𝑓 ‘ ( 𝑥 ( .r ‘ 𝑟 ) 𝑦 ) ) = ( ( 𝑓 ‘ 𝑥 ) ( .r ‘ 𝑠 ) ( 𝑓 ‘ 𝑦 ) ) ∧ ( 𝑓 ‘ ( 1r ‘ 𝑟 ) ) = ( 1r ‘ 𝑠 ) ) } )
60 34 59 ineq12d ⊢ ( ( 𝑟 ∈ Ring ∧ 𝑠 ∈ Ring ) → ( ( 𝑟 GrpHom 𝑠 ) ∩ ( ( mulGrp ‘ 𝑟 ) MndHom ( mulGrp ‘ 𝑠 ) ) ) = ( { 𝑓 ∈ ( ( Base ‘ 𝑠 ) ↑m ( Base ‘ 𝑟 ) ) ∣ ∀ 𝑥 ∈ ( Base ‘ 𝑟 ) ∀ 𝑦 ∈ ( Base ‘ 𝑟 ) ( 𝑓 ‘ ( 𝑥 ( +g ‘ 𝑟 ) 𝑦 ) ) = ( ( 𝑓 ‘ 𝑥 ) ( +g ‘ 𝑠 ) ( 𝑓 ‘ 𝑦 ) ) } ∩ { 𝑓 ∈ ( ( Base ‘ 𝑠 ) ↑m ( Base ‘ 𝑟 ) ) ∣ ( ∀ 𝑥 ∈ ( Base ‘ 𝑟 ) ∀ 𝑦 ∈ ( Base ‘ 𝑟 ) ( 𝑓 ‘ ( 𝑥 ( .r ‘ 𝑟 ) 𝑦 ) ) = ( ( 𝑓 ‘ 𝑥 ) ( .r ‘ 𝑠 ) ( 𝑓 ‘ 𝑦 ) ) ∧ ( 𝑓 ‘ ( 1r ‘ 𝑟 ) ) = ( 1r ‘ 𝑠 ) ) } ) )
61 19 60 eqtr4id ⊢ ( ( 𝑟 ∈ Ring ∧ 𝑠 ∈ Ring ) → ⦋ ( Base ‘ 𝑟 ) / 𝑣 ⦌ ⦋ ( Base ‘ 𝑠 ) / 𝑤 ⦌ { 𝑓 ∈ ( 𝑤 ↑m 𝑣 ) ∣ ( ( 𝑓 ‘ ( 1r ‘ 𝑟 ) ) = ( 1r ‘ 𝑠 ) ∧ ∀ 𝑥 ∈ 𝑣 ∀ 𝑦 ∈ 𝑣 ( ( 𝑓 ‘ ( 𝑥 ( +g ‘ 𝑟 ) 𝑦 ) ) = ( ( 𝑓 ‘ 𝑥 ) ( +g ‘ 𝑠 ) ( 𝑓 ‘ 𝑦 ) ) ∧ ( 𝑓 ‘ ( 𝑥 ( .r ‘ 𝑟 ) 𝑦 ) ) = ( ( 𝑓 ‘ 𝑥 ) ( .r ‘ 𝑠 ) ( 𝑓 ‘ 𝑦 ) ) ) ) } = ( ( 𝑟 GrpHom 𝑠 ) ∩ ( ( mulGrp ‘ 𝑟 ) MndHom ( mulGrp ‘ 𝑠 ) ) ) )
62 61 mpoeq3ia ⊢ ( 𝑟 ∈ Ring , 𝑠 ∈ Ring ↦ ⦋ ( Base ‘ 𝑟 ) / 𝑣 ⦌ ⦋ ( Base ‘ 𝑠 ) / 𝑤 ⦌ { 𝑓 ∈ ( 𝑤 ↑m 𝑣 ) ∣ ( ( 𝑓 ‘ ( 1r ‘ 𝑟 ) ) = ( 1r ‘ 𝑠 ) ∧ ∀ 𝑥 ∈ 𝑣 ∀ 𝑦 ∈ 𝑣 ( ( 𝑓 ‘ ( 𝑥 ( +g ‘ 𝑟 ) 𝑦 ) ) = ( ( 𝑓 ‘ 𝑥 ) ( +g ‘ 𝑠 ) ( 𝑓 ‘ 𝑦 ) ) ∧ ( 𝑓 ‘ ( 𝑥 ( .r ‘ 𝑟 ) 𝑦 ) ) = ( ( 𝑓 ‘ 𝑥 ) ( .r ‘ 𝑠 ) ( 𝑓 ‘ 𝑦 ) ) ) ) } ) = ( 𝑟 ∈ Ring , 𝑠 ∈ Ring ↦ ( ( 𝑟 GrpHom 𝑠 ) ∩ ( ( mulGrp ‘ 𝑟 ) MndHom ( mulGrp ‘ 𝑠 ) ) ) )
63 1 62 eqtri ⊢ RingHom = ( 𝑟 ∈ Ring , 𝑠 ∈ Ring ↦ ( ( 𝑟 GrpHom 𝑠 ) ∩ ( ( mulGrp ‘ 𝑟 ) MndHom ( mulGrp ‘ 𝑠 ) ) ) )