Metamath Proof Explorer

Theorem rngohom1

Description: Obsolete theorem, use rhm1 instead. A ring homomorphism preserves 1 . (Contributed by Jeff Madsen, 24-Jun-2011) (Proof modification is discouraged.) (New usage is discouraged.)

		Ref	Expression
	Hypotheses	rnghom1.1	$⊢ H = 2^{nd} (R)$
		rnghom1.2	$⊢ U = GId (H)$
		rnghom1.3	$⊢ K = 2^{nd} (S)$
		rnghom1.4	$⊢ V = GId (K)$
	Assertion	rngohom1	$⊢ (R \in RingOps \land S \in RingOps \land F \in (R RingOpsHom S)) \to F (U) = V$

Proof

Step	Hyp	Ref	Expression
1		rnghom1.1	$⊢ H = 2^{nd} (R)$
2		rnghom1.2	$⊢ U = GId (H)$
3		rnghom1.3	$⊢ K = 2^{nd} (S)$
4		rnghom1.4	$⊢ V = GId (K)$
5		eqid	$⊢ 1^{st} (R) = 1^{st} (R)$
6		eqid	$⊢ ran 1^{st} (R) = ran 1^{st} (R)$
7		eqid	$⊢ 1^{st} (S) = 1^{st} (S)$
8		eqid	$⊢ ran 1^{st} (S) = ran 1^{st} (S)$
9	5 1 6 2 7 3 8 4	isrngohom	$⊢ (R \in RingOps \land S \in RingOps) \to (F \in (R RingOpsHom S) \leftrightarrow (F : ran 1^{st} (R) ⟶ ran 1^{st} (S) \land F (U) = V \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 H y) = F (x) K F (y))))$
10	9	biimpa	$⊢ ((R \in RingOps \land S \in RingOps) \land F \in (R RingOpsHom S)) \to (F : ran 1^{st} (R) ⟶ ran 1^{st} (S) \land F (U) = V \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 H y) = F (x) K F (y)))$
11	10	simp2d	$⊢ ((R \in RingOps \land S \in RingOps) \land F \in (R RingOpsHom S)) \to F (U) = V$
12	11	3impa	$⊢ (R \in RingOps \land S \in RingOps \land F \in (R RingOpsHom S)) \to F (U) = V$