Step |
Hyp |
Ref |
Expression |
1 |
|
cayhamlem2.k |
|- K = ( Base ` R ) |
2 |
|
cayhamlem2.a |
|- A = ( N Mat R ) |
3 |
|
cayhamlem2.b |
|- B = ( Base ` A ) |
4 |
|
cayhamlem2.1 |
|- .1. = ( 1r ` A ) |
5 |
|
cayhamlem2.m |
|- .* = ( .s ` A ) |
6 |
|
cayhamlem2.e |
|- .^ = ( .g ` ( mulGrp ` A ) ) |
7 |
|
cayhamlem2.r |
|- .x. = ( .r ` A ) |
8 |
|
elmapi |
|- ( H e. ( K ^m NN0 ) -> H : NN0 --> K ) |
9 |
8
|
ffvelrnda |
|- ( ( H e. ( K ^m NN0 ) /\ L e. NN0 ) -> ( H ` L ) e. K ) |
10 |
9
|
adantl |
|- ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( H e. ( K ^m NN0 ) /\ L e. NN0 ) ) -> ( H ` L ) e. K ) |
11 |
2
|
matsca2 |
|- ( ( N e. Fin /\ R e. CRing ) -> R = ( Scalar ` A ) ) |
12 |
11
|
3adant3 |
|- ( ( N e. Fin /\ R e. CRing /\ M e. B ) -> R = ( Scalar ` A ) ) |
13 |
12
|
fveq2d |
|- ( ( N e. Fin /\ R e. CRing /\ M e. B ) -> ( Base ` R ) = ( Base ` ( Scalar ` A ) ) ) |
14 |
1 13
|
syl5req |
|- ( ( N e. Fin /\ R e. CRing /\ M e. B ) -> ( Base ` ( Scalar ` A ) ) = K ) |
15 |
14
|
eleq2d |
|- ( ( N e. Fin /\ R e. CRing /\ M e. B ) -> ( ( H ` L ) e. ( Base ` ( Scalar ` A ) ) <-> ( H ` L ) e. K ) ) |
16 |
15
|
adantr |
|- ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( H e. ( K ^m NN0 ) /\ L e. NN0 ) ) -> ( ( H ` L ) e. ( Base ` ( Scalar ` A ) ) <-> ( H ` L ) e. K ) ) |
17 |
10 16
|
mpbird |
|- ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( H e. ( K ^m NN0 ) /\ L e. NN0 ) ) -> ( H ` L ) e. ( Base ` ( Scalar ` A ) ) ) |
18 |
|
eqid |
|- ( algSc ` A ) = ( algSc ` A ) |
19 |
|
eqid |
|- ( Scalar ` A ) = ( Scalar ` A ) |
20 |
|
eqid |
|- ( Base ` ( Scalar ` A ) ) = ( Base ` ( Scalar ` A ) ) |
21 |
18 19 20 5 4
|
asclval |
|- ( ( H ` L ) e. ( Base ` ( Scalar ` A ) ) -> ( ( algSc ` A ) ` ( H ` L ) ) = ( ( H ` L ) .* .1. ) ) |
22 |
17 21
|
syl |
|- ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( H e. ( K ^m NN0 ) /\ L e. NN0 ) ) -> ( ( algSc ` A ) ` ( H ` L ) ) = ( ( H ` L ) .* .1. ) ) |
23 |
22
|
eqcomd |
|- ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( H e. ( K ^m NN0 ) /\ L e. NN0 ) ) -> ( ( H ` L ) .* .1. ) = ( ( algSc ` A ) ` ( H ` L ) ) ) |
24 |
23
|
oveq2d |
|- ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( H e. ( K ^m NN0 ) /\ L e. NN0 ) ) -> ( ( L .^ M ) .x. ( ( H ` L ) .* .1. ) ) = ( ( L .^ M ) .x. ( ( algSc ` A ) ` ( H ` L ) ) ) ) |
25 |
2
|
matassa |
|- ( ( N e. Fin /\ R e. CRing ) -> A e. AssAlg ) |
26 |
25
|
3adant3 |
|- ( ( N e. Fin /\ R e. CRing /\ M e. B ) -> A e. AssAlg ) |
27 |
26
|
adantr |
|- ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( H e. ( K ^m NN0 ) /\ L e. NN0 ) ) -> A e. AssAlg ) |
28 |
|
crngring |
|- ( R e. CRing -> R e. Ring ) |
29 |
28
|
anim2i |
|- ( ( N e. Fin /\ R e. CRing ) -> ( N e. Fin /\ R e. Ring ) ) |
30 |
29
|
3adant3 |
|- ( ( N e. Fin /\ R e. CRing /\ M e. B ) -> ( N e. Fin /\ R e. Ring ) ) |
31 |
2
|
matring |
|- ( ( N e. Fin /\ R e. Ring ) -> A e. Ring ) |
32 |
|
eqid |
|- ( mulGrp ` A ) = ( mulGrp ` A ) |
33 |
32
|
ringmgp |
|- ( A e. Ring -> ( mulGrp ` A ) e. Mnd ) |
34 |
30 31 33
|
3syl |
|- ( ( N e. Fin /\ R e. CRing /\ M e. B ) -> ( mulGrp ` A ) e. Mnd ) |
35 |
34
|
adantr |
|- ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( H e. ( K ^m NN0 ) /\ L e. NN0 ) ) -> ( mulGrp ` A ) e. Mnd ) |
36 |
|
simprr |
|- ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( H e. ( K ^m NN0 ) /\ L e. NN0 ) ) -> L e. NN0 ) |
37 |
|
simpl3 |
|- ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( H e. ( K ^m NN0 ) /\ L e. NN0 ) ) -> M e. B ) |
38 |
32 3
|
mgpbas |
|- B = ( Base ` ( mulGrp ` A ) ) |
39 |
38 6
|
mulgnn0cl |
|- ( ( ( mulGrp ` A ) e. Mnd /\ L e. NN0 /\ M e. B ) -> ( L .^ M ) e. B ) |
40 |
35 36 37 39
|
syl3anc |
|- ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( H e. ( K ^m NN0 ) /\ L e. NN0 ) ) -> ( L .^ M ) e. B ) |
41 |
18 19 20 3 7 5
|
asclmul2 |
|- ( ( A e. AssAlg /\ ( H ` L ) e. ( Base ` ( Scalar ` A ) ) /\ ( L .^ M ) e. B ) -> ( ( L .^ M ) .x. ( ( algSc ` A ) ` ( H ` L ) ) ) = ( ( H ` L ) .* ( L .^ M ) ) ) |
42 |
27 17 40 41
|
syl3anc |
|- ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( H e. ( K ^m NN0 ) /\ L e. NN0 ) ) -> ( ( L .^ M ) .x. ( ( algSc ` A ) ` ( H ` L ) ) ) = ( ( H ` L ) .* ( L .^ M ) ) ) |
43 |
24 42
|
eqtr2d |
|- ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( H e. ( K ^m NN0 ) /\ L e. NN0 ) ) -> ( ( H ` L ) .* ( L .^ M ) ) = ( ( L .^ M ) .x. ( ( H ` L ) .* .1. ) ) ) |