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 = (r \in Ring, s \in Ring ⟼ (r GrpHom s) \cap ({mulGrp}_{r} MndHom {mulGrp}_{s}))$

Proof

Step	Hyp	Ref	Expression
1		df-rnghom	$⊢ RingHom = (r \in Ring, s \in Ring ⟼ ⦋ {Base}_{r} / v ⦌ ⦋ {Base}_{s} / w ⦌ \{f \in (w^{v}) \| (f (1_{r}) = 1_{s} \land \forall x \in v \forall y \in v (f (x +_{r} y) = f (x) +_{s} f (y) \land f (x \cdot_{r} y) = f (x) \cdot_{s} f (y)))\})$
2		ringgrp	$⊢ r \in Ring \to r \in Grp$
3		ringgrp	$⊢ s \in Ring \to s \in Grp$
4		eqid	$⊢ {Base}_{r} = {Base}_{r}$
5		eqid	$⊢ {Base}_{s} = {Base}_{s}$
6		eqid	$⊢ +_{r} = +_{r}$
7		eqid	$⊢ +_{s} = +_{s}$
8	4 5 6 7	isghm3	$⊢ (r \in Grp \land s \in Grp) \to (f \in (r GrpHom s) \leftrightarrow (f : {Base}_{r} ⟶ {Base}_{s} \land \forall x \in {Base}_{r} \forall y \in {Base}_{r} f (x +_{r} y) = f (x) +_{s} f (y)))$
9	2 3 8	syl2an	$⊢ (r \in Ring \land s \in Ring) \to (f \in (r GrpHom s) \leftrightarrow (f : {Base}_{r} ⟶ {Base}_{s} \land \forall x \in {Base}_{r} \forall y \in {Base}_{r} f (x +_{r} y) = f (x) +_{s} f (y)))$
10	9	abbi2dv	$⊢ (r \in Ring \land s \in Ring) \to r GrpHom s = \{f \| (f : {Base}_{r} ⟶ {Base}_{s} \land \forall x \in {Base}_{r} \forall y \in {Base}_{r} f (x +_{r} y) = f (x) +_{s} f (y))\}$
11		df-rab	$⊢ \{f \in ({Base}_{s}^{{Base}_{r}}) \| \forall x \in {Base}_{r} \forall y \in {Base}_{r} f (x +_{r} y) = f (x) +_{s} f (y)\} = \{f \| (f \in ({Base}_{s}^{{Base}_{r}}) \land \forall x \in {Base}_{r} \forall y \in {Base}_{r} f (x +_{r} y) = f (x) +_{s} f (y))\}$
12		fvex	$⊢ {Base}_{s} \in V$
13		fvex	$⊢ {Base}_{r} \in V$
14	12 13	elmap	$⊢ f \in ({Base}_{s}^{{Base}_{r}}) \leftrightarrow f : {Base}_{r} ⟶ {Base}_{s}$
15	14	anbi1i	$⊢ (f \in ({Base}_{s}^{{Base}_{r}}) \land \forall x \in {Base}_{r} \forall y \in {Base}_{r} f (x +_{r} y) = f (x) +_{s} f (y)) \leftrightarrow (f : {Base}_{r} ⟶ {Base}_{s} \land \forall x \in {Base}_{r} \forall y \in {Base}_{r} f (x +_{r} y) = f (x) +_{s} f (y))$
16	15	abbii	$⊢ \{f \| (f \in ({Base}_{s}^{{Base}_{r}}) \land \forall x \in {Base}_{r} \forall y \in {Base}_{r} f (x +_{r} y) = f (x) +_{s} f (y))\} = \{f \| (f : {Base}_{r} ⟶ {Base}_{s} \land \forall x \in {Base}_{r} \forall y \in {Base}_{r} f (x +_{r} y) = f (x) +_{s} f (y))\}$
17	11 16	eqtri	$⊢ \{f \in ({Base}_{s}^{{Base}_{r}}) \| \forall x \in {Base}_{r} \forall y \in {Base}_{r} f (x +_{r} y) = f (x) +_{s} f (y)\} = \{f \| (f : {Base}_{r} ⟶ {Base}_{s} \land \forall x \in {Base}_{r} \forall y \in {Base}_{r} f (x +_{r} y) = f (x) +_{s} f (y))\}$
18	10 17	eqtr4di	$⊢ (r \in Ring \land s \in Ring) \to r GrpHom s = \{f \in ({Base}_{s}^{{Base}_{r}}) \| \forall x \in {Base}_{r} \forall y \in {Base}_{r} f (x +_{r} y) = f (x) +_{s} f (y)\}$
19		eqid	$⊢ {mulGrp}_{r} = {mulGrp}_{r}$
20	19	ringmgp	$⊢ r \in Ring \to {mulGrp}_{r} \in Mnd$
21		eqid	$⊢ {mulGrp}_{s} = {mulGrp}_{s}$
22	21	ringmgp	$⊢ s \in Ring \to {mulGrp}_{s} \in Mnd$
23	19 4	mgpbas	$⊢ {Base}_{r} = {Base}_{{mulGrp}_{r}}$
24	21 5	mgpbas	$⊢ {Base}_{s} = {Base}_{{mulGrp}_{s}}$
25		eqid	$⊢ \cdot_{r} = \cdot_{r}$
26	19 25	mgpplusg	$⊢ \cdot_{r} = +_{{mulGrp}_{r}}$
27		eqid	$⊢ \cdot_{s} = \cdot_{s}$
28	21 27	mgpplusg	$⊢ \cdot_{s} = +_{{mulGrp}_{s}}$
29		eqid	$⊢ 1_{r} = 1_{r}$
30	19 29	ringidval	$⊢ 1_{r} = 0_{{mulGrp}_{r}}$
31		eqid	$⊢ 1_{s} = 1_{s}$
32	21 31	ringidval	$⊢ 1_{s} = 0_{{mulGrp}_{s}}$
33	23 24 26 28 30 32	ismhm	$⊢ f \in ({mulGrp}_{r} MndHom {mulGrp}_{s}) \leftrightarrow (({mulGrp}_{r} \in Mnd \land {mulGrp}_{s} \in Mnd) \land (f : {Base}_{r} ⟶ {Base}_{s} \land \forall x \in {Base}_{r} \forall y \in {Base}_{r} f (x \cdot_{r} y) = f (x) \cdot_{s} f (y) \land f (1_{r}) = 1_{s}))$
34	33	baib	$⊢ ({mulGrp}_{r} \in Mnd \land {mulGrp}_{s} \in Mnd) \to (f \in ({mulGrp}_{r} MndHom {mulGrp}_{s}) \leftrightarrow (f : {Base}_{r} ⟶ {Base}_{s} \land \forall x \in {Base}_{r} \forall y \in {Base}_{r} f (x \cdot_{r} y) = f (x) \cdot_{s} f (y) \land f (1_{r}) = 1_{s}))$
35	20 22 34	syl2an	$⊢ (r \in Ring \land s \in Ring) \to (f \in ({mulGrp}_{r} MndHom {mulGrp}_{s}) \leftrightarrow (f : {Base}_{r} ⟶ {Base}_{s} \land \forall x \in {Base}_{r} \forall y \in {Base}_{r} f (x \cdot_{r} y) = f (x) \cdot_{s} f (y) \land f (1_{r}) = 1_{s}))$
36	35	abbi2dv	$⊢ (r \in Ring \land s \in Ring) \to {mulGrp}_{r} MndHom {mulGrp}_{s} = \{f \| (f : {Base}_{r} ⟶ {Base}_{s} \land \forall x \in {Base}_{r} \forall y \in {Base}_{r} f (x \cdot_{r} y) = f (x) \cdot_{s} f (y) \land f (1_{r}) = 1_{s})\}$
37		df-rab	$⊢ \{f \in ({Base}_{s}^{{Base}_{r}}) \| (\forall x \in {Base}_{r} \forall y \in {Base}_{r} f (x \cdot_{r} y) = f (x) \cdot_{s} f (y) \land f (1_{r}) = 1_{s})\} = \{f \| (f \in ({Base}_{s}^{{Base}_{r}}) \land (\forall x \in {Base}_{r} \forall y \in {Base}_{r} f (x \cdot_{r} y) = f (x) \cdot_{s} f (y) \land f (1_{r}) = 1_{s}))\}$
38	14	anbi1i	$⊢ (f \in ({Base}_{s}^{{Base}_{r}}) \land (\forall x \in {Base}_{r} \forall y \in {Base}_{r} f (x \cdot_{r} y) = f (x) \cdot_{s} f (y) \land f (1_{r}) = 1_{s})) \leftrightarrow (f : {Base}_{r} ⟶ {Base}_{s} \land (\forall x \in {Base}_{r} \forall y \in {Base}_{r} f (x \cdot_{r} y) = f (x) \cdot_{s} f (y) \land f (1_{r}) = 1_{s}))$
39		3anass	$⊢ (f : {Base}_{r} ⟶ {Base}_{s} \land \forall x \in {Base}_{r} \forall y \in {Base}_{r} f (x \cdot_{r} y) = f (x) \cdot_{s} f (y) \land f (1_{r}) = 1_{s}) \leftrightarrow (f : {Base}_{r} ⟶ {Base}_{s} \land (\forall x \in {Base}_{r} \forall y \in {Base}_{r} f (x \cdot_{r} y) = f (x) \cdot_{s} f (y) \land f (1_{r}) = 1_{s}))$
40	38 39	bitr4i	$⊢ (f \in ({Base}_{s}^{{Base}_{r}}) \land (\forall x \in {Base}_{r} \forall y \in {Base}_{r} f (x \cdot_{r} y) = f (x) \cdot_{s} f (y) \land f (1_{r}) = 1_{s})) \leftrightarrow (f : {Base}_{r} ⟶ {Base}_{s} \land \forall x \in {Base}_{r} \forall y \in {Base}_{r} f (x \cdot_{r} y) = f (x) \cdot_{s} f (y) \land f (1_{r}) = 1_{s})$
41	40	abbii	$⊢ \{f \| (f \in ({Base}_{s}^{{Base}_{r}}) \land (\forall x \in {Base}_{r} \forall y \in {Base}_{r} f (x \cdot_{r} y) = f (x) \cdot_{s} f (y) \land f (1_{r}) = 1_{s}))\} = \{f \| (f : {Base}_{r} ⟶ {Base}_{s} \land \forall x \in {Base}_{r} \forall y \in {Base}_{r} f (x \cdot_{r} y) = f (x) \cdot_{s} f (y) \land f (1_{r}) = 1_{s})\}$
42	37 41	eqtri	$⊢ \{f \in ({Base}_{s}^{{Base}_{r}}) \| (\forall x \in {Base}_{r} \forall y \in {Base}_{r} f (x \cdot_{r} y) = f (x) \cdot_{s} f (y) \land f (1_{r}) = 1_{s})\} = \{f \| (f : {Base}_{r} ⟶ {Base}_{s} \land \forall x \in {Base}_{r} \forall y \in {Base}_{r} f (x \cdot_{r} y) = f (x) \cdot_{s} f (y) \land f (1_{r}) = 1_{s})\}$
43	36 42	eqtr4di	$⊢ (r \in Ring \land s \in Ring) \to {mulGrp}_{r} MndHom {mulGrp}_{s} = \{f \in ({Base}_{s}^{{Base}_{r}}) \| (\forall x \in {Base}_{r} \forall y \in {Base}_{r} f (x \cdot_{r} y) = f (x) \cdot_{s} f (y) \land f (1_{r}) = 1_{s})\}$
44	18 43	ineq12d	$⊢ (r \in Ring \land s \in Ring) \to (r GrpHom s) \cap ({mulGrp}_{r} MndHom {mulGrp}_{s}) = \{f \in ({Base}_{s}^{{Base}_{r}}) \| \forall x \in {Base}_{r} \forall y \in {Base}_{r} f (x +_{r} y) = f (x) +_{s} f (y)\} \cap \{f \in ({Base}_{s}^{{Base}_{r}}) \| (\forall x \in {Base}_{r} \forall y \in {Base}_{r} f (x \cdot_{r} y) = f (x) \cdot_{s} f (y) \land f (1_{r}) = 1_{s})\}$
45		ancom	$⊢ (f (1_{r}) = 1_{s} \land \forall x \in {Base}_{r} \forall y \in {Base}_{r} (f (x +_{r} y) = f (x) +_{s} f (y) \land f (x \cdot_{r} y) = f (x) \cdot_{s} f (y))) \leftrightarrow (\forall x \in {Base}_{r} \forall y \in {Base}_{r} (f (x +_{r} y) = f (x) +_{s} f (y) \land f (x \cdot_{r} y) = f (x) \cdot_{s} f (y)) \land f (1_{r}) = 1_{s})$
46		r19.26-2	$⊢ \forall x \in {Base}_{r} \forall y \in {Base}_{r} (f (x +_{r} y) = f (x) +_{s} f (y) \land f (x \cdot_{r} y) = f (x) \cdot_{s} f (y)) \leftrightarrow (\forall x \in {Base}_{r} \forall y \in {Base}_{r} f (x +_{r} y) = f (x) +_{s} f (y) \land \forall x \in {Base}_{r} \forall y \in {Base}_{r} f (x \cdot_{r} y) = f (x) \cdot_{s} f (y))$
47	46	anbi1i	$⊢ (\forall x \in {Base}_{r} \forall y \in {Base}_{r} (f (x +_{r} y) = f (x) +_{s} f (y) \land f (x \cdot_{r} y) = f (x) \cdot_{s} f (y)) \land f (1_{r}) = 1_{s}) \leftrightarrow ((\forall x \in {Base}_{r} \forall y \in {Base}_{r} f (x +_{r} y) = f (x) +_{s} f (y) \land \forall x \in {Base}_{r} \forall y \in {Base}_{r} f (x \cdot_{r} y) = f (x) \cdot_{s} f (y)) \land f (1_{r}) = 1_{s})$
48		anass	$⊢ ((\forall x \in {Base}_{r} \forall y \in {Base}_{r} f (x +_{r} y) = f (x) +_{s} f (y) \land \forall x \in {Base}_{r} \forall y \in {Base}_{r} f (x \cdot_{r} y) = f (x) \cdot_{s} f (y)) \land f (1_{r}) = 1_{s}) \leftrightarrow (\forall x \in {Base}_{r} \forall y \in {Base}_{r} f (x +_{r} y) = f (x) +_{s} f (y) \land (\forall x \in {Base}_{r} \forall y \in {Base}_{r} f (x \cdot_{r} y) = f (x) \cdot_{s} f (y) \land f (1_{r}) = 1_{s}))$
49	45 47 48	3bitri	$⊢ (f (1_{r}) = 1_{s} \land \forall x \in {Base}_{r} \forall y \in {Base}_{r} (f (x +_{r} y) = f (x) +_{s} f (y) \land f (x \cdot_{r} y) = f (x) \cdot_{s} f (y))) \leftrightarrow (\forall x \in {Base}_{r} \forall y \in {Base}_{r} f (x +_{r} y) = f (x) +_{s} f (y) \land (\forall x \in {Base}_{r} \forall y \in {Base}_{r} f (x \cdot_{r} y) = f (x) \cdot_{s} f (y) \land f (1_{r}) = 1_{s}))$
50	49	rabbii	$⊢ \{f \in ({Base}_{s}^{{Base}_{r}}) \| (f (1_{r}) = 1_{s} \land \forall x \in {Base}_{r} \forall y \in {Base}_{r} (f (x +_{r} y) = f (x) +_{s} f (y) \land f (x \cdot_{r} y) = f (x) \cdot_{s} f (y)))\} = \{f \in ({Base}_{s}^{{Base}_{r}}) \| (\forall x \in {Base}_{r} \forall y \in {Base}_{r} f (x +_{r} y) = f (x) +_{s} f (y) \land (\forall x \in {Base}_{r} \forall y \in {Base}_{r} f (x \cdot_{r} y) = f (x) \cdot_{s} f (y) \land f (1_{r}) = 1_{s}))\}$
51		oveq12	$⊢ (w = {Base}_{s} \land v = {Base}_{r}) \to w^{v} = {Base}_{s}^{{Base}_{r}}$
52	51	ancoms	$⊢ (v = {Base}_{r} \land w = {Base}_{s}) \to w^{v} = {Base}_{s}^{{Base}_{r}}$
53		raleq	$⊢ v = {Base}_{r} \to (\forall y \in v (f (x +_{r} y) = f (x) +_{s} f (y) \land f (x \cdot_{r} y) = f (x) \cdot_{s} f (y)) \leftrightarrow \forall y \in {Base}_{r} (f (x +_{r} y) = f (x) +_{s} f (y) \land f (x \cdot_{r} y) = f (x) \cdot_{s} f (y)))$
54	53	raleqbi1dv	$⊢ v = {Base}_{r} \to (\forall x \in v \forall y \in v (f (x +_{r} y) = f (x) +_{s} f (y) \land f (x \cdot_{r} y) = f (x) \cdot_{s} f (y)) \leftrightarrow \forall x \in {Base}_{r} \forall y \in {Base}_{r} (f (x +_{r} y) = f (x) +_{s} f (y) \land f (x \cdot_{r} y) = f (x) \cdot_{s} f (y)))$
55	54	adantr	$⊢ (v = {Base}_{r} \land w = {Base}_{s}) \to (\forall x \in v \forall y \in v (f (x +_{r} y) = f (x) +_{s} f (y) \land f (x \cdot_{r} y) = f (x) \cdot_{s} f (y)) \leftrightarrow \forall x \in {Base}_{r} \forall y \in {Base}_{r} (f (x +_{r} y) = f (x) +_{s} f (y) \land f (x \cdot_{r} y) = f (x) \cdot_{s} f (y)))$
56	55	anbi2d	$⊢ (v = {Base}_{r} \land w = {Base}_{s}) \to ((f (1_{r}) = 1_{s} \land \forall x \in v \forall y \in v (f (x +_{r} y) = f (x) +_{s} f (y) \land f (x \cdot_{r} y) = f (x) \cdot_{s} f (y))) \leftrightarrow (f (1_{r}) = 1_{s} \land \forall x \in {Base}_{r} \forall y \in {Base}_{r} (f (x +_{r} y) = f (x) +_{s} f (y) \land f (x \cdot_{r} y) = f (x) \cdot_{s} f (y))))$
57	52 56	rabeqbidv	$⊢ (v = {Base}_{r} \land w = {Base}_{s}) \to \{f \in (w^{v}) \| (f (1_{r}) = 1_{s} \land \forall x \in v \forall y \in v (f (x +_{r} y) = f (x) +_{s} f (y) \land f (x \cdot_{r} y) = f (x) \cdot_{s} f (y)))\} = \{f \in ({Base}_{s}^{{Base}_{r}}) \| (f (1_{r}) = 1_{s} \land \forall x \in {Base}_{r} \forall y \in {Base}_{r} (f (x +_{r} y) = f (x) +_{s} f (y) \land f (x \cdot_{r} y) = f (x) \cdot_{s} f (y)))\}$
58	13 12 57	csbie2	$⊢ ⦋ {Base}_{r} / v ⦌ ⦋ {Base}_{s} / w ⦌ \{f \in (w^{v}) \| (f (1_{r}) = 1_{s} \land \forall x \in v \forall y \in v (f (x +_{r} y) = f (x) +_{s} f (y) \land f (x \cdot_{r} y) = f (x) \cdot_{s} f (y)))\} = \{f \in ({Base}_{s}^{{Base}_{r}}) \| (f (1_{r}) = 1_{s} \land \forall x \in {Base}_{r} \forall y \in {Base}_{r} (f (x +_{r} y) = f (x) +_{s} f (y) \land f (x \cdot_{r} y) = f (x) \cdot_{s} f (y)))\}$
59		inrab	$⊢ \{f \in ({Base}_{s}^{{Base}_{r}}) \| \forall x \in {Base}_{r} \forall y \in {Base}_{r} f (x +_{r} y) = f (x) +_{s} f (y)\} \cap \{f \in ({Base}_{s}^{{Base}_{r}}) \| (\forall x \in {Base}_{r} \forall y \in {Base}_{r} f (x \cdot_{r} y) = f (x) \cdot_{s} f (y) \land f (1_{r}) = 1_{s})\} = \{f \in ({Base}_{s}^{{Base}_{r}}) \| (\forall x \in {Base}_{r} \forall y \in {Base}_{r} f (x +_{r} y) = f (x) +_{s} f (y) \land (\forall x \in {Base}_{r} \forall y \in {Base}_{r} f (x \cdot_{r} y) = f (x) \cdot_{s} f (y) \land f (1_{r}) = 1_{s}))\}$
60	50 58 59	3eqtr4i	$⊢ ⦋ {Base}_{r} / v ⦌ ⦋ {Base}_{s} / w ⦌ \{f \in (w^{v}) \| (f (1_{r}) = 1_{s} \land \forall x \in v \forall y \in v (f (x +_{r} y) = f (x) +_{s} f (y) \land f (x \cdot_{r} y) = f (x) \cdot_{s} f (y)))\} = \{f \in ({Base}_{s}^{{Base}_{r}}) \| \forall x \in {Base}_{r} \forall y \in {Base}_{r} f (x +_{r} y) = f (x) +_{s} f (y)\} \cap \{f \in ({Base}_{s}^{{Base}_{r}}) \| (\forall x \in {Base}_{r} \forall y \in {Base}_{r} f (x \cdot_{r} y) = f (x) \cdot_{s} f (y) \land f (1_{r}) = 1_{s})\}$
61	44 60	syl6reqr	$⊢ (r \in Ring \land s \in Ring) \to ⦋ {Base}_{r} / v ⦌ ⦋ {Base}_{s} / w ⦌ \{f \in (w^{v}) \| (f (1_{r}) = 1_{s} \land \forall x \in v \forall y \in v (f (x +_{r} y) = f (x) +_{s} f (y) \land f (x \cdot_{r} y) = f (x) \cdot_{s} f (y)))\} = (r GrpHom s) \cap ({mulGrp}_{r} MndHom {mulGrp}_{s})$
62	61	mpoeq3ia	$⊢ (r \in Ring, s \in Ring ⟼ ⦋ {Base}_{r} / v ⦌ ⦋ {Base}_{s} / w ⦌ \{f \in (w^{v}) \| (f (1_{r}) = 1_{s} \land \forall x \in v \forall y \in v (f (x +_{r} y) = f (x) +_{s} f (y) \land f (x \cdot_{r} y) = f (x) \cdot_{s} f (y)))\}) = (r \in Ring, s \in Ring ⟼ (r GrpHom s) \cap ({mulGrp}_{r} MndHom {mulGrp}_{s}))$
63	1 62	eqtri	$⊢ RingHom = (r \in Ring, s \in Ring ⟼ (r GrpHom s) \cap ({mulGrp}_{r} MndHom {mulGrp}_{s}))$

Metamath Proof Explorer

Theorem dfrhm2

Proof