Metamath Proof Explorer

Theorem aks6d1c1p5

Description: The product of exponents is introspective. (Contributed by metakunt, 26-Apr-2025)

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

Proof

Step Hyp Ref Expression
1 aks6d1c1p5.1 
 |-  .~ = { <. e , f >. | ( e e. NN /\ f e. B /\ A. y e. ( V PrimRoots R ) ( e .^ ( ( O ` f ) ` y ) ) = ( ( O ` f ) ` ( e .^ y ) ) ) }
2 aks6d1c1p5.2 
 |-  S = ( Poly1 ` K )
3 aks6d1c1p5.3 
 |-  B = ( Base ` S )
4 aks6d1c1p5.4 
 |-  X = ( var1 ` K )
5 aks6d1c1p5.5 
 |-  W = ( mulGrp ` S )
6 aks6d1c1p5.6 
 |-  V = ( mulGrp ` K )
7 aks6d1c1p5.7 
 |-  .^ = ( .g ` V )
8 aks6d1c1p5.8 
 |-  C = ( algSc ` S )
9 aks6d1c1p5.10 
 |-  P = ( chr ` K )
10 aks6d1c1p5.11 
 |-  O = ( eval1 ` K )
11 aks6d1c1p5.12 
 |-  .+ = ( +g ` S )
12 aks6d1c1p5.13 
 |-  ( ph -> K e. Field )
13 aks6d1c1p5.14 
 |-  ( ph -> P e. Prime )
14 aks6d1c1p5.15 
 |-  ( ph -> R e. NN )
15 aks6d1c1p5.16 
 |-  ( ph -> ( E gcd R ) = 1 )
16 aks6d1c1p5.17 
 |-  ( ph -> P || N )
17 aks6d1c1p5.18 
 |-  ( ph -> D .~ F )
18 aks6d1c1p5.19 
 |-  ( ph -> E .~ F )
19 12 fldcrngd 
 |-  ( ph -> K e. CRing )
20 6 crngmgp 
 |-  ( K e. CRing -> V e. CMnd )
21 19 20 syl 
 |-  ( ph -> V e. CMnd )
22 21 cmnmndd 
 |-  ( ph -> V e. Mnd )
23 22 adantr 
 |-  ( ( ph /\ y e. ( V PrimRoots R ) ) -> V e. Mnd )
24 1 17 aks6d1c1p1rcl 
 |-  ( ph -> ( D e. NN /\ F e. B ) )
25 24 simpld 
 |-  ( ph -> D e. NN )
26 25 nnnn0d 
 |-  ( ph -> D e. NN0 )
27 26 adantr 
 |-  ( ( ph /\ y e. ( V PrimRoots R ) ) -> D e. NN0 )
28 1 18 aks6d1c1p1rcl 
 |-  ( ph -> ( E e. NN /\ F e. B ) )
29 28 simpld 
 |-  ( ph -> E e. NN )
30 29 nnnn0d 
 |-  ( ph -> E e. NN0 )
31 30 adantr 
 |-  ( ( ph /\ y e. ( V PrimRoots R ) ) -> E e. NN0 )
32 eqid 
 |-  ( Base ` K ) = ( Base ` K )
33 19 adantr 
 |-  ( ( ph /\ y e. ( V PrimRoots R ) ) -> K e. CRing )
34 14 nnnn0d 
 |-  ( ph -> R e. NN0 )
35 21 34 7 isprimroot 
 |-  ( ph -> ( y e. ( V PrimRoots R ) <-> ( y e. ( Base ` V ) /\ ( R .^ y ) = ( 0g ` V ) /\ A. q e. NN0 ( ( q .^ y ) = ( 0g ` V ) -> R || q ) ) ) )
36 35 biimpd 
 |-  ( ph -> ( y e. ( V PrimRoots R ) -> ( y e. ( Base ` V ) /\ ( R .^ y ) = ( 0g ` V ) /\ A. q e. NN0 ( ( q .^ y ) = ( 0g ` V ) -> R || q ) ) ) )
37 36 imp 
 |-  ( ( ph /\ y e. ( V PrimRoots R ) ) -> ( y e. ( Base ` V ) /\ ( R .^ y ) = ( 0g ` V ) /\ A. q e. NN0 ( ( q .^ y ) = ( 0g ` V ) -> R || q ) ) )
38 37 simp1d 
 |-  ( ( ph /\ y e. ( V PrimRoots R ) ) -> y e. ( Base ` V ) )
39 6 32 mgpbas 
 |-  ( Base ` K ) = ( Base ` V )
40 39 a1i 
 |-  ( ph -> ( Base ` K ) = ( Base ` V ) )
41 40 eqcomd 
 |-  ( ph -> ( Base ` V ) = ( Base ` K ) )
42 41 adantr 
 |-  ( ( ph /\ y e. ( V PrimRoots R ) ) -> ( Base ` V ) = ( Base ` K ) )
43 38 42 eleqtrd 
 |-  ( ( ph /\ y e. ( V PrimRoots R ) ) -> y e. ( Base ` K ) )
44 24 simprd 
 |-  ( ph -> F e. B )
45 44 adantr 
 |-  ( ( ph /\ y e. ( V PrimRoots R ) ) -> F e. B )
46 10 2 32 3 33 43 45 fveval1fvcl 
 |-  ( ( ph /\ y e. ( V PrimRoots R ) ) -> ( ( O ` F ) ` y ) e. ( Base ` K ) )
47 42 eleq2d 
 |-  ( ( ph /\ y e. ( V PrimRoots R ) ) -> ( ( ( O ` F ) ` y ) e. ( Base ` V ) <-> ( ( O ` F ) ` y ) e. ( Base ` K ) ) )
48 46 47 mpbird 
 |-  ( ( ph /\ y e. ( V PrimRoots R ) ) -> ( ( O ` F ) ` y ) e. ( Base ` V ) )
49 27 31 48 3jca 
 |-  ( ( ph /\ y e. ( V PrimRoots R ) ) -> ( D e. NN0 /\ E e. NN0 /\ ( ( O ` F ) ` y ) e. ( Base ` V ) ) )
50 eqid 
 |-  ( Base ` V ) = ( Base ` V )
51 50 7 mulgnn0ass 
 |-  ( ( V e. Mnd /\ ( D e. NN0 /\ E e. NN0 /\ ( ( O ` F ) ` y ) e. ( Base ` V ) ) ) -> ( ( D x. E ) .^ ( ( O ` F ) ` y ) ) = ( D .^ ( E .^ ( ( O ` F ) ` y ) ) ) )
52 23 49 51 syl2anc 
 |-  ( ( ph /\ y e. ( V PrimRoots R ) ) -> ( ( D x. E ) .^ ( ( O ` F ) ` y ) ) = ( D .^ ( E .^ ( ( O ` F ) ` y ) ) ) )
53 eqidd 
 |-  ( ( ph /\ y e. ( V PrimRoots R ) ) -> ( l e. ( V PrimRoots R ) |-> ( E .^ l ) ) = ( l e. ( V PrimRoots R ) |-> ( E .^ l ) ) )
54 simpr 
 |-  ( ( ( ph /\ y e. ( V PrimRoots R ) ) /\ l = y ) -> l = y )
55 54 oveq2d 
 |-  ( ( ( ph /\ y e. ( V PrimRoots R ) ) /\ l = y ) -> ( E .^ l ) = ( E .^ y ) )
56 simpr 
 |-  ( ( ph /\ y e. ( V PrimRoots R ) ) -> y e. ( V PrimRoots R ) )
57 50 7 23 31 38 mulgnn0cld 
 |-  ( ( ph /\ y e. ( V PrimRoots R ) ) -> ( E .^ y ) e. ( Base ` V ) )
58 53 55 56 57 fvmptd 
 |-  ( ( ph /\ y e. ( V PrimRoots R ) ) -> ( ( l e. ( V PrimRoots R ) |-> ( E .^ l ) ) ` y ) = ( E .^ y ) )
59 58 fveq2d 
 |-  ( ( ph /\ y e. ( V PrimRoots R ) ) -> ( ( O ` F ) ` ( ( l e. ( V PrimRoots R ) |-> ( E .^ l ) ) ` y ) ) = ( ( O ` F ) ` ( E .^ y ) ) )
60 59 oveq2d 
 |-  ( ( ph /\ y e. ( V PrimRoots R ) ) -> ( D .^ ( ( O ` F ) ` ( ( l e. ( V PrimRoots R ) |-> ( E .^ l ) ) ` y ) ) ) = ( D .^ ( ( O ` F ) ` ( E .^ y ) ) ) )
61 60 eqcomd 
 |-  ( ( ph /\ y e. ( V PrimRoots R ) ) -> ( D .^ ( ( O ` F ) ` ( E .^ y ) ) ) = ( D .^ ( ( O ` F ) ` ( ( l e. ( V PrimRoots R ) |-> ( E .^ l ) ) ` y ) ) ) )
62 2fveq3 
 |-  ( i = y -> ( ( O ` F ) ` ( ( l e. ( V PrimRoots R ) |-> ( E .^ l ) ) ` i ) ) = ( ( O ` F ) ` ( ( l e. ( V PrimRoots R ) |-> ( E .^ l ) ) ` y ) ) )
63 62 oveq2d 
 |-  ( i = y -> ( D .^ ( ( O ` F ) ` ( ( l e. ( V PrimRoots R ) |-> ( E .^ l ) ) ` i ) ) ) = ( D .^ ( ( O ` F ) ` ( ( l e. ( V PrimRoots R ) |-> ( E .^ l ) ) ` y ) ) ) )
64 fveq2 
 |-  ( i = y -> ( ( l e. ( V PrimRoots R ) |-> ( E .^ l ) ) ` i ) = ( ( l e. ( V PrimRoots R ) |-> ( E .^ l ) ) ` y ) )
65 64 oveq2d 
 |-  ( i = y -> ( D .^ ( ( l e. ( V PrimRoots R ) |-> ( E .^ l ) ) ` i ) ) = ( D .^ ( ( l e. ( V PrimRoots R ) |-> ( E .^ l ) ) ` y ) ) )
66 65 fveq2d 
 |-  ( i = y -> ( ( O ` F ) ` ( D .^ ( ( l e. ( V PrimRoots R ) |-> ( E .^ l ) ) ` i ) ) ) = ( ( O ` F ) ` ( D .^ ( ( l e. ( V PrimRoots R ) |-> ( E .^ l ) ) ` y ) ) ) )
67 63 66 eqeq12d 
 |-  ( i = y -> ( ( D .^ ( ( O ` F ) ` ( ( l e. ( V PrimRoots R ) |-> ( E .^ l ) ) ` i ) ) ) = ( ( O ` F ) ` ( D .^ ( ( l e. ( V PrimRoots R ) |-> ( E .^ l ) ) ` i ) ) ) <-> ( D .^ ( ( O ` F ) ` ( ( l e. ( V PrimRoots R ) |-> ( E .^ l ) ) ` y ) ) ) = ( ( O ` F ) ` ( D .^ ( ( l e. ( V PrimRoots R ) |-> ( E .^ l ) ) ` y ) ) ) ) )
68 1 44 25 aks6d1c1p1 
 |-  ( ph -> ( D .~ F <-> A. y e. ( V PrimRoots R ) ( D .^ ( ( O ` F ) ` y ) ) = ( ( O ` F ) ` ( D .^ y ) ) ) )
69 68 biimpd 
 |-  ( ph -> ( D .~ F -> A. y e. ( V PrimRoots R ) ( D .^ ( ( O ` F ) ` y ) ) = ( ( O ` F ) ` ( D .^ y ) ) ) )
70 17 69 mpd 
 |-  ( ph -> A. y e. ( V PrimRoots R ) ( D .^ ( ( O ` F ) ` y ) ) = ( ( O ` F ) ` ( D .^ y ) ) )
71 7 oveqi 
 |-  ( E .^ l ) = ( E ( .g ` V ) l )
72 71 a1i 
 |-  ( l e. ( V PrimRoots R ) -> ( E .^ l ) = ( E ( .g ` V ) l ) )
73 72 mpteq2ia 
 |-  ( l e. ( V PrimRoots R ) |-> ( E .^ l ) ) = ( l e. ( V PrimRoots R ) |-> ( E ( .g ` V ) l ) )
74 73 21 14 29 15 primrootscoprbij2 
 |-  ( ph -> ( l e. ( V PrimRoots R ) |-> ( E .^ l ) ) : ( V PrimRoots R ) -1-1-onto-> ( V PrimRoots R ) )
75 f1ofo 
 |-  ( ( l e. ( V PrimRoots R ) |-> ( E .^ l ) ) : ( V PrimRoots R ) -1-1-onto-> ( V PrimRoots R ) -> ( l e. ( V PrimRoots R ) |-> ( E .^ l ) ) : ( V PrimRoots R ) -onto-> ( V PrimRoots R ) )
76 74 75 syl 
 |-  ( ph -> ( l e. ( V PrimRoots R ) |-> ( E .^ l ) ) : ( V PrimRoots R ) -onto-> ( V PrimRoots R ) )
77 fveq2 
 |-  ( ( ( l e. ( V PrimRoots R ) |-> ( E .^ l ) ) ` i ) = y -> ( ( O ` F ) ` ( ( l e. ( V PrimRoots R ) |-> ( E .^ l ) ) ` i ) ) = ( ( O ` F ) ` y ) )
78 77 oveq2d 
 |-  ( ( ( l e. ( V PrimRoots R ) |-> ( E .^ l ) ) ` i ) = y -> ( D .^ ( ( O ` F ) ` ( ( l e. ( V PrimRoots R ) |-> ( E .^ l ) ) ` i ) ) ) = ( D .^ ( ( O ` F ) ` y ) ) )
79 oveq2 
 |-  ( ( ( l e. ( V PrimRoots R ) |-> ( E .^ l ) ) ` i ) = y -> ( D .^ ( ( l e. ( V PrimRoots R ) |-> ( E .^ l ) ) ` i ) ) = ( D .^ y ) )
80 79 fveq2d 
 |-  ( ( ( l e. ( V PrimRoots R ) |-> ( E .^ l ) ) ` i ) = y -> ( ( O ` F ) ` ( D .^ ( ( l e. ( V PrimRoots R ) |-> ( E .^ l ) ) ` i ) ) ) = ( ( O ` F ) ` ( D .^ y ) ) )
81 78 80 eqeq12d 
 |-  ( ( ( l e. ( V PrimRoots R ) |-> ( E .^ l ) ) ` i ) = y -> ( ( D .^ ( ( O ` F ) ` ( ( l e. ( V PrimRoots R ) |-> ( E .^ l ) ) ` i ) ) ) = ( ( O ` F ) ` ( D .^ ( ( l e. ( V PrimRoots R ) |-> ( E .^ l ) ) ` i ) ) ) <-> ( D .^ ( ( O ` F ) ` y ) ) = ( ( O ` F ) ` ( D .^ y ) ) ) )
82 81 cbvfo 
 |-  ( ( l e. ( V PrimRoots R ) |-> ( E .^ l ) ) : ( V PrimRoots R ) -onto-> ( V PrimRoots R ) -> ( A. i e. ( V PrimRoots R ) ( D .^ ( ( O ` F ) ` ( ( l e. ( V PrimRoots R ) |-> ( E .^ l ) ) ` i ) ) ) = ( ( O ` F ) ` ( D .^ ( ( l e. ( V PrimRoots R ) |-> ( E .^ l ) ) ` i ) ) ) <-> A. y e. ( V PrimRoots R ) ( D .^ ( ( O ` F ) ` y ) ) = ( ( O ` F ) ` ( D .^ y ) ) ) )
83 76 82 syl 
 |-  ( ph -> ( A. i e. ( V PrimRoots R ) ( D .^ ( ( O ` F ) ` ( ( l e. ( V PrimRoots R ) |-> ( E .^ l ) ) ` i ) ) ) = ( ( O ` F ) ` ( D .^ ( ( l e. ( V PrimRoots R ) |-> ( E .^ l ) ) ` i ) ) ) <-> A. y e. ( V PrimRoots R ) ( D .^ ( ( O ` F ) ` y ) ) = ( ( O ` F ) ` ( D .^ y ) ) ) )
84 70 83 mpbird 
 |-  ( ph -> A. i e. ( V PrimRoots R ) ( D .^ ( ( O ` F ) ` ( ( l e. ( V PrimRoots R ) |-> ( E .^ l ) ) ` i ) ) ) = ( ( O ` F ) ` ( D .^ ( ( l e. ( V PrimRoots R ) |-> ( E .^ l ) ) ` i ) ) ) )
85 84 adantr 
 |-  ( ( ph /\ y e. ( V PrimRoots R ) ) -> A. i e. ( V PrimRoots R ) ( D .^ ( ( O ` F ) ` ( ( l e. ( V PrimRoots R ) |-> ( E .^ l ) ) ` i ) ) ) = ( ( O ` F ) ` ( D .^ ( ( l e. ( V PrimRoots R ) |-> ( E .^ l ) ) ` i ) ) ) )
86 67 85 56 rspcdva 
 |-  ( ( ph /\ y e. ( V PrimRoots R ) ) -> ( D .^ ( ( O ` F ) ` ( ( l e. ( V PrimRoots R ) |-> ( E .^ l ) ) ` y ) ) ) = ( ( O ` F ) ` ( D .^ ( ( l e. ( V PrimRoots R ) |-> ( E .^ l ) ) ` y ) ) ) )
87 58 oveq2d 
 |-  ( ( ph /\ y e. ( V PrimRoots R ) ) -> ( D .^ ( ( l e. ( V PrimRoots R ) |-> ( E .^ l ) ) ` y ) ) = ( D .^ ( E .^ y ) ) )
88 87 fveq2d 
 |-  ( ( ph /\ y e. ( V PrimRoots R ) ) -> ( ( O ` F ) ` ( D .^ ( ( l e. ( V PrimRoots R ) |-> ( E .^ l ) ) ` y ) ) ) = ( ( O ` F ) ` ( D .^ ( E .^ y ) ) ) )
89 86 88 eqtrd 
 |-  ( ( ph /\ y e. ( V PrimRoots R ) ) -> ( D .^ ( ( O ` F ) ` ( ( l e. ( V PrimRoots R ) |-> ( E .^ l ) ) ` y ) ) ) = ( ( O ` F ) ` ( D .^ ( E .^ y ) ) ) )
90 61 89 eqtr2d 
 |-  ( ( ph /\ y e. ( V PrimRoots R ) ) -> ( ( O ` F ) ` ( D .^ ( E .^ y ) ) ) = ( D .^ ( ( O ` F ) ` ( E .^ y ) ) ) )
91 fveq2 
 |-  ( z = y -> ( ( O ` F ) ` z ) = ( ( O ` F ) ` y ) )
92 91 oveq2d 
 |-  ( z = y -> ( E .^ ( ( O ` F ) ` z ) ) = ( E .^ ( ( O ` F ) ` y ) ) )
93 oveq2 
 |-  ( z = y -> ( E .^ z ) = ( E .^ y ) )
94 93 fveq2d 
 |-  ( z = y -> ( ( O ` F ) ` ( E .^ z ) ) = ( ( O ` F ) ` ( E .^ y ) ) )
95 92 94 eqeq12d 
 |-  ( z = y -> ( ( E .^ ( ( O ` F ) ` z ) ) = ( ( O ` F ) ` ( E .^ z ) ) <-> ( E .^ ( ( O ` F ) ` y ) ) = ( ( O ` F ) ` ( E .^ y ) ) ) )
96 1 44 29 aks6d1c1p1 
 |-  ( ph -> ( E .~ F <-> A. y e. ( V PrimRoots R ) ( E .^ ( ( O ` F ) ` y ) ) = ( ( O ` F ) ` ( E .^ y ) ) ) )
97 96 biimpd 
 |-  ( ph -> ( E .~ F -> A. y e. ( V PrimRoots R ) ( E .^ ( ( O ` F ) ` y ) ) = ( ( O ` F ) ` ( E .^ y ) ) ) )
98 18 97 mpd 
 |-  ( ph -> A. y e. ( V PrimRoots R ) ( E .^ ( ( O ` F ) ` y ) ) = ( ( O ` F ) ` ( E .^ y ) ) )
99 nfv 
 |-  F/ y ( E .^ ( ( O ` F ) ` z ) ) = ( ( O ` F ) ` ( E .^ z ) )
100 nfv 
 |-  F/ z ( E .^ ( ( O ` F ) ` y ) ) = ( ( O ` F ) ` ( E .^ y ) )
101 99 100 95 cbvralw 
 |-  ( A. z e. ( V PrimRoots R ) ( E .^ ( ( O ` F ) ` z ) ) = ( ( O ` F ) ` ( E .^ z ) ) <-> A. y e. ( V PrimRoots R ) ( E .^ ( ( O ` F ) ` y ) ) = ( ( O ` F ) ` ( E .^ y ) ) )
102 98 101 sylibr 
 |-  ( ph -> A. z e. ( V PrimRoots R ) ( E .^ ( ( O ` F ) ` z ) ) = ( ( O ` F ) ` ( E .^ z ) ) )
103 102 adantr 
 |-  ( ( ph /\ y e. ( V PrimRoots R ) ) -> A. z e. ( V PrimRoots R ) ( E .^ ( ( O ` F ) ` z ) ) = ( ( O ` F ) ` ( E .^ z ) ) )
104 95 103 56 rspcdva 
 |-  ( ( ph /\ y e. ( V PrimRoots R ) ) -> ( E .^ ( ( O ` F ) ` y ) ) = ( ( O ` F ) ` ( E .^ y ) ) )
105 104 eqcomd 
 |-  ( ( ph /\ y e. ( V PrimRoots R ) ) -> ( ( O ` F ) ` ( E .^ y ) ) = ( E .^ ( ( O ` F ) ` y ) ) )
106 105 oveq2d 
 |-  ( ( ph /\ y e. ( V PrimRoots R ) ) -> ( D .^ ( ( O ` F ) ` ( E .^ y ) ) ) = ( D .^ ( E .^ ( ( O ` F ) ` y ) ) ) )
107 90 106 eqtrd 
 |-  ( ( ph /\ y e. ( V PrimRoots R ) ) -> ( ( O ` F ) ` ( D .^ ( E .^ y ) ) ) = ( D .^ ( E .^ ( ( O ` F ) ` y ) ) ) )
108 107 eqcomd 
 |-  ( ( ph /\ y e. ( V PrimRoots R ) ) -> ( D .^ ( E .^ ( ( O ` F ) ` y ) ) ) = ( ( O ` F ) ` ( D .^ ( E .^ y ) ) ) )
109 27 31 38 3jca 
 |-  ( ( ph /\ y e. ( V PrimRoots R ) ) -> ( D e. NN0 /\ E e. NN0 /\ y e. ( Base ` V ) ) )
110 50 7 mulgnn0ass 
 |-  ( ( V e. Mnd /\ ( D e. NN0 /\ E e. NN0 /\ y e. ( Base ` V ) ) ) -> ( ( D x. E ) .^ y ) = ( D .^ ( E .^ y ) ) )
111 110 eqcomd 
 |-  ( ( V e. Mnd /\ ( D e. NN0 /\ E e. NN0 /\ y e. ( Base ` V ) ) ) -> ( D .^ ( E .^ y ) ) = ( ( D x. E ) .^ y ) )
112 23 109 111 syl2anc 
 |-  ( ( ph /\ y e. ( V PrimRoots R ) ) -> ( D .^ ( E .^ y ) ) = ( ( D x. E ) .^ y ) )
113 112 fveq2d 
 |-  ( ( ph /\ y e. ( V PrimRoots R ) ) -> ( ( O ` F ) ` ( D .^ ( E .^ y ) ) ) = ( ( O ` F ) ` ( ( D x. E ) .^ y ) ) )
114 52 108 113 3eqtrd 
 |-  ( ( ph /\ y e. ( V PrimRoots R ) ) -> ( ( D x. E ) .^ ( ( O ` F ) ` y ) ) = ( ( O ` F ) ` ( ( D x. E ) .^ y ) ) )
115 114 ralrimiva 
 |-  ( ph -> A. y e. ( V PrimRoots R ) ( ( D x. E ) .^ ( ( O ` F ) ` y ) ) = ( ( O ` F ) ` ( ( D x. E ) .^ y ) ) )
116 25 29 nnmulcld 
 |-  ( ph -> ( D x. E ) e. NN )
117 1 44 116 aks6d1c1p1 
 |-  ( ph -> ( ( D x. E ) .~ F <-> A. y e. ( V PrimRoots R ) ( ( D x. E ) .^ ( ( O ` F ) ` y ) ) = ( ( O ` F ) ` ( ( D x. E ) .^ y ) ) ) )
118 115 117 mpbird 
 |-  ( ph -> ( D x. E ) .~ F )