Step | Hyp | Ref
| Expression |
1 | | ablfac.1 |
. . 3
⊢ (𝜑 → 𝐺 ∈ Abel) |
2 | | ablgrp 18198 |
. . 3
⊢ (𝐺 ∈ Abel → 𝐺 ∈ Grp) |
3 | | ablfac.b |
. . . 4
⊢ 𝐵 = (Base‘𝐺) |
4 | 3 | subgid 17596 |
. . 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 𝑠) = 𝑔)}) |
11 | 3, 5, 1, 6, 7, 8, 9, 10 | ablfaclem1 18484 |
. . 3
⊢ (𝐵 ∈ (SubGrp‘𝐺) → (𝑊‘𝐵) = {𝑠 ∈ Word 𝐶 ∣ (𝐺dom DProd 𝑠 ∧ (𝐺 DProd 𝑠) = 𝐵)}) |
12 | 1, 2, 4, 11 | 4syl 19 |
. 2
⊢ (𝜑 → (𝑊‘𝐵) = {𝑠 ∈ Word 𝐶 ∣ (𝐺dom DProd 𝑠 ∧ (𝐺 DProd 𝑠) = 𝐵)}) |
13 | | ablfaclem2.f |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝐹:𝐴⟶Word 𝐶) |
14 | 13 | ffvelrnda 6359 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐴) → (𝐹‘𝑦) ∈ Word 𝐶) |
15 | | wrdf 13310 |
. . . . . . . . . . . . 13
⊢ ((𝐹‘𝑦) ∈ Word 𝐶 → (𝐹‘𝑦):(0..^(#‘(𝐹‘𝑦)))⟶𝐶) |
16 | 14, 15 | syl 17 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐴) → (𝐹‘𝑦):(0..^(#‘(𝐹‘𝑦)))⟶𝐶) |
17 | | fdm 6051 |
. . . . . . . . . . . . . 14
⊢ ((𝐹‘𝑦):(0..^(#‘(𝐹‘𝑦)))⟶𝐶 → dom (𝐹‘𝑦) = (0..^(#‘(𝐹‘𝑦)))) |
18 | 16, 17 | syl 17 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐴) → dom (𝐹‘𝑦) = (0..^(#‘(𝐹‘𝑦)))) |
19 | 18 | feq2d 6031 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐴) → ((𝐹‘𝑦):dom (𝐹‘𝑦)⟶𝐶 ↔ (𝐹‘𝑦):(0..^(#‘(𝐹‘𝑦)))⟶𝐶)) |
20 | 16, 19 | mpbird 247 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐴) → (𝐹‘𝑦):dom (𝐹‘𝑦)⟶𝐶) |
21 | 20 | ffvelrnda 6359 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑦 ∈ 𝐴) ∧ 𝑧 ∈ dom (𝐹‘𝑦)) → ((𝐹‘𝑦)‘𝑧) ∈ 𝐶) |
22 | 21 | anasss 679 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑦 ∈ 𝐴 ∧ 𝑧 ∈ dom (𝐹‘𝑦))) → ((𝐹‘𝑦)‘𝑧) ∈ 𝐶) |
23 | 22 | ralrimivva 2971 |
. . . . . . . 8
⊢ (𝜑 → ∀𝑦 ∈ 𝐴 ∀𝑧 ∈ dom (𝐹‘𝑦)((𝐹‘𝑦)‘𝑧) ∈ 𝐶) |
24 | | eqid 2622 |
. . . . . . . . 9
⊢ (𝑦 ∈ 𝐴, 𝑧 ∈ dom (𝐹‘𝑦) ↦ ((𝐹‘𝑦)‘𝑧)) = (𝑦 ∈ 𝐴, 𝑧 ∈ dom (𝐹‘𝑦) ↦ ((𝐹‘𝑦)‘𝑧)) |
25 | 24 | fmpt2x 7236 |
. . . . . . . 8
⊢
(∀𝑦 ∈
𝐴 ∀𝑧 ∈ dom (𝐹‘𝑦)((𝐹‘𝑦)‘𝑧) ∈ 𝐶 ↔ (𝑦 ∈ 𝐴, 𝑧 ∈ dom (𝐹‘𝑦) ↦ ((𝐹‘𝑦)‘𝑧)):∪ 𝑦 ∈ 𝐴 ({𝑦} × dom (𝐹‘𝑦))⟶𝐶) |
26 | 23, 25 | sylib 208 |
. . . . . . 7
⊢ (𝜑 → (𝑦 ∈ 𝐴, 𝑧 ∈ dom (𝐹‘𝑦) ↦ ((𝐹‘𝑦)‘𝑧)):∪ 𝑦 ∈ 𝐴 ({𝑦} × dom (𝐹‘𝑦))⟶𝐶) |
27 | | ablfaclem2.l |
. . . . . . . 8
⊢ 𝐿 = ∪ 𝑦 ∈ 𝐴 ({𝑦} × dom (𝐹‘𝑦)) |
28 | 27 | feq2i 6037 |
. . . . . . 7
⊢ ((𝑦 ∈ 𝐴, 𝑧 ∈ dom (𝐹‘𝑦) ↦ ((𝐹‘𝑦)‘𝑧)):𝐿⟶𝐶 ↔ (𝑦 ∈ 𝐴, 𝑧 ∈ dom (𝐹‘𝑦) ↦ ((𝐹‘𝑦)‘𝑧)):∪ 𝑦 ∈ 𝐴 ({𝑦} × dom (𝐹‘𝑦))⟶𝐶) |
29 | 26, 28 | sylibr 224 |
. . . . . 6
⊢ (𝜑 → (𝑦 ∈ 𝐴, 𝑧 ∈ dom (𝐹‘𝑦) ↦ ((𝐹‘𝑦)‘𝑧)):𝐿⟶𝐶) |
30 | | ablfaclem2.g |
. . . . . . 7
⊢ (𝜑 → 𝐻:(0..^(#‘𝐿))–1-1-onto→𝐿) |
31 | | f1of 6137 |
. . . . . . 7
⊢ (𝐻:(0..^(#‘𝐿))–1-1-onto→𝐿 → 𝐻:(0..^(#‘𝐿))⟶𝐿) |
32 | 30, 31 | syl 17 |
. . . . . 6
⊢ (𝜑 → 𝐻:(0..^(#‘𝐿))⟶𝐿) |
33 | | fco 6058 |
. . . . . 6
⊢ (((𝑦 ∈ 𝐴, 𝑧 ∈ dom (𝐹‘𝑦) ↦ ((𝐹‘𝑦)‘𝑧)):𝐿⟶𝐶 ∧ 𝐻:(0..^(#‘𝐿))⟶𝐿) → ((𝑦 ∈ 𝐴, 𝑧 ∈ dom (𝐹‘𝑦) ↦ ((𝐹‘𝑦)‘𝑧)) ∘ 𝐻):(0..^(#‘𝐿))⟶𝐶) |
34 | 29, 32, 33 | syl2anc 693 |
. . . . 5
⊢ (𝜑 → ((𝑦 ∈ 𝐴, 𝑧 ∈ dom (𝐹‘𝑦) ↦ ((𝐹‘𝑦)‘𝑧)) ∘ 𝐻):(0..^(#‘𝐿))⟶𝐶) |
35 | | iswrdi 13309 |
. . . . 5
⊢ (((𝑦 ∈ 𝐴, 𝑧 ∈ dom (𝐹‘𝑦) ↦ ((𝐹‘𝑦)‘𝑧)) ∘ 𝐻):(0..^(#‘𝐿))⟶𝐶 → ((𝑦 ∈ 𝐴, 𝑧 ∈ dom (𝐹‘𝑦) ↦ ((𝐹‘𝑦)‘𝑧)) ∘ 𝐻) ∈ Word 𝐶) |
36 | 34, 35 | syl 17 |
. . . 4
⊢ (𝜑 → ((𝑦 ∈ 𝐴, 𝑧 ∈ dom (𝐹‘𝑦) ↦ ((𝐹‘𝑦)‘𝑧)) ∘ 𝐻) ∈ Word 𝐶) |
37 | | ablfaclem2.q |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → ∀𝑦 ∈ 𝐴 (𝐹‘𝑦) ∈ (𝑊‘(𝑆‘𝑦))) |
38 | 37 | r19.21bi 2932 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐴) → (𝐹‘𝑦) ∈ (𝑊‘(𝑆‘𝑦))) |
39 | | ssrab2 3687 |
. . . . . . . . . . . . . . . . . . . 20
⊢ {𝑤 ∈ ℙ ∣ 𝑤 ∥ (#‘𝐵)} ⊆
ℙ |
40 | 8, 39 | eqsstri 3635 |
. . . . . . . . . . . . . . . . . . 19
⊢ 𝐴 ⊆
ℙ |
41 | 40 | a1i 11 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → 𝐴 ⊆ ℙ) |
42 | 3, 7, 9, 1, 6, 41 | ablfac1b 18469 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → 𝐺dom DProd 𝑆) |
43 | | fvex 6201 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(Base‘𝐺)
∈ V |
44 | 3, 43 | eqeltri 2697 |
. . . . . . . . . . . . . . . . . . . 20
⊢ 𝐵 ∈ V |
45 | 44 | rabex 4813 |
. . . . . . . . . . . . . . . . . . 19
⊢ {𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ (𝑝↑(𝑝 pCnt (#‘𝐵)))} ∈ V |
46 | 45, 9 | dmmpti 6023 |
. . . . . . . . . . . . . . . . . 18
⊢ dom 𝑆 = 𝐴 |
47 | 46 | a1i 11 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → dom 𝑆 = 𝐴) |
48 | 42, 47 | dprdf2 18406 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → 𝑆:𝐴⟶(SubGrp‘𝐺)) |
49 | 48 | ffvelrnda 6359 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐴) → (𝑆‘𝑦) ∈ (SubGrp‘𝐺)) |
50 | 3, 5, 1, 6, 7, 8, 9, 10 | ablfaclem1 18484 |
. . . . . . . . . . . . . . 15
⊢ ((𝑆‘𝑦) ∈ (SubGrp‘𝐺) → (𝑊‘(𝑆‘𝑦)) = {𝑠 ∈ Word 𝐶 ∣ (𝐺dom DProd 𝑠 ∧ (𝐺 DProd 𝑠) = (𝑆‘𝑦))}) |
51 | 49, 50 | syl 17 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐴) → (𝑊‘(𝑆‘𝑦)) = {𝑠 ∈ Word 𝐶 ∣ (𝐺dom DProd 𝑠 ∧ (𝐺 DProd 𝑠) = (𝑆‘𝑦))}) |
52 | 38, 51 | eleqtrd 2703 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐴) → (𝐹‘𝑦) ∈ {𝑠 ∈ Word 𝐶 ∣ (𝐺dom DProd 𝑠 ∧ (𝐺 DProd 𝑠) = (𝑆‘𝑦))}) |
53 | | breq2 4657 |
. . . . . . . . . . . . . . . 16
⊢ (𝑠 = (𝐹‘𝑦) → (𝐺dom DProd 𝑠 ↔ 𝐺dom DProd (𝐹‘𝑦))) |
54 | | oveq2 6658 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑠 = (𝐹‘𝑦) → (𝐺 DProd 𝑠) = (𝐺 DProd (𝐹‘𝑦))) |
55 | 54 | eqeq1d 2624 |
. . . . . . . . . . . . . . . 16
⊢ (𝑠 = (𝐹‘𝑦) → ((𝐺 DProd 𝑠) = (𝑆‘𝑦) ↔ (𝐺 DProd (𝐹‘𝑦)) = (𝑆‘𝑦))) |
56 | 53, 55 | anbi12d 747 |
. . . . . . . . . . . . . . 15
⊢ (𝑠 = (𝐹‘𝑦) → ((𝐺dom DProd 𝑠 ∧ (𝐺 DProd 𝑠) = (𝑆‘𝑦)) ↔ (𝐺dom DProd (𝐹‘𝑦) ∧ (𝐺 DProd (𝐹‘𝑦)) = (𝑆‘𝑦)))) |
57 | 56 | elrab 3363 |
. . . . . . . . . . . . . 14
⊢ ((𝐹‘𝑦) ∈ {𝑠 ∈ Word 𝐶 ∣ (𝐺dom DProd 𝑠 ∧ (𝐺 DProd 𝑠) = (𝑆‘𝑦))} ↔ ((𝐹‘𝑦) ∈ Word 𝐶 ∧ (𝐺dom DProd (𝐹‘𝑦) ∧ (𝐺 DProd (𝐹‘𝑦)) = (𝑆‘𝑦)))) |
58 | 57 | simprbi 480 |
. . . . . . . . . . . . 13
⊢ ((𝐹‘𝑦) ∈ {𝑠 ∈ Word 𝐶 ∣ (𝐺dom DProd 𝑠 ∧ (𝐺 DProd 𝑠) = (𝑆‘𝑦))} → (𝐺dom DProd (𝐹‘𝑦) ∧ (𝐺 DProd (𝐹‘𝑦)) = (𝑆‘𝑦))) |
59 | 52, 58 | syl 17 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐴) → (𝐺dom DProd (𝐹‘𝑦) ∧ (𝐺 DProd (𝐹‘𝑦)) = (𝑆‘𝑦))) |
60 | 59 | simpld 475 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐴) → 𝐺dom DProd (𝐹‘𝑦)) |
61 | | dprdf 18405 |
. . . . . . . . . . 11
⊢ (𝐺dom DProd (𝐹‘𝑦) → (𝐹‘𝑦):dom (𝐹‘𝑦)⟶(SubGrp‘𝐺)) |
62 | 60, 61 | syl 17 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐴) → (𝐹‘𝑦):dom (𝐹‘𝑦)⟶(SubGrp‘𝐺)) |
63 | 62 | ffvelrnda 6359 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑦 ∈ 𝐴) ∧ 𝑧 ∈ dom (𝐹‘𝑦)) → ((𝐹‘𝑦)‘𝑧) ∈ (SubGrp‘𝐺)) |
64 | 63 | anasss 679 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑦 ∈ 𝐴 ∧ 𝑧 ∈ dom (𝐹‘𝑦))) → ((𝐹‘𝑦)‘𝑧) ∈ (SubGrp‘𝐺)) |
65 | 62 | feqmptd 6249 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐴) → (𝐹‘𝑦) = (𝑧 ∈ dom (𝐹‘𝑦) ↦ ((𝐹‘𝑦)‘𝑧))) |
66 | 60, 65 | breqtrd 4679 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐴) → 𝐺dom DProd (𝑧 ∈ dom (𝐹‘𝑦) ↦ ((𝐹‘𝑦)‘𝑧))) |
67 | 48 | feqmptd 6249 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑆 = (𝑦 ∈ 𝐴 ↦ (𝑆‘𝑦))) |
68 | 65 | oveq2d 6666 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐴) → (𝐺 DProd (𝐹‘𝑦)) = (𝐺 DProd (𝑧 ∈ dom (𝐹‘𝑦) ↦ ((𝐹‘𝑦)‘𝑧)))) |
69 | 59 | simprd 479 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐴) → (𝐺 DProd (𝐹‘𝑦)) = (𝑆‘𝑦)) |
70 | 68, 69 | eqtr3d 2658 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐴) → (𝐺 DProd (𝑧 ∈ dom (𝐹‘𝑦) ↦ ((𝐹‘𝑦)‘𝑧))) = (𝑆‘𝑦)) |
71 | 70 | mpteq2dva 4744 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑦 ∈ 𝐴 ↦ (𝐺 DProd (𝑧 ∈ dom (𝐹‘𝑦) ↦ ((𝐹‘𝑦)‘𝑧)))) = (𝑦 ∈ 𝐴 ↦ (𝑆‘𝑦))) |
72 | 67, 71 | eqtr4d 2659 |
. . . . . . . . 9
⊢ (𝜑 → 𝑆 = (𝑦 ∈ 𝐴 ↦ (𝐺 DProd (𝑧 ∈ dom (𝐹‘𝑦) ↦ ((𝐹‘𝑦)‘𝑧))))) |
73 | 42, 72 | breqtrd 4679 |
. . . . . . . 8
⊢ (𝜑 → 𝐺dom DProd (𝑦 ∈ 𝐴 ↦ (𝐺 DProd (𝑧 ∈ dom (𝐹‘𝑦) ↦ ((𝐹‘𝑦)‘𝑧))))) |
74 | 64, 66, 73 | dprd2d2 18443 |
. . . . . . 7
⊢ (𝜑 → (𝐺dom DProd (𝑦 ∈ 𝐴, 𝑧 ∈ dom (𝐹‘𝑦) ↦ ((𝐹‘𝑦)‘𝑧)) ∧ (𝐺 DProd (𝑦 ∈ 𝐴, 𝑧 ∈ dom (𝐹‘𝑦) ↦ ((𝐹‘𝑦)‘𝑧))) = (𝐺 DProd (𝑦 ∈ 𝐴 ↦ (𝐺 DProd (𝑧 ∈ dom (𝐹‘𝑦) ↦ ((𝐹‘𝑦)‘𝑧))))))) |
75 | 74 | simpld 475 |
. . . . . 6
⊢ (𝜑 → 𝐺dom DProd (𝑦 ∈ 𝐴, 𝑧 ∈ dom (𝐹‘𝑦) ↦ ((𝐹‘𝑦)‘𝑧))) |
76 | | fdm 6051 |
. . . . . . 7
⊢ ((𝑦 ∈ 𝐴, 𝑧 ∈ dom (𝐹‘𝑦) ↦ ((𝐹‘𝑦)‘𝑧)):𝐿⟶𝐶 → dom (𝑦 ∈ 𝐴, 𝑧 ∈ dom (𝐹‘𝑦) ↦ ((𝐹‘𝑦)‘𝑧)) = 𝐿) |
77 | 29, 76 | syl 17 |
. . . . . 6
⊢ (𝜑 → dom (𝑦 ∈ 𝐴, 𝑧 ∈ dom (𝐹‘𝑦) ↦ ((𝐹‘𝑦)‘𝑧)) = 𝐿) |
78 | 75, 77, 30 | dprdf1o 18431 |
. . . . 5
⊢ (𝜑 → (𝐺dom DProd ((𝑦 ∈ 𝐴, 𝑧 ∈ dom (𝐹‘𝑦) ↦ ((𝐹‘𝑦)‘𝑧)) ∘ 𝐻) ∧ (𝐺 DProd ((𝑦 ∈ 𝐴, 𝑧 ∈ dom (𝐹‘𝑦) ↦ ((𝐹‘𝑦)‘𝑧)) ∘ 𝐻)) = (𝐺 DProd (𝑦 ∈ 𝐴, 𝑧 ∈ dom (𝐹‘𝑦) ↦ ((𝐹‘𝑦)‘𝑧))))) |
79 | 78 | simpld 475 |
. . . 4
⊢ (𝜑 → 𝐺dom DProd ((𝑦 ∈ 𝐴, 𝑧 ∈ dom (𝐹‘𝑦) ↦ ((𝐹‘𝑦)‘𝑧)) ∘ 𝐻)) |
80 | 78 | simprd 479 |
. . . . 5
⊢ (𝜑 → (𝐺 DProd ((𝑦 ∈ 𝐴, 𝑧 ∈ dom (𝐹‘𝑦) ↦ ((𝐹‘𝑦)‘𝑧)) ∘ 𝐻)) = (𝐺 DProd (𝑦 ∈ 𝐴, 𝑧 ∈ dom (𝐹‘𝑦) ↦ ((𝐹‘𝑦)‘𝑧)))) |
81 | 74 | simprd 479 |
. . . . 5
⊢ (𝜑 → (𝐺 DProd (𝑦 ∈ 𝐴, 𝑧 ∈ dom (𝐹‘𝑦) ↦ ((𝐹‘𝑦)‘𝑧))) = (𝐺 DProd (𝑦 ∈ 𝐴 ↦ (𝐺 DProd (𝑧 ∈ dom (𝐹‘𝑦) ↦ ((𝐹‘𝑦)‘𝑧)))))) |
82 | 72 | oveq2d 6666 |
. . . . . 6
⊢ (𝜑 → (𝐺 DProd 𝑆) = (𝐺 DProd (𝑦 ∈ 𝐴 ↦ (𝐺 DProd (𝑧 ∈ dom (𝐹‘𝑦) ↦ ((𝐹‘𝑦)‘𝑧)))))) |
83 | | ssid 3624 |
. . . . . . . 8
⊢ 𝐴 ⊆ 𝐴 |
84 | 83 | a1i 11 |
. . . . . . 7
⊢ (𝜑 → 𝐴 ⊆ 𝐴) |
85 | 3, 7, 9, 1, 6, 41,
8, 84 | ablfac1c 18470 |
. . . . . 6
⊢ (𝜑 → (𝐺 DProd 𝑆) = 𝐵) |
86 | 82, 85 | eqtr3d 2658 |
. . . . 5
⊢ (𝜑 → (𝐺 DProd (𝑦 ∈ 𝐴 ↦ (𝐺 DProd (𝑧 ∈ dom (𝐹‘𝑦) ↦ ((𝐹‘𝑦)‘𝑧))))) = 𝐵) |
87 | 80, 81, 86 | 3eqtrd 2660 |
. . . 4
⊢ (𝜑 → (𝐺 DProd ((𝑦 ∈ 𝐴, 𝑧 ∈ dom (𝐹‘𝑦) ↦ ((𝐹‘𝑦)‘𝑧)) ∘ 𝐻)) = 𝐵) |
88 | | breq2 4657 |
. . . . . 6
⊢ (𝑠 = ((𝑦 ∈ 𝐴, 𝑧 ∈ dom (𝐹‘𝑦) ↦ ((𝐹‘𝑦)‘𝑧)) ∘ 𝐻) → (𝐺dom DProd 𝑠 ↔ 𝐺dom DProd ((𝑦 ∈ 𝐴, 𝑧 ∈ dom (𝐹‘𝑦) ↦ ((𝐹‘𝑦)‘𝑧)) ∘ 𝐻))) |
89 | | oveq2 6658 |
. . . . . . 7
⊢ (𝑠 = ((𝑦 ∈ 𝐴, 𝑧 ∈ dom (𝐹‘𝑦) ↦ ((𝐹‘𝑦)‘𝑧)) ∘ 𝐻) → (𝐺 DProd 𝑠) = (𝐺 DProd ((𝑦 ∈ 𝐴, 𝑧 ∈ dom (𝐹‘𝑦) ↦ ((𝐹‘𝑦)‘𝑧)) ∘ 𝐻))) |
90 | 89 | eqeq1d 2624 |
. . . . . 6
⊢ (𝑠 = ((𝑦 ∈ 𝐴, 𝑧 ∈ dom (𝐹‘𝑦) ↦ ((𝐹‘𝑦)‘𝑧)) ∘ 𝐻) → ((𝐺 DProd 𝑠) = 𝐵 ↔ (𝐺 DProd ((𝑦 ∈ 𝐴, 𝑧 ∈ dom (𝐹‘𝑦) ↦ ((𝐹‘𝑦)‘𝑧)) ∘ 𝐻)) = 𝐵)) |
91 | 88, 90 | anbi12d 747 |
. . . . 5
⊢ (𝑠 = ((𝑦 ∈ 𝐴, 𝑧 ∈ dom (𝐹‘𝑦) ↦ ((𝐹‘𝑦)‘𝑧)) ∘ 𝐻) → ((𝐺dom DProd 𝑠 ∧ (𝐺 DProd 𝑠) = 𝐵) ↔ (𝐺dom DProd ((𝑦 ∈ 𝐴, 𝑧 ∈ dom (𝐹‘𝑦) ↦ ((𝐹‘𝑦)‘𝑧)) ∘ 𝐻) ∧ (𝐺 DProd ((𝑦 ∈ 𝐴, 𝑧 ∈ dom (𝐹‘𝑦) ↦ ((𝐹‘𝑦)‘𝑧)) ∘ 𝐻)) = 𝐵))) |
92 | 91 | rspcev 3309 |
. . . 4
⊢ ((((𝑦 ∈ 𝐴, 𝑧 ∈ dom (𝐹‘𝑦) ↦ ((𝐹‘𝑦)‘𝑧)) ∘ 𝐻) ∈ Word 𝐶 ∧ (𝐺dom DProd ((𝑦 ∈ 𝐴, 𝑧 ∈ dom (𝐹‘𝑦) ↦ ((𝐹‘𝑦)‘𝑧)) ∘ 𝐻) ∧ (𝐺 DProd ((𝑦 ∈ 𝐴, 𝑧 ∈ dom (𝐹‘𝑦) ↦ ((𝐹‘𝑦)‘𝑧)) ∘ 𝐻)) = 𝐵)) → ∃𝑠 ∈ Word 𝐶(𝐺dom DProd 𝑠 ∧ (𝐺 DProd 𝑠) = 𝐵)) |
93 | 36, 79, 87, 92 | syl12anc 1324 |
. . 3
⊢ (𝜑 → ∃𝑠 ∈ Word 𝐶(𝐺dom DProd 𝑠 ∧ (𝐺 DProd 𝑠) = 𝐵)) |
94 | | rabn0 3958 |
. . 3
⊢ ({𝑠 ∈ Word 𝐶 ∣ (𝐺dom DProd 𝑠 ∧ (𝐺 DProd 𝑠) = 𝐵)} ≠ ∅ ↔ ∃𝑠 ∈ Word 𝐶(𝐺dom DProd 𝑠 ∧ (𝐺 DProd 𝑠) = 𝐵)) |
95 | 93, 94 | sylibr 224 |
. 2
⊢ (𝜑 → {𝑠 ∈ Word 𝐶 ∣ (𝐺dom DProd 𝑠 ∧ (𝐺 DProd 𝑠) = 𝐵)} ≠ ∅) |
96 | 12, 95 | eqnetrd 2861 |
1
⊢ (𝜑 → (𝑊‘𝐵) ≠ ∅) |