Metamath Proof Explorer

Theorem aks6d1c1p4

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

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

Proof

Step Hyp Ref Expression
1 aks6d1c1p4.1 
 |-  .~ = { <. e , f >. | ( e e. NN /\ f e. B /\ A. y e. ( V PrimRoots R ) ( e .^ ( ( O ` f ) ` y ) ) = ( ( O ` f ) ` ( e .^ y ) ) ) }
2 aks6d1c1p4.2 
 |-  S = ( Poly1 ` K )
3 aks6d1c1p4.3 
 |-  B = ( Base ` S )
4 aks6d1c1p4.4 
 |-  X = ( var1 ` K )
5 aks6d1c1p4.5 
 |-  W = ( mulGrp ` S )
6 aks6d1c1p4.6 
 |-  V = ( mulGrp ` K )
7 aks6d1c1p4.7 
 |-  .^ = ( .g ` V )
8 aks6d1c1p4.8 
 |-  C = ( algSc ` S )
9 aks6d1c1p4.9 
 |-  D = ( .g ` W )
10 aks6d1c1p4.10 
 |-  P = ( chr ` K )
11 aks6d1c1p4.11 
 |-  O = ( eval1 ` K )
12 aks6d1c1p4.12 
 |-  .+ = ( +g ` S )
13 aks6d1c1p4.13 
 |-  ( ph -> K e. Field )
14 aks6d1c1p4.14 
 |-  ( ph -> P e. Prime )
15 aks6d1c1p4.15 
 |-  ( ph -> R e. NN )
16 aks6d1c1p4.16 
 |-  ( ph -> ( N gcd R ) = 1 )
17 aks6d1c1p4.17 
 |-  ( ph -> P || N )
18 aks6d1c1p4.18 
 |-  ( ph -> E .~ F )
19 aks6d1c1p4.19 
 |-  ( ph -> E .~ G )
20 eqid 
 |-  ( Base ` K ) = ( Base ` K )
21 13 fldcrngd 
 |-  ( ph -> K e. CRing )
22 21 adantr 
 |-  ( ( ph /\ y e. ( V PrimRoots R ) ) -> K e. CRing )
23 6 20 mgpbas 
 |-  ( Base ` K ) = ( Base ` V )
24 6 crngmgp 
 |-  ( K e. CRing -> V e. CMnd )
25 21 24 syl 
 |-  ( ph -> V e. CMnd )
26 25 cmnmndd 
 |-  ( ph -> V e. Mnd )
27 26 adantr 
 |-  ( ( ph /\ y e. ( V PrimRoots R ) ) -> V e. Mnd )
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 15 nnnn0d 
 |-  ( ph -> R e. NN0 )
33 eqid 
 |-  ( .g ` V ) = ( .g ` V )
34 25 32 33 isprimroot 
 |-  ( ph -> ( y e. ( V PrimRoots R ) <-> ( y e. ( Base ` V ) /\ ( R ( .g ` V ) y ) = ( 0g ` V ) /\ A. l e. NN0 ( ( l ( .g ` V ) y ) = ( 0g ` V ) -> R || l ) ) ) )
35 34 biimpd 
 |-  ( ph -> ( y e. ( V PrimRoots R ) -> ( y e. ( Base ` V ) /\ ( R ( .g ` V ) y ) = ( 0g ` V ) /\ A. l e. NN0 ( ( l ( .g ` V ) y ) = ( 0g ` V ) -> R || l ) ) ) )
36 35 imp 
 |-  ( ( ph /\ y e. ( V PrimRoots R ) ) -> ( y e. ( Base ` V ) /\ ( R ( .g ` V ) y ) = ( 0g ` V ) /\ A. l e. NN0 ( ( l ( .g ` V ) y ) = ( 0g ` V ) -> R || l ) ) )
37 36 simp1d 
 |-  ( ( ph /\ y e. ( V PrimRoots R ) ) -> y e. ( Base ` V ) )
38 37 23 eleqtrrdi 
 |-  ( ( ph /\ y e. ( V PrimRoots R ) ) -> y e. ( Base ` K ) )
39 23 7 27 31 38 mulgnn0cld 
 |-  ( ( ph /\ y e. ( V PrimRoots R ) ) -> ( E .^ y ) e. ( Base ` K ) )
40 28 simprd 
 |-  ( ph -> F e. B )
41 40 adantr 
 |-  ( ( ph /\ y e. ( V PrimRoots R ) ) -> F e. B )
42 eqidd 
 |-  ( ( ph /\ y e. ( V PrimRoots R ) ) -> ( ( O ` F ) ` ( E .^ y ) ) = ( ( O ` F ) ` ( E .^ y ) ) )
43 41 42 jca 
 |-  ( ( ph /\ y e. ( V PrimRoots R ) ) -> ( F e. B /\ ( ( O ` F ) ` ( E .^ y ) ) = ( ( O ` F ) ` ( E .^ y ) ) ) )
44 1 19 aks6d1c1p1rcl 
 |-  ( ph -> ( E e. NN /\ G e. B ) )
45 44 simprd 
 |-  ( ph -> G e. B )
46 45 adantr 
 |-  ( ( ph /\ y e. ( V PrimRoots R ) ) -> G e. B )
47 eqidd 
 |-  ( ( ph /\ y e. ( V PrimRoots R ) ) -> ( ( O ` G ) ` ( E .^ y ) ) = ( ( O ` G ) ` ( E .^ y ) ) )
48 46 47 jca 
 |-  ( ( ph /\ y e. ( V PrimRoots R ) ) -> ( G e. B /\ ( ( O ` G ) ` ( E .^ y ) ) = ( ( O ` G ) ` ( E .^ y ) ) ) )
49 eqid 
 |-  ( .r ` S ) = ( .r ` S )
50 5 49 mgpplusg 
 |-  ( .r ` S ) = ( +g ` W )
51 50 eqcomi 
 |-  ( +g ` W ) = ( .r ` S )
52 eqid 
 |-  ( .r ` K ) = ( .r ` K )
53 11 2 20 3 22 39 43 48 51 52 evl1muld 
 |-  ( ( ph /\ y e. ( V PrimRoots R ) ) -> ( ( F ( +g ` W ) G ) e. B /\ ( ( O ` ( F ( +g ` W ) G ) ) ` ( E .^ y ) ) = ( ( ( O ` F ) ` ( E .^ y ) ) ( .r ` K ) ( ( O ` G ) ` ( E .^ y ) ) ) ) )
54 53 simprd 
 |-  ( ( ph /\ y e. ( V PrimRoots R ) ) -> ( ( O ` ( F ( +g ` W ) G ) ) ` ( E .^ y ) ) = ( ( ( O ` F ) ` ( E .^ y ) ) ( .r ` K ) ( ( O ` G ) ` ( E .^ y ) ) ) )
55 25 adantr 
 |-  ( ( ph /\ y e. ( V PrimRoots R ) ) -> V e. CMnd )
56 11 2 20 3 22 38 41 fveval1fvcl 
 |-  ( ( ph /\ y e. ( V PrimRoots R ) ) -> ( ( O ` F ) ` y ) e. ( Base ` K ) )
57 6 eqcomi 
 |-  ( mulGrp ` K ) = V
58 57 fveq2i 
 |-  ( Base ` ( mulGrp ` K ) ) = ( Base ` V )
59 23 58 eqtr4i 
 |-  ( Base ` K ) = ( Base ` ( mulGrp ` K ) )
60 59 a1i 
 |-  ( ( ph /\ y e. ( V PrimRoots R ) ) -> ( Base ` K ) = ( Base ` ( mulGrp ` K ) ) )
61 60 eleq2d 
 |-  ( ( ph /\ y e. ( V PrimRoots R ) ) -> ( ( ( O ` F ) ` y ) e. ( Base ` K ) <-> ( ( O ` F ) ` y ) e. ( Base ` ( mulGrp ` K ) ) ) )
62 56 61 mpbid 
 |-  ( ( ph /\ y e. ( V PrimRoots R ) ) -> ( ( O ` F ) ` y ) e. ( Base ` ( mulGrp ` K ) ) )
63 11 2 20 3 22 38 46 fveval1fvcl 
 |-  ( ( ph /\ y e. ( V PrimRoots R ) ) -> ( ( O ` G ) ` y ) e. ( Base ` K ) )
64 60 eleq2d 
 |-  ( ( ph /\ y e. ( V PrimRoots R ) ) -> ( ( ( O ` G ) ` y ) e. ( Base ` K ) <-> ( ( O ` G ) ` y ) e. ( Base ` ( mulGrp ` K ) ) ) )
65 63 64 mpbid 
 |-  ( ( ph /\ y e. ( V PrimRoots R ) ) -> ( ( O ` G ) ` y ) e. ( Base ` ( mulGrp ` K ) ) )
66 31 62 65 3jca 
 |-  ( ( ph /\ y e. ( V PrimRoots R ) ) -> ( E e. NN0 /\ ( ( O ` F ) ` y ) e. ( Base ` ( mulGrp ` K ) ) /\ ( ( O ` G ) ` y ) e. ( Base ` ( mulGrp ` K ) ) ) )
67 57 fveq2i 
 |-  ( +g ` ( mulGrp ` K ) ) = ( +g ` V )
68 58 7 67 mulgnn0di 
 |-  ( ( V e. CMnd /\ ( E e. NN0 /\ ( ( O ` F ) ` y ) e. ( Base ` ( mulGrp ` K ) ) /\ ( ( O ` G ) ` y ) e. ( Base ` ( mulGrp ` K ) ) ) ) -> ( E .^ ( ( ( O ` F ) ` y ) ( +g ` ( mulGrp ` K ) ) ( ( O ` G ) ` y ) ) ) = ( ( E .^ ( ( O ` F ) ` y ) ) ( +g ` ( mulGrp ` K ) ) ( E .^ ( ( O ` G ) ` y ) ) ) )
69 55 66 68 syl2anc 
 |-  ( ( ph /\ y e. ( V PrimRoots R ) ) -> ( E .^ ( ( ( O ` F ) ` y ) ( +g ` ( mulGrp ` K ) ) ( ( O ` G ) ` y ) ) ) = ( ( E .^ ( ( O ` F ) ` y ) ) ( +g ` ( mulGrp ` K ) ) ( E .^ ( ( O ` G ) ` y ) ) ) )
70 6 52 mgpplusg 
 |-  ( .r ` K ) = ( +g ` V )
71 6 fveq2i 
 |-  ( +g ` V ) = ( +g ` ( mulGrp ` K ) )
72 70 71 eqtri 
 |-  ( .r ` K ) = ( +g ` ( mulGrp ` K ) )
73 72 a1i 
 |-  ( ( ph /\ y e. ( V PrimRoots R ) ) -> ( .r ` K ) = ( +g ` ( mulGrp ` K ) ) )
74 73 eqcomd 
 |-  ( ( ph /\ y e. ( V PrimRoots R ) ) -> ( +g ` ( mulGrp ` K ) ) = ( .r ` K ) )
75 fveq2 
 |-  ( z = y -> ( ( O ` F ) ` z ) = ( ( O ` F ) ` y ) )
76 75 oveq2d 
 |-  ( z = y -> ( E .^ ( ( O ` F ) ` z ) ) = ( E .^ ( ( O ` F ) ` y ) ) )
77 oveq2 
 |-  ( z = y -> ( E .^ z ) = ( E .^ y ) )
78 77 fveq2d 
 |-  ( z = y -> ( ( O ` F ) ` ( E .^ z ) ) = ( ( O ` F ) ` ( E .^ y ) ) )
79 76 78 eqeq12d 
 |-  ( z = y -> ( ( E .^ ( ( O ` F ) ` z ) ) = ( ( O ` F ) ` ( E .^ z ) ) <-> ( E .^ ( ( O ` F ) ` y ) ) = ( ( O ` F ) ` ( E .^ y ) ) ) )
80 1 40 29 aks6d1c1p1 
 |-  ( ph -> ( E .~ F <-> A. y e. ( V PrimRoots R ) ( E .^ ( ( O ` F ) ` y ) ) = ( ( O ` F ) ` ( E .^ y ) ) ) )
81 18 80 mpbid 
 |-  ( ph -> A. y e. ( V PrimRoots R ) ( E .^ ( ( O ` F ) ` y ) ) = ( ( O ` F ) ` ( E .^ y ) ) )
82 fveq2 
 |-  ( y = z -> ( ( O ` F ) ` y ) = ( ( O ` F ) ` z ) )
83 82 oveq2d 
 |-  ( y = z -> ( E .^ ( ( O ` F ) ` y ) ) = ( E .^ ( ( O ` F ) ` z ) ) )
84 oveq2 
 |-  ( y = z -> ( E .^ y ) = ( E .^ z ) )
85 84 fveq2d 
 |-  ( y = z -> ( ( O ` F ) ` ( E .^ y ) ) = ( ( O ` F ) ` ( E .^ z ) ) )
86 83 85 eqeq12d 
 |-  ( y = z -> ( ( E .^ ( ( O ` F ) ` y ) ) = ( ( O ` F ) ` ( E .^ y ) ) <-> ( E .^ ( ( O ` F ) ` z ) ) = ( ( O ` F ) ` ( E .^ z ) ) ) )
87 86 cbvralvw 
 |-  ( A. y e. ( V PrimRoots R ) ( E .^ ( ( O ` F ) ` y ) ) = ( ( O ` F ) ` ( E .^ y ) ) <-> A. z e. ( V PrimRoots R ) ( E .^ ( ( O ` F ) ` z ) ) = ( ( O ` F ) ` ( E .^ z ) ) )
88 81 87 sylib 
 |-  ( ph -> A. z e. ( V PrimRoots R ) ( E .^ ( ( O ` F ) ` z ) ) = ( ( O ` F ) ` ( E .^ z ) ) )
89 88 adantr 
 |-  ( ( ph /\ y e. ( V PrimRoots R ) ) -> A. z e. ( V PrimRoots R ) ( E .^ ( ( O ` F ) ` z ) ) = ( ( O ` F ) ` ( E .^ z ) ) )
90 simpr 
 |-  ( ( ph /\ y e. ( V PrimRoots R ) ) -> y e. ( V PrimRoots R ) )
91 79 89 90 rspcdva 
 |-  ( ( ph /\ y e. ( V PrimRoots R ) ) -> ( E .^ ( ( O ` F ) ` y ) ) = ( ( O ` F ) ` ( E .^ y ) ) )
92 fveq2 
 |-  ( z = y -> ( ( O ` G ) ` z ) = ( ( O ` G ) ` y ) )
93 92 oveq2d 
 |-  ( z = y -> ( E .^ ( ( O ` G ) ` z ) ) = ( E .^ ( ( O ` G ) ` y ) ) )
94 77 fveq2d 
 |-  ( z = y -> ( ( O ` G ) ` ( E .^ z ) ) = ( ( O ` G ) ` ( E .^ y ) ) )
95 93 94 eqeq12d 
 |-  ( z = y -> ( ( E .^ ( ( O ` G ) ` z ) ) = ( ( O ` G ) ` ( E .^ z ) ) <-> ( E .^ ( ( O ` G ) ` y ) ) = ( ( O ` G ) ` ( E .^ y ) ) ) )
96 1 45 29 aks6d1c1p1 
 |-  ( ph -> ( E .~ G <-> A. y e. ( V PrimRoots R ) ( E .^ ( ( O ` G ) ` y ) ) = ( ( O ` G ) ` ( E .^ y ) ) ) )
97 19 96 mpbid 
 |-  ( ph -> A. y e. ( V PrimRoots R ) ( E .^ ( ( O ` G ) ` y ) ) = ( ( O ` G ) ` ( E .^ y ) ) )
98 fveq2 
 |-  ( y = z -> ( ( O ` G ) ` y ) = ( ( O ` G ) ` z ) )
99 98 oveq2d 
 |-  ( y = z -> ( E .^ ( ( O ` G ) ` y ) ) = ( E .^ ( ( O ` G ) ` z ) ) )
100 84 fveq2d 
 |-  ( y = z -> ( ( O ` G ) ` ( E .^ y ) ) = ( ( O ` G ) ` ( E .^ z ) ) )
101 99 100 eqeq12d 
 |-  ( y = z -> ( ( E .^ ( ( O ` G ) ` y ) ) = ( ( O ` G ) ` ( E .^ y ) ) <-> ( E .^ ( ( O ` G ) ` z ) ) = ( ( O ` G ) ` ( E .^ z ) ) ) )
102 101 cbvralvw 
 |-  ( A. y e. ( V PrimRoots R ) ( E .^ ( ( O ` G ) ` y ) ) = ( ( O ` G ) ` ( E .^ y ) ) <-> A. z e. ( V PrimRoots R ) ( E .^ ( ( O ` G ) ` z ) ) = ( ( O ` G ) ` ( E .^ z ) ) )
103 97 102 sylib 
 |-  ( ph -> A. z e. ( V PrimRoots R ) ( E .^ ( ( O ` G ) ` z ) ) = ( ( O ` G ) ` ( E .^ z ) ) )
104 103 adantr 
 |-  ( ( ph /\ y e. ( V PrimRoots R ) ) -> A. z e. ( V PrimRoots R ) ( E .^ ( ( O ` G ) ` z ) ) = ( ( O ` G ) ` ( E .^ z ) ) )
105 95 104 90 rspcdva 
 |-  ( ( ph /\ y e. ( V PrimRoots R ) ) -> ( E .^ ( ( O ` G ) ` y ) ) = ( ( O ` G ) ` ( E .^ y ) ) )
106 74 91 105 oveq123d 
 |-  ( ( ph /\ y e. ( V PrimRoots R ) ) -> ( ( E .^ ( ( O ` F ) ` y ) ) ( +g ` ( mulGrp ` K ) ) ( E .^ ( ( O ` G ) ` y ) ) ) = ( ( ( O ` F ) ` ( E .^ y ) ) ( .r ` K ) ( ( O ` G ) ` ( E .^ y ) ) ) )
107 69 106 eqtr2d 
 |-  ( ( ph /\ y e. ( V PrimRoots R ) ) -> ( ( ( O ` F ) ` ( E .^ y ) ) ( .r ` K ) ( ( O ` G ) ` ( E .^ y ) ) ) = ( E .^ ( ( ( O ` F ) ` y ) ( +g ` ( mulGrp ` K ) ) ( ( O ` G ) ` y ) ) ) )
108 72 eqcomi 
 |-  ( +g ` ( mulGrp ` K ) ) = ( .r ` K )
109 108 a1i 
 |-  ( ( ph /\ y e. ( V PrimRoots R ) ) -> ( +g ` ( mulGrp ` K ) ) = ( .r ` K ) )
110 109 oveqd 
 |-  ( ( ph /\ y e. ( V PrimRoots R ) ) -> ( ( ( O ` F ) ` y ) ( +g ` ( mulGrp ` K ) ) ( ( O ` G ) ` y ) ) = ( ( ( O ` F ) ` y ) ( .r ` K ) ( ( O ` G ) ` y ) ) )
111 110 oveq2d 
 |-  ( ( ph /\ y e. ( V PrimRoots R ) ) -> ( E .^ ( ( ( O ` F ) ` y ) ( +g ` ( mulGrp ` K ) ) ( ( O ` G ) ` y ) ) ) = ( E .^ ( ( ( O ` F ) ` y ) ( .r ` K ) ( ( O ` G ) ` y ) ) ) )
112 107 111 eqtrd 
 |-  ( ( ph /\ y e. ( V PrimRoots R ) ) -> ( ( ( O ` F ) ` ( E .^ y ) ) ( .r ` K ) ( ( O ` G ) ` ( E .^ y ) ) ) = ( E .^ ( ( ( O ` F ) ` y ) ( .r ` K ) ( ( O ` G ) ` y ) ) ) )
113 eqidd 
 |-  ( ( ph /\ y e. ( V PrimRoots R ) ) -> ( ( O ` F ) ` y ) = ( ( O ` F ) ` y ) )
114 41 113 jca 
 |-  ( ( ph /\ y e. ( V PrimRoots R ) ) -> ( F e. B /\ ( ( O ` F ) ` y ) = ( ( O ` F ) ` y ) ) )
115 eqidd 
 |-  ( ( ph /\ y e. ( V PrimRoots R ) ) -> ( ( O ` G ) ` y ) = ( ( O ` G ) ` y ) )
116 46 115 jca 
 |-  ( ( ph /\ y e. ( V PrimRoots R ) ) -> ( G e. B /\ ( ( O ` G ) ` y ) = ( ( O ` G ) ` y ) ) )
117 11 2 20 3 22 38 114 116 51 52 evl1muld 
 |-  ( ( ph /\ y e. ( V PrimRoots R ) ) -> ( ( F ( +g ` W ) G ) e. B /\ ( ( O ` ( F ( +g ` W ) G ) ) ` y ) = ( ( ( O ` F ) ` y ) ( .r ` K ) ( ( O ` G ) ` y ) ) ) )
118 117 simprd 
 |-  ( ( ph /\ y e. ( V PrimRoots R ) ) -> ( ( O ` ( F ( +g ` W ) G ) ) ` y ) = ( ( ( O ` F ) ` y ) ( .r ` K ) ( ( O ` G ) ` y ) ) )
119 118 eqcomd 
 |-  ( ( ph /\ y e. ( V PrimRoots R ) ) -> ( ( ( O ` F ) ` y ) ( .r ` K ) ( ( O ` G ) ` y ) ) = ( ( O ` ( F ( +g ` W ) G ) ) ` y ) )
120 119 oveq2d 
 |-  ( ( ph /\ y e. ( V PrimRoots R ) ) -> ( E .^ ( ( ( O ` F ) ` y ) ( .r ` K ) ( ( O ` G ) ` y ) ) ) = ( E .^ ( ( O ` ( F ( +g ` W ) G ) ) ` y ) ) )
121 112 120 eqtrd 
 |-  ( ( ph /\ y e. ( V PrimRoots R ) ) -> ( ( ( O ` F ) ` ( E .^ y ) ) ( .r ` K ) ( ( O ` G ) ` ( E .^ y ) ) ) = ( E .^ ( ( O ` ( F ( +g ` W ) G ) ) ` y ) ) )
122 54 121 eqtrd 
 |-  ( ( ph /\ y e. ( V PrimRoots R ) ) -> ( ( O ` ( F ( +g ` W ) G ) ) ` ( E .^ y ) ) = ( E .^ ( ( O ` ( F ( +g ` W ) G ) ) ` y ) ) )
123 122 eqcomd 
 |-  ( ( ph /\ y e. ( V PrimRoots R ) ) -> ( E .^ ( ( O ` ( F ( +g ` W ) G ) ) ` y ) ) = ( ( O ` ( F ( +g ` W ) G ) ) ` ( E .^ y ) ) )
124 123 ralrimiva 
 |-  ( ph -> A. y e. ( V PrimRoots R ) ( E .^ ( ( O ` ( F ( +g ` W ) G ) ) ` y ) ) = ( ( O ` ( F ( +g ` W ) G ) ) ` ( E .^ y ) ) )
125 2 ply1crng 
 |-  ( K e. CRing -> S e. CRing )
126 21 125 syl 
 |-  ( ph -> S e. CRing )
127 126 crngringd 
 |-  ( ph -> S e. Ring )
128 3 51 127 40 45 ringcld 
 |-  ( ph -> ( F ( +g ` W ) G ) e. B )
129 1 128 29 aks6d1c1p1 
 |-  ( ph -> ( E .~ ( F ( +g ` W ) G ) <-> A. y e. ( V PrimRoots R ) ( E .^ ( ( O ` ( F ( +g ` W ) G ) ) ` y ) ) = ( ( O ` ( F ( +g ` W ) G ) ) ` ( E .^ y ) ) ) )
130 124 129 mpbird 
 |-  ( ph -> E .~ ( F ( +g ` W ) G ) )