Metamath Proof Explorer

Theorem mat0dimscm

Description: The scalar multiplication in the algebra of matrices with dimension 0. (Contributed by AV, 6-Aug-2019)

Ref Expression
Hypothesis mat0dim.a 
|- A = ( (/) Mat R )
Assertion mat0dimscm 
|- ( ( R e. Ring /\ X e. ( Base ` R ) ) -> ( X ( .s ` A ) (/) ) = (/) )

Proof

Step Hyp Ref Expression
1 mat0dim.a 
 |-  A = ( (/) Mat R )
2 simpl 
 |-  ( ( R e. Ring /\ X e. ( Base ` R ) ) -> R e. Ring )
3 0fi 
 |-  (/) e. Fin
4 1 matlmod 
 |-  ( ( (/) e. Fin /\ R e. Ring ) -> A e. LMod )
5 3 2 4 sylancr 
 |-  ( ( R e. Ring /\ X e. ( Base ` R ) ) -> A e. LMod )
6 1 matsca2 
 |-  ( ( (/) e. Fin /\ R e. Ring ) -> R = ( Scalar ` A ) )
7 3 6 mpan 
 |-  ( R e. Ring -> R = ( Scalar ` A ) )
8 7 fveq2d 
 |-  ( R e. Ring -> ( Base ` R ) = ( Base ` ( Scalar ` A ) ) )
9 8 eleq2d 
 |-  ( R e. Ring -> ( X e. ( Base ` R ) <-> X e. ( Base ` ( Scalar ` A ) ) ) )
10 9 biimpa 
 |-  ( ( R e. Ring /\ X e. ( Base ` R ) ) -> X e. ( Base ` ( Scalar ` A ) ) )
11 0ex 
 |-  (/) e. _V
12 11 snid 
 |-  (/) e. { (/) }
13 1 fveq2i 
 |-  ( Base ` A ) = ( Base ` ( (/) Mat R ) )
14 mat0dimbas0 
 |-  ( R e. Ring -> ( Base ` ( (/) Mat R ) ) = { (/) } )
15 13 14 eqtrid 
 |-  ( R e. Ring -> ( Base ` A ) = { (/) } )
16 12 15 eleqtrrid 
 |-  ( R e. Ring -> (/) e. ( Base ` A ) )
17 16 adantr 
 |-  ( ( R e. Ring /\ X e. ( Base ` R ) ) -> (/) e. ( Base ` A ) )
18 eqid 
 |-  ( Base ` A ) = ( Base ` A )
19 eqid 
 |-  ( Scalar ` A ) = ( Scalar ` A )
20 eqid 
 |-  ( .s ` A ) = ( .s ` A )
21 eqid 
 |-  ( Base ` ( Scalar ` A ) ) = ( Base ` ( Scalar ` A ) )
22 18 19 20 21 lmodvscl 
 |-  ( ( A e. LMod /\ X e. ( Base ` ( Scalar ` A ) ) /\ (/) e. ( Base ` A ) ) -> ( X ( .s ` A ) (/) ) e. ( Base ` A ) )
23 5 10 17 22 syl3anc 
 |-  ( ( R e. Ring /\ X e. ( Base ` R ) ) -> ( X ( .s ` A ) (/) ) e. ( Base ` A ) )
24 15 eleq2d 
 |-  ( R e. Ring -> ( ( X ( .s ` A ) (/) ) e. ( Base ` A ) <-> ( X ( .s ` A ) (/) ) e. { (/) } ) )
25 elsni 
 |-  ( ( X ( .s ` A ) (/) ) e. { (/) } -> ( X ( .s ` A ) (/) ) = (/) )
26 24 25 biimtrdi 
 |-  ( R e. Ring -> ( ( X ( .s ` A ) (/) ) e. ( Base ` A ) -> ( X ( .s ` A ) (/) ) = (/) ) )
27 2 23 26 sylc 
 |-  ( ( R e. Ring /\ X e. ( Base ` R ) ) -> ( X ( .s ` A ) (/) ) = (/) )