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 18396

Description: Lemma for pgpfac 18399. (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	. . . . . . . . 9 ⊢ (𝜑 → 𝑈 ∈ (SubGrp‘𝐺))
4		pgpfac.h	. . . . . . . . . 10 ⊢ 𝐻 = (𝐺 ↾_s 𝑈)
5	4	subggrp 17513	. . . . . . . . 9 ⊢ (𝑈 ∈ (SubGrp‘𝐺) → 𝐻 ∈ Grp)
6	3, 5	syl 17	. . . . . . . 8 ⊢ (𝜑 → 𝐻 ∈ Grp)
7		eqid 2626	. . . . . . . . 9 ⊢ (Base‘𝐻) = (Base‘𝐻)
8	7	subgacs 17545	. . . . . . . 8 ⊢ (𝐻 ∈ Grp → (SubGrp‘𝐻) ∈ (ACS‘(Base‘𝐻)))
9		acsmre 16229	. . . . . . . 8 ⊢ ((SubGrp‘𝐻) ∈ (ACS‘(Base‘𝐻)) → (SubGrp‘𝐻) ∈ (Moore‘(Base‘𝐻)))
10	6, 8, 9	3syl 18	. . . . . . 7 ⊢ (𝜑 → (SubGrp‘𝐻) ∈ (Moore‘(Base‘𝐻)))
11		pgpfac.x	. . . . . . . 8 ⊢ (𝜑 → 𝑋 ∈ 𝑈)
12	4	subgbas 17514	. . . . . . . . 9 ⊢ (𝑈 ∈ (SubGrp‘𝐺) → 𝑈 = (Base‘𝐻))
13	3, 12	syl 17	. . . . . . . 8 ⊢ (𝜑 → 𝑈 = (Base‘𝐻))
14	11, 13	eleqtrd 2706	. . . . . . 7 ⊢ (𝜑 → 𝑋 ∈ (Base‘𝐻))
15		pgpfac.k	. . . . . . . 8 ⊢ 𝐾 = (mrCls‘(SubGrp‘𝐻))
16	15	mrcsncl 16188	. . . . . . 7 ⊢ (((SubGrp‘𝐻) ∈ (Moore‘(Base‘𝐻)) ∧ 𝑋 ∈ (Base‘𝐻)) → (𝐾‘{𝑋}) ∈ (SubGrp‘𝐻))
17	10, 14, 16	syl2anc 692	. . . . . 6 ⊢ (𝜑 → (𝐾‘{𝑋}) ∈ (SubGrp‘𝐻))
18	4	subsubg 17533	. . . . . . 7 ⊢ (𝑈 ∈ (SubGrp‘𝐺) → ((𝐾‘{𝑋}) ∈ (SubGrp‘𝐻) ↔ ((𝐾‘{𝑋}) ∈ (SubGrp‘𝐺) ∧ (𝐾‘{𝑋}) ⊆ 𝑈)))
19	3, 18	syl 17	. . . . . 6 ⊢ (𝜑 → ((𝐾‘{𝑋}) ∈ (SubGrp‘𝐻) ↔ ((𝐾‘{𝑋}) ∈ (SubGrp‘𝐺) ∧ (𝐾‘{𝑋}) ⊆ 𝑈)))
20	17, 19	mpbid 222	. . . . 5 ⊢ (𝜑 → ((𝐾‘{𝑋}) ∈ (SubGrp‘𝐺) ∧ (𝐾‘{𝑋}) ⊆ 𝑈))
21	20	simpld 475	. . . 4 ⊢ (𝜑 → (𝐾‘{𝑋}) ∈ (SubGrp‘𝐺))
22	4	oveq1i 6615	. . . . . . 7 ⊢ (𝐻 ↾_s (𝐾‘{𝑋})) = ((𝐺 ↾_s 𝑈) ↾_s (𝐾‘{𝑋}))
23	20	simprd 479	. . . . . . . 8 ⊢ (𝜑 → (𝐾‘{𝑋}) ⊆ 𝑈)
24		ressabs 15855	. . . . . . . 8 ⊢ ((𝑈 ∈ (SubGrp‘𝐺) ∧ (𝐾‘{𝑋}) ⊆ 𝑈) → ((𝐺 ↾_s 𝑈) ↾_s (𝐾‘{𝑋})) = (𝐺 ↾_s (𝐾‘{𝑋})))
25	3, 23, 24	syl2anc 692	. . . . . . 7 ⊢ (𝜑 → ((𝐺 ↾_s 𝑈) ↾_s (𝐾‘{𝑋})) = (𝐺 ↾_s (𝐾‘{𝑋})))
26	22, 25	syl5eq 2672	. . . . . 6 ⊢ (𝜑 → (𝐻 ↾_s (𝐾‘{𝑋})) = (𝐺 ↾_s (𝐾‘{𝑋})))
27	7, 15	cycsubgcyg2 18219	. . . . . . 7 ⊢ ((𝐻 ∈ Grp ∧ 𝑋 ∈ (Base‘𝐻)) → (𝐻 ↾_s (𝐾‘{𝑋})) ∈ CycGrp)
28	6, 14, 27	syl2anc 692	. . . . . 6 ⊢ (𝜑 → (𝐻 ↾_s (𝐾‘{𝑋})) ∈ CycGrp)
29	26, 28	eqeltrrd 2705	. . . . 5 ⊢ (𝜑 → (𝐺 ↾_s (𝐾‘{𝑋})) ∈ CycGrp)
30		pgpfac.p	. . . . . . 7 ⊢ (𝜑 → 𝑃 pGrp 𝐺)
31		pgpprm 17924	. . . . . . 7 ⊢ (𝑃 pGrp 𝐺 → 𝑃 ∈ ℙ)
32	30, 31	syl 17	. . . . . 6 ⊢ (𝜑 → 𝑃 ∈ ℙ)
33		subgpgp 17928	. . . . . . 7 ⊢ ((𝑃 pGrp 𝐺 ∧ (𝐾‘{𝑋}) ∈ (SubGrp‘𝐺)) → 𝑃 pGrp (𝐺 ↾_s (𝐾‘{𝑋})))
34	30, 21, 33	syl2anc 692	. . . . . 6 ⊢ (𝜑 → 𝑃 pGrp (𝐺 ↾_s (𝐾‘{𝑋})))
35		brelrng 5319	. . . . . 6 ⊢ ((𝑃 ∈ ℙ ∧ (𝐺 ↾_s (𝐾‘{𝑋})) ∈ CycGrp ∧ 𝑃 pGrp (𝐺 ↾_s (𝐾‘{𝑋}))) → (𝐺 ↾_s (𝐾‘{𝑋})) ∈ ran pGrp )
36	32, 29, 34, 35	syl3anc 1323	. . . . 5 ⊢ (𝜑 → (𝐺 ↾_s (𝐾‘{𝑋})) ∈ ran pGrp )
37	29, 36	elind 3781	. . . 4 ⊢ (𝜑 → (𝐺 ↾_s (𝐾‘{𝑋})) ∈ (CycGrp ∩ ran pGrp ))
38		oveq2 6613	. . . . . 6 ⊢ (𝑟 = (𝐾‘{𝑋}) → (𝐺 ↾_s 𝑟) = (𝐺 ↾_s (𝐾‘{𝑋})))
39	38	eleq1d 2688	. . . . 5 ⊢ (𝑟 = (𝐾‘{𝑋}) → ((𝐺 ↾_s 𝑟) ∈ (CycGrp ∩ ran pGrp ) ↔ (𝐺 ↾_s (𝐾‘{𝑋})) ∈ (CycGrp ∩ ran pGrp )))
40		pgpfac.c	. . . . 5 ⊢ 𝐶 = {𝑟 ∈ (SubGrp‘𝐺) ∣ (𝐺 ↾_s 𝑟) ∈ (CycGrp ∩ ran pGrp )}
41	39, 40	elrab2 3353	. . . 4 ⊢ ((𝐾‘{𝑋}) ∈ 𝐶 ↔ ((𝐾‘{𝑋}) ∈ (SubGrp‘𝐺) ∧ (𝐺 ↾_s (𝐾‘{𝑋})) ∈ (CycGrp ∩ ran pGrp )))
42	21, 37, 41	sylanbrc 697	. . 3 ⊢ (𝜑 → (𝐾‘{𝑋}) ∈ 𝐶)
43	1, 2, 42	cats1cld 13532	. 2 ⊢ (𝜑 → 𝑇 ∈ Word 𝐶)
44		wrdf 13244	. . . . 5 ⊢ (𝑇 ∈ Word 𝐶 → 𝑇:(0..^(#‘𝑇))⟶𝐶)
45	43, 44	syl 17	. . . 4 ⊢ (𝜑 → 𝑇:(0..^(#‘𝑇))⟶𝐶)
46		ssrab2 3671	. . . . 5 ⊢ {𝑟 ∈ (SubGrp‘𝐺) ∣ (𝐺 ↾_s 𝑟) ∈ (CycGrp ∩ ran pGrp )} ⊆ (SubGrp‘𝐺)
47	40, 46	eqsstri 3619	. . . 4 ⊢ 𝐶 ⊆ (SubGrp‘𝐺)
48		fss 6015	. . . 4 ⊢ ((𝑇:(0..^(#‘𝑇))⟶𝐶 ∧ 𝐶 ⊆ (SubGrp‘𝐺)) → 𝑇:(0..^(#‘𝑇))⟶(SubGrp‘𝐺))
49	45, 47, 48	sylancl 693	. . 3 ⊢ (𝜑 → 𝑇:(0..^(#‘𝑇))⟶(SubGrp‘𝐺))
50		fzodisj 12440	. . . 4 ⊢ ((0..^(#‘𝑆)) ∩ ((#‘𝑆)..^((#‘𝑆) + 1))) = ∅
51		lencl 13258	. . . . . . . 8 ⊢ (𝑆 ∈ Word 𝐶 → (#‘𝑆) ∈ ℕ₀)
52	2, 51	syl 17	. . . . . . 7 ⊢ (𝜑 → (#‘𝑆) ∈ ℕ₀)
53	52	nn0zd 11424	. . . . . 6 ⊢ (𝜑 → (#‘𝑆) ∈ ℤ)
54		fzosn 12476	. . . . . 6 ⊢ ((#‘𝑆) ∈ ℤ → ((#‘𝑆)..^((#‘𝑆) + 1)) = {(#‘𝑆)})
55	53, 54	syl 17	. . . . 5 ⊢ (𝜑 → ((#‘𝑆)..^((#‘𝑆) + 1)) = {(#‘𝑆)})
56	55	ineq2d 3797	. . . 4 ⊢ (𝜑 → ((0..^(#‘𝑆)) ∩ ((#‘𝑆)..^((#‘𝑆) + 1))) = ((0..^(#‘𝑆)) ∩ {(#‘𝑆)}))
57	50, 56	syl5reqr 2675	. . 3 ⊢ (𝜑 → ((0..^(#‘𝑆)) ∩ {(#‘𝑆)}) = ∅)
58	1	fveq2i 6153	. . . . . . 7 ⊢ (#‘𝑇) = (#‘(𝑆 ++ ⟨“(𝐾‘{𝑋})”⟩))
59	42	s1cld 13317	. . . . . . . 8 ⊢ (𝜑 → ⟨“(𝐾‘{𝑋})”⟩ ∈ Word 𝐶)
60		ccatlen 13294	. . . . . . . 8 ⊢ ((𝑆 ∈ Word 𝐶 ∧ ⟨“(𝐾‘{𝑋})”⟩ ∈ Word 𝐶) → (#‘(𝑆 ++ ⟨“(𝐾‘{𝑋})”⟩)) = ((#‘𝑆) + (#‘⟨“(𝐾‘{𝑋})”⟩)))
61	2, 59, 60	syl2anc 692	. . . . . . 7 ⊢ (𝜑 → (#‘(𝑆 ++ ⟨“(𝐾‘{𝑋})”⟩)) = ((#‘𝑆) + (#‘⟨“(𝐾‘{𝑋})”⟩)))
62	58, 61	syl5eq 2672	. . . . . 6 ⊢ (𝜑 → (#‘𝑇) = ((#‘𝑆) + (#‘⟨“(𝐾‘{𝑋})”⟩)))
63		s1len 13319	. . . . . . 7 ⊢ (#‘⟨“(𝐾‘{𝑋})”⟩) = 1
64	63	oveq2i 6616	. . . . . 6 ⊢ ((#‘𝑆) + (#‘⟨“(𝐾‘{𝑋})”⟩)) = ((#‘𝑆) + 1)
65	62, 64	syl6eq 2676	. . . . 5 ⊢ (𝜑 → (#‘𝑇) = ((#‘𝑆) + 1))
66	65	oveq2d 6621	. . . 4 ⊢ (𝜑 → (0..^(#‘𝑇)) = (0..^((#‘𝑆) + 1)))
67		nn0uz 11666	. . . . . 6 ⊢ ℕ₀ = (ℤ_≥‘0)
68	52, 67	syl6eleq 2714	. . . . 5 ⊢ (𝜑 → (#‘𝑆) ∈ (ℤ_≥‘0))
69		fzosplitsn 12514	. . . . 5 ⊢ ((#‘𝑆) ∈ (ℤ_≥‘0) → (0..^((#‘𝑆) + 1)) = ((0..^(#‘𝑆)) ∪ {(#‘𝑆)}))
70	68, 69	syl 17	. . . 4 ⊢ (𝜑 → (0..^((#‘𝑆) + 1)) = ((0..^(#‘𝑆)) ∪ {(#‘𝑆)}))
71	66, 70	eqtrd 2660	. . 3 ⊢ (𝜑 → (0..^(#‘𝑇)) = ((0..^(#‘𝑆)) ∪ {(#‘𝑆)}))
72		eqid 2626	. . 3 ⊢ (Cntz‘𝐺) = (Cntz‘𝐺)
73		eqid 2626	. . 3 ⊢ (0_g‘𝐺) = (0_g‘𝐺)
74		pgpfac.4	. . . 4 ⊢ (𝜑 → 𝐺dom DProd 𝑆)
75		cats1un 13408	. . . . . . . 8 ⊢ ((𝑆 ∈ Word 𝐶 ∧ (𝐾‘{𝑋}) ∈ 𝐶) → (𝑆 ++ ⟨“(𝐾‘{𝑋})”⟩) = (𝑆 ∪ {⟨(#‘𝑆), (𝐾‘{𝑋})⟩}))
76	2, 42, 75	syl2anc 692	. . . . . . 7 ⊢ (𝜑 → (𝑆 ++ ⟨“(𝐾‘{𝑋})”⟩) = (𝑆 ∪ {⟨(#‘𝑆), (𝐾‘{𝑋})⟩}))
77	1, 76	syl5eq 2672	. . . . . 6 ⊢ (𝜑 → 𝑇 = (𝑆 ∪ {⟨(#‘𝑆), (𝐾‘{𝑋})⟩}))
78	77	reseq1d 5359	. . . . 5 ⊢ (𝜑 → (𝑇 ↾ (0..^(#‘𝑆))) = ((𝑆 ∪ {⟨(#‘𝑆), (𝐾‘{𝑋})⟩}) ↾ (0..^(#‘𝑆))))
79		wrdf 13244	. . . . . . 7 ⊢ (𝑆 ∈ Word 𝐶 → 𝑆:(0..^(#‘𝑆))⟶𝐶)
80		ffn 6004	. . . . . . 7 ⊢ (𝑆:(0..^(#‘𝑆))⟶𝐶 → 𝑆 Fn (0..^(#‘𝑆)))
81	2, 79, 80	3syl 18	. . . . . 6 ⊢ (𝜑 → 𝑆 Fn (0..^(#‘𝑆)))
82		fzonel 12421	. . . . . 6 ⊢ ¬ (#‘𝑆) ∈ (0..^(#‘𝑆))
83		fsnunres 6409	. . . . . 6 ⊢ ((𝑆 Fn (0..^(#‘𝑆)) ∧ ¬ (#‘𝑆) ∈ (0..^(#‘𝑆))) → ((𝑆 ∪ {⟨(#‘𝑆), (𝐾‘{𝑋})⟩}) ↾ (0..^(#‘𝑆))) = 𝑆)
84	81, 82, 83	sylancl 693	. . . . 5 ⊢ (𝜑 → ((𝑆 ∪ {⟨(#‘𝑆), (𝐾‘{𝑋})⟩}) ↾ (0..^(#‘𝑆))) = 𝑆)
85	78, 84	eqtrd 2660	. . . 4 ⊢ (𝜑 → (𝑇 ↾ (0..^(#‘𝑆))) = 𝑆)
86	74, 85	breqtrrd 4646	. . 3 ⊢ (𝜑 → 𝐺dom DProd (𝑇 ↾ (0..^(#‘𝑆))))
87		fvex 6160	. . . . . 6 ⊢ (#‘𝑆) ∈ V
88		dprdsn 18351	. . . . . 6 ⊢ (((#‘𝑆) ∈ V ∧ (𝐾‘{𝑋}) ∈ (SubGrp‘𝐺)) → (𝐺dom DProd {⟨(#‘𝑆), (𝐾‘{𝑋})⟩} ∧ (𝐺 DProd {⟨(#‘𝑆), (𝐾‘{𝑋})⟩}) = (𝐾‘{𝑋})))
89	87, 21, 88	sylancr 694	. . . . 5 ⊢ (𝜑 → (𝐺dom DProd {⟨(#‘𝑆), (𝐾‘{𝑋})⟩} ∧ (𝐺 DProd {⟨(#‘𝑆), (𝐾‘{𝑋})⟩}) = (𝐾‘{𝑋})))
90	89	simpld 475	. . . 4 ⊢ (𝜑 → 𝐺dom DProd {⟨(#‘𝑆), (𝐾‘{𝑋})⟩})
91		ffn 6004	. . . . . . 7 ⊢ (𝑇:(0..^(#‘𝑇))⟶𝐶 → 𝑇 Fn (0..^(#‘𝑇)))
92	43, 44, 91	3syl 18	. . . . . 6 ⊢ (𝜑 → 𝑇 Fn (0..^(#‘𝑇)))
93		ssun2 3760	. . . . . . . 8 ⊢ {(#‘𝑆)} ⊆ ((0..^(#‘𝑆)) ∪ {(#‘𝑆)})
94	87	snss 4291	. . . . . . . 8 ⊢ ((#‘𝑆) ∈ ((0..^(#‘𝑆)) ∪ {(#‘𝑆)}) ↔ {(#‘𝑆)} ⊆ ((0..^(#‘𝑆)) ∪ {(#‘𝑆)}))
95	93, 94	mpbir 221	. . . . . . 7 ⊢ (#‘𝑆) ∈ ((0..^(#‘𝑆)) ∪ {(#‘𝑆)})
96	95, 71	syl5eleqr 2711	. . . . . 6 ⊢ (𝜑 → (#‘𝑆) ∈ (0..^(#‘𝑇)))
97		fnressn 6380	. . . . . 6 ⊢ ((𝑇 Fn (0..^(#‘𝑇)) ∧ (#‘𝑆) ∈ (0..^(#‘𝑇))) → (𝑇 ↾ {(#‘𝑆)}) = {⟨(#‘𝑆), (𝑇‘(#‘𝑆))⟩})
98	92, 96, 97	syl2anc 692	. . . . 5 ⊢ (𝜑 → (𝑇 ↾ {(#‘𝑆)}) = {⟨(#‘𝑆), (𝑇‘(#‘𝑆))⟩})
99	1	fveq1i 6151	. . . . . . . . 9 ⊢ (𝑇‘(#‘𝑆)) = ((𝑆 ++ ⟨“(𝐾‘{𝑋})”⟩)‘(#‘𝑆))
100	52	nn0cnd 11298	. . . . . . . . . . . 12 ⊢ (𝜑 → (#‘𝑆) ∈ ℂ)
101	100	addid2d 10182	. . . . . . . . . . 11 ⊢ (𝜑 → (0 + (#‘𝑆)) = (#‘𝑆))
102	101	eqcomd 2632	. . . . . . . . . 10 ⊢ (𝜑 → (#‘𝑆) = (0 + (#‘𝑆)))
103	102	fveq2d 6154	. . . . . . . . 9 ⊢ (𝜑 → ((𝑆 ++ ⟨“(𝐾‘{𝑋})”⟩)‘(#‘𝑆)) = ((𝑆 ++ ⟨“(𝐾‘{𝑋})”⟩)‘(0 + (#‘𝑆))))
104	99, 103	syl5eq 2672	. . . . . . . 8 ⊢ (𝜑 → (𝑇‘(#‘𝑆)) = ((𝑆 ++ ⟨“(𝐾‘{𝑋})”⟩)‘(0 + (#‘𝑆))))
105		1nn 10976	. . . . . . . . . . . 12 ⊢ 1 ∈ ℕ
106	105	a1i 11	. . . . . . . . . . 11 ⊢ (𝜑 → 1 ∈ ℕ)
107	63, 106	syl5eqel 2708	. . . . . . . . . 10 ⊢ (𝜑 → (#‘⟨“(𝐾‘{𝑋})”⟩) ∈ ℕ)
108		lbfzo0 12445	. . . . . . . . . 10 ⊢ (0 ∈ (0..^(#‘⟨“(𝐾‘{𝑋})”⟩)) ↔ (#‘⟨“(𝐾‘{𝑋})”⟩) ∈ ℕ)
109	107, 108	sylibr 224	. . . . . . . . 9 ⊢ (𝜑 → 0 ∈ (0..^(#‘⟨“(𝐾‘{𝑋})”⟩)))
110		ccatval3 13297	. . . . . . . . 9 ⊢ ((𝑆 ∈ Word 𝐶 ∧ ⟨“(𝐾‘{𝑋})”⟩ ∈ Word 𝐶 ∧ 0 ∈ (0..^(#‘⟨“(𝐾‘{𝑋})”⟩))) → ((𝑆 ++ ⟨“(𝐾‘{𝑋})”⟩)‘(0 + (#‘𝑆))) = (⟨“(𝐾‘{𝑋})”⟩‘0))
111	2, 59, 109, 110	syl3anc 1323	. . . . . . . 8 ⊢ (𝜑 → ((𝑆 ++ ⟨“(𝐾‘{𝑋})”⟩)‘(0 + (#‘𝑆))) = (⟨“(𝐾‘{𝑋})”⟩‘0))
112		fvex 6160	. . . . . . . . 9 ⊢ (𝐾‘{𝑋}) ∈ V
113		s1fv 13324	. . . . . . . . 9 ⊢ ((𝐾‘{𝑋}) ∈ V → (⟨“(𝐾‘{𝑋})”⟩‘0) = (𝐾‘{𝑋}))
114	112, 113	mp1i 13	. . . . . . . 8 ⊢ (𝜑 → (⟨“(𝐾‘{𝑋})”⟩‘0) = (𝐾‘{𝑋}))
115	104, 111, 114	3eqtrd 2664	. . . . . . 7 ⊢ (𝜑 → (𝑇‘(#‘𝑆)) = (𝐾‘{𝑋}))
116	115	opeq2d 4382	. . . . . 6 ⊢ (𝜑 → ⟨(#‘𝑆), (𝑇‘(#‘𝑆))⟩ = ⟨(#‘𝑆), (𝐾‘{𝑋})⟩)
117	116	sneqd 4165	. . . . 5 ⊢ (𝜑 → {⟨(#‘𝑆), (𝑇‘(#‘𝑆))⟩} = {⟨(#‘𝑆), (𝐾‘{𝑋})⟩})
118	98, 117	eqtrd 2660	. . . 4 ⊢ (𝜑 → (𝑇 ↾ {(#‘𝑆)}) = {⟨(#‘𝑆), (𝐾‘{𝑋})⟩})
119	90, 118	breqtrrd 4646	. . 3 ⊢ (𝜑 → 𝐺dom DProd (𝑇 ↾ {(#‘𝑆)}))
120		pgpfac.g	. . . 4 ⊢ (𝜑 → 𝐺 ∈ Abel)
121		dprdsubg 18339	. . . . 5 ⊢ (𝐺dom DProd (𝑇 ↾ (0..^(#‘𝑆))) → (𝐺 DProd (𝑇 ↾ (0..^(#‘𝑆)))) ∈ (SubGrp‘𝐺))
122	86, 121	syl 17	. . . 4 ⊢ (𝜑 → (𝐺 DProd (𝑇 ↾ (0..^(#‘𝑆)))) ∈ (SubGrp‘𝐺))
123		dprdsubg 18339	. . . . 5 ⊢ (𝐺dom DProd (𝑇 ↾ {(#‘𝑆)}) → (𝐺 DProd (𝑇 ↾ {(#‘𝑆)})) ∈ (SubGrp‘𝐺))
124	119, 123	syl 17	. . . 4 ⊢ (𝜑 → (𝐺 DProd (𝑇 ↾ {(#‘𝑆)})) ∈ (SubGrp‘𝐺))
125	72, 120, 122, 124	ablcntzd 18176	. . 3 ⊢ (𝜑 → (𝐺 DProd (𝑇 ↾ (0..^(#‘𝑆)))) ⊆ ((Cntz‘𝐺)‘(𝐺 DProd (𝑇 ↾ {(#‘𝑆)}))))
126		pgpfac.i	. . . 4 ⊢ (𝜑 → ((𝐾‘{𝑋}) ∩ 𝑊) = { 0 })
127	85	oveq2d 6621	. . . . . . 7 ⊢ (𝜑 → (𝐺 DProd (𝑇 ↾ (0..^(#‘𝑆)))) = (𝐺 DProd 𝑆))
128		pgpfac.5	. . . . . . 7 ⊢ (𝜑 → (𝐺 DProd 𝑆) = 𝑊)
129	127, 128	eqtrd 2660	. . . . . 6 ⊢ (𝜑 → (𝐺 DProd (𝑇 ↾ (0..^(#‘𝑆)))) = 𝑊)
130	118	oveq2d 6621	. . . . . . 7 ⊢ (𝜑 → (𝐺 DProd (𝑇 ↾ {(#‘𝑆)})) = (𝐺 DProd {⟨(#‘𝑆), (𝐾‘{𝑋})⟩}))
131	89	simprd 479	. . . . . . 7 ⊢ (𝜑 → (𝐺 DProd {⟨(#‘𝑆), (𝐾‘{𝑋})⟩}) = (𝐾‘{𝑋}))
132	130, 131	eqtrd 2660	. . . . . 6 ⊢ (𝜑 → (𝐺 DProd (𝑇 ↾ {(#‘𝑆)})) = (𝐾‘{𝑋}))
133	129, 132	ineq12d 3798	. . . . 5 ⊢ (𝜑 → ((𝐺 DProd (𝑇 ↾ (0..^(#‘𝑆)))) ∩ (𝐺 DProd (𝑇 ↾ {(#‘𝑆)}))) = (𝑊 ∩ (𝐾‘{𝑋})))
134		incom 3788	. . . . 5 ⊢ (𝑊 ∩ (𝐾‘{𝑋})) = ((𝐾‘{𝑋}) ∩ 𝑊)
135	133, 134	syl6eq 2676	. . . 4 ⊢ (𝜑 → ((𝐺 DProd (𝑇 ↾ (0..^(#‘𝑆)))) ∩ (𝐺 DProd (𝑇 ↾ {(#‘𝑆)}))) = ((𝐾‘{𝑋}) ∩ 𝑊))
136	4, 73	subg0 17516	. . . . . . 7 ⊢ (𝑈 ∈ (SubGrp‘𝐺) → (0_g‘𝐺) = (0_g‘𝐻))
137	3, 136	syl 17	. . . . . 6 ⊢ (𝜑 → (0_g‘𝐺) = (0_g‘𝐻))
138		pgpfac.0	. . . . . 6 ⊢ 0 = (0_g‘𝐻)
139	137, 138	syl6eqr 2678	. . . . 5 ⊢ (𝜑 → (0_g‘𝐺) = 0 )
140	139	sneqd 4165	. . . 4 ⊢ (𝜑 → {(0_g‘𝐺)} = { 0 })
141	126, 135, 140	3eqtr4d 2670	. . 3 ⊢ (𝜑 → ((𝐺 DProd (𝑇 ↾ (0..^(#‘𝑆)))) ∩ (𝐺 DProd (𝑇 ↾ {(#‘𝑆)}))) = {(0_g‘𝐺)})
142	49, 57, 71, 72, 73, 86, 119, 125, 141	dmdprdsplit2 18361	. 2 ⊢ (𝜑 → 𝐺dom DProd 𝑇)
143		eqid 2626	. . . . 5 ⊢ (LSSum‘𝐺) = (LSSum‘𝐺)
144	49, 57, 71, 143, 142	dprdsplit 18363	. . . 4 ⊢ (𝜑 → (𝐺 DProd 𝑇) = ((𝐺 DProd (𝑇 ↾ (0..^(#‘𝑆))))(LSSum‘𝐺)(𝐺 DProd (𝑇 ↾ {(#‘𝑆)}))))
145	129, 132	oveq12d 6623	. . . 4 ⊢ (𝜑 → ((𝐺 DProd (𝑇 ↾ (0..^(#‘𝑆))))(LSSum‘𝐺)(𝐺 DProd (𝑇 ↾ {(#‘𝑆)}))) = (𝑊(LSSum‘𝐺)(𝐾‘{𝑋})))
146	129, 122	eqeltrrd 2705	. . . . 5 ⊢ (𝜑 → 𝑊 ∈ (SubGrp‘𝐺))
147	143	lsmcom 18177	. . . . 5 ⊢ ((𝐺 ∈ Abel ∧ 𝑊 ∈ (SubGrp‘𝐺) ∧ (𝐾‘{𝑋}) ∈ (SubGrp‘𝐺)) → (𝑊(LSSum‘𝐺)(𝐾‘{𝑋})) = ((𝐾‘{𝑋})(LSSum‘𝐺)𝑊))
148	120, 146, 21, 147	syl3anc 1323	. . . 4 ⊢ (𝜑 → (𝑊(LSSum‘𝐺)(𝐾‘{𝑋})) = ((𝐾‘{𝑋})(LSSum‘𝐺)𝑊))
149	144, 145, 148	3eqtrd 2664	. . 3 ⊢ (𝜑 → (𝐺 DProd 𝑇) = ((𝐾‘{𝑋})(LSSum‘𝐺)𝑊))
150		pgpfac.w	. . . . . 6 ⊢ (𝜑 → 𝑊 ∈ (SubGrp‘𝐻))
151	7	subgss 17511	. . . . . 6 ⊢ (𝑊 ∈ (SubGrp‘𝐻) → 𝑊 ⊆ (Base‘𝐻))
152	150, 151	syl 17	. . . . 5 ⊢ (𝜑 → 𝑊 ⊆ (Base‘𝐻))
153	152, 13	sseqtr4d 3626	. . . 4 ⊢ (𝜑 → 𝑊 ⊆ 𝑈)
154		pgpfac.l	. . . . 5 ⊢ ⊕ = (LSSum‘𝐻)
155	4, 143, 154	subglsm 18002	. . . 4 ⊢ ((𝑈 ∈ (SubGrp‘𝐺) ∧ (𝐾‘{𝑋}) ⊆ 𝑈 ∧ 𝑊 ⊆ 𝑈) → ((𝐾‘{𝑋})(LSSum‘𝐺)𝑊) = ((𝐾‘{𝑋}) ⊕ 𝑊))
156	3, 23, 153, 155	syl3anc 1323	. . 3 ⊢ (𝜑 → ((𝐾‘{𝑋})(LSSum‘𝐺)𝑊) = ((𝐾‘{𝑋}) ⊕ 𝑊))
157		pgpfac.s	. . 3 ⊢ (𝜑 → ((𝐾‘{𝑋}) ⊕ 𝑊) = 𝑈)
158	149, 156, 157	3eqtrd 2664	. 2 ⊢ (𝜑 → (𝐺 DProd 𝑇) = 𝑈)
159		breq2 4622	. . . 4 ⊢ (𝑠 = 𝑇 → (𝐺dom DProd 𝑠 ↔ 𝐺dom DProd 𝑇))
160		oveq2 6613	. . . . 5 ⊢ (𝑠 = 𝑇 → (𝐺 DProd 𝑠) = (𝐺 DProd 𝑇))
161	160	eqeq1d 2628	. . . 4 ⊢ (𝑠 = 𝑇 → ((𝐺 DProd 𝑠) = 𝑈 ↔ (𝐺 DProd 𝑇) = 𝑈))
162	159, 161	anbi12d 746	. . 3 ⊢ (𝑠 = 𝑇 → ((𝐺dom DProd 𝑠 ∧ (𝐺 DProd 𝑠) = 𝑈) ↔ (𝐺dom DProd 𝑇 ∧ (𝐺 DProd 𝑇) = 𝑈)))
163	162	rspcev 3300	. 2 ⊢ ((𝑇 ∈ Word 𝐶 ∧ (𝐺dom DProd 𝑇 ∧ (𝐺 DProd 𝑇) = 𝑈)) → ∃𝑠 ∈ Word 𝐶(𝐺dom DProd 𝑠 ∧ (𝐺 DProd 𝑠) = 𝑈))
164	43, 142, 158, 163	syl12anc 1321	1 ⊢ (𝜑 → ∃𝑠 ∈ Word 𝐶(𝐺dom DProd 𝑠 ∧ (𝐺 DProd 𝑠) = 𝑈))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 196 ∧ wa 384 = wceq 1480 ∈ wcel 1992 ≠ wne 2796 ∀wral 2912 ∃wrex 2913 {crab 2916 Vcvv 3191 ∪ cun 3558 ∩ cin 3559 ⊆ wss 3560 ⊊ wpss 3561 ∅c0 3896 {csn 4153 ⟨cop 4159 class class class wbr 4618 dom cdm 5079 ran crn 5080 ↾ cres 5081 Fn wfn 5845 ⟶wf 5846 ‘cfv 5850 (class class class)co 6605 Fincfn 7900 0cc0 9881 1c1 9882 + caddc 9884 ℕcn 10965 ℕ₀cn0 11237 ℤcz 11322 ℤ_≥cuz 11631 ..^cfzo 12403 #chash 13054 Word cword 13225 ++ cconcat 13227 ⟨“cs1 13228 ℙcprime 15304 Basecbs 15776 ↾_s cress 15777 0_gc0g 16016 Moorecmre 16158 mrClscmrc 16159 ACScacs 16161 Grpcgrp 17338 SubGrpcsubg 17504 Cntzccntz 17664 odcod 17860 gExcgex 17861 pGrp cpgp 17862 LSSumclsm 17965 Abelcabl 18110 CycGrpccyg 18195 DProd cdprd 18308

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1719 ax-4 1734 ax-5 1841 ax-6 1890 ax-7 1937 ax-8 1994 ax-9 2001 ax-10 2021 ax-11 2036 ax-12 2049 ax-13 2250 ax-ext 2606 ax-rep 4736 ax-sep 4746 ax-nul 4754 ax-pow 4808 ax-pr 4872 ax-un 6903 ax-inf2 8483 ax-cnex 9937 ax-resscn 9938 ax-1cn 9939 ax-icn 9940 ax-addcl 9941 ax-addrcl 9942 ax-mulcl 9943 ax-mulrcl 9944 ax-mulcom 9945 ax-addass 9946 ax-mulass 9947 ax-distr 9948 ax-i2m1 9949 ax-1ne0 9950 ax-1rid 9951 ax-rnegex 9952 ax-rrecex 9953 ax-cnre 9954 ax-pre-lttri 9955 ax-pre-lttrn 9956 ax-pre-ltadd 9957 ax-pre-mulgt0 9958

This theorem depends on definitions: df-bi 197 df-or 385 df-an 386 df-3or 1037 df-3an 1038 df-tru 1483 df-ex 1702 df-nf 1707 df-sb 1883 df-eu 2478 df-mo 2479 df-clab 2613 df-cleq 2619 df-clel 2622 df-nfc 2756 df-ne 2797 df-nel 2900 df-ral 2917 df-rex 2918 df-reu 2919 df-rmo 2920 df-rab 2921 df-v 3193 df-sbc 3423 df-csb 3520 df-dif 3563 df-un 3565 df-in 3567 df-ss 3574 df-pss 3576 df-nul 3897 df-if 4064 df-pw 4137 df-sn 4154 df-pr 4156 df-tp 4158 df-op 4160 df-uni 4408 df-int 4446 df-iun 4492 df-iin 4493 df-br 4619 df-opab 4679 df-mpt 4680 df-tr 4718 df-eprel 4990 df-id 4994 df-po 5000 df-so 5001 df-fr 5038 df-se 5039 df-we 5040 df-xp 5085 df-rel 5086 df-cnv 5087 df-co 5088 df-dm 5089 df-rn 5090 df-res 5091 df-ima 5092 df-pred 5642 df-ord 5688 df-on 5689 df-lim 5690 df-suc 5691 df-iota 5813 df-fun 5852 df-fn 5853 df-f 5854 df-f1 5855 df-fo 5856 df-f1o 5857 df-fv 5858 df-isom 5859 df-riota 6566 df-ov 6608 df-oprab 6609 df-mpt2 6610 df-of 6851 df-om 7014 df-1st 7116 df-2nd 7117 df-supp 7242 df-tpos 7298 df-wrecs 7353 df-recs 7414 df-rdg 7452 df-1o 7506 df-oadd 7510 df-er 7688 df-map 7805 df-ixp 7854 df-en 7901 df-dom 7902 df-sdom 7903 df-fin 7904 df-fsupp 8221 df-sup 8293 df-inf 8294 df-oi 8360 df-card 8710 df-pnf 10021 df-mnf 10022 df-xr 10023 df-ltxr 10024 df-le 10025 df-sub 10213 df-neg 10214 df-nn 10966 df-2 11024 df-n0 11238 df-z 11323 df-uz 11632 df-fz 12266 df-fzo 12404 df-seq 12739 df-hash 13055 df-word 13233 df-concat 13235 df-s1 13236 df-ndx 15779 df-slot 15780 df-base 15781 df-sets 15782 df-ress 15783 df-plusg 15870 df-0g 16018 df-gsum 16019 df-mre 16162 df-mrc 16163 df-acs 16165 df-mgm 17158 df-sgrp 17200 df-mnd 17211 df-mhm 17251 df-submnd 17252 df-grp 17341 df-minusg 17342 df-sbg 17343 df-mulg 17457 df-subg 17507 df-ghm 17574 df-gim 17617 df-cntz 17666 df-oppg 17692 df-od 17864 df-pgp 17866 df-lsm 17967 df-cmn 18111 df-abl 18112 df-cyg 18196 df-dprd 18310

This theorem is referenced by: pgpfaclem2 18397

W3C validator