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 ffvelcdmda 
 |-  ( ( ( ( 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 28 31 rexeqtrrdv 
 |-  ( ( ( ( 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 ) ) ) )
33 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 ) )
34 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 )
35 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 ) )
36 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 ) )
37 33 34 35 36 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 ) )
38 37 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 ) ) )
39 38 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 ) ) )
40 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 ) ) ) )
41 39 40 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 ) ) ) ) )
42 41 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 ) ) ) ) )
43 32 42 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 ) )
44 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 ) ) )
45 20 43 44 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 ) )
46 45 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 ) )
47 oveq2 
 |-  ( x = ( w ` k ) -> ( n .x. x ) = ( n .x. ( w ` k ) ) )
48 47 mpteq2dv 
 |-  ( x = ( w ` k ) -> ( n e. ZZ |-> ( n .x. x ) ) = ( n e. ZZ |-> ( n .x. ( w ` k ) ) ) )
49 48 rneqd 
 |-  ( x = ( w ` k ) -> ran ( n e. ZZ |-> ( n .x. x ) ) = ran ( n e. ZZ |-> ( n .x. ( w ` k ) ) ) )
50 49 eqeq1d 
 |-  ( x = ( w ` k ) -> ( ran ( n e. ZZ |-> ( n .x. x ) ) = ( s ` k ) <-> ran ( n e. ZZ |-> ( n .x. ( w ` k ) ) ) = ( s ` k ) ) )
51 50 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 ) ) )
52 11 46 51 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 ) ) )
53 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 )
54 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 ) ) )
55 54 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 ) )
56 53 55 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 )
57 iswrdi 
 |-  ( w : ( 0 ..^ ( # ` s ) ) --> B -> w e. Word B )
58 56 57 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 )
59 53 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 )
60 59 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 ) )
61 60 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 )
62 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 ) )
63 simpl 
 |-  ( ( k = j /\ n e. ZZ ) -> k = j )
64 63 fveq2d 
 |-  ( ( k = j /\ n e. ZZ ) -> ( w ` k ) = ( w ` j ) )
65 64 oveq2d 
 |-  ( ( k = j /\ n e. ZZ ) -> ( n .x. ( w ` k ) ) = ( n .x. ( w ` j ) ) )
66 65 mpteq2dva 
 |-  ( k = j -> ( n e. ZZ |-> ( n .x. ( w ` k ) ) ) = ( n e. ZZ |-> ( n .x. ( w ` j ) ) ) )
67 66 rneqd 
 |-  ( k = j -> ran ( n e. ZZ |-> ( n .x. ( w ` k ) ) ) = ran ( n e. ZZ |-> ( n .x. ( w ` j ) ) ) )
68 fveq2 
 |-  ( k = j -> ( s ` k ) = ( s ` j ) )
69 67 68 eqeq12d 
 |-  ( k = j -> ( ran ( n e. ZZ |-> ( n .x. ( w ` k ) ) ) = ( s ` k ) <-> ran ( n e. ZZ |-> ( n .x. ( w ` j ) ) ) = ( s ` j ) ) )
70 69 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 ) )
71 62 70 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 ) )
72 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 )
73 72 ffvelcdmda 
 |-  ( ( ( ( ( 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 )
74 71 73 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 )
75 61 74 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 )
76 fveq2 
 |-  ( k = j -> ( w ` k ) = ( w ` j ) )
77 76 oveq2d 
 |-  ( k = j -> ( n .x. ( w ` k ) ) = ( n .x. ( w ` j ) ) )
78 77 mpteq2dv 
 |-  ( k = j -> ( n e. ZZ |-> ( n .x. ( w ` k ) ) ) = ( n e. ZZ |-> ( n .x. ( w ` j ) ) ) )
79 78 rneqd 
 |-  ( k = j -> ran ( n e. ZZ |-> ( n .x. ( w ` k ) ) ) = ran ( n e. ZZ |-> ( n .x. ( w ` j ) ) ) )
80 79 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 ) ) ) )
81 6 80 eqtri 
 |-  S = ( j e. dom w |-> ran ( n e. ZZ |-> ( n .x. ( w ` j ) ) ) )
82 75 81 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 )
83 simprl 
 |-  ( ( ( ph /\ s e. Word C ) /\ ( G dom DProd s /\ ( G DProd s ) = B ) ) -> G dom DProd s )
84 83 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 )
85 62 59 raleqtrrdv 
 |-  ( ( ( ( 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 ) )
86 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 ) ) )
87 59 85 86 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 ) ) )
88 6 87 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 ) ) )
89 dprdf 
 |-  ( G dom DProd s -> s : dom s --> ( SubGrp ` G ) )
90 84 89 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 ) )
91 90 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 ) ) )
92 88 91 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 )
93 84 92 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 )
94 92 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 ) )
95 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 )
96 94 95 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 )
97 82 93 96 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 ) )
98 58 97 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 ) ) )
99 98 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 ) ) ) )
100 99 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 ) ) ) )
101 52 100 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 ) ) )
102 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 ) ) )
103 101 102 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 ) )
104 1 2 3 4 ablfac 
 |-  ( ph -> E. s e. Word C ( G dom DProd s /\ ( G DProd s ) = B ) )
105 103 104 r19.29a 
 |-  ( ph -> E. w e. Word B ( S : dom w --> C /\ G dom DProd S /\ ( G DProd S ) = B ) )