Metamath Proof Explorer

Theorem mat1dimmul

Description: The ring multiplication in the algebra of matrices with dimension 1. (Contributed by AV, 16-Aug-2019) (Proof shortened by AV, 18-Apr-2021)

Ref Expression
Hypotheses mat1dim.a 
|- A = ( { E } Mat R )
mat1dim.b 
|- B = ( Base ` R )
mat1dim.o 
|- O = <. E , E >.
Assertion mat1dimmul 
|- ( ( ( R e. Ring /\ E e. V ) /\ ( X e. B /\ Y e. B ) ) -> ( { <. O , X >. } ( .r ` 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 snfi 
 |-  { E } e. Fin
5 simpl 
 |-  ( ( R e. Ring /\ E e. V ) -> R e. Ring )
6 eqid 
 |-  ( R maMul <. { E } , { E } , { E } >. ) = ( R maMul <. { E } , { E } , { E } >. )
7 1 6 matmulr 
 |-  ( ( { E } e. Fin /\ R e. Ring ) -> ( R maMul <. { E } , { E } , { E } >. ) = ( .r ` A ) )
8 7 eqcomd 
 |-  ( ( { E } e. Fin /\ R e. Ring ) -> ( .r ` A ) = ( R maMul <. { E } , { E } , { E } >. ) )
9 4 5 8 sylancr 
 |-  ( ( R e. Ring /\ E e. V ) -> ( .r ` A ) = ( R maMul <. { E } , { E } , { E } >. ) )
10 9 adantr 
 |-  ( ( ( R e. Ring /\ E e. V ) /\ ( X e. B /\ Y e. B ) ) -> ( .r ` A ) = ( R maMul <. { E } , { E } , { E } >. ) )
11 10 oveqd 
 |-  ( ( ( R e. Ring /\ E e. V ) /\ ( X e. B /\ Y e. B ) ) -> ( { <. O , X >. } ( .r ` A ) { <. O , Y >. } ) = ( { <. O , X >. } ( R maMul <. { E } , { E } , { E } >. ) { <. O , Y >. } ) )
12 eqid 
 |-  ( .r ` R ) = ( .r ` R )
13 5 adantr 
 |-  ( ( ( R e. Ring /\ E e. V ) /\ ( X e. B /\ Y e. B ) ) -> R e. Ring )
14 4 a1i 
 |-  ( ( ( R e. Ring /\ E e. V ) /\ ( X e. B /\ Y e. B ) ) -> { E } e. Fin )
15 opex 
 |-  <. E , E >. e. _V
16 15 a1i 
 |-  ( ( ( R e. Ring /\ E e. V ) /\ ( X e. B /\ Y e. B ) ) -> <. E , E >. e. _V )
17 simpl 
 |-  ( ( X e. B /\ Y e. B ) -> X e. B )
18 17 adantl 
 |-  ( ( ( R e. Ring /\ E e. V ) /\ ( X e. B /\ Y e. B ) ) -> X e. B )
19 16 18 fsnd 
 |-  ( ( ( R e. Ring /\ E e. V ) /\ ( X e. B /\ Y e. B ) ) -> { <. <. E , E >. , X >. } : { <. E , E >. } --> B )
20 3 opeq1i 
 |-  <. O , X >. = <. <. E , E >. , X >.
21 20 sneqi 
 |-  { <. O , X >. } = { <. <. E , E >. , X >. }
22 21 a1i 
 |-  ( E e. V -> { <. O , X >. } = { <. <. E , E >. , X >. } )
23 xpsng 
 |-  ( ( E e. V /\ E e. V ) -> ( { E } X. { E } ) = { <. E , E >. } )
24 23 anidms 
 |-  ( E e. V -> ( { E } X. { E } ) = { <. E , E >. } )
25 22 24 feq12d 
 |-  ( E e. V -> ( { <. O , X >. } : ( { E } X. { E } ) --> B <-> { <. <. E , E >. , X >. } : { <. E , E >. } --> B ) )
26 25 ad2antlr 
 |-  ( ( ( R e. Ring /\ E e. V ) /\ ( X e. B /\ Y e. B ) ) -> ( { <. O , X >. } : ( { E } X. { E } ) --> B <-> { <. <. E , E >. , X >. } : { <. E , E >. } --> B ) )
27 19 26 mpbird 
 |-  ( ( ( R e. Ring /\ E e. V ) /\ ( X e. B /\ Y e. B ) ) -> { <. O , X >. } : ( { E } X. { E } ) --> B )
28 2 fvexi 
 |-  B e. _V
29 28 a1i 
 |-  ( ( ( R e. Ring /\ E e. V ) /\ ( X e. B /\ Y e. B ) ) -> B e. _V )
30 snex 
 |-  { E } e. _V
31 30 30 xpex 
 |-  ( { E } X. { E } ) e. _V
32 31 a1i 
 |-  ( ( ( R e. Ring /\ E e. V ) /\ ( X e. B /\ Y e. B ) ) -> ( { E } X. { E } ) e. _V )
33 29 32 elmapd 
 |-  ( ( ( R e. Ring /\ E e. V ) /\ ( X e. B /\ Y e. B ) ) -> ( { <. O , X >. } e. ( B ^m ( { E } X. { E } ) ) <-> { <. O , X >. } : ( { E } X. { E } ) --> B ) )
34 27 33 mpbird 
 |-  ( ( ( R e. Ring /\ E e. V ) /\ ( X e. B /\ Y e. B ) ) -> { <. O , X >. } e. ( B ^m ( { E } X. { E } ) ) )
35 simpr 
 |-  ( ( X e. B /\ Y e. B ) -> Y e. B )
36 35 adantl 
 |-  ( ( ( R e. Ring /\ E e. V ) /\ ( X e. B /\ Y e. B ) ) -> Y e. B )
37 16 36 fsnd 
 |-  ( ( ( R e. Ring /\ E e. V ) /\ ( X e. B /\ Y e. B ) ) -> { <. <. E , E >. , Y >. } : { <. E , E >. } --> B )
38 3 opeq1i 
 |-  <. O , Y >. = <. <. E , E >. , Y >.
39 38 sneqi 
 |-  { <. O , Y >. } = { <. <. E , E >. , Y >. }
40 39 a1i 
 |-  ( E e. V -> { <. O , Y >. } = { <. <. E , E >. , Y >. } )
41 40 24 feq12d 
 |-  ( E e. V -> ( { <. O , Y >. } : ( { E } X. { E } ) --> B <-> { <. <. E , E >. , Y >. } : { <. E , E >. } --> B ) )
42 41 ad2antlr 
 |-  ( ( ( R e. Ring /\ E e. V ) /\ ( X e. B /\ Y e. B ) ) -> ( { <. O , Y >. } : ( { E } X. { E } ) --> B <-> { <. <. E , E >. , Y >. } : { <. E , E >. } --> B ) )
43 37 42 mpbird 
 |-  ( ( ( R e. Ring /\ E e. V ) /\ ( X e. B /\ Y e. B ) ) -> { <. O , Y >. } : ( { E } X. { E } ) --> B )
44 29 32 elmapd 
 |-  ( ( ( R e. Ring /\ E e. V ) /\ ( X e. B /\ Y e. B ) ) -> ( { <. O , Y >. } e. ( B ^m ( { E } X. { E } ) ) <-> { <. O , Y >. } : ( { E } X. { E } ) --> B ) )
45 43 44 mpbird 
 |-  ( ( ( R e. Ring /\ E e. V ) /\ ( X e. B /\ Y e. B ) ) -> { <. O , Y >. } e. ( B ^m ( { E } X. { E } ) ) )
46 6 2 12 13 14 14 14 34 45 mamuval 
 |-  ( ( ( R e. Ring /\ E e. V ) /\ ( X e. B /\ Y e. B ) ) -> ( { <. O , X >. } ( R maMul <. { E } , { E } , { E } >. ) { <. O , Y >. } ) = ( x e. { E } , y e. { E } |-> ( R gsum ( k e. { E } |-> ( ( x { <. O , X >. } k ) ( .r ` R ) ( k { <. O , Y >. } y ) ) ) ) ) )
47 simpr 
 |-  ( ( R e. Ring /\ E e. V ) -> E e. V )
48 47 adantr 
 |-  ( ( ( R e. Ring /\ E e. V ) /\ ( X e. B /\ Y e. B ) ) -> E e. V )
49 eqid 
 |-  ( Base ` R ) = ( Base ` R )
50 ringcmn 
 |-  ( R e. Ring -> R e. CMnd )
51 50 ad2antrr 
 |-  ( ( ( R e. Ring /\ E e. V ) /\ ( X e. B /\ Y e. B ) ) -> R e. CMnd )
52 df-ov 
 |-  ( E { <. O , X >. } E ) = ( { <. O , X >. } ` <. E , E >. )
53 21 fveq1i 
 |-  ( { <. O , X >. } ` <. E , E >. ) = ( { <. <. E , E >. , X >. } ` <. E , E >. )
54 52 53 eqtri 
 |-  ( E { <. O , X >. } E ) = ( { <. <. E , E >. , X >. } ` <. E , E >. )
55 15 a1i 
 |-  ( Y e. B -> <. E , E >. e. _V )
56 55 anim2i 
 |-  ( ( X e. B /\ Y e. B ) -> ( X e. B /\ <. E , E >. e. _V ) )
57 56 ancomd 
 |-  ( ( X e. B /\ Y e. B ) -> ( <. E , E >. e. _V /\ X e. B ) )
58 fvsng 
 |-  ( ( <. E , E >. e. _V /\ X e. B ) -> ( { <. <. E , E >. , X >. } ` <. E , E >. ) = X )
59 57 58 syl 
 |-  ( ( X e. B /\ Y e. B ) -> ( { <. <. E , E >. , X >. } ` <. E , E >. ) = X )
60 59 adantl 
 |-  ( ( ( R e. Ring /\ E e. V ) /\ ( X e. B /\ Y e. B ) ) -> ( { <. <. E , E >. , X >. } ` <. E , E >. ) = X )
61 54 60 syl5eq 
 |-  ( ( ( R e. Ring /\ E e. V ) /\ ( X e. B /\ Y e. B ) ) -> ( E { <. O , X >. } E ) = X )
62 61 18 eqeltrd 
 |-  ( ( ( R e. Ring /\ E e. V ) /\ ( X e. B /\ Y e. B ) ) -> ( E { <. O , X >. } E ) e. B )
63 df-ov 
 |-  ( E { <. O , Y >. } E ) = ( { <. O , Y >. } ` <. E , E >. )
64 39 fveq1i 
 |-  ( { <. O , Y >. } ` <. E , E >. ) = ( { <. <. E , E >. , Y >. } ` <. E , E >. )
65 63 64 eqtri 
 |-  ( E { <. O , Y >. } E ) = ( { <. <. E , E >. , Y >. } ` <. E , E >. )
66 15 a1i 
 |-  ( X e. B -> <. E , E >. e. _V )
67 fvsng 
 |-  ( ( <. E , E >. e. _V /\ Y e. B ) -> ( { <. <. E , E >. , Y >. } ` <. E , E >. ) = Y )
68 66 67 sylan 
 |-  ( ( X e. B /\ Y e. B ) -> ( { <. <. E , E >. , Y >. } ` <. E , E >. ) = Y )
69 68 adantl 
 |-  ( ( ( R e. Ring /\ E e. V ) /\ ( X e. B /\ Y e. B ) ) -> ( { <. <. E , E >. , Y >. } ` <. E , E >. ) = Y )
70 65 69 syl5eq 
 |-  ( ( ( R e. Ring /\ E e. V ) /\ ( X e. B /\ Y e. B ) ) -> ( E { <. O , Y >. } E ) = Y )
71 70 36 eqeltrd 
 |-  ( ( ( R e. Ring /\ E e. V ) /\ ( X e. B /\ Y e. B ) ) -> ( E { <. O , Y >. } E ) e. B )
72 2 12 ringcl 
 |-  ( ( R e. Ring /\ ( E { <. O , X >. } E ) e. B /\ ( E { <. O , Y >. } E ) e. B ) -> ( ( E { <. O , X >. } E ) ( .r ` R ) ( E { <. O , Y >. } E ) ) e. B )
73 13 62 71 72 syl3anc 
 |-  ( ( ( R e. Ring /\ E e. V ) /\ ( X e. B /\ Y e. B ) ) -> ( ( E { <. O , X >. } E ) ( .r ` R ) ( E { <. O , Y >. } E ) ) e. B )
74 oveq2 
 |-  ( k = E -> ( E { <. O , X >. } k ) = ( E { <. O , X >. } E ) )
75 oveq1 
 |-  ( k = E -> ( k { <. O , Y >. } E ) = ( E { <. O , Y >. } E ) )
76 74 75 oveq12d 
 |-  ( k = E -> ( ( E { <. O , X >. } k ) ( .r ` R ) ( k { <. O , Y >. } E ) ) = ( ( E { <. O , X >. } E ) ( .r ` R ) ( E { <. O , Y >. } E ) ) )
77 2 eqcomi 
 |-  ( Base ` R ) = B
78 77 a1i 
 |-  ( k = E -> ( Base ` R ) = B )
79 76 78 eleq12d 
 |-  ( k = E -> ( ( ( E { <. O , X >. } k ) ( .r ` R ) ( k { <. O , Y >. } E ) ) e. ( Base ` R ) <-> ( ( E { <. O , X >. } E ) ( .r ` R ) ( E { <. O , Y >. } E ) ) e. B ) )
80 79 ralsng 
 |-  ( E e. V -> ( A. k e. { E } ( ( E { <. O , X >. } k ) ( .r ` R ) ( k { <. O , Y >. } E ) ) e. ( Base ` R ) <-> ( ( E { <. O , X >. } E ) ( .r ` R ) ( E { <. O , Y >. } E ) ) e. B ) )
81 80 ad2antlr 
 |-  ( ( ( R e. Ring /\ E e. V ) /\ ( X e. B /\ Y e. B ) ) -> ( A. k e. { E } ( ( E { <. O , X >. } k ) ( .r ` R ) ( k { <. O , Y >. } E ) ) e. ( Base ` R ) <-> ( ( E { <. O , X >. } E ) ( .r ` R ) ( E { <. O , Y >. } E ) ) e. B ) )
82 73 81 mpbird 
 |-  ( ( ( R e. Ring /\ E e. V ) /\ ( X e. B /\ Y e. B ) ) -> A. k e. { E } ( ( E { <. O , X >. } k ) ( .r ` R ) ( k { <. O , Y >. } E ) ) e. ( Base ` R ) )
83 49 51 14 82 gsummptcl 
 |-  ( ( ( R e. Ring /\ E e. V ) /\ ( X e. B /\ Y e. B ) ) -> ( R gsum ( k e. { E } |-> ( ( E { <. O , X >. } k ) ( .r ` R ) ( k { <. O , Y >. } E ) ) ) ) e. ( Base ` R ) )
84 eqid 
 |-  ( x e. { E } , y e. { E } |-> ( R gsum ( k e. { E } |-> ( ( x { <. O , X >. } k ) ( .r ` R ) ( k { <. O , Y >. } y ) ) ) ) ) = ( x e. { E } , y e. { E } |-> ( R gsum ( k e. { E } |-> ( ( x { <. O , X >. } k ) ( .r ` R ) ( k { <. O , Y >. } y ) ) ) ) )
85 oveq1 
 |-  ( x = E -> ( x { <. O , X >. } k ) = ( E { <. O , X >. } k ) )
86 85 oveq1d 
 |-  ( x = E -> ( ( x { <. O , X >. } k ) ( .r ` R ) ( k { <. O , Y >. } y ) ) = ( ( E { <. O , X >. } k ) ( .r ` R ) ( k { <. O , Y >. } y ) ) )
87 86 mpteq2dv 
 |-  ( x = E -> ( k e. { E } |-> ( ( x { <. O , X >. } k ) ( .r ` R ) ( k { <. O , Y >. } y ) ) ) = ( k e. { E } |-> ( ( E { <. O , X >. } k ) ( .r ` R ) ( k { <. O , Y >. } y ) ) ) )
88 87 oveq2d 
 |-  ( x = E -> ( R gsum ( k e. { E } |-> ( ( x { <. O , X >. } k ) ( .r ` R ) ( k { <. O , Y >. } y ) ) ) ) = ( R gsum ( k e. { E } |-> ( ( E { <. O , X >. } k ) ( .r ` R ) ( k { <. O , Y >. } y ) ) ) ) )
89 oveq2 
 |-  ( y = E -> ( k { <. O , Y >. } y ) = ( k { <. O , Y >. } E ) )
90 89 oveq2d 
 |-  ( y = E -> ( ( E { <. O , X >. } k ) ( .r ` R ) ( k { <. O , Y >. } y ) ) = ( ( E { <. O , X >. } k ) ( .r ` R ) ( k { <. O , Y >. } E ) ) )
91 90 mpteq2dv 
 |-  ( y = E -> ( k e. { E } |-> ( ( E { <. O , X >. } k ) ( .r ` R ) ( k { <. O , Y >. } y ) ) ) = ( k e. { E } |-> ( ( E { <. O , X >. } k ) ( .r ` R ) ( k { <. O , Y >. } E ) ) ) )
92 91 oveq2d 
 |-  ( y = E -> ( R gsum ( k e. { E } |-> ( ( E { <. O , X >. } k ) ( .r ` R ) ( k { <. O , Y >. } y ) ) ) ) = ( R gsum ( k e. { E } |-> ( ( E { <. O , X >. } k ) ( .r ` R ) ( k { <. O , Y >. } E ) ) ) ) )
93 84 88 92 mposn 
 |-  ( ( E e. V /\ E e. V /\ ( R gsum ( k e. { E } |-> ( ( E { <. O , X >. } k ) ( .r ` R ) ( k { <. O , Y >. } E ) ) ) ) e. ( Base ` R ) ) -> ( x e. { E } , y e. { E } |-> ( R gsum ( k e. { E } |-> ( ( x { <. O , X >. } k ) ( .r ` R ) ( k { <. O , Y >. } y ) ) ) ) ) = { <. <. E , E >. , ( R gsum ( k e. { E } |-> ( ( E { <. O , X >. } k ) ( .r ` R ) ( k { <. O , Y >. } E ) ) ) ) >. } )
94 48 48 83 93 syl3anc 
 |-  ( ( ( R e. Ring /\ E e. V ) /\ ( X e. B /\ Y e. B ) ) -> ( x e. { E } , y e. { E } |-> ( R gsum ( k e. { E } |-> ( ( x { <. O , X >. } k ) ( .r ` R ) ( k { <. O , Y >. } y ) ) ) ) ) = { <. <. E , E >. , ( R gsum ( k e. { E } |-> ( ( E { <. O , X >. } k ) ( .r ` R ) ( k { <. O , Y >. } E ) ) ) ) >. } )
95 3 eqcomi 
 |-  <. E , E >. = O
96 95 a1i 
 |-  ( ( ( R e. Ring /\ E e. V ) /\ ( X e. B /\ Y e. B ) ) -> <. E , E >. = O )
97 ringmnd 
 |-  ( R e. Ring -> R e. Mnd )
98 97 ad2antrr 
 |-  ( ( ( R e. Ring /\ E e. V ) /\ ( X e. B /\ Y e. B ) ) -> R e. Mnd )
99 2 76 gsumsn 
 |-  ( ( R e. Mnd /\ E e. V /\ ( ( E { <. O , X >. } E ) ( .r ` R ) ( E { <. O , Y >. } E ) ) e. B ) -> ( R gsum ( k e. { E } |-> ( ( E { <. O , X >. } k ) ( .r ` R ) ( k { <. O , Y >. } E ) ) ) ) = ( ( E { <. O , X >. } E ) ( .r ` R ) ( E { <. O , Y >. } E ) ) )
100 98 48 73 99 syl3anc 
 |-  ( ( ( R e. Ring /\ E e. V ) /\ ( X e. B /\ Y e. B ) ) -> ( R gsum ( k e. { E } |-> ( ( E { <. O , X >. } k ) ( .r ` R ) ( k { <. O , Y >. } E ) ) ) ) = ( ( E { <. O , X >. } E ) ( .r ` R ) ( E { <. O , Y >. } E ) ) )
101 96 100 opeq12d 
 |-  ( ( ( R e. Ring /\ E e. V ) /\ ( X e. B /\ Y e. B ) ) -> <. <. E , E >. , ( R gsum ( k e. { E } |-> ( ( E { <. O , X >. } k ) ( .r ` R ) ( k { <. O , Y >. } E ) ) ) ) >. = <. O , ( ( E { <. O , X >. } E ) ( .r ` R ) ( E { <. O , Y >. } E ) ) >. )
102 101 sneqd 
 |-  ( ( ( R e. Ring /\ E e. V ) /\ ( X e. B /\ Y e. B ) ) -> { <. <. E , E >. , ( R gsum ( k e. { E } |-> ( ( E { <. O , X >. } k ) ( .r ` R ) ( k { <. O , Y >. } E ) ) ) ) >. } = { <. O , ( ( E { <. O , X >. } E ) ( .r ` R ) ( E { <. O , Y >. } E ) ) >. } )
103 61 70 oveq12d 
 |-  ( ( ( R e. Ring /\ E e. V ) /\ ( X e. B /\ Y e. B ) ) -> ( ( E { <. O , X >. } E ) ( .r ` R ) ( E { <. O , Y >. } E ) ) = ( X ( .r ` R ) Y ) )
104 103 opeq2d 
 |-  ( ( ( R e. Ring /\ E e. V ) /\ ( X e. B /\ Y e. B ) ) -> <. O , ( ( E { <. O , X >. } E ) ( .r ` R ) ( E { <. O , Y >. } E ) ) >. = <. O , ( X ( .r ` R ) Y ) >. )
105 104 sneqd 
 |-  ( ( ( R e. Ring /\ E e. V ) /\ ( X e. B /\ Y e. B ) ) -> { <. O , ( ( E { <. O , X >. } E ) ( .r ` R ) ( E { <. O , Y >. } E ) ) >. } = { <. O , ( X ( .r ` R ) Y ) >. } )
106 94 102 105 3eqtrd 
 |-  ( ( ( R e. Ring /\ E e. V ) /\ ( X e. B /\ Y e. B ) ) -> ( x e. { E } , y e. { E } |-> ( R gsum ( k e. { E } |-> ( ( x { <. O , X >. } k ) ( .r ` R ) ( k { <. O , Y >. } y ) ) ) ) ) = { <. O , ( X ( .r ` R ) Y ) >. } )
107 11 46 106 3eqtrd 
 |-  ( ( ( R e. Ring /\ E e. V ) /\ ( X e. B /\ Y e. B ) ) -> ( { <. O , X >. } ( .r ` A ) { <. O , Y >. } ) = { <. O , ( X ( .r ` R ) Y ) >. } )