| Step | Hyp | Ref
| Expression |
| 1 | | ablfac.1 |
. . 3
⊢ (𝜑 → 𝐺 ∈ Abel) |
| 2 | | ablgrp 19803 |
. . 3
⊢ (𝐺 ∈ Abel → 𝐺 ∈ Grp) |
| 3 | | ablfac.b |
. . . 4
⊢ 𝐵 = (Base‘𝐺) |
| 4 | 3 | subgid 19146 |
. . 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 20105 |
. . 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 | ffvelcdmda 7104 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐴) → (𝐹‘𝑦) ∈ Word 𝐶) |
| 15 | | wrdf 14557 |
. . . . . . . . . . . . 13
⊢ ((𝐹‘𝑦) ∈ Word 𝐶 → (𝐹‘𝑦):(0..^(♯‘(𝐹‘𝑦)))⟶𝐶) |
| 16 | 14, 15 | syl 17 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐴) → (𝐹‘𝑦):(0..^(♯‘(𝐹‘𝑦)))⟶𝐶) |
| 17 | 16 | ffdmd 6766 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐴) → (𝐹‘𝑦):dom (𝐹‘𝑦)⟶𝐶) |
| 18 | 17 | ffvelcdmda 7104 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑦 ∈ 𝐴) ∧ 𝑧 ∈ dom (𝐹‘𝑦)) → ((𝐹‘𝑦)‘𝑧) ∈ 𝐶) |
| 19 | 18 | anasss 466 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑦 ∈ 𝐴 ∧ 𝑧 ∈ dom (𝐹‘𝑦))) → ((𝐹‘𝑦)‘𝑧) ∈ 𝐶) |
| 20 | 19 | ralrimivva 3202 |
. . . . . . . 8
⊢ (𝜑 → ∀𝑦 ∈ 𝐴 ∀𝑧 ∈ dom (𝐹‘𝑦)((𝐹‘𝑦)‘𝑧) ∈ 𝐶) |
| 21 | | eqid 2737 |
. . . . . . . . 9
⊢ (𝑦 ∈ 𝐴, 𝑧 ∈ dom (𝐹‘𝑦) ↦ ((𝐹‘𝑦)‘𝑧)) = (𝑦 ∈ 𝐴, 𝑧 ∈ dom (𝐹‘𝑦) ↦ ((𝐹‘𝑦)‘𝑧)) |
| 22 | 21 | fmpox 8092 |
. . . . . . . 8
⊢
(∀𝑦 ∈
𝐴 ∀𝑧 ∈ dom (𝐹‘𝑦)((𝐹‘𝑦)‘𝑧) ∈ 𝐶 ↔ (𝑦 ∈ 𝐴, 𝑧 ∈ dom (𝐹‘𝑦) ↦ ((𝐹‘𝑦)‘𝑧)):∪ 𝑦 ∈ 𝐴 ({𝑦} × dom (𝐹‘𝑦))⟶𝐶) |
| 23 | 20, 22 | sylib 218 |
. . . . . . 7
⊢ (𝜑 → (𝑦 ∈ 𝐴, 𝑧 ∈ dom (𝐹‘𝑦) ↦ ((𝐹‘𝑦)‘𝑧)):∪ 𝑦 ∈ 𝐴 ({𝑦} × dom (𝐹‘𝑦))⟶𝐶) |
| 24 | | ablfaclem2.l |
. . . . . . . 8
⊢ 𝐿 = ∪ 𝑦 ∈ 𝐴 ({𝑦} × dom (𝐹‘𝑦)) |
| 25 | 24 | feq2i 6728 |
. . . . . . 7
⊢ ((𝑦 ∈ 𝐴, 𝑧 ∈ dom (𝐹‘𝑦) ↦ ((𝐹‘𝑦)‘𝑧)):𝐿⟶𝐶 ↔ (𝑦 ∈ 𝐴, 𝑧 ∈ dom (𝐹‘𝑦) ↦ ((𝐹‘𝑦)‘𝑧)):∪ 𝑦 ∈ 𝐴 ({𝑦} × dom (𝐹‘𝑦))⟶𝐶) |
| 26 | 23, 25 | sylibr 234 |
. . . . . 6
⊢ (𝜑 → (𝑦 ∈ 𝐴, 𝑧 ∈ dom (𝐹‘𝑦) ↦ ((𝐹‘𝑦)‘𝑧)):𝐿⟶𝐶) |
| 27 | | ablfaclem2.g |
. . . . . . 7
⊢ (𝜑 → 𝐻:(0..^(♯‘𝐿))–1-1-onto→𝐿) |
| 28 | | f1of 6848 |
. . . . . . 7
⊢ (𝐻:(0..^(♯‘𝐿))–1-1-onto→𝐿 → 𝐻:(0..^(♯‘𝐿))⟶𝐿) |
| 29 | 27, 28 | syl 17 |
. . . . . 6
⊢ (𝜑 → 𝐻:(0..^(♯‘𝐿))⟶𝐿) |
| 30 | | fco 6760 |
. . . . . 6
⊢ (((𝑦 ∈ 𝐴, 𝑧 ∈ dom (𝐹‘𝑦) ↦ ((𝐹‘𝑦)‘𝑧)):𝐿⟶𝐶 ∧ 𝐻:(0..^(♯‘𝐿))⟶𝐿) → ((𝑦 ∈ 𝐴, 𝑧 ∈ dom (𝐹‘𝑦) ↦ ((𝐹‘𝑦)‘𝑧)) ∘ 𝐻):(0..^(♯‘𝐿))⟶𝐶) |
| 31 | 26, 29, 30 | syl2anc 584 |
. . . . 5
⊢ (𝜑 → ((𝑦 ∈ 𝐴, 𝑧 ∈ dom (𝐹‘𝑦) ↦ ((𝐹‘𝑦)‘𝑧)) ∘ 𝐻):(0..^(♯‘𝐿))⟶𝐶) |
| 32 | | iswrdi 14556 |
. . . . 5
⊢ (((𝑦 ∈ 𝐴, 𝑧 ∈ dom (𝐹‘𝑦) ↦ ((𝐹‘𝑦)‘𝑧)) ∘ 𝐻):(0..^(♯‘𝐿))⟶𝐶 → ((𝑦 ∈ 𝐴, 𝑧 ∈ dom (𝐹‘𝑦) ↦ ((𝐹‘𝑦)‘𝑧)) ∘ 𝐻) ∈ Word 𝐶) |
| 33 | 31, 32 | syl 17 |
. . . 4
⊢ (𝜑 → ((𝑦 ∈ 𝐴, 𝑧 ∈ dom (𝐹‘𝑦) ↦ ((𝐹‘𝑦)‘𝑧)) ∘ 𝐻) ∈ Word 𝐶) |
| 34 | | ablfaclem2.q |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → ∀𝑦 ∈ 𝐴 (𝐹‘𝑦) ∈ (𝑊‘(𝑆‘𝑦))) |
| 35 | 34 | r19.21bi 3251 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐴) → (𝐹‘𝑦) ∈ (𝑊‘(𝑆‘𝑦))) |
| 36 | 8 | ssrab3 4082 |
. . . . . . . . . . . . . . . . . . 19
⊢ 𝐴 ⊆
ℙ |
| 37 | 36 | a1i 11 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → 𝐴 ⊆ ℙ) |
| 38 | 3, 7, 9, 1, 6, 37 | ablfac1b 20090 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → 𝐺dom DProd 𝑆) |
| 39 | 3 | fvexi 6920 |
. . . . . . . . . . . . . . . . . . . 20
⊢ 𝐵 ∈ V |
| 40 | 39 | rabex 5339 |
. . . . . . . . . . . . . . . . . . 19
⊢ {𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ (𝑝↑(𝑝 pCnt (♯‘𝐵)))} ∈ V |
| 41 | 40, 9 | dmmpti 6712 |
. . . . . . . . . . . . . . . . . 18
⊢ dom 𝑆 = 𝐴 |
| 42 | 41 | a1i 11 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → dom 𝑆 = 𝐴) |
| 43 | 38, 42 | dprdf2 20027 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → 𝑆:𝐴⟶(SubGrp‘𝐺)) |
| 44 | 43 | ffvelcdmda 7104 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐴) → (𝑆‘𝑦) ∈ (SubGrp‘𝐺)) |
| 45 | 3, 5, 1, 6, 7, 8, 9, 10 | ablfaclem1 20105 |
. . . . . . . . . . . . . . 15
⊢ ((𝑆‘𝑦) ∈ (SubGrp‘𝐺) → (𝑊‘(𝑆‘𝑦)) = {𝑠 ∈ Word 𝐶 ∣ (𝐺dom DProd 𝑠 ∧ (𝐺 DProd 𝑠) = (𝑆‘𝑦))}) |
| 46 | 44, 45 | syl 17 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐴) → (𝑊‘(𝑆‘𝑦)) = {𝑠 ∈ Word 𝐶 ∣ (𝐺dom DProd 𝑠 ∧ (𝐺 DProd 𝑠) = (𝑆‘𝑦))}) |
| 47 | 35, 46 | eleqtrd 2843 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐴) → (𝐹‘𝑦) ∈ {𝑠 ∈ Word 𝐶 ∣ (𝐺dom DProd 𝑠 ∧ (𝐺 DProd 𝑠) = (𝑆‘𝑦))}) |
| 48 | | breq2 5147 |
. . . . . . . . . . . . . . . 16
⊢ (𝑠 = (𝐹‘𝑦) → (𝐺dom DProd 𝑠 ↔ 𝐺dom DProd (𝐹‘𝑦))) |
| 49 | | oveq2 7439 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑠 = (𝐹‘𝑦) → (𝐺 DProd 𝑠) = (𝐺 DProd (𝐹‘𝑦))) |
| 50 | 49 | eqeq1d 2739 |
. . . . . . . . . . . . . . . 16
⊢ (𝑠 = (𝐹‘𝑦) → ((𝐺 DProd 𝑠) = (𝑆‘𝑦) ↔ (𝐺 DProd (𝐹‘𝑦)) = (𝑆‘𝑦))) |
| 51 | 48, 50 | anbi12d 632 |
. . . . . . . . . . . . . . 15
⊢ (𝑠 = (𝐹‘𝑦) → ((𝐺dom DProd 𝑠 ∧ (𝐺 DProd 𝑠) = (𝑆‘𝑦)) ↔ (𝐺dom DProd (𝐹‘𝑦) ∧ (𝐺 DProd (𝐹‘𝑦)) = (𝑆‘𝑦)))) |
| 52 | 51 | elrab 3692 |
. . . . . . . . . . . . . 14
⊢ ((𝐹‘𝑦) ∈ {𝑠 ∈ Word 𝐶 ∣ (𝐺dom DProd 𝑠 ∧ (𝐺 DProd 𝑠) = (𝑆‘𝑦))} ↔ ((𝐹‘𝑦) ∈ Word 𝐶 ∧ (𝐺dom DProd (𝐹‘𝑦) ∧ (𝐺 DProd (𝐹‘𝑦)) = (𝑆‘𝑦)))) |
| 53 | 52 | simprbi 496 |
. . . . . . . . . . . . 13
⊢ ((𝐹‘𝑦) ∈ {𝑠 ∈ Word 𝐶 ∣ (𝐺dom DProd 𝑠 ∧ (𝐺 DProd 𝑠) = (𝑆‘𝑦))} → (𝐺dom DProd (𝐹‘𝑦) ∧ (𝐺 DProd (𝐹‘𝑦)) = (𝑆‘𝑦))) |
| 54 | 47, 53 | syl 17 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐴) → (𝐺dom DProd (𝐹‘𝑦) ∧ (𝐺 DProd (𝐹‘𝑦)) = (𝑆‘𝑦))) |
| 55 | 54 | simpld 494 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐴) → 𝐺dom DProd (𝐹‘𝑦)) |
| 56 | | dprdf 20026 |
. . . . . . . . . . 11
⊢ (𝐺dom DProd (𝐹‘𝑦) → (𝐹‘𝑦):dom (𝐹‘𝑦)⟶(SubGrp‘𝐺)) |
| 57 | 55, 56 | syl 17 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐴) → (𝐹‘𝑦):dom (𝐹‘𝑦)⟶(SubGrp‘𝐺)) |
| 58 | 57 | ffvelcdmda 7104 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑦 ∈ 𝐴) ∧ 𝑧 ∈ dom (𝐹‘𝑦)) → ((𝐹‘𝑦)‘𝑧) ∈ (SubGrp‘𝐺)) |
| 59 | 58 | anasss 466 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑦 ∈ 𝐴 ∧ 𝑧 ∈ dom (𝐹‘𝑦))) → ((𝐹‘𝑦)‘𝑧) ∈ (SubGrp‘𝐺)) |
| 60 | 57 | feqmptd 6977 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐴) → (𝐹‘𝑦) = (𝑧 ∈ dom (𝐹‘𝑦) ↦ ((𝐹‘𝑦)‘𝑧))) |
| 61 | 55, 60 | breqtrd 5169 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐴) → 𝐺dom DProd (𝑧 ∈ dom (𝐹‘𝑦) ↦ ((𝐹‘𝑦)‘𝑧))) |
| 62 | 43 | feqmptd 6977 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑆 = (𝑦 ∈ 𝐴 ↦ (𝑆‘𝑦))) |
| 63 | 60 | oveq2d 7447 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐴) → (𝐺 DProd (𝐹‘𝑦)) = (𝐺 DProd (𝑧 ∈ dom (𝐹‘𝑦) ↦ ((𝐹‘𝑦)‘𝑧)))) |
| 64 | 54 | simprd 495 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐴) → (𝐺 DProd (𝐹‘𝑦)) = (𝑆‘𝑦)) |
| 65 | 63, 64 | eqtr3d 2779 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐴) → (𝐺 DProd (𝑧 ∈ dom (𝐹‘𝑦) ↦ ((𝐹‘𝑦)‘𝑧))) = (𝑆‘𝑦)) |
| 66 | 65 | mpteq2dva 5242 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑦 ∈ 𝐴 ↦ (𝐺 DProd (𝑧 ∈ dom (𝐹‘𝑦) ↦ ((𝐹‘𝑦)‘𝑧)))) = (𝑦 ∈ 𝐴 ↦ (𝑆‘𝑦))) |
| 67 | 62, 66 | eqtr4d 2780 |
. . . . . . . . 9
⊢ (𝜑 → 𝑆 = (𝑦 ∈ 𝐴 ↦ (𝐺 DProd (𝑧 ∈ dom (𝐹‘𝑦) ↦ ((𝐹‘𝑦)‘𝑧))))) |
| 68 | 38, 67 | breqtrd 5169 |
. . . . . . . 8
⊢ (𝜑 → 𝐺dom DProd (𝑦 ∈ 𝐴 ↦ (𝐺 DProd (𝑧 ∈ dom (𝐹‘𝑦) ↦ ((𝐹‘𝑦)‘𝑧))))) |
| 69 | 59, 61, 68 | dprd2d2 20064 |
. . . . . . 7
⊢ (𝜑 → (𝐺dom DProd (𝑦 ∈ 𝐴, 𝑧 ∈ dom (𝐹‘𝑦) ↦ ((𝐹‘𝑦)‘𝑧)) ∧ (𝐺 DProd (𝑦 ∈ 𝐴, 𝑧 ∈ dom (𝐹‘𝑦) ↦ ((𝐹‘𝑦)‘𝑧))) = (𝐺 DProd (𝑦 ∈ 𝐴 ↦ (𝐺 DProd (𝑧 ∈ dom (𝐹‘𝑦) ↦ ((𝐹‘𝑦)‘𝑧))))))) |
| 70 | 69 | simpld 494 |
. . . . . 6
⊢ (𝜑 → 𝐺dom DProd (𝑦 ∈ 𝐴, 𝑧 ∈ dom (𝐹‘𝑦) ↦ ((𝐹‘𝑦)‘𝑧))) |
| 71 | 26 | fdmd 6746 |
. . . . . 6
⊢ (𝜑 → dom (𝑦 ∈ 𝐴, 𝑧 ∈ dom (𝐹‘𝑦) ↦ ((𝐹‘𝑦)‘𝑧)) = 𝐿) |
| 72 | 70, 71, 27 | dprdf1o 20052 |
. . . . 5
⊢ (𝜑 → (𝐺dom DProd ((𝑦 ∈ 𝐴, 𝑧 ∈ dom (𝐹‘𝑦) ↦ ((𝐹‘𝑦)‘𝑧)) ∘ 𝐻) ∧ (𝐺 DProd ((𝑦 ∈ 𝐴, 𝑧 ∈ dom (𝐹‘𝑦) ↦ ((𝐹‘𝑦)‘𝑧)) ∘ 𝐻)) = (𝐺 DProd (𝑦 ∈ 𝐴, 𝑧 ∈ dom (𝐹‘𝑦) ↦ ((𝐹‘𝑦)‘𝑧))))) |
| 73 | 72 | simpld 494 |
. . . 4
⊢ (𝜑 → 𝐺dom DProd ((𝑦 ∈ 𝐴, 𝑧 ∈ dom (𝐹‘𝑦) ↦ ((𝐹‘𝑦)‘𝑧)) ∘ 𝐻)) |
| 74 | 72 | simprd 495 |
. . . . 5
⊢ (𝜑 → (𝐺 DProd ((𝑦 ∈ 𝐴, 𝑧 ∈ dom (𝐹‘𝑦) ↦ ((𝐹‘𝑦)‘𝑧)) ∘ 𝐻)) = (𝐺 DProd (𝑦 ∈ 𝐴, 𝑧 ∈ dom (𝐹‘𝑦) ↦ ((𝐹‘𝑦)‘𝑧)))) |
| 75 | 69 | simprd 495 |
. . . . 5
⊢ (𝜑 → (𝐺 DProd (𝑦 ∈ 𝐴, 𝑧 ∈ dom (𝐹‘𝑦) ↦ ((𝐹‘𝑦)‘𝑧))) = (𝐺 DProd (𝑦 ∈ 𝐴 ↦ (𝐺 DProd (𝑧 ∈ dom (𝐹‘𝑦) ↦ ((𝐹‘𝑦)‘𝑧)))))) |
| 76 | 67 | oveq2d 7447 |
. . . . . 6
⊢ (𝜑 → (𝐺 DProd 𝑆) = (𝐺 DProd (𝑦 ∈ 𝐴 ↦ (𝐺 DProd (𝑧 ∈ dom (𝐹‘𝑦) ↦ ((𝐹‘𝑦)‘𝑧)))))) |
| 77 | | ssidd 4007 |
. . . . . . 7
⊢ (𝜑 → 𝐴 ⊆ 𝐴) |
| 78 | 3, 7, 9, 1, 6, 37,
8, 77 | ablfac1c 20091 |
. . . . . 6
⊢ (𝜑 → (𝐺 DProd 𝑆) = 𝐵) |
| 79 | 76, 78 | eqtr3d 2779 |
. . . . 5
⊢ (𝜑 → (𝐺 DProd (𝑦 ∈ 𝐴 ↦ (𝐺 DProd (𝑧 ∈ dom (𝐹‘𝑦) ↦ ((𝐹‘𝑦)‘𝑧))))) = 𝐵) |
| 80 | 74, 75, 79 | 3eqtrd 2781 |
. . . 4
⊢ (𝜑 → (𝐺 DProd ((𝑦 ∈ 𝐴, 𝑧 ∈ dom (𝐹‘𝑦) ↦ ((𝐹‘𝑦)‘𝑧)) ∘ 𝐻)) = 𝐵) |
| 81 | | breq2 5147 |
. . . . . 6
⊢ (𝑠 = ((𝑦 ∈ 𝐴, 𝑧 ∈ dom (𝐹‘𝑦) ↦ ((𝐹‘𝑦)‘𝑧)) ∘ 𝐻) → (𝐺dom DProd 𝑠 ↔ 𝐺dom DProd ((𝑦 ∈ 𝐴, 𝑧 ∈ dom (𝐹‘𝑦) ↦ ((𝐹‘𝑦)‘𝑧)) ∘ 𝐻))) |
| 82 | | oveq2 7439 |
. . . . . . 7
⊢ (𝑠 = ((𝑦 ∈ 𝐴, 𝑧 ∈ dom (𝐹‘𝑦) ↦ ((𝐹‘𝑦)‘𝑧)) ∘ 𝐻) → (𝐺 DProd 𝑠) = (𝐺 DProd ((𝑦 ∈ 𝐴, 𝑧 ∈ dom (𝐹‘𝑦) ↦ ((𝐹‘𝑦)‘𝑧)) ∘ 𝐻))) |
| 83 | 82 | eqeq1d 2739 |
. . . . . 6
⊢ (𝑠 = ((𝑦 ∈ 𝐴, 𝑧 ∈ dom (𝐹‘𝑦) ↦ ((𝐹‘𝑦)‘𝑧)) ∘ 𝐻) → ((𝐺 DProd 𝑠) = 𝐵 ↔ (𝐺 DProd ((𝑦 ∈ 𝐴, 𝑧 ∈ dom (𝐹‘𝑦) ↦ ((𝐹‘𝑦)‘𝑧)) ∘ 𝐻)) = 𝐵)) |
| 84 | 81, 83 | anbi12d 632 |
. . . . 5
⊢ (𝑠 = ((𝑦 ∈ 𝐴, 𝑧 ∈ dom (𝐹‘𝑦) ↦ ((𝐹‘𝑦)‘𝑧)) ∘ 𝐻) → ((𝐺dom DProd 𝑠 ∧ (𝐺 DProd 𝑠) = 𝐵) ↔ (𝐺dom DProd ((𝑦 ∈ 𝐴, 𝑧 ∈ dom (𝐹‘𝑦) ↦ ((𝐹‘𝑦)‘𝑧)) ∘ 𝐻) ∧ (𝐺 DProd ((𝑦 ∈ 𝐴, 𝑧 ∈ dom (𝐹‘𝑦) ↦ ((𝐹‘𝑦)‘𝑧)) ∘ 𝐻)) = 𝐵))) |
| 85 | 84 | rspcev 3622 |
. . . 4
⊢ ((((𝑦 ∈ 𝐴, 𝑧 ∈ dom (𝐹‘𝑦) ↦ ((𝐹‘𝑦)‘𝑧)) ∘ 𝐻) ∈ Word 𝐶 ∧ (𝐺dom DProd ((𝑦 ∈ 𝐴, 𝑧 ∈ dom (𝐹‘𝑦) ↦ ((𝐹‘𝑦)‘𝑧)) ∘ 𝐻) ∧ (𝐺 DProd ((𝑦 ∈ 𝐴, 𝑧 ∈ dom (𝐹‘𝑦) ↦ ((𝐹‘𝑦)‘𝑧)) ∘ 𝐻)) = 𝐵)) → ∃𝑠 ∈ Word 𝐶(𝐺dom DProd 𝑠 ∧ (𝐺 DProd 𝑠) = 𝐵)) |
| 86 | 33, 73, 80, 85 | syl12anc 837 |
. . 3
⊢ (𝜑 → ∃𝑠 ∈ Word 𝐶(𝐺dom DProd 𝑠 ∧ (𝐺 DProd 𝑠) = 𝐵)) |
| 87 | | rabn0 4389 |
. . 3
⊢ ({𝑠 ∈ Word 𝐶 ∣ (𝐺dom DProd 𝑠 ∧ (𝐺 DProd 𝑠) = 𝐵)} ≠ ∅ ↔ ∃𝑠 ∈ Word 𝐶(𝐺dom DProd 𝑠 ∧ (𝐺 DProd 𝑠) = 𝐵)) |
| 88 | 86, 87 | sylibr 234 |
. 2
⊢ (𝜑 → {𝑠 ∈ Word 𝐶 ∣ (𝐺dom DProd 𝑠 ∧ (𝐺 DProd 𝑠) = 𝐵)} ≠ ∅) |
| 89 | 12, 88 | eqnetrd 3008 |
1
⊢ (𝜑 → (𝑊‘𝐵) ≠ ∅) |