Metamath Proof Explorer

Theorem cayhamlem2

Description: Lemma for cayhamlem3 . (Contributed by AV, 24-Nov-2019)

Ref Expression
Hypotheses cayhamlem2.k 
|- K = ( Base ` R )
cayhamlem2.a 
|- A = ( N Mat R )
cayhamlem2.b 
|- B = ( Base ` A )
cayhamlem2.1 
|- .1. = ( 1r ` A )
cayhamlem2.m 
|- .* = ( .s ` A )
cayhamlem2.e 
|- .^ = ( .g ` ( mulGrp ` A ) )
cayhamlem2.r 
|- .x. = ( .r ` A )
Assertion cayhamlem2 
|- ( ( ( 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. ) ) )

Proof

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 eqtr2id 
 |-  ( ( 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. ) ) )