pgpfaclem1 - Metamath Proof Explorer

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

Theorem pgpfaclem1 20152

Description: Lemma for pgpfac 20155. (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 = (0_g‘𝐻)
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**
Step	Hyp	Ref	Expression
1		pgpfac.t	. . 3 ⊢ 𝑇 = (𝑆 ++ ⟨“(𝐾‘{𝑋})”⟩)
2		pgpfac.2	. . 3 ⊢ (𝜑 → 𝑆 ∈ Word 𝐶)
3		pgpfac.u	. . . . . . . . . 10 ⊢ (𝜑 → 𝑈 ∈ (SubGrp‘𝐺))
4		pgpfac.h	. . . . . . . . . . 11 ⊢ 𝐻 = (𝐺 ↾_s 𝑈)
5	4	subggrp 19194	. . . . . . . . . 10 ⊢ (𝑈 ∈ (SubGrp‘𝐺) → 𝐻 ∈ Grp)
6	3, 5	syl 18	. . . . . . . . 9 ⊢ (𝜑 → 𝐻 ∈ Grp)
7		eqid 2761	. . . . . . . . . 10 ⊢ (Base‘𝐻) = (Base‘𝐻)
8	7	subgacs 19226	. . . . . . . . 9 ⊢ (𝐻 ∈ Grp → (SubGrp‘𝐻) ∈ (ACS‘(Base‘𝐻)))
9	6, 8	syl 18	. . . . . . . 8 ⊢ (𝜑 → (SubGrp‘𝐻) ∈ (ACS‘(Base‘𝐻)))
10	9	acsmred 17711	. . . . . . 7 ⊢ (𝜑 → (SubGrp‘𝐻) ∈ (Moore‘(Base‘𝐻)))
11		pgpfac.x	. . . . . . . 8 ⊢ (𝜑 → 𝑋 ∈ 𝑈)
12	4	subgbas 19195	. . . . . . . . 9 ⊢ (𝑈 ∈ (SubGrp‘𝐺) → 𝑈 = (Base‘𝐻))
13	3, 12	syl 18	. . . . . . . 8 ⊢ (𝜑 → 𝑈 = (Base‘𝐻))
14	11, 13	eleqtrd 2863	. . . . . . 7 ⊢ (𝜑 → 𝑋 ∈ (Base‘𝐻))
15		pgpfac.k	. . . . . . . 8 ⊢ 𝐾 = (mrCls‘(SubGrp‘𝐻))
16	15	mrcsncl 17667	. . . . . . 7 ⊢ (((SubGrp‘𝐻) ∈ (Moore‘(Base‘𝐻)) ∧ 𝑋 ∈ (Base‘𝐻)) → (𝐾‘{𝑋}) ∈ (SubGrp‘𝐻))
17	10, 14, 16	syl2anc 595	. . . . . 6 ⊢ (𝜑 → (𝐾‘{𝑋}) ∈ (SubGrp‘𝐻))
18	4	subsubg 19215	. . . . . . 7 ⊢ (𝑈 ∈ (SubGrp‘𝐺) → ((𝐾‘{𝑋}) ∈ (SubGrp‘𝐻) ↔ ((𝐾‘{𝑋}) ∈ (SubGrp‘𝐺) ∧ (𝐾‘{𝑋}) ⊆ 𝑈)))
19	3, 18	syl 18	. . . . . 6 ⊢ (𝜑 → ((𝐾‘{𝑋}) ∈ (SubGrp‘𝐻) ↔ ((𝐾‘{𝑋}) ∈ (SubGrp‘𝐺) ∧ (𝐾‘{𝑋}) ⊆ 𝑈)))
20	17, 19	mpbid 235	. . . . 5 ⊢ (𝜑 → ((𝐾‘{𝑋}) ∈ (SubGrp‘𝐺) ∧ (𝐾‘{𝑋}) ⊆ 𝑈))
21	20	simpld 499	. . . 4 ⊢ (𝜑 → (𝐾‘{𝑋}) ∈ (SubGrp‘𝐺))
22	4	oveq1i 7420	. . . . . . 7 ⊢ (𝐻 ↾_s (𝐾‘{𝑋})) = ((𝐺 ↾_s 𝑈) ↾_s (𝐾‘{𝑋}))
23	20	simprd 500	. . . . . . . 8 ⊢ (𝜑 → (𝐾‘{𝑋}) ⊆ 𝑈)
24		ressabs 17307	. . . . . . . 8 ⊢ ((𝑈 ∈ (SubGrp‘𝐺) ∧ (𝐾‘{𝑋}) ⊆ 𝑈) → ((𝐺 ↾_s 𝑈) ↾_s (𝐾‘{𝑋})) = (𝐺 ↾_s (𝐾‘{𝑋})))
25	3, 23, 24	syl2anc 595	. . . . . . 7 ⊢ (𝜑 → ((𝐺 ↾_s 𝑈) ↾_s (𝐾‘{𝑋})) = (𝐺 ↾_s (𝐾‘{𝑋})))
26	22, 25	eqtrid 2808	. . . . . 6 ⊢ (𝜑 → (𝐻 ↾_s (𝐾‘{𝑋})) = (𝐺 ↾_s (𝐾‘{𝑋})))
27	7, 15	cycsubgcyg2 19971	. . . . . . 7 ⊢ ((𝐻 ∈ Grp ∧ 𝑋 ∈ (Base‘𝐻)) → (𝐻 ↾_s (𝐾‘{𝑋})) ∈ CycGrp)
28	6, 14, 27	syl2anc 595	. . . . . 6 ⊢ (𝜑 → (𝐻 ↾_s (𝐾‘{𝑋})) ∈ CycGrp)
29	26, 28	eqeltrrd 2862	. . . . 5 ⊢ (𝜑 → (𝐺 ↾_s (𝐾‘{𝑋})) ∈ CycGrp)
30		pgpfac.p	. . . . . . 7 ⊢ (𝜑 → 𝑃 pGrp 𝐺)
31		pgpprm 19662	. . . . . . 7 ⊢ (𝑃 pGrp 𝐺 → 𝑃 ∈ ℙ)
32	30, 31	syl 18	. . . . . 6 ⊢ (𝜑 → 𝑃 ∈ ℙ)
33		subgpgp 19666	. . . . . . 7 ⊢ ((𝑃 pGrp 𝐺 ∧ (𝐾‘{𝑋}) ∈ (SubGrp‘𝐺)) → 𝑃 pGrp (𝐺 ↾_s (𝐾‘{𝑋})))
34	30, 21, 33	syl2anc 595	. . . . . 6 ⊢ (𝜑 → 𝑃 pGrp (𝐺 ↾_s (𝐾‘{𝑋})))
35		brelrng 5931	. . . . . 6 ⊢ ((𝑃 ∈ ℙ ∧ (𝐺 ↾_s (𝐾‘{𝑋})) ∈ CycGrp ∧ 𝑃 pGrp (𝐺 ↾_s (𝐾‘{𝑋}))) → (𝐺 ↾_s (𝐾‘{𝑋})) ∈ ran pGrp )
36	32, 29, 34, 35	syl3anc 1396	. . . . 5 ⊢ (𝜑 → (𝐺 ↾_s (𝐾‘{𝑋})) ∈ ran pGrp )
37	29, 36	elind 4152	. . . 4 ⊢ (𝜑 → (𝐺 ↾_s (𝐾‘{𝑋})) ∈ (CycGrp ∩ ran pGrp ))
38		oveq2 7418	. . . . . 6 ⊢ (𝑟 = (𝐾‘{𝑋}) → (𝐺 ↾_s 𝑟) = (𝐺 ↾_s (𝐾‘{𝑋})))
39	38	eleq1d 2846	. . . . 5 ⊢ (𝑟 = (𝐾‘{𝑋}) → ((𝐺 ↾_s 𝑟) ∈ (CycGrp ∩ ran pGrp ) ↔ (𝐺 ↾_s (𝐾‘{𝑋})) ∈ (CycGrp ∩ ran pGrp )))
40		pgpfac.c	. . . . 5 ⊢ 𝐶 = {𝑟 ∈ (SubGrp‘𝐺) ∣ (𝐺 ↾_s 𝑟) ∈ (CycGrp ∩ ran pGrp )}
41	39, 40	elrab2 3653	. . . 4 ⊢ ((𝐾‘{𝑋}) ∈ 𝐶 ↔ ((𝐾‘{𝑋}) ∈ (SubGrp‘𝐺) ∧ (𝐺 ↾_s (𝐾‘{𝑋})) ∈ (CycGrp ∩ ran pGrp )))
42	21, 37, 41	sylanbrc 594	. . 3 ⊢ (𝜑 → (𝐾‘{𝑋}) ∈ 𝐶)
43	1, 2, 42	cats1cld 14892	. 2 ⊢ (𝜑 → 𝑇 ∈ Word 𝐶)
44		wrdf 14555	. . . . 5 ⊢ (𝑇 ∈ Word 𝐶 → 𝑇:(0..^(♯‘𝑇))⟶𝐶)
45	43, 44	syl 18	. . . 4 ⊢ (𝜑 → 𝑇:(0..^(♯‘𝑇))⟶𝐶)
46	40	ssrab3 4035	. . . 4 ⊢ 𝐶 ⊆ (SubGrp‘𝐺)
47		fss 6722	. . . 4 ⊢ ((𝑇:(0..^(♯‘𝑇))⟶𝐶 ∧ 𝐶 ⊆ (SubGrp‘𝐺)) → 𝑇:(0..^(♯‘𝑇))⟶(SubGrp‘𝐺))
48	45, 46, 47	sylancl 597	. . 3 ⊢ (𝜑 → 𝑇:(0..^(♯‘𝑇))⟶(SubGrp‘𝐺))
49		lencl 14570	. . . . . . . 8 ⊢ (𝑆 ∈ Word 𝐶 → (♯‘𝑆) ∈ ℕ₀)
50	2, 49	syl 18	. . . . . . 7 ⊢ (𝜑 → (♯‘𝑆) ∈ ℕ₀)
51	50	nn0zd 12615	. . . . . 6 ⊢ (𝜑 → (♯‘𝑆) ∈ ℤ)
52		fzosn 13765	. . . . . 6 ⊢ ((♯‘𝑆) ∈ ℤ → ((♯‘𝑆)..^((♯‘𝑆) + 1)) = {(♯‘𝑆)})
53	51, 52	syl 18	. . . . 5 ⊢ (𝜑 → ((♯‘𝑆)..^((♯‘𝑆) + 1)) = {(♯‘𝑆)})
54	53	ineq2d 4172	. . . 4 ⊢ (𝜑 → ((0..^(♯‘𝑆)) ∩ ((♯‘𝑆)..^((♯‘𝑆) + 1))) = ((0..^(♯‘𝑆)) ∩ {(♯‘𝑆)}))
55		fzodisj 13722	. . . 4 ⊢ ((0..^(♯‘𝑆)) ∩ ((♯‘𝑆)..^((♯‘𝑆) + 1))) = ∅
56	54, 55	eqtr3di 2811	. . 3 ⊢ (𝜑 → ((0..^(♯‘𝑆)) ∩ {(♯‘𝑆)}) = ∅)
57	1	fveq2i 6884	. . . . . . 7 ⊢ (♯‘𝑇) = (♯‘(𝑆 ++ ⟨“(𝐾‘{𝑋})”⟩))
58	42	s1cld 14641	. . . . . . . 8 ⊢ (𝜑 → ⟨“(𝐾‘{𝑋})”⟩ ∈ Word 𝐶)
59		ccatlen 14612	. . . . . . . 8 ⊢ ((𝑆 ∈ Word 𝐶 ∧ ⟨“(𝐾‘{𝑋})”⟩ ∈ Word 𝐶) → (♯‘(𝑆 ++ ⟨“(𝐾‘{𝑋})”⟩)) = ((♯‘𝑆) + (♯‘⟨“(𝐾‘{𝑋})”⟩)))
60	2, 58, 59	syl2anc 595	. . . . . . 7 ⊢ (𝜑 → (♯‘(𝑆 ++ ⟨“(𝐾‘{𝑋})”⟩)) = ((♯‘𝑆) + (♯‘⟨“(𝐾‘{𝑋})”⟩)))
61	57, 60	eqtrid 2808	. . . . . 6 ⊢ (𝜑 → (♯‘𝑇) = ((♯‘𝑆) + (♯‘⟨“(𝐾‘{𝑋})”⟩)))
62		s1len 14644	. . . . . . 7 ⊢ (♯‘⟨“(𝐾‘{𝑋})”⟩) = 1
63	62	oveq2i 7421	. . . . . 6 ⊢ ((♯‘𝑆) + (♯‘⟨“(𝐾‘{𝑋})”⟩)) = ((♯‘𝑆) + 1)
64	61, 63	eqtrdi 2812	. . . . 5 ⊢ (𝜑 → (♯‘𝑇) = ((♯‘𝑆) + 1))
65	64	oveq2d 7426	. . . 4 ⊢ (𝜑 → (0..^(♯‘𝑇)) = (0..^((♯‘𝑆) + 1)))
66		nn0uz 12899	. . . . . 6 ⊢ ℕ₀ = (ℤ_≥‘0)
67	50, 66	eleqtrdi 2871	. . . . 5 ⊢ (𝜑 → (♯‘𝑆) ∈ (ℤ_≥‘0))
68		fzosplitsn 13805	. . . . 5 ⊢ ((♯‘𝑆) ∈ (ℤ_≥‘0) → (0..^((♯‘𝑆) + 1)) = ((0..^(♯‘𝑆)) ∪ {(♯‘𝑆)}))
69	67, 68	syl 18	. . . 4 ⊢ (𝜑 → (0..^((♯‘𝑆) + 1)) = ((0..^(♯‘𝑆)) ∪ {(♯‘𝑆)}))
70	65, 69	eqtrd 2796	. . 3 ⊢ (𝜑 → (0..^(♯‘𝑇)) = ((0..^(♯‘𝑆)) ∪ {(♯‘𝑆)}))
71		eqid 2761	. . 3 ⊢ (Cntz‘𝐺) = (Cntz‘𝐺)
72		eqid 2761	. . 3 ⊢ (0_g‘𝐺) = (0_g‘𝐺)
73		pgpfac.4	. . . 4 ⊢ (𝜑 → 𝐺dom DProd 𝑆)
74		cats1un 14758	. . . . . . . 8 ⊢ ((𝑆 ∈ Word 𝐶 ∧ (𝐾‘{𝑋}) ∈ 𝐶) → (𝑆 ++ ⟨“(𝐾‘{𝑋})”⟩) = (𝑆 ∪ {⟨(♯‘𝑆), (𝐾‘{𝑋})⟩}))
75	2, 42, 74	syl2anc 595	. . . . . . 7 ⊢ (𝜑 → (𝑆 ++ ⟨“(𝐾‘{𝑋})”⟩) = (𝑆 ∪ {⟨(♯‘𝑆), (𝐾‘{𝑋})⟩}))
76	1, 75	eqtrid 2808	. . . . . 6 ⊢ (𝜑 → 𝑇 = (𝑆 ∪ {⟨(♯‘𝑆), (𝐾‘{𝑋})⟩}))
77	76	reseq1d 5977	. . . . 5 ⊢ (𝜑 → (𝑇 ↾ (0..^(♯‘𝑆))) = ((𝑆 ∪ {⟨(♯‘𝑆), (𝐾‘{𝑋})⟩}) ↾ (0..^(♯‘𝑆))))
78		wrdfn 14565	. . . . . . 7 ⊢ (𝑆 ∈ Word 𝐶 → 𝑆 Fn (0..^(♯‘𝑆)))
79	2, 78	syl 18	. . . . . 6 ⊢ (𝜑 → 𝑆 Fn (0..^(♯‘𝑆)))
80		fzonel 13702	. . . . . 6 ⊢ ¬ (♯‘𝑆) ∈ (0..^(♯‘𝑆))
81		fsnunres 7186	. . . . . 6 ⊢ ((𝑆 Fn (0..^(♯‘𝑆)) ∧ ¬ (♯‘𝑆) ∈ (0..^(♯‘𝑆))) → ((𝑆 ∪ {⟨(♯‘𝑆), (𝐾‘{𝑋})⟩}) ↾ (0..^(♯‘𝑆))) = 𝑆)
82	79, 80, 81	sylancl 597	. . . . 5 ⊢ (𝜑 → ((𝑆 ∪ {⟨(♯‘𝑆), (𝐾‘{𝑋})⟩}) ↾ (0..^(♯‘𝑆))) = 𝑆)
83	77, 82	eqtrd 2796	. . . 4 ⊢ (𝜑 → (𝑇 ↾ (0..^(♯‘𝑆))) = 𝑆)
84	73, 83	breqtrrd 5138	. . 3 ⊢ (𝜑 → 𝐺dom DProd (𝑇 ↾ (0..^(♯‘𝑆))))
85		fvex 6894	. . . . . 6 ⊢ (♯‘𝑆) ∈ V
86		dprdsn 20107	. . . . . 6 ⊢ (((♯‘𝑆) ∈ V ∧ (𝐾‘{𝑋}) ∈ (SubGrp‘𝐺)) → (𝐺dom DProd {⟨(♯‘𝑆), (𝐾‘{𝑋})⟩} ∧ (𝐺 DProd {⟨(♯‘𝑆), (𝐾‘{𝑋})⟩}) = (𝐾‘{𝑋})))
87	85, 21, 86	sylancr 598	. . . . 5 ⊢ (𝜑 → (𝐺dom DProd {⟨(♯‘𝑆), (𝐾‘{𝑋})⟩} ∧ (𝐺 DProd {⟨(♯‘𝑆), (𝐾‘{𝑋})⟩}) = (𝐾‘{𝑋})))
88	87	simpld 499	. . . 4 ⊢ (𝜑 → 𝐺dom DProd {⟨(♯‘𝑆), (𝐾‘{𝑋})⟩})
89		wrdfn 14565	. . . . . . 7 ⊢ (𝑇 ∈ Word 𝐶 → 𝑇 Fn (0..^(♯‘𝑇)))
90	43, 89	syl 18	. . . . . 6 ⊢ (𝜑 → 𝑇 Fn (0..^(♯‘𝑇)))
91		ssun2 4131	. . . . . . . 8 ⊢ {(♯‘𝑆)} ⊆ ((0..^(♯‘𝑆)) ∪ {(♯‘𝑆)})
92	85	snss 4749	. . . . . . . 8 ⊢ ((♯‘𝑆) ∈ ((0..^(♯‘𝑆)) ∪ {(♯‘𝑆)}) ↔ {(♯‘𝑆)} ⊆ ((0..^(♯‘𝑆)) ∪ {(♯‘𝑆)}))
93	91, 92	mpbir 234	. . . . . . 7 ⊢ (♯‘𝑆) ∈ ((0..^(♯‘𝑆)) ∪ {(♯‘𝑆)})
94	93, 70	eleqtrrid 2868	. . . . . 6 ⊢ (𝜑 → (♯‘𝑆) ∈ (0..^(♯‘𝑇)))
95		fnressn 7155	. . . . . 6 ⊢ ((𝑇 Fn (0..^(♯‘𝑇)) ∧ (♯‘𝑆) ∈ (0..^(♯‘𝑇))) → (𝑇 ↾ {(♯‘𝑆)}) = {⟨(♯‘𝑆), (𝑇‘(♯‘𝑆))⟩})
96	90, 94, 95	syl2anc 595	. . . . 5 ⊢ (𝜑 → (𝑇 ↾ {(♯‘𝑆)}) = {⟨(♯‘𝑆), (𝑇‘(♯‘𝑆))⟩})
97	1	fveq1i 6882	. . . . . . . . 9 ⊢ (𝑇‘(♯‘𝑆)) = ((𝑆 ++ ⟨“(𝐾‘{𝑋})”⟩)‘(♯‘𝑆))
98	50	nn0cnd 12566	. . . . . . . . . . 11 ⊢ (𝜑 → (♯‘𝑆) ∈ ℂ)
99	98	addlidd 11410	. . . . . . . . . 10 ⊢ (𝜑 → (0 + (♯‘𝑆)) = (♯‘𝑆))
100	99	fveq2d 6885	. . . . . . . . 9 ⊢ (𝜑 → ((𝑆 ++ ⟨“(𝐾‘{𝑋})”⟩)‘(0 + (♯‘𝑆))) = ((𝑆 ++ ⟨“(𝐾‘{𝑋})”⟩)‘(♯‘𝑆)))
101	97, 100	eqtr4id 2815	. . . . . . . 8 ⊢ (𝜑 → (𝑇‘(♯‘𝑆)) = ((𝑆 ++ ⟨“(𝐾‘{𝑋})”⟩)‘(0 + (♯‘𝑆))))
102		1nn 12243	. . . . . . . . . . . 12 ⊢ 1 ∈ ℕ
103	62, 102	eqeltri 2857	. . . . . . . . . . 11 ⊢ (♯‘⟨“(𝐾‘{𝑋})”⟩) ∈ ℕ
104		lbfzo0 13728	. . . . . . . . . . 11 ⊢ (0 ∈ (0..^(♯‘⟨“(𝐾‘{𝑋})”⟩)) ↔ (♯‘⟨“(𝐾‘{𝑋})”⟩) ∈ ℕ)
105	103, 104	mpbir 234	. . . . . . . . . 10 ⊢ 0 ∈ (0..^(♯‘⟨“(𝐾‘{𝑋})”⟩))
106	105	a1i 11	. . . . . . . . 9 ⊢ (𝜑 → 0 ∈ (0..^(♯‘⟨“(𝐾‘{𝑋})”⟩)))
107		ccatval3 14616	. . . . . . . . 9 ⊢ ((𝑆 ∈ Word 𝐶 ∧ ⟨“(𝐾‘{𝑋})”⟩ ∈ Word 𝐶 ∧ 0 ∈ (0..^(♯‘⟨“(𝐾‘{𝑋})”⟩))) → ((𝑆 ++ ⟨“(𝐾‘{𝑋})”⟩)‘(0 + (♯‘𝑆))) = (⟨“(𝐾‘{𝑋})”⟩‘0))
108	2, 58, 106, 107	syl3anc 1396	. . . . . . . 8 ⊢ (𝜑 → ((𝑆 ++ ⟨“(𝐾‘{𝑋})”⟩)‘(0 + (♯‘𝑆))) = (⟨“(𝐾‘{𝑋})”⟩‘0))
109		fvex 6894	. . . . . . . . 9 ⊢ (𝐾‘{𝑋}) ∈ V
110		s1fv 14648	. . . . . . . . 9 ⊢ ((𝐾‘{𝑋}) ∈ V → (⟨“(𝐾‘{𝑋})”⟩‘0) = (𝐾‘{𝑋}))
111	109, 110	mp1i 14	. . . . . . . 8 ⊢ (𝜑 → (⟨“(𝐾‘{𝑋})”⟩‘0) = (𝐾‘{𝑋}))
112	101, 108, 111	3eqtrd 2800	. . . . . . 7 ⊢ (𝜑 → (𝑇‘(♯‘𝑆)) = (𝐾‘{𝑋}))
113	112	opeq2d 4844	. . . . . 6 ⊢ (𝜑 → ⟨(♯‘𝑆), (𝑇‘(♯‘𝑆))⟩ = ⟨(♯‘𝑆), (𝐾‘{𝑋})⟩)
114	113	sneqd 4600	. . . . 5 ⊢ (𝜑 → {⟨(♯‘𝑆), (𝑇‘(♯‘𝑆))⟩} = {⟨(♯‘𝑆), (𝐾‘{𝑋})⟩})
115	96, 114	eqtrd 2796	. . . 4 ⊢ (𝜑 → (𝑇 ↾ {(♯‘𝑆)}) = {⟨(♯‘𝑆), (𝐾‘{𝑋})⟩})
116	88, 115	breqtrrd 5138	. . 3 ⊢ (𝜑 → 𝐺dom DProd (𝑇 ↾ {(♯‘𝑆)}))
117		pgpfac.g	. . . 4 ⊢ (𝜑 → 𝐺 ∈ Abel)
118		dprdsubg 20095	. . . . 5 ⊢ (𝐺dom DProd (𝑇 ↾ (0..^(♯‘𝑆))) → (𝐺 DProd (𝑇 ↾ (0..^(♯‘𝑆)))) ∈ (SubGrp‘𝐺))
119	84, 118	syl 18	. . . 4 ⊢ (𝜑 → (𝐺 DProd (𝑇 ↾ (0..^(♯‘𝑆)))) ∈ (SubGrp‘𝐺))
120		dprdsubg 20095	. . . . 5 ⊢ (𝐺dom DProd (𝑇 ↾ {(♯‘𝑆)}) → (𝐺 DProd (𝑇 ↾ {(♯‘𝑆)})) ∈ (SubGrp‘𝐺))
121	116, 120	syl 18	. . . 4 ⊢ (𝜑 → (𝐺 DProd (𝑇 ↾ {(♯‘𝑆)})) ∈ (SubGrp‘𝐺))
122	71, 117, 119, 121	ablcntzd 19926	. . 3 ⊢ (𝜑 → (𝐺 DProd (𝑇 ↾ (0..^(♯‘𝑆)))) ⊆ ((Cntz‘𝐺)‘(𝐺 DProd (𝑇 ↾ {(♯‘𝑆)}))))
123		pgpfac.i	. . . 4 ⊢ (𝜑 → ((𝐾‘{𝑋}) ∩ 𝑊) = { 0 })
124	83	oveq2d 7426	. . . . . . 7 ⊢ (𝜑 → (𝐺 DProd (𝑇 ↾ (0..^(♯‘𝑆)))) = (𝐺 DProd 𝑆))
125		pgpfac.5	. . . . . . 7 ⊢ (𝜑 → (𝐺 DProd 𝑆) = 𝑊)
126	124, 125	eqtrd 2796	. . . . . 6 ⊢ (𝜑 → (𝐺 DProd (𝑇 ↾ (0..^(♯‘𝑆)))) = 𝑊)
127	115	oveq2d 7426	. . . . . . 7 ⊢ (𝜑 → (𝐺 DProd (𝑇 ↾ {(♯‘𝑆)})) = (𝐺 DProd {⟨(♯‘𝑆), (𝐾‘{𝑋})⟩}))
128	87	simprd 500	. . . . . . 7 ⊢ (𝜑 → (𝐺 DProd {⟨(♯‘𝑆), (𝐾‘{𝑋})⟩}) = (𝐾‘{𝑋}))
129	127, 128	eqtrd 2796	. . . . . 6 ⊢ (𝜑 → (𝐺 DProd (𝑇 ↾ {(♯‘𝑆)})) = (𝐾‘{𝑋}))
130	126, 129	ineq12d 4173	. . . . 5 ⊢ (𝜑 → ((𝐺 DProd (𝑇 ↾ (0..^(♯‘𝑆)))) ∩ (𝐺 DProd (𝑇 ↾ {(♯‘𝑆)}))) = (𝑊 ∩ (𝐾‘{𝑋})))
131		incom 4161	. . . . 5 ⊢ (𝑊 ∩ (𝐾‘{𝑋})) = ((𝐾‘{𝑋}) ∩ 𝑊)
132	130, 131	eqtrdi 2812	. . . 4 ⊢ (𝜑 → ((𝐺 DProd (𝑇 ↾ (0..^(♯‘𝑆)))) ∩ (𝐺 DProd (𝑇 ↾ {(♯‘𝑆)}))) = ((𝐾‘{𝑋}) ∩ 𝑊))
133	4, 72	subg0 19197	. . . . . . 7 ⊢ (𝑈 ∈ (SubGrp‘𝐺) → (0_g‘𝐺) = (0_g‘𝐻))
134	3, 133	syl 18	. . . . . 6 ⊢ (𝜑 → (0_g‘𝐺) = (0_g‘𝐻))
135		pgpfac.0	. . . . . 6 ⊢ 0 = (0_g‘𝐻)
136	134, 135	eqtr4di 2814	. . . . 5 ⊢ (𝜑 → (0_g‘𝐺) = 0 )
137	136	sneqd 4600	. . . 4 ⊢ (𝜑 → {(0_g‘𝐺)} = { 0 })
138	123, 132, 137	3eqtr4d 2806	. . 3 ⊢ (𝜑 → ((𝐺 DProd (𝑇 ↾ (0..^(♯‘𝑆)))) ∩ (𝐺 DProd (𝑇 ↾ {(♯‘𝑆)}))) = {(0_g‘𝐺)})
139	48, 56, 70, 71, 72, 84, 116, 122, 138	dmdprdsplit2 20117	. 2 ⊢ (𝜑 → 𝐺dom DProd 𝑇)
140		eqid 2761	. . . . 5 ⊢ (LSSum‘𝐺) = (LSSum‘𝐺)
141	48, 56, 70, 140, 139	dprdsplit 20119	. . . 4 ⊢ (𝜑 → (𝐺 DProd 𝑇) = ((𝐺 DProd (𝑇 ↾ (0..^(♯‘𝑆))))(LSSum‘𝐺)(𝐺 DProd (𝑇 ↾ {(♯‘𝑆)}))))
142	126, 129	oveq12d 7428	. . . 4 ⊢ (𝜑 → ((𝐺 DProd (𝑇 ↾ (0..^(♯‘𝑆))))(LSSum‘𝐺)(𝐺 DProd (𝑇 ↾ {(♯‘𝑆)}))) = (𝑊(LSSum‘𝐺)(𝐾‘{𝑋})))
143	126, 119	eqeltrrd 2862	. . . . 5 ⊢ (𝜑 → 𝑊 ∈ (SubGrp‘𝐺))
144	140	lsmcom 19927	. . . . 5 ⊢ ((𝐺 ∈ Abel ∧ 𝑊 ∈ (SubGrp‘𝐺) ∧ (𝐾‘{𝑋}) ∈ (SubGrp‘𝐺)) → (𝑊(LSSum‘𝐺)(𝐾‘{𝑋})) = ((𝐾‘{𝑋})(LSSum‘𝐺)𝑊))
145	117, 143, 21, 144	syl3anc 1396	. . . 4 ⊢ (𝜑 → (𝑊(LSSum‘𝐺)(𝐾‘{𝑋})) = ((𝐾‘{𝑋})(LSSum‘𝐺)𝑊))
146	141, 142, 145	3eqtrd 2800	. . 3 ⊢ (𝜑 → (𝐺 DProd 𝑇) = ((𝐾‘{𝑋})(LSSum‘𝐺)𝑊))
147		pgpfac.w	. . . . . 6 ⊢ (𝜑 → 𝑊 ∈ (SubGrp‘𝐻))
148	7	subgss 19192	. . . . . 6 ⊢ (𝑊 ∈ (SubGrp‘𝐻) → 𝑊 ⊆ (Base‘𝐻))
149	147, 148	syl 18	. . . . 5 ⊢ (𝜑 → 𝑊 ⊆ (Base‘𝐻))
150	149, 13	sseqtrrd 3973	. . . 4 ⊢ (𝜑 → 𝑊 ⊆ 𝑈)
151		pgpfac.l	. . . . 5 ⊢ ⊕ = (LSSum‘𝐻)
152	4, 140, 151	subglsm 19742	. . . 4 ⊢ ((𝑈 ∈ (SubGrp‘𝐺) ∧ (𝐾‘{𝑋}) ⊆ 𝑈 ∧ 𝑊 ⊆ 𝑈) → ((𝐾‘{𝑋})(LSSum‘𝐺)𝑊) = ((𝐾‘{𝑋}) ⊕ 𝑊))
153	3, 23, 150, 152	syl3anc 1396	. . 3 ⊢ (𝜑 → ((𝐾‘{𝑋})(LSSum‘𝐺)𝑊) = ((𝐾‘{𝑋}) ⊕ 𝑊))
154		pgpfac.s	. . 3 ⊢ (𝜑 → ((𝐾‘{𝑋}) ⊕ 𝑊) = 𝑈)
155	146, 153, 154	3eqtrd 2800	. 2 ⊢ (𝜑 → (𝐺 DProd 𝑇) = 𝑈)
156		breq2 5112	. . . 4 ⊢ (𝑠 = 𝑇 → (𝐺dom DProd 𝑠 ↔ 𝐺dom DProd 𝑇))
157		oveq2 7418	. . . . 5 ⊢ (𝑠 = 𝑇 → (𝐺 DProd 𝑠) = (𝐺 DProd 𝑇))
158	157	eqeq1d 2763	. . . 4 ⊢ (𝑠 = 𝑇 → ((𝐺 DProd 𝑠) = 𝑈 ↔ (𝐺 DProd 𝑇) = 𝑈))
159	156, 158	anbi12d 643	. . 3 ⊢ (𝑠 = 𝑇 → ((𝐺dom DProd 𝑠 ∧ (𝐺 DProd 𝑠) = 𝑈) ↔ (𝐺dom DProd 𝑇 ∧ (𝐺 DProd 𝑇) = 𝑈)))
160	159	rspcev 3580	. 2 ⊢ ((𝑇 ∈ Word 𝐶 ∧ (𝐺dom DProd 𝑇 ∧ (𝐺 DProd 𝑇) = 𝑈)) → ∃𝑠 ∈ Word 𝐶(𝐺dom DProd 𝑠 ∧ (𝐺 DProd 𝑠) = 𝑈))
161	43, 139, 155, 160	syl12anc 849	1 ⊢ (𝜑 → ∃𝑠 ∈ Word 𝐶(𝐺dom DProd 𝑠 ∧ (𝐺 DProd 𝑠) = 𝑈))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 209 ∧ wa 400 = wceq 1568 ∈ wcel 2141 ≠ wne 2956 ∀wral 3077 ∃wrex 3087 {crab 3414 Vcvv 3453 ∪ cun 3902 ∩ cin 3903 ⊆ wss 3904 ⊊ wpss 3905 ∅c0 4285 {csn 4588 ⟨cop 4594 class class class wbr 5108 dom cdm 5661 ran crn 5662 ↾ cres 5663 Fn wfn 6531 ⟶wf 6532 ‘cfv 6536 (class class class)co 7410 Fincfn 8942 0cc0 11099 1c1 11100 + caddc 11102 ℕcn 12232 ℕ₀cn0 12503 ℤcz 12590 ℤ_≥cuz 12861 ..^cfzo 13682 ♯chash 14366 Word cword 14550 ++ cconcat 14607 ⟨“cs1 14633 ℙcprime 16728 Basecbs 17268 ↾_s cress 17289 0_gc0g 17491 Moorecmre 17633 mrClscmrc 17634 ACScacs 17636 Grpcgrp 18999 SubGrpcsubg 19185 Cntzccntz 19384 odcod 19593 gExcgex 19594 pGrp cpgp 19595 LSSumclsm 19703 Abelcabl 19850 CycGrpccyg 19946 DProd cdprd 20064

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1823 ax-4 1837 ax-5 1938 ax-6 1995 ax-7 2036 ax-8 2143 ax-9 2151 ax-10 2174 ax-11 2190 ax-12 2211 ax-ext 2733 ax-rep 5237 ax-sep 5256 ax-nul 5268 ax-pow 5336 ax-pr 5404 ax-un 7732 ax-cnex 11155 ax-resscn 11156 ax-1cn 11157 ax-icn 11158 ax-addcl 11159 ax-addrcl 11160 ax-mulcl 11161 ax-mulrcl 11162 ax-mulcom 11163 ax-addass 11164 ax-mulass 11165 ax-distr 11166 ax-i2m1 11167 ax-1ne0 11168 ax-1rid 11169 ax-rnegex 11170 ax-rrecex 11171 ax-cnre 11172 ax-pre-lttri 11173 ax-pre-lttrn 11174 ax-pre-ltadd 11175 ax-pre-mulgt0 11176

This theorem depends on definitions: df-bi 210 df-an 401 df-or 861 df-3or 1102 df-3an 1103 df-tru 1571 df-fal 1581 df-ex 1808 df-nf 1812 df-sb 2095 df-mo 2565 df-eu 2595 df-clab 2740 df-cleq 2753 df-clel 2836 df-nfc 2910 df-ne 2957 df-nel 3063 df-ral 3078 df-rex 3088 df-rmo 3367 df-reu 3368 df-rab 3415 df-v 3455 df-sbc 3744 df-csb 3853 df-dif 3907 df-un 3909 df-in 3911 df-ss 3921 df-pss 3924 df-nul 4286 df-if 4487 df-pw 4563 df-sn 4589 df-pr 4591 df-op 4595 df-uni 4872 df-int 4912 df-iun 4957 df-iin 4958 df-br 5109 df-opab 5173 df-mpt 5192 df-tr 5218 df-id 5556 df-eprel 5561 df-po 5569 df-so 5570 df-fr 5614 df-se 5615 df-we 5616 df-xp 5667 df-rel 5668 df-cnv 5669 df-co 5670 df-dm 5671 df-rn 5672 df-res 5673 df-ima 5674 df-pred 6302 df-ord 6363 df-on 6364 df-lim 6365 df-suc 6366 df-iota 6492 df-fun 6538 df-fn 6539 df-f 6540 df-f1 6541 df-fo 6542 df-f1o 6543 df-fv 6544 df-isom 6545 df-riota 7367 df-ov 7413 df-oprab 7414 df-mpo 7415 df-of 7674 df-om 7862 df-1st 7985 df-2nd 7986 df-supp 8156 df-tpos 8221 df-frecs 8277 df-wrecs 8308 df-recs 8357 df-rdg 8396 df-1o 8452 df-2o 8453 df-er 8693 df-map 8825 df-ixp 8895 df-en 8943 df-dom 8944 df-sdom 8945 df-fin 8946 df-fsupp 9321 df-sup 9401 df-inf 9402 df-oi 9471 df-card 9924 df-pnf 11244 df-mnf 11245 df-xr 11246 df-ltxr 11247 df-le 11248 df-sub 11442 df-neg 11443 df-nn 12233 df-2 12302 df-n0 12504 df-z 12591 df-uz 12862 df-fz 13535 df-fzo 13683 df-seq 14038 df-hash 14367 df-word 14551 df-concat 14608 df-s1 14634 df-sets 17223 df-slot 17241 df-ndx 17253 df-base 17269 df-ress 17290 df-plusg 17322 df-0g 17493 df-gsum 17494 df-mre 17637 df-mrc 17638 df-acs 17640 df-mgm 18697 df-sgrp 18776 df-mnd 18792 df-mhm 18840 df-submnd 18841 df-grp 19002 df-minusg 19003 df-sbg 19004 df-mulg 19133 df-subg 19188 df-ghm 19283 df-gim 19328 df-cntz 19386 df-oppg 19415 df-od 19597 df-pgp 19599 df-lsm 19705 df-cmn 19851 df-abl 19852 df-cyg 19947 df-dprd 20066

This theorem is referenced by: pgpfaclem2 20153

W3C validator