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

Theorem ablfaclem2 18683
Description: Lemma for ablfac 18685. (Contributed by Mario Carneiro, 27-Apr-2016.) (Proof shortened by Mario Carneiro, 3-May-2016.)
Hypotheses
Ref Expression
ablfac.b 𝐵 = (Base‘𝐺)
ablfac.c 𝐶 = {𝑟 ∈ (SubGrp‘𝐺) ∣ (𝐺s 𝑟) ∈ (CycGrp ∩ ran pGrp )}
ablfac.1 (𝜑𝐺 ∈ Abel)
ablfac.2 (𝜑𝐵 ∈ Fin)
ablfac.o 𝑂 = (od‘𝐺)
ablfac.a 𝐴 = {𝑤 ∈ ℙ ∣ 𝑤 ∥ (♯‘𝐵)}
ablfac.s 𝑆 = (𝑝𝐴 ↦ {𝑥𝐵 ∣ (𝑂𝑥) ∥ (𝑝↑(𝑝 pCnt (♯‘𝐵)))})
ablfac.w 𝑊 = (𝑔 ∈ (SubGrp‘𝐺) ↦ {𝑠 ∈ Word 𝐶 ∣ (𝐺dom DProd 𝑠 ∧ (𝐺 DProd 𝑠) = 𝑔)})
ablfaclem2.f (𝜑𝐹:𝐴⟶Word 𝐶)
ablfaclem2.q (𝜑 → ∀𝑦𝐴 (𝐹𝑦) ∈ (𝑊‘(𝑆𝑦)))
ablfaclem2.l 𝐿 = 𝑦𝐴 ({𝑦} × dom (𝐹𝑦))
ablfaclem2.g (𝜑𝐻:(0..^(♯‘𝐿))–1-1-onto𝐿)
Assertion
Ref Expression
ablfaclem2 (𝜑 → (𝑊𝐵) ≠ ∅)
Distinct variable groups:   𝑠,𝑝,𝑥,𝑦,𝐴   𝐹,𝑠   𝑔,𝑟,𝑠,𝑦,𝑆   𝑔,𝑝,𝑤,𝑥,𝐵,𝑟,𝑠   𝑂,𝑝,𝑥   𝐶,𝑔,𝑝,𝑠   𝑦,𝑤,𝐶,𝑥   𝑊,𝑝,𝑤,𝑥,𝑦   𝐻,𝑠   𝜑,𝑝,𝑠,𝑤,𝑥,𝑦   𝑔,𝐺,𝑝,𝑟,𝑠,𝑤,𝑥,𝑦
Allowed substitution hints:   𝜑(𝑔,𝑟)   𝐴(𝑤,𝑔,𝑟)   𝐵(𝑦)   𝐶(𝑟)   𝑆(𝑥,𝑤,𝑝)   𝐹(𝑥,𝑦,𝑤,𝑔,𝑟,𝑝)   𝐻(𝑥,𝑦,𝑤,𝑔,𝑟,𝑝)   𝐿(𝑥,𝑦,𝑤,𝑔,𝑠,𝑟,𝑝)   𝑂(𝑦,𝑤,𝑔,𝑠,𝑟)   𝑊(𝑔,𝑠,𝑟)

Proof of Theorem ablfaclem2
Dummy variable 𝑧 is distinct from all other variables.
StepHypRef Expression
1 ablfac.1 . . 3 (𝜑𝐺 ∈ Abel)
2 ablgrp 18395 . . 3 (𝐺 ∈ Abel → 𝐺 ∈ Grp)
3 ablfac.b . . . 4 𝐵 = (Base‘𝐺)
43subgid 17794 . . 3 (𝐺 ∈ Grp → 𝐵 ∈ (SubGrp‘𝐺))
5 ablfac.c . . . 4 𝐶 = {𝑟 ∈ (SubGrp‘𝐺) ∣ (𝐺s 𝑟) ∈ (CycGrp ∩ ran pGrp )}
6 ablfac.2 . . . 4 (𝜑𝐵 ∈ Fin)
7 ablfac.o . . . 4 𝑂 = (od‘𝐺)
8 ablfac.a . . . 4 𝐴 = {𝑤 ∈ ℙ ∣ 𝑤 ∥ (♯‘𝐵)}
9 ablfac.s . . . 4 𝑆 = (𝑝𝐴 ↦ {𝑥𝐵 ∣ (𝑂𝑥) ∥ (𝑝↑(𝑝 pCnt (♯‘𝐵)))})
10 ablfac.w . . . 4 𝑊 = (𝑔 ∈ (SubGrp‘𝐺) ↦ {𝑠 ∈ Word 𝐶 ∣ (𝐺dom DProd 𝑠 ∧ (𝐺 DProd 𝑠) = 𝑔)})
113, 5, 1, 6, 7, 8, 9, 10ablfaclem1 18682 . . 3 (𝐵 ∈ (SubGrp‘𝐺) → (𝑊𝐵) = {𝑠 ∈ Word 𝐶 ∣ (𝐺dom DProd 𝑠 ∧ (𝐺 DProd 𝑠) = 𝐵)})
121, 2, 4, 114syl 19 . 2 (𝜑 → (𝑊𝐵) = {𝑠 ∈ Word 𝐶 ∣ (𝐺dom DProd 𝑠 ∧ (𝐺 DProd 𝑠) = 𝐵)})
13 ablfaclem2.f . . . . . . . . . . . . . 14 (𝜑𝐹:𝐴⟶Word 𝐶)
1413ffvelrnda 6578 . . . . . . . . . . . . 13 ((𝜑𝑦𝐴) → (𝐹𝑦) ∈ Word 𝐶)
15 wrdf 13517 . . . . . . . . . . . . 13 ((𝐹𝑦) ∈ Word 𝐶 → (𝐹𝑦):(0..^(♯‘(𝐹𝑦)))⟶𝐶)
1614, 15syl 17 . . . . . . . . . . . 12 ((𝜑𝑦𝐴) → (𝐹𝑦):(0..^(♯‘(𝐹𝑦)))⟶𝐶)
1716fdmd 6262 . . . . . . . . . . . . 13 ((𝜑𝑦𝐴) → dom (𝐹𝑦) = (0..^(♯‘(𝐹𝑦))))
1817feq2d 6239 . . . . . . . . . . . 12 ((𝜑𝑦𝐴) → ((𝐹𝑦):dom (𝐹𝑦)⟶𝐶 ↔ (𝐹𝑦):(0..^(♯‘(𝐹𝑦)))⟶𝐶))
1916, 18mpbird 248 . . . . . . . . . . 11 ((𝜑𝑦𝐴) → (𝐹𝑦):dom (𝐹𝑦)⟶𝐶)
2019ffvelrnda 6578 . . . . . . . . . 10 (((𝜑𝑦𝐴) ∧ 𝑧 ∈ dom (𝐹𝑦)) → ((𝐹𝑦)‘𝑧) ∈ 𝐶)
2120anasss 454 . . . . . . . . 9 ((𝜑 ∧ (𝑦𝐴𝑧 ∈ dom (𝐹𝑦))) → ((𝐹𝑦)‘𝑧) ∈ 𝐶)
2221ralrimivva 3158 . . . . . . . 8 (𝜑 → ∀𝑦𝐴𝑧 ∈ dom (𝐹𝑦)((𝐹𝑦)‘𝑧) ∈ 𝐶)
23 eqid 2805 . . . . . . . . 9 (𝑦𝐴, 𝑧 ∈ dom (𝐹𝑦) ↦ ((𝐹𝑦)‘𝑧)) = (𝑦𝐴, 𝑧 ∈ dom (𝐹𝑦) ↦ ((𝐹𝑦)‘𝑧))
2423fmpt2x 7466 . . . . . . . 8 (∀𝑦𝐴𝑧 ∈ dom (𝐹𝑦)((𝐹𝑦)‘𝑧) ∈ 𝐶 ↔ (𝑦𝐴, 𝑧 ∈ dom (𝐹𝑦) ↦ ((𝐹𝑦)‘𝑧)): 𝑦𝐴 ({𝑦} × dom (𝐹𝑦))⟶𝐶)
2522, 24sylib 209 . . . . . . 7 (𝜑 → (𝑦𝐴, 𝑧 ∈ dom (𝐹𝑦) ↦ ((𝐹𝑦)‘𝑧)): 𝑦𝐴 ({𝑦} × dom (𝐹𝑦))⟶𝐶)
26 ablfaclem2.l . . . . . . . 8 𝐿 = 𝑦𝐴 ({𝑦} × dom (𝐹𝑦))
2726feq2i 6245 . . . . . . 7 ((𝑦𝐴, 𝑧 ∈ dom (𝐹𝑦) ↦ ((𝐹𝑦)‘𝑧)):𝐿𝐶 ↔ (𝑦𝐴, 𝑧 ∈ dom (𝐹𝑦) ↦ ((𝐹𝑦)‘𝑧)): 𝑦𝐴 ({𝑦} × dom (𝐹𝑦))⟶𝐶)
2825, 27sylibr 225 . . . . . 6 (𝜑 → (𝑦𝐴, 𝑧 ∈ dom (𝐹𝑦) ↦ ((𝐹𝑦)‘𝑧)):𝐿𝐶)
29 ablfaclem2.g . . . . . . 7 (𝜑𝐻:(0..^(♯‘𝐿))–1-1-onto𝐿)
30 f1of 6350 . . . . . . 7 (𝐻:(0..^(♯‘𝐿))–1-1-onto𝐿𝐻:(0..^(♯‘𝐿))⟶𝐿)
3129, 30syl 17 . . . . . 6 (𝜑𝐻:(0..^(♯‘𝐿))⟶𝐿)
32 fco 6270 . . . . . 6 (((𝑦𝐴, 𝑧 ∈ dom (𝐹𝑦) ↦ ((𝐹𝑦)‘𝑧)):𝐿𝐶𝐻:(0..^(♯‘𝐿))⟶𝐿) → ((𝑦𝐴, 𝑧 ∈ dom (𝐹𝑦) ↦ ((𝐹𝑦)‘𝑧)) ∘ 𝐻):(0..^(♯‘𝐿))⟶𝐶)
3328, 31, 32syl2anc 575 . . . . 5 (𝜑 → ((𝑦𝐴, 𝑧 ∈ dom (𝐹𝑦) ↦ ((𝐹𝑦)‘𝑧)) ∘ 𝐻):(0..^(♯‘𝐿))⟶𝐶)
34 iswrdi 13516 . . . . 5 (((𝑦𝐴, 𝑧 ∈ dom (𝐹𝑦) ↦ ((𝐹𝑦)‘𝑧)) ∘ 𝐻):(0..^(♯‘𝐿))⟶𝐶 → ((𝑦𝐴, 𝑧 ∈ dom (𝐹𝑦) ↦ ((𝐹𝑦)‘𝑧)) ∘ 𝐻) ∈ Word 𝐶)
3533, 34syl 17 . . . 4 (𝜑 → ((𝑦𝐴, 𝑧 ∈ dom (𝐹𝑦) ↦ ((𝐹𝑦)‘𝑧)) ∘ 𝐻) ∈ Word 𝐶)
36 ablfaclem2.q . . . . . . . . . . . . . . 15 (𝜑 → ∀𝑦𝐴 (𝐹𝑦) ∈ (𝑊‘(𝑆𝑦)))
3736r19.21bi 3119 . . . . . . . . . . . . . 14 ((𝜑𝑦𝐴) → (𝐹𝑦) ∈ (𝑊‘(𝑆𝑦)))
38 ssrab2 3881 . . . . . . . . . . . . . . . . . . . 20 {𝑤 ∈ ℙ ∣ 𝑤 ∥ (♯‘𝐵)} ⊆ ℙ
398, 38eqsstri 3829 . . . . . . . . . . . . . . . . . . 19 𝐴 ⊆ ℙ
4039a1i 11 . . . . . . . . . . . . . . . . . 18 (𝜑𝐴 ⊆ ℙ)
413, 7, 9, 1, 6, 40ablfac1b 18667 . . . . . . . . . . . . . . . . 17 (𝜑𝐺dom DProd 𝑆)
423fvexi 6419 . . . . . . . . . . . . . . . . . . . 20 𝐵 ∈ V
4342rabex 5004 . . . . . . . . . . . . . . . . . . 19 {𝑥𝐵 ∣ (𝑂𝑥) ∥ (𝑝↑(𝑝 pCnt (♯‘𝐵)))} ∈ V
4443, 9dmmpti 6231 . . . . . . . . . . . . . . . . . 18 dom 𝑆 = 𝐴
4544a1i 11 . . . . . . . . . . . . . . . . 17 (𝜑 → dom 𝑆 = 𝐴)
4641, 45dprdf2 18604 . . . . . . . . . . . . . . . 16 (𝜑𝑆:𝐴⟶(SubGrp‘𝐺))
4746ffvelrnda 6578 . . . . . . . . . . . . . . 15 ((𝜑𝑦𝐴) → (𝑆𝑦) ∈ (SubGrp‘𝐺))
483, 5, 1, 6, 7, 8, 9, 10ablfaclem1 18682 . . . . . . . . . . . . . . 15 ((𝑆𝑦) ∈ (SubGrp‘𝐺) → (𝑊‘(𝑆𝑦)) = {𝑠 ∈ Word 𝐶 ∣ (𝐺dom DProd 𝑠 ∧ (𝐺 DProd 𝑠) = (𝑆𝑦))})
4947, 48syl 17 . . . . . . . . . . . . . 14 ((𝜑𝑦𝐴) → (𝑊‘(𝑆𝑦)) = {𝑠 ∈ Word 𝐶 ∣ (𝐺dom DProd 𝑠 ∧ (𝐺 DProd 𝑠) = (𝑆𝑦))})
5037, 49eleqtrd 2886 . . . . . . . . . . . . 13 ((𝜑𝑦𝐴) → (𝐹𝑦) ∈ {𝑠 ∈ Word 𝐶 ∣ (𝐺dom DProd 𝑠 ∧ (𝐺 DProd 𝑠) = (𝑆𝑦))})
51 breq2 4844 . . . . . . . . . . . . . . . 16 (𝑠 = (𝐹𝑦) → (𝐺dom DProd 𝑠𝐺dom DProd (𝐹𝑦)))
52 oveq2 6879 . . . . . . . . . . . . . . . . 17 (𝑠 = (𝐹𝑦) → (𝐺 DProd 𝑠) = (𝐺 DProd (𝐹𝑦)))
5352eqeq1d 2807 . . . . . . . . . . . . . . . 16 (𝑠 = (𝐹𝑦) → ((𝐺 DProd 𝑠) = (𝑆𝑦) ↔ (𝐺 DProd (𝐹𝑦)) = (𝑆𝑦)))
5451, 53anbi12d 618 . . . . . . . . . . . . . . 15 (𝑠 = (𝐹𝑦) → ((𝐺dom DProd 𝑠 ∧ (𝐺 DProd 𝑠) = (𝑆𝑦)) ↔ (𝐺dom DProd (𝐹𝑦) ∧ (𝐺 DProd (𝐹𝑦)) = (𝑆𝑦))))
5554elrab 3558 . . . . . . . . . . . . . 14 ((𝐹𝑦) ∈ {𝑠 ∈ Word 𝐶 ∣ (𝐺dom DProd 𝑠 ∧ (𝐺 DProd 𝑠) = (𝑆𝑦))} ↔ ((𝐹𝑦) ∈ Word 𝐶 ∧ (𝐺dom DProd (𝐹𝑦) ∧ (𝐺 DProd (𝐹𝑦)) = (𝑆𝑦))))
5655simprbi 486 . . . . . . . . . . . . 13 ((𝐹𝑦) ∈ {𝑠 ∈ Word 𝐶 ∣ (𝐺dom DProd 𝑠 ∧ (𝐺 DProd 𝑠) = (𝑆𝑦))} → (𝐺dom DProd (𝐹𝑦) ∧ (𝐺 DProd (𝐹𝑦)) = (𝑆𝑦)))
5750, 56syl 17 . . . . . . . . . . . 12 ((𝜑𝑦𝐴) → (𝐺dom DProd (𝐹𝑦) ∧ (𝐺 DProd (𝐹𝑦)) = (𝑆𝑦)))
5857simpld 484 . . . . . . . . . . 11 ((𝜑𝑦𝐴) → 𝐺dom DProd (𝐹𝑦))
59 dprdf 18603 . . . . . . . . . . 11 (𝐺dom DProd (𝐹𝑦) → (𝐹𝑦):dom (𝐹𝑦)⟶(SubGrp‘𝐺))
6058, 59syl 17 . . . . . . . . . 10 ((𝜑𝑦𝐴) → (𝐹𝑦):dom (𝐹𝑦)⟶(SubGrp‘𝐺))
6160ffvelrnda 6578 . . . . . . . . 9 (((𝜑𝑦𝐴) ∧ 𝑧 ∈ dom (𝐹𝑦)) → ((𝐹𝑦)‘𝑧) ∈ (SubGrp‘𝐺))
6261anasss 454 . . . . . . . 8 ((𝜑 ∧ (𝑦𝐴𝑧 ∈ dom (𝐹𝑦))) → ((𝐹𝑦)‘𝑧) ∈ (SubGrp‘𝐺))
6360feqmptd 6467 . . . . . . . . 9 ((𝜑𝑦𝐴) → (𝐹𝑦) = (𝑧 ∈ dom (𝐹𝑦) ↦ ((𝐹𝑦)‘𝑧)))
6458, 63breqtrd 4866 . . . . . . . 8 ((𝜑𝑦𝐴) → 𝐺dom DProd (𝑧 ∈ dom (𝐹𝑦) ↦ ((𝐹𝑦)‘𝑧)))
6546feqmptd 6467 . . . . . . . . . 10 (𝜑𝑆 = (𝑦𝐴 ↦ (𝑆𝑦)))
6663oveq2d 6887 . . . . . . . . . . . 12 ((𝜑𝑦𝐴) → (𝐺 DProd (𝐹𝑦)) = (𝐺 DProd (𝑧 ∈ dom (𝐹𝑦) ↦ ((𝐹𝑦)‘𝑧))))
6757simprd 485 . . . . . . . . . . . 12 ((𝜑𝑦𝐴) → (𝐺 DProd (𝐹𝑦)) = (𝑆𝑦))
6866, 67eqtr3d 2841 . . . . . . . . . . 11 ((𝜑𝑦𝐴) → (𝐺 DProd (𝑧 ∈ dom (𝐹𝑦) ↦ ((𝐹𝑦)‘𝑧))) = (𝑆𝑦))
6968mpteq2dva 4934 . . . . . . . . . 10 (𝜑 → (𝑦𝐴 ↦ (𝐺 DProd (𝑧 ∈ dom (𝐹𝑦) ↦ ((𝐹𝑦)‘𝑧)))) = (𝑦𝐴 ↦ (𝑆𝑦)))
7065, 69eqtr4d 2842 . . . . . . . . 9 (𝜑𝑆 = (𝑦𝐴 ↦ (𝐺 DProd (𝑧 ∈ dom (𝐹𝑦) ↦ ((𝐹𝑦)‘𝑧)))))
7141, 70breqtrd 4866 . . . . . . . 8 (𝜑𝐺dom DProd (𝑦𝐴 ↦ (𝐺 DProd (𝑧 ∈ dom (𝐹𝑦) ↦ ((𝐹𝑦)‘𝑧)))))
7262, 64, 71dprd2d2 18641 . . . . . . 7 (𝜑 → (𝐺dom DProd (𝑦𝐴, 𝑧 ∈ dom (𝐹𝑦) ↦ ((𝐹𝑦)‘𝑧)) ∧ (𝐺 DProd (𝑦𝐴, 𝑧 ∈ dom (𝐹𝑦) ↦ ((𝐹𝑦)‘𝑧))) = (𝐺 DProd (𝑦𝐴 ↦ (𝐺 DProd (𝑧 ∈ dom (𝐹𝑦) ↦ ((𝐹𝑦)‘𝑧)))))))
7372simpld 484 . . . . . 6 (𝜑𝐺dom DProd (𝑦𝐴, 𝑧 ∈ dom (𝐹𝑦) ↦ ((𝐹𝑦)‘𝑧)))
7428fdmd 6262 . . . . . 6 (𝜑 → dom (𝑦𝐴, 𝑧 ∈ dom (𝐹𝑦) ↦ ((𝐹𝑦)‘𝑧)) = 𝐿)
7573, 74, 29dprdf1o 18629 . . . . 5 (𝜑 → (𝐺dom DProd ((𝑦𝐴, 𝑧 ∈ dom (𝐹𝑦) ↦ ((𝐹𝑦)‘𝑧)) ∘ 𝐻) ∧ (𝐺 DProd ((𝑦𝐴, 𝑧 ∈ dom (𝐹𝑦) ↦ ((𝐹𝑦)‘𝑧)) ∘ 𝐻)) = (𝐺 DProd (𝑦𝐴, 𝑧 ∈ dom (𝐹𝑦) ↦ ((𝐹𝑦)‘𝑧)))))
7675simpld 484 . . . 4 (𝜑𝐺dom DProd ((𝑦𝐴, 𝑧 ∈ dom (𝐹𝑦) ↦ ((𝐹𝑦)‘𝑧)) ∘ 𝐻))
7775simprd 485 . . . . 5 (𝜑 → (𝐺 DProd ((𝑦𝐴, 𝑧 ∈ dom (𝐹𝑦) ↦ ((𝐹𝑦)‘𝑧)) ∘ 𝐻)) = (𝐺 DProd (𝑦𝐴, 𝑧 ∈ dom (𝐹𝑦) ↦ ((𝐹𝑦)‘𝑧))))
7872simprd 485 . . . . 5 (𝜑 → (𝐺 DProd (𝑦𝐴, 𝑧 ∈ dom (𝐹𝑦) ↦ ((𝐹𝑦)‘𝑧))) = (𝐺 DProd (𝑦𝐴 ↦ (𝐺 DProd (𝑧 ∈ dom (𝐹𝑦) ↦ ((𝐹𝑦)‘𝑧))))))
7970oveq2d 6887 . . . . . 6 (𝜑 → (𝐺 DProd 𝑆) = (𝐺 DProd (𝑦𝐴 ↦ (𝐺 DProd (𝑧 ∈ dom (𝐹𝑦) ↦ ((𝐹𝑦)‘𝑧))))))
80 ssidd 3818 . . . . . . 7 (𝜑𝐴𝐴)
813, 7, 9, 1, 6, 40, 8, 80ablfac1c 18668 . . . . . 6 (𝜑 → (𝐺 DProd 𝑆) = 𝐵)
8279, 81eqtr3d 2841 . . . . 5 (𝜑 → (𝐺 DProd (𝑦𝐴 ↦ (𝐺 DProd (𝑧 ∈ dom (𝐹𝑦) ↦ ((𝐹𝑦)‘𝑧))))) = 𝐵)
8377, 78, 823eqtrd 2843 . . . 4 (𝜑 → (𝐺 DProd ((𝑦𝐴, 𝑧 ∈ dom (𝐹𝑦) ↦ ((𝐹𝑦)‘𝑧)) ∘ 𝐻)) = 𝐵)
84 breq2 4844 . . . . . 6 (𝑠 = ((𝑦𝐴, 𝑧 ∈ dom (𝐹𝑦) ↦ ((𝐹𝑦)‘𝑧)) ∘ 𝐻) → (𝐺dom DProd 𝑠𝐺dom DProd ((𝑦𝐴, 𝑧 ∈ dom (𝐹𝑦) ↦ ((𝐹𝑦)‘𝑧)) ∘ 𝐻)))
85 oveq2 6879 . . . . . . 7 (𝑠 = ((𝑦𝐴, 𝑧 ∈ dom (𝐹𝑦) ↦ ((𝐹𝑦)‘𝑧)) ∘ 𝐻) → (𝐺 DProd 𝑠) = (𝐺 DProd ((𝑦𝐴, 𝑧 ∈ dom (𝐹𝑦) ↦ ((𝐹𝑦)‘𝑧)) ∘ 𝐻)))
8685eqeq1d 2807 . . . . . 6 (𝑠 = ((𝑦𝐴, 𝑧 ∈ dom (𝐹𝑦) ↦ ((𝐹𝑦)‘𝑧)) ∘ 𝐻) → ((𝐺 DProd 𝑠) = 𝐵 ↔ (𝐺 DProd ((𝑦𝐴, 𝑧 ∈ dom (𝐹𝑦) ↦ ((𝐹𝑦)‘𝑧)) ∘ 𝐻)) = 𝐵))
8784, 86anbi12d 618 . . . . 5 (𝑠 = ((𝑦𝐴, 𝑧 ∈ dom (𝐹𝑦) ↦ ((𝐹𝑦)‘𝑧)) ∘ 𝐻) → ((𝐺dom DProd 𝑠 ∧ (𝐺 DProd 𝑠) = 𝐵) ↔ (𝐺dom DProd ((𝑦𝐴, 𝑧 ∈ dom (𝐹𝑦) ↦ ((𝐹𝑦)‘𝑧)) ∘ 𝐻) ∧ (𝐺 DProd ((𝑦𝐴, 𝑧 ∈ dom (𝐹𝑦) ↦ ((𝐹𝑦)‘𝑧)) ∘ 𝐻)) = 𝐵)))
8887rspcev 3501 . . . 4 ((((𝑦𝐴, 𝑧 ∈ dom (𝐹𝑦) ↦ ((𝐹𝑦)‘𝑧)) ∘ 𝐻) ∈ Word 𝐶 ∧ (𝐺dom DProd ((𝑦𝐴, 𝑧 ∈ dom (𝐹𝑦) ↦ ((𝐹𝑦)‘𝑧)) ∘ 𝐻) ∧ (𝐺 DProd ((𝑦𝐴, 𝑧 ∈ dom (𝐹𝑦) ↦ ((𝐹𝑦)‘𝑧)) ∘ 𝐻)) = 𝐵)) → ∃𝑠 ∈ Word 𝐶(𝐺dom DProd 𝑠 ∧ (𝐺 DProd 𝑠) = 𝐵))
8935, 76, 83, 88syl12anc 856 . . 3 (𝜑 → ∃𝑠 ∈ Word 𝐶(𝐺dom DProd 𝑠 ∧ (𝐺 DProd 𝑠) = 𝐵))
90 rabn0 4155 . . 3 ({𝑠 ∈ Word 𝐶 ∣ (𝐺dom DProd 𝑠 ∧ (𝐺 DProd 𝑠) = 𝐵)} ≠ ∅ ↔ ∃𝑠 ∈ Word 𝐶(𝐺dom DProd 𝑠 ∧ (𝐺 DProd 𝑠) = 𝐵))
9189, 90sylibr 225 . 2 (𝜑 → {𝑠 ∈ Word 𝐶 ∣ (𝐺dom DProd 𝑠 ∧ (𝐺 DProd 𝑠) = 𝐵)} ≠ ∅)
9212, 91eqnetrd 3044 1 (𝜑 → (𝑊𝐵) ≠ ∅)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 384   = wceq 1637  wcel 2158  wne 2977  wral 3095  wrex 3096  {crab 3099  cin 3765  wss 3766  c0 4113  {csn 4367   ciun 4708   class class class wbr 4840  cmpt 4919   × cxp 5306  dom cdm 5308  ran crn 5309  ccom 5312  wf 6094  1-1-ontowf1o 6097  cfv 6098  (class class class)co 6871  cmpt2 6873  Fincfn 8189  0cc0 10218  ..^cfzo 12685  cexp 13079  chash 13333  Word cword 13498  cdvds 15199  cprime 15599   pCnt cpc 15754  Basecbs 16064  s cress 16065  Grpcgrp 17623  SubGrpcsubg 17786  odcod 18141   pGrp cpgp 18143  Abelcabl 18391  CycGrpccyg 18476   DProd cdprd 18590
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1880  ax-4 1897  ax-5 2004  ax-6 2070  ax-7 2106  ax-8 2160  ax-9 2167  ax-10 2187  ax-11 2203  ax-12 2216  ax-13 2422  ax-ext 2784  ax-rep 4960  ax-sep 4971  ax-nul 4980  ax-pow 5032  ax-pr 5093  ax-un 7176  ax-inf2 8782  ax-cnex 10274  ax-resscn 10275  ax-1cn 10276  ax-icn 10277  ax-addcl 10278  ax-addrcl 10279  ax-mulcl 10280  ax-mulrcl 10281  ax-mulcom 10282  ax-addass 10283  ax-mulass 10284  ax-distr 10285  ax-i2m1 10286  ax-1ne0 10287  ax-1rid 10288  ax-rnegex 10289  ax-rrecex 10290  ax-cnre 10291  ax-pre-lttri 10292  ax-pre-lttrn 10293  ax-pre-ltadd 10294  ax-pre-mulgt0 10295  ax-pre-sup 10296
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-3or 1101  df-3an 1102  df-tru 1641  df-fal 1651  df-ex 1860  df-nf 1865  df-sb 2063  df-eu 2636  df-mo 2637  df-clab 2792  df-cleq 2798  df-clel 2801  df-nfc 2936  df-ne 2978  df-nel 3081  df-ral 3100  df-rex 3101  df-reu 3102  df-rmo 3103  df-rab 3104  df-v 3392  df-sbc 3631  df-csb 3726  df-dif 3769  df-un 3771  df-in 3773  df-ss 3780  df-pss 3782  df-nul 4114  df-if 4277  df-pw 4350  df-sn 4368  df-pr 4370  df-tp 4372  df-op 4374  df-uni 4627  df-int 4666  df-iun 4710  df-iin 4711  df-disj 4809  df-br 4841  df-opab 4903  df-mpt 4920  df-tr 4943  df-id 5216  df-eprel 5221  df-po 5229  df-so 5230  df-fr 5267  df-se 5268  df-we 5269  df-xp 5314  df-rel 5315  df-cnv 5316  df-co 5317  df-dm 5318  df-rn 5319  df-res 5320  df-ima 5321  df-pred 5890  df-ord 5936  df-on 5937  df-lim 5938  df-suc 5939  df-iota 6061  df-fun 6100  df-fn 6101  df-f 6102  df-f1 6103  df-fo 6104  df-f1o 6105  df-fv 6106  df-isom 6107  df-riota 6832  df-ov 6874  df-oprab 6875  df-mpt2 6876  df-of 7124  df-om 7293  df-1st 7395  df-2nd 7396  df-supp 7527  df-tpos 7584  df-wrecs 7639  df-recs 7701  df-rdg 7739  df-1o 7793  df-2o 7794  df-oadd 7797  df-omul 7798  df-er 7976  df-ec 7978  df-qs 7982  df-map 8091  df-pm 8092  df-ixp 8143  df-en 8190  df-dom 8191  df-sdom 8192  df-fin 8193  df-fsupp 8512  df-sup 8584  df-inf 8585  df-oi 8651  df-card 9045  df-acn 9048  df-cda 9272  df-pnf 10358  df-mnf 10359  df-xr 10360  df-ltxr 10361  df-le 10362  df-sub 10550  df-neg 10551  df-div 10967  df-nn 11303  df-2 11360  df-3 11361  df-n0 11556  df-xnn0 11626  df-z 11640  df-uz 11901  df-q 12004  df-rp 12043  df-fz 12546  df-fzo 12686  df-fl 12813  df-mod 12889  df-seq 13021  df-exp 13080  df-fac 13277  df-bc 13306  df-hash 13334  df-word 13506  df-cj 14058  df-re 14059  df-im 14060  df-sqrt 14194  df-abs 14195  df-clim 14438  df-sum 14636  df-dvds 15200  df-gcd 15432  df-prm 15600  df-pc 15755  df-ndx 16067  df-slot 16068  df-base 16070  df-sets 16071  df-ress 16072  df-plusg 16162  df-0g 16303  df-gsum 16304  df-mre 16447  df-mrc 16448  df-acs 16450  df-mgm 17443  df-sgrp 17485  df-mnd 17496  df-mhm 17536  df-submnd 17537  df-grp 17626  df-minusg 17627  df-sbg 17628  df-mulg 17742  df-subg 17789  df-eqg 17791  df-ghm 17856  df-gim 17899  df-ga 17920  df-cntz 17947  df-oppg 17973  df-od 18145  df-lsm 18248  df-pj1 18249  df-cmn 18392  df-abl 18393  df-dprd 18592
This theorem is referenced by:  ablfaclem3  18684
  Copyright terms: Public domain W3C validator