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 = algSc (W)$
	asclf1.b	$⊢ B = {Base}_{W}$
	asclf1.s	$⊢ S = Scalar (W)$
	asclf1.k	$⊢ K = {Base}_{S}$
	asclf1.0	$⊢ \underset{˙}{0} = 0_{W}$
	asclf1.n	$⊢ N = 0_{S}$
	asclf1.r	$⊢ φ \to W \in Ring$
	asclf1.m	$⊢ φ \to W \in LMod$
Assertion	asclf1	$⊢ φ \to (A : K \underset{1-1}{⟶} B \leftrightarrow \forall s \in K (A (s) = \underset{˙}{0} \to s = N))$

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

Metamath Proof Explorer