Step |
Hyp |
Ref |
Expression |
1 |
|
mattposvs.a |
|- A = ( N Mat R ) |
2 |
|
mattposvs.b |
|- B = ( Base ` A ) |
3 |
|
mattposvs.k |
|- K = ( Base ` R ) |
4 |
|
mattposvs.v |
|- .x. = ( .s ` A ) |
5 |
1 2
|
matrcl |
|- ( Y e. B -> ( N e. Fin /\ R e. _V ) ) |
6 |
5
|
simpld |
|- ( Y e. B -> N e. Fin ) |
7 |
|
sqxpexg |
|- ( N e. Fin -> ( N X. N ) e. _V ) |
8 |
6 7
|
syl |
|- ( Y e. B -> ( N X. N ) e. _V ) |
9 |
|
snex |
|- { X } e. _V |
10 |
|
xpexg |
|- ( ( ( N X. N ) e. _V /\ { X } e. _V ) -> ( ( N X. N ) X. { X } ) e. _V ) |
11 |
8 9 10
|
sylancl |
|- ( Y e. B -> ( ( N X. N ) X. { X } ) e. _V ) |
12 |
|
oftpos |
|- ( ( ( ( N X. N ) X. { X } ) e. _V /\ Y e. B ) -> tpos ( ( ( N X. N ) X. { X } ) oF ( .r ` R ) Y ) = ( tpos ( ( N X. N ) X. { X } ) oF ( .r ` R ) tpos Y ) ) |
13 |
11 12
|
mpancom |
|- ( Y e. B -> tpos ( ( ( N X. N ) X. { X } ) oF ( .r ` R ) Y ) = ( tpos ( ( N X. N ) X. { X } ) oF ( .r ` R ) tpos Y ) ) |
14 |
|
tposconst |
|- tpos ( ( N X. N ) X. { X } ) = ( ( N X. N ) X. { X } ) |
15 |
14
|
oveq1i |
|- ( tpos ( ( N X. N ) X. { X } ) oF ( .r ` R ) tpos Y ) = ( ( ( N X. N ) X. { X } ) oF ( .r ` R ) tpos Y ) |
16 |
13 15
|
eqtrdi |
|- ( Y e. B -> tpos ( ( ( N X. N ) X. { X } ) oF ( .r ` R ) Y ) = ( ( ( N X. N ) X. { X } ) oF ( .r ` R ) tpos Y ) ) |
17 |
16
|
adantl |
|- ( ( X e. K /\ Y e. B ) -> tpos ( ( ( N X. N ) X. { X } ) oF ( .r ` R ) Y ) = ( ( ( N X. N ) X. { X } ) oF ( .r ` R ) tpos Y ) ) |
18 |
|
eqid |
|- ( .r ` R ) = ( .r ` R ) |
19 |
|
eqid |
|- ( N X. N ) = ( N X. N ) |
20 |
1 2 3 4 18 19
|
matvsca2 |
|- ( ( X e. K /\ Y e. B ) -> ( X .x. Y ) = ( ( ( N X. N ) X. { X } ) oF ( .r ` R ) Y ) ) |
21 |
20
|
tposeqd |
|- ( ( X e. K /\ Y e. B ) -> tpos ( X .x. Y ) = tpos ( ( ( N X. N ) X. { X } ) oF ( .r ` R ) Y ) ) |
22 |
1 2
|
mattposcl |
|- ( Y e. B -> tpos Y e. B ) |
23 |
1 2 3 4 18 19
|
matvsca2 |
|- ( ( X e. K /\ tpos Y e. B ) -> ( X .x. tpos Y ) = ( ( ( N X. N ) X. { X } ) oF ( .r ` R ) tpos Y ) ) |
24 |
22 23
|
sylan2 |
|- ( ( X e. K /\ Y e. B ) -> ( X .x. tpos Y ) = ( ( ( N X. N ) X. { X } ) oF ( .r ` R ) tpos Y ) ) |
25 |
17 21 24
|
3eqtr4d |
|- ( ( X e. K /\ Y e. B ) -> tpos ( X .x. Y ) = ( X .x. tpos Y ) ) |