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

Metamath Proof Explorer

Theorem ablfaclem3

Description: Lemma for ablfac . (Contributed by Mario Carneiro, 27-Apr-2016) (Revised by Mario Carneiro, 3-May-2016)

Ref Expression
Hypotheses ablfac.b ⊢ 𝐵 = ( Base ‘ 𝐺 )
ablfac.c ⊢ 𝐶 = { 𝑟 ∈ ( SubGrp ‘ 𝐺 ) ∣ ( 𝐺 ↾s 𝑟 ) ∈ ( CycGrp ∩ ran pGrp ) }
ablfac.1 ⊢ ( 𝜑 → 𝐺 ∈ Abel )
ablfac.2 ⊢ ( 𝜑 → 𝐵 ∈ Fin )
ablfac.o ⊢ 𝑂 = ( od ‘ 𝐺 )
ablfac.a ⊢ 𝐴 = { 𝑤 ∈ ℙ ∣ 𝑤 ∥ ( ♯ ‘ 𝐵 ) }
ablfac.s ⊢ 𝑆 = ( 𝑝 ∈ 𝐴 ↦ { 𝑥 ∈ 𝐵 ∣ ( 𝑂 ‘ 𝑥 ) ∥ ( 𝑝 ↑ ( 𝑝 pCnt ( ♯ ‘ 𝐵 ) ) ) } )
ablfac.w ⊢ 𝑊 = ( 𝑔 ∈ ( SubGrp ‘ 𝐺 ) ↦ { 𝑠 ∈ Word 𝐶 ∣ ( 𝐺 dom DProd 𝑠 ∧ ( 𝐺 DProd 𝑠 ) = 𝑔 ) } )
Assertion ablfaclem3 ( 𝜑 → ( 𝑊 ‘ 𝐵 ) ≠ ∅ )

Proof

Step Hyp Ref Expression
1 ablfac.b ⊢ 𝐵 = ( Base ‘ 𝐺 )
2 ablfac.c ⊢ 𝐶 = { 𝑟 ∈ ( SubGrp ‘ 𝐺 ) ∣ ( 𝐺 ↾s 𝑟 ) ∈ ( CycGrp ∩ ran pGrp ) }
3 ablfac.1 ⊢ ( 𝜑 → 𝐺 ∈ Abel )
4 ablfac.2 ⊢ ( 𝜑 → 𝐵 ∈ Fin )
5 ablfac.o ⊢ 𝑂 = ( od ‘ 𝐺 )
6 ablfac.a ⊢ 𝐴 = { 𝑤 ∈ ℙ ∣ 𝑤 ∥ ( ♯ ‘ 𝐵 ) }
7 ablfac.s ⊢ 𝑆 = ( 𝑝 ∈ 𝐴 ↦ { 𝑥 ∈ 𝐵 ∣ ( 𝑂 ‘ 𝑥 ) ∥ ( 𝑝 ↑ ( 𝑝 pCnt ( ♯ ‘ 𝐵 ) ) ) } )
8 ablfac.w ⊢ 𝑊 = ( 𝑔 ∈ ( SubGrp ‘ 𝐺 ) ↦ { 𝑠 ∈ Word 𝐶 ∣ ( 𝐺 dom DProd 𝑠 ∧ ( 𝐺 DProd 𝑠 ) = 𝑔 ) } )
9 fzfid ⊢ ( 𝜑 → ( 1 ... ( ♯ ‘ 𝐵 ) ) ∈ Fin )
10 prmnn ⊢ ( 𝑤 ∈ ℙ → 𝑤 ∈ ℕ )
11 10 3ad2ant2 ⊢ ( ( 𝜑 ∧ 𝑤 ∈ ℙ ∧ 𝑤 ∥ ( ♯ ‘ 𝐵 ) ) → 𝑤 ∈ ℕ )
12 prmz ⊢ ( 𝑤 ∈ ℙ → 𝑤 ∈ ℤ )
13 ablgrp ⊢ ( 𝐺 ∈ Abel → 𝐺 ∈ Grp )
14 1 grpbn0 ⊢ ( 𝐺 ∈ Grp → 𝐵 ≠ ∅ )
15 3 13 14 3syl ⊢ ( 𝜑 → 𝐵 ≠ ∅ )
16 hashnncl ⊢ ( 𝐵 ∈ Fin → ( ( ♯ ‘ 𝐵 ) ∈ ℕ ↔ 𝐵 ≠ ∅ ) )
17 4 16 syl ⊢ ( 𝜑 → ( ( ♯ ‘ 𝐵 ) ∈ ℕ ↔ 𝐵 ≠ ∅ ) )
18 15 17 mpbird ⊢ ( 𝜑 → ( ♯ ‘ 𝐵 ) ∈ ℕ )
19 dvdsle ⊢ ( ( 𝑤 ∈ ℤ ∧ ( ♯ ‘ 𝐵 ) ∈ ℕ ) → ( 𝑤 ∥ ( ♯ ‘ 𝐵 ) → 𝑤 ≤ ( ♯ ‘ 𝐵 ) ) )
20 12 18 19 syl2anr ⊢ ( ( 𝜑 ∧ 𝑤 ∈ ℙ ) → ( 𝑤 ∥ ( ♯ ‘ 𝐵 ) → 𝑤 ≤ ( ♯ ‘ 𝐵 ) ) )
21 20 3impia ⊢ ( ( 𝜑 ∧ 𝑤 ∈ ℙ ∧ 𝑤 ∥ ( ♯ ‘ 𝐵 ) ) → 𝑤 ≤ ( ♯ ‘ 𝐵 ) )
22 18 nnzd ⊢ ( 𝜑 → ( ♯ ‘ 𝐵 ) ∈ ℤ )
23 22 3ad2ant1 ⊢ ( ( 𝜑 ∧ 𝑤 ∈ ℙ ∧ 𝑤 ∥ ( ♯ ‘ 𝐵 ) ) → ( ♯ ‘ 𝐵 ) ∈ ℤ )
24 fznn ⊢ ( ( ♯ ‘ 𝐵 ) ∈ ℤ → ( 𝑤 ∈ ( 1 ... ( ♯ ‘ 𝐵 ) ) ↔ ( 𝑤 ∈ ℕ ∧ 𝑤 ≤ ( ♯ ‘ 𝐵 ) ) ) )
25 23 24 syl ⊢ ( ( 𝜑 ∧ 𝑤 ∈ ℙ ∧ 𝑤 ∥ ( ♯ ‘ 𝐵 ) ) → ( 𝑤 ∈ ( 1 ... ( ♯ ‘ 𝐵 ) ) ↔ ( 𝑤 ∈ ℕ ∧ 𝑤 ≤ ( ♯ ‘ 𝐵 ) ) ) )
26 11 21 25 mpbir2and ⊢ ( ( 𝜑 ∧ 𝑤 ∈ ℙ ∧ 𝑤 ∥ ( ♯ ‘ 𝐵 ) ) → 𝑤 ∈ ( 1 ... ( ♯ ‘ 𝐵 ) ) )
27 26 rabssdv ⊢ ( 𝜑 → { 𝑤 ∈ ℙ ∣ 𝑤 ∥ ( ♯ ‘ 𝐵 ) } ⊆ ( 1 ... ( ♯ ‘ 𝐵 ) ) )
28 6 27 eqsstrid ⊢ ( 𝜑 → 𝐴 ⊆ ( 1 ... ( ♯ ‘ 𝐵 ) ) )
29 9 28 ssfid ⊢ ( 𝜑 → 𝐴 ∈ Fin )
30 dfin5 ⊢ ( Word 𝐶 ∩ ( 𝑊 ‘ ( 𝑆 ‘ 𝑞 ) ) ) = { 𝑦 ∈ Word 𝐶 ∣ 𝑦 ∈ ( 𝑊 ‘ ( 𝑆 ‘ 𝑞 ) ) }
31 6 ssrab3 ⊢ 𝐴 ⊆ ℙ
32 31 a1i ⊢ ( 𝜑 → 𝐴 ⊆ ℙ )
33 1 5 7 3 4 32 ablfac1b ⊢ ( 𝜑 → 𝐺 dom DProd 𝑆 )
34 1 fvexi ⊢ 𝐵 ∈ V
35 34 rabex ⊢ { 𝑥 ∈ 𝐵 ∣ ( 𝑂 ‘ 𝑥 ) ∥ ( 𝑝 ↑ ( 𝑝 pCnt ( ♯ ‘ 𝐵 ) ) ) } ∈ V
36 35 7 dmmpti ⊢ dom 𝑆 = 𝐴
37 36 a1i ⊢ ( 𝜑 → dom 𝑆 = 𝐴 )
38 33 37 dprdf2 ⊢ ( 𝜑 → 𝑆 : 𝐴 ⟶ ( SubGrp ‘ 𝐺 ) )
39 38 ffvelcdmda ⊢ ( ( 𝜑 ∧ 𝑞 ∈ 𝐴 ) → ( 𝑆 ‘ 𝑞 ) ∈ ( SubGrp ‘ 𝐺 ) )
40 1 2 3 4 5 6 7 8 ablfaclem1 ⊢ ( ( 𝑆 ‘ 𝑞 ) ∈ ( SubGrp ‘ 𝐺 ) → ( 𝑊 ‘ ( 𝑆 ‘ 𝑞 ) ) = { 𝑠 ∈ Word 𝐶 ∣ ( 𝐺 dom DProd 𝑠 ∧ ( 𝐺 DProd 𝑠 ) = ( 𝑆 ‘ 𝑞 ) ) } )
41 39 40 syl ⊢ ( ( 𝜑 ∧ 𝑞 ∈ 𝐴 ) → ( 𝑊 ‘ ( 𝑆 ‘ 𝑞 ) ) = { 𝑠 ∈ Word 𝐶 ∣ ( 𝐺 dom DProd 𝑠 ∧ ( 𝐺 DProd 𝑠 ) = ( 𝑆 ‘ 𝑞 ) ) } )
42 ssrab2 ⊢ { 𝑠 ∈ Word 𝐶 ∣ ( 𝐺 dom DProd 𝑠 ∧ ( 𝐺 DProd 𝑠 ) = ( 𝑆 ‘ 𝑞 ) ) } ⊆ Word 𝐶
43 41 42 eqsstrdi ⊢ ( ( 𝜑 ∧ 𝑞 ∈ 𝐴 ) → ( 𝑊 ‘ ( 𝑆 ‘ 𝑞 ) ) ⊆ Word 𝐶 )
44 sseqin2 ⊢ ( ( 𝑊 ‘ ( 𝑆 ‘ 𝑞 ) ) ⊆ Word 𝐶 ↔ ( Word 𝐶 ∩ ( 𝑊 ‘ ( 𝑆 ‘ 𝑞 ) ) ) = ( 𝑊 ‘ ( 𝑆 ‘ 𝑞 ) ) )
45 43 44 sylib ⊢ ( ( 𝜑 ∧ 𝑞 ∈ 𝐴 ) → ( Word 𝐶 ∩ ( 𝑊 ‘ ( 𝑆 ‘ 𝑞 ) ) ) = ( 𝑊 ‘ ( 𝑆 ‘ 𝑞 ) ) )
46 30 45 eqtr3id ⊢ ( ( 𝜑 ∧ 𝑞 ∈ 𝐴 ) → { 𝑦 ∈ Word 𝐶 ∣ 𝑦 ∈ ( 𝑊 ‘ ( 𝑆 ‘ 𝑞 ) ) } = ( 𝑊 ‘ ( 𝑆 ‘ 𝑞 ) ) )
47 46 41 eqtrd ⊢ ( ( 𝜑 ∧ 𝑞 ∈ 𝐴 ) → { 𝑦 ∈ Word 𝐶 ∣ 𝑦 ∈ ( 𝑊 ‘ ( 𝑆 ‘ 𝑞 ) ) } = { 𝑠 ∈ Word 𝐶 ∣ ( 𝐺 dom DProd 𝑠 ∧ ( 𝐺 DProd 𝑠 ) = ( 𝑆 ‘ 𝑞 ) ) } )
48 eqid ⊢ ( Base ‘ ( 𝐺 ↾s ( 𝑆 ‘ 𝑞 ) ) ) = ( Base ‘ ( 𝐺 ↾s ( 𝑆 ‘ 𝑞 ) ) )
49 eqid ⊢ { 𝑟 ∈ ( SubGrp ‘ ( 𝐺 ↾s ( 𝑆 ‘ 𝑞 ) ) ) ∣ ( ( 𝐺 ↾s ( 𝑆 ‘ 𝑞 ) ) ↾s 𝑟 ) ∈ ( CycGrp ∩ ran pGrp ) } = { 𝑟 ∈ ( SubGrp ‘ ( 𝐺 ↾s ( 𝑆 ‘ 𝑞 ) ) ) ∣ ( ( 𝐺 ↾s ( 𝑆 ‘ 𝑞 ) ) ↾s 𝑟 ) ∈ ( CycGrp ∩ ran pGrp ) }
50 eqid ⊢ ( 𝐺 ↾s ( 𝑆 ‘ 𝑞 ) ) = ( 𝐺 ↾s ( 𝑆 ‘ 𝑞 ) )
51 50 subgabl ⊢ ( ( 𝐺 ∈ Abel ∧ ( 𝑆 ‘ 𝑞 ) ∈ ( SubGrp ‘ 𝐺 ) ) → ( 𝐺 ↾s ( 𝑆 ‘ 𝑞 ) ) ∈ Abel )
52 3 39 51 syl2an2r ⊢ ( ( 𝜑 ∧ 𝑞 ∈ 𝐴 ) → ( 𝐺 ↾s ( 𝑆 ‘ 𝑞 ) ) ∈ Abel )
53 32 sselda ⊢ ( ( 𝜑 ∧ 𝑞 ∈ 𝐴 ) → 𝑞 ∈ ℙ )
54 50 subgbas ⊢ ( ( 𝑆 ‘ 𝑞 ) ∈ ( SubGrp ‘ 𝐺 ) → ( 𝑆 ‘ 𝑞 ) = ( Base ‘ ( 𝐺 ↾s ( 𝑆 ‘ 𝑞 ) ) ) )
55 39 54 syl ⊢ ( ( 𝜑 ∧ 𝑞 ∈ 𝐴 ) → ( 𝑆 ‘ 𝑞 ) = ( Base ‘ ( 𝐺 ↾s ( 𝑆 ‘ 𝑞 ) ) ) )
56 55 fveq2d ⊢ ( ( 𝜑 ∧ 𝑞 ∈ 𝐴 ) → ( ♯ ‘ ( 𝑆 ‘ 𝑞 ) ) = ( ♯ ‘ ( Base ‘ ( 𝐺 ↾s ( 𝑆 ‘ 𝑞 ) ) ) ) )
57 1 5 7 3 4 32 ablfac1a ⊢ ( ( 𝜑 ∧ 𝑞 ∈ 𝐴 ) → ( ♯ ‘ ( 𝑆 ‘ 𝑞 ) ) = ( 𝑞 ↑ ( 𝑞 pCnt ( ♯ ‘ 𝐵 ) ) ) )
58 56 57 eqtr3d ⊢ ( ( 𝜑 ∧ 𝑞 ∈ 𝐴 ) → ( ♯ ‘ ( Base ‘ ( 𝐺 ↾s ( 𝑆 ‘ 𝑞 ) ) ) ) = ( 𝑞 ↑ ( 𝑞 pCnt ( ♯ ‘ 𝐵 ) ) ) )
59 58 oveq2d ⊢ ( ( 𝜑 ∧ 𝑞 ∈ 𝐴 ) → ( 𝑞 pCnt ( ♯ ‘ ( Base ‘ ( 𝐺 ↾s ( 𝑆 ‘ 𝑞 ) ) ) ) ) = ( 𝑞 pCnt ( 𝑞 ↑ ( 𝑞 pCnt ( ♯ ‘ 𝐵 ) ) ) ) )
60 18 adantr ⊢ ( ( 𝜑 ∧ 𝑞 ∈ 𝐴 ) → ( ♯ ‘ 𝐵 ) ∈ ℕ )
61 53 60 pccld ⊢ ( ( 𝜑 ∧ 𝑞 ∈ 𝐴 ) → ( 𝑞 pCnt ( ♯ ‘ 𝐵 ) ) ∈ ℕ0 )
62 61 nn0zd ⊢ ( ( 𝜑 ∧ 𝑞 ∈ 𝐴 ) → ( 𝑞 pCnt ( ♯ ‘ 𝐵 ) ) ∈ ℤ )
63 pcid ⊢ ( ( 𝑞 ∈ ℙ ∧ ( 𝑞 pCnt ( ♯ ‘ 𝐵 ) ) ∈ ℤ ) → ( 𝑞 pCnt ( 𝑞 ↑ ( 𝑞 pCnt ( ♯ ‘ 𝐵 ) ) ) ) = ( 𝑞 pCnt ( ♯ ‘ 𝐵 ) ) )
64 53 62 63 syl2anc ⊢ ( ( 𝜑 ∧ 𝑞 ∈ 𝐴 ) → ( 𝑞 pCnt ( 𝑞 ↑ ( 𝑞 pCnt ( ♯ ‘ 𝐵 ) ) ) ) = ( 𝑞 pCnt ( ♯ ‘ 𝐵 ) ) )
65 59 64 eqtrd ⊢ ( ( 𝜑 ∧ 𝑞 ∈ 𝐴 ) → ( 𝑞 pCnt ( ♯ ‘ ( Base ‘ ( 𝐺 ↾s ( 𝑆 ‘ 𝑞 ) ) ) ) ) = ( 𝑞 pCnt ( ♯ ‘ 𝐵 ) ) )
66 65 oveq2d ⊢ ( ( 𝜑 ∧ 𝑞 ∈ 𝐴 ) → ( 𝑞 ↑ ( 𝑞 pCnt ( ♯ ‘ ( Base ‘ ( 𝐺 ↾s ( 𝑆 ‘ 𝑞 ) ) ) ) ) ) = ( 𝑞 ↑ ( 𝑞 pCnt ( ♯ ‘ 𝐵 ) ) ) )
67 58 66 eqtr4d ⊢ ( ( 𝜑 ∧ 𝑞 ∈ 𝐴 ) → ( ♯ ‘ ( Base ‘ ( 𝐺 ↾s ( 𝑆 ‘ 𝑞 ) ) ) ) = ( 𝑞 ↑ ( 𝑞 pCnt ( ♯ ‘ ( Base ‘ ( 𝐺 ↾s ( 𝑆 ‘ 𝑞 ) ) ) ) ) ) )
68 50 subggrp ⊢ ( ( 𝑆 ‘ 𝑞 ) ∈ ( SubGrp ‘ 𝐺 ) → ( 𝐺 ↾s ( 𝑆 ‘ 𝑞 ) ) ∈ Grp )
69 39 68 syl ⊢ ( ( 𝜑 ∧ 𝑞 ∈ 𝐴 ) → ( 𝐺 ↾s ( 𝑆 ‘ 𝑞 ) ) ∈ Grp )
70 4 adantr ⊢ ( ( 𝜑 ∧ 𝑞 ∈ 𝐴 ) → 𝐵 ∈ Fin )
71 1 subgss ⊢ ( ( 𝑆 ‘ 𝑞 ) ∈ ( SubGrp ‘ 𝐺 ) → ( 𝑆 ‘ 𝑞 ) ⊆ 𝐵 )
72 39 71 syl ⊢ ( ( 𝜑 ∧ 𝑞 ∈ 𝐴 ) → ( 𝑆 ‘ 𝑞 ) ⊆ 𝐵 )
73 70 72 ssfid ⊢ ( ( 𝜑 ∧ 𝑞 ∈ 𝐴 ) → ( 𝑆 ‘ 𝑞 ) ∈ Fin )
74 55 73 eqeltrrd ⊢ ( ( 𝜑 ∧ 𝑞 ∈ 𝐴 ) → ( Base ‘ ( 𝐺 ↾s ( 𝑆 ‘ 𝑞 ) ) ) ∈ Fin )
75 48 pgpfi2 ⊢ ( ( ( 𝐺 ↾s ( 𝑆 ‘ 𝑞 ) ) ∈ Grp ∧ ( Base ‘ ( 𝐺 ↾s ( 𝑆 ‘ 𝑞 ) ) ) ∈ Fin ) → ( 𝑞 pGrp ( 𝐺 ↾s ( 𝑆 ‘ 𝑞 ) ) ↔ ( 𝑞 ∈ ℙ ∧ ( ♯ ‘ ( Base ‘ ( 𝐺 ↾s ( 𝑆 ‘ 𝑞 ) ) ) ) = ( 𝑞 ↑ ( 𝑞 pCnt ( ♯ ‘ ( Base ‘ ( 𝐺 ↾s ( 𝑆 ‘ 𝑞 ) ) ) ) ) ) ) ) )
76 69 74 75 syl2anc ⊢ ( ( 𝜑 ∧ 𝑞 ∈ 𝐴 ) → ( 𝑞 pGrp ( 𝐺 ↾s ( 𝑆 ‘ 𝑞 ) ) ↔ ( 𝑞 ∈ ℙ ∧ ( ♯ ‘ ( Base ‘ ( 𝐺 ↾s ( 𝑆 ‘ 𝑞 ) ) ) ) = ( 𝑞 ↑ ( 𝑞 pCnt ( ♯ ‘ ( Base ‘ ( 𝐺 ↾s ( 𝑆 ‘ 𝑞 ) ) ) ) ) ) ) ) )
77 53 67 76 mpbir2and ⊢ ( ( 𝜑 ∧ 𝑞 ∈ 𝐴 ) → 𝑞 pGrp ( 𝐺 ↾s ( 𝑆 ‘ 𝑞 ) ) )
78 48 49 52 77 74 pgpfac ⊢ ( ( 𝜑 ∧ 𝑞 ∈ 𝐴 ) → ∃ 𝑠 ∈ Word { 𝑟 ∈ ( SubGrp ‘ ( 𝐺 ↾s ( 𝑆 ‘ 𝑞 ) ) ) ∣ ( ( 𝐺 ↾s ( 𝑆 ‘ 𝑞 ) ) ↾s 𝑟 ) ∈ ( CycGrp ∩ ran pGrp ) } ( ( 𝐺 ↾s ( 𝑆 ‘ 𝑞 ) ) dom DProd 𝑠 ∧ ( ( 𝐺 ↾s ( 𝑆 ‘ 𝑞 ) ) DProd 𝑠 ) = ( Base ‘ ( 𝐺 ↾s ( 𝑆 ‘ 𝑞 ) ) ) ) )
79 ssrab2 ⊢ { 𝑟 ∈ ( SubGrp ‘ ( 𝐺 ↾s ( 𝑆 ‘ 𝑞 ) ) ) ∣ ( ( 𝐺 ↾s ( 𝑆 ‘ 𝑞 ) ) ↾s 𝑟 ) ∈ ( CycGrp ∩ ran pGrp ) } ⊆ ( SubGrp ‘ ( 𝐺 ↾s ( 𝑆 ‘ 𝑞 ) ) )
80 sswrd ⊢ ( { 𝑟 ∈ ( SubGrp ‘ ( 𝐺 ↾s ( 𝑆 ‘ 𝑞 ) ) ) ∣ ( ( 𝐺 ↾s ( 𝑆 ‘ 𝑞 ) ) ↾s 𝑟 ) ∈ ( CycGrp ∩ ran pGrp ) } ⊆ ( SubGrp ‘ ( 𝐺 ↾s ( 𝑆 ‘ 𝑞 ) ) ) → Word { 𝑟 ∈ ( SubGrp ‘ ( 𝐺 ↾s ( 𝑆 ‘ 𝑞 ) ) ) ∣ ( ( 𝐺 ↾s ( 𝑆 ‘ 𝑞 ) ) ↾s 𝑟 ) ∈ ( CycGrp ∩ ran pGrp ) } ⊆ Word ( SubGrp ‘ ( 𝐺 ↾s ( 𝑆 ‘ 𝑞 ) ) ) )
81 79 80 ax-mp ⊢ Word { 𝑟 ∈ ( SubGrp ‘ ( 𝐺 ↾s ( 𝑆 ‘ 𝑞 ) ) ) ∣ ( ( 𝐺 ↾s ( 𝑆 ‘ 𝑞 ) ) ↾s 𝑟 ) ∈ ( CycGrp ∩ ran pGrp ) } ⊆ Word ( SubGrp ‘ ( 𝐺 ↾s ( 𝑆 ‘ 𝑞 ) ) )
82 81 sseli ⊢ ( 𝑠 ∈ Word { 𝑟 ∈ ( SubGrp ‘ ( 𝐺 ↾s ( 𝑆 ‘ 𝑞 ) ) ) ∣ ( ( 𝐺 ↾s ( 𝑆 ‘ 𝑞 ) ) ↾s 𝑟 ) ∈ ( CycGrp ∩ ran pGrp ) } → 𝑠 ∈ Word ( SubGrp ‘ ( 𝐺 ↾s ( 𝑆 ‘ 𝑞 ) ) ) )
83 39 adantr ⊢ ( ( ( 𝜑 ∧ 𝑞 ∈ 𝐴 ) ∧ 𝑠 ∈ Word ( SubGrp ‘ ( 𝐺 ↾s ( 𝑆 ‘ 𝑞 ) ) ) ) → ( 𝑆 ‘ 𝑞 ) ∈ ( SubGrp ‘ 𝐺 ) )
84 83 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑞 ∈ 𝐴 ) ∧ 𝑠 ∈ Word ( SubGrp ‘ ( 𝐺 ↾s ( 𝑆 ‘ 𝑞 ) ) ) ) ∧ ( 𝐺 ↾s ( 𝑆 ‘ 𝑞 ) ) dom DProd 𝑠 ) → ( 𝑆 ‘ 𝑞 ) ∈ ( SubGrp ‘ 𝐺 ) )
85 50 subgdmdprd ⊢ ( ( 𝑆 ‘ 𝑞 ) ∈ ( SubGrp ‘ 𝐺 ) → ( ( 𝐺 ↾s ( 𝑆 ‘ 𝑞 ) ) dom DProd 𝑠 ↔ ( 𝐺 dom DProd 𝑠 ∧ ran 𝑠 ⊆ 𝒫 ( 𝑆 ‘ 𝑞 ) ) ) )
86 83 85 syl ⊢ ( ( ( 𝜑 ∧ 𝑞 ∈ 𝐴 ) ∧ 𝑠 ∈ Word ( SubGrp ‘ ( 𝐺 ↾s ( 𝑆 ‘ 𝑞 ) ) ) ) → ( ( 𝐺 ↾s ( 𝑆 ‘ 𝑞 ) ) dom DProd 𝑠 ↔ ( 𝐺 dom DProd 𝑠 ∧ ran 𝑠 ⊆ 𝒫 ( 𝑆 ‘ 𝑞 ) ) ) )
87 86 simprbda ⊢ ( ( ( ( 𝜑 ∧ 𝑞 ∈ 𝐴 ) ∧ 𝑠 ∈ Word ( SubGrp ‘ ( 𝐺 ↾s ( 𝑆 ‘ 𝑞 ) ) ) ) ∧ ( 𝐺 ↾s ( 𝑆 ‘ 𝑞 ) ) dom DProd 𝑠 ) → 𝐺 dom DProd 𝑠 )
88 86 simplbda ⊢ ( ( ( ( 𝜑 ∧ 𝑞 ∈ 𝐴 ) ∧ 𝑠 ∈ Word ( SubGrp ‘ ( 𝐺 ↾s ( 𝑆 ‘ 𝑞 ) ) ) ) ∧ ( 𝐺 ↾s ( 𝑆 ‘ 𝑞 ) ) dom DProd 𝑠 ) → ran 𝑠 ⊆ 𝒫 ( 𝑆 ‘ 𝑞 ) )
89 50 84 87 88 subgdprd ⊢ ( ( ( ( 𝜑 ∧ 𝑞 ∈ 𝐴 ) ∧ 𝑠 ∈ Word ( SubGrp ‘ ( 𝐺 ↾s ( 𝑆 ‘ 𝑞 ) ) ) ) ∧ ( 𝐺 ↾s ( 𝑆 ‘ 𝑞 ) ) dom DProd 𝑠 ) → ( ( 𝐺 ↾s ( 𝑆 ‘ 𝑞 ) ) DProd 𝑠 ) = ( 𝐺 DProd 𝑠 ) )
90 55 ad2antrr ⊢ ( ( ( ( 𝜑 ∧ 𝑞 ∈ 𝐴 ) ∧ 𝑠 ∈ Word ( SubGrp ‘ ( 𝐺 ↾s ( 𝑆 ‘ 𝑞 ) ) ) ) ∧ ( 𝐺 ↾s ( 𝑆 ‘ 𝑞 ) ) dom DProd 𝑠 ) → ( 𝑆 ‘ 𝑞 ) = ( Base ‘ ( 𝐺 ↾s ( 𝑆 ‘ 𝑞 ) ) ) )
91 90 eqcomd ⊢ ( ( ( ( 𝜑 ∧ 𝑞 ∈ 𝐴 ) ∧ 𝑠 ∈ Word ( SubGrp ‘ ( 𝐺 ↾s ( 𝑆 ‘ 𝑞 ) ) ) ) ∧ ( 𝐺 ↾s ( 𝑆 ‘ 𝑞 ) ) dom DProd 𝑠 ) → ( Base ‘ ( 𝐺 ↾s ( 𝑆 ‘ 𝑞 ) ) ) = ( 𝑆 ‘ 𝑞 ) )
92 89 91 eqeq12d ⊢ ( ( ( ( 𝜑 ∧ 𝑞 ∈ 𝐴 ) ∧ 𝑠 ∈ Word ( SubGrp ‘ ( 𝐺 ↾s ( 𝑆 ‘ 𝑞 ) ) ) ) ∧ ( 𝐺 ↾s ( 𝑆 ‘ 𝑞 ) ) dom DProd 𝑠 ) → ( ( ( 𝐺 ↾s ( 𝑆 ‘ 𝑞 ) ) DProd 𝑠 ) = ( Base ‘ ( 𝐺 ↾s ( 𝑆 ‘ 𝑞 ) ) ) ↔ ( 𝐺 DProd 𝑠 ) = ( 𝑆 ‘ 𝑞 ) ) )
93 92 biimpd ⊢ ( ( ( ( 𝜑 ∧ 𝑞 ∈ 𝐴 ) ∧ 𝑠 ∈ Word ( SubGrp ‘ ( 𝐺 ↾s ( 𝑆 ‘ 𝑞 ) ) ) ) ∧ ( 𝐺 ↾s ( 𝑆 ‘ 𝑞 ) ) dom DProd 𝑠 ) → ( ( ( 𝐺 ↾s ( 𝑆 ‘ 𝑞 ) ) DProd 𝑠 ) = ( Base ‘ ( 𝐺 ↾s ( 𝑆 ‘ 𝑞 ) ) ) → ( 𝐺 DProd 𝑠 ) = ( 𝑆 ‘ 𝑞 ) ) )
94 93 87 jctild ⊢ ( ( ( ( 𝜑 ∧ 𝑞 ∈ 𝐴 ) ∧ 𝑠 ∈ Word ( SubGrp ‘ ( 𝐺 ↾s ( 𝑆 ‘ 𝑞 ) ) ) ) ∧ ( 𝐺 ↾s ( 𝑆 ‘ 𝑞 ) ) dom DProd 𝑠 ) → ( ( ( 𝐺 ↾s ( 𝑆 ‘ 𝑞 ) ) DProd 𝑠 ) = ( Base ‘ ( 𝐺 ↾s ( 𝑆 ‘ 𝑞 ) ) ) → ( 𝐺 dom DProd 𝑠 ∧ ( 𝐺 DProd 𝑠 ) = ( 𝑆 ‘ 𝑞 ) ) ) )
95 94 expimpd ⊢ ( ( ( 𝜑 ∧ 𝑞 ∈ 𝐴 ) ∧ 𝑠 ∈ Word ( SubGrp ‘ ( 𝐺 ↾s ( 𝑆 ‘ 𝑞 ) ) ) ) → ( ( ( 𝐺 ↾s ( 𝑆 ‘ 𝑞 ) ) dom DProd 𝑠 ∧ ( ( 𝐺 ↾s ( 𝑆 ‘ 𝑞 ) ) DProd 𝑠 ) = ( Base ‘ ( 𝐺 ↾s ( 𝑆 ‘ 𝑞 ) ) ) ) → ( 𝐺 dom DProd 𝑠 ∧ ( 𝐺 DProd 𝑠 ) = ( 𝑆 ‘ 𝑞 ) ) ) )
96 82 95 sylan2 ⊢ ( ( ( 𝜑 ∧ 𝑞 ∈ 𝐴 ) ∧ 𝑠 ∈ Word { 𝑟 ∈ ( SubGrp ‘ ( 𝐺 ↾s ( 𝑆 ‘ 𝑞 ) ) ) ∣ ( ( 𝐺 ↾s ( 𝑆 ‘ 𝑞 ) ) ↾s 𝑟 ) ∈ ( CycGrp ∩ ran pGrp ) } ) → ( ( ( 𝐺 ↾s ( 𝑆 ‘ 𝑞 ) ) dom DProd 𝑠 ∧ ( ( 𝐺 ↾s ( 𝑆 ‘ 𝑞 ) ) DProd 𝑠 ) = ( Base ‘ ( 𝐺 ↾s ( 𝑆 ‘ 𝑞 ) ) ) ) → ( 𝐺 dom DProd 𝑠 ∧ ( 𝐺 DProd 𝑠 ) = ( 𝑆 ‘ 𝑞 ) ) ) )
97 oveq2 ⊢ ( 𝑟 = 𝑦 → ( ( 𝐺 ↾s ( 𝑆 ‘ 𝑞 ) ) ↾s 𝑟 ) = ( ( 𝐺 ↾s ( 𝑆 ‘ 𝑞 ) ) ↾s 𝑦 ) )
98 97 eleq1d ⊢ ( 𝑟 = 𝑦 → ( ( ( 𝐺 ↾s ( 𝑆 ‘ 𝑞 ) ) ↾s 𝑟 ) ∈ ( CycGrp ∩ ran pGrp ) ↔ ( ( 𝐺 ↾s ( 𝑆 ‘ 𝑞 ) ) ↾s 𝑦 ) ∈ ( CycGrp ∩ ran pGrp ) ) )
99 98 cbvrabv ⊢ { 𝑟 ∈ ( SubGrp ‘ ( 𝐺 ↾s ( 𝑆 ‘ 𝑞 ) ) ) ∣ ( ( 𝐺 ↾s ( 𝑆 ‘ 𝑞 ) ) ↾s 𝑟 ) ∈ ( CycGrp ∩ ran pGrp ) } = { 𝑦 ∈ ( SubGrp ‘ ( 𝐺 ↾s ( 𝑆 ‘ 𝑞 ) ) ) ∣ ( ( 𝐺 ↾s ( 𝑆 ‘ 𝑞 ) ) ↾s 𝑦 ) ∈ ( CycGrp ∩ ran pGrp ) }
100 50 subsubg ⊢ ( ( 𝑆 ‘ 𝑞 ) ∈ ( SubGrp ‘ 𝐺 ) → ( 𝑦 ∈ ( SubGrp ‘ ( 𝐺 ↾s ( 𝑆 ‘ 𝑞 ) ) ) ↔ ( 𝑦 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑦 ⊆ ( 𝑆 ‘ 𝑞 ) ) ) )
101 39 100 syl ⊢ ( ( 𝜑 ∧ 𝑞 ∈ 𝐴 ) → ( 𝑦 ∈ ( SubGrp ‘ ( 𝐺 ↾s ( 𝑆 ‘ 𝑞 ) ) ) ↔ ( 𝑦 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑦 ⊆ ( 𝑆 ‘ 𝑞 ) ) ) )
102 101 simprbda ⊢ ( ( ( 𝜑 ∧ 𝑞 ∈ 𝐴 ) ∧ 𝑦 ∈ ( SubGrp ‘ ( 𝐺 ↾s ( 𝑆 ‘ 𝑞 ) ) ) ) → 𝑦 ∈ ( SubGrp ‘ 𝐺 ) )
103 102 3adant3 ⊢ ( ( ( 𝜑 ∧ 𝑞 ∈ 𝐴 ) ∧ 𝑦 ∈ ( SubGrp ‘ ( 𝐺 ↾s ( 𝑆 ‘ 𝑞 ) ) ) ∧ ( ( 𝐺 ↾s ( 𝑆 ‘ 𝑞 ) ) ↾s 𝑦 ) ∈ ( CycGrp ∩ ran pGrp ) ) → 𝑦 ∈ ( SubGrp ‘ 𝐺 ) )
104 39 3ad2ant1 ⊢ ( ( ( 𝜑 ∧ 𝑞 ∈ 𝐴 ) ∧ 𝑦 ∈ ( SubGrp ‘ ( 𝐺 ↾s ( 𝑆 ‘ 𝑞 ) ) ) ∧ ( ( 𝐺 ↾s ( 𝑆 ‘ 𝑞 ) ) ↾s 𝑦 ) ∈ ( CycGrp ∩ ran pGrp ) ) → ( 𝑆 ‘ 𝑞 ) ∈ ( SubGrp ‘ 𝐺 ) )
105 101 simplbda ⊢ ( ( ( 𝜑 ∧ 𝑞 ∈ 𝐴 ) ∧ 𝑦 ∈ ( SubGrp ‘ ( 𝐺 ↾s ( 𝑆 ‘ 𝑞 ) ) ) ) → 𝑦 ⊆ ( 𝑆 ‘ 𝑞 ) )
106 105 3adant3 ⊢ ( ( ( 𝜑 ∧ 𝑞 ∈ 𝐴 ) ∧ 𝑦 ∈ ( SubGrp ‘ ( 𝐺 ↾s ( 𝑆 ‘ 𝑞 ) ) ) ∧ ( ( 𝐺 ↾s ( 𝑆 ‘ 𝑞 ) ) ↾s 𝑦 ) ∈ ( CycGrp ∩ ran pGrp ) ) → 𝑦 ⊆ ( 𝑆 ‘ 𝑞 ) )
107 ressabs ⊢ ( ( ( 𝑆 ‘ 𝑞 ) ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑦 ⊆ ( 𝑆 ‘ 𝑞 ) ) → ( ( 𝐺 ↾s ( 𝑆 ‘ 𝑞 ) ) ↾s 𝑦 ) = ( 𝐺 ↾s 𝑦 ) )
108 104 106 107 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑞 ∈ 𝐴 ) ∧ 𝑦 ∈ ( SubGrp ‘ ( 𝐺 ↾s ( 𝑆 ‘ 𝑞 ) ) ) ∧ ( ( 𝐺 ↾s ( 𝑆 ‘ 𝑞 ) ) ↾s 𝑦 ) ∈ ( CycGrp ∩ ran pGrp ) ) → ( ( 𝐺 ↾s ( 𝑆 ‘ 𝑞 ) ) ↾s 𝑦 ) = ( 𝐺 ↾s 𝑦 ) )
109 simp3 ⊢ ( ( ( 𝜑 ∧ 𝑞 ∈ 𝐴 ) ∧ 𝑦 ∈ ( SubGrp ‘ ( 𝐺 ↾s ( 𝑆 ‘ 𝑞 ) ) ) ∧ ( ( 𝐺 ↾s ( 𝑆 ‘ 𝑞 ) ) ↾s 𝑦 ) ∈ ( CycGrp ∩ ran pGrp ) ) → ( ( 𝐺 ↾s ( 𝑆 ‘ 𝑞 ) ) ↾s 𝑦 ) ∈ ( CycGrp ∩ ran pGrp ) )
110 108 109 eqeltrrd ⊢ ( ( ( 𝜑 ∧ 𝑞 ∈ 𝐴 ) ∧ 𝑦 ∈ ( SubGrp ‘ ( 𝐺 ↾s ( 𝑆 ‘ 𝑞 ) ) ) ∧ ( ( 𝐺 ↾s ( 𝑆 ‘ 𝑞 ) ) ↾s 𝑦 ) ∈ ( CycGrp ∩ ran pGrp ) ) → ( 𝐺 ↾s 𝑦 ) ∈ ( CycGrp ∩ ran pGrp ) )
111 oveq2 ⊢ ( 𝑟 = 𝑦 → ( 𝐺 ↾s 𝑟 ) = ( 𝐺 ↾s 𝑦 ) )
112 111 eleq1d ⊢ ( 𝑟 = 𝑦 → ( ( 𝐺 ↾s 𝑟 ) ∈ ( CycGrp ∩ ran pGrp ) ↔ ( 𝐺 ↾s 𝑦 ) ∈ ( CycGrp ∩ ran pGrp ) ) )
113 112 2 elrab2 ⊢ ( 𝑦 ∈ 𝐶 ↔ ( 𝑦 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( 𝐺 ↾s 𝑦 ) ∈ ( CycGrp ∩ ran pGrp ) ) )
114 103 110 113 sylanbrc ⊢ ( ( ( 𝜑 ∧ 𝑞 ∈ 𝐴 ) ∧ 𝑦 ∈ ( SubGrp ‘ ( 𝐺 ↾s ( 𝑆 ‘ 𝑞 ) ) ) ∧ ( ( 𝐺 ↾s ( 𝑆 ‘ 𝑞 ) ) ↾s 𝑦 ) ∈ ( CycGrp ∩ ran pGrp ) ) → 𝑦 ∈ 𝐶 )
115 114 rabssdv ⊢ ( ( 𝜑 ∧ 𝑞 ∈ 𝐴 ) → { 𝑦 ∈ ( SubGrp ‘ ( 𝐺 ↾s ( 𝑆 ‘ 𝑞 ) ) ) ∣ ( ( 𝐺 ↾s ( 𝑆 ‘ 𝑞 ) ) ↾s 𝑦 ) ∈ ( CycGrp ∩ ran pGrp ) } ⊆ 𝐶 )
116 99 115 eqsstrid ⊢ ( ( 𝜑 ∧ 𝑞 ∈ 𝐴 ) → { 𝑟 ∈ ( SubGrp ‘ ( 𝐺 ↾s ( 𝑆 ‘ 𝑞 ) ) ) ∣ ( ( 𝐺 ↾s ( 𝑆 ‘ 𝑞 ) ) ↾s 𝑟 ) ∈ ( CycGrp ∩ ran pGrp ) } ⊆ 𝐶 )
117 sswrd ⊢ ( { 𝑟 ∈ ( SubGrp ‘ ( 𝐺 ↾s ( 𝑆 ‘ 𝑞 ) ) ) ∣ ( ( 𝐺 ↾s ( 𝑆 ‘ 𝑞 ) ) ↾s 𝑟 ) ∈ ( CycGrp ∩ ran pGrp ) } ⊆ 𝐶 → Word { 𝑟 ∈ ( SubGrp ‘ ( 𝐺 ↾s ( 𝑆 ‘ 𝑞 ) ) ) ∣ ( ( 𝐺 ↾s ( 𝑆 ‘ 𝑞 ) ) ↾s 𝑟 ) ∈ ( CycGrp ∩ ran pGrp ) } ⊆ Word 𝐶 )
118 116 117 syl ⊢ ( ( 𝜑 ∧ 𝑞 ∈ 𝐴 ) → Word { 𝑟 ∈ ( SubGrp ‘ ( 𝐺 ↾s ( 𝑆 ‘ 𝑞 ) ) ) ∣ ( ( 𝐺 ↾s ( 𝑆 ‘ 𝑞 ) ) ↾s 𝑟 ) ∈ ( CycGrp ∩ ran pGrp ) } ⊆ Word 𝐶 )
119 118 sselda ⊢ ( ( ( 𝜑 ∧ 𝑞 ∈ 𝐴 ) ∧ 𝑠 ∈ Word { 𝑟 ∈ ( SubGrp ‘ ( 𝐺 ↾s ( 𝑆 ‘ 𝑞 ) ) ) ∣ ( ( 𝐺 ↾s ( 𝑆 ‘ 𝑞 ) ) ↾s 𝑟 ) ∈ ( CycGrp ∩ ran pGrp ) } ) → 𝑠 ∈ Word 𝐶 )
120 96 119 jctild ⊢ ( ( ( 𝜑 ∧ 𝑞 ∈ 𝐴 ) ∧ 𝑠 ∈ Word { 𝑟 ∈ ( SubGrp ‘ ( 𝐺 ↾s ( 𝑆 ‘ 𝑞 ) ) ) ∣ ( ( 𝐺 ↾s ( 𝑆 ‘ 𝑞 ) ) ↾s 𝑟 ) ∈ ( CycGrp ∩ ran pGrp ) } ) → ( ( ( 𝐺 ↾s ( 𝑆 ‘ 𝑞 ) ) dom DProd 𝑠 ∧ ( ( 𝐺 ↾s ( 𝑆 ‘ 𝑞 ) ) DProd 𝑠 ) = ( Base ‘ ( 𝐺 ↾s ( 𝑆 ‘ 𝑞 ) ) ) ) → ( 𝑠 ∈ Word 𝐶 ∧ ( 𝐺 dom DProd 𝑠 ∧ ( 𝐺 DProd 𝑠 ) = ( 𝑆 ‘ 𝑞 ) ) ) ) )
121 120 expimpd ⊢ ( ( 𝜑 ∧ 𝑞 ∈ 𝐴 ) → ( ( 𝑠 ∈ Word { 𝑟 ∈ ( SubGrp ‘ ( 𝐺 ↾s ( 𝑆 ‘ 𝑞 ) ) ) ∣ ( ( 𝐺 ↾s ( 𝑆 ‘ 𝑞 ) ) ↾s 𝑟 ) ∈ ( CycGrp ∩ ran pGrp ) } ∧ ( ( 𝐺 ↾s ( 𝑆 ‘ 𝑞 ) ) dom DProd 𝑠 ∧ ( ( 𝐺 ↾s ( 𝑆 ‘ 𝑞 ) ) DProd 𝑠 ) = ( Base ‘ ( 𝐺 ↾s ( 𝑆 ‘ 𝑞 ) ) ) ) ) → ( 𝑠 ∈ Word 𝐶 ∧ ( 𝐺 dom DProd 𝑠 ∧ ( 𝐺 DProd 𝑠 ) = ( 𝑆 ‘ 𝑞 ) ) ) ) )
122 121 reximdv2 ⊢ ( ( 𝜑 ∧ 𝑞 ∈ 𝐴 ) → ( ∃ 𝑠 ∈ Word { 𝑟 ∈ ( SubGrp ‘ ( 𝐺 ↾s ( 𝑆 ‘ 𝑞 ) ) ) ∣ ( ( 𝐺 ↾s ( 𝑆 ‘ 𝑞 ) ) ↾s 𝑟 ) ∈ ( CycGrp ∩ ran pGrp ) } ( ( 𝐺 ↾s ( 𝑆 ‘ 𝑞 ) ) dom DProd 𝑠 ∧ ( ( 𝐺 ↾s ( 𝑆 ‘ 𝑞 ) ) DProd 𝑠 ) = ( Base ‘ ( 𝐺 ↾s ( 𝑆 ‘ 𝑞 ) ) ) ) → ∃ 𝑠 ∈ Word 𝐶 ( 𝐺 dom DProd 𝑠 ∧ ( 𝐺 DProd 𝑠 ) = ( 𝑆 ‘ 𝑞 ) ) ) )
123 78 122 mpd ⊢ ( ( 𝜑 ∧ 𝑞 ∈ 𝐴 ) → ∃ 𝑠 ∈ Word 𝐶 ( 𝐺 dom DProd 𝑠 ∧ ( 𝐺 DProd 𝑠 ) = ( 𝑆 ‘ 𝑞 ) ) )
124 rabn0 ⊢ ( { 𝑠 ∈ Word 𝐶 ∣ ( 𝐺 dom DProd 𝑠 ∧ ( 𝐺 DProd 𝑠 ) = ( 𝑆 ‘ 𝑞 ) ) } ≠ ∅ ↔ ∃ 𝑠 ∈ Word 𝐶 ( 𝐺 dom DProd 𝑠 ∧ ( 𝐺 DProd 𝑠 ) = ( 𝑆 ‘ 𝑞 ) ) )
125 123 124 sylibr ⊢ ( ( 𝜑 ∧ 𝑞 ∈ 𝐴 ) → { 𝑠 ∈ Word 𝐶 ∣ ( 𝐺 dom DProd 𝑠 ∧ ( 𝐺 DProd 𝑠 ) = ( 𝑆 ‘ 𝑞 ) ) } ≠ ∅ )
126 47 125 eqnetrd ⊢ ( ( 𝜑 ∧ 𝑞 ∈ 𝐴 ) → { 𝑦 ∈ Word 𝐶 ∣ 𝑦 ∈ ( 𝑊 ‘ ( 𝑆 ‘ 𝑞 ) ) } ≠ ∅ )
127 rabn0 ⊢ ( { 𝑦 ∈ Word 𝐶 ∣ 𝑦 ∈ ( 𝑊 ‘ ( 𝑆 ‘ 𝑞 ) ) } ≠ ∅ ↔ ∃ 𝑦 ∈ Word 𝐶 𝑦 ∈ ( 𝑊 ‘ ( 𝑆 ‘ 𝑞 ) ) )
128 126 127 sylib ⊢ ( ( 𝜑 ∧ 𝑞 ∈ 𝐴 ) → ∃ 𝑦 ∈ Word 𝐶 𝑦 ∈ ( 𝑊 ‘ ( 𝑆 ‘ 𝑞 ) ) )
129 128 ralrimiva ⊢ ( 𝜑 → ∀ 𝑞 ∈ 𝐴 ∃ 𝑦 ∈ Word 𝐶 𝑦 ∈ ( 𝑊 ‘ ( 𝑆 ‘ 𝑞 ) ) )
130 eleq1 ⊢ ( 𝑦 = ( 𝑓 ‘ 𝑞 ) → ( 𝑦 ∈ ( 𝑊 ‘ ( 𝑆 ‘ 𝑞 ) ) ↔ ( 𝑓 ‘ 𝑞 ) ∈ ( 𝑊 ‘ ( 𝑆 ‘ 𝑞 ) ) ) )
131 130 ac6sfi ⊢ ( ( 𝐴 ∈ Fin ∧ ∀ 𝑞 ∈ 𝐴 ∃ 𝑦 ∈ Word 𝐶 𝑦 ∈ ( 𝑊 ‘ ( 𝑆 ‘ 𝑞 ) ) ) → ∃ 𝑓 ( 𝑓 : 𝐴 ⟶ Word 𝐶 ∧ ∀ 𝑞 ∈ 𝐴 ( 𝑓 ‘ 𝑞 ) ∈ ( 𝑊 ‘ ( 𝑆 ‘ 𝑞 ) ) ) )
132 29 129 131 syl2anc ⊢ ( 𝜑 → ∃ 𝑓 ( 𝑓 : 𝐴 ⟶ Word 𝐶 ∧ ∀ 𝑞 ∈ 𝐴 ( 𝑓 ‘ 𝑞 ) ∈ ( 𝑊 ‘ ( 𝑆 ‘ 𝑞 ) ) ) )
133 sneq ⊢ ( 𝑞 = 𝑦 → { 𝑞 } = { 𝑦 } )
134 fveq2 ⊢ ( 𝑞 = 𝑦 → ( 𝑓 ‘ 𝑞 ) = ( 𝑓 ‘ 𝑦 ) )
135 134 dmeqd ⊢ ( 𝑞 = 𝑦 → dom ( 𝑓 ‘ 𝑞 ) = dom ( 𝑓 ‘ 𝑦 ) )
136 133 135 xpeq12d ⊢ ( 𝑞 = 𝑦 → ( { 𝑞 } × dom ( 𝑓 ‘ 𝑞 ) ) = ( { 𝑦 } × dom ( 𝑓 ‘ 𝑦 ) ) )
137 136 cbviunv ⊢ ∪ 𝑞 ∈ 𝐴 ( { 𝑞 } × dom ( 𝑓 ‘ 𝑞 ) ) = ∪ 𝑦 ∈ 𝐴 ( { 𝑦 } × dom ( 𝑓 ‘ 𝑦 ) )
138 snfi ⊢ { 𝑦 } ∈ Fin
139 simprl ⊢ ( ( 𝜑 ∧ ( 𝑓 : 𝐴 ⟶ Word 𝐶 ∧ ∀ 𝑞 ∈ 𝐴 ( 𝑓 ‘ 𝑞 ) ∈ ( 𝑊 ‘ ( 𝑆 ‘ 𝑞 ) ) ) ) → 𝑓 : 𝐴 ⟶ Word 𝐶 )
140 139 ffvelcdmda ⊢ ( ( ( 𝜑 ∧ ( 𝑓 : 𝐴 ⟶ Word 𝐶 ∧ ∀ 𝑞 ∈ 𝐴 ( 𝑓 ‘ 𝑞 ) ∈ ( 𝑊 ‘ ( 𝑆 ‘ 𝑞 ) ) ) ) ∧ 𝑦 ∈ 𝐴 ) → ( 𝑓 ‘ 𝑦 ) ∈ Word 𝐶 )
141 wrdf ⊢ ( ( 𝑓 ‘ 𝑦 ) ∈ Word 𝐶 → ( 𝑓 ‘ 𝑦 ) : ( 0 ..^ ( ♯ ‘ ( 𝑓 ‘ 𝑦 ) ) ) ⟶ 𝐶 )
142 fdm ⊢ ( ( 𝑓 ‘ 𝑦 ) : ( 0 ..^ ( ♯ ‘ ( 𝑓 ‘ 𝑦 ) ) ) ⟶ 𝐶 → dom ( 𝑓 ‘ 𝑦 ) = ( 0 ..^ ( ♯ ‘ ( 𝑓 ‘ 𝑦 ) ) ) )
143 140 141 142 3syl ⊢ ( ( ( 𝜑 ∧ ( 𝑓 : 𝐴 ⟶ Word 𝐶 ∧ ∀ 𝑞 ∈ 𝐴 ( 𝑓 ‘ 𝑞 ) ∈ ( 𝑊 ‘ ( 𝑆 ‘ 𝑞 ) ) ) ) ∧ 𝑦 ∈ 𝐴 ) → dom ( 𝑓 ‘ 𝑦 ) = ( 0 ..^ ( ♯ ‘ ( 𝑓 ‘ 𝑦 ) ) ) )
144 fzofi ⊢ ( 0 ..^ ( ♯ ‘ ( 𝑓 ‘ 𝑦 ) ) ) ∈ Fin
145 143 144 eqeltrdi ⊢ ( ( ( 𝜑 ∧ ( 𝑓 : 𝐴 ⟶ Word 𝐶 ∧ ∀ 𝑞 ∈ 𝐴 ( 𝑓 ‘ 𝑞 ) ∈ ( 𝑊 ‘ ( 𝑆 ‘ 𝑞 ) ) ) ) ∧ 𝑦 ∈ 𝐴 ) → dom ( 𝑓 ‘ 𝑦 ) ∈ Fin )
146 xpfi ⊢ ( ( { 𝑦 } ∈ Fin ∧ dom ( 𝑓 ‘ 𝑦 ) ∈ Fin ) → ( { 𝑦 } × dom ( 𝑓 ‘ 𝑦 ) ) ∈ Fin )
147 138 145 146 sylancr ⊢ ( ( ( 𝜑 ∧ ( 𝑓 : 𝐴 ⟶ Word 𝐶 ∧ ∀ 𝑞 ∈ 𝐴 ( 𝑓 ‘ 𝑞 ) ∈ ( 𝑊 ‘ ( 𝑆 ‘ 𝑞 ) ) ) ) ∧ 𝑦 ∈ 𝐴 ) → ( { 𝑦 } × dom ( 𝑓 ‘ 𝑦 ) ) ∈ Fin )
148 147 ralrimiva ⊢ ( ( 𝜑 ∧ ( 𝑓 : 𝐴 ⟶ Word 𝐶 ∧ ∀ 𝑞 ∈ 𝐴 ( 𝑓 ‘ 𝑞 ) ∈ ( 𝑊 ‘ ( 𝑆 ‘ 𝑞 ) ) ) ) → ∀ 𝑦 ∈ 𝐴 ( { 𝑦 } × dom ( 𝑓 ‘ 𝑦 ) ) ∈ Fin )
149 iunfi ⊢ ( ( 𝐴 ∈ Fin ∧ ∀ 𝑦 ∈ 𝐴 ( { 𝑦 } × dom ( 𝑓 ‘ 𝑦 ) ) ∈ Fin ) → ∪ 𝑦 ∈ 𝐴 ( { 𝑦 } × dom ( 𝑓 ‘ 𝑦 ) ) ∈ Fin )
150 29 148 149 syl2an2r ⊢ ( ( 𝜑 ∧ ( 𝑓 : 𝐴 ⟶ Word 𝐶 ∧ ∀ 𝑞 ∈ 𝐴 ( 𝑓 ‘ 𝑞 ) ∈ ( 𝑊 ‘ ( 𝑆 ‘ 𝑞 ) ) ) ) → ∪ 𝑦 ∈ 𝐴 ( { 𝑦 } × dom ( 𝑓 ‘ 𝑦 ) ) ∈ Fin )
151 137 150 eqeltrid ⊢ ( ( 𝜑 ∧ ( 𝑓 : 𝐴 ⟶ Word 𝐶 ∧ ∀ 𝑞 ∈ 𝐴 ( 𝑓 ‘ 𝑞 ) ∈ ( 𝑊 ‘ ( 𝑆 ‘ 𝑞 ) ) ) ) → ∪ 𝑞 ∈ 𝐴 ( { 𝑞 } × dom ( 𝑓 ‘ 𝑞 ) ) ∈ Fin )
152 hashcl ⊢ ( ∪ 𝑞 ∈ 𝐴 ( { 𝑞 } × dom ( 𝑓 ‘ 𝑞 ) ) ∈ Fin → ( ♯ ‘ ∪ 𝑞 ∈ 𝐴 ( { 𝑞 } × dom ( 𝑓 ‘ 𝑞 ) ) ) ∈ ℕ0 )
153 hashfzo0 ⊢ ( ( ♯ ‘ ∪ 𝑞 ∈ 𝐴 ( { 𝑞 } × dom ( 𝑓 ‘ 𝑞 ) ) ) ∈ ℕ0 → ( ♯ ‘ ( 0 ..^ ( ♯ ‘ ∪ 𝑞 ∈ 𝐴 ( { 𝑞 } × dom ( 𝑓 ‘ 𝑞 ) ) ) ) ) = ( ♯ ‘ ∪ 𝑞 ∈ 𝐴 ( { 𝑞 } × dom ( 𝑓 ‘ 𝑞 ) ) ) )
154 151 152 153 3syl ⊢ ( ( 𝜑 ∧ ( 𝑓 : 𝐴 ⟶ Word 𝐶 ∧ ∀ 𝑞 ∈ 𝐴 ( 𝑓 ‘ 𝑞 ) ∈ ( 𝑊 ‘ ( 𝑆 ‘ 𝑞 ) ) ) ) → ( ♯ ‘ ( 0 ..^ ( ♯ ‘ ∪ 𝑞 ∈ 𝐴 ( { 𝑞 } × dom ( 𝑓 ‘ 𝑞 ) ) ) ) ) = ( ♯ ‘ ∪ 𝑞 ∈ 𝐴 ( { 𝑞 } × dom ( 𝑓 ‘ 𝑞 ) ) ) )
155 fzofi ⊢ ( 0 ..^ ( ♯ ‘ ∪ 𝑞 ∈ 𝐴 ( { 𝑞 } × dom ( 𝑓 ‘ 𝑞 ) ) ) ) ∈ Fin
156 hashen ⊢ ( ( ( 0 ..^ ( ♯ ‘ ∪ 𝑞 ∈ 𝐴 ( { 𝑞 } × dom ( 𝑓 ‘ 𝑞 ) ) ) ) ∈ Fin ∧ ∪ 𝑞 ∈ 𝐴 ( { 𝑞 } × dom ( 𝑓 ‘ 𝑞 ) ) ∈ Fin ) → ( ( ♯ ‘ ( 0 ..^ ( ♯ ‘ ∪ 𝑞 ∈ 𝐴 ( { 𝑞 } × dom ( 𝑓 ‘ 𝑞 ) ) ) ) ) = ( ♯ ‘ ∪ 𝑞 ∈ 𝐴 ( { 𝑞 } × dom ( 𝑓 ‘ 𝑞 ) ) ) ↔ ( 0 ..^ ( ♯ ‘ ∪ 𝑞 ∈ 𝐴 ( { 𝑞 } × dom ( 𝑓 ‘ 𝑞 ) ) ) ) ≈ ∪ 𝑞 ∈ 𝐴 ( { 𝑞 } × dom ( 𝑓 ‘ 𝑞 ) ) ) )
157 155 151 156 sylancr ⊢ ( ( 𝜑 ∧ ( 𝑓 : 𝐴 ⟶ Word 𝐶 ∧ ∀ 𝑞 ∈ 𝐴 ( 𝑓 ‘ 𝑞 ) ∈ ( 𝑊 ‘ ( 𝑆 ‘ 𝑞 ) ) ) ) → ( ( ♯ ‘ ( 0 ..^ ( ♯ ‘ ∪ 𝑞 ∈ 𝐴 ( { 𝑞 } × dom ( 𝑓 ‘ 𝑞 ) ) ) ) ) = ( ♯ ‘ ∪ 𝑞 ∈ 𝐴 ( { 𝑞 } × dom ( 𝑓 ‘ 𝑞 ) ) ) ↔ ( 0 ..^ ( ♯ ‘ ∪ 𝑞 ∈ 𝐴 ( { 𝑞 } × dom ( 𝑓 ‘ 𝑞 ) ) ) ) ≈ ∪ 𝑞 ∈ 𝐴 ( { 𝑞 } × dom ( 𝑓 ‘ 𝑞 ) ) ) )
158 154 157 mpbid ⊢ ( ( 𝜑 ∧ ( 𝑓 : 𝐴 ⟶ Word 𝐶 ∧ ∀ 𝑞 ∈ 𝐴 ( 𝑓 ‘ 𝑞 ) ∈ ( 𝑊 ‘ ( 𝑆 ‘ 𝑞 ) ) ) ) → ( 0 ..^ ( ♯ ‘ ∪ 𝑞 ∈ 𝐴 ( { 𝑞 } × dom ( 𝑓 ‘ 𝑞 ) ) ) ) ≈ ∪ 𝑞 ∈ 𝐴 ( { 𝑞 } × dom ( 𝑓 ‘ 𝑞 ) ) )
159 bren ⊢ ( ( 0 ..^ ( ♯ ‘ ∪ 𝑞 ∈ 𝐴 ( { 𝑞 } × dom ( 𝑓 ‘ 𝑞 ) ) ) ) ≈ ∪ 𝑞 ∈ 𝐴 ( { 𝑞 } × dom ( 𝑓 ‘ 𝑞 ) ) ↔ ∃ ℎ ℎ : ( 0 ..^ ( ♯ ‘ ∪ 𝑞 ∈ 𝐴 ( { 𝑞 } × dom ( 𝑓 ‘ 𝑞 ) ) ) ) –1-1-onto→ ∪ 𝑞 ∈ 𝐴 ( { 𝑞 } × dom ( 𝑓 ‘ 𝑞 ) ) )
160 158 159 sylib ⊢ ( ( 𝜑 ∧ ( 𝑓 : 𝐴 ⟶ Word 𝐶 ∧ ∀ 𝑞 ∈ 𝐴 ( 𝑓 ‘ 𝑞 ) ∈ ( 𝑊 ‘ ( 𝑆 ‘ 𝑞 ) ) ) ) → ∃ ℎ ℎ : ( 0 ..^ ( ♯ ‘ ∪ 𝑞 ∈ 𝐴 ( { 𝑞 } × dom ( 𝑓 ‘ 𝑞 ) ) ) ) –1-1-onto→ ∪ 𝑞 ∈ 𝐴 ( { 𝑞 } × dom ( 𝑓 ‘ 𝑞 ) ) )
161 3 adantr ⊢ ( ( 𝜑 ∧ ( ( 𝑓 : 𝐴 ⟶ Word 𝐶 ∧ ∀ 𝑞 ∈ 𝐴 ( 𝑓 ‘ 𝑞 ) ∈ ( 𝑊 ‘ ( 𝑆 ‘ 𝑞 ) ) ) ∧ ℎ : ( 0 ..^ ( ♯ ‘ ∪ 𝑞 ∈ 𝐴 ( { 𝑞 } × dom ( 𝑓 ‘ 𝑞 ) ) ) ) –1-1-onto→ ∪ 𝑞 ∈ 𝐴 ( { 𝑞 } × dom ( 𝑓 ‘ 𝑞 ) ) ) ) → 𝐺 ∈ Abel )
162 4 adantr ⊢ ( ( 𝜑 ∧ ( ( 𝑓 : 𝐴 ⟶ Word 𝐶 ∧ ∀ 𝑞 ∈ 𝐴 ( 𝑓 ‘ 𝑞 ) ∈ ( 𝑊 ‘ ( 𝑆 ‘ 𝑞 ) ) ) ∧ ℎ : ( 0 ..^ ( ♯ ‘ ∪ 𝑞 ∈ 𝐴 ( { 𝑞 } × dom ( 𝑓 ‘ 𝑞 ) ) ) ) –1-1-onto→ ∪ 𝑞 ∈ 𝐴 ( { 𝑞 } × dom ( 𝑓 ‘ 𝑞 ) ) ) ) → 𝐵 ∈ Fin )
163 breq1 ⊢ ( 𝑤 = 𝑎 → ( 𝑤 ∥ ( ♯ ‘ 𝐵 ) ↔ 𝑎 ∥ ( ♯ ‘ 𝐵 ) ) )
164 163 cbvrabv ⊢ { 𝑤 ∈ ℙ ∣ 𝑤 ∥ ( ♯ ‘ 𝐵 ) } = { 𝑎 ∈ ℙ ∣ 𝑎 ∥ ( ♯ ‘ 𝐵 ) }
165 6 164 eqtri ⊢ 𝐴 = { 𝑎 ∈ ℙ ∣ 𝑎 ∥ ( ♯ ‘ 𝐵 ) }
166 fveq2 ⊢ ( 𝑥 = 𝑐 → ( 𝑂 ‘ 𝑥 ) = ( 𝑂 ‘ 𝑐 ) )
167 166 breq1d ⊢ ( 𝑥 = 𝑐 → ( ( 𝑂 ‘ 𝑥 ) ∥ ( 𝑝 ↑ ( 𝑝 pCnt ( ♯ ‘ 𝐵 ) ) ) ↔ ( 𝑂 ‘ 𝑐 ) ∥ ( 𝑝 ↑ ( 𝑝 pCnt ( ♯ ‘ 𝐵 ) ) ) ) )
168 167 cbvrabv ⊢ { 𝑥 ∈ 𝐵 ∣ ( 𝑂 ‘ 𝑥 ) ∥ ( 𝑝 ↑ ( 𝑝 pCnt ( ♯ ‘ 𝐵 ) ) ) } = { 𝑐 ∈ 𝐵 ∣ ( 𝑂 ‘ 𝑐 ) ∥ ( 𝑝 ↑ ( 𝑝 pCnt ( ♯ ‘ 𝐵 ) ) ) }
169 id ⊢ ( 𝑝 = 𝑏 → 𝑝 = 𝑏 )
170 oveq1 ⊢ ( 𝑝 = 𝑏 → ( 𝑝 pCnt ( ♯ ‘ 𝐵 ) ) = ( 𝑏 pCnt ( ♯ ‘ 𝐵 ) ) )
171 169 170 oveq12d ⊢ ( 𝑝 = 𝑏 → ( 𝑝 ↑ ( 𝑝 pCnt ( ♯ ‘ 𝐵 ) ) ) = ( 𝑏 ↑ ( 𝑏 pCnt ( ♯ ‘ 𝐵 ) ) ) )
172 171 breq2d ⊢ ( 𝑝 = 𝑏 → ( ( 𝑂 ‘ 𝑐 ) ∥ ( 𝑝 ↑ ( 𝑝 pCnt ( ♯ ‘ 𝐵 ) ) ) ↔ ( 𝑂 ‘ 𝑐 ) ∥ ( 𝑏 ↑ ( 𝑏 pCnt ( ♯ ‘ 𝐵 ) ) ) ) )
173 172 rabbidv ⊢ ( 𝑝 = 𝑏 → { 𝑐 ∈ 𝐵 ∣ ( 𝑂 ‘ 𝑐 ) ∥ ( 𝑝 ↑ ( 𝑝 pCnt ( ♯ ‘ 𝐵 ) ) ) } = { 𝑐 ∈ 𝐵 ∣ ( 𝑂 ‘ 𝑐 ) ∥ ( 𝑏 ↑ ( 𝑏 pCnt ( ♯ ‘ 𝐵 ) ) ) } )
174 168 173 eqtrid ⊢ ( 𝑝 = 𝑏 → { 𝑥 ∈ 𝐵 ∣ ( 𝑂 ‘ 𝑥 ) ∥ ( 𝑝 ↑ ( 𝑝 pCnt ( ♯ ‘ 𝐵 ) ) ) } = { 𝑐 ∈ 𝐵 ∣ ( 𝑂 ‘ 𝑐 ) ∥ ( 𝑏 ↑ ( 𝑏 pCnt ( ♯ ‘ 𝐵 ) ) ) } )
175 174 cbvmptv ⊢ ( 𝑝 ∈ 𝐴 ↦ { 𝑥 ∈ 𝐵 ∣ ( 𝑂 ‘ 𝑥 ) ∥ ( 𝑝 ↑ ( 𝑝 pCnt ( ♯ ‘ 𝐵 ) ) ) } ) = ( 𝑏 ∈ 𝐴 ↦ { 𝑐 ∈ 𝐵 ∣ ( 𝑂 ‘ 𝑐 ) ∥ ( 𝑏 ↑ ( 𝑏 pCnt ( ♯ ‘ 𝐵 ) ) ) } )
176 7 175 eqtri ⊢ 𝑆 = ( 𝑏 ∈ 𝐴 ↦ { 𝑐 ∈ 𝐵 ∣ ( 𝑂 ‘ 𝑐 ) ∥ ( 𝑏 ↑ ( 𝑏 pCnt ( ♯ ‘ 𝐵 ) ) ) } )
177 breq2 ⊢ ( 𝑠 = 𝑡 → ( 𝐺 dom DProd 𝑠 ↔ 𝐺 dom DProd 𝑡 ) )
178 oveq2 ⊢ ( 𝑠 = 𝑡 → ( 𝐺 DProd 𝑠 ) = ( 𝐺 DProd 𝑡 ) )
179 178 eqeq1d ⊢ ( 𝑠 = 𝑡 → ( ( 𝐺 DProd 𝑠 ) = 𝑔 ↔ ( 𝐺 DProd 𝑡 ) = 𝑔 ) )
180 177 179 anbi12d ⊢ ( 𝑠 = 𝑡 → ( ( 𝐺 dom DProd 𝑠 ∧ ( 𝐺 DProd 𝑠 ) = 𝑔 ) ↔ ( 𝐺 dom DProd 𝑡 ∧ ( 𝐺 DProd 𝑡 ) = 𝑔 ) ) )
181 180 cbvrabv ⊢ { 𝑠 ∈ Word 𝐶 ∣ ( 𝐺 dom DProd 𝑠 ∧ ( 𝐺 DProd 𝑠 ) = 𝑔 ) } = { 𝑡 ∈ Word 𝐶 ∣ ( 𝐺 dom DProd 𝑡 ∧ ( 𝐺 DProd 𝑡 ) = 𝑔 ) }
182 181 mpteq2i ⊢ ( 𝑔 ∈ ( SubGrp ‘ 𝐺 ) ↦ { 𝑠 ∈ Word 𝐶 ∣ ( 𝐺 dom DProd 𝑠 ∧ ( 𝐺 DProd 𝑠 ) = 𝑔 ) } ) = ( 𝑔 ∈ ( SubGrp ‘ 𝐺 ) ↦ { 𝑡 ∈ Word 𝐶 ∣ ( 𝐺 dom DProd 𝑡 ∧ ( 𝐺 DProd 𝑡 ) = 𝑔 ) } )
183 8 182 eqtri ⊢ 𝑊 = ( 𝑔 ∈ ( SubGrp ‘ 𝐺 ) ↦ { 𝑡 ∈ Word 𝐶 ∣ ( 𝐺 dom DProd 𝑡 ∧ ( 𝐺 DProd 𝑡 ) = 𝑔 ) } )
184 simprll ⊢ ( ( 𝜑 ∧ ( ( 𝑓 : 𝐴 ⟶ Word 𝐶 ∧ ∀ 𝑞 ∈ 𝐴 ( 𝑓 ‘ 𝑞 ) ∈ ( 𝑊 ‘ ( 𝑆 ‘ 𝑞 ) ) ) ∧ ℎ : ( 0 ..^ ( ♯ ‘ ∪ 𝑞 ∈ 𝐴 ( { 𝑞 } × dom ( 𝑓 ‘ 𝑞 ) ) ) ) –1-1-onto→ ∪ 𝑞 ∈ 𝐴 ( { 𝑞 } × dom ( 𝑓 ‘ 𝑞 ) ) ) ) → 𝑓 : 𝐴 ⟶ Word 𝐶 )
185 simprlr ⊢ ( ( 𝜑 ∧ ( ( 𝑓 : 𝐴 ⟶ Word 𝐶 ∧ ∀ 𝑞 ∈ 𝐴 ( 𝑓 ‘ 𝑞 ) ∈ ( 𝑊 ‘ ( 𝑆 ‘ 𝑞 ) ) ) ∧ ℎ : ( 0 ..^ ( ♯ ‘ ∪ 𝑞 ∈ 𝐴 ( { 𝑞 } × dom ( 𝑓 ‘ 𝑞 ) ) ) ) –1-1-onto→ ∪ 𝑞 ∈ 𝐴 ( { 𝑞 } × dom ( 𝑓 ‘ 𝑞 ) ) ) ) → ∀ 𝑞 ∈ 𝐴 ( 𝑓 ‘ 𝑞 ) ∈ ( 𝑊 ‘ ( 𝑆 ‘ 𝑞 ) ) )
186 2fveq3 ⊢ ( 𝑞 = 𝑦 → ( 𝑊 ‘ ( 𝑆 ‘ 𝑞 ) ) = ( 𝑊 ‘ ( 𝑆 ‘ 𝑦 ) ) )
187 134 186 eleq12d ⊢ ( 𝑞 = 𝑦 → ( ( 𝑓 ‘ 𝑞 ) ∈ ( 𝑊 ‘ ( 𝑆 ‘ 𝑞 ) ) ↔ ( 𝑓 ‘ 𝑦 ) ∈ ( 𝑊 ‘ ( 𝑆 ‘ 𝑦 ) ) ) )
188 187 cbvralvw ⊢ ( ∀ 𝑞 ∈ 𝐴 ( 𝑓 ‘ 𝑞 ) ∈ ( 𝑊 ‘ ( 𝑆 ‘ 𝑞 ) ) ↔ ∀ 𝑦 ∈ 𝐴 ( 𝑓 ‘ 𝑦 ) ∈ ( 𝑊 ‘ ( 𝑆 ‘ 𝑦 ) ) )
189 185 188 sylib ⊢ ( ( 𝜑 ∧ ( ( 𝑓 : 𝐴 ⟶ Word 𝐶 ∧ ∀ 𝑞 ∈ 𝐴 ( 𝑓 ‘ 𝑞 ) ∈ ( 𝑊 ‘ ( 𝑆 ‘ 𝑞 ) ) ) ∧ ℎ : ( 0 ..^ ( ♯ ‘ ∪ 𝑞 ∈ 𝐴 ( { 𝑞 } × dom ( 𝑓 ‘ 𝑞 ) ) ) ) –1-1-onto→ ∪ 𝑞 ∈ 𝐴 ( { 𝑞 } × dom ( 𝑓 ‘ 𝑞 ) ) ) ) → ∀ 𝑦 ∈ 𝐴 ( 𝑓 ‘ 𝑦 ) ∈ ( 𝑊 ‘ ( 𝑆 ‘ 𝑦 ) ) )
190 simprr ⊢ ( ( 𝜑 ∧ ( ( 𝑓 : 𝐴 ⟶ Word 𝐶 ∧ ∀ 𝑞 ∈ 𝐴 ( 𝑓 ‘ 𝑞 ) ∈ ( 𝑊 ‘ ( 𝑆 ‘ 𝑞 ) ) ) ∧ ℎ : ( 0 ..^ ( ♯ ‘ ∪ 𝑞 ∈ 𝐴 ( { 𝑞 } × dom ( 𝑓 ‘ 𝑞 ) ) ) ) –1-1-onto→ ∪ 𝑞 ∈ 𝐴 ( { 𝑞 } × dom ( 𝑓 ‘ 𝑞 ) ) ) ) → ℎ : ( 0 ..^ ( ♯ ‘ ∪ 𝑞 ∈ 𝐴 ( { 𝑞 } × dom ( 𝑓 ‘ 𝑞 ) ) ) ) –1-1-onto→ ∪ 𝑞 ∈ 𝐴 ( { 𝑞 } × dom ( 𝑓 ‘ 𝑞 ) ) )
191 1 2 161 162 5 165 176 183 184 189 137 190 ablfaclem2 ⊢ ( ( 𝜑 ∧ ( ( 𝑓 : 𝐴 ⟶ Word 𝐶 ∧ ∀ 𝑞 ∈ 𝐴 ( 𝑓 ‘ 𝑞 ) ∈ ( 𝑊 ‘ ( 𝑆 ‘ 𝑞 ) ) ) ∧ ℎ : ( 0 ..^ ( ♯ ‘ ∪ 𝑞 ∈ 𝐴 ( { 𝑞 } × dom ( 𝑓 ‘ 𝑞 ) ) ) ) –1-1-onto→ ∪ 𝑞 ∈ 𝐴 ( { 𝑞 } × dom ( 𝑓 ‘ 𝑞 ) ) ) ) → ( 𝑊 ‘ 𝐵 ) ≠ ∅ )
192 191 expr ⊢ ( ( 𝜑 ∧ ( 𝑓 : 𝐴 ⟶ Word 𝐶 ∧ ∀ 𝑞 ∈ 𝐴 ( 𝑓 ‘ 𝑞 ) ∈ ( 𝑊 ‘ ( 𝑆 ‘ 𝑞 ) ) ) ) → ( ℎ : ( 0 ..^ ( ♯ ‘ ∪ 𝑞 ∈ 𝐴 ( { 𝑞 } × dom ( 𝑓 ‘ 𝑞 ) ) ) ) –1-1-onto→ ∪ 𝑞 ∈ 𝐴 ( { 𝑞 } × dom ( 𝑓 ‘ 𝑞 ) ) → ( 𝑊 ‘ 𝐵 ) ≠ ∅ ) )
193 192 exlimdv ⊢ ( ( 𝜑 ∧ ( 𝑓 : 𝐴 ⟶ Word 𝐶 ∧ ∀ 𝑞 ∈ 𝐴 ( 𝑓 ‘ 𝑞 ) ∈ ( 𝑊 ‘ ( 𝑆 ‘ 𝑞 ) ) ) ) → ( ∃ ℎ ℎ : ( 0 ..^ ( ♯ ‘ ∪ 𝑞 ∈ 𝐴 ( { 𝑞 } × dom ( 𝑓 ‘ 𝑞 ) ) ) ) –1-1-onto→ ∪ 𝑞 ∈ 𝐴 ( { 𝑞 } × dom ( 𝑓 ‘ 𝑞 ) ) → ( 𝑊 ‘ 𝐵 ) ≠ ∅ ) )
194 160 193 mpd ⊢ ( ( 𝜑 ∧ ( 𝑓 : 𝐴 ⟶ Word 𝐶 ∧ ∀ 𝑞 ∈ 𝐴 ( 𝑓 ‘ 𝑞 ) ∈ ( 𝑊 ‘ ( 𝑆 ‘ 𝑞 ) ) ) ) → ( 𝑊 ‘ 𝐵 ) ≠ ∅ )
195 132 194 exlimddv ⊢ ( 𝜑 → ( 𝑊 ‘ 𝐵 ) ≠ ∅ )