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

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 ⊢ 𝐵 = ( Base ‘ 𝐺 )
ablfac.c ⊢ 𝐶 = { 𝑟 ∈ ( SubGrp ‘ 𝐺 ) ∣ ( 𝐺 ↾s 𝑟 ) ∈ ( CycGrp ∩ ran pGrp ) }
ablfac.1 ⊢ ( 𝜑 → 𝐺 ∈ Abel )
ablfac.2 ⊢ ( 𝜑 → 𝐵 ∈ Fin )
ablfac2.m ⊢ · = ( .g ‘ 𝐺 )
ablfac2.s ⊢ 𝑆 = ( 𝑘 ∈ dom 𝑤 ↦ ran ( 𝑛 ∈ ℤ ↦ ( 𝑛 · ( 𝑤 ‘ 𝑘 ) ) ) )
Assertion ablfac2 ( 𝜑 → ∃ 𝑤 ∈ Word 𝐵 ( 𝑆 : dom 𝑤 ⟶ 𝐶 ∧ 𝐺 dom DProd 𝑆 ∧ ( 𝐺 DProd 𝑆 ) = 𝐵 ) )

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 ablfac2.m ⊢ · = ( .g ‘ 𝐺 )
6 ablfac2.s ⊢ 𝑆 = ( 𝑘 ∈ dom 𝑤 ↦ ran ( 𝑛 ∈ ℤ ↦ ( 𝑛 · ( 𝑤 ‘ 𝑘 ) ) ) )
7 wrdf ⊢ ( 𝑠 ∈ Word 𝐶 → 𝑠 : ( 0 ..^ ( ♯ ‘ 𝑠 ) ) ⟶ 𝐶 )
8 7 ad2antlr ⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ Word 𝐶 ) ∧ ( 𝐺 dom DProd 𝑠 ∧ ( 𝐺 DProd 𝑠 ) = 𝐵 ) ) → 𝑠 : ( 0 ..^ ( ♯ ‘ 𝑠 ) ) ⟶ 𝐶 )
9 8 fdmd ⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ Word 𝐶 ) ∧ ( 𝐺 dom DProd 𝑠 ∧ ( 𝐺 DProd 𝑠 ) = 𝐵 ) ) → dom 𝑠 = ( 0 ..^ ( ♯ ‘ 𝑠 ) ) )
10 fzofi ⊢ ( 0 ..^ ( ♯ ‘ 𝑠 ) ) ∈ Fin
11 9 10 eqeltrdi ⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ Word 𝐶 ) ∧ ( 𝐺 dom DProd 𝑠 ∧ ( 𝐺 DProd 𝑠 ) = 𝐵 ) ) → dom 𝑠 ∈ Fin )
12 8 ffdmd ⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ Word 𝐶 ) ∧ ( 𝐺 dom DProd 𝑠 ∧ ( 𝐺 DProd 𝑠 ) = 𝐵 ) ) → 𝑠 : dom 𝑠 ⟶ 𝐶 )
13 12 ffvelcdmda ⊢ ( ( ( ( 𝜑 ∧ 𝑠 ∈ Word 𝐶 ) ∧ ( 𝐺 dom DProd 𝑠 ∧ ( 𝐺 DProd 𝑠 ) = 𝐵 ) ) ∧ 𝑘 ∈ dom 𝑠 ) → ( 𝑠 ‘ 𝑘 ) ∈ 𝐶 )
14 oveq2 ⊢ ( 𝑟 = ( 𝑠 ‘ 𝑘 ) → ( 𝐺 ↾s 𝑟 ) = ( 𝐺 ↾s ( 𝑠 ‘ 𝑘 ) ) )
15 14 eleq1d ⊢ ( 𝑟 = ( 𝑠 ‘ 𝑘 ) → ( ( 𝐺 ↾s 𝑟 ) ∈ ( CycGrp ∩ ran pGrp ) ↔ ( 𝐺 ↾s ( 𝑠 ‘ 𝑘 ) ) ∈ ( CycGrp ∩ ran pGrp ) ) )
16 15 2 elrab2 ⊢ ( ( 𝑠 ‘ 𝑘 ) ∈ 𝐶 ↔ ( ( 𝑠 ‘ 𝑘 ) ∈ ( SubGrp ‘ 𝐺 ) ∧ ( 𝐺 ↾s ( 𝑠 ‘ 𝑘 ) ) ∈ ( CycGrp ∩ ran pGrp ) ) )
17 16 simplbi ⊢ ( ( 𝑠 ‘ 𝑘 ) ∈ 𝐶 → ( 𝑠 ‘ 𝑘 ) ∈ ( SubGrp ‘ 𝐺 ) )
18 13 17 syl ⊢ ( ( ( ( 𝜑 ∧ 𝑠 ∈ Word 𝐶 ) ∧ ( 𝐺 dom DProd 𝑠 ∧ ( 𝐺 DProd 𝑠 ) = 𝐵 ) ) ∧ 𝑘 ∈ dom 𝑠 ) → ( 𝑠 ‘ 𝑘 ) ∈ ( SubGrp ‘ 𝐺 ) )
19 1 subgss ⊢ ( ( 𝑠 ‘ 𝑘 ) ∈ ( SubGrp ‘ 𝐺 ) → ( 𝑠 ‘ 𝑘 ) ⊆ 𝐵 )
20 18 19 syl ⊢ ( ( ( ( 𝜑 ∧ 𝑠 ∈ Word 𝐶 ) ∧ ( 𝐺 dom DProd 𝑠 ∧ ( 𝐺 DProd 𝑠 ) = 𝐵 ) ) ∧ 𝑘 ∈ dom 𝑠 ) → ( 𝑠 ‘ 𝑘 ) ⊆ 𝐵 )
21 16 simprbi ⊢ ( ( 𝑠 ‘ 𝑘 ) ∈ 𝐶 → ( 𝐺 ↾s ( 𝑠 ‘ 𝑘 ) ) ∈ ( CycGrp ∩ ran pGrp ) )
22 13 21 syl ⊢ ( ( ( ( 𝜑 ∧ 𝑠 ∈ Word 𝐶 ) ∧ ( 𝐺 dom DProd 𝑠 ∧ ( 𝐺 DProd 𝑠 ) = 𝐵 ) ) ∧ 𝑘 ∈ dom 𝑠 ) → ( 𝐺 ↾s ( 𝑠 ‘ 𝑘 ) ) ∈ ( CycGrp ∩ ran pGrp ) )
23 22 elin1d ⊢ ( ( ( ( 𝜑 ∧ 𝑠 ∈ Word 𝐶 ) ∧ ( 𝐺 dom DProd 𝑠 ∧ ( 𝐺 DProd 𝑠 ) = 𝐵 ) ) ∧ 𝑘 ∈ dom 𝑠 ) → ( 𝐺 ↾s ( 𝑠 ‘ 𝑘 ) ) ∈ CycGrp )
24 eqid ⊢ ( Base ‘ ( 𝐺 ↾s ( 𝑠 ‘ 𝑘 ) ) ) = ( Base ‘ ( 𝐺 ↾s ( 𝑠 ‘ 𝑘 ) ) )
25 eqid ⊢ ( .g ‘ ( 𝐺 ↾s ( 𝑠 ‘ 𝑘 ) ) ) = ( .g ‘ ( 𝐺 ↾s ( 𝑠 ‘ 𝑘 ) ) )
26 24 25 iscyg ⊢ ( ( 𝐺 ↾s ( 𝑠 ‘ 𝑘 ) ) ∈ CycGrp ↔ ( ( 𝐺 ↾s ( 𝑠 ‘ 𝑘 ) ) ∈ Grp ∧ ∃ 𝑥 ∈ ( Base ‘ ( 𝐺 ↾s ( 𝑠 ‘ 𝑘 ) ) ) ran ( 𝑛 ∈ ℤ ↦ ( 𝑛 ( .g ‘ ( 𝐺 ↾s ( 𝑠 ‘ 𝑘 ) ) ) 𝑥 ) ) = ( Base ‘ ( 𝐺 ↾s ( 𝑠 ‘ 𝑘 ) ) ) ) )
27 26 simprbi ⊢ ( ( 𝐺 ↾s ( 𝑠 ‘ 𝑘 ) ) ∈ CycGrp → ∃ 𝑥 ∈ ( Base ‘ ( 𝐺 ↾s ( 𝑠 ‘ 𝑘 ) ) ) ran ( 𝑛 ∈ ℤ ↦ ( 𝑛 ( .g ‘ ( 𝐺 ↾s ( 𝑠 ‘ 𝑘 ) ) ) 𝑥 ) ) = ( Base ‘ ( 𝐺 ↾s ( 𝑠 ‘ 𝑘 ) ) ) )
28 23 27 syl ⊢ ( ( ( ( 𝜑 ∧ 𝑠 ∈ Word 𝐶 ) ∧ ( 𝐺 dom DProd 𝑠 ∧ ( 𝐺 DProd 𝑠 ) = 𝐵 ) ) ∧ 𝑘 ∈ dom 𝑠 ) → ∃ 𝑥 ∈ ( Base ‘ ( 𝐺 ↾s ( 𝑠 ‘ 𝑘 ) ) ) ran ( 𝑛 ∈ ℤ ↦ ( 𝑛 ( .g ‘ ( 𝐺 ↾s ( 𝑠 ‘ 𝑘 ) ) ) 𝑥 ) ) = ( Base ‘ ( 𝐺 ↾s ( 𝑠 ‘ 𝑘 ) ) ) )
29 eqid ⊢ ( 𝐺 ↾s ( 𝑠 ‘ 𝑘 ) ) = ( 𝐺 ↾s ( 𝑠 ‘ 𝑘 ) )
30 29 subgbas ⊢ ( ( 𝑠 ‘ 𝑘 ) ∈ ( SubGrp ‘ 𝐺 ) → ( 𝑠 ‘ 𝑘 ) = ( Base ‘ ( 𝐺 ↾s ( 𝑠 ‘ 𝑘 ) ) ) )
31 18 30 syl ⊢ ( ( ( ( 𝜑 ∧ 𝑠 ∈ Word 𝐶 ) ∧ ( 𝐺 dom DProd 𝑠 ∧ ( 𝐺 DProd 𝑠 ) = 𝐵 ) ) ∧ 𝑘 ∈ dom 𝑠 ) → ( 𝑠 ‘ 𝑘 ) = ( Base ‘ ( 𝐺 ↾s ( 𝑠 ‘ 𝑘 ) ) ) )
32 28 31 rexeqtrrdv ⊢ ( ( ( ( 𝜑 ∧ 𝑠 ∈ Word 𝐶 ) ∧ ( 𝐺 dom DProd 𝑠 ∧ ( 𝐺 DProd 𝑠 ) = 𝐵 ) ) ∧ 𝑘 ∈ dom 𝑠 ) → ∃ 𝑥 ∈ ( 𝑠 ‘ 𝑘 ) ran ( 𝑛 ∈ ℤ ↦ ( 𝑛 ( .g ‘ ( 𝐺 ↾s ( 𝑠 ‘ 𝑘 ) ) ) 𝑥 ) ) = ( Base ‘ ( 𝐺 ↾s ( 𝑠 ‘ 𝑘 ) ) ) )
33 18 ad2antrr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑠 ∈ Word 𝐶 ) ∧ ( 𝐺 dom DProd 𝑠 ∧ ( 𝐺 DProd 𝑠 ) = 𝐵 ) ) ∧ 𝑘 ∈ dom 𝑠 ) ∧ 𝑥 ∈ ( 𝑠 ‘ 𝑘 ) ) ∧ 𝑛 ∈ ℤ ) → ( 𝑠 ‘ 𝑘 ) ∈ ( SubGrp ‘ 𝐺 ) )
34 simpr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑠 ∈ Word 𝐶 ) ∧ ( 𝐺 dom DProd 𝑠 ∧ ( 𝐺 DProd 𝑠 ) = 𝐵 ) ) ∧ 𝑘 ∈ dom 𝑠 ) ∧ 𝑥 ∈ ( 𝑠 ‘ 𝑘 ) ) ∧ 𝑛 ∈ ℤ ) → 𝑛 ∈ ℤ )
35 simplr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑠 ∈ Word 𝐶 ) ∧ ( 𝐺 dom DProd 𝑠 ∧ ( 𝐺 DProd 𝑠 ) = 𝐵 ) ) ∧ 𝑘 ∈ dom 𝑠 ) ∧ 𝑥 ∈ ( 𝑠 ‘ 𝑘 ) ) ∧ 𝑛 ∈ ℤ ) → 𝑥 ∈ ( 𝑠 ‘ 𝑘 ) )
36 5 29 25 subgmulg ⊢ ( ( ( 𝑠 ‘ 𝑘 ) ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑛 ∈ ℤ ∧ 𝑥 ∈ ( 𝑠 ‘ 𝑘 ) ) → ( 𝑛 · 𝑥 ) = ( 𝑛 ( .g ‘ ( 𝐺 ↾s ( 𝑠 ‘ 𝑘 ) ) ) 𝑥 ) )
37 33 34 35 36 syl3anc ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑠 ∈ Word 𝐶 ) ∧ ( 𝐺 dom DProd 𝑠 ∧ ( 𝐺 DProd 𝑠 ) = 𝐵 ) ) ∧ 𝑘 ∈ dom 𝑠 ) ∧ 𝑥 ∈ ( 𝑠 ‘ 𝑘 ) ) ∧ 𝑛 ∈ ℤ ) → ( 𝑛 · 𝑥 ) = ( 𝑛 ( .g ‘ ( 𝐺 ↾s ( 𝑠 ‘ 𝑘 ) ) ) 𝑥 ) )
38 37 mpteq2dva ⊢ ( ( ( ( ( 𝜑 ∧ 𝑠 ∈ Word 𝐶 ) ∧ ( 𝐺 dom DProd 𝑠 ∧ ( 𝐺 DProd 𝑠 ) = 𝐵 ) ) ∧ 𝑘 ∈ dom 𝑠 ) ∧ 𝑥 ∈ ( 𝑠 ‘ 𝑘 ) ) → ( 𝑛 ∈ ℤ ↦ ( 𝑛 · 𝑥 ) ) = ( 𝑛 ∈ ℤ ↦ ( 𝑛 ( .g ‘ ( 𝐺 ↾s ( 𝑠 ‘ 𝑘 ) ) ) 𝑥 ) ) )
39 38 rneqd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑠 ∈ Word 𝐶 ) ∧ ( 𝐺 dom DProd 𝑠 ∧ ( 𝐺 DProd 𝑠 ) = 𝐵 ) ) ∧ 𝑘 ∈ dom 𝑠 ) ∧ 𝑥 ∈ ( 𝑠 ‘ 𝑘 ) ) → ran ( 𝑛 ∈ ℤ ↦ ( 𝑛 · 𝑥 ) ) = ran ( 𝑛 ∈ ℤ ↦ ( 𝑛 ( .g ‘ ( 𝐺 ↾s ( 𝑠 ‘ 𝑘 ) ) ) 𝑥 ) ) )
40 31 adantr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑠 ∈ Word 𝐶 ) ∧ ( 𝐺 dom DProd 𝑠 ∧ ( 𝐺 DProd 𝑠 ) = 𝐵 ) ) ∧ 𝑘 ∈ dom 𝑠 ) ∧ 𝑥 ∈ ( 𝑠 ‘ 𝑘 ) ) → ( 𝑠 ‘ 𝑘 ) = ( Base ‘ ( 𝐺 ↾s ( 𝑠 ‘ 𝑘 ) ) ) )
41 39 40 eqeq12d ⊢ ( ( ( ( ( 𝜑 ∧ 𝑠 ∈ Word 𝐶 ) ∧ ( 𝐺 dom DProd 𝑠 ∧ ( 𝐺 DProd 𝑠 ) = 𝐵 ) ) ∧ 𝑘 ∈ dom 𝑠 ) ∧ 𝑥 ∈ ( 𝑠 ‘ 𝑘 ) ) → ( ran ( 𝑛 ∈ ℤ ↦ ( 𝑛 · 𝑥 ) ) = ( 𝑠 ‘ 𝑘 ) ↔ ran ( 𝑛 ∈ ℤ ↦ ( 𝑛 ( .g ‘ ( 𝐺 ↾s ( 𝑠 ‘ 𝑘 ) ) ) 𝑥 ) ) = ( Base ‘ ( 𝐺 ↾s ( 𝑠 ‘ 𝑘 ) ) ) ) )
42 41 rexbidva ⊢ ( ( ( ( 𝜑 ∧ 𝑠 ∈ Word 𝐶 ) ∧ ( 𝐺 dom DProd 𝑠 ∧ ( 𝐺 DProd 𝑠 ) = 𝐵 ) ) ∧ 𝑘 ∈ dom 𝑠 ) → ( ∃ 𝑥 ∈ ( 𝑠 ‘ 𝑘 ) ran ( 𝑛 ∈ ℤ ↦ ( 𝑛 · 𝑥 ) ) = ( 𝑠 ‘ 𝑘 ) ↔ ∃ 𝑥 ∈ ( 𝑠 ‘ 𝑘 ) ran ( 𝑛 ∈ ℤ ↦ ( 𝑛 ( .g ‘ ( 𝐺 ↾s ( 𝑠 ‘ 𝑘 ) ) ) 𝑥 ) ) = ( Base ‘ ( 𝐺 ↾s ( 𝑠 ‘ 𝑘 ) ) ) ) )
43 32 42 mpbird ⊢ ( ( ( ( 𝜑 ∧ 𝑠 ∈ Word 𝐶 ) ∧ ( 𝐺 dom DProd 𝑠 ∧ ( 𝐺 DProd 𝑠 ) = 𝐵 ) ) ∧ 𝑘 ∈ dom 𝑠 ) → ∃ 𝑥 ∈ ( 𝑠 ‘ 𝑘 ) ran ( 𝑛 ∈ ℤ ↦ ( 𝑛 · 𝑥 ) ) = ( 𝑠 ‘ 𝑘 ) )
44 ssrexv ⊢ ( ( 𝑠 ‘ 𝑘 ) ⊆ 𝐵 → ( ∃ 𝑥 ∈ ( 𝑠 ‘ 𝑘 ) ran ( 𝑛 ∈ ℤ ↦ ( 𝑛 · 𝑥 ) ) = ( 𝑠 ‘ 𝑘 ) → ∃ 𝑥 ∈ 𝐵 ran ( 𝑛 ∈ ℤ ↦ ( 𝑛 · 𝑥 ) ) = ( 𝑠 ‘ 𝑘 ) ) )
45 20 43 44 sylc ⊢ ( ( ( ( 𝜑 ∧ 𝑠 ∈ Word 𝐶 ) ∧ ( 𝐺 dom DProd 𝑠 ∧ ( 𝐺 DProd 𝑠 ) = 𝐵 ) ) ∧ 𝑘 ∈ dom 𝑠 ) → ∃ 𝑥 ∈ 𝐵 ran ( 𝑛 ∈ ℤ ↦ ( 𝑛 · 𝑥 ) ) = ( 𝑠 ‘ 𝑘 ) )
46 45 ralrimiva ⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ Word 𝐶 ) ∧ ( 𝐺 dom DProd 𝑠 ∧ ( 𝐺 DProd 𝑠 ) = 𝐵 ) ) → ∀ 𝑘 ∈ dom 𝑠 ∃ 𝑥 ∈ 𝐵 ran ( 𝑛 ∈ ℤ ↦ ( 𝑛 · 𝑥 ) ) = ( 𝑠 ‘ 𝑘 ) )
47 oveq2 ⊢ ( 𝑥 = ( 𝑤 ‘ 𝑘 ) → ( 𝑛 · 𝑥 ) = ( 𝑛 · ( 𝑤 ‘ 𝑘 ) ) )
48 47 mpteq2dv ⊢ ( 𝑥 = ( 𝑤 ‘ 𝑘 ) → ( 𝑛 ∈ ℤ ↦ ( 𝑛 · 𝑥 ) ) = ( 𝑛 ∈ ℤ ↦ ( 𝑛 · ( 𝑤 ‘ 𝑘 ) ) ) )
49 48 rneqd ⊢ ( 𝑥 = ( 𝑤 ‘ 𝑘 ) → ran ( 𝑛 ∈ ℤ ↦ ( 𝑛 · 𝑥 ) ) = ran ( 𝑛 ∈ ℤ ↦ ( 𝑛 · ( 𝑤 ‘ 𝑘 ) ) ) )
50 49 eqeq1d ⊢ ( 𝑥 = ( 𝑤 ‘ 𝑘 ) → ( ran ( 𝑛 ∈ ℤ ↦ ( 𝑛 · 𝑥 ) ) = ( 𝑠 ‘ 𝑘 ) ↔ ran ( 𝑛 ∈ ℤ ↦ ( 𝑛 · ( 𝑤 ‘ 𝑘 ) ) ) = ( 𝑠 ‘ 𝑘 ) ) )
51 50 ac6sfi ⊢ ( ( dom 𝑠 ∈ Fin ∧ ∀ 𝑘 ∈ dom 𝑠 ∃ 𝑥 ∈ 𝐵 ran ( 𝑛 ∈ ℤ ↦ ( 𝑛 · 𝑥 ) ) = ( 𝑠 ‘ 𝑘 ) ) → ∃ 𝑤 ( 𝑤 : dom 𝑠 ⟶ 𝐵 ∧ ∀ 𝑘 ∈ dom 𝑠 ran ( 𝑛 ∈ ℤ ↦ ( 𝑛 · ( 𝑤 ‘ 𝑘 ) ) ) = ( 𝑠 ‘ 𝑘 ) ) )
52 11 46 51 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ Word 𝐶 ) ∧ ( 𝐺 dom DProd 𝑠 ∧ ( 𝐺 DProd 𝑠 ) = 𝐵 ) ) → ∃ 𝑤 ( 𝑤 : dom 𝑠 ⟶ 𝐵 ∧ ∀ 𝑘 ∈ dom 𝑠 ran ( 𝑛 ∈ ℤ ↦ ( 𝑛 · ( 𝑤 ‘ 𝑘 ) ) ) = ( 𝑠 ‘ 𝑘 ) ) )
53 simprl ⊢ ( ( ( ( 𝜑 ∧ 𝑠 ∈ Word 𝐶 ) ∧ ( 𝐺 dom DProd 𝑠 ∧ ( 𝐺 DProd 𝑠 ) = 𝐵 ) ) ∧ ( 𝑤 : dom 𝑠 ⟶ 𝐵 ∧ ∀ 𝑘 ∈ dom 𝑠 ran ( 𝑛 ∈ ℤ ↦ ( 𝑛 · ( 𝑤 ‘ 𝑘 ) ) ) = ( 𝑠 ‘ 𝑘 ) ) ) → 𝑤 : dom 𝑠 ⟶ 𝐵 )
54 9 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑠 ∈ Word 𝐶 ) ∧ ( 𝐺 dom DProd 𝑠 ∧ ( 𝐺 DProd 𝑠 ) = 𝐵 ) ) ∧ ( 𝑤 : dom 𝑠 ⟶ 𝐵 ∧ ∀ 𝑘 ∈ dom 𝑠 ran ( 𝑛 ∈ ℤ ↦ ( 𝑛 · ( 𝑤 ‘ 𝑘 ) ) ) = ( 𝑠 ‘ 𝑘 ) ) ) → dom 𝑠 = ( 0 ..^ ( ♯ ‘ 𝑠 ) ) )
55 54 feq2d ⊢ ( ( ( ( 𝜑 ∧ 𝑠 ∈ Word 𝐶 ) ∧ ( 𝐺 dom DProd 𝑠 ∧ ( 𝐺 DProd 𝑠 ) = 𝐵 ) ) ∧ ( 𝑤 : dom 𝑠 ⟶ 𝐵 ∧ ∀ 𝑘 ∈ dom 𝑠 ran ( 𝑛 ∈ ℤ ↦ ( 𝑛 · ( 𝑤 ‘ 𝑘 ) ) ) = ( 𝑠 ‘ 𝑘 ) ) ) → ( 𝑤 : dom 𝑠 ⟶ 𝐵 ↔ 𝑤 : ( 0 ..^ ( ♯ ‘ 𝑠 ) ) ⟶ 𝐵 ) )
56 53 55 mpbid ⊢ ( ( ( ( 𝜑 ∧ 𝑠 ∈ Word 𝐶 ) ∧ ( 𝐺 dom DProd 𝑠 ∧ ( 𝐺 DProd 𝑠 ) = 𝐵 ) ) ∧ ( 𝑤 : dom 𝑠 ⟶ 𝐵 ∧ ∀ 𝑘 ∈ dom 𝑠 ran ( 𝑛 ∈ ℤ ↦ ( 𝑛 · ( 𝑤 ‘ 𝑘 ) ) ) = ( 𝑠 ‘ 𝑘 ) ) ) → 𝑤 : ( 0 ..^ ( ♯ ‘ 𝑠 ) ) ⟶ 𝐵 )
57 iswrdi ⊢ ( 𝑤 : ( 0 ..^ ( ♯ ‘ 𝑠 ) ) ⟶ 𝐵 → 𝑤 ∈ Word 𝐵 )
58 56 57 syl ⊢ ( ( ( ( 𝜑 ∧ 𝑠 ∈ Word 𝐶 ) ∧ ( 𝐺 dom DProd 𝑠 ∧ ( 𝐺 DProd 𝑠 ) = 𝐵 ) ) ∧ ( 𝑤 : dom 𝑠 ⟶ 𝐵 ∧ ∀ 𝑘 ∈ dom 𝑠 ran ( 𝑛 ∈ ℤ ↦ ( 𝑛 · ( 𝑤 ‘ 𝑘 ) ) ) = ( 𝑠 ‘ 𝑘 ) ) ) → 𝑤 ∈ Word 𝐵 )
59 53 fdmd ⊢ ( ( ( ( 𝜑 ∧ 𝑠 ∈ Word 𝐶 ) ∧ ( 𝐺 dom DProd 𝑠 ∧ ( 𝐺 DProd 𝑠 ) = 𝐵 ) ) ∧ ( 𝑤 : dom 𝑠 ⟶ 𝐵 ∧ ∀ 𝑘 ∈ dom 𝑠 ran ( 𝑛 ∈ ℤ ↦ ( 𝑛 · ( 𝑤 ‘ 𝑘 ) ) ) = ( 𝑠 ‘ 𝑘 ) ) ) → dom 𝑤 = dom 𝑠 )
60 59 eleq2d ⊢ ( ( ( ( 𝜑 ∧ 𝑠 ∈ Word 𝐶 ) ∧ ( 𝐺 dom DProd 𝑠 ∧ ( 𝐺 DProd 𝑠 ) = 𝐵 ) ) ∧ ( 𝑤 : dom 𝑠 ⟶ 𝐵 ∧ ∀ 𝑘 ∈ dom 𝑠 ran ( 𝑛 ∈ ℤ ↦ ( 𝑛 · ( 𝑤 ‘ 𝑘 ) ) ) = ( 𝑠 ‘ 𝑘 ) ) ) → ( 𝑗 ∈ dom 𝑤 ↔ 𝑗 ∈ dom 𝑠 ) )
61 60 biimpa ⊢ ( ( ( ( ( 𝜑 ∧ 𝑠 ∈ Word 𝐶 ) ∧ ( 𝐺 dom DProd 𝑠 ∧ ( 𝐺 DProd 𝑠 ) = 𝐵 ) ) ∧ ( 𝑤 : dom 𝑠 ⟶ 𝐵 ∧ ∀ 𝑘 ∈ dom 𝑠 ran ( 𝑛 ∈ ℤ ↦ ( 𝑛 · ( 𝑤 ‘ 𝑘 ) ) ) = ( 𝑠 ‘ 𝑘 ) ) ) ∧ 𝑗 ∈ dom 𝑤 ) → 𝑗 ∈ dom 𝑠 )
62 simprr ⊢ ( ( ( ( 𝜑 ∧ 𝑠 ∈ Word 𝐶 ) ∧ ( 𝐺 dom DProd 𝑠 ∧ ( 𝐺 DProd 𝑠 ) = 𝐵 ) ) ∧ ( 𝑤 : dom 𝑠 ⟶ 𝐵 ∧ ∀ 𝑘 ∈ dom 𝑠 ran ( 𝑛 ∈ ℤ ↦ ( 𝑛 · ( 𝑤 ‘ 𝑘 ) ) ) = ( 𝑠 ‘ 𝑘 ) ) ) → ∀ 𝑘 ∈ dom 𝑠 ran ( 𝑛 ∈ ℤ ↦ ( 𝑛 · ( 𝑤 ‘ 𝑘 ) ) ) = ( 𝑠 ‘ 𝑘 ) )
63 simpl ⊢ ( ( 𝑘 = 𝑗 ∧ 𝑛 ∈ ℤ ) → 𝑘 = 𝑗 )
64 63 fveq2d ⊢ ( ( 𝑘 = 𝑗 ∧ 𝑛 ∈ ℤ ) → ( 𝑤 ‘ 𝑘 ) = ( 𝑤 ‘ 𝑗 ) )
65 64 oveq2d ⊢ ( ( 𝑘 = 𝑗 ∧ 𝑛 ∈ ℤ ) → ( 𝑛 · ( 𝑤 ‘ 𝑘 ) ) = ( 𝑛 · ( 𝑤 ‘ 𝑗 ) ) )
66 65 mpteq2dva ⊢ ( 𝑘 = 𝑗 → ( 𝑛 ∈ ℤ ↦ ( 𝑛 · ( 𝑤 ‘ 𝑘 ) ) ) = ( 𝑛 ∈ ℤ ↦ ( 𝑛 · ( 𝑤 ‘ 𝑗 ) ) ) )
67 66 rneqd ⊢ ( 𝑘 = 𝑗 → ran ( 𝑛 ∈ ℤ ↦ ( 𝑛 · ( 𝑤 ‘ 𝑘 ) ) ) = ran ( 𝑛 ∈ ℤ ↦ ( 𝑛 · ( 𝑤 ‘ 𝑗 ) ) ) )
68 fveq2 ⊢ ( 𝑘 = 𝑗 → ( 𝑠 ‘ 𝑘 ) = ( 𝑠 ‘ 𝑗 ) )
69 67 68 eqeq12d ⊢ ( 𝑘 = 𝑗 → ( ran ( 𝑛 ∈ ℤ ↦ ( 𝑛 · ( 𝑤 ‘ 𝑘 ) ) ) = ( 𝑠 ‘ 𝑘 ) ↔ ran ( 𝑛 ∈ ℤ ↦ ( 𝑛 · ( 𝑤 ‘ 𝑗 ) ) ) = ( 𝑠 ‘ 𝑗 ) ) )
70 69 rspccva ⊢ ( ( ∀ 𝑘 ∈ dom 𝑠 ran ( 𝑛 ∈ ℤ ↦ ( 𝑛 · ( 𝑤 ‘ 𝑘 ) ) ) = ( 𝑠 ‘ 𝑘 ) ∧ 𝑗 ∈ dom 𝑠 ) → ran ( 𝑛 ∈ ℤ ↦ ( 𝑛 · ( 𝑤 ‘ 𝑗 ) ) ) = ( 𝑠 ‘ 𝑗 ) )
71 62 70 sylan ⊢ ( ( ( ( ( 𝜑 ∧ 𝑠 ∈ Word 𝐶 ) ∧ ( 𝐺 dom DProd 𝑠 ∧ ( 𝐺 DProd 𝑠 ) = 𝐵 ) ) ∧ ( 𝑤 : dom 𝑠 ⟶ 𝐵 ∧ ∀ 𝑘 ∈ dom 𝑠 ran ( 𝑛 ∈ ℤ ↦ ( 𝑛 · ( 𝑤 ‘ 𝑘 ) ) ) = ( 𝑠 ‘ 𝑘 ) ) ) ∧ 𝑗 ∈ dom 𝑠 ) → ran ( 𝑛 ∈ ℤ ↦ ( 𝑛 · ( 𝑤 ‘ 𝑗 ) ) ) = ( 𝑠 ‘ 𝑗 ) )
72 12 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑠 ∈ Word 𝐶 ) ∧ ( 𝐺 dom DProd 𝑠 ∧ ( 𝐺 DProd 𝑠 ) = 𝐵 ) ) ∧ ( 𝑤 : dom 𝑠 ⟶ 𝐵 ∧ ∀ 𝑘 ∈ dom 𝑠 ran ( 𝑛 ∈ ℤ ↦ ( 𝑛 · ( 𝑤 ‘ 𝑘 ) ) ) = ( 𝑠 ‘ 𝑘 ) ) ) → 𝑠 : dom 𝑠 ⟶ 𝐶 )
73 72 ffvelcdmda ⊢ ( ( ( ( ( 𝜑 ∧ 𝑠 ∈ Word 𝐶 ) ∧ ( 𝐺 dom DProd 𝑠 ∧ ( 𝐺 DProd 𝑠 ) = 𝐵 ) ) ∧ ( 𝑤 : dom 𝑠 ⟶ 𝐵 ∧ ∀ 𝑘 ∈ dom 𝑠 ran ( 𝑛 ∈ ℤ ↦ ( 𝑛 · ( 𝑤 ‘ 𝑘 ) ) ) = ( 𝑠 ‘ 𝑘 ) ) ) ∧ 𝑗 ∈ dom 𝑠 ) → ( 𝑠 ‘ 𝑗 ) ∈ 𝐶 )
74 71 73 eqeltrd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑠 ∈ Word 𝐶 ) ∧ ( 𝐺 dom DProd 𝑠 ∧ ( 𝐺 DProd 𝑠 ) = 𝐵 ) ) ∧ ( 𝑤 : dom 𝑠 ⟶ 𝐵 ∧ ∀ 𝑘 ∈ dom 𝑠 ran ( 𝑛 ∈ ℤ ↦ ( 𝑛 · ( 𝑤 ‘ 𝑘 ) ) ) = ( 𝑠 ‘ 𝑘 ) ) ) ∧ 𝑗 ∈ dom 𝑠 ) → ran ( 𝑛 ∈ ℤ ↦ ( 𝑛 · ( 𝑤 ‘ 𝑗 ) ) ) ∈ 𝐶 )
75 61 74 syldan ⊢ ( ( ( ( ( 𝜑 ∧ 𝑠 ∈ Word 𝐶 ) ∧ ( 𝐺 dom DProd 𝑠 ∧ ( 𝐺 DProd 𝑠 ) = 𝐵 ) ) ∧ ( 𝑤 : dom 𝑠 ⟶ 𝐵 ∧ ∀ 𝑘 ∈ dom 𝑠 ran ( 𝑛 ∈ ℤ ↦ ( 𝑛 · ( 𝑤 ‘ 𝑘 ) ) ) = ( 𝑠 ‘ 𝑘 ) ) ) ∧ 𝑗 ∈ dom 𝑤 ) → ran ( 𝑛 ∈ ℤ ↦ ( 𝑛 · ( 𝑤 ‘ 𝑗 ) ) ) ∈ 𝐶 )
76 fveq2 ⊢ ( 𝑘 = 𝑗 → ( 𝑤 ‘ 𝑘 ) = ( 𝑤 ‘ 𝑗 ) )
77 76 oveq2d ⊢ ( 𝑘 = 𝑗 → ( 𝑛 · ( 𝑤 ‘ 𝑘 ) ) = ( 𝑛 · ( 𝑤 ‘ 𝑗 ) ) )
78 77 mpteq2dv ⊢ ( 𝑘 = 𝑗 → ( 𝑛 ∈ ℤ ↦ ( 𝑛 · ( 𝑤 ‘ 𝑘 ) ) ) = ( 𝑛 ∈ ℤ ↦ ( 𝑛 · ( 𝑤 ‘ 𝑗 ) ) ) )
79 78 rneqd ⊢ ( 𝑘 = 𝑗 → ran ( 𝑛 ∈ ℤ ↦ ( 𝑛 · ( 𝑤 ‘ 𝑘 ) ) ) = ran ( 𝑛 ∈ ℤ ↦ ( 𝑛 · ( 𝑤 ‘ 𝑗 ) ) ) )
80 79 cbvmptv ⊢ ( 𝑘 ∈ dom 𝑤 ↦ ran ( 𝑛 ∈ ℤ ↦ ( 𝑛 · ( 𝑤 ‘ 𝑘 ) ) ) ) = ( 𝑗 ∈ dom 𝑤 ↦ ran ( 𝑛 ∈ ℤ ↦ ( 𝑛 · ( 𝑤 ‘ 𝑗 ) ) ) )
81 6 80 eqtri ⊢ 𝑆 = ( 𝑗 ∈ dom 𝑤 ↦ ran ( 𝑛 ∈ ℤ ↦ ( 𝑛 · ( 𝑤 ‘ 𝑗 ) ) ) )
82 75 81 fmptd ⊢ ( ( ( ( 𝜑 ∧ 𝑠 ∈ Word 𝐶 ) ∧ ( 𝐺 dom DProd 𝑠 ∧ ( 𝐺 DProd 𝑠 ) = 𝐵 ) ) ∧ ( 𝑤 : dom 𝑠 ⟶ 𝐵 ∧ ∀ 𝑘 ∈ dom 𝑠 ran ( 𝑛 ∈ ℤ ↦ ( 𝑛 · ( 𝑤 ‘ 𝑘 ) ) ) = ( 𝑠 ‘ 𝑘 ) ) ) → 𝑆 : dom 𝑤 ⟶ 𝐶 )
83 simprl ⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ Word 𝐶 ) ∧ ( 𝐺 dom DProd 𝑠 ∧ ( 𝐺 DProd 𝑠 ) = 𝐵 ) ) → 𝐺 dom DProd 𝑠 )
84 83 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑠 ∈ Word 𝐶 ) ∧ ( 𝐺 dom DProd 𝑠 ∧ ( 𝐺 DProd 𝑠 ) = 𝐵 ) ) ∧ ( 𝑤 : dom 𝑠 ⟶ 𝐵 ∧ ∀ 𝑘 ∈ dom 𝑠 ran ( 𝑛 ∈ ℤ ↦ ( 𝑛 · ( 𝑤 ‘ 𝑘 ) ) ) = ( 𝑠 ‘ 𝑘 ) ) ) → 𝐺 dom DProd 𝑠 )
85 62 59 raleqtrrdv ⊢ ( ( ( ( 𝜑 ∧ 𝑠 ∈ Word 𝐶 ) ∧ ( 𝐺 dom DProd 𝑠 ∧ ( 𝐺 DProd 𝑠 ) = 𝐵 ) ) ∧ ( 𝑤 : dom 𝑠 ⟶ 𝐵 ∧ ∀ 𝑘 ∈ dom 𝑠 ran ( 𝑛 ∈ ℤ ↦ ( 𝑛 · ( 𝑤 ‘ 𝑘 ) ) ) = ( 𝑠 ‘ 𝑘 ) ) ) → ∀ 𝑘 ∈ dom 𝑤 ran ( 𝑛 ∈ ℤ ↦ ( 𝑛 · ( 𝑤 ‘ 𝑘 ) ) ) = ( 𝑠 ‘ 𝑘 ) )
86 mpteq12 ⊢ ( ( dom 𝑤 = dom 𝑠 ∧ ∀ 𝑘 ∈ dom 𝑤 ran ( 𝑛 ∈ ℤ ↦ ( 𝑛 · ( 𝑤 ‘ 𝑘 ) ) ) = ( 𝑠 ‘ 𝑘 ) ) → ( 𝑘 ∈ dom 𝑤 ↦ ran ( 𝑛 ∈ ℤ ↦ ( 𝑛 · ( 𝑤 ‘ 𝑘 ) ) ) ) = ( 𝑘 ∈ dom 𝑠 ↦ ( 𝑠 ‘ 𝑘 ) ) )
87 59 85 86 syl2anc ⊢ ( ( ( ( 𝜑 ∧ 𝑠 ∈ Word 𝐶 ) ∧ ( 𝐺 dom DProd 𝑠 ∧ ( 𝐺 DProd 𝑠 ) = 𝐵 ) ) ∧ ( 𝑤 : dom 𝑠 ⟶ 𝐵 ∧ ∀ 𝑘 ∈ dom 𝑠 ran ( 𝑛 ∈ ℤ ↦ ( 𝑛 · ( 𝑤 ‘ 𝑘 ) ) ) = ( 𝑠 ‘ 𝑘 ) ) ) → ( 𝑘 ∈ dom 𝑤 ↦ ran ( 𝑛 ∈ ℤ ↦ ( 𝑛 · ( 𝑤 ‘ 𝑘 ) ) ) ) = ( 𝑘 ∈ dom 𝑠 ↦ ( 𝑠 ‘ 𝑘 ) ) )
88 6 87 eqtrid ⊢ ( ( ( ( 𝜑 ∧ 𝑠 ∈ Word 𝐶 ) ∧ ( 𝐺 dom DProd 𝑠 ∧ ( 𝐺 DProd 𝑠 ) = 𝐵 ) ) ∧ ( 𝑤 : dom 𝑠 ⟶ 𝐵 ∧ ∀ 𝑘 ∈ dom 𝑠 ran ( 𝑛 ∈ ℤ ↦ ( 𝑛 · ( 𝑤 ‘ 𝑘 ) ) ) = ( 𝑠 ‘ 𝑘 ) ) ) → 𝑆 = ( 𝑘 ∈ dom 𝑠 ↦ ( 𝑠 ‘ 𝑘 ) ) )
89 dprdf ⊢ ( 𝐺 dom DProd 𝑠 → 𝑠 : dom 𝑠 ⟶ ( SubGrp ‘ 𝐺 ) )
90 84 89 syl ⊢ ( ( ( ( 𝜑 ∧ 𝑠 ∈ Word 𝐶 ) ∧ ( 𝐺 dom DProd 𝑠 ∧ ( 𝐺 DProd 𝑠 ) = 𝐵 ) ) ∧ ( 𝑤 : dom 𝑠 ⟶ 𝐵 ∧ ∀ 𝑘 ∈ dom 𝑠 ran ( 𝑛 ∈ ℤ ↦ ( 𝑛 · ( 𝑤 ‘ 𝑘 ) ) ) = ( 𝑠 ‘ 𝑘 ) ) ) → 𝑠 : dom 𝑠 ⟶ ( SubGrp ‘ 𝐺 ) )
91 90 feqmptd ⊢ ( ( ( ( 𝜑 ∧ 𝑠 ∈ Word 𝐶 ) ∧ ( 𝐺 dom DProd 𝑠 ∧ ( 𝐺 DProd 𝑠 ) = 𝐵 ) ) ∧ ( 𝑤 : dom 𝑠 ⟶ 𝐵 ∧ ∀ 𝑘 ∈ dom 𝑠 ran ( 𝑛 ∈ ℤ ↦ ( 𝑛 · ( 𝑤 ‘ 𝑘 ) ) ) = ( 𝑠 ‘ 𝑘 ) ) ) → 𝑠 = ( 𝑘 ∈ dom 𝑠 ↦ ( 𝑠 ‘ 𝑘 ) ) )
92 88 91 eqtr4d ⊢ ( ( ( ( 𝜑 ∧ 𝑠 ∈ Word 𝐶 ) ∧ ( 𝐺 dom DProd 𝑠 ∧ ( 𝐺 DProd 𝑠 ) = 𝐵 ) ) ∧ ( 𝑤 : dom 𝑠 ⟶ 𝐵 ∧ ∀ 𝑘 ∈ dom 𝑠 ran ( 𝑛 ∈ ℤ ↦ ( 𝑛 · ( 𝑤 ‘ 𝑘 ) ) ) = ( 𝑠 ‘ 𝑘 ) ) ) → 𝑆 = 𝑠 )
93 84 92 breqtrrd ⊢ ( ( ( ( 𝜑 ∧ 𝑠 ∈ Word 𝐶 ) ∧ ( 𝐺 dom DProd 𝑠 ∧ ( 𝐺 DProd 𝑠 ) = 𝐵 ) ) ∧ ( 𝑤 : dom 𝑠 ⟶ 𝐵 ∧ ∀ 𝑘 ∈ dom 𝑠 ran ( 𝑛 ∈ ℤ ↦ ( 𝑛 · ( 𝑤 ‘ 𝑘 ) ) ) = ( 𝑠 ‘ 𝑘 ) ) ) → 𝐺 dom DProd 𝑆 )
94 92 oveq2d ⊢ ( ( ( ( 𝜑 ∧ 𝑠 ∈ Word 𝐶 ) ∧ ( 𝐺 dom DProd 𝑠 ∧ ( 𝐺 DProd 𝑠 ) = 𝐵 ) ) ∧ ( 𝑤 : dom 𝑠 ⟶ 𝐵 ∧ ∀ 𝑘 ∈ dom 𝑠 ran ( 𝑛 ∈ ℤ ↦ ( 𝑛 · ( 𝑤 ‘ 𝑘 ) ) ) = ( 𝑠 ‘ 𝑘 ) ) ) → ( 𝐺 DProd 𝑆 ) = ( 𝐺 DProd 𝑠 ) )
95 simplrr ⊢ ( ( ( ( 𝜑 ∧ 𝑠 ∈ Word 𝐶 ) ∧ ( 𝐺 dom DProd 𝑠 ∧ ( 𝐺 DProd 𝑠 ) = 𝐵 ) ) ∧ ( 𝑤 : dom 𝑠 ⟶ 𝐵 ∧ ∀ 𝑘 ∈ dom 𝑠 ran ( 𝑛 ∈ ℤ ↦ ( 𝑛 · ( 𝑤 ‘ 𝑘 ) ) ) = ( 𝑠 ‘ 𝑘 ) ) ) → ( 𝐺 DProd 𝑠 ) = 𝐵 )
96 94 95 eqtrd ⊢ ( ( ( ( 𝜑 ∧ 𝑠 ∈ Word 𝐶 ) ∧ ( 𝐺 dom DProd 𝑠 ∧ ( 𝐺 DProd 𝑠 ) = 𝐵 ) ) ∧ ( 𝑤 : dom 𝑠 ⟶ 𝐵 ∧ ∀ 𝑘 ∈ dom 𝑠 ran ( 𝑛 ∈ ℤ ↦ ( 𝑛 · ( 𝑤 ‘ 𝑘 ) ) ) = ( 𝑠 ‘ 𝑘 ) ) ) → ( 𝐺 DProd 𝑆 ) = 𝐵 )
97 82 93 96 3jca ⊢ ( ( ( ( 𝜑 ∧ 𝑠 ∈ Word 𝐶 ) ∧ ( 𝐺 dom DProd 𝑠 ∧ ( 𝐺 DProd 𝑠 ) = 𝐵 ) ) ∧ ( 𝑤 : dom 𝑠 ⟶ 𝐵 ∧ ∀ 𝑘 ∈ dom 𝑠 ran ( 𝑛 ∈ ℤ ↦ ( 𝑛 · ( 𝑤 ‘ 𝑘 ) ) ) = ( 𝑠 ‘ 𝑘 ) ) ) → ( 𝑆 : dom 𝑤 ⟶ 𝐶 ∧ 𝐺 dom DProd 𝑆 ∧ ( 𝐺 DProd 𝑆 ) = 𝐵 ) )
98 58 97 jca ⊢ ( ( ( ( 𝜑 ∧ 𝑠 ∈ Word 𝐶 ) ∧ ( 𝐺 dom DProd 𝑠 ∧ ( 𝐺 DProd 𝑠 ) = 𝐵 ) ) ∧ ( 𝑤 : dom 𝑠 ⟶ 𝐵 ∧ ∀ 𝑘 ∈ dom 𝑠 ran ( 𝑛 ∈ ℤ ↦ ( 𝑛 · ( 𝑤 ‘ 𝑘 ) ) ) = ( 𝑠 ‘ 𝑘 ) ) ) → ( 𝑤 ∈ Word 𝐵 ∧ ( 𝑆 : dom 𝑤 ⟶ 𝐶 ∧ 𝐺 dom DProd 𝑆 ∧ ( 𝐺 DProd 𝑆 ) = 𝐵 ) ) )
99 98 ex ⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ Word 𝐶 ) ∧ ( 𝐺 dom DProd 𝑠 ∧ ( 𝐺 DProd 𝑠 ) = 𝐵 ) ) → ( ( 𝑤 : dom 𝑠 ⟶ 𝐵 ∧ ∀ 𝑘 ∈ dom 𝑠 ran ( 𝑛 ∈ ℤ ↦ ( 𝑛 · ( 𝑤 ‘ 𝑘 ) ) ) = ( 𝑠 ‘ 𝑘 ) ) → ( 𝑤 ∈ Word 𝐵 ∧ ( 𝑆 : dom 𝑤 ⟶ 𝐶 ∧ 𝐺 dom DProd 𝑆 ∧ ( 𝐺 DProd 𝑆 ) = 𝐵 ) ) ) )
100 99 eximdv ⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ Word 𝐶 ) ∧ ( 𝐺 dom DProd 𝑠 ∧ ( 𝐺 DProd 𝑠 ) = 𝐵 ) ) → ( ∃ 𝑤 ( 𝑤 : dom 𝑠 ⟶ 𝐵 ∧ ∀ 𝑘 ∈ dom 𝑠 ran ( 𝑛 ∈ ℤ ↦ ( 𝑛 · ( 𝑤 ‘ 𝑘 ) ) ) = ( 𝑠 ‘ 𝑘 ) ) → ∃ 𝑤 ( 𝑤 ∈ Word 𝐵 ∧ ( 𝑆 : dom 𝑤 ⟶ 𝐶 ∧ 𝐺 dom DProd 𝑆 ∧ ( 𝐺 DProd 𝑆 ) = 𝐵 ) ) ) )
101 52 100 mpd ⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ Word 𝐶 ) ∧ ( 𝐺 dom DProd 𝑠 ∧ ( 𝐺 DProd 𝑠 ) = 𝐵 ) ) → ∃ 𝑤 ( 𝑤 ∈ Word 𝐵 ∧ ( 𝑆 : dom 𝑤 ⟶ 𝐶 ∧ 𝐺 dom DProd 𝑆 ∧ ( 𝐺 DProd 𝑆 ) = 𝐵 ) ) )
102 df-rex ⊢ ( ∃ 𝑤 ∈ Word 𝐵 ( 𝑆 : dom 𝑤 ⟶ 𝐶 ∧ 𝐺 dom DProd 𝑆 ∧ ( 𝐺 DProd 𝑆 ) = 𝐵 ) ↔ ∃ 𝑤 ( 𝑤 ∈ Word 𝐵 ∧ ( 𝑆 : dom 𝑤 ⟶ 𝐶 ∧ 𝐺 dom DProd 𝑆 ∧ ( 𝐺 DProd 𝑆 ) = 𝐵 ) ) )
103 101 102 sylibr ⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ Word 𝐶 ) ∧ ( 𝐺 dom DProd 𝑠 ∧ ( 𝐺 DProd 𝑠 ) = 𝐵 ) ) → ∃ 𝑤 ∈ Word 𝐵 ( 𝑆 : dom 𝑤 ⟶ 𝐶 ∧ 𝐺 dom DProd 𝑆 ∧ ( 𝐺 DProd 𝑆 ) = 𝐵 ) )
104 1 2 3 4 ablfac ⊢ ( 𝜑 → ∃ 𝑠 ∈ Word 𝐶 ( 𝐺 dom DProd 𝑠 ∧ ( 𝐺 DProd 𝑠 ) = 𝐵 ) )
105 103 104 r19.29a ⊢ ( 𝜑 → ∃ 𝑤 ∈ Word 𝐵 ( 𝑆 : dom 𝑤 ⟶ 𝐶 ∧ 𝐺 dom DProd 𝑆 ∧ ( 𝐺 DProd 𝑆 ) = 𝐵 ) )