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 20159

Description: Lemma for pgpfac 20162. (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 19201	. . . . . . . . . 10 ⊢ (𝑈 ∈ (SubGrp‘𝐺) → 𝐻 ∈ Grp)
6	3, 5	syl 18	. . . . . . . . 9 ⊢ (𝜑 → 𝐻 ∈ Grp)
7		eqid 2762	. . . . . . . . . 10 ⊢ (Base‘𝐻) = (Base‘𝐻)
8	7	subgacs 19233	. . . . . . . . 9 ⊢ (𝐻 ∈ Grp → (SubGrp‘𝐻) ∈ (ACS‘(Base‘𝐻)))
9	6, 8	syl 18	. . . . . . . 8 ⊢ (𝜑 → (SubGrp‘𝐻) ∈ (ACS‘(Base‘𝐻)))
10	9	acsmred 17718	. . . . . . 7 ⊢ (𝜑 → (SubGrp‘𝐻) ∈ (Moore‘(Base‘𝐻)))
11		pgpfac.x	. . . . . . . 8 ⊢ (𝜑 → 𝑋 ∈ 𝑈)
12	4	subgbas 19202	. . . . . . . . 9 ⊢ (𝑈 ∈ (SubGrp‘𝐺) → 𝑈 = (Base‘𝐻))
13	3, 12	syl 18	. . . . . . . 8 ⊢ (𝜑 → 𝑈 = (Base‘𝐻))
14	11, 13	eleqtrd 2864	. . . . . . 7 ⊢ (𝜑 → 𝑋 ∈ (Base‘𝐻))
15		pgpfac.k	. . . . . . . 8 ⊢ 𝐾 = (mrCls‘(SubGrp‘𝐻))
16	15	mrcsncl 17674	. . . . . . 7 ⊢ (((SubGrp‘𝐻) ∈ (Moore‘(Base‘𝐻)) ∧ 𝑋 ∈ (Base‘𝐻)) → (𝐾‘{𝑋}) ∈ (SubGrp‘𝐻))
17	10, 14, 16	syl2anc 595	. . . . . 6 ⊢ (𝜑 → (𝐾‘{𝑋}) ∈ (SubGrp‘𝐻))
18	4	subsubg 19222	. . . . . . 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 7422	. . . . . . 7 ⊢ (𝐻 ↾_s (𝐾‘{𝑋})) = ((𝐺 ↾_s 𝑈) ↾_s (𝐾‘{𝑋}))
23	20	simprd 500	. . . . . . . 8 ⊢ (𝜑 → (𝐾‘{𝑋}) ⊆ 𝑈)
24		ressabs 17314	. . . . . . . 8 ⊢ ((𝑈 ∈ (SubGrp‘𝐺) ∧ (𝐾‘{𝑋}) ⊆ 𝑈) → ((𝐺 ↾_s 𝑈) ↾_s (𝐾‘{𝑋})) = (𝐺 ↾_s (𝐾‘{𝑋})))
25	3, 23, 24	syl2anc 595	. . . . . . 7 ⊢ (𝜑 → ((𝐺 ↾_s 𝑈) ↾_s (𝐾‘{𝑋})) = (𝐺 ↾_s (𝐾‘{𝑋})))
26	22, 25	eqtrid 2809	. . . . . 6 ⊢ (𝜑 → (𝐻 ↾_s (𝐾‘{𝑋})) = (𝐺 ↾_s (𝐾‘{𝑋})))
27	7, 15	cycsubgcyg2 19978	. . . . . . 7 ⊢ ((𝐻 ∈ Grp ∧ 𝑋 ∈ (Base‘𝐻)) → (𝐻 ↾_s (𝐾‘{𝑋})) ∈ CycGrp)
28	6, 14, 27	syl2anc 595	. . . . . 6 ⊢ (𝜑 → (𝐻 ↾_s (𝐾‘{𝑋})) ∈ CycGrp)
29	26, 28	eqeltrrd 2863	. . . . 5 ⊢ (𝜑 → (𝐺 ↾_s (𝐾‘{𝑋})) ∈ CycGrp)
30		pgpfac.p	. . . . . . 7 ⊢ (𝜑 → 𝑃 pGrp 𝐺)
31		pgpprm 19669	. . . . . . 7 ⊢ (𝑃 pGrp 𝐺 → 𝑃 ∈ ℙ)
32	30, 31	syl 18	. . . . . 6 ⊢ (𝜑 → 𝑃 ∈ ℙ)
33		subgpgp 19673	. . . . . . 7 ⊢ ((𝑃 pGrp 𝐺 ∧ (𝐾‘{𝑋}) ∈ (SubGrp‘𝐺)) → 𝑃 pGrp (𝐺 ↾_s (𝐾‘{𝑋})))
34	30, 21, 33	syl2anc 595	. . . . . 6 ⊢ (𝜑 → 𝑃 pGrp (𝐺 ↾_s (𝐾‘{𝑋})))
35		brelrng 5930	. . . . . 6 ⊢ ((𝑃 ∈ ℙ ∧ (𝐺 ↾_s (𝐾‘{𝑋})) ∈ CycGrp ∧ 𝑃 pGrp (𝐺 ↾_s (𝐾‘{𝑋}))) → (𝐺 ↾_s (𝐾‘{𝑋})) ∈ ran pGrp )
36	32, 29, 34, 35	syl3anc 1397	. . . . 5 ⊢ (𝜑 → (𝐺 ↾_s (𝐾‘{𝑋})) ∈ ran pGrp )
37	29, 36	elind 4152	. . . 4 ⊢ (𝜑 → (𝐺 ↾_s (𝐾‘{𝑋})) ∈ (CycGrp ∩ ran pGrp ))
38		oveq2 7420	. . . . . 6 ⊢ (𝑟 = (𝐾‘{𝑋}) → (𝐺 ↾_s 𝑟) = (𝐺 ↾_s (𝐾‘{𝑋})))
39	38	eleq1d 2847	. . . . 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 14899	. 2 ⊢ (𝜑 → 𝑇 ∈ Word 𝐶)
44		wrdf 14562	. . . . 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 14577	. . . . . . . 8 ⊢ (𝑆 ∈ Word 𝐶 → (♯‘𝑆) ∈ ℕ₀)
50	2, 49	syl 18	. . . . . . 7 ⊢ (𝜑 → (♯‘𝑆) ∈ ℕ₀)
51	50	nn0zd 12622	. . . . . 6 ⊢ (𝜑 → (♯‘𝑆) ∈ ℤ)
52		fzosn 13772	. . . . . 6 ⊢ ((♯‘𝑆) ∈ ℤ → ((♯‘𝑆)..^((♯‘𝑆) + 1)) = {(♯‘𝑆)})
53	51, 52	syl 18	. . . . 5 ⊢ (𝜑 → ((♯‘𝑆)..^((♯‘𝑆) + 1)) = {(♯‘𝑆)})
54	53	ineq2d 4172	. . . 4 ⊢ (𝜑 → ((0..^(♯‘𝑆)) ∩ ((♯‘𝑆)..^((♯‘𝑆) + 1))) = ((0..^(♯‘𝑆)) ∩ {(♯‘𝑆)}))
55		fzodisj 13729	. . . 4 ⊢ ((0..^(♯‘𝑆)) ∩ ((♯‘𝑆)..^((♯‘𝑆) + 1))) = ∅
56	54, 55	eqtr3di 2812	. . 3 ⊢ (𝜑 → ((0..^(♯‘𝑆)) ∩ {(♯‘𝑆)}) = ∅)
57	1	fveq2i 6884	. . . . . . 7 ⊢ (♯‘𝑇) = (♯‘(𝑆 ++ ⟨“(𝐾‘{𝑋})”⟩))
58	42	s1cld 14648	. . . . . . . 8 ⊢ (𝜑 → ⟨“(𝐾‘{𝑋})”⟩ ∈ Word 𝐶)
59		ccatlen 14619	. . . . . . . 8 ⊢ ((𝑆 ∈ Word 𝐶 ∧ ⟨“(𝐾‘{𝑋})”⟩ ∈ Word 𝐶) → (♯‘(𝑆 ++ ⟨“(𝐾‘{𝑋})”⟩)) = ((♯‘𝑆) + (♯‘⟨“(𝐾‘{𝑋})”⟩)))
60	2, 58, 59	syl2anc 595	. . . . . . 7 ⊢ (𝜑 → (♯‘(𝑆 ++ ⟨“(𝐾‘{𝑋})”⟩)) = ((♯‘𝑆) + (♯‘⟨“(𝐾‘{𝑋})”⟩)))
61	57, 60	eqtrid 2809	. . . . . 6 ⊢ (𝜑 → (♯‘𝑇) = ((♯‘𝑆) + (♯‘⟨“(𝐾‘{𝑋})”⟩)))
62		s1len 14651	. . . . . . 7 ⊢ (♯‘⟨“(𝐾‘{𝑋})”⟩) = 1
63	62	oveq2i 7423	. . . . . 6 ⊢ ((♯‘𝑆) + (♯‘⟨“(𝐾‘{𝑋})”⟩)) = ((♯‘𝑆) + 1)
64	61, 63	eqtrdi 2813	. . . . 5 ⊢ (𝜑 → (♯‘𝑇) = ((♯‘𝑆) + 1))
65	64	oveq2d 7428	. . . 4 ⊢ (𝜑 → (0..^(♯‘𝑇)) = (0..^((♯‘𝑆) + 1)))
66		nn0uz 12906	. . . . . 6 ⊢ ℕ₀ = (ℤ_≥‘0)
67	50, 66	eleqtrdi 2872	. . . . 5 ⊢ (𝜑 → (♯‘𝑆) ∈ (ℤ_≥‘0))
68		fzosplitsn 13812	. . . . 5 ⊢ ((♯‘𝑆) ∈ (ℤ_≥‘0) → (0..^((♯‘𝑆) + 1)) = ((0..^(♯‘𝑆)) ∪ {(♯‘𝑆)}))
69	67, 68	syl 18	. . . 4 ⊢ (𝜑 → (0..^((♯‘𝑆) + 1)) = ((0..^(♯‘𝑆)) ∪ {(♯‘𝑆)}))
70	65, 69	eqtrd 2797	. . 3 ⊢ (𝜑 → (0..^(♯‘𝑇)) = ((0..^(♯‘𝑆)) ∪ {(♯‘𝑆)}))
71		eqid 2762	. . 3 ⊢ (Cntz‘𝐺) = (Cntz‘𝐺)
72		eqid 2762	. . 3 ⊢ (0_g‘𝐺) = (0_g‘𝐺)
73		pgpfac.4	. . . 4 ⊢ (𝜑 → 𝐺dom DProd 𝑆)
74		cats1un 14765	. . . . . . . 8 ⊢ ((𝑆 ∈ Word 𝐶 ∧ (𝐾‘{𝑋}) ∈ 𝐶) → (𝑆 ++ ⟨“(𝐾‘{𝑋})”⟩) = (𝑆 ∪ {⟨(♯‘𝑆), (𝐾‘{𝑋})⟩}))
75	2, 42, 74	syl2anc 595	. . . . . . 7 ⊢ (𝜑 → (𝑆 ++ ⟨“(𝐾‘{𝑋})”⟩) = (𝑆 ∪ {⟨(♯‘𝑆), (𝐾‘{𝑋})⟩}))
76	1, 75	eqtrid 2809	. . . . . 6 ⊢ (𝜑 → 𝑇 = (𝑆 ∪ {⟨(♯‘𝑆), (𝐾‘{𝑋})⟩}))
77	76	reseq1d 5976	. . . . 5 ⊢ (𝜑 → (𝑇 ↾ (0..^(♯‘𝑆))) = ((𝑆 ∪ {⟨(♯‘𝑆), (𝐾‘{𝑋})⟩}) ↾ (0..^(♯‘𝑆))))
78		wrdfn 14572	. . . . . . 7 ⊢ (𝑆 ∈ Word 𝐶 → 𝑆 Fn (0..^(♯‘𝑆)))
79	2, 78	syl 18	. . . . . 6 ⊢ (𝜑 → 𝑆 Fn (0..^(♯‘𝑆)))
80		fzonel 13709	. . . . . 6 ⊢ ¬ (♯‘𝑆) ∈ (0..^(♯‘𝑆))
81		fsnunres 7186	. . . . . 6 ⊢ ((𝑆 Fn (0..^(♯‘𝑆)) ∧ ¬ (♯‘𝑆) ∈ (0..^(♯‘𝑆))) → ((𝑆 ∪ {⟨(♯‘𝑆), (𝐾‘{𝑋})⟩}) ↾ (0..^(♯‘𝑆))) = 𝑆)
82	79, 80, 81	sylancl 597	. . . . 5 ⊢ (𝜑 → ((𝑆 ∪ {⟨(♯‘𝑆), (𝐾‘{𝑋})⟩}) ↾ (0..^(♯‘𝑆))) = 𝑆)
83	77, 82	eqtrd 2797	. . . 4 ⊢ (𝜑 → (𝑇 ↾ (0..^(♯‘𝑆))) = 𝑆)
84	73, 83	breqtrrd 5138	. . 3 ⊢ (𝜑 → 𝐺dom DProd (𝑇 ↾ (0..^(♯‘𝑆))))
85		fvex 6894	. . . . . 6 ⊢ (♯‘𝑆) ∈ V
86		dprdsn 20114	. . . . . 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 14572	. . . . . . 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 2869	. . . . . 6 ⊢ (𝜑 → (♯‘𝑆) ∈ (0..^(♯‘𝑇)))
95		fnressn 7155	. . . . . 6 ⊢ ((𝑇 Fn (0..^(♯‘𝑇)) ∧ (♯‘𝑆) ∈ (0..^(♯‘𝑇))) → (𝑇 ↾ {(♯‘𝑆)}) = {⟨(♯‘𝑆), (𝑇‘(♯‘𝑆))⟩})
96	90, 94, 95	syl2anc 595	. . . . 5 ⊢ (𝜑 → (𝑇 ↾ {(♯‘𝑆)}) = {⟨(♯‘𝑆), (𝑇‘(♯‘𝑆))⟩})
97	1	fveq1i 6882	. . . . . . . . 9 ⊢ (𝑇‘(♯‘𝑆)) = ((𝑆 ++ ⟨“(𝐾‘{𝑋})”⟩)‘(♯‘𝑆))
98	50	nn0cnd 12573	. . . . . . . . . . 11 ⊢ (𝜑 → (♯‘𝑆) ∈ ℂ)
99	98	addlidd 11417	. . . . . . . . . 10 ⊢ (𝜑 → (0 + (♯‘𝑆)) = (♯‘𝑆))
100	99	fveq2d 6885	. . . . . . . . 9 ⊢ (𝜑 → ((𝑆 ++ ⟨“(𝐾‘{𝑋})”⟩)‘(0 + (♯‘𝑆))) = ((𝑆 ++ ⟨“(𝐾‘{𝑋})”⟩)‘(♯‘𝑆)))
101	97, 100	eqtr4id 2816	. . . . . . . 8 ⊢ (𝜑 → (𝑇‘(♯‘𝑆)) = ((𝑆 ++ ⟨“(𝐾‘{𝑋})”⟩)‘(0 + (♯‘𝑆))))
102		1nn 12250	. . . . . . . . . . . 12 ⊢ 1 ∈ ℕ
103	62, 102	eqeltri 2858	. . . . . . . . . . 11 ⊢ (♯‘⟨“(𝐾‘{𝑋})”⟩) ∈ ℕ
104		lbfzo0 13735	. . . . . . . . . . 11 ⊢ (0 ∈ (0..^(♯‘⟨“(𝐾‘{𝑋})”⟩)) ↔ (♯‘⟨“(𝐾‘{𝑋})”⟩) ∈ ℕ)
105	103, 104	mpbir 234	. . . . . . . . . 10 ⊢ 0 ∈ (0..^(♯‘⟨“(𝐾‘{𝑋})”⟩))
106	105	a1i 11	. . . . . . . . 9 ⊢ (𝜑 → 0 ∈ (0..^(♯‘⟨“(𝐾‘{𝑋})”⟩)))
107		ccatval3 14623	. . . . . . . . 9 ⊢ ((𝑆 ∈ Word 𝐶 ∧ ⟨“(𝐾‘{𝑋})”⟩ ∈ Word 𝐶 ∧ 0 ∈ (0..^(♯‘⟨“(𝐾‘{𝑋})”⟩))) → ((𝑆 ++ ⟨“(𝐾‘{𝑋})”⟩)‘(0 + (♯‘𝑆))) = (⟨“(𝐾‘{𝑋})”⟩‘0))
108	2, 58, 106, 107	syl3anc 1397	. . . . . . . 8 ⊢ (𝜑 → ((𝑆 ++ ⟨“(𝐾‘{𝑋})”⟩)‘(0 + (♯‘𝑆))) = (⟨“(𝐾‘{𝑋})”⟩‘0))
109		fvex 6894	. . . . . . . . 9 ⊢ (𝐾‘{𝑋}) ∈ V
110		s1fv 14655	. . . . . . . . 9 ⊢ ((𝐾‘{𝑋}) ∈ V → (⟨“(𝐾‘{𝑋})”⟩‘0) = (𝐾‘{𝑋}))
111	109, 110	mp1i 14	. . . . . . . 8 ⊢ (𝜑 → (⟨“(𝐾‘{𝑋})”⟩‘0) = (𝐾‘{𝑋}))
112	101, 108, 111	3eqtrd 2801	. . . . . . 7 ⊢ (𝜑 → (𝑇‘(♯‘𝑆)) = (𝐾‘{𝑋}))
113	112	opeq2d 4844	. . . . . 6 ⊢ (𝜑 → ⟨(♯‘𝑆), (𝑇‘(♯‘𝑆))⟩ = ⟨(♯‘𝑆), (𝐾‘{𝑋})⟩)
114	113	sneqd 4600	. . . . 5 ⊢ (𝜑 → {⟨(♯‘𝑆), (𝑇‘(♯‘𝑆))⟩} = {⟨(♯‘𝑆), (𝐾‘{𝑋})⟩})
115	96, 114	eqtrd 2797	. . . 4 ⊢ (𝜑 → (𝑇 ↾ {(♯‘𝑆)}) = {⟨(♯‘𝑆), (𝐾‘{𝑋})⟩})
116	88, 115	breqtrrd 5138	. . 3 ⊢ (𝜑 → 𝐺dom DProd (𝑇 ↾ {(♯‘𝑆)}))
117		pgpfac.g	. . . 4 ⊢ (𝜑 → 𝐺 ∈ Abel)
118		dprdsubg 20102	. . . . 5 ⊢ (𝐺dom DProd (𝑇 ↾ (0..^(♯‘𝑆))) → (𝐺 DProd (𝑇 ↾ (0..^(♯‘𝑆)))) ∈ (SubGrp‘𝐺))
119	84, 118	syl 18	. . . 4 ⊢ (𝜑 → (𝐺 DProd (𝑇 ↾ (0..^(♯‘𝑆)))) ∈ (SubGrp‘𝐺))
120		dprdsubg 20102	. . . . 5 ⊢ (𝐺dom DProd (𝑇 ↾ {(♯‘𝑆)}) → (𝐺 DProd (𝑇 ↾ {(♯‘𝑆)})) ∈ (SubGrp‘𝐺))
121	116, 120	syl 18	. . . 4 ⊢ (𝜑 → (𝐺 DProd (𝑇 ↾ {(♯‘𝑆)})) ∈ (SubGrp‘𝐺))
122	71, 117, 119, 121	ablcntzd 19933	. . 3 ⊢ (𝜑 → (𝐺 DProd (𝑇 ↾ (0..^(♯‘𝑆)))) ⊆ ((Cntz‘𝐺)‘(𝐺 DProd (𝑇 ↾ {(♯‘𝑆)}))))
123		pgpfac.i	. . . 4 ⊢ (𝜑 → ((𝐾‘{𝑋}) ∩ 𝑊) = { 0 })
124	83	oveq2d 7428	. . . . . . 7 ⊢ (𝜑 → (𝐺 DProd (𝑇 ↾ (0..^(♯‘𝑆)))) = (𝐺 DProd 𝑆))
125		pgpfac.5	. . . . . . 7 ⊢ (𝜑 → (𝐺 DProd 𝑆) = 𝑊)
126	124, 125	eqtrd 2797	. . . . . 6 ⊢ (𝜑 → (𝐺 DProd (𝑇 ↾ (0..^(♯‘𝑆)))) = 𝑊)
127	115	oveq2d 7428	. . . . . . 7 ⊢ (𝜑 → (𝐺 DProd (𝑇 ↾ {(♯‘𝑆)})) = (𝐺 DProd {⟨(♯‘𝑆), (𝐾‘{𝑋})⟩}))
128	87	simprd 500	. . . . . . 7 ⊢ (𝜑 → (𝐺 DProd {⟨(♯‘𝑆), (𝐾‘{𝑋})⟩}) = (𝐾‘{𝑋}))
129	127, 128	eqtrd 2797	. . . . . 6 ⊢ (𝜑 → (𝐺 DProd (𝑇 ↾ {(♯‘𝑆)})) = (𝐾‘{𝑋}))
130	126, 129	ineq12d 4173	. . . . 5 ⊢ (𝜑 → ((𝐺 DProd (𝑇 ↾ (0..^(♯‘𝑆)))) ∩ (𝐺 DProd (𝑇 ↾ {(♯‘𝑆)}))) = (𝑊 ∩ (𝐾‘{𝑋})))
131		incom 4161	. . . . 5 ⊢ (𝑊 ∩ (𝐾‘{𝑋})) = ((𝐾‘{𝑋}) ∩ 𝑊)
132	130, 131	eqtrdi 2813	. . . 4 ⊢ (𝜑 → ((𝐺 DProd (𝑇 ↾ (0..^(♯‘𝑆)))) ∩ (𝐺 DProd (𝑇 ↾ {(♯‘𝑆)}))) = ((𝐾‘{𝑋}) ∩ 𝑊))
133	4, 72	subg0 19204	. . . . . . 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 2815	. . . . 5 ⊢ (𝜑 → (0_g‘𝐺) = 0 )
137	136	sneqd 4600	. . . 4 ⊢ (𝜑 → {(0_g‘𝐺)} = { 0 })
138	123, 132, 137	3eqtr4d 2807	. . 3 ⊢ (𝜑 → ((𝐺 DProd (𝑇 ↾ (0..^(♯‘𝑆)))) ∩ (𝐺 DProd (𝑇 ↾ {(♯‘𝑆)}))) = {(0_g‘𝐺)})
139	48, 56, 70, 71, 72, 84, 116, 122, 138	dmdprdsplit2 20124	. 2 ⊢ (𝜑 → 𝐺dom DProd 𝑇)
140		eqid 2762	. . . . 5 ⊢ (LSSum‘𝐺) = (LSSum‘𝐺)
141	48, 56, 70, 140, 139	dprdsplit 20126	. . . 4 ⊢ (𝜑 → (𝐺 DProd 𝑇) = ((𝐺 DProd (𝑇 ↾ (0..^(♯‘𝑆))))(LSSum‘𝐺)(𝐺 DProd (𝑇 ↾ {(♯‘𝑆)}))))
142	126, 129	oveq12d 7430	. . . 4 ⊢ (𝜑 → ((𝐺 DProd (𝑇 ↾ (0..^(♯‘𝑆))))(LSSum‘𝐺)(𝐺 DProd (𝑇 ↾ {(♯‘𝑆)}))) = (𝑊(LSSum‘𝐺)(𝐾‘{𝑋})))
143	126, 119	eqeltrrd 2863	. . . . 5 ⊢ (𝜑 → 𝑊 ∈ (SubGrp‘𝐺))
144	140	lsmcom 19934	. . . . 5 ⊢ ((𝐺 ∈ Abel ∧ 𝑊 ∈ (SubGrp‘𝐺) ∧ (𝐾‘{𝑋}) ∈ (SubGrp‘𝐺)) → (𝑊(LSSum‘𝐺)(𝐾‘{𝑋})) = ((𝐾‘{𝑋})(LSSum‘𝐺)𝑊))
145	117, 143, 21, 144	syl3anc 1397	. . . 4 ⊢ (𝜑 → (𝑊(LSSum‘𝐺)(𝐾‘{𝑋})) = ((𝐾‘{𝑋})(LSSum‘𝐺)𝑊))
146	141, 142, 145	3eqtrd 2801	. . 3 ⊢ (𝜑 → (𝐺 DProd 𝑇) = ((𝐾‘{𝑋})(LSSum‘𝐺)𝑊))
147		pgpfac.w	. . . . . 6 ⊢ (𝜑 → 𝑊 ∈ (SubGrp‘𝐻))
148	7	subgss 19199	. . . . . 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 19749	. . . 4 ⊢ ((𝑈 ∈ (SubGrp‘𝐺) ∧ (𝐾‘{𝑋}) ⊆ 𝑈 ∧ 𝑊 ⊆ 𝑈) → ((𝐾‘{𝑋})(LSSum‘𝐺)𝑊) = ((𝐾‘{𝑋}) ⊕ 𝑊))
153	3, 23, 150, 152	syl3anc 1397	. . 3 ⊢ (𝜑 → ((𝐾‘{𝑋})(LSSum‘𝐺)𝑊) = ((𝐾‘{𝑋}) ⊕ 𝑊))
154		pgpfac.s	. . 3 ⊢ (𝜑 → ((𝐾‘{𝑋}) ⊕ 𝑊) = 𝑈)
155	146, 153, 154	3eqtrd 2801	. 2 ⊢ (𝜑 → (𝐺 DProd 𝑇) = 𝑈)
156		breq2 5112	. . . 4 ⊢ (𝑠 = 𝑇 → (𝐺dom DProd 𝑠 ↔ 𝐺dom DProd 𝑇))
157		oveq2 7420	. . . . 5 ⊢ (𝑠 = 𝑇 → (𝐺 DProd 𝑠) = (𝐺 DProd 𝑇))
158	157	eqeq1d 2764	. . . 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

This proof depends on syntax axioms: ¬ wn 3 → wi 4 ↔ wb 209 ∧ wa 400 = wceq 1569 ∈ wcel 2142 ≠ wne 2957 ∀wral 3078 ∃wrex 3088 {crab 3415 Vcvv 3454 ∪ cun 3902 ∩ cin 3903 ⊆ wss 3904 ⊊ wpss 3905 ∅c0 4285 {csn 4588 ⟨cop 4594 class class class wbr 5108 dom cdm 5660 ran crn 5661 ↾ cres 5662 Fn wfn 6531 ⟶wf 6532 ‘cfv 6536 (class class class)co 7412 Fincfn 8941 0cc0 11106 1c1 11107 + caddc 11109 ℕcn 12239 ℕ₀cn0 12510 ℤcz 12597 ℤ_≥cuz 12868 ..^cfzo 13689 ♯chash 14373 Word cword 14557 ++ cconcat 14614 ⟨“cs1 14640 ℙcprime 16735 Basecbs 17275 ↾_s cress 17296 0_gc0g 17498 Moorecmre 17640 mrClscmrc 17641 ACScacs 17643 Grpcgrp 19006 SubGrpcsubg 19192 Cntzccntz 19391 odcod 19600 gExcgex 19601 pGrp cpgp 19602 LSSumclsm 19710 Abelcabl 19857 CycGrpccyg 19953 DProd cdprd 20071

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1824 ax-4 1838 ax-5 1939 ax-6 1996 ax-7 2037 ax-8 2144 ax-9 2152 ax-10 2175 ax-11 2191 ax-12 2212 ax-ext 2734 ax-rep 5237 ax-sep 5256 ax-nul 5268 ax-pow 5335 ax-pr 5403 ax-un 7734 ax-cnex 11162 ax-resscn 11163 ax-1cn 11164 ax-icn 11165 ax-addcl 11166 ax-addrcl 11167 ax-mulcl 11168 ax-mulrcl 11169 ax-mulcom 11170 ax-addass 11171 ax-mulass 11172 ax-distr 11173 ax-i2m1 11174 ax-1ne0 11175 ax-1rid 11176 ax-rnegex 11177 ax-rrecex 11178 ax-cnre 11179 ax-pre-lttri 11180 ax-pre-lttrn 11181 ax-pre-ltadd 11182 ax-pre-mulgt0 11183

This proof depends on definitions: df-bi 210 df-an 401 df-or 861 df-3or 1103 df-3an 1104 df-tru 1572 df-fal 1582 df-ex 1809 df-nf 1813 df-sb 2096 df-mo 2566 df-eu 2596 df-clab 2741 df-cleq 2754 df-clel 2837 df-nfc 2911 df-ne 2958 df-nel 3064 df-ral 3079 df-rex 3089 df-rmo 3368 df-reu 3369 df-rab 3416 df-v 3456 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 5555 df-eprel 5560 df-po 5568 df-so 5569 df-fr 5613 df-se 5614 df-we 5615 df-xp 5666 df-rel 5667 df-cnv 5668 df-co 5669 df-dm 5670 df-rn 5671 df-res 5672 df-ima 5673 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 7369 df-ov 7415 df-oprab 7416 df-mpo 7417 df-of 7676 df-om 7861 df-1st 7984 df-2nd 7985 df-supp 8155 df-tpos 8220 df-frecs 8276 df-wrecs 8307 df-recs 8356 df-rdg 8395 df-1o 8451 df-2o 8452 df-er 8692 df-map 8824 df-ixp 8894 df-en 8942 df-dom 8943 df-sdom 8944 df-fin 8945 df-fsupp 9320 df-sup 9400 df-inf 9401 df-oi 9470 df-card 9932 df-pnf 11251 df-mnf 11252 df-xr 11253 df-ltxr 11254 df-le 11255 df-sub 11449 df-neg 11450 df-nn 12240 df-2 12309 df-n0 12511 df-z 12598 df-uz 12869 df-fz 13542 df-fzo 13690 df-seq 14045 df-hash 14374 df-word 14558 df-concat 14615 df-s1 14641 df-sets 17230 df-slot 17248 df-ndx 17260 df-base 17276 df-ress 17297 df-plusg 17329 df-0g 17500 df-gsum 17501 df-mre 17644 df-mrc 17645 df-acs 17647 df-mgm 18704 df-sgrp 18783 df-mnd 18799 df-mhm 18847 df-submnd 18848 df-grp 19009 df-minusg 19010 df-sbg 19011 df-mulg 19140 df-subg 19195 df-ghm 19290 df-gim 19335 df-cntz 19393 df-oppg 19422 df-od 19604 df-pgp 19606 df-lsm 19712 df-cmn 19858 df-abl 19859 df-cyg 19954 df-dprd 20073

This theorem is used by: pgpfaclem2 20160

W3C validator