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

Theorem ablfac2 20089
Description: Choose generators for each cyclic group in ablfac 20088. (Contributed by Mario Carneiro, 28-Apr-2016.)
Hypotheses
Ref Expression
ablfac.b 𝐵 = (Base‘𝐺)
ablfac.c 𝐶 = {𝑟 ∈ (SubGrp‘𝐺) ∣ (𝐺s 𝑟) ∈ (CycGrp ∩ ran pGrp )}
ablfac.1 (𝜑𝐺 ∈ Abel)
ablfac.2 (𝜑𝐵 ∈ Fin)
ablfac2.m · = (.g𝐺)
ablfac2.s 𝑆 = (𝑘 ∈ dom 𝑤 ↦ ran (𝑛 ∈ ℤ ↦ (𝑛 · (𝑤𝑘))))
Assertion
Ref Expression
ablfac2 (𝜑 → ∃𝑤 ∈ Word 𝐵(𝑆:dom 𝑤𝐶𝐺dom DProd 𝑆 ∧ (𝐺 DProd 𝑆) = 𝐵))
Distinct variable groups:   𝑆,𝑟   𝑘,𝑛,𝑟,𝑤,𝐵   · ,𝑘,𝑤   𝐶,𝑘,𝑛,𝑤   𝜑,𝑘,𝑛,𝑤   𝑘,𝐺,𝑛,𝑟,𝑤
Allowed substitution hints:   𝜑(𝑟)   𝐶(𝑟)   𝑆(𝑤,𝑘,𝑛)   · (𝑛,𝑟)

Proof of Theorem ablfac2
Dummy variables 𝑠 𝑥 𝑗 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 wrdf 14527 . . . . . . . 8 (𝑠 ∈ Word 𝐶𝑠:(0..^(♯‘𝑠))⟶𝐶)
21ad2antlr 725 . . . . . . 7 (((𝜑𝑠 ∈ Word 𝐶) ∧ (𝐺dom DProd 𝑠 ∧ (𝐺 DProd 𝑠) = 𝐵)) → 𝑠:(0..^(♯‘𝑠))⟶𝐶)
32fdmd 6738 . . . . . 6 (((𝜑𝑠 ∈ Word 𝐶) ∧ (𝐺dom DProd 𝑠 ∧ (𝐺 DProd 𝑠) = 𝐵)) → dom 𝑠 = (0..^(♯‘𝑠)))
4 fzofi 13994 . . . . . 6 (0..^(♯‘𝑠)) ∈ Fin
53, 4eqeltrdi 2834 . . . . 5 (((𝜑𝑠 ∈ Word 𝐶) ∧ (𝐺dom DProd 𝑠 ∧ (𝐺 DProd 𝑠) = 𝐵)) → dom 𝑠 ∈ Fin)
62ffdmd 6759 . . . . . . . . . 10 (((𝜑𝑠 ∈ Word 𝐶) ∧ (𝐺dom DProd 𝑠 ∧ (𝐺 DProd 𝑠) = 𝐵)) → 𝑠:dom 𝑠𝐶)
76ffvelcdmda 7098 . . . . . . . . 9 ((((𝜑𝑠 ∈ Word 𝐶) ∧ (𝐺dom DProd 𝑠 ∧ (𝐺 DProd 𝑠) = 𝐵)) ∧ 𝑘 ∈ dom 𝑠) → (𝑠𝑘) ∈ 𝐶)
8 oveq2 7432 . . . . . . . . . . . 12 (𝑟 = (𝑠𝑘) → (𝐺s 𝑟) = (𝐺s (𝑠𝑘)))
98eleq1d 2811 . . . . . . . . . . 11 (𝑟 = (𝑠𝑘) → ((𝐺s 𝑟) ∈ (CycGrp ∩ ran pGrp ) ↔ (𝐺s (𝑠𝑘)) ∈ (CycGrp ∩ ran pGrp )))
10 ablfac.c . . . . . . . . . . 11 𝐶 = {𝑟 ∈ (SubGrp‘𝐺) ∣ (𝐺s 𝑟) ∈ (CycGrp ∩ ran pGrp )}
119, 10elrab2 3684 . . . . . . . . . 10 ((𝑠𝑘) ∈ 𝐶 ↔ ((𝑠𝑘) ∈ (SubGrp‘𝐺) ∧ (𝐺s (𝑠𝑘)) ∈ (CycGrp ∩ ran pGrp )))
1211simplbi 496 . . . . . . . . 9 ((𝑠𝑘) ∈ 𝐶 → (𝑠𝑘) ∈ (SubGrp‘𝐺))
137, 12syl 17 . . . . . . . 8 ((((𝜑𝑠 ∈ Word 𝐶) ∧ (𝐺dom DProd 𝑠 ∧ (𝐺 DProd 𝑠) = 𝐵)) ∧ 𝑘 ∈ dom 𝑠) → (𝑠𝑘) ∈ (SubGrp‘𝐺))
14 ablfac.b . . . . . . . . 9 𝐵 = (Base‘𝐺)
1514subgss 19121 . . . . . . . 8 ((𝑠𝑘) ∈ (SubGrp‘𝐺) → (𝑠𝑘) ⊆ 𝐵)
1613, 15syl 17 . . . . . . 7 ((((𝜑𝑠 ∈ Word 𝐶) ∧ (𝐺dom DProd 𝑠 ∧ (𝐺 DProd 𝑠) = 𝐵)) ∧ 𝑘 ∈ dom 𝑠) → (𝑠𝑘) ⊆ 𝐵)
1711simprbi 495 . . . . . . . . . . . 12 ((𝑠𝑘) ∈ 𝐶 → (𝐺s (𝑠𝑘)) ∈ (CycGrp ∩ ran pGrp ))
187, 17syl 17 . . . . . . . . . . 11 ((((𝜑𝑠 ∈ Word 𝐶) ∧ (𝐺dom DProd 𝑠 ∧ (𝐺 DProd 𝑠) = 𝐵)) ∧ 𝑘 ∈ dom 𝑠) → (𝐺s (𝑠𝑘)) ∈ (CycGrp ∩ ran pGrp ))
1918elin1d 4199 . . . . . . . . . 10 ((((𝜑𝑠 ∈ Word 𝐶) ∧ (𝐺dom DProd 𝑠 ∧ (𝐺 DProd 𝑠) = 𝐵)) ∧ 𝑘 ∈ dom 𝑠) → (𝐺s (𝑠𝑘)) ∈ CycGrp)
20 eqid 2726 . . . . . . . . . . . 12 (Base‘(𝐺s (𝑠𝑘))) = (Base‘(𝐺s (𝑠𝑘)))
21 eqid 2726 . . . . . . . . . . . 12 (.g‘(𝐺s (𝑠𝑘))) = (.g‘(𝐺s (𝑠𝑘)))
2220, 21iscyg 19877 . . . . . . . . . . 11 ((𝐺s (𝑠𝑘)) ∈ CycGrp ↔ ((𝐺s (𝑠𝑘)) ∈ Grp ∧ ∃𝑥 ∈ (Base‘(𝐺s (𝑠𝑘)))ran (𝑛 ∈ ℤ ↦ (𝑛(.g‘(𝐺s (𝑠𝑘)))𝑥)) = (Base‘(𝐺s (𝑠𝑘)))))
2322simprbi 495 . . . . . . . . . 10 ((𝐺s (𝑠𝑘)) ∈ CycGrp → ∃𝑥 ∈ (Base‘(𝐺s (𝑠𝑘)))ran (𝑛 ∈ ℤ ↦ (𝑛(.g‘(𝐺s (𝑠𝑘)))𝑥)) = (Base‘(𝐺s (𝑠𝑘))))
2419, 23syl 17 . . . . . . . . 9 ((((𝜑𝑠 ∈ Word 𝐶) ∧ (𝐺dom DProd 𝑠 ∧ (𝐺 DProd 𝑠) = 𝐵)) ∧ 𝑘 ∈ dom 𝑠) → ∃𝑥 ∈ (Base‘(𝐺s (𝑠𝑘)))ran (𝑛 ∈ ℤ ↦ (𝑛(.g‘(𝐺s (𝑠𝑘)))𝑥)) = (Base‘(𝐺s (𝑠𝑘))))
25 eqid 2726 . . . . . . . . . . . 12 (𝐺s (𝑠𝑘)) = (𝐺s (𝑠𝑘))
2625subgbas 19124 . . . . . . . . . . 11 ((𝑠𝑘) ∈ (SubGrp‘𝐺) → (𝑠𝑘) = (Base‘(𝐺s (𝑠𝑘))))
2713, 26syl 17 . . . . . . . . . 10 ((((𝜑𝑠 ∈ Word 𝐶) ∧ (𝐺dom DProd 𝑠 ∧ (𝐺 DProd 𝑠) = 𝐵)) ∧ 𝑘 ∈ dom 𝑠) → (𝑠𝑘) = (Base‘(𝐺s (𝑠𝑘))))
2827rexeqdv 3316 . . . . . . . . 9 ((((𝜑𝑠 ∈ Word 𝐶) ∧ (𝐺dom DProd 𝑠 ∧ (𝐺 DProd 𝑠) = 𝐵)) ∧ 𝑘 ∈ dom 𝑠) → (∃𝑥 ∈ (𝑠𝑘)ran (𝑛 ∈ ℤ ↦ (𝑛(.g‘(𝐺s (𝑠𝑘)))𝑥)) = (Base‘(𝐺s (𝑠𝑘))) ↔ ∃𝑥 ∈ (Base‘(𝐺s (𝑠𝑘)))ran (𝑛 ∈ ℤ ↦ (𝑛(.g‘(𝐺s (𝑠𝑘)))𝑥)) = (Base‘(𝐺s (𝑠𝑘)))))
2924, 28mpbird 256 . . . . . . . 8 ((((𝜑𝑠 ∈ Word 𝐶) ∧ (𝐺dom DProd 𝑠 ∧ (𝐺 DProd 𝑠) = 𝐵)) ∧ 𝑘 ∈ dom 𝑠) → ∃𝑥 ∈ (𝑠𝑘)ran (𝑛 ∈ ℤ ↦ (𝑛(.g‘(𝐺s (𝑠𝑘)))𝑥)) = (Base‘(𝐺s (𝑠𝑘))))
3013ad2antrr 724 . . . . . . . . . . . . 13 ((((((𝜑𝑠 ∈ Word 𝐶) ∧ (𝐺dom DProd 𝑠 ∧ (𝐺 DProd 𝑠) = 𝐵)) ∧ 𝑘 ∈ dom 𝑠) ∧ 𝑥 ∈ (𝑠𝑘)) ∧ 𝑛 ∈ ℤ) → (𝑠𝑘) ∈ (SubGrp‘𝐺))
31 simpr 483 . . . . . . . . . . . . 13 ((((((𝜑𝑠 ∈ Word 𝐶) ∧ (𝐺dom DProd 𝑠 ∧ (𝐺 DProd 𝑠) = 𝐵)) ∧ 𝑘 ∈ dom 𝑠) ∧ 𝑥 ∈ (𝑠𝑘)) ∧ 𝑛 ∈ ℤ) → 𝑛 ∈ ℤ)
32 simplr 767 . . . . . . . . . . . . 13 ((((((𝜑𝑠 ∈ Word 𝐶) ∧ (𝐺dom DProd 𝑠 ∧ (𝐺 DProd 𝑠) = 𝐵)) ∧ 𝑘 ∈ dom 𝑠) ∧ 𝑥 ∈ (𝑠𝑘)) ∧ 𝑛 ∈ ℤ) → 𝑥 ∈ (𝑠𝑘))
33 ablfac2.m . . . . . . . . . . . . . 14 · = (.g𝐺)
3433, 25, 21subgmulg 19134 . . . . . . . . . . . . 13 (((𝑠𝑘) ∈ (SubGrp‘𝐺) ∧ 𝑛 ∈ ℤ ∧ 𝑥 ∈ (𝑠𝑘)) → (𝑛 · 𝑥) = (𝑛(.g‘(𝐺s (𝑠𝑘)))𝑥))
3530, 31, 32, 34syl3anc 1368 . . . . . . . . . . . 12 ((((((𝜑𝑠 ∈ Word 𝐶) ∧ (𝐺dom DProd 𝑠 ∧ (𝐺 DProd 𝑠) = 𝐵)) ∧ 𝑘 ∈ dom 𝑠) ∧ 𝑥 ∈ (𝑠𝑘)) ∧ 𝑛 ∈ ℤ) → (𝑛 · 𝑥) = (𝑛(.g‘(𝐺s (𝑠𝑘)))𝑥))
3635mpteq2dva 5253 . . . . . . . . . . 11 (((((𝜑𝑠 ∈ Word 𝐶) ∧ (𝐺dom DProd 𝑠 ∧ (𝐺 DProd 𝑠) = 𝐵)) ∧ 𝑘 ∈ dom 𝑠) ∧ 𝑥 ∈ (𝑠𝑘)) → (𝑛 ∈ ℤ ↦ (𝑛 · 𝑥)) = (𝑛 ∈ ℤ ↦ (𝑛(.g‘(𝐺s (𝑠𝑘)))𝑥)))
3736rneqd 5944 . . . . . . . . . 10 (((((𝜑𝑠 ∈ Word 𝐶) ∧ (𝐺dom DProd 𝑠 ∧ (𝐺 DProd 𝑠) = 𝐵)) ∧ 𝑘 ∈ dom 𝑠) ∧ 𝑥 ∈ (𝑠𝑘)) → ran (𝑛 ∈ ℤ ↦ (𝑛 · 𝑥)) = ran (𝑛 ∈ ℤ ↦ (𝑛(.g‘(𝐺s (𝑠𝑘)))𝑥)))
3827adantr 479 . . . . . . . . . 10 (((((𝜑𝑠 ∈ Word 𝐶) ∧ (𝐺dom DProd 𝑠 ∧ (𝐺 DProd 𝑠) = 𝐵)) ∧ 𝑘 ∈ dom 𝑠) ∧ 𝑥 ∈ (𝑠𝑘)) → (𝑠𝑘) = (Base‘(𝐺s (𝑠𝑘))))
3937, 38eqeq12d 2742 . . . . . . . . 9 (((((𝜑𝑠 ∈ Word 𝐶) ∧ (𝐺dom DProd 𝑠 ∧ (𝐺 DProd 𝑠) = 𝐵)) ∧ 𝑘 ∈ dom 𝑠) ∧ 𝑥 ∈ (𝑠𝑘)) → (ran (𝑛 ∈ ℤ ↦ (𝑛 · 𝑥)) = (𝑠𝑘) ↔ ran (𝑛 ∈ ℤ ↦ (𝑛(.g‘(𝐺s (𝑠𝑘)))𝑥)) = (Base‘(𝐺s (𝑠𝑘)))))
4039rexbidva 3167 . . . . . . . 8 ((((𝜑𝑠 ∈ Word 𝐶) ∧ (𝐺dom DProd 𝑠 ∧ (𝐺 DProd 𝑠) = 𝐵)) ∧ 𝑘 ∈ dom 𝑠) → (∃𝑥 ∈ (𝑠𝑘)ran (𝑛 ∈ ℤ ↦ (𝑛 · 𝑥)) = (𝑠𝑘) ↔ ∃𝑥 ∈ (𝑠𝑘)ran (𝑛 ∈ ℤ ↦ (𝑛(.g‘(𝐺s (𝑠𝑘)))𝑥)) = (Base‘(𝐺s (𝑠𝑘)))))
4129, 40mpbird 256 . . . . . . 7 ((((𝜑𝑠 ∈ Word 𝐶) ∧ (𝐺dom DProd 𝑠 ∧ (𝐺 DProd 𝑠) = 𝐵)) ∧ 𝑘 ∈ dom 𝑠) → ∃𝑥 ∈ (𝑠𝑘)ran (𝑛 ∈ ℤ ↦ (𝑛 · 𝑥)) = (𝑠𝑘))
42 ssrexv 4049 . . . . . . 7 ((𝑠𝑘) ⊆ 𝐵 → (∃𝑥 ∈ (𝑠𝑘)ran (𝑛 ∈ ℤ ↦ (𝑛 · 𝑥)) = (𝑠𝑘) → ∃𝑥𝐵 ran (𝑛 ∈ ℤ ↦ (𝑛 · 𝑥)) = (𝑠𝑘)))
4316, 41, 42sylc 65 . . . . . 6 ((((𝜑𝑠 ∈ Word 𝐶) ∧ (𝐺dom DProd 𝑠 ∧ (𝐺 DProd 𝑠) = 𝐵)) ∧ 𝑘 ∈ dom 𝑠) → ∃𝑥𝐵 ran (𝑛 ∈ ℤ ↦ (𝑛 · 𝑥)) = (𝑠𝑘))
4443ralrimiva 3136 . . . . 5 (((𝜑𝑠 ∈ Word 𝐶) ∧ (𝐺dom DProd 𝑠 ∧ (𝐺 DProd 𝑠) = 𝐵)) → ∀𝑘 ∈ dom 𝑠𝑥𝐵 ran (𝑛 ∈ ℤ ↦ (𝑛 · 𝑥)) = (𝑠𝑘))
45 oveq2 7432 . . . . . . . . 9 (𝑥 = (𝑤𝑘) → (𝑛 · 𝑥) = (𝑛 · (𝑤𝑘)))
4645mpteq2dv 5255 . . . . . . . 8 (𝑥 = (𝑤𝑘) → (𝑛 ∈ ℤ ↦ (𝑛 · 𝑥)) = (𝑛 ∈ ℤ ↦ (𝑛 · (𝑤𝑘))))
4746rneqd 5944 . . . . . . 7 (𝑥 = (𝑤𝑘) → ran (𝑛 ∈ ℤ ↦ (𝑛 · 𝑥)) = ran (𝑛 ∈ ℤ ↦ (𝑛 · (𝑤𝑘))))
4847eqeq1d 2728 . . . . . 6 (𝑥 = (𝑤𝑘) → (ran (𝑛 ∈ ℤ ↦ (𝑛 · 𝑥)) = (𝑠𝑘) ↔ ran (𝑛 ∈ ℤ ↦ (𝑛 · (𝑤𝑘))) = (𝑠𝑘)))
4948ac6sfi 9321 . . . . 5 ((dom 𝑠 ∈ Fin ∧ ∀𝑘 ∈ dom 𝑠𝑥𝐵 ran (𝑛 ∈ ℤ ↦ (𝑛 · 𝑥)) = (𝑠𝑘)) → ∃𝑤(𝑤:dom 𝑠𝐵 ∧ ∀𝑘 ∈ dom 𝑠ran (𝑛 ∈ ℤ ↦ (𝑛 · (𝑤𝑘))) = (𝑠𝑘)))
505, 44, 49syl2anc 582 . . . 4 (((𝜑𝑠 ∈ Word 𝐶) ∧ (𝐺dom DProd 𝑠 ∧ (𝐺 DProd 𝑠) = 𝐵)) → ∃𝑤(𝑤:dom 𝑠𝐵 ∧ ∀𝑘 ∈ dom 𝑠ran (𝑛 ∈ ℤ ↦ (𝑛 · (𝑤𝑘))) = (𝑠𝑘)))
51 simprl 769 . . . . . . . . 9 ((((𝜑𝑠 ∈ Word 𝐶) ∧ (𝐺dom DProd 𝑠 ∧ (𝐺 DProd 𝑠) = 𝐵)) ∧ (𝑤:dom 𝑠𝐵 ∧ ∀𝑘 ∈ dom 𝑠ran (𝑛 ∈ ℤ ↦ (𝑛 · (𝑤𝑘))) = (𝑠𝑘))) → 𝑤:dom 𝑠𝐵)
523adantr 479 . . . . . . . . . 10 ((((𝜑𝑠 ∈ Word 𝐶) ∧ (𝐺dom DProd 𝑠 ∧ (𝐺 DProd 𝑠) = 𝐵)) ∧ (𝑤:dom 𝑠𝐵 ∧ ∀𝑘 ∈ dom 𝑠ran (𝑛 ∈ ℤ ↦ (𝑛 · (𝑤𝑘))) = (𝑠𝑘))) → dom 𝑠 = (0..^(♯‘𝑠)))
5352feq2d 6714 . . . . . . . . 9 ((((𝜑𝑠 ∈ Word 𝐶) ∧ (𝐺dom DProd 𝑠 ∧ (𝐺 DProd 𝑠) = 𝐵)) ∧ (𝑤:dom 𝑠𝐵 ∧ ∀𝑘 ∈ dom 𝑠ran (𝑛 ∈ ℤ ↦ (𝑛 · (𝑤𝑘))) = (𝑠𝑘))) → (𝑤:dom 𝑠𝐵𝑤:(0..^(♯‘𝑠))⟶𝐵))
5451, 53mpbid 231 . . . . . . . 8 ((((𝜑𝑠 ∈ Word 𝐶) ∧ (𝐺dom DProd 𝑠 ∧ (𝐺 DProd 𝑠) = 𝐵)) ∧ (𝑤:dom 𝑠𝐵 ∧ ∀𝑘 ∈ dom 𝑠ran (𝑛 ∈ ℤ ↦ (𝑛 · (𝑤𝑘))) = (𝑠𝑘))) → 𝑤:(0..^(♯‘𝑠))⟶𝐵)
55 iswrdi 14526 . . . . . . . 8 (𝑤:(0..^(♯‘𝑠))⟶𝐵𝑤 ∈ Word 𝐵)
5654, 55syl 17 . . . . . . 7 ((((𝜑𝑠 ∈ Word 𝐶) ∧ (𝐺dom DProd 𝑠 ∧ (𝐺 DProd 𝑠) = 𝐵)) ∧ (𝑤:dom 𝑠𝐵 ∧ ∀𝑘 ∈ dom 𝑠ran (𝑛 ∈ ℤ ↦ (𝑛 · (𝑤𝑘))) = (𝑠𝑘))) → 𝑤 ∈ Word 𝐵)
5751fdmd 6738 . . . . . . . . . . . 12 ((((𝜑𝑠 ∈ Word 𝐶) ∧ (𝐺dom DProd 𝑠 ∧ (𝐺 DProd 𝑠) = 𝐵)) ∧ (𝑤:dom 𝑠𝐵 ∧ ∀𝑘 ∈ dom 𝑠ran (𝑛 ∈ ℤ ↦ (𝑛 · (𝑤𝑘))) = (𝑠𝑘))) → dom 𝑤 = dom 𝑠)
5857eleq2d 2812 . . . . . . . . . . 11 ((((𝜑𝑠 ∈ Word 𝐶) ∧ (𝐺dom DProd 𝑠 ∧ (𝐺 DProd 𝑠) = 𝐵)) ∧ (𝑤:dom 𝑠𝐵 ∧ ∀𝑘 ∈ dom 𝑠ran (𝑛 ∈ ℤ ↦ (𝑛 · (𝑤𝑘))) = (𝑠𝑘))) → (𝑗 ∈ dom 𝑤𝑗 ∈ dom 𝑠))
5958biimpa 475 . . . . . . . . . 10 (((((𝜑𝑠 ∈ Word 𝐶) ∧ (𝐺dom DProd 𝑠 ∧ (𝐺 DProd 𝑠) = 𝐵)) ∧ (𝑤:dom 𝑠𝐵 ∧ ∀𝑘 ∈ dom 𝑠ran (𝑛 ∈ ℤ ↦ (𝑛 · (𝑤𝑘))) = (𝑠𝑘))) ∧ 𝑗 ∈ dom 𝑤) → 𝑗 ∈ dom 𝑠)
60 simprr 771 . . . . . . . . . . . 12 ((((𝜑𝑠 ∈ Word 𝐶) ∧ (𝐺dom DProd 𝑠 ∧ (𝐺 DProd 𝑠) = 𝐵)) ∧ (𝑤:dom 𝑠𝐵 ∧ ∀𝑘 ∈ dom 𝑠ran (𝑛 ∈ ℤ ↦ (𝑛 · (𝑤𝑘))) = (𝑠𝑘))) → ∀𝑘 ∈ dom 𝑠ran (𝑛 ∈ ℤ ↦ (𝑛 · (𝑤𝑘))) = (𝑠𝑘))
61 simpl 481 . . . . . . . . . . . . . . . . . 18 ((𝑘 = 𝑗𝑛 ∈ ℤ) → 𝑘 = 𝑗)
6261fveq2d 6905 . . . . . . . . . . . . . . . . 17 ((𝑘 = 𝑗𝑛 ∈ ℤ) → (𝑤𝑘) = (𝑤𝑗))
6362oveq2d 7440 . . . . . . . . . . . . . . . 16 ((𝑘 = 𝑗𝑛 ∈ ℤ) → (𝑛 · (𝑤𝑘)) = (𝑛 · (𝑤𝑗)))
6463mpteq2dva 5253 . . . . . . . . . . . . . . 15 (𝑘 = 𝑗 → (𝑛 ∈ ℤ ↦ (𝑛 · (𝑤𝑘))) = (𝑛 ∈ ℤ ↦ (𝑛 · (𝑤𝑗))))
6564rneqd 5944 . . . . . . . . . . . . . 14 (𝑘 = 𝑗 → ran (𝑛 ∈ ℤ ↦ (𝑛 · (𝑤𝑘))) = ran (𝑛 ∈ ℤ ↦ (𝑛 · (𝑤𝑗))))
66 fveq2 6901 . . . . . . . . . . . . . 14 (𝑘 = 𝑗 → (𝑠𝑘) = (𝑠𝑗))
6765, 66eqeq12d 2742 . . . . . . . . . . . . 13 (𝑘 = 𝑗 → (ran (𝑛 ∈ ℤ ↦ (𝑛 · (𝑤𝑘))) = (𝑠𝑘) ↔ ran (𝑛 ∈ ℤ ↦ (𝑛 · (𝑤𝑗))) = (𝑠𝑗)))
6867rspccva 3607 . . . . . . . . . . . 12 ((∀𝑘 ∈ dom 𝑠ran (𝑛 ∈ ℤ ↦ (𝑛 · (𝑤𝑘))) = (𝑠𝑘) ∧ 𝑗 ∈ dom 𝑠) → ran (𝑛 ∈ ℤ ↦ (𝑛 · (𝑤𝑗))) = (𝑠𝑗))
6960, 68sylan 578 . . . . . . . . . . 11 (((((𝜑𝑠 ∈ Word 𝐶) ∧ (𝐺dom DProd 𝑠 ∧ (𝐺 DProd 𝑠) = 𝐵)) ∧ (𝑤:dom 𝑠𝐵 ∧ ∀𝑘 ∈ dom 𝑠ran (𝑛 ∈ ℤ ↦ (𝑛 · (𝑤𝑘))) = (𝑠𝑘))) ∧ 𝑗 ∈ dom 𝑠) → ran (𝑛 ∈ ℤ ↦ (𝑛 · (𝑤𝑗))) = (𝑠𝑗))
706adantr 479 . . . . . . . . . . . 12 ((((𝜑𝑠 ∈ Word 𝐶) ∧ (𝐺dom DProd 𝑠 ∧ (𝐺 DProd 𝑠) = 𝐵)) ∧ (𝑤:dom 𝑠𝐵 ∧ ∀𝑘 ∈ dom 𝑠ran (𝑛 ∈ ℤ ↦ (𝑛 · (𝑤𝑘))) = (𝑠𝑘))) → 𝑠:dom 𝑠𝐶)
7170ffvelcdmda 7098 . . . . . . . . . . 11 (((((𝜑𝑠 ∈ Word 𝐶) ∧ (𝐺dom DProd 𝑠 ∧ (𝐺 DProd 𝑠) = 𝐵)) ∧ (𝑤:dom 𝑠𝐵 ∧ ∀𝑘 ∈ dom 𝑠ran (𝑛 ∈ ℤ ↦ (𝑛 · (𝑤𝑘))) = (𝑠𝑘))) ∧ 𝑗 ∈ dom 𝑠) → (𝑠𝑗) ∈ 𝐶)
7269, 71eqeltrd 2826 . . . . . . . . . 10 (((((𝜑𝑠 ∈ Word 𝐶) ∧ (𝐺dom DProd 𝑠 ∧ (𝐺 DProd 𝑠) = 𝐵)) ∧ (𝑤:dom 𝑠𝐵 ∧ ∀𝑘 ∈ dom 𝑠ran (𝑛 ∈ ℤ ↦ (𝑛 · (𝑤𝑘))) = (𝑠𝑘))) ∧ 𝑗 ∈ dom 𝑠) → ran (𝑛 ∈ ℤ ↦ (𝑛 · (𝑤𝑗))) ∈ 𝐶)
7359, 72syldan 589 . . . . . . . . 9 (((((𝜑𝑠 ∈ Word 𝐶) ∧ (𝐺dom DProd 𝑠 ∧ (𝐺 DProd 𝑠) = 𝐵)) ∧ (𝑤:dom 𝑠𝐵 ∧ ∀𝑘 ∈ dom 𝑠ran (𝑛 ∈ ℤ ↦ (𝑛 · (𝑤𝑘))) = (𝑠𝑘))) ∧ 𝑗 ∈ dom 𝑤) → ran (𝑛 ∈ ℤ ↦ (𝑛 · (𝑤𝑗))) ∈ 𝐶)
74 ablfac2.s . . . . . . . . . 10 𝑆 = (𝑘 ∈ dom 𝑤 ↦ ran (𝑛 ∈ ℤ ↦ (𝑛 · (𝑤𝑘))))
75 fveq2 6901 . . . . . . . . . . . . . 14 (𝑘 = 𝑗 → (𝑤𝑘) = (𝑤𝑗))
7675oveq2d 7440 . . . . . . . . . . . . 13 (𝑘 = 𝑗 → (𝑛 · (𝑤𝑘)) = (𝑛 · (𝑤𝑗)))
7776mpteq2dv 5255 . . . . . . . . . . . 12 (𝑘 = 𝑗 → (𝑛 ∈ ℤ ↦ (𝑛 · (𝑤𝑘))) = (𝑛 ∈ ℤ ↦ (𝑛 · (𝑤𝑗))))
7877rneqd 5944 . . . . . . . . . . 11 (𝑘 = 𝑗 → ran (𝑛 ∈ ℤ ↦ (𝑛 · (𝑤𝑘))) = ran (𝑛 ∈ ℤ ↦ (𝑛 · (𝑤𝑗))))
7978cbvmptv 5266 . . . . . . . . . 10 (𝑘 ∈ dom 𝑤 ↦ ran (𝑛 ∈ ℤ ↦ (𝑛 · (𝑤𝑘)))) = (𝑗 ∈ dom 𝑤 ↦ ran (𝑛 ∈ ℤ ↦ (𝑛 · (𝑤𝑗))))
8074, 79eqtri 2754 . . . . . . . . 9 𝑆 = (𝑗 ∈ dom 𝑤 ↦ ran (𝑛 ∈ ℤ ↦ (𝑛 · (𝑤𝑗))))
8173, 80fmptd 7128 . . . . . . . 8 ((((𝜑𝑠 ∈ Word 𝐶) ∧ (𝐺dom DProd 𝑠 ∧ (𝐺 DProd 𝑠) = 𝐵)) ∧ (𝑤:dom 𝑠𝐵 ∧ ∀𝑘 ∈ dom 𝑠ran (𝑛 ∈ ℤ ↦ (𝑛 · (𝑤𝑘))) = (𝑠𝑘))) → 𝑆:dom 𝑤𝐶)
82 simprl 769 . . . . . . . . . 10 (((𝜑𝑠 ∈ Word 𝐶) ∧ (𝐺dom DProd 𝑠 ∧ (𝐺 DProd 𝑠) = 𝐵)) → 𝐺dom DProd 𝑠)
8382adantr 479 . . . . . . . . 9 ((((𝜑𝑠 ∈ Word 𝐶) ∧ (𝐺dom DProd 𝑠 ∧ (𝐺 DProd 𝑠) = 𝐵)) ∧ (𝑤:dom 𝑠𝐵 ∧ ∀𝑘 ∈ dom 𝑠ran (𝑛 ∈ ℤ ↦ (𝑛 · (𝑤𝑘))) = (𝑠𝑘))) → 𝐺dom DProd 𝑠)
8457raleqdv 3315 . . . . . . . . . . . . 13 ((((𝜑𝑠 ∈ Word 𝐶) ∧ (𝐺dom DProd 𝑠 ∧ (𝐺 DProd 𝑠) = 𝐵)) ∧ (𝑤:dom 𝑠𝐵 ∧ ∀𝑘 ∈ dom 𝑠ran (𝑛 ∈ ℤ ↦ (𝑛 · (𝑤𝑘))) = (𝑠𝑘))) → (∀𝑘 ∈ dom 𝑤ran (𝑛 ∈ ℤ ↦ (𝑛 · (𝑤𝑘))) = (𝑠𝑘) ↔ ∀𝑘 ∈ dom 𝑠ran (𝑛 ∈ ℤ ↦ (𝑛 · (𝑤𝑘))) = (𝑠𝑘)))
8560, 84mpbird 256 . . . . . . . . . . . 12 ((((𝜑𝑠 ∈ Word 𝐶) ∧ (𝐺dom DProd 𝑠 ∧ (𝐺 DProd 𝑠) = 𝐵)) ∧ (𝑤:dom 𝑠𝐵 ∧ ∀𝑘 ∈ dom 𝑠ran (𝑛 ∈ ℤ ↦ (𝑛 · (𝑤𝑘))) = (𝑠𝑘))) → ∀𝑘 ∈ dom 𝑤ran (𝑛 ∈ ℤ ↦ (𝑛 · (𝑤𝑘))) = (𝑠𝑘))
86 mpteq12 5245 . . . . . . . . . . . 12 ((dom 𝑤 = dom 𝑠 ∧ ∀𝑘 ∈ dom 𝑤ran (𝑛 ∈ ℤ ↦ (𝑛 · (𝑤𝑘))) = (𝑠𝑘)) → (𝑘 ∈ dom 𝑤 ↦ ran (𝑛 ∈ ℤ ↦ (𝑛 · (𝑤𝑘)))) = (𝑘 ∈ dom 𝑠 ↦ (𝑠𝑘)))
8757, 85, 86syl2anc 582 . . . . . . . . . . 11 ((((𝜑𝑠 ∈ Word 𝐶) ∧ (𝐺dom DProd 𝑠 ∧ (𝐺 DProd 𝑠) = 𝐵)) ∧ (𝑤:dom 𝑠𝐵 ∧ ∀𝑘 ∈ dom 𝑠ran (𝑛 ∈ ℤ ↦ (𝑛 · (𝑤𝑘))) = (𝑠𝑘))) → (𝑘 ∈ dom 𝑤 ↦ ran (𝑛 ∈ ℤ ↦ (𝑛 · (𝑤𝑘)))) = (𝑘 ∈ dom 𝑠 ↦ (𝑠𝑘)))
8874, 87eqtrid 2778 . . . . . . . . . 10 ((((𝜑𝑠 ∈ Word 𝐶) ∧ (𝐺dom DProd 𝑠 ∧ (𝐺 DProd 𝑠) = 𝐵)) ∧ (𝑤:dom 𝑠𝐵 ∧ ∀𝑘 ∈ dom 𝑠ran (𝑛 ∈ ℤ ↦ (𝑛 · (𝑤𝑘))) = (𝑠𝑘))) → 𝑆 = (𝑘 ∈ dom 𝑠 ↦ (𝑠𝑘)))
89 dprdf 20006 . . . . . . . . . . . 12 (𝐺dom DProd 𝑠𝑠:dom 𝑠⟶(SubGrp‘𝐺))
9083, 89syl 17 . . . . . . . . . . 11 ((((𝜑𝑠 ∈ Word 𝐶) ∧ (𝐺dom DProd 𝑠 ∧ (𝐺 DProd 𝑠) = 𝐵)) ∧ (𝑤:dom 𝑠𝐵 ∧ ∀𝑘 ∈ dom 𝑠ran (𝑛 ∈ ℤ ↦ (𝑛 · (𝑤𝑘))) = (𝑠𝑘))) → 𝑠:dom 𝑠⟶(SubGrp‘𝐺))
9190feqmptd 6971 . . . . . . . . . 10 ((((𝜑𝑠 ∈ Word 𝐶) ∧ (𝐺dom DProd 𝑠 ∧ (𝐺 DProd 𝑠) = 𝐵)) ∧ (𝑤:dom 𝑠𝐵 ∧ ∀𝑘 ∈ dom 𝑠ran (𝑛 ∈ ℤ ↦ (𝑛 · (𝑤𝑘))) = (𝑠𝑘))) → 𝑠 = (𝑘 ∈ dom 𝑠 ↦ (𝑠𝑘)))
9288, 91eqtr4d 2769 . . . . . . . . 9 ((((𝜑𝑠 ∈ Word 𝐶) ∧ (𝐺dom DProd 𝑠 ∧ (𝐺 DProd 𝑠) = 𝐵)) ∧ (𝑤:dom 𝑠𝐵 ∧ ∀𝑘 ∈ dom 𝑠ran (𝑛 ∈ ℤ ↦ (𝑛 · (𝑤𝑘))) = (𝑠𝑘))) → 𝑆 = 𝑠)
9383, 92breqtrrd 5181 . . . . . . . 8 ((((𝜑𝑠 ∈ Word 𝐶) ∧ (𝐺dom DProd 𝑠 ∧ (𝐺 DProd 𝑠) = 𝐵)) ∧ (𝑤:dom 𝑠𝐵 ∧ ∀𝑘 ∈ dom 𝑠ran (𝑛 ∈ ℤ ↦ (𝑛 · (𝑤𝑘))) = (𝑠𝑘))) → 𝐺dom DProd 𝑆)
9492oveq2d 7440 . . . . . . . . 9 ((((𝜑𝑠 ∈ Word 𝐶) ∧ (𝐺dom DProd 𝑠 ∧ (𝐺 DProd 𝑠) = 𝐵)) ∧ (𝑤:dom 𝑠𝐵 ∧ ∀𝑘 ∈ dom 𝑠ran (𝑛 ∈ ℤ ↦ (𝑛 · (𝑤𝑘))) = (𝑠𝑘))) → (𝐺 DProd 𝑆) = (𝐺 DProd 𝑠))
95 simplrr 776 . . . . . . . . 9 ((((𝜑𝑠 ∈ Word 𝐶) ∧ (𝐺dom DProd 𝑠 ∧ (𝐺 DProd 𝑠) = 𝐵)) ∧ (𝑤:dom 𝑠𝐵 ∧ ∀𝑘 ∈ dom 𝑠ran (𝑛 ∈ ℤ ↦ (𝑛 · (𝑤𝑘))) = (𝑠𝑘))) → (𝐺 DProd 𝑠) = 𝐵)
9694, 95eqtrd 2766 . . . . . . . 8 ((((𝜑𝑠 ∈ Word 𝐶) ∧ (𝐺dom DProd 𝑠 ∧ (𝐺 DProd 𝑠) = 𝐵)) ∧ (𝑤:dom 𝑠𝐵 ∧ ∀𝑘 ∈ dom 𝑠ran (𝑛 ∈ ℤ ↦ (𝑛 · (𝑤𝑘))) = (𝑠𝑘))) → (𝐺 DProd 𝑆) = 𝐵)
9781, 93, 963jca 1125 . . . . . . 7 ((((𝜑𝑠 ∈ Word 𝐶) ∧ (𝐺dom DProd 𝑠 ∧ (𝐺 DProd 𝑠) = 𝐵)) ∧ (𝑤:dom 𝑠𝐵 ∧ ∀𝑘 ∈ dom 𝑠ran (𝑛 ∈ ℤ ↦ (𝑛 · (𝑤𝑘))) = (𝑠𝑘))) → (𝑆:dom 𝑤𝐶𝐺dom DProd 𝑆 ∧ (𝐺 DProd 𝑆) = 𝐵))
9856, 97jca 510 . . . . . 6 ((((𝜑𝑠 ∈ Word 𝐶) ∧ (𝐺dom DProd 𝑠 ∧ (𝐺 DProd 𝑠) = 𝐵)) ∧ (𝑤:dom 𝑠𝐵 ∧ ∀𝑘 ∈ dom 𝑠ran (𝑛 ∈ ℤ ↦ (𝑛 · (𝑤𝑘))) = (𝑠𝑘))) → (𝑤 ∈ Word 𝐵 ∧ (𝑆:dom 𝑤𝐶𝐺dom DProd 𝑆 ∧ (𝐺 DProd 𝑆) = 𝐵)))
9998ex 411 . . . . 5 (((𝜑𝑠 ∈ Word 𝐶) ∧ (𝐺dom DProd 𝑠 ∧ (𝐺 DProd 𝑠) = 𝐵)) → ((𝑤:dom 𝑠𝐵 ∧ ∀𝑘 ∈ dom 𝑠ran (𝑛 ∈ ℤ ↦ (𝑛 · (𝑤𝑘))) = (𝑠𝑘)) → (𝑤 ∈ Word 𝐵 ∧ (𝑆:dom 𝑤𝐶𝐺dom DProd 𝑆 ∧ (𝐺 DProd 𝑆) = 𝐵))))
10099eximdv 1913 . . . 4 (((𝜑𝑠 ∈ Word 𝐶) ∧ (𝐺dom DProd 𝑠 ∧ (𝐺 DProd 𝑠) = 𝐵)) → (∃𝑤(𝑤:dom 𝑠𝐵 ∧ ∀𝑘 ∈ dom 𝑠ran (𝑛 ∈ ℤ ↦ (𝑛 · (𝑤𝑘))) = (𝑠𝑘)) → ∃𝑤(𝑤 ∈ Word 𝐵 ∧ (𝑆:dom 𝑤𝐶𝐺dom DProd 𝑆 ∧ (𝐺 DProd 𝑆) = 𝐵))))
10150, 100mpd 15 . . 3 (((𝜑𝑠 ∈ Word 𝐶) ∧ (𝐺dom DProd 𝑠 ∧ (𝐺 DProd 𝑠) = 𝐵)) → ∃𝑤(𝑤 ∈ Word 𝐵 ∧ (𝑆:dom 𝑤𝐶𝐺dom DProd 𝑆 ∧ (𝐺 DProd 𝑆) = 𝐵)))
102 df-rex 3061 . . 3 (∃𝑤 ∈ Word 𝐵(𝑆:dom 𝑤𝐶𝐺dom DProd 𝑆 ∧ (𝐺 DProd 𝑆) = 𝐵) ↔ ∃𝑤(𝑤 ∈ Word 𝐵 ∧ (𝑆:dom 𝑤𝐶𝐺dom DProd 𝑆 ∧ (𝐺 DProd 𝑆) = 𝐵)))
103101, 102sylibr 233 . 2 (((𝜑𝑠 ∈ Word 𝐶) ∧ (𝐺dom DProd 𝑠 ∧ (𝐺 DProd 𝑠) = 𝐵)) → ∃𝑤 ∈ Word 𝐵(𝑆:dom 𝑤𝐶𝐺dom DProd 𝑆 ∧ (𝐺 DProd 𝑆) = 𝐵))
104 ablfac.1 . . 3 (𝜑𝐺 ∈ Abel)
105 ablfac.2 . . 3 (𝜑𝐵 ∈ Fin)
10614, 10, 104, 105ablfac 20088 . 2 (𝜑 → ∃𝑠 ∈ Word 𝐶(𝐺dom DProd 𝑠 ∧ (𝐺 DProd 𝑠) = 𝐵))
107103, 106r19.29a 3152 1 (𝜑 → ∃𝑤 ∈ Word 𝐵(𝑆:dom 𝑤𝐶𝐺dom DProd 𝑆 ∧ (𝐺 DProd 𝑆) = 𝐵))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 394  w3a 1084   = wceq 1534  wex 1774  wcel 2099  wral 3051  wrex 3060  {crab 3419  cin 3946  wss 3947   class class class wbr 5153  cmpt 5236  dom cdm 5682  ran crn 5683  wf 6550  cfv 6554  (class class class)co 7424  Fincfn 8974  0cc0 11158  cz 12610  ..^cfzo 13681  chash 14347  Word cword 14522  Basecbs 17213  s cress 17242  Grpcgrp 18928  .gcmg 19061  SubGrpcsubg 19114   pGrp cpgp 19524  Abelcabl 19779  CycGrpccyg 19875   DProd cdprd 19993
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-10 2130  ax-11 2147  ax-12 2167  ax-ext 2697  ax-rep 5290  ax-sep 5304  ax-nul 5311  ax-pow 5369  ax-pr 5433  ax-un 7746  ax-inf2 9684  ax-cnex 11214  ax-resscn 11215  ax-1cn 11216  ax-icn 11217  ax-addcl 11218  ax-addrcl 11219  ax-mulcl 11220  ax-mulrcl 11221  ax-mulcom 11222  ax-addass 11223  ax-mulass 11224  ax-distr 11225  ax-i2m1 11226  ax-1ne0 11227  ax-1rid 11228  ax-rnegex 11229  ax-rrecex 11230  ax-cnre 11231  ax-pre-lttri 11232  ax-pre-lttrn 11233  ax-pre-ltadd 11234  ax-pre-mulgt0 11235  ax-pre-sup 11236
This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3or 1085  df-3an 1086  df-tru 1537  df-fal 1547  df-ex 1775  df-nf 1779  df-sb 2061  df-mo 2529  df-eu 2558  df-clab 2704  df-cleq 2718  df-clel 2803  df-nfc 2878  df-ne 2931  df-nel 3037  df-ral 3052  df-rex 3061  df-rmo 3364  df-reu 3365  df-rab 3420  df-v 3464  df-sbc 3777  df-csb 3893  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-pss 3967  df-nul 4326  df-if 4534  df-pw 4609  df-sn 4634  df-pr 4636  df-op 4640  df-uni 4914  df-int 4955  df-iun 5003  df-iin 5004  df-disj 5119  df-br 5154  df-opab 5216  df-mpt 5237  df-tr 5271  df-id 5580  df-eprel 5586  df-po 5594  df-so 5595  df-fr 5637  df-se 5638  df-we 5639  df-xp 5688  df-rel 5689  df-cnv 5690  df-co 5691  df-dm 5692  df-rn 5693  df-res 5694  df-ima 5695  df-pred 6312  df-ord 6379  df-on 6380  df-lim 6381  df-suc 6382  df-iota 6506  df-fun 6556  df-fn 6557  df-f 6558  df-f1 6559  df-fo 6560  df-f1o 6561  df-fv 6562  df-isom 6563  df-riota 7380  df-ov 7427  df-oprab 7428  df-mpo 7429  df-of 7690  df-rpss 7734  df-om 7877  df-1st 8003  df-2nd 8004  df-supp 8175  df-tpos 8241  df-frecs 8296  df-wrecs 8327  df-recs 8401  df-rdg 8440  df-1o 8496  df-2o 8497  df-oadd 8500  df-omul 8501  df-er 8734  df-ec 8736  df-qs 8740  df-map 8857  df-ixp 8927  df-en 8975  df-dom 8976  df-sdom 8977  df-fin 8978  df-fsupp 9406  df-sup 9485  df-inf 9486  df-oi 9553  df-dju 9944  df-card 9982  df-acn 9985  df-pnf 11300  df-mnf 11301  df-xr 11302  df-ltxr 11303  df-le 11304  df-sub 11496  df-neg 11497  df-div 11922  df-nn 12265  df-2 12327  df-3 12328  df-n0 12525  df-xnn0 12597  df-z 12611  df-uz 12875  df-q 12985  df-rp 13029  df-fz 13539  df-fzo 13682  df-fl 13812  df-mod 13890  df-seq 14022  df-exp 14082  df-fac 14291  df-bc 14320  df-hash 14348  df-word 14523  df-concat 14579  df-s1 14604  df-cj 15104  df-re 15105  df-im 15106  df-sqrt 15240  df-abs 15241  df-clim 15490  df-sum 15691  df-dvds 16257  df-gcd 16495  df-prm 16673  df-pc 16839  df-sets 17166  df-slot 17184  df-ndx 17196  df-base 17214  df-ress 17243  df-plusg 17279  df-0g 17456  df-gsum 17457  df-mre 17599  df-mrc 17600  df-acs 17602  df-mgm 18633  df-sgrp 18712  df-mnd 18728  df-mhm 18773  df-submnd 18774  df-grp 18931  df-minusg 18932  df-sbg 18933  df-mulg 19062  df-subg 19117  df-eqg 19119  df-ghm 19207  df-gim 19253  df-ga 19284  df-cntz 19311  df-oppg 19340  df-od 19526  df-gex 19527  df-pgp 19528  df-lsm 19634  df-pj1 19635  df-cmn 19780  df-abl 19781  df-cyg 19876  df-dprd 19995
This theorem is referenced by:  dchrpt  27296
  Copyright terms: Public domain W3C validator