Metamath Proof Explorer

Theorem ablfac2

Description: Choose generators for each cyclic group in ablfac . (Contributed by Mario Carneiro, 28-Apr-2016)

Ref Expression
Hypotheses ablfac.b 
|- B = ( Base ` G )
ablfac.c 
|- C = { r e. ( SubGrp ` G ) | ( G |`s r ) e. ( CycGrp i^i ran pGrp ) }
ablfac.1 
|- ( ph -> G e. Abel )
ablfac.2 
|- ( ph -> B e. Fin )
ablfac2.m 
|- .x. = ( .g ` G )
ablfac2.s 
|- S = ( k e. dom w |-> ran ( n e. ZZ |-> ( n .x. ( w ` k ) ) ) )
Assertion ablfac2 
|- ( ph -> E. w e. Word B ( S : dom w --> C /\ G dom DProd S /\ ( G DProd S ) = B ) )

Proof

Step Hyp Ref Expression
1 ablfac.b 
 |-  B = ( Base ` G )
2 ablfac.c 
 |-  C = { r e. ( SubGrp ` G ) | ( G |`s r ) e. ( CycGrp i^i ran pGrp ) }
3 ablfac.1 
 |-  ( ph -> G e. Abel )
4 ablfac.2 
 |-  ( ph -> B e. Fin )
5 ablfac2.m 
 |-  .x. = ( .g ` G )
6 ablfac2.s 
 |-  S = ( k e. dom w |-> ran ( n e. ZZ |-> ( n .x. ( w ` k ) ) ) )
7 wrdf 
 |-  ( s e. Word C -> s : ( 0 ..^ ( # ` s ) ) --> C )
8 7 ad2antlr 
 |-  ( ( ( ph /\ s e. Word C ) /\ ( G dom DProd s /\ ( G DProd s ) = B ) ) -> s : ( 0 ..^ ( # ` s ) ) --> C )
9 8 fdmd 
 |-  ( ( ( ph /\ s e. Word C ) /\ ( G dom DProd s /\ ( G DProd s ) = B ) ) -> dom s = ( 0 ..^ ( # ` s ) ) )
10 fzofi 
 |-  ( 0 ..^ ( # ` s ) ) e. Fin
11 9 10 eqeltrdi 
 |-  ( ( ( ph /\ s e. Word C ) /\ ( G dom DProd s /\ ( G DProd s ) = B ) ) -> dom s e. Fin )
12 8 ffdmd 
 |-  ( ( ( ph /\ s e. Word C ) /\ ( G dom DProd s /\ ( G DProd s ) = B ) ) -> s : dom s --> C )
13 12 ffvelrnda 
 |-  ( ( ( ( ph /\ s e. Word C ) /\ ( G dom DProd s /\ ( G DProd s ) = B ) ) /\ k e. dom s ) -> ( s ` k ) e. C )
14 oveq2 
 |-  ( r = ( s ` k ) -> ( G |`s r ) = ( G |`s ( s ` k ) ) )
15 14 eleq1d 
 |-  ( r = ( s ` k ) -> ( ( G |`s r ) e. ( CycGrp i^i ran pGrp ) <-> ( G |`s ( s ` k ) ) e. ( CycGrp i^i ran pGrp ) ) )
16 15 2 elrab2 
 |-  ( ( s ` k ) e. C <-> ( ( s ` k ) e. ( SubGrp ` G ) /\ ( G |`s ( s ` k ) ) e. ( CycGrp i^i ran pGrp ) ) )
17 16 simplbi 
 |-  ( ( s ` k ) e. C -> ( s ` k ) e. ( SubGrp ` G ) )
18 13 17 syl 
 |-  ( ( ( ( ph /\ s e. Word C ) /\ ( G dom DProd s /\ ( G DProd s ) = B ) ) /\ k e. dom s ) -> ( s ` k ) e. ( SubGrp ` G ) )
19 1 subgss 
 |-  ( ( s ` k ) e. ( SubGrp ` G ) -> ( s ` k ) C_ B )
20 18 19 syl 
 |-  ( ( ( ( ph /\ s e. Word C ) /\ ( G dom DProd s /\ ( G DProd s ) = B ) ) /\ k e. dom s ) -> ( s ` k ) C_ B )
21 16 simprbi 
 |-  ( ( s ` k ) e. C -> ( G |`s ( s ` k ) ) e. ( CycGrp i^i ran pGrp ) )
22 13 21 syl 
 |-  ( ( ( ( ph /\ s e. Word C ) /\ ( G dom DProd s /\ ( G DProd s ) = B ) ) /\ k e. dom s ) -> ( G |`s ( s ` k ) ) e. ( CycGrp i^i ran pGrp ) )
23 22 elin1d 
 |-  ( ( ( ( ph /\ s e. Word C ) /\ ( G dom DProd s /\ ( G DProd s ) = B ) ) /\ k e. dom s ) -> ( G |`s ( s ` k ) ) e. CycGrp )
24 eqid 
 |-  ( Base ` ( G |`s ( s ` k ) ) ) = ( Base ` ( G |`s ( s ` k ) ) )
25 eqid 
 |-  ( .g ` ( G |`s ( s ` k ) ) ) = ( .g ` ( G |`s ( s ` k ) ) )
26 24 25 iscyg 
 |-  ( ( G |`s ( s ` k ) ) e. CycGrp <-> ( ( G |`s ( s ` k ) ) e. Grp /\ E. x e. ( Base ` ( G |`s ( s ` k ) ) ) ran ( n e. ZZ |-> ( n ( .g ` ( G |`s ( s ` k ) ) ) x ) ) = ( Base ` ( G |`s ( s ` k ) ) ) ) )
27 26 simprbi 
 |-  ( ( G |`s ( s ` k ) ) e. CycGrp -> E. x e. ( Base ` ( G |`s ( s ` k ) ) ) ran ( n e. ZZ |-> ( n ( .g ` ( G |`s ( s ` k ) ) ) x ) ) = ( Base ` ( G |`s ( s ` k ) ) ) )
28 23 27 syl 
 |-  ( ( ( ( ph /\ s e. Word C ) /\ ( G dom DProd s /\ ( G DProd s ) = B ) ) /\ k e. dom s ) -> E. x e. ( Base ` ( G |`s ( s ` k ) ) ) ran ( n e. ZZ |-> ( n ( .g ` ( G |`s ( s ` k ) ) ) x ) ) = ( Base ` ( G |`s ( s ` k ) ) ) )
29 eqid 
 |-  ( G |`s ( s ` k ) ) = ( G |`s ( s ` k ) )
30 29 subgbas 
 |-  ( ( s ` k ) e. ( SubGrp ` G ) -> ( s ` k ) = ( Base ` ( G |`s ( s ` k ) ) ) )
31 18 30 syl 
 |-  ( ( ( ( ph /\ s e. Word C ) /\ ( G dom DProd s /\ ( G DProd s ) = B ) ) /\ k e. dom s ) -> ( s ` k ) = ( Base ` ( G |`s ( s ` k ) ) ) )
32 31 rexeqdv 
 |-  ( ( ( ( ph /\ s e. Word C ) /\ ( G dom DProd s /\ ( G DProd s ) = B ) ) /\ k e. dom s ) -> ( E. x e. ( s ` k ) ran ( n e. ZZ |-> ( n ( .g ` ( G |`s ( s ` k ) ) ) x ) ) = ( Base ` ( G |`s ( s ` k ) ) ) <-> E. x e. ( Base ` ( G |`s ( s ` k ) ) ) ran ( n e. ZZ |-> ( n ( .g ` ( G |`s ( s ` k ) ) ) x ) ) = ( Base ` ( G |`s ( s ` k ) ) ) ) )
33 28 32 mpbird 
 |-  ( ( ( ( ph /\ s e. Word C ) /\ ( G dom DProd s /\ ( G DProd s ) = B ) ) /\ k e. dom s ) -> E. x e. ( s ` k ) ran ( n e. ZZ |-> ( n ( .g ` ( G |`s ( s ` k ) ) ) x ) ) = ( Base ` ( G |`s ( s ` k ) ) ) )
34 18 ad2antrr 
 |-  ( ( ( ( ( ( ph /\ s e. Word C ) /\ ( G dom DProd s /\ ( G DProd s ) = B ) ) /\ k e. dom s ) /\ x e. ( s ` k ) ) /\ n e. ZZ ) -> ( s ` k ) e. ( SubGrp ` G ) )
35 simpr 
 |-  ( ( ( ( ( ( ph /\ s e. Word C ) /\ ( G dom DProd s /\ ( G DProd s ) = B ) ) /\ k e. dom s ) /\ x e. ( s ` k ) ) /\ n e. ZZ ) -> n e. ZZ )
36 simplr 
 |-  ( ( ( ( ( ( ph /\ s e. Word C ) /\ ( G dom DProd s /\ ( G DProd s ) = B ) ) /\ k e. dom s ) /\ x e. ( s ` k ) ) /\ n e. ZZ ) -> x e. ( s ` k ) )
37 5 29 25 subgmulg 
 |-  ( ( ( s ` k ) e. ( SubGrp ` G ) /\ n e. ZZ /\ x e. ( s ` k ) ) -> ( n .x. x ) = ( n ( .g ` ( G |`s ( s ` k ) ) ) x ) )
38 34 35 36 37 syl3anc 
 |-  ( ( ( ( ( ( ph /\ s e. Word C ) /\ ( G dom DProd s /\ ( G DProd s ) = B ) ) /\ k e. dom s ) /\ x e. ( s ` k ) ) /\ n e. ZZ ) -> ( n .x. x ) = ( n ( .g ` ( G |`s ( s ` k ) ) ) x ) )
39 38 mpteq2dva 
 |-  ( ( ( ( ( ph /\ s e. Word C ) /\ ( G dom DProd s /\ ( G DProd s ) = B ) ) /\ k e. dom s ) /\ x e. ( s ` k ) ) -> ( n e. ZZ |-> ( n .x. x ) ) = ( n e. ZZ |-> ( n ( .g ` ( G |`s ( s ` k ) ) ) x ) ) )
40 39 rneqd 
 |-  ( ( ( ( ( ph /\ s e. Word C ) /\ ( G dom DProd s /\ ( G DProd s ) = B ) ) /\ k e. dom s ) /\ x e. ( s ` k ) ) -> ran ( n e. ZZ |-> ( n .x. x ) ) = ran ( n e. ZZ |-> ( n ( .g ` ( G |`s ( s ` k ) ) ) x ) ) )
41 31 adantr 
 |-  ( ( ( ( ( ph /\ s e. Word C ) /\ ( G dom DProd s /\ ( G DProd s ) = B ) ) /\ k e. dom s ) /\ x e. ( s ` k ) ) -> ( s ` k ) = ( Base ` ( G |`s ( s ` k ) ) ) )
42 40 41 eqeq12d 
 |-  ( ( ( ( ( ph /\ s e. Word C ) /\ ( G dom DProd s /\ ( G DProd s ) = B ) ) /\ k e. dom s ) /\ x e. ( s ` k ) ) -> ( ran ( n e. ZZ |-> ( n .x. x ) ) = ( s ` k ) <-> ran ( n e. ZZ |-> ( n ( .g ` ( G |`s ( s ` k ) ) ) x ) ) = ( Base ` ( G |`s ( s ` k ) ) ) ) )
43 42 rexbidva 
 |-  ( ( ( ( ph /\ s e. Word C ) /\ ( G dom DProd s /\ ( G DProd s ) = B ) ) /\ k e. dom s ) -> ( E. x e. ( s ` k ) ran ( n e. ZZ |-> ( n .x. x ) ) = ( s ` k ) <-> E. x e. ( s ` k ) ran ( n e. ZZ |-> ( n ( .g ` ( G |`s ( s ` k ) ) ) x ) ) = ( Base ` ( G |`s ( s ` k ) ) ) ) )
44 33 43 mpbird 
 |-  ( ( ( ( ph /\ s e. Word C ) /\ ( G dom DProd s /\ ( G DProd s ) = B ) ) /\ k e. dom s ) -> E. x e. ( s ` k ) ran ( n e. ZZ |-> ( n .x. x ) ) = ( s ` k ) )
45 ssrexv 
 |-  ( ( s ` k ) C_ B -> ( E. x e. ( s ` k ) ran ( n e. ZZ |-> ( n .x. x ) ) = ( s ` k ) -> E. x e. B ran ( n e. ZZ |-> ( n .x. x ) ) = ( s ` k ) ) )
46 20 44 45 sylc 
 |-  ( ( ( ( ph /\ s e. Word C ) /\ ( G dom DProd s /\ ( G DProd s ) = B ) ) /\ k e. dom s ) -> E. x e. B ran ( n e. ZZ |-> ( n .x. x ) ) = ( s ` k ) )
47 46 ralrimiva 
 |-  ( ( ( ph /\ s e. Word C ) /\ ( G dom DProd s /\ ( G DProd s ) = B ) ) -> A. k e. dom s E. x e. B ran ( n e. ZZ |-> ( n .x. x ) ) = ( s ` k ) )
48 oveq2 
 |-  ( x = ( w ` k ) -> ( n .x. x ) = ( n .x. ( w ` k ) ) )
49 48 mpteq2dv 
 |-  ( x = ( w ` k ) -> ( n e. ZZ |-> ( n .x. x ) ) = ( n e. ZZ |-> ( n .x. ( w ` k ) ) ) )
50 49 rneqd 
 |-  ( x = ( w ` k ) -> ran ( n e. ZZ |-> ( n .x. x ) ) = ran ( n e. ZZ |-> ( n .x. ( w ` k ) ) ) )
51 50 eqeq1d 
 |-  ( x = ( w ` k ) -> ( ran ( n e. ZZ |-> ( n .x. x ) ) = ( s ` k ) <-> ran ( n e. ZZ |-> ( n .x. ( w ` k ) ) ) = ( s ` k ) ) )
52 51 ac6sfi 
 |-  ( ( dom s e. Fin /\ A. k e. dom s E. x e. B ran ( n e. ZZ |-> ( n .x. x ) ) = ( s ` k ) ) -> E. w ( w : dom s --> B /\ A. k e. dom s ran ( n e. ZZ |-> ( n .x. ( w ` k ) ) ) = ( s ` k ) ) )
53 11 47 52 syl2anc 
 |-  ( ( ( ph /\ s e. Word C ) /\ ( G dom DProd s /\ ( G DProd s ) = B ) ) -> E. w ( w : dom s --> B /\ A. k e. dom s ran ( n e. ZZ |-> ( n .x. ( w ` k ) ) ) = ( s ` k ) ) )
54 simprl 
 |-  ( ( ( ( ph /\ s e. Word C ) /\ ( G dom DProd s /\ ( G DProd s ) = B ) ) /\ ( w : dom s --> B /\ A. k e. dom s ran ( n e. ZZ |-> ( n .x. ( w ` k ) ) ) = ( s ` k ) ) ) -> w : dom s --> B )
55 9 adantr 
 |-  ( ( ( ( ph /\ s e. Word C ) /\ ( G dom DProd s /\ ( G DProd s ) = B ) ) /\ ( w : dom s --> B /\ A. k e. dom s ran ( n e. ZZ |-> ( n .x. ( w ` k ) ) ) = ( s ` k ) ) ) -> dom s = ( 0 ..^ ( # ` s ) ) )
56 55 feq2d 
 |-  ( ( ( ( ph /\ s e. Word C ) /\ ( G dom DProd s /\ ( G DProd s ) = B ) ) /\ ( w : dom s --> B /\ A. k e. dom s ran ( n e. ZZ |-> ( n .x. ( w ` k ) ) ) = ( s ` k ) ) ) -> ( w : dom s --> B <-> w : ( 0 ..^ ( # ` s ) ) --> B ) )
57 54 56 mpbid 
 |-  ( ( ( ( ph /\ s e. Word C ) /\ ( G dom DProd s /\ ( G DProd s ) = B ) ) /\ ( w : dom s --> B /\ A. k e. dom s ran ( n e. ZZ |-> ( n .x. ( w ` k ) ) ) = ( s ` k ) ) ) -> w : ( 0 ..^ ( # ` s ) ) --> B )
58 iswrdi 
 |-  ( w : ( 0 ..^ ( # ` s ) ) --> B -> w e. Word B )
59 57 58 syl 
 |-  ( ( ( ( ph /\ s e. Word C ) /\ ( G dom DProd s /\ ( G DProd s ) = B ) ) /\ ( w : dom s --> B /\ A. k e. dom s ran ( n e. ZZ |-> ( n .x. ( w ` k ) ) ) = ( s ` k ) ) ) -> w e. Word B )
60 54 fdmd 
 |-  ( ( ( ( ph /\ s e. Word C ) /\ ( G dom DProd s /\ ( G DProd s ) = B ) ) /\ ( w : dom s --> B /\ A. k e. dom s ran ( n e. ZZ |-> ( n .x. ( w ` k ) ) ) = ( s ` k ) ) ) -> dom w = dom s )
61 60 eleq2d 
 |-  ( ( ( ( ph /\ s e. Word C ) /\ ( G dom DProd s /\ ( G DProd s ) = B ) ) /\ ( w : dom s --> B /\ A. k e. dom s ran ( n e. ZZ |-> ( n .x. ( w ` k ) ) ) = ( s ` k ) ) ) -> ( j e. dom w <-> j e. dom s ) )
62 61 biimpa 
 |-  ( ( ( ( ( ph /\ s e. Word C ) /\ ( G dom DProd s /\ ( G DProd s ) = B ) ) /\ ( w : dom s --> B /\ A. k e. dom s ran ( n e. ZZ |-> ( n .x. ( w ` k ) ) ) = ( s ` k ) ) ) /\ j e. dom w ) -> j e. dom s )
63 simprr 
 |-  ( ( ( ( ph /\ s e. Word C ) /\ ( G dom DProd s /\ ( G DProd s ) = B ) ) /\ ( w : dom s --> B /\ A. k e. dom s ran ( n e. ZZ |-> ( n .x. ( w ` k ) ) ) = ( s ` k ) ) ) -> A. k e. dom s ran ( n e. ZZ |-> ( n .x. ( w ` k ) ) ) = ( s ` k ) )
64 simpl 
 |-  ( ( k = j /\ n e. ZZ ) -> k = j )
65 64 fveq2d 
 |-  ( ( k = j /\ n e. ZZ ) -> ( w ` k ) = ( w ` j ) )
66 65 oveq2d 
 |-  ( ( k = j /\ n e. ZZ ) -> ( n .x. ( w ` k ) ) = ( n .x. ( w ` j ) ) )
67 66 mpteq2dva 
 |-  ( k = j -> ( n e. ZZ |-> ( n .x. ( w ` k ) ) ) = ( n e. ZZ |-> ( n .x. ( w ` j ) ) ) )
68 67 rneqd 
 |-  ( k = j -> ran ( n e. ZZ |-> ( n .x. ( w ` k ) ) ) = ran ( n e. ZZ |-> ( n .x. ( w ` j ) ) ) )
69 fveq2 
 |-  ( k = j -> ( s ` k ) = ( s ` j ) )
70 68 69 eqeq12d 
 |-  ( k = j -> ( ran ( n e. ZZ |-> ( n .x. ( w ` k ) ) ) = ( s ` k ) <-> ran ( n e. ZZ |-> ( n .x. ( w ` j ) ) ) = ( s ` j ) ) )
71 70 rspccva 
 |-  ( ( A. k e. dom s ran ( n e. ZZ |-> ( n .x. ( w ` k ) ) ) = ( s ` k ) /\ j e. dom s ) -> ran ( n e. ZZ |-> ( n .x. ( w ` j ) ) ) = ( s ` j ) )
72 63 71 sylan 
 |-  ( ( ( ( ( ph /\ s e. Word C ) /\ ( G dom DProd s /\ ( G DProd s ) = B ) ) /\ ( w : dom s --> B /\ A. k e. dom s ran ( n e. ZZ |-> ( n .x. ( w ` k ) ) ) = ( s ` k ) ) ) /\ j e. dom s ) -> ran ( n e. ZZ |-> ( n .x. ( w ` j ) ) ) = ( s ` j ) )
73 12 adantr 
 |-  ( ( ( ( ph /\ s e. Word C ) /\ ( G dom DProd s /\ ( G DProd s ) = B ) ) /\ ( w : dom s --> B /\ A. k e. dom s ran ( n e. ZZ |-> ( n .x. ( w ` k ) ) ) = ( s ` k ) ) ) -> s : dom s --> C )
74 73 ffvelrnda 
 |-  ( ( ( ( ( ph /\ s e. Word C ) /\ ( G dom DProd s /\ ( G DProd s ) = B ) ) /\ ( w : dom s --> B /\ A. k e. dom s ran ( n e. ZZ |-> ( n .x. ( w ` k ) ) ) = ( s ` k ) ) ) /\ j e. dom s ) -> ( s ` j ) e. C )
75 72 74 eqeltrd 
 |-  ( ( ( ( ( ph /\ s e. Word C ) /\ ( G dom DProd s /\ ( G DProd s ) = B ) ) /\ ( w : dom s --> B /\ A. k e. dom s ran ( n e. ZZ |-> ( n .x. ( w ` k ) ) ) = ( s ` k ) ) ) /\ j e. dom s ) -> ran ( n e. ZZ |-> ( n .x. ( w ` j ) ) ) e. C )
76 62 75 syldan 
 |-  ( ( ( ( ( ph /\ s e. Word C ) /\ ( G dom DProd s /\ ( G DProd s ) = B ) ) /\ ( w : dom s --> B /\ A. k e. dom s ran ( n e. ZZ |-> ( n .x. ( w ` k ) ) ) = ( s ` k ) ) ) /\ j e. dom w ) -> ran ( n e. ZZ |-> ( n .x. ( w ` j ) ) ) e. C )
77 fveq2 
 |-  ( k = j -> ( w ` k ) = ( w ` j ) )
78 77 oveq2d 
 |-  ( k = j -> ( n .x. ( w ` k ) ) = ( n .x. ( w ` j ) ) )
79 78 mpteq2dv 
 |-  ( k = j -> ( n e. ZZ |-> ( n .x. ( w ` k ) ) ) = ( n e. ZZ |-> ( n .x. ( w ` j ) ) ) )
80 79 rneqd 
 |-  ( k = j -> ran ( n e. ZZ |-> ( n .x. ( w ` k ) ) ) = ran ( n e. ZZ |-> ( n .x. ( w ` j ) ) ) )
81 80 cbvmptv 
 |-  ( k e. dom w |-> ran ( n e. ZZ |-> ( n .x. ( w ` k ) ) ) ) = ( j e. dom w |-> ran ( n e. ZZ |-> ( n .x. ( w ` j ) ) ) )
82 6 81 eqtri 
 |-  S = ( j e. dom w |-> ran ( n e. ZZ |-> ( n .x. ( w ` j ) ) ) )
83 76 82 fmptd 
 |-  ( ( ( ( ph /\ s e. Word C ) /\ ( G dom DProd s /\ ( G DProd s ) = B ) ) /\ ( w : dom s --> B /\ A. k e. dom s ran ( n e. ZZ |-> ( n .x. ( w ` k ) ) ) = ( s ` k ) ) ) -> S : dom w --> C )
84 simprl 
 |-  ( ( ( ph /\ s e. Word C ) /\ ( G dom DProd s /\ ( G DProd s ) = B ) ) -> G dom DProd s )
85 84 adantr 
 |-  ( ( ( ( ph /\ s e. Word C ) /\ ( G dom DProd s /\ ( G DProd s ) = B ) ) /\ ( w : dom s --> B /\ A. k e. dom s ran ( n e. ZZ |-> ( n .x. ( w ` k ) ) ) = ( s ` k ) ) ) -> G dom DProd s )
86 60 raleqdv 
 |-  ( ( ( ( ph /\ s e. Word C ) /\ ( G dom DProd s /\ ( G DProd s ) = B ) ) /\ ( w : dom s --> B /\ A. k e. dom s ran ( n e. ZZ |-> ( n .x. ( w ` k ) ) ) = ( s ` k ) ) ) -> ( A. k e. dom w ran ( n e. ZZ |-> ( n .x. ( w ` k ) ) ) = ( s ` k ) <-> A. k e. dom s ran ( n e. ZZ |-> ( n .x. ( w ` k ) ) ) = ( s ` k ) ) )
87 63 86 mpbird 
 |-  ( ( ( ( ph /\ s e. Word C ) /\ ( G dom DProd s /\ ( G DProd s ) = B ) ) /\ ( w : dom s --> B /\ A. k e. dom s ran ( n e. ZZ |-> ( n .x. ( w ` k ) ) ) = ( s ` k ) ) ) -> A. k e. dom w ran ( n e. ZZ |-> ( n .x. ( w ` k ) ) ) = ( s ` k ) )
88 mpteq12 
 |-  ( ( dom w = dom s /\ A. k e. dom w ran ( n e. ZZ |-> ( n .x. ( w ` k ) ) ) = ( s ` k ) ) -> ( k e. dom w |-> ran ( n e. ZZ |-> ( n .x. ( w ` k ) ) ) ) = ( k e. dom s |-> ( s ` k ) ) )
89 60 87 88 syl2anc 
 |-  ( ( ( ( ph /\ s e. Word C ) /\ ( G dom DProd s /\ ( G DProd s ) = B ) ) /\ ( w : dom s --> B /\ A. k e. dom s ran ( n e. ZZ |-> ( n .x. ( w ` k ) ) ) = ( s ` k ) ) ) -> ( k e. dom w |-> ran ( n e. ZZ |-> ( n .x. ( w ` k ) ) ) ) = ( k e. dom s |-> ( s ` k ) ) )
90 6 89 eqtrid 
 |-  ( ( ( ( ph /\ s e. Word C ) /\ ( G dom DProd s /\ ( G DProd s ) = B ) ) /\ ( w : dom s --> B /\ A. k e. dom s ran ( n e. ZZ |-> ( n .x. ( w ` k ) ) ) = ( s ` k ) ) ) -> S = ( k e. dom s |-> ( s ` k ) ) )
91 dprdf 
 |-  ( G dom DProd s -> s : dom s --> ( SubGrp ` G ) )
92 85 91 syl 
 |-  ( ( ( ( ph /\ s e. Word C ) /\ ( G dom DProd s /\ ( G DProd s ) = B ) ) /\ ( w : dom s --> B /\ A. k e. dom s ran ( n e. ZZ |-> ( n .x. ( w ` k ) ) ) = ( s ` k ) ) ) -> s : dom s --> ( SubGrp ` G ) )
93 92 feqmptd 
 |-  ( ( ( ( ph /\ s e. Word C ) /\ ( G dom DProd s /\ ( G DProd s ) = B ) ) /\ ( w : dom s --> B /\ A. k e. dom s ran ( n e. ZZ |-> ( n .x. ( w ` k ) ) ) = ( s ` k ) ) ) -> s = ( k e. dom s |-> ( s ` k ) ) )
94 90 93 eqtr4d 
 |-  ( ( ( ( ph /\ s e. Word C ) /\ ( G dom DProd s /\ ( G DProd s ) = B ) ) /\ ( w : dom s --> B /\ A. k e. dom s ran ( n e. ZZ |-> ( n .x. ( w ` k ) ) ) = ( s ` k ) ) ) -> S = s )
95 85 94 breqtrrd 
 |-  ( ( ( ( ph /\ s e. Word C ) /\ ( G dom DProd s /\ ( G DProd s ) = B ) ) /\ ( w : dom s --> B /\ A. k e. dom s ran ( n e. ZZ |-> ( n .x. ( w ` k ) ) ) = ( s ` k ) ) ) -> G dom DProd S )
96 94 oveq2d 
 |-  ( ( ( ( ph /\ s e. Word C ) /\ ( G dom DProd s /\ ( G DProd s ) = B ) ) /\ ( w : dom s --> B /\ A. k e. dom s ran ( n e. ZZ |-> ( n .x. ( w ` k ) ) ) = ( s ` k ) ) ) -> ( G DProd S ) = ( G DProd s ) )
97 simplrr 
 |-  ( ( ( ( ph /\ s e. Word C ) /\ ( G dom DProd s /\ ( G DProd s ) = B ) ) /\ ( w : dom s --> B /\ A. k e. dom s ran ( n e. ZZ |-> ( n .x. ( w ` k ) ) ) = ( s ` k ) ) ) -> ( G DProd s ) = B )
98 96 97 eqtrd 
 |-  ( ( ( ( ph /\ s e. Word C ) /\ ( G dom DProd s /\ ( G DProd s ) = B ) ) /\ ( w : dom s --> B /\ A. k e. dom s ran ( n e. ZZ |-> ( n .x. ( w ` k ) ) ) = ( s ` k ) ) ) -> ( G DProd S ) = B )
99 83 95 98 3jca 
 |-  ( ( ( ( ph /\ s e. Word C ) /\ ( G dom DProd s /\ ( G DProd s ) = B ) ) /\ ( w : dom s --> B /\ A. k e. dom s ran ( n e. ZZ |-> ( n .x. ( w ` k ) ) ) = ( s ` k ) ) ) -> ( S : dom w --> C /\ G dom DProd S /\ ( G DProd S ) = B ) )
100 59 99 jca 
 |-  ( ( ( ( ph /\ s e. Word C ) /\ ( G dom DProd s /\ ( G DProd s ) = B ) ) /\ ( w : dom s --> B /\ A. k e. dom s ran ( n e. ZZ |-> ( n .x. ( w ` k ) ) ) = ( s ` k ) ) ) -> ( w e. Word B /\ ( S : dom w --> C /\ G dom DProd S /\ ( G DProd S ) = B ) ) )
101 100 ex 
 |-  ( ( ( ph /\ s e. Word C ) /\ ( G dom DProd s /\ ( G DProd s ) = B ) ) -> ( ( w : dom s --> B /\ A. k e. dom s ran ( n e. ZZ |-> ( n .x. ( w ` k ) ) ) = ( s ` k ) ) -> ( w e. Word B /\ ( S : dom w --> C /\ G dom DProd S /\ ( G DProd S ) = B ) ) ) )
102 101 eximdv 
 |-  ( ( ( ph /\ s e. Word C ) /\ ( G dom DProd s /\ ( G DProd s ) = B ) ) -> ( E. w ( w : dom s --> B /\ A. k e. dom s ran ( n e. ZZ |-> ( n .x. ( w ` k ) ) ) = ( s ` k ) ) -> E. w ( w e. Word B /\ ( S : dom w --> C /\ G dom DProd S /\ ( G DProd S ) = B ) ) ) )
103 53 102 mpd 
 |-  ( ( ( ph /\ s e. Word C ) /\ ( G dom DProd s /\ ( G DProd s ) = B ) ) -> E. w ( w e. Word B /\ ( S : dom w --> C /\ G dom DProd S /\ ( G DProd S ) = B ) ) )
104 df-rex 
 |-  ( E. w e. Word B ( S : dom w --> C /\ G dom DProd S /\ ( G DProd S ) = B ) <-> E. w ( w e. Word B /\ ( S : dom w --> C /\ G dom DProd S /\ ( G DProd S ) = B ) ) )
105 103 104 sylibr 
 |-  ( ( ( ph /\ s e. Word C ) /\ ( G dom DProd s /\ ( G DProd s ) = B ) ) -> E. w e. Word B ( S : dom w --> C /\ G dom DProd S /\ ( G DProd S ) = B ) )
106 1 2 3 4 ablfac 
 |-  ( ph -> E. s e. Word C ( G dom DProd s /\ ( G DProd s ) = B ) )
107 105 106 r19.29a 
 |-  ( ph -> E. w e. Word B ( S : dom w --> C /\ G dom DProd S /\ ( G DProd S ) = B ) )