Theorem dfrhm2 13653

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 13651	. 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 2623	. . . . . . . 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 2746	. . . . 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 12679	. . . . . . 7 ⊢ Base Fn V
9		vex 2763	. . . . . . 7 ⊢ 𝑟 ∈ V
10		funfvex 5572	. . . . . . . 8 ⊢ ((Fun Base ∧ 𝑟 ∈ dom Base) → (Base‘𝑟) ∈ V)
11	10	funfni 5355	. . . . . . 7 ⊢ ((Base Fn V ∧ 𝑟 ∈ V) → (Base‘𝑟) ∈ V)
12	8, 9, 11	mp2an 426	. . . . . 6 ⊢ (Base‘𝑟) ∈ V
13		vex 2763	. . . . . . 7 ⊢ 𝑠 ∈ V
14		funfvex 5572	. . . . . . . 8 ⊢ ((Fun Base ∧ 𝑠 ∈ dom Base) → (Base‘𝑠) ∈ V)
15	14	funfni 5355	. . . . . . 7 ⊢ ((Base Fn V ∧ 𝑠 ∈ V) → (Base‘𝑠) ∈ V)
16	8, 13, 15	mp2an 426	. . . . . 6 ⊢ (Base‘𝑠) ∈ V
17		oveq12 5928	. . . . . . . 8 ⊢ ((𝑤 = (Base‘𝑠) ∧ 𝑣 = (Base‘𝑟)) → (𝑤 ↑𝑚 𝑣) = ((Base‘𝑠) ↑𝑚 (Base‘𝑟)))
18	17	ancoms 268	. . . . . . 7 ⊢ ((𝑣 = (Base‘𝑟) ∧ 𝑤 = (Base‘𝑠)) → (𝑤 ↑𝑚 𝑣) = ((Base‘𝑠) ↑𝑚 (Base‘𝑟)))
19		raleq 2690	. . . . . . . . . 10 ⊢ (𝑣 = (Base‘𝑟) → (∀𝑦 ∈ 𝑣 ((𝑓‘(𝑥(+g‘𝑟)𝑦)) = ((𝑓‘𝑥)(+g‘𝑠)(𝑓‘𝑦)) ∧ (𝑓‘(𝑥(.r‘𝑟)𝑦)) = ((𝑓‘𝑥)(.r‘𝑠)(𝑓‘𝑦))) ↔ ∀𝑦 ∈ (Base‘𝑟)((𝑓‘(𝑥(+g‘𝑟)𝑦)) = ((𝑓‘𝑥)(+g‘𝑠)(𝑓‘𝑦)) ∧ (𝑓‘(𝑥(.r‘𝑟)𝑦)) = ((𝑓‘𝑥)(.r‘𝑠)(𝑓‘𝑦)))))
20	19	raleqbi1dv 2702	. . . . . . . . 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 2755	. . . . . 6 ⊢ ((𝑣 = (Base‘𝑟) ∧ 𝑤 = (Base‘𝑠)) → {𝑓 ∈ (𝑤 ↑𝑚 𝑣) ∣ ((𝑓‘(1r‘𝑟)) = (1r‘𝑠) ∧ ∀𝑥 ∈ 𝑣 ∀𝑦 ∈ 𝑣 ((𝑓‘(𝑥(+g‘𝑟)𝑦)) = ((𝑓‘𝑥)(+g‘𝑠)(𝑓‘𝑦)) ∧ (𝑓‘(𝑥(.r‘𝑟)𝑦)) = ((𝑓‘𝑥)(.r‘𝑠)(𝑓‘𝑦))))} = {𝑓 ∈ ((Base‘𝑠) ↑𝑚 (Base‘𝑟)) ∣ ((𝑓‘(1r‘𝑟)) = (1r‘𝑠) ∧ ∀𝑥 ∈ (Base‘𝑟)∀𝑦 ∈ (Base‘𝑟)((𝑓‘(𝑥(+g‘𝑟)𝑦)) = ((𝑓‘𝑥)(+g‘𝑠)(𝑓‘𝑦)) ∧ (𝑓‘(𝑥(.r‘𝑟)𝑦)) = ((𝑓‘𝑥)(.r‘𝑠)(𝑓‘𝑦))))})
24	12, 16, 23	csbie2 3131	. . . . 5 ⊢ ⦋(Base‘𝑟) / 𝑣⦌⦋(Base‘𝑠) / 𝑤⦌{𝑓 ∈ (𝑤 ↑𝑚 𝑣) ∣ ((𝑓‘(1r‘𝑟)) = (1r‘𝑠) ∧ ∀𝑥 ∈ 𝑣 ∀𝑦 ∈ 𝑣 ((𝑓‘(𝑥(+g‘𝑟)𝑦)) = ((𝑓‘𝑥)(+g‘𝑠)(𝑓‘𝑦)) ∧ (𝑓‘(𝑥(.r‘𝑟)𝑦)) = ((𝑓‘𝑥)(.r‘𝑠)(𝑓‘𝑦))))} = {𝑓 ∈ ((Base‘𝑠) ↑𝑚 (Base‘𝑟)) ∣ ((𝑓‘(1r‘𝑟)) = (1r‘𝑠) ∧ ∀𝑥 ∈ (Base‘𝑟)∀𝑦 ∈ (Base‘𝑟)((𝑓‘(𝑥(+g‘𝑟)𝑦)) = ((𝑓‘𝑥)(+g‘𝑠)(𝑓‘𝑦)) ∧ (𝑓‘(𝑥(.r‘𝑟)𝑦)) = ((𝑓‘𝑥)(.r‘𝑠)(𝑓‘𝑦))))}
25		inrab 3432	. . . . 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 2224	. . . 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 13500	. . . . . . . 8 ⊢ (𝑟 ∈ Ring → 𝑟 ∈ Grp)
28		ringgrp 13500	. . . . . . . 8 ⊢ (𝑠 ∈ Ring → 𝑠 ∈ Grp)
29		eqid 2193	. . . . . . . . 9 ⊢ (Base‘𝑟) = (Base‘𝑟)
30		eqid 2193	. . . . . . . . 9 ⊢ (Base‘𝑠) = (Base‘𝑠)
31		eqid 2193	. . . . . . . . 9 ⊢ (+g‘𝑟) = (+g‘𝑟)
32		eqid 2193	. . . . . . . . 9 ⊢ (+g‘𝑠) = (+g‘𝑠)
33	29, 30, 31, 32	isghm3 13317	. . . . . . . 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 2322	. . . . . 6 ⊢ ((𝑟 ∈ Ring ∧ 𝑠 ∈ Ring) → (𝑟 GrpHom 𝑠) = {𝑓 ∣ (𝑓:(Base‘𝑟)⟶(Base‘𝑠) ∧ ∀𝑥 ∈ (Base‘𝑟)∀𝑦 ∈ (Base‘𝑟)(𝑓‘(𝑥(+g‘𝑟)𝑦)) = ((𝑓‘𝑥)(+g‘𝑠)(𝑓‘𝑦)))})
36		df-rab 2481	. . . . . . 7 ⊢ {𝑓 ∈ ((Base‘𝑠) ↑𝑚 (Base‘𝑟)) ∣ ∀𝑥 ∈ (Base‘𝑟)∀𝑦 ∈ (Base‘𝑟)(𝑓‘(𝑥(+g‘𝑟)𝑦)) = ((𝑓‘𝑥)(+g‘𝑠)(𝑓‘𝑦))} = {𝑓 ∣ (𝑓 ∈ ((Base‘𝑠) ↑𝑚 (Base‘𝑟)) ∧ ∀𝑥 ∈ (Base‘𝑟)∀𝑦 ∈ (Base‘𝑟)(𝑓‘(𝑥(+g‘𝑟)𝑦)) = ((𝑓‘𝑥)(+g‘𝑠)(𝑓‘𝑦)))}
37	16, 12	elmap 6733	. . . . . . . . 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 2309	. . . . . . 7 ⊢ {𝑓 ∣ (𝑓 ∈ ((Base‘𝑠) ↑𝑚 (Base‘𝑟)) ∧ ∀𝑥 ∈ (Base‘𝑟)∀𝑦 ∈ (Base‘𝑟)(𝑓‘(𝑥(+g‘𝑟)𝑦)) = ((𝑓‘𝑥)(+g‘𝑠)(𝑓‘𝑦)))} = {𝑓 ∣ (𝑓:(Base‘𝑟)⟶(Base‘𝑠) ∧ ∀𝑥 ∈ (Base‘𝑟)∀𝑦 ∈ (Base‘𝑟)(𝑓‘(𝑥(+g‘𝑟)𝑦)) = ((𝑓‘𝑥)(+g‘𝑠)(𝑓‘𝑦)))}
40	36, 39	eqtri 2214	. . . . . 6 ⊢ {𝑓 ∈ ((Base‘𝑠) ↑𝑚 (Base‘𝑟)) ∣ ∀𝑥 ∈ (Base‘𝑟)∀𝑦 ∈ (Base‘𝑟)(𝑓‘(𝑥(+g‘𝑟)𝑦)) = ((𝑓‘𝑥)(+g‘𝑠)(𝑓‘𝑦))} = {𝑓 ∣ (𝑓:(Base‘𝑟)⟶(Base‘𝑠) ∧ ∀𝑥 ∈ (Base‘𝑟)∀𝑦 ∈ (Base‘𝑟)(𝑓‘(𝑥(+g‘𝑟)𝑦)) = ((𝑓‘𝑥)(+g‘𝑠)(𝑓‘𝑦)))}
41	35, 40	eqtr4di 2244	. . . . 5 ⊢ ((𝑟 ∈ Ring ∧ 𝑠 ∈ Ring) → (𝑟 GrpHom 𝑠) = {𝑓 ∈ ((Base‘𝑠) ↑𝑚 (Base‘𝑟)) ∣ ∀𝑥 ∈ (Base‘𝑟)∀𝑦 ∈ (Base‘𝑟)(𝑓‘(𝑥(+g‘𝑟)𝑦)) = ((𝑓‘𝑥)(+g‘𝑠)(𝑓‘𝑦))})
42		eqid 2193	. . . . . . . . 9 ⊢ (mulGrp‘𝑟) = (mulGrp‘𝑟)
43	42	ringmgp 13501	. . . . . . . 8 ⊢ (𝑟 ∈ Ring → (mulGrp‘𝑟) ∈ Mnd)
44		eqid 2193	. . . . . . . . 9 ⊢ (mulGrp‘𝑠) = (mulGrp‘𝑠)
45	44	ringmgp 13501	. . . . . . . 8 ⊢ (𝑠 ∈ Ring → (mulGrp‘𝑠) ∈ Mnd)
46	42, 29	mgpbasg 13425	. . . . . . . . . . 11 ⊢ (𝑟 ∈ V → (Base‘𝑟) = (Base‘(mulGrp‘𝑟)))
47	46	elv 2764	. . . . . . . . . 10 ⊢ (Base‘𝑟) = (Base‘(mulGrp‘𝑟))
48	44, 30	mgpbasg 13425	. . . . . . . . . . 11 ⊢ (𝑠 ∈ V → (Base‘𝑠) = (Base‘(mulGrp‘𝑠)))
49	48	elv 2764	. . . . . . . . . 10 ⊢ (Base‘𝑠) = (Base‘(mulGrp‘𝑠))
50		eqid 2193	. . . . . . . . . . . 12 ⊢ (.r‘𝑟) = (.r‘𝑟)
51	42, 50	mgpplusgg 13423	. . . . . . . . . . 11 ⊢ (𝑟 ∈ V → (.r‘𝑟) = (+g‘(mulGrp‘𝑟)))
52	51	elv 2764	. . . . . . . . . 10 ⊢ (.r‘𝑟) = (+g‘(mulGrp‘𝑟))
53		eqid 2193	. . . . . . . . . . . 12 ⊢ (.r‘𝑠) = (.r‘𝑠)
54	44, 53	mgpplusgg 13423	. . . . . . . . . . 11 ⊢ (𝑠 ∈ V → (.r‘𝑠) = (+g‘(mulGrp‘𝑠)))
55	54	elv 2764	. . . . . . . . . 10 ⊢ (.r‘𝑠) = (+g‘(mulGrp‘𝑠))
56		eqid 2193	. . . . . . . . . . . 12 ⊢ (1r‘𝑟) = (1r‘𝑟)
57	42, 56	ringidvalg 13460	. . . . . . . . . . 11 ⊢ (𝑟 ∈ V → (1r‘𝑟) = (0g‘(mulGrp‘𝑟)))
58	57	elv 2764	. . . . . . . . . 10 ⊢ (1r‘𝑟) = (0g‘(mulGrp‘𝑟))
59		eqid 2193	. . . . . . . . . . . 12 ⊢ (1r‘𝑠) = (1r‘𝑠)
60	44, 59	ringidvalg 13460	. . . . . . . . . . 11 ⊢ (𝑠 ∈ V → (1r‘𝑠) = (0g‘(mulGrp‘𝑠)))
61	60	elv 2764	. . . . . . . . . 10 ⊢ (1r‘𝑠) = (0g‘(mulGrp‘𝑠))
62	47, 49, 52, 55, 58, 61	ismhm 13036	. . . . . . . . 9 ⊢ (𝑓 ∈ ((mulGrp‘𝑟) MndHom (mulGrp‘𝑠)) ↔ (((mulGrp‘𝑟) ∈ Mnd ∧ (mulGrp‘𝑠) ∈ Mnd) ∧ (𝑓:(Base‘𝑟)⟶(Base‘𝑠) ∧ ∀𝑥 ∈ (Base‘𝑟)∀𝑦 ∈ (Base‘𝑟)(𝑓‘(𝑥(.r‘𝑟)𝑦)) = ((𝑓‘𝑥)(.r‘𝑠)(𝑓‘𝑦)) ∧ (𝑓‘(1r‘𝑟)) = (1r‘𝑠))))
63	62	baib 920	. . . . . . . 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 2322	. . . . . 6 ⊢ ((𝑟 ∈ Ring ∧ 𝑠 ∈ Ring) → ((mulGrp‘𝑟) MndHom (mulGrp‘𝑠)) = {𝑓 ∣ (𝑓:(Base‘𝑟)⟶(Base‘𝑠) ∧ ∀𝑥 ∈ (Base‘𝑟)∀𝑦 ∈ (Base‘𝑟)(𝑓‘(𝑥(.r‘𝑟)𝑦)) = ((𝑓‘𝑥)(.r‘𝑠)(𝑓‘𝑦)) ∧ (𝑓‘(1r‘𝑟)) = (1r‘𝑠))})
66		df-rab 2481	. . . . . . 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 984	. . . . . . . . 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 2309	. . . . . . 7 ⊢ {𝑓 ∣ (𝑓 ∈ ((Base‘𝑠) ↑𝑚 (Base‘𝑟)) ∧ (∀𝑥 ∈ (Base‘𝑟)∀𝑦 ∈ (Base‘𝑟)(𝑓‘(𝑥(.r‘𝑟)𝑦)) = ((𝑓‘𝑥)(.r‘𝑠)(𝑓‘𝑦)) ∧ (𝑓‘(1r‘𝑟)) = (1r‘𝑠)))} = {𝑓 ∣ (𝑓:(Base‘𝑟)⟶(Base‘𝑠) ∧ ∀𝑥 ∈ (Base‘𝑟)∀𝑦 ∈ (Base‘𝑟)(𝑓‘(𝑥(.r‘𝑟)𝑦)) = ((𝑓‘𝑥)(.r‘𝑠)(𝑓‘𝑦)) ∧ (𝑓‘(1r‘𝑟)) = (1r‘𝑠))}
71	66, 70	eqtri 2214	. . . . . 6 ⊢ {𝑓 ∈ ((Base‘𝑠) ↑𝑚 (Base‘𝑟)) ∣ (∀𝑥 ∈ (Base‘𝑟)∀𝑦 ∈ (Base‘𝑟)(𝑓‘(𝑥(.r‘𝑟)𝑦)) = ((𝑓‘𝑥)(.r‘𝑠)(𝑓‘𝑦)) ∧ (𝑓‘(1r‘𝑟)) = (1r‘𝑠))} = {𝑓 ∣ (𝑓:(Base‘𝑟)⟶(Base‘𝑠) ∧ ∀𝑥 ∈ (Base‘𝑟)∀𝑦 ∈ (Base‘𝑟)(𝑓‘(𝑥(.r‘𝑟)𝑦)) = ((𝑓‘𝑥)(.r‘𝑠)(𝑓‘𝑦)) ∧ (𝑓‘(1r‘𝑟)) = (1r‘𝑠))}
72	65, 71	eqtr4di 2244	. . . . 5 ⊢ ((𝑟 ∈ Ring ∧ 𝑠 ∈ Ring) → ((mulGrp‘𝑟) MndHom (mulGrp‘𝑠)) = {𝑓 ∈ ((Base‘𝑠) ↑𝑚 (Base‘𝑟)) ∣ (∀𝑥 ∈ (Base‘𝑟)∀𝑦 ∈ (Base‘𝑟)(𝑓‘(𝑥(.r‘𝑟)𝑦)) = ((𝑓‘𝑥)(.r‘𝑠)(𝑓‘𝑦)) ∧ (𝑓‘(1r‘𝑟)) = (1r‘𝑠))})
73	41, 72	ineq12d 3362	. . . 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 2245	. . 3 ⊢ ((𝑟 ∈ Ring ∧ 𝑠 ∈ Ring) → ⦋(Base‘𝑟) / 𝑣⦌⦋(Base‘𝑠) / 𝑤⦌{𝑓 ∈ (𝑤 ↑𝑚 𝑣) ∣ ((𝑓‘(1r‘𝑟)) = (1r‘𝑠) ∧ ∀𝑥 ∈ 𝑣 ∀𝑦 ∈ 𝑣 ((𝑓‘(𝑥(+g‘𝑟)𝑦)) = ((𝑓‘𝑥)(+g‘𝑠)(𝑓‘𝑦)) ∧ (𝑓‘(𝑥(.r‘𝑟)𝑦)) = ((𝑓‘𝑥)(.r‘𝑠)(𝑓‘𝑦))))} = ((𝑟 GrpHom 𝑠) ∩ ((mulGrp‘𝑟) MndHom (mulGrp‘𝑠))))
75	74	mpoeq3ia 5984	. 2 ⊢ (𝑟 ∈ Ring, 𝑠 ∈ Ring ↦ ⦋(Base‘𝑟) / 𝑣⦌⦋(Base‘𝑠) / 𝑤⦌{𝑓 ∈ (𝑤 ↑𝑚 𝑣) ∣ ((𝑓‘(1r‘𝑟)) = (1r‘𝑠) ∧ ∀𝑥 ∈ 𝑣 ∀𝑦 ∈ 𝑣 ((𝑓‘(𝑥(+g‘𝑟)𝑦)) = ((𝑓‘𝑥)(+g‘𝑠)(𝑓‘𝑦)) ∧ (𝑓‘(𝑥(.r‘𝑟)𝑦)) = ((𝑓‘𝑥)(.r‘𝑠)(𝑓‘𝑦))))}) = (𝑟 ∈ Ring, 𝑠 ∈ Ring ↦ ((𝑟 GrpHom 𝑠) ∩ ((mulGrp‘𝑟) MndHom (mulGrp‘𝑠))))
76	1, 75	eqtri 2214	1 ⊢ RingHom = (𝑟 ∈ Ring, 𝑠 ∈ Ring ↦ ((𝑟 GrpHom 𝑠) ∩ ((mulGrp‘𝑟) MndHom (mulGrp‘𝑠))))

Syntax hints:   ∧ wa 104   ↔ wb 105   ∧ w3a 980   = wceq 1364   ∈ wcel 2164  {cab 2179  ∀wral 2472  {crab 2476  Vcvv 2760  ⦋csb 3081   ∩ cin 3153   Fn wfn 5250  ⟶wf 5251  ‘cfv 5255  (class class class)co 5919   ∈ cmpo 5921   ↑_𝑚 cmap 6704  Basecbs 12621  +_gcplusg 12698  ._rcmulr 12699  0_gc0g 12870  Mndcmnd 13000   MndHom cmhm 13032  Grpcgrp 13075   GrpHom cghm 13313  mulGrpcmgp 13419  1_rcur 13458  Ringcrg 13495   RingHom crh 13649

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 615  ax-in2 616  ax-io 710  ax-5 1458  ax-7 1459  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-8 1515  ax-10 1516  ax-11 1517  ax-i12 1518  ax-bndl 1520  ax-4 1521  ax-17 1537  ax-i9 1541  ax-ial 1545  ax-i5r 1546  ax-13 2166  ax-14 2167  ax-ext 2175  ax-coll 4145  ax-sep 4148  ax-pow 4204  ax-pr 4239  ax-un 4465  ax-setind 4570  ax-cnex 7965  ax-resscn 7966  ax-1cn 7967  ax-1re 7968  ax-icn 7969  ax-addcl 7970  ax-addrcl 7971  ax-mulcl 7972  ax-addcom 7974  ax-addass 7976  ax-i2m1 7979  ax-0lt1 7980  ax-0id 7982  ax-rnegex 7983  ax-pre-ltirr 7986  ax-pre-ltadd 7990

This theorem depends on definitions:  df-bi 117  df-3an 982  df-tru 1367  df-fal 1370  df-nf 1472  df-sb 1774  df-eu 2045  df-mo 2046  df-clab 2180  df-cleq 2186  df-clel 2189  df-nfc 2325  df-ne 2365  df-nel 2460  df-ral 2477  df-rex 2478  df-reu 2479  df-rab 2481  df-v 2762  df-sbc 2987  df-csb 3082  df-dif 3156  df-un 3158  df-in 3160  df-ss 3167  df-nul 3448  df-pw 3604  df-sn 3625  df-pr 3626  df-op 3628  df-uni 3837  df-int 3872  df-iun 3915  df-br 4031  df-opab 4092  df-mpt 4093  df-id 4325  df-xp 4666  df-rel 4667  df-cnv 4668  df-co 4669  df-dm 4670  df-rn 4671  df-res 4672  df-ima 4673  df-iota 5216  df-fun 5257  df-fn 5258  df-f 5259  df-f1 5260  df-fo 5261  df-f1o 5262  df-fv 5263  df-ov 5922  df-oprab 5923  df-mpo 5924  df-1st 6195  df-2nd 6196  df-map 6706  df-pnf 8058  df-mnf 8059  df-ltxr 8061  df-inn 8985  df-2 9043  df-3 9044  df-ndx 12624  df-slot 12625  df-base 12627  df-sets 12628  df-plusg 12711  df-mulr 12712  df-mhm 13034  df-ghm 13314  df-mgp 13420  df-ur 13459  df-ring 13497  df-rhm 13651

This theorem is referenced by:  rhmrcl1  13654  rhmrcl2  13655  isrhm  13657  rhmfn  13671  rhmval  13672