Metamath Proof Explorer

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 
|- K = ( Base ` R )
matvscl.a 
|- A = ( N Mat R )
matvscl.b 
|- B = ( Base ` A )
matvscl.s 
|- .x. = ( .s ` A )
Assertion matvscl 
|- ( ( ( N e. Fin /\ R e. Ring ) /\ ( C e. K /\ X e. B ) ) -> ( C .x. X ) e. B )

Proof

Step Hyp Ref Expression
1 matvscl.k 
 |-  K = ( Base ` R )
2 matvscl.a 
 |-  A = ( N Mat R )
3 matvscl.b 
 |-  B = ( Base ` A )
4 matvscl.s 
 |-  .x. = ( .s ` A )
5 2 matlmod 
 |-  ( ( N e. Fin /\ R e. Ring ) -> A e. LMod )
6 5 adantr 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( C e. K /\ X e. B ) ) -> A e. LMod )
7 2 matsca2 
 |-  ( ( N e. Fin /\ R e. Ring ) -> R = ( Scalar ` A ) )
8 7 fveq2d 
 |-  ( ( N e. Fin /\ R e. Ring ) -> ( Base ` R ) = ( Base ` ( Scalar ` A ) ) )
9 1 8 syl5eq 
 |-  ( ( N e. Fin /\ R e. Ring ) -> K = ( Base ` ( Scalar ` A ) ) )
10 9 eleq2d 
 |-  ( ( N e. Fin /\ R e. Ring ) -> ( C e. K <-> C e. ( Base ` ( Scalar ` A ) ) ) )
11 10 biimpd 
 |-  ( ( N e. Fin /\ R e. Ring ) -> ( C e. K -> C e. ( Base ` ( Scalar ` A ) ) ) )
12 11 adantrd 
 |-  ( ( N e. Fin /\ R e. Ring ) -> ( ( C e. K /\ X e. B ) -> C e. ( Base ` ( Scalar ` A ) ) ) )
13 12 imp 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( C e. K /\ X e. B ) ) -> C e. ( Base ` ( Scalar ` A ) ) )
14 simprr 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( C e. K /\ X e. B ) ) -> X e. B )
15 eqid 
 |-  ( Scalar ` A ) = ( Scalar ` A )
16 eqid 
 |-  ( Base ` ( Scalar ` A ) ) = ( Base ` ( Scalar ` A ) )
17 3 15 4 16 lmodvscl 
 |-  ( ( A e. LMod /\ C e. ( Base ` ( Scalar ` A ) ) /\ X e. B ) -> ( C .x. X ) e. B )
18 6 13 14 17 syl3anc 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( C e. K /\ X e. B ) ) -> ( C .x. X ) e. B )