Metamath Proof Explorer

Theorem pgpfaclem2

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 ⊢ ( 𝜑 → ( ( 𝐾 ‘ { 𝑋 } ) ⊕ 𝑊 ) = 𝑈 )
Assertion pgpfaclem2 ( 𝜑 → ∃ 𝑠 ∈ 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 8 subsubg ⊢ ( 𝑈 ∈ ( SubGrp ‘ 𝐺 ) → ( 𝑊 ∈ ( SubGrp ‘ 𝐻 ) ↔ ( 𝑊 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑊 ⊆ 𝑈 ) ) )
21 6 20 syl ⊢ ( 𝜑 → ( 𝑊 ∈ ( SubGrp ‘ 𝐻 ) ↔ ( 𝑊 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑊 ⊆ 𝑈 ) ) )
22 17 21 mpbid ⊢ ( 𝜑 → ( 𝑊 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑊 ⊆ 𝑈 ) )
23 22 simprd ⊢ ( 𝜑 → 𝑊 ⊆ 𝑈 )
24 1 subgss ⊢ ( 𝑈 ∈ ( SubGrp ‘ 𝐺 ) → 𝑈 ⊆ 𝐵 )
25 6 24 syl ⊢ ( 𝜑 → 𝑈 ⊆ 𝐵 )
26 5 25 ssfid ⊢ ( 𝜑 → 𝑈 ∈ Fin )
27 26 23 ssfid ⊢ ( 𝜑 → 𝑊 ∈ Fin )
28 hashcl ⊢ ( 𝑊 ∈ Fin → ( ♯ ‘ 𝑊 ) ∈ ℕ0 )
29 27 28 syl ⊢ ( 𝜑 → ( ♯ ‘ 𝑊 ) ∈ ℕ0 )
30 29 nn0red ⊢ ( 𝜑 → ( ♯ ‘ 𝑊 ) ∈ ℝ )
31 12 fvexi ⊢ 0 ∈ V
32 hashsng ⊢ ( 0 ∈ V → ( ♯ ‘ { 0 } ) = 1 )
33 31 32 ax-mp ⊢ ( ♯ ‘ { 0 } ) = 1
34 subgrcl ⊢ ( 𝑊 ∈ ( SubGrp ‘ 𝐻 ) → 𝐻 ∈ Grp )
35 eqid ⊢ ( Base ‘ 𝐻 ) = ( Base ‘ 𝐻 )
36 35 subgacs ⊢ ( 𝐻 ∈ Grp → ( SubGrp ‘ 𝐻 ) ∈ ( ACS ‘ ( Base ‘ 𝐻 ) ) )
37 acsmre ⊢ ( ( SubGrp ‘ 𝐻 ) ∈ ( ACS ‘ ( Base ‘ 𝐻 ) ) → ( SubGrp ‘ 𝐻 ) ∈ ( Moore ‘ ( Base ‘ 𝐻 ) ) )
38 17 34 36 37 4syl ⊢ ( 𝜑 → ( SubGrp ‘ 𝐻 ) ∈ ( Moore ‘ ( Base ‘ 𝐻 ) ) )
39 38 9 mrcssvd ⊢ ( 𝜑 → ( 𝐾 ‘ { 𝑋 } ) ⊆ ( Base ‘ 𝐻 ) )
40 8 subgbas ⊢ ( 𝑈 ∈ ( SubGrp ‘ 𝐺 ) → 𝑈 = ( Base ‘ 𝐻 ) )
41 6 40 syl ⊢ ( 𝜑 → 𝑈 = ( Base ‘ 𝐻 ) )
42 39 41 sseqtrrd ⊢ ( 𝜑 → ( 𝐾 ‘ { 𝑋 } ) ⊆ 𝑈 )
43 26 42 ssfid ⊢ ( 𝜑 → ( 𝐾 ‘ { 𝑋 } ) ∈ Fin )
44 15 41 eleqtrd ⊢ ( 𝜑 → 𝑋 ∈ ( Base ‘ 𝐻 ) )
45 9 mrcsncl ⊢ ( ( ( SubGrp ‘ 𝐻 ) ∈ ( Moore ‘ ( Base ‘ 𝐻 ) ) ∧ 𝑋 ∈ ( Base ‘ 𝐻 ) ) → ( 𝐾 ‘ { 𝑋 } ) ∈ ( SubGrp ‘ 𝐻 ) )
46 38 44 45 syl2anc ⊢ ( 𝜑 → ( 𝐾 ‘ { 𝑋 } ) ∈ ( SubGrp ‘ 𝐻 ) )
47 12 subg0cl ⊢ ( ( 𝐾 ‘ { 𝑋 } ) ∈ ( SubGrp ‘ 𝐻 ) → 0 ∈ ( 𝐾 ‘ { 𝑋 } ) )
48 46 47 syl ⊢ ( 𝜑 → 0 ∈ ( 𝐾 ‘ { 𝑋 } ) )
49 48 snssd ⊢ ( 𝜑 → { 0 } ⊆ ( 𝐾 ‘ { 𝑋 } ) )
50 44 snssd ⊢ ( 𝜑 → { 𝑋 } ⊆ ( Base ‘ 𝐻 ) )
51 38 9 50 mrcssidd ⊢ ( 𝜑 → { 𝑋 } ⊆ ( 𝐾 ‘ { 𝑋 } ) )
52 snssg ⊢ ( 𝑋 ∈ 𝑈 → ( 𝑋 ∈ ( 𝐾 ‘ { 𝑋 } ) ↔ { 𝑋 } ⊆ ( 𝐾 ‘ { 𝑋 } ) ) )
53 15 52 syl ⊢ ( 𝜑 → ( 𝑋 ∈ ( 𝐾 ‘ { 𝑋 } ) ↔ { 𝑋 } ⊆ ( 𝐾 ‘ { 𝑋 } ) ) )
54 51 53 mpbird ⊢ ( 𝜑 → 𝑋 ∈ ( 𝐾 ‘ { 𝑋 } ) )
55 16 14 eqnetrd ⊢ ( 𝜑 → ( 𝑂 ‘ 𝑋 ) ≠ 1 )
56 10 12 od1 ⊢ ( 𝐻 ∈ Grp → ( 𝑂 ‘ 0 ) = 1 )
57 17 34 56 3syl ⊢ ( 𝜑 → ( 𝑂 ‘ 0 ) = 1 )
58 elsni ⊢ ( 𝑋 ∈ { 0 } → 𝑋 = 0 )
59 58 fveqeq2d ⊢ ( 𝑋 ∈ { 0 } → ( ( 𝑂 ‘ 𝑋 ) = 1 ↔ ( 𝑂 ‘ 0 ) = 1 ) )
60 57 59 syl5ibrcom ⊢ ( 𝜑 → ( 𝑋 ∈ { 0 } → ( 𝑂 ‘ 𝑋 ) = 1 ) )
61 60 necon3ad ⊢ ( 𝜑 → ( ( 𝑂 ‘ 𝑋 ) ≠ 1 → ¬ 𝑋 ∈ { 0 } ) )
62 55 61 mpd ⊢ ( 𝜑 → ¬ 𝑋 ∈ { 0 } )
63 49 54 62 ssnelpssd ⊢ ( 𝜑 → { 0 } ⊊ ( 𝐾 ‘ { 𝑋 } ) )
64 php3 ⊢ ( ( ( 𝐾 ‘ { 𝑋 } ) ∈ Fin ∧ { 0 } ⊊ ( 𝐾 ‘ { 𝑋 } ) ) → { 0 } ≺ ( 𝐾 ‘ { 𝑋 } ) )
65 43 63 64 syl2anc ⊢ ( 𝜑 → { 0 } ≺ ( 𝐾 ‘ { 𝑋 } ) )
66 snfi ⊢ { 0 } ∈ Fin
67 hashsdom ⊢ ( ( { 0 } ∈ Fin ∧ ( 𝐾 ‘ { 𝑋 } ) ∈ Fin ) → ( ( ♯ ‘ { 0 } ) < ( ♯ ‘ ( 𝐾 ‘ { 𝑋 } ) ) ↔ { 0 } ≺ ( 𝐾 ‘ { 𝑋 } ) ) )
68 66 43 67 sylancr ⊢ ( 𝜑 → ( ( ♯ ‘ { 0 } ) < ( ♯ ‘ ( 𝐾 ‘ { 𝑋 } ) ) ↔ { 0 } ≺ ( 𝐾 ‘ { 𝑋 } ) ) )
69 65 68 mpbird ⊢ ( 𝜑 → ( ♯ ‘ { 0 } ) < ( ♯ ‘ ( 𝐾 ‘ { 𝑋 } ) ) )
70 33 69 eqbrtrrid ⊢ ( 𝜑 → 1 < ( ♯ ‘ ( 𝐾 ‘ { 𝑋 } ) ) )
71 1red ⊢ ( 𝜑 → 1 ∈ ℝ )
72 hashcl ⊢ ( ( 𝐾 ‘ { 𝑋 } ) ∈ Fin → ( ♯ ‘ ( 𝐾 ‘ { 𝑋 } ) ) ∈ ℕ0 )
73 43 72 syl ⊢ ( 𝜑 → ( ♯ ‘ ( 𝐾 ‘ { 𝑋 } ) ) ∈ ℕ0 )
74 73 nn0red ⊢ ( 𝜑 → ( ♯ ‘ ( 𝐾 ‘ { 𝑋 } ) ) ∈ ℝ )
75 12 subg0cl ⊢ ( 𝑊 ∈ ( SubGrp ‘ 𝐻 ) → 0 ∈ 𝑊 )
76 ne0i ⊢ ( 0 ∈ 𝑊 → 𝑊 ≠ ∅ )
77 17 75 76 3syl ⊢ ( 𝜑 → 𝑊 ≠ ∅ )
78 hashnncl ⊢ ( 𝑊 ∈ Fin → ( ( ♯ ‘ 𝑊 ) ∈ ℕ ↔ 𝑊 ≠ ∅ ) )
79 27 78 syl ⊢ ( 𝜑 → ( ( ♯ ‘ 𝑊 ) ∈ ℕ ↔ 𝑊 ≠ ∅ ) )
80 77 79 mpbird ⊢ ( 𝜑 → ( ♯ ‘ 𝑊 ) ∈ ℕ )
81 80 nngt0d ⊢ ( 𝜑 → 0 < ( ♯ ‘ 𝑊 ) )
82 ltmul1 ⊢ ( ( 1 ∈ ℝ ∧ ( ♯ ‘ ( 𝐾 ‘ { 𝑋 } ) ) ∈ ℝ ∧ ( ( ♯ ‘ 𝑊 ) ∈ ℝ ∧ 0 < ( ♯ ‘ 𝑊 ) ) ) → ( 1 < ( ♯ ‘ ( 𝐾 ‘ { 𝑋 } ) ) ↔ ( 1 · ( ♯ ‘ 𝑊 ) ) < ( ( ♯ ‘ ( 𝐾 ‘ { 𝑋 } ) ) · ( ♯ ‘ 𝑊 ) ) ) )
83 71 74 30 81 82 syl112anc ⊢ ( 𝜑 → ( 1 < ( ♯ ‘ ( 𝐾 ‘ { 𝑋 } ) ) ↔ ( 1 · ( ♯ ‘ 𝑊 ) ) < ( ( ♯ ‘ ( 𝐾 ‘ { 𝑋 } ) ) · ( ♯ ‘ 𝑊 ) ) ) )
84 70 83 mpbid ⊢ ( 𝜑 → ( 1 · ( ♯ ‘ 𝑊 ) ) < ( ( ♯ ‘ ( 𝐾 ‘ { 𝑋 } ) ) · ( ♯ ‘ 𝑊 ) ) )
85 30 recnd ⊢ ( 𝜑 → ( ♯ ‘ 𝑊 ) ∈ ℂ )
86 85 mulid2d ⊢ ( 𝜑 → ( 1 · ( ♯ ‘ 𝑊 ) ) = ( ♯ ‘ 𝑊 ) )
87 eqid ⊢ ( Cntz ‘ 𝐻 ) = ( Cntz ‘ 𝐻 )
88 8 subgabl ⊢ ( ( 𝐺 ∈ Abel ∧ 𝑈 ∈ ( SubGrp ‘ 𝐺 ) ) → 𝐻 ∈ Abel )
89 3 6 88 syl2anc ⊢ ( 𝜑 → 𝐻 ∈ Abel )
90 87 89 46 17 ablcntzd ⊢ ( 𝜑 → ( 𝐾 ‘ { 𝑋 } ) ⊆ ( ( Cntz ‘ 𝐻 ) ‘ 𝑊 ) )
91 13 12 87 46 17 18 90 43 27 lsmhash ⊢ ( 𝜑 → ( ♯ ‘ ( ( 𝐾 ‘ { 𝑋 } ) ⊕ 𝑊 ) ) = ( ( ♯ ‘ ( 𝐾 ‘ { 𝑋 } ) ) · ( ♯ ‘ 𝑊 ) ) )
92 19 fveq2d ⊢ ( 𝜑 → ( ♯ ‘ ( ( 𝐾 ‘ { 𝑋 } ) ⊕ 𝑊 ) ) = ( ♯ ‘ 𝑈 ) )
93 91 92 eqtr3d ⊢ ( 𝜑 → ( ( ♯ ‘ ( 𝐾 ‘ { 𝑋 } ) ) · ( ♯ ‘ 𝑊 ) ) = ( ♯ ‘ 𝑈 ) )
94 84 86 93 3brtr3d ⊢ ( 𝜑 → ( ♯ ‘ 𝑊 ) < ( ♯ ‘ 𝑈 ) )
95 30 94 ltned ⊢ ( 𝜑 → ( ♯ ‘ 𝑊 ) ≠ ( ♯ ‘ 𝑈 ) )
96 fveq2 ⊢ ( 𝑊 = 𝑈 → ( ♯ ‘ 𝑊 ) = ( ♯ ‘ 𝑈 ) )
97 96 necon3i ⊢ ( ( ♯ ‘ 𝑊 ) ≠ ( ♯ ‘ 𝑈 ) → 𝑊 ≠ 𝑈 )
98 95 97 syl ⊢ ( 𝜑 → 𝑊 ≠ 𝑈 )
99 df-pss ⊢ ( 𝑊 ⊊ 𝑈 ↔ ( 𝑊 ⊆ 𝑈 ∧ 𝑊 ≠ 𝑈 ) )
100 23 98 99 sylanbrc ⊢ ( 𝜑 → 𝑊 ⊊ 𝑈 )
101 psseq1 ⊢ ( 𝑡 = 𝑊 → ( 𝑡 ⊊ 𝑈 ↔ 𝑊 ⊊ 𝑈 ) )
102 eqeq2 ⊢ ( 𝑡 = 𝑊 → ( ( 𝐺 DProd 𝑠 ) = 𝑡 ↔ ( 𝐺 DProd 𝑠 ) = 𝑊 ) )
103 102 anbi2d ⊢ ( 𝑡 = 𝑊 → ( ( 𝐺 dom DProd 𝑠 ∧ ( 𝐺 DProd 𝑠 ) = 𝑡 ) ↔ ( 𝐺 dom DProd 𝑠 ∧ ( 𝐺 DProd 𝑠 ) = 𝑊 ) ) )
104 103 rexbidv ⊢ ( 𝑡 = 𝑊 → ( ∃ 𝑠 ∈ Word 𝐶 ( 𝐺 dom DProd 𝑠 ∧ ( 𝐺 DProd 𝑠 ) = 𝑡 ) ↔ ∃ 𝑠 ∈ Word 𝐶 ( 𝐺 dom DProd 𝑠 ∧ ( 𝐺 DProd 𝑠 ) = 𝑊 ) ) )
105 101 104 imbi12d ⊢ ( 𝑡 = 𝑊 → ( ( 𝑡 ⊊ 𝑈 → ∃ 𝑠 ∈ Word 𝐶 ( 𝐺 dom DProd 𝑠 ∧ ( 𝐺 DProd 𝑠 ) = 𝑡 ) ) ↔ ( 𝑊 ⊊ 𝑈 → ∃ 𝑠 ∈ Word 𝐶 ( 𝐺 dom DProd 𝑠 ∧ ( 𝐺 DProd 𝑠 ) = 𝑊 ) ) ) )
106 22 simpld ⊢ ( 𝜑 → 𝑊 ∈ ( SubGrp ‘ 𝐺 ) )
107 105 7 106 rspcdva ⊢ ( 𝜑 → ( 𝑊 ⊊ 𝑈 → ∃ 𝑠 ∈ Word 𝐶 ( 𝐺 dom DProd 𝑠 ∧ ( 𝐺 DProd 𝑠 ) = 𝑊 ) ) )
108 100 107 mpd ⊢ ( 𝜑 → ∃ 𝑠 ∈ Word 𝐶 ( 𝐺 dom DProd 𝑠 ∧ ( 𝐺 DProd 𝑠 ) = 𝑊 ) )
109 breq2 ⊢ ( 𝑠 = 𝑎 → ( 𝐺 dom DProd 𝑠 ↔ 𝐺 dom DProd 𝑎 ) )
110 oveq2 ⊢ ( 𝑠 = 𝑎 → ( 𝐺 DProd 𝑠 ) = ( 𝐺 DProd 𝑎 ) )
111 110 eqeq1d ⊢ ( 𝑠 = 𝑎 → ( ( 𝐺 DProd 𝑠 ) = 𝑊 ↔ ( 𝐺 DProd 𝑎 ) = 𝑊 ) )
112 109 111 anbi12d ⊢ ( 𝑠 = 𝑎 → ( ( 𝐺 dom DProd 𝑠 ∧ ( 𝐺 DProd 𝑠 ) = 𝑊 ) ↔ ( 𝐺 dom DProd 𝑎 ∧ ( 𝐺 DProd 𝑎 ) = 𝑊 ) ) )
113 112 cbvrexvw ⊢ ( ∃ 𝑠 ∈ Word 𝐶 ( 𝐺 dom DProd 𝑠 ∧ ( 𝐺 DProd 𝑠 ) = 𝑊 ) ↔ ∃ 𝑎 ∈ Word 𝐶 ( 𝐺 dom DProd 𝑎 ∧ ( 𝐺 DProd 𝑎 ) = 𝑊 ) )
114 108 113 sylib ⊢ ( 𝜑 → ∃ 𝑎 ∈ Word 𝐶 ( 𝐺 dom DProd 𝑎 ∧ ( 𝐺 DProd 𝑎 ) = 𝑊 ) )
115 3 adantr ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ Word 𝐶 ∧ ( 𝐺 dom DProd 𝑎 ∧ ( 𝐺 DProd 𝑎 ) = 𝑊 ) ) ) → 𝐺 ∈ Abel )
116 4 adantr ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ Word 𝐶 ∧ ( 𝐺 dom DProd 𝑎 ∧ ( 𝐺 DProd 𝑎 ) = 𝑊 ) ) ) → 𝑃 pGrp 𝐺 )
117 5 adantr ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ Word 𝐶 ∧ ( 𝐺 dom DProd 𝑎 ∧ ( 𝐺 DProd 𝑎 ) = 𝑊 ) ) ) → 𝐵 ∈ Fin )
118 6 adantr ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ Word 𝐶 ∧ ( 𝐺 dom DProd 𝑎 ∧ ( 𝐺 DProd 𝑎 ) = 𝑊 ) ) ) → 𝑈 ∈ ( SubGrp ‘ 𝐺 ) )
119 7 adantr ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ Word 𝐶 ∧ ( 𝐺 dom DProd 𝑎 ∧ ( 𝐺 DProd 𝑎 ) = 𝑊 ) ) ) → ∀ 𝑡 ∈ ( SubGrp ‘ 𝐺 ) ( 𝑡 ⊊ 𝑈 → ∃ 𝑠 ∈ Word 𝐶 ( 𝐺 dom DProd 𝑠 ∧ ( 𝐺 DProd 𝑠 ) = 𝑡 ) ) )
120 14 adantr ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ Word 𝐶 ∧ ( 𝐺 dom DProd 𝑎 ∧ ( 𝐺 DProd 𝑎 ) = 𝑊 ) ) ) → 𝐸 ≠ 1 )
121 15 adantr ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ Word 𝐶 ∧ ( 𝐺 dom DProd 𝑎 ∧ ( 𝐺 DProd 𝑎 ) = 𝑊 ) ) ) → 𝑋 ∈ 𝑈 )
122 16 adantr ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ Word 𝐶 ∧ ( 𝐺 dom DProd 𝑎 ∧ ( 𝐺 DProd 𝑎 ) = 𝑊 ) ) ) → ( 𝑂 ‘ 𝑋 ) = 𝐸 )
123 17 adantr ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ Word 𝐶 ∧ ( 𝐺 dom DProd 𝑎 ∧ ( 𝐺 DProd 𝑎 ) = 𝑊 ) ) ) → 𝑊 ∈ ( SubGrp ‘ 𝐻 ) )
124 18 adantr ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ Word 𝐶 ∧ ( 𝐺 dom DProd 𝑎 ∧ ( 𝐺 DProd 𝑎 ) = 𝑊 ) ) ) → ( ( 𝐾 ‘ { 𝑋 } ) ∩ 𝑊 ) = { 0 } )
125 19 adantr ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ Word 𝐶 ∧ ( 𝐺 dom DProd 𝑎 ∧ ( 𝐺 DProd 𝑎 ) = 𝑊 ) ) ) → ( ( 𝐾 ‘ { 𝑋 } ) ⊕ 𝑊 ) = 𝑈 )
126 simprl ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ Word 𝐶 ∧ ( 𝐺 dom DProd 𝑎 ∧ ( 𝐺 DProd 𝑎 ) = 𝑊 ) ) ) → 𝑎 ∈ Word 𝐶 )
127 simprrl ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ Word 𝐶 ∧ ( 𝐺 dom DProd 𝑎 ∧ ( 𝐺 DProd 𝑎 ) = 𝑊 ) ) ) → 𝐺 dom DProd 𝑎 )
128 simprrr ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ Word 𝐶 ∧ ( 𝐺 dom DProd 𝑎 ∧ ( 𝐺 DProd 𝑎 ) = 𝑊 ) ) ) → ( 𝐺 DProd 𝑎 ) = 𝑊 )
129 eqid ⊢ ( 𝑎 ++ ⟨“ ( 𝐾 ‘ { 𝑋 } ) ”⟩ ) = ( 𝑎 ++ ⟨“ ( 𝐾 ‘ { 𝑋 } ) ”⟩ )
130 1 2 115 116 117 118 119 8 9 10 11 12 13 120 121 122 123 124 125 126 127 128 129 pgpfaclem1 ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ Word 𝐶 ∧ ( 𝐺 dom DProd 𝑎 ∧ ( 𝐺 DProd 𝑎 ) = 𝑊 ) ) ) → ∃ 𝑠 ∈ Word 𝐶 ( 𝐺 dom DProd 𝑠 ∧ ( 𝐺 DProd 𝑠 ) = 𝑈 ) )
131 114 130 rexlimddv ⊢ ( 𝜑 → ∃ 𝑠 ∈ Word 𝐶 ( 𝐺 dom DProd 𝑠 ∧ ( 𝐺 DProd 𝑠 ) = 𝑈 ) )