Metamath Proof Explorer

Theorem aks6d1c1p2

Description: P and linear factors are introspective. (Contributed by metakunt, 25-Apr-2025)

Ref Expression
Hypotheses aks6d1c1p2.1 
|- .~ = { <. e , f >. | ( e e. NN /\ f e. B /\ A. y e. ( V PrimRoots R ) ( e .^ ( ( O ` f ) ` y ) ) = ( ( O ` f ) ` ( e .^ y ) ) ) }
aks6d1c1p2.2 
|- S = ( Poly1 ` K )
aks6d1c1p2.3 
|- B = ( Base ` S )
aks6d1c1p2.4 
|- X = ( var1 ` K )
aks6d1c1p2.5 
|- W = ( mulGrp ` S )
aks6d1c1p2.6 
|- V = ( mulGrp ` K )
aks6d1c1p2.7 
|- .^ = ( .g ` V )
aks6d1c1p2.8 
|- C = ( algSc ` S )
aks6d1c1p2.9 
|- D = ( .g ` W )
aks6d1c1p2.10 
|- P = ( chr ` K )
aks6d1c1p2.11 
|- O = ( eval1 ` K )
aks6d1c1p2.12 
|- .+ = ( +g ` S )
aks6d1c1p2.13 
|- ( ph -> K e. Field )
aks6d1c1p2.14 
|- ( ph -> P e. Prime )
aks6d1c1p2.15 
|- ( ph -> R e. NN )
aks6d1c1p2.16 
|- ( ph -> ( N gcd R ) = 1 )
aks6d1c1p2.17 
|- ( ph -> P || N )
aks6d1c1p2.18 
|- F = ( X .+ ( C ` ( ( ZRHom ` K ) ` A ) ) )
aks6d1c1p2.19 
|- ( ph -> A e. ZZ )
Assertion aks6d1c1p2 
|- ( ph -> P .~ F )

Proof

Step Hyp Ref Expression
1 aks6d1c1p2.1 
 |-  .~ = { <. e , f >. | ( e e. NN /\ f e. B /\ A. y e. ( V PrimRoots R ) ( e .^ ( ( O ` f ) ` y ) ) = ( ( O ` f ) ` ( e .^ y ) ) ) }
2 aks6d1c1p2.2 
 |-  S = ( Poly1 ` K )
3 aks6d1c1p2.3 
 |-  B = ( Base ` S )
4 aks6d1c1p2.4 
 |-  X = ( var1 ` K )
5 aks6d1c1p2.5 
 |-  W = ( mulGrp ` S )
6 aks6d1c1p2.6 
 |-  V = ( mulGrp ` K )
7 aks6d1c1p2.7 
 |-  .^ = ( .g ` V )
8 aks6d1c1p2.8 
 |-  C = ( algSc ` S )
9 aks6d1c1p2.9 
 |-  D = ( .g ` W )
10 aks6d1c1p2.10 
 |-  P = ( chr ` K )
11 aks6d1c1p2.11 
 |-  O = ( eval1 ` K )
12 aks6d1c1p2.12 
 |-  .+ = ( +g ` S )
13 aks6d1c1p2.13 
 |-  ( ph -> K e. Field )
14 aks6d1c1p2.14 
 |-  ( ph -> P e. Prime )
15 aks6d1c1p2.15 
 |-  ( ph -> R e. NN )
16 aks6d1c1p2.16 
 |-  ( ph -> ( N gcd R ) = 1 )
17 aks6d1c1p2.17 
 |-  ( ph -> P || N )
18 aks6d1c1p2.18 
 |-  F = ( X .+ ( C ` ( ( ZRHom ` K ) ` A ) ) )
19 aks6d1c1p2.19 
 |-  ( ph -> A e. ZZ )
20 isfld 
 |-  ( K e. Field <-> ( K e. DivRing /\ K e. CRing ) )
21 13 20 sylib 
 |-  ( ph -> ( K e. DivRing /\ K e. CRing ) )
22 21 simprd 
 |-  ( ph -> K e. CRing )
23 6 crngmgp 
 |-  ( K e. CRing -> V e. CMnd )
24 22 23 syl 
 |-  ( ph -> V e. CMnd )
25 15 nnnn0d 
 |-  ( ph -> R e. NN0 )
26 24 25 7 isprimroot 
 |-  ( ph -> ( y e. ( V PrimRoots R ) <-> ( y e. ( Base ` V ) /\ ( R .^ y ) = ( 0g ` V ) /\ A. l e. NN0 ( ( l .^ y ) = ( 0g ` V ) -> R || l ) ) ) )
27 26 biimpd 
 |-  ( ph -> ( y e. ( V PrimRoots R ) -> ( y e. ( Base ` V ) /\ ( R .^ y ) = ( 0g ` V ) /\ A. l e. NN0 ( ( l .^ y ) = ( 0g ` V ) -> R || l ) ) ) )
28 27 imp 
 |-  ( ( ph /\ y e. ( V PrimRoots R ) ) -> ( y e. ( Base ` V ) /\ ( R .^ y ) = ( 0g ` V ) /\ A. l e. NN0 ( ( l .^ y ) = ( 0g ` V ) -> R || l ) ) )
29 28 simp1d 
 |-  ( ( ph /\ y e. ( V PrimRoots R ) ) -> y e. ( Base ` V ) )
30 eqid 
 |-  ( Base ` K ) = ( Base ` K )
31 6 30 mgpbas 
 |-  ( Base ` K ) = ( Base ` V )
32 31 eqcomi 
 |-  ( Base ` V ) = ( Base ` K )
33 32 a1i 
 |-  ( ph -> ( Base ` V ) = ( Base ` K ) )
34 33 adantr 
 |-  ( ( ph /\ y e. ( V PrimRoots R ) ) -> ( Base ` V ) = ( Base ` K ) )
35 34 eleq2d 
 |-  ( ( ph /\ y e. ( V PrimRoots R ) ) -> ( y e. ( Base ` V ) <-> y e. ( Base ` K ) ) )
36 29 35 mpbid 
 |-  ( ( ph /\ y e. ( V PrimRoots R ) ) -> y e. ( Base ` K ) )
37 36 ex 
 |-  ( ph -> ( y e. ( V PrimRoots R ) -> y e. ( Base ` K ) ) )
38 18 a1i 
 |-  ( ( ph /\ y e. ( Base ` K ) ) -> F = ( X .+ ( C ` ( ( ZRHom ` K ) ` A ) ) ) )
39 38 fveq2d 
 |-  ( ( ph /\ y e. ( Base ` K ) ) -> ( O ` F ) = ( O ` ( X .+ ( C ` ( ( ZRHom ` K ) ` A ) ) ) ) )
40 39 fveq1d 
 |-  ( ( ph /\ y e. ( Base ` K ) ) -> ( ( O ` F ) ` y ) = ( ( O ` ( X .+ ( C ` ( ( ZRHom ` K ) ` A ) ) ) ) ` y ) )
41 40 oveq2d 
 |-  ( ( ph /\ y e. ( Base ` K ) ) -> ( P .^ ( ( O ` F ) ` y ) ) = ( P .^ ( ( O ` ( X .+ ( C ` ( ( ZRHom ` K ) ` A ) ) ) ) ` y ) ) )
42 22 adantr 
 |-  ( ( ph /\ y e. ( Base ` K ) ) -> K e. CRing )
43 simpr 
 |-  ( ( ph /\ y e. ( Base ` K ) ) -> y e. ( Base ` K ) )
44 crngring 
 |-  ( K e. CRing -> K e. Ring )
45 4 2 3 vr1cl 
 |-  ( K e. Ring -> X e. B )
46 42 44 45 3syl 
 |-  ( ( ph /\ y e. ( Base ` K ) ) -> X e. B )
47 11 4 30 2 3 42 43 evl1vard 
 |-  ( ( ph /\ y e. ( Base ` K ) ) -> ( X e. B /\ ( ( O ` X ) ` y ) = y ) )
48 47 simprd 
 |-  ( ( ph /\ y e. ( Base ` K ) ) -> ( ( O ` X ) ` y ) = y )
49 46 48 jca 
 |-  ( ( ph /\ y e. ( Base ` K ) ) -> ( X e. B /\ ( ( O ` X ) ` y ) = y ) )
50 22 44 syl 
 |-  ( ph -> K e. Ring )
51 22 crngringd 
 |-  ( ph -> K e. Ring )
52 eqid 
 |-  ( ZRHom ` K ) = ( ZRHom ` K )
53 52 zrhrhm 
 |-  ( K e. Ring -> ( ZRHom ` K ) e. ( ZZring RingHom K ) )
54 rhmghm 
 |-  ( ( ZRHom ` K ) e. ( ZZring RingHom K ) -> ( ZRHom ` K ) e. ( ZZring GrpHom K ) )
55 zringbas 
 |-  ZZ = ( Base ` ZZring )
56 55 30 ghmf 
 |-  ( ( ZRHom ` K ) e. ( ZZring GrpHom K ) -> ( ZRHom ` K ) : ZZ --> ( Base ` K ) )
57 51 53 54 56 4syl 
 |-  ( ph -> ( ZRHom ` K ) : ZZ --> ( Base ` K ) )
58 57 19 ffvelcdmd 
 |-  ( ph -> ( ( ZRHom ` K ) ` A ) e. ( Base ` K ) )
59 2 8 30 3 ply1sclcl 
 |-  ( ( K e. Ring /\ ( ( ZRHom ` K ) ` A ) e. ( Base ` K ) ) -> ( C ` ( ( ZRHom ` K ) ` A ) ) e. B )
60 50 58 59 syl2anc 
 |-  ( ph -> ( C ` ( ( ZRHom ` K ) ` A ) ) e. B )
61 60 adantr 
 |-  ( ( ph /\ y e. ( Base ` K ) ) -> ( C ` ( ( ZRHom ` K ) ` A ) ) e. B )
62 58 adantr 
 |-  ( ( ph /\ y e. ( Base ` K ) ) -> ( ( ZRHom ` K ) ` A ) e. ( Base ` K ) )
63 11 2 30 8 3 42 62 43 evl1scad 
 |-  ( ( ph /\ y e. ( Base ` K ) ) -> ( ( C ` ( ( ZRHom ` K ) ` A ) ) e. B /\ ( ( O ` ( C ` ( ( ZRHom ` K ) ` A ) ) ) ` y ) = ( ( ZRHom ` K ) ` A ) ) )
64 63 simprd 
 |-  ( ( ph /\ y e. ( Base ` K ) ) -> ( ( O ` ( C ` ( ( ZRHom ` K ) ` A ) ) ) ` y ) = ( ( ZRHom ` K ) ` A ) )
65 61 64 jca 
 |-  ( ( ph /\ y e. ( Base ` K ) ) -> ( ( C ` ( ( ZRHom ` K ) ` A ) ) e. B /\ ( ( O ` ( C ` ( ( ZRHom ` K ) ` A ) ) ) ` y ) = ( ( ZRHom ` K ) ` A ) ) )
66 eqid 
 |-  ( +g ` K ) = ( +g ` K )
67 11 2 30 3 42 43 49 65 12 66 evl1addd 
 |-  ( ( ph /\ y e. ( Base ` K ) ) -> ( ( X .+ ( C ` ( ( ZRHom ` K ) ` A ) ) ) e. B /\ ( ( O ` ( X .+ ( C ` ( ( ZRHom ` K ) ` A ) ) ) ) ` y ) = ( y ( +g ` K ) ( ( ZRHom ` K ) ` A ) ) ) )
68 67 simprd 
 |-  ( ( ph /\ y e. ( Base ` K ) ) -> ( ( O ` ( X .+ ( C ` ( ( ZRHom ` K ) ` A ) ) ) ) ` y ) = ( y ( +g ` K ) ( ( ZRHom ` K ) ` A ) ) )
69 68 oveq2d 
 |-  ( ( ph /\ y e. ( Base ` K ) ) -> ( P .^ ( ( O ` ( X .+ ( C ` ( ( ZRHom ` K ) ` A ) ) ) ) ` y ) ) = ( P .^ ( y ( +g ` K ) ( ( ZRHom ` K ) ` A ) ) ) )
70 41 69 eqtrd 
 |-  ( ( ph /\ y e. ( Base ` K ) ) -> ( P .^ ( ( O ` F ) ` y ) ) = ( P .^ ( y ( +g ` K ) ( ( ZRHom ` K ) ` A ) ) ) )
71 39 fveq1d 
 |-  ( ( ph /\ y e. ( Base ` K ) ) -> ( ( O ` F ) ` ( P .^ y ) ) = ( ( O ` ( X .+ ( C ` ( ( ZRHom ` K ) ` A ) ) ) ) ` ( P .^ y ) ) )
72 eqid 
 |-  ( Base ` V ) = ( Base ` V )
73 6 ringmgp 
 |-  ( K e. Ring -> V e. Mnd )
74 42 44 73 3syl 
 |-  ( ( ph /\ y e. ( Base ` K ) ) -> V e. Mnd )
75 prmnn 
 |-  ( P e. Prime -> P e. NN )
76 14 75 syl 
 |-  ( ph -> P e. NN )
77 76 nnnn0d 
 |-  ( ph -> P e. NN0 )
78 77 adantr 
 |-  ( ( ph /\ y e. ( Base ` K ) ) -> P e. NN0 )
79 43 31 eleqtrdi 
 |-  ( ( ph /\ y e. ( Base ` K ) ) -> y e. ( Base ` V ) )
80 72 7 74 78 79 mulgnn0cld 
 |-  ( ( ph /\ y e. ( Base ` K ) ) -> ( P .^ y ) e. ( Base ` V ) )
81 80 32 eleqtrdi 
 |-  ( ( ph /\ y e. ( Base ` K ) ) -> ( P .^ y ) e. ( Base ` K ) )
82 11 4 30 2 3 42 81 evl1vard 
 |-  ( ( ph /\ y e. ( Base ` K ) ) -> ( X e. B /\ ( ( O ` X ) ` ( P .^ y ) ) = ( P .^ y ) ) )
83 11 2 30 8 3 42 62 81 evl1scad 
 |-  ( ( ph /\ y e. ( Base ` K ) ) -> ( ( C ` ( ( ZRHom ` K ) ` A ) ) e. B /\ ( ( O ` ( C ` ( ( ZRHom ` K ) ` A ) ) ) ` ( P .^ y ) ) = ( ( ZRHom ` K ) ` A ) ) )
84 83 simprd 
 |-  ( ( ph /\ y e. ( Base ` K ) ) -> ( ( O ` ( C ` ( ( ZRHom ` K ) ` A ) ) ) ` ( P .^ y ) ) = ( ( ZRHom ` K ) ` A ) )
85 61 84 jca 
 |-  ( ( ph /\ y e. ( Base ` K ) ) -> ( ( C ` ( ( ZRHom ` K ) ` A ) ) e. B /\ ( ( O ` ( C ` ( ( ZRHom ` K ) ` A ) ) ) ` ( P .^ y ) ) = ( ( ZRHom ` K ) ` A ) ) )
86 11 2 30 3 42 81 82 85 12 66 evl1addd 
 |-  ( ( ph /\ y e. ( Base ` K ) ) -> ( ( X .+ ( C ` ( ( ZRHom ` K ) ` A ) ) ) e. B /\ ( ( O ` ( X .+ ( C ` ( ( ZRHom ` K ) ` A ) ) ) ) ` ( P .^ y ) ) = ( ( P .^ y ) ( +g ` K ) ( ( ZRHom ` K ) ` A ) ) ) )
87 86 simprd 
 |-  ( ( ph /\ y e. ( Base ` K ) ) -> ( ( O ` ( X .+ ( C ` ( ( ZRHom ` K ) ` A ) ) ) ) ` ( P .^ y ) ) = ( ( P .^ y ) ( +g ` K ) ( ( ZRHom ` K ) ` A ) ) )
88 71 87 eqtrd 
 |-  ( ( ph /\ y e. ( Base ` K ) ) -> ( ( O ` F ) ` ( P .^ y ) ) = ( ( P .^ y ) ( +g ` K ) ( ( ZRHom ` K ) ` A ) ) )
89 5 fveq2i 
 |-  ( .g ` W ) = ( .g ` ( mulGrp ` S ) )
90 9 89 eqtri 
 |-  D = ( .g ` ( mulGrp ` S ) )
91 6 fveq2i 
 |-  ( .g ` V ) = ( .g ` ( mulGrp ` K ) )
92 7 91 eqtri 
 |-  .^ = ( .g ` ( mulGrp ` K ) )
93 11 2 30 3 42 43 47 90 92 78 evl1expd 
 |-  ( ( ph /\ y e. ( Base ` K ) ) -> ( ( P D X ) e. B /\ ( ( O ` ( P D X ) ) ` y ) = ( P .^ y ) ) )
94 eqid 
 |-  ( +g ` S ) = ( +g ` S )
95 11 2 30 3 42 43 93 65 94 66 evl1addd 
 |-  ( ( ph /\ y e. ( Base ` K ) ) -> ( ( ( P D X ) ( +g ` S ) ( C ` ( ( ZRHom ` K ) ` A ) ) ) e. B /\ ( ( O ` ( ( P D X ) ( +g ` S ) ( C ` ( ( ZRHom ` K ) ` A ) ) ) ) ` y ) = ( ( P .^ y ) ( +g ` K ) ( ( ZRHom ` K ) ` A ) ) ) )
96 95 simprd 
 |-  ( ( ph /\ y e. ( Base ` K ) ) -> ( ( O ` ( ( P D X ) ( +g ` S ) ( C ` ( ( ZRHom ` K ) ` A ) ) ) ) ` y ) = ( ( P .^ y ) ( +g ` K ) ( ( ZRHom ` K ) ` A ) ) )
97 eqidd 
 |-  ( ( ph /\ y e. ( Base ` K ) ) -> ( ( P .^ y ) ( +g ` K ) ( ( ZRHom ` K ) ` A ) ) = ( ( P .^ y ) ( +g ` K ) ( ( ZRHom ` K ) ` A ) ) )
98 96 97 eqtrd 
 |-  ( ( ph /\ y e. ( Base ` K ) ) -> ( ( O ` ( ( P D X ) ( +g ` S ) ( C ` ( ( ZRHom ` K ) ` A ) ) ) ) ` y ) = ( ( P .^ y ) ( +g ` K ) ( ( ZRHom ` K ) ` A ) ) )
99 98 eqcomd 
 |-  ( ( ph /\ y e. ( Base ` K ) ) -> ( ( P .^ y ) ( +g ` K ) ( ( ZRHom ` K ) ` A ) ) = ( ( O ` ( ( P D X ) ( +g ` S ) ( C ` ( ( ZRHom ` K ) ` A ) ) ) ) ` y ) )
100 eqid 
 |-  ( C ` ( ( ZRHom ` K ) ` A ) ) = ( C ` ( ( ZRHom ` K ) ` A ) )
101 2 4 94 5 9 8 100 10 22 14 19 ply1fermltlchr 
 |-  ( ph -> ( P D ( X ( +g ` S ) ( C ` ( ( ZRHom ` K ) ` A ) ) ) ) = ( ( P D X ) ( +g ` S ) ( C ` ( ( ZRHom ` K ) ` A ) ) ) )
102 101 fveq2d 
 |-  ( ph -> ( O ` ( P D ( X ( +g ` S ) ( C ` ( ( ZRHom ` K ) ` A ) ) ) ) ) = ( O ` ( ( P D X ) ( +g ` S ) ( C ` ( ( ZRHom ` K ) ` A ) ) ) ) )
103 102 fveq1d 
 |-  ( ph -> ( ( O ` ( P D ( X ( +g ` S ) ( C ` ( ( ZRHom ` K ) ` A ) ) ) ) ) ` y ) = ( ( O ` ( ( P D X ) ( +g ` S ) ( C ` ( ( ZRHom ` K ) ` A ) ) ) ) ` y ) )
104 103 eqcomd 
 |-  ( ph -> ( ( O ` ( ( P D X ) ( +g ` S ) ( C ` ( ( ZRHom ` K ) ` A ) ) ) ) ` y ) = ( ( O ` ( P D ( X ( +g ` S ) ( C ` ( ( ZRHom ` K ) ` A ) ) ) ) ) ` y ) )
105 104 adantr 
 |-  ( ( ph /\ y e. ( Base ` K ) ) -> ( ( O ` ( ( P D X ) ( +g ` S ) ( C ` ( ( ZRHom ` K ) ` A ) ) ) ) ` y ) = ( ( O ` ( P D ( X ( +g ` S ) ( C ` ( ( ZRHom ` K ) ` A ) ) ) ) ) ` y ) )
106 11 2 30 3 42 43 47 63 94 66 evl1addd 
 |-  ( ( ph /\ y e. ( Base ` K ) ) -> ( ( X ( +g ` S ) ( C ` ( ( ZRHom ` K ) ` A ) ) ) e. B /\ ( ( O ` ( X ( +g ` S ) ( C ` ( ( ZRHom ` K ) ` A ) ) ) ) ` y ) = ( y ( +g ` K ) ( ( ZRHom ` K ) ` A ) ) ) )
107 11 2 30 3 42 43 106 90 92 78 evl1expd 
 |-  ( ( ph /\ y e. ( Base ` K ) ) -> ( ( P D ( X ( +g ` S ) ( C ` ( ( ZRHom ` K ) ` A ) ) ) ) e. B /\ ( ( O ` ( P D ( X ( +g ` S ) ( C ` ( ( ZRHom ` K ) ` A ) ) ) ) ) ` y ) = ( P .^ ( y ( +g ` K ) ( ( ZRHom ` K ) ` A ) ) ) ) )
108 107 simprd 
 |-  ( ( ph /\ y e. ( Base ` K ) ) -> ( ( O ` ( P D ( X ( +g ` S ) ( C ` ( ( ZRHom ` K ) ` A ) ) ) ) ) ` y ) = ( P .^ ( y ( +g ` K ) ( ( ZRHom ` K ) ` A ) ) ) )
109 99 105 108 3eqtrd 
 |-  ( ( ph /\ y e. ( Base ` K ) ) -> ( ( P .^ y ) ( +g ` K ) ( ( ZRHom ` K ) ` A ) ) = ( P .^ ( y ( +g ` K ) ( ( ZRHom ` K ) ` A ) ) ) )
110 88 109 eqtrd 
 |-  ( ( ph /\ y e. ( Base ` K ) ) -> ( ( O ` F ) ` ( P .^ y ) ) = ( P .^ ( y ( +g ` K ) ( ( ZRHom ` K ) ` A ) ) ) )
111 110 eqcomd 
 |-  ( ( ph /\ y e. ( Base ` K ) ) -> ( P .^ ( y ( +g ` K ) ( ( ZRHom ` K ) ` A ) ) ) = ( ( O ` F ) ` ( P .^ y ) ) )
112 70 111 eqtrd 
 |-  ( ( ph /\ y e. ( Base ` K ) ) -> ( P .^ ( ( O ` F ) ` y ) ) = ( ( O ` F ) ` ( P .^ y ) ) )
113 112 adantlr 
 |-  ( ( ( ph /\ y e. ( V PrimRoots R ) ) /\ y e. ( Base ` K ) ) -> ( P .^ ( ( O ` F ) ` y ) ) = ( ( O ` F ) ` ( P .^ y ) ) )
114 113 ex 
 |-  ( ( ph /\ y e. ( V PrimRoots R ) ) -> ( y e. ( Base ` K ) -> ( P .^ ( ( O ` F ) ` y ) ) = ( ( O ` F ) ` ( P .^ y ) ) ) )
115 114 ex 
 |-  ( ph -> ( y e. ( V PrimRoots R ) -> ( y e. ( Base ` K ) -> ( P .^ ( ( O ` F ) ` y ) ) = ( ( O ` F ) ` ( P .^ y ) ) ) ) )
116 37 115 mpdd 
 |-  ( ph -> ( y e. ( V PrimRoots R ) -> ( P .^ ( ( O ` F ) ` y ) ) = ( ( O ` F ) ` ( P .^ y ) ) ) )
117 116 imp 
 |-  ( ( ph /\ y e. ( V PrimRoots R ) ) -> ( P .^ ( ( O ` F ) ` y ) ) = ( ( O ` F ) ` ( P .^ y ) ) )
118 117 ralrimiva 
 |-  ( ph -> A. y e. ( V PrimRoots R ) ( P .^ ( ( O ` F ) ` y ) ) = ( ( O ` F ) ` ( P .^ y ) ) )
119 2 ply1crng 
 |-  ( K e. CRing -> S e. CRing )
120 22 119 syl 
 |-  ( ph -> S e. CRing )
121 crngring 
 |-  ( S e. CRing -> S e. Ring )
122 120 121 syl 
 |-  ( ph -> S e. Ring )
123 122 ringgrpd 
 |-  ( ph -> S e. Grp )
124 51 45 syl 
 |-  ( ph -> X e. B )
125 123 124 60 3jca 
 |-  ( ph -> ( S e. Grp /\ X e. B /\ ( C ` ( ( ZRHom ` K ) ` A ) ) e. B ) )
126 3 12 grpcl 
 |-  ( ( S e. Grp /\ X e. B /\ ( C ` ( ( ZRHom ` K ) ` A ) ) e. B ) -> ( X .+ ( C ` ( ( ZRHom ` K ) ` A ) ) ) e. B )
127 125 126 syl 
 |-  ( ph -> ( X .+ ( C ` ( ( ZRHom ` K ) ` A ) ) ) e. B )
128 18 a1i 
 |-  ( ph -> F = ( X .+ ( C ` ( ( ZRHom ` K ) ` A ) ) ) )
129 128 eleq1d 
 |-  ( ph -> ( F e. B <-> ( X .+ ( C ` ( ( ZRHom ` K ) ` A ) ) ) e. B ) )
130 127 129 mpbird 
 |-  ( ph -> F e. B )
131 1 130 76 aks6d1c1p1 
 |-  ( ph -> ( P .~ F <-> A. y e. ( V PrimRoots R ) ( P .^ ( ( O ` F ) ` y ) ) = ( ( O ` F ) ` ( P .^ y ) ) ) )
132 118 131 mpbird 
 |-  ( ph -> P .~ F )