This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem elrgspnsubrunlem2

Description: Lemma for elrgspnsubrun , second direction. (Contributed by Thierry Arnoux, 13-Oct-2025)

Ref Expression
Hypotheses elrgspnsubrun.b 
|- B = ( Base ` R )
elrgspnsubrun.t 
|- .x. = ( .r ` R )
elrgspnsubrun.z 
|- .0. = ( 0g ` R )
elrgspnsubrun.n 
|- N = ( RingSpan ` R )
elrgspnsubrun.r 
|- ( ph -> R e. CRing )
elrgspnsubrun.e 
|- ( ph -> E e. ( SubRing ` R ) )
elrgspnsubrun.f 
|- ( ph -> F e. ( SubRing ` R ) )
elrgspnsubrunlem2.x 
|- ( ph -> X e. B )
elrgspnsubrunlem2.1 
|- ( ph -> G : Word ( E u. F ) --> ZZ )
elrgspnsubrunlem2.2 
|- ( ph -> G finSupp 0 )
elrgspnsubrunlem2.3 
|- ( ph -> X = ( R gsum ( w e. Word ( E u. F ) |-> ( ( G ` w ) ( .g ` R ) ( ( mulGrp ` R ) gsum w ) ) ) ) )
Assertion elrgspnsubrunlem2 
|- ( ph -> E. p e. ( E ^m F ) ( p finSupp .0. /\ X = ( R gsum ( f e. F |-> ( ( p ` f ) .x. f ) ) ) ) )

Proof

Step Hyp Ref Expression
1 elrgspnsubrun.b 
 |-  B = ( Base ` R )
2 elrgspnsubrun.t 
 |-  .x. = ( .r ` R )
3 elrgspnsubrun.z 
 |-  .0. = ( 0g ` R )
4 elrgspnsubrun.n 
 |-  N = ( RingSpan ` R )
5 elrgspnsubrun.r 
 |-  ( ph -> R e. CRing )
6 elrgspnsubrun.e 
 |-  ( ph -> E e. ( SubRing ` R ) )
7 elrgspnsubrun.f 
 |-  ( ph -> F e. ( SubRing ` R ) )
8 elrgspnsubrunlem2.x 
 |-  ( ph -> X e. B )
9 elrgspnsubrunlem2.1 
 |-  ( ph -> G : Word ( E u. F ) --> ZZ )
10 elrgspnsubrunlem2.2 
 |-  ( ph -> G finSupp 0 )
11 elrgspnsubrunlem2.3 
 |-  ( ph -> X = ( R gsum ( w e. Word ( E u. F ) |-> ( ( G ` w ) ( .g ` R ) ( ( mulGrp ` R ) gsum w ) ) ) ) )
12 6 ad2antrr 
 |-  ( ( ( ph /\ q e. ( ( E X. F ) ^m Word ( E u. F ) ) ) /\ A. w e. Word ( E u. F ) ( ( mulGrp ` R ) gsum w ) = ( ( 1st ` ( q ` w ) ) .x. ( 2nd ` ( q ` w ) ) ) ) -> E e. ( SubRing ` R ) )
13 7 ad2antrr 
 |-  ( ( ( ph /\ q e. ( ( E X. F ) ^m Word ( E u. F ) ) ) /\ A. w e. Word ( E u. F ) ( ( mulGrp ` R ) gsum w ) = ( ( 1st ` ( q ` w ) ) .x. ( 2nd ` ( q ` w ) ) ) ) -> F e. ( SubRing ` R ) )
14 5 crngringd 
 |-  ( ph -> R e. Ring )
15 14 ringabld 
 |-  ( ph -> R e. Abel )
16 15 ad3antrrr 
 |-  ( ( ( ( ph /\ q e. ( ( E X. F ) ^m Word ( E u. F ) ) ) /\ A. w e. Word ( E u. F ) ( ( mulGrp ` R ) gsum w ) = ( ( 1st ` ( q ` w ) ) .x. ( 2nd ` ( q ` w ) ) ) ) /\ f e. F ) -> R e. Abel )
17 vex 
 |-  q e. _V
18 17 cnvex 
 |-  `' q e. _V
19 18 imaex 
 |-  ( `' q " ( E X. { f } ) ) e. _V
20 19 a1i 
 |-  ( ( ( ( ph /\ q e. ( ( E X. F ) ^m Word ( E u. F ) ) ) /\ A. w e. Word ( E u. F ) ( ( mulGrp ` R ) gsum w ) = ( ( 1st ` ( q ` w ) ) .x. ( 2nd ` ( q ` w ) ) ) ) /\ f e. F ) -> ( `' q " ( E X. { f } ) ) e. _V )
21 subrgsubg 
 |-  ( E e. ( SubRing ` R ) -> E e. ( SubGrp ` R ) )
22 6 21 syl 
 |-  ( ph -> E e. ( SubGrp ` R ) )
23 22 ad3antrrr 
 |-  ( ( ( ( ph /\ q e. ( ( E X. F ) ^m Word ( E u. F ) ) ) /\ A. w e. Word ( E u. F ) ( ( mulGrp ` R ) gsum w ) = ( ( 1st ` ( q ` w ) ) .x. ( 2nd ` ( q ` w ) ) ) ) /\ f e. F ) -> E e. ( SubGrp ` R ) )
24 eqid 
 |-  ( .g ` R ) = ( .g ` R )
25 5 crnggrpd 
 |-  ( ph -> R e. Grp )
26 25 ad4antr 
 |-  ( ( ( ( ( ph /\ q e. ( ( E X. F ) ^m Word ( E u. F ) ) ) /\ A. w e. Word ( E u. F ) ( ( mulGrp ` R ) gsum w ) = ( ( 1st ` ( q ` w ) ) .x. ( 2nd ` ( q ` w ) ) ) ) /\ f e. F ) /\ v e. ( `' q " ( E X. { f } ) ) ) -> R e. Grp )
27 6 7 xpexd 
 |-  ( ph -> ( E X. F ) e. _V )
28 6 7 unexd 
 |-  ( ph -> ( E u. F ) e. _V )
29 wrdexg 
 |-  ( ( E u. F ) e. _V -> Word ( E u. F ) e. _V )
30 28 29 syl 
 |-  ( ph -> Word ( E u. F ) e. _V )
31 27 30 elmapd 
 |-  ( ph -> ( q e. ( ( E X. F ) ^m Word ( E u. F ) ) <-> q : Word ( E u. F ) --> ( E X. F ) ) )
32 31 biimpa 
 |-  ( ( ph /\ q e. ( ( E X. F ) ^m Word ( E u. F ) ) ) -> q : Word ( E u. F ) --> ( E X. F ) )
33 32 ffund 
 |-  ( ( ph /\ q e. ( ( E X. F ) ^m Word ( E u. F ) ) ) -> Fun q )
34 33 ad3antrrr 
 |-  ( ( ( ( ( ph /\ q e. ( ( E X. F ) ^m Word ( E u. F ) ) ) /\ A. w e. Word ( E u. F ) ( ( mulGrp ` R ) gsum w ) = ( ( 1st ` ( q ` w ) ) .x. ( 2nd ` ( q ` w ) ) ) ) /\ f e. F ) /\ v e. ( `' q " ( E X. { f } ) ) ) -> Fun q )
35 fvimacnvi 
 |-  ( ( Fun q /\ v e. ( `' q " ( E X. { f } ) ) ) -> ( q ` v ) e. ( E X. { f } ) )
36 34 35 sylancom 
 |-  ( ( ( ( ( ph /\ q e. ( ( E X. F ) ^m Word ( E u. F ) ) ) /\ A. w e. Word ( E u. F ) ( ( mulGrp ` R ) gsum w ) = ( ( 1st ` ( q ` w ) ) .x. ( 2nd ` ( q ` w ) ) ) ) /\ f e. F ) /\ v e. ( `' q " ( E X. { f } ) ) ) -> ( q ` v ) e. ( E X. { f } ) )
37 xp1st 
 |-  ( ( q ` v ) e. ( E X. { f } ) -> ( 1st ` ( q ` v ) ) e. E )
38 36 37 syl 
 |-  ( ( ( ( ( ph /\ q e. ( ( E X. F ) ^m Word ( E u. F ) ) ) /\ A. w e. Word ( E u. F ) ( ( mulGrp ` R ) gsum w ) = ( ( 1st ` ( q ` w ) ) .x. ( 2nd ` ( q ` w ) ) ) ) /\ f e. F ) /\ v e. ( `' q " ( E X. { f } ) ) ) -> ( 1st ` ( q ` v ) ) e. E )
39 23 adantr 
 |-  ( ( ( ( ( ph /\ q e. ( ( E X. F ) ^m Word ( E u. F ) ) ) /\ A. w e. Word ( E u. F ) ( ( mulGrp ` R ) gsum w ) = ( ( 1st ` ( q ` w ) ) .x. ( 2nd ` ( q ` w ) ) ) ) /\ f e. F ) /\ v e. ( `' q " ( E X. { f } ) ) ) -> E e. ( SubGrp ` R ) )
40 9 ad4antr 
 |-  ( ( ( ( ( ph /\ q e. ( ( E X. F ) ^m Word ( E u. F ) ) ) /\ A. w e. Word ( E u. F ) ( ( mulGrp ` R ) gsum w ) = ( ( 1st ` ( q ` w ) ) .x. ( 2nd ` ( q ` w ) ) ) ) /\ f e. F ) /\ v e. ( `' q " ( E X. { f } ) ) ) -> G : Word ( E u. F ) --> ZZ )
41 cnvimass 
 |-  ( `' q " ( E X. { f } ) ) C_ dom q
42 32 fdmd 
 |-  ( ( ph /\ q e. ( ( E X. F ) ^m Word ( E u. F ) ) ) -> dom q = Word ( E u. F ) )
43 42 ad2antrr 
 |-  ( ( ( ( ph /\ q e. ( ( E X. F ) ^m Word ( E u. F ) ) ) /\ A. w e. Word ( E u. F ) ( ( mulGrp ` R ) gsum w ) = ( ( 1st ` ( q ` w ) ) .x. ( 2nd ` ( q ` w ) ) ) ) /\ f e. F ) -> dom q = Word ( E u. F ) )
44 41 43 sseqtrid 
 |-  ( ( ( ( ph /\ q e. ( ( E X. F ) ^m Word ( E u. F ) ) ) /\ A. w e. Word ( E u. F ) ( ( mulGrp ` R ) gsum w ) = ( ( 1st ` ( q ` w ) ) .x. ( 2nd ` ( q ` w ) ) ) ) /\ f e. F ) -> ( `' q " ( E X. { f } ) ) C_ Word ( E u. F ) )
45 44 sselda 
 |-  ( ( ( ( ( ph /\ q e. ( ( E X. F ) ^m Word ( E u. F ) ) ) /\ A. w e. Word ( E u. F ) ( ( mulGrp ` R ) gsum w ) = ( ( 1st ` ( q ` w ) ) .x. ( 2nd ` ( q ` w ) ) ) ) /\ f e. F ) /\ v e. ( `' q " ( E X. { f } ) ) ) -> v e. Word ( E u. F ) )
46 40 45 ffvelcdmd 
 |-  ( ( ( ( ( ph /\ q e. ( ( E X. F ) ^m Word ( E u. F ) ) ) /\ A. w e. Word ( E u. F ) ( ( mulGrp ` R ) gsum w ) = ( ( 1st ` ( q ` w ) ) .x. ( 2nd ` ( q ` w ) ) ) ) /\ f e. F ) /\ v e. ( `' q " ( E X. { f } ) ) ) -> ( G ` v ) e. ZZ )
47 1 24 26 38 39 46 subgmulgcld 
 |-  ( ( ( ( ( ph /\ q e. ( ( E X. F ) ^m Word ( E u. F ) ) ) /\ A. w e. Word ( E u. F ) ( ( mulGrp ` R ) gsum w ) = ( ( 1st ` ( q ` w ) ) .x. ( 2nd ` ( q ` w ) ) ) ) /\ f e. F ) /\ v e. ( `' q " ( E X. { f } ) ) ) -> ( ( G ` v ) ( .g ` R ) ( 1st ` ( q ` v ) ) ) e. E )
48 47 fmpttd 
 |-  ( ( ( ( ph /\ q e. ( ( E X. F ) ^m Word ( E u. F ) ) ) /\ A. w e. Word ( E u. F ) ( ( mulGrp ` R ) gsum w ) = ( ( 1st ` ( q ` w ) ) .x. ( 2nd ` ( q ` w ) ) ) ) /\ f e. F ) -> ( v e. ( `' q " ( E X. { f } ) ) |-> ( ( G ` v ) ( .g ` R ) ( 1st ` ( q ` v ) ) ) ) : ( `' q " ( E X. { f } ) ) --> E )
49 9 feqmptd 
 |-  ( ph -> G = ( v e. Word ( E u. F ) |-> ( G ` v ) ) )
50 49 10 eqbrtrrd 
 |-  ( ph -> ( v e. Word ( E u. F ) |-> ( G ` v ) ) finSupp 0 )
51 50 ad3antrrr 
 |-  ( ( ( ( ph /\ q e. ( ( E X. F ) ^m Word ( E u. F ) ) ) /\ A. w e. Word ( E u. F ) ( ( mulGrp ` R ) gsum w ) = ( ( 1st ` ( q ` w ) ) .x. ( 2nd ` ( q ` w ) ) ) ) /\ f e. F ) -> ( v e. Word ( E u. F ) |-> ( G ` v ) ) finSupp 0 )
52 0zd 
 |-  ( ( ( ( ph /\ q e. ( ( E X. F ) ^m Word ( E u. F ) ) ) /\ A. w e. Word ( E u. F ) ( ( mulGrp ` R ) gsum w ) = ( ( 1st ` ( q ` w ) ) .x. ( 2nd ` ( q ` w ) ) ) ) /\ f e. F ) -> 0 e. ZZ )
53 51 44 52 fmptssfisupp 
 |-  ( ( ( ( ph /\ q e. ( ( E X. F ) ^m Word ( E u. F ) ) ) /\ A. w e. Word ( E u. F ) ( ( mulGrp ` R ) gsum w ) = ( ( 1st ` ( q ` w ) ) .x. ( 2nd ` ( q ` w ) ) ) ) /\ f e. F ) -> ( v e. ( `' q " ( E X. { f } ) ) |-> ( G ` v ) ) finSupp 0 )
54 1 subrgss 
 |-  ( E e. ( SubRing ` R ) -> E C_ B )
55 6 54 syl 
 |-  ( ph -> E C_ B )
56 55 ad3antrrr 
 |-  ( ( ( ( ph /\ q e. ( ( E X. F ) ^m Word ( E u. F ) ) ) /\ A. w e. Word ( E u. F ) ( ( mulGrp ` R ) gsum w ) = ( ( 1st ` ( q ` w ) ) .x. ( 2nd ` ( q ` w ) ) ) ) /\ f e. F ) -> E C_ B )
57 56 sselda 
 |-  ( ( ( ( ( ph /\ q e. ( ( E X. F ) ^m Word ( E u. F ) ) ) /\ A. w e. Word ( E u. F ) ( ( mulGrp ` R ) gsum w ) = ( ( 1st ` ( q ` w ) ) .x. ( 2nd ` ( q ` w ) ) ) ) /\ f e. F ) /\ y e. E ) -> y e. B )
58 1 3 24 mulg0 
 |-  ( y e. B -> ( 0 ( .g ` R ) y ) = .0. )
59 57 58 syl 
 |-  ( ( ( ( ( ph /\ q e. ( ( E X. F ) ^m Word ( E u. F ) ) ) /\ A. w e. Word ( E u. F ) ( ( mulGrp ` R ) gsum w ) = ( ( 1st ` ( q ` w ) ) .x. ( 2nd ` ( q ` w ) ) ) ) /\ f e. F ) /\ y e. E ) -> ( 0 ( .g ` R ) y ) = .0. )
60 3 fvexi 
 |-  .0. e. _V
61 60 a1i 
 |-  ( ( ( ( ph /\ q e. ( ( E X. F ) ^m Word ( E u. F ) ) ) /\ A. w e. Word ( E u. F ) ( ( mulGrp ` R ) gsum w ) = ( ( 1st ` ( q ` w ) ) .x. ( 2nd ` ( q ` w ) ) ) ) /\ f e. F ) -> .0. e. _V )
62 53 59 46 38 61 fsuppssov1 
 |-  ( ( ( ( ph /\ q e. ( ( E X. F ) ^m Word ( E u. F ) ) ) /\ A. w e. Word ( E u. F ) ( ( mulGrp ` R ) gsum w ) = ( ( 1st ` ( q ` w ) ) .x. ( 2nd ` ( q ` w ) ) ) ) /\ f e. F ) -> ( v e. ( `' q " ( E X. { f } ) ) |-> ( ( G ` v ) ( .g ` R ) ( 1st ` ( q ` v ) ) ) ) finSupp .0. )
63 3 16 20 23 48 62 gsumsubgcl 
 |-  ( ( ( ( ph /\ q e. ( ( E X. F ) ^m Word ( E u. F ) ) ) /\ A. w e. Word ( E u. F ) ( ( mulGrp ` R ) gsum w ) = ( ( 1st ` ( q ` w ) ) .x. ( 2nd ` ( q ` w ) ) ) ) /\ f e. F ) -> ( R gsum ( v e. ( `' q " ( E X. { f } ) ) |-> ( ( G ` v ) ( .g ` R ) ( 1st ` ( q ` v ) ) ) ) ) e. E )
64 63 fmpttd 
 |-  ( ( ( ph /\ q e. ( ( E X. F ) ^m Word ( E u. F ) ) ) /\ A. w e. Word ( E u. F ) ( ( mulGrp ` R ) gsum w ) = ( ( 1st ` ( q ` w ) ) .x. ( 2nd ` ( q ` w ) ) ) ) -> ( f e. F |-> ( R gsum ( v e. ( `' q " ( E X. { f } ) ) |-> ( ( G ` v ) ( .g ` R ) ( 1st ` ( q ` v ) ) ) ) ) ) : F --> E )
65 12 13 64 elmapdd 
 |-  ( ( ( ph /\ q e. ( ( E X. F ) ^m Word ( E u. F ) ) ) /\ A. w e. Word ( E u. F ) ( ( mulGrp ` R ) gsum w ) = ( ( 1st ` ( q ` w ) ) .x. ( 2nd ` ( q ` w ) ) ) ) -> ( f e. F |-> ( R gsum ( v e. ( `' q " ( E X. { f } ) ) |-> ( ( G ` v ) ( .g ` R ) ( 1st ` ( q ` v ) ) ) ) ) ) e. ( E ^m F ) )
66 breq1 
 |-  ( p = ( f e. F |-> ( R gsum ( v e. ( `' q " ( E X. { f } ) ) |-> ( ( G ` v ) ( .g ` R ) ( 1st ` ( q ` v ) ) ) ) ) ) -> ( p finSupp .0. <-> ( f e. F |-> ( R gsum ( v e. ( `' q " ( E X. { f } ) ) |-> ( ( G ` v ) ( .g ` R ) ( 1st ` ( q ` v ) ) ) ) ) ) finSupp .0. ) )
67 66 adantl 
 |-  ( ( ( ( ph /\ q e. ( ( E X. F ) ^m Word ( E u. F ) ) ) /\ A. w e. Word ( E u. F ) ( ( mulGrp ` R ) gsum w ) = ( ( 1st ` ( q ` w ) ) .x. ( 2nd ` ( q ` w ) ) ) ) /\ p = ( f e. F |-> ( R gsum ( v e. ( `' q " ( E X. { f } ) ) |-> ( ( G ` v ) ( .g ` R ) ( 1st ` ( q ` v ) ) ) ) ) ) ) -> ( p finSupp .0. <-> ( f e. F |-> ( R gsum ( v e. ( `' q " ( E X. { f } ) ) |-> ( ( G ` v ) ( .g ` R ) ( 1st ` ( q ` v ) ) ) ) ) ) finSupp .0. ) )
68 nfv 
 |-  F/ f ( ( ph /\ q e. ( ( E X. F ) ^m Word ( E u. F ) ) ) /\ A. w e. Word ( E u. F ) ( ( mulGrp ` R ) gsum w ) = ( ( 1st ` ( q ` w ) ) .x. ( 2nd ` ( q ` w ) ) ) )
69 nfmpt1 
 |-  F/_ f ( f e. F |-> ( R gsum ( v e. ( `' q " ( E X. { f } ) ) |-> ( ( G ` v ) ( .g ` R ) ( 1st ` ( q ` v ) ) ) ) ) )
70 69 nfeq2 
 |-  F/ f p = ( f e. F |-> ( R gsum ( v e. ( `' q " ( E X. { f } ) ) |-> ( ( G ` v ) ( .g ` R ) ( 1st ` ( q ` v ) ) ) ) ) )
71 68 70 nfan 
 |-  F/ f ( ( ( ph /\ q e. ( ( E X. F ) ^m Word ( E u. F ) ) ) /\ A. w e. Word ( E u. F ) ( ( mulGrp ` R ) gsum w ) = ( ( 1st ` ( q ` w ) ) .x. ( 2nd ` ( q ` w ) ) ) ) /\ p = ( f e. F |-> ( R gsum ( v e. ( `' q " ( E X. { f } ) ) |-> ( ( G ` v ) ( .g ` R ) ( 1st ` ( q ` v ) ) ) ) ) ) )
72 simpr 
 |-  ( ( ( ( ph /\ q e. ( ( E X. F ) ^m Word ( E u. F ) ) ) /\ A. w e. Word ( E u. F ) ( ( mulGrp ` R ) gsum w ) = ( ( 1st ` ( q ` w ) ) .x. ( 2nd ` ( q ` w ) ) ) ) /\ p = ( f e. F |-> ( R gsum ( v e. ( `' q " ( E X. { f } ) ) |-> ( ( G ` v ) ( .g ` R ) ( 1st ` ( q ` v ) ) ) ) ) ) ) -> p = ( f e. F |-> ( R gsum ( v e. ( `' q " ( E X. { f } ) ) |-> ( ( G ` v ) ( .g ` R ) ( 1st ` ( q ` v ) ) ) ) ) ) )
73 ovexd 
 |-  ( ( ( ( ( ph /\ q e. ( ( E X. F ) ^m Word ( E u. F ) ) ) /\ A. w e. Word ( E u. F ) ( ( mulGrp ` R ) gsum w ) = ( ( 1st ` ( q ` w ) ) .x. ( 2nd ` ( q ` w ) ) ) ) /\ p = ( f e. F |-> ( R gsum ( v e. ( `' q " ( E X. { f } ) ) |-> ( ( G ` v ) ( .g ` R ) ( 1st ` ( q ` v ) ) ) ) ) ) ) /\ f e. F ) -> ( R gsum ( v e. ( `' q " ( E X. { f } ) ) |-> ( ( G ` v ) ( .g ` R ) ( 1st ` ( q ` v ) ) ) ) ) e. _V )
74 72 73 fvmpt2d 
 |-  ( ( ( ( ( ph /\ q e. ( ( E X. F ) ^m Word ( E u. F ) ) ) /\ A. w e. Word ( E u. F ) ( ( mulGrp ` R ) gsum w ) = ( ( 1st ` ( q ` w ) ) .x. ( 2nd ` ( q ` w ) ) ) ) /\ p = ( f e. F |-> ( R gsum ( v e. ( `' q " ( E X. { f } ) ) |-> ( ( G ` v ) ( .g ` R ) ( 1st ` ( q ` v ) ) ) ) ) ) ) /\ f e. F ) -> ( p ` f ) = ( R gsum ( v e. ( `' q " ( E X. { f } ) ) |-> ( ( G ` v ) ( .g ` R ) ( 1st ` ( q ` v ) ) ) ) ) )
75 74 oveq1d 
 |-  ( ( ( ( ( ph /\ q e. ( ( E X. F ) ^m Word ( E u. F ) ) ) /\ A. w e. Word ( E u. F ) ( ( mulGrp ` R ) gsum w ) = ( ( 1st ` ( q ` w ) ) .x. ( 2nd ` ( q ` w ) ) ) ) /\ p = ( f e. F |-> ( R gsum ( v e. ( `' q " ( E X. { f } ) ) |-> ( ( G ` v ) ( .g ` R ) ( 1st ` ( q ` v ) ) ) ) ) ) ) /\ f e. F ) -> ( ( p ` f ) .x. f ) = ( ( R gsum ( v e. ( `' q " ( E X. { f } ) ) |-> ( ( G ` v ) ( .g ` R ) ( 1st ` ( q ` v ) ) ) ) ) .x. f ) )
76 71 75 mpteq2da 
 |-  ( ( ( ( ph /\ q e. ( ( E X. F ) ^m Word ( E u. F ) ) ) /\ A. w e. Word ( E u. F ) ( ( mulGrp ` R ) gsum w ) = ( ( 1st ` ( q ` w ) ) .x. ( 2nd ` ( q ` w ) ) ) ) /\ p = ( f e. F |-> ( R gsum ( v e. ( `' q " ( E X. { f } ) ) |-> ( ( G ` v ) ( .g ` R ) ( 1st ` ( q ` v ) ) ) ) ) ) ) -> ( f e. F |-> ( ( p ` f ) .x. f ) ) = ( f e. F |-> ( ( R gsum ( v e. ( `' q " ( E X. { f } ) ) |-> ( ( G ` v ) ( .g ` R ) ( 1st ` ( q ` v ) ) ) ) ) .x. f ) ) )
77 76 oveq2d 
 |-  ( ( ( ( ph /\ q e. ( ( E X. F ) ^m Word ( E u. F ) ) ) /\ A. w e. Word ( E u. F ) ( ( mulGrp ` R ) gsum w ) = ( ( 1st ` ( q ` w ) ) .x. ( 2nd ` ( q ` w ) ) ) ) /\ p = ( f e. F |-> ( R gsum ( v e. ( `' q " ( E X. { f } ) ) |-> ( ( G ` v ) ( .g ` R ) ( 1st ` ( q ` v ) ) ) ) ) ) ) -> ( R gsum ( f e. F |-> ( ( p ` f ) .x. f ) ) ) = ( R gsum ( f e. F |-> ( ( R gsum ( v e. ( `' q " ( E X. { f } ) ) |-> ( ( G ` v ) ( .g ` R ) ( 1st ` ( q ` v ) ) ) ) ) .x. f ) ) ) )
78 77 eqeq2d 
 |-  ( ( ( ( ph /\ q e. ( ( E X. F ) ^m Word ( E u. F ) ) ) /\ A. w e. Word ( E u. F ) ( ( mulGrp ` R ) gsum w ) = ( ( 1st ` ( q ` w ) ) .x. ( 2nd ` ( q ` w ) ) ) ) /\ p = ( f e. F |-> ( R gsum ( v e. ( `' q " ( E X. { f } ) ) |-> ( ( G ` v ) ( .g ` R ) ( 1st ` ( q ` v ) ) ) ) ) ) ) -> ( X = ( R gsum ( f e. F |-> ( ( p ` f ) .x. f ) ) ) <-> X = ( R gsum ( f e. F |-> ( ( R gsum ( v e. ( `' q " ( E X. { f } ) ) |-> ( ( G ` v ) ( .g ` R ) ( 1st ` ( q ` v ) ) ) ) ) .x. f ) ) ) ) )
79 67 78 anbi12d 
 |-  ( ( ( ( ph /\ q e. ( ( E X. F ) ^m Word ( E u. F ) ) ) /\ A. w e. Word ( E u. F ) ( ( mulGrp ` R ) gsum w ) = ( ( 1st ` ( q ` w ) ) .x. ( 2nd ` ( q ` w ) ) ) ) /\ p = ( f e. F |-> ( R gsum ( v e. ( `' q " ( E X. { f } ) ) |-> ( ( G ` v ) ( .g ` R ) ( 1st ` ( q ` v ) ) ) ) ) ) ) -> ( ( p finSupp .0. /\ X = ( R gsum ( f e. F |-> ( ( p ` f ) .x. f ) ) ) ) <-> ( ( f e. F |-> ( R gsum ( v e. ( `' q " ( E X. { f } ) ) |-> ( ( G ` v ) ( .g ` R ) ( 1st ` ( q ` v ) ) ) ) ) ) finSupp .0. /\ X = ( R gsum ( f e. F |-> ( ( R gsum ( v e. ( `' q " ( E X. { f } ) ) |-> ( ( G ` v ) ( .g ` R ) ( 1st ` ( q ` v ) ) ) ) ) .x. f ) ) ) ) ) )
80 60 a1i 
 |-  ( ( ( ph /\ q e. ( ( E X. F ) ^m Word ( E u. F ) ) ) /\ A. w e. Word ( E u. F ) ( ( mulGrp ` R ) gsum w ) = ( ( 1st ` ( q ` w ) ) .x. ( 2nd ` ( q ` w ) ) ) ) -> .0. e. _V )
81 64 ffund 
 |-  ( ( ( ph /\ q e. ( ( E X. F ) ^m Word ( E u. F ) ) ) /\ A. w e. Word ( E u. F ) ( ( mulGrp ` R ) gsum w ) = ( ( 1st ` ( q ` w ) ) .x. ( 2nd ` ( q ` w ) ) ) ) -> Fun ( f e. F |-> ( R gsum ( v e. ( `' q " ( E X. { f } ) ) |-> ( ( G ` v ) ( .g ` R ) ( 1st ` ( q ` v ) ) ) ) ) ) )
82 33 adantr 
 |-  ( ( ( ph /\ q e. ( ( E X. F ) ^m Word ( E u. F ) ) ) /\ A. w e. Word ( E u. F ) ( ( mulGrp ` R ) gsum w ) = ( ( 1st ` ( q ` w ) ) .x. ( 2nd ` ( q ` w ) ) ) ) -> Fun q )
83 10 fsuppimpd 
 |-  ( ph -> ( G supp 0 ) e. Fin )
84 83 ad2antrr 
 |-  ( ( ( ph /\ q e. ( ( E X. F ) ^m Word ( E u. F ) ) ) /\ A. w e. Word ( E u. F ) ( ( mulGrp ` R ) gsum w ) = ( ( 1st ` ( q ` w ) ) .x. ( 2nd ` ( q ` w ) ) ) ) -> ( G supp 0 ) e. Fin )
85 imafi 
 |-  ( ( Fun q /\ ( G supp 0 ) e. Fin ) -> ( q " ( G supp 0 ) ) e. Fin )
86 82 84 85 syl2anc 
 |-  ( ( ( ph /\ q e. ( ( E X. F ) ^m Word ( E u. F ) ) ) /\ A. w e. Word ( E u. F ) ( ( mulGrp ` R ) gsum w ) = ( ( 1st ` ( q ` w ) ) .x. ( 2nd ` ( q ` w ) ) ) ) -> ( q " ( G supp 0 ) ) e. Fin )
87 rnfi 
 |-  ( ( q " ( G supp 0 ) ) e. Fin -> ran ( q " ( G supp 0 ) ) e. Fin )
88 86 87 syl 
 |-  ( ( ( ph /\ q e. ( ( E X. F ) ^m Word ( E u. F ) ) ) /\ A. w e. Word ( E u. F ) ( ( mulGrp ` R ) gsum w ) = ( ( 1st ` ( q ` w ) ) .x. ( 2nd ` ( q ` w ) ) ) ) -> ran ( q " ( G supp 0 ) ) e. Fin )
89 9 ffnd 
 |-  ( ph -> G Fn Word ( E u. F ) )
90 89 ad4antr 
 |-  ( ( ( ( ( ph /\ q e. ( ( E X. F ) ^m Word ( E u. F ) ) ) /\ A. w e. Word ( E u. F ) ( ( mulGrp ` R ) gsum w ) = ( ( 1st ` ( q ` w ) ) .x. ( 2nd ` ( q ` w ) ) ) ) /\ f e. ( F \ ran ( q " ( G supp 0 ) ) ) ) /\ v e. ( `' q " ( E X. { f } ) ) ) -> G Fn Word ( E u. F ) )
91 30 ad4antr 
 |-  ( ( ( ( ( ph /\ q e. ( ( E X. F ) ^m Word ( E u. F ) ) ) /\ A. w e. Word ( E u. F ) ( ( mulGrp ` R ) gsum w ) = ( ( 1st ` ( q ` w ) ) .x. ( 2nd ` ( q ` w ) ) ) ) /\ f e. ( F \ ran ( q " ( G supp 0 ) ) ) ) /\ v e. ( `' q " ( E X. { f } ) ) ) -> Word ( E u. F ) e. _V )
92 0zd 
 |-  ( ( ( ( ( ph /\ q e. ( ( E X. F ) ^m Word ( E u. F ) ) ) /\ A. w e. Word ( E u. F ) ( ( mulGrp ` R ) gsum w ) = ( ( 1st ` ( q ` w ) ) .x. ( 2nd ` ( q ` w ) ) ) ) /\ f e. ( F \ ran ( q " ( G supp 0 ) ) ) ) /\ v e. ( `' q " ( E X. { f } ) ) ) -> 0 e. ZZ )
93 snssi 
 |-  ( f e. ( F \ ran ( q " ( G supp 0 ) ) ) -> { f } C_ ( F \ ran ( q " ( G supp 0 ) ) ) )
94 93 adantl 
 |-  ( ( ( ph /\ q e. ( ( E X. F ) ^m Word ( E u. F ) ) ) /\ f e. ( F \ ran ( q " ( G supp 0 ) ) ) ) -> { f } C_ ( F \ ran ( q " ( G supp 0 ) ) ) )
95 xpss2 
 |-  ( { f } C_ ( F \ ran ( q " ( G supp 0 ) ) ) -> ( E X. { f } ) C_ ( E X. ( F \ ran ( q " ( G supp 0 ) ) ) ) )
96 ssun2 
 |-  ( E X. ( F \ ran ( q " ( G supp 0 ) ) ) ) C_ ( ( ( E \ dom ( q " ( G supp 0 ) ) ) X. F ) u. ( E X. ( F \ ran ( q " ( G supp 0 ) ) ) ) )
97 difxp 
 |-  ( ( E X. F ) \ ( dom ( q " ( G supp 0 ) ) X. ran ( q " ( G supp 0 ) ) ) ) = ( ( ( E \ dom ( q " ( G supp 0 ) ) ) X. F ) u. ( E X. ( F \ ran ( q " ( G supp 0 ) ) ) ) )
98 96 97 sseqtrri 
 |-  ( E X. ( F \ ran ( q " ( G supp 0 ) ) ) ) C_ ( ( E X. F ) \ ( dom ( q " ( G supp 0 ) ) X. ran ( q " ( G supp 0 ) ) ) )
99 95 98 sstrdi 
 |-  ( { f } C_ ( F \ ran ( q " ( G supp 0 ) ) ) -> ( E X. { f } ) C_ ( ( E X. F ) \ ( dom ( q " ( G supp 0 ) ) X. ran ( q " ( G supp 0 ) ) ) ) )
100 94 99 syl 
 |-  ( ( ( ph /\ q e. ( ( E X. F ) ^m Word ( E u. F ) ) ) /\ f e. ( F \ ran ( q " ( G supp 0 ) ) ) ) -> ( E X. { f } ) C_ ( ( E X. F ) \ ( dom ( q " ( G supp 0 ) ) X. ran ( q " ( G supp 0 ) ) ) ) )
101 imassrn 
 |-  ( q " ( G supp 0 ) ) C_ ran q
102 32 frnd 
 |-  ( ( ph /\ q e. ( ( E X. F ) ^m Word ( E u. F ) ) ) -> ran q C_ ( E X. F ) )
103 102 adantr 
 |-  ( ( ( ph /\ q e. ( ( E X. F ) ^m Word ( E u. F ) ) ) /\ f e. ( F \ ran ( q " ( G supp 0 ) ) ) ) -> ran q C_ ( E X. F ) )
104 101 103 sstrid 
 |-  ( ( ( ph /\ q e. ( ( E X. F ) ^m Word ( E u. F ) ) ) /\ f e. ( F \ ran ( q " ( G supp 0 ) ) ) ) -> ( q " ( G supp 0 ) ) C_ ( E X. F ) )
105 relxp 
 |-  Rel ( E X. F )
106 relss 
 |-  ( ( q " ( G supp 0 ) ) C_ ( E X. F ) -> ( Rel ( E X. F ) -> Rel ( q " ( G supp 0 ) ) ) )
107 105 106 mpi 
 |-  ( ( q " ( G supp 0 ) ) C_ ( E X. F ) -> Rel ( q " ( G supp 0 ) ) )
108 relssdmrn 
 |-  ( Rel ( q " ( G supp 0 ) ) -> ( q " ( G supp 0 ) ) C_ ( dom ( q " ( G supp 0 ) ) X. ran ( q " ( G supp 0 ) ) ) )
109 104 107 108 3syl 
 |-  ( ( ( ph /\ q e. ( ( E X. F ) ^m Word ( E u. F ) ) ) /\ f e. ( F \ ran ( q " ( G supp 0 ) ) ) ) -> ( q " ( G supp 0 ) ) C_ ( dom ( q " ( G supp 0 ) ) X. ran ( q " ( G supp 0 ) ) ) )
110 109 sscond 
 |-  ( ( ( ph /\ q e. ( ( E X. F ) ^m Word ( E u. F ) ) ) /\ f e. ( F \ ran ( q " ( G supp 0 ) ) ) ) -> ( ( E X. F ) \ ( dom ( q " ( G supp 0 ) ) X. ran ( q " ( G supp 0 ) ) ) ) C_ ( ( E X. F ) \ ( q " ( G supp 0 ) ) ) )
111 100 110 sstrd 
 |-  ( ( ( ph /\ q e. ( ( E X. F ) ^m Word ( E u. F ) ) ) /\ f e. ( F \ ran ( q " ( G supp 0 ) ) ) ) -> ( E X. { f } ) C_ ( ( E X. F ) \ ( q " ( G supp 0 ) ) ) )
112 imass2 
 |-  ( ( E X. { f } ) C_ ( ( E X. F ) \ ( q " ( G supp 0 ) ) ) -> ( `' q " ( E X. { f } ) ) C_ ( `' q " ( ( E X. F ) \ ( q " ( G supp 0 ) ) ) ) )
113 111 112 syl 
 |-  ( ( ( ph /\ q e. ( ( E X. F ) ^m Word ( E u. F ) ) ) /\ f e. ( F \ ran ( q " ( G supp 0 ) ) ) ) -> ( `' q " ( E X. { f } ) ) C_ ( `' q " ( ( E X. F ) \ ( q " ( G supp 0 ) ) ) ) )
114 113 adantlr 
 |-  ( ( ( ( ph /\ q e. ( ( E X. F ) ^m Word ( E u. F ) ) ) /\ A. w e. Word ( E u. F ) ( ( mulGrp ` R ) gsum w ) = ( ( 1st ` ( q ` w ) ) .x. ( 2nd ` ( q ` w ) ) ) ) /\ f e. ( F \ ran ( q " ( G supp 0 ) ) ) ) -> ( `' q " ( E X. { f } ) ) C_ ( `' q " ( ( E X. F ) \ ( q " ( G supp 0 ) ) ) ) )
115 82 adantr 
 |-  ( ( ( ( ph /\ q e. ( ( E X. F ) ^m Word ( E u. F ) ) ) /\ A. w e. Word ( E u. F ) ( ( mulGrp ` R ) gsum w ) = ( ( 1st ` ( q ` w ) ) .x. ( 2nd ` ( q ` w ) ) ) ) /\ f e. ( F \ ran ( q " ( G supp 0 ) ) ) ) -> Fun q )
116 difpreima 
 |-  ( Fun q -> ( `' q " ( ( E X. F ) \ ( q " ( G supp 0 ) ) ) ) = ( ( `' q " ( E X. F ) ) \ ( `' q " ( q " ( G supp 0 ) ) ) ) )
117 115 116 syl 
 |-  ( ( ( ( ph /\ q e. ( ( E X. F ) ^m Word ( E u. F ) ) ) /\ A. w e. Word ( E u. F ) ( ( mulGrp ` R ) gsum w ) = ( ( 1st ` ( q ` w ) ) .x. ( 2nd ` ( q ` w ) ) ) ) /\ f e. ( F \ ran ( q " ( G supp 0 ) ) ) ) -> ( `' q " ( ( E X. F ) \ ( q " ( G supp 0 ) ) ) ) = ( ( `' q " ( E X. F ) ) \ ( `' q " ( q " ( G supp 0 ) ) ) ) )
118 cnvimass 
 |-  ( `' q " ( E X. F ) ) C_ dom q
119 42 ad2antrr 
 |-  ( ( ( ( ph /\ q e. ( ( E X. F ) ^m Word ( E u. F ) ) ) /\ A. w e. Word ( E u. F ) ( ( mulGrp ` R ) gsum w ) = ( ( 1st ` ( q ` w ) ) .x. ( 2nd ` ( q ` w ) ) ) ) /\ f e. ( F \ ran ( q " ( G supp 0 ) ) ) ) -> dom q = Word ( E u. F ) )
120 118 119 sseqtrid 
 |-  ( ( ( ( ph /\ q e. ( ( E X. F ) ^m Word ( E u. F ) ) ) /\ A. w e. Word ( E u. F ) ( ( mulGrp ` R ) gsum w ) = ( ( 1st ` ( q ` w ) ) .x. ( 2nd ` ( q ` w ) ) ) ) /\ f e. ( F \ ran ( q " ( G supp 0 ) ) ) ) -> ( `' q " ( E X. F ) ) C_ Word ( E u. F ) )
121 suppssdm 
 |-  ( G supp 0 ) C_ dom G
122 9 fdmd 
 |-  ( ph -> dom G = Word ( E u. F ) )
123 122 ad3antrrr 
 |-  ( ( ( ( ph /\ q e. ( ( E X. F ) ^m Word ( E u. F ) ) ) /\ A. w e. Word ( E u. F ) ( ( mulGrp ` R ) gsum w ) = ( ( 1st ` ( q ` w ) ) .x. ( 2nd ` ( q ` w ) ) ) ) /\ f e. ( F \ ran ( q " ( G supp 0 ) ) ) ) -> dom G = Word ( E u. F ) )
124 121 123 sseqtrid 
 |-  ( ( ( ( ph /\ q e. ( ( E X. F ) ^m Word ( E u. F ) ) ) /\ A. w e. Word ( E u. F ) ( ( mulGrp ` R ) gsum w ) = ( ( 1st ` ( q ` w ) ) .x. ( 2nd ` ( q ` w ) ) ) ) /\ f e. ( F \ ran ( q " ( G supp 0 ) ) ) ) -> ( G supp 0 ) C_ Word ( E u. F ) )
125 124 119 sseqtrrd 
 |-  ( ( ( ( ph /\ q e. ( ( E X. F ) ^m Word ( E u. F ) ) ) /\ A. w e. Word ( E u. F ) ( ( mulGrp ` R ) gsum w ) = ( ( 1st ` ( q ` w ) ) .x. ( 2nd ` ( q ` w ) ) ) ) /\ f e. ( F \ ran ( q " ( G supp 0 ) ) ) ) -> ( G supp 0 ) C_ dom q )
126 sseqin2 
 |-  ( ( G supp 0 ) C_ dom q <-> ( dom q i^i ( G supp 0 ) ) = ( G supp 0 ) )
127 126 biimpi 
 |-  ( ( G supp 0 ) C_ dom q -> ( dom q i^i ( G supp 0 ) ) = ( G supp 0 ) )
128 dminss 
 |-  ( dom q i^i ( G supp 0 ) ) C_ ( `' q " ( q " ( G supp 0 ) ) )
129 127 128 eqsstrrdi 
 |-  ( ( G supp 0 ) C_ dom q -> ( G supp 0 ) C_ ( `' q " ( q " ( G supp 0 ) ) ) )
130 125 129 syl 
 |-  ( ( ( ( ph /\ q e. ( ( E X. F ) ^m Word ( E u. F ) ) ) /\ A. w e. Word ( E u. F ) ( ( mulGrp ` R ) gsum w ) = ( ( 1st ` ( q ` w ) ) .x. ( 2nd ` ( q ` w ) ) ) ) /\ f e. ( F \ ran ( q " ( G supp 0 ) ) ) ) -> ( G supp 0 ) C_ ( `' q " ( q " ( G supp 0 ) ) ) )
131 120 130 ssdif2d 
 |-  ( ( ( ( ph /\ q e. ( ( E X. F ) ^m Word ( E u. F ) ) ) /\ A. w e. Word ( E u. F ) ( ( mulGrp ` R ) gsum w ) = ( ( 1st ` ( q ` w ) ) .x. ( 2nd ` ( q ` w ) ) ) ) /\ f e. ( F \ ran ( q " ( G supp 0 ) ) ) ) -> ( ( `' q " ( E X. F ) ) \ ( `' q " ( q " ( G supp 0 ) ) ) ) C_ ( Word ( E u. F ) \ ( G supp 0 ) ) )
132 117 131 eqsstrd 
 |-  ( ( ( ( ph /\ q e. ( ( E X. F ) ^m Word ( E u. F ) ) ) /\ A. w e. Word ( E u. F ) ( ( mulGrp ` R ) gsum w ) = ( ( 1st ` ( q ` w ) ) .x. ( 2nd ` ( q ` w ) ) ) ) /\ f e. ( F \ ran ( q " ( G supp 0 ) ) ) ) -> ( `' q " ( ( E X. F ) \ ( q " ( G supp 0 ) ) ) ) C_ ( Word ( E u. F ) \ ( G supp 0 ) ) )
133 114 132 sstrd 
 |-  ( ( ( ( ph /\ q e. ( ( E X. F ) ^m Word ( E u. F ) ) ) /\ A. w e. Word ( E u. F ) ( ( mulGrp ` R ) gsum w ) = ( ( 1st ` ( q ` w ) ) .x. ( 2nd ` ( q ` w ) ) ) ) /\ f e. ( F \ ran ( q " ( G supp 0 ) ) ) ) -> ( `' q " ( E X. { f } ) ) C_ ( Word ( E u. F ) \ ( G supp 0 ) ) )
134 133 sselda 
 |-  ( ( ( ( ( ph /\ q e. ( ( E X. F ) ^m Word ( E u. F ) ) ) /\ A. w e. Word ( E u. F ) ( ( mulGrp ` R ) gsum w ) = ( ( 1st ` ( q ` w ) ) .x. ( 2nd ` ( q ` w ) ) ) ) /\ f e. ( F \ ran ( q " ( G supp 0 ) ) ) ) /\ v e. ( `' q " ( E X. { f } ) ) ) -> v e. ( Word ( E u. F ) \ ( G supp 0 ) ) )
135 90 91 92 134 fvdifsupp 
 |-  ( ( ( ( ( ph /\ q e. ( ( E X. F ) ^m Word ( E u. F ) ) ) /\ A. w e. Word ( E u. F ) ( ( mulGrp ` R ) gsum w ) = ( ( 1st ` ( q ` w ) ) .x. ( 2nd ` ( q ` w ) ) ) ) /\ f e. ( F \ ran ( q " ( G supp 0 ) ) ) ) /\ v e. ( `' q " ( E X. { f } ) ) ) -> ( G ` v ) = 0 )
136 135 oveq1d 
 |-  ( ( ( ( ( ph /\ q e. ( ( E X. F ) ^m Word ( E u. F ) ) ) /\ A. w e. Word ( E u. F ) ( ( mulGrp ` R ) gsum w ) = ( ( 1st ` ( q ` w ) ) .x. ( 2nd ` ( q ` w ) ) ) ) /\ f e. ( F \ ran ( q " ( G supp 0 ) ) ) ) /\ v e. ( `' q " ( E X. { f } ) ) ) -> ( ( G ` v ) ( .g ` R ) ( 1st ` ( q ` v ) ) ) = ( 0 ( .g ` R ) ( 1st ` ( q ` v ) ) ) )
137 55 ad4antr 
 |-  ( ( ( ( ( ph /\ q e. ( ( E X. F ) ^m Word ( E u. F ) ) ) /\ A. w e. Word ( E u. F ) ( ( mulGrp ` R ) gsum w ) = ( ( 1st ` ( q ` w ) ) .x. ( 2nd ` ( q ` w ) ) ) ) /\ f e. ( F \ ran ( q " ( G supp 0 ) ) ) ) /\ v e. ( `' q " ( E X. { f } ) ) ) -> E C_ B )
138 32 ad3antrrr 
 |-  ( ( ( ( ( ph /\ q e. ( ( E X. F ) ^m Word ( E u. F ) ) ) /\ A. w e. Word ( E u. F ) ( ( mulGrp ` R ) gsum w ) = ( ( 1st ` ( q ` w ) ) .x. ( 2nd ` ( q ` w ) ) ) ) /\ f e. ( F \ ran ( q " ( G supp 0 ) ) ) ) /\ v e. ( `' q " ( E X. { f } ) ) ) -> q : Word ( E u. F ) --> ( E X. F ) )
139 41 42 sseqtrid 
 |-  ( ( ph /\ q e. ( ( E X. F ) ^m Word ( E u. F ) ) ) -> ( `' q " ( E X. { f } ) ) C_ Word ( E u. F ) )
140 139 ad2antrr 
 |-  ( ( ( ( ph /\ q e. ( ( E X. F ) ^m Word ( E u. F ) ) ) /\ A. w e. Word ( E u. F ) ( ( mulGrp ` R ) gsum w ) = ( ( 1st ` ( q ` w ) ) .x. ( 2nd ` ( q ` w ) ) ) ) /\ f e. ( F \ ran ( q " ( G supp 0 ) ) ) ) -> ( `' q " ( E X. { f } ) ) C_ Word ( E u. F ) )
141 140 sselda 
 |-  ( ( ( ( ( ph /\ q e. ( ( E X. F ) ^m Word ( E u. F ) ) ) /\ A. w e. Word ( E u. F ) ( ( mulGrp ` R ) gsum w ) = ( ( 1st ` ( q ` w ) ) .x. ( 2nd ` ( q ` w ) ) ) ) /\ f e. ( F \ ran ( q " ( G supp 0 ) ) ) ) /\ v e. ( `' q " ( E X. { f } ) ) ) -> v e. Word ( E u. F ) )
142 138 141 ffvelcdmd 
 |-  ( ( ( ( ( ph /\ q e. ( ( E X. F ) ^m Word ( E u. F ) ) ) /\ A. w e. Word ( E u. F ) ( ( mulGrp ` R ) gsum w ) = ( ( 1st ` ( q ` w ) ) .x. ( 2nd ` ( q ` w ) ) ) ) /\ f e. ( F \ ran ( q " ( G supp 0 ) ) ) ) /\ v e. ( `' q " ( E X. { f } ) ) ) -> ( q ` v ) e. ( E X. F ) )
143 xp1st 
 |-  ( ( q ` v ) e. ( E X. F ) -> ( 1st ` ( q ` v ) ) e. E )
144 142 143 syl 
 |-  ( ( ( ( ( ph /\ q e. ( ( E X. F ) ^m Word ( E u. F ) ) ) /\ A. w e. Word ( E u. F ) ( ( mulGrp ` R ) gsum w ) = ( ( 1st ` ( q ` w ) ) .x. ( 2nd ` ( q ` w ) ) ) ) /\ f e. ( F \ ran ( q " ( G supp 0 ) ) ) ) /\ v e. ( `' q " ( E X. { f } ) ) ) -> ( 1st ` ( q ` v ) ) e. E )
145 137 144 sseldd 
 |-  ( ( ( ( ( ph /\ q e. ( ( E X. F ) ^m Word ( E u. F ) ) ) /\ A. w e. Word ( E u. F ) ( ( mulGrp ` R ) gsum w ) = ( ( 1st ` ( q ` w ) ) .x. ( 2nd ` ( q ` w ) ) ) ) /\ f e. ( F \ ran ( q " ( G supp 0 ) ) ) ) /\ v e. ( `' q " ( E X. { f } ) ) ) -> ( 1st ` ( q ` v ) ) e. B )
146 1 3 24 mulg0 
 |-  ( ( 1st ` ( q ` v ) ) e. B -> ( 0 ( .g ` R ) ( 1st ` ( q ` v ) ) ) = .0. )
147 145 146 syl 
 |-  ( ( ( ( ( ph /\ q e. ( ( E X. F ) ^m Word ( E u. F ) ) ) /\ A. w e. Word ( E u. F ) ( ( mulGrp ` R ) gsum w ) = ( ( 1st ` ( q ` w ) ) .x. ( 2nd ` ( q ` w ) ) ) ) /\ f e. ( F \ ran ( q " ( G supp 0 ) ) ) ) /\ v e. ( `' q " ( E X. { f } ) ) ) -> ( 0 ( .g ` R ) ( 1st ` ( q ` v ) ) ) = .0. )
148 136 147 eqtrd 
 |-  ( ( ( ( ( ph /\ q e. ( ( E X. F ) ^m Word ( E u. F ) ) ) /\ A. w e. Word ( E u. F ) ( ( mulGrp ` R ) gsum w ) = ( ( 1st ` ( q ` w ) ) .x. ( 2nd ` ( q ` w ) ) ) ) /\ f e. ( F \ ran ( q " ( G supp 0 ) ) ) ) /\ v e. ( `' q " ( E X. { f } ) ) ) -> ( ( G ` v ) ( .g ` R ) ( 1st ` ( q ` v ) ) ) = .0. )
149 148 mpteq2dva 
 |-  ( ( ( ( ph /\ q e. ( ( E X. F ) ^m Word ( E u. F ) ) ) /\ A. w e. Word ( E u. F ) ( ( mulGrp ` R ) gsum w ) = ( ( 1st ` ( q ` w ) ) .x. ( 2nd ` ( q ` w ) ) ) ) /\ f e. ( F \ ran ( q " ( G supp 0 ) ) ) ) -> ( v e. ( `' q " ( E X. { f } ) ) |-> ( ( G ` v ) ( .g ` R ) ( 1st ` ( q ` v ) ) ) ) = ( v e. ( `' q " ( E X. { f } ) ) |-> .0. ) )
150 149 oveq2d 
 |-  ( ( ( ( ph /\ q e. ( ( E X. F ) ^m Word ( E u. F ) ) ) /\ A. w e. Word ( E u. F ) ( ( mulGrp ` R ) gsum w ) = ( ( 1st ` ( q ` w ) ) .x. ( 2nd ` ( q ` w ) ) ) ) /\ f e. ( F \ ran ( q " ( G supp 0 ) ) ) ) -> ( R gsum ( v e. ( `' q " ( E X. { f } ) ) |-> ( ( G ` v ) ( .g ` R ) ( 1st ` ( q ` v ) ) ) ) ) = ( R gsum ( v e. ( `' q " ( E X. { f } ) ) |-> .0. ) ) )
151 25 grpmndd 
 |-  ( ph -> R e. Mnd )
152 151 ad3antrrr 
 |-  ( ( ( ( ph /\ q e. ( ( E X. F ) ^m Word ( E u. F ) ) ) /\ A. w e. Word ( E u. F ) ( ( mulGrp ` R ) gsum w ) = ( ( 1st ` ( q ` w ) ) .x. ( 2nd ` ( q ` w ) ) ) ) /\ f e. ( F \ ran ( q " ( G supp 0 ) ) ) ) -> R e. Mnd )
153 19 a1i 
 |-  ( ( ( ( ph /\ q e. ( ( E X. F ) ^m Word ( E u. F ) ) ) /\ A. w e. Word ( E u. F ) ( ( mulGrp ` R ) gsum w ) = ( ( 1st ` ( q ` w ) ) .x. ( 2nd ` ( q ` w ) ) ) ) /\ f e. ( F \ ran ( q " ( G supp 0 ) ) ) ) -> ( `' q " ( E X. { f } ) ) e. _V )
154 3 gsumz 
 |-  ( ( R e. Mnd /\ ( `' q " ( E X. { f } ) ) e. _V ) -> ( R gsum ( v e. ( `' q " ( E X. { f } ) ) |-> .0. ) ) = .0. )
155 152 153 154 syl2anc 
 |-  ( ( ( ( ph /\ q e. ( ( E X. F ) ^m Word ( E u. F ) ) ) /\ A. w e. Word ( E u. F ) ( ( mulGrp ` R ) gsum w ) = ( ( 1st ` ( q ` w ) ) .x. ( 2nd ` ( q ` w ) ) ) ) /\ f e. ( F \ ran ( q " ( G supp 0 ) ) ) ) -> ( R gsum ( v e. ( `' q " ( E X. { f } ) ) |-> .0. ) ) = .0. )
156 150 155 eqtrd 
 |-  ( ( ( ( ph /\ q e. ( ( E X. F ) ^m Word ( E u. F ) ) ) /\ A. w e. Word ( E u. F ) ( ( mulGrp ` R ) gsum w ) = ( ( 1st ` ( q ` w ) ) .x. ( 2nd ` ( q ` w ) ) ) ) /\ f e. ( F \ ran ( q " ( G supp 0 ) ) ) ) -> ( R gsum ( v e. ( `' q " ( E X. { f } ) ) |-> ( ( G ` v ) ( .g ` R ) ( 1st ` ( q ` v ) ) ) ) ) = .0. )
157 156 13 suppss2 
 |-  ( ( ( ph /\ q e. ( ( E X. F ) ^m Word ( E u. F ) ) ) /\ A. w e. Word ( E u. F ) ( ( mulGrp ` R ) gsum w ) = ( ( 1st ` ( q ` w ) ) .x. ( 2nd ` ( q ` w ) ) ) ) -> ( ( f e. F |-> ( R gsum ( v e. ( `' q " ( E X. { f } ) ) |-> ( ( G ` v ) ( .g ` R ) ( 1st ` ( q ` v ) ) ) ) ) ) supp .0. ) C_ ran ( q " ( G supp 0 ) ) )
158 88 157 ssfid 
 |-  ( ( ( ph /\ q e. ( ( E X. F ) ^m Word ( E u. F ) ) ) /\ A. w e. Word ( E u. F ) ( ( mulGrp ` R ) gsum w ) = ( ( 1st ` ( q ` w ) ) .x. ( 2nd ` ( q ` w ) ) ) ) -> ( ( f e. F |-> ( R gsum ( v e. ( `' q " ( E X. { f } ) ) |-> ( ( G ` v ) ( .g ` R ) ( 1st ` ( q ` v ) ) ) ) ) ) supp .0. ) e. Fin )
159 65 80 81 158 isfsuppd 
 |-  ( ( ( ph /\ q e. ( ( E X. F ) ^m Word ( E u. F ) ) ) /\ A. w e. Word ( E u. F ) ( ( mulGrp ` R ) gsum w ) = ( ( 1st ` ( q ` w ) ) .x. ( 2nd ` ( q ` w ) ) ) ) -> ( f e. F |-> ( R gsum ( v e. ( `' q " ( E X. { f } ) ) |-> ( ( G ` v ) ( .g ` R ) ( 1st ` ( q ` v ) ) ) ) ) ) finSupp .0. )
160 15 ablcmnd 
 |-  ( ph -> R e. CMnd )
161 160 adantr 
 |-  ( ( ph /\ q e. ( ( E X. F ) ^m Word ( E u. F ) ) ) -> R e. CMnd )
162 30 adantr 
 |-  ( ( ph /\ q e. ( ( E X. F ) ^m Word ( E u. F ) ) ) -> Word ( E u. F ) e. _V )
163 89 ad2antrr 
 |-  ( ( ( ph /\ q e. ( ( E X. F ) ^m Word ( E u. F ) ) ) /\ w e. ( Word ( E u. F ) \ ( G supp 0 ) ) ) -> G Fn Word ( E u. F ) )
164 162 adantr 
 |-  ( ( ( ph /\ q e. ( ( E X. F ) ^m Word ( E u. F ) ) ) /\ w e. ( Word ( E u. F ) \ ( G supp 0 ) ) ) -> Word ( E u. F ) e. _V )
165 0zd 
 |-  ( ( ( ph /\ q e. ( ( E X. F ) ^m Word ( E u. F ) ) ) /\ w e. ( Word ( E u. F ) \ ( G supp 0 ) ) ) -> 0 e. ZZ )
166 simpr 
 |-  ( ( ( ph /\ q e. ( ( E X. F ) ^m Word ( E u. F ) ) ) /\ w e. ( Word ( E u. F ) \ ( G supp 0 ) ) ) -> w e. ( Word ( E u. F ) \ ( G supp 0 ) ) )
167 163 164 165 166 fvdifsupp 
 |-  ( ( ( ph /\ q e. ( ( E X. F ) ^m Word ( E u. F ) ) ) /\ w e. ( Word ( E u. F ) \ ( G supp 0 ) ) ) -> ( G ` w ) = 0 )
168 167 oveq1d 
 |-  ( ( ( ph /\ q e. ( ( E X. F ) ^m Word ( E u. F ) ) ) /\ w e. ( Word ( E u. F ) \ ( G supp 0 ) ) ) -> ( ( G ` w ) ( .g ` R ) ( ( mulGrp ` R ) gsum w ) ) = ( 0 ( .g ` R ) ( ( mulGrp ` R ) gsum w ) ) )
169 eqid 
 |-  ( mulGrp ` R ) = ( mulGrp ` R )
170 169 crngmgp 
 |-  ( R e. CRing -> ( mulGrp ` R ) e. CMnd )
171 5 170 syl 
 |-  ( ph -> ( mulGrp ` R ) e. CMnd )
172 171 cmnmndd 
 |-  ( ph -> ( mulGrp ` R ) e. Mnd )
173 172 ad2antrr 
 |-  ( ( ( ph /\ q e. ( ( E X. F ) ^m Word ( E u. F ) ) ) /\ w e. ( Word ( E u. F ) \ ( G supp 0 ) ) ) -> ( mulGrp ` R ) e. Mnd )
174 1 subrgss 
 |-  ( F e. ( SubRing ` R ) -> F C_ B )
175 7 174 syl 
 |-  ( ph -> F C_ B )
176 55 175 unssd 
 |-  ( ph -> ( E u. F ) C_ B )
177 sswrd 
 |-  ( ( E u. F ) C_ B -> Word ( E u. F ) C_ Word B )
178 176 177 syl 
 |-  ( ph -> Word ( E u. F ) C_ Word B )
179 178 adantr 
 |-  ( ( ph /\ q e. ( ( E X. F ) ^m Word ( E u. F ) ) ) -> Word ( E u. F ) C_ Word B )
180 179 adantr 
 |-  ( ( ( ph /\ q e. ( ( E X. F ) ^m Word ( E u. F ) ) ) /\ w e. ( Word ( E u. F ) \ ( G supp 0 ) ) ) -> Word ( E u. F ) C_ Word B )
181 166 eldifad 
 |-  ( ( ( ph /\ q e. ( ( E X. F ) ^m Word ( E u. F ) ) ) /\ w e. ( Word ( E u. F ) \ ( G supp 0 ) ) ) -> w e. Word ( E u. F ) )
182 180 181 sseldd 
 |-  ( ( ( ph /\ q e. ( ( E X. F ) ^m Word ( E u. F ) ) ) /\ w e. ( Word ( E u. F ) \ ( G supp 0 ) ) ) -> w e. Word B )
183 169 1 mgpbas 
 |-  B = ( Base ` ( mulGrp ` R ) )
184 183 gsumwcl 
 |-  ( ( ( mulGrp ` R ) e. Mnd /\ w e. Word B ) -> ( ( mulGrp ` R ) gsum w ) e. B )
185 173 182 184 syl2anc 
 |-  ( ( ( ph /\ q e. ( ( E X. F ) ^m Word ( E u. F ) ) ) /\ w e. ( Word ( E u. F ) \ ( G supp 0 ) ) ) -> ( ( mulGrp ` R ) gsum w ) e. B )
186 1 3 24 mulg0 
 |-  ( ( ( mulGrp ` R ) gsum w ) e. B -> ( 0 ( .g ` R ) ( ( mulGrp ` R ) gsum w ) ) = .0. )
187 185 186 syl 
 |-  ( ( ( ph /\ q e. ( ( E X. F ) ^m Word ( E u. F ) ) ) /\ w e. ( Word ( E u. F ) \ ( G supp 0 ) ) ) -> ( 0 ( .g ` R ) ( ( mulGrp ` R ) gsum w ) ) = .0. )
188 168 187 eqtrd 
 |-  ( ( ( ph /\ q e. ( ( E X. F ) ^m Word ( E u. F ) ) ) /\ w e. ( Word ( E u. F ) \ ( G supp 0 ) ) ) -> ( ( G ` w ) ( .g ` R ) ( ( mulGrp ` R ) gsum w ) ) = .0. )
189 83 adantr 
 |-  ( ( ph /\ q e. ( ( E X. F ) ^m Word ( E u. F ) ) ) -> ( G supp 0 ) e. Fin )
190 25 ad2antrr 
 |-  ( ( ( ph /\ q e. ( ( E X. F ) ^m Word ( E u. F ) ) ) /\ w e. Word ( E u. F ) ) -> R e. Grp )
191 9 adantr 
 |-  ( ( ph /\ q e. ( ( E X. F ) ^m Word ( E u. F ) ) ) -> G : Word ( E u. F ) --> ZZ )
192 191 ffvelcdmda 
 |-  ( ( ( ph /\ q e. ( ( E X. F ) ^m Word ( E u. F ) ) ) /\ w e. Word ( E u. F ) ) -> ( G ` w ) e. ZZ )
193 172 ad2antrr 
 |-  ( ( ( ph /\ q e. ( ( E X. F ) ^m Word ( E u. F ) ) ) /\ w e. Word ( E u. F ) ) -> ( mulGrp ` R ) e. Mnd )
194 179 sselda 
 |-  ( ( ( ph /\ q e. ( ( E X. F ) ^m Word ( E u. F ) ) ) /\ w e. Word ( E u. F ) ) -> w e. Word B )
195 193 194 184 syl2anc 
 |-  ( ( ( ph /\ q e. ( ( E X. F ) ^m Word ( E u. F ) ) ) /\ w e. Word ( E u. F ) ) -> ( ( mulGrp ` R ) gsum w ) e. B )
196 1 24 190 192 195 mulgcld 
 |-  ( ( ( ph /\ q e. ( ( E X. F ) ^m Word ( E u. F ) ) ) /\ w e. Word ( E u. F ) ) -> ( ( G ` w ) ( .g ` R ) ( ( mulGrp ` R ) gsum w ) ) e. B )
197 121 122 sseqtrid 
 |-  ( ph -> ( G supp 0 ) C_ Word ( E u. F ) )
198 197 adantr 
 |-  ( ( ph /\ q e. ( ( E X. F ) ^m Word ( E u. F ) ) ) -> ( G supp 0 ) C_ Word ( E u. F ) )
199 1 3 161 162 188 189 196 198 gsummptres2 
 |-  ( ( ph /\ q e. ( ( E X. F ) ^m Word ( E u. F ) ) ) -> ( R gsum ( w e. Word ( E u. F ) |-> ( ( G ` w ) ( .g ` R ) ( ( mulGrp ` R ) gsum w ) ) ) ) = ( R gsum ( w e. ( G supp 0 ) |-> ( ( G ` w ) ( .g ` R ) ( ( mulGrp ` R ) gsum w ) ) ) ) )
200 7 adantr 
 |-  ( ( ph /\ q e. ( ( E X. F ) ^m Word ( E u. F ) ) ) -> F e. ( SubRing ` R ) )
201 25 ad2antrr 
 |-  ( ( ( ph /\ q e. ( ( E X. F ) ^m Word ( E u. F ) ) ) /\ w e. ( G supp 0 ) ) -> R e. Grp )
202 9 ad2antrr 
 |-  ( ( ( ph /\ q e. ( ( E X. F ) ^m Word ( E u. F ) ) ) /\ w e. ( G supp 0 ) ) -> G : Word ( E u. F ) --> ZZ )
203 198 sselda 
 |-  ( ( ( ph /\ q e. ( ( E X. F ) ^m Word ( E u. F ) ) ) /\ w e. ( G supp 0 ) ) -> w e. Word ( E u. F ) )
204 202 203 ffvelcdmd 
 |-  ( ( ( ph /\ q e. ( ( E X. F ) ^m Word ( E u. F ) ) ) /\ w e. ( G supp 0 ) ) -> ( G ` w ) e. ZZ )
205 172 ad2antrr 
 |-  ( ( ( ph /\ q e. ( ( E X. F ) ^m Word ( E u. F ) ) ) /\ w e. ( G supp 0 ) ) -> ( mulGrp ` R ) e. Mnd )
206 198 179 sstrd 
 |-  ( ( ph /\ q e. ( ( E X. F ) ^m Word ( E u. F ) ) ) -> ( G supp 0 ) C_ Word B )
207 206 sselda 
 |-  ( ( ( ph /\ q e. ( ( E X. F ) ^m Word ( E u. F ) ) ) /\ w e. ( G supp 0 ) ) -> w e. Word B )
208 205 207 184 syl2anc 
 |-  ( ( ( ph /\ q e. ( ( E X. F ) ^m Word ( E u. F ) ) ) /\ w e. ( G supp 0 ) ) -> ( ( mulGrp ` R ) gsum w ) e. B )
209 1 24 201 204 208 mulgcld 
 |-  ( ( ( ph /\ q e. ( ( E X. F ) ^m Word ( E u. F ) ) ) /\ w e. ( G supp 0 ) ) -> ( ( G ` w ) ( .g ` R ) ( ( mulGrp ` R ) gsum w ) ) e. B )
210 32 adantr 
 |-  ( ( ( ph /\ q e. ( ( E X. F ) ^m Word ( E u. F ) ) ) /\ w e. ( G supp 0 ) ) -> q : Word ( E u. F ) --> ( E X. F ) )
211 210 203 ffvelcdmd 
 |-  ( ( ( ph /\ q e. ( ( E X. F ) ^m Word ( E u. F ) ) ) /\ w e. ( G supp 0 ) ) -> ( q ` w ) e. ( E X. F ) )
212 xp2nd 
 |-  ( ( q ` w ) e. ( E X. F ) -> ( 2nd ` ( q ` w ) ) e. F )
213 211 212 syl 
 |-  ( ( ( ph /\ q e. ( ( E X. F ) ^m Word ( E u. F ) ) ) /\ w e. ( G supp 0 ) ) -> ( 2nd ` ( q ` w ) ) e. F )
214 2fveq3 
 |-  ( v = w -> ( 2nd ` ( q ` v ) ) = ( 2nd ` ( q ` w ) ) )
215 214 cbvmptv 
 |-  ( v e. ( G supp 0 ) |-> ( 2nd ` ( q ` v ) ) ) = ( w e. ( G supp 0 ) |-> ( 2nd ` ( q ` w ) ) )
216 1 3 161 189 200 209 213 215 gsummpt2co 
 |-  ( ( ph /\ q e. ( ( E X. F ) ^m Word ( E u. F ) ) ) -> ( R gsum ( w e. ( G supp 0 ) |-> ( ( G ` w ) ( .g ` R ) ( ( mulGrp ` R ) gsum w ) ) ) ) = ( R gsum ( f e. F |-> ( R gsum ( w e. ( `' ( v e. ( G supp 0 ) |-> ( 2nd ` ( q ` v ) ) ) " { f } ) |-> ( ( G ` w ) ( .g ` R ) ( ( mulGrp ` R ) gsum w ) ) ) ) ) ) )
217 199 216 eqtrd 
 |-  ( ( ph /\ q e. ( ( E X. F ) ^m Word ( E u. F ) ) ) -> ( R gsum ( w e. Word ( E u. F ) |-> ( ( G ` w ) ( .g ` R ) ( ( mulGrp ` R ) gsum w ) ) ) ) = ( R gsum ( f e. F |-> ( R gsum ( w e. ( `' ( v e. ( G supp 0 ) |-> ( 2nd ` ( q ` v ) ) ) " { f } ) |-> ( ( G ` w ) ( .g ` R ) ( ( mulGrp ` R ) gsum w ) ) ) ) ) ) )
218 217 adantr 
 |-  ( ( ( ph /\ q e. ( ( E X. F ) ^m Word ( E u. F ) ) ) /\ A. w e. Word ( E u. F ) ( ( mulGrp ` R ) gsum w ) = ( ( 1st ` ( q ` w ) ) .x. ( 2nd ` ( q ` w ) ) ) ) -> ( R gsum ( w e. Word ( E u. F ) |-> ( ( G ` w ) ( .g ` R ) ( ( mulGrp ` R ) gsum w ) ) ) ) = ( R gsum ( f e. F |-> ( R gsum ( w e. ( `' ( v e. ( G supp 0 ) |-> ( 2nd ` ( q ` v ) ) ) " { f } ) |-> ( ( G ` w ) ( .g ` R ) ( ( mulGrp ` R ) gsum w ) ) ) ) ) ) )
219 11 ad2antrr 
 |-  ( ( ( ph /\ q e. ( ( E X. F ) ^m Word ( E u. F ) ) ) /\ A. w e. Word ( E u. F ) ( ( mulGrp ` R ) gsum w ) = ( ( 1st ` ( q ` w ) ) .x. ( 2nd ` ( q ` w ) ) ) ) -> X = ( R gsum ( w e. Word ( E u. F ) |-> ( ( G ` w ) ( .g ` R ) ( ( mulGrp ` R ) gsum w ) ) ) ) )
220 14 ad4antr 
 |-  ( ( ( ( ( ph /\ q e. ( ( E X. F ) ^m Word ( E u. F ) ) ) /\ A. w e. Word ( E u. F ) ( ( mulGrp ` R ) gsum w ) = ( ( 1st ` ( q ` w ) ) .x. ( 2nd ` ( q ` w ) ) ) ) /\ f e. F ) /\ v e. ( `' q " ( E X. { f } ) ) ) -> R e. Ring )
221 55 ad3antrrr 
 |-  ( ( ( ( ph /\ q e. ( ( E X. F ) ^m Word ( E u. F ) ) ) /\ f e. F ) /\ v e. ( `' q " ( E X. { f } ) ) ) -> E C_ B )
222 32 ad2antrr 
 |-  ( ( ( ( ph /\ q e. ( ( E X. F ) ^m Word ( E u. F ) ) ) /\ f e. F ) /\ v e. ( `' q " ( E X. { f } ) ) ) -> q : Word ( E u. F ) --> ( E X. F ) )
223 139 adantr 
 |-  ( ( ( ph /\ q e. ( ( E X. F ) ^m Word ( E u. F ) ) ) /\ f e. F ) -> ( `' q " ( E X. { f } ) ) C_ Word ( E u. F ) )
224 223 sselda 
 |-  ( ( ( ( ph /\ q e. ( ( E X. F ) ^m Word ( E u. F ) ) ) /\ f e. F ) /\ v e. ( `' q " ( E X. { f } ) ) ) -> v e. Word ( E u. F ) )
225 222 224 ffvelcdmd 
 |-  ( ( ( ( ph /\ q e. ( ( E X. F ) ^m Word ( E u. F ) ) ) /\ f e. F ) /\ v e. ( `' q " ( E X. { f } ) ) ) -> ( q ` v ) e. ( E X. F ) )
226 225 143 syl 
 |-  ( ( ( ( ph /\ q e. ( ( E X. F ) ^m Word ( E u. F ) ) ) /\ f e. F ) /\ v e. ( `' q " ( E X. { f } ) ) ) -> ( 1st ` ( q ` v ) ) e. E )
227 221 226 sseldd 
 |-  ( ( ( ( ph /\ q e. ( ( E X. F ) ^m Word ( E u. F ) ) ) /\ f e. F ) /\ v e. ( `' q " ( E X. { f } ) ) ) -> ( 1st ` ( q ` v ) ) e. B )
228 227 adantllr 
 |-  ( ( ( ( ( ph /\ q e. ( ( E X. F ) ^m Word ( E u. F ) ) ) /\ A. w e. Word ( E u. F ) ( ( mulGrp ` R ) gsum w ) = ( ( 1st ` ( q ` w ) ) .x. ( 2nd ` ( q ` w ) ) ) ) /\ f e. F ) /\ v e. ( `' q " ( E X. { f } ) ) ) -> ( 1st ` ( q ` v ) ) e. B )
229 200 174 syl 
 |-  ( ( ph /\ q e. ( ( E X. F ) ^m Word ( E u. F ) ) ) -> F C_ B )
230 229 sselda 
 |-  ( ( ( ph /\ q e. ( ( E X. F ) ^m Word ( E u. F ) ) ) /\ f e. F ) -> f e. B )
231 230 ad4ant13 
 |-  ( ( ( ( ( ph /\ q e. ( ( E X. F ) ^m Word ( E u. F ) ) ) /\ A. w e. Word ( E u. F ) ( ( mulGrp ` R ) gsum w ) = ( ( 1st ` ( q ` w ) ) .x. ( 2nd ` ( q ` w ) ) ) ) /\ f e. F ) /\ v e. ( `' q " ( E X. { f } ) ) ) -> f e. B )
232 1 24 2 mulgass2 
 |-  ( ( R e. Ring /\ ( ( G ` v ) e. ZZ /\ ( 1st ` ( q ` v ) ) e. B /\ f e. B ) ) -> ( ( ( G ` v ) ( .g ` R ) ( 1st ` ( q ` v ) ) ) .x. f ) = ( ( G ` v ) ( .g ` R ) ( ( 1st ` ( q ` v ) ) .x. f ) ) )
233 220 46 228 231 232 syl13anc 
 |-  ( ( ( ( ( ph /\ q e. ( ( E X. F ) ^m Word ( E u. F ) ) ) /\ A. w e. Word ( E u. F ) ( ( mulGrp ` R ) gsum w ) = ( ( 1st ` ( q ` w ) ) .x. ( 2nd ` ( q ` w ) ) ) ) /\ f e. F ) /\ v e. ( `' q " ( E X. { f } ) ) ) -> ( ( ( G ` v ) ( .g ` R ) ( 1st ` ( q ` v ) ) ) .x. f ) = ( ( G ` v ) ( .g ` R ) ( ( 1st ` ( q ` v ) ) .x. f ) ) )
234 oveq2 
 |-  ( w = v -> ( ( mulGrp ` R ) gsum w ) = ( ( mulGrp ` R ) gsum v ) )
235 2fveq3 
 |-  ( w = v -> ( 1st ` ( q ` w ) ) = ( 1st ` ( q ` v ) ) )
236 2fveq3 
 |-  ( w = v -> ( 2nd ` ( q ` w ) ) = ( 2nd ` ( q ` v ) ) )
237 235 236 oveq12d 
 |-  ( w = v -> ( ( 1st ` ( q ` w ) ) .x. ( 2nd ` ( q ` w ) ) ) = ( ( 1st ` ( q ` v ) ) .x. ( 2nd ` ( q ` v ) ) ) )
238 234 237 eqeq12d 
 |-  ( w = v -> ( ( ( mulGrp ` R ) gsum w ) = ( ( 1st ` ( q ` w ) ) .x. ( 2nd ` ( q ` w ) ) ) <-> ( ( mulGrp ` R ) gsum v ) = ( ( 1st ` ( q ` v ) ) .x. ( 2nd ` ( q ` v ) ) ) ) )
239 simpllr 
 |-  ( ( ( ( ( ph /\ q e. ( ( E X. F ) ^m Word ( E u. F ) ) ) /\ A. w e. Word ( E u. F ) ( ( mulGrp ` R ) gsum w ) = ( ( 1st ` ( q ` w ) ) .x. ( 2nd ` ( q ` w ) ) ) ) /\ f e. F ) /\ v e. ( `' q " ( E X. { f } ) ) ) -> A. w e. Word ( E u. F ) ( ( mulGrp ` R ) gsum w ) = ( ( 1st ` ( q ` w ) ) .x. ( 2nd ` ( q ` w ) ) ) )
240 238 239 45 rspcdva 
 |-  ( ( ( ( ( ph /\ q e. ( ( E X. F ) ^m Word ( E u. F ) ) ) /\ A. w e. Word ( E u. F ) ( ( mulGrp ` R ) gsum w ) = ( ( 1st ` ( q ` w ) ) .x. ( 2nd ` ( q ` w ) ) ) ) /\ f e. F ) /\ v e. ( `' q " ( E X. { f } ) ) ) -> ( ( mulGrp ` R ) gsum v ) = ( ( 1st ` ( q ` v ) ) .x. ( 2nd ` ( q ` v ) ) ) )
241 32 ffnd 
 |-  ( ( ph /\ q e. ( ( E X. F ) ^m Word ( E u. F ) ) ) -> q Fn Word ( E u. F ) )
242 241 ad2antrr 
 |-  ( ( ( ( ph /\ q e. ( ( E X. F ) ^m Word ( E u. F ) ) ) /\ f e. F ) /\ v e. ( `' q " ( E X. { f } ) ) ) -> q Fn Word ( E u. F ) )
243 elpreima 
 |-  ( q Fn Word ( E u. F ) -> ( v e. ( `' q " ( E X. { f } ) ) <-> ( v e. Word ( E u. F ) /\ ( q ` v ) e. ( E X. { f } ) ) ) )
244 243 simplbda 
 |-  ( ( q Fn Word ( E u. F ) /\ v e. ( `' q " ( E X. { f } ) ) ) -> ( q ` v ) e. ( E X. { f } ) )
245 242 244 sylancom 
 |-  ( ( ( ( ph /\ q e. ( ( E X. F ) ^m Word ( E u. F ) ) ) /\ f e. F ) /\ v e. ( `' q " ( E X. { f } ) ) ) -> ( q ` v ) e. ( E X. { f } ) )
246 xp2nd 
 |-  ( ( q ` v ) e. ( E X. { f } ) -> ( 2nd ` ( q ` v ) ) e. { f } )
247 245 246 syl 
 |-  ( ( ( ( ph /\ q e. ( ( E X. F ) ^m Word ( E u. F ) ) ) /\ f e. F ) /\ v e. ( `' q " ( E X. { f } ) ) ) -> ( 2nd ` ( q ` v ) ) e. { f } )
248 247 elsnd 
 |-  ( ( ( ( ph /\ q e. ( ( E X. F ) ^m Word ( E u. F ) ) ) /\ f e. F ) /\ v e. ( `' q " ( E X. { f } ) ) ) -> ( 2nd ` ( q ` v ) ) = f )
249 248 adantllr 
 |-  ( ( ( ( ( ph /\ q e. ( ( E X. F ) ^m Word ( E u. F ) ) ) /\ A. w e. Word ( E u. F ) ( ( mulGrp ` R ) gsum w ) = ( ( 1st ` ( q ` w ) ) .x. ( 2nd ` ( q ` w ) ) ) ) /\ f e. F ) /\ v e. ( `' q " ( E X. { f } ) ) ) -> ( 2nd ` ( q ` v ) ) = f )
250 249 oveq2d 
 |-  ( ( ( ( ( ph /\ q e. ( ( E X. F ) ^m Word ( E u. F ) ) ) /\ A. w e. Word ( E u. F ) ( ( mulGrp ` R ) gsum w ) = ( ( 1st ` ( q ` w ) ) .x. ( 2nd ` ( q ` w ) ) ) ) /\ f e. F ) /\ v e. ( `' q " ( E X. { f } ) ) ) -> ( ( 1st ` ( q ` v ) ) .x. ( 2nd ` ( q ` v ) ) ) = ( ( 1st ` ( q ` v ) ) .x. f ) )
251 240 250 eqtrd 
 |-  ( ( ( ( ( ph /\ q e. ( ( E X. F ) ^m Word ( E u. F ) ) ) /\ A. w e. Word ( E u. F ) ( ( mulGrp ` R ) gsum w ) = ( ( 1st ` ( q ` w ) ) .x. ( 2nd ` ( q ` w ) ) ) ) /\ f e. F ) /\ v e. ( `' q " ( E X. { f } ) ) ) -> ( ( mulGrp ` R ) gsum v ) = ( ( 1st ` ( q ` v ) ) .x. f ) )
252 251 oveq2d 
 |-  ( ( ( ( ( ph /\ q e. ( ( E X. F ) ^m Word ( E u. F ) ) ) /\ A. w e. Word ( E u. F ) ( ( mulGrp ` R ) gsum w ) = ( ( 1st ` ( q ` w ) ) .x. ( 2nd ` ( q ` w ) ) ) ) /\ f e. F ) /\ v e. ( `' q " ( E X. { f } ) ) ) -> ( ( G ` v ) ( .g ` R ) ( ( mulGrp ` R ) gsum v ) ) = ( ( G ` v ) ( .g ` R ) ( ( 1st ` ( q ` v ) ) .x. f ) ) )
253 233 252 eqtr4d 
 |-  ( ( ( ( ( ph /\ q e. ( ( E X. F ) ^m Word ( E u. F ) ) ) /\ A. w e. Word ( E u. F ) ( ( mulGrp ` R ) gsum w ) = ( ( 1st ` ( q ` w ) ) .x. ( 2nd ` ( q ` w ) ) ) ) /\ f e. F ) /\ v e. ( `' q " ( E X. { f } ) ) ) -> ( ( ( G ` v ) ( .g ` R ) ( 1st ` ( q ` v ) ) ) .x. f ) = ( ( G ` v ) ( .g ` R ) ( ( mulGrp ` R ) gsum v ) ) )
254 253 mpteq2dva 
 |-  ( ( ( ( ph /\ q e. ( ( E X. F ) ^m Word ( E u. F ) ) ) /\ A. w e. Word ( E u. F ) ( ( mulGrp ` R ) gsum w ) = ( ( 1st ` ( q ` w ) ) .x. ( 2nd ` ( q ` w ) ) ) ) /\ f e. F ) -> ( v e. ( `' q " ( E X. { f } ) ) |-> ( ( ( G ` v ) ( .g ` R ) ( 1st ` ( q ` v ) ) ) .x. f ) ) = ( v e. ( `' q " ( E X. { f } ) ) |-> ( ( G ` v ) ( .g ` R ) ( ( mulGrp ` R ) gsum v ) ) ) )
255 fveq2 
 |-  ( v = w -> ( G ` v ) = ( G ` w ) )
256 oveq2 
 |-  ( v = w -> ( ( mulGrp ` R ) gsum v ) = ( ( mulGrp ` R ) gsum w ) )
257 255 256 oveq12d 
 |-  ( v = w -> ( ( G ` v ) ( .g ` R ) ( ( mulGrp ` R ) gsum v ) ) = ( ( G ` w ) ( .g ` R ) ( ( mulGrp ` R ) gsum w ) ) )
258 257 cbvmptv 
 |-  ( v e. ( `' q " ( E X. { f } ) ) |-> ( ( G ` v ) ( .g ` R ) ( ( mulGrp ` R ) gsum v ) ) ) = ( w e. ( `' q " ( E X. { f } ) ) |-> ( ( G ` w ) ( .g ` R ) ( ( mulGrp ` R ) gsum w ) ) )
259 254 258 eqtrdi 
 |-  ( ( ( ( ph /\ q e. ( ( E X. F ) ^m Word ( E u. F ) ) ) /\ A. w e. Word ( E u. F ) ( ( mulGrp ` R ) gsum w ) = ( ( 1st ` ( q ` w ) ) .x. ( 2nd ` ( q ` w ) ) ) ) /\ f e. F ) -> ( v e. ( `' q " ( E X. { f } ) ) |-> ( ( ( G ` v ) ( .g ` R ) ( 1st ` ( q ` v ) ) ) .x. f ) ) = ( w e. ( `' q " ( E X. { f } ) ) |-> ( ( G ` w ) ( .g ` R ) ( ( mulGrp ` R ) gsum w ) ) ) )
260 259 oveq2d 
 |-  ( ( ( ( ph /\ q e. ( ( E X. F ) ^m Word ( E u. F ) ) ) /\ A. w e. Word ( E u. F ) ( ( mulGrp ` R ) gsum w ) = ( ( 1st ` ( q ` w ) ) .x. ( 2nd ` ( q ` w ) ) ) ) /\ f e. F ) -> ( R gsum ( v e. ( `' q " ( E X. { f } ) ) |-> ( ( ( G ` v ) ( .g ` R ) ( 1st ` ( q ` v ) ) ) .x. f ) ) ) = ( R gsum ( w e. ( `' q " ( E X. { f } ) ) |-> ( ( G ` w ) ( .g ` R ) ( ( mulGrp ` R ) gsum w ) ) ) ) )
261 14 ad2antrr 
 |-  ( ( ( ph /\ q e. ( ( E X. F ) ^m Word ( E u. F ) ) ) /\ f e. F ) -> R e. Ring )
262 19 a1i 
 |-  ( ( ( ph /\ q e. ( ( E X. F ) ^m Word ( E u. F ) ) ) /\ f e. F ) -> ( `' q " ( E X. { f } ) ) e. _V )
263 25 ad3antrrr 
 |-  ( ( ( ( ph /\ q e. ( ( E X. F ) ^m Word ( E u. F ) ) ) /\ f e. F ) /\ v e. ( `' q " ( E X. { f } ) ) ) -> R e. Grp )
264 191 ad2antrr 
 |-  ( ( ( ( ph /\ q e. ( ( E X. F ) ^m Word ( E u. F ) ) ) /\ f e. F ) /\ v e. ( `' q " ( E X. { f } ) ) ) -> G : Word ( E u. F ) --> ZZ )
265 264 224 ffvelcdmd 
 |-  ( ( ( ( ph /\ q e. ( ( E X. F ) ^m Word ( E u. F ) ) ) /\ f e. F ) /\ v e. ( `' q " ( E X. { f } ) ) ) -> ( G ` v ) e. ZZ )
266 1 24 263 265 227 mulgcld 
 |-  ( ( ( ( ph /\ q e. ( ( E X. F ) ^m Word ( E u. F ) ) ) /\ f e. F ) /\ v e. ( `' q " ( E X. { f } ) ) ) -> ( ( G ` v ) ( .g ` R ) ( 1st ` ( q ` v ) ) ) e. B )
267 50 ad2antrr 
 |-  ( ( ( ph /\ q e. ( ( E X. F ) ^m Word ( E u. F ) ) ) /\ f e. F ) -> ( v e. Word ( E u. F ) |-> ( G ` v ) ) finSupp 0 )
268 0zd 
 |-  ( ( ( ph /\ q e. ( ( E X. F ) ^m Word ( E u. F ) ) ) /\ f e. F ) -> 0 e. ZZ )
269 267 223 268 fmptssfisupp 
 |-  ( ( ( ph /\ q e. ( ( E X. F ) ^m Word ( E u. F ) ) ) /\ f e. F ) -> ( v e. ( `' q " ( E X. { f } ) ) |-> ( G ` v ) ) finSupp 0 )
270 58 adantl 
 |-  ( ( ( ( ph /\ q e. ( ( E X. F ) ^m Word ( E u. F ) ) ) /\ f e. F ) /\ y e. B ) -> ( 0 ( .g ` R ) y ) = .0. )
271 60 a1i 
 |-  ( ( ( ph /\ q e. ( ( E X. F ) ^m Word ( E u. F ) ) ) /\ f e. F ) -> .0. e. _V )
272 269 270 265 227 271 fsuppssov1 
 |-  ( ( ( ph /\ q e. ( ( E X. F ) ^m Word ( E u. F ) ) ) /\ f e. F ) -> ( v e. ( `' q " ( E X. { f } ) ) |-> ( ( G ` v ) ( .g ` R ) ( 1st ` ( q ` v ) ) ) ) finSupp .0. )
273 1 3 2 261 262 230 266 272 gsummulc1 
 |-  ( ( ( ph /\ q e. ( ( E X. F ) ^m Word ( E u. F ) ) ) /\ f e. F ) -> ( R gsum ( v e. ( `' q " ( E X. { f } ) ) |-> ( ( ( G ` v ) ( .g ` R ) ( 1st ` ( q ` v ) ) ) .x. f ) ) ) = ( ( R gsum ( v e. ( `' q " ( E X. { f } ) ) |-> ( ( G ` v ) ( .g ` R ) ( 1st ` ( q ` v ) ) ) ) ) .x. f ) )
274 273 adantlr 
 |-  ( ( ( ( ph /\ q e. ( ( E X. F ) ^m Word ( E u. F ) ) ) /\ A. w e. Word ( E u. F ) ( ( mulGrp ` R ) gsum w ) = ( ( 1st ` ( q ` w ) ) .x. ( 2nd ` ( q ` w ) ) ) ) /\ f e. F ) -> ( R gsum ( v e. ( `' q " ( E X. { f } ) ) |-> ( ( ( G ` v ) ( .g ` R ) ( 1st ` ( q ` v ) ) ) .x. f ) ) ) = ( ( R gsum ( v e. ( `' q " ( E X. { f } ) ) |-> ( ( G ` v ) ( .g ` R ) ( 1st ` ( q ` v ) ) ) ) ) .x. f ) )
275 161 adantr 
 |-  ( ( ( ph /\ q e. ( ( E X. F ) ^m Word ( E u. F ) ) ) /\ f e. F ) -> R e. CMnd )
276 89 ad3antrrr 
 |-  ( ( ( ( ph /\ q e. ( ( E X. F ) ^m Word ( E u. F ) ) ) /\ f e. F ) /\ v e. ( ( `' q " ( E X. { f } ) ) \ ( `' ( u e. ( G supp 0 ) |-> ( 2nd ` ( q ` u ) ) ) " { f } ) ) ) -> G Fn Word ( E u. F ) )
277 162 ad2antrr 
 |-  ( ( ( ( ph /\ q e. ( ( E X. F ) ^m Word ( E u. F ) ) ) /\ f e. F ) /\ v e. ( ( `' q " ( E X. { f } ) ) \ ( `' ( u e. ( G supp 0 ) |-> ( 2nd ` ( q ` u ) ) ) " { f } ) ) ) -> Word ( E u. F ) e. _V )
278 0zd 
 |-  ( ( ( ( ph /\ q e. ( ( E X. F ) ^m Word ( E u. F ) ) ) /\ f e. F ) /\ v e. ( ( `' q " ( E X. { f } ) ) \ ( `' ( u e. ( G supp 0 ) |-> ( 2nd ` ( q ` u ) ) ) " { f } ) ) ) -> 0 e. ZZ )
279 139 ad2antrr 
 |-  ( ( ( ( ph /\ q e. ( ( E X. F ) ^m Word ( E u. F ) ) ) /\ f e. F ) /\ v e. ( ( `' q " ( E X. { f } ) ) \ ( `' ( u e. ( G supp 0 ) |-> ( 2nd ` ( q ` u ) ) ) " { f } ) ) ) -> ( `' q " ( E X. { f } ) ) C_ Word ( E u. F ) )
280 simpr 
 |-  ( ( ( ( ph /\ q e. ( ( E X. F ) ^m Word ( E u. F ) ) ) /\ f e. F ) /\ v e. ( ( `' q " ( E X. { f } ) ) \ ( `' ( u e. ( G supp 0 ) |-> ( 2nd ` ( q ` u ) ) ) " { f } ) ) ) -> v e. ( ( `' q " ( E X. { f } ) ) \ ( `' ( u e. ( G supp 0 ) |-> ( 2nd ` ( q ` u ) ) ) " { f } ) ) )
281 280 eldifad 
 |-  ( ( ( ( ph /\ q e. ( ( E X. F ) ^m Word ( E u. F ) ) ) /\ f e. F ) /\ v e. ( ( `' q " ( E X. { f } ) ) \ ( `' ( u e. ( G supp 0 ) |-> ( 2nd ` ( q ` u ) ) ) " { f } ) ) ) -> v e. ( `' q " ( E X. { f } ) ) )
282 279 281 sseldd 
 |-  ( ( ( ( ph /\ q e. ( ( E X. F ) ^m Word ( E u. F ) ) ) /\ f e. F ) /\ v e. ( ( `' q " ( E X. { f } ) ) \ ( `' ( u e. ( G supp 0 ) |-> ( 2nd ` ( q ` u ) ) ) " { f } ) ) ) -> v e. Word ( E u. F ) )
283 eldif 
 |-  ( v e. ( ( `' q " ( E X. { f } ) ) \ ( `' ( u e. ( G supp 0 ) |-> ( 2nd ` ( q ` u ) ) ) " { f } ) ) <-> ( v e. ( `' q " ( E X. { f } ) ) /\ -. v e. ( `' ( u e. ( G supp 0 ) |-> ( 2nd ` ( q ` u ) ) ) " { f } ) ) )
284 nfv 
 |-  F/ u ( ( ( ph /\ q e. ( ( E X. F ) ^m Word ( E u. F ) ) ) /\ f e. F ) /\ v e. ( G supp 0 ) )
285 fvexd 
 |-  ( ( ( ( ( ph /\ q e. ( ( E X. F ) ^m Word ( E u. F ) ) ) /\ f e. F ) /\ v e. ( G supp 0 ) ) /\ u e. ( G supp 0 ) ) -> ( 2nd ` ( q ` u ) ) e. _V )
286 eqid 
 |-  ( u e. ( G supp 0 ) |-> ( 2nd ` ( q ` u ) ) ) = ( u e. ( G supp 0 ) |-> ( 2nd ` ( q ` u ) ) )
287 284 285 286 fnmptd 
 |-  ( ( ( ( ph /\ q e. ( ( E X. F ) ^m Word ( E u. F ) ) ) /\ f e. F ) /\ v e. ( G supp 0 ) ) -> ( u e. ( G supp 0 ) |-> ( 2nd ` ( q ` u ) ) ) Fn ( G supp 0 ) )
288 287 adantlr 
 |-  ( ( ( ( ( ph /\ q e. ( ( E X. F ) ^m Word ( E u. F ) ) ) /\ f e. F ) /\ v e. ( `' q " ( E X. { f } ) ) ) /\ v e. ( G supp 0 ) ) -> ( u e. ( G supp 0 ) |-> ( 2nd ` ( q ` u ) ) ) Fn ( G supp 0 ) )
289 simpr 
 |-  ( ( ( ( ( ph /\ q e. ( ( E X. F ) ^m Word ( E u. F ) ) ) /\ f e. F ) /\ v e. ( `' q " ( E X. { f } ) ) ) /\ v e. ( G supp 0 ) ) -> v e. ( G supp 0 ) )
290 2fveq3 
 |-  ( u = v -> ( 2nd ` ( q ` u ) ) = ( 2nd ` ( q ` v ) ) )
291 simpr 
 |-  ( ( ( ( ph /\ q e. ( ( E X. F ) ^m Word ( E u. F ) ) ) /\ f e. F ) /\ v e. ( G supp 0 ) ) -> v e. ( G supp 0 ) )
292 fvexd 
 |-  ( ( ( ( ph /\ q e. ( ( E X. F ) ^m Word ( E u. F ) ) ) /\ f e. F ) /\ v e. ( G supp 0 ) ) -> ( 2nd ` ( q ` v ) ) e. _V )
293 286 290 291 292 fvmptd3 
 |-  ( ( ( ( ph /\ q e. ( ( E X. F ) ^m Word ( E u. F ) ) ) /\ f e. F ) /\ v e. ( G supp 0 ) ) -> ( ( u e. ( G supp 0 ) |-> ( 2nd ` ( q ` u ) ) ) ` v ) = ( 2nd ` ( q ` v ) ) )
294 293 adantlr 
 |-  ( ( ( ( ( ph /\ q e. ( ( E X. F ) ^m Word ( E u. F ) ) ) /\ f e. F ) /\ v e. ( `' q " ( E X. { f } ) ) ) /\ v e. ( G supp 0 ) ) -> ( ( u e. ( G supp 0 ) |-> ( 2nd ` ( q ` u ) ) ) ` v ) = ( 2nd ` ( q ` v ) ) )
295 241 ad3antrrr 
 |-  ( ( ( ( ( ph /\ q e. ( ( E X. F ) ^m Word ( E u. F ) ) ) /\ f e. F ) /\ v e. ( `' q " ( E X. { f } ) ) ) /\ v e. ( G supp 0 ) ) -> q Fn Word ( E u. F ) )
296 simplr 
 |-  ( ( ( ( ( ph /\ q e. ( ( E X. F ) ^m Word ( E u. F ) ) ) /\ f e. F ) /\ v e. ( `' q " ( E X. { f } ) ) ) /\ v e. ( G supp 0 ) ) -> v e. ( `' q " ( E X. { f } ) ) )
297 295 296 244 syl2anc 
 |-  ( ( ( ( ( ph /\ q e. ( ( E X. F ) ^m Word ( E u. F ) ) ) /\ f e. F ) /\ v e. ( `' q " ( E X. { f } ) ) ) /\ v e. ( G supp 0 ) ) -> ( q ` v ) e. ( E X. { f } ) )
298 297 246 syl 
 |-  ( ( ( ( ( ph /\ q e. ( ( E X. F ) ^m Word ( E u. F ) ) ) /\ f e. F ) /\ v e. ( `' q " ( E X. { f } ) ) ) /\ v e. ( G supp 0 ) ) -> ( 2nd ` ( q ` v ) ) e. { f } )
299 294 298 eqeltrd 
 |-  ( ( ( ( ( ph /\ q e. ( ( E X. F ) ^m Word ( E u. F ) ) ) /\ f e. F ) /\ v e. ( `' q " ( E X. { f } ) ) ) /\ v e. ( G supp 0 ) ) -> ( ( u e. ( G supp 0 ) |-> ( 2nd ` ( q ` u ) ) ) ` v ) e. { f } )
300 288 289 299 elpreimad 
 |-  ( ( ( ( ( ph /\ q e. ( ( E X. F ) ^m Word ( E u. F ) ) ) /\ f e. F ) /\ v e. ( `' q " ( E X. { f } ) ) ) /\ v e. ( G supp 0 ) ) -> v e. ( `' ( u e. ( G supp 0 ) |-> ( 2nd ` ( q ` u ) ) ) " { f } ) )
301 300 stoic1a 
 |-  ( ( ( ( ( ph /\ q e. ( ( E X. F ) ^m Word ( E u. F ) ) ) /\ f e. F ) /\ v e. ( `' q " ( E X. { f } ) ) ) /\ -. v e. ( `' ( u e. ( G supp 0 ) |-> ( 2nd ` ( q ` u ) ) ) " { f } ) ) -> -. v e. ( G supp 0 ) )
302 301 anasss 
 |-  ( ( ( ( ph /\ q e. ( ( E X. F ) ^m Word ( E u. F ) ) ) /\ f e. F ) /\ ( v e. ( `' q " ( E X. { f } ) ) /\ -. v e. ( `' ( u e. ( G supp 0 ) |-> ( 2nd ` ( q ` u ) ) ) " { f } ) ) ) -> -. v e. ( G supp 0 ) )
303 283 302 sylan2b 
 |-  ( ( ( ( ph /\ q e. ( ( E X. F ) ^m Word ( E u. F ) ) ) /\ f e. F ) /\ v e. ( ( `' q " ( E X. { f } ) ) \ ( `' ( u e. ( G supp 0 ) |-> ( 2nd ` ( q ` u ) ) ) " { f } ) ) ) -> -. v e. ( G supp 0 ) )
304 282 303 eldifd 
 |-  ( ( ( ( ph /\ q e. ( ( E X. F ) ^m Word ( E u. F ) ) ) /\ f e. F ) /\ v e. ( ( `' q " ( E X. { f } ) ) \ ( `' ( u e. ( G supp 0 ) |-> ( 2nd ` ( q ` u ) ) ) " { f } ) ) ) -> v e. ( Word ( E u. F ) \ ( G supp 0 ) ) )
305 276 277 278 304 fvdifsupp 
 |-  ( ( ( ( ph /\ q e. ( ( E X. F ) ^m Word ( E u. F ) ) ) /\ f e. F ) /\ v e. ( ( `' q " ( E X. { f } ) ) \ ( `' ( u e. ( G supp 0 ) |-> ( 2nd ` ( q ` u ) ) ) " { f } ) ) ) -> ( G ` v ) = 0 )
306 305 oveq1d 
 |-  ( ( ( ( ph /\ q e. ( ( E X. F ) ^m Word ( E u. F ) ) ) /\ f e. F ) /\ v e. ( ( `' q " ( E X. { f } ) ) \ ( `' ( u e. ( G supp 0 ) |-> ( 2nd ` ( q ` u ) ) ) " { f } ) ) ) -> ( ( G ` v ) ( .g ` R ) ( ( mulGrp ` R ) gsum v ) ) = ( 0 ( .g ` R ) ( ( mulGrp ` R ) gsum v ) ) )
307 172 ad3antrrr 
 |-  ( ( ( ( ph /\ q e. ( ( E X. F ) ^m Word ( E u. F ) ) ) /\ f e. F ) /\ v e. ( ( `' q " ( E X. { f } ) ) \ ( `' ( u e. ( G supp 0 ) |-> ( 2nd ` ( q ` u ) ) ) " { f } ) ) ) -> ( mulGrp ` R ) e. Mnd )
308 179 adantr 
 |-  ( ( ( ph /\ q e. ( ( E X. F ) ^m Word ( E u. F ) ) ) /\ f e. F ) -> Word ( E u. F ) C_ Word B )
309 223 308 sstrd 
 |-  ( ( ( ph /\ q e. ( ( E X. F ) ^m Word ( E u. F ) ) ) /\ f e. F ) -> ( `' q " ( E X. { f } ) ) C_ Word B )
310 309 ssdifssd 
 |-  ( ( ( ph /\ q e. ( ( E X. F ) ^m Word ( E u. F ) ) ) /\ f e. F ) -> ( ( `' q " ( E X. { f } ) ) \ ( `' ( u e. ( G supp 0 ) |-> ( 2nd ` ( q ` u ) ) ) " { f } ) ) C_ Word B )
311 310 sselda 
 |-  ( ( ( ( ph /\ q e. ( ( E X. F ) ^m Word ( E u. F ) ) ) /\ f e. F ) /\ v e. ( ( `' q " ( E X. { f } ) ) \ ( `' ( u e. ( G supp 0 ) |-> ( 2nd ` ( q ` u ) ) ) " { f } ) ) ) -> v e. Word B )
312 183 gsumwcl 
 |-  ( ( ( mulGrp ` R ) e. Mnd /\ v e. Word B ) -> ( ( mulGrp ` R ) gsum v ) e. B )
313 307 311 312 syl2anc 
 |-  ( ( ( ( ph /\ q e. ( ( E X. F ) ^m Word ( E u. F ) ) ) /\ f e. F ) /\ v e. ( ( `' q " ( E X. { f } ) ) \ ( `' ( u e. ( G supp 0 ) |-> ( 2nd ` ( q ` u ) ) ) " { f } ) ) ) -> ( ( mulGrp ` R ) gsum v ) e. B )
314 1 3 24 mulg0 
 |-  ( ( ( mulGrp ` R ) gsum v ) e. B -> ( 0 ( .g ` R ) ( ( mulGrp ` R ) gsum v ) ) = .0. )
315 313 314 syl 
 |-  ( ( ( ( ph /\ q e. ( ( E X. F ) ^m Word ( E u. F ) ) ) /\ f e. F ) /\ v e. ( ( `' q " ( E X. { f } ) ) \ ( `' ( u e. ( G supp 0 ) |-> ( 2nd ` ( q ` u ) ) ) " { f } ) ) ) -> ( 0 ( .g ` R ) ( ( mulGrp ` R ) gsum v ) ) = .0. )
316 306 315 eqtrd 
 |-  ( ( ( ( ph /\ q e. ( ( E X. F ) ^m Word ( E u. F ) ) ) /\ f e. F ) /\ v e. ( ( `' q " ( E X. { f } ) ) \ ( `' ( u e. ( G supp 0 ) |-> ( 2nd ` ( q ` u ) ) ) " { f } ) ) ) -> ( ( G ` v ) ( .g ` R ) ( ( mulGrp ` R ) gsum v ) ) = .0. )
317 316 ralrimiva 
 |-  ( ( ( ph /\ q e. ( ( E X. F ) ^m Word ( E u. F ) ) ) /\ f e. F ) -> A. v e. ( ( `' q " ( E X. { f } ) ) \ ( `' ( u e. ( G supp 0 ) |-> ( 2nd ` ( q ` u ) ) ) " { f } ) ) ( ( G ` v ) ( .g ` R ) ( ( mulGrp ` R ) gsum v ) ) = .0. )
318 257 eqeq1d 
 |-  ( v = w -> ( ( ( G ` v ) ( .g ` R ) ( ( mulGrp ` R ) gsum v ) ) = .0. <-> ( ( G ` w ) ( .g ` R ) ( ( mulGrp ` R ) gsum w ) ) = .0. ) )
319 318 cbvralvw 
 |-  ( A. v e. ( ( `' q " ( E X. { f } ) ) \ ( `' ( u e. ( G supp 0 ) |-> ( 2nd ` ( q ` u ) ) ) " { f } ) ) ( ( G ` v ) ( .g ` R ) ( ( mulGrp ` R ) gsum v ) ) = .0. <-> A. w e. ( ( `' q " ( E X. { f } ) ) \ ( `' ( u e. ( G supp 0 ) |-> ( 2nd ` ( q ` u ) ) ) " { f } ) ) ( ( G ` w ) ( .g ` R ) ( ( mulGrp ` R ) gsum w ) ) = .0. )
320 2fveq3 
 |-  ( u = w -> ( 2nd ` ( q ` u ) ) = ( 2nd ` ( q ` w ) ) )
321 320 cbvmptv 
 |-  ( u e. ( G supp 0 ) |-> ( 2nd ` ( q ` u ) ) ) = ( w e. ( G supp 0 ) |-> ( 2nd ` ( q ` w ) ) )
322 321 215 eqtr4i 
 |-  ( u e. ( G supp 0 ) |-> ( 2nd ` ( q ` u ) ) ) = ( v e. ( G supp 0 ) |-> ( 2nd ` ( q ` v ) ) )
323 322 cnveqi 
 |-  `' ( u e. ( G supp 0 ) |-> ( 2nd ` ( q ` u ) ) ) = `' ( v e. ( G supp 0 ) |-> ( 2nd ` ( q ` v ) ) )
324 323 imaeq1i 
 |-  ( `' ( u e. ( G supp 0 ) |-> ( 2nd ` ( q ` u ) ) ) " { f } ) = ( `' ( v e. ( G supp 0 ) |-> ( 2nd ` ( q ` v ) ) ) " { f } )
325 324 difeq2i 
 |-  ( ( `' q " ( E X. { f } ) ) \ ( `' ( u e. ( G supp 0 ) |-> ( 2nd ` ( q ` u ) ) ) " { f } ) ) = ( ( `' q " ( E X. { f } ) ) \ ( `' ( v e. ( G supp 0 ) |-> ( 2nd ` ( q ` v ) ) ) " { f } ) )
326 325 raleqi 
 |-  ( A. w e. ( ( `' q " ( E X. { f } ) ) \ ( `' ( u e. ( G supp 0 ) |-> ( 2nd ` ( q ` u ) ) ) " { f } ) ) ( ( G ` w ) ( .g ` R ) ( ( mulGrp ` R ) gsum w ) ) = .0. <-> A. w e. ( ( `' q " ( E X. { f } ) ) \ ( `' ( v e. ( G supp 0 ) |-> ( 2nd ` ( q ` v ) ) ) " { f } ) ) ( ( G ` w ) ( .g ` R ) ( ( mulGrp ` R ) gsum w ) ) = .0. )
327 319 326 bitri 
 |-  ( A. v e. ( ( `' q " ( E X. { f } ) ) \ ( `' ( u e. ( G supp 0 ) |-> ( 2nd ` ( q ` u ) ) ) " { f } ) ) ( ( G ` v ) ( .g ` R ) ( ( mulGrp ` R ) gsum v ) ) = .0. <-> A. w e. ( ( `' q " ( E X. { f } ) ) \ ( `' ( v e. ( G supp 0 ) |-> ( 2nd ` ( q ` v ) ) ) " { f } ) ) ( ( G ` w ) ( .g ` R ) ( ( mulGrp ` R ) gsum w ) ) = .0. )
328 317 327 sylib 
 |-  ( ( ( ph /\ q e. ( ( E X. F ) ^m Word ( E u. F ) ) ) /\ f e. F ) -> A. w e. ( ( `' q " ( E X. { f } ) ) \ ( `' ( v e. ( G supp 0 ) |-> ( 2nd ` ( q ` v ) ) ) " { f } ) ) ( ( G ` w ) ( .g ` R ) ( ( mulGrp ` R ) gsum w ) ) = .0. )
329 328 r19.21bi 
 |-  ( ( ( ( ph /\ q e. ( ( E X. F ) ^m Word ( E u. F ) ) ) /\ f e. F ) /\ w e. ( ( `' q " ( E X. { f } ) ) \ ( `' ( v e. ( G supp 0 ) |-> ( 2nd ` ( q ` v ) ) ) " { f } ) ) ) -> ( ( G ` w ) ( .g ` R ) ( ( mulGrp ` R ) gsum w ) ) = .0. )
330 189 adantr 
 |-  ( ( ( ph /\ q e. ( ( E X. F ) ^m Word ( E u. F ) ) ) /\ f e. F ) -> ( G supp 0 ) e. Fin )
331 330 cnvimamptfin 
 |-  ( ( ( ph /\ q e. ( ( E X. F ) ^m Word ( E u. F ) ) ) /\ f e. F ) -> ( `' ( v e. ( G supp 0 ) |-> ( 2nd ` ( q ` v ) ) ) " { f } ) e. Fin )
332 25 ad3antrrr 
 |-  ( ( ( ( ph /\ q e. ( ( E X. F ) ^m Word ( E u. F ) ) ) /\ f e. F ) /\ w e. ( `' q " ( E X. { f } ) ) ) -> R e. Grp )
333 191 ad2antrr 
 |-  ( ( ( ( ph /\ q e. ( ( E X. F ) ^m Word ( E u. F ) ) ) /\ f e. F ) /\ w e. ( `' q " ( E X. { f } ) ) ) -> G : Word ( E u. F ) --> ZZ )
334 223 sselda 
 |-  ( ( ( ( ph /\ q e. ( ( E X. F ) ^m Word ( E u. F ) ) ) /\ f e. F ) /\ w e. ( `' q " ( E X. { f } ) ) ) -> w e. Word ( E u. F ) )
335 333 334 ffvelcdmd 
 |-  ( ( ( ( ph /\ q e. ( ( E X. F ) ^m Word ( E u. F ) ) ) /\ f e. F ) /\ w e. ( `' q " ( E X. { f } ) ) ) -> ( G ` w ) e. ZZ )
336 172 ad3antrrr 
 |-  ( ( ( ( ph /\ q e. ( ( E X. F ) ^m Word ( E u. F ) ) ) /\ f e. F ) /\ w e. ( `' q " ( E X. { f } ) ) ) -> ( mulGrp ` R ) e. Mnd )
337 309 sselda 
 |-  ( ( ( ( ph /\ q e. ( ( E X. F ) ^m Word ( E u. F ) ) ) /\ f e. F ) /\ w e. ( `' q " ( E X. { f } ) ) ) -> w e. Word B )
338 336 337 184 syl2anc 
 |-  ( ( ( ( ph /\ q e. ( ( E X. F ) ^m Word ( E u. F ) ) ) /\ f e. F ) /\ w e. ( `' q " ( E X. { f } ) ) ) -> ( ( mulGrp ` R ) gsum w ) e. B )
339 1 24 332 335 338 mulgcld 
 |-  ( ( ( ( ph /\ q e. ( ( E X. F ) ^m Word ( E u. F ) ) ) /\ f e. F ) /\ w e. ( `' q " ( E X. { f } ) ) ) -> ( ( G ` w ) ( .g ` R ) ( ( mulGrp ` R ) gsum w ) ) e. B )
340 241 ad2antrr 
 |-  ( ( ( ( ph /\ q e. ( ( E X. F ) ^m Word ( E u. F ) ) ) /\ f e. F ) /\ v e. ( `' ( u e. ( G supp 0 ) |-> ( 2nd ` ( q ` u ) ) ) " { f } ) ) -> q Fn Word ( E u. F ) )
341 198 ad2antrr 
 |-  ( ( ( ( ph /\ q e. ( ( E X. F ) ^m Word ( E u. F ) ) ) /\ f e. F ) /\ v e. ( `' ( u e. ( G supp 0 ) |-> ( 2nd ` ( q ` u ) ) ) " { f } ) ) -> ( G supp 0 ) C_ Word ( E u. F ) )
342 nfv 
 |-  F/ w ( ( ( ph /\ q e. ( ( E X. F ) ^m Word ( E u. F ) ) ) /\ f e. F ) /\ v e. ( `' ( u e. ( G supp 0 ) |-> ( 2nd ` ( q ` u ) ) ) " { f } ) )
343 fvexd 
 |-  ( ( ( ( ( ph /\ q e. ( ( E X. F ) ^m Word ( E u. F ) ) ) /\ f e. F ) /\ v e. ( `' ( u e. ( G supp 0 ) |-> ( 2nd ` ( q ` u ) ) ) " { f } ) ) /\ w e. ( G supp 0 ) ) -> ( 2nd ` ( q ` w ) ) e. _V )
344 342 343 321 fnmptd 
 |-  ( ( ( ( ph /\ q e. ( ( E X. F ) ^m Word ( E u. F ) ) ) /\ f e. F ) /\ v e. ( `' ( u e. ( G supp 0 ) |-> ( 2nd ` ( q ` u ) ) ) " { f } ) ) -> ( u e. ( G supp 0 ) |-> ( 2nd ` ( q ` u ) ) ) Fn ( G supp 0 ) )
345 elpreima 
 |-  ( ( u e. ( G supp 0 ) |-> ( 2nd ` ( q ` u ) ) ) Fn ( G supp 0 ) -> ( v e. ( `' ( u e. ( G supp 0 ) |-> ( 2nd ` ( q ` u ) ) ) " { f } ) <-> ( v e. ( G supp 0 ) /\ ( ( u e. ( G supp 0 ) |-> ( 2nd ` ( q ` u ) ) ) ` v ) e. { f } ) ) )
346 345 simprbda 
 |-  ( ( ( u e. ( G supp 0 ) |-> ( 2nd ` ( q ` u ) ) ) Fn ( G supp 0 ) /\ v e. ( `' ( u e. ( G supp 0 ) |-> ( 2nd ` ( q ` u ) ) ) " { f } ) ) -> v e. ( G supp 0 ) )
347 344 346 sylancom 
 |-  ( ( ( ( ph /\ q e. ( ( E X. F ) ^m Word ( E u. F ) ) ) /\ f e. F ) /\ v e. ( `' ( u e. ( G supp 0 ) |-> ( 2nd ` ( q ` u ) ) ) " { f } ) ) -> v e. ( G supp 0 ) )
348 341 347 sseldd 
 |-  ( ( ( ( ph /\ q e. ( ( E X. F ) ^m Word ( E u. F ) ) ) /\ f e. F ) /\ v e. ( `' ( u e. ( G supp 0 ) |-> ( 2nd ` ( q ` u ) ) ) " { f } ) ) -> v e. Word ( E u. F ) )
349 32 ad2antrr 
 |-  ( ( ( ( ph /\ q e. ( ( E X. F ) ^m Word ( E u. F ) ) ) /\ f e. F ) /\ v e. ( `' ( u e. ( G supp 0 ) |-> ( 2nd ` ( q ` u ) ) ) " { f } ) ) -> q : Word ( E u. F ) --> ( E X. F ) )
350 349 348 ffvelcdmd 
 |-  ( ( ( ( ph /\ q e. ( ( E X. F ) ^m Word ( E u. F ) ) ) /\ f e. F ) /\ v e. ( `' ( u e. ( G supp 0 ) |-> ( 2nd ` ( q ` u ) ) ) " { f } ) ) -> ( q ` v ) e. ( E X. F ) )
351 1st2nd2 
 |-  ( ( q ` v ) e. ( E X. F ) -> ( q ` v ) = <. ( 1st ` ( q ` v ) ) , ( 2nd ` ( q ` v ) ) >. )
352 350 351 syl 
 |-  ( ( ( ( ph /\ q e. ( ( E X. F ) ^m Word ( E u. F ) ) ) /\ f e. F ) /\ v e. ( `' ( u e. ( G supp 0 ) |-> ( 2nd ` ( q ` u ) ) ) " { f } ) ) -> ( q ` v ) = <. ( 1st ` ( q ` v ) ) , ( 2nd ` ( q ` v ) ) >. )
353 350 143 syl 
 |-  ( ( ( ( ph /\ q e. ( ( E X. F ) ^m Word ( E u. F ) ) ) /\ f e. F ) /\ v e. ( `' ( u e. ( G supp 0 ) |-> ( 2nd ` ( q ` u ) ) ) " { f } ) ) -> ( 1st ` ( q ` v ) ) e. E )
354 347 293 syldan 
 |-  ( ( ( ( ph /\ q e. ( ( E X. F ) ^m Word ( E u. F ) ) ) /\ f e. F ) /\ v e. ( `' ( u e. ( G supp 0 ) |-> ( 2nd ` ( q ` u ) ) ) " { f } ) ) -> ( ( u e. ( G supp 0 ) |-> ( 2nd ` ( q ` u ) ) ) ` v ) = ( 2nd ` ( q ` v ) ) )
355 345 simplbda 
 |-  ( ( ( u e. ( G supp 0 ) |-> ( 2nd ` ( q ` u ) ) ) Fn ( G supp 0 ) /\ v e. ( `' ( u e. ( G supp 0 ) |-> ( 2nd ` ( q ` u ) ) ) " { f } ) ) -> ( ( u e. ( G supp 0 ) |-> ( 2nd ` ( q ` u ) ) ) ` v ) e. { f } )
356 344 355 sylancom 
 |-  ( ( ( ( ph /\ q e. ( ( E X. F ) ^m Word ( E u. F ) ) ) /\ f e. F ) /\ v e. ( `' ( u e. ( G supp 0 ) |-> ( 2nd ` ( q ` u ) ) ) " { f } ) ) -> ( ( u e. ( G supp 0 ) |-> ( 2nd ` ( q ` u ) ) ) ` v ) e. { f } )
357 354 356 eqeltrrd 
 |-  ( ( ( ( ph /\ q e. ( ( E X. F ) ^m Word ( E u. F ) ) ) /\ f e. F ) /\ v e. ( `' ( u e. ( G supp 0 ) |-> ( 2nd ` ( q ` u ) ) ) " { f } ) ) -> ( 2nd ` ( q ` v ) ) e. { f } )
358 353 357 opelxpd 
 |-  ( ( ( ( ph /\ q e. ( ( E X. F ) ^m Word ( E u. F ) ) ) /\ f e. F ) /\ v e. ( `' ( u e. ( G supp 0 ) |-> ( 2nd ` ( q ` u ) ) ) " { f } ) ) -> <. ( 1st ` ( q ` v ) ) , ( 2nd ` ( q ` v ) ) >. e. ( E X. { f } ) )
359 352 358 eqeltrd 
 |-  ( ( ( ( ph /\ q e. ( ( E X. F ) ^m Word ( E u. F ) ) ) /\ f e. F ) /\ v e. ( `' ( u e. ( G supp 0 ) |-> ( 2nd ` ( q ` u ) ) ) " { f } ) ) -> ( q ` v ) e. ( E X. { f } ) )
360 340 348 359 elpreimad 
 |-  ( ( ( ( ph /\ q e. ( ( E X. F ) ^m Word ( E u. F ) ) ) /\ f e. F ) /\ v e. ( `' ( u e. ( G supp 0 ) |-> ( 2nd ` ( q ` u ) ) ) " { f } ) ) -> v e. ( `' q " ( E X. { f } ) ) )
361 360 ex 
 |-  ( ( ( ph /\ q e. ( ( E X. F ) ^m Word ( E u. F ) ) ) /\ f e. F ) -> ( v e. ( `' ( u e. ( G supp 0 ) |-> ( 2nd ` ( q ` u ) ) ) " { f } ) -> v e. ( `' q " ( E X. { f } ) ) ) )
362 361 ssrdv 
 |-  ( ( ( ph /\ q e. ( ( E X. F ) ^m Word ( E u. F ) ) ) /\ f e. F ) -> ( `' ( u e. ( G supp 0 ) |-> ( 2nd ` ( q ` u ) ) ) " { f } ) C_ ( `' q " ( E X. { f } ) ) )
363 324 362 eqsstrrid 
 |-  ( ( ( ph /\ q e. ( ( E X. F ) ^m Word ( E u. F ) ) ) /\ f e. F ) -> ( `' ( v e. ( G supp 0 ) |-> ( 2nd ` ( q ` v ) ) ) " { f } ) C_ ( `' q " ( E X. { f } ) ) )
364 1 3 275 262 329 331 339 363 gsummptres2 
 |-  ( ( ( ph /\ q e. ( ( E X. F ) ^m Word ( E u. F ) ) ) /\ f e. F ) -> ( R gsum ( w e. ( `' q " ( E X. { f } ) ) |-> ( ( G ` w ) ( .g ` R ) ( ( mulGrp ` R ) gsum w ) ) ) ) = ( R gsum ( w e. ( `' ( v e. ( G supp 0 ) |-> ( 2nd ` ( q ` v ) ) ) " { f } ) |-> ( ( G ` w ) ( .g ` R ) ( ( mulGrp ` R ) gsum w ) ) ) ) )
365 364 adantlr 
 |-  ( ( ( ( ph /\ q e. ( ( E X. F ) ^m Word ( E u. F ) ) ) /\ A. w e. Word ( E u. F ) ( ( mulGrp ` R ) gsum w ) = ( ( 1st ` ( q ` w ) ) .x. ( 2nd ` ( q ` w ) ) ) ) /\ f e. F ) -> ( R gsum ( w e. ( `' q " ( E X. { f } ) ) |-> ( ( G ` w ) ( .g ` R ) ( ( mulGrp ` R ) gsum w ) ) ) ) = ( R gsum ( w e. ( `' ( v e. ( G supp 0 ) |-> ( 2nd ` ( q ` v ) ) ) " { f } ) |-> ( ( G ` w ) ( .g ` R ) ( ( mulGrp ` R ) gsum w ) ) ) ) )
366 260 274 365 3eqtr3d 
 |-  ( ( ( ( ph /\ q e. ( ( E X. F ) ^m Word ( E u. F ) ) ) /\ A. w e. Word ( E u. F ) ( ( mulGrp ` R ) gsum w ) = ( ( 1st ` ( q ` w ) ) .x. ( 2nd ` ( q ` w ) ) ) ) /\ f e. F ) -> ( ( R gsum ( v e. ( `' q " ( E X. { f } ) ) |-> ( ( G ` v ) ( .g ` R ) ( 1st ` ( q ` v ) ) ) ) ) .x. f ) = ( R gsum ( w e. ( `' ( v e. ( G supp 0 ) |-> ( 2nd ` ( q ` v ) ) ) " { f } ) |-> ( ( G ` w ) ( .g ` R ) ( ( mulGrp ` R ) gsum w ) ) ) ) )
367 366 mpteq2dva 
 |-  ( ( ( ph /\ q e. ( ( E X. F ) ^m Word ( E u. F ) ) ) /\ A. w e. Word ( E u. F ) ( ( mulGrp ` R ) gsum w ) = ( ( 1st ` ( q ` w ) ) .x. ( 2nd ` ( q ` w ) ) ) ) -> ( f e. F |-> ( ( R gsum ( v e. ( `' q " ( E X. { f } ) ) |-> ( ( G ` v ) ( .g ` R ) ( 1st ` ( q ` v ) ) ) ) ) .x. f ) ) = ( f e. F |-> ( R gsum ( w e. ( `' ( v e. ( G supp 0 ) |-> ( 2nd ` ( q ` v ) ) ) " { f } ) |-> ( ( G ` w ) ( .g ` R ) ( ( mulGrp ` R ) gsum w ) ) ) ) ) )
368 367 oveq2d 
 |-  ( ( ( ph /\ q e. ( ( E X. F ) ^m Word ( E u. F ) ) ) /\ A. w e. Word ( E u. F ) ( ( mulGrp ` R ) gsum w ) = ( ( 1st ` ( q ` w ) ) .x. ( 2nd ` ( q ` w ) ) ) ) -> ( R gsum ( f e. F |-> ( ( R gsum ( v e. ( `' q " ( E X. { f } ) ) |-> ( ( G ` v ) ( .g ` R ) ( 1st ` ( q ` v ) ) ) ) ) .x. f ) ) ) = ( R gsum ( f e. F |-> ( R gsum ( w e. ( `' ( v e. ( G supp 0 ) |-> ( 2nd ` ( q ` v ) ) ) " { f } ) |-> ( ( G ` w ) ( .g ` R ) ( ( mulGrp ` R ) gsum w ) ) ) ) ) ) )
369 218 219 368 3eqtr4d 
 |-  ( ( ( ph /\ q e. ( ( E X. F ) ^m Word ( E u. F ) ) ) /\ A. w e. Word ( E u. F ) ( ( mulGrp ` R ) gsum w ) = ( ( 1st ` ( q ` w ) ) .x. ( 2nd ` ( q ` w ) ) ) ) -> X = ( R gsum ( f e. F |-> ( ( R gsum ( v e. ( `' q " ( E X. { f } ) ) |-> ( ( G ` v ) ( .g ` R ) ( 1st ` ( q ` v ) ) ) ) ) .x. f ) ) ) )
370 159 369 jca 
 |-  ( ( ( ph /\ q e. ( ( E X. F ) ^m Word ( E u. F ) ) ) /\ A. w e. Word ( E u. F ) ( ( mulGrp ` R ) gsum w ) = ( ( 1st ` ( q ` w ) ) .x. ( 2nd ` ( q ` w ) ) ) ) -> ( ( f e. F |-> ( R gsum ( v e. ( `' q " ( E X. { f } ) ) |-> ( ( G ` v ) ( .g ` R ) ( 1st ` ( q ` v ) ) ) ) ) ) finSupp .0. /\ X = ( R gsum ( f e. F |-> ( ( R gsum ( v e. ( `' q " ( E X. { f } ) ) |-> ( ( G ` v ) ( .g ` R ) ( 1st ` ( q ` v ) ) ) ) ) .x. f ) ) ) ) )
371 65 79 370 rspcedvd 
 |-  ( ( ( ph /\ q e. ( ( E X. F ) ^m Word ( E u. F ) ) ) /\ A. w e. Word ( E u. F ) ( ( mulGrp ` R ) gsum w ) = ( ( 1st ` ( q ` w ) ) .x. ( 2nd ` ( q ` w ) ) ) ) -> E. p e. ( E ^m F ) ( p finSupp .0. /\ X = ( R gsum ( f e. F |-> ( ( p ` f ) .x. f ) ) ) ) )
372 fveq2 
 |-  ( a = ( q ` w ) -> ( 1st ` a ) = ( 1st ` ( q ` w ) ) )
373 fveq2 
 |-  ( a = ( q ` w ) -> ( 2nd ` a ) = ( 2nd ` ( q ` w ) ) )
374 372 373 oveq12d 
 |-  ( a = ( q ` w ) -> ( ( 1st ` a ) .x. ( 2nd ` a ) ) = ( ( 1st ` ( q ` w ) ) .x. ( 2nd ` ( q ` w ) ) ) )
375 374 eqeq2d 
 |-  ( a = ( q ` w ) -> ( ( ( mulGrp ` R ) gsum w ) = ( ( 1st ` a ) .x. ( 2nd ` a ) ) <-> ( ( mulGrp ` R ) gsum w ) = ( ( 1st ` ( q ` w ) ) .x. ( 2nd ` ( q ` w ) ) ) ) )
376 vex 
 |-  e e. _V
377 vex 
 |-  f e. _V
378 376 377 op1std 
 |-  ( a = <. e , f >. -> ( 1st ` a ) = e )
379 376 377 op2ndd 
 |-  ( a = <. e , f >. -> ( 2nd ` a ) = f )
380 378 379 oveq12d 
 |-  ( a = <. e , f >. -> ( ( 1st ` a ) .x. ( 2nd ` a ) ) = ( e .x. f ) )
381 380 eqeq2d 
 |-  ( a = <. e , f >. -> ( ( ( mulGrp ` R ) gsum w ) = ( ( 1st ` a ) .x. ( 2nd ` a ) ) <-> ( ( mulGrp ` R ) gsum w ) = ( e .x. f ) ) )
382 simpllr 
 |-  ( ( ( ( ( ph /\ w e. Word ( E u. F ) ) /\ e e. E ) /\ f e. F ) /\ ( ( mulGrp ` R ) gsum w ) = ( e .x. f ) ) -> e e. E )
383 simplr 
 |-  ( ( ( ( ( ph /\ w e. Word ( E u. F ) ) /\ e e. E ) /\ f e. F ) /\ ( ( mulGrp ` R ) gsum w ) = ( e .x. f ) ) -> f e. F )
384 382 383 opelxpd 
 |-  ( ( ( ( ( ph /\ w e. Word ( E u. F ) ) /\ e e. E ) /\ f e. F ) /\ ( ( mulGrp ` R ) gsum w ) = ( e .x. f ) ) -> <. e , f >. e. ( E X. F ) )
385 simpr 
 |-  ( ( ( ( ( ph /\ w e. Word ( E u. F ) ) /\ e e. E ) /\ f e. F ) /\ ( ( mulGrp ` R ) gsum w ) = ( e .x. f ) ) -> ( ( mulGrp ` R ) gsum w ) = ( e .x. f ) )
386 381 384 385 rspcedvdw 
 |-  ( ( ( ( ( ph /\ w e. Word ( E u. F ) ) /\ e e. E ) /\ f e. F ) /\ ( ( mulGrp ` R ) gsum w ) = ( e .x. f ) ) -> E. a e. ( E X. F ) ( ( mulGrp ` R ) gsum w ) = ( ( 1st ` a ) .x. ( 2nd ` a ) ) )
387 169 2 mgpplusg 
 |-  .x. = ( +g ` ( mulGrp ` R ) )
388 171 adantr 
 |-  ( ( ph /\ w e. Word ( E u. F ) ) -> ( mulGrp ` R ) e. CMnd )
389 169 subrgsubm 
 |-  ( E e. ( SubRing ` R ) -> E e. ( SubMnd ` ( mulGrp ` R ) ) )
390 6 389 syl 
 |-  ( ph -> E e. ( SubMnd ` ( mulGrp ` R ) ) )
391 390 adantr 
 |-  ( ( ph /\ w e. Word ( E u. F ) ) -> E e. ( SubMnd ` ( mulGrp ` R ) ) )
392 169 subrgsubm 
 |-  ( F e. ( SubRing ` R ) -> F e. ( SubMnd ` ( mulGrp ` R ) ) )
393 7 392 syl 
 |-  ( ph -> F e. ( SubMnd ` ( mulGrp ` R ) ) )
394 393 adantr 
 |-  ( ( ph /\ w e. Word ( E u. F ) ) -> F e. ( SubMnd ` ( mulGrp ` R ) ) )
395 simpr 
 |-  ( ( ph /\ w e. Word ( E u. F ) ) -> w e. Word ( E u. F ) )
396 387 388 391 394 395 gsumwun 
 |-  ( ( ph /\ w e. Word ( E u. F ) ) -> E. e e. E E. f e. F ( ( mulGrp ` R ) gsum w ) = ( e .x. f ) )
397 386 396 r19.29vva 
 |-  ( ( ph /\ w e. Word ( E u. F ) ) -> E. a e. ( E X. F ) ( ( mulGrp ` R ) gsum w ) = ( ( 1st ` a ) .x. ( 2nd ` a ) ) )
398 375 30 27 397 ac6mapd 
 |-  ( ph -> E. q e. ( ( E X. F ) ^m Word ( E u. F ) ) A. w e. Word ( E u. F ) ( ( mulGrp ` R ) gsum w ) = ( ( 1st ` ( q ` w ) ) .x. ( 2nd ` ( q ` w ) ) ) )
399 371 398 r19.29a 
 |-  ( ph -> E. p e. ( E ^m F ) ( p finSupp .0. /\ X = ( R gsum ( f e. F |-> ( ( p ` f ) .x. f ) ) ) ) )