Theorem asclf1

Description: Two ways of saying the scalar injection is one-to-one. (Contributed by SN, 3-Jul-2025)

	Ref	Expression
Hypotheses	asclf1.a	$$⊢A=\mathrm{algSc}\left(W\right)$$
	asclf1.b	$$⊢B={\mathrm{Base}}_W$$
	asclf1.s	$$⊢S=\mathrm{Scalar}\left(W\right)$$
	asclf1.k	$$⊢K={\mathrm{Base}}_S$$
	asclf1.0	$$⊢\underset{\dot{}}{0}=0_W$$
	asclf1.n	$$⊢N=0_S$$
	asclf1.r	$$⊢\phi \to W\in \mathrm{Ring}$$
	asclf1.m	$$⊢\phi \to W\in \mathrm{LMod}$$
Assertion	asclf1	$$⊢\phi \to \left(A:K\underset{1-1}{⟶}B\leftrightarrow \forall s\in K\left(A\left(s\right)=\underset{\dot{}}{0}\to s=N\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		asclf1.a	$$⊢A=\mathrm{algSc}\left(W\right)$$
2		asclf1.b	$$⊢B={\mathrm{Base}}_W$$
3		asclf1.s	$$⊢S=\mathrm{Scalar}\left(W\right)$$
4		asclf1.k	$$⊢K={\mathrm{Base}}_S$$
5		asclf1.0	$$⊢\underset{\dot{}}{0}=0_W$$
6		asclf1.n	$$⊢N=0_S$$
7		asclf1.r	$$⊢\phi \to W\in \mathrm{Ring}$$
8		asclf1.m	$$⊢\phi \to W\in \mathrm{LMod}$$
9	1 3 7 8	asclghm	$$⊢\phi \to A\in \left(S\mathrm{GrpHom}W\right)$$
10	4 2 6 5	ghmf1	$$⊢A\in \left(S\mathrm{GrpHom}W\right)\to \left(A:K\underset{1-1}{⟶}B\leftrightarrow \forall s\in K\left(A\left(s\right)=\underset{\dot{}}{0}\to s=N\right)\right)$$
11	9 10	syl	$$⊢\phi \to \left(A:K\underset{1-1}{⟶}B\leftrightarrow \forall s\in K\left(A\left(s\right)=\underset{\dot{}}{0}\to s=N\right)\right)$$