df-rnghom

Description: Define the set of ring homomorphisms from r to s . (Contributed by Stefan O'Rear, 7-Mar-2015)

		Ref	Expression
	Assertion	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)))\})$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		crh	$class RingHom$
1		vr	$setvar r$
2		crg	$class Ring$
3		vs	$setvar s$
4		cbs	$class Base$
5	1	cv	$setvar r$
6	5 4	cfv	$class {Base}_{r}$
7		vv	$setvar v$
8	3	cv	$setvar s$
9	8 4	cfv	$class {Base}_{s}$
10		vw	$setvar w$
11		vf	$setvar f$
12	10	cv	$setvar w$
13		cmap	$class ↑_{𝑚}$
14	7	cv	$setvar v$
15	12 14 13	co	$class (w^{v})$
16	11	cv	$setvar f$
17		cur	$class 1_{r}$
18	5 17	cfv	$class 1_{r}$
19	18 16	cfv	$class f (1_{r})$
20	8 17	cfv	$class 1_{s}$
21	19 20	wceq	$wff f (1_{r}) = 1_{s}$
22		vx	$setvar x$
23		vy	$setvar y$
24	22	cv	$setvar x$
25		cplusg	$class +_{𝑔}$
26	5 25	cfv	$class +_{r}$
27	23	cv	$setvar y$
28	24 27 26	co	$class (x +_{r} y)$
29	28 16	cfv	$class f (x +_{r} y)$
30	24 16	cfv	$class f (x)$
31	8 25	cfv	$class +_{s}$
32	27 16	cfv	$class f (y)$
33	30 32 31	co	$class (f (x) +_{s} f (y))$
34	29 33	wceq	$wff f (x +_{r} y) = f (x) +_{s} f (y)$
35		cmulr	$class \cdot_{𝑟}$
36	5 35	cfv	$class \cdot_{r}$
37	24 27 36	co	$class (x \cdot_{r} y)$
38	37 16	cfv	$class f (x \cdot_{r} y)$
39	8 35	cfv	$class \cdot_{s}$
40	30 32 39	co	$class (f (x) \cdot_{s} f (y))$
41	38 40	wceq	$wff f (x \cdot_{r} y) = f (x) \cdot_{s} f (y)$
42	34 41	wa	$wff (f (x +_{r} y) = f (x) +_{s} f (y) \land f (x \cdot_{r} y) = f (x) \cdot_{s} f (y))$
43	42 23 14	wral	$wff \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))$
44	43 22 14	wral	$wff \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))$
45	21 44	wa	$wff (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)))$
46	45 11 15	crab	$class \{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)))\}$
47	10 9 46	csb	$class ⦋ {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)))\}$
48	7 6 47	csb	$class ⦋ {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)))\}$
49	1 3 2 2 48	cmpo	$class (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)))\})$
50	0 49	wceq	$wff 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)))\})$

Metamath Proof Explorer

Definition df-rnghom

Detailed syntax breakdown