Metamath Proof Explorer

Theorem smatvscl

Description: Closure of the scalar multiplication in the ring of scalar matrices. ( matvscl analog.) (Contributed by AV, 24-Dec-2019)

Ref Expression
Hypotheses smatvscl.k 
|- K = ( Base ` R )
smatvscl.a 
|- A = ( N Mat R )
smatvscl.s 
|- S = ( N ScMat R )
smatvscl.t 
|- .* = ( .s ` A )
Assertion smatvscl 
|- ( ( ( N e. Fin /\ R e. Ring ) /\ ( C e. K /\ X e. S ) ) -> ( C .* X ) e. S )

Proof

Step Hyp Ref Expression
1 smatvscl.k 
 |-  K = ( Base ` R )
2 smatvscl.a 
 |-  A = ( N Mat R )
3 smatvscl.s 
 |-  S = ( N ScMat R )
4 smatvscl.t 
 |-  .* = ( .s ` A )
5 eqid 
 |-  ( Base ` R ) = ( Base ` R )
6 eqid 
 |-  ( Base ` A ) = ( Base ` A )
7 eqid 
 |-  ( 1r ` A ) = ( 1r ` A )
8 5 2 6 7 4 3 scmatel 
 |-  ( ( N e. Fin /\ R e. Ring ) -> ( X e. S <-> ( X e. ( Base ` A ) /\ E. c e. ( Base ` R ) X = ( c .* ( 1r ` A ) ) ) ) )
9 oveq2 
 |-  ( X = ( c .* ( 1r ` A ) ) -> ( C .* X ) = ( C .* ( c .* ( 1r ` A ) ) ) )
10 9 adantl 
 |-  ( ( ( ( ( ( N e. Fin /\ R e. Ring ) /\ C e. K ) /\ X e. ( Base ` A ) ) /\ c e. ( Base ` R ) ) /\ X = ( c .* ( 1r ` A ) ) ) -> ( C .* X ) = ( C .* ( c .* ( 1r ` A ) ) ) )
11 2 matlmod 
 |-  ( ( N e. Fin /\ R e. Ring ) -> A e. LMod )
12 11 ad3antrrr 
 |-  ( ( ( ( ( N e. Fin /\ R e. Ring ) /\ C e. K ) /\ X e. ( Base ` A ) ) /\ c e. ( Base ` R ) ) -> A e. LMod )
13 2 matsca2 
 |-  ( ( N e. Fin /\ R e. Ring ) -> R = ( Scalar ` A ) )
14 13 fveq2d 
 |-  ( ( N e. Fin /\ R e. Ring ) -> ( Base ` R ) = ( Base ` ( Scalar ` A ) ) )
15 1 14 syl5eq 
 |-  ( ( N e. Fin /\ R e. Ring ) -> K = ( Base ` ( Scalar ` A ) ) )
16 15 eleq2d 
 |-  ( ( N e. Fin /\ R e. Ring ) -> ( C e. K <-> C e. ( Base ` ( Scalar ` A ) ) ) )
17 16 biimpa 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ C e. K ) -> C e. ( Base ` ( Scalar ` A ) ) )
18 17 ad2antrr 
 |-  ( ( ( ( ( N e. Fin /\ R e. Ring ) /\ C e. K ) /\ X e. ( Base ` A ) ) /\ c e. ( Base ` R ) ) -> C e. ( Base ` ( Scalar ` A ) ) )
19 13 ad2antrr 
 |-  ( ( ( ( N e. Fin /\ R e. Ring ) /\ C e. K ) /\ X e. ( Base ` A ) ) -> R = ( Scalar ` A ) )
20 19 fveq2d 
 |-  ( ( ( ( N e. Fin /\ R e. Ring ) /\ C e. K ) /\ X e. ( Base ` A ) ) -> ( Base ` R ) = ( Base ` ( Scalar ` A ) ) )
21 20 eleq2d 
 |-  ( ( ( ( N e. Fin /\ R e. Ring ) /\ C e. K ) /\ X e. ( Base ` A ) ) -> ( c e. ( Base ` R ) <-> c e. ( Base ` ( Scalar ` A ) ) ) )
22 21 biimpa 
 |-  ( ( ( ( ( N e. Fin /\ R e. Ring ) /\ C e. K ) /\ X e. ( Base ` A ) ) /\ c e. ( Base ` R ) ) -> c e. ( Base ` ( Scalar ` A ) ) )
23 2 matring 
 |-  ( ( N e. Fin /\ R e. Ring ) -> A e. Ring )
24 6 7 ringidcl 
 |-  ( A e. Ring -> ( 1r ` A ) e. ( Base ` A ) )
25 23 24 syl 
 |-  ( ( N e. Fin /\ R e. Ring ) -> ( 1r ` A ) e. ( Base ` A ) )
26 25 ad3antrrr 
 |-  ( ( ( ( ( N e. Fin /\ R e. Ring ) /\ C e. K ) /\ X e. ( Base ` A ) ) /\ c e. ( Base ` R ) ) -> ( 1r ` A ) e. ( Base ` A ) )
27 eqid 
 |-  ( Scalar ` A ) = ( Scalar ` A )
28 eqid 
 |-  ( Base ` ( Scalar ` A ) ) = ( Base ` ( Scalar ` A ) )
29 eqid 
 |-  ( .r ` ( Scalar ` A ) ) = ( .r ` ( Scalar ` A ) )
30 6 27 4 28 29 lmodvsass 
 |-  ( ( A e. LMod /\ ( C e. ( Base ` ( Scalar ` A ) ) /\ c e. ( Base ` ( Scalar ` A ) ) /\ ( 1r ` A ) e. ( Base ` A ) ) ) -> ( ( C ( .r ` ( Scalar ` A ) ) c ) .* ( 1r ` A ) ) = ( C .* ( c .* ( 1r ` A ) ) ) )
31 12 18 22 26 30 syl13anc 
 |-  ( ( ( ( ( N e. Fin /\ R e. Ring ) /\ C e. K ) /\ X e. ( Base ` A ) ) /\ c e. ( Base ` R ) ) -> ( ( C ( .r ` ( Scalar ` A ) ) c ) .* ( 1r ` A ) ) = ( C .* ( c .* ( 1r ` A ) ) ) )
32 31 eqcomd 
 |-  ( ( ( ( ( N e. Fin /\ R e. Ring ) /\ C e. K ) /\ X e. ( Base ` A ) ) /\ c e. ( Base ` R ) ) -> ( C .* ( c .* ( 1r ` A ) ) ) = ( ( C ( .r ` ( Scalar ` A ) ) c ) .* ( 1r ` A ) ) )
33 simplll 
 |-  ( ( ( ( ( N e. Fin /\ R e. Ring ) /\ C e. K ) /\ X e. ( Base ` A ) ) /\ c e. ( Base ` R ) ) -> ( N e. Fin /\ R e. Ring ) )
34 13 adantr 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ C e. K ) -> R = ( Scalar ` A ) )
35 34 eqcomd 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ C e. K ) -> ( Scalar ` A ) = R )
36 35 ad2antrr 
 |-  ( ( ( ( ( N e. Fin /\ R e. Ring ) /\ C e. K ) /\ X e. ( Base ` A ) ) /\ c e. ( Base ` R ) ) -> ( Scalar ` A ) = R )
37 36 fveq2d 
 |-  ( ( ( ( ( N e. Fin /\ R e. Ring ) /\ C e. K ) /\ X e. ( Base ` A ) ) /\ c e. ( Base ` R ) ) -> ( .r ` ( Scalar ` A ) ) = ( .r ` R ) )
38 37 oveqd 
 |-  ( ( ( ( ( N e. Fin /\ R e. Ring ) /\ C e. K ) /\ X e. ( Base ` A ) ) /\ c e. ( Base ` R ) ) -> ( C ( .r ` ( Scalar ` A ) ) c ) = ( C ( .r ` R ) c ) )
39 simp-4r 
 |-  ( ( ( ( ( N e. Fin /\ R e. Ring ) /\ C e. K ) /\ X e. ( Base ` A ) ) /\ c e. ( Base ` R ) ) -> R e. Ring )
40 simpllr 
 |-  ( ( ( ( ( N e. Fin /\ R e. Ring ) /\ C e. K ) /\ X e. ( Base ` A ) ) /\ c e. ( Base ` R ) ) -> C e. K )
41 1 eqcomi 
 |-  ( Base ` R ) = K
42 41 eleq2i 
 |-  ( c e. ( Base ` R ) <-> c e. K )
43 42 biimpi 
 |-  ( c e. ( Base ` R ) -> c e. K )
44 43 adantl 
 |-  ( ( ( ( ( N e. Fin /\ R e. Ring ) /\ C e. K ) /\ X e. ( Base ` A ) ) /\ c e. ( Base ` R ) ) -> c e. K )
45 eqid 
 |-  ( .r ` R ) = ( .r ` R )
46 1 45 ringcl 
 |-  ( ( R e. Ring /\ C e. K /\ c e. K ) -> ( C ( .r ` R ) c ) e. K )
47 39 40 44 46 syl3anc 
 |-  ( ( ( ( ( N e. Fin /\ R e. Ring ) /\ C e. K ) /\ X e. ( Base ` A ) ) /\ c e. ( Base ` R ) ) -> ( C ( .r ` R ) c ) e. K )
48 38 47 eqeltrd 
 |-  ( ( ( ( ( N e. Fin /\ R e. Ring ) /\ C e. K ) /\ X e. ( Base ` A ) ) /\ c e. ( Base ` R ) ) -> ( C ( .r ` ( Scalar ` A ) ) c ) e. K )
49 1 2 6 4 matvscl 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( ( C ( .r ` ( Scalar ` A ) ) c ) e. K /\ ( 1r ` A ) e. ( Base ` A ) ) ) -> ( ( C ( .r ` ( Scalar ` A ) ) c ) .* ( 1r ` A ) ) e. ( Base ` A ) )
50 33 48 26 49 syl12anc 
 |-  ( ( ( ( ( N e. Fin /\ R e. Ring ) /\ C e. K ) /\ X e. ( Base ` A ) ) /\ c e. ( Base ` R ) ) -> ( ( C ( .r ` ( Scalar ` A ) ) c ) .* ( 1r ` A ) ) e. ( Base ` A ) )
51 oveq1 
 |-  ( ( C ( .r ` ( Scalar ` A ) ) c ) = e -> ( ( C ( .r ` ( Scalar ` A ) ) c ) .* ( 1r ` A ) ) = ( e .* ( 1r ` A ) ) )
52 51 eqcoms 
 |-  ( e = ( C ( .r ` ( Scalar ` A ) ) c ) -> ( ( C ( .r ` ( Scalar ` A ) ) c ) .* ( 1r ` A ) ) = ( e .* ( 1r ` A ) ) )
53 52 adantl 
 |-  ( ( ( ( ( ( N e. Fin /\ R e. Ring ) /\ C e. K ) /\ X e. ( Base ` A ) ) /\ c e. ( Base ` R ) ) /\ e = ( C ( .r ` ( Scalar ` A ) ) c ) ) -> ( ( C ( .r ` ( Scalar ` A ) ) c ) .* ( 1r ` A ) ) = ( e .* ( 1r ` A ) ) )
54 48 53 rspcedeq2vd 
 |-  ( ( ( ( ( N e. Fin /\ R e. Ring ) /\ C e. K ) /\ X e. ( Base ` A ) ) /\ c e. ( Base ` R ) ) -> E. e e. K ( ( C ( .r ` ( Scalar ` A ) ) c ) .* ( 1r ` A ) ) = ( e .* ( 1r ` A ) ) )
55 1 2 6 7 4 3 scmatel 
 |-  ( ( N e. Fin /\ R e. Ring ) -> ( ( ( C ( .r ` ( Scalar ` A ) ) c ) .* ( 1r ` A ) ) e. S <-> ( ( ( C ( .r ` ( Scalar ` A ) ) c ) .* ( 1r ` A ) ) e. ( Base ` A ) /\ E. e e. K ( ( C ( .r ` ( Scalar ` A ) ) c ) .* ( 1r ` A ) ) = ( e .* ( 1r ` A ) ) ) ) )
56 55 ad3antrrr 
 |-  ( ( ( ( ( N e. Fin /\ R e. Ring ) /\ C e. K ) /\ X e. ( Base ` A ) ) /\ c e. ( Base ` R ) ) -> ( ( ( C ( .r ` ( Scalar ` A ) ) c ) .* ( 1r ` A ) ) e. S <-> ( ( ( C ( .r ` ( Scalar ` A ) ) c ) .* ( 1r ` A ) ) e. ( Base ` A ) /\ E. e e. K ( ( C ( .r ` ( Scalar ` A ) ) c ) .* ( 1r ` A ) ) = ( e .* ( 1r ` A ) ) ) ) )
57 50 54 56 mpbir2and 
 |-  ( ( ( ( ( N e. Fin /\ R e. Ring ) /\ C e. K ) /\ X e. ( Base ` A ) ) /\ c e. ( Base ` R ) ) -> ( ( C ( .r ` ( Scalar ` A ) ) c ) .* ( 1r ` A ) ) e. S )
58 32 57 eqeltrd 
 |-  ( ( ( ( ( N e. Fin /\ R e. Ring ) /\ C e. K ) /\ X e. ( Base ` A ) ) /\ c e. ( Base ` R ) ) -> ( C .* ( c .* ( 1r ` A ) ) ) e. S )
59 58 adantr 
 |-  ( ( ( ( ( ( N e. Fin /\ R e. Ring ) /\ C e. K ) /\ X e. ( Base ` A ) ) /\ c e. ( Base ` R ) ) /\ X = ( c .* ( 1r ` A ) ) ) -> ( C .* ( c .* ( 1r ` A ) ) ) e. S )
60 10 59 eqeltrd 
 |-  ( ( ( ( ( ( N e. Fin /\ R e. Ring ) /\ C e. K ) /\ X e. ( Base ` A ) ) /\ c e. ( Base ` R ) ) /\ X = ( c .* ( 1r ` A ) ) ) -> ( C .* X ) e. S )
61 60 rexlimdva2 
 |-  ( ( ( ( N e. Fin /\ R e. Ring ) /\ C e. K ) /\ X e. ( Base ` A ) ) -> ( E. c e. ( Base ` R ) X = ( c .* ( 1r ` A ) ) -> ( C .* X ) e. S ) )
62 61 expimpd 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ C e. K ) -> ( ( X e. ( Base ` A ) /\ E. c e. ( Base ` R ) X = ( c .* ( 1r ` A ) ) ) -> ( C .* X ) e. S ) )
63 62 ex 
 |-  ( ( N e. Fin /\ R e. Ring ) -> ( C e. K -> ( ( X e. ( Base ` A ) /\ E. c e. ( Base ` R ) X = ( c .* ( 1r ` A ) ) ) -> ( C .* X ) e. S ) ) )
64 63 com23 
 |-  ( ( N e. Fin /\ R e. Ring ) -> ( ( X e. ( Base ` A ) /\ E. c e. ( Base ` R ) X = ( c .* ( 1r ` A ) ) ) -> ( C e. K -> ( C .* X ) e. S ) ) )
65 8 64 sylbid 
 |-  ( ( N e. Fin /\ R e. Ring ) -> ( X e. S -> ( C e. K -> ( C .* X ) e. S ) ) )
66 65 com23 
 |-  ( ( N e. Fin /\ R e. Ring ) -> ( C e. K -> ( X e. S -> ( C .* X ) e. S ) ) )
67 66 imp32 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( C e. K /\ X e. S ) ) -> ( C .* X ) e. S )