Theorem matvscl

Description: Closure of the scalar multiplication in the matrix ring. ( lmodvscl analog.) (Contributed by AV, 27-Nov-2019)

	Ref	Expression
Hypotheses	matvscl.k	⊢ 𝐾 = ( Base ‘ 𝑅 )
	matvscl.a	⊢ 𝐴 = ( 𝑁 Mat 𝑅 )
	matvscl.b	⊢ 𝐵 = ( Base ‘ 𝐴 )
	matvscl.s	⊢ · = ( ·𝑠 ‘ 𝐴 )
Assertion	matvscl	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝐶 ∈ 𝐾 ∧ 𝑋 ∈ 𝐵 ) ) → ( 𝐶 · 𝑋 ) ∈ 𝐵 )

Proof

Step	Hyp	Ref	Expression
1		matvscl.k	⊢ 𝐾 = ( Base ‘ 𝑅 )
2		matvscl.a	⊢ 𝐴 = ( 𝑁 Mat 𝑅 )
3		matvscl.b	⊢ 𝐵 = ( Base ‘ 𝐴 )
4		matvscl.s	⊢ · = ( ·𝑠 ‘ 𝐴 )
5	2	matlmod	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → 𝐴 ∈ LMod )
6	5	adantr	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝐶 ∈ 𝐾 ∧ 𝑋 ∈ 𝐵 ) ) → 𝐴 ∈ LMod )
7	2	matsca2	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → 𝑅 = ( Scalar ‘ 𝐴 ) )
8	7	fveq2d	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → ( Base ‘ 𝑅 ) = ( Base ‘ ( Scalar ‘ 𝐴 ) ) )
9	1 8	syl5eq	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → 𝐾 = ( Base ‘ ( Scalar ‘ 𝐴 ) ) )
10	9	eleq2d	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → ( 𝐶 ∈ 𝐾 ↔ 𝐶 ∈ ( Base ‘ ( Scalar ‘ 𝐴 ) ) ) )
11	10	biimpd	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → ( 𝐶 ∈ 𝐾 → 𝐶 ∈ ( Base ‘ ( Scalar ‘ 𝐴 ) ) ) )
12	11	adantrd	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → ( ( 𝐶 ∈ 𝐾 ∧ 𝑋 ∈ 𝐵 ) → 𝐶 ∈ ( Base ‘ ( Scalar ‘ 𝐴 ) ) ) )
13	12	imp	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝐶 ∈ 𝐾 ∧ 𝑋 ∈ 𝐵 ) ) → 𝐶 ∈ ( Base ‘ ( Scalar ‘ 𝐴 ) ) )
14		simprr	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝐶 ∈ 𝐾 ∧ 𝑋 ∈ 𝐵 ) ) → 𝑋 ∈ 𝐵 )
15		eqid	⊢ ( Scalar ‘ 𝐴 ) = ( Scalar ‘ 𝐴 )
16		eqid	⊢ ( Base ‘ ( Scalar ‘ 𝐴 ) ) = ( Base ‘ ( Scalar ‘ 𝐴 ) )
17	3 15 4 16	lmodvscl	⊢ ( ( 𝐴 ∈ LMod ∧ 𝐶 ∈ ( Base ‘ ( Scalar ‘ 𝐴 ) ) ∧ 𝑋 ∈ 𝐵 ) → ( 𝐶 · 𝑋 ) ∈ 𝐵 )
18	6 13 14 17	syl3anc	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝐶 ∈ 𝐾 ∧ 𝑋 ∈ 𝐵 ) ) → ( 𝐶 · 𝑋 ) ∈ 𝐵 )