df-rngohom

Description: Define the function which gives the set of ring homomorphisms between two given rings. (Contributed by Jeff Madsen, 19-Jun-2010)

		Ref	Expression
	Assertion	df-rngohom	$⊢ RngHom = (r \in RingOps, s \in RingOps ⟼ \{f \in ({ran 1^{st} (s)}^{ran 1^{st} (r)}) \| (f (GId (2^{nd} (r))) = GId (2^{nd} (s)) \land \forall x \in ran 1^{st} (r) \forall y \in ran 1^{st} (r) (f (x 1^{st} (r) y) = f (x) 1^{st} (s) f (y) \land f (x 2^{nd} (r) y) = f (x) 2^{nd} (s) f (y)))\})$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		crnghom	$class RngHom$
1		vr	$setvar r$
2		crngo	$class RingOps$
3		vs	$setvar s$
4		vf	$setvar f$
5		c1st	$class 1^{st}$
6	3	cv	$setvar s$
7	6 5	cfv	$class 1^{st} (s)$
8	7	crn	$class ran 1^{st} (s)$
9		cmap	$class ↑_{𝑚}$
10	1	cv	$setvar r$
11	10 5	cfv	$class 1^{st} (r)$
12	11	crn	$class ran 1^{st} (r)$
13	8 12 9	co	$class ({ran 1^{st} (s)}^{ran 1^{st} (r)})$
14	4	cv	$setvar f$
15		cgi	$class GId$
16		c2nd	$class 2^{nd}$
17	10 16	cfv	$class 2^{nd} (r)$
18	17 15	cfv	$class GId (2^{nd} (r))$
19	18 14	cfv	$class f (GId (2^{nd} (r)))$
20	6 16	cfv	$class 2^{nd} (s)$
21	20 15	cfv	$class GId (2^{nd} (s))$
22	19 21	wceq	$wff f (GId (2^{nd} (r))) = GId (2^{nd} (s))$
23		vx	$setvar x$
24		vy	$setvar y$
25	23	cv	$setvar x$
26	24	cv	$setvar y$
27	25 26 11	co	$class (x 1^{st} (r) y)$
28	27 14	cfv	$class f (x 1^{st} (r) y)$
29	25 14	cfv	$class f (x)$
30	26 14	cfv	$class f (y)$
31	29 30 7	co	$class (f (x) 1^{st} (s) f (y))$
32	28 31	wceq	$wff f (x 1^{st} (r) y) = f (x) 1^{st} (s) f (y)$
33	25 26 17	co	$class (x 2^{nd} (r) y)$
34	33 14	cfv	$class f (x 2^{nd} (r) y)$
35	29 30 20	co	$class (f (x) 2^{nd} (s) f (y))$
36	34 35	wceq	$wff f (x 2^{nd} (r) y) = f (x) 2^{nd} (s) f (y)$
37	32 36	wa	$wff (f (x 1^{st} (r) y) = f (x) 1^{st} (s) f (y) \land f (x 2^{nd} (r) y) = f (x) 2^{nd} (s) f (y))$
38	37 24 12	wral	$wff \forall y \in ran 1^{st} (r) (f (x 1^{st} (r) y) = f (x) 1^{st} (s) f (y) \land f (x 2^{nd} (r) y) = f (x) 2^{nd} (s) f (y))$
39	38 23 12	wral	$wff \forall x \in ran 1^{st} (r) \forall y \in ran 1^{st} (r) (f (x 1^{st} (r) y) = f (x) 1^{st} (s) f (y) \land f (x 2^{nd} (r) y) = f (x) 2^{nd} (s) f (y))$
40	22 39	wa	$wff (f (GId (2^{nd} (r))) = GId (2^{nd} (s)) \land \forall x \in ran 1^{st} (r) \forall y \in ran 1^{st} (r) (f (x 1^{st} (r) y) = f (x) 1^{st} (s) f (y) \land f (x 2^{nd} (r) y) = f (x) 2^{nd} (s) f (y)))$
41	40 4 13	crab	$class \{f \in ({ran 1^{st} (s)}^{ran 1^{st} (r)}) \| (f (GId (2^{nd} (r))) = GId (2^{nd} (s)) \land \forall x \in ran 1^{st} (r) \forall y \in ran 1^{st} (r) (f (x 1^{st} (r) y) = f (x) 1^{st} (s) f (y) \land f (x 2^{nd} (r) y) = f (x) 2^{nd} (s) f (y)))\}$
42	1 3 2 2 41	cmpo	$class (r \in RingOps, s \in RingOps ⟼ \{f \in ({ran 1^{st} (s)}^{ran 1^{st} (r)}) \| (f (GId (2^{nd} (r))) = GId (2^{nd} (s)) \land \forall x \in ran 1^{st} (r) \forall y \in ran 1^{st} (r) (f (x 1^{st} (r) y) = f (x) 1^{st} (s) f (y) \land f (x 2^{nd} (r) y) = f (x) 2^{nd} (s) f (y)))\})$
43	0 42	wceq	$wff RngHom = (r \in RingOps, s \in RingOps ⟼ \{f \in ({ran 1^{st} (s)}^{ran 1^{st} (r)}) \| (f (GId (2^{nd} (r))) = GId (2^{nd} (s)) \land \forall x \in ran 1^{st} (r) \forall y \in ran 1^{st} (r) (f (x 1^{st} (r) y) = f (x) 1^{st} (s) f (y) \land f (x 2^{nd} (r) y) = f (x) 2^{nd} (s) f (y)))\})$

Metamath Proof Explorer

Definition df-rngohom

Detailed syntax breakdown