MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  pgpfaclem1 Structured version   Visualization version   GIF version

Theorem pgpfaclem1 18956
Description: Lemma for pgpfac 18959. (Contributed by Mario Carneiro, 27-Apr-2016.) (Revised by Mario Carneiro, 3-May-2016.)
Hypotheses
Ref Expression
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
Ref Expression
pgpfaclem1 (𝜑 → ∃𝑠 ∈ Word 𝐶(𝐺dom DProd 𝑠 ∧ (𝐺 DProd 𝑠) = 𝑈))
Distinct variable groups:   𝑡,𝑠,𝐶   𝑠,𝑟,𝑡,𝐺   𝐾,𝑟,𝑠   𝜑,𝑡   𝐵,𝑠,𝑡   𝑈,𝑟,𝑠,𝑡   𝑊,𝑠,𝑡   𝑋,𝑟,𝑠   𝑇,𝑠
Allowed substitution hints:   𝜑(𝑠,𝑟)   𝐵(𝑟)   𝐶(𝑟)   𝑃(𝑡,𝑠,𝑟)   (𝑡,𝑠,𝑟)   𝑆(𝑡,𝑠,𝑟)   𝑇(𝑡,𝑟)   𝐸(𝑡,𝑠,𝑟)   𝐻(𝑡,𝑠,𝑟)   𝐾(𝑡)   𝑂(𝑡,𝑠,𝑟)   𝑊(𝑟)   𝑋(𝑡)   0 (𝑡,𝑠,𝑟)

Proof of Theorem pgpfaclem1
StepHypRef Expression
1 pgpfac.t . . 3 𝑇 = (𝑆 ++ ⟨“(𝐾‘{𝑋})”⟩)
2 pgpfac.2 . . 3 (𝜑𝑆 ∈ Word 𝐶)
3 pgpfac.u . . . . . . . . 9 (𝜑𝑈 ∈ (SubGrp‘𝐺))
4 pgpfac.h . . . . . . . . . 10 𝐻 = (𝐺s 𝑈)
54subggrp 18069 . . . . . . . . 9 (𝑈 ∈ (SubGrp‘𝐺) → 𝐻 ∈ Grp)
63, 5syl 17 . . . . . . . 8 (𝜑𝐻 ∈ Grp)
7 eqid 2778 . . . . . . . . 9 (Base‘𝐻) = (Base‘𝐻)
87subgacs 18101 . . . . . . . 8 (𝐻 ∈ Grp → (SubGrp‘𝐻) ∈ (ACS‘(Base‘𝐻)))
9 acsmre 16784 . . . . . . . 8 ((SubGrp‘𝐻) ∈ (ACS‘(Base‘𝐻)) → (SubGrp‘𝐻) ∈ (Moore‘(Base‘𝐻)))
106, 8, 93syl 18 . . . . . . 7 (𝜑 → (SubGrp‘𝐻) ∈ (Moore‘(Base‘𝐻)))
11 pgpfac.x . . . . . . . 8 (𝜑𝑋𝑈)
124subgbas 18070 . . . . . . . . 9 (𝑈 ∈ (SubGrp‘𝐺) → 𝑈 = (Base‘𝐻))
133, 12syl 17 . . . . . . . 8 (𝜑𝑈 = (Base‘𝐻))
1411, 13eleqtrd 2868 . . . . . . 7 (𝜑𝑋 ∈ (Base‘𝐻))
15 pgpfac.k . . . . . . . 8 𝐾 = (mrCls‘(SubGrp‘𝐻))
1615mrcsncl 16744 . . . . . . 7 (((SubGrp‘𝐻) ∈ (Moore‘(Base‘𝐻)) ∧ 𝑋 ∈ (Base‘𝐻)) → (𝐾‘{𝑋}) ∈ (SubGrp‘𝐻))
1710, 14, 16syl2anc 576 . . . . . 6 (𝜑 → (𝐾‘{𝑋}) ∈ (SubGrp‘𝐻))
184subsubg 18089 . . . . . . 7 (𝑈 ∈ (SubGrp‘𝐺) → ((𝐾‘{𝑋}) ∈ (SubGrp‘𝐻) ↔ ((𝐾‘{𝑋}) ∈ (SubGrp‘𝐺) ∧ (𝐾‘{𝑋}) ⊆ 𝑈)))
193, 18syl 17 . . . . . 6 (𝜑 → ((𝐾‘{𝑋}) ∈ (SubGrp‘𝐻) ↔ ((𝐾‘{𝑋}) ∈ (SubGrp‘𝐺) ∧ (𝐾‘{𝑋}) ⊆ 𝑈)))
2017, 19mpbid 224 . . . . 5 (𝜑 → ((𝐾‘{𝑋}) ∈ (SubGrp‘𝐺) ∧ (𝐾‘{𝑋}) ⊆ 𝑈))
2120simpld 487 . . . 4 (𝜑 → (𝐾‘{𝑋}) ∈ (SubGrp‘𝐺))
224oveq1i 6988 . . . . . . 7 (𝐻s (𝐾‘{𝑋})) = ((𝐺s 𝑈) ↾s (𝐾‘{𝑋}))
2320simprd 488 . . . . . . . 8 (𝜑 → (𝐾‘{𝑋}) ⊆ 𝑈)
24 ressabs 16422 . . . . . . . 8 ((𝑈 ∈ (SubGrp‘𝐺) ∧ (𝐾‘{𝑋}) ⊆ 𝑈) → ((𝐺s 𝑈) ↾s (𝐾‘{𝑋})) = (𝐺s (𝐾‘{𝑋})))
253, 23, 24syl2anc 576 . . . . . . 7 (𝜑 → ((𝐺s 𝑈) ↾s (𝐾‘{𝑋})) = (𝐺s (𝐾‘{𝑋})))
2622, 25syl5eq 2826 . . . . . 6 (𝜑 → (𝐻s (𝐾‘{𝑋})) = (𝐺s (𝐾‘{𝑋})))
277, 15cycsubgcyg2 18779 . . . . . . 7 ((𝐻 ∈ Grp ∧ 𝑋 ∈ (Base‘𝐻)) → (𝐻s (𝐾‘{𝑋})) ∈ CycGrp)
286, 14, 27syl2anc 576 . . . . . 6 (𝜑 → (𝐻s (𝐾‘{𝑋})) ∈ CycGrp)
2926, 28eqeltrrd 2867 . . . . 5 (𝜑 → (𝐺s (𝐾‘{𝑋})) ∈ CycGrp)
30 pgpfac.p . . . . . . 7 (𝜑𝑃 pGrp 𝐺)
31 pgpprm 18482 . . . . . . 7 (𝑃 pGrp 𝐺𝑃 ∈ ℙ)
3230, 31syl 17 . . . . . 6 (𝜑𝑃 ∈ ℙ)
33 subgpgp 18486 . . . . . . 7 ((𝑃 pGrp 𝐺 ∧ (𝐾‘{𝑋}) ∈ (SubGrp‘𝐺)) → 𝑃 pGrp (𝐺s (𝐾‘{𝑋})))
3430, 21, 33syl2anc 576 . . . . . 6 (𝜑𝑃 pGrp (𝐺s (𝐾‘{𝑋})))
35 brelrng 5655 . . . . . 6 ((𝑃 ∈ ℙ ∧ (𝐺s (𝐾‘{𝑋})) ∈ CycGrp ∧ 𝑃 pGrp (𝐺s (𝐾‘{𝑋}))) → (𝐺s (𝐾‘{𝑋})) ∈ ran pGrp )
3632, 29, 34, 35syl3anc 1351 . . . . 5 (𝜑 → (𝐺s (𝐾‘{𝑋})) ∈ ran pGrp )
3729, 36elind 4061 . . . 4 (𝜑 → (𝐺s (𝐾‘{𝑋})) ∈ (CycGrp ∩ ran pGrp ))
38 oveq2 6986 . . . . . 6 (𝑟 = (𝐾‘{𝑋}) → (𝐺s 𝑟) = (𝐺s (𝐾‘{𝑋})))
3938eleq1d 2850 . . . . 5 (𝑟 = (𝐾‘{𝑋}) → ((𝐺s 𝑟) ∈ (CycGrp ∩ ran pGrp ) ↔ (𝐺s (𝐾‘{𝑋})) ∈ (CycGrp ∩ ran pGrp )))
40 pgpfac.c . . . . 5 𝐶 = {𝑟 ∈ (SubGrp‘𝐺) ∣ (𝐺s 𝑟) ∈ (CycGrp ∩ ran pGrp )}
4139, 40elrab2 3599 . . . 4 ((𝐾‘{𝑋}) ∈ 𝐶 ↔ ((𝐾‘{𝑋}) ∈ (SubGrp‘𝐺) ∧ (𝐺s (𝐾‘{𝑋})) ∈ (CycGrp ∩ ran pGrp )))
4221, 37, 41sylanbrc 575 . . 3 (𝜑 → (𝐾‘{𝑋}) ∈ 𝐶)
431, 2, 42cats1cld 14082 . 2 (𝜑𝑇 ∈ Word 𝐶)
44 wrdf 13680 . . . . 5 (𝑇 ∈ Word 𝐶𝑇:(0..^(♯‘𝑇))⟶𝐶)
4543, 44syl 17 . . . 4 (𝜑𝑇:(0..^(♯‘𝑇))⟶𝐶)
4640ssrab3 3949 . . . 4 𝐶 ⊆ (SubGrp‘𝐺)
47 fss 6359 . . . 4 ((𝑇:(0..^(♯‘𝑇))⟶𝐶𝐶 ⊆ (SubGrp‘𝐺)) → 𝑇:(0..^(♯‘𝑇))⟶(SubGrp‘𝐺))
4845, 46, 47sylancl 577 . . 3 (𝜑𝑇:(0..^(♯‘𝑇))⟶(SubGrp‘𝐺))
49 fzodisj 12889 . . . 4 ((0..^(♯‘𝑆)) ∩ ((♯‘𝑆)..^((♯‘𝑆) + 1))) = ∅
50 lencl 13697 . . . . . . . 8 (𝑆 ∈ Word 𝐶 → (♯‘𝑆) ∈ ℕ0)
512, 50syl 17 . . . . . . 7 (𝜑 → (♯‘𝑆) ∈ ℕ0)
5251nn0zd 11901 . . . . . 6 (𝜑 → (♯‘𝑆) ∈ ℤ)
53 fzosn 12926 . . . . . 6 ((♯‘𝑆) ∈ ℤ → ((♯‘𝑆)..^((♯‘𝑆) + 1)) = {(♯‘𝑆)})
5452, 53syl 17 . . . . 5 (𝜑 → ((♯‘𝑆)..^((♯‘𝑆) + 1)) = {(♯‘𝑆)})
5554ineq2d 4078 . . . 4 (𝜑 → ((0..^(♯‘𝑆)) ∩ ((♯‘𝑆)..^((♯‘𝑆) + 1))) = ((0..^(♯‘𝑆)) ∩ {(♯‘𝑆)}))
5649, 55syl5reqr 2829 . . 3 (𝜑 → ((0..^(♯‘𝑆)) ∩ {(♯‘𝑆)}) = ∅)
571fveq2i 6504 . . . . . . 7 (♯‘𝑇) = (♯‘(𝑆 ++ ⟨“(𝐾‘{𝑋})”⟩))
5842s1cld 13769 . . . . . . . 8 (𝜑 → ⟨“(𝐾‘{𝑋})”⟩ ∈ Word 𝐶)
59 ccatlen 13741 . . . . . . . 8 ((𝑆 ∈ Word 𝐶 ∧ ⟨“(𝐾‘{𝑋})”⟩ ∈ Word 𝐶) → (♯‘(𝑆 ++ ⟨“(𝐾‘{𝑋})”⟩)) = ((♯‘𝑆) + (♯‘⟨“(𝐾‘{𝑋})”⟩)))
602, 58, 59syl2anc 576 . . . . . . 7 (𝜑 → (♯‘(𝑆 ++ ⟨“(𝐾‘{𝑋})”⟩)) = ((♯‘𝑆) + (♯‘⟨“(𝐾‘{𝑋})”⟩)))
6157, 60syl5eq 2826 . . . . . 6 (𝜑 → (♯‘𝑇) = ((♯‘𝑆) + (♯‘⟨“(𝐾‘{𝑋})”⟩)))
62 s1len 13772 . . . . . . 7 (♯‘⟨“(𝐾‘{𝑋})”⟩) = 1
6362oveq2i 6989 . . . . . 6 ((♯‘𝑆) + (♯‘⟨“(𝐾‘{𝑋})”⟩)) = ((♯‘𝑆) + 1)
6461, 63syl6eq 2830 . . . . 5 (𝜑 → (♯‘𝑇) = ((♯‘𝑆) + 1))
6564oveq2d 6994 . . . 4 (𝜑 → (0..^(♯‘𝑇)) = (0..^((♯‘𝑆) + 1)))
66 nn0uz 12097 . . . . . 6 0 = (ℤ‘0)
6751, 66syl6eleq 2876 . . . . 5 (𝜑 → (♯‘𝑆) ∈ (ℤ‘0))
68 fzosplitsn 12963 . . . . 5 ((♯‘𝑆) ∈ (ℤ‘0) → (0..^((♯‘𝑆) + 1)) = ((0..^(♯‘𝑆)) ∪ {(♯‘𝑆)}))
6967, 68syl 17 . . . 4 (𝜑 → (0..^((♯‘𝑆) + 1)) = ((0..^(♯‘𝑆)) ∪ {(♯‘𝑆)}))
7065, 69eqtrd 2814 . . 3 (𝜑 → (0..^(♯‘𝑇)) = ((0..^(♯‘𝑆)) ∪ {(♯‘𝑆)}))
71 eqid 2778 . . 3 (Cntz‘𝐺) = (Cntz‘𝐺)
72 eqid 2778 . . 3 (0g𝐺) = (0g𝐺)
73 pgpfac.4 . . . 4 (𝜑𝐺dom DProd 𝑆)
74 cats1un 13917 . . . . . . . 8 ((𝑆 ∈ Word 𝐶 ∧ (𝐾‘{𝑋}) ∈ 𝐶) → (𝑆 ++ ⟨“(𝐾‘{𝑋})”⟩) = (𝑆 ∪ {⟨(♯‘𝑆), (𝐾‘{𝑋})⟩}))
752, 42, 74syl2anc 576 . . . . . . 7 (𝜑 → (𝑆 ++ ⟨“(𝐾‘{𝑋})”⟩) = (𝑆 ∪ {⟨(♯‘𝑆), (𝐾‘{𝑋})⟩}))
761, 75syl5eq 2826 . . . . . 6 (𝜑𝑇 = (𝑆 ∪ {⟨(♯‘𝑆), (𝐾‘{𝑋})⟩}))
7776reseq1d 5695 . . . . 5 (𝜑 → (𝑇 ↾ (0..^(♯‘𝑆))) = ((𝑆 ∪ {⟨(♯‘𝑆), (𝐾‘{𝑋})⟩}) ↾ (0..^(♯‘𝑆))))
78 wrdf 13680 . . . . . . 7 (𝑆 ∈ Word 𝐶𝑆:(0..^(♯‘𝑆))⟶𝐶)
79 ffn 6346 . . . . . . 7 (𝑆:(0..^(♯‘𝑆))⟶𝐶𝑆 Fn (0..^(♯‘𝑆)))
802, 78, 793syl 18 . . . . . 6 (𝜑𝑆 Fn (0..^(♯‘𝑆)))
81 fzonel 12870 . . . . . 6 ¬ (♯‘𝑆) ∈ (0..^(♯‘𝑆))
82 fsnunres 6779 . . . . . 6 ((𝑆 Fn (0..^(♯‘𝑆)) ∧ ¬ (♯‘𝑆) ∈ (0..^(♯‘𝑆))) → ((𝑆 ∪ {⟨(♯‘𝑆), (𝐾‘{𝑋})⟩}) ↾ (0..^(♯‘𝑆))) = 𝑆)
8380, 81, 82sylancl 577 . . . . 5 (𝜑 → ((𝑆 ∪ {⟨(♯‘𝑆), (𝐾‘{𝑋})⟩}) ↾ (0..^(♯‘𝑆))) = 𝑆)
8477, 83eqtrd 2814 . . . 4 (𝜑 → (𝑇 ↾ (0..^(♯‘𝑆))) = 𝑆)
8573, 84breqtrrd 4958 . . 3 (𝜑𝐺dom DProd (𝑇 ↾ (0..^(♯‘𝑆))))
86 fvex 6514 . . . . . 6 (♯‘𝑆) ∈ V
87 dprdsn 18911 . . . . . 6 (((♯‘𝑆) ∈ V ∧ (𝐾‘{𝑋}) ∈ (SubGrp‘𝐺)) → (𝐺dom DProd {⟨(♯‘𝑆), (𝐾‘{𝑋})⟩} ∧ (𝐺 DProd {⟨(♯‘𝑆), (𝐾‘{𝑋})⟩}) = (𝐾‘{𝑋})))
8886, 21, 87sylancr 578 . . . . 5 (𝜑 → (𝐺dom DProd {⟨(♯‘𝑆), (𝐾‘{𝑋})⟩} ∧ (𝐺 DProd {⟨(♯‘𝑆), (𝐾‘{𝑋})⟩}) = (𝐾‘{𝑋})))
8988simpld 487 . . . 4 (𝜑𝐺dom DProd {⟨(♯‘𝑆), (𝐾‘{𝑋})⟩})
90 ffn 6346 . . . . . . 7 (𝑇:(0..^(♯‘𝑇))⟶𝐶𝑇 Fn (0..^(♯‘𝑇)))
9143, 44, 903syl 18 . . . . . 6 (𝜑𝑇 Fn (0..^(♯‘𝑇)))
92 ssun2 4040 . . . . . . . 8 {(♯‘𝑆)} ⊆ ((0..^(♯‘𝑆)) ∪ {(♯‘𝑆)})
9386snss 4593 . . . . . . . 8 ((♯‘𝑆) ∈ ((0..^(♯‘𝑆)) ∪ {(♯‘𝑆)}) ↔ {(♯‘𝑆)} ⊆ ((0..^(♯‘𝑆)) ∪ {(♯‘𝑆)}))
9492, 93mpbir 223 . . . . . . 7 (♯‘𝑆) ∈ ((0..^(♯‘𝑆)) ∪ {(♯‘𝑆)})
9594, 70syl5eleqr 2873 . . . . . 6 (𝜑 → (♯‘𝑆) ∈ (0..^(♯‘𝑇)))
96 fnressn 6745 . . . . . 6 ((𝑇 Fn (0..^(♯‘𝑇)) ∧ (♯‘𝑆) ∈ (0..^(♯‘𝑇))) → (𝑇 ↾ {(♯‘𝑆)}) = {⟨(♯‘𝑆), (𝑇‘(♯‘𝑆))⟩})
9791, 95, 96syl2anc 576 . . . . 5 (𝜑 → (𝑇 ↾ {(♯‘𝑆)}) = {⟨(♯‘𝑆), (𝑇‘(♯‘𝑆))⟩})
981fveq1i 6502 . . . . . . . . 9 (𝑇‘(♯‘𝑆)) = ((𝑆 ++ ⟨“(𝐾‘{𝑋})”⟩)‘(♯‘𝑆))
9951nn0cnd 11772 . . . . . . . . . . . 12 (𝜑 → (♯‘𝑆) ∈ ℂ)
10099addid2d 10643 . . . . . . . . . . 11 (𝜑 → (0 + (♯‘𝑆)) = (♯‘𝑆))
101100eqcomd 2784 . . . . . . . . . 10 (𝜑 → (♯‘𝑆) = (0 + (♯‘𝑆)))
102101fveq2d 6505 . . . . . . . . 9 (𝜑 → ((𝑆 ++ ⟨“(𝐾‘{𝑋})”⟩)‘(♯‘𝑆)) = ((𝑆 ++ ⟨“(𝐾‘{𝑋})”⟩)‘(0 + (♯‘𝑆))))
10398, 102syl5eq 2826 . . . . . . . 8 (𝜑 → (𝑇‘(♯‘𝑆)) = ((𝑆 ++ ⟨“(𝐾‘{𝑋})”⟩)‘(0 + (♯‘𝑆))))
104 1nn 11454 . . . . . . . . . . . 12 1 ∈ ℕ
105104a1i 11 . . . . . . . . . . 11 (𝜑 → 1 ∈ ℕ)
10662, 105syl5eqel 2870 . . . . . . . . . 10 (𝜑 → (♯‘⟨“(𝐾‘{𝑋})”⟩) ∈ ℕ)
107 lbfzo0 12895 . . . . . . . . . 10 (0 ∈ (0..^(♯‘⟨“(𝐾‘{𝑋})”⟩)) ↔ (♯‘⟨“(𝐾‘{𝑋})”⟩) ∈ ℕ)
108106, 107sylibr 226 . . . . . . . . 9 (𝜑 → 0 ∈ (0..^(♯‘⟨“(𝐾‘{𝑋})”⟩)))
109 ccatval3 13745 . . . . . . . . 9 ((𝑆 ∈ Word 𝐶 ∧ ⟨“(𝐾‘{𝑋})”⟩ ∈ Word 𝐶 ∧ 0 ∈ (0..^(♯‘⟨“(𝐾‘{𝑋})”⟩))) → ((𝑆 ++ ⟨“(𝐾‘{𝑋})”⟩)‘(0 + (♯‘𝑆))) = (⟨“(𝐾‘{𝑋})”⟩‘0))
1102, 58, 108, 109syl3anc 1351 . . . . . . . 8 (𝜑 → ((𝑆 ++ ⟨“(𝐾‘{𝑋})”⟩)‘(0 + (♯‘𝑆))) = (⟨“(𝐾‘{𝑋})”⟩‘0))
111 fvex 6514 . . . . . . . . 9 (𝐾‘{𝑋}) ∈ V
112 s1fv 13776 . . . . . . . . 9 ((𝐾‘{𝑋}) ∈ V → (⟨“(𝐾‘{𝑋})”⟩‘0) = (𝐾‘{𝑋}))
113111, 112mp1i 13 . . . . . . . 8 (𝜑 → (⟨“(𝐾‘{𝑋})”⟩‘0) = (𝐾‘{𝑋}))
114103, 110, 1133eqtrd 2818 . . . . . . 7 (𝜑 → (𝑇‘(♯‘𝑆)) = (𝐾‘{𝑋}))
115114opeq2d 4685 . . . . . 6 (𝜑 → ⟨(♯‘𝑆), (𝑇‘(♯‘𝑆))⟩ = ⟨(♯‘𝑆), (𝐾‘{𝑋})⟩)
116115sneqd 4454 . . . . 5 (𝜑 → {⟨(♯‘𝑆), (𝑇‘(♯‘𝑆))⟩} = {⟨(♯‘𝑆), (𝐾‘{𝑋})⟩})
11797, 116eqtrd 2814 . . . 4 (𝜑 → (𝑇 ↾ {(♯‘𝑆)}) = {⟨(♯‘𝑆), (𝐾‘{𝑋})⟩})
11889, 117breqtrrd 4958 . . 3 (𝜑𝐺dom DProd (𝑇 ↾ {(♯‘𝑆)}))
119 pgpfac.g . . . 4 (𝜑𝐺 ∈ Abel)
120 dprdsubg 18899 . . . . 5 (𝐺dom DProd (𝑇 ↾ (0..^(♯‘𝑆))) → (𝐺 DProd (𝑇 ↾ (0..^(♯‘𝑆)))) ∈ (SubGrp‘𝐺))
12185, 120syl 17 . . . 4 (𝜑 → (𝐺 DProd (𝑇 ↾ (0..^(♯‘𝑆)))) ∈ (SubGrp‘𝐺))
122 dprdsubg 18899 . . . . 5 (𝐺dom DProd (𝑇 ↾ {(♯‘𝑆)}) → (𝐺 DProd (𝑇 ↾ {(♯‘𝑆)})) ∈ (SubGrp‘𝐺))
123118, 122syl 17 . . . 4 (𝜑 → (𝐺 DProd (𝑇 ↾ {(♯‘𝑆)})) ∈ (SubGrp‘𝐺))
12471, 119, 121, 123ablcntzd 18736 . . 3 (𝜑 → (𝐺 DProd (𝑇 ↾ (0..^(♯‘𝑆)))) ⊆ ((Cntz‘𝐺)‘(𝐺 DProd (𝑇 ↾ {(♯‘𝑆)}))))
125 pgpfac.i . . . 4 (𝜑 → ((𝐾‘{𝑋}) ∩ 𝑊) = { 0 })
12684oveq2d 6994 . . . . . . 7 (𝜑 → (𝐺 DProd (𝑇 ↾ (0..^(♯‘𝑆)))) = (𝐺 DProd 𝑆))
127 pgpfac.5 . . . . . . 7 (𝜑 → (𝐺 DProd 𝑆) = 𝑊)
128126, 127eqtrd 2814 . . . . . 6 (𝜑 → (𝐺 DProd (𝑇 ↾ (0..^(♯‘𝑆)))) = 𝑊)
129117oveq2d 6994 . . . . . . 7 (𝜑 → (𝐺 DProd (𝑇 ↾ {(♯‘𝑆)})) = (𝐺 DProd {⟨(♯‘𝑆), (𝐾‘{𝑋})⟩}))
13088simprd 488 . . . . . . 7 (𝜑 → (𝐺 DProd {⟨(♯‘𝑆), (𝐾‘{𝑋})⟩}) = (𝐾‘{𝑋}))
131129, 130eqtrd 2814 . . . . . 6 (𝜑 → (𝐺 DProd (𝑇 ↾ {(♯‘𝑆)})) = (𝐾‘{𝑋}))
132128, 131ineq12d 4079 . . . . 5 (𝜑 → ((𝐺 DProd (𝑇 ↾ (0..^(♯‘𝑆)))) ∩ (𝐺 DProd (𝑇 ↾ {(♯‘𝑆)}))) = (𝑊 ∩ (𝐾‘{𝑋})))
133 incom 4068 . . . . 5 (𝑊 ∩ (𝐾‘{𝑋})) = ((𝐾‘{𝑋}) ∩ 𝑊)
134132, 133syl6eq 2830 . . . 4 (𝜑 → ((𝐺 DProd (𝑇 ↾ (0..^(♯‘𝑆)))) ∩ (𝐺 DProd (𝑇 ↾ {(♯‘𝑆)}))) = ((𝐾‘{𝑋}) ∩ 𝑊))
1354, 72subg0 18072 . . . . . . 7 (𝑈 ∈ (SubGrp‘𝐺) → (0g𝐺) = (0g𝐻))
1363, 135syl 17 . . . . . 6 (𝜑 → (0g𝐺) = (0g𝐻))
137 pgpfac.0 . . . . . 6 0 = (0g𝐻)
138136, 137syl6eqr 2832 . . . . 5 (𝜑 → (0g𝐺) = 0 )
139138sneqd 4454 . . . 4 (𝜑 → {(0g𝐺)} = { 0 })
140125, 134, 1393eqtr4d 2824 . . 3 (𝜑 → ((𝐺 DProd (𝑇 ↾ (0..^(♯‘𝑆)))) ∩ (𝐺 DProd (𝑇 ↾ {(♯‘𝑆)}))) = {(0g𝐺)})
14148, 56, 70, 71, 72, 85, 118, 124, 140dmdprdsplit2 18921 . 2 (𝜑𝐺dom DProd 𝑇)
142 eqid 2778 . . . . 5 (LSSum‘𝐺) = (LSSum‘𝐺)
14348, 56, 70, 142, 141dprdsplit 18923 . . . 4 (𝜑 → (𝐺 DProd 𝑇) = ((𝐺 DProd (𝑇 ↾ (0..^(♯‘𝑆))))(LSSum‘𝐺)(𝐺 DProd (𝑇 ↾ {(♯‘𝑆)}))))
144128, 131oveq12d 6996 . . . 4 (𝜑 → ((𝐺 DProd (𝑇 ↾ (0..^(♯‘𝑆))))(LSSum‘𝐺)(𝐺 DProd (𝑇 ↾ {(♯‘𝑆)}))) = (𝑊(LSSum‘𝐺)(𝐾‘{𝑋})))
145128, 121eqeltrrd 2867 . . . . 5 (𝜑𝑊 ∈ (SubGrp‘𝐺))
146142lsmcom 18737 . . . . 5 ((𝐺 ∈ Abel ∧ 𝑊 ∈ (SubGrp‘𝐺) ∧ (𝐾‘{𝑋}) ∈ (SubGrp‘𝐺)) → (𝑊(LSSum‘𝐺)(𝐾‘{𝑋})) = ((𝐾‘{𝑋})(LSSum‘𝐺)𝑊))
147119, 145, 21, 146syl3anc 1351 . . . 4 (𝜑 → (𝑊(LSSum‘𝐺)(𝐾‘{𝑋})) = ((𝐾‘{𝑋})(LSSum‘𝐺)𝑊))
148143, 144, 1473eqtrd 2818 . . 3 (𝜑 → (𝐺 DProd 𝑇) = ((𝐾‘{𝑋})(LSSum‘𝐺)𝑊))
149 pgpfac.w . . . . . 6 (𝜑𝑊 ∈ (SubGrp‘𝐻))
1507subgss 18067 . . . . . 6 (𝑊 ∈ (SubGrp‘𝐻) → 𝑊 ⊆ (Base‘𝐻))
151149, 150syl 17 . . . . 5 (𝜑𝑊 ⊆ (Base‘𝐻))
152151, 13sseqtr4d 3900 . . . 4 (𝜑𝑊𝑈)
153 pgpfac.l . . . . 5 = (LSSum‘𝐻)
1544, 142, 153subglsm 18560 . . . 4 ((𝑈 ∈ (SubGrp‘𝐺) ∧ (𝐾‘{𝑋}) ⊆ 𝑈𝑊𝑈) → ((𝐾‘{𝑋})(LSSum‘𝐺)𝑊) = ((𝐾‘{𝑋}) 𝑊))
1553, 23, 152, 154syl3anc 1351 . . 3 (𝜑 → ((𝐾‘{𝑋})(LSSum‘𝐺)𝑊) = ((𝐾‘{𝑋}) 𝑊))
156 pgpfac.s . . 3 (𝜑 → ((𝐾‘{𝑋}) 𝑊) = 𝑈)
157148, 155, 1563eqtrd 2818 . 2 (𝜑 → (𝐺 DProd 𝑇) = 𝑈)
158 breq2 4934 . . . 4 (𝑠 = 𝑇 → (𝐺dom DProd 𝑠𝐺dom DProd 𝑇))
159 oveq2 6986 . . . . 5 (𝑠 = 𝑇 → (𝐺 DProd 𝑠) = (𝐺 DProd 𝑇))
160159eqeq1d 2780 . . . 4 (𝑠 = 𝑇 → ((𝐺 DProd 𝑠) = 𝑈 ↔ (𝐺 DProd 𝑇) = 𝑈))
161158, 160anbi12d 621 . . 3 (𝑠 = 𝑇 → ((𝐺dom DProd 𝑠 ∧ (𝐺 DProd 𝑠) = 𝑈) ↔ (𝐺dom DProd 𝑇 ∧ (𝐺 DProd 𝑇) = 𝑈)))
162161rspcev 3535 . 2 ((𝑇 ∈ Word 𝐶 ∧ (𝐺dom DProd 𝑇 ∧ (𝐺 DProd 𝑇) = 𝑈)) → ∃𝑠 ∈ Word 𝐶(𝐺dom DProd 𝑠 ∧ (𝐺 DProd 𝑠) = 𝑈))
16343, 141, 157, 162syl12anc 824 1 (𝜑 → ∃𝑠 ∈ Word 𝐶(𝐺dom DProd 𝑠 ∧ (𝐺 DProd 𝑠) = 𝑈))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 198  wa 387   = wceq 1507  wcel 2050  wne 2967  wral 3088  wrex 3089  {crab 3092  Vcvv 3415  cun 3829  cin 3830  wss 3831  wpss 3832  c0 4180  {csn 4442  cop 4448   class class class wbr 4930  dom cdm 5408  ran crn 5409  cres 5410   Fn wfn 6185  wf 6186  cfv 6190  (class class class)co 6978  Fincfn 8308  0cc0 10337  1c1 10338   + caddc 10340  cn 11441  0cn0 11710  cz 11796  cuz 12061  ..^cfzo 12852  chash 13508  Word cword 13675   ++ cconcat 13736  ⟨“cs1 13761  cprime 15874  Basecbs 16342  s cress 16343  0gc0g 16572  Moorecmre 16714  mrClscmrc 16715  ACScacs 16717  Grpcgrp 17894  SubGrpcsubg 18060  Cntzccntz 18219  odcod 18417  gExcgex 18418   pGrp cpgp 18419  LSSumclsm 18523  Abelcabl 18670  CycGrpccyg 18755   DProd cdprd 18868
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1758  ax-4 1772  ax-5 1869  ax-6 1928  ax-7 1965  ax-8 2052  ax-9 2059  ax-10 2079  ax-11 2093  ax-12 2106  ax-13 2301  ax-ext 2750  ax-rep 5050  ax-sep 5061  ax-nul 5068  ax-pow 5120  ax-pr 5187  ax-un 7281  ax-cnex 10393  ax-resscn 10394  ax-1cn 10395  ax-icn 10396  ax-addcl 10397  ax-addrcl 10398  ax-mulcl 10399  ax-mulrcl 10400  ax-mulcom 10401  ax-addass 10402  ax-mulass 10403  ax-distr 10404  ax-i2m1 10405  ax-1ne0 10406  ax-1rid 10407  ax-rnegex 10408  ax-rrecex 10409  ax-cnre 10410  ax-pre-lttri 10411  ax-pre-lttrn 10412  ax-pre-ltadd 10413  ax-pre-mulgt0 10414
This theorem depends on definitions:  df-bi 199  df-an 388  df-or 834  df-3or 1069  df-3an 1070  df-tru 1510  df-ex 1743  df-nf 1747  df-sb 2016  df-mo 2547  df-eu 2583  df-clab 2759  df-cleq 2771  df-clel 2846  df-nfc 2918  df-ne 2968  df-nel 3074  df-ral 3093  df-rex 3094  df-reu 3095  df-rmo 3096  df-rab 3097  df-v 3417  df-sbc 3684  df-csb 3789  df-dif 3834  df-un 3836  df-in 3838  df-ss 3845  df-pss 3847  df-nul 4181  df-if 4352  df-pw 4425  df-sn 4443  df-pr 4445  df-tp 4447  df-op 4449  df-uni 4714  df-int 4751  df-iun 4795  df-iin 4796  df-br 4931  df-opab 4993  df-mpt 5010  df-tr 5032  df-id 5313  df-eprel 5318  df-po 5327  df-so 5328  df-fr 5367  df-se 5368  df-we 5369  df-xp 5414  df-rel 5415  df-cnv 5416  df-co 5417  df-dm 5418  df-rn 5419  df-res 5420  df-ima 5421  df-pred 5988  df-ord 6034  df-on 6035  df-lim 6036  df-suc 6037  df-iota 6154  df-fun 6192  df-fn 6193  df-f 6194  df-f1 6195  df-fo 6196  df-f1o 6197  df-fv 6198  df-isom 6199  df-riota 6939  df-ov 6981  df-oprab 6982  df-mpo 6983  df-of 7229  df-om 7399  df-1st 7503  df-2nd 7504  df-supp 7636  df-tpos 7697  df-wrecs 7752  df-recs 7814  df-rdg 7852  df-1o 7907  df-oadd 7911  df-er 8091  df-map 8210  df-ixp 8262  df-en 8309  df-dom 8310  df-sdom 8311  df-fin 8312  df-fsupp 8631  df-sup 8703  df-inf 8704  df-oi 8771  df-card 9164  df-pnf 10478  df-mnf 10479  df-xr 10480  df-ltxr 10481  df-le 10482  df-sub 10674  df-neg 10675  df-nn 11442  df-2 11506  df-n0 11711  df-z 11797  df-uz 12062  df-fz 12712  df-fzo 12853  df-seq 13188  df-hash 13509  df-word 13676  df-concat 13737  df-s1 13762  df-ndx 16345  df-slot 16346  df-base 16348  df-sets 16349  df-ress 16350  df-plusg 16437  df-0g 16574  df-gsum 16575  df-mre 16718  df-mrc 16719  df-acs 16721  df-mgm 17713  df-sgrp 17755  df-mnd 17766  df-mhm 17806  df-submnd 17807  df-grp 17897  df-minusg 17898  df-sbg 17899  df-mulg 18015  df-subg 18063  df-ghm 18130  df-gim 18173  df-cntz 18221  df-oppg 18248  df-od 18421  df-pgp 18423  df-lsm 18525  df-cmn 18671  df-abl 18672  df-cyg 18756  df-dprd 18870
This theorem is referenced by:  pgpfaclem2  18957
  Copyright terms: Public domain W3C validator