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 20047

Description: Lemma for pgpfac 20050. (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 19094	. . . . . . . . . 10 ⊢ (𝑈 ∈ (SubGrp‘𝐺) → 𝐻 ∈ Grp)
6	3, 5	syl 17	. . . . . . . . 9 ⊢ (𝜑 → 𝐻 ∈ Grp)
7		eqid 2737	. . . . . . . . . 10 ⊢ (Base‘𝐻) = (Base‘𝐻)
8	7	subgacs 19125	. . . . . . . . 9 ⊢ (𝐻 ∈ Grp → (SubGrp‘𝐻) ∈ (ACS‘(Base‘𝐻)))
9	6, 8	syl 17	. . . . . . . 8 ⊢ (𝜑 → (SubGrp‘𝐻) ∈ (ACS‘(Base‘𝐻)))
10	9	acsmred 17611	. . . . . . 7 ⊢ (𝜑 → (SubGrp‘𝐻) ∈ (Moore‘(Base‘𝐻)))
11		pgpfac.x	. . . . . . . 8 ⊢ (𝜑 → 𝑋 ∈ 𝑈)
12	4	subgbas 19095	. . . . . . . . 9 ⊢ (𝑈 ∈ (SubGrp‘𝐺) → 𝑈 = (Base‘𝐻))
13	3, 12	syl 17	. . . . . . . 8 ⊢ (𝜑 → 𝑈 = (Base‘𝐻))
14	11, 13	eleqtrd 2839	. . . . . . 7 ⊢ (𝜑 → 𝑋 ∈ (Base‘𝐻))
15		pgpfac.k	. . . . . . . 8 ⊢ 𝐾 = (mrCls‘(SubGrp‘𝐻))
16	15	mrcsncl 17567	. . . . . . 7 ⊢ (((SubGrp‘𝐻) ∈ (Moore‘(Base‘𝐻)) ∧ 𝑋 ∈ (Base‘𝐻)) → (𝐾‘{𝑋}) ∈ (SubGrp‘𝐻))
17	10, 14, 16	syl2anc 585	. . . . . 6 ⊢ (𝜑 → (𝐾‘{𝑋}) ∈ (SubGrp‘𝐻))
18	4	subsubg 19114	. . . . . . 7 ⊢ (𝑈 ∈ (SubGrp‘𝐺) → ((𝐾‘{𝑋}) ∈ (SubGrp‘𝐻) ↔ ((𝐾‘{𝑋}) ∈ (SubGrp‘𝐺) ∧ (𝐾‘{𝑋}) ⊆ 𝑈)))
19	3, 18	syl 17	. . . . . 6 ⊢ (𝜑 → ((𝐾‘{𝑋}) ∈ (SubGrp‘𝐻) ↔ ((𝐾‘{𝑋}) ∈ (SubGrp‘𝐺) ∧ (𝐾‘{𝑋}) ⊆ 𝑈)))
20	17, 19	mpbid 232	. . . . 5 ⊢ (𝜑 → ((𝐾‘{𝑋}) ∈ (SubGrp‘𝐺) ∧ (𝐾‘{𝑋}) ⊆ 𝑈))
21	20	simpld 494	. . . 4 ⊢ (𝜑 → (𝐾‘{𝑋}) ∈ (SubGrp‘𝐺))
22	4	oveq1i 7368	. . . . . . 7 ⊢ (𝐻 ↾_s (𝐾‘{𝑋})) = ((𝐺 ↾_s 𝑈) ↾_s (𝐾‘{𝑋}))
23	20	simprd 495	. . . . . . . 8 ⊢ (𝜑 → (𝐾‘{𝑋}) ⊆ 𝑈)
24		ressabs 17207	. . . . . . . 8 ⊢ ((𝑈 ∈ (SubGrp‘𝐺) ∧ (𝐾‘{𝑋}) ⊆ 𝑈) → ((𝐺 ↾_s 𝑈) ↾_s (𝐾‘{𝑋})) = (𝐺 ↾_s (𝐾‘{𝑋})))
25	3, 23, 24	syl2anc 585	. . . . . . 7 ⊢ (𝜑 → ((𝐺 ↾_s 𝑈) ↾_s (𝐾‘{𝑋})) = (𝐺 ↾_s (𝐾‘{𝑋})))
26	22, 25	eqtrid 2784	. . . . . 6 ⊢ (𝜑 → (𝐻 ↾_s (𝐾‘{𝑋})) = (𝐺 ↾_s (𝐾‘{𝑋})))
27	7, 15	cycsubgcyg2 19866	. . . . . . 7 ⊢ ((𝐻 ∈ Grp ∧ 𝑋 ∈ (Base‘𝐻)) → (𝐻 ↾_s (𝐾‘{𝑋})) ∈ CycGrp)
28	6, 14, 27	syl2anc 585	. . . . . 6 ⊢ (𝜑 → (𝐻 ↾_s (𝐾‘{𝑋})) ∈ CycGrp)
29	26, 28	eqeltrrd 2838	. . . . 5 ⊢ (𝜑 → (𝐺 ↾_s (𝐾‘{𝑋})) ∈ CycGrp)
30		pgpfac.p	. . . . . . 7 ⊢ (𝜑 → 𝑃 pGrp 𝐺)
31		pgpprm 19557	. . . . . . 7 ⊢ (𝑃 pGrp 𝐺 → 𝑃 ∈ ℙ)
32	30, 31	syl 17	. . . . . 6 ⊢ (𝜑 → 𝑃 ∈ ℙ)
33		subgpgp 19561	. . . . . . 7 ⊢ ((𝑃 pGrp 𝐺 ∧ (𝐾‘{𝑋}) ∈ (SubGrp‘𝐺)) → 𝑃 pGrp (𝐺 ↾_s (𝐾‘{𝑋})))
34	30, 21, 33	syl2anc 585	. . . . . 6 ⊢ (𝜑 → 𝑃 pGrp (𝐺 ↾_s (𝐾‘{𝑋})))
35		brelrng 5888	. . . . . 6 ⊢ ((𝑃 ∈ ℙ ∧ (𝐺 ↾_s (𝐾‘{𝑋})) ∈ CycGrp ∧ 𝑃 pGrp (𝐺 ↾_s (𝐾‘{𝑋}))) → (𝐺 ↾_s (𝐾‘{𝑋})) ∈ ran pGrp )
36	32, 29, 34, 35	syl3anc 1374	. . . . 5 ⊢ (𝜑 → (𝐺 ↾_s (𝐾‘{𝑋})) ∈ ran pGrp )
37	29, 36	elind 4141	. . . 4 ⊢ (𝜑 → (𝐺 ↾_s (𝐾‘{𝑋})) ∈ (CycGrp ∩ ran pGrp ))
38		oveq2 7366	. . . . . 6 ⊢ (𝑟 = (𝐾‘{𝑋}) → (𝐺 ↾_s 𝑟) = (𝐺 ↾_s (𝐾‘{𝑋})))
39	38	eleq1d 2822	. . . . 5 ⊢ (𝑟 = (𝐾‘{𝑋}) → ((𝐺 ↾_s 𝑟) ∈ (CycGrp ∩ ran pGrp ) ↔ (𝐺 ↾_s (𝐾‘{𝑋})) ∈ (CycGrp ∩ ran pGrp )))
40		pgpfac.c	. . . . 5 ⊢ 𝐶 = {𝑟 ∈ (SubGrp‘𝐺) ∣ (𝐺 ↾_s 𝑟) ∈ (CycGrp ∩ ran pGrp )}
41	39, 40	elrab2 3638	. . . 4 ⊢ ((𝐾‘{𝑋}) ∈ 𝐶 ↔ ((𝐾‘{𝑋}) ∈ (SubGrp‘𝐺) ∧ (𝐺 ↾_s (𝐾‘{𝑋})) ∈ (CycGrp ∩ ran pGrp )))
42	21, 37, 41	sylanbrc 584	. . 3 ⊢ (𝜑 → (𝐾‘{𝑋}) ∈ 𝐶)
43	1, 2, 42	cats1cld 14806	. 2 ⊢ (𝜑 → 𝑇 ∈ Word 𝐶)
44		wrdf 14469	. . . . 5 ⊢ (𝑇 ∈ Word 𝐶 → 𝑇:(0..^(♯‘𝑇))⟶𝐶)
45	43, 44	syl 17	. . . 4 ⊢ (𝜑 → 𝑇:(0..^(♯‘𝑇))⟶𝐶)
46	40	ssrab3 4023	. . . 4 ⊢ 𝐶 ⊆ (SubGrp‘𝐺)
47		fss 6676	. . . 4 ⊢ ((𝑇:(0..^(♯‘𝑇))⟶𝐶 ∧ 𝐶 ⊆ (SubGrp‘𝐺)) → 𝑇:(0..^(♯‘𝑇))⟶(SubGrp‘𝐺))
48	45, 46, 47	sylancl 587	. . 3 ⊢ (𝜑 → 𝑇:(0..^(♯‘𝑇))⟶(SubGrp‘𝐺))
49		lencl 14484	. . . . . . . 8 ⊢ (𝑆 ∈ Word 𝐶 → (♯‘𝑆) ∈ ℕ₀)
50	2, 49	syl 17	. . . . . . 7 ⊢ (𝜑 → (♯‘𝑆) ∈ ℕ₀)
51	50	nn0zd 12538	. . . . . 6 ⊢ (𝜑 → (♯‘𝑆) ∈ ℤ)
52		fzosn 13680	. . . . . 6 ⊢ ((♯‘𝑆) ∈ ℤ → ((♯‘𝑆)..^((♯‘𝑆) + 1)) = {(♯‘𝑆)})
53	51, 52	syl 17	. . . . 5 ⊢ (𝜑 → ((♯‘𝑆)..^((♯‘𝑆) + 1)) = {(♯‘𝑆)})
54	53	ineq2d 4161	. . . 4 ⊢ (𝜑 → ((0..^(♯‘𝑆)) ∩ ((♯‘𝑆)..^((♯‘𝑆) + 1))) = ((0..^(♯‘𝑆)) ∩ {(♯‘𝑆)}))
55		fzodisj 13637	. . . 4 ⊢ ((0..^(♯‘𝑆)) ∩ ((♯‘𝑆)..^((♯‘𝑆) + 1))) = ∅
56	54, 55	eqtr3di 2787	. . 3 ⊢ (𝜑 → ((0..^(♯‘𝑆)) ∩ {(♯‘𝑆)}) = ∅)
57	1	fveq2i 6835	. . . . . . 7 ⊢ (♯‘𝑇) = (♯‘(𝑆 ++ ⟨“(𝐾‘{𝑋})”⟩))
58	42	s1cld 14555	. . . . . . . 8 ⊢ (𝜑 → ⟨“(𝐾‘{𝑋})”⟩ ∈ Word 𝐶)
59		ccatlen 14526	. . . . . . . 8 ⊢ ((𝑆 ∈ Word 𝐶 ∧ ⟨“(𝐾‘{𝑋})”⟩ ∈ Word 𝐶) → (♯‘(𝑆 ++ ⟨“(𝐾‘{𝑋})”⟩)) = ((♯‘𝑆) + (♯‘⟨“(𝐾‘{𝑋})”⟩)))
60	2, 58, 59	syl2anc 585	. . . . . . 7 ⊢ (𝜑 → (♯‘(𝑆 ++ ⟨“(𝐾‘{𝑋})”⟩)) = ((♯‘𝑆) + (♯‘⟨“(𝐾‘{𝑋})”⟩)))
61	57, 60	eqtrid 2784	. . . . . 6 ⊢ (𝜑 → (♯‘𝑇) = ((♯‘𝑆) + (♯‘⟨“(𝐾‘{𝑋})”⟩)))
62		s1len 14558	. . . . . . 7 ⊢ (♯‘⟨“(𝐾‘{𝑋})”⟩) = 1
63	62	oveq2i 7369	. . . . . 6 ⊢ ((♯‘𝑆) + (♯‘⟨“(𝐾‘{𝑋})”⟩)) = ((♯‘𝑆) + 1)
64	61, 63	eqtrdi 2788	. . . . 5 ⊢ (𝜑 → (♯‘𝑇) = ((♯‘𝑆) + 1))
65	64	oveq2d 7374	. . . 4 ⊢ (𝜑 → (0..^(♯‘𝑇)) = (0..^((♯‘𝑆) + 1)))
66		nn0uz 12815	. . . . . 6 ⊢ ℕ₀ = (ℤ_≥‘0)
67	50, 66	eleqtrdi 2847	. . . . 5 ⊢ (𝜑 → (♯‘𝑆) ∈ (ℤ_≥‘0))
68		fzosplitsn 13720	. . . . 5 ⊢ ((♯‘𝑆) ∈ (ℤ_≥‘0) → (0..^((♯‘𝑆) + 1)) = ((0..^(♯‘𝑆)) ∪ {(♯‘𝑆)}))
69	67, 68	syl 17	. . . 4 ⊢ (𝜑 → (0..^((♯‘𝑆) + 1)) = ((0..^(♯‘𝑆)) ∪ {(♯‘𝑆)}))
70	65, 69	eqtrd 2772	. . 3 ⊢ (𝜑 → (0..^(♯‘𝑇)) = ((0..^(♯‘𝑆)) ∪ {(♯‘𝑆)}))
71		eqid 2737	. . 3 ⊢ (Cntz‘𝐺) = (Cntz‘𝐺)
72		eqid 2737	. . 3 ⊢ (0_g‘𝐺) = (0_g‘𝐺)
73		pgpfac.4	. . . 4 ⊢ (𝜑 → 𝐺dom DProd 𝑆)
74		cats1un 14672	. . . . . . . 8 ⊢ ((𝑆 ∈ Word 𝐶 ∧ (𝐾‘{𝑋}) ∈ 𝐶) → (𝑆 ++ ⟨“(𝐾‘{𝑋})”⟩) = (𝑆 ∪ {⟨(♯‘𝑆), (𝐾‘{𝑋})⟩}))
75	2, 42, 74	syl2anc 585	. . . . . . 7 ⊢ (𝜑 → (𝑆 ++ ⟨“(𝐾‘{𝑋})”⟩) = (𝑆 ∪ {⟨(♯‘𝑆), (𝐾‘{𝑋})⟩}))
76	1, 75	eqtrid 2784	. . . . . 6 ⊢ (𝜑 → 𝑇 = (𝑆 ∪ {⟨(♯‘𝑆), (𝐾‘{𝑋})⟩}))
77	76	reseq1d 5935	. . . . 5 ⊢ (𝜑 → (𝑇 ↾ (0..^(♯‘𝑆))) = ((𝑆 ∪ {⟨(♯‘𝑆), (𝐾‘{𝑋})⟩}) ↾ (0..^(♯‘𝑆))))
78		wrdfn 14479	. . . . . . 7 ⊢ (𝑆 ∈ Word 𝐶 → 𝑆 Fn (0..^(♯‘𝑆)))
79	2, 78	syl 17	. . . . . 6 ⊢ (𝜑 → 𝑆 Fn (0..^(♯‘𝑆)))
80		fzonel 13617	. . . . . 6 ⊢ ¬ (♯‘𝑆) ∈ (0..^(♯‘𝑆))
81		fsnunres 7134	. . . . . 6 ⊢ ((𝑆 Fn (0..^(♯‘𝑆)) ∧ ¬ (♯‘𝑆) ∈ (0..^(♯‘𝑆))) → ((𝑆 ∪ {⟨(♯‘𝑆), (𝐾‘{𝑋})⟩}) ↾ (0..^(♯‘𝑆))) = 𝑆)
82	79, 80, 81	sylancl 587	. . . . 5 ⊢ (𝜑 → ((𝑆 ∪ {⟨(♯‘𝑆), (𝐾‘{𝑋})⟩}) ↾ (0..^(♯‘𝑆))) = 𝑆)
83	77, 82	eqtrd 2772	. . . 4 ⊢ (𝜑 → (𝑇 ↾ (0..^(♯‘𝑆))) = 𝑆)
84	73, 83	breqtrrd 5114	. . 3 ⊢ (𝜑 → 𝐺dom DProd (𝑇 ↾ (0..^(♯‘𝑆))))
85		fvex 6845	. . . . . 6 ⊢ (♯‘𝑆) ∈ V
86		dprdsn 20002	. . . . . 6 ⊢ (((♯‘𝑆) ∈ V ∧ (𝐾‘{𝑋}) ∈ (SubGrp‘𝐺)) → (𝐺dom DProd {⟨(♯‘𝑆), (𝐾‘{𝑋})⟩} ∧ (𝐺 DProd {⟨(♯‘𝑆), (𝐾‘{𝑋})⟩}) = (𝐾‘{𝑋})))
87	85, 21, 86	sylancr 588	. . . . 5 ⊢ (𝜑 → (𝐺dom DProd {⟨(♯‘𝑆), (𝐾‘{𝑋})⟩} ∧ (𝐺 DProd {⟨(♯‘𝑆), (𝐾‘{𝑋})⟩}) = (𝐾‘{𝑋})))
88	87	simpld 494	. . . 4 ⊢ (𝜑 → 𝐺dom DProd {⟨(♯‘𝑆), (𝐾‘{𝑋})⟩})
89		wrdfn 14479	. . . . . . 7 ⊢ (𝑇 ∈ Word 𝐶 → 𝑇 Fn (0..^(♯‘𝑇)))
90	43, 89	syl 17	. . . . . 6 ⊢ (𝜑 → 𝑇 Fn (0..^(♯‘𝑇)))
91		ssun2 4120	. . . . . . . 8 ⊢ {(♯‘𝑆)} ⊆ ((0..^(♯‘𝑆)) ∪ {(♯‘𝑆)})
92	85	snss 4729	. . . . . . . 8 ⊢ ((♯‘𝑆) ∈ ((0..^(♯‘𝑆)) ∪ {(♯‘𝑆)}) ↔ {(♯‘𝑆)} ⊆ ((0..^(♯‘𝑆)) ∪ {(♯‘𝑆)}))
93	91, 92	mpbir 231	. . . . . . 7 ⊢ (♯‘𝑆) ∈ ((0..^(♯‘𝑆)) ∪ {(♯‘𝑆)})
94	93, 70	eleqtrrid 2844	. . . . . 6 ⊢ (𝜑 → (♯‘𝑆) ∈ (0..^(♯‘𝑇)))
95		fnressn 7103	. . . . . 6 ⊢ ((𝑇 Fn (0..^(♯‘𝑇)) ∧ (♯‘𝑆) ∈ (0..^(♯‘𝑇))) → (𝑇 ↾ {(♯‘𝑆)}) = {⟨(♯‘𝑆), (𝑇‘(♯‘𝑆))⟩})
96	90, 94, 95	syl2anc 585	. . . . 5 ⊢ (𝜑 → (𝑇 ↾ {(♯‘𝑆)}) = {⟨(♯‘𝑆), (𝑇‘(♯‘𝑆))⟩})
97	1	fveq1i 6833	. . . . . . . . 9 ⊢ (𝑇‘(♯‘𝑆)) = ((𝑆 ++ ⟨“(𝐾‘{𝑋})”⟩)‘(♯‘𝑆))
98	50	nn0cnd 12489	. . . . . . . . . . 11 ⊢ (𝜑 → (♯‘𝑆) ∈ ℂ)
99	98	addlidd 11336	. . . . . . . . . 10 ⊢ (𝜑 → (0 + (♯‘𝑆)) = (♯‘𝑆))
100	99	fveq2d 6836	. . . . . . . . 9 ⊢ (𝜑 → ((𝑆 ++ ⟨“(𝐾‘{𝑋})”⟩)‘(0 + (♯‘𝑆))) = ((𝑆 ++ ⟨“(𝐾‘{𝑋})”⟩)‘(♯‘𝑆)))
101	97, 100	eqtr4id 2791	. . . . . . . 8 ⊢ (𝜑 → (𝑇‘(♯‘𝑆)) = ((𝑆 ++ ⟨“(𝐾‘{𝑋})”⟩)‘(0 + (♯‘𝑆))))
102		1nn 12174	. . . . . . . . . . . 12 ⊢ 1 ∈ ℕ
103	62, 102	eqeltri 2833	. . . . . . . . . . 11 ⊢ (♯‘⟨“(𝐾‘{𝑋})”⟩) ∈ ℕ
104		lbfzo0 13643	. . . . . . . . . . 11 ⊢ (0 ∈ (0..^(♯‘⟨“(𝐾‘{𝑋})”⟩)) ↔ (♯‘⟨“(𝐾‘{𝑋})”⟩) ∈ ℕ)
105	103, 104	mpbir 231	. . . . . . . . . 10 ⊢ 0 ∈ (0..^(♯‘⟨“(𝐾‘{𝑋})”⟩))
106	105	a1i 11	. . . . . . . . 9 ⊢ (𝜑 → 0 ∈ (0..^(♯‘⟨“(𝐾‘{𝑋})”⟩)))
107		ccatval3 14530	. . . . . . . . 9 ⊢ ((𝑆 ∈ Word 𝐶 ∧ ⟨“(𝐾‘{𝑋})”⟩ ∈ Word 𝐶 ∧ 0 ∈ (0..^(♯‘⟨“(𝐾‘{𝑋})”⟩))) → ((𝑆 ++ ⟨“(𝐾‘{𝑋})”⟩)‘(0 + (♯‘𝑆))) = (⟨“(𝐾‘{𝑋})”⟩‘0))
108	2, 58, 106, 107	syl3anc 1374	. . . . . . . 8 ⊢ (𝜑 → ((𝑆 ++ ⟨“(𝐾‘{𝑋})”⟩)‘(0 + (♯‘𝑆))) = (⟨“(𝐾‘{𝑋})”⟩‘0))
109		fvex 6845	. . . . . . . . 9 ⊢ (𝐾‘{𝑋}) ∈ V
110		s1fv 14562	. . . . . . . . 9 ⊢ ((𝐾‘{𝑋}) ∈ V → (⟨“(𝐾‘{𝑋})”⟩‘0) = (𝐾‘{𝑋}))
111	109, 110	mp1i 13	. . . . . . . 8 ⊢ (𝜑 → (⟨“(𝐾‘{𝑋})”⟩‘0) = (𝐾‘{𝑋}))
112	101, 108, 111	3eqtrd 2776	. . . . . . 7 ⊢ (𝜑 → (𝑇‘(♯‘𝑆)) = (𝐾‘{𝑋}))
113	112	opeq2d 4824	. . . . . 6 ⊢ (𝜑 → ⟨(♯‘𝑆), (𝑇‘(♯‘𝑆))⟩ = ⟨(♯‘𝑆), (𝐾‘{𝑋})⟩)
114	113	sneqd 4580	. . . . 5 ⊢ (𝜑 → {⟨(♯‘𝑆), (𝑇‘(♯‘𝑆))⟩} = {⟨(♯‘𝑆), (𝐾‘{𝑋})⟩})
115	96, 114	eqtrd 2772	. . . 4 ⊢ (𝜑 → (𝑇 ↾ {(♯‘𝑆)}) = {⟨(♯‘𝑆), (𝐾‘{𝑋})⟩})
116	88, 115	breqtrrd 5114	. . 3 ⊢ (𝜑 → 𝐺dom DProd (𝑇 ↾ {(♯‘𝑆)}))
117		pgpfac.g	. . . 4 ⊢ (𝜑 → 𝐺 ∈ Abel)
118		dprdsubg 19990	. . . . 5 ⊢ (𝐺dom DProd (𝑇 ↾ (0..^(♯‘𝑆))) → (𝐺 DProd (𝑇 ↾ (0..^(♯‘𝑆)))) ∈ (SubGrp‘𝐺))
119	84, 118	syl 17	. . . 4 ⊢ (𝜑 → (𝐺 DProd (𝑇 ↾ (0..^(♯‘𝑆)))) ∈ (SubGrp‘𝐺))
120		dprdsubg 19990	. . . . 5 ⊢ (𝐺dom DProd (𝑇 ↾ {(♯‘𝑆)}) → (𝐺 DProd (𝑇 ↾ {(♯‘𝑆)})) ∈ (SubGrp‘𝐺))
121	116, 120	syl 17	. . . 4 ⊢ (𝜑 → (𝐺 DProd (𝑇 ↾ {(♯‘𝑆)})) ∈ (SubGrp‘𝐺))
122	71, 117, 119, 121	ablcntzd 19821	. . 3 ⊢ (𝜑 → (𝐺 DProd (𝑇 ↾ (0..^(♯‘𝑆)))) ⊆ ((Cntz‘𝐺)‘(𝐺 DProd (𝑇 ↾ {(♯‘𝑆)}))))
123		pgpfac.i	. . . 4 ⊢ (𝜑 → ((𝐾‘{𝑋}) ∩ 𝑊) = { 0 })
124	83	oveq2d 7374	. . . . . . 7 ⊢ (𝜑 → (𝐺 DProd (𝑇 ↾ (0..^(♯‘𝑆)))) = (𝐺 DProd 𝑆))
125		pgpfac.5	. . . . . . 7 ⊢ (𝜑 → (𝐺 DProd 𝑆) = 𝑊)
126	124, 125	eqtrd 2772	. . . . . 6 ⊢ (𝜑 → (𝐺 DProd (𝑇 ↾ (0..^(♯‘𝑆)))) = 𝑊)
127	115	oveq2d 7374	. . . . . . 7 ⊢ (𝜑 → (𝐺 DProd (𝑇 ↾ {(♯‘𝑆)})) = (𝐺 DProd {⟨(♯‘𝑆), (𝐾‘{𝑋})⟩}))
128	87	simprd 495	. . . . . . 7 ⊢ (𝜑 → (𝐺 DProd {⟨(♯‘𝑆), (𝐾‘{𝑋})⟩}) = (𝐾‘{𝑋}))
129	127, 128	eqtrd 2772	. . . . . 6 ⊢ (𝜑 → (𝐺 DProd (𝑇 ↾ {(♯‘𝑆)})) = (𝐾‘{𝑋}))
130	126, 129	ineq12d 4162	. . . . 5 ⊢ (𝜑 → ((𝐺 DProd (𝑇 ↾ (0..^(♯‘𝑆)))) ∩ (𝐺 DProd (𝑇 ↾ {(♯‘𝑆)}))) = (𝑊 ∩ (𝐾‘{𝑋})))
131		incom 4150	. . . . 5 ⊢ (𝑊 ∩ (𝐾‘{𝑋})) = ((𝐾‘{𝑋}) ∩ 𝑊)
132	130, 131	eqtrdi 2788	. . . 4 ⊢ (𝜑 → ((𝐺 DProd (𝑇 ↾ (0..^(♯‘𝑆)))) ∩ (𝐺 DProd (𝑇 ↾ {(♯‘𝑆)}))) = ((𝐾‘{𝑋}) ∩ 𝑊))
133	4, 72	subg0 19097	. . . . . . 7 ⊢ (𝑈 ∈ (SubGrp‘𝐺) → (0_g‘𝐺) = (0_g‘𝐻))
134	3, 133	syl 17	. . . . . 6 ⊢ (𝜑 → (0_g‘𝐺) = (0_g‘𝐻))
135		pgpfac.0	. . . . . 6 ⊢ 0 = (0_g‘𝐻)
136	134, 135	eqtr4di 2790	. . . . 5 ⊢ (𝜑 → (0_g‘𝐺) = 0 )
137	136	sneqd 4580	. . . 4 ⊢ (𝜑 → {(0_g‘𝐺)} = { 0 })
138	123, 132, 137	3eqtr4d 2782	. . 3 ⊢ (𝜑 → ((𝐺 DProd (𝑇 ↾ (0..^(♯‘𝑆)))) ∩ (𝐺 DProd (𝑇 ↾ {(♯‘𝑆)}))) = {(0_g‘𝐺)})
139	48, 56, 70, 71, 72, 84, 116, 122, 138	dmdprdsplit2 20012	. 2 ⊢ (𝜑 → 𝐺dom DProd 𝑇)
140		eqid 2737	. . . . 5 ⊢ (LSSum‘𝐺) = (LSSum‘𝐺)
141	48, 56, 70, 140, 139	dprdsplit 20014	. . . 4 ⊢ (𝜑 → (𝐺 DProd 𝑇) = ((𝐺 DProd (𝑇 ↾ (0..^(♯‘𝑆))))(LSSum‘𝐺)(𝐺 DProd (𝑇 ↾ {(♯‘𝑆)}))))
142	126, 129	oveq12d 7376	. . . 4 ⊢ (𝜑 → ((𝐺 DProd (𝑇 ↾ (0..^(♯‘𝑆))))(LSSum‘𝐺)(𝐺 DProd (𝑇 ↾ {(♯‘𝑆)}))) = (𝑊(LSSum‘𝐺)(𝐾‘{𝑋})))
143	126, 119	eqeltrrd 2838	. . . . 5 ⊢ (𝜑 → 𝑊 ∈ (SubGrp‘𝐺))
144	140	lsmcom 19822	. . . . 5 ⊢ ((𝐺 ∈ Abel ∧ 𝑊 ∈ (SubGrp‘𝐺) ∧ (𝐾‘{𝑋}) ∈ (SubGrp‘𝐺)) → (𝑊(LSSum‘𝐺)(𝐾‘{𝑋})) = ((𝐾‘{𝑋})(LSSum‘𝐺)𝑊))
145	117, 143, 21, 144	syl3anc 1374	. . . 4 ⊢ (𝜑 → (𝑊(LSSum‘𝐺)(𝐾‘{𝑋})) = ((𝐾‘{𝑋})(LSSum‘𝐺)𝑊))
146	141, 142, 145	3eqtrd 2776	. . 3 ⊢ (𝜑 → (𝐺 DProd 𝑇) = ((𝐾‘{𝑋})(LSSum‘𝐺)𝑊))
147		pgpfac.w	. . . . . 6 ⊢ (𝜑 → 𝑊 ∈ (SubGrp‘𝐻))
148	7	subgss 19092	. . . . . 6 ⊢ (𝑊 ∈ (SubGrp‘𝐻) → 𝑊 ⊆ (Base‘𝐻))
149	147, 148	syl 17	. . . . 5 ⊢ (𝜑 → 𝑊 ⊆ (Base‘𝐻))
150	149, 13	sseqtrrd 3960	. . . 4 ⊢ (𝜑 → 𝑊 ⊆ 𝑈)
151		pgpfac.l	. . . . 5 ⊢ ⊕ = (LSSum‘𝐻)
152	4, 140, 151	subglsm 19637	. . . 4 ⊢ ((𝑈 ∈ (SubGrp‘𝐺) ∧ (𝐾‘{𝑋}) ⊆ 𝑈 ∧ 𝑊 ⊆ 𝑈) → ((𝐾‘{𝑋})(LSSum‘𝐺)𝑊) = ((𝐾‘{𝑋}) ⊕ 𝑊))
153	3, 23, 150, 152	syl3anc 1374	. . 3 ⊢ (𝜑 → ((𝐾‘{𝑋})(LSSum‘𝐺)𝑊) = ((𝐾‘{𝑋}) ⊕ 𝑊))
154		pgpfac.s	. . 3 ⊢ (𝜑 → ((𝐾‘{𝑋}) ⊕ 𝑊) = 𝑈)
155	146, 153, 154	3eqtrd 2776	. 2 ⊢ (𝜑 → (𝐺 DProd 𝑇) = 𝑈)
156		breq2 5090	. . . 4 ⊢ (𝑠 = 𝑇 → (𝐺dom DProd 𝑠 ↔ 𝐺dom DProd 𝑇))
157		oveq2 7366	. . . . 5 ⊢ (𝑠 = 𝑇 → (𝐺 DProd 𝑠) = (𝐺 DProd 𝑇))
158	157	eqeq1d 2739	. . . 4 ⊢ (𝑠 = 𝑇 → ((𝐺 DProd 𝑠) = 𝑈 ↔ (𝐺 DProd 𝑇) = 𝑈))
159	156, 158	anbi12d 633	. . 3 ⊢ (𝑠 = 𝑇 → ((𝐺dom DProd 𝑠 ∧ (𝐺 DProd 𝑠) = 𝑈) ↔ (𝐺dom DProd 𝑇 ∧ (𝐺 DProd 𝑇) = 𝑈)))
160	159	rspcev 3565	. 2 ⊢ ((𝑇 ∈ Word 𝐶 ∧ (𝐺dom DProd 𝑇 ∧ (𝐺 DProd 𝑇) = 𝑈)) → ∃𝑠 ∈ Word 𝐶(𝐺dom DProd 𝑠 ∧ (𝐺 DProd 𝑠) = 𝑈))
161	43, 139, 155, 160	syl12anc 837	1 ⊢ (𝜑 → ∃𝑠 ∈ Word 𝐶(𝐺dom DProd 𝑠 ∧ (𝐺 DProd 𝑠) = 𝑈))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 206 ∧ wa 395 = wceq 1542 ∈ wcel 2114 ≠ wne 2933 ∀wral 3052 ∃wrex 3062 {crab 3390 Vcvv 3430 ∪ cun 3888 ∩ cin 3889 ⊆ wss 3890 ⊊ wpss 3891 ∅c0 4274 {csn 4568 ⟨cop 4574 class class class wbr 5086 dom cdm 5622 ran crn 5623 ↾ cres 5624 Fn wfn 6485 ⟶wf 6486 ‘cfv 6490 (class class class)co 7358 Fincfn 8884 0cc0 11027 1c1 11028 + caddc 11030 ℕcn 12163 ℕ₀cn0 12426 ℤcz 12513 ℤ_≥cuz 12777 ..^cfzo 13597 ♯chash 14281 Word cword 14464 ++ cconcat 14521 ⟨“cs1 14547 ℙcprime 16629 Basecbs 17168 ↾_s cress 17189 0_gc0g 17391 Moorecmre 17533 mrClscmrc 17534 ACScacs 17536 Grpcgrp 18898 SubGrpcsubg 19085 Cntzccntz 19279 odcod 19488 gExcgex 19489 pGrp cpgp 19490 LSSumclsm 19598 Abelcabl 19745 CycGrpccyg 19841 DProd cdprd 19959

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1912 ax-6 1969 ax-7 2010 ax-8 2116 ax-9 2124 ax-10 2147 ax-11 2163 ax-12 2185 ax-ext 2709 ax-rep 5212 ax-sep 5231 ax-nul 5241 ax-pow 5300 ax-pr 5368 ax-un 7680 ax-cnex 11083 ax-resscn 11084 ax-1cn 11085 ax-icn 11086 ax-addcl 11087 ax-addrcl 11088 ax-mulcl 11089 ax-mulrcl 11090 ax-mulcom 11091 ax-addass 11092 ax-mulass 11093 ax-distr 11094 ax-i2m1 11095 ax-1ne0 11096 ax-1rid 11097 ax-rnegex 11098 ax-rrecex 11099 ax-cnre 11100 ax-pre-lttri 11101 ax-pre-lttrn 11102 ax-pre-ltadd 11103 ax-pre-mulgt0 11104

This theorem depends on definitions: df-bi 207 df-an 396 df-or 849 df-3or 1088 df-3an 1089 df-tru 1545 df-fal 1555 df-ex 1782 df-nf 1786 df-sb 2069 df-mo 2540 df-eu 2570 df-clab 2716 df-cleq 2729 df-clel 2812 df-nfc 2886 df-ne 2934 df-nel 3038 df-ral 3053 df-rex 3063 df-rmo 3343 df-reu 3344 df-rab 3391 df-v 3432 df-sbc 3730 df-csb 3839 df-dif 3893 df-un 3895 df-in 3897 df-ss 3907 df-pss 3910 df-nul 4275 df-if 4468 df-pw 4544 df-sn 4569 df-pr 4571 df-op 4575 df-uni 4852 df-int 4891 df-iun 4936 df-iin 4937 df-br 5087 df-opab 5149 df-mpt 5168 df-tr 5194 df-id 5517 df-eprel 5522 df-po 5530 df-so 5531 df-fr 5575 df-se 5576 df-we 5577 df-xp 5628 df-rel 5629 df-cnv 5630 df-co 5631 df-dm 5632 df-rn 5633 df-res 5634 df-ima 5635 df-pred 6257 df-ord 6318 df-on 6319 df-lim 6320 df-suc 6321 df-iota 6446 df-fun 6492 df-fn 6493 df-f 6494 df-f1 6495 df-fo 6496 df-f1o 6497 df-fv 6498 df-isom 6499 df-riota 7315 df-ov 7361 df-oprab 7362 df-mpo 7363 df-of 7622 df-om 7809 df-1st 7933 df-2nd 7934 df-supp 8102 df-tpos 8167 df-frecs 8222 df-wrecs 8253 df-recs 8302 df-rdg 8340 df-1o 8396 df-2o 8397 df-er 8634 df-map 8766 df-ixp 8837 df-en 8885 df-dom 8886 df-sdom 8887 df-fin 8888 df-fsupp 9266 df-sup 9346 df-inf 9347 df-oi 9416 df-card 9852 df-pnf 11170 df-mnf 11171 df-xr 11172 df-ltxr 11173 df-le 11174 df-sub 11368 df-neg 11369 df-nn 12164 df-2 12233 df-n0 12427 df-z 12514 df-uz 12778 df-fz 13451 df-fzo 13598 df-seq 13953 df-hash 14282 df-word 14465 df-concat 14522 df-s1 14548 df-sets 17123 df-slot 17141 df-ndx 17153 df-base 17169 df-ress 17190 df-plusg 17222 df-0g 17393 df-gsum 17394 df-mre 17537 df-mrc 17538 df-acs 17540 df-mgm 18597 df-sgrp 18676 df-mnd 18692 df-mhm 18740 df-submnd 18741 df-grp 18901 df-minusg 18902 df-sbg 18903 df-mulg 19033 df-subg 19088 df-ghm 19177 df-gim 19223 df-cntz 19281 df-oppg 19310 df-od 19492 df-pgp 19494 df-lsm 19600 df-cmn 19746 df-abl 19747 df-cyg 19842 df-dprd 19961

This theorem is referenced by: pgpfaclem2 20048

W3C validator