Users' Mathboxes Mathbox for Alexander van der Vekens < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  mat1dimmul Structured version   Unicode version

Theorem mat1dimmul 31037
Description: The ring multiplication in the algebra of matrices with dimension 1. (Contributed by AV, 16-Aug-2019.)
Hypotheses
Ref Expression
mat1dim.a  |-  A  =  ( { E } Mat  R )
mat1dim.b  |-  B  =  ( Base `  R
)
mat1dim.o  |-  O  = 
<. E ,  E >.
Assertion
Ref Expression
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 of Theorem mat1dimmul
Dummy variables  x  y  k are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 snfi 7499 . . . . . 6  |-  { E }  e.  Fin
21a1i 11 . . . . 5  |-  ( ( R  e.  Ring  /\  E  e.  V )  ->  { E }  e.  Fin )
3 simpl 457 . . . . 5  |-  ( ( R  e.  Ring  /\  E  e.  V )  ->  R  e.  Ring )
4 mat1dim.a . . . . . . 7  |-  A  =  ( { E } Mat  R )
5 eqid 2454 . . . . . . 7  |-  ( R maMul  <. { E } ,  { E } ,  { E } >. )  =  ( R maMul  <. { E } ,  { E } ,  { E } >. )
64, 5matmulr 18437 . . . . . 6  |-  ( ( { E }  e.  Fin  /\  R  e.  Ring )  ->  ( R maMul  <. { E } ,  { E } ,  { E } >. )  =  ( .r `  A ) )
76eqcomd 2462 . . . . 5  |-  ( ( { E }  e.  Fin  /\  R  e.  Ring )  ->  ( .r `  A )  =  ( R maMul  <. { E } ,  { E } ,  { E } >. )
)
82, 3, 7syl2anc 661 . . . 4  |-  ( ( R  e.  Ring  /\  E  e.  V )  ->  ( .r `  A )  =  ( R maMul  <. { E } ,  { E } ,  { E } >. ) )
98adantr 465 . . 3  |-  ( ( ( R  e.  Ring  /\  E  e.  V )  /\  ( X  e.  B  /\  Y  e.  B ) )  -> 
( .r `  A
)  =  ( R maMul  <. { E } ,  { E } ,  { E } >. ) )
109oveqd 6216 . 2  |-  ( ( ( 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 >. } ) )
11 mat1dim.b . . 3  |-  B  =  ( Base `  R
)
12 eqid 2454 . . 3  |-  ( .r
`  R )  =  ( .r `  R
)
133adantr 465 . . 3  |-  ( ( ( R  e.  Ring  /\  E  e.  V )  /\  ( X  e.  B  /\  Y  e.  B ) )  ->  R  e.  Ring )
141a1i 11 . . 3  |-  ( ( ( R  e.  Ring  /\  E  e.  V )  /\  ( X  e.  B  /\  Y  e.  B ) )  ->  { E }  e.  Fin )
15 opex 4663 . . . . . . . . 9  |-  <. E ,  E >.  e.  _V
1615a1i 11 . . . . . . . 8  |-  ( ( R  e.  Ring  /\  E  e.  V )  ->  <. E ,  E >.  e.  _V )
17 simpl 457 . . . . . . . 8  |-  ( ( X  e.  B  /\  Y  e.  B )  ->  X  e.  B )
18 f1osng 5786 . . . . . . . 8  |-  ( (
<. E ,  E >.  e. 
_V  /\  X  e.  B )  ->  { <. <. E ,  E >. ,  X >. } : { <. E ,  E >. } -1-1-onto-> { X } )
1916, 17, 18syl2an 477 . . . . . . 7  |-  ( ( ( R  e.  Ring  /\  E  e.  V )  /\  ( X  e.  B  /\  Y  e.  B ) )  ->  { <. <. E ,  E >. ,  X >. } : { <. E ,  E >. } -1-1-onto-> { X } )
20 f1of 5748 . . . . . . 7  |-  ( {
<. <. E ,  E >. ,  X >. } : { <. E ,  E >. } -1-1-onto-> { X }  ->  {
<. <. E ,  E >. ,  X >. } : { <. E ,  E >. } --> { X }
)
2119, 20syl 16 . . . . . 6  |-  ( ( ( R  e.  Ring  /\  E  e.  V )  /\  ( X  e.  B  /\  Y  e.  B ) )  ->  { <. <. E ,  E >. ,  X >. } : { <. E ,  E >. } --> { X }
)
22 mat1dim.o . . . . . . . . . 10  |-  O  = 
<. E ,  E >.
2322a1i 11 . . . . . . . . 9  |-  ( ( ( R  e.  Ring  /\  E  e.  V )  /\  ( X  e.  B  /\  Y  e.  B ) )  ->  O  =  <. E ,  E >. )
2423opeq1d 4172 . . . . . . . 8  |-  ( ( ( R  e.  Ring  /\  E  e.  V )  /\  ( X  e.  B  /\  Y  e.  B ) )  ->  <. O ,  X >.  = 
<. <. E ,  E >. ,  X >. )
2524sneqd 3996 . . . . . . 7  |-  ( ( ( R  e.  Ring  /\  E  e.  V )  /\  ( X  e.  B  /\  Y  e.  B ) )  ->  { <. O ,  X >. }  =  { <. <. E ,  E >. ,  X >. } )
26 simpr 461 . . . . . . . . 9  |-  ( ( R  e.  Ring  /\  E  e.  V )  ->  E  e.  V )
27 xpsng 5992 . . . . . . . . 9  |-  ( ( E  e.  V  /\  E  e.  V )  ->  ( { E }  X.  { E } )  =  { <. E ,  E >. } )
2826, 26, 27syl2anc 661 . . . . . . . 8  |-  ( ( R  e.  Ring  /\  E  e.  V )  ->  ( { E }  X.  { E } )  =  { <. E ,  E >. } )
2928adantr 465 . . . . . . 7  |-  ( ( ( R  e.  Ring  /\  E  e.  V )  /\  ( X  e.  B  /\  Y  e.  B ) )  -> 
( { E }  X.  { E } )  =  { <. E ,  E >. } )
3025, 29feq12d 5655 . . . . . 6  |-  ( ( ( R  e.  Ring  /\  E  e.  V )  /\  ( X  e.  B  /\  Y  e.  B ) )  -> 
( { <. O ,  X >. } : ( { E }  X.  { E } ) --> { X }  <->  { <. <. E ,  E >. ,  X >. } : { <. E ,  E >. } --> { X } ) )
3121, 30mpbird 232 . . . . 5  |-  ( ( ( R  e.  Ring  /\  E  e.  V )  /\  ( X  e.  B  /\  Y  e.  B ) )  ->  { <. O ,  X >. } : ( { E }  X.  { E } ) --> { X } )
32 snssi 4124 . . . . . . 7  |-  ( X  e.  B  ->  { X }  C_  B )
3332adantr 465 . . . . . 6  |-  ( ( X  e.  B  /\  Y  e.  B )  ->  { X }  C_  B )
3433adantl 466 . . . . 5  |-  ( ( ( R  e.  Ring  /\  E  e.  V )  /\  ( X  e.  B  /\  Y  e.  B ) )  ->  { X }  C_  B
)
35 fss 5674 . . . . 5  |-  ( ( { <. O ,  X >. } : ( { E }  X.  { E } ) --> { X }  /\  { X }  C_  B )  ->  { <. O ,  X >. } :
( { E }  X.  { E } ) --> B )
3631, 34, 35syl2anc 661 . . . 4  |-  ( ( ( R  e.  Ring  /\  E  e.  V )  /\  ( X  e.  B  /\  Y  e.  B ) )  ->  { <. O ,  X >. } : ( { E }  X.  { E } ) --> B )
37 fvex 5808 . . . . . . 7  |-  ( Base `  R )  e.  _V
3811, 37eqeltri 2538 . . . . . 6  |-  B  e. 
_V
3938a1i 11 . . . . 5  |-  ( ( ( R  e.  Ring  /\  E  e.  V )  /\  ( X  e.  B  /\  Y  e.  B ) )  ->  B  e.  _V )
40 snex 4640 . . . . . . 7  |-  { E }  e.  _V
4140, 40xpex 6617 . . . . . 6  |-  ( { E }  X.  { E } )  e.  _V
4241a1i 11 . . . . 5  |-  ( ( ( R  e.  Ring  /\  E  e.  V )  /\  ( X  e.  B  /\  Y  e.  B ) )  -> 
( { E }  X.  { E } )  e.  _V )
43 elmapg 7336 . . . . 5  |-  ( ( B  e.  _V  /\  ( { E }  X.  { E } )  e. 
_V )  ->  ( { <. O ,  X >. }  e.  ( B  ^m  ( { E }  X.  { E }
) )  <->  { <. O ,  X >. } : ( { E }  X.  { E } ) --> B ) )
4439, 42, 43syl2anc 661 . . . 4  |-  ( ( ( 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 ) )
4536, 44mpbird 232 . . 3  |-  ( ( ( R  e.  Ring  /\  E  e.  V )  /\  ( X  e.  B  /\  Y  e.  B ) )  ->  { <. O ,  X >. }  e.  ( B  ^m  ( { E }  X.  { E }
) ) )
46 simpr 461 . . . . . . . 8  |-  ( ( X  e.  B  /\  Y  e.  B )  ->  Y  e.  B )
47 f1osng 5786 . . . . . . . 8  |-  ( (
<. E ,  E >.  e. 
_V  /\  Y  e.  B )  ->  { <. <. E ,  E >. ,  Y >. } : { <. E ,  E >. } -1-1-onto-> { Y } )
4816, 46, 47syl2an 477 . . . . . . 7  |-  ( ( ( R  e.  Ring  /\  E  e.  V )  /\  ( X  e.  B  /\  Y  e.  B ) )  ->  { <. <. E ,  E >. ,  Y >. } : { <. E ,  E >. } -1-1-onto-> { Y } )
49 f1of 5748 . . . . . . 7  |-  ( {
<. <. E ,  E >. ,  Y >. } : { <. E ,  E >. } -1-1-onto-> { Y }  ->  {
<. <. E ,  E >. ,  Y >. } : { <. E ,  E >. } --> { Y }
)
5048, 49syl 16 . . . . . 6  |-  ( ( ( R  e.  Ring  /\  E  e.  V )  /\  ( X  e.  B  /\  Y  e.  B ) )  ->  { <. <. E ,  E >. ,  Y >. } : { <. E ,  E >. } --> { Y }
)
5123opeq1d 4172 . . . . . . . 8  |-  ( ( ( R  e.  Ring  /\  E  e.  V )  /\  ( X  e.  B  /\  Y  e.  B ) )  ->  <. O ,  Y >.  = 
<. <. E ,  E >. ,  Y >. )
5251sneqd 3996 . . . . . . 7  |-  ( ( ( R  e.  Ring  /\  E  e.  V )  /\  ( X  e.  B  /\  Y  e.  B ) )  ->  { <. O ,  Y >. }  =  { <. <. E ,  E >. ,  Y >. } )
5352, 29feq12d 5655 . . . . . 6  |-  ( ( ( R  e.  Ring  /\  E  e.  V )  /\  ( X  e.  B  /\  Y  e.  B ) )  -> 
( { <. O ,  Y >. } : ( { E }  X.  { E } ) --> { Y }  <->  { <. <. E ,  E >. ,  Y >. } : { <. E ,  E >. } --> { Y } ) )
5450, 53mpbird 232 . . . . 5  |-  ( ( ( R  e.  Ring  /\  E  e.  V )  /\  ( X  e.  B  /\  Y  e.  B ) )  ->  { <. O ,  Y >. } : ( { E }  X.  { E } ) --> { Y } )
55 snssi 4124 . . . . . . 7  |-  ( Y  e.  B  ->  { Y }  C_  B )
5655adantl 466 . . . . . 6  |-  ( ( X  e.  B  /\  Y  e.  B )  ->  { Y }  C_  B )
5756adantl 466 . . . . 5  |-  ( ( ( R  e.  Ring  /\  E  e.  V )  /\  ( X  e.  B  /\  Y  e.  B ) )  ->  { Y }  C_  B
)
58 fss 5674 . . . . 5  |-  ( ( { <. O ,  Y >. } : ( { E }  X.  { E } ) --> { Y }  /\  { Y }  C_  B )  ->  { <. O ,  Y >. } :
( { E }  X.  { E } ) --> B )
5954, 57, 58syl2anc 661 . . . 4  |-  ( ( ( R  e.  Ring  /\  E  e.  V )  /\  ( X  e.  B  /\  Y  e.  B ) )  ->  { <. O ,  Y >. } : ( { E }  X.  { E } ) --> B )
60 elmapg 7336 . . . . 5  |-  ( ( B  e.  _V  /\  ( { E }  X.  { E } )  e. 
_V )  ->  ( { <. O ,  Y >. }  e.  ( B  ^m  ( { E }  X.  { E }
) )  <->  { <. O ,  Y >. } : ( { E }  X.  { E } ) --> B ) )
6139, 42, 60syl2anc 661 . . . 4  |-  ( ( ( 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 ) )
6259, 61mpbird 232 . . 3  |-  ( ( ( R  e.  Ring  /\  E  e.  V )  /\  ( X  e.  B  /\  Y  e.  B ) )  ->  { <. O ,  Y >. }  e.  ( B  ^m  ( { E }  X.  { E }
) ) )
635, 11, 12, 13, 14, 14, 14, 45, 62mamuval 18408 . 2  |-  ( ( ( 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  gsumg  ( k  e.  { E }  |->  ( ( x { <. O ,  X >. } k ) ( .r
`  R ) ( k { <. O ,  Y >. } y ) ) ) ) ) )
6426adantr 465 . . . 4  |-  ( ( ( R  e.  Ring  /\  E  e.  V )  /\  ( X  e.  B  /\  Y  e.  B ) )  ->  E  e.  V )
65 eqid 2454 . . . . 5  |-  ( Base `  R )  =  (
Base `  R )
66 rngcmn 16797 . . . . . . 7  |-  ( R  e.  Ring  ->  R  e. CMnd
)
6766adantr 465 . . . . . 6  |-  ( ( R  e.  Ring  /\  E  e.  V )  ->  R  e. CMnd )
6867adantr 465 . . . . 5  |-  ( ( ( R  e.  Ring  /\  E  e.  V )  /\  ( X  e.  B  /\  Y  e.  B ) )  ->  R  e. CMnd )
69 df-ov 6202 . . . . . . . . . 10  |-  ( E { <. O ,  X >. } E )  =  ( { <. O ,  X >. } `  <. E ,  E >. )
7022opeq1i 4169 . . . . . . . . . . . 12  |-  <. O ,  X >.  =  <. <. E ,  E >. ,  X >.
7170sneqi 3995 . . . . . . . . . . 11  |-  { <. O ,  X >. }  =  { <. <. E ,  E >. ,  X >. }
7271fveq1i 5799 . . . . . . . . . 10  |-  ( {
<. O ,  X >. } `
 <. E ,  E >. )  =  ( {
<. <. E ,  E >. ,  X >. } `  <. E ,  E >. )
7369, 72eqtri 2483 . . . . . . . . 9  |-  ( E { <. O ,  X >. } E )  =  ( { <. <. E ,  E >. ,  X >. } `
 <. E ,  E >. )
7415a1i 11 . . . . . . . . . . . . 13  |-  ( Y  e.  B  ->  <. E ,  E >.  e.  _V )
7574anim2i 569 . . . . . . . . . . . 12  |-  ( ( X  e.  B  /\  Y  e.  B )  ->  ( X  e.  B  /\  <. E ,  E >.  e.  _V ) )
7675ancomd 451 . . . . . . . . . . 11  |-  ( ( X  e.  B  /\  Y  e.  B )  ->  ( <. E ,  E >.  e.  _V  /\  X  e.  B ) )
77 fvsng 6020 . . . . . . . . . . 11  |-  ( (
<. E ,  E >.  e. 
_V  /\  X  e.  B )  ->  ( { <. <. E ,  E >. ,  X >. } `  <. E ,  E >. )  =  X )
7876, 77syl 16 . . . . . . . . . 10  |-  ( ( X  e.  B  /\  Y  e.  B )  ->  ( { <. <. E ,  E >. ,  X >. } `
 <. E ,  E >. )  =  X )
7978adantl 466 . . . . . . . . 9  |-  ( ( ( R  e.  Ring  /\  E  e.  V )  /\  ( X  e.  B  /\  Y  e.  B ) )  -> 
( { <. <. E ,  E >. ,  X >. } `
 <. E ,  E >. )  =  X )
8073, 79syl5eq 2507 . . . . . . . 8  |-  ( ( ( R  e.  Ring  /\  E  e.  V )  /\  ( X  e.  B  /\  Y  e.  B ) )  -> 
( E { <. O ,  X >. } E
)  =  X )
8117adantl 466 . . . . . . . 8  |-  ( ( ( R  e.  Ring  /\  E  e.  V )  /\  ( X  e.  B  /\  Y  e.  B ) )  ->  X  e.  B )
8280, 81eqeltrd 2542 . . . . . . 7  |-  ( ( ( R  e.  Ring  /\  E  e.  V )  /\  ( X  e.  B  /\  Y  e.  B ) )  -> 
( E { <. O ,  X >. } E
)  e.  B )
83 df-ov 6202 . . . . . . . . . 10  |-  ( E { <. O ,  Y >. } E )  =  ( { <. O ,  Y >. } `  <. E ,  E >. )
8422opeq1i 4169 . . . . . . . . . . . 12  |-  <. O ,  Y >.  =  <. <. E ,  E >. ,  Y >.
8584sneqi 3995 . . . . . . . . . . 11  |-  { <. O ,  Y >. }  =  { <. <. E ,  E >. ,  Y >. }
8685fveq1i 5799 . . . . . . . . . 10  |-  ( {
<. O ,  Y >. } `
 <. E ,  E >. )  =  ( {
<. <. E ,  E >. ,  Y >. } `  <. E ,  E >. )
8783, 86eqtri 2483 . . . . . . . . 9  |-  ( E { <. O ,  Y >. } E )  =  ( { <. <. E ,  E >. ,  Y >. } `
 <. E ,  E >. )
8815a1i 11 . . . . . . . . . . 11  |-  ( X  e.  B  ->  <. E ,  E >.  e.  _V )
89 fvsng 6020 . . . . . . . . . . 11  |-  ( (
<. E ,  E >.  e. 
_V  /\  Y  e.  B )  ->  ( { <. <. E ,  E >. ,  Y >. } `  <. E ,  E >. )  =  Y )
9088, 89sylan 471 . . . . . . . . . 10  |-  ( ( X  e.  B  /\  Y  e.  B )  ->  ( { <. <. E ,  E >. ,  Y >. } `
 <. E ,  E >. )  =  Y )
9190adantl 466 . . . . . . . . 9  |-  ( ( ( R  e.  Ring  /\  E  e.  V )  /\  ( X  e.  B  /\  Y  e.  B ) )  -> 
( { <. <. E ,  E >. ,  Y >. } `
 <. E ,  E >. )  =  Y )
9287, 91syl5eq 2507 . . . . . . . 8  |-  ( ( ( R  e.  Ring  /\  E  e.  V )  /\  ( X  e.  B  /\  Y  e.  B ) )  -> 
( E { <. O ,  Y >. } E
)  =  Y )
9346adantl 466 . . . . . . . 8  |-  ( ( ( R  e.  Ring  /\  E  e.  V )  /\  ( X  e.  B  /\  Y  e.  B ) )  ->  Y  e.  B )
9492, 93eqeltrd 2542 . . . . . . 7  |-  ( ( ( R  e.  Ring  /\  E  e.  V )  /\  ( X  e.  B  /\  Y  e.  B ) )  -> 
( E { <. O ,  Y >. } E
)  e.  B )
9511, 12rngcl 16780 . . . . . . 7  |-  ( ( 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 )
9613, 82, 94, 95syl3anc 1219 . . . . . 6  |-  ( ( ( R  e.  Ring  /\  E  e.  V )  /\  ( X  e.  B  /\  Y  e.  B ) )  -> 
( ( E { <. O ,  X >. } E ) ( .r
`  R ) ( E { <. O ,  Y >. } E ) )  e.  B )
97 oveq2 6207 . . . . . . . . . . 11  |-  ( k  =  E  ->  ( E { <. O ,  X >. } k )  =  ( E { <. O ,  X >. } E
) )
98 oveq1 6206 . . . . . . . . . . 11  |-  ( k  =  E  ->  (
k { <. O ,  Y >. } E )  =  ( E { <. O ,  Y >. } E ) )
9997, 98oveq12d 6217 . . . . . . . . . 10  |-  ( k  =  E  ->  (
( E { <. O ,  X >. } k ) ( .r `  R ) ( k { <. O ,  Y >. } E ) )  =  ( ( E { <. O ,  X >. } E ) ( .r `  R ) ( E { <. O ,  Y >. } E
) ) )
10011eqcomi 2467 . . . . . . . . . . 11  |-  ( Base `  R )  =  B
101100a1i 11 . . . . . . . . . 10  |-  ( k  =  E  ->  ( Base `  R )  =  B )
10299, 101eleq12d 2536 . . . . . . . . 9  |-  ( 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
) )
103102ralsng 4019 . . . . . . . 8  |-  ( 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 ) )
104103adantl 466 . . . . . . 7  |-  ( ( R  e.  Ring  /\  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 ) )
105104adantr 465 . . . . . 6  |-  ( ( ( 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
) )
10696, 105mpbird 232 . . . . 5  |-  ( ( ( 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 )
)
10765, 68, 14, 106gsummptcl 16579 . . . 4  |-  ( ( ( R  e.  Ring  /\  E  e.  V )  /\  ( X  e.  B  /\  Y  e.  B ) )  -> 
( R  gsumg  ( k  e.  { E }  |->  ( ( E { <. O ,  X >. } k ) ( .r `  R
) ( k {
<. O ,  Y >. } E ) ) ) )  e.  ( Base `  R ) )
108 eqid 2454 . . . . 5  |-  ( x  e.  { E } ,  y  e.  { E }  |->  ( R  gsumg  ( k  e.  { E }  |->  ( ( x { <. O ,  X >. } k ) ( .r
`  R ) ( k { <. O ,  Y >. } y ) ) ) ) )  =  ( x  e. 
{ E } , 
y  e.  { E }  |->  ( R  gsumg  ( k  e.  { E }  |->  ( ( x { <. O ,  X >. } k ) ( .r
`  R ) ( k { <. O ,  Y >. } y ) ) ) ) )
109 oveq1 6206 . . . . . . . 8  |-  ( x  =  E  ->  (
x { <. O ,  X >. } k )  =  ( E { <. O ,  X >. } k ) )
110109oveq1d 6214 . . . . . . 7  |-  ( x  =  E  ->  (
( x { <. O ,  X >. } k ) ( .r `  R ) ( k { <. O ,  Y >. } y ) )  =  ( ( E { <. O ,  X >. } k ) ( .r `  R ) ( k { <. O ,  Y >. } y ) ) )
111110mpteq2dv 4486 . . . . . 6  |-  ( 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 ) ) ) )
112111oveq2d 6215 . . . . 5  |-  ( x  =  E  ->  ( R  gsumg  ( k  e.  { E }  |->  ( ( x { <. O ,  X >. } k ) ( .r `  R
) ( k {
<. O ,  Y >. } y ) ) ) )  =  ( R 
gsumg  ( k  e.  { E }  |->  ( ( E { <. O ,  X >. } k ) ( .r `  R
) ( k {
<. O ,  Y >. } y ) ) ) ) )
113 oveq2 6207 . . . . . . . 8  |-  ( y  =  E  ->  (
k { <. O ,  Y >. } y )  =  ( k {
<. O ,  Y >. } E ) )
114113oveq2d 6215 . . . . . . 7  |-  ( y  =  E  ->  (
( E { <. O ,  X >. } k ) ( .r `  R ) ( k { <. O ,  Y >. } y ) )  =  ( ( E { <. O ,  X >. } k ) ( .r `  R ) ( k { <. O ,  Y >. } E
) ) )
115114mpteq2dv 4486 . . . . . 6  |-  ( 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 ) ) ) )
116115oveq2d 6215 . . . . 5  |-  ( y  =  E  ->  ( R  gsumg  ( k  e.  { E }  |->  ( ( E { <. O ,  X >. } k ) ( .r `  R
) ( k {
<. O ,  Y >. } y ) ) ) )  =  ( R 
gsumg  ( k  e.  { E }  |->  ( ( E { <. O ,  X >. } k ) ( .r `  R
) ( k {
<. O ,  Y >. } E ) ) ) ) )
117108, 112, 116mpt2sn 30870 . . . 4  |-  ( ( E  e.  V  /\  E  e.  V  /\  ( R  gsumg  ( k  e.  { E }  |->  ( ( E { <. O ,  X >. } k ) ( .r `  R
) ( k {
<. O ,  Y >. } E ) ) ) )  e.  ( Base `  R ) )  -> 
( x  e.  { E } ,  y  e. 
{ E }  |->  ( R  gsumg  ( k  e.  { E }  |->  ( ( x { <. O ,  X >. } k ) ( .r `  R
) ( k {
<. O ,  Y >. } y ) ) ) ) )  =  { <. <. E ,  E >. ,  ( R  gsumg  ( k  e.  { E }  |->  ( ( E { <. O ,  X >. } k ) ( .r
`  R ) ( k { <. O ,  Y >. } E ) ) ) ) >. } )
11864, 64, 107, 117syl3anc 1219 . . 3  |-  ( ( ( R  e.  Ring  /\  E  e.  V )  /\  ( X  e.  B  /\  Y  e.  B ) )  -> 
( x  e.  { E } ,  y  e. 
{ E }  |->  ( R  gsumg  ( k  e.  { E }  |->  ( ( x { <. O ,  X >. } k ) ( .r `  R
) ( k {
<. O ,  Y >. } y ) ) ) ) )  =  { <. <. E ,  E >. ,  ( R  gsumg  ( k  e.  { E }  |->  ( ( E { <. O ,  X >. } k ) ( .r
`  R ) ( k { <. O ,  Y >. } E ) ) ) ) >. } )
11922eqcomi 2467 . . . . . 6  |-  <. E ,  E >.  =  O
120119a1i 11 . . . . 5  |-  ( ( ( R  e.  Ring  /\  E  e.  V )  /\  ( X  e.  B  /\  Y  e.  B ) )  ->  <. E ,  E >.  =  O )
121 rngmnd 16776 . . . . . . . 8  |-  ( R  e.  Ring  ->  R  e. 
Mnd )
122121adantr 465 . . . . . . 7  |-  ( ( R  e.  Ring  /\  E  e.  V )  ->  R  e.  Mnd )
123122adantr 465 . . . . . 6  |-  ( ( ( R  e.  Ring  /\  E  e.  V )  /\  ( X  e.  B  /\  Y  e.  B ) )  ->  R  e.  Mnd )
12411, 99gsumsn 16570 . . . . . 6  |-  ( ( R  e.  Mnd  /\  E  e.  V  /\  ( ( E { <. O ,  X >. } E ) ( .r
`  R ) ( E { <. O ,  Y >. } E ) )  e.  B )  ->  ( R  gsumg  ( k  e.  { E }  |->  ( ( E { <. O ,  X >. } k ) ( .r
`  R ) ( k { <. O ,  Y >. } E ) ) ) )  =  ( ( E { <. O ,  X >. } E ) ( .r
`  R ) ( E { <. O ,  Y >. } E ) ) )
125123, 64, 96, 124syl3anc 1219 . . . . 5  |-  ( ( ( R  e.  Ring  /\  E  e.  V )  /\  ( X  e.  B  /\  Y  e.  B ) )  -> 
( R  gsumg  ( k  e.  { E }  |->  ( ( E { <. O ,  X >. } k ) ( .r `  R
) ( k {
<. O ,  Y >. } E ) ) ) )  =  ( ( E { <. O ,  X >. } E ) ( .r `  R
) ( E { <. O ,  Y >. } E ) ) )
126120, 125opeq12d 4174 . . . 4  |-  ( ( ( R  e.  Ring  /\  E  e.  V )  /\  ( X  e.  B  /\  Y  e.  B ) )  ->  <. <. E ,  E >. ,  ( R  gsumg  ( k  e.  { E }  |->  ( ( E { <. O ,  X >. } k ) ( .r
`  R ) ( k { <. O ,  Y >. } E ) ) ) ) >.  =  <. O ,  ( ( E { <. O ,  X >. } E
) ( .r `  R ) ( E { <. O ,  Y >. } E ) )
>. )
127126sneqd 3996 . . 3  |-  ( ( ( R  e.  Ring  /\  E  e.  V )  /\  ( X  e.  B  /\  Y  e.  B ) )  ->  { <. <. E ,  E >. ,  ( R  gsumg  ( k  e.  { E }  |->  ( ( E { <. O ,  X >. } k ) ( .r
`  R ) ( k { <. O ,  Y >. } E ) ) ) ) >. }  =  { <. O , 
( ( E { <. O ,  X >. } E ) ( .r
`  R ) ( E { <. O ,  Y >. } E ) ) >. } )
12880, 92oveq12d 6217 . . . . 5  |-  ( ( ( 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 ) )
129128opeq2d 4173 . . . 4  |-  ( ( ( 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 )
>. )
130129sneqd 3996 . . 3  |-  ( ( ( 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 ) >. } )
131118, 127, 1303eqtrd 2499 . 2  |-  ( ( ( R  e.  Ring  /\  E  e.  V )  /\  ( X  e.  B  /\  Y  e.  B ) )  -> 
( x  e.  { E } ,  y  e. 
{ E }  |->  ( R  gsumg  ( k  e.  { E }  |->  ( ( x { <. O ,  X >. } k ) ( .r `  R
) ( k {
<. O ,  Y >. } y ) ) ) ) )  =  { <. O ,  ( X ( .r `  R
) Y ) >. } )
13210, 63, 1313eqtrd 2499 1  |-  ( ( ( R  e.  Ring  /\  E  e.  V )  /\  ( X  e.  B  /\  Y  e.  B ) )  -> 
( { <. O ,  X >. }  ( .r
`  A ) {
<. O ,  Y >. } )  =  { <. O ,  ( X ( .r `  R ) Y ) >. } )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184    /\ wa 369    = wceq 1370    e. wcel 1758   A.wral 2798   _Vcvv 3076    C_ wss 3435   {csn 3984   <.cop 3990   <.cotp 3992    |-> cmpt 4457    X. cxp 4945   -->wf 5521   -1-1-onto->wf1o 5524   ` cfv 5525  (class class class)co 6199    |-> cmpt2 6201    ^m cmap 7323   Fincfn 7419   Basecbs 14291   .rcmulr 14357    gsumg cgsu 14497   Mndcmnd 15527  CMndccmn 16397   Ringcrg 16767   maMul cmmul 18403   Mat cmat 18404
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-8 1760  ax-9 1762  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1955  ax-ext 2432  ax-rep 4510  ax-sep 4520  ax-nul 4528  ax-pow 4577  ax-pr 4638  ax-un 6481  ax-inf2 7957  ax-cnex 9448  ax-resscn 9449  ax-1cn 9450  ax-icn 9451  ax-addcl 9452  ax-addrcl 9453  ax-mulcl 9454  ax-mulrcl 9455  ax-mulcom 9456  ax-addass 9457  ax-mulass 9458  ax-distr 9459  ax-i2m1 9460  ax-1ne0 9461  ax-1rid 9462  ax-rnegex 9463  ax-rrecex 9464  ax-cnre 9465  ax-pre-lttri 9466  ax-pre-lttrn 9467  ax-pre-ltadd 9468  ax-pre-mulgt0 9469
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 966  df-3an 967  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-eu 2266  df-mo 2267  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-ne 2649  df-nel 2650  df-ral 2803  df-rex 2804  df-reu 2805  df-rmo 2806  df-rab 2807  df-v 3078  df-sbc 3293  df-csb 3395  df-dif 3438  df-un 3440  df-in 3442  df-ss 3449  df-pss 3451  df-nul 3745  df-if 3899  df-pw 3969  df-sn 3985  df-pr 3987  df-tp 3989  df-op 3991  df-ot 3993  df-uni 4199  df-int 4236  df-iun 4280  df-br 4400  df-opab 4458  df-mpt 4459  df-tr 4493  df-eprel 4739  df-id 4743  df-po 4748  df-so 4749  df-fr 4786  df-se 4787  df-we 4788  df-ord 4829  df-on 4830  df-lim 4831  df-suc 4832  df-xp 4953  df-rel 4954  df-cnv 4955  df-co 4956  df-dm 4957  df-rn 4958  df-res 4959  df-ima 4960  df-iota 5488  df-fun 5527  df-fn 5528  df-f 5529  df-f1 5530  df-fo 5531  df-f1o 5532  df-fv 5533  df-isom 5534  df-riota 6160  df-ov 6202  df-oprab 6203  df-mpt2 6204  df-om 6586  df-1st 6686  df-2nd 6687  df-supp 6800  df-recs 6941  df-rdg 6975  df-1o 7029  df-oadd 7033  df-er 7210  df-map 7325  df-en 7420  df-dom 7421  df-sdom 7422  df-fin 7423  df-fsupp 7731  df-oi 7834  df-card 8219  df-pnf 9530  df-mnf 9531  df-xr 9532  df-ltxr 9533  df-le 9534  df-sub 9707  df-neg 9708  df-nn 10433  df-2 10490  df-3 10491  df-n0 10690  df-z 10757  df-uz 10972  df-fz 11554  df-fzo 11665  df-seq 11923  df-hash 12220  df-ndx 14294  df-slot 14295  df-base 14296  df-sets 14297  df-plusg 14369  df-mulr 14370  df-0g 14498  df-gsum 14499  df-mnd 15533  df-grp 15663  df-minusg 15664  df-mulg 15666  df-cntz 15953  df-cmn 16399  df-abl 16400  df-mgp 16713  df-ur 16725  df-rng 16769  df-mamu 18405  df-mat 18406
This theorem is referenced by:  mat1dimcrng  31038
  Copyright terms: Public domain W3C validator