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 20298

Description: Lemma for pgpfac 20301. (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 19340	. . . . . . . . . 10 ⊢ (𝑈 ∈ (SubGrp‘𝐺) → 𝐻 ∈ Grp)
6	3, 5	syl 18	. . . . . . . . 9 ⊢ (𝜑 → 𝐻 ∈ Grp)
7		eqid 2760	. . . . . . . . . 10 ⊢ (Base‘𝐻) = (Base‘𝐻)
8	7	subgacs 19372	. . . . . . . . 9 ⊢ (𝐻 ∈ Grp → (SubGrp‘𝐻) ∈ (ACS‘(Base‘𝐻)))
9	6, 8	syl 18	. . . . . . . 8 ⊢ (𝜑 → (SubGrp‘𝐻) ∈ (ACS‘(Base‘𝐻)))
10	9	acsmred 17831	. . . . . . 7 ⊢ (𝜑 → (SubGrp‘𝐻) ∈ (Moore‘(Base‘𝐻)))
11		pgpfac.x	. . . . . . . 8 ⊢ (𝜑 → 𝑋 ∈ 𝑈)
12	4	subgbas 19341	. . . . . . . . 9 ⊢ (𝑈 ∈ (SubGrp‘𝐺) → 𝑈 = (Base‘𝐻))
13	3, 12	syl 18	. . . . . . . 8 ⊢ (𝜑 → 𝑈 = (Base‘𝐻))
14	11, 13	eleqtrd 2862	. . . . . . 7 ⊢ (𝜑 → 𝑋 ∈ (Base‘𝐻))
15		pgpfac.k	. . . . . . . 8 ⊢ 𝐾 = (mrCls‘(SubGrp‘𝐻))
16	15	mrcsncl 17787	. . . . . . 7 ⊢ (((SubGrp‘𝐻) ∈ (Moore‘(Base‘𝐻)) ∧ 𝑋 ∈ (Base‘𝐻)) → (𝐾‘{𝑋}) ∈ (SubGrp‘𝐻))
17	10, 14, 16	syl2anc 596	. . . . . 6 ⊢ (𝜑 → (𝐾‘{𝑋}) ∈ (SubGrp‘𝐻))
18	4	subsubg 19361	. . . . . . 7 ⊢ (𝑈 ∈ (SubGrp‘𝐺) → ((𝐾‘{𝑋}) ∈ (SubGrp‘𝐻) ↔ ((𝐾‘{𝑋}) ∈ (SubGrp‘𝐺) ∧ (𝐾‘{𝑋}) ⊆ 𝑈)))
19	3, 18	syl 18	. . . . . 6 ⊢ (𝜑 → ((𝐾‘{𝑋}) ∈ (SubGrp‘𝐻) ↔ ((𝐾‘{𝑋}) ∈ (SubGrp‘𝐺) ∧ (𝐾‘{𝑋}) ⊆ 𝑈)))
20	17, 19	mpbid 235	. . . . 5 ⊢ (𝜑 → ((𝐾‘{𝑋}) ∈ (SubGrp‘𝐺) ∧ (𝐾‘{𝑋}) ⊆ 𝑈))
21	20	simpld 500	. . . 4 ⊢ (𝜑 → (𝐾‘{𝑋}) ∈ (SubGrp‘𝐺))
22	4	oveq1i 7430	. . . . . . 7 ⊢ (𝐻 ↾_s (𝐾‘{𝑋})) = ((𝐺 ↾_s 𝑈) ↾_s (𝐾‘{𝑋}))
23	20	simprd 501	. . . . . . . 8 ⊢ (𝜑 → (𝐾‘{𝑋}) ⊆ 𝑈)
24		ressabs 17427	. . . . . . . 8 ⊢ ((𝑈 ∈ (SubGrp‘𝐺) ∧ (𝐾‘{𝑋}) ⊆ 𝑈) → ((𝐺 ↾_s 𝑈) ↾_s (𝐾‘{𝑋})) = (𝐺 ↾_s (𝐾‘{𝑋})))
25	3, 23, 24	syl2anc 596	. . . . . . 7 ⊢ (𝜑 → ((𝐺 ↾_s 𝑈) ↾_s (𝐾‘{𝑋})) = (𝐺 ↾_s (𝐾‘{𝑋})))
26	22, 25	eqtrid 2807	. . . . . 6 ⊢ (𝜑 → (𝐻 ↾_s (𝐾‘{𝑋})) = (𝐺 ↾_s (𝐾‘{𝑋})))
27	7, 15	cycsubgcyg2 20117	. . . . . . 7 ⊢ ((𝐻 ∈ Grp ∧ 𝑋 ∈ (Base‘𝐻)) → (𝐻 ↾_s (𝐾‘{𝑋})) ∈ CycGrp)
28	6, 14, 27	syl2anc 596	. . . . . 6 ⊢ (𝜑 → (𝐻 ↾_s (𝐾‘{𝑋})) ∈ CycGrp)
29	26, 28	eqeltrrd 2861	. . . . 5 ⊢ (𝜑 → (𝐺 ↾_s (𝐾‘{𝑋})) ∈ CycGrp)
30		pgpfac.p	. . . . . . 7 ⊢ (𝜑 → 𝑃 pGrp 𝐺)
31		pgpprm 19808	. . . . . . 7 ⊢ (𝑃 pGrp 𝐺 → 𝑃 ∈ ℙ)
32	30, 31	syl 18	. . . . . 6 ⊢ (𝜑 → 𝑃 ∈ ℙ)
33		subgpgp 19812	. . . . . . 7 ⊢ ((𝑃 pGrp 𝐺 ∧ (𝐾‘{𝑋}) ∈ (SubGrp‘𝐺)) → 𝑃 pGrp (𝐺 ↾_s (𝐾‘{𝑋})))
34	30, 21, 33	syl2anc 596	. . . . . 6 ⊢ (𝜑 → 𝑃 pGrp (𝐺 ↾_s (𝐾‘{𝑋})))
35		brelrng 5922	. . . . . 6 ⊢ ((𝑃 ∈ ℙ ∧ (𝐺 ↾_s (𝐾‘{𝑋})) ∈ CycGrp ∧ 𝑃 pGrp (𝐺 ↾_s (𝐾‘{𝑋}))) → (𝐺 ↾_s (𝐾‘{𝑋})) ∈ ran pGrp )
36	32, 29, 34, 35	syl3anc 1398	. . . . 5 ⊢ (𝜑 → (𝐺 ↾_s (𝐾‘{𝑋})) ∈ ran pGrp )
37	29, 36	elind 4097	. . . 4 ⊢ (𝜑 → (𝐺 ↾_s (𝐾‘{𝑋})) ∈ (CycGrp ∩ ran pGrp ))
38		oveq2 7428	. . . . . 6 ⊢ (𝑟 = (𝐾‘{𝑋}) → (𝐺 ↾_s 𝑟) = (𝐺 ↾_s (𝐾‘{𝑋})))
39	38	eleq1d 2845	. . . . 5 ⊢ (𝑟 = (𝐾‘{𝑋}) → ((𝐺 ↾_s 𝑟) ∈ (CycGrp ∩ ran pGrp ) ↔ (𝐺 ↾_s (𝐾‘{𝑋})) ∈ (CycGrp ∩ ran pGrp )))
40		pgpfac.c	. . . . 5 ⊢ 𝐶 = {𝑟 ∈ (SubGrp‘𝐺) ∣ (𝐺 ↾_s 𝑟) ∈ (CycGrp ∩ ran pGrp )}
41	39, 40	elrab2 3648	. . . 4 ⊢ ((𝐾‘{𝑋}) ∈ 𝐶 ↔ ((𝐾‘{𝑋}) ∈ (SubGrp‘𝐺) ∧ (𝐺 ↾_s (𝐾‘{𝑋})) ∈ (CycGrp ∩ ran pGrp )))
42	21, 37, 41	sylanbrc 595	. . 3 ⊢ (𝜑 → (𝐾‘{𝑋}) ∈ 𝐶)
43	1, 2, 42	cats1cld 15007	. 2 ⊢ (𝜑 → 𝑇 ∈ Word 𝐶)
44		wrdf 14664	. . . . 5 ⊢ (𝑇 ∈ Word 𝐶 → 𝑇:(0..^(♯‘𝑇))⟶𝐶)
45	43, 44	syl 18	. . . 4 ⊢ (𝜑 → 𝑇:(0..^(♯‘𝑇))⟶𝐶)
46	40	ssrab3 4007	. . . 4 ⊢ 𝐶 ⊆ (SubGrp‘𝐺)
47		fss 6726	. . . 4 ⊢ ((𝑇:(0..^(♯‘𝑇))⟶𝐶 ∧ 𝐶 ⊆ (SubGrp‘𝐺)) → 𝑇:(0..^(♯‘𝑇))⟶(SubGrp‘𝐺))
48	45, 46, 47	sylancl 598	. . 3 ⊢ (𝜑 → 𝑇:(0..^(♯‘𝑇))⟶(SubGrp‘𝐺))
49		lencl 14679	. . . . . . . 8 ⊢ (𝑆 ∈ Word 𝐶 → (♯‘𝑆) ∈ ℕ₀)
50	2, 49	syl 18	. . . . . . 7 ⊢ (𝜑 → (♯‘𝑆) ∈ ℕ₀)
51	50	nn0zd 12719	. . . . . 6 ⊢ (𝜑 → (♯‘𝑆) ∈ ℤ)
52		fzosn 13872	. . . . . 6 ⊢ ((♯‘𝑆) ∈ ℤ → ((♯‘𝑆)..^((♯‘𝑆) + 1)) = {(♯‘𝑆)})
53	51, 52	syl 18	. . . . 5 ⊢ (𝜑 → ((♯‘𝑆)..^((♯‘𝑆) + 1)) = {(♯‘𝑆)})
54	53	ineq2d 4117	. . . 4 ⊢ (𝜑 → ((0..^(♯‘𝑆)) ∩ ((♯‘𝑆)..^((♯‘𝑆) + 1))) = ((0..^(♯‘𝑆)) ∩ {(♯‘𝑆)}))
55		fzodisj 13829	. . . 4 ⊢ ((0..^(♯‘𝑆)) ∩ ((♯‘𝑆)..^((♯‘𝑆) + 1))) = ∅
56	54, 55	eqtr3di 2810	. . 3 ⊢ (𝜑 → ((0..^(♯‘𝑆)) ∩ {(♯‘𝑆)}) = ∅)
57	1	fveq2i 6888	. . . . . . 7 ⊢ (♯‘𝑇) = (♯‘(𝑆 ++ ⟨“(𝐾‘{𝑋})”⟩))
58	42	s1cld 14751	. . . . . . . 8 ⊢ (𝜑 → ⟨“(𝐾‘{𝑋})”⟩ ∈ Word 𝐶)
59		ccatlen 14721	. . . . . . . 8 ⊢ ((𝑆 ∈ Word 𝐶 ∧ ⟨“(𝐾‘{𝑋})”⟩ ∈ Word 𝐶) → (♯‘(𝑆 ++ ⟨“(𝐾‘{𝑋})”⟩)) = ((♯‘𝑆) + (♯‘⟨“(𝐾‘{𝑋})”⟩)))
60	2, 58, 59	syl2anc 596	. . . . . . 7 ⊢ (𝜑 → (♯‘(𝑆 ++ ⟨“(𝐾‘{𝑋})”⟩)) = ((♯‘𝑆) + (♯‘⟨“(𝐾‘{𝑋})”⟩)))
61	57, 60	eqtrid 2807	. . . . . 6 ⊢ (𝜑 → (♯‘𝑇) = ((♯‘𝑆) + (♯‘⟨“(𝐾‘{𝑋})”⟩)))
62		s1len 14754	. . . . . . 7 ⊢ (♯‘⟨“(𝐾‘{𝑋})”⟩) = 1
63	62	oveq2i 7431	. . . . . 6 ⊢ ((♯‘𝑆) + (♯‘⟨“(𝐾‘{𝑋})”⟩)) = ((♯‘𝑆) + 1)
64	61, 63	eqtrdi 2811	. . . . 5 ⊢ (𝜑 → (♯‘𝑇) = ((♯‘𝑆) + 1))
65	64	oveq2d 7436	. . . 4 ⊢ (𝜑 → (0..^(♯‘𝑇)) = (0..^((♯‘𝑆) + 1)))
66		nn0uz 13004	. . . . . 6 ⊢ ℕ₀ = (ℤ_≥‘0)
67	50, 66	eleqtrdi 2870	. . . . 5 ⊢ (𝜑 → (♯‘𝑆) ∈ (ℤ_≥‘0))
68		fzosplitsn 13912	. . . . 5 ⊢ ((♯‘𝑆) ∈ (ℤ_≥‘0) → (0..^((♯‘𝑆) + 1)) = ((0..^(♯‘𝑆)) ∪ {(♯‘𝑆)}))
69	67, 68	syl 18	. . . 4 ⊢ (𝜑 → (0..^((♯‘𝑆) + 1)) = ((0..^(♯‘𝑆)) ∪ {(♯‘𝑆)}))
70	65, 69	eqtrd 2795	. . 3 ⊢ (𝜑 → (0..^(♯‘𝑇)) = ((0..^(♯‘𝑆)) ∪ {(♯‘𝑆)}))
71		eqid 2760	. . 3 ⊢ (Cntz‘𝐺) = (Cntz‘𝐺)
72		eqid 2760	. . 3 ⊢ (0_g‘𝐺) = (0_g‘𝐺)
73		pgpfac.4	. . . 4 ⊢ (𝜑 → 𝐺dom DProd 𝑆)
74		cats1un 14871	. . . . . . . 8 ⊢ ((𝑆 ∈ Word 𝐶 ∧ (𝐾‘{𝑋}) ∈ 𝐶) → (𝑆 ++ ⟨“(𝐾‘{𝑋})”⟩) = (𝑆 ∪ {⟨(♯‘𝑆), (𝐾‘{𝑋})⟩}))
75	2, 42, 74	syl2anc 596	. . . . . . 7 ⊢ (𝜑 → (𝑆 ++ ⟨“(𝐾‘{𝑋})”⟩) = (𝑆 ∪ {⟨(♯‘𝑆), (𝐾‘{𝑋})⟩}))
76	1, 75	eqtrid 2807	. . . . . 6 ⊢ (𝜑 → 𝑇 = (𝑆 ∪ {⟨(♯‘𝑆), (𝐾‘{𝑋})⟩}))
77	76	reseq1d 5968	. . . . 5 ⊢ (𝜑 → (𝑇 ↾ (0..^(♯‘𝑆))) = ((𝑆 ∪ {⟨(♯‘𝑆), (𝐾‘{𝑋})⟩}) ↾ (0..^(♯‘𝑆))))
78		wrdfn 14674	. . . . . . 7 ⊢ (𝑆 ∈ Word 𝐶 → 𝑆 Fn (0..^(♯‘𝑆)))
79	2, 78	syl 18	. . . . . 6 ⊢ (𝜑 → 𝑆 Fn (0..^(♯‘𝑆)))
80		fzonel 13809	. . . . . 6 ⊢ ¬ (♯‘𝑆) ∈ (0..^(♯‘𝑆))
81		fsnunres 7193	. . . . . 6 ⊢ ((𝑆 Fn (0..^(♯‘𝑆)) ∧ ¬ (♯‘𝑆) ∈ (0..^(♯‘𝑆))) → ((𝑆 ∪ {⟨(♯‘𝑆), (𝐾‘{𝑋})⟩}) ↾ (0..^(♯‘𝑆))) = 𝑆)
82	79, 80, 81	sylancl 598	. . . . 5 ⊢ (𝜑 → ((𝑆 ∪ {⟨(♯‘𝑆), (𝐾‘{𝑋})⟩}) ↾ (0..^(♯‘𝑆))) = 𝑆)
83	77, 82	eqtrd 2795	. . . 4 ⊢ (𝜑 → (𝑇 ↾ (0..^(♯‘𝑆))) = 𝑆)
84	73, 83	breqtrrd 5132	. . 3 ⊢ (𝜑 → 𝐺dom DProd (𝑇 ↾ (0..^(♯‘𝑆))))
85		fvex 6898	. . . . . 6 ⊢ (♯‘𝑆) ∈ V
86		dprdsn 20253	. . . . . 6 ⊢ (((♯‘𝑆) ∈ V ∧ (𝐾‘{𝑋}) ∈ (SubGrp‘𝐺)) → (𝐺dom DProd {⟨(♯‘𝑆), (𝐾‘{𝑋})⟩} ∧ (𝐺 DProd {⟨(♯‘𝑆), (𝐾‘{𝑋})⟩}) = (𝐾‘{𝑋})))
87	85, 21, 86	sylancr 599	. . . . 5 ⊢ (𝜑 → (𝐺dom DProd {⟨(♯‘𝑆), (𝐾‘{𝑋})⟩} ∧ (𝐺 DProd {⟨(♯‘𝑆), (𝐾‘{𝑋})⟩}) = (𝐾‘{𝑋})))
88	87	simpld 500	. . . 4 ⊢ (𝜑 → 𝐺dom DProd {⟨(♯‘𝑆), (𝐾‘{𝑋})⟩})
89		wrdfn 14674	. . . . . . 7 ⊢ (𝑇 ∈ Word 𝐶 → 𝑇 Fn (0..^(♯‘𝑇)))
90	43, 89	syl 18	. . . . . 6 ⊢ (𝜑 → 𝑇 Fn (0..^(♯‘𝑇)))
91		ssun2 4177	. . . . . . . 8 ⊢ {(♯‘𝑆)} ⊆ ((0..^(♯‘𝑆)) ∪ {(♯‘𝑆)})
92	85	snss 4744	. . . . . . . 8 ⊢ ((♯‘𝑆) ∈ ((0..^(♯‘𝑆)) ∪ {(♯‘𝑆)}) ↔ {(♯‘𝑆)} ⊆ ((0..^(♯‘𝑆)) ∪ {(♯‘𝑆)}))
93	91, 92	mpbir 234	. . . . . . 7 ⊢ (♯‘𝑆) ∈ ((0..^(♯‘𝑆)) ∪ {(♯‘𝑆)})
94	93, 70	eleqtrrid 2867	. . . . . 6 ⊢ (𝜑 → (♯‘𝑆) ∈ (0..^(♯‘𝑇)))
95		fnressn 7162	. . . . . 6 ⊢ ((𝑇 Fn (0..^(♯‘𝑇)) ∧ (♯‘𝑆) ∈ (0..^(♯‘𝑇))) → (𝑇 ↾ {(♯‘𝑆)}) = {⟨(♯‘𝑆), (𝑇‘(♯‘𝑆))⟩})
96	90, 94, 95	syl2anc 596	. . . . 5 ⊢ (𝜑 → (𝑇 ↾ {(♯‘𝑆)}) = {⟨(♯‘𝑆), (𝑇‘(♯‘𝑆))⟩})
97	1	fveq1i 6886	. . . . . . . . 9 ⊢ (𝑇‘(♯‘𝑆)) = ((𝑆 ++ ⟨“(𝐾‘{𝑋})”⟩)‘(♯‘𝑆))
98	50	nn0cnd 12670	. . . . . . . . . . 11 ⊢ (𝜑 → (♯‘𝑆) ∈ ℂ)
99	98	addlidd 11512	. . . . . . . . . 10 ⊢ (𝜑 → (0 + (♯‘𝑆)) = (♯‘𝑆))
100	99	fveq2d 6889	. . . . . . . . 9 ⊢ (𝜑 → ((𝑆 ++ ⟨“(𝐾‘{𝑋})”⟩)‘(0 + (♯‘𝑆))) = ((𝑆 ++ ⟨“(𝐾‘{𝑋})”⟩)‘(♯‘𝑆)))
101	97, 100	eqtr4id 2814	. . . . . . . 8 ⊢ (𝜑 → (𝑇‘(♯‘𝑆)) = ((𝑆 ++ ⟨“(𝐾‘{𝑋})”⟩)‘(0 + (♯‘𝑆))))
102		1nn 12347	. . . . . . . . . . . 12 ⊢ 1 ∈ ℕ
103	62, 102	eqeltri 2856	. . . . . . . . . . 11 ⊢ (♯‘⟨“(𝐾‘{𝑋})”⟩) ∈ ℕ
104		lbfzo0 13835	. . . . . . . . . . 11 ⊢ (0 ∈ (0..^(♯‘⟨“(𝐾‘{𝑋})”⟩)) ↔ (♯‘⟨“(𝐾‘{𝑋})”⟩) ∈ ℕ)
105	103, 104	mpbir 234	. . . . . . . . . 10 ⊢ 0 ∈ (0..^(♯‘⟨“(𝐾‘{𝑋})”⟩))
106	105	a1i 11	. . . . . . . . 9 ⊢ (𝜑 → 0 ∈ (0..^(♯‘⟨“(𝐾‘{𝑋})”⟩)))
107		ccatval3 14725	. . . . . . . . 9 ⊢ ((𝑆 ∈ Word 𝐶 ∧ ⟨“(𝐾‘{𝑋})”⟩ ∈ Word 𝐶 ∧ 0 ∈ (0..^(♯‘⟨“(𝐾‘{𝑋})”⟩))) → ((𝑆 ++ ⟨“(𝐾‘{𝑋})”⟩)‘(0 + (♯‘𝑆))) = (⟨“(𝐾‘{𝑋})”⟩‘0))
108	2, 58, 106, 107	syl3anc 1398	. . . . . . . 8 ⊢ (𝜑 → ((𝑆 ++ ⟨“(𝐾‘{𝑋})”⟩)‘(0 + (♯‘𝑆))) = (⟨“(𝐾‘{𝑋})”⟩‘0))
109		fvex 6898	. . . . . . . . 9 ⊢ (𝐾‘{𝑋}) ∈ V
110		s1fv 14759	. . . . . . . . 9 ⊢ ((𝐾‘{𝑋}) ∈ V → (⟨“(𝐾‘{𝑋})”⟩‘0) = (𝐾‘{𝑋}))
111	109, 110	mp1i 14	. . . . . . . 8 ⊢ (𝜑 → (⟨“(𝐾‘{𝑋})”⟩‘0) = (𝐾‘{𝑋}))
112	101, 108, 111	3eqtrd 2799	. . . . . . 7 ⊢ (𝜑 → (𝑇‘(♯‘𝑆)) = (𝐾‘{𝑋}))
113	112	opeq2d 4839	. . . . . 6 ⊢ (𝜑 → ⟨(♯‘𝑆), (𝑇‘(♯‘𝑆))⟩ = ⟨(♯‘𝑆), (𝐾‘{𝑋})⟩)
114	113	sneqd 4595	. . . . 5 ⊢ (𝜑 → {⟨(♯‘𝑆), (𝑇‘(♯‘𝑆))⟩} = {⟨(♯‘𝑆), (𝐾‘{𝑋})⟩})
115	96, 114	eqtrd 2795	. . . 4 ⊢ (𝜑 → (𝑇 ↾ {(♯‘𝑆)}) = {⟨(♯‘𝑆), (𝐾‘{𝑋})⟩})
116	88, 115	breqtrrd 5132	. . 3 ⊢ (𝜑 → 𝐺dom DProd (𝑇 ↾ {(♯‘𝑆)}))
117		pgpfac.g	. . . 4 ⊢ (𝜑 → 𝐺 ∈ Abel)
118		dprdsubg 20241	. . . . 5 ⊢ (𝐺dom DProd (𝑇 ↾ (0..^(♯‘𝑆))) → (𝐺 DProd (𝑇 ↾ (0..^(♯‘𝑆)))) ∈ (SubGrp‘𝐺))
119	84, 118	syl 18	. . . 4 ⊢ (𝜑 → (𝐺 DProd (𝑇 ↾ (0..^(♯‘𝑆)))) ∈ (SubGrp‘𝐺))
120		dprdsubg 20241	. . . . 5 ⊢ (𝐺dom DProd (𝑇 ↾ {(♯‘𝑆)}) → (𝐺 DProd (𝑇 ↾ {(♯‘𝑆)})) ∈ (SubGrp‘𝐺))
121	116, 120	syl 18	. . . 4 ⊢ (𝜑 → (𝐺 DProd (𝑇 ↾ {(♯‘𝑆)})) ∈ (SubGrp‘𝐺))
122	71, 117, 119, 121	ablcntzd 20072	. . 3 ⊢ (𝜑 → (𝐺 DProd (𝑇 ↾ (0..^(♯‘𝑆)))) ⊆ ((Cntz‘𝐺)‘(𝐺 DProd (𝑇 ↾ {(♯‘𝑆)}))))
123		pgpfac.i	. . . 4 ⊢ (𝜑 → ((𝐾‘{𝑋}) ∩ 𝑊) = { 0 })
124	83	oveq2d 7436	. . . . . . 7 ⊢ (𝜑 → (𝐺 DProd (𝑇 ↾ (0..^(♯‘𝑆)))) = (𝐺 DProd 𝑆))
125		pgpfac.5	. . . . . . 7 ⊢ (𝜑 → (𝐺 DProd 𝑆) = 𝑊)
126	124, 125	eqtrd 2795	. . . . . 6 ⊢ (𝜑 → (𝐺 DProd (𝑇 ↾ (0..^(♯‘𝑆)))) = 𝑊)
127	115	oveq2d 7436	. . . . . . 7 ⊢ (𝜑 → (𝐺 DProd (𝑇 ↾ {(♯‘𝑆)})) = (𝐺 DProd {⟨(♯‘𝑆), (𝐾‘{𝑋})⟩}))
128	87	simprd 501	. . . . . . 7 ⊢ (𝜑 → (𝐺 DProd {⟨(♯‘𝑆), (𝐾‘{𝑋})⟩}) = (𝐾‘{𝑋}))
129	127, 128	eqtrd 2795	. . . . . 6 ⊢ (𝜑 → (𝐺 DProd (𝑇 ↾ {(♯‘𝑆)})) = (𝐾‘{𝑋}))
130	126, 129	ineq12d 4118	. . . . 5 ⊢ (𝜑 → ((𝐺 DProd (𝑇 ↾ (0..^(♯‘𝑆)))) ∩ (𝐺 DProd (𝑇 ↾ {(♯‘𝑆)}))) = (𝑊 ∩ (𝐾‘{𝑋})))
131		incom 4106	. . . . 5 ⊢ (𝑊 ∩ (𝐾‘{𝑋})) = ((𝐾‘{𝑋}) ∩ 𝑊)
132	130, 131	eqtrdi 2811	. . . 4 ⊢ (𝜑 → ((𝐺 DProd (𝑇 ↾ (0..^(♯‘𝑆)))) ∩ (𝐺 DProd (𝑇 ↾ {(♯‘𝑆)}))) = ((𝐾‘{𝑋}) ∩ 𝑊))
133	4, 72	subg0 19343	. . . . . . 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 2813	. . . . 5 ⊢ (𝜑 → (0_g‘𝐺) = 0 )
137	136	sneqd 4595	. . . 4 ⊢ (𝜑 → {(0_g‘𝐺)} = { 0 })
138	123, 132, 137	3eqtr4d 2805	. . 3 ⊢ (𝜑 → ((𝐺 DProd (𝑇 ↾ (0..^(♯‘𝑆)))) ∩ (𝐺 DProd (𝑇 ↾ {(♯‘𝑆)}))) = {(0_g‘𝐺)})
139	48, 56, 70, 71, 72, 84, 116, 122, 138	dmdprdsplit2 20263	. 2 ⊢ (𝜑 → 𝐺dom DProd 𝑇)
140		eqid 2760	. . . . 5 ⊢ (LSSum‘𝐺) = (LSSum‘𝐺)
141	48, 56, 70, 140, 139	dprdsplit 20265	. . . 4 ⊢ (𝜑 → (𝐺 DProd 𝑇) = ((𝐺 DProd (𝑇 ↾ (0..^(♯‘𝑆))))(LSSum‘𝐺)(𝐺 DProd (𝑇 ↾ {(♯‘𝑆)}))))
142	126, 129	oveq12d 7438	. . . 4 ⊢ (𝜑 → ((𝐺 DProd (𝑇 ↾ (0..^(♯‘𝑆))))(LSSum‘𝐺)(𝐺 DProd (𝑇 ↾ {(♯‘𝑆)}))) = (𝑊(LSSum‘𝐺)(𝐾‘{𝑋})))
143	126, 119	eqeltrrd 2861	. . . . 5 ⊢ (𝜑 → 𝑊 ∈ (SubGrp‘𝐺))
144	140	lsmcom 20073	. . . . 5 ⊢ ((𝐺 ∈ Abel ∧ 𝑊 ∈ (SubGrp‘𝐺) ∧ (𝐾‘{𝑋}) ∈ (SubGrp‘𝐺)) → (𝑊(LSSum‘𝐺)(𝐾‘{𝑋})) = ((𝐾‘{𝑋})(LSSum‘𝐺)𝑊))
145	117, 143, 21, 144	syl3anc 1398	. . . 4 ⊢ (𝜑 → (𝑊(LSSum‘𝐺)(𝐾‘{𝑋})) = ((𝐾‘{𝑋})(LSSum‘𝐺)𝑊))
146	141, 142, 145	3eqtrd 2799	. . 3 ⊢ (𝜑 → (𝐺 DProd 𝑇) = ((𝐾‘{𝑋})(LSSum‘𝐺)𝑊))
147		pgpfac.w	. . . . . 6 ⊢ (𝜑 → 𝑊 ∈ (SubGrp‘𝐻))
148	7	subgss 19338	. . . . . 6 ⊢ (𝑊 ∈ (SubGrp‘𝐻) → 𝑊 ⊆ (Base‘𝐻))
149	147, 148	syl 18	. . . . 5 ⊢ (𝜑 → 𝑊 ⊆ (Base‘𝐻))
150	149, 13	sseqtrrd 3945	. . . 4 ⊢ (𝜑 → 𝑊 ⊆ 𝑈)
151		pgpfac.l	. . . . 5 ⊢ ⊕ = (LSSum‘𝐻)
152	4, 140, 151	subglsm 19888	. . . 4 ⊢ ((𝑈 ∈ (SubGrp‘𝐺) ∧ (𝐾‘{𝑋}) ⊆ 𝑈 ∧ 𝑊 ⊆ 𝑈) → ((𝐾‘{𝑋})(LSSum‘𝐺)𝑊) = ((𝐾‘{𝑋}) ⊕ 𝑊))
153	3, 23, 150, 152	syl3anc 1398	. . 3 ⊢ (𝜑 → ((𝐾‘{𝑋})(LSSum‘𝐺)𝑊) = ((𝐾‘{𝑋}) ⊕ 𝑊))
154		pgpfac.s	. . 3 ⊢ (𝜑 → ((𝐾‘{𝑋}) ⊕ 𝑊) = 𝑈)
155	146, 153, 154	3eqtrd 2799	. 2 ⊢ (𝜑 → (𝐺 DProd 𝑇) = 𝑈)
156		breq2 5106	. . . 4 ⊢ (𝑠 = 𝑇 → (𝐺dom DProd 𝑠 ↔ 𝐺dom DProd 𝑇))
157		oveq2 7428	. . . . 5 ⊢ (𝑠 = 𝑇 → (𝐺 DProd 𝑠) = (𝐺 DProd 𝑇))
158	157	eqeq1d 2762	. . . 4 ⊢ (𝑠 = 𝑇 → ((𝐺 DProd 𝑠) = 𝑈 ↔ (𝐺 DProd 𝑇) = 𝑈))
159	156, 158	anbi12d 644	. . 3 ⊢ (𝑠 = 𝑇 → ((𝐺dom DProd 𝑠 ∧ (𝐺 DProd 𝑠) = 𝑈) ↔ (𝐺dom DProd 𝑇 ∧ (𝐺 DProd 𝑇) = 𝑈)))
160	159	rspcev 3576	. 2 ⊢ ((𝑇 ∈ Word 𝐶 ∧ (𝐺dom DProd 𝑇 ∧ (𝐺 DProd 𝑇) = 𝑈)) → ∃𝑠 ∈ Word 𝐶(𝐺dom DProd 𝑠 ∧ (𝐺 DProd 𝑠) = 𝑈))
161	43, 139, 155, 160	syl12anc 850	1 ⊢ (𝜑 → ∃𝑠 ∈ Word 𝐶(𝐺dom DProd 𝑠 ∧ (𝐺 DProd 𝑠) = 𝑈))

Colors of variables: wff setvar class

This proof depends on syntax axioms: ¬ wn 3 → wi 4 ↔ wb 209 ∧ wa 401 = wceq 1569 ∈ wcel 2144 ≠ wne 2955 ∀wral 3076 ∃wrex 3086 {crab 3412 Vcvv 3450 ⊆ wss 3895 ⊊ wpss 4013 ∩ cin 4089 ∪ cun 4149 ∅c0 4278 {csn 4583 ⟨cop 4589 class class class wbr 5102 dom cdm 5650 ran crn 5651 ↾ cres 5652 Fn wfn 6533 ⟶wf 6534 ‘cfv 6538 (class class class)co 7420 Fincfn 8974 0cc0 11201 1c1 11202 + caddc 11204 ℕcn 12336 ℕ₀cn0 12607 ℤcz 12694 ℤ_≥cuz 12966 ..^cfzo 13789 ♯chash 14475 Word cword 14659 ++ cconcat 14716 ⟨“cs1 14743 ℙcprime 16847 Basecbs 17388 ↾_s cress 17409 0_gc0g 17611 Moorecmre 17753 mrClscmrc 17754 ACScacs 17756 Grpcgrp 19145 SubGrpcsubg 19331 Cntzccntz 19530 odcod 19739 gExcgex 19740 pGrp cpgp 19741 LSSumclsm 19849 Abelcabl 19996 CycGrpccyg 20092 DProd cdprd 20210

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1827 ax-4 1841 ax-5 1942 ax-6 1999 ax-7 2040 ax-8 2146 ax-9 2154 ax-10 2177 ax-11 2193 ax-12 2212 ax-ext 2732 ax-rep 5231 ax-sep 5248 ax-nul 5259 ax-pow 5326 ax-pr 5390 ax-un 7751 ax-cnex 11257 ax-resscn 11258 ax-1cn 11259 ax-icn 11260 ax-addcl 11261 ax-addrcl 11262 ax-mulcl 11263 ax-mulrcl 11264 ax-mulcom 11265 ax-addass 11266 ax-mulass 11267 ax-distr 11268 ax-i2m1 11269 ax-1ne0 11270 ax-1rid 11271 ax-rnegex 11272 ax-rrecex 11273 ax-cnre 11274 ax-pre-lttri 11275 ax-pre-lttrn 11276 ax-pre-ltadd 11277 ax-pre-mulgt0 11278

This proof depends on definitions: df-bi 210 df-an 402 df-or 862 df-3or 1104 df-3an 1105 df-tru 1572 df-fal 1582 df-ex 1812 df-nf 1816 df-sb 2099 df-mo 2564 df-eu 2594 df-clab 2739 df-cleq 2752 df-clel 2835 df-nfc 2909 df-ne 2956 df-nel 3062 df-ral 3077 df-rex 3087 df-rmo 3365 df-reu 3366 df-rab 3413 df-v 3452 df-sbc 3739 df-csb 3847 df-ss 3896 df-pss 4014 df-dif 4047 df-in 4091 df-un 4151 df-nul 4279 df-if 4482 df-pw 4558 df-sn 4584 df-pr 4586 df-op 4590 df-uni 4867 df-int 4907 df-iun 4952 df-iin 4953 df-br 5103 df-opab 5167 df-mpt 5186 df-tr 5212 df-id 5545 df-eprel 5550 df-po 5558 df-so 5559 df-fr 5603 df-se 5604 df-we 5605 df-xp 5656 df-rel 5657 df-cnv 5658 df-co 5659 df-dm 5660 df-rn 5661 df-res 5662 df-ima 5663 df-pred 6304 df-ord 6365 df-on 6366 df-lim 6367 df-suc 6368 df-iota 6494 df-fun 6540 df-fn 6541 df-f 6542 df-f1 6543 df-fo 6544 df-f1o 6545 df-fv 6546 df-isom 6547 df-riota 7377 df-ov 7423 df-oprab 7424 df-mpo 7425 df-of 7693 df-om 7878 df-1st 8001 df-2nd 8002 df-supp 8178 df-tpos 8244 df-frecs 8300 df-wrecs 8331 df-recs 8380 df-rdg 8419 df-1o 8477 df-2o 8478 df-er 8718 df-map 8850 df-ixp 8927 df-en 8975 df-dom 8976 df-sdom 8977 df-fin 8978 df-fsupp 9355 df-sup 9435 df-inf 9436 df-oi 9505 df-card 10021 df-pnf 11346 df-mnf 11347 df-xr 11348 df-ltxr 11349 df-le 11350 df-sub 11544 df-neg 11545 df-nn 12337 df-2 12406 df-n0 12608 df-z 12695 df-uz 12967 df-fz 13641 df-fzo 13790 df-seq 14146 df-hash 14476 df-word 14660 df-concat 14717 df-s1 14744 df-sets 17343 df-slot 17361 df-ndx 17373 df-base 17389 df-ress 17410 df-plusg 17442 df-0g 17613 df-gsum 17614 df-mre 17757 df-mrc 17758 df-acs 17760 df-mgm 18817 df-sgrp 18909 df-mnd 18925 df-mhm 18979 df-submnd 18980 df-grp 19148 df-minusg 19149 df-sbg 19150 df-mulg 19279 df-subg 19334 df-ghm 19429 df-gim 19474 df-cntz 19532 df-oppg 19561 df-od 19743 df-pgp 19745 df-lsm 19851 df-cmn 19997 df-abl 19998 df-cyg 20093 df-dprd 20212

This theorem is used by: pgpfaclem2 20299

W3C validator