Step |
Hyp |
Ref |
Expression |
1 |
|
lmod1.m |
|- M = ( { <. ( Base ` ndx ) , { I } >. , <. ( +g ` ndx ) , { <. <. I , I >. , I >. } >. , <. ( Scalar ` ndx ) , R >. } u. { <. ( .s ` ndx ) , ( x e. ( Base ` R ) , y e. { I } |-> y ) >. } ) |
2 |
|
fvex |
|- ( Base ` R ) e. _V |
3 |
|
snex |
|- { I } e. _V |
4 |
2 3
|
pm3.2i |
|- ( ( Base ` R ) e. _V /\ { I } e. _V ) |
5 |
4
|
a1i |
|- ( ( ( I e. V /\ R e. Ring ) /\ ( q e. ( Base ` R ) /\ r e. ( Base ` R ) ) ) -> ( ( Base ` R ) e. _V /\ { I } e. _V ) ) |
6 |
|
mpoexga |
|- ( ( ( Base ` R ) e. _V /\ { I } e. _V ) -> ( x e. ( Base ` R ) , y e. { I } |-> y ) e. _V ) |
7 |
1
|
lmodvsca |
|- ( ( x e. ( Base ` R ) , y e. { I } |-> y ) e. _V -> ( x e. ( Base ` R ) , y e. { I } |-> y ) = ( .s ` M ) ) |
8 |
5 6 7
|
3syl |
|- ( ( ( I e. V /\ R e. Ring ) /\ ( q e. ( Base ` R ) /\ r e. ( Base ` R ) ) ) -> ( x e. ( Base ` R ) , y e. { I } |-> y ) = ( .s ` M ) ) |
9 |
8
|
eqcomd |
|- ( ( ( I e. V /\ R e. Ring ) /\ ( q e. ( Base ` R ) /\ r e. ( Base ` R ) ) ) -> ( .s ` M ) = ( x e. ( Base ` R ) , y e. { I } |-> y ) ) |
10 |
|
simprr |
|- ( ( ( ( I e. V /\ R e. Ring ) /\ ( q e. ( Base ` R ) /\ r e. ( Base ` R ) ) ) /\ ( x = q /\ y = I ) ) -> y = I ) |
11 |
|
simprl |
|- ( ( ( I e. V /\ R e. Ring ) /\ ( q e. ( Base ` R ) /\ r e. ( Base ` R ) ) ) -> q e. ( Base ` R ) ) |
12 |
|
snidg |
|- ( I e. V -> I e. { I } ) |
13 |
12
|
ad2antrr |
|- ( ( ( I e. V /\ R e. Ring ) /\ ( q e. ( Base ` R ) /\ r e. ( Base ` R ) ) ) -> I e. { I } ) |
14 |
9 10 11 13 13
|
ovmpod |
|- ( ( ( I e. V /\ R e. Ring ) /\ ( q e. ( Base ` R ) /\ r e. ( Base ` R ) ) ) -> ( q ( .s ` M ) I ) = I ) |
15 |
|
simprr |
|- ( ( ( ( I e. V /\ R e. Ring ) /\ ( q e. ( Base ` R ) /\ r e. ( Base ` R ) ) ) /\ ( x = r /\ y = I ) ) -> y = I ) |
16 |
|
simprr |
|- ( ( ( I e. V /\ R e. Ring ) /\ ( q e. ( Base ` R ) /\ r e. ( Base ` R ) ) ) -> r e. ( Base ` R ) ) |
17 |
9 15 16 13 13
|
ovmpod |
|- ( ( ( I e. V /\ R e. Ring ) /\ ( q e. ( Base ` R ) /\ r e. ( Base ` R ) ) ) -> ( r ( .s ` M ) I ) = I ) |
18 |
17
|
oveq2d |
|- ( ( ( I e. V /\ R e. Ring ) /\ ( q e. ( Base ` R ) /\ r e. ( Base ` R ) ) ) -> ( q ( .s ` M ) ( r ( .s ` M ) I ) ) = ( q ( .s ` M ) I ) ) |
19 |
|
simprr |
|- ( ( ( ( I e. V /\ R e. Ring ) /\ ( q e. ( Base ` R ) /\ r e. ( Base ` R ) ) ) /\ ( x = ( q ( .r ` ( Scalar ` M ) ) r ) /\ y = I ) ) -> y = I ) |
20 |
|
simplr |
|- ( ( ( I e. V /\ R e. Ring ) /\ ( q e. ( Base ` R ) /\ r e. ( Base ` R ) ) ) -> R e. Ring ) |
21 |
1
|
lmodsca |
|- ( R e. Ring -> R = ( Scalar ` M ) ) |
22 |
21
|
fveq2d |
|- ( R e. Ring -> ( .r ` R ) = ( .r ` ( Scalar ` M ) ) ) |
23 |
20 22
|
syl |
|- ( ( ( I e. V /\ R e. Ring ) /\ ( q e. ( Base ` R ) /\ r e. ( Base ` R ) ) ) -> ( .r ` R ) = ( .r ` ( Scalar ` M ) ) ) |
24 |
23
|
eqcomd |
|- ( ( ( I e. V /\ R e. Ring ) /\ ( q e. ( Base ` R ) /\ r e. ( Base ` R ) ) ) -> ( .r ` ( Scalar ` M ) ) = ( .r ` R ) ) |
25 |
24
|
oveqd |
|- ( ( ( I e. V /\ R e. Ring ) /\ ( q e. ( Base ` R ) /\ r e. ( Base ` R ) ) ) -> ( q ( .r ` ( Scalar ` M ) ) r ) = ( q ( .r ` R ) r ) ) |
26 |
|
eqid |
|- ( Base ` R ) = ( Base ` R ) |
27 |
|
eqid |
|- ( .r ` R ) = ( .r ` R ) |
28 |
26 27
|
ringcl |
|- ( ( R e. Ring /\ q e. ( Base ` R ) /\ r e. ( Base ` R ) ) -> ( q ( .r ` R ) r ) e. ( Base ` R ) ) |
29 |
20 11 16 28
|
syl3anc |
|- ( ( ( I e. V /\ R e. Ring ) /\ ( q e. ( Base ` R ) /\ r e. ( Base ` R ) ) ) -> ( q ( .r ` R ) r ) e. ( Base ` R ) ) |
30 |
25 29
|
eqeltrd |
|- ( ( ( I e. V /\ R e. Ring ) /\ ( q e. ( Base ` R ) /\ r e. ( Base ` R ) ) ) -> ( q ( .r ` ( Scalar ` M ) ) r ) e. ( Base ` R ) ) |
31 |
9 19 30 13 13
|
ovmpod |
|- ( ( ( I e. V /\ R e. Ring ) /\ ( q e. ( Base ` R ) /\ r e. ( Base ` R ) ) ) -> ( ( q ( .r ` ( Scalar ` M ) ) r ) ( .s ` M ) I ) = I ) |
32 |
14 18 31
|
3eqtr4rd |
|- ( ( ( I e. V /\ R e. Ring ) /\ ( q e. ( Base ` R ) /\ r e. ( Base ` R ) ) ) -> ( ( q ( .r ` ( Scalar ` M ) ) r ) ( .s ` M ) I ) = ( q ( .s ` M ) ( r ( .s ` M ) I ) ) ) |