Metamath Proof Explorer

Theorem mat1dimscm

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

Ref Expression
Hypotheses mat1dim.a 
|- A = ( { E } Mat R )
mat1dim.b 
|- B = ( Base ` R )
mat1dim.o 
|- O = <. E , E >.
Assertion mat1dimscm 
|- ( ( ( R e. Ring /\ E e. V ) /\ ( X e. B /\ Y e. B ) ) -> ( X ( .s ` A ) { <. O , Y >. } ) = { <. O , ( X ( .r ` R ) Y ) >. } )

Proof

Step Hyp Ref Expression
1 mat1dim.a 
 |-  A = ( { E } Mat R )
2 mat1dim.b 
 |-  B = ( Base ` R )
3 mat1dim.o 
 |-  O = <. E , E >.
4 opex 
 |-  <. E , E >. e. _V
5 3 4 eqeltri 
 |-  O e. _V
6 5 a1i 
 |-  ( Y e. B -> O e. _V )
7 6 anim2i 
 |-  ( ( X e. B /\ Y e. B ) -> ( X e. B /\ O e. _V ) )
8 7 ancomd 
 |-  ( ( X e. B /\ Y e. B ) -> ( O e. _V /\ X e. B ) )
9 fnsng 
 |-  ( ( O e. _V /\ X e. B ) -> { <. O , X >. } Fn { O } )
10 8 9 syl 
 |-  ( ( X e. B /\ Y e. B ) -> { <. O , X >. } Fn { O } )
11 10 adantl 
 |-  ( ( ( R e. Ring /\ E e. V ) /\ ( X e. B /\ Y e. B ) ) -> { <. O , X >. } Fn { O } )
12 xpsng 
 |-  ( ( O e. _V /\ X e. B ) -> ( { O } X. { X } ) = { <. O , X >. } )
13 8 12 syl 
 |-  ( ( X e. B /\ Y e. B ) -> ( { O } X. { X } ) = { <. O , X >. } )
14 13 adantl 
 |-  ( ( ( R e. Ring /\ E e. V ) /\ ( X e. B /\ Y e. B ) ) -> ( { O } X. { X } ) = { <. O , X >. } )
15 14 fneq1d 
 |-  ( ( ( R e. Ring /\ E e. V ) /\ ( X e. B /\ Y e. B ) ) -> ( ( { O } X. { X } ) Fn { O } <-> { <. O , X >. } Fn { O } ) )
16 11 15 mpbird 
 |-  ( ( ( R e. Ring /\ E e. V ) /\ ( X e. B /\ Y e. B ) ) -> ( { O } X. { X } ) Fn { O } )
17 xpsng 
 |-  ( ( E e. V /\ E e. V ) -> ( { E } X. { E } ) = { <. E , E >. } )
18 3 sneqi 
 |-  { O } = { <. E , E >. }
19 17 18 eqtr4di 
 |-  ( ( E e. V /\ E e. V ) -> ( { E } X. { E } ) = { O } )
20 19 anidms 
 |-  ( E e. V -> ( { E } X. { E } ) = { O } )
21 20 ad2antlr 
 |-  ( ( ( R e. Ring /\ E e. V ) /\ ( X e. B /\ Y e. B ) ) -> ( { E } X. { E } ) = { O } )
22 21 xpeq1d 
 |-  ( ( ( R e. Ring /\ E e. V ) /\ ( X e. B /\ Y e. B ) ) -> ( ( { E } X. { E } ) X. { X } ) = ( { O } X. { X } ) )
23 22 fneq1d 
 |-  ( ( ( R e. Ring /\ E e. V ) /\ ( X e. B /\ Y e. B ) ) -> ( ( ( { E } X. { E } ) X. { X } ) Fn { O } <-> ( { O } X. { X } ) Fn { O } ) )
24 16 23 mpbird 
 |-  ( ( ( R e. Ring /\ E e. V ) /\ ( X e. B /\ Y e. B ) ) -> ( ( { E } X. { E } ) X. { X } ) Fn { O } )
25 5 a1i 
 |-  ( X e. B -> O e. _V )
26 fnsng 
 |-  ( ( O e. _V /\ Y e. B ) -> { <. O , Y >. } Fn { O } )
27 25 26 sylan 
 |-  ( ( X e. B /\ Y e. B ) -> { <. O , Y >. } Fn { O } )
28 27 adantl 
 |-  ( ( ( R e. Ring /\ E e. V ) /\ ( X e. B /\ Y e. B ) ) -> { <. O , Y >. } Fn { O } )
29 snex 
 |-  { O } e. _V
30 29 a1i 
 |-  ( ( ( R e. Ring /\ E e. V ) /\ ( X e. B /\ Y e. B ) ) -> { O } e. _V )
31 inidm 
 |-  ( { O } i^i { O } ) = { O }
32 elsni 
 |-  ( x e. { O } -> x = O )
33 fveq2 
 |-  ( x = O -> ( ( ( { E } X. { E } ) X. { X } ) ` x ) = ( ( ( { E } X. { E } ) X. { X } ) ` O ) )
34 17 anidms 
 |-  ( E e. V -> ( { E } X. { E } ) = { <. E , E >. } )
35 34 ad2antlr 
 |-  ( ( ( R e. Ring /\ E e. V ) /\ ( X e. B /\ Y e. B ) ) -> ( { E } X. { E } ) = { <. E , E >. } )
36 35 xpeq1d 
 |-  ( ( ( R e. Ring /\ E e. V ) /\ ( X e. B /\ Y e. B ) ) -> ( ( { E } X. { E } ) X. { X } ) = ( { <. E , E >. } X. { X } ) )
37 4 a1i 
 |-  ( Y e. B -> <. E , E >. e. _V )
38 37 anim2i 
 |-  ( ( X e. B /\ Y e. B ) -> ( X e. B /\ <. E , E >. e. _V ) )
39 38 ancomd 
 |-  ( ( X e. B /\ Y e. B ) -> ( <. E , E >. e. _V /\ X e. B ) )
40 xpsng 
 |-  ( ( <. E , E >. e. _V /\ X e. B ) -> ( { <. E , E >. } X. { X } ) = { <. <. E , E >. , X >. } )
41 3 eqcomi 
 |-  <. E , E >. = O
42 41 opeq1i 
 |-  <. <. E , E >. , X >. = <. O , X >.
43 42 sneqi 
 |-  { <. <. E , E >. , X >. } = { <. O , X >. }
44 40 43 eqtrdi 
 |-  ( ( <. E , E >. e. _V /\ X e. B ) -> ( { <. E , E >. } X. { X } ) = { <. O , X >. } )
45 39 44 syl 
 |-  ( ( X e. B /\ Y e. B ) -> ( { <. E , E >. } X. { X } ) = { <. O , X >. } )
46 45 adantl 
 |-  ( ( ( R e. Ring /\ E e. V ) /\ ( X e. B /\ Y e. B ) ) -> ( { <. E , E >. } X. { X } ) = { <. O , X >. } )
47 36 46 eqtrd 
 |-  ( ( ( R e. Ring /\ E e. V ) /\ ( X e. B /\ Y e. B ) ) -> ( ( { E } X. { E } ) X. { X } ) = { <. O , X >. } )
48 47 fveq1d 
 |-  ( ( ( R e. Ring /\ E e. V ) /\ ( X e. B /\ Y e. B ) ) -> ( ( ( { E } X. { E } ) X. { X } ) ` O ) = ( { <. O , X >. } ` O ) )
49 fvsng 
 |-  ( ( O e. _V /\ X e. B ) -> ( { <. O , X >. } ` O ) = X )
50 8 49 syl 
 |-  ( ( X e. B /\ Y e. B ) -> ( { <. O , X >. } ` O ) = X )
51 50 adantl 
 |-  ( ( ( R e. Ring /\ E e. V ) /\ ( X e. B /\ Y e. B ) ) -> ( { <. O , X >. } ` O ) = X )
52 48 51 eqtrd 
 |-  ( ( ( R e. Ring /\ E e. V ) /\ ( X e. B /\ Y e. B ) ) -> ( ( ( { E } X. { E } ) X. { X } ) ` O ) = X )
53 33 52 sylan9eq 
 |-  ( ( x = O /\ ( ( R e. Ring /\ E e. V ) /\ ( X e. B /\ Y e. B ) ) ) -> ( ( ( { E } X. { E } ) X. { X } ) ` x ) = X )
54 53 ex 
 |-  ( x = O -> ( ( ( R e. Ring /\ E e. V ) /\ ( X e. B /\ Y e. B ) ) -> ( ( ( { E } X. { E } ) X. { X } ) ` x ) = X ) )
55 32 54 syl 
 |-  ( x e. { O } -> ( ( ( R e. Ring /\ E e. V ) /\ ( X e. B /\ Y e. B ) ) -> ( ( ( { E } X. { E } ) X. { X } ) ` x ) = X ) )
56 55 impcom 
 |-  ( ( ( ( R e. Ring /\ E e. V ) /\ ( X e. B /\ Y e. B ) ) /\ x e. { O } ) -> ( ( ( { E } X. { E } ) X. { X } ) ` x ) = X )
57 fveq2 
 |-  ( x = O -> ( { <. O , Y >. } ` x ) = ( { <. O , Y >. } ` O ) )
58 fvsng 
 |-  ( ( O e. _V /\ Y e. B ) -> ( { <. O , Y >. } ` O ) = Y )
59 25 58 sylan 
 |-  ( ( X e. B /\ Y e. B ) -> ( { <. O , Y >. } ` O ) = Y )
60 59 adantl 
 |-  ( ( ( R e. Ring /\ E e. V ) /\ ( X e. B /\ Y e. B ) ) -> ( { <. O , Y >. } ` O ) = Y )
61 57 60 sylan9eq 
 |-  ( ( x = O /\ ( ( R e. Ring /\ E e. V ) /\ ( X e. B /\ Y e. B ) ) ) -> ( { <. O , Y >. } ` x ) = Y )
62 61 ex 
 |-  ( x = O -> ( ( ( R e. Ring /\ E e. V ) /\ ( X e. B /\ Y e. B ) ) -> ( { <. O , Y >. } ` x ) = Y ) )
63 32 62 syl 
 |-  ( x e. { O } -> ( ( ( R e. Ring /\ E e. V ) /\ ( X e. B /\ Y e. B ) ) -> ( { <. O , Y >. } ` x ) = Y ) )
64 63 impcom 
 |-  ( ( ( ( R e. Ring /\ E e. V ) /\ ( X e. B /\ Y e. B ) ) /\ x e. { O } ) -> ( { <. O , Y >. } ` x ) = Y )
65 24 28 30 30 31 56 64 offval 
 |-  ( ( ( R e. Ring /\ E e. V ) /\ ( X e. B /\ Y e. B ) ) -> ( ( ( { E } X. { E } ) X. { X } ) oF ( .r ` R ) { <. O , Y >. } ) = ( x e. { O } |-> ( X ( .r ` R ) Y ) ) )
66 simprl 
 |-  ( ( ( R e. Ring /\ E e. V ) /\ ( X e. B /\ Y e. B ) ) -> X e. B )
67 simpr 
 |-  ( ( X e. B /\ Y e. B ) -> Y e. B )
68 67 anim2i 
 |-  ( ( ( R e. Ring /\ E e. V ) /\ ( X e. B /\ Y e. B ) ) -> ( ( R e. Ring /\ E e. V ) /\ Y e. B ) )
69 df-3an 
 |-  ( ( R e. Ring /\ E e. V /\ Y e. B ) <-> ( ( R e. Ring /\ E e. V ) /\ Y e. B ) )
70 68 69 sylibr 
 |-  ( ( ( R e. Ring /\ E e. V ) /\ ( X e. B /\ Y e. B ) ) -> ( R e. Ring /\ E e. V /\ Y e. B ) )
71 1 2 3 mat1dimbas 
 |-  ( ( R e. Ring /\ E e. V /\ Y e. B ) -> { <. O , Y >. } e. ( Base ` A ) )
72 70 71 syl 
 |-  ( ( ( R e. Ring /\ E e. V ) /\ ( X e. B /\ Y e. B ) ) -> { <. O , Y >. } e. ( Base ` A ) )
73 eqid 
 |-  ( Base ` A ) = ( Base ` A )
74 eqid 
 |-  ( .s ` A ) = ( .s ` A )
75 eqid 
 |-  ( .r ` R ) = ( .r ` R )
76 eqid 
 |-  ( { E } X. { E } ) = ( { E } X. { E } )
77 1 73 2 74 75 76 matvsca2 
 |-  ( ( X e. B /\ { <. O , Y >. } e. ( Base ` A ) ) -> ( X ( .s ` A ) { <. O , Y >. } ) = ( ( ( { E } X. { E } ) X. { X } ) oF ( .r ` R ) { <. O , Y >. } ) )
78 66 72 77 syl2anc 
 |-  ( ( ( R e. Ring /\ E e. V ) /\ ( X e. B /\ Y e. B ) ) -> ( X ( .s ` A ) { <. O , Y >. } ) = ( ( ( { E } X. { E } ) X. { X } ) oF ( .r ` R ) { <. O , Y >. } ) )
79 3anass 
 |-  ( ( R e. Ring /\ X e. B /\ Y e. B ) <-> ( R e. Ring /\ ( X e. B /\ Y e. B ) ) )
80 79 biimpri 
 |-  ( ( R e. Ring /\ ( X e. B /\ Y e. B ) ) -> ( R e. Ring /\ X e. B /\ Y e. B ) )
81 80 adantlr 
 |-  ( ( ( R e. Ring /\ E e. V ) /\ ( X e. B /\ Y e. B ) ) -> ( R e. Ring /\ X e. B /\ Y e. B ) )
82 2 75 ringcl 
 |-  ( ( R e. Ring /\ X e. B /\ Y e. B ) -> ( X ( .r ` R ) Y ) e. B )
83 81 82 syl 
 |-  ( ( ( R e. Ring /\ E e. V ) /\ ( X e. B /\ Y e. B ) ) -> ( X ( .r ` R ) Y ) e. B )
84 fmptsn 
 |-  ( ( O e. _V /\ ( X ( .r ` R ) Y ) e. B ) -> { <. O , ( X ( .r ` R ) Y ) >. } = ( x e. { O } |-> ( X ( .r ` R ) Y ) ) )
85 5 83 84 sylancr 
 |-  ( ( ( R e. Ring /\ E e. V ) /\ ( X e. B /\ Y e. B ) ) -> { <. O , ( X ( .r ` R ) Y ) >. } = ( x e. { O } |-> ( X ( .r ` R ) Y ) ) )
86 65 78 85 3eqtr4d 
 |-  ( ( ( R e. Ring /\ E e. V ) /\ ( X e. B /\ Y e. B ) ) -> ( X ( .s ` A ) { <. O , Y >. } ) = { <. O , ( X ( .r ` R ) Y ) >. } )