Metamath Proof Explorer

Theorem pgpfaclem3

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 𝑠 ) = 𝑡 ) ) )
Assertion pgpfaclem3 ( 𝜑 → ∃ 𝑠 ∈ 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 wrd0 ⊢ ∅ ∈ Word 𝐶
9 ablgrp ⊢ ( 𝐺 ∈ Abel → 𝐺 ∈ Grp )
10 eqid ⊢ ( 0g ‘ 𝐺 ) = ( 0g ‘ 𝐺 )
11 10 dprd0 ⊢ ( 𝐺 ∈ Grp → ( 𝐺 dom DProd ∅ ∧ ( 𝐺 DProd ∅ ) = { ( 0g ‘ 𝐺 ) } ) )
12 3 9 11 3syl ⊢ ( 𝜑 → ( 𝐺 dom DProd ∅ ∧ ( 𝐺 DProd ∅ ) = { ( 0g ‘ 𝐺 ) } ) )
13 12 adantr ⊢ ( ( 𝜑 ∧ ( gEx ‘ ( 𝐺 ↾s 𝑈 ) ) = 1 ) → ( 𝐺 dom DProd ∅ ∧ ( 𝐺 DProd ∅ ) = { ( 0g ‘ 𝐺 ) } ) )
14 10 subg0cl ⊢ ( 𝑈 ∈ ( SubGrp ‘ 𝐺 ) → ( 0g ‘ 𝐺 ) ∈ 𝑈 )
15 6 14 syl ⊢ ( 𝜑 → ( 0g ‘ 𝐺 ) ∈ 𝑈 )
16 15 adantr ⊢ ( ( 𝜑 ∧ ( gEx ‘ ( 𝐺 ↾s 𝑈 ) ) = 1 ) → ( 0g ‘ 𝐺 ) ∈ 𝑈 )
17 eqid ⊢ ( 𝐺 ↾s 𝑈 ) = ( 𝐺 ↾s 𝑈 )
18 17 subgbas ⊢ ( 𝑈 ∈ ( SubGrp ‘ 𝐺 ) → 𝑈 = ( Base ‘ ( 𝐺 ↾s 𝑈 ) ) )
19 6 18 syl ⊢ ( 𝜑 → 𝑈 = ( Base ‘ ( 𝐺 ↾s 𝑈 ) ) )
20 19 adantr ⊢ ( ( 𝜑 ∧ ( gEx ‘ ( 𝐺 ↾s 𝑈 ) ) = 1 ) → 𝑈 = ( Base ‘ ( 𝐺 ↾s 𝑈 ) ) )
21 17 subggrp ⊢ ( 𝑈 ∈ ( SubGrp ‘ 𝐺 ) → ( 𝐺 ↾s 𝑈 ) ∈ Grp )
22 6 21 syl ⊢ ( 𝜑 → ( 𝐺 ↾s 𝑈 ) ∈ Grp )
23 grpmnd ⊢ ( ( 𝐺 ↾s 𝑈 ) ∈ Grp → ( 𝐺 ↾s 𝑈 ) ∈ Mnd )
24 eqid ⊢ ( Base ‘ ( 𝐺 ↾s 𝑈 ) ) = ( Base ‘ ( 𝐺 ↾s 𝑈 ) )
25 eqid ⊢ ( gEx ‘ ( 𝐺 ↾s 𝑈 ) ) = ( gEx ‘ ( 𝐺 ↾s 𝑈 ) )
26 24 25 gex1 ⊢ ( ( 𝐺 ↾s 𝑈 ) ∈ Mnd → ( ( gEx ‘ ( 𝐺 ↾s 𝑈 ) ) = 1 ↔ ( Base ‘ ( 𝐺 ↾s 𝑈 ) ) ≈ 1o ) )
27 22 23 26 3syl ⊢ ( 𝜑 → ( ( gEx ‘ ( 𝐺 ↾s 𝑈 ) ) = 1 ↔ ( Base ‘ ( 𝐺 ↾s 𝑈 ) ) ≈ 1o ) )
28 27 biimpa ⊢ ( ( 𝜑 ∧ ( gEx ‘ ( 𝐺 ↾s 𝑈 ) ) = 1 ) → ( Base ‘ ( 𝐺 ↾s 𝑈 ) ) ≈ 1o )
29 20 28 eqbrtrd ⊢ ( ( 𝜑 ∧ ( gEx ‘ ( 𝐺 ↾s 𝑈 ) ) = 1 ) → 𝑈 ≈ 1o )
30 en1eqsn ⊢ ( ( ( 0g ‘ 𝐺 ) ∈ 𝑈 ∧ 𝑈 ≈ 1o ) → 𝑈 = { ( 0g ‘ 𝐺 ) } )
31 16 29 30 syl2anc ⊢ ( ( 𝜑 ∧ ( gEx ‘ ( 𝐺 ↾s 𝑈 ) ) = 1 ) → 𝑈 = { ( 0g ‘ 𝐺 ) } )
32 31 eqeq2d ⊢ ( ( 𝜑 ∧ ( gEx ‘ ( 𝐺 ↾s 𝑈 ) ) = 1 ) → ( ( 𝐺 DProd ∅ ) = 𝑈 ↔ ( 𝐺 DProd ∅ ) = { ( 0g ‘ 𝐺 ) } ) )
33 32 anbi2d ⊢ ( ( 𝜑 ∧ ( gEx ‘ ( 𝐺 ↾s 𝑈 ) ) = 1 ) → ( ( 𝐺 dom DProd ∅ ∧ ( 𝐺 DProd ∅ ) = 𝑈 ) ↔ ( 𝐺 dom DProd ∅ ∧ ( 𝐺 DProd ∅ ) = { ( 0g ‘ 𝐺 ) } ) ) )
34 13 33 mpbird ⊢ ( ( 𝜑 ∧ ( gEx ‘ ( 𝐺 ↾s 𝑈 ) ) = 1 ) → ( 𝐺 dom DProd ∅ ∧ ( 𝐺 DProd ∅ ) = 𝑈 ) )
35 breq2 ⊢ ( 𝑠 = ∅ → ( 𝐺 dom DProd 𝑠 ↔ 𝐺 dom DProd ∅ ) )
36 oveq2 ⊢ ( 𝑠 = ∅ → ( 𝐺 DProd 𝑠 ) = ( 𝐺 DProd ∅ ) )
37 36 eqeq1d ⊢ ( 𝑠 = ∅ → ( ( 𝐺 DProd 𝑠 ) = 𝑈 ↔ ( 𝐺 DProd ∅ ) = 𝑈 ) )
38 35 37 anbi12d ⊢ ( 𝑠 = ∅ → ( ( 𝐺 dom DProd 𝑠 ∧ ( 𝐺 DProd 𝑠 ) = 𝑈 ) ↔ ( 𝐺 dom DProd ∅ ∧ ( 𝐺 DProd ∅ ) = 𝑈 ) ) )
39 38 rspcev ⊢ ( ( ∅ ∈ Word 𝐶 ∧ ( 𝐺 dom DProd ∅ ∧ ( 𝐺 DProd ∅ ) = 𝑈 ) ) → ∃ 𝑠 ∈ Word 𝐶 ( 𝐺 dom DProd 𝑠 ∧ ( 𝐺 DProd 𝑠 ) = 𝑈 ) )
40 8 34 39 sylancr ⊢ ( ( 𝜑 ∧ ( gEx ‘ ( 𝐺 ↾s 𝑈 ) ) = 1 ) → ∃ 𝑠 ∈ Word 𝐶 ( 𝐺 dom DProd 𝑠 ∧ ( 𝐺 DProd 𝑠 ) = 𝑈 ) )
41 17 subgabl ⊢ ( ( 𝐺 ∈ Abel ∧ 𝑈 ∈ ( SubGrp ‘ 𝐺 ) ) → ( 𝐺 ↾s 𝑈 ) ∈ Abel )
42 3 6 41 syl2anc ⊢ ( 𝜑 → ( 𝐺 ↾s 𝑈 ) ∈ Abel )
43 1 subgss ⊢ ( 𝑈 ∈ ( SubGrp ‘ 𝐺 ) → 𝑈 ⊆ 𝐵 )
44 6 43 syl ⊢ ( 𝜑 → 𝑈 ⊆ 𝐵 )
45 5 44 ssfid ⊢ ( 𝜑 → 𝑈 ∈ Fin )
46 19 45 eqeltrrd ⊢ ( 𝜑 → ( Base ‘ ( 𝐺 ↾s 𝑈 ) ) ∈ Fin )
47 24 25 gexcl2 ⊢ ( ( ( 𝐺 ↾s 𝑈 ) ∈ Grp ∧ ( Base ‘ ( 𝐺 ↾s 𝑈 ) ) ∈ Fin ) → ( gEx ‘ ( 𝐺 ↾s 𝑈 ) ) ∈ ℕ )
48 22 46 47 syl2anc ⊢ ( 𝜑 → ( gEx ‘ ( 𝐺 ↾s 𝑈 ) ) ∈ ℕ )
49 eqid ⊢ ( od ‘ ( 𝐺 ↾s 𝑈 ) ) = ( od ‘ ( 𝐺 ↾s 𝑈 ) )
50 24 25 49 gexex ⊢ ( ( ( 𝐺 ↾s 𝑈 ) ∈ Abel ∧ ( gEx ‘ ( 𝐺 ↾s 𝑈 ) ) ∈ ℕ ) → ∃ 𝑥 ∈ ( Base ‘ ( 𝐺 ↾s 𝑈 ) ) ( ( od ‘ ( 𝐺 ↾s 𝑈 ) ) ‘ 𝑥 ) = ( gEx ‘ ( 𝐺 ↾s 𝑈 ) ) )
51 42 48 50 syl2anc ⊢ ( 𝜑 → ∃ 𝑥 ∈ ( Base ‘ ( 𝐺 ↾s 𝑈 ) ) ( ( od ‘ ( 𝐺 ↾s 𝑈 ) ) ‘ 𝑥 ) = ( gEx ‘ ( 𝐺 ↾s 𝑈 ) ) )
52 51 adantr ⊢ ( ( 𝜑 ∧ ( gEx ‘ ( 𝐺 ↾s 𝑈 ) ) ≠ 1 ) → ∃ 𝑥 ∈ ( Base ‘ ( 𝐺 ↾s 𝑈 ) ) ( ( od ‘ ( 𝐺 ↾s 𝑈 ) ) ‘ 𝑥 ) = ( gEx ‘ ( 𝐺 ↾s 𝑈 ) ) )
53 eqid ⊢ ( mrCls ‘ ( SubGrp ‘ ( 𝐺 ↾s 𝑈 ) ) ) = ( mrCls ‘ ( SubGrp ‘ ( 𝐺 ↾s 𝑈 ) ) )
54 eqid ⊢ ( ( mrCls ‘ ( SubGrp ‘ ( 𝐺 ↾s 𝑈 ) ) ) ‘ { 𝑥 } ) = ( ( mrCls ‘ ( SubGrp ‘ ( 𝐺 ↾s 𝑈 ) ) ) ‘ { 𝑥 } )
55 eqid ⊢ ( 0g ‘ ( 𝐺 ↾s 𝑈 ) ) = ( 0g ‘ ( 𝐺 ↾s 𝑈 ) )
56 eqid ⊢ ( LSSum ‘ ( 𝐺 ↾s 𝑈 ) ) = ( LSSum ‘ ( 𝐺 ↾s 𝑈 ) )
57 subgpgp ⊢ ( ( 𝑃 pGrp 𝐺 ∧ 𝑈 ∈ ( SubGrp ‘ 𝐺 ) ) → 𝑃 pGrp ( 𝐺 ↾s 𝑈 ) )
58 4 6 57 syl2anc ⊢ ( 𝜑 → 𝑃 pGrp ( 𝐺 ↾s 𝑈 ) )
59 58 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( gEx ‘ ( 𝐺 ↾s 𝑈 ) ) ≠ 1 ) ∧ ( 𝑥 ∈ ( Base ‘ ( 𝐺 ↾s 𝑈 ) ) ∧ ( ( od ‘ ( 𝐺 ↾s 𝑈 ) ) ‘ 𝑥 ) = ( gEx ‘ ( 𝐺 ↾s 𝑈 ) ) ) ) → 𝑃 pGrp ( 𝐺 ↾s 𝑈 ) )
60 42 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( gEx ‘ ( 𝐺 ↾s 𝑈 ) ) ≠ 1 ) ∧ ( 𝑥 ∈ ( Base ‘ ( 𝐺 ↾s 𝑈 ) ) ∧ ( ( od ‘ ( 𝐺 ↾s 𝑈 ) ) ‘ 𝑥 ) = ( gEx ‘ ( 𝐺 ↾s 𝑈 ) ) ) ) → ( 𝐺 ↾s 𝑈 ) ∈ Abel )
61 46 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( gEx ‘ ( 𝐺 ↾s 𝑈 ) ) ≠ 1 ) ∧ ( 𝑥 ∈ ( Base ‘ ( 𝐺 ↾s 𝑈 ) ) ∧ ( ( od ‘ ( 𝐺 ↾s 𝑈 ) ) ‘ 𝑥 ) = ( gEx ‘ ( 𝐺 ↾s 𝑈 ) ) ) ) → ( Base ‘ ( 𝐺 ↾s 𝑈 ) ) ∈ Fin )
62 simprr ⊢ ( ( ( 𝜑 ∧ ( gEx ‘ ( 𝐺 ↾s 𝑈 ) ) ≠ 1 ) ∧ ( 𝑥 ∈ ( Base ‘ ( 𝐺 ↾s 𝑈 ) ) ∧ ( ( od ‘ ( 𝐺 ↾s 𝑈 ) ) ‘ 𝑥 ) = ( gEx ‘ ( 𝐺 ↾s 𝑈 ) ) ) ) → ( ( od ‘ ( 𝐺 ↾s 𝑈 ) ) ‘ 𝑥 ) = ( gEx ‘ ( 𝐺 ↾s 𝑈 ) ) )
63 simprl ⊢ ( ( ( 𝜑 ∧ ( gEx ‘ ( 𝐺 ↾s 𝑈 ) ) ≠ 1 ) ∧ ( 𝑥 ∈ ( Base ‘ ( 𝐺 ↾s 𝑈 ) ) ∧ ( ( od ‘ ( 𝐺 ↾s 𝑈 ) ) ‘ 𝑥 ) = ( gEx ‘ ( 𝐺 ↾s 𝑈 ) ) ) ) → 𝑥 ∈ ( Base ‘ ( 𝐺 ↾s 𝑈 ) ) )
64 53 54 24 49 25 55 56 59 60 61 62 63 pgpfac1 ⊢ ( ( ( 𝜑 ∧ ( gEx ‘ ( 𝐺 ↾s 𝑈 ) ) ≠ 1 ) ∧ ( 𝑥 ∈ ( Base ‘ ( 𝐺 ↾s 𝑈 ) ) ∧ ( ( od ‘ ( 𝐺 ↾s 𝑈 ) ) ‘ 𝑥 ) = ( gEx ‘ ( 𝐺 ↾s 𝑈 ) ) ) ) → ∃ 𝑤 ∈ ( SubGrp ‘ ( 𝐺 ↾s 𝑈 ) ) ( ( ( ( mrCls ‘ ( SubGrp ‘ ( 𝐺 ↾s 𝑈 ) ) ) ‘ { 𝑥 } ) ∩ 𝑤 ) = { ( 0g ‘ ( 𝐺 ↾s 𝑈 ) ) } ∧ ( ( ( mrCls ‘ ( SubGrp ‘ ( 𝐺 ↾s 𝑈 ) ) ) ‘ { 𝑥 } ) ( LSSum ‘ ( 𝐺 ↾s 𝑈 ) ) 𝑤 ) = ( Base ‘ ( 𝐺 ↾s 𝑈 ) ) ) )
65 3 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ ( gEx ‘ ( 𝐺 ↾s 𝑈 ) ) ≠ 1 ) ∧ ( 𝑥 ∈ ( Base ‘ ( 𝐺 ↾s 𝑈 ) ) ∧ ( ( od ‘ ( 𝐺 ↾s 𝑈 ) ) ‘ 𝑥 ) = ( gEx ‘ ( 𝐺 ↾s 𝑈 ) ) ) ) ∧ ( 𝑤 ∈ ( SubGrp ‘ ( 𝐺 ↾s 𝑈 ) ) ∧ ( ( ( ( mrCls ‘ ( SubGrp ‘ ( 𝐺 ↾s 𝑈 ) ) ) ‘ { 𝑥 } ) ∩ 𝑤 ) = { ( 0g ‘ ( 𝐺 ↾s 𝑈 ) ) } ∧ ( ( ( mrCls ‘ ( SubGrp ‘ ( 𝐺 ↾s 𝑈 ) ) ) ‘ { 𝑥 } ) ( LSSum ‘ ( 𝐺 ↾s 𝑈 ) ) 𝑤 ) = ( Base ‘ ( 𝐺 ↾s 𝑈 ) ) ) ) ) → 𝐺 ∈ Abel )
66 4 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ ( gEx ‘ ( 𝐺 ↾s 𝑈 ) ) ≠ 1 ) ∧ ( 𝑥 ∈ ( Base ‘ ( 𝐺 ↾s 𝑈 ) ) ∧ ( ( od ‘ ( 𝐺 ↾s 𝑈 ) ) ‘ 𝑥 ) = ( gEx ‘ ( 𝐺 ↾s 𝑈 ) ) ) ) ∧ ( 𝑤 ∈ ( SubGrp ‘ ( 𝐺 ↾s 𝑈 ) ) ∧ ( ( ( ( mrCls ‘ ( SubGrp ‘ ( 𝐺 ↾s 𝑈 ) ) ) ‘ { 𝑥 } ) ∩ 𝑤 ) = { ( 0g ‘ ( 𝐺 ↾s 𝑈 ) ) } ∧ ( ( ( mrCls ‘ ( SubGrp ‘ ( 𝐺 ↾s 𝑈 ) ) ) ‘ { 𝑥 } ) ( LSSum ‘ ( 𝐺 ↾s 𝑈 ) ) 𝑤 ) = ( Base ‘ ( 𝐺 ↾s 𝑈 ) ) ) ) ) → 𝑃 pGrp 𝐺 )
67 5 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ ( gEx ‘ ( 𝐺 ↾s 𝑈 ) ) ≠ 1 ) ∧ ( 𝑥 ∈ ( Base ‘ ( 𝐺 ↾s 𝑈 ) ) ∧ ( ( od ‘ ( 𝐺 ↾s 𝑈 ) ) ‘ 𝑥 ) = ( gEx ‘ ( 𝐺 ↾s 𝑈 ) ) ) ) ∧ ( 𝑤 ∈ ( SubGrp ‘ ( 𝐺 ↾s 𝑈 ) ) ∧ ( ( ( ( mrCls ‘ ( SubGrp ‘ ( 𝐺 ↾s 𝑈 ) ) ) ‘ { 𝑥 } ) ∩ 𝑤 ) = { ( 0g ‘ ( 𝐺 ↾s 𝑈 ) ) } ∧ ( ( ( mrCls ‘ ( SubGrp ‘ ( 𝐺 ↾s 𝑈 ) ) ) ‘ { 𝑥 } ) ( LSSum ‘ ( 𝐺 ↾s 𝑈 ) ) 𝑤 ) = ( Base ‘ ( 𝐺 ↾s 𝑈 ) ) ) ) ) → 𝐵 ∈ Fin )
68 6 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ ( gEx ‘ ( 𝐺 ↾s 𝑈 ) ) ≠ 1 ) ∧ ( 𝑥 ∈ ( Base ‘ ( 𝐺 ↾s 𝑈 ) ) ∧ ( ( od ‘ ( 𝐺 ↾s 𝑈 ) ) ‘ 𝑥 ) = ( gEx ‘ ( 𝐺 ↾s 𝑈 ) ) ) ) ∧ ( 𝑤 ∈ ( SubGrp ‘ ( 𝐺 ↾s 𝑈 ) ) ∧ ( ( ( ( mrCls ‘ ( SubGrp ‘ ( 𝐺 ↾s 𝑈 ) ) ) ‘ { 𝑥 } ) ∩ 𝑤 ) = { ( 0g ‘ ( 𝐺 ↾s 𝑈 ) ) } ∧ ( ( ( mrCls ‘ ( SubGrp ‘ ( 𝐺 ↾s 𝑈 ) ) ) ‘ { 𝑥 } ) ( LSSum ‘ ( 𝐺 ↾s 𝑈 ) ) 𝑤 ) = ( Base ‘ ( 𝐺 ↾s 𝑈 ) ) ) ) ) → 𝑈 ∈ ( SubGrp ‘ 𝐺 ) )
69 7 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ ( gEx ‘ ( 𝐺 ↾s 𝑈 ) ) ≠ 1 ) ∧ ( 𝑥 ∈ ( Base ‘ ( 𝐺 ↾s 𝑈 ) ) ∧ ( ( od ‘ ( 𝐺 ↾s 𝑈 ) ) ‘ 𝑥 ) = ( gEx ‘ ( 𝐺 ↾s 𝑈 ) ) ) ) ∧ ( 𝑤 ∈ ( SubGrp ‘ ( 𝐺 ↾s 𝑈 ) ) ∧ ( ( ( ( mrCls ‘ ( SubGrp ‘ ( 𝐺 ↾s 𝑈 ) ) ) ‘ { 𝑥 } ) ∩ 𝑤 ) = { ( 0g ‘ ( 𝐺 ↾s 𝑈 ) ) } ∧ ( ( ( mrCls ‘ ( SubGrp ‘ ( 𝐺 ↾s 𝑈 ) ) ) ‘ { 𝑥 } ) ( LSSum ‘ ( 𝐺 ↾s 𝑈 ) ) 𝑤 ) = ( Base ‘ ( 𝐺 ↾s 𝑈 ) ) ) ) ) → ∀ 𝑡 ∈ ( SubGrp ‘ 𝐺 ) ( 𝑡 ⊊ 𝑈 → ∃ 𝑠 ∈ Word 𝐶 ( 𝐺 dom DProd 𝑠 ∧ ( 𝐺 DProd 𝑠 ) = 𝑡 ) ) )
70 simpllr ⊢ ( ( ( ( 𝜑 ∧ ( gEx ‘ ( 𝐺 ↾s 𝑈 ) ) ≠ 1 ) ∧ ( 𝑥 ∈ ( Base ‘ ( 𝐺 ↾s 𝑈 ) ) ∧ ( ( od ‘ ( 𝐺 ↾s 𝑈 ) ) ‘ 𝑥 ) = ( gEx ‘ ( 𝐺 ↾s 𝑈 ) ) ) ) ∧ ( 𝑤 ∈ ( SubGrp ‘ ( 𝐺 ↾s 𝑈 ) ) ∧ ( ( ( ( mrCls ‘ ( SubGrp ‘ ( 𝐺 ↾s 𝑈 ) ) ) ‘ { 𝑥 } ) ∩ 𝑤 ) = { ( 0g ‘ ( 𝐺 ↾s 𝑈 ) ) } ∧ ( ( ( mrCls ‘ ( SubGrp ‘ ( 𝐺 ↾s 𝑈 ) ) ) ‘ { 𝑥 } ) ( LSSum ‘ ( 𝐺 ↾s 𝑈 ) ) 𝑤 ) = ( Base ‘ ( 𝐺 ↾s 𝑈 ) ) ) ) ) → ( gEx ‘ ( 𝐺 ↾s 𝑈 ) ) ≠ 1 )
71 simplrl ⊢ ( ( ( ( 𝜑 ∧ ( gEx ‘ ( 𝐺 ↾s 𝑈 ) ) ≠ 1 ) ∧ ( 𝑥 ∈ ( Base ‘ ( 𝐺 ↾s 𝑈 ) ) ∧ ( ( od ‘ ( 𝐺 ↾s 𝑈 ) ) ‘ 𝑥 ) = ( gEx ‘ ( 𝐺 ↾s 𝑈 ) ) ) ) ∧ ( 𝑤 ∈ ( SubGrp ‘ ( 𝐺 ↾s 𝑈 ) ) ∧ ( ( ( ( mrCls ‘ ( SubGrp ‘ ( 𝐺 ↾s 𝑈 ) ) ) ‘ { 𝑥 } ) ∩ 𝑤 ) = { ( 0g ‘ ( 𝐺 ↾s 𝑈 ) ) } ∧ ( ( ( mrCls ‘ ( SubGrp ‘ ( 𝐺 ↾s 𝑈 ) ) ) ‘ { 𝑥 } ) ( LSSum ‘ ( 𝐺 ↾s 𝑈 ) ) 𝑤 ) = ( Base ‘ ( 𝐺 ↾s 𝑈 ) ) ) ) ) → 𝑥 ∈ ( Base ‘ ( 𝐺 ↾s 𝑈 ) ) )
72 68 18 syl ⊢ ( ( ( ( 𝜑 ∧ ( gEx ‘ ( 𝐺 ↾s 𝑈 ) ) ≠ 1 ) ∧ ( 𝑥 ∈ ( Base ‘ ( 𝐺 ↾s 𝑈 ) ) ∧ ( ( od ‘ ( 𝐺 ↾s 𝑈 ) ) ‘ 𝑥 ) = ( gEx ‘ ( 𝐺 ↾s 𝑈 ) ) ) ) ∧ ( 𝑤 ∈ ( SubGrp ‘ ( 𝐺 ↾s 𝑈 ) ) ∧ ( ( ( ( mrCls ‘ ( SubGrp ‘ ( 𝐺 ↾s 𝑈 ) ) ) ‘ { 𝑥 } ) ∩ 𝑤 ) = { ( 0g ‘ ( 𝐺 ↾s 𝑈 ) ) } ∧ ( ( ( mrCls ‘ ( SubGrp ‘ ( 𝐺 ↾s 𝑈 ) ) ) ‘ { 𝑥 } ) ( LSSum ‘ ( 𝐺 ↾s 𝑈 ) ) 𝑤 ) = ( Base ‘ ( 𝐺 ↾s 𝑈 ) ) ) ) ) → 𝑈 = ( Base ‘ ( 𝐺 ↾s 𝑈 ) ) )
73 71 72 eleqtrrd ⊢ ( ( ( ( 𝜑 ∧ ( gEx ‘ ( 𝐺 ↾s 𝑈 ) ) ≠ 1 ) ∧ ( 𝑥 ∈ ( Base ‘ ( 𝐺 ↾s 𝑈 ) ) ∧ ( ( od ‘ ( 𝐺 ↾s 𝑈 ) ) ‘ 𝑥 ) = ( gEx ‘ ( 𝐺 ↾s 𝑈 ) ) ) ) ∧ ( 𝑤 ∈ ( SubGrp ‘ ( 𝐺 ↾s 𝑈 ) ) ∧ ( ( ( ( mrCls ‘ ( SubGrp ‘ ( 𝐺 ↾s 𝑈 ) ) ) ‘ { 𝑥 } ) ∩ 𝑤 ) = { ( 0g ‘ ( 𝐺 ↾s 𝑈 ) ) } ∧ ( ( ( mrCls ‘ ( SubGrp ‘ ( 𝐺 ↾s 𝑈 ) ) ) ‘ { 𝑥 } ) ( LSSum ‘ ( 𝐺 ↾s 𝑈 ) ) 𝑤 ) = ( Base ‘ ( 𝐺 ↾s 𝑈 ) ) ) ) ) → 𝑥 ∈ 𝑈 )
74 simplrr ⊢ ( ( ( ( 𝜑 ∧ ( gEx ‘ ( 𝐺 ↾s 𝑈 ) ) ≠ 1 ) ∧ ( 𝑥 ∈ ( Base ‘ ( 𝐺 ↾s 𝑈 ) ) ∧ ( ( od ‘ ( 𝐺 ↾s 𝑈 ) ) ‘ 𝑥 ) = ( gEx ‘ ( 𝐺 ↾s 𝑈 ) ) ) ) ∧ ( 𝑤 ∈ ( SubGrp ‘ ( 𝐺 ↾s 𝑈 ) ) ∧ ( ( ( ( mrCls ‘ ( SubGrp ‘ ( 𝐺 ↾s 𝑈 ) ) ) ‘ { 𝑥 } ) ∩ 𝑤 ) = { ( 0g ‘ ( 𝐺 ↾s 𝑈 ) ) } ∧ ( ( ( mrCls ‘ ( SubGrp ‘ ( 𝐺 ↾s 𝑈 ) ) ) ‘ { 𝑥 } ) ( LSSum ‘ ( 𝐺 ↾s 𝑈 ) ) 𝑤 ) = ( Base ‘ ( 𝐺 ↾s 𝑈 ) ) ) ) ) → ( ( od ‘ ( 𝐺 ↾s 𝑈 ) ) ‘ 𝑥 ) = ( gEx ‘ ( 𝐺 ↾s 𝑈 ) ) )
75 simprl ⊢ ( ( ( ( 𝜑 ∧ ( gEx ‘ ( 𝐺 ↾s 𝑈 ) ) ≠ 1 ) ∧ ( 𝑥 ∈ ( Base ‘ ( 𝐺 ↾s 𝑈 ) ) ∧ ( ( od ‘ ( 𝐺 ↾s 𝑈 ) ) ‘ 𝑥 ) = ( gEx ‘ ( 𝐺 ↾s 𝑈 ) ) ) ) ∧ ( 𝑤 ∈ ( SubGrp ‘ ( 𝐺 ↾s 𝑈 ) ) ∧ ( ( ( ( mrCls ‘ ( SubGrp ‘ ( 𝐺 ↾s 𝑈 ) ) ) ‘ { 𝑥 } ) ∩ 𝑤 ) = { ( 0g ‘ ( 𝐺 ↾s 𝑈 ) ) } ∧ ( ( ( mrCls ‘ ( SubGrp ‘ ( 𝐺 ↾s 𝑈 ) ) ) ‘ { 𝑥 } ) ( LSSum ‘ ( 𝐺 ↾s 𝑈 ) ) 𝑤 ) = ( Base ‘ ( 𝐺 ↾s 𝑈 ) ) ) ) ) → 𝑤 ∈ ( SubGrp ‘ ( 𝐺 ↾s 𝑈 ) ) )
76 simprrl ⊢ ( ( ( ( 𝜑 ∧ ( gEx ‘ ( 𝐺 ↾s 𝑈 ) ) ≠ 1 ) ∧ ( 𝑥 ∈ ( Base ‘ ( 𝐺 ↾s 𝑈 ) ) ∧ ( ( od ‘ ( 𝐺 ↾s 𝑈 ) ) ‘ 𝑥 ) = ( gEx ‘ ( 𝐺 ↾s 𝑈 ) ) ) ) ∧ ( 𝑤 ∈ ( SubGrp ‘ ( 𝐺 ↾s 𝑈 ) ) ∧ ( ( ( ( mrCls ‘ ( SubGrp ‘ ( 𝐺 ↾s 𝑈 ) ) ) ‘ { 𝑥 } ) ∩ 𝑤 ) = { ( 0g ‘ ( 𝐺 ↾s 𝑈 ) ) } ∧ ( ( ( mrCls ‘ ( SubGrp ‘ ( 𝐺 ↾s 𝑈 ) ) ) ‘ { 𝑥 } ) ( LSSum ‘ ( 𝐺 ↾s 𝑈 ) ) 𝑤 ) = ( Base ‘ ( 𝐺 ↾s 𝑈 ) ) ) ) ) → ( ( ( mrCls ‘ ( SubGrp ‘ ( 𝐺 ↾s 𝑈 ) ) ) ‘ { 𝑥 } ) ∩ 𝑤 ) = { ( 0g ‘ ( 𝐺 ↾s 𝑈 ) ) } )
77 simprrr ⊢ ( ( ( ( 𝜑 ∧ ( gEx ‘ ( 𝐺 ↾s 𝑈 ) ) ≠ 1 ) ∧ ( 𝑥 ∈ ( Base ‘ ( 𝐺 ↾s 𝑈 ) ) ∧ ( ( od ‘ ( 𝐺 ↾s 𝑈 ) ) ‘ 𝑥 ) = ( gEx ‘ ( 𝐺 ↾s 𝑈 ) ) ) ) ∧ ( 𝑤 ∈ ( SubGrp ‘ ( 𝐺 ↾s 𝑈 ) ) ∧ ( ( ( ( mrCls ‘ ( SubGrp ‘ ( 𝐺 ↾s 𝑈 ) ) ) ‘ { 𝑥 } ) ∩ 𝑤 ) = { ( 0g ‘ ( 𝐺 ↾s 𝑈 ) ) } ∧ ( ( ( mrCls ‘ ( SubGrp ‘ ( 𝐺 ↾s 𝑈 ) ) ) ‘ { 𝑥 } ) ( LSSum ‘ ( 𝐺 ↾s 𝑈 ) ) 𝑤 ) = ( Base ‘ ( 𝐺 ↾s 𝑈 ) ) ) ) ) → ( ( ( mrCls ‘ ( SubGrp ‘ ( 𝐺 ↾s 𝑈 ) ) ) ‘ { 𝑥 } ) ( LSSum ‘ ( 𝐺 ↾s 𝑈 ) ) 𝑤 ) = ( Base ‘ ( 𝐺 ↾s 𝑈 ) ) )
78 77 72 eqtr4d ⊢ ( ( ( ( 𝜑 ∧ ( gEx ‘ ( 𝐺 ↾s 𝑈 ) ) ≠ 1 ) ∧ ( 𝑥 ∈ ( Base ‘ ( 𝐺 ↾s 𝑈 ) ) ∧ ( ( od ‘ ( 𝐺 ↾s 𝑈 ) ) ‘ 𝑥 ) = ( gEx ‘ ( 𝐺 ↾s 𝑈 ) ) ) ) ∧ ( 𝑤 ∈ ( SubGrp ‘ ( 𝐺 ↾s 𝑈 ) ) ∧ ( ( ( ( mrCls ‘ ( SubGrp ‘ ( 𝐺 ↾s 𝑈 ) ) ) ‘ { 𝑥 } ) ∩ 𝑤 ) = { ( 0g ‘ ( 𝐺 ↾s 𝑈 ) ) } ∧ ( ( ( mrCls ‘ ( SubGrp ‘ ( 𝐺 ↾s 𝑈 ) ) ) ‘ { 𝑥 } ) ( LSSum ‘ ( 𝐺 ↾s 𝑈 ) ) 𝑤 ) = ( Base ‘ ( 𝐺 ↾s 𝑈 ) ) ) ) ) → ( ( ( mrCls ‘ ( SubGrp ‘ ( 𝐺 ↾s 𝑈 ) ) ) ‘ { 𝑥 } ) ( LSSum ‘ ( 𝐺 ↾s 𝑈 ) ) 𝑤 ) = 𝑈 )
79 1 2 65 66 67 68 69 17 53 49 25 55 56 70 73 74 75 76 78 pgpfaclem2 ⊢ ( ( ( ( 𝜑 ∧ ( gEx ‘ ( 𝐺 ↾s 𝑈 ) ) ≠ 1 ) ∧ ( 𝑥 ∈ ( Base ‘ ( 𝐺 ↾s 𝑈 ) ) ∧ ( ( od ‘ ( 𝐺 ↾s 𝑈 ) ) ‘ 𝑥 ) = ( gEx ‘ ( 𝐺 ↾s 𝑈 ) ) ) ) ∧ ( 𝑤 ∈ ( SubGrp ‘ ( 𝐺 ↾s 𝑈 ) ) ∧ ( ( ( ( mrCls ‘ ( SubGrp ‘ ( 𝐺 ↾s 𝑈 ) ) ) ‘ { 𝑥 } ) ∩ 𝑤 ) = { ( 0g ‘ ( 𝐺 ↾s 𝑈 ) ) } ∧ ( ( ( mrCls ‘ ( SubGrp ‘ ( 𝐺 ↾s 𝑈 ) ) ) ‘ { 𝑥 } ) ( LSSum ‘ ( 𝐺 ↾s 𝑈 ) ) 𝑤 ) = ( Base ‘ ( 𝐺 ↾s 𝑈 ) ) ) ) ) → ∃ 𝑠 ∈ Word 𝐶 ( 𝐺 dom DProd 𝑠 ∧ ( 𝐺 DProd 𝑠 ) = 𝑈 ) )
80 64 79 rexlimddv ⊢ ( ( ( 𝜑 ∧ ( gEx ‘ ( 𝐺 ↾s 𝑈 ) ) ≠ 1 ) ∧ ( 𝑥 ∈ ( Base ‘ ( 𝐺 ↾s 𝑈 ) ) ∧ ( ( od ‘ ( 𝐺 ↾s 𝑈 ) ) ‘ 𝑥 ) = ( gEx ‘ ( 𝐺 ↾s 𝑈 ) ) ) ) → ∃ 𝑠 ∈ Word 𝐶 ( 𝐺 dom DProd 𝑠 ∧ ( 𝐺 DProd 𝑠 ) = 𝑈 ) )
81 52 80 rexlimddv ⊢ ( ( 𝜑 ∧ ( gEx ‘ ( 𝐺 ↾s 𝑈 ) ) ≠ 1 ) → ∃ 𝑠 ∈ Word 𝐶 ( 𝐺 dom DProd 𝑠 ∧ ( 𝐺 DProd 𝑠 ) = 𝑈 ) )
82 40 81 pm2.61dane ⊢ ( 𝜑 → ∃ 𝑠 ∈ Word 𝐶 ( 𝐺 dom DProd 𝑠 ∧ ( 𝐺 DProd 𝑠 ) = 𝑈 ) )