Theorem f1rhm0to0ALT

Description: Alternate proof for f1ghm0to0 . Using ghmf1 does not make the proof shorter and requires disjoint variable restrictions! (Contributed by AV, 24-Oct-2019) (New usage is discouraged.) (Proof modification is discouraged.)

	Ref	Expression
Hypotheses	gim0to0ALT.a	$$⊢A={\mathrm{Base}}_R$$
	gim0to0ALT.b	$$⊢B={\mathrm{Base}}_S$$
	gim0to0ALT.n	$$⊢N=0_S$$
	gim0to0ALT.0	$$⊢\underset{\dot{}}{0}=0_R$$
Assertion	f1rhm0to0ALT	$$⊢\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		gim0to0ALT.a	$$⊢A={\mathrm{Base}}_R$$
2		gim0to0ALT.b	$$⊢B={\mathrm{Base}}_S$$
3		gim0to0ALT.n	$$⊢N=0_S$$
4		gim0to0ALT.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	5	adantr	$$⊢\left(F\in \left(R\mathrm{RingHom}S\right)\wedge X\in A\right)\to F\in \left(R\mathrm{GrpHom}S\right)$$
7	1 2 4 3	ghmf1	$$⊢F\in \left(R\mathrm{GrpHom}S\right)\to \left(F:A\underset{1-1}{⟶}B\leftrightarrow \forall x\in A\left(F\left(x\right)=N\to x=\underset{\dot{}}{0}\right)\right)$$
8	6 7	syl	$$⊢\left(F\in \left(R\mathrm{RingHom}S\right)\wedge X\in A\right)\to \left(F:A\underset{1-1}{⟶}B\leftrightarrow \forall x\in A\left(F\left(x\right)=N\to x=\underset{\dot{}}{0}\right)\right)$$
9		fveq2	$$⊢x=X\to F\left(x\right)=F\left(X\right)$$
10	9	eqeq1d	$$⊢x=X\to \left(F\left(x\right)=N\leftrightarrow F\left(X\right)=N\right)$$
11		eqeq1	$$⊢x=X\to \left(x=\underset{\dot{}}{0}\leftrightarrow X=\underset{\dot{}}{0}\right)$$
12	10 11	imbi12d	$$⊢x=X\to \left(\left(F\left(x\right)=N\to x=\underset{\dot{}}{0}\right)\leftrightarrow \left(F\left(X\right)=N\to X=\underset{\dot{}}{0}\right)\right)$$
13	12	rspcv	$$⊢X\in A\to \left(\forall x\in A\left(F\left(x\right)=N\to x=\underset{\dot{}}{0}\right)\to \left(F\left(X\right)=N\to X=\underset{\dot{}}{0}\right)\right)$$
14	13	adantl	$$⊢\left(F\in \left(R\mathrm{RingHom}S\right)\wedge X\in A\right)\to \left(\forall x\in A\left(F\left(x\right)=N\to x=\underset{\dot{}}{0}\right)\to \left(F\left(X\right)=N\to X=\underset{\dot{}}{0}\right)\right)$$
15	8 14	sylbid	$$⊢\left(F\in \left(R\mathrm{RingHom}S\right)\wedge X\in A\right)\to \left(F:A\underset{1-1}{⟶}B\to \left(F\left(X\right)=N\to X=\underset{\dot{}}{0}\right)\right)$$
16	15	ex	$$⊢F\in \left(R\mathrm{RingHom}S\right)\to \left(X\in A\to \left(F:A\underset{1-1}{⟶}B\to \left(F\left(X\right)=N\to X=\underset{\dot{}}{0}\right)\right)\right)$$
17	16	com23	$$⊢F\in \left(R\mathrm{RingHom}S\right)\to \left(F:A\underset{1-1}{⟶}B\to \left(X\in A\to \left(F\left(X\right)=N\to X=\underset{\dot{}}{0}\right)\right)\right)$$
18	17	3imp	$$⊢\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	4 3	ghmid	$$⊢F\in \left(R\mathrm{GrpHom}S\right)\to F\left(\underset{\dot{}}{0}\right)=N$$
21	5 20	syl	$$⊢F\in \left(R\mathrm{RingHom}S\right)\to F\left(\underset{\dot{}}{0}\right)=N$$
22	21	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$$
23	19 22	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$$
24	23	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)$$
25	18 24	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)$$