Theorem rnasclmulcl

Description: (Vector) multiplication is closed for scalar multiples of the unit vector. (Contributed by SN, 5-Nov-2023)

	Ref	Expression
Hypotheses	rnasclmulcl.c	|- C = ( algSc ` W )
	rnasclmulcl.x	|- .X. = ( .r ` W )
	rnasclmulcl.w	|- ( ph -> W e. AssAlg )
Assertion	rnasclmulcl	|- ( ( ph /\ ( X e. ran C /\ Y e. ran C ) ) -> ( X .X. Y ) e. ran C )

Proof

Step	Hyp	Ref	Expression
1		rnasclmulcl.c	|- C = ( algSc ` W )
2		rnasclmulcl.x	|- .X. = ( .r ` W )
3		rnasclmulcl.w	|- ( ph -> W e. AssAlg )
4	1 3	rnasclsubrg	|- ( ph -> ran C e. ( SubRing ` W ) )
5	2	subrgmcl	|- ( ( ran C e. ( SubRing ` W ) /\ X e. ran C /\ Y e. ran C ) -> ( X .X. Y ) e. ran C )
6	4 5	syl3an1	|- ( ( ph /\ X e. ran C /\ Y e. ran C ) -> ( X .X. Y ) e. ran C )
7	6	3expb	|- ( ( ph /\ ( X e. ran C /\ Y e. ran C ) ) -> ( X .X. Y ) e. ran C )