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	$⊢ \underset{˙}{\times} = \cdot_{W}$
	rnasclmulcl.w	$⊢ φ \to W \in AssAlg$
Assertion	rnasclmulcl	$⊢ (φ \land (X \in ran C \land Y \in ran C)) \to X \underset{˙}{\times} Y \in ran C$

Step	Hyp	Ref	Expression
1		rnasclmulcl.c	$⊢ C = algSc (W)$
2		rnasclmulcl.x	$⊢ \underset{˙}{\times} = \cdot_{W}$
3		rnasclmulcl.w	$⊢ φ \to W \in AssAlg$
4	1 3	rnasclsubrg	$⊢ φ \to ran C \in SubRing (W)$
5	2	subrgmcl	$⊢ (ran C \in SubRing (W) \land X \in ran C \land Y \in ran C) \to X \underset{˙}{\times} Y \in ran C$
6	4 5	syl3an1	$⊢ (φ \land X \in ran C \land Y \in ran C) \to X \underset{˙}{\times} Y \in ran C$
7	6	3expb	$⊢ (φ \land (X \in ran C \land Y \in ran C)) \to X \underset{˙}{\times} Y \in ran C$

Metamath Proof Explorer