isrngohom

Description: The predicate "is a ring homomorphism from R to S ". (Contributed by Jeff Madsen, 19-Jun-2010)

	Ref	Expression
Hypotheses	rnghomval.1	$⊢ G = 1^{st} (R)$
	rnghomval.2	$⊢ H = 2^{nd} (R)$
	rnghomval.3	$⊢ X = ran G$
	rnghomval.4	$⊢ U = GId (H)$
	rnghomval.5	$⊢ J = 1^{st} (S)$
	rnghomval.6	$⊢ K = 2^{nd} (S)$
	rnghomval.7	$⊢ Y = ran J$
	rnghomval.8	$⊢ V = GId (K)$
Assertion	isrngohom	$⊢ (R \in RingOps \land S \in RingOps) \to (F \in (R RngHom S) \leftrightarrow (F : X ⟶ Y \land F (U) = V \land \forall x \in X \forall y \in X (F (x G y) = F (x) J F (y) \land F (x H y) = F (x) K F (y))))$

Proof

Step	Hyp	Ref	Expression
1		rnghomval.1	$⊢ G = 1^{st} (R)$
2		rnghomval.2	$⊢ H = 2^{nd} (R)$
3		rnghomval.3	$⊢ X = ran G$
4		rnghomval.4	$⊢ U = GId (H)$
5		rnghomval.5	$⊢ J = 1^{st} (S)$
6		rnghomval.6	$⊢ K = 2^{nd} (S)$
7		rnghomval.7	$⊢ Y = ran J$
8		rnghomval.8	$⊢ V = GId (K)$
9	1 2 3 4 5 6 7 8	rngohomval	$⊢ (R \in RingOps \land S \in RingOps) \to R RngHom S = \{f \in (Y^{X}) \| (f (U) = V \land \forall x \in X \forall y \in X (f (x G y) = f (x) J f (y) \land f (x H y) = f (x) K f (y)))\}$
10	9	eleq2d	$⊢ (R \in RingOps \land S \in RingOps) \to (F \in (R RngHom S) \leftrightarrow F \in \{f \in (Y^{X}) \| (f (U) = V \land \forall x \in X \forall y \in X (f (x G y) = f (x) J f (y) \land f (x H y) = f (x) K f (y)))\})$
11	5	fvexi	$⊢ J \in V$
12	11	rnex	$⊢ ran J \in V$
13	7 12	eqeltri	$⊢ Y \in V$
14	1	fvexi	$⊢ G \in V$
15	14	rnex	$⊢ ran G \in V$
16	3 15	eqeltri	$⊢ X \in V$
17	13 16	elmap	$⊢ F \in (Y^{X}) \leftrightarrow F : X ⟶ Y$
18	17	anbi1i	$⊢ (F \in (Y^{X}) \land (F (U) = V \land \forall x \in X \forall y \in X (F (x G y) = F (x) J F (y) \land F (x H y) = F (x) K F (y)))) \leftrightarrow (F : X ⟶ Y \land (F (U) = V \land \forall x \in X \forall y \in X (F (x G y) = F (x) J F (y) \land F (x H y) = F (x) K F (y))))$
19		fveq1	$⊢ f = F \to f (U) = F (U)$
20	19	eqeq1d	$⊢ f = F \to (f (U) = V \leftrightarrow F (U) = V)$
21		fveq1	$⊢ f = F \to f (x G y) = F (x G y)$
22		fveq1	$⊢ f = F \to f (x) = F (x)$
23		fveq1	$⊢ f = F \to f (y) = F (y)$
24	22 23	oveq12d	$⊢ f = F \to f (x) J f (y) = F (x) J F (y)$
25	21 24	eqeq12d	$⊢ f = F \to (f (x G y) = f (x) J f (y) \leftrightarrow F (x G y) = F (x) J F (y))$
26		fveq1	$⊢ f = F \to f (x H y) = F (x H y)$
27	22 23	oveq12d	$⊢ f = F \to f (x) K f (y) = F (x) K F (y)$
28	26 27	eqeq12d	$⊢ f = F \to (f (x H y) = f (x) K f (y) \leftrightarrow F (x H y) = F (x) K F (y))$
29	25 28	anbi12d	$⊢ f = F \to ((f (x G y) = f (x) J f (y) \land f (x H y) = f (x) K f (y)) \leftrightarrow (F (x G y) = F (x) J F (y) \land F (x H y) = F (x) K F (y)))$
30	29	2ralbidv	$⊢ f = F \to (\forall x \in X \forall y \in X (f (x G y) = f (x) J f (y) \land f (x H y) = f (x) K f (y)) \leftrightarrow \forall x \in X \forall y \in X (F (x G y) = F (x) J F (y) \land F (x H y) = F (x) K F (y)))$
31	20 30	anbi12d	$⊢ f = F \to ((f (U) = V \land \forall x \in X \forall y \in X (f (x G y) = f (x) J f (y) \land f (x H y) = f (x) K f (y))) \leftrightarrow (F (U) = V \land \forall x \in X \forall y \in X (F (x G y) = F (x) J F (y) \land F (x H y) = F (x) K F (y))))$
32	31	elrab	$⊢ F \in \{f \in (Y^{X}) \| (f (U) = V \land \forall x \in X \forall y \in X (f (x G y) = f (x) J f (y) \land f (x H y) = f (x) K f (y)))\} \leftrightarrow (F \in (Y^{X}) \land (F (U) = V \land \forall x \in X \forall y \in X (F (x G y) = F (x) J F (y) \land F (x H y) = F (x) K F (y))))$
33		3anass	$⊢ (F : X ⟶ Y \land F (U) = V \land \forall x \in X \forall y \in X (F (x G y) = F (x) J F (y) \land F (x H y) = F (x) K F (y))) \leftrightarrow (F : X ⟶ Y \land (F (U) = V \land \forall x \in X \forall y \in X (F (x G y) = F (x) J F (y) \land F (x H y) = F (x) K F (y))))$
34	18 32 33	3bitr4i	$⊢ F \in \{f \in (Y^{X}) \| (f (U) = V \land \forall x \in X \forall y \in X (f (x G y) = f (x) J f (y) \land f (x H y) = f (x) K f (y)))\} \leftrightarrow (F : X ⟶ Y \land F (U) = V \land \forall x \in X \forall y \in X (F (x G y) = F (x) J F (y) \land F (x H y) = F (x) K F (y)))$
35	10 34	bitrdi	$⊢ (R \in RingOps \land S \in RingOps) \to (F \in (R RngHom S) \leftrightarrow (F : X ⟶ Y \land F (U) = V \land \forall x \in X \forall y \in X (F (x G y) = F (x) J F (y) \land F (x H y) = F (x) K F (y))))$

Metamath Proof Explorer

Theorem isrngohom

Proof