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 fld 𝑠 0
cytpval.o O = od T
cytpval.p P = Poly 1 fld
cytpval.x X = var 1 fld
cytpval.q Q = mulGrp P
cytpval.m - ˙ = - P
cytpval.a A = algSc P
Assertion cytpval N CytP N = Q r O -1 N X - ˙ A r

Proof

Step Hyp Ref Expression
1 cytpval.t T = mulGrp fld 𝑠 0
2 cytpval.o O = od T
3 cytpval.p P = Poly 1 fld
4 cytpval.x X = var 1 fld
5 cytpval.q Q = mulGrp P
6 cytpval.m - ˙ = - P
7 cytpval.a A = algSc P
8 3 eqcomi Poly 1 fld = P
9 8 fveq2i mulGrp Poly 1 fld = mulGrp P
10 9 5 eqtr4i mulGrp Poly 1 fld = Q
11 10 a1i n = N mulGrp Poly 1 fld = Q
12 1 fveq2i od T = od mulGrp fld 𝑠 0
13 2 12 eqtri O = od mulGrp fld 𝑠 0
14 13 cnveqi O -1 = od mulGrp fld 𝑠 0 -1
15 14 imaeq1i O -1 n = od mulGrp fld 𝑠 0 -1 n
16 sneq n = N n = N
17 16 imaeq2d n = N O -1 n = O -1 N
18 15 17 eqtr3id n = N od mulGrp fld 𝑠 0 -1 n = O -1 N
19 3 fveq2i algSc P = algSc Poly 1 fld
20 7 19 eqtri A = algSc Poly 1 fld
21 20 fveq1i A r = algSc Poly 1 fld r
22 3 fveq2i - P = - Poly 1 fld
23 6 22 eqtri - ˙ = - Poly 1 fld
24 4 21 23 oveq123i X - ˙ A r = var 1 fld - Poly 1 fld algSc Poly 1 fld r
25 24 eqcomi var 1 fld - Poly 1 fld algSc Poly 1 fld r = X - ˙ A r
26 25 a1i n = N var 1 fld - Poly 1 fld algSc Poly 1 fld r = X - ˙ A r
27 18 26 mpteq12dv n = N r od mulGrp fld 𝑠 0 -1 n var 1 fld - Poly 1 fld algSc Poly 1 fld r = r O -1 N X - ˙ A r
28 11 27 oveq12d n = N mulGrp Poly 1 fld r od mulGrp fld 𝑠 0 -1 n var 1 fld - Poly 1 fld algSc Poly 1 fld r = Q r O -1 N X - ˙ A r
29 df-cytp CytP = n mulGrp Poly 1 fld r od mulGrp fld 𝑠 0 -1 n var 1 fld - Poly 1 fld algSc Poly 1 fld r
30 ovex Q r O -1 N X - ˙ A r V
31 28 29 30 fvmpt N CytP N = Q r O -1 N X - ˙ A r