Metamath Proof Explorer

Theorem rim0to0OLD

Description: Obsolete version of gim0to0 as of 13-May-2023. (Contributed by AV, 24-Oct-2019) (New usage is discouraged.) (Proof modification is discouraged.)

		Ref	Expression
	Hypotheses	f1rhm0to0OLD.a	$⊢ A = {Base}_{R}$
		f1rhm0to0OLD.b	$⊢ B = {Base}_{S}$
		f1rhm0to0OLD.n	$⊢ N = 0_{S}$
		f1rhm0to0OLD.0	$⊢ \underset{˙}{0} = 0_{R}$
	Assertion	rim0to0OLD	$⊢ (F \in (R RingIso S) \land X \in A) \to (F (X) = N \leftrightarrow X = \underset{˙}{0})$

Proof

Step	Hyp	Ref	Expression
1		f1rhm0to0OLD.a	$⊢ A = {Base}_{R}$
2		f1rhm0to0OLD.b	$⊢ B = {Base}_{S}$
3		f1rhm0to0OLD.n	$⊢ N = 0_{S}$
4		f1rhm0to0OLD.0	$⊢ \underset{˙}{0} = 0_{R}$
5	1 2	rimrhm	$⊢ F \in (R RingIso S) \to F \in (R RingHom S)$
6	1 2	rimf1o	$⊢ F \in (R RingIso S) \to F : A \underset{1-1 onto}{⟶} B$
7		f1of1	$⊢ F : A \underset{1-1 onto}{⟶} B \to F : A \underset{1-1}{⟶} B$
8	6 7	syl	$⊢ F \in (R RingIso S) \to F : A \underset{1-1}{⟶} B$
9	5 8	jca	$⊢ F \in (R RingIso S) \to (F \in (R RingHom S) \land F : A \underset{1-1}{⟶} B)$
10	9	anim1i	$⊢ (F \in (R RingIso S) \land X \in A) \to ((F \in (R RingHom S) \land F : A \underset{1-1}{⟶} B) \land X \in A)$
11		df-3an	$⊢ (F \in (R RingHom S) \land F : A \underset{1-1}{⟶} B \land X \in A) \leftrightarrow ((F \in (R RingHom S) \land F : A \underset{1-1}{⟶} B) \land X \in A)$
12	10 11	sylibr	$⊢ (F \in (R RingIso S) \land X \in A) \to (F \in (R RingHom S) \land F : A \underset{1-1}{⟶} B \land X \in A)$
13	1 2 3 4	f1rhm0to0OLD	$⊢ (F \in (R RingHom S) \land F : A \underset{1-1}{⟶} B \land X \in A) \to (F (X) = N \leftrightarrow X = \underset{˙}{0})$
14	12 13	syl	$⊢ (F \in (R RingIso S) \land X \in A) \to (F (X) = N \leftrightarrow X = \underset{˙}{0})$