Metamath Proof Explorer


Theorem pgpfaclem1

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

Ref Expression
Hypotheses pgpfac.b 𝐵 = ( Base ‘ 𝐺 )
pgpfac.c 𝐶 = { 𝑟 ∈ ( SubGrp ‘ 𝐺 ) ∣ ( 𝐺s 𝑟 ) ∈ ( CycGrp ∩ ran pGrp ) }
pgpfac.g ( 𝜑𝐺 ∈ Abel )
pgpfac.p ( 𝜑𝑃 pGrp 𝐺 )
pgpfac.f ( 𝜑𝐵 ∈ Fin )
pgpfac.u ( 𝜑𝑈 ∈ ( SubGrp ‘ 𝐺 ) )
pgpfac.a ( 𝜑 → ∀ 𝑡 ∈ ( SubGrp ‘ 𝐺 ) ( 𝑡𝑈 → ∃ 𝑠 ∈ Word 𝐶 ( 𝐺 dom DProd 𝑠 ∧ ( 𝐺 DProd 𝑠 ) = 𝑡 ) ) )
pgpfac.h 𝐻 = ( 𝐺s 𝑈 )
pgpfac.k 𝐾 = ( mrCls ‘ ( SubGrp ‘ 𝐻 ) )
pgpfac.o 𝑂 = ( od ‘ 𝐻 )
pgpfac.e 𝐸 = ( gEx ‘ 𝐻 )
pgpfac.0 0 = ( 0g𝐻 )
pgpfac.l = ( LSSum ‘ 𝐻 )
pgpfac.1 ( 𝜑𝐸 ≠ 1 )
pgpfac.x ( 𝜑𝑋𝑈 )
pgpfac.oe ( 𝜑 → ( 𝑂𝑋 ) = 𝐸 )
pgpfac.w ( 𝜑𝑊 ∈ ( SubGrp ‘ 𝐻 ) )
pgpfac.i ( 𝜑 → ( ( 𝐾 ‘ { 𝑋 } ) ∩ 𝑊 ) = { 0 } )
pgpfac.s ( 𝜑 → ( ( 𝐾 ‘ { 𝑋 } ) 𝑊 ) = 𝑈 )
pgpfac.2 ( 𝜑𝑆 ∈ Word 𝐶 )
pgpfac.4 ( 𝜑𝐺 dom DProd 𝑆 )
pgpfac.5 ( 𝜑 → ( 𝐺 DProd 𝑆 ) = 𝑊 )
pgpfac.t 𝑇 = ( 𝑆 ++ ⟨“ ( 𝐾 ‘ { 𝑋 } ) ”⟩ )
Assertion pgpfaclem1 ( 𝜑 → ∃ 𝑠 ∈ Word 𝐶 ( 𝐺 dom DProd 𝑠 ∧ ( 𝐺 DProd 𝑠 ) = 𝑈 ) )

Proof

Step Hyp Ref Expression
1 pgpfac.b 𝐵 = ( Base ‘ 𝐺 )
2 pgpfac.c 𝐶 = { 𝑟 ∈ ( SubGrp ‘ 𝐺 ) ∣ ( 𝐺s 𝑟 ) ∈ ( CycGrp ∩ ran pGrp ) }
3 pgpfac.g ( 𝜑𝐺 ∈ Abel )
4 pgpfac.p ( 𝜑𝑃 pGrp 𝐺 )
5 pgpfac.f ( 𝜑𝐵 ∈ Fin )
6 pgpfac.u ( 𝜑𝑈 ∈ ( SubGrp ‘ 𝐺 ) )
7 pgpfac.a ( 𝜑 → ∀ 𝑡 ∈ ( SubGrp ‘ 𝐺 ) ( 𝑡𝑈 → ∃ 𝑠 ∈ Word 𝐶 ( 𝐺 dom DProd 𝑠 ∧ ( 𝐺 DProd 𝑠 ) = 𝑡 ) ) )
8 pgpfac.h 𝐻 = ( 𝐺s 𝑈 )
9 pgpfac.k 𝐾 = ( mrCls ‘ ( SubGrp ‘ 𝐻 ) )
10 pgpfac.o 𝑂 = ( od ‘ 𝐻 )
11 pgpfac.e 𝐸 = ( gEx ‘ 𝐻 )
12 pgpfac.0 0 = ( 0g𝐻 )
13 pgpfac.l = ( LSSum ‘ 𝐻 )
14 pgpfac.1 ( 𝜑𝐸 ≠ 1 )
15 pgpfac.x ( 𝜑𝑋𝑈 )
16 pgpfac.oe ( 𝜑 → ( 𝑂𝑋 ) = 𝐸 )
17 pgpfac.w ( 𝜑𝑊 ∈ ( SubGrp ‘ 𝐻 ) )
18 pgpfac.i ( 𝜑 → ( ( 𝐾 ‘ { 𝑋 } ) ∩ 𝑊 ) = { 0 } )
19 pgpfac.s ( 𝜑 → ( ( 𝐾 ‘ { 𝑋 } ) 𝑊 ) = 𝑈 )
20 pgpfac.2 ( 𝜑𝑆 ∈ Word 𝐶 )
21 pgpfac.4 ( 𝜑𝐺 dom DProd 𝑆 )
22 pgpfac.5 ( 𝜑 → ( 𝐺 DProd 𝑆 ) = 𝑊 )
23 pgpfac.t 𝑇 = ( 𝑆 ++ ⟨“ ( 𝐾 ‘ { 𝑋 } ) ”⟩ )
24 8 subggrp ( 𝑈 ∈ ( SubGrp ‘ 𝐺 ) → 𝐻 ∈ Grp )
25 6 24 syl ( 𝜑𝐻 ∈ Grp )
26 eqid ( Base ‘ 𝐻 ) = ( Base ‘ 𝐻 )
27 26 subgacs ( 𝐻 ∈ Grp → ( SubGrp ‘ 𝐻 ) ∈ ( ACS ‘ ( Base ‘ 𝐻 ) ) )
28 25 27 syl ( 𝜑 → ( SubGrp ‘ 𝐻 ) ∈ ( ACS ‘ ( Base ‘ 𝐻 ) ) )
29 28 acsmred ( 𝜑 → ( SubGrp ‘ 𝐻 ) ∈ ( Moore ‘ ( Base ‘ 𝐻 ) ) )
30 8 subgbas ( 𝑈 ∈ ( SubGrp ‘ 𝐺 ) → 𝑈 = ( Base ‘ 𝐻 ) )
31 6 30 syl ( 𝜑𝑈 = ( Base ‘ 𝐻 ) )
32 15 31 eleqtrd ( 𝜑𝑋 ∈ ( Base ‘ 𝐻 ) )
33 9 mrcsncl ( ( ( SubGrp ‘ 𝐻 ) ∈ ( Moore ‘ ( Base ‘ 𝐻 ) ) ∧ 𝑋 ∈ ( Base ‘ 𝐻 ) ) → ( 𝐾 ‘ { 𝑋 } ) ∈ ( SubGrp ‘ 𝐻 ) )
34 29 32 33 syl2anc ( 𝜑 → ( 𝐾 ‘ { 𝑋 } ) ∈ ( SubGrp ‘ 𝐻 ) )
35 8 subsubg ( 𝑈 ∈ ( SubGrp ‘ 𝐺 ) → ( ( 𝐾 ‘ { 𝑋 } ) ∈ ( SubGrp ‘ 𝐻 ) ↔ ( ( 𝐾 ‘ { 𝑋 } ) ∈ ( SubGrp ‘ 𝐺 ) ∧ ( 𝐾 ‘ { 𝑋 } ) ⊆ 𝑈 ) ) )
36 6 35 syl ( 𝜑 → ( ( 𝐾 ‘ { 𝑋 } ) ∈ ( SubGrp ‘ 𝐻 ) ↔ ( ( 𝐾 ‘ { 𝑋 } ) ∈ ( SubGrp ‘ 𝐺 ) ∧ ( 𝐾 ‘ { 𝑋 } ) ⊆ 𝑈 ) ) )
37 34 36 mpbid ( 𝜑 → ( ( 𝐾 ‘ { 𝑋 } ) ∈ ( SubGrp ‘ 𝐺 ) ∧ ( 𝐾 ‘ { 𝑋 } ) ⊆ 𝑈 ) )
38 37 simpld ( 𝜑 → ( 𝐾 ‘ { 𝑋 } ) ∈ ( SubGrp ‘ 𝐺 ) )
39 8 oveq1i ( 𝐻s ( 𝐾 ‘ { 𝑋 } ) ) = ( ( 𝐺s 𝑈 ) ↾s ( 𝐾 ‘ { 𝑋 } ) )
40 37 simprd ( 𝜑 → ( 𝐾 ‘ { 𝑋 } ) ⊆ 𝑈 )
41 ressabs ( ( 𝑈 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( 𝐾 ‘ { 𝑋 } ) ⊆ 𝑈 ) → ( ( 𝐺s 𝑈 ) ↾s ( 𝐾 ‘ { 𝑋 } ) ) = ( 𝐺s ( 𝐾 ‘ { 𝑋 } ) ) )
42 6 40 41 syl2anc ( 𝜑 → ( ( 𝐺s 𝑈 ) ↾s ( 𝐾 ‘ { 𝑋 } ) ) = ( 𝐺s ( 𝐾 ‘ { 𝑋 } ) ) )
43 39 42 syl5eq ( 𝜑 → ( 𝐻s ( 𝐾 ‘ { 𝑋 } ) ) = ( 𝐺s ( 𝐾 ‘ { 𝑋 } ) ) )
44 26 9 cycsubgcyg2 ( ( 𝐻 ∈ Grp ∧ 𝑋 ∈ ( Base ‘ 𝐻 ) ) → ( 𝐻s ( 𝐾 ‘ { 𝑋 } ) ) ∈ CycGrp )
45 25 32 44 syl2anc ( 𝜑 → ( 𝐻s ( 𝐾 ‘ { 𝑋 } ) ) ∈ CycGrp )
46 43 45 eqeltrrd ( 𝜑 → ( 𝐺s ( 𝐾 ‘ { 𝑋 } ) ) ∈ CycGrp )
47 pgpprm ( 𝑃 pGrp 𝐺𝑃 ∈ ℙ )
48 4 47 syl ( 𝜑𝑃 ∈ ℙ )
49 subgpgp ( ( 𝑃 pGrp 𝐺 ∧ ( 𝐾 ‘ { 𝑋 } ) ∈ ( SubGrp ‘ 𝐺 ) ) → 𝑃 pGrp ( 𝐺s ( 𝐾 ‘ { 𝑋 } ) ) )
50 4 38 49 syl2anc ( 𝜑𝑃 pGrp ( 𝐺s ( 𝐾 ‘ { 𝑋 } ) ) )
51 brelrng ( ( 𝑃 ∈ ℙ ∧ ( 𝐺s ( 𝐾 ‘ { 𝑋 } ) ) ∈ CycGrp ∧ 𝑃 pGrp ( 𝐺s ( 𝐾 ‘ { 𝑋 } ) ) ) → ( 𝐺s ( 𝐾 ‘ { 𝑋 } ) ) ∈ ran pGrp )
52 48 46 50 51 syl3anc ( 𝜑 → ( 𝐺s ( 𝐾 ‘ { 𝑋 } ) ) ∈ ran pGrp )
53 46 52 elind ( 𝜑 → ( 𝐺s ( 𝐾 ‘ { 𝑋 } ) ) ∈ ( CycGrp ∩ ran pGrp ) )
54 oveq2 ( 𝑟 = ( 𝐾 ‘ { 𝑋 } ) → ( 𝐺s 𝑟 ) = ( 𝐺s ( 𝐾 ‘ { 𝑋 } ) ) )
55 54 eleq1d ( 𝑟 = ( 𝐾 ‘ { 𝑋 } ) → ( ( 𝐺s 𝑟 ) ∈ ( CycGrp ∩ ran pGrp ) ↔ ( 𝐺s ( 𝐾 ‘ { 𝑋 } ) ) ∈ ( CycGrp ∩ ran pGrp ) ) )
56 55 2 elrab2 ( ( 𝐾 ‘ { 𝑋 } ) ∈ 𝐶 ↔ ( ( 𝐾 ‘ { 𝑋 } ) ∈ ( SubGrp ‘ 𝐺 ) ∧ ( 𝐺s ( 𝐾 ‘ { 𝑋 } ) ) ∈ ( CycGrp ∩ ran pGrp ) ) )
57 38 53 56 sylanbrc ( 𝜑 → ( 𝐾 ‘ { 𝑋 } ) ∈ 𝐶 )
58 23 20 57 cats1cld ( 𝜑𝑇 ∈ Word 𝐶 )
59 wrdf ( 𝑇 ∈ Word 𝐶𝑇 : ( 0 ..^ ( ♯ ‘ 𝑇 ) ) ⟶ 𝐶 )
60 58 59 syl ( 𝜑𝑇 : ( 0 ..^ ( ♯ ‘ 𝑇 ) ) ⟶ 𝐶 )
61 2 ssrab3 𝐶 ⊆ ( SubGrp ‘ 𝐺 )
62 fss ( ( 𝑇 : ( 0 ..^ ( ♯ ‘ 𝑇 ) ) ⟶ 𝐶𝐶 ⊆ ( SubGrp ‘ 𝐺 ) ) → 𝑇 : ( 0 ..^ ( ♯ ‘ 𝑇 ) ) ⟶ ( SubGrp ‘ 𝐺 ) )
63 60 61 62 sylancl ( 𝜑𝑇 : ( 0 ..^ ( ♯ ‘ 𝑇 ) ) ⟶ ( SubGrp ‘ 𝐺 ) )
64 lencl ( 𝑆 ∈ Word 𝐶 → ( ♯ ‘ 𝑆 ) ∈ ℕ0 )
65 20 64 syl ( 𝜑 → ( ♯ ‘ 𝑆 ) ∈ ℕ0 )
66 65 nn0zd ( 𝜑 → ( ♯ ‘ 𝑆 ) ∈ ℤ )
67 fzosn ( ( ♯ ‘ 𝑆 ) ∈ ℤ → ( ( ♯ ‘ 𝑆 ) ..^ ( ( ♯ ‘ 𝑆 ) + 1 ) ) = { ( ♯ ‘ 𝑆 ) } )
68 66 67 syl ( 𝜑 → ( ( ♯ ‘ 𝑆 ) ..^ ( ( ♯ ‘ 𝑆 ) + 1 ) ) = { ( ♯ ‘ 𝑆 ) } )
69 68 ineq2d ( 𝜑 → ( ( 0 ..^ ( ♯ ‘ 𝑆 ) ) ∩ ( ( ♯ ‘ 𝑆 ) ..^ ( ( ♯ ‘ 𝑆 ) + 1 ) ) ) = ( ( 0 ..^ ( ♯ ‘ 𝑆 ) ) ∩ { ( ♯ ‘ 𝑆 ) } ) )
70 fzodisj ( ( 0 ..^ ( ♯ ‘ 𝑆 ) ) ∩ ( ( ♯ ‘ 𝑆 ) ..^ ( ( ♯ ‘ 𝑆 ) + 1 ) ) ) = ∅
71 69 70 eqtr3di ( 𝜑 → ( ( 0 ..^ ( ♯ ‘ 𝑆 ) ) ∩ { ( ♯ ‘ 𝑆 ) } ) = ∅ )
72 23 fveq2i ( ♯ ‘ 𝑇 ) = ( ♯ ‘ ( 𝑆 ++ ⟨“ ( 𝐾 ‘ { 𝑋 } ) ”⟩ ) )
73 57 s1cld ( 𝜑 → ⟨“ ( 𝐾 ‘ { 𝑋 } ) ”⟩ ∈ Word 𝐶 )
74 ccatlen ( ( 𝑆 ∈ Word 𝐶 ∧ ⟨“ ( 𝐾 ‘ { 𝑋 } ) ”⟩ ∈ Word 𝐶 ) → ( ♯ ‘ ( 𝑆 ++ ⟨“ ( 𝐾 ‘ { 𝑋 } ) ”⟩ ) ) = ( ( ♯ ‘ 𝑆 ) + ( ♯ ‘ ⟨“ ( 𝐾 ‘ { 𝑋 } ) ”⟩ ) ) )
75 20 73 74 syl2anc ( 𝜑 → ( ♯ ‘ ( 𝑆 ++ ⟨“ ( 𝐾 ‘ { 𝑋 } ) ”⟩ ) ) = ( ( ♯ ‘ 𝑆 ) + ( ♯ ‘ ⟨“ ( 𝐾 ‘ { 𝑋 } ) ”⟩ ) ) )
76 72 75 syl5eq ( 𝜑 → ( ♯ ‘ 𝑇 ) = ( ( ♯ ‘ 𝑆 ) + ( ♯ ‘ ⟨“ ( 𝐾 ‘ { 𝑋 } ) ”⟩ ) ) )
77 s1len ( ♯ ‘ ⟨“ ( 𝐾 ‘ { 𝑋 } ) ”⟩ ) = 1
78 77 oveq2i ( ( ♯ ‘ 𝑆 ) + ( ♯ ‘ ⟨“ ( 𝐾 ‘ { 𝑋 } ) ”⟩ ) ) = ( ( ♯ ‘ 𝑆 ) + 1 )
79 76 78 eqtrdi ( 𝜑 → ( ♯ ‘ 𝑇 ) = ( ( ♯ ‘ 𝑆 ) + 1 ) )
80 79 oveq2d ( 𝜑 → ( 0 ..^ ( ♯ ‘ 𝑇 ) ) = ( 0 ..^ ( ( ♯ ‘ 𝑆 ) + 1 ) ) )
81 nn0uz 0 = ( ℤ ‘ 0 )
82 65 81 eleqtrdi ( 𝜑 → ( ♯ ‘ 𝑆 ) ∈ ( ℤ ‘ 0 ) )
83 fzosplitsn ( ( ♯ ‘ 𝑆 ) ∈ ( ℤ ‘ 0 ) → ( 0 ..^ ( ( ♯ ‘ 𝑆 ) + 1 ) ) = ( ( 0 ..^ ( ♯ ‘ 𝑆 ) ) ∪ { ( ♯ ‘ 𝑆 ) } ) )
84 82 83 syl ( 𝜑 → ( 0 ..^ ( ( ♯ ‘ 𝑆 ) + 1 ) ) = ( ( 0 ..^ ( ♯ ‘ 𝑆 ) ) ∪ { ( ♯ ‘ 𝑆 ) } ) )
85 80 84 eqtrd ( 𝜑 → ( 0 ..^ ( ♯ ‘ 𝑇 ) ) = ( ( 0 ..^ ( ♯ ‘ 𝑆 ) ) ∪ { ( ♯ ‘ 𝑆 ) } ) )
86 eqid ( Cntz ‘ 𝐺 ) = ( Cntz ‘ 𝐺 )
87 eqid ( 0g𝐺 ) = ( 0g𝐺 )
88 cats1un ( ( 𝑆 ∈ Word 𝐶 ∧ ( 𝐾 ‘ { 𝑋 } ) ∈ 𝐶 ) → ( 𝑆 ++ ⟨“ ( 𝐾 ‘ { 𝑋 } ) ”⟩ ) = ( 𝑆 ∪ { ⟨ ( ♯ ‘ 𝑆 ) , ( 𝐾 ‘ { 𝑋 } ) ⟩ } ) )
89 20 57 88 syl2anc ( 𝜑 → ( 𝑆 ++ ⟨“ ( 𝐾 ‘ { 𝑋 } ) ”⟩ ) = ( 𝑆 ∪ { ⟨ ( ♯ ‘ 𝑆 ) , ( 𝐾 ‘ { 𝑋 } ) ⟩ } ) )
90 23 89 syl5eq ( 𝜑𝑇 = ( 𝑆 ∪ { ⟨ ( ♯ ‘ 𝑆 ) , ( 𝐾 ‘ { 𝑋 } ) ⟩ } ) )
91 90 reseq1d ( 𝜑 → ( 𝑇 ↾ ( 0 ..^ ( ♯ ‘ 𝑆 ) ) ) = ( ( 𝑆 ∪ { ⟨ ( ♯ ‘ 𝑆 ) , ( 𝐾 ‘ { 𝑋 } ) ⟩ } ) ↾ ( 0 ..^ ( ♯ ‘ 𝑆 ) ) ) )
92 wrdfn ( 𝑆 ∈ Word 𝐶𝑆 Fn ( 0 ..^ ( ♯ ‘ 𝑆 ) ) )
93 20 92 syl ( 𝜑𝑆 Fn ( 0 ..^ ( ♯ ‘ 𝑆 ) ) )
94 fzonel ¬ ( ♯ ‘ 𝑆 ) ∈ ( 0 ..^ ( ♯ ‘ 𝑆 ) )
95 fsnunres ( ( 𝑆 Fn ( 0 ..^ ( ♯ ‘ 𝑆 ) ) ∧ ¬ ( ♯ ‘ 𝑆 ) ∈ ( 0 ..^ ( ♯ ‘ 𝑆 ) ) ) → ( ( 𝑆 ∪ { ⟨ ( ♯ ‘ 𝑆 ) , ( 𝐾 ‘ { 𝑋 } ) ⟩ } ) ↾ ( 0 ..^ ( ♯ ‘ 𝑆 ) ) ) = 𝑆 )
96 93 94 95 sylancl ( 𝜑 → ( ( 𝑆 ∪ { ⟨ ( ♯ ‘ 𝑆 ) , ( 𝐾 ‘ { 𝑋 } ) ⟩ } ) ↾ ( 0 ..^ ( ♯ ‘ 𝑆 ) ) ) = 𝑆 )
97 91 96 eqtrd ( 𝜑 → ( 𝑇 ↾ ( 0 ..^ ( ♯ ‘ 𝑆 ) ) ) = 𝑆 )
98 21 97 breqtrrd ( 𝜑𝐺 dom DProd ( 𝑇 ↾ ( 0 ..^ ( ♯ ‘ 𝑆 ) ) ) )
99 fvex ( ♯ ‘ 𝑆 ) ∈ V
100 dprdsn ( ( ( ♯ ‘ 𝑆 ) ∈ V ∧ ( 𝐾 ‘ { 𝑋 } ) ∈ ( SubGrp ‘ 𝐺 ) ) → ( 𝐺 dom DProd { ⟨ ( ♯ ‘ 𝑆 ) , ( 𝐾 ‘ { 𝑋 } ) ⟩ } ∧ ( 𝐺 DProd { ⟨ ( ♯ ‘ 𝑆 ) , ( 𝐾 ‘ { 𝑋 } ) ⟩ } ) = ( 𝐾 ‘ { 𝑋 } ) ) )
101 99 38 100 sylancr ( 𝜑 → ( 𝐺 dom DProd { ⟨ ( ♯ ‘ 𝑆 ) , ( 𝐾 ‘ { 𝑋 } ) ⟩ } ∧ ( 𝐺 DProd { ⟨ ( ♯ ‘ 𝑆 ) , ( 𝐾 ‘ { 𝑋 } ) ⟩ } ) = ( 𝐾 ‘ { 𝑋 } ) ) )
102 101 simpld ( 𝜑𝐺 dom DProd { ⟨ ( ♯ ‘ 𝑆 ) , ( 𝐾 ‘ { 𝑋 } ) ⟩ } )
103 wrdfn ( 𝑇 ∈ Word 𝐶𝑇 Fn ( 0 ..^ ( ♯ ‘ 𝑇 ) ) )
104 58 103 syl ( 𝜑𝑇 Fn ( 0 ..^ ( ♯ ‘ 𝑇 ) ) )
105 ssun2 { ( ♯ ‘ 𝑆 ) } ⊆ ( ( 0 ..^ ( ♯ ‘ 𝑆 ) ) ∪ { ( ♯ ‘ 𝑆 ) } )
106 99 snss ( ( ♯ ‘ 𝑆 ) ∈ ( ( 0 ..^ ( ♯ ‘ 𝑆 ) ) ∪ { ( ♯ ‘ 𝑆 ) } ) ↔ { ( ♯ ‘ 𝑆 ) } ⊆ ( ( 0 ..^ ( ♯ ‘ 𝑆 ) ) ∪ { ( ♯ ‘ 𝑆 ) } ) )
107 105 106 mpbir ( ♯ ‘ 𝑆 ) ∈ ( ( 0 ..^ ( ♯ ‘ 𝑆 ) ) ∪ { ( ♯ ‘ 𝑆 ) } )
108 107 85 eleqtrrid ( 𝜑 → ( ♯ ‘ 𝑆 ) ∈ ( 0 ..^ ( ♯ ‘ 𝑇 ) ) )
109 fnressn ( ( 𝑇 Fn ( 0 ..^ ( ♯ ‘ 𝑇 ) ) ∧ ( ♯ ‘ 𝑆 ) ∈ ( 0 ..^ ( ♯ ‘ 𝑇 ) ) ) → ( 𝑇 ↾ { ( ♯ ‘ 𝑆 ) } ) = { ⟨ ( ♯ ‘ 𝑆 ) , ( 𝑇 ‘ ( ♯ ‘ 𝑆 ) ) ⟩ } )
110 104 108 109 syl2anc ( 𝜑 → ( 𝑇 ↾ { ( ♯ ‘ 𝑆 ) } ) = { ⟨ ( ♯ ‘ 𝑆 ) , ( 𝑇 ‘ ( ♯ ‘ 𝑆 ) ) ⟩ } )
111 23 fveq1i ( 𝑇 ‘ ( ♯ ‘ 𝑆 ) ) = ( ( 𝑆 ++ ⟨“ ( 𝐾 ‘ { 𝑋 } ) ”⟩ ) ‘ ( ♯ ‘ 𝑆 ) )
112 65 nn0cnd ( 𝜑 → ( ♯ ‘ 𝑆 ) ∈ ℂ )
113 112 addid2d ( 𝜑 → ( 0 + ( ♯ ‘ 𝑆 ) ) = ( ♯ ‘ 𝑆 ) )
114 113 fveq2d ( 𝜑 → ( ( 𝑆 ++ ⟨“ ( 𝐾 ‘ { 𝑋 } ) ”⟩ ) ‘ ( 0 + ( ♯ ‘ 𝑆 ) ) ) = ( ( 𝑆 ++ ⟨“ ( 𝐾 ‘ { 𝑋 } ) ”⟩ ) ‘ ( ♯ ‘ 𝑆 ) ) )
115 111 114 eqtr4id ( 𝜑 → ( 𝑇 ‘ ( ♯ ‘ 𝑆 ) ) = ( ( 𝑆 ++ ⟨“ ( 𝐾 ‘ { 𝑋 } ) ”⟩ ) ‘ ( 0 + ( ♯ ‘ 𝑆 ) ) ) )
116 1nn 1 ∈ ℕ
117 77 116 eqeltri ( ♯ ‘ ⟨“ ( 𝐾 ‘ { 𝑋 } ) ”⟩ ) ∈ ℕ
118 lbfzo0 ( 0 ∈ ( 0 ..^ ( ♯ ‘ ⟨“ ( 𝐾 ‘ { 𝑋 } ) ”⟩ ) ) ↔ ( ♯ ‘ ⟨“ ( 𝐾 ‘ { 𝑋 } ) ”⟩ ) ∈ ℕ )
119 117 118 mpbir 0 ∈ ( 0 ..^ ( ♯ ‘ ⟨“ ( 𝐾 ‘ { 𝑋 } ) ”⟩ ) )
120 119 a1i ( 𝜑 → 0 ∈ ( 0 ..^ ( ♯ ‘ ⟨“ ( 𝐾 ‘ { 𝑋 } ) ”⟩ ) ) )
121 ccatval3 ( ( 𝑆 ∈ Word 𝐶 ∧ ⟨“ ( 𝐾 ‘ { 𝑋 } ) ”⟩ ∈ Word 𝐶 ∧ 0 ∈ ( 0 ..^ ( ♯ ‘ ⟨“ ( 𝐾 ‘ { 𝑋 } ) ”⟩ ) ) ) → ( ( 𝑆 ++ ⟨“ ( 𝐾 ‘ { 𝑋 } ) ”⟩ ) ‘ ( 0 + ( ♯ ‘ 𝑆 ) ) ) = ( ⟨“ ( 𝐾 ‘ { 𝑋 } ) ”⟩ ‘ 0 ) )
122 20 73 120 121 syl3anc ( 𝜑 → ( ( 𝑆 ++ ⟨“ ( 𝐾 ‘ { 𝑋 } ) ”⟩ ) ‘ ( 0 + ( ♯ ‘ 𝑆 ) ) ) = ( ⟨“ ( 𝐾 ‘ { 𝑋 } ) ”⟩ ‘ 0 ) )
123 fvex ( 𝐾 ‘ { 𝑋 } ) ∈ V
124 s1fv ( ( 𝐾 ‘ { 𝑋 } ) ∈ V → ( ⟨“ ( 𝐾 ‘ { 𝑋 } ) ”⟩ ‘ 0 ) = ( 𝐾 ‘ { 𝑋 } ) )
125 123 124 mp1i ( 𝜑 → ( ⟨“ ( 𝐾 ‘ { 𝑋 } ) ”⟩ ‘ 0 ) = ( 𝐾 ‘ { 𝑋 } ) )
126 115 122 125 3eqtrd ( 𝜑 → ( 𝑇 ‘ ( ♯ ‘ 𝑆 ) ) = ( 𝐾 ‘ { 𝑋 } ) )
127 126 opeq2d ( 𝜑 → ⟨ ( ♯ ‘ 𝑆 ) , ( 𝑇 ‘ ( ♯ ‘ 𝑆 ) ) ⟩ = ⟨ ( ♯ ‘ 𝑆 ) , ( 𝐾 ‘ { 𝑋 } ) ⟩ )
128 127 sneqd ( 𝜑 → { ⟨ ( ♯ ‘ 𝑆 ) , ( 𝑇 ‘ ( ♯ ‘ 𝑆 ) ) ⟩ } = { ⟨ ( ♯ ‘ 𝑆 ) , ( 𝐾 ‘ { 𝑋 } ) ⟩ } )
129 110 128 eqtrd ( 𝜑 → ( 𝑇 ↾ { ( ♯ ‘ 𝑆 ) } ) = { ⟨ ( ♯ ‘ 𝑆 ) , ( 𝐾 ‘ { 𝑋 } ) ⟩ } )
130 102 129 breqtrrd ( 𝜑𝐺 dom DProd ( 𝑇 ↾ { ( ♯ ‘ 𝑆 ) } ) )
131 dprdsubg ( 𝐺 dom DProd ( 𝑇 ↾ ( 0 ..^ ( ♯ ‘ 𝑆 ) ) ) → ( 𝐺 DProd ( 𝑇 ↾ ( 0 ..^ ( ♯ ‘ 𝑆 ) ) ) ) ∈ ( SubGrp ‘ 𝐺 ) )
132 98 131 syl ( 𝜑 → ( 𝐺 DProd ( 𝑇 ↾ ( 0 ..^ ( ♯ ‘ 𝑆 ) ) ) ) ∈ ( SubGrp ‘ 𝐺 ) )
133 dprdsubg ( 𝐺 dom DProd ( 𝑇 ↾ { ( ♯ ‘ 𝑆 ) } ) → ( 𝐺 DProd ( 𝑇 ↾ { ( ♯ ‘ 𝑆 ) } ) ) ∈ ( SubGrp ‘ 𝐺 ) )
134 130 133 syl ( 𝜑 → ( 𝐺 DProd ( 𝑇 ↾ { ( ♯ ‘ 𝑆 ) } ) ) ∈ ( SubGrp ‘ 𝐺 ) )
135 86 3 132 134 ablcntzd ( 𝜑 → ( 𝐺 DProd ( 𝑇 ↾ ( 0 ..^ ( ♯ ‘ 𝑆 ) ) ) ) ⊆ ( ( Cntz ‘ 𝐺 ) ‘ ( 𝐺 DProd ( 𝑇 ↾ { ( ♯ ‘ 𝑆 ) } ) ) ) )
136 97 oveq2d ( 𝜑 → ( 𝐺 DProd ( 𝑇 ↾ ( 0 ..^ ( ♯ ‘ 𝑆 ) ) ) ) = ( 𝐺 DProd 𝑆 ) )
137 136 22 eqtrd ( 𝜑 → ( 𝐺 DProd ( 𝑇 ↾ ( 0 ..^ ( ♯ ‘ 𝑆 ) ) ) ) = 𝑊 )
138 129 oveq2d ( 𝜑 → ( 𝐺 DProd ( 𝑇 ↾ { ( ♯ ‘ 𝑆 ) } ) ) = ( 𝐺 DProd { ⟨ ( ♯ ‘ 𝑆 ) , ( 𝐾 ‘ { 𝑋 } ) ⟩ } ) )
139 101 simprd ( 𝜑 → ( 𝐺 DProd { ⟨ ( ♯ ‘ 𝑆 ) , ( 𝐾 ‘ { 𝑋 } ) ⟩ } ) = ( 𝐾 ‘ { 𝑋 } ) )
140 138 139 eqtrd ( 𝜑 → ( 𝐺 DProd ( 𝑇 ↾ { ( ♯ ‘ 𝑆 ) } ) ) = ( 𝐾 ‘ { 𝑋 } ) )
141 137 140 ineq12d ( 𝜑 → ( ( 𝐺 DProd ( 𝑇 ↾ ( 0 ..^ ( ♯ ‘ 𝑆 ) ) ) ) ∩ ( 𝐺 DProd ( 𝑇 ↾ { ( ♯ ‘ 𝑆 ) } ) ) ) = ( 𝑊 ∩ ( 𝐾 ‘ { 𝑋 } ) ) )
142 incom ( 𝑊 ∩ ( 𝐾 ‘ { 𝑋 } ) ) = ( ( 𝐾 ‘ { 𝑋 } ) ∩ 𝑊 )
143 141 142 eqtrdi ( 𝜑 → ( ( 𝐺 DProd ( 𝑇 ↾ ( 0 ..^ ( ♯ ‘ 𝑆 ) ) ) ) ∩ ( 𝐺 DProd ( 𝑇 ↾ { ( ♯ ‘ 𝑆 ) } ) ) ) = ( ( 𝐾 ‘ { 𝑋 } ) ∩ 𝑊 ) )
144 8 87 subg0 ( 𝑈 ∈ ( SubGrp ‘ 𝐺 ) → ( 0g𝐺 ) = ( 0g𝐻 ) )
145 6 144 syl ( 𝜑 → ( 0g𝐺 ) = ( 0g𝐻 ) )
146 145 12 eqtr4di ( 𝜑 → ( 0g𝐺 ) = 0 )
147 146 sneqd ( 𝜑 → { ( 0g𝐺 ) } = { 0 } )
148 18 143 147 3eqtr4d ( 𝜑 → ( ( 𝐺 DProd ( 𝑇 ↾ ( 0 ..^ ( ♯ ‘ 𝑆 ) ) ) ) ∩ ( 𝐺 DProd ( 𝑇 ↾ { ( ♯ ‘ 𝑆 ) } ) ) ) = { ( 0g𝐺 ) } )
149 63 71 85 86 87 98 130 135 148 dmdprdsplit2 ( 𝜑𝐺 dom DProd 𝑇 )
150 eqid ( LSSum ‘ 𝐺 ) = ( LSSum ‘ 𝐺 )
151 63 71 85 150 149 dprdsplit ( 𝜑 → ( 𝐺 DProd 𝑇 ) = ( ( 𝐺 DProd ( 𝑇 ↾ ( 0 ..^ ( ♯ ‘ 𝑆 ) ) ) ) ( LSSum ‘ 𝐺 ) ( 𝐺 DProd ( 𝑇 ↾ { ( ♯ ‘ 𝑆 ) } ) ) ) )
152 137 140 oveq12d ( 𝜑 → ( ( 𝐺 DProd ( 𝑇 ↾ ( 0 ..^ ( ♯ ‘ 𝑆 ) ) ) ) ( LSSum ‘ 𝐺 ) ( 𝐺 DProd ( 𝑇 ↾ { ( ♯ ‘ 𝑆 ) } ) ) ) = ( 𝑊 ( LSSum ‘ 𝐺 ) ( 𝐾 ‘ { 𝑋 } ) ) )
153 137 132 eqeltrrd ( 𝜑𝑊 ∈ ( SubGrp ‘ 𝐺 ) )
154 150 lsmcom ( ( 𝐺 ∈ Abel ∧ 𝑊 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( 𝐾 ‘ { 𝑋 } ) ∈ ( SubGrp ‘ 𝐺 ) ) → ( 𝑊 ( LSSum ‘ 𝐺 ) ( 𝐾 ‘ { 𝑋 } ) ) = ( ( 𝐾 ‘ { 𝑋 } ) ( LSSum ‘ 𝐺 ) 𝑊 ) )
155 3 153 38 154 syl3anc ( 𝜑 → ( 𝑊 ( LSSum ‘ 𝐺 ) ( 𝐾 ‘ { 𝑋 } ) ) = ( ( 𝐾 ‘ { 𝑋 } ) ( LSSum ‘ 𝐺 ) 𝑊 ) )
156 151 152 155 3eqtrd ( 𝜑 → ( 𝐺 DProd 𝑇 ) = ( ( 𝐾 ‘ { 𝑋 } ) ( LSSum ‘ 𝐺 ) 𝑊 ) )
157 26 subgss ( 𝑊 ∈ ( SubGrp ‘ 𝐻 ) → 𝑊 ⊆ ( Base ‘ 𝐻 ) )
158 17 157 syl ( 𝜑𝑊 ⊆ ( Base ‘ 𝐻 ) )
159 158 31 sseqtrrd ( 𝜑𝑊𝑈 )
160 8 150 13 subglsm ( ( 𝑈 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( 𝐾 ‘ { 𝑋 } ) ⊆ 𝑈𝑊𝑈 ) → ( ( 𝐾 ‘ { 𝑋 } ) ( LSSum ‘ 𝐺 ) 𝑊 ) = ( ( 𝐾 ‘ { 𝑋 } ) 𝑊 ) )
161 6 40 159 160 syl3anc ( 𝜑 → ( ( 𝐾 ‘ { 𝑋 } ) ( LSSum ‘ 𝐺 ) 𝑊 ) = ( ( 𝐾 ‘ { 𝑋 } ) 𝑊 ) )
162 156 161 19 3eqtrd ( 𝜑 → ( 𝐺 DProd 𝑇 ) = 𝑈 )
163 breq2 ( 𝑠 = 𝑇 → ( 𝐺 dom DProd 𝑠𝐺 dom DProd 𝑇 ) )
164 oveq2 ( 𝑠 = 𝑇 → ( 𝐺 DProd 𝑠 ) = ( 𝐺 DProd 𝑇 ) )
165 164 eqeq1d ( 𝑠 = 𝑇 → ( ( 𝐺 DProd 𝑠 ) = 𝑈 ↔ ( 𝐺 DProd 𝑇 ) = 𝑈 ) )
166 163 165 anbi12d ( 𝑠 = 𝑇 → ( ( 𝐺 dom DProd 𝑠 ∧ ( 𝐺 DProd 𝑠 ) = 𝑈 ) ↔ ( 𝐺 dom DProd 𝑇 ∧ ( 𝐺 DProd 𝑇 ) = 𝑈 ) ) )
167 166 rspcev ( ( 𝑇 ∈ Word 𝐶 ∧ ( 𝐺 dom DProd 𝑇 ∧ ( 𝐺 DProd 𝑇 ) = 𝑈 ) ) → ∃ 𝑠 ∈ Word 𝐶 ( 𝐺 dom DProd 𝑠 ∧ ( 𝐺 DProd 𝑠 ) = 𝑈 ) )
168 58 149 162 167 syl12anc ( 𝜑 → ∃ 𝑠 ∈ Word 𝐶 ( 𝐺 dom DProd 𝑠 ∧ ( 𝐺 DProd 𝑠 ) = 𝑈 ) )