Theorem f1rhm0to0OLD

Description: Obsolete version of f1ghm0to0 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={\mathrm{Base}}_R$$
	f1rhm0to0OLD.b	$$⊢B={\mathrm{Base}}_S$$
	f1rhm0to0OLD.n	$$⊢N=0_S$$
	f1rhm0to0OLD.0	$$⊢\underset{\dot{}}{0}=0_R$$
Assertion	f1rhm0to0OLD	$$⊢\left(F\in \left(R\mathrm{RingHom}S\right)\wedge F:A\underset{1-1}{⟶}B\wedge X\in A\right)\to \left(F\left(X\right)=N\leftrightarrow X=\underset{\dot{}}{0}\right)$$

Proof

Step	Hyp	Ref	Expression
1		f1rhm0to0OLD.a	$$⊢A={\mathrm{Base}}_R$$
2		f1rhm0to0OLD.b	$$⊢B={\mathrm{Base}}_S$$
3		f1rhm0to0OLD.n	$$⊢N=0_S$$
4		f1rhm0to0OLD.0	$$⊢\underset{\dot{}}{0}=0_R$$
5		rhmghm	$$⊢F\in \left(R\mathrm{RingHom}S\right)\to F\in \left(R\mathrm{GrpHom}S\right)$$
6	4 3	ghmid	$$⊢F\in \left(R\mathrm{GrpHom}S\right)\to F\left(\underset{\dot{}}{0}\right)=N$$
7	5 6	syl	$$⊢F\in \left(R\mathrm{RingHom}S\right)\to F\left(\underset{\dot{}}{0}\right)=N$$
8	7	3ad2ant1	$$⊢\left(F\in \left(R\mathrm{RingHom}S\right)\wedge F:A\underset{1-1}{⟶}B\wedge X\in A\right)\to F\left(\underset{\dot{}}{0}\right)=N$$
9	8	eqeq2d	$$⊢\left(F\in \left(R\mathrm{RingHom}S\right)\wedge F:A\underset{1-1}{⟶}B\wedge X\in A\right)\to \left(F\left(X\right)=F\left(\underset{\dot{}}{0}\right)\leftrightarrow F\left(X\right)=N\right)$$
10		simp2	$$⊢\left(F\in \left(R\mathrm{RingHom}S\right)\wedge F:A\underset{1-1}{⟶}B\wedge X\in A\right)\to F:A\underset{1-1}{⟶}B$$
11		simp3	$$⊢\left(F\in \left(R\mathrm{RingHom}S\right)\wedge F:A\underset{1-1}{⟶}B\wedge X\in A\right)\to X\in A$$
12		rhmrcl1	$$⊢F\in \left(R\mathrm{RingHom}S\right)\to R\in \mathrm{Ring}$$
13	1 4	ring0cl	$$⊢R\in \mathrm{Ring}\to \underset{\dot{}}{0}\in A$$
14	12 13	syl	$$⊢F\in \left(R\mathrm{RingHom}S\right)\to \underset{\dot{}}{0}\in A$$
15	14	3ad2ant1	$$⊢\left(F\in \left(R\mathrm{RingHom}S\right)\wedge F:A\underset{1-1}{⟶}B\wedge X\in A\right)\to \underset{\dot{}}{0}\in A$$
16		f1veqaeq	$$⊢\left(F:A\underset{1-1}{⟶}B\wedge \left(X\in A\wedge \underset{\dot{}}{0}\in A\right)\right)\to \left(F\left(X\right)=F\left(\underset{\dot{}}{0}\right)\to X=\underset{\dot{}}{0}\right)$$
17	10 11 15 16	syl12anc	$$⊢\left(F\in \left(R\mathrm{RingHom}S\right)\wedge F:A\underset{1-1}{⟶}B\wedge X\in A\right)\to \left(F\left(X\right)=F\left(\underset{\dot{}}{0}\right)\to X=\underset{\dot{}}{0}\right)$$
18	9 17	sylbird	$$⊢\left(F\in \left(R\mathrm{RingHom}S\right)\wedge F:A\underset{1-1}{⟶}B\wedge X\in A\right)\to \left(F\left(X\right)=N\to X=\underset{\dot{}}{0}\right)$$
19		fveq2	$$⊢X=\underset{\dot{}}{0}\to F\left(X\right)=F\left(\underset{\dot{}}{0}\right)$$
20	19 8	sylan9eqr	$$⊢\left(\left(F\in \left(R\mathrm{RingHom}S\right)\wedge F:A\underset{1-1}{⟶}B\wedge X\in A\right)\wedge X=\underset{\dot{}}{0}\right)\to F\left(X\right)=N$$
21	20	ex	$$⊢\left(F\in \left(R\mathrm{RingHom}S\right)\wedge F:A\underset{1-1}{⟶}B\wedge X\in A\right)\to \left(X=\underset{\dot{}}{0}\to F\left(X\right)=N\right)$$
22	18 21	impbid	$$⊢\left(F\in \left(R\mathrm{RingHom}S\right)\wedge F:A\underset{1-1}{⟶}B\wedge X\in A\right)\to \left(F\left(X\right)=N\leftrightarrow X=\underset{\dot{}}{0}\right)$$