Metamath Proof Explorer

Theorem cytpval

Description: Substitutions for the Nth cyclotomic polynomial. (Contributed by Stefan O'Rear, 5-Sep-2015)

Ref Expression
Hypotheses cytpval.t 
|- T = ( ( mulGrp ` CCfld ) |`s ( CC \ { 0 } ) )
cytpval.o 
|- O = ( od ` T )
cytpval.p 
|- P = ( Poly1 ` CCfld )
cytpval.x 
|- X = ( var1 ` CCfld )
cytpval.q 
|- Q = ( mulGrp ` P )
cytpval.m 
|- .- = ( -g ` P )
cytpval.a 
|- A = ( algSc ` P )
Assertion cytpval 
|- ( N e. NN -> ( CytP ` N ) = ( Q gsum ( r e. ( `' O " { N } ) |-> ( X .- ( A ` r ) ) ) ) )

Proof

Step Hyp Ref Expression
1 cytpval.t 
 |-  T = ( ( mulGrp ` CCfld ) |`s ( CC \ { 0 } ) )
2 cytpval.o 
 |-  O = ( od ` T )
3 cytpval.p 
 |-  P = ( Poly1 ` CCfld )
4 cytpval.x 
 |-  X = ( var1 ` CCfld )
5 cytpval.q 
 |-  Q = ( mulGrp ` P )
6 cytpval.m 
 |-  .- = ( -g ` P )
7 cytpval.a 
 |-  A = ( algSc ` P )
8 3 eqcomi 
 |-  ( Poly1 ` CCfld ) = P
9 8 fveq2i 
 |-  ( mulGrp ` ( Poly1 ` CCfld ) ) = ( mulGrp ` P )
10 9 5 eqtr4i 
 |-  ( mulGrp ` ( Poly1 ` CCfld ) ) = Q
11 10 a1i 
 |-  ( n = N -> ( mulGrp ` ( Poly1 ` CCfld ) ) = Q )
12 1 fveq2i 
 |-  ( od ` T ) = ( od ` ( ( mulGrp ` CCfld ) |`s ( CC \ { 0 } ) ) )
13 2 12 eqtri 
 |-  O = ( od ` ( ( mulGrp ` CCfld ) |`s ( CC \ { 0 } ) ) )
14 13 cnveqi 
 |-  `' O = `' ( od ` ( ( mulGrp ` CCfld ) |`s ( CC \ { 0 } ) ) )
15 14 imaeq1i 
 |-  ( `' O " { n } ) = ( `' ( od ` ( ( mulGrp ` CCfld ) |`s ( CC \ { 0 } ) ) ) " { n } )
16 sneq 
 |-  ( n = N -> { n } = { N } )
17 16 imaeq2d 
 |-  ( n = N -> ( `' O " { n } ) = ( `' O " { N } ) )
18 15 17 eqtr3id 
 |-  ( n = N -> ( `' ( od ` ( ( mulGrp ` CCfld ) |`s ( CC \ { 0 } ) ) ) " { n } ) = ( `' O " { N } ) )
19 3 fveq2i 
 |-  ( algSc ` P ) = ( algSc ` ( Poly1 ` CCfld ) )
20 7 19 eqtri 
 |-  A = ( algSc ` ( Poly1 ` CCfld ) )
21 20 fveq1i 
 |-  ( A ` r ) = ( ( algSc ` ( Poly1 ` CCfld ) ) ` r )
22 3 fveq2i 
 |-  ( -g ` P ) = ( -g ` ( Poly1 ` CCfld ) )
23 6 22 eqtri 
 |-  .- = ( -g ` ( Poly1 ` CCfld ) )
24 4 21 23 oveq123i 
 |-  ( X .- ( A ` r ) ) = ( ( var1 ` CCfld ) ( -g ` ( Poly1 ` CCfld ) ) ( ( algSc ` ( Poly1 ` CCfld ) ) ` r ) )
25 24 eqcomi 
 |-  ( ( var1 ` CCfld ) ( -g ` ( Poly1 ` CCfld ) ) ( ( algSc ` ( Poly1 ` CCfld ) ) ` r ) ) = ( X .- ( A ` r ) )
26 25 a1i 
 |-  ( n = N -> ( ( var1 ` CCfld ) ( -g ` ( Poly1 ` CCfld ) ) ( ( algSc ` ( Poly1 ` CCfld ) ) ` r ) ) = ( X .- ( A ` r ) ) )
27 18 26 mpteq12dv 
 |-  ( n = N -> ( r e. ( `' ( od ` ( ( mulGrp ` CCfld ) |`s ( CC \ { 0 } ) ) ) " { n } ) |-> ( ( var1 ` CCfld ) ( -g ` ( Poly1 ` CCfld ) ) ( ( algSc ` ( Poly1 ` CCfld ) ) ` r ) ) ) = ( r e. ( `' O " { N } ) |-> ( X .- ( A ` r ) ) ) )
28 11 27 oveq12d 
 |-  ( n = N -> ( ( mulGrp ` ( Poly1 ` CCfld ) ) gsum ( r e. ( `' ( od ` ( ( mulGrp ` CCfld ) |`s ( CC \ { 0 } ) ) ) " { n } ) |-> ( ( var1 ` CCfld ) ( -g ` ( Poly1 ` CCfld ) ) ( ( algSc ` ( Poly1 ` CCfld ) ) ` r ) ) ) ) = ( Q gsum ( r e. ( `' O " { N } ) |-> ( X .- ( A ` r ) ) ) ) )
29 df-cytp 
 |-  CytP = ( n e. NN |-> ( ( mulGrp ` ( Poly1 ` CCfld ) ) gsum ( r e. ( `' ( od ` ( ( mulGrp ` CCfld ) |`s ( CC \ { 0 } ) ) ) " { n } ) |-> ( ( var1 ` CCfld ) ( -g ` ( Poly1 ` CCfld ) ) ( ( algSc ` ( Poly1 ` CCfld ) ) ` r ) ) ) ) )
30 ovex 
 |-  ( Q gsum ( r e. ( `' O " { N } ) |-> ( X .- ( A ` r ) ) ) ) e. _V
31 28 29 30 fvmpt 
 |-  ( N e. NN -> ( CytP ` N ) = ( Q gsum ( r e. ( `' O " { N } ) |-> ( X .- ( A ` r ) ) ) ) )