Metamath Proof Explorer

Theorem aks6d1c1p3

Description: In a field with a Frobenius isomorphism (read: algebraic closure or finite field), N and linear factors are introspective. (Contributed by metakunt, 25-Apr-2025)

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

Proof

Step Hyp Ref Expression
1 aks6d1c1p3.1 
 |-  .~ = { <. e , f >. | ( e e. NN /\ f e. B /\ A. y e. ( V PrimRoots R ) ( e .^ ( ( O ` f ) ` y ) ) = ( ( O ` f ) ` ( e .^ y ) ) ) }
2 aks6d1c1p3.2 
 |-  S = ( Poly1 ` K )
3 aks6d1c1p3.3 
 |-  B = ( Base ` S )
4 aks6d1c1p3.4 
 |-  X = ( var1 ` K )
5 aks6d1c1p3.5 
 |-  W = ( mulGrp ` S )
6 aks6d1c1p3.6 
 |-  V = ( mulGrp ` K )
7 aks6d1c1p3.7 
 |-  .^ = ( .g ` V )
8 aks6d1c1p3.8 
 |-  C = ( algSc ` S )
9 aks6d1c1p3.9 
 |-  D = ( .g ` W )
10 aks6d1c1p3.10 
 |-  P = ( chr ` K )
11 aks6d1c1p3.11 
 |-  O = ( eval1 ` K )
12 aks6d1c1p3.12 
 |-  .+ = ( +g ` S )
13 aks6d1c1p3.13 
 |-  ( ph -> K e. Field )
14 aks6d1c1p3.14 
 |-  ( ph -> P e. Prime )
15 aks6d1c1p3.15 
 |-  ( ph -> R e. NN )
16 aks6d1c1p3.16 
 |-  ( ph -> ( N gcd R ) = 1 )
17 aks6d1c1p3.17 
 |-  ( ph -> P || N )
18 aks6d1c1p3.18 
 |-  F = ( X .+ ( C ` ( ( ZRHom ` K ) ` A ) ) )
19 aks6d1c1p3.19 
 |-  ( ph -> A e. ZZ )
20 aks6d1c1p3.20 
 |-  ( ph -> N .~ F )
21 aks6d1c1p3.21 
 |-  ( ph -> ( x e. ( Base ` K ) |-> ( P .^ x ) ) e. ( K RingIso K ) )
22 18 a1i 
 |-  ( ( ph /\ y e. ( V PrimRoots R ) ) -> F = ( X .+ ( C ` ( ( ZRHom ` K ) ` A ) ) ) )
23 22 fveq2d 
 |-  ( ( ph /\ y e. ( V PrimRoots R ) ) -> ( O ` F ) = ( O ` ( X .+ ( C ` ( ( ZRHom ` K ) ` A ) ) ) ) )
24 23 fveq1d 
 |-  ( ( ph /\ y e. ( V PrimRoots R ) ) -> ( ( O ` F ) ` ( ( N / P ) .^ y ) ) = ( ( O ` ( X .+ ( C ` ( ( ZRHom ` K ) ` A ) ) ) ) ` ( ( N / P ) .^ y ) ) )
25 eqid 
 |-  ( Base ` K ) = ( Base ` K )
26 13 fldcrngd 
 |-  ( ph -> K e. CRing )
27 26 adantr 
 |-  ( ( ph /\ y e. ( V PrimRoots R ) ) -> K e. CRing )
28 eqid 
 |-  ( Base ` V ) = ( Base ` V )
29 6 crngmgp 
 |-  ( K e. CRing -> V e. CMnd )
30 26 29 syl 
 |-  ( ph -> V e. CMnd )
31 30 cmnmndd 
 |-  ( ph -> V e. Mnd )
32 31 adantr 
 |-  ( ( ph /\ y e. ( V PrimRoots R ) ) -> V e. Mnd )
33 1 20 aks6d1c1p1rcl 
 |-  ( ph -> ( N e. NN /\ F e. B ) )
34 33 simpld 
 |-  ( ph -> N e. NN )
35 prmnn 
 |-  ( P e. Prime -> P e. NN )
36 14 35 syl 
 |-  ( ph -> P e. NN )
37 nndivdvds 
 |-  ( ( N e. NN /\ P e. NN ) -> ( P || N <-> ( N / P ) e. NN ) )
38 34 36 37 syl2anc 
 |-  ( ph -> ( P || N <-> ( N / P ) e. NN ) )
39 17 38 mpbid 
 |-  ( ph -> ( N / P ) e. NN )
40 39 nnnn0d 
 |-  ( ph -> ( N / P ) e. NN0 )
41 40 adantr 
 |-  ( ( ph /\ y e. ( V PrimRoots R ) ) -> ( N / P ) e. NN0 )
42 15 nnnn0d 
 |-  ( ph -> R e. NN0 )
43 30 42 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 ) ) ) )
44 43 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 ) ) ) )
45 44 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 ) ) )
46 45 simp1d 
 |-  ( ( ph /\ y e. ( V PrimRoots R ) ) -> y e. ( Base ` V ) )
47 28 7 32 41 46 mulgnn0cld 
 |-  ( ( ph /\ y e. ( V PrimRoots R ) ) -> ( ( N / P ) .^ y ) e. ( Base ` V ) )
48 6 25 mgpbas 
 |-  ( Base ` K ) = ( Base ` V )
49 48 eqcomi 
 |-  ( Base ` V ) = ( Base ` K )
50 49 a1i 
 |-  ( ph -> ( Base ` V ) = ( Base ` K ) )
51 50 adantr 
 |-  ( ( ph /\ y e. ( V PrimRoots R ) ) -> ( Base ` V ) = ( Base ` K ) )
52 47 51 eleqtrd 
 |-  ( ( ph /\ y e. ( V PrimRoots R ) ) -> ( ( N / P ) .^ y ) e. ( Base ` K ) )
53 11 4 25 2 3 27 52 evl1vard 
 |-  ( ( ph /\ y e. ( V PrimRoots R ) ) -> ( X e. B /\ ( ( O ` X ) ` ( ( N / P ) .^ y ) ) = ( ( N / P ) .^ y ) ) )
54 26 crngringd 
 |-  ( ph -> K e. Ring )
55 eqid 
 |-  ( ZRHom ` K ) = ( ZRHom ` K )
56 55 zrhrhm 
 |-  ( K e. Ring -> ( ZRHom ` K ) e. ( ZZring RingHom K ) )
57 rhmghm 
 |-  ( ( ZRHom ` K ) e. ( ZZring RingHom K ) -> ( ZRHom ` K ) e. ( ZZring GrpHom K ) )
58 zringbas 
 |-  ZZ = ( Base ` ZZring )
59 58 25 ghmf 
 |-  ( ( ZRHom ` K ) e. ( ZZring GrpHom K ) -> ( ZRHom ` K ) : ZZ --> ( Base ` K ) )
60 54 56 57 59 4syl 
 |-  ( ph -> ( ZRHom ` K ) : ZZ --> ( Base ` K ) )
61 60 19 ffvelcdmd 
 |-  ( ph -> ( ( ZRHom ` K ) ` A ) e. ( Base ` K ) )
62 61 adantr 
 |-  ( ( ph /\ y e. ( V PrimRoots R ) ) -> ( ( ZRHom ` K ) ` A ) e. ( Base ` K ) )
63 11 2 25 8 3 27 62 52 evl1scad 
 |-  ( ( ph /\ y e. ( V PrimRoots R ) ) -> ( ( C ` ( ( ZRHom ` K ) ` A ) ) e. B /\ ( ( O ` ( C ` ( ( ZRHom ` K ) ` A ) ) ) ` ( ( N / P ) .^ y ) ) = ( ( ZRHom ` K ) ` A ) ) )
64 eqid 
 |-  ( +g ` K ) = ( +g ` K )
65 11 2 25 3 27 52 53 63 12 64 evl1addd 
 |-  ( ( ph /\ y e. ( V PrimRoots R ) ) -> ( ( X .+ ( C ` ( ( ZRHom ` K ) ` A ) ) ) e. B /\ ( ( O ` ( X .+ ( C ` ( ( ZRHom ` K ) ` A ) ) ) ) ` ( ( N / P ) .^ y ) ) = ( ( ( N / P ) .^ y ) ( +g ` K ) ( ( ZRHom ` K ) ` A ) ) ) )
66 65 simprd 
 |-  ( ( ph /\ y e. ( V PrimRoots R ) ) -> ( ( O ` ( X .+ ( C ` ( ( ZRHom ` K ) ` A ) ) ) ) ` ( ( N / P ) .^ y ) ) = ( ( ( N / P ) .^ y ) ( +g ` K ) ( ( ZRHom ` K ) ` A ) ) )
67 24 66 eqtrd 
 |-  ( ( ph /\ y e. ( V PrimRoots R ) ) -> ( ( O ` F ) ` ( ( N / P ) .^ y ) ) = ( ( ( N / P ) .^ y ) ( +g ` K ) ( ( ZRHom ` K ) ` A ) ) )
68 23 fveq1d 
 |-  ( ( ph /\ y e. ( V PrimRoots R ) ) -> ( ( O ` F ) ` y ) = ( ( O ` ( X .+ ( C ` ( ( ZRHom ` K ) ` A ) ) ) ) ` y ) )
69 68 oveq2d 
 |-  ( ( ph /\ y e. ( V PrimRoots R ) ) -> ( ( N / P ) .^ ( ( O ` F ) ` y ) ) = ( ( N / P ) .^ ( ( O ` ( X .+ ( C ` ( ( ZRHom ` K ) ` A ) ) ) ) ` y ) ) )
70 51 eleq2d 
 |-  ( ( ph /\ y e. ( V PrimRoots R ) ) -> ( y e. ( Base ` V ) <-> y e. ( Base ` K ) ) )
71 46 70 mpbid 
 |-  ( ( ph /\ y e. ( V PrimRoots R ) ) -> y e. ( Base ` K ) )
72 11 4 49 2 3 27 46 evl1vard 
 |-  ( ( ph /\ y e. ( V PrimRoots R ) ) -> ( X e. B /\ ( ( O ` X ) ` y ) = y ) )
73 11 2 25 8 3 27 62 71 evl1scad 
 |-  ( ( ph /\ y e. ( V PrimRoots R ) ) -> ( ( C ` ( ( ZRHom ` K ) ` A ) ) e. B /\ ( ( O ` ( C ` ( ( ZRHom ` K ) ` A ) ) ) ` y ) = ( ( ZRHom ` K ) ` A ) ) )
74 11 2 25 3 27 71 72 73 12 64 evl1addd 
 |-  ( ( ph /\ y e. ( V PrimRoots R ) ) -> ( ( X .+ ( C ` ( ( ZRHom ` K ) ` A ) ) ) e. B /\ ( ( O ` ( X .+ ( C ` ( ( ZRHom ` K ) ` A ) ) ) ) ` y ) = ( y ( +g ` K ) ( ( ZRHom ` K ) ` A ) ) ) )
75 74 simprd 
 |-  ( ( ph /\ y e. ( V PrimRoots R ) ) -> ( ( O ` ( X .+ ( C ` ( ( ZRHom ` K ) ` A ) ) ) ) ` y ) = ( y ( +g ` K ) ( ( ZRHom ` K ) ` A ) ) )
76 75 oveq2d 
 |-  ( ( ph /\ y e. ( V PrimRoots R ) ) -> ( ( N / P ) .^ ( ( O ` ( X .+ ( C ` ( ( ZRHom ` K ) ` A ) ) ) ) ` y ) ) = ( ( N / P ) .^ ( y ( +g ` K ) ( ( ZRHom ` K ) ` A ) ) ) )
77 69 76 eqtrd 
 |-  ( ( ph /\ y e. ( V PrimRoots R ) ) -> ( ( N / P ) .^ ( ( O ` F ) ` y ) ) = ( ( N / P ) .^ ( y ( +g ` K ) ( ( ZRHom ` K ) ` A ) ) ) )
78 25 25 isrim 
 |-  ( ( x e. ( Base ` K ) |-> ( P .^ x ) ) e. ( K RingIso K ) <-> ( ( x e. ( Base ` K ) |-> ( P .^ x ) ) e. ( K RingHom K ) /\ ( x e. ( Base ` K ) |-> ( P .^ x ) ) : ( Base ` K ) -1-1-onto-> ( Base ` K ) ) )
79 21 78 sylib 
 |-  ( ph -> ( ( x e. ( Base ` K ) |-> ( P .^ x ) ) e. ( K RingHom K ) /\ ( x e. ( Base ` K ) |-> ( P .^ x ) ) : ( Base ` K ) -1-1-onto-> ( Base ` K ) ) )
80 79 simprd 
 |-  ( ph -> ( x e. ( Base ` K ) |-> ( P .^ x ) ) : ( Base ` K ) -1-1-onto-> ( Base ` K ) )
81 80 adantr 
 |-  ( ( ph /\ y e. ( V PrimRoots R ) ) -> ( x e. ( Base ` K ) |-> ( P .^ x ) ) : ( Base ` K ) -1-1-onto-> ( Base ` K ) )
82 27 crnggrpd 
 |-  ( ( ph /\ y e. ( V PrimRoots R ) ) -> K e. Grp )
83 25 64 82 52 62 grpcld 
 |-  ( ( ph /\ y e. ( V PrimRoots R ) ) -> ( ( ( N / P ) .^ y ) ( +g ` K ) ( ( ZRHom ` K ) ` A ) ) e. ( Base ` K ) )
84 f1ocnvfv1 
 |-  ( ( ( x e. ( Base ` K ) |-> ( P .^ x ) ) : ( Base ` K ) -1-1-onto-> ( Base ` K ) /\ ( ( ( N / P ) .^ y ) ( +g ` K ) ( ( ZRHom ` K ) ` A ) ) e. ( Base ` K ) ) -> ( `' ( x e. ( Base ` K ) |-> ( P .^ x ) ) ` ( ( x e. ( Base ` K ) |-> ( P .^ x ) ) ` ( ( ( N / P ) .^ y ) ( +g ` K ) ( ( ZRHom ` K ) ` A ) ) ) ) = ( ( ( N / P ) .^ y ) ( +g ` K ) ( ( ZRHom ` K ) ` A ) ) )
85 81 83 84 syl2anc 
 |-  ( ( ph /\ y e. ( V PrimRoots R ) ) -> ( `' ( x e. ( Base ` K ) |-> ( P .^ x ) ) ` ( ( x e. ( Base ` K ) |-> ( P .^ x ) ) ` ( ( ( N / P ) .^ y ) ( +g ` K ) ( ( ZRHom ` K ) ` A ) ) ) ) = ( ( ( N / P ) .^ y ) ( +g ` K ) ( ( ZRHom ` K ) ` A ) ) )
86 85 eqcomd 
 |-  ( ( ph /\ y e. ( V PrimRoots R ) ) -> ( ( ( N / P ) .^ y ) ( +g ` K ) ( ( ZRHom ` K ) ` A ) ) = ( `' ( x e. ( Base ` K ) |-> ( P .^ x ) ) ` ( ( x e. ( Base ` K ) |-> ( P .^ x ) ) ` ( ( ( N / P ) .^ y ) ( +g ` K ) ( ( ZRHom ` K ) ` A ) ) ) ) )
87 eqidd 
 |-  ( ( ph /\ y e. ( V PrimRoots R ) ) -> ( x e. ( Base ` K ) |-> ( P .^ x ) ) = ( x e. ( Base ` K ) |-> ( P .^ x ) ) )
88 id 
 |-  ( x = ( ( ( N / P ) .^ y ) ( +g ` K ) ( ( ZRHom ` K ) ` A ) ) -> x = ( ( ( N / P ) .^ y ) ( +g ` K ) ( ( ZRHom ` K ) ` A ) ) )
89 88 adantl 
 |-  ( ( ( ph /\ y e. ( V PrimRoots R ) ) /\ x = ( ( ( N / P ) .^ y ) ( +g ` K ) ( ( ZRHom ` K ) ` A ) ) ) -> x = ( ( ( N / P ) .^ y ) ( +g ` K ) ( ( ZRHom ` K ) ` A ) ) )
90 89 oveq2d 
 |-  ( ( ( ph /\ y e. ( V PrimRoots R ) ) /\ x = ( ( ( N / P ) .^ y ) ( +g ` K ) ( ( ZRHom ` K ) ` A ) ) ) -> ( P .^ x ) = ( P .^ ( ( ( N / P ) .^ y ) ( +g ` K ) ( ( ZRHom ` K ) ` A ) ) ) )
91 eqid 
 |-  ( mulGrp ` K ) = ( mulGrp ` K )
92 91 25 mgpbas 
 |-  ( Base ` K ) = ( Base ` ( mulGrp ` K ) )
93 6 fveq2i 
 |-  ( .g ` V ) = ( .g ` ( mulGrp ` K ) )
94 7 93 eqtri 
 |-  .^ = ( .g ` ( mulGrp ` K ) )
95 91 ringmgp 
 |-  ( K e. Ring -> ( mulGrp ` K ) e. Mnd )
96 54 95 syl 
 |-  ( ph -> ( mulGrp ` K ) e. Mnd )
97 96 adantr 
 |-  ( ( ph /\ y e. ( V PrimRoots R ) ) -> ( mulGrp ` K ) e. Mnd )
98 36 nnnn0d 
 |-  ( ph -> P e. NN0 )
99 98 adantr 
 |-  ( ( ph /\ y e. ( V PrimRoots R ) ) -> P e. NN0 )
100 92 94 97 99 83 mulgnn0cld 
 |-  ( ( ph /\ y e. ( V PrimRoots R ) ) -> ( P .^ ( ( ( N / P ) .^ y ) ( +g ` K ) ( ( ZRHom ` K ) ` A ) ) ) e. ( Base ` K ) )
101 87 90 83 100 fvmptd 
 |-  ( ( ph /\ y e. ( V PrimRoots R ) ) -> ( ( x e. ( Base ` K ) |-> ( P .^ x ) ) ` ( ( ( N / P ) .^ y ) ( +g ` K ) ( ( ZRHom ` K ) ` A ) ) ) = ( P .^ ( ( ( N / P ) .^ y ) ( +g ` K ) ( ( ZRHom ` K ) ` A ) ) ) )
102 101 eqcomd 
 |-  ( ( ph /\ y e. ( V PrimRoots R ) ) -> ( P .^ ( ( ( N / P ) .^ y ) ( +g ` K ) ( ( ZRHom ` K ) ` A ) ) ) = ( ( x e. ( Base ` K ) |-> ( P .^ x ) ) ` ( ( ( N / P ) .^ y ) ( +g ` K ) ( ( ZRHom ` K ) ` A ) ) ) )
103 79 simpld 
 |-  ( ph -> ( x e. ( Base ` K ) |-> ( P .^ x ) ) e. ( K RingHom K ) )
104 rhmghm 
 |-  ( ( x e. ( Base ` K ) |-> ( P .^ x ) ) e. ( K RingHom K ) -> ( x e. ( Base ` K ) |-> ( P .^ x ) ) e. ( K GrpHom K ) )
105 103 104 syl 
 |-  ( ph -> ( x e. ( Base ` K ) |-> ( P .^ x ) ) e. ( K GrpHom K ) )
106 105 adantr 
 |-  ( ( ph /\ y e. ( V PrimRoots R ) ) -> ( x e. ( Base ` K ) |-> ( P .^ x ) ) e. ( K GrpHom K ) )
107 25 64 64 ghmlin 
 |-  ( ( ( x e. ( Base ` K ) |-> ( P .^ x ) ) e. ( K GrpHom K ) /\ ( ( N / P ) .^ y ) e. ( Base ` K ) /\ ( ( ZRHom ` K ) ` A ) e. ( Base ` K ) ) -> ( ( x e. ( Base ` K ) |-> ( P .^ x ) ) ` ( ( ( N / P ) .^ y ) ( +g ` K ) ( ( ZRHom ` K ) ` A ) ) ) = ( ( ( x e. ( Base ` K ) |-> ( P .^ x ) ) ` ( ( N / P ) .^ y ) ) ( +g ` K ) ( ( x e. ( Base ` K ) |-> ( P .^ x ) ) ` ( ( ZRHom ` K ) ` A ) ) ) )
108 106 52 62 107 syl3anc 
 |-  ( ( ph /\ y e. ( V PrimRoots R ) ) -> ( ( x e. ( Base ` K ) |-> ( P .^ x ) ) ` ( ( ( N / P ) .^ y ) ( +g ` K ) ( ( ZRHom ` K ) ` A ) ) ) = ( ( ( x e. ( Base ` K ) |-> ( P .^ x ) ) ` ( ( N / P ) .^ y ) ) ( +g ` K ) ( ( x e. ( Base ` K ) |-> ( P .^ x ) ) ` ( ( ZRHom ` K ) ` A ) ) ) )
109 id 
 |-  ( x = ( ( N / P ) .^ y ) -> x = ( ( N / P ) .^ y ) )
110 109 adantl 
 |-  ( ( ( ph /\ y e. ( V PrimRoots R ) ) /\ x = ( ( N / P ) .^ y ) ) -> x = ( ( N / P ) .^ y ) )
111 110 oveq2d 
 |-  ( ( ( ph /\ y e. ( V PrimRoots R ) ) /\ x = ( ( N / P ) .^ y ) ) -> ( P .^ x ) = ( P .^ ( ( N / P ) .^ y ) ) )
112 92 94 97 99 52 mulgnn0cld 
 |-  ( ( ph /\ y e. ( V PrimRoots R ) ) -> ( P .^ ( ( N / P ) .^ y ) ) e. ( Base ` K ) )
113 87 111 52 112 fvmptd 
 |-  ( ( ph /\ y e. ( V PrimRoots R ) ) -> ( ( x e. ( Base ` K ) |-> ( P .^ x ) ) ` ( ( N / P ) .^ y ) ) = ( P .^ ( ( N / P ) .^ y ) ) )
114 id 
 |-  ( x = ( ( ZRHom ` K ) ` A ) -> x = ( ( ZRHom ` K ) ` A ) )
115 114 oveq2d 
 |-  ( x = ( ( ZRHom ` K ) ` A ) -> ( P .^ x ) = ( P .^ ( ( ZRHom ` K ) ` A ) ) )
116 115 adantl 
 |-  ( ( ( ph /\ y e. ( V PrimRoots R ) ) /\ x = ( ( ZRHom ` K ) ` A ) ) -> ( P .^ x ) = ( P .^ ( ( ZRHom ` K ) ` A ) ) )
117 eqid 
 |-  ( ( ZRHom ` K ) ` A ) = ( ( ZRHom ` K ) ` A )
118 10 25 94 117 14 19 26 fermltlchr 
 |-  ( ph -> ( P .^ ( ( ZRHom ` K ) ` A ) ) = ( ( ZRHom ` K ) ` A ) )
119 118 eqcomd 
 |-  ( ph -> ( ( ZRHom ` K ) ` A ) = ( P .^ ( ( ZRHom ` K ) ` A ) ) )
120 119 adantr 
 |-  ( ( ph /\ y e. ( V PrimRoots R ) ) -> ( ( ZRHom ` K ) ` A ) = ( P .^ ( ( ZRHom ` K ) ` A ) ) )
121 120 62 eqeltrrd 
 |-  ( ( ph /\ y e. ( V PrimRoots R ) ) -> ( P .^ ( ( ZRHom ` K ) ` A ) ) e. ( Base ` K ) )
122 87 116 62 121 fvmptd 
 |-  ( ( ph /\ y e. ( V PrimRoots R ) ) -> ( ( x e. ( Base ` K ) |-> ( P .^ x ) ) ` ( ( ZRHom ` K ) ` A ) ) = ( P .^ ( ( ZRHom ` K ) ` A ) ) )
123 113 122 oveq12d 
 |-  ( ( ph /\ y e. ( V PrimRoots R ) ) -> ( ( ( x e. ( Base ` K ) |-> ( P .^ x ) ) ` ( ( N / P ) .^ y ) ) ( +g ` K ) ( ( x e. ( Base ` K ) |-> ( P .^ x ) ) ` ( ( ZRHom ` K ) ` A ) ) ) = ( ( P .^ ( ( N / P ) .^ y ) ) ( +g ` K ) ( P .^ ( ( ZRHom ` K ) ` A ) ) ) )
124 102 108 123 3eqtrd 
 |-  ( ( ph /\ y e. ( V PrimRoots R ) ) -> ( P .^ ( ( ( N / P ) .^ y ) ( +g ` K ) ( ( ZRHom ` K ) ` A ) ) ) = ( ( P .^ ( ( N / P ) .^ y ) ) ( +g ` K ) ( P .^ ( ( ZRHom ` K ) ` A ) ) ) )
125 34 nncnd 
 |-  ( ph -> N e. CC )
126 125 adantr 
 |-  ( ( ph /\ y e. ( V PrimRoots R ) ) -> N e. CC )
127 36 nncnd 
 |-  ( ph -> P e. CC )
128 127 adantr 
 |-  ( ( ph /\ y e. ( V PrimRoots R ) ) -> P e. CC )
129 36 nnne0d 
 |-  ( ph -> P =/= 0 )
130 129 adantr 
 |-  ( ( ph /\ y e. ( V PrimRoots R ) ) -> P =/= 0 )
131 126 128 130 divcan2d 
 |-  ( ( ph /\ y e. ( V PrimRoots R ) ) -> ( P x. ( N / P ) ) = N )
132 131 oveq1d 
 |-  ( ( ph /\ y e. ( V PrimRoots R ) ) -> ( ( P x. ( N / P ) ) .^ ( y ( +g ` K ) ( ( ZRHom ` K ) ` A ) ) ) = ( N .^ ( y ( +g ` K ) ( ( ZRHom ` K ) ` A ) ) ) )
133 68 oveq2d 
 |-  ( ( ph /\ y e. ( V PrimRoots R ) ) -> ( N .^ ( ( O ` F ) ` y ) ) = ( N .^ ( ( O ` ( X .+ ( C ` ( ( ZRHom ` K ) ` A ) ) ) ) ` y ) ) )
134 75 oveq2d 
 |-  ( ( ph /\ y e. ( V PrimRoots R ) ) -> ( N .^ ( ( O ` ( X .+ ( C ` ( ( ZRHom ` K ) ` A ) ) ) ) ` y ) ) = ( N .^ ( y ( +g ` K ) ( ( ZRHom ` K ) ` A ) ) ) )
135 133 134 eqtrd 
 |-  ( ( ph /\ y e. ( V PrimRoots R ) ) -> ( N .^ ( ( O ` F ) ` y ) ) = ( N .^ ( y ( +g ` K ) ( ( ZRHom ` K ) ` A ) ) ) )
136 135 eqcomd 
 |-  ( ( ph /\ y e. ( V PrimRoots R ) ) -> ( N .^ ( y ( +g ` K ) ( ( ZRHom ` K ) ` A ) ) ) = ( N .^ ( ( O ` F ) ` y ) ) )
137 fveq2 
 |-  ( z = y -> ( ( O ` F ) ` z ) = ( ( O ` F ) ` y ) )
138 137 oveq2d 
 |-  ( z = y -> ( N .^ ( ( O ` F ) ` z ) ) = ( N .^ ( ( O ` F ) ` y ) ) )
139 oveq2 
 |-  ( z = y -> ( N .^ z ) = ( N .^ y ) )
140 139 fveq2d 
 |-  ( z = y -> ( ( O ` F ) ` ( N .^ z ) ) = ( ( O ` F ) ` ( N .^ y ) ) )
141 138 140 eqeq12d 
 |-  ( z = y -> ( ( N .^ ( ( O ` F ) ` z ) ) = ( ( O ` F ) ` ( N .^ z ) ) <-> ( N .^ ( ( O ` F ) ` y ) ) = ( ( O ` F ) ` ( N .^ y ) ) ) )
142 2 ply1crng 
 |-  ( K e. CRing -> S e. CRing )
143 26 142 syl 
 |-  ( ph -> S e. CRing )
144 143 crnggrpd 
 |-  ( ph -> S e. Grp )
145 4 2 3 vr1cl 
 |-  ( K e. Ring -> X e. B )
146 54 145 syl 
 |-  ( ph -> X e. B )
147 2 8 25 3 ply1sclcl 
 |-  ( ( K e. Ring /\ ( ( ZRHom ` K ) ` A ) e. ( Base ` K ) ) -> ( C ` ( ( ZRHom ` K ) ` A ) ) e. B )
148 54 61 147 syl2anc 
 |-  ( ph -> ( C ` ( ( ZRHom ` K ) ` A ) ) e. B )
149 144 146 148 3jca 
 |-  ( ph -> ( S e. Grp /\ X e. B /\ ( C ` ( ( ZRHom ` K ) ` A ) ) e. B ) )
150 3 12 grpcl 
 |-  ( ( S e. Grp /\ X e. B /\ ( C ` ( ( ZRHom ` K ) ` A ) ) e. B ) -> ( X .+ ( C ` ( ( ZRHom ` K ) ` A ) ) ) e. B )
151 149 150 syl 
 |-  ( ph -> ( X .+ ( C ` ( ( ZRHom ` K ) ` A ) ) ) e. B )
152 18 a1i 
 |-  ( ph -> F = ( X .+ ( C ` ( ( ZRHom ` K ) ` A ) ) ) )
153 152 eleq1d 
 |-  ( ph -> ( F e. B <-> ( X .+ ( C ` ( ( ZRHom ` K ) ` A ) ) ) e. B ) )
154 151 153 mpbird 
 |-  ( ph -> F e. B )
155 1 154 34 aks6d1c1p1 
 |-  ( ph -> ( N .~ F <-> A. y e. ( V PrimRoots R ) ( N .^ ( ( O ` F ) ` y ) ) = ( ( O ` F ) ` ( N .^ y ) ) ) )
156 20 155 mpbid 
 |-  ( ph -> A. y e. ( V PrimRoots R ) ( N .^ ( ( O ` F ) ` y ) ) = ( ( O ` F ) ` ( N .^ y ) ) )
157 fveq2 
 |-  ( y = z -> ( ( O ` F ) ` y ) = ( ( O ` F ) ` z ) )
158 157 oveq2d 
 |-  ( y = z -> ( N .^ ( ( O ` F ) ` y ) ) = ( N .^ ( ( O ` F ) ` z ) ) )
159 oveq2 
 |-  ( y = z -> ( N .^ y ) = ( N .^ z ) )
160 159 fveq2d 
 |-  ( y = z -> ( ( O ` F ) ` ( N .^ y ) ) = ( ( O ` F ) ` ( N .^ z ) ) )
161 158 160 eqeq12d 
 |-  ( y = z -> ( ( N .^ ( ( O ` F ) ` y ) ) = ( ( O ` F ) ` ( N .^ y ) ) <-> ( N .^ ( ( O ` F ) ` z ) ) = ( ( O ` F ) ` ( N .^ z ) ) ) )
162 161 cbvralvw 
 |-  ( A. y e. ( V PrimRoots R ) ( N .^ ( ( O ` F ) ` y ) ) = ( ( O ` F ) ` ( N .^ y ) ) <-> A. z e. ( V PrimRoots R ) ( N .^ ( ( O ` F ) ` z ) ) = ( ( O ` F ) ` ( N .^ z ) ) )
163 156 162 sylib 
 |-  ( ph -> A. z e. ( V PrimRoots R ) ( N .^ ( ( O ` F ) ` z ) ) = ( ( O ` F ) ` ( N .^ z ) ) )
164 163 adantr 
 |-  ( ( ph /\ y e. ( V PrimRoots R ) ) -> A. z e. ( V PrimRoots R ) ( N .^ ( ( O ` F ) ` z ) ) = ( ( O ` F ) ` ( N .^ z ) ) )
165 simpr 
 |-  ( ( ph /\ y e. ( V PrimRoots R ) ) -> y e. ( V PrimRoots R ) )
166 141 164 165 rspcdva 
 |-  ( ( ph /\ y e. ( V PrimRoots R ) ) -> ( N .^ ( ( O ` F ) ` y ) ) = ( ( O ` F ) ` ( N .^ y ) ) )
167 23 fveq1d 
 |-  ( ( ph /\ y e. ( V PrimRoots R ) ) -> ( ( O ` F ) ` ( N .^ y ) ) = ( ( O ` ( X .+ ( C ` ( ( ZRHom ` K ) ` A ) ) ) ) ` ( N .^ y ) ) )
168 34 nnnn0d 
 |-  ( ph -> N e. NN0 )
169 168 adantr 
 |-  ( ( ph /\ y e. ( V PrimRoots R ) ) -> N e. NN0 )
170 28 7 32 169 46 mulgnn0cld 
 |-  ( ( ph /\ y e. ( V PrimRoots R ) ) -> ( N .^ y ) e. ( Base ` V ) )
171 170 51 eleqtrd 
 |-  ( ( ph /\ y e. ( V PrimRoots R ) ) -> ( N .^ y ) e. ( Base ` K ) )
172 146 adantr 
 |-  ( ( ph /\ y e. ( V PrimRoots R ) ) -> X e. B )
173 11 4 25 2 3 27 171 evl1vard 
 |-  ( ( ph /\ y e. ( V PrimRoots R ) ) -> ( X e. B /\ ( ( O ` X ) ` ( N .^ y ) ) = ( N .^ y ) ) )
174 173 simprd 
 |-  ( ( ph /\ y e. ( V PrimRoots R ) ) -> ( ( O ` X ) ` ( N .^ y ) ) = ( N .^ y ) )
175 172 174 jca 
 |-  ( ( ph /\ y e. ( V PrimRoots R ) ) -> ( X e. B /\ ( ( O ` X ) ` ( N .^ y ) ) = ( N .^ y ) ) )
176 148 adantr 
 |-  ( ( ph /\ y e. ( V PrimRoots R ) ) -> ( C ` ( ( ZRHom ` K ) ` A ) ) e. B )
177 11 2 25 8 3 27 62 171 evl1scad 
 |-  ( ( ph /\ y e. ( V PrimRoots R ) ) -> ( ( C ` ( ( ZRHom ` K ) ` A ) ) e. B /\ ( ( O ` ( C ` ( ( ZRHom ` K ) ` A ) ) ) ` ( N .^ y ) ) = ( ( ZRHom ` K ) ` A ) ) )
178 177 simprd 
 |-  ( ( ph /\ y e. ( V PrimRoots R ) ) -> ( ( O ` ( C ` ( ( ZRHom ` K ) ` A ) ) ) ` ( N .^ y ) ) = ( ( ZRHom ` K ) ` A ) )
179 176 178 jca 
 |-  ( ( ph /\ y e. ( V PrimRoots R ) ) -> ( ( C ` ( ( ZRHom ` K ) ` A ) ) e. B /\ ( ( O ` ( C ` ( ( ZRHom ` K ) ` A ) ) ) ` ( N .^ y ) ) = ( ( ZRHom ` K ) ` A ) ) )
180 11 2 25 3 27 171 175 179 12 64 evl1addd 
 |-  ( ( ph /\ y e. ( V PrimRoots R ) ) -> ( ( X .+ ( C ` ( ( ZRHom ` K ) ` A ) ) ) e. B /\ ( ( O ` ( X .+ ( C ` ( ( ZRHom ` K ) ` A ) ) ) ) ` ( N .^ y ) ) = ( ( N .^ y ) ( +g ` K ) ( ( ZRHom ` K ) ` A ) ) ) )
181 180 simprd 
 |-  ( ( ph /\ y e. ( V PrimRoots R ) ) -> ( ( O ` ( X .+ ( C ` ( ( ZRHom ` K ) ` A ) ) ) ) ` ( N .^ y ) ) = ( ( N .^ y ) ( +g ` K ) ( ( ZRHom ` K ) ` A ) ) )
182 167 181 eqtrd 
 |-  ( ( ph /\ y e. ( V PrimRoots R ) ) -> ( ( O ` F ) ` ( N .^ y ) ) = ( ( N .^ y ) ( +g ` K ) ( ( ZRHom ` K ) ` A ) ) )
183 166 182 eqtrd 
 |-  ( ( ph /\ y e. ( V PrimRoots R ) ) -> ( N .^ ( ( O ` F ) ` y ) ) = ( ( N .^ y ) ( +g ` K ) ( ( ZRHom ` K ) ` A ) ) )
184 136 183 eqtrd 
 |-  ( ( ph /\ y e. ( V PrimRoots R ) ) -> ( N .^ ( y ( +g ` K ) ( ( ZRHom ` K ) ` A ) ) ) = ( ( N .^ y ) ( +g ` K ) ( ( ZRHom ` K ) ` A ) ) )
185 132 184 eqtrd 
 |-  ( ( ph /\ y e. ( V PrimRoots R ) ) -> ( ( P x. ( N / P ) ) .^ ( y ( +g ` K ) ( ( ZRHom ` K ) ` A ) ) ) = ( ( N .^ y ) ( +g ` K ) ( ( ZRHom ` K ) ` A ) ) )
186 131 eqcomd 
 |-  ( ( ph /\ y e. ( V PrimRoots R ) ) -> N = ( P x. ( N / P ) ) )
187 186 oveq1d 
 |-  ( ( ph /\ y e. ( V PrimRoots R ) ) -> ( N .^ y ) = ( ( P x. ( N / P ) ) .^ y ) )
188 187 120 oveq12d 
 |-  ( ( ph /\ y e. ( V PrimRoots R ) ) -> ( ( N .^ y ) ( +g ` K ) ( ( ZRHom ` K ) ` A ) ) = ( ( ( P x. ( N / P ) ) .^ y ) ( +g ` K ) ( P .^ ( ( ZRHom ` K ) ` A ) ) ) )
189 185 188 eqtr2d 
 |-  ( ( ph /\ y e. ( V PrimRoots R ) ) -> ( ( ( P x. ( N / P ) ) .^ y ) ( +g ` K ) ( P .^ ( ( ZRHom ` K ) ` A ) ) ) = ( ( P x. ( N / P ) ) .^ ( y ( +g ` K ) ( ( ZRHom ` K ) ` A ) ) ) )
190 71 92 eleqtrdi 
 |-  ( ( ph /\ y e. ( V PrimRoots R ) ) -> y e. ( Base ` ( mulGrp ` K ) ) )
191 99 41 190 3jca 
 |-  ( ( ph /\ y e. ( V PrimRoots R ) ) -> ( P e. NN0 /\ ( N / P ) e. NN0 /\ y e. ( Base ` ( mulGrp ` K ) ) ) )
192 eqid 
 |-  ( Base ` ( mulGrp ` K ) ) = ( Base ` ( mulGrp ` K ) )
193 192 94 mulgnn0ass 
 |-  ( ( ( mulGrp ` K ) e. Mnd /\ ( P e. NN0 /\ ( N / P ) e. NN0 /\ y e. ( Base ` ( mulGrp ` K ) ) ) ) -> ( ( P x. ( N / P ) ) .^ y ) = ( P .^ ( ( N / P ) .^ y ) ) )
194 97 191 193 syl2anc 
 |-  ( ( ph /\ y e. ( V PrimRoots R ) ) -> ( ( P x. ( N / P ) ) .^ y ) = ( P .^ ( ( N / P ) .^ y ) ) )
195 194 oveq1d 
 |-  ( ( ph /\ y e. ( V PrimRoots R ) ) -> ( ( ( P x. ( N / P ) ) .^ y ) ( +g ` K ) ( P .^ ( ( ZRHom ` K ) ` A ) ) ) = ( ( P .^ ( ( N / P ) .^ y ) ) ( +g ` K ) ( P .^ ( ( ZRHom ` K ) ` A ) ) ) )
196 189 195 eqtr3d 
 |-  ( ( ph /\ y e. ( V PrimRoots R ) ) -> ( ( P x. ( N / P ) ) .^ ( y ( +g ` K ) ( ( ZRHom ` K ) ` A ) ) ) = ( ( P .^ ( ( N / P ) .^ y ) ) ( +g ` K ) ( P .^ ( ( ZRHom ` K ) ` A ) ) ) )
197 25 64 82 71 62 grpcld 
 |-  ( ( ph /\ y e. ( V PrimRoots R ) ) -> ( y ( +g ` K ) ( ( ZRHom ` K ) ` A ) ) e. ( Base ` K ) )
198 197 92 eleqtrdi 
 |-  ( ( ph /\ y e. ( V PrimRoots R ) ) -> ( y ( +g ` K ) ( ( ZRHom ` K ) ` A ) ) e. ( Base ` ( mulGrp ` K ) ) )
199 99 41 198 3jca 
 |-  ( ( ph /\ y e. ( V PrimRoots R ) ) -> ( P e. NN0 /\ ( N / P ) e. NN0 /\ ( y ( +g ` K ) ( ( ZRHom ` K ) ` A ) ) e. ( Base ` ( mulGrp ` K ) ) ) )
200 192 94 mulgnn0ass 
 |-  ( ( ( mulGrp ` K ) e. Mnd /\ ( P e. NN0 /\ ( N / P ) e. NN0 /\ ( y ( +g ` K ) ( ( ZRHom ` K ) ` A ) ) e. ( Base ` ( mulGrp ` K ) ) ) ) -> ( ( P x. ( N / P ) ) .^ ( y ( +g ` K ) ( ( ZRHom ` K ) ` A ) ) ) = ( P .^ ( ( N / P ) .^ ( y ( +g ` K ) ( ( ZRHom ` K ) ` A ) ) ) ) )
201 97 199 200 syl2anc 
 |-  ( ( ph /\ y e. ( V PrimRoots R ) ) -> ( ( P x. ( N / P ) ) .^ ( y ( +g ` K ) ( ( ZRHom ` K ) ` A ) ) ) = ( P .^ ( ( N / P ) .^ ( y ( +g ` K ) ( ( ZRHom ` K ) ` A ) ) ) ) )
202 196 201 eqtr3d 
 |-  ( ( ph /\ y e. ( V PrimRoots R ) ) -> ( ( P .^ ( ( N / P ) .^ y ) ) ( +g ` K ) ( P .^ ( ( ZRHom ` K ) ` A ) ) ) = ( P .^ ( ( N / P ) .^ ( y ( +g ` K ) ( ( ZRHom ` K ) ` A ) ) ) ) )
203 124 202 eqtrd 
 |-  ( ( ph /\ y e. ( V PrimRoots R ) ) -> ( P .^ ( ( ( N / P ) .^ y ) ( +g ` K ) ( ( ZRHom ` K ) ` A ) ) ) = ( P .^ ( ( N / P ) .^ ( y ( +g ` K ) ( ( ZRHom ` K ) ` A ) ) ) ) )
204 id 
 |-  ( x = ( ( N / P ) .^ ( y ( +g ` K ) ( ( ZRHom ` K ) ` A ) ) ) -> x = ( ( N / P ) .^ ( y ( +g ` K ) ( ( ZRHom ` K ) ` A ) ) ) )
205 204 oveq2d 
 |-  ( x = ( ( N / P ) .^ ( y ( +g ` K ) ( ( ZRHom ` K ) ` A ) ) ) -> ( P .^ x ) = ( P .^ ( ( N / P ) .^ ( y ( +g ` K ) ( ( ZRHom ` K ) ` A ) ) ) ) )
206 205 adantl 
 |-  ( ( ( ph /\ y e. ( V PrimRoots R ) ) /\ x = ( ( N / P ) .^ ( y ( +g ` K ) ( ( ZRHom ` K ) ` A ) ) ) ) -> ( P .^ x ) = ( P .^ ( ( N / P ) .^ ( y ( +g ` K ) ( ( ZRHom ` K ) ` A ) ) ) ) )
207 92 94 97 41 197 mulgnn0cld 
 |-  ( ( ph /\ y e. ( V PrimRoots R ) ) -> ( ( N / P ) .^ ( y ( +g ` K ) ( ( ZRHom ` K ) ` A ) ) ) e. ( Base ` K ) )
208 203 100 eqeltrrd 
 |-  ( ( ph /\ y e. ( V PrimRoots R ) ) -> ( P .^ ( ( N / P ) .^ ( y ( +g ` K ) ( ( ZRHom ` K ) ` A ) ) ) ) e. ( Base ` K ) )
209 87 206 207 208 fvmptd 
 |-  ( ( ph /\ y e. ( V PrimRoots R ) ) -> ( ( x e. ( Base ` K ) |-> ( P .^ x ) ) ` ( ( N / P ) .^ ( y ( +g ` K ) ( ( ZRHom ` K ) ` A ) ) ) ) = ( P .^ ( ( N / P ) .^ ( y ( +g ` K ) ( ( ZRHom ` K ) ` A ) ) ) ) )
210 209 eqcomd 
 |-  ( ( ph /\ y e. ( V PrimRoots R ) ) -> ( P .^ ( ( N / P ) .^ ( y ( +g ` K ) ( ( ZRHom ` K ) ` A ) ) ) ) = ( ( x e. ( Base ` K ) |-> ( P .^ x ) ) ` ( ( N / P ) .^ ( y ( +g ` K ) ( ( ZRHom ` K ) ` A ) ) ) ) )
211 101 203 210 3eqtrd 
 |-  ( ( ph /\ y e. ( V PrimRoots R ) ) -> ( ( x e. ( Base ` K ) |-> ( P .^ x ) ) ` ( ( ( N / P ) .^ y ) ( +g ` K ) ( ( ZRHom ` K ) ` A ) ) ) = ( ( x e. ( Base ` K ) |-> ( P .^ x ) ) ` ( ( N / P ) .^ ( y ( +g ` K ) ( ( ZRHom ` K ) ` A ) ) ) ) )
212 211 fveq2d 
 |-  ( ( ph /\ y e. ( V PrimRoots R ) ) -> ( `' ( x e. ( Base ` K ) |-> ( P .^ x ) ) ` ( ( x e. ( Base ` K ) |-> ( P .^ x ) ) ` ( ( ( N / P ) .^ y ) ( +g ` K ) ( ( ZRHom ` K ) ` A ) ) ) ) = ( `' ( x e. ( Base ` K ) |-> ( P .^ x ) ) ` ( ( x e. ( Base ` K ) |-> ( P .^ x ) ) ` ( ( N / P ) .^ ( y ( +g ` K ) ( ( ZRHom ` K ) ` A ) ) ) ) ) )
213 f1ocnvfv1 
 |-  ( ( ( x e. ( Base ` K ) |-> ( P .^ x ) ) : ( Base ` K ) -1-1-onto-> ( Base ` K ) /\ ( ( N / P ) .^ ( y ( +g ` K ) ( ( ZRHom ` K ) ` A ) ) ) e. ( Base ` K ) ) -> ( `' ( x e. ( Base ` K ) |-> ( P .^ x ) ) ` ( ( x e. ( Base ` K ) |-> ( P .^ x ) ) ` ( ( N / P ) .^ ( y ( +g ` K ) ( ( ZRHom ` K ) ` A ) ) ) ) ) = ( ( N / P ) .^ ( y ( +g ` K ) ( ( ZRHom ` K ) ` A ) ) ) )
214 81 207 213 syl2anc 
 |-  ( ( ph /\ y e. ( V PrimRoots R ) ) -> ( `' ( x e. ( Base ` K ) |-> ( P .^ x ) ) ` ( ( x e. ( Base ` K ) |-> ( P .^ x ) ) ` ( ( N / P ) .^ ( y ( +g ` K ) ( ( ZRHom ` K ) ` A ) ) ) ) ) = ( ( N / P ) .^ ( y ( +g ` K ) ( ( ZRHom ` K ) ` A ) ) ) )
215 86 212 214 3eqtrd 
 |-  ( ( ph /\ y e. ( V PrimRoots R ) ) -> ( ( ( N / P ) .^ y ) ( +g ` K ) ( ( ZRHom ` K ) ` A ) ) = ( ( N / P ) .^ ( y ( +g ` K ) ( ( ZRHom ` K ) ` A ) ) ) )
216 215 eqcomd 
 |-  ( ( ph /\ y e. ( V PrimRoots R ) ) -> ( ( N / P ) .^ ( y ( +g ` K ) ( ( ZRHom ` K ) ` A ) ) ) = ( ( ( N / P ) .^ y ) ( +g ` K ) ( ( ZRHom ` K ) ` A ) ) )
217 77 216 eqtr2d 
 |-  ( ( ph /\ y e. ( V PrimRoots R ) ) -> ( ( ( N / P ) .^ y ) ( +g ` K ) ( ( ZRHom ` K ) ` A ) ) = ( ( N / P ) .^ ( ( O ` F ) ` y ) ) )
218 67 217 eqtrd 
 |-  ( ( ph /\ y e. ( V PrimRoots R ) ) -> ( ( O ` F ) ` ( ( N / P ) .^ y ) ) = ( ( N / P ) .^ ( ( O ` F ) ` y ) ) )
219 218 eqcomd 
 |-  ( ( ph /\ y e. ( V PrimRoots R ) ) -> ( ( N / P ) .^ ( ( O ` F ) ` y ) ) = ( ( O ` F ) ` ( ( N / P ) .^ y ) ) )
220 219 ralrimiva 
 |-  ( ph -> A. y e. ( V PrimRoots R ) ( ( N / P ) .^ ( ( O ` F ) ` y ) ) = ( ( O ` F ) ` ( ( N / P ) .^ y ) ) )
221 1 154 39 aks6d1c1p1 
 |-  ( ph -> ( ( N / P ) .~ F <-> A. y e. ( V PrimRoots R ) ( ( N / P ) .^ ( ( O ` F ) ` y ) ) = ( ( O ` F ) ` ( ( N / P ) .^ y ) ) ) )
222 220 221 mpbird 
 |-  ( ph -> ( N / P ) .~ F )