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 ffvelcdmda 
 |-  ( ( 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 eqid 
 |-  ( mulGrp ` A ) = ( mulGrp ` A )
29 28 3 mgpbas 
 |-  B = ( Base ` ( mulGrp ` A ) )
30 crngring 
 |-  ( R e. CRing -> R e. Ring )
31 30 anim2i 
 |-  ( ( N e. Fin /\ R e. CRing ) -> ( N e. Fin /\ R e. Ring ) )
32 31 3adant3 
 |-  ( ( N e. Fin /\ R e. CRing /\ M e. B ) -> ( N e. Fin /\ R e. Ring ) )
33 2 matring 
 |-  ( ( N e. Fin /\ R e. Ring ) -> A e. Ring )
34 28 ringmgp 
 |-  ( A e. Ring -> ( mulGrp ` A ) e. Mnd )
35 32 33 34 3syl 
 |-  ( ( N e. Fin /\ R e. CRing /\ M e. B ) -> ( mulGrp ` A ) e. Mnd )
36 35 adantr 
 |-  ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( H e. ( K ^m NN0 ) /\ L e. NN0 ) ) -> ( mulGrp ` A ) e. Mnd )
37 simprr 
 |-  ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( H e. ( K ^m NN0 ) /\ L e. NN0 ) ) -> L e. NN0 )
38 simpl3 
 |-  ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( H e. ( K ^m NN0 ) /\ L e. NN0 ) ) -> M e. B )
39 29 6 36 37 38 mulgnn0cld 
 |-  ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( H e. ( K ^m NN0 ) /\ L e. NN0 ) ) -> ( L .^ M ) e. B )
40 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 ) ) )
41 27 17 39 40 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 ) ) )
42 24 41 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. ) ) )