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	⊢ 𝐶 = ( algSc ‘ 𝑊 )
	rnasclmulcl.x	⊢ × = ( .r ‘ 𝑊 )
	rnasclmulcl.w	⊢ ( 𝜑 → 𝑊 ∈ AssAlg )
Assertion	rnasclmulcl	⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ ran 𝐶 ∧ 𝑌 ∈ ran 𝐶 ) ) → ( 𝑋 × 𝑌 ) ∈ ran 𝐶 )

Proof

Step	Hyp	Ref	Expression
1		rnasclmulcl.c	⊢ 𝐶 = ( algSc ‘ 𝑊 )
2		rnasclmulcl.x	⊢ × = ( .r ‘ 𝑊 )
3		rnasclmulcl.w	⊢ ( 𝜑 → 𝑊 ∈ AssAlg )
4	1 3	rnasclsubrg	⊢ ( 𝜑 → ran 𝐶 ∈ ( SubRing ‘ 𝑊 ) )
5	2	subrgmcl	⊢ ( ( ran 𝐶 ∈ ( SubRing ‘ 𝑊 ) ∧ 𝑋 ∈ ran 𝐶 ∧ 𝑌 ∈ ran 𝐶 ) → ( 𝑋 × 𝑌 ) ∈ ran 𝐶 )
6	4 5	syl3an1	⊢ ( ( 𝜑 ∧ 𝑋 ∈ ran 𝐶 ∧ 𝑌 ∈ ran 𝐶 ) → ( 𝑋 × 𝑌 ) ∈ ran 𝐶 )
7	6	3expb	⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ ran 𝐶 ∧ 𝑌 ∈ ran 𝐶 ) ) → ( 𝑋 × 𝑌 ) ∈ ran 𝐶 )