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

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 eqtrid ⊢ ( 𝜑 → ( 𝐻 ↾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 eqtrid ⊢ ( 𝜑 → ( ♯ ‘ 𝑇 ) = ( ( ♯ ‘ 𝑆 ) + ( ♯ ‘ ⟨“ ( 𝐾 ‘ { 𝑋 } ) ”⟩ ) ) )
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 eqtrid ⊢ ( 𝜑 → 𝑇 = ( 𝑆 ∪ { ⟨ ( ♯ ‘ 𝑆 ) , ( 𝐾 ‘ { 𝑋 } ) ⟩ } ) )
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 addlidd ⊢ ( 𝜑 → ( 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 𝑠 ) = 𝑈 ) )