Step |
Hyp |
Ref |
Expression |
1 |
|
mattposm.a |
|- A = ( N Mat R ) |
2 |
|
mattposm.b |
|- B = ( Base ` A ) |
3 |
|
mattposm.t |
|- .x. = ( .r ` A ) |
4 |
|
eqid |
|- ( R maMul <. N , N , N >. ) = ( R maMul <. N , N , N >. ) |
5 |
|
eqid |
|- ( Base ` R ) = ( Base ` R ) |
6 |
|
simp1 |
|- ( ( R e. CRing /\ X e. B /\ Y e. B ) -> R e. CRing ) |
7 |
1 2
|
matrcl |
|- ( Y e. B -> ( N e. Fin /\ R e. _V ) ) |
8 |
7
|
simpld |
|- ( Y e. B -> N e. Fin ) |
9 |
8
|
3ad2ant3 |
|- ( ( R e. CRing /\ X e. B /\ Y e. B ) -> N e. Fin ) |
10 |
1 5 2
|
matbas2i |
|- ( X e. B -> X e. ( ( Base ` R ) ^m ( N X. N ) ) ) |
11 |
10
|
3ad2ant2 |
|- ( ( R e. CRing /\ X e. B /\ Y e. B ) -> X e. ( ( Base ` R ) ^m ( N X. N ) ) ) |
12 |
1 5 2
|
matbas2i |
|- ( Y e. B -> Y e. ( ( Base ` R ) ^m ( N X. N ) ) ) |
13 |
12
|
3ad2ant3 |
|- ( ( R e. CRing /\ X e. B /\ Y e. B ) -> Y e. ( ( Base ` R ) ^m ( N X. N ) ) ) |
14 |
4 4 5 6 9 9 9 11 13
|
mamutpos |
|- ( ( R e. CRing /\ X e. B /\ Y e. B ) -> tpos ( X ( R maMul <. N , N , N >. ) Y ) = ( tpos Y ( R maMul <. N , N , N >. ) tpos X ) ) |
15 |
1 4
|
matmulr |
|- ( ( N e. Fin /\ R e. CRing ) -> ( R maMul <. N , N , N >. ) = ( .r ` A ) ) |
16 |
9 6 15
|
syl2anc |
|- ( ( R e. CRing /\ X e. B /\ Y e. B ) -> ( R maMul <. N , N , N >. ) = ( .r ` A ) ) |
17 |
3 16
|
eqtr4id |
|- ( ( R e. CRing /\ X e. B /\ Y e. B ) -> .x. = ( R maMul <. N , N , N >. ) ) |
18 |
17
|
oveqd |
|- ( ( R e. CRing /\ X e. B /\ Y e. B ) -> ( X .x. Y ) = ( X ( R maMul <. N , N , N >. ) Y ) ) |
19 |
18
|
tposeqd |
|- ( ( R e. CRing /\ X e. B /\ Y e. B ) -> tpos ( X .x. Y ) = tpos ( X ( R maMul <. N , N , N >. ) Y ) ) |
20 |
17
|
oveqd |
|- ( ( R e. CRing /\ X e. B /\ Y e. B ) -> ( tpos Y .x. tpos X ) = ( tpos Y ( R maMul <. N , N , N >. ) tpos X ) ) |
21 |
14 19 20
|
3eqtr4d |
|- ( ( R e. CRing /\ X e. B /\ Y e. B ) -> tpos ( X .x. Y ) = ( tpos Y .x. tpos X ) ) |