Metamath Proof Explorer

Theorem aks6d1c6lem1

Description: Lemma for claim 6, deduce exact degree of the polynomial. (Contributed by metakunt, 7-May-2025)

Ref Expression
Hypotheses aks6d1c6.1 
|- .~ = { <. e , f >. | ( e e. NN /\ f e. ( Base ` ( Poly1 ` K ) ) /\ A. y e. ( ( mulGrp ` K ) PrimRoots R ) ( e ( .g ` ( mulGrp ` K ) ) ( ( ( eval1 ` K ) ` f ) ` y ) ) = ( ( ( eval1 ` K ) ` f ) ` ( e ( .g ` ( mulGrp ` K ) ) y ) ) ) }
aks6d1c6.2 
|- P = ( chr ` K )
aks6d1c6.3 
|- ( ph -> K e. Field )
aks6d1c6.4 
|- ( ph -> P e. Prime )
aks6d1c6.5 
|- ( ph -> R e. NN )
aks6d1c6.6 
|- ( ph -> N e. NN )
aks6d1c6.7 
|- ( ph -> P || N )
aks6d1c6.8 
|- ( ph -> ( N gcd R ) = 1 )
aks6d1c6.9 
|- ( ph -> A < P )
aks6d1c6.10 
|- G = ( g e. ( NN0 ^m ( 0 ... A ) ) |-> ( ( mulGrp ` ( Poly1 ` K ) ) gsum ( i e. ( 0 ... A ) |-> ( ( g ` i ) ( .g ` ( mulGrp ` ( Poly1 ` K ) ) ) ( ( var1 ` K ) ( +g ` ( Poly1 ` K ) ) ( ( algSc ` ( Poly1 ` K ) ) ` ( ( ZRHom ` K ) ` i ) ) ) ) ) ) )
aks6d1c6.11 
|- ( ph -> A e. NN0 )
aks6d1c6.12 
|- E = ( k e. NN0 , l e. NN0 |-> ( ( P ^ k ) x. ( ( N / P ) ^ l ) ) )
aks6d1c6.13 
|- L = ( ZRHom ` ( Z/nZ ` R ) )
aks6d1c6.14 
|- ( ph -> A. a e. ( 1 ... A ) N .~ ( ( var1 ` K ) ( +g ` ( Poly1 ` K ) ) ( ( algSc ` ( Poly1 ` K ) ) ` ( ( ZRHom ` K ) ` a ) ) ) )
aks6d1c6.15 
|- ( ph -> ( x e. ( Base ` K ) |-> ( P ( .g ` ( mulGrp ` K ) ) x ) ) e. ( K RingIso K ) )
aks6d1c6.16 
|- ( ph -> M e. ( ( mulGrp ` K ) PrimRoots R ) )
aks6d1c6.17 
|- H = ( h e. ( NN0 ^m ( 0 ... A ) ) |-> ( ( ( eval1 ` K ) ` ( G ` h ) ) ` M ) )
aks6d1c6.18 
|- D = ( # ` ( L " ( E " ( NN0 X. NN0 ) ) ) )
aks6d1c6.19 
|- S = { s e. ( NN0 ^m ( 0 ... A ) ) | sum_ t e. ( 0 ... A ) ( s ` t ) <_ ( D - 1 ) }
aks6d1c6lem1.1 
|- ( ph -> U e. ( NN0 ^m ( 0 ... A ) ) )
Assertion aks6d1c6lem1 
|- ( ph -> ( ( deg1 ` K ) ` ( G ` U ) ) = sum_ t e. ( 0 ... A ) ( U ` t ) )

Proof

Step Hyp Ref Expression
1 aks6d1c6.1 
 |-  .~ = { <. e , f >. | ( e e. NN /\ f e. ( Base ` ( Poly1 ` K ) ) /\ A. y e. ( ( mulGrp ` K ) PrimRoots R ) ( e ( .g ` ( mulGrp ` K ) ) ( ( ( eval1 ` K ) ` f ) ` y ) ) = ( ( ( eval1 ` K ) ` f ) ` ( e ( .g ` ( mulGrp ` K ) ) y ) ) ) }
2 aks6d1c6.2 
 |-  P = ( chr ` K )
3 aks6d1c6.3 
 |-  ( ph -> K e. Field )
4 aks6d1c6.4 
 |-  ( ph -> P e. Prime )
5 aks6d1c6.5 
 |-  ( ph -> R e. NN )
6 aks6d1c6.6 
 |-  ( ph -> N e. NN )
7 aks6d1c6.7 
 |-  ( ph -> P || N )
8 aks6d1c6.8 
 |-  ( ph -> ( N gcd R ) = 1 )
9 aks6d1c6.9 
 |-  ( ph -> A < P )
10 aks6d1c6.10 
 |-  G = ( g e. ( NN0 ^m ( 0 ... A ) ) |-> ( ( mulGrp ` ( Poly1 ` K ) ) gsum ( i e. ( 0 ... A ) |-> ( ( g ` i ) ( .g ` ( mulGrp ` ( Poly1 ` K ) ) ) ( ( var1 ` K ) ( +g ` ( Poly1 ` K ) ) ( ( algSc ` ( Poly1 ` K ) ) ` ( ( ZRHom ` K ) ` i ) ) ) ) ) ) )
11 aks6d1c6.11 
 |-  ( ph -> A e. NN0 )
12 aks6d1c6.12 
 |-  E = ( k e. NN0 , l e. NN0 |-> ( ( P ^ k ) x. ( ( N / P ) ^ l ) ) )
13 aks6d1c6.13 
 |-  L = ( ZRHom ` ( Z/nZ ` R ) )
14 aks6d1c6.14 
 |-  ( ph -> A. a e. ( 1 ... A ) N .~ ( ( var1 ` K ) ( +g ` ( Poly1 ` K ) ) ( ( algSc ` ( Poly1 ` K ) ) ` ( ( ZRHom ` K ) ` a ) ) ) )
15 aks6d1c6.15 
 |-  ( ph -> ( x e. ( Base ` K ) |-> ( P ( .g ` ( mulGrp ` K ) ) x ) ) e. ( K RingIso K ) )
16 aks6d1c6.16 
 |-  ( ph -> M e. ( ( mulGrp ` K ) PrimRoots R ) )
17 aks6d1c6.17 
 |-  H = ( h e. ( NN0 ^m ( 0 ... A ) ) |-> ( ( ( eval1 ` K ) ` ( G ` h ) ) ` M ) )
18 aks6d1c6.18 
 |-  D = ( # ` ( L " ( E " ( NN0 X. NN0 ) ) ) )
19 aks6d1c6.19 
 |-  S = { s e. ( NN0 ^m ( 0 ... A ) ) | sum_ t e. ( 0 ... A ) ( s ` t ) <_ ( D - 1 ) }
20 aks6d1c6lem1.1 
 |-  ( ph -> U e. ( NN0 ^m ( 0 ... A ) ) )
21 10 a1i 
 |-  ( ph -> G = ( g e. ( NN0 ^m ( 0 ... A ) ) |-> ( ( mulGrp ` ( Poly1 ` K ) ) gsum ( i e. ( 0 ... A ) |-> ( ( g ` i ) ( .g ` ( mulGrp ` ( Poly1 ` K ) ) ) ( ( var1 ` K ) ( +g ` ( Poly1 ` K ) ) ( ( algSc ` ( Poly1 ` K ) ) ` ( ( ZRHom ` K ) ` i ) ) ) ) ) ) ) )
22 21 fveq1d 
 |-  ( ph -> ( G ` U ) = ( ( g e. ( NN0 ^m ( 0 ... A ) ) |-> ( ( mulGrp ` ( Poly1 ` K ) ) gsum ( i e. ( 0 ... A ) |-> ( ( g ` i ) ( .g ` ( mulGrp ` ( Poly1 ` K ) ) ) ( ( var1 ` K ) ( +g ` ( Poly1 ` K ) ) ( ( algSc ` ( Poly1 ` K ) ) ` ( ( ZRHom ` K ) ` i ) ) ) ) ) ) ) ` U ) )
23 22 fveq2d 
 |-  ( ph -> ( ( deg1 ` K ) ` ( G ` U ) ) = ( ( deg1 ` K ) ` ( ( g e. ( NN0 ^m ( 0 ... A ) ) |-> ( ( mulGrp ` ( Poly1 ` K ) ) gsum ( i e. ( 0 ... A ) |-> ( ( g ` i ) ( .g ` ( mulGrp ` ( Poly1 ` K ) ) ) ( ( var1 ` K ) ( +g ` ( Poly1 ` K ) ) ( ( algSc ` ( Poly1 ` K ) ) ` ( ( ZRHom ` K ) ` i ) ) ) ) ) ) ) ` U ) ) )
24 eqidd 
 |-  ( ph -> ( g e. ( NN0 ^m ( 0 ... A ) ) |-> ( ( mulGrp ` ( Poly1 ` K ) ) gsum ( i e. ( 0 ... A ) |-> ( ( g ` i ) ( .g ` ( mulGrp ` ( Poly1 ` K ) ) ) ( ( var1 ` K ) ( +g ` ( Poly1 ` K ) ) ( ( algSc ` ( Poly1 ` K ) ) ` ( ( ZRHom ` K ) ` i ) ) ) ) ) ) ) = ( g e. ( NN0 ^m ( 0 ... A ) ) |-> ( ( mulGrp ` ( Poly1 ` K ) ) gsum ( i e. ( 0 ... A ) |-> ( ( g ` i ) ( .g ` ( mulGrp ` ( Poly1 ` K ) ) ) ( ( var1 ` K ) ( +g ` ( Poly1 ` K ) ) ( ( algSc ` ( Poly1 ` K ) ) ` ( ( ZRHom ` K ) ` i ) ) ) ) ) ) ) )
25 simplr 
 |-  ( ( ( ph /\ g = U ) /\ i e. ( 0 ... A ) ) -> g = U )
26 25 fveq1d 
 |-  ( ( ( ph /\ g = U ) /\ i e. ( 0 ... A ) ) -> ( g ` i ) = ( U ` i ) )
27 26 oveq1d 
 |-  ( ( ( ph /\ g = U ) /\ i e. ( 0 ... A ) ) -> ( ( g ` i ) ( .g ` ( mulGrp ` ( Poly1 ` K ) ) ) ( ( var1 ` K ) ( +g ` ( Poly1 ` K ) ) ( ( algSc ` ( Poly1 ` K ) ) ` ( ( ZRHom ` K ) ` i ) ) ) ) = ( ( U ` i ) ( .g ` ( mulGrp ` ( Poly1 ` K ) ) ) ( ( var1 ` K ) ( +g ` ( Poly1 ` K ) ) ( ( algSc ` ( Poly1 ` K ) ) ` ( ( ZRHom ` K ) ` i ) ) ) ) )
28 27 mpteq2dva 
 |-  ( ( ph /\ g = U ) -> ( i e. ( 0 ... A ) |-> ( ( g ` i ) ( .g ` ( mulGrp ` ( Poly1 ` K ) ) ) ( ( var1 ` K ) ( +g ` ( Poly1 ` K ) ) ( ( algSc ` ( Poly1 ` K ) ) ` ( ( ZRHom ` K ) ` i ) ) ) ) ) = ( i e. ( 0 ... A ) |-> ( ( U ` i ) ( .g ` ( mulGrp ` ( Poly1 ` K ) ) ) ( ( var1 ` K ) ( +g ` ( Poly1 ` K ) ) ( ( algSc ` ( Poly1 ` K ) ) ` ( ( ZRHom ` K ) ` i ) ) ) ) ) )
29 28 oveq2d 
 |-  ( ( ph /\ g = U ) -> ( ( mulGrp ` ( Poly1 ` K ) ) gsum ( i e. ( 0 ... A ) |-> ( ( g ` i ) ( .g ` ( mulGrp ` ( Poly1 ` K ) ) ) ( ( var1 ` K ) ( +g ` ( Poly1 ` K ) ) ( ( algSc ` ( Poly1 ` K ) ) ` ( ( ZRHom ` K ) ` i ) ) ) ) ) ) = ( ( mulGrp ` ( Poly1 ` K ) ) gsum ( i e. ( 0 ... A ) |-> ( ( U ` i ) ( .g ` ( mulGrp ` ( Poly1 ` K ) ) ) ( ( var1 ` K ) ( +g ` ( Poly1 ` K ) ) ( ( algSc ` ( Poly1 ` K ) ) ` ( ( ZRHom ` K ) ` i ) ) ) ) ) ) )
30 ovexd 
 |-  ( ph -> ( ( mulGrp ` ( Poly1 ` K ) ) gsum ( i e. ( 0 ... A ) |-> ( ( U ` i ) ( .g ` ( mulGrp ` ( Poly1 ` K ) ) ) ( ( var1 ` K ) ( +g ` ( Poly1 ` K ) ) ( ( algSc ` ( Poly1 ` K ) ) ` ( ( ZRHom ` K ) ` i ) ) ) ) ) ) e. _V )
31 24 29 20 30 fvmptd 
 |-  ( ph -> ( ( g e. ( NN0 ^m ( 0 ... A ) ) |-> ( ( mulGrp ` ( Poly1 ` K ) ) gsum ( i e. ( 0 ... A ) |-> ( ( g ` i ) ( .g ` ( mulGrp ` ( Poly1 ` K ) ) ) ( ( var1 ` K ) ( +g ` ( Poly1 ` K ) ) ( ( algSc ` ( Poly1 ` K ) ) ` ( ( ZRHom ` K ) ` i ) ) ) ) ) ) ) ` U ) = ( ( mulGrp ` ( Poly1 ` K ) ) gsum ( i e. ( 0 ... A ) |-> ( ( U ` i ) ( .g ` ( mulGrp ` ( Poly1 ` K ) ) ) ( ( var1 ` K ) ( +g ` ( Poly1 ` K ) ) ( ( algSc ` ( Poly1 ` K ) ) ` ( ( ZRHom ` K ) ` i ) ) ) ) ) ) )
32 31 fveq2d 
 |-  ( ph -> ( ( deg1 ` K ) ` ( ( g e. ( NN0 ^m ( 0 ... A ) ) |-> ( ( mulGrp ` ( Poly1 ` K ) ) gsum ( i e. ( 0 ... A ) |-> ( ( g ` i ) ( .g ` ( mulGrp ` ( Poly1 ` K ) ) ) ( ( var1 ` K ) ( +g ` ( Poly1 ` K ) ) ( ( algSc ` ( Poly1 ` K ) ) ` ( ( ZRHom ` K ) ` i ) ) ) ) ) ) ) ` U ) ) = ( ( deg1 ` K ) ` ( ( mulGrp ` ( Poly1 ` K ) ) gsum ( i e. ( 0 ... A ) |-> ( ( U ` i ) ( .g ` ( mulGrp ` ( Poly1 ` K ) ) ) ( ( var1 ` K ) ( +g ` ( Poly1 ` K ) ) ( ( algSc ` ( Poly1 ` K ) ) ` ( ( ZRHom ` K ) ` i ) ) ) ) ) ) ) )
33 fldidom 
 |-  ( K e. Field -> K e. IDomn )
34 3 33 syl 
 |-  ( ph -> K e. IDomn )
35 fzfid 
 |-  ( ph -> ( 0 ... A ) e. Fin )
36 eqid 
 |-  ( mulGrp ` ( Poly1 ` K ) ) = ( mulGrp ` ( Poly1 ` K ) )
37 eqid 
 |-  ( Base ` ( Poly1 ` K ) ) = ( Base ` ( Poly1 ` K ) )
38 36 37 mgpbas 
 |-  ( Base ` ( Poly1 ` K ) ) = ( Base ` ( mulGrp ` ( Poly1 ` K ) ) )
39 eqid 
 |-  ( .g ` ( mulGrp ` ( Poly1 ` K ) ) ) = ( .g ` ( mulGrp ` ( Poly1 ` K ) ) )
40 3 fldcrngd 
 |-  ( ph -> K e. CRing )
41 crngring 
 |-  ( K e. CRing -> K e. Ring )
42 40 41 syl 
 |-  ( ph -> K e. Ring )
43 eqid 
 |-  ( Poly1 ` K ) = ( Poly1 ` K )
44 43 ply1ring 
 |-  ( K e. Ring -> ( Poly1 ` K ) e. Ring )
45 42 44 syl 
 |-  ( ph -> ( Poly1 ` K ) e. Ring )
46 36 ringmgp 
 |-  ( ( Poly1 ` K ) e. Ring -> ( mulGrp ` ( Poly1 ` K ) ) e. Mnd )
47 45 46 syl 
 |-  ( ph -> ( mulGrp ` ( Poly1 ` K ) ) e. Mnd )
48 47 adantr 
 |-  ( ( ph /\ i e. ( 0 ... A ) ) -> ( mulGrp ` ( Poly1 ` K ) ) e. Mnd )
49 nn0ex 
 |-  NN0 e. _V
50 49 a1i 
 |-  ( ph -> NN0 e. _V )
51 ovexd 
 |-  ( ph -> ( 0 ... A ) e. _V )
52 50 51 elmapd 
 |-  ( ph -> ( U e. ( NN0 ^m ( 0 ... A ) ) <-> U : ( 0 ... A ) --> NN0 ) )
53 20 52 mpbid 
 |-  ( ph -> U : ( 0 ... A ) --> NN0 )
54 53 adantr 
 |-  ( ( ph /\ i e. ( 0 ... A ) ) -> U : ( 0 ... A ) --> NN0 )
55 simpr 
 |-  ( ( ph /\ i e. ( 0 ... A ) ) -> i e. ( 0 ... A ) )
56 54 55 ffvelcdmd 
 |-  ( ( ph /\ i e. ( 0 ... A ) ) -> ( U ` i ) e. NN0 )
57 2fveq3 
 |-  ( t = i -> ( ( algSc ` ( Poly1 ` K ) ) ` ( ( ZRHom ` K ) ` t ) ) = ( ( algSc ` ( Poly1 ` K ) ) ` ( ( ZRHom ` K ) ` i ) ) )
58 57 oveq2d 
 |-  ( t = i -> ( ( var1 ` K ) ( +g ` ( Poly1 ` K ) ) ( ( algSc ` ( Poly1 ` K ) ) ` ( ( ZRHom ` K ) ` t ) ) ) = ( ( var1 ` K ) ( +g ` ( Poly1 ` K ) ) ( ( algSc ` ( Poly1 ` K ) ) ` ( ( ZRHom ` K ) ` i ) ) ) )
59 58 eleq1d 
 |-  ( t = i -> ( ( ( var1 ` K ) ( +g ` ( Poly1 ` K ) ) ( ( algSc ` ( Poly1 ` K ) ) ` ( ( ZRHom ` K ) ` t ) ) ) e. ( Base ` ( Poly1 ` K ) ) <-> ( ( var1 ` K ) ( +g ` ( Poly1 ` K ) ) ( ( algSc ` ( Poly1 ` K ) ) ` ( ( ZRHom ` K ) ` i ) ) ) e. ( Base ` ( Poly1 ` K ) ) ) )
60 ringmnd 
 |-  ( ( Poly1 ` K ) e. Ring -> ( Poly1 ` K ) e. Mnd )
61 45 60 syl 
 |-  ( ph -> ( Poly1 ` K ) e. Mnd )
62 61 adantr 
 |-  ( ( ph /\ t e. ( 0 ... A ) ) -> ( Poly1 ` K ) e. Mnd )
63 42 adantr 
 |-  ( ( ph /\ t e. ( 0 ... A ) ) -> K e. Ring )
64 eqid 
 |-  ( var1 ` K ) = ( var1 ` K )
65 64 43 37 vr1cl 
 |-  ( K e. Ring -> ( var1 ` K ) e. ( Base ` ( Poly1 ` K ) ) )
66 63 65 syl 
 |-  ( ( ph /\ t e. ( 0 ... A ) ) -> ( var1 ` K ) e. ( Base ` ( Poly1 ` K ) ) )
67 eqid 
 |-  ( ZRHom ` K ) = ( ZRHom ` K )
68 67 zrhrhm 
 |-  ( K e. Ring -> ( ZRHom ` K ) e. ( ZZring RingHom K ) )
69 42 68 syl 
 |-  ( ph -> ( ZRHom ` K ) e. ( ZZring RingHom K ) )
70 zringbas 
 |-  ZZ = ( Base ` ZZring )
71 eqid 
 |-  ( Base ` K ) = ( Base ` K )
72 70 71 rhmf 
 |-  ( ( ZRHom ` K ) e. ( ZZring RingHom K ) -> ( ZRHom ` K ) : ZZ --> ( Base ` K ) )
73 69 72 syl 
 |-  ( ph -> ( ZRHom ` K ) : ZZ --> ( Base ` K ) )
74 73 adantr 
 |-  ( ( ph /\ t e. ( 0 ... A ) ) -> ( ZRHom ` K ) : ZZ --> ( Base ` K ) )
75 elfzelz 
 |-  ( t e. ( 0 ... A ) -> t e. ZZ )
76 75 adantl 
 |-  ( ( ph /\ t e. ( 0 ... A ) ) -> t e. ZZ )
77 74 76 ffvelcdmd 
 |-  ( ( ph /\ t e. ( 0 ... A ) ) -> ( ( ZRHom ` K ) ` t ) e. ( Base ` K ) )
78 eqid 
 |-  ( algSc ` ( Poly1 ` K ) ) = ( algSc ` ( Poly1 ` K ) )
79 43 78 71 37 ply1sclcl 
 |-  ( ( K e. Ring /\ ( ( ZRHom ` K ) ` t ) e. ( Base ` K ) ) -> ( ( algSc ` ( Poly1 ` K ) ) ` ( ( ZRHom ` K ) ` t ) ) e. ( Base ` ( Poly1 ` K ) ) )
80 63 77 79 syl2anc 
 |-  ( ( ph /\ t e. ( 0 ... A ) ) -> ( ( algSc ` ( Poly1 ` K ) ) ` ( ( ZRHom ` K ) ` t ) ) e. ( Base ` ( Poly1 ` K ) ) )
81 eqid 
 |-  ( +g ` ( Poly1 ` K ) ) = ( +g ` ( Poly1 ` K ) )
82 37 81 mndcl 
 |-  ( ( ( Poly1 ` K ) e. Mnd /\ ( var1 ` K ) e. ( Base ` ( Poly1 ` K ) ) /\ ( ( algSc ` ( Poly1 ` K ) ) ` ( ( ZRHom ` K ) ` t ) ) e. ( Base ` ( Poly1 ` K ) ) ) -> ( ( var1 ` K ) ( +g ` ( Poly1 ` K ) ) ( ( algSc ` ( Poly1 ` K ) ) ` ( ( ZRHom ` K ) ` t ) ) ) e. ( Base ` ( Poly1 ` K ) ) )
83 62 66 80 82 syl3anc 
 |-  ( ( ph /\ t e. ( 0 ... A ) ) -> ( ( var1 ` K ) ( +g ` ( Poly1 ` K ) ) ( ( algSc ` ( Poly1 ` K ) ) ` ( ( ZRHom ` K ) ` t ) ) ) e. ( Base ` ( Poly1 ` K ) ) )
84 83 ralrimiva 
 |-  ( ph -> A. t e. ( 0 ... A ) ( ( var1 ` K ) ( +g ` ( Poly1 ` K ) ) ( ( algSc ` ( Poly1 ` K ) ) ` ( ( ZRHom ` K ) ` t ) ) ) e. ( Base ` ( Poly1 ` K ) ) )
85 84 adantr 
 |-  ( ( ph /\ i e. ( 0 ... A ) ) -> A. t e. ( 0 ... A ) ( ( var1 ` K ) ( +g ` ( Poly1 ` K ) ) ( ( algSc ` ( Poly1 ` K ) ) ` ( ( ZRHom ` K ) ` t ) ) ) e. ( Base ` ( Poly1 ` K ) ) )
86 59 85 55 rspcdva 
 |-  ( ( ph /\ i e. ( 0 ... A ) ) -> ( ( var1 ` K ) ( +g ` ( Poly1 ` K ) ) ( ( algSc ` ( Poly1 ` K ) ) ` ( ( ZRHom ` K ) ` i ) ) ) e. ( Base ` ( Poly1 ` K ) ) )
87 38 39 48 56 86 mulgnn0cld 
 |-  ( ( ph /\ i e. ( 0 ... A ) ) -> ( ( U ` i ) ( .g ` ( mulGrp ` ( Poly1 ` K ) ) ) ( ( var1 ` K ) ( +g ` ( Poly1 ` K ) ) ( ( algSc ` ( Poly1 ` K ) ) ` ( ( ZRHom ` K ) ` i ) ) ) ) e. ( Base ` ( Poly1 ` K ) ) )
88 43 ply1idom 
 |-  ( K e. IDomn -> ( Poly1 ` K ) e. IDomn )
89 34 88 syl 
 |-  ( ph -> ( Poly1 ` K ) e. IDomn )
90 89 adantr 
 |-  ( ( ph /\ i e. ( 0 ... A ) ) -> ( Poly1 ` K ) e. IDomn )
91 58 neeq1d 
 |-  ( t = i -> ( ( ( var1 ` K ) ( +g ` ( Poly1 ` K ) ) ( ( algSc ` ( Poly1 ` K ) ) ` ( ( ZRHom ` K ) ` t ) ) ) =/= ( 0g ` ( Poly1 ` K ) ) <-> ( ( var1 ` K ) ( +g ` ( Poly1 ` K ) ) ( ( algSc ` ( Poly1 ` K ) ) ` ( ( ZRHom ` K ) ` i ) ) ) =/= ( 0g ` ( Poly1 ` K ) ) ) )
92 eqid 
 |-  ( deg1 ` K ) = ( deg1 ` K )
93 92 43 37 deg1xrcl 
 |-  ( ( ( algSc ` ( Poly1 ` K ) ) ` ( ( ZRHom ` K ) ` t ) ) e. ( Base ` ( Poly1 ` K ) ) -> ( ( deg1 ` K ) ` ( ( algSc ` ( Poly1 ` K ) ) ` ( ( ZRHom ` K ) ` t ) ) ) e. RR* )
94 80 93 syl 
 |-  ( ( ph /\ t e. ( 0 ... A ) ) -> ( ( deg1 ` K ) ` ( ( algSc ` ( Poly1 ` K ) ) ` ( ( ZRHom ` K ) ` t ) ) ) e. RR* )
95 0xr 
 |-  0 e. RR*
96 95 a1i 
 |-  ( ( ph /\ t e. ( 0 ... A ) ) -> 0 e. RR* )
97 1xr 
 |-  1 e. RR*
98 97 a1i 
 |-  ( ( ph /\ t e. ( 0 ... A ) ) -> 1 e. RR* )
99 92 43 71 78 deg1sclle 
 |-  ( ( K e. Ring /\ ( ( ZRHom ` K ) ` t ) e. ( Base ` K ) ) -> ( ( deg1 ` K ) ` ( ( algSc ` ( Poly1 ` K ) ) ` ( ( ZRHom ` K ) ` t ) ) ) <_ 0 )
100 63 77 99 syl2anc 
 |-  ( ( ph /\ t e. ( 0 ... A ) ) -> ( ( deg1 ` K ) ` ( ( algSc ` ( Poly1 ` K ) ) ` ( ( ZRHom ` K ) ` t ) ) ) <_ 0 )
101 0lt1 
 |-  0 < 1
102 101 a1i 
 |-  ( ( ph /\ t e. ( 0 ... A ) ) -> 0 < 1 )
103 94 96 98 100 102 xrlelttrd 
 |-  ( ( ph /\ t e. ( 0 ... A ) ) -> ( ( deg1 ` K ) ` ( ( algSc ` ( Poly1 ` K ) ) ` ( ( ZRHom ` K ) ` t ) ) ) < 1 )
104 38 39 mulg1 
 |-  ( ( var1 ` K ) e. ( Base ` ( Poly1 ` K ) ) -> ( 1 ( .g ` ( mulGrp ` ( Poly1 ` K ) ) ) ( var1 ` K ) ) = ( var1 ` K ) )
105 66 104 syl 
 |-  ( ( ph /\ t e. ( 0 ... A ) ) -> ( 1 ( .g ` ( mulGrp ` ( Poly1 ` K ) ) ) ( var1 ` K ) ) = ( var1 ` K ) )
106 105 eqcomd 
 |-  ( ( ph /\ t e. ( 0 ... A ) ) -> ( var1 ` K ) = ( 1 ( .g ` ( mulGrp ` ( Poly1 ` K ) ) ) ( var1 ` K ) ) )
107 106 fveq2d 
 |-  ( ( ph /\ t e. ( 0 ... A ) ) -> ( ( deg1 ` K ) ` ( var1 ` K ) ) = ( ( deg1 ` K ) ` ( 1 ( .g ` ( mulGrp ` ( Poly1 ` K ) ) ) ( var1 ` K ) ) ) )
108 isfld 
 |-  ( K e. Field <-> ( K e. DivRing /\ K e. CRing ) )
109 drngnzr 
 |-  ( K e. DivRing -> K e. NzRing )
110 109 adantr 
 |-  ( ( K e. DivRing /\ K e. CRing ) -> K e. NzRing )
111 108 110 sylbi 
 |-  ( K e. Field -> K e. NzRing )
112 3 111 syl 
 |-  ( ph -> K e. NzRing )
113 112 adantr 
 |-  ( ( ph /\ t e. ( 0 ... A ) ) -> K e. NzRing )
114 1nn0 
 |-  1 e. NN0
115 114 a1i 
 |-  ( ( ph /\ t e. ( 0 ... A ) ) -> 1 e. NN0 )
116 92 43 64 36 39 deg1pw 
 |-  ( ( K e. NzRing /\ 1 e. NN0 ) -> ( ( deg1 ` K ) ` ( 1 ( .g ` ( mulGrp ` ( Poly1 ` K ) ) ) ( var1 ` K ) ) ) = 1 )
117 113 115 116 syl2anc 
 |-  ( ( ph /\ t e. ( 0 ... A ) ) -> ( ( deg1 ` K ) ` ( 1 ( .g ` ( mulGrp ` ( Poly1 ` K ) ) ) ( var1 ` K ) ) ) = 1 )
118 107 117 eqtr2d 
 |-  ( ( ph /\ t e. ( 0 ... A ) ) -> 1 = ( ( deg1 ` K ) ` ( var1 ` K ) ) )
119 103 118 breqtrd 
 |-  ( ( ph /\ t e. ( 0 ... A ) ) -> ( ( deg1 ` K ) ` ( ( algSc ` ( Poly1 ` K ) ) ` ( ( ZRHom ` K ) ` t ) ) ) < ( ( deg1 ` K ) ` ( var1 ` K ) ) )
120 43 92 63 37 81 66 80 119 deg1add 
 |-  ( ( ph /\ t e. ( 0 ... A ) ) -> ( ( deg1 ` K ) ` ( ( var1 ` K ) ( +g ` ( Poly1 ` K ) ) ( ( algSc ` ( Poly1 ` K ) ) ` ( ( ZRHom ` K ) ` t ) ) ) ) = ( ( deg1 ` K ) ` ( var1 ` K ) ) )
121 107 117 eqtrd 
 |-  ( ( ph /\ t e. ( 0 ... A ) ) -> ( ( deg1 ` K ) ` ( var1 ` K ) ) = 1 )
122 120 121 eqtrd 
 |-  ( ( ph /\ t e. ( 0 ... A ) ) -> ( ( deg1 ` K ) ` ( ( var1 ` K ) ( +g ` ( Poly1 ` K ) ) ( ( algSc ` ( Poly1 ` K ) ) ` ( ( ZRHom ` K ) ` t ) ) ) ) = 1 )
123 122 115 eqeltrd 
 |-  ( ( ph /\ t e. ( 0 ... A ) ) -> ( ( deg1 ` K ) ` ( ( var1 ` K ) ( +g ` ( Poly1 ` K ) ) ( ( algSc ` ( Poly1 ` K ) ) ` ( ( ZRHom ` K ) ` t ) ) ) ) e. NN0 )
124 eqid 
 |-  ( 0g ` ( Poly1 ` K ) ) = ( 0g ` ( Poly1 ` K ) )
125 92 43 124 37 deg1nn0clb 
 |-  ( ( K e. Ring /\ ( ( var1 ` K ) ( +g ` ( Poly1 ` K ) ) ( ( algSc ` ( Poly1 ` K ) ) ` ( ( ZRHom ` K ) ` t ) ) ) e. ( Base ` ( Poly1 ` K ) ) ) -> ( ( ( var1 ` K ) ( +g ` ( Poly1 ` K ) ) ( ( algSc ` ( Poly1 ` K ) ) ` ( ( ZRHom ` K ) ` t ) ) ) =/= ( 0g ` ( Poly1 ` K ) ) <-> ( ( deg1 ` K ) ` ( ( var1 ` K ) ( +g ` ( Poly1 ` K ) ) ( ( algSc ` ( Poly1 ` K ) ) ` ( ( ZRHom ` K ) ` t ) ) ) ) e. NN0 ) )
126 63 83 125 syl2anc 
 |-  ( ( ph /\ t e. ( 0 ... A ) ) -> ( ( ( var1 ` K ) ( +g ` ( Poly1 ` K ) ) ( ( algSc ` ( Poly1 ` K ) ) ` ( ( ZRHom ` K ) ` t ) ) ) =/= ( 0g ` ( Poly1 ` K ) ) <-> ( ( deg1 ` K ) ` ( ( var1 ` K ) ( +g ` ( Poly1 ` K ) ) ( ( algSc ` ( Poly1 ` K ) ) ` ( ( ZRHom ` K ) ` t ) ) ) ) e. NN0 ) )
127 123 126 mpbird 
 |-  ( ( ph /\ t e. ( 0 ... A ) ) -> ( ( var1 ` K ) ( +g ` ( Poly1 ` K ) ) ( ( algSc ` ( Poly1 ` K ) ) ` ( ( ZRHom ` K ) ` t ) ) ) =/= ( 0g ` ( Poly1 ` K ) ) )
128 127 ralrimiva 
 |-  ( ph -> A. t e. ( 0 ... A ) ( ( var1 ` K ) ( +g ` ( Poly1 ` K ) ) ( ( algSc ` ( Poly1 ` K ) ) ` ( ( ZRHom ` K ) ` t ) ) ) =/= ( 0g ` ( Poly1 ` K ) ) )
129 128 adantr 
 |-  ( ( ph /\ i e. ( 0 ... A ) ) -> A. t e. ( 0 ... A ) ( ( var1 ` K ) ( +g ` ( Poly1 ` K ) ) ( ( algSc ` ( Poly1 ` K ) ) ` ( ( ZRHom ` K ) ` t ) ) ) =/= ( 0g ` ( Poly1 ` K ) ) )
130 91 129 55 rspcdva 
 |-  ( ( ph /\ i e. ( 0 ... A ) ) -> ( ( var1 ` K ) ( +g ` ( Poly1 ` K ) ) ( ( algSc ` ( Poly1 ` K ) ) ` ( ( ZRHom ` K ) ` i ) ) ) =/= ( 0g ` ( Poly1 ` K ) ) )
131 90 86 130 56 39 idomnnzpownz 
 |-  ( ( ph /\ i e. ( 0 ... A ) ) -> ( ( U ` i ) ( .g ` ( mulGrp ` ( Poly1 ` K ) ) ) ( ( var1 ` K ) ( +g ` ( Poly1 ` K ) ) ( ( algSc ` ( Poly1 ` K ) ) ` ( ( ZRHom ` K ) ` i ) ) ) ) =/= ( 0g ` ( Poly1 ` K ) ) )
132 87 131 jca 
 |-  ( ( ph /\ i e. ( 0 ... A ) ) -> ( ( ( U ` i ) ( .g ` ( mulGrp ` ( Poly1 ` K ) ) ) ( ( var1 ` K ) ( +g ` ( Poly1 ` K ) ) ( ( algSc ` ( Poly1 ` K ) ) ` ( ( ZRHom ` K ) ` i ) ) ) ) e. ( Base ` ( Poly1 ` K ) ) /\ ( ( U ` i ) ( .g ` ( mulGrp ` ( Poly1 ` K ) ) ) ( ( var1 ` K ) ( +g ` ( Poly1 ` K ) ) ( ( algSc ` ( Poly1 ` K ) ) ` ( ( ZRHom ` K ) ` i ) ) ) ) =/= ( 0g ` ( Poly1 ` K ) ) ) )
133 132 ralrimiva 
 |-  ( ph -> A. i e. ( 0 ... A ) ( ( ( U ` i ) ( .g ` ( mulGrp ` ( Poly1 ` K ) ) ) ( ( var1 ` K ) ( +g ` ( Poly1 ` K ) ) ( ( algSc ` ( Poly1 ` K ) ) ` ( ( ZRHom ` K ) ` i ) ) ) ) e. ( Base ` ( Poly1 ` K ) ) /\ ( ( U ` i ) ( .g ` ( mulGrp ` ( Poly1 ` K ) ) ) ( ( var1 ` K ) ( +g ` ( Poly1 ` K ) ) ( ( algSc ` ( Poly1 ` K ) ) ` ( ( ZRHom ` K ) ` i ) ) ) ) =/= ( 0g ` ( Poly1 ` K ) ) ) )
134 34 35 133 deg1gprod 
 |-  ( ph -> ( ( ( deg1 ` K ) ` ( ( mulGrp ` ( Poly1 ` K ) ) gsum ( i e. ( 0 ... A ) |-> ( ( U ` i ) ( .g ` ( mulGrp ` ( Poly1 ` K ) ) ) ( ( var1 ` K ) ( +g ` ( Poly1 ` K ) ) ( ( algSc ` ( Poly1 ` K ) ) ` ( ( ZRHom ` K ) ` i ) ) ) ) ) ) ) = sum_ t e. ( 0 ... A ) ( ( deg1 ` K ) ` ( ( i e. ( 0 ... A ) |-> ( ( U ` i ) ( .g ` ( mulGrp ` ( Poly1 ` K ) ) ) ( ( var1 ` K ) ( +g ` ( Poly1 ` K ) ) ( ( algSc ` ( Poly1 ` K ) ) ` ( ( ZRHom ` K ) ` i ) ) ) ) ) ` t ) ) /\ 0 <_ ( ( deg1 ` K ) ` ( ( mulGrp ` ( Poly1 ` K ) ) gsum ( i e. ( 0 ... A ) |-> ( ( U ` i ) ( .g ` ( mulGrp ` ( Poly1 ` K ) ) ) ( ( var1 ` K ) ( +g ` ( Poly1 ` K ) ) ( ( algSc ` ( Poly1 ` K ) ) ` ( ( ZRHom ` K ) ` i ) ) ) ) ) ) ) ) )
135 134 simpld 
 |-  ( ph -> ( ( deg1 ` K ) ` ( ( mulGrp ` ( Poly1 ` K ) ) gsum ( i e. ( 0 ... A ) |-> ( ( U ` i ) ( .g ` ( mulGrp ` ( Poly1 ` K ) ) ) ( ( var1 ` K ) ( +g ` ( Poly1 ` K ) ) ( ( algSc ` ( Poly1 ` K ) ) ` ( ( ZRHom ` K ) ` i ) ) ) ) ) ) ) = sum_ t e. ( 0 ... A ) ( ( deg1 ` K ) ` ( ( i e. ( 0 ... A ) |-> ( ( U ` i ) ( .g ` ( mulGrp ` ( Poly1 ` K ) ) ) ( ( var1 ` K ) ( +g ` ( Poly1 ` K ) ) ( ( algSc ` ( Poly1 ` K ) ) ` ( ( ZRHom ` K ) ` i ) ) ) ) ) ` t ) ) )
136 eqidd 
 |-  ( ( ph /\ t e. ( 0 ... A ) ) -> ( i e. ( 0 ... A ) |-> ( ( U ` i ) ( .g ` ( mulGrp ` ( Poly1 ` K ) ) ) ( ( var1 ` K ) ( +g ` ( Poly1 ` K ) ) ( ( algSc ` ( Poly1 ` K ) ) ` ( ( ZRHom ` K ) ` i ) ) ) ) ) = ( i e. ( 0 ... A ) |-> ( ( U ` i ) ( .g ` ( mulGrp ` ( Poly1 ` K ) ) ) ( ( var1 ` K ) ( +g ` ( Poly1 ` K ) ) ( ( algSc ` ( Poly1 ` K ) ) ` ( ( ZRHom ` K ) ` i ) ) ) ) ) )
137 simpr 
 |-  ( ( ( ph /\ t e. ( 0 ... A ) ) /\ i = t ) -> i = t )
138 137 fveq2d 
 |-  ( ( ( ph /\ t e. ( 0 ... A ) ) /\ i = t ) -> ( U ` i ) = ( U ` t ) )
139 137 fveq2d 
 |-  ( ( ( ph /\ t e. ( 0 ... A ) ) /\ i = t ) -> ( ( ZRHom ` K ) ` i ) = ( ( ZRHom ` K ) ` t ) )
140 139 fveq2d 
 |-  ( ( ( ph /\ t e. ( 0 ... A ) ) /\ i = t ) -> ( ( algSc ` ( Poly1 ` K ) ) ` ( ( ZRHom ` K ) ` i ) ) = ( ( algSc ` ( Poly1 ` K ) ) ` ( ( ZRHom ` K ) ` t ) ) )
141 140 oveq2d 
 |-  ( ( ( ph /\ t e. ( 0 ... A ) ) /\ i = t ) -> ( ( var1 ` K ) ( +g ` ( Poly1 ` K ) ) ( ( algSc ` ( Poly1 ` K ) ) ` ( ( ZRHom ` K ) ` i ) ) ) = ( ( var1 ` K ) ( +g ` ( Poly1 ` K ) ) ( ( algSc ` ( Poly1 ` K ) ) ` ( ( ZRHom ` K ) ` t ) ) ) )
142 138 141 oveq12d 
 |-  ( ( ( ph /\ t e. ( 0 ... A ) ) /\ i = t ) -> ( ( U ` i ) ( .g ` ( mulGrp ` ( Poly1 ` K ) ) ) ( ( var1 ` K ) ( +g ` ( Poly1 ` K ) ) ( ( algSc ` ( Poly1 ` K ) ) ` ( ( ZRHom ` K ) ` i ) ) ) ) = ( ( U ` t ) ( .g ` ( mulGrp ` ( Poly1 ` K ) ) ) ( ( var1 ` K ) ( +g ` ( Poly1 ` K ) ) ( ( algSc ` ( Poly1 ` K ) ) ` ( ( ZRHom ` K ) ` t ) ) ) ) )
143 simpr 
 |-  ( ( ph /\ t e. ( 0 ... A ) ) -> t e. ( 0 ... A ) )
144 ovexd 
 |-  ( ( ph /\ t e. ( 0 ... A ) ) -> ( ( U ` t ) ( .g ` ( mulGrp ` ( Poly1 ` K ) ) ) ( ( var1 ` K ) ( +g ` ( Poly1 ` K ) ) ( ( algSc ` ( Poly1 ` K ) ) ` ( ( ZRHom ` K ) ` t ) ) ) ) e. _V )
145 136 142 143 144 fvmptd 
 |-  ( ( ph /\ t e. ( 0 ... A ) ) -> ( ( i e. ( 0 ... A ) |-> ( ( U ` i ) ( .g ` ( mulGrp ` ( Poly1 ` K ) ) ) ( ( var1 ` K ) ( +g ` ( Poly1 ` K ) ) ( ( algSc ` ( Poly1 ` K ) ) ` ( ( ZRHom ` K ) ` i ) ) ) ) ) ` t ) = ( ( U ` t ) ( .g ` ( mulGrp ` ( Poly1 ` K ) ) ) ( ( var1 ` K ) ( +g ` ( Poly1 ` K ) ) ( ( algSc ` ( Poly1 ` K ) ) ` ( ( ZRHom ` K ) ` t ) ) ) ) )
146 145 fveq2d 
 |-  ( ( ph /\ t e. ( 0 ... A ) ) -> ( ( deg1 ` K ) ` ( ( i e. ( 0 ... A ) |-> ( ( U ` i ) ( .g ` ( mulGrp ` ( Poly1 ` K ) ) ) ( ( var1 ` K ) ( +g ` ( Poly1 ` K ) ) ( ( algSc ` ( Poly1 ` K ) ) ` ( ( ZRHom ` K ) ` i ) ) ) ) ) ` t ) ) = ( ( deg1 ` K ) ` ( ( U ` t ) ( .g ` ( mulGrp ` ( Poly1 ` K ) ) ) ( ( var1 ` K ) ( +g ` ( Poly1 ` K ) ) ( ( algSc ` ( Poly1 ` K ) ) ` ( ( ZRHom ` K ) ` t ) ) ) ) ) )
147 34 adantr 
 |-  ( ( ph /\ t e. ( 0 ... A ) ) -> K e. IDomn )
148 53 ffvelcdmda 
 |-  ( ( ph /\ t e. ( 0 ... A ) ) -> ( U ` t ) e. NN0 )
149 147 83 127 148 39 92 deg1pow 
 |-  ( ( ph /\ t e. ( 0 ... A ) ) -> ( ( deg1 ` K ) ` ( ( U ` t ) ( .g ` ( mulGrp ` ( Poly1 ` K ) ) ) ( ( var1 ` K ) ( +g ` ( Poly1 ` K ) ) ( ( algSc ` ( Poly1 ` K ) ) ` ( ( ZRHom ` K ) ` t ) ) ) ) ) = ( ( U ` t ) x. ( ( deg1 ` K ) ` ( ( var1 ` K ) ( +g ` ( Poly1 ` K ) ) ( ( algSc ` ( Poly1 ` K ) ) ` ( ( ZRHom ` K ) ` t ) ) ) ) ) )
150 122 oveq2d 
 |-  ( ( ph /\ t e. ( 0 ... A ) ) -> ( ( U ` t ) x. ( ( deg1 ` K ) ` ( ( var1 ` K ) ( +g ` ( Poly1 ` K ) ) ( ( algSc ` ( Poly1 ` K ) ) ` ( ( ZRHom ` K ) ` t ) ) ) ) ) = ( ( U ` t ) x. 1 ) )
151 148 nn0cnd 
 |-  ( ( ph /\ t e. ( 0 ... A ) ) -> ( U ` t ) e. CC )
152 151 mulridd 
 |-  ( ( ph /\ t e. ( 0 ... A ) ) -> ( ( U ` t ) x. 1 ) = ( U ` t ) )
153 150 152 eqtrd 
 |-  ( ( ph /\ t e. ( 0 ... A ) ) -> ( ( U ` t ) x. ( ( deg1 ` K ) ` ( ( var1 ` K ) ( +g ` ( Poly1 ` K ) ) ( ( algSc ` ( Poly1 ` K ) ) ` ( ( ZRHom ` K ) ` t ) ) ) ) ) = ( U ` t ) )
154 149 153 eqtrd 
 |-  ( ( ph /\ t e. ( 0 ... A ) ) -> ( ( deg1 ` K ) ` ( ( U ` t ) ( .g ` ( mulGrp ` ( Poly1 ` K ) ) ) ( ( var1 ` K ) ( +g ` ( Poly1 ` K ) ) ( ( algSc ` ( Poly1 ` K ) ) ` ( ( ZRHom ` K ) ` t ) ) ) ) ) = ( U ` t ) )
155 146 154 eqtrd 
 |-  ( ( ph /\ t e. ( 0 ... A ) ) -> ( ( deg1 ` K ) ` ( ( i e. ( 0 ... A ) |-> ( ( U ` i ) ( .g ` ( mulGrp ` ( Poly1 ` K ) ) ) ( ( var1 ` K ) ( +g ` ( Poly1 ` K ) ) ( ( algSc ` ( Poly1 ` K ) ) ` ( ( ZRHom ` K ) ` i ) ) ) ) ) ` t ) ) = ( U ` t ) )
156 155 sumeq2dv 
 |-  ( ph -> sum_ t e. ( 0 ... A ) ( ( deg1 ` K ) ` ( ( i e. ( 0 ... A ) |-> ( ( U ` i ) ( .g ` ( mulGrp ` ( Poly1 ` K ) ) ) ( ( var1 ` K ) ( +g ` ( Poly1 ` K ) ) ( ( algSc ` ( Poly1 ` K ) ) ` ( ( ZRHom ` K ) ` i ) ) ) ) ) ` t ) ) = sum_ t e. ( 0 ... A ) ( U ` t ) )
157 135 156 eqtrd 
 |-  ( ph -> ( ( deg1 ` K ) ` ( ( mulGrp ` ( Poly1 ` K ) ) gsum ( i e. ( 0 ... A ) |-> ( ( U ` i ) ( .g ` ( mulGrp ` ( Poly1 ` K ) ) ) ( ( var1 ` K ) ( +g ` ( Poly1 ` K ) ) ( ( algSc ` ( Poly1 ` K ) ) ` ( ( ZRHom ` K ) ` i ) ) ) ) ) ) ) = sum_ t e. ( 0 ... A ) ( U ` t ) )
158 32 157 eqtrd 
 |-  ( ph -> ( ( deg1 ` K ) ` ( ( g e. ( NN0 ^m ( 0 ... A ) ) |-> ( ( mulGrp ` ( Poly1 ` K ) ) gsum ( i e. ( 0 ... A ) |-> ( ( g ` i ) ( .g ` ( mulGrp ` ( Poly1 ` K ) ) ) ( ( var1 ` K ) ( +g ` ( Poly1 ` K ) ) ( ( algSc ` ( Poly1 ` K ) ) ` ( ( ZRHom ` K ) ` i ) ) ) ) ) ) ) ` U ) ) = sum_ t e. ( 0 ... A ) ( U ` t ) )
159 23 158 eqtrd 
 |-  ( ph -> ( ( deg1 ` K ) ` ( G ` U ) ) = sum_ t e. ( 0 ... A ) ( U ` t ) )