Metamath Proof Explorer

Theorem cayhamlem3

Description: Lemma for cayhamlem4 . (Contributed by AV, 24-Nov-2019) (Revised by AV, 15-Dec-2019)

Ref Expression
Hypotheses chcoeffeq.a 
|- A = ( N Mat R )
chcoeffeq.b 
|- B = ( Base ` A )
chcoeffeq.p 
|- P = ( Poly1 ` R )
chcoeffeq.y 
|- Y = ( N Mat P )
chcoeffeq.r 
|- .X. = ( .r ` Y )
chcoeffeq.s 
|- .- = ( -g ` Y )
chcoeffeq.0 
|- .0. = ( 0g ` Y )
chcoeffeq.t 
|- T = ( N matToPolyMat R )
chcoeffeq.c 
|- C = ( N CharPlyMat R )
chcoeffeq.k 
|- K = ( C ` M )
chcoeffeq.g 
|- G = ( n e. NN0 |-> if ( n = 0 , ( .0. .- ( ( T ` M ) .X. ( T ` ( b ` 0 ) ) ) ) , if ( n = ( s + 1 ) , ( T ` ( b ` s ) ) , if ( ( s + 1 ) < n , .0. , ( ( T ` ( b ` ( n - 1 ) ) ) .- ( ( T ` M ) .X. ( T ` ( b ` n ) ) ) ) ) ) ) )
chcoeffeq.w 
|- W = ( Base ` Y )
chcoeffeq.1 
|- .1. = ( 1r ` A )
chcoeffeq.m 
|- .* = ( .s ` A )
chcoeffeq.u 
|- U = ( N cPolyMatToMat R )
cayhamlem.e1 
|- .^ = ( .g ` ( mulGrp ` A ) )
cayhamlem.r 
|- .x. = ( .r ` A )
Assertion cayhamlem3 
|- ( ( N e. Fin /\ R e. CRing /\ M e. B ) -> E. s e. NN E. b e. ( B ^m ( 0 ... s ) ) ( A gsum ( n e. NN0 |-> ( ( ( coe1 ` K ) ` n ) .* ( n .^ M ) ) ) ) = ( A gsum ( n e. NN0 |-> ( ( n .^ M ) .x. ( U ` ( G ` n ) ) ) ) ) )

Proof

Step Hyp Ref Expression
1 chcoeffeq.a 
 |-  A = ( N Mat R )
2 chcoeffeq.b 
 |-  B = ( Base ` A )
3 chcoeffeq.p 
 |-  P = ( Poly1 ` R )
4 chcoeffeq.y 
 |-  Y = ( N Mat P )
5 chcoeffeq.r 
 |-  .X. = ( .r ` Y )
6 chcoeffeq.s 
 |-  .- = ( -g ` Y )
7 chcoeffeq.0 
 |-  .0. = ( 0g ` Y )
8 chcoeffeq.t 
 |-  T = ( N matToPolyMat R )
9 chcoeffeq.c 
 |-  C = ( N CharPlyMat R )
10 chcoeffeq.k 
 |-  K = ( C ` M )
11 chcoeffeq.g 
 |-  G = ( n e. NN0 |-> if ( n = 0 , ( .0. .- ( ( T ` M ) .X. ( T ` ( b ` 0 ) ) ) ) , if ( n = ( s + 1 ) , ( T ` ( b ` s ) ) , if ( ( s + 1 ) < n , .0. , ( ( T ` ( b ` ( n - 1 ) ) ) .- ( ( T ` M ) .X. ( T ` ( b ` n ) ) ) ) ) ) ) )
12 chcoeffeq.w 
 |-  W = ( Base ` Y )
13 chcoeffeq.1 
 |-  .1. = ( 1r ` A )
14 chcoeffeq.m 
 |-  .* = ( .s ` A )
15 chcoeffeq.u 
 |-  U = ( N cPolyMatToMat R )
16 cayhamlem.e1 
 |-  .^ = ( .g ` ( mulGrp ` A ) )
17 cayhamlem.r 
 |-  .x. = ( .r ` A )
18 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 chcoeffeq 
 |-  ( ( N e. Fin /\ R e. CRing /\ M e. B ) -> E. s e. NN E. b e. ( B ^m ( 0 ... s ) ) A. n e. NN0 ( U ` ( G ` n ) ) = ( ( ( coe1 ` K ) ` n ) .* .1. ) )
19 2fveq3 
 |-  ( n = l -> ( U ` ( G ` n ) ) = ( U ` ( G ` l ) ) )
20 fveq2 
 |-  ( n = l -> ( ( coe1 ` K ) ` n ) = ( ( coe1 ` K ) ` l ) )
21 20 oveq1d 
 |-  ( n = l -> ( ( ( coe1 ` K ) ` n ) .* .1. ) = ( ( ( coe1 ` K ) ` l ) .* .1. ) )
22 19 21 eqeq12d 
 |-  ( n = l -> ( ( U ` ( G ` n ) ) = ( ( ( coe1 ` K ) ` n ) .* .1. ) <-> ( U ` ( G ` l ) ) = ( ( ( coe1 ` K ) ` l ) .* .1. ) ) )
23 22 cbvralvw 
 |-  ( A. n e. NN0 ( U ` ( G ` n ) ) = ( ( ( coe1 ` K ) ` n ) .* .1. ) <-> A. l e. NN0 ( U ` ( G ` l ) ) = ( ( ( coe1 ` K ) ` l ) .* .1. ) )
24 2fveq3 
 |-  ( l = n -> ( U ` ( G ` l ) ) = ( U ` ( G ` n ) ) )
25 fveq2 
 |-  ( l = n -> ( ( coe1 ` K ) ` l ) = ( ( coe1 ` K ) ` n ) )
26 25 oveq1d 
 |-  ( l = n -> ( ( ( coe1 ` K ) ` l ) .* .1. ) = ( ( ( coe1 ` K ) ` n ) .* .1. ) )
27 24 26 eqeq12d 
 |-  ( l = n -> ( ( U ` ( G ` l ) ) = ( ( ( coe1 ` K ) ` l ) .* .1. ) <-> ( U ` ( G ` n ) ) = ( ( ( coe1 ` K ) ` n ) .* .1. ) ) )
28 27 rspccva 
 |-  ( ( A. l e. NN0 ( U ` ( G ` l ) ) = ( ( ( coe1 ` K ) ` l ) .* .1. ) /\ n e. NN0 ) -> ( U ` ( G ` n ) ) = ( ( ( coe1 ` K ) ` n ) .* .1. ) )
29 simprll 
 |-  ( ( n e. NN0 /\ ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ s e. NN ) /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> ( N e. Fin /\ R e. CRing /\ M e. B ) )
30 eqid 
 |-  ( Base ` P ) = ( Base ` P )
31 9 1 2 3 30 chpmatply1 
 |-  ( ( N e. Fin /\ R e. CRing /\ M e. B ) -> ( C ` M ) e. ( Base ` P ) )
32 29 31 syl 
 |-  ( ( n e. NN0 /\ ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ s e. NN ) /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> ( C ` M ) e. ( Base ` P ) )
33 10 32 eqeltrid 
 |-  ( ( n e. NN0 /\ ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ s e. NN ) /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> K e. ( Base ` P ) )
34 eqid 
 |-  ( coe1 ` K ) = ( coe1 ` K )
35 eqid 
 |-  ( Base ` R ) = ( Base ` R )
36 34 30 3 35 coe1f 
 |-  ( K e. ( Base ` P ) -> ( coe1 ` K ) : NN0 --> ( Base ` R ) )
37 33 36 syl 
 |-  ( ( n e. NN0 /\ ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ s e. NN ) /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> ( coe1 ` K ) : NN0 --> ( Base ` R ) )
38 fvex 
 |-  ( Base ` R ) e. _V
39 nn0ex 
 |-  NN0 e. _V
40 38 39 pm3.2i 
 |-  ( ( Base ` R ) e. _V /\ NN0 e. _V )
41 elmapg 
 |-  ( ( ( Base ` R ) e. _V /\ NN0 e. _V ) -> ( ( coe1 ` K ) e. ( ( Base ` R ) ^m NN0 ) <-> ( coe1 ` K ) : NN0 --> ( Base ` R ) ) )
42 40 41 mp1i 
 |-  ( ( n e. NN0 /\ ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ s e. NN ) /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> ( ( coe1 ` K ) e. ( ( Base ` R ) ^m NN0 ) <-> ( coe1 ` K ) : NN0 --> ( Base ` R ) ) )
43 37 42 mpbird 
 |-  ( ( n e. NN0 /\ ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ s e. NN ) /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> ( coe1 ` K ) e. ( ( Base ` R ) ^m NN0 ) )
44 simpl 
 |-  ( ( n e. NN0 /\ ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ s e. NN ) /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> n e. NN0 )
45 35 1 2 13 14 16 17 cayhamlem2 
 |-  ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ ( ( coe1 ` K ) e. ( ( Base ` R ) ^m NN0 ) /\ n e. NN0 ) ) -> ( ( ( coe1 ` K ) ` n ) .* ( n .^ M ) ) = ( ( n .^ M ) .x. ( ( ( coe1 ` K ) ` n ) .* .1. ) ) )
46 29 43 44 45 syl12anc 
 |-  ( ( n e. NN0 /\ ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ s e. NN ) /\ b e. ( B ^m ( 0 ... s ) ) ) ) -> ( ( ( coe1 ` K ) ` n ) .* ( n .^ M ) ) = ( ( n .^ M ) .x. ( ( ( coe1 ` K ) ` n ) .* .1. ) ) )
47 46 adantl 
 |-  ( ( ( U ` ( G ` n ) ) = ( ( ( coe1 ` K ) ` n ) .* .1. ) /\ ( n e. NN0 /\ ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ s e. NN ) /\ b e. ( B ^m ( 0 ... s ) ) ) ) ) -> ( ( ( coe1 ` K ) ` n ) .* ( n .^ M ) ) = ( ( n .^ M ) .x. ( ( ( coe1 ` K ) ` n ) .* .1. ) ) )
48 oveq2 
 |-  ( ( U ` ( G ` n ) ) = ( ( ( coe1 ` K ) ` n ) .* .1. ) -> ( ( n .^ M ) .x. ( U ` ( G ` n ) ) ) = ( ( n .^ M ) .x. ( ( ( coe1 ` K ) ` n ) .* .1. ) ) )
49 48 adantr 
 |-  ( ( ( U ` ( G ` n ) ) = ( ( ( coe1 ` K ) ` n ) .* .1. ) /\ ( n e. NN0 /\ ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ s e. NN ) /\ b e. ( B ^m ( 0 ... s ) ) ) ) ) -> ( ( n .^ M ) .x. ( U ` ( G ` n ) ) ) = ( ( n .^ M ) .x. ( ( ( coe1 ` K ) ` n ) .* .1. ) ) )
50 47 49 eqtr4d 
 |-  ( ( ( U ` ( G ` n ) ) = ( ( ( coe1 ` K ) ` n ) .* .1. ) /\ ( n e. NN0 /\ ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ s e. NN ) /\ b e. ( B ^m ( 0 ... s ) ) ) ) ) -> ( ( ( coe1 ` K ) ` n ) .* ( n .^ M ) ) = ( ( n .^ M ) .x. ( U ` ( G ` n ) ) ) )
51 50 exp32 
 |-  ( ( U ` ( G ` n ) ) = ( ( ( coe1 ` K ) ` n ) .* .1. ) -> ( n e. NN0 -> ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ s e. NN ) /\ b e. ( B ^m ( 0 ... s ) ) ) -> ( ( ( coe1 ` K ) ` n ) .* ( n .^ M ) ) = ( ( n .^ M ) .x. ( U ` ( G ` n ) ) ) ) ) )
52 51 com12 
 |-  ( n e. NN0 -> ( ( U ` ( G ` n ) ) = ( ( ( coe1 ` K ) ` n ) .* .1. ) -> ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ s e. NN ) /\ b e. ( B ^m ( 0 ... s ) ) ) -> ( ( ( coe1 ` K ) ` n ) .* ( n .^ M ) ) = ( ( n .^ M ) .x. ( U ` ( G ` n ) ) ) ) ) )
53 52 adantl 
 |-  ( ( A. l e. NN0 ( U ` ( G ` l ) ) = ( ( ( coe1 ` K ) ` l ) .* .1. ) /\ n e. NN0 ) -> ( ( U ` ( G ` n ) ) = ( ( ( coe1 ` K ) ` n ) .* .1. ) -> ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ s e. NN ) /\ b e. ( B ^m ( 0 ... s ) ) ) -> ( ( ( coe1 ` K ) ` n ) .* ( n .^ M ) ) = ( ( n .^ M ) .x. ( U ` ( G ` n ) ) ) ) ) )
54 28 53 mpd 
 |-  ( ( A. l e. NN0 ( U ` ( G ` l ) ) = ( ( ( coe1 ` K ) ` l ) .* .1. ) /\ n e. NN0 ) -> ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ s e. NN ) /\ b e. ( B ^m ( 0 ... s ) ) ) -> ( ( ( coe1 ` K ) ` n ) .* ( n .^ M ) ) = ( ( n .^ M ) .x. ( U ` ( G ` n ) ) ) ) )
55 54 com12 
 |-  ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ s e. NN ) /\ b e. ( B ^m ( 0 ... s ) ) ) -> ( ( A. l e. NN0 ( U ` ( G ` l ) ) = ( ( ( coe1 ` K ) ` l ) .* .1. ) /\ n e. NN0 ) -> ( ( ( coe1 ` K ) ` n ) .* ( n .^ M ) ) = ( ( n .^ M ) .x. ( U ` ( G ` n ) ) ) ) )
56 55 impl 
 |-  ( ( ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ s e. NN ) /\ b e. ( B ^m ( 0 ... s ) ) ) /\ A. l e. NN0 ( U ` ( G ` l ) ) = ( ( ( coe1 ` K ) ` l ) .* .1. ) ) /\ n e. NN0 ) -> ( ( ( coe1 ` K ) ` n ) .* ( n .^ M ) ) = ( ( n .^ M ) .x. ( U ` ( G ` n ) ) ) )
57 56 mpteq2dva 
 |-  ( ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ s e. NN ) /\ b e. ( B ^m ( 0 ... s ) ) ) /\ A. l e. NN0 ( U ` ( G ` l ) ) = ( ( ( coe1 ` K ) ` l ) .* .1. ) ) -> ( n e. NN0 |-> ( ( ( coe1 ` K ) ` n ) .* ( n .^ M ) ) ) = ( n e. NN0 |-> ( ( n .^ M ) .x. ( U ` ( G ` n ) ) ) ) )
58 57 oveq2d 
 |-  ( ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ s e. NN ) /\ b e. ( B ^m ( 0 ... s ) ) ) /\ A. l e. NN0 ( U ` ( G ` l ) ) = ( ( ( coe1 ` K ) ` l ) .* .1. ) ) -> ( A gsum ( n e. NN0 |-> ( ( ( coe1 ` K ) ` n ) .* ( n .^ M ) ) ) ) = ( A gsum ( n e. NN0 |-> ( ( n .^ M ) .x. ( U ` ( G ` n ) ) ) ) ) )
59 58 ex 
 |-  ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ s e. NN ) /\ b e. ( B ^m ( 0 ... s ) ) ) -> ( A. l e. NN0 ( U ` ( G ` l ) ) = ( ( ( coe1 ` K ) ` l ) .* .1. ) -> ( A gsum ( n e. NN0 |-> ( ( ( coe1 ` K ) ` n ) .* ( n .^ M ) ) ) ) = ( A gsum ( n e. NN0 |-> ( ( n .^ M ) .x. ( U ` ( G ` n ) ) ) ) ) ) )
60 23 59 biimtrid 
 |-  ( ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ s e. NN ) /\ b e. ( B ^m ( 0 ... s ) ) ) -> ( A. n e. NN0 ( U ` ( G ` n ) ) = ( ( ( coe1 ` K ) ` n ) .* .1. ) -> ( A gsum ( n e. NN0 |-> ( ( ( coe1 ` K ) ` n ) .* ( n .^ M ) ) ) ) = ( A gsum ( n e. NN0 |-> ( ( n .^ M ) .x. ( U ` ( G ` n ) ) ) ) ) ) )
61 60 reximdva 
 |-  ( ( ( N e. Fin /\ R e. CRing /\ M e. B ) /\ s e. NN ) -> ( E. b e. ( B ^m ( 0 ... s ) ) A. n e. NN0 ( U ` ( G ` n ) ) = ( ( ( coe1 ` K ) ` n ) .* .1. ) -> E. b e. ( B ^m ( 0 ... s ) ) ( A gsum ( n e. NN0 |-> ( ( ( coe1 ` K ) ` n ) .* ( n .^ M ) ) ) ) = ( A gsum ( n e. NN0 |-> ( ( n .^ M ) .x. ( U ` ( G ` n ) ) ) ) ) ) )
62 61 reximdva 
 |-  ( ( N e. Fin /\ R e. CRing /\ M e. B ) -> ( E. s e. NN E. b e. ( B ^m ( 0 ... s ) ) A. n e. NN0 ( U ` ( G ` n ) ) = ( ( ( coe1 ` K ) ` n ) .* .1. ) -> E. s e. NN E. b e. ( B ^m ( 0 ... s ) ) ( A gsum ( n e. NN0 |-> ( ( ( coe1 ` K ) ` n ) .* ( n .^ M ) ) ) ) = ( A gsum ( n e. NN0 |-> ( ( n .^ M ) .x. ( U ` ( G ` n ) ) ) ) ) ) )
63 18 62 mpd 
 |-  ( ( N e. Fin /\ R e. CRing /\ M e. B ) -> E. s e. NN E. b e. ( B ^m ( 0 ... s ) ) ( A gsum ( n e. NN0 |-> ( ( ( coe1 ` K ) ` n ) .* ( n .^ M ) ) ) ) = ( A gsum ( n e. NN0 |-> ( ( n .^ M ) .x. ( U ` ( G ` n ) ) ) ) ) )