Theorem dfrhm2 14399

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.)

Assertion

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

Distinct variable group:   𝑠,𝑟

Proof of Theorem dfrhm2

Dummy variables 𝑣 𝑤 𝑓 𝑥 𝑦 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		df-rhm 14397	. 2 ⊢ RingHom = (𝑟 ∈ Ring, 𝑠 ∈ Ring ↦ ⦋(Base‘𝑟) / 𝑣⦌⦋(Base‘𝑠) / 𝑤⦌{𝑓 ∈ (𝑤 ↑𝑚 𝑣) ∣ ((𝑓‘(1r‘𝑟)) = (1r‘𝑠) ∧ ∀𝑥 ∈ 𝑣 ∀𝑦 ∈ 𝑣 ((𝑓‘(𝑥(+g‘𝑟)𝑦)) = ((𝑓‘𝑥)(+g‘𝑠)(𝑓‘𝑦)) ∧ (𝑓‘(𝑥(.r‘𝑟)𝑦)) = ((𝑓‘𝑥)(.r‘𝑠)(𝑓‘𝑦))))})
2		ancom 266	. . . . . . 7 ⊢ (((𝑓‘(1r‘𝑟)) = (1r‘𝑠) ∧ ∀𝑥 ∈ (Base‘𝑟)∀𝑦 ∈ (Base‘𝑟)((𝑓‘(𝑥(+g‘𝑟)𝑦)) = ((𝑓‘𝑥)(+g‘𝑠)(𝑓‘𝑦)) ∧ (𝑓‘(𝑥(.r‘𝑟)𝑦)) = ((𝑓‘𝑥)(.r‘𝑠)(𝑓‘𝑦)))) ↔ (∀𝑥 ∈ (Base‘𝑟)∀𝑦 ∈ (Base‘𝑟)((𝑓‘(𝑥(+g‘𝑟)𝑦)) = ((𝑓‘𝑥)(+g‘𝑠)(𝑓‘𝑦)) ∧ (𝑓‘(𝑥(.r‘𝑟)𝑦)) = ((𝑓‘𝑥)(.r‘𝑠)(𝑓‘𝑦))) ∧ (𝑓‘(1r‘𝑟)) = (1r‘𝑠)))
3		r19.26-2 2674	. . . . . . . 8 ⊢ (∀𝑥 ∈ (Base‘𝑟)∀𝑦 ∈ (Base‘𝑟)((𝑓‘(𝑥(+g‘𝑟)𝑦)) = ((𝑓‘𝑥)(+g‘𝑠)(𝑓‘𝑦)) ∧ (𝑓‘(𝑥(.r‘𝑟)𝑦)) = ((𝑓‘𝑥)(.r‘𝑠)(𝑓‘𝑦))) ↔ (∀𝑥 ∈ (Base‘𝑟)∀𝑦 ∈ (Base‘𝑟)(𝑓‘(𝑥(+g‘𝑟)𝑦)) = ((𝑓‘𝑥)(+g‘𝑠)(𝑓‘𝑦)) ∧ ∀𝑥 ∈ (Base‘𝑟)∀𝑦 ∈ (Base‘𝑟)(𝑓‘(𝑥(.r‘𝑟)𝑦)) = ((𝑓‘𝑥)(.r‘𝑠)(𝑓‘𝑦))))
4	3	anbi1i 458	. . . . . . 7 ⊢ ((∀𝑥 ∈ (Base‘𝑟)∀𝑦 ∈ (Base‘𝑟)((𝑓‘(𝑥(+g‘𝑟)𝑦)) = ((𝑓‘𝑥)(+g‘𝑠)(𝑓‘𝑦)) ∧ (𝑓‘(𝑥(.r‘𝑟)𝑦)) = ((𝑓‘𝑥)(.r‘𝑠)(𝑓‘𝑦))) ∧ (𝑓‘(1r‘𝑟)) = (1r‘𝑠)) ↔ ((∀𝑥 ∈ (Base‘𝑟)∀𝑦 ∈ (Base‘𝑟)(𝑓‘(𝑥(+g‘𝑟)𝑦)) = ((𝑓‘𝑥)(+g‘𝑠)(𝑓‘𝑦)) ∧ ∀𝑥 ∈ (Base‘𝑟)∀𝑦 ∈ (Base‘𝑟)(𝑓‘(𝑥(.r‘𝑟)𝑦)) = ((𝑓‘𝑥)(.r‘𝑠)(𝑓‘𝑦))) ∧ (𝑓‘(1r‘𝑟)) = (1r‘𝑠)))
5		anass 401	. . . . . . 7 ⊢ (((∀𝑥 ∈ (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 206	. . . . . 6 ⊢ (((𝑓‘(1r‘𝑟)) = (1r‘𝑠) ∧ ∀𝑥 ∈ (Base‘𝑟)∀𝑦 ∈ (Base‘𝑟)((𝑓‘(𝑥(+g‘𝑟)𝑦)) = ((𝑓‘𝑥)(+g‘𝑠)(𝑓‘𝑦)) ∧ (𝑓‘(𝑥(.r‘𝑟)𝑦)) = ((𝑓‘𝑥)(.r‘𝑠)(𝑓‘𝑦)))) ↔ (∀𝑥 ∈ (Base‘𝑟)∀𝑦 ∈ (Base‘𝑟)(𝑓‘(𝑥(+g‘𝑟)𝑦)) = ((𝑓‘𝑥)(+g‘𝑠)(𝑓‘𝑦)) ∧ (∀𝑥 ∈ (Base‘𝑟)∀𝑦 ∈ (Base‘𝑟)(𝑓‘(𝑥(.r‘𝑟)𝑦)) = ((𝑓‘𝑥)(.r‘𝑠)(𝑓‘𝑦)) ∧ (𝑓‘(1r‘𝑟)) = (1r‘𝑠))))
7	6	rabbii 2802	. . . . 5 ⊢ {𝑓 ∈ ((Base‘𝑠) ↑𝑚 (Base‘𝑟)) ∣ ((𝑓‘(1r‘𝑟)) = (1r‘𝑠) ∧ ∀𝑥 ∈ (Base‘𝑟)∀𝑦 ∈ (Base‘𝑟)((𝑓‘(𝑥(+g‘𝑟)𝑦)) = ((𝑓‘𝑥)(+g‘𝑠)(𝑓‘𝑦)) ∧ (𝑓‘(𝑥(.r‘𝑟)𝑦)) = ((𝑓‘𝑥)(.r‘𝑠)(𝑓‘𝑦))))} = {𝑓 ∈ ((Base‘𝑠) ↑𝑚 (Base‘𝑟)) ∣ (∀𝑥 ∈ (Base‘𝑟)∀𝑦 ∈ (Base‘𝑟)(𝑓‘(𝑥(+g‘𝑟)𝑦)) = ((𝑓‘𝑥)(+g‘𝑠)(𝑓‘𝑦)) ∧ (∀𝑥 ∈ (Base‘𝑟)∀𝑦 ∈ (Base‘𝑟)(𝑓‘(𝑥(.r‘𝑟)𝑦)) = ((𝑓‘𝑥)(.r‘𝑠)(𝑓‘𝑦)) ∧ (𝑓‘(1r‘𝑟)) = (1r‘𝑠)))}
8		basfn 13355	. . . . . . 7 ⊢ Base Fn V
9		vex 2818	. . . . . . 7 ⊢ 𝑟 ∈ V
10		funfvex 5692	. . . . . . . 8 ⊢ ((Fun Base ∧ 𝑟 ∈ dom Base) → (Base‘𝑟) ∈ V)
11	10	funfni 5463	. . . . . . 7 ⊢ ((Base Fn V ∧ 𝑟 ∈ V) → (Base‘𝑟) ∈ V)
12	8, 9, 11	mp2an 426	. . . . . 6 ⊢ (Base‘𝑟) ∈ V
13		vex 2818	. . . . . . 7 ⊢ 𝑠 ∈ V
14		funfvex 5692	. . . . . . . 8 ⊢ ((Fun Base ∧ 𝑠 ∈ dom Base) → (Base‘𝑠) ∈ V)
15	14	funfni 5463	. . . . . . 7 ⊢ ((Base Fn V ∧ 𝑠 ∈ V) → (Base‘𝑠) ∈ V)
16	8, 13, 15	mp2an 426	. . . . . 6 ⊢ (Base‘𝑠) ∈ V
17		oveq12 6067	. . . . . . . 8 ⊢ ((𝑤 = (Base‘𝑠) ∧ 𝑣 = (Base‘𝑟)) → (𝑤 ↑𝑚 𝑣) = ((Base‘𝑠) ↑𝑚 (Base‘𝑟)))
18	17	ancoms 268	. . . . . . 7 ⊢ ((𝑣 = (Base‘𝑟) ∧ 𝑤 = (Base‘𝑠)) → (𝑤 ↑𝑚 𝑣) = ((Base‘𝑠) ↑𝑚 (Base‘𝑟)))
19		raleq 2743	. . . . . . . . . 10 ⊢ (𝑣 = (Base‘𝑟) → (∀𝑦 ∈ 𝑣 ((𝑓‘(𝑥(+g‘𝑟)𝑦)) = ((𝑓‘𝑥)(+g‘𝑠)(𝑓‘𝑦)) ∧ (𝑓‘(𝑥(.r‘𝑟)𝑦)) = ((𝑓‘𝑥)(.r‘𝑠)(𝑓‘𝑦))) ↔ ∀𝑦 ∈ (Base‘𝑟)((𝑓‘(𝑥(+g‘𝑟)𝑦)) = ((𝑓‘𝑥)(+g‘𝑠)(𝑓‘𝑦)) ∧ (𝑓‘(𝑥(.r‘𝑟)𝑦)) = ((𝑓‘𝑥)(.r‘𝑠)(𝑓‘𝑦)))))
20	19	raleqbi1dv 2755	. . . . . . . . 9 ⊢ (𝑣 = (Base‘𝑟) → (∀𝑥 ∈ 𝑣 ∀𝑦 ∈ 𝑣 ((𝑓‘(𝑥(+g‘𝑟)𝑦)) = ((𝑓‘𝑥)(+g‘𝑠)(𝑓‘𝑦)) ∧ (𝑓‘(𝑥(.r‘𝑟)𝑦)) = ((𝑓‘𝑥)(.r‘𝑠)(𝑓‘𝑦))) ↔ ∀𝑥 ∈ (Base‘𝑟)∀𝑦 ∈ (Base‘𝑟)((𝑓‘(𝑥(+g‘𝑟)𝑦)) = ((𝑓‘𝑥)(+g‘𝑠)(𝑓‘𝑦)) ∧ (𝑓‘(𝑥(.r‘𝑟)𝑦)) = ((𝑓‘𝑥)(.r‘𝑠)(𝑓‘𝑦)))))
21	20	adantr 276	. . . . . . . 8 ⊢ ((𝑣 = (Base‘𝑟) ∧ 𝑤 = (Base‘𝑠)) → (∀𝑥 ∈ 𝑣 ∀𝑦 ∈ 𝑣 ((𝑓‘(𝑥(+g‘𝑟)𝑦)) = ((𝑓‘𝑥)(+g‘𝑠)(𝑓‘𝑦)) ∧ (𝑓‘(𝑥(.r‘𝑟)𝑦)) = ((𝑓‘𝑥)(.r‘𝑠)(𝑓‘𝑦))) ↔ ∀𝑥 ∈ (Base‘𝑟)∀𝑦 ∈ (Base‘𝑟)((𝑓‘(𝑥(+g‘𝑟)𝑦)) = ((𝑓‘𝑥)(+g‘𝑠)(𝑓‘𝑦)) ∧ (𝑓‘(𝑥(.r‘𝑟)𝑦)) = ((𝑓‘𝑥)(.r‘𝑠)(𝑓‘𝑦)))))
22	21	anbi2d 464	. . . . . . 7 ⊢ ((𝑣 = (Base‘𝑟) ∧ 𝑤 = (Base‘𝑠)) → (((𝑓‘(1r‘𝑟)) = (1r‘𝑠) ∧ ∀𝑥 ∈ 𝑣 ∀𝑦 ∈ 𝑣 ((𝑓‘(𝑥(+g‘𝑟)𝑦)) = ((𝑓‘𝑥)(+g‘𝑠)(𝑓‘𝑦)) ∧ (𝑓‘(𝑥(.r‘𝑟)𝑦)) = ((𝑓‘𝑥)(.r‘𝑠)(𝑓‘𝑦)))) ↔ ((𝑓‘(1r‘𝑟)) = (1r‘𝑠) ∧ ∀𝑥 ∈ (Base‘𝑟)∀𝑦 ∈ (Base‘𝑟)((𝑓‘(𝑥(+g‘𝑟)𝑦)) = ((𝑓‘𝑥)(+g‘𝑠)(𝑓‘𝑦)) ∧ (𝑓‘(𝑥(.r‘𝑟)𝑦)) = ((𝑓‘𝑥)(.r‘𝑠)(𝑓‘𝑦))))))
23	18, 22	rabeqbidv 2810	. . . . . 6 ⊢ ((𝑣 = (Base‘𝑟) ∧ 𝑤 = (Base‘𝑠)) → {𝑓 ∈ (𝑤 ↑𝑚 𝑣) ∣ ((𝑓‘(1r‘𝑟)) = (1r‘𝑠) ∧ ∀𝑥 ∈ 𝑣 ∀𝑦 ∈ 𝑣 ((𝑓‘(𝑥(+g‘𝑟)𝑦)) = ((𝑓‘𝑥)(+g‘𝑠)(𝑓‘𝑦)) ∧ (𝑓‘(𝑥(.r‘𝑟)𝑦)) = ((𝑓‘𝑥)(.r‘𝑠)(𝑓‘𝑦))))} = {𝑓 ∈ ((Base‘𝑠) ↑𝑚 (Base‘𝑟)) ∣ ((𝑓‘(1r‘𝑟)) = (1r‘𝑠) ∧ ∀𝑥 ∈ (Base‘𝑟)∀𝑦 ∈ (Base‘𝑟)((𝑓‘(𝑥(+g‘𝑟)𝑦)) = ((𝑓‘𝑥)(+g‘𝑠)(𝑓‘𝑦)) ∧ (𝑓‘(𝑥(.r‘𝑟)𝑦)) = ((𝑓‘𝑥)(.r‘𝑠)(𝑓‘𝑦))))})
24	12, 16, 23	csbie2 3191	. . . . 5 ⊢ ⦋(Base‘𝑟) / 𝑣⦌⦋(Base‘𝑠) / 𝑤⦌{𝑓 ∈ (𝑤 ↑𝑚 𝑣) ∣ ((𝑓‘(1r‘𝑟)) = (1r‘𝑠) ∧ ∀𝑥 ∈ 𝑣 ∀𝑦 ∈ 𝑣 ((𝑓‘(𝑥(+g‘𝑟)𝑦)) = ((𝑓‘𝑥)(+g‘𝑠)(𝑓‘𝑦)) ∧ (𝑓‘(𝑥(.r‘𝑟)𝑦)) = ((𝑓‘𝑥)(.r‘𝑠)(𝑓‘𝑦))))} = {𝑓 ∈ ((Base‘𝑠) ↑𝑚 (Base‘𝑟)) ∣ ((𝑓‘(1r‘𝑟)) = (1r‘𝑠) ∧ ∀𝑥 ∈ (Base‘𝑟)∀𝑦 ∈ (Base‘𝑟)((𝑓‘(𝑥(+g‘𝑟)𝑦)) = ((𝑓‘𝑥)(+g‘𝑠)(𝑓‘𝑦)) ∧ (𝑓‘(𝑥(.r‘𝑟)𝑦)) = ((𝑓‘𝑥)(.r‘𝑠)(𝑓‘𝑦))))}
25		inrab 3497	. . . . 5 ⊢ ({𝑓 ∈ ((Base‘𝑠) ↑𝑚 (Base‘𝑟)) ∣ ∀𝑥 ∈ (Base‘𝑟)∀𝑦 ∈ (Base‘𝑟)(𝑓‘(𝑥(+g‘𝑟)𝑦)) = ((𝑓‘𝑥)(+g‘𝑠)(𝑓‘𝑦))} ∩ {𝑓 ∈ ((Base‘𝑠) ↑𝑚 (Base‘𝑟)) ∣ (∀𝑥 ∈ (Base‘𝑟)∀𝑦 ∈ (Base‘𝑟)(𝑓‘(𝑥(.r‘𝑟)𝑦)) = ((𝑓‘𝑥)(.r‘𝑠)(𝑓‘𝑦)) ∧ (𝑓‘(1r‘𝑟)) = (1r‘𝑠))}) = {𝑓 ∈ ((Base‘𝑠) ↑𝑚 (Base‘𝑟)) ∣ (∀𝑥 ∈ (Base‘𝑟)∀𝑦 ∈ (Base‘𝑟)(𝑓‘(𝑥(+g‘𝑟)𝑦)) = ((𝑓‘𝑥)(+g‘𝑠)(𝑓‘𝑦)) ∧ (∀𝑥 ∈ (Base‘𝑟)∀𝑦 ∈ (Base‘𝑟)(𝑓‘(𝑥(.r‘𝑟)𝑦)) = ((𝑓‘𝑥)(.r‘𝑠)(𝑓‘𝑦)) ∧ (𝑓‘(1r‘𝑟)) = (1r‘𝑠)))}
26	7, 24, 25	3eqtr4i 2265	. . . 4 ⊢ ⦋(Base‘𝑟) / 𝑣⦌⦋(Base‘𝑠) / 𝑤⦌{𝑓 ∈ (𝑤 ↑𝑚 𝑣) ∣ ((𝑓‘(1r‘𝑟)) = (1r‘𝑠) ∧ ∀𝑥 ∈ 𝑣 ∀𝑦 ∈ 𝑣 ((𝑓‘(𝑥(+g‘𝑟)𝑦)) = ((𝑓‘𝑥)(+g‘𝑠)(𝑓‘𝑦)) ∧ (𝑓‘(𝑥(.r‘𝑟)𝑦)) = ((𝑓‘𝑥)(.r‘𝑠)(𝑓‘𝑦))))} = ({𝑓 ∈ ((Base‘𝑠) ↑𝑚 (Base‘𝑟)) ∣ ∀𝑥 ∈ (Base‘𝑟)∀𝑦 ∈ (Base‘𝑟)(𝑓‘(𝑥(+g‘𝑟)𝑦)) = ((𝑓‘𝑥)(+g‘𝑠)(𝑓‘𝑦))} ∩ {𝑓 ∈ ((Base‘𝑠) ↑𝑚 (Base‘𝑟)) ∣ (∀𝑥 ∈ (Base‘𝑟)∀𝑦 ∈ (Base‘𝑟)(𝑓‘(𝑥(.r‘𝑟)𝑦)) = ((𝑓‘𝑥)(.r‘𝑠)(𝑓‘𝑦)) ∧ (𝑓‘(1r‘𝑟)) = (1r‘𝑠))})
27		ringgrp 14244	. . . . . . . 8 ⊢ (𝑟 ∈ Ring → 𝑟 ∈ Grp)
28		ringgrp 14244	. . . . . . . 8 ⊢ (𝑠 ∈ Ring → 𝑠 ∈ Grp)
29		eqid 2234	. . . . . . . . 9 ⊢ (Base‘𝑟) = (Base‘𝑟)
30		eqid 2234	. . . . . . . . 9 ⊢ (Base‘𝑠) = (Base‘𝑠)
31		eqid 2234	. . . . . . . . 9 ⊢ (+g‘𝑟) = (+g‘𝑟)
32		eqid 2234	. . . . . . . . 9 ⊢ (+g‘𝑠) = (+g‘𝑠)
33	29, 30, 31, 32	isghm3 13997	. . . . . . . 8 ⊢ ((𝑟 ∈ Grp ∧ 𝑠 ∈ Grp) → (𝑓 ∈ (𝑟 GrpHom 𝑠) ↔ (𝑓:(Base‘𝑟)⟶(Base‘𝑠) ∧ ∀𝑥 ∈ (Base‘𝑟)∀𝑦 ∈ (Base‘𝑟)(𝑓‘(𝑥(+g‘𝑟)𝑦)) = ((𝑓‘𝑥)(+g‘𝑠)(𝑓‘𝑦)))))
34	27, 28, 33	syl2an 289	. . . . . . 7 ⊢ ((𝑟 ∈ Ring ∧ 𝑠 ∈ Ring) → (𝑓 ∈ (𝑟 GrpHom 𝑠) ↔ (𝑓:(Base‘𝑟)⟶(Base‘𝑠) ∧ ∀𝑥 ∈ (Base‘𝑟)∀𝑦 ∈ (Base‘𝑟)(𝑓‘(𝑥(+g‘𝑟)𝑦)) = ((𝑓‘𝑥)(+g‘𝑠)(𝑓‘𝑦)))))
35	34	eqabdv 2365	. . . . . 6 ⊢ ((𝑟 ∈ Ring ∧ 𝑠 ∈ Ring) → (𝑟 GrpHom 𝑠) = {𝑓 ∣ (𝑓:(Base‘𝑟)⟶(Base‘𝑠) ∧ ∀𝑥 ∈ (Base‘𝑟)∀𝑦 ∈ (Base‘𝑟)(𝑓‘(𝑥(+g‘𝑟)𝑦)) = ((𝑓‘𝑥)(+g‘𝑠)(𝑓‘𝑦)))})
36		df-rab 2531	. . . . . . 7 ⊢ {𝑓 ∈ ((Base‘𝑠) ↑𝑚 (Base‘𝑟)) ∣ ∀𝑥 ∈ (Base‘𝑟)∀𝑦 ∈ (Base‘𝑟)(𝑓‘(𝑥(+g‘𝑟)𝑦)) = ((𝑓‘𝑥)(+g‘𝑠)(𝑓‘𝑦))} = {𝑓 ∣ (𝑓 ∈ ((Base‘𝑠) ↑𝑚 (Base‘𝑟)) ∧ ∀𝑥 ∈ (Base‘𝑟)∀𝑦 ∈ (Base‘𝑟)(𝑓‘(𝑥(+g‘𝑟)𝑦)) = ((𝑓‘𝑥)(+g‘𝑠)(𝑓‘𝑦)))}
37	16, 12	elmap 6924	. . . . . . . . 9 ⊢ (𝑓 ∈ ((Base‘𝑠) ↑𝑚 (Base‘𝑟)) ↔ 𝑓:(Base‘𝑟)⟶(Base‘𝑠))
38	37	anbi1i 458	. . . . . . . 8 ⊢ ((𝑓 ∈ ((Base‘𝑠) ↑𝑚 (Base‘𝑟)) ∧ ∀𝑥 ∈ (Base‘𝑟)∀𝑦 ∈ (Base‘𝑟)(𝑓‘(𝑥(+g‘𝑟)𝑦)) = ((𝑓‘𝑥)(+g‘𝑠)(𝑓‘𝑦))) ↔ (𝑓:(Base‘𝑟)⟶(Base‘𝑠) ∧ ∀𝑥 ∈ (Base‘𝑟)∀𝑦 ∈ (Base‘𝑟)(𝑓‘(𝑥(+g‘𝑟)𝑦)) = ((𝑓‘𝑥)(+g‘𝑠)(𝑓‘𝑦))))
39	38	abbii 2350	. . . . . . 7 ⊢ {𝑓 ∣ (𝑓 ∈ ((Base‘𝑠) ↑𝑚 (Base‘𝑟)) ∧ ∀𝑥 ∈ (Base‘𝑟)∀𝑦 ∈ (Base‘𝑟)(𝑓‘(𝑥(+g‘𝑟)𝑦)) = ((𝑓‘𝑥)(+g‘𝑠)(𝑓‘𝑦)))} = {𝑓 ∣ (𝑓:(Base‘𝑟)⟶(Base‘𝑠) ∧ ∀𝑥 ∈ (Base‘𝑟)∀𝑦 ∈ (Base‘𝑟)(𝑓‘(𝑥(+g‘𝑟)𝑦)) = ((𝑓‘𝑥)(+g‘𝑠)(𝑓‘𝑦)))}
40	36, 39	eqtri 2255	. . . . . 6 ⊢ {𝑓 ∈ ((Base‘𝑠) ↑𝑚 (Base‘𝑟)) ∣ ∀𝑥 ∈ (Base‘𝑟)∀𝑦 ∈ (Base‘𝑟)(𝑓‘(𝑥(+g‘𝑟)𝑦)) = ((𝑓‘𝑥)(+g‘𝑠)(𝑓‘𝑦))} = {𝑓 ∣ (𝑓:(Base‘𝑟)⟶(Base‘𝑠) ∧ ∀𝑥 ∈ (Base‘𝑟)∀𝑦 ∈ (Base‘𝑟)(𝑓‘(𝑥(+g‘𝑟)𝑦)) = ((𝑓‘𝑥)(+g‘𝑠)(𝑓‘𝑦)))}
41	35, 40	eqtr4di 2285	. . . . 5 ⊢ ((𝑟 ∈ Ring ∧ 𝑠 ∈ Ring) → (𝑟 GrpHom 𝑠) = {𝑓 ∈ ((Base‘𝑠) ↑𝑚 (Base‘𝑟)) ∣ ∀𝑥 ∈ (Base‘𝑟)∀𝑦 ∈ (Base‘𝑟)(𝑓‘(𝑥(+g‘𝑟)𝑦)) = ((𝑓‘𝑥)(+g‘𝑠)(𝑓‘𝑦))})
42		eqid 2234	. . . . . . . . 9 ⊢ (mulGrp‘𝑟) = (mulGrp‘𝑟)
43	42	ringmgp 14245	. . . . . . . 8 ⊢ (𝑟 ∈ Ring → (mulGrp‘𝑟) ∈ Mnd)
44		eqid 2234	. . . . . . . . 9 ⊢ (mulGrp‘𝑠) = (mulGrp‘𝑠)
45	44	ringmgp 14245	. . . . . . . 8 ⊢ (𝑠 ∈ Ring → (mulGrp‘𝑠) ∈ Mnd)
46	42, 29	mgpbasg 14165	. . . . . . . . . . 11 ⊢ (𝑟 ∈ V → (Base‘𝑟) = (Base‘(mulGrp‘𝑟)))
47	46	elv 2819	. . . . . . . . . 10 ⊢ (Base‘𝑟) = (Base‘(mulGrp‘𝑟))
48	44, 30	mgpbasg 14165	. . . . . . . . . . 11 ⊢ (𝑠 ∈ V → (Base‘𝑠) = (Base‘(mulGrp‘𝑠)))
49	48	elv 2819	. . . . . . . . . 10 ⊢ (Base‘𝑠) = (Base‘(mulGrp‘𝑠))
50		eqid 2234	. . . . . . . . . . . 12 ⊢ (.r‘𝑟) = (.r‘𝑟)
51	42, 50	mgpplusgg 14163	. . . . . . . . . . 11 ⊢ (𝑟 ∈ V → (.r‘𝑟) = (+g‘(mulGrp‘𝑟)))
52	51	elv 2819	. . . . . . . . . 10 ⊢ (.r‘𝑟) = (+g‘(mulGrp‘𝑟))
53		eqid 2234	. . . . . . . . . . . 12 ⊢ (.r‘𝑠) = (.r‘𝑠)
54	44, 53	mgpplusgg 14163	. . . . . . . . . . 11 ⊢ (𝑠 ∈ V → (.r‘𝑠) = (+g‘(mulGrp‘𝑠)))
55	54	elv 2819	. . . . . . . . . 10 ⊢ (.r‘𝑠) = (+g‘(mulGrp‘𝑠))
56		eqid 2234	. . . . . . . . . . . 12 ⊢ (1r‘𝑟) = (1r‘𝑟)
57	42, 56	ringidvalg 14204	. . . . . . . . . . 11 ⊢ (𝑟 ∈ V → (1r‘𝑟) = (0g‘(mulGrp‘𝑟)))
58	57	elv 2819	. . . . . . . . . 10 ⊢ (1r‘𝑟) = (0g‘(mulGrp‘𝑟))
59		eqid 2234	. . . . . . . . . . . 12 ⊢ (1r‘𝑠) = (1r‘𝑠)
60	44, 59	ringidvalg 14204	. . . . . . . . . . 11 ⊢ (𝑠 ∈ V → (1r‘𝑠) = (0g‘(mulGrp‘𝑠)))
61	60	elv 2819	. . . . . . . . . 10 ⊢ (1r‘𝑠) = (0g‘(mulGrp‘𝑠))
62	47, 49, 52, 55, 58, 61	ismhm 13716	. . . . . . . . 9 ⊢ (𝑓 ∈ ((mulGrp‘𝑟) MndHom (mulGrp‘𝑠)) ↔ (((mulGrp‘𝑟) ∈ Mnd ∧ (mulGrp‘𝑠) ∈ Mnd) ∧ (𝑓:(Base‘𝑟)⟶(Base‘𝑠) ∧ ∀𝑥 ∈ (Base‘𝑟)∀𝑦 ∈ (Base‘𝑟)(𝑓‘(𝑥(.r‘𝑟)𝑦)) = ((𝑓‘𝑥)(.r‘𝑠)(𝑓‘𝑦)) ∧ (𝑓‘(1r‘𝑟)) = (1r‘𝑠))))
63	62	baib 927	. . . . . . . 8 ⊢ (((mulGrp‘𝑟) ∈ Mnd ∧ (mulGrp‘𝑠) ∈ Mnd) → (𝑓 ∈ ((mulGrp‘𝑟) MndHom (mulGrp‘𝑠)) ↔ (𝑓:(Base‘𝑟)⟶(Base‘𝑠) ∧ ∀𝑥 ∈ (Base‘𝑟)∀𝑦 ∈ (Base‘𝑟)(𝑓‘(𝑥(.r‘𝑟)𝑦)) = ((𝑓‘𝑥)(.r‘𝑠)(𝑓‘𝑦)) ∧ (𝑓‘(1r‘𝑟)) = (1r‘𝑠))))
64	43, 45, 63	syl2an 289	. . . . . . 7 ⊢ ((𝑟 ∈ Ring ∧ 𝑠 ∈ Ring) → (𝑓 ∈ ((mulGrp‘𝑟) MndHom (mulGrp‘𝑠)) ↔ (𝑓:(Base‘𝑟)⟶(Base‘𝑠) ∧ ∀𝑥 ∈ (Base‘𝑟)∀𝑦 ∈ (Base‘𝑟)(𝑓‘(𝑥(.r‘𝑟)𝑦)) = ((𝑓‘𝑥)(.r‘𝑠)(𝑓‘𝑦)) ∧ (𝑓‘(1r‘𝑟)) = (1r‘𝑠))))
65	64	eqabdv 2365	. . . . . 6 ⊢ ((𝑟 ∈ Ring ∧ 𝑠 ∈ Ring) → ((mulGrp‘𝑟) MndHom (mulGrp‘𝑠)) = {𝑓 ∣ (𝑓:(Base‘𝑟)⟶(Base‘𝑠) ∧ ∀𝑥 ∈ (Base‘𝑟)∀𝑦 ∈ (Base‘𝑟)(𝑓‘(𝑥(.r‘𝑟)𝑦)) = ((𝑓‘𝑥)(.r‘𝑠)(𝑓‘𝑦)) ∧ (𝑓‘(1r‘𝑟)) = (1r‘𝑠))})
66		df-rab 2531	. . . . . . 7 ⊢ {𝑓 ∈ ((Base‘𝑠) ↑𝑚 (Base‘𝑟)) ∣ (∀𝑥 ∈ (Base‘𝑟)∀𝑦 ∈ (Base‘𝑟)(𝑓‘(𝑥(.r‘𝑟)𝑦)) = ((𝑓‘𝑥)(.r‘𝑠)(𝑓‘𝑦)) ∧ (𝑓‘(1r‘𝑟)) = (1r‘𝑠))} = {𝑓 ∣ (𝑓 ∈ ((Base‘𝑠) ↑𝑚 (Base‘𝑟)) ∧ (∀𝑥 ∈ (Base‘𝑟)∀𝑦 ∈ (Base‘𝑟)(𝑓‘(𝑥(.r‘𝑟)𝑦)) = ((𝑓‘𝑥)(.r‘𝑠)(𝑓‘𝑦)) ∧ (𝑓‘(1r‘𝑟)) = (1r‘𝑠)))}
67	37	anbi1i 458	. . . . . . . . 9 ⊢ ((𝑓 ∈ ((Base‘𝑠) ↑𝑚 (Base‘𝑟)) ∧ (∀𝑥 ∈ (Base‘𝑟)∀𝑦 ∈ (Base‘𝑟)(𝑓‘(𝑥(.r‘𝑟)𝑦)) = ((𝑓‘𝑥)(.r‘𝑠)(𝑓‘𝑦)) ∧ (𝑓‘(1r‘𝑟)) = (1r‘𝑠))) ↔ (𝑓:(Base‘𝑟)⟶(Base‘𝑠) ∧ (∀𝑥 ∈ (Base‘𝑟)∀𝑦 ∈ (Base‘𝑟)(𝑓‘(𝑥(.r‘𝑟)𝑦)) = ((𝑓‘𝑥)(.r‘𝑠)(𝑓‘𝑦)) ∧ (𝑓‘(1r‘𝑟)) = (1r‘𝑠))))
68		3anass 1009	. . . . . . . . 9 ⊢ ((𝑓:(Base‘𝑟)⟶(Base‘𝑠) ∧ ∀𝑥 ∈ (Base‘𝑟)∀𝑦 ∈ (Base‘𝑟)(𝑓‘(𝑥(.r‘𝑟)𝑦)) = ((𝑓‘𝑥)(.r‘𝑠)(𝑓‘𝑦)) ∧ (𝑓‘(1r‘𝑟)) = (1r‘𝑠)) ↔ (𝑓:(Base‘𝑟)⟶(Base‘𝑠) ∧ (∀𝑥 ∈ (Base‘𝑟)∀𝑦 ∈ (Base‘𝑟)(𝑓‘(𝑥(.r‘𝑟)𝑦)) = ((𝑓‘𝑥)(.r‘𝑠)(𝑓‘𝑦)) ∧ (𝑓‘(1r‘𝑟)) = (1r‘𝑠))))
69	67, 68	bitr4i 187	. . . . . . . 8 ⊢ ((𝑓 ∈ ((Base‘𝑠) ↑𝑚 (Base‘𝑟)) ∧ (∀𝑥 ∈ (Base‘𝑟)∀𝑦 ∈ (Base‘𝑟)(𝑓‘(𝑥(.r‘𝑟)𝑦)) = ((𝑓‘𝑥)(.r‘𝑠)(𝑓‘𝑦)) ∧ (𝑓‘(1r‘𝑟)) = (1r‘𝑠))) ↔ (𝑓:(Base‘𝑟)⟶(Base‘𝑠) ∧ ∀𝑥 ∈ (Base‘𝑟)∀𝑦 ∈ (Base‘𝑟)(𝑓‘(𝑥(.r‘𝑟)𝑦)) = ((𝑓‘𝑥)(.r‘𝑠)(𝑓‘𝑦)) ∧ (𝑓‘(1r‘𝑟)) = (1r‘𝑠)))
70	69	abbii 2350	. . . . . . 7 ⊢ {𝑓 ∣ (𝑓 ∈ ((Base‘𝑠) ↑𝑚 (Base‘𝑟)) ∧ (∀𝑥 ∈ (Base‘𝑟)∀𝑦 ∈ (Base‘𝑟)(𝑓‘(𝑥(.r‘𝑟)𝑦)) = ((𝑓‘𝑥)(.r‘𝑠)(𝑓‘𝑦)) ∧ (𝑓‘(1r‘𝑟)) = (1r‘𝑠)))} = {𝑓 ∣ (𝑓:(Base‘𝑟)⟶(Base‘𝑠) ∧ ∀𝑥 ∈ (Base‘𝑟)∀𝑦 ∈ (Base‘𝑟)(𝑓‘(𝑥(.r‘𝑟)𝑦)) = ((𝑓‘𝑥)(.r‘𝑠)(𝑓‘𝑦)) ∧ (𝑓‘(1r‘𝑟)) = (1r‘𝑠))}
71	66, 70	eqtri 2255	. . . . . 6 ⊢ {𝑓 ∈ ((Base‘𝑠) ↑𝑚 (Base‘𝑟)) ∣ (∀𝑥 ∈ (Base‘𝑟)∀𝑦 ∈ (Base‘𝑟)(𝑓‘(𝑥(.r‘𝑟)𝑦)) = ((𝑓‘𝑥)(.r‘𝑠)(𝑓‘𝑦)) ∧ (𝑓‘(1r‘𝑟)) = (1r‘𝑠))} = {𝑓 ∣ (𝑓:(Base‘𝑟)⟶(Base‘𝑠) ∧ ∀𝑥 ∈ (Base‘𝑟)∀𝑦 ∈ (Base‘𝑟)(𝑓‘(𝑥(.r‘𝑟)𝑦)) = ((𝑓‘𝑥)(.r‘𝑠)(𝑓‘𝑦)) ∧ (𝑓‘(1r‘𝑟)) = (1r‘𝑠))}
72	65, 71	eqtr4di 2285	. . . . 5 ⊢ ((𝑟 ∈ Ring ∧ 𝑠 ∈ Ring) → ((mulGrp‘𝑟) MndHom (mulGrp‘𝑠)) = {𝑓 ∈ ((Base‘𝑠) ↑𝑚 (Base‘𝑟)) ∣ (∀𝑥 ∈ (Base‘𝑟)∀𝑦 ∈ (Base‘𝑟)(𝑓‘(𝑥(.r‘𝑟)𝑦)) = ((𝑓‘𝑥)(.r‘𝑠)(𝑓‘𝑦)) ∧ (𝑓‘(1r‘𝑟)) = (1r‘𝑠))})
73	41, 72	ineq12d 3427	. . . 4 ⊢ ((𝑟 ∈ Ring ∧ 𝑠 ∈ Ring) → ((𝑟 GrpHom 𝑠) ∩ ((mulGrp‘𝑟) MndHom (mulGrp‘𝑠))) = ({𝑓 ∈ ((Base‘𝑠) ↑𝑚 (Base‘𝑟)) ∣ ∀𝑥 ∈ (Base‘𝑟)∀𝑦 ∈ (Base‘𝑟)(𝑓‘(𝑥(+g‘𝑟)𝑦)) = ((𝑓‘𝑥)(+g‘𝑠)(𝑓‘𝑦))} ∩ {𝑓 ∈ ((Base‘𝑠) ↑𝑚 (Base‘𝑟)) ∣ (∀𝑥 ∈ (Base‘𝑟)∀𝑦 ∈ (Base‘𝑟)(𝑓‘(𝑥(.r‘𝑟)𝑦)) = ((𝑓‘𝑥)(.r‘𝑠)(𝑓‘𝑦)) ∧ (𝑓‘(1r‘𝑟)) = (1r‘𝑠))}))
74	26, 73	eqtr4id 2286	. . 3 ⊢ ((𝑟 ∈ Ring ∧ 𝑠 ∈ Ring) → ⦋(Base‘𝑟) / 𝑣⦌⦋(Base‘𝑠) / 𝑤⦌{𝑓 ∈ (𝑤 ↑𝑚 𝑣) ∣ ((𝑓‘(1r‘𝑟)) = (1r‘𝑠) ∧ ∀𝑥 ∈ 𝑣 ∀𝑦 ∈ 𝑣 ((𝑓‘(𝑥(+g‘𝑟)𝑦)) = ((𝑓‘𝑥)(+g‘𝑠)(𝑓‘𝑦)) ∧ (𝑓‘(𝑥(.r‘𝑟)𝑦)) = ((𝑓‘𝑥)(.r‘𝑠)(𝑓‘𝑦))))} = ((𝑟 GrpHom 𝑠) ∩ ((mulGrp‘𝑟) MndHom (mulGrp‘𝑠))))
75	74	mpoeq3ia 6126	. 2 ⊢ (𝑟 ∈ Ring, 𝑠 ∈ Ring ↦ ⦋(Base‘𝑟) / 𝑣⦌⦋(Base‘𝑠) / 𝑤⦌{𝑓 ∈ (𝑤 ↑𝑚 𝑣) ∣ ((𝑓‘(1r‘𝑟)) = (1r‘𝑠) ∧ ∀𝑥 ∈ 𝑣 ∀𝑦 ∈ 𝑣 ((𝑓‘(𝑥(+g‘𝑟)𝑦)) = ((𝑓‘𝑥)(+g‘𝑠)(𝑓‘𝑦)) ∧ (𝑓‘(𝑥(.r‘𝑟)𝑦)) = ((𝑓‘𝑥)(.r‘𝑠)(𝑓‘𝑦))))}) = (𝑟 ∈ Ring, 𝑠 ∈ Ring ↦ ((𝑟 GrpHom 𝑠) ∩ ((mulGrp‘𝑟) MndHom (mulGrp‘𝑠))))
76	1, 75	eqtri 2255	1 ⊢ RingHom = (𝑟 ∈ Ring, 𝑠 ∈ Ring ↦ ((𝑟 GrpHom 𝑠) ∩ ((mulGrp‘𝑟) MndHom (mulGrp‘𝑠))))

Syntax hints:   ∧ wa 104   ↔ wb 105   ∧ w3a 1005   = wceq 1398   ∈ wcel 2205  {cab 2220  ∀wral 2522  {crab 2526  Vcvv 2815  ⦋csb 3141   ∩ cin 3213   Fn wfn 5352  ⟶wf 5353  ‘cfv 5357  (class class class)co 6058   ∈ cmpo 6060   ↑_𝑚 cmap 6895  Basecbs 13296  +_gcplusg 13374  ._rcmulr 13375  0_gc0g 13553  Mndcmnd 13677   MndHom cmhm 13712  Grpcgrp 13755   GrpHom cghm 13993  mulGrpcmgp 14159  1_rcur 14202  Ringcrg 14239   RingHom crh 14395

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in1 619  ax-in2 620  ax-io 717  ax-5 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-10 1554  ax-11 1555  ax-i12 1556  ax-bndl 1558  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-13 2207  ax-14 2208  ax-ext 2216  ax-coll 4230  ax-sep 4233  ax-pow 4292  ax-pr 4327  ax-un 4559  ax-setind 4664  ax-cnex 8234  ax-resscn 8235  ax-1cn 8236  ax-1re 8237  ax-icn 8238  ax-addcl 8239  ax-addrcl 8240  ax-mulcl 8241  ax-addcom 8243  ax-addass 8245  ax-i2m1 8248  ax-0lt1 8249  ax-0id 8251  ax-rnegex 8252  ax-pre-ltirr 8255  ax-pre-ltadd 8259

This theorem depends on definitions:  df-bi 117  df-3an 1007  df-tru 1401  df-fal 1404  df-nf 1510  df-sb 1812  df-eu 2085  df-mo 2086  df-clab 2221  df-cleq 2227  df-clel 2230  df-nfc 2375  df-ne 2415  df-nel 2510  df-ral 2527  df-rex 2528  df-reu 2529  df-rab 2531  df-v 2817  df-sbc 3046  df-csb 3142  df-dif 3216  df-un 3218  df-in 3220  df-ss 3227  df-nul 3513  df-pw 3676  df-sn 3700  df-pr 3701  df-op 3703  df-uni 3920  df-int 3955  df-iun 3998  df-br 4115  df-opab 4177  df-mpt 4178  df-id 4419  df-xp 4760  df-rel 4761  df-cnv 4762  df-co 4763  df-dm 4764  df-rn 4765  df-res 4766  df-ima 4767  df-iota 5317  df-fun 5359  df-fn 5360  df-f 5361  df-f1 5362  df-fo 5363  df-f1o 5364  df-fv 5365  df-ov 6061  df-oprab 6062  df-mpo 6063  df-1st 6347  df-2nd 6348  df-map 6897  df-pnf 8326  df-mnf 8327  df-ltxr 8329  df-inn 9255  df-2 9313  df-3 9314  df-ndx 13299  df-slot 13300  df-base 13302  df-sets 13303  df-plusg 13387  df-mulr 13388  df-mhm 13714  df-ghm 13994  df-mgp 14160  df-ur 14203  df-ring 14241  df-rhm 14397

This theorem is referenced by:  rhmrcl1  14400  rhmrcl2  14401  isrhm  14403  rhmfn  14417  rhmval  14418