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 = ( algSc ` W )
	asclf1.b	|- B = ( Base ` W )
	asclf1.s	|- S = ( Scalar ` W )
	asclf1.k	|- K = ( Base ` S )
	asclf1.0	|- .0. = ( 0g ` W )
	asclf1.n	|- N = ( 0g ` S )
	asclf1.r	|- ( ph -> W e. Ring )
	asclf1.m	|- ( ph -> W e. LMod )
Assertion	asclf1	|- ( ph -> ( A : K -1-1-> B <-> A. s e. K ( ( A ` s ) = .0. -> s = N ) ) )

Proof

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	|- .0. = ( 0g ` W )
6		asclf1.n	|- N = ( 0g ` S )
7		asclf1.r	|- ( ph -> W e. Ring )
8		asclf1.m	|- ( ph -> W e. LMod )
9	1 3 7 8	asclghm	|- ( ph -> A e. ( S GrpHom W ) )
10	4 2 6 5	ghmf1	|- ( A e. ( S GrpHom W ) -> ( A : K -1-1-> B <-> A. s e. K ( ( A ` s ) = .0. -> s = N ) ) )
11	9 10	syl	|- ( ph -> ( A : K -1-1-> B <-> A. s e. K ( ( A ` s ) = .0. -> s = N ) ) )