Step | Hyp | Ref
| Expression |
1 | | simplr 769 |
. . . . 5
⊢ ((((𝐷 ∈ Fin ∧ 𝑄 ∈ 𝐴) ∧ 𝑣 ∈ Word ran (pmTrsp‘𝐷)) ∧ 𝑄 = (𝑆 Σg 𝑣)) → 𝑣 ∈ Word ran (pmTrsp‘𝐷)) |
2 | | lencl 13974 |
. . . . . . . 8
⊢ (𝑣 ∈ Word ran
(pmTrsp‘𝐷) →
(♯‘𝑣) ∈
ℕ0) |
3 | 2 | ad2antlr 727 |
. . . . . . 7
⊢ ((((𝐷 ∈ Fin ∧ 𝑄 ∈ 𝐴) ∧ 𝑣 ∈ Word ran (pmTrsp‘𝐷)) ∧ 𝑄 = (𝑆 Σg 𝑣)) → (♯‘𝑣) ∈
ℕ0) |
4 | 3 | nn0zd 12166 |
. . . . . 6
⊢ ((((𝐷 ∈ Fin ∧ 𝑄 ∈ 𝐴) ∧ 𝑣 ∈ Word ran (pmTrsp‘𝐷)) ∧ 𝑄 = (𝑆 Σg 𝑣)) → (♯‘𝑣) ∈
ℤ) |
5 | | simpr 488 |
. . . . . . . 8
⊢ ((((𝐷 ∈ Fin ∧ 𝑄 ∈ 𝐴) ∧ 𝑣 ∈ Word ran (pmTrsp‘𝐷)) ∧ 𝑄 = (𝑆 Σg 𝑣)) → 𝑄 = (𝑆 Σg 𝑣)) |
6 | 5 | fveq2d 6678 |
. . . . . . 7
⊢ ((((𝐷 ∈ Fin ∧ 𝑄 ∈ 𝐴) ∧ 𝑣 ∈ Word ran (pmTrsp‘𝐷)) ∧ 𝑄 = (𝑆 Σg 𝑣)) → ((pmSgn‘𝐷)‘𝑄) = ((pmSgn‘𝐷)‘(𝑆 Σg 𝑣))) |
7 | | simplll 775 |
. . . . . . . 8
⊢ ((((𝐷 ∈ Fin ∧ 𝑄 ∈ 𝐴) ∧ 𝑣 ∈ Word ran (pmTrsp‘𝐷)) ∧ 𝑄 = (𝑆 Σg 𝑣)) → 𝐷 ∈ Fin) |
8 | | simpllr 776 |
. . . . . . . . 9
⊢ ((((𝐷 ∈ Fin ∧ 𝑄 ∈ 𝐴) ∧ 𝑣 ∈ Word ran (pmTrsp‘𝐷)) ∧ 𝑄 = (𝑆 Σg 𝑣)) → 𝑄 ∈ 𝐴) |
9 | | cyc3genpm.a |
. . . . . . . . 9
⊢ 𝐴 = (pmEven‘𝐷) |
10 | 8, 9 | eleqtrdi 2843 |
. . . . . . . 8
⊢ ((((𝐷 ∈ Fin ∧ 𝑄 ∈ 𝐴) ∧ 𝑣 ∈ Word ran (pmTrsp‘𝐷)) ∧ 𝑄 = (𝑆 Σg 𝑣)) → 𝑄 ∈ (pmEven‘𝐷)) |
11 | | cyc3genpm.s |
. . . . . . . . 9
⊢ 𝑆 = (SymGrp‘𝐷) |
12 | | eqid 2738 |
. . . . . . . . 9
⊢
(Base‘𝑆) =
(Base‘𝑆) |
13 | | eqid 2738 |
. . . . . . . . 9
⊢
(pmSgn‘𝐷) =
(pmSgn‘𝐷) |
14 | 11, 12, 13 | psgnevpm 20405 |
. . . . . . . 8
⊢ ((𝐷 ∈ Fin ∧ 𝑄 ∈ (pmEven‘𝐷)) → ((pmSgn‘𝐷)‘𝑄) = 1) |
15 | 7, 10, 14 | syl2anc 587 |
. . . . . . 7
⊢ ((((𝐷 ∈ Fin ∧ 𝑄 ∈ 𝐴) ∧ 𝑣 ∈ Word ran (pmTrsp‘𝐷)) ∧ 𝑄 = (𝑆 Σg 𝑣)) → ((pmSgn‘𝐷)‘𝑄) = 1) |
16 | | eqid 2738 |
. . . . . . . . 9
⊢ ran
(pmTrsp‘𝐷) = ran
(pmTrsp‘𝐷) |
17 | 11, 16, 13 | psgnvalii 18755 |
. . . . . . . 8
⊢ ((𝐷 ∈ Fin ∧ 𝑣 ∈ Word ran
(pmTrsp‘𝐷)) →
((pmSgn‘𝐷)‘(𝑆 Σg 𝑣)) =
(-1↑(♯‘𝑣))) |
18 | 7, 1, 17 | syl2anc 587 |
. . . . . . 7
⊢ ((((𝐷 ∈ Fin ∧ 𝑄 ∈ 𝐴) ∧ 𝑣 ∈ Word ran (pmTrsp‘𝐷)) ∧ 𝑄 = (𝑆 Σg 𝑣)) → ((pmSgn‘𝐷)‘(𝑆 Σg 𝑣)) =
(-1↑(♯‘𝑣))) |
19 | 6, 15, 18 | 3eqtr3rd 2782 |
. . . . . 6
⊢ ((((𝐷 ∈ Fin ∧ 𝑄 ∈ 𝐴) ∧ 𝑣 ∈ Word ran (pmTrsp‘𝐷)) ∧ 𝑄 = (𝑆 Σg 𝑣)) →
(-1↑(♯‘𝑣))
= 1) |
20 | | m1exp1 15821 |
. . . . . . 7
⊢
((♯‘𝑣)
∈ ℤ → ((-1↑(♯‘𝑣)) = 1 ↔ 2 ∥ (♯‘𝑣))) |
21 | 20 | biimpa 480 |
. . . . . 6
⊢
(((♯‘𝑣)
∈ ℤ ∧ (-1↑(♯‘𝑣)) = 1) → 2 ∥ (♯‘𝑣)) |
22 | 4, 19, 21 | syl2anc 587 |
. . . . 5
⊢ ((((𝐷 ∈ Fin ∧ 𝑄 ∈ 𝐴) ∧ 𝑣 ∈ Word ran (pmTrsp‘𝐷)) ∧ 𝑄 = (𝑆 Σg 𝑣)) → 2 ∥
(♯‘𝑣)) |
23 | | oveq2 7178 |
. . . . . . . . . 10
⊢ (𝑥 = ∅ → (𝑆 Σg
𝑥) = (𝑆 Σg
∅)) |
24 | 23 | eqeq1d 2740 |
. . . . . . . . 9
⊢ (𝑥 = ∅ → ((𝑆 Σg
𝑥) = (𝑆 Σg 𝑤) ↔ (𝑆 Σg ∅) =
(𝑆
Σg 𝑤))) |
25 | 24 | rexbidv 3207 |
. . . . . . . 8
⊢ (𝑥 = ∅ → (∃𝑤 ∈ Word 𝐶(𝑆 Σg 𝑥) = (𝑆 Σg 𝑤) ↔ ∃𝑤 ∈ Word 𝐶(𝑆 Σg ∅) =
(𝑆
Σg 𝑤))) |
26 | 25 | imbi2d 344 |
. . . . . . 7
⊢ (𝑥 = ∅ → ((𝐷 ∈ Fin → ∃𝑤 ∈ Word 𝐶(𝑆 Σg 𝑥) = (𝑆 Σg 𝑤)) ↔ (𝐷 ∈ Fin → ∃𝑤 ∈ Word 𝐶(𝑆 Σg ∅) =
(𝑆
Σg 𝑤)))) |
27 | | oveq2 7178 |
. . . . . . . . . 10
⊢ (𝑥 = 𝑢 → (𝑆 Σg 𝑥) = (𝑆 Σg 𝑢)) |
28 | 27 | eqeq1d 2740 |
. . . . . . . . 9
⊢ (𝑥 = 𝑢 → ((𝑆 Σg 𝑥) = (𝑆 Σg 𝑤) ↔ (𝑆 Σg 𝑢) = (𝑆 Σg 𝑤))) |
29 | 28 | rexbidv 3207 |
. . . . . . . 8
⊢ (𝑥 = 𝑢 → (∃𝑤 ∈ Word 𝐶(𝑆 Σg 𝑥) = (𝑆 Σg 𝑤) ↔ ∃𝑤 ∈ Word 𝐶(𝑆 Σg 𝑢) = (𝑆 Σg 𝑤))) |
30 | 29 | imbi2d 344 |
. . . . . . 7
⊢ (𝑥 = 𝑢 → ((𝐷 ∈ Fin → ∃𝑤 ∈ Word 𝐶(𝑆 Σg 𝑥) = (𝑆 Σg 𝑤)) ↔ (𝐷 ∈ Fin → ∃𝑤 ∈ Word 𝐶(𝑆 Σg 𝑢) = (𝑆 Σg 𝑤)))) |
31 | | oveq2 7178 |
. . . . . . . . . 10
⊢ (𝑥 = (𝑢 ++ 〈“𝑖𝑗”〉) → (𝑆 Σg 𝑥) = (𝑆 Σg (𝑢 ++ 〈“𝑖𝑗”〉))) |
32 | 31 | eqeq1d 2740 |
. . . . . . . . 9
⊢ (𝑥 = (𝑢 ++ 〈“𝑖𝑗”〉) → ((𝑆 Σg 𝑥) = (𝑆 Σg 𝑤) ↔ (𝑆 Σg (𝑢 ++ 〈“𝑖𝑗”〉)) = (𝑆 Σg 𝑤))) |
33 | 32 | rexbidv 3207 |
. . . . . . . 8
⊢ (𝑥 = (𝑢 ++ 〈“𝑖𝑗”〉) → (∃𝑤 ∈ Word 𝐶(𝑆 Σg 𝑥) = (𝑆 Σg 𝑤) ↔ ∃𝑤 ∈ Word 𝐶(𝑆 Σg (𝑢 ++ 〈“𝑖𝑗”〉)) = (𝑆 Σg 𝑤))) |
34 | 33 | imbi2d 344 |
. . . . . . 7
⊢ (𝑥 = (𝑢 ++ 〈“𝑖𝑗”〉) → ((𝐷 ∈ Fin → ∃𝑤 ∈ Word 𝐶(𝑆 Σg 𝑥) = (𝑆 Σg 𝑤)) ↔ (𝐷 ∈ Fin → ∃𝑤 ∈ Word 𝐶(𝑆 Σg (𝑢 ++ 〈“𝑖𝑗”〉)) = (𝑆 Σg 𝑤)))) |
35 | | oveq2 7178 |
. . . . . . . . . 10
⊢ (𝑥 = 𝑣 → (𝑆 Σg 𝑥) = (𝑆 Σg 𝑣)) |
36 | 35 | eqeq1d 2740 |
. . . . . . . . 9
⊢ (𝑥 = 𝑣 → ((𝑆 Σg 𝑥) = (𝑆 Σg 𝑤) ↔ (𝑆 Σg 𝑣) = (𝑆 Σg 𝑤))) |
37 | 36 | rexbidv 3207 |
. . . . . . . 8
⊢ (𝑥 = 𝑣 → (∃𝑤 ∈ Word 𝐶(𝑆 Σg 𝑥) = (𝑆 Σg 𝑤) ↔ ∃𝑤 ∈ Word 𝐶(𝑆 Σg 𝑣) = (𝑆 Σg 𝑤))) |
38 | 37 | imbi2d 344 |
. . . . . . 7
⊢ (𝑥 = 𝑣 → ((𝐷 ∈ Fin → ∃𝑤 ∈ Word 𝐶(𝑆 Σg 𝑥) = (𝑆 Σg 𝑤)) ↔ (𝐷 ∈ Fin → ∃𝑤 ∈ Word 𝐶(𝑆 Σg 𝑣) = (𝑆 Σg 𝑤)))) |
39 | | wrd0 13980 |
. . . . . . . . 9
⊢ ∅
∈ Word 𝐶 |
40 | 39 | a1i 11 |
. . . . . . . 8
⊢ (𝐷 ∈ Fin → ∅
∈ Word 𝐶) |
41 | | simpr 488 |
. . . . . . . . . 10
⊢ ((𝐷 ∈ Fin ∧ 𝑤 = ∅) → 𝑤 = ∅) |
42 | 41 | oveq2d 7186 |
. . . . . . . . 9
⊢ ((𝐷 ∈ Fin ∧ 𝑤 = ∅) → (𝑆 Σg
𝑤) = (𝑆 Σg
∅)) |
43 | 42 | eqeq2d 2749 |
. . . . . . . 8
⊢ ((𝐷 ∈ Fin ∧ 𝑤 = ∅) → ((𝑆 Σg
∅) = (𝑆
Σg 𝑤) ↔ (𝑆 Σg ∅) =
(𝑆
Σg ∅))) |
44 | | eqidd 2739 |
. . . . . . . 8
⊢ (𝐷 ∈ Fin → (𝑆 Σg
∅) = (𝑆
Σg ∅)) |
45 | 40, 43, 44 | rspcedvd 3529 |
. . . . . . 7
⊢ (𝐷 ∈ Fin → ∃𝑤 ∈ Word 𝐶(𝑆 Σg ∅) =
(𝑆
Σg 𝑤)) |
46 | | ccatcl 14015 |
. . . . . . . . . . . . . 14
⊢ ((𝑣 ∈ Word 𝐶 ∧ 𝑐 ∈ Word 𝐶) → (𝑣 ++ 𝑐) ∈ Word 𝐶) |
47 | 46 | ad5ant24 761 |
. . . . . . . . . . . . 13
⊢
((((((((𝑢 ∈
Word ran (pmTrsp‘𝐷)
∧ 𝑖 ∈ ran
(pmTrsp‘𝐷)) ∧
𝑗 ∈ ran
(pmTrsp‘𝐷)) ∧
𝐷 ∈ Fin) ∧ 𝑣 ∈ Word 𝐶) ∧ (𝑆 Σg 𝑢) = (𝑆 Σg 𝑣)) ∧ 𝑐 ∈ Word 𝐶) ∧ (𝑖(+g‘𝑆)𝑗) = (𝑆 Σg 𝑐)) → (𝑣 ++ 𝑐) ∈ Word 𝐶) |
48 | | oveq2 7178 |
. . . . . . . . . . . . . . 15
⊢ (𝑤 = (𝑣 ++ 𝑐) → (𝑆 Σg 𝑤) = (𝑆 Σg (𝑣 ++ 𝑐))) |
49 | 48 | eqeq2d 2749 |
. . . . . . . . . . . . . 14
⊢ (𝑤 = (𝑣 ++ 𝑐) → ((𝑆 Σg (𝑢 ++ 〈“𝑖𝑗”〉)) = (𝑆 Σg 𝑤) ↔ (𝑆 Σg (𝑢 ++ 〈“𝑖𝑗”〉)) = (𝑆 Σg (𝑣 ++ 𝑐)))) |
50 | 49 | adantl 485 |
. . . . . . . . . . . . 13
⊢
(((((((((𝑢 ∈
Word ran (pmTrsp‘𝐷)
∧ 𝑖 ∈ ran
(pmTrsp‘𝐷)) ∧
𝑗 ∈ ran
(pmTrsp‘𝐷)) ∧
𝐷 ∈ Fin) ∧ 𝑣 ∈ Word 𝐶) ∧ (𝑆 Σg 𝑢) = (𝑆 Σg 𝑣)) ∧ 𝑐 ∈ Word 𝐶) ∧ (𝑖(+g‘𝑆)𝑗) = (𝑆 Σg 𝑐)) ∧ 𝑤 = (𝑣 ++ 𝑐)) → ((𝑆 Σg (𝑢 ++ 〈“𝑖𝑗”〉)) = (𝑆 Σg 𝑤) ↔ (𝑆 Σg (𝑢 ++ 〈“𝑖𝑗”〉)) = (𝑆 Σg (𝑣 ++ 𝑐)))) |
51 | | simpllr 776 |
. . . . . . . . . . . . . . 15
⊢
((((((((𝑢 ∈
Word ran (pmTrsp‘𝐷)
∧ 𝑖 ∈ ran
(pmTrsp‘𝐷)) ∧
𝑗 ∈ ran
(pmTrsp‘𝐷)) ∧
𝐷 ∈ Fin) ∧ 𝑣 ∈ Word 𝐶) ∧ (𝑆 Σg 𝑢) = (𝑆 Σg 𝑣)) ∧ 𝑐 ∈ Word 𝐶) ∧ (𝑖(+g‘𝑆)𝑗) = (𝑆 Σg 𝑐)) → (𝑆 Σg 𝑢) = (𝑆 Σg 𝑣)) |
52 | | simpllr 776 |
. . . . . . . . . . . . . . . . . . 19
⊢
((((((𝑢 ∈ Word
ran (pmTrsp‘𝐷) ∧
𝑖 ∈ ran
(pmTrsp‘𝐷)) ∧
𝑗 ∈ ran
(pmTrsp‘𝐷)) ∧
𝐷 ∈ Fin) ∧ 𝑣 ∈ Word 𝐶) ∧ (𝑆 Σg 𝑢) = (𝑆 Σg 𝑣)) → 𝐷 ∈ Fin) |
53 | 52 | ad2antrr 726 |
. . . . . . . . . . . . . . . . . 18
⊢
((((((((𝑢 ∈
Word ran (pmTrsp‘𝐷)
∧ 𝑖 ∈ ran
(pmTrsp‘𝐷)) ∧
𝑗 ∈ ran
(pmTrsp‘𝐷)) ∧
𝐷 ∈ Fin) ∧ 𝑣 ∈ Word 𝐶) ∧ (𝑆 Σg 𝑢) = (𝑆 Σg 𝑣)) ∧ 𝑐 ∈ Word 𝐶) ∧ (𝑖(+g‘𝑆)𝑗) = (𝑆 Σg 𝑐)) → 𝐷 ∈ Fin) |
54 | 11 | symggrp 18646 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝐷 ∈ Fin → 𝑆 ∈ Grp) |
55 | | grpmnd 18226 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑆 ∈ Grp → 𝑆 ∈ Mnd) |
56 | 53, 54, 55 | 3syl 18 |
. . . . . . . . . . . . . . . . 17
⊢
((((((((𝑢 ∈
Word ran (pmTrsp‘𝐷)
∧ 𝑖 ∈ ran
(pmTrsp‘𝐷)) ∧
𝑗 ∈ ran
(pmTrsp‘𝐷)) ∧
𝐷 ∈ Fin) ∧ 𝑣 ∈ Word 𝐶) ∧ (𝑆 Σg 𝑢) = (𝑆 Σg 𝑣)) ∧ 𝑐 ∈ Word 𝐶) ∧ (𝑖(+g‘𝑆)𝑗) = (𝑆 Σg 𝑐)) → 𝑆 ∈ Mnd) |
57 | 16, 11, 12 | symgtrf 18715 |
. . . . . . . . . . . . . . . . . . 19
⊢ ran
(pmTrsp‘𝐷) ⊆
(Base‘𝑆) |
58 | 57 | a1i 11 |
. . . . . . . . . . . . . . . . . 18
⊢
((((((((𝑢 ∈
Word ran (pmTrsp‘𝐷)
∧ 𝑖 ∈ ran
(pmTrsp‘𝐷)) ∧
𝑗 ∈ ran
(pmTrsp‘𝐷)) ∧
𝐷 ∈ Fin) ∧ 𝑣 ∈ Word 𝐶) ∧ (𝑆 Σg 𝑢) = (𝑆 Σg 𝑣)) ∧ 𝑐 ∈ Word 𝐶) ∧ (𝑖(+g‘𝑆)𝑗) = (𝑆 Σg 𝑐)) → ran
(pmTrsp‘𝐷) ⊆
(Base‘𝑆)) |
59 | | simp-5r 786 |
. . . . . . . . . . . . . . . . . . 19
⊢
((((((𝑢 ∈ Word
ran (pmTrsp‘𝐷) ∧
𝑖 ∈ ran
(pmTrsp‘𝐷)) ∧
𝑗 ∈ ran
(pmTrsp‘𝐷)) ∧
𝐷 ∈ Fin) ∧ 𝑣 ∈ Word 𝐶) ∧ (𝑆 Σg 𝑢) = (𝑆 Σg 𝑣)) → 𝑖 ∈ ran (pmTrsp‘𝐷)) |
60 | 59 | ad2antrr 726 |
. . . . . . . . . . . . . . . . . 18
⊢
((((((((𝑢 ∈
Word ran (pmTrsp‘𝐷)
∧ 𝑖 ∈ ran
(pmTrsp‘𝐷)) ∧
𝑗 ∈ ran
(pmTrsp‘𝐷)) ∧
𝐷 ∈ Fin) ∧ 𝑣 ∈ Word 𝐶) ∧ (𝑆 Σg 𝑢) = (𝑆 Σg 𝑣)) ∧ 𝑐 ∈ Word 𝐶) ∧ (𝑖(+g‘𝑆)𝑗) = (𝑆 Σg 𝑐)) → 𝑖 ∈ ran (pmTrsp‘𝐷)) |
61 | 58, 60 | sseldd 3878 |
. . . . . . . . . . . . . . . . 17
⊢
((((((((𝑢 ∈
Word ran (pmTrsp‘𝐷)
∧ 𝑖 ∈ ran
(pmTrsp‘𝐷)) ∧
𝑗 ∈ ran
(pmTrsp‘𝐷)) ∧
𝐷 ∈ Fin) ∧ 𝑣 ∈ Word 𝐶) ∧ (𝑆 Σg 𝑢) = (𝑆 Σg 𝑣)) ∧ 𝑐 ∈ Word 𝐶) ∧ (𝑖(+g‘𝑆)𝑗) = (𝑆 Σg 𝑐)) → 𝑖 ∈ (Base‘𝑆)) |
62 | | simp-6r 788 |
. . . . . . . . . . . . . . . . . 18
⊢
((((((((𝑢 ∈
Word ran (pmTrsp‘𝐷)
∧ 𝑖 ∈ ran
(pmTrsp‘𝐷)) ∧
𝑗 ∈ ran
(pmTrsp‘𝐷)) ∧
𝐷 ∈ Fin) ∧ 𝑣 ∈ Word 𝐶) ∧ (𝑆 Σg 𝑢) = (𝑆 Σg 𝑣)) ∧ 𝑐 ∈ Word 𝐶) ∧ (𝑖(+g‘𝑆)𝑗) = (𝑆 Σg 𝑐)) → 𝑗 ∈ ran (pmTrsp‘𝐷)) |
63 | 58, 62 | sseldd 3878 |
. . . . . . . . . . . . . . . . 17
⊢
((((((((𝑢 ∈
Word ran (pmTrsp‘𝐷)
∧ 𝑖 ∈ ran
(pmTrsp‘𝐷)) ∧
𝑗 ∈ ran
(pmTrsp‘𝐷)) ∧
𝐷 ∈ Fin) ∧ 𝑣 ∈ Word 𝐶) ∧ (𝑆 Σg 𝑢) = (𝑆 Σg 𝑣)) ∧ 𝑐 ∈ Word 𝐶) ∧ (𝑖(+g‘𝑆)𝑗) = (𝑆 Σg 𝑐)) → 𝑗 ∈ (Base‘𝑆)) |
64 | | eqid 2738 |
. . . . . . . . . . . . . . . . . 18
⊢
(+g‘𝑆) = (+g‘𝑆) |
65 | 12, 64 | gsumws2 18123 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑆 ∈ Mnd ∧ 𝑖 ∈ (Base‘𝑆) ∧ 𝑗 ∈ (Base‘𝑆)) → (𝑆 Σg
〈“𝑖𝑗”〉) = (𝑖(+g‘𝑆)𝑗)) |
66 | 56, 61, 63, 65 | syl3anc 1372 |
. . . . . . . . . . . . . . . 16
⊢
((((((((𝑢 ∈
Word ran (pmTrsp‘𝐷)
∧ 𝑖 ∈ ran
(pmTrsp‘𝐷)) ∧
𝑗 ∈ ran
(pmTrsp‘𝐷)) ∧
𝐷 ∈ Fin) ∧ 𝑣 ∈ Word 𝐶) ∧ (𝑆 Σg 𝑢) = (𝑆 Σg 𝑣)) ∧ 𝑐 ∈ Word 𝐶) ∧ (𝑖(+g‘𝑆)𝑗) = (𝑆 Σg 𝑐)) → (𝑆 Σg
〈“𝑖𝑗”〉) = (𝑖(+g‘𝑆)𝑗)) |
67 | | simpr 488 |
. . . . . . . . . . . . . . . 16
⊢
((((((((𝑢 ∈
Word ran (pmTrsp‘𝐷)
∧ 𝑖 ∈ ran
(pmTrsp‘𝐷)) ∧
𝑗 ∈ ran
(pmTrsp‘𝐷)) ∧
𝐷 ∈ Fin) ∧ 𝑣 ∈ Word 𝐶) ∧ (𝑆 Σg 𝑢) = (𝑆 Σg 𝑣)) ∧ 𝑐 ∈ Word 𝐶) ∧ (𝑖(+g‘𝑆)𝑗) = (𝑆 Σg 𝑐)) → (𝑖(+g‘𝑆)𝑗) = (𝑆 Σg 𝑐)) |
68 | 66, 67 | eqtrd 2773 |
. . . . . . . . . . . . . . 15
⊢
((((((((𝑢 ∈
Word ran (pmTrsp‘𝐷)
∧ 𝑖 ∈ ran
(pmTrsp‘𝐷)) ∧
𝑗 ∈ ran
(pmTrsp‘𝐷)) ∧
𝐷 ∈ Fin) ∧ 𝑣 ∈ Word 𝐶) ∧ (𝑆 Σg 𝑢) = (𝑆 Σg 𝑣)) ∧ 𝑐 ∈ Word 𝐶) ∧ (𝑖(+g‘𝑆)𝑗) = (𝑆 Σg 𝑐)) → (𝑆 Σg
〈“𝑖𝑗”〉) = (𝑆 Σg
𝑐)) |
69 | 51, 68 | oveq12d 7188 |
. . . . . . . . . . . . . 14
⊢
((((((((𝑢 ∈
Word ran (pmTrsp‘𝐷)
∧ 𝑖 ∈ ran
(pmTrsp‘𝐷)) ∧
𝑗 ∈ ran
(pmTrsp‘𝐷)) ∧
𝐷 ∈ Fin) ∧ 𝑣 ∈ Word 𝐶) ∧ (𝑆 Σg 𝑢) = (𝑆 Σg 𝑣)) ∧ 𝑐 ∈ Word 𝐶) ∧ (𝑖(+g‘𝑆)𝑗) = (𝑆 Σg 𝑐)) → ((𝑆 Σg 𝑢)(+g‘𝑆)(𝑆 Σg
〈“𝑖𝑗”〉)) = ((𝑆 Σg
𝑣)(+g‘𝑆)(𝑆 Σg 𝑐))) |
70 | | sswrd 13963 |
. . . . . . . . . . . . . . . . 17
⊢ (ran
(pmTrsp‘𝐷) ⊆
(Base‘𝑆) → Word
ran (pmTrsp‘𝐷)
⊆ Word (Base‘𝑆)) |
71 | 58, 70 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢
((((((((𝑢 ∈
Word ran (pmTrsp‘𝐷)
∧ 𝑖 ∈ ran
(pmTrsp‘𝐷)) ∧
𝑗 ∈ ran
(pmTrsp‘𝐷)) ∧
𝐷 ∈ Fin) ∧ 𝑣 ∈ Word 𝐶) ∧ (𝑆 Σg 𝑢) = (𝑆 Σg 𝑣)) ∧ 𝑐 ∈ Word 𝐶) ∧ (𝑖(+g‘𝑆)𝑗) = (𝑆 Σg 𝑐)) → Word ran
(pmTrsp‘𝐷) ⊆
Word (Base‘𝑆)) |
72 | | simp-7l 789 |
. . . . . . . . . . . . . . . 16
⊢
((((((((𝑢 ∈
Word ran (pmTrsp‘𝐷)
∧ 𝑖 ∈ ran
(pmTrsp‘𝐷)) ∧
𝑗 ∈ ran
(pmTrsp‘𝐷)) ∧
𝐷 ∈ Fin) ∧ 𝑣 ∈ Word 𝐶) ∧ (𝑆 Σg 𝑢) = (𝑆 Σg 𝑣)) ∧ 𝑐 ∈ Word 𝐶) ∧ (𝑖(+g‘𝑆)𝑗) = (𝑆 Σg 𝑐)) → 𝑢 ∈ Word ran (pmTrsp‘𝐷)) |
73 | 71, 72 | sseldd 3878 |
. . . . . . . . . . . . . . 15
⊢
((((((((𝑢 ∈
Word ran (pmTrsp‘𝐷)
∧ 𝑖 ∈ ran
(pmTrsp‘𝐷)) ∧
𝑗 ∈ ran
(pmTrsp‘𝐷)) ∧
𝐷 ∈ Fin) ∧ 𝑣 ∈ Word 𝐶) ∧ (𝑆 Σg 𝑢) = (𝑆 Σg 𝑣)) ∧ 𝑐 ∈ Word 𝐶) ∧ (𝑖(+g‘𝑆)𝑗) = (𝑆 Σg 𝑐)) → 𝑢 ∈ Word (Base‘𝑆)) |
74 | 61, 63 | s2cld 14322 |
. . . . . . . . . . . . . . 15
⊢
((((((((𝑢 ∈
Word ran (pmTrsp‘𝐷)
∧ 𝑖 ∈ ran
(pmTrsp‘𝐷)) ∧
𝑗 ∈ ran
(pmTrsp‘𝐷)) ∧
𝐷 ∈ Fin) ∧ 𝑣 ∈ Word 𝐶) ∧ (𝑆 Σg 𝑢) = (𝑆 Σg 𝑣)) ∧ 𝑐 ∈ Word 𝐶) ∧ (𝑖(+g‘𝑆)𝑗) = (𝑆 Σg 𝑐)) → 〈“𝑖𝑗”〉 ∈ Word (Base‘𝑆)) |
75 | 12, 64 | gsumccat 18122 |
. . . . . . . . . . . . . . 15
⊢ ((𝑆 ∈ Mnd ∧ 𝑢 ∈ Word (Base‘𝑆) ∧ 〈“𝑖𝑗”〉 ∈ Word (Base‘𝑆)) → (𝑆 Σg (𝑢 ++ 〈“𝑖𝑗”〉)) = ((𝑆 Σg 𝑢)(+g‘𝑆)(𝑆 Σg
〈“𝑖𝑗”〉))) |
76 | 56, 73, 74, 75 | syl3anc 1372 |
. . . . . . . . . . . . . 14
⊢
((((((((𝑢 ∈
Word ran (pmTrsp‘𝐷)
∧ 𝑖 ∈ ran
(pmTrsp‘𝐷)) ∧
𝑗 ∈ ran
(pmTrsp‘𝐷)) ∧
𝐷 ∈ Fin) ∧ 𝑣 ∈ Word 𝐶) ∧ (𝑆 Σg 𝑢) = (𝑆 Σg 𝑣)) ∧ 𝑐 ∈ Word 𝐶) ∧ (𝑖(+g‘𝑆)𝑗) = (𝑆 Σg 𝑐)) → (𝑆 Σg (𝑢 ++ 〈“𝑖𝑗”〉)) = ((𝑆 Σg 𝑢)(+g‘𝑆)(𝑆 Σg
〈“𝑖𝑗”〉))) |
77 | | cyc3genpm.t |
. . . . . . . . . . . . . . . . . . . 20
⊢ 𝐶 = (𝑀 “ (◡♯ “ {3})) |
78 | | cyc3genpm.m |
. . . . . . . . . . . . . . . . . . . . 21
⊢ 𝑀 = (toCyc‘𝐷) |
79 | 78 | imaeq1i 5900 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑀 “ (◡♯ “ {3})) = ((toCyc‘𝐷) “ (◡♯ “ {3})) |
80 | 77, 79 | eqtri 2761 |
. . . . . . . . . . . . . . . . . . 19
⊢ 𝐶 = ((toCyc‘𝐷) “ (◡♯ “ {3})) |
81 | 80, 9 | cyc3evpm 30994 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝐷 ∈ Fin → 𝐶 ⊆ 𝐴) |
82 | 11, 12 | evpmss 20402 |
. . . . . . . . . . . . . . . . . . 19
⊢
(pmEven‘𝐷)
⊆ (Base‘𝑆) |
83 | 9, 82 | eqsstri 3911 |
. . . . . . . . . . . . . . . . . 18
⊢ 𝐴 ⊆ (Base‘𝑆) |
84 | 81, 83 | sstrdi 3889 |
. . . . . . . . . . . . . . . . 17
⊢ (𝐷 ∈ Fin → 𝐶 ⊆ (Base‘𝑆)) |
85 | | sswrd 13963 |
. . . . . . . . . . . . . . . . 17
⊢ (𝐶 ⊆ (Base‘𝑆) → Word 𝐶 ⊆ Word (Base‘𝑆)) |
86 | 53, 84, 85 | 3syl 18 |
. . . . . . . . . . . . . . . 16
⊢
((((((((𝑢 ∈
Word ran (pmTrsp‘𝐷)
∧ 𝑖 ∈ ran
(pmTrsp‘𝐷)) ∧
𝑗 ∈ ran
(pmTrsp‘𝐷)) ∧
𝐷 ∈ Fin) ∧ 𝑣 ∈ Word 𝐶) ∧ (𝑆 Σg 𝑢) = (𝑆 Σg 𝑣)) ∧ 𝑐 ∈ Word 𝐶) ∧ (𝑖(+g‘𝑆)𝑗) = (𝑆 Σg 𝑐)) → Word 𝐶 ⊆ Word (Base‘𝑆)) |
87 | | simp-4r 784 |
. . . . . . . . . . . . . . . 16
⊢
((((((((𝑢 ∈
Word ran (pmTrsp‘𝐷)
∧ 𝑖 ∈ ran
(pmTrsp‘𝐷)) ∧
𝑗 ∈ ran
(pmTrsp‘𝐷)) ∧
𝐷 ∈ Fin) ∧ 𝑣 ∈ Word 𝐶) ∧ (𝑆 Σg 𝑢) = (𝑆 Σg 𝑣)) ∧ 𝑐 ∈ Word 𝐶) ∧ (𝑖(+g‘𝑆)𝑗) = (𝑆 Σg 𝑐)) → 𝑣 ∈ Word 𝐶) |
88 | 86, 87 | sseldd 3878 |
. . . . . . . . . . . . . . 15
⊢
((((((((𝑢 ∈
Word ran (pmTrsp‘𝐷)
∧ 𝑖 ∈ ran
(pmTrsp‘𝐷)) ∧
𝑗 ∈ ran
(pmTrsp‘𝐷)) ∧
𝐷 ∈ Fin) ∧ 𝑣 ∈ Word 𝐶) ∧ (𝑆 Σg 𝑢) = (𝑆 Σg 𝑣)) ∧ 𝑐 ∈ Word 𝐶) ∧ (𝑖(+g‘𝑆)𝑗) = (𝑆 Σg 𝑐)) → 𝑣 ∈ Word (Base‘𝑆)) |
89 | | simplr 769 |
. . . . . . . . . . . . . . . 16
⊢
((((((((𝑢 ∈
Word ran (pmTrsp‘𝐷)
∧ 𝑖 ∈ ran
(pmTrsp‘𝐷)) ∧
𝑗 ∈ ran
(pmTrsp‘𝐷)) ∧
𝐷 ∈ Fin) ∧ 𝑣 ∈ Word 𝐶) ∧ (𝑆 Σg 𝑢) = (𝑆 Σg 𝑣)) ∧ 𝑐 ∈ Word 𝐶) ∧ (𝑖(+g‘𝑆)𝑗) = (𝑆 Σg 𝑐)) → 𝑐 ∈ Word 𝐶) |
90 | 86, 89 | sseldd 3878 |
. . . . . . . . . . . . . . 15
⊢
((((((((𝑢 ∈
Word ran (pmTrsp‘𝐷)
∧ 𝑖 ∈ ran
(pmTrsp‘𝐷)) ∧
𝑗 ∈ ran
(pmTrsp‘𝐷)) ∧
𝐷 ∈ Fin) ∧ 𝑣 ∈ Word 𝐶) ∧ (𝑆 Σg 𝑢) = (𝑆 Σg 𝑣)) ∧ 𝑐 ∈ Word 𝐶) ∧ (𝑖(+g‘𝑆)𝑗) = (𝑆 Σg 𝑐)) → 𝑐 ∈ Word (Base‘𝑆)) |
91 | 12, 64 | gsumccat 18122 |
. . . . . . . . . . . . . . 15
⊢ ((𝑆 ∈ Mnd ∧ 𝑣 ∈ Word (Base‘𝑆) ∧ 𝑐 ∈ Word (Base‘𝑆)) → (𝑆 Σg (𝑣 ++ 𝑐)) = ((𝑆 Σg 𝑣)(+g‘𝑆)(𝑆 Σg 𝑐))) |
92 | 56, 88, 90, 91 | syl3anc 1372 |
. . . . . . . . . . . . . 14
⊢
((((((((𝑢 ∈
Word ran (pmTrsp‘𝐷)
∧ 𝑖 ∈ ran
(pmTrsp‘𝐷)) ∧
𝑗 ∈ ran
(pmTrsp‘𝐷)) ∧
𝐷 ∈ Fin) ∧ 𝑣 ∈ Word 𝐶) ∧ (𝑆 Σg 𝑢) = (𝑆 Σg 𝑣)) ∧ 𝑐 ∈ Word 𝐶) ∧ (𝑖(+g‘𝑆)𝑗) = (𝑆 Σg 𝑐)) → (𝑆 Σg (𝑣 ++ 𝑐)) = ((𝑆 Σg 𝑣)(+g‘𝑆)(𝑆 Σg 𝑐))) |
93 | 69, 76, 92 | 3eqtr4d 2783 |
. . . . . . . . . . . . 13
⊢
((((((((𝑢 ∈
Word ran (pmTrsp‘𝐷)
∧ 𝑖 ∈ ran
(pmTrsp‘𝐷)) ∧
𝑗 ∈ ran
(pmTrsp‘𝐷)) ∧
𝐷 ∈ Fin) ∧ 𝑣 ∈ Word 𝐶) ∧ (𝑆 Σg 𝑢) = (𝑆 Σg 𝑣)) ∧ 𝑐 ∈ Word 𝐶) ∧ (𝑖(+g‘𝑆)𝑗) = (𝑆 Σg 𝑐)) → (𝑆 Σg (𝑢 ++ 〈“𝑖𝑗”〉)) = (𝑆 Σg (𝑣 ++ 𝑐))) |
94 | 47, 50, 93 | rspcedvd 3529 |
. . . . . . . . . . . 12
⊢
((((((((𝑢 ∈
Word ran (pmTrsp‘𝐷)
∧ 𝑖 ∈ ran
(pmTrsp‘𝐷)) ∧
𝑗 ∈ ran
(pmTrsp‘𝐷)) ∧
𝐷 ∈ Fin) ∧ 𝑣 ∈ Word 𝐶) ∧ (𝑆 Σg 𝑢) = (𝑆 Σg 𝑣)) ∧ 𝑐 ∈ Word 𝐶) ∧ (𝑖(+g‘𝑆)𝑗) = (𝑆 Σg 𝑐)) → ∃𝑤 ∈ Word 𝐶(𝑆 Σg (𝑢 ++ 〈“𝑖𝑗”〉)) = (𝑆 Σg 𝑤)) |
95 | | cyc3genpm.n |
. . . . . . . . . . . . . . 15
⊢ 𝑁 = (♯‘𝐷) |
96 | | simp-6r 788 |
. . . . . . . . . . . . . . 15
⊢
((((((((((((𝑢 ∈
Word ran (pmTrsp‘𝐷)
∧ 𝑖 ∈ ran
(pmTrsp‘𝐷)) ∧
𝑗 ∈ ran
(pmTrsp‘𝐷)) ∧
𝐷 ∈ Fin) ∧ 𝑣 ∈ Word 𝐶) ∧ (𝑆 Σg 𝑢) = (𝑆 Σg 𝑣)) ∧ 𝑒 ∈ 𝐷) ∧ 𝑓 ∈ 𝐷) ∧ (𝑒 ≠ 𝑓 ∧ 𝑖 = (𝑀‘〈“𝑒𝑓”〉))) ∧ 𝑔 ∈ 𝐷) ∧ ℎ ∈ 𝐷) ∧ (𝑔 ≠ ℎ ∧ 𝑗 = (𝑀‘〈“𝑔ℎ”〉))) → 𝑒 ∈ 𝐷) |
97 | | simp-5r 786 |
. . . . . . . . . . . . . . 15
⊢
((((((((((((𝑢 ∈
Word ran (pmTrsp‘𝐷)
∧ 𝑖 ∈ ran
(pmTrsp‘𝐷)) ∧
𝑗 ∈ ran
(pmTrsp‘𝐷)) ∧
𝐷 ∈ Fin) ∧ 𝑣 ∈ Word 𝐶) ∧ (𝑆 Σg 𝑢) = (𝑆 Σg 𝑣)) ∧ 𝑒 ∈ 𝐷) ∧ 𝑓 ∈ 𝐷) ∧ (𝑒 ≠ 𝑓 ∧ 𝑖 = (𝑀‘〈“𝑒𝑓”〉))) ∧ 𝑔 ∈ 𝐷) ∧ ℎ ∈ 𝐷) ∧ (𝑔 ≠ ℎ ∧ 𝑗 = (𝑀‘〈“𝑔ℎ”〉))) → 𝑓 ∈ 𝐷) |
98 | | simpllr 776 |
. . . . . . . . . . . . . . 15
⊢
((((((((((((𝑢 ∈
Word ran (pmTrsp‘𝐷)
∧ 𝑖 ∈ ran
(pmTrsp‘𝐷)) ∧
𝑗 ∈ ran
(pmTrsp‘𝐷)) ∧
𝐷 ∈ Fin) ∧ 𝑣 ∈ Word 𝐶) ∧ (𝑆 Σg 𝑢) = (𝑆 Σg 𝑣)) ∧ 𝑒 ∈ 𝐷) ∧ 𝑓 ∈ 𝐷) ∧ (𝑒 ≠ 𝑓 ∧ 𝑖 = (𝑀‘〈“𝑒𝑓”〉))) ∧ 𝑔 ∈ 𝐷) ∧ ℎ ∈ 𝐷) ∧ (𝑔 ≠ ℎ ∧ 𝑗 = (𝑀‘〈“𝑔ℎ”〉))) → 𝑔 ∈ 𝐷) |
99 | | simplr 769 |
. . . . . . . . . . . . . . 15
⊢
((((((((((((𝑢 ∈
Word ran (pmTrsp‘𝐷)
∧ 𝑖 ∈ ran
(pmTrsp‘𝐷)) ∧
𝑗 ∈ ran
(pmTrsp‘𝐷)) ∧
𝐷 ∈ Fin) ∧ 𝑣 ∈ Word 𝐶) ∧ (𝑆 Σg 𝑢) = (𝑆 Σg 𝑣)) ∧ 𝑒 ∈ 𝐷) ∧ 𝑓 ∈ 𝐷) ∧ (𝑒 ≠ 𝑓 ∧ 𝑖 = (𝑀‘〈“𝑒𝑓”〉))) ∧ 𝑔 ∈ 𝐷) ∧ ℎ ∈ 𝐷) ∧ (𝑔 ≠ ℎ ∧ 𝑗 = (𝑀‘〈“𝑔ℎ”〉))) → ℎ ∈ 𝐷) |
100 | | simp-4r 784 |
. . . . . . . . . . . . . . . 16
⊢
((((((((((((𝑢 ∈
Word ran (pmTrsp‘𝐷)
∧ 𝑖 ∈ ran
(pmTrsp‘𝐷)) ∧
𝑗 ∈ ran
(pmTrsp‘𝐷)) ∧
𝐷 ∈ Fin) ∧ 𝑣 ∈ Word 𝐶) ∧ (𝑆 Σg 𝑢) = (𝑆 Σg 𝑣)) ∧ 𝑒 ∈ 𝐷) ∧ 𝑓 ∈ 𝐷) ∧ (𝑒 ≠ 𝑓 ∧ 𝑖 = (𝑀‘〈“𝑒𝑓”〉))) ∧ 𝑔 ∈ 𝐷) ∧ ℎ ∈ 𝐷) ∧ (𝑔 ≠ ℎ ∧ 𝑗 = (𝑀‘〈“𝑔ℎ”〉))) → (𝑒 ≠ 𝑓 ∧ 𝑖 = (𝑀‘〈“𝑒𝑓”〉))) |
101 | 100 | simprd 499 |
. . . . . . . . . . . . . . 15
⊢
((((((((((((𝑢 ∈
Word ran (pmTrsp‘𝐷)
∧ 𝑖 ∈ ran
(pmTrsp‘𝐷)) ∧
𝑗 ∈ ran
(pmTrsp‘𝐷)) ∧
𝐷 ∈ Fin) ∧ 𝑣 ∈ Word 𝐶) ∧ (𝑆 Σg 𝑢) = (𝑆 Σg 𝑣)) ∧ 𝑒 ∈ 𝐷) ∧ 𝑓 ∈ 𝐷) ∧ (𝑒 ≠ 𝑓 ∧ 𝑖 = (𝑀‘〈“𝑒𝑓”〉))) ∧ 𝑔 ∈ 𝐷) ∧ ℎ ∈ 𝐷) ∧ (𝑔 ≠ ℎ ∧ 𝑗 = (𝑀‘〈“𝑔ℎ”〉))) → 𝑖 = (𝑀‘〈“𝑒𝑓”〉)) |
102 | | simprr 773 |
. . . . . . . . . . . . . . 15
⊢
((((((((((((𝑢 ∈
Word ran (pmTrsp‘𝐷)
∧ 𝑖 ∈ ran
(pmTrsp‘𝐷)) ∧
𝑗 ∈ ran
(pmTrsp‘𝐷)) ∧
𝐷 ∈ Fin) ∧ 𝑣 ∈ Word 𝐶) ∧ (𝑆 Σg 𝑢) = (𝑆 Σg 𝑣)) ∧ 𝑒 ∈ 𝐷) ∧ 𝑓 ∈ 𝐷) ∧ (𝑒 ≠ 𝑓 ∧ 𝑖 = (𝑀‘〈“𝑒𝑓”〉))) ∧ 𝑔 ∈ 𝐷) ∧ ℎ ∈ 𝐷) ∧ (𝑔 ≠ ℎ ∧ 𝑗 = (𝑀‘〈“𝑔ℎ”〉))) → 𝑗 = (𝑀‘〈“𝑔ℎ”〉)) |
103 | 52 | ad6antr 736 |
. . . . . . . . . . . . . . 15
⊢
((((((((((((𝑢 ∈
Word ran (pmTrsp‘𝐷)
∧ 𝑖 ∈ ran
(pmTrsp‘𝐷)) ∧
𝑗 ∈ ran
(pmTrsp‘𝐷)) ∧
𝐷 ∈ Fin) ∧ 𝑣 ∈ Word 𝐶) ∧ (𝑆 Σg 𝑢) = (𝑆 Σg 𝑣)) ∧ 𝑒 ∈ 𝐷) ∧ 𝑓 ∈ 𝐷) ∧ (𝑒 ≠ 𝑓 ∧ 𝑖 = (𝑀‘〈“𝑒𝑓”〉))) ∧ 𝑔 ∈ 𝐷) ∧ ℎ ∈ 𝐷) ∧ (𝑔 ≠ ℎ ∧ 𝑗 = (𝑀‘〈“𝑔ℎ”〉))) → 𝐷 ∈ Fin) |
104 | 100 | simpld 498 |
. . . . . . . . . . . . . . 15
⊢
((((((((((((𝑢 ∈
Word ran (pmTrsp‘𝐷)
∧ 𝑖 ∈ ran
(pmTrsp‘𝐷)) ∧
𝑗 ∈ ran
(pmTrsp‘𝐷)) ∧
𝐷 ∈ Fin) ∧ 𝑣 ∈ Word 𝐶) ∧ (𝑆 Σg 𝑢) = (𝑆 Σg 𝑣)) ∧ 𝑒 ∈ 𝐷) ∧ 𝑓 ∈ 𝐷) ∧ (𝑒 ≠ 𝑓 ∧ 𝑖 = (𝑀‘〈“𝑒𝑓”〉))) ∧ 𝑔 ∈ 𝐷) ∧ ℎ ∈ 𝐷) ∧ (𝑔 ≠ ℎ ∧ 𝑗 = (𝑀‘〈“𝑔ℎ”〉))) → 𝑒 ≠ 𝑓) |
105 | | simprl 771 |
. . . . . . . . . . . . . . 15
⊢
((((((((((((𝑢 ∈
Word ran (pmTrsp‘𝐷)
∧ 𝑖 ∈ ran
(pmTrsp‘𝐷)) ∧
𝑗 ∈ ran
(pmTrsp‘𝐷)) ∧
𝐷 ∈ Fin) ∧ 𝑣 ∈ Word 𝐶) ∧ (𝑆 Σg 𝑢) = (𝑆 Σg 𝑣)) ∧ 𝑒 ∈ 𝐷) ∧ 𝑓 ∈ 𝐷) ∧ (𝑒 ≠ 𝑓 ∧ 𝑖 = (𝑀‘〈“𝑒𝑓”〉))) ∧ 𝑔 ∈ 𝐷) ∧ ℎ ∈ 𝐷) ∧ (𝑔 ≠ ℎ ∧ 𝑗 = (𝑀‘〈“𝑔ℎ”〉))) → 𝑔 ≠ ℎ) |
106 | 77, 9, 11, 95, 78, 64, 96, 97, 98, 99, 101, 102, 103, 104, 105 | cyc3genpmlem 30995 |
. . . . . . . . . . . . . 14
⊢
((((((((((((𝑢 ∈
Word ran (pmTrsp‘𝐷)
∧ 𝑖 ∈ ran
(pmTrsp‘𝐷)) ∧
𝑗 ∈ ran
(pmTrsp‘𝐷)) ∧
𝐷 ∈ Fin) ∧ 𝑣 ∈ Word 𝐶) ∧ (𝑆 Σg 𝑢) = (𝑆 Σg 𝑣)) ∧ 𝑒 ∈ 𝐷) ∧ 𝑓 ∈ 𝐷) ∧ (𝑒 ≠ 𝑓 ∧ 𝑖 = (𝑀‘〈“𝑒𝑓”〉))) ∧ 𝑔 ∈ 𝐷) ∧ ℎ ∈ 𝐷) ∧ (𝑔 ≠ ℎ ∧ 𝑗 = (𝑀‘〈“𝑔ℎ”〉))) → ∃𝑐 ∈ Word 𝐶(𝑖(+g‘𝑆)𝑗) = (𝑆 Σg 𝑐)) |
107 | | simp-6r 788 |
. . . . . . . . . . . . . . 15
⊢
(((((((((𝑢 ∈
Word ran (pmTrsp‘𝐷)
∧ 𝑖 ∈ ran
(pmTrsp‘𝐷)) ∧
𝑗 ∈ ran
(pmTrsp‘𝐷)) ∧
𝐷 ∈ Fin) ∧ 𝑣 ∈ Word 𝐶) ∧ (𝑆 Σg 𝑢) = (𝑆 Σg 𝑣)) ∧ 𝑒 ∈ 𝐷) ∧ 𝑓 ∈ 𝐷) ∧ (𝑒 ≠ 𝑓 ∧ 𝑖 = (𝑀‘〈“𝑒𝑓”〉))) → 𝐷 ∈ Fin) |
108 | | simp-7r 790 |
. . . . . . . . . . . . . . 15
⊢
(((((((((𝑢 ∈
Word ran (pmTrsp‘𝐷)
∧ 𝑖 ∈ ran
(pmTrsp‘𝐷)) ∧
𝑗 ∈ ran
(pmTrsp‘𝐷)) ∧
𝐷 ∈ Fin) ∧ 𝑣 ∈ Word 𝐶) ∧ (𝑆 Σg 𝑢) = (𝑆 Σg 𝑣)) ∧ 𝑒 ∈ 𝐷) ∧ 𝑓 ∈ 𝐷) ∧ (𝑒 ≠ 𝑓 ∧ 𝑖 = (𝑀‘〈“𝑒𝑓”〉))) → 𝑗 ∈ ran (pmTrsp‘𝐷)) |
109 | 16, 78 | trsp2cyc 30967 |
. . . . . . . . . . . . . . 15
⊢ ((𝐷 ∈ Fin ∧ 𝑗 ∈ ran (pmTrsp‘𝐷)) → ∃𝑔 ∈ 𝐷 ∃ℎ ∈ 𝐷 (𝑔 ≠ ℎ ∧ 𝑗 = (𝑀‘〈“𝑔ℎ”〉))) |
110 | 107, 108,
109 | syl2anc 587 |
. . . . . . . . . . . . . 14
⊢
(((((((((𝑢 ∈
Word ran (pmTrsp‘𝐷)
∧ 𝑖 ∈ ran
(pmTrsp‘𝐷)) ∧
𝑗 ∈ ran
(pmTrsp‘𝐷)) ∧
𝐷 ∈ Fin) ∧ 𝑣 ∈ Word 𝐶) ∧ (𝑆 Σg 𝑢) = (𝑆 Σg 𝑣)) ∧ 𝑒 ∈ 𝐷) ∧ 𝑓 ∈ 𝐷) ∧ (𝑒 ≠ 𝑓 ∧ 𝑖 = (𝑀‘〈“𝑒𝑓”〉))) → ∃𝑔 ∈ 𝐷 ∃ℎ ∈ 𝐷 (𝑔 ≠ ℎ ∧ 𝑗 = (𝑀‘〈“𝑔ℎ”〉))) |
111 | 106, 110 | r19.29vva 3243 |
. . . . . . . . . . . . 13
⊢
(((((((((𝑢 ∈
Word ran (pmTrsp‘𝐷)
∧ 𝑖 ∈ ran
(pmTrsp‘𝐷)) ∧
𝑗 ∈ ran
(pmTrsp‘𝐷)) ∧
𝐷 ∈ Fin) ∧ 𝑣 ∈ Word 𝐶) ∧ (𝑆 Σg 𝑢) = (𝑆 Σg 𝑣)) ∧ 𝑒 ∈ 𝐷) ∧ 𝑓 ∈ 𝐷) ∧ (𝑒 ≠ 𝑓 ∧ 𝑖 = (𝑀‘〈“𝑒𝑓”〉))) → ∃𝑐 ∈ Word 𝐶(𝑖(+g‘𝑆)𝑗) = (𝑆 Σg 𝑐)) |
112 | 16, 78 | trsp2cyc 30967 |
. . . . . . . . . . . . . 14
⊢ ((𝐷 ∈ Fin ∧ 𝑖 ∈ ran (pmTrsp‘𝐷)) → ∃𝑒 ∈ 𝐷 ∃𝑓 ∈ 𝐷 (𝑒 ≠ 𝑓 ∧ 𝑖 = (𝑀‘〈“𝑒𝑓”〉))) |
113 | 52, 59, 112 | syl2anc 587 |
. . . . . . . . . . . . 13
⊢
((((((𝑢 ∈ Word
ran (pmTrsp‘𝐷) ∧
𝑖 ∈ ran
(pmTrsp‘𝐷)) ∧
𝑗 ∈ ran
(pmTrsp‘𝐷)) ∧
𝐷 ∈ Fin) ∧ 𝑣 ∈ Word 𝐶) ∧ (𝑆 Σg 𝑢) = (𝑆 Σg 𝑣)) → ∃𝑒 ∈ 𝐷 ∃𝑓 ∈ 𝐷 (𝑒 ≠ 𝑓 ∧ 𝑖 = (𝑀‘〈“𝑒𝑓”〉))) |
114 | 111, 113 | r19.29vva 3243 |
. . . . . . . . . . . 12
⊢
((((((𝑢 ∈ Word
ran (pmTrsp‘𝐷) ∧
𝑖 ∈ ran
(pmTrsp‘𝐷)) ∧
𝑗 ∈ ran
(pmTrsp‘𝐷)) ∧
𝐷 ∈ Fin) ∧ 𝑣 ∈ Word 𝐶) ∧ (𝑆 Σg 𝑢) = (𝑆 Σg 𝑣)) → ∃𝑐 ∈ Word 𝐶(𝑖(+g‘𝑆)𝑗) = (𝑆 Σg 𝑐)) |
115 | 94, 114 | r19.29a 3199 |
. . . . . . . . . . 11
⊢
((((((𝑢 ∈ Word
ran (pmTrsp‘𝐷) ∧
𝑖 ∈ ran
(pmTrsp‘𝐷)) ∧
𝑗 ∈ ran
(pmTrsp‘𝐷)) ∧
𝐷 ∈ Fin) ∧ 𝑣 ∈ Word 𝐶) ∧ (𝑆 Σg 𝑢) = (𝑆 Σg 𝑣)) → ∃𝑤 ∈ Word 𝐶(𝑆 Σg (𝑢 ++ 〈“𝑖𝑗”〉)) = (𝑆 Σg 𝑤)) |
116 | 115 | adantl3r 750 |
. . . . . . . . . 10
⊢
(((((((𝑢 ∈ Word
ran (pmTrsp‘𝐷) ∧
𝑖 ∈ ran
(pmTrsp‘𝐷)) ∧
𝑗 ∈ ran
(pmTrsp‘𝐷)) ∧
(𝐷 ∈ Fin →
∃𝑤 ∈ Word 𝐶(𝑆 Σg 𝑢) = (𝑆 Σg 𝑤))) ∧ 𝐷 ∈ Fin) ∧ 𝑣 ∈ Word 𝐶) ∧ (𝑆 Σg 𝑢) = (𝑆 Σg 𝑣)) → ∃𝑤 ∈ Word 𝐶(𝑆 Σg (𝑢 ++ 〈“𝑖𝑗”〉)) = (𝑆 Σg 𝑤)) |
117 | | simpr 488 |
. . . . . . . . . . . 12
⊢
(((((𝑢 ∈ Word
ran (pmTrsp‘𝐷) ∧
𝑖 ∈ ran
(pmTrsp‘𝐷)) ∧
𝑗 ∈ ran
(pmTrsp‘𝐷)) ∧
(𝐷 ∈ Fin →
∃𝑤 ∈ Word 𝐶(𝑆 Σg 𝑢) = (𝑆 Σg 𝑤))) ∧ 𝐷 ∈ Fin) → 𝐷 ∈ Fin) |
118 | | simplr 769 |
. . . . . . . . . . . 12
⊢
(((((𝑢 ∈ Word
ran (pmTrsp‘𝐷) ∧
𝑖 ∈ ran
(pmTrsp‘𝐷)) ∧
𝑗 ∈ ran
(pmTrsp‘𝐷)) ∧
(𝐷 ∈ Fin →
∃𝑤 ∈ Word 𝐶(𝑆 Σg 𝑢) = (𝑆 Σg 𝑤))) ∧ 𝐷 ∈ Fin) → (𝐷 ∈ Fin → ∃𝑤 ∈ Word 𝐶(𝑆 Σg 𝑢) = (𝑆 Σg 𝑤))) |
119 | 117, 118 | mpd 15 |
. . . . . . . . . . 11
⊢
(((((𝑢 ∈ Word
ran (pmTrsp‘𝐷) ∧
𝑖 ∈ ran
(pmTrsp‘𝐷)) ∧
𝑗 ∈ ran
(pmTrsp‘𝐷)) ∧
(𝐷 ∈ Fin →
∃𝑤 ∈ Word 𝐶(𝑆 Σg 𝑢) = (𝑆 Σg 𝑤))) ∧ 𝐷 ∈ Fin) → ∃𝑤 ∈ Word 𝐶(𝑆 Σg 𝑢) = (𝑆 Σg 𝑤)) |
120 | | oveq2 7178 |
. . . . . . . . . . . . 13
⊢ (𝑣 = 𝑤 → (𝑆 Σg 𝑣) = (𝑆 Σg 𝑤)) |
121 | 120 | eqeq2d 2749 |
. . . . . . . . . . . 12
⊢ (𝑣 = 𝑤 → ((𝑆 Σg 𝑢) = (𝑆 Σg 𝑣) ↔ (𝑆 Σg 𝑢) = (𝑆 Σg 𝑤))) |
122 | 121 | cbvrexvw 3350 |
. . . . . . . . . . 11
⊢
(∃𝑣 ∈
Word 𝐶(𝑆 Σg 𝑢) = (𝑆 Σg 𝑣) ↔ ∃𝑤 ∈ Word 𝐶(𝑆 Σg 𝑢) = (𝑆 Σg 𝑤)) |
123 | 119, 122 | sylibr 237 |
. . . . . . . . . 10
⊢
(((((𝑢 ∈ Word
ran (pmTrsp‘𝐷) ∧
𝑖 ∈ ran
(pmTrsp‘𝐷)) ∧
𝑗 ∈ ran
(pmTrsp‘𝐷)) ∧
(𝐷 ∈ Fin →
∃𝑤 ∈ Word 𝐶(𝑆 Σg 𝑢) = (𝑆 Σg 𝑤))) ∧ 𝐷 ∈ Fin) → ∃𝑣 ∈ Word 𝐶(𝑆 Σg 𝑢) = (𝑆 Σg 𝑣)) |
124 | 116, 123 | r19.29a 3199 |
. . . . . . . . 9
⊢
(((((𝑢 ∈ Word
ran (pmTrsp‘𝐷) ∧
𝑖 ∈ ran
(pmTrsp‘𝐷)) ∧
𝑗 ∈ ran
(pmTrsp‘𝐷)) ∧
(𝐷 ∈ Fin →
∃𝑤 ∈ Word 𝐶(𝑆 Σg 𝑢) = (𝑆 Σg 𝑤))) ∧ 𝐷 ∈ Fin) → ∃𝑤 ∈ Word 𝐶(𝑆 Σg (𝑢 ++ 〈“𝑖𝑗”〉)) = (𝑆 Σg 𝑤)) |
125 | 124 | ex 416 |
. . . . . . . 8
⊢ ((((𝑢 ∈ Word ran
(pmTrsp‘𝐷) ∧
𝑖 ∈ ran
(pmTrsp‘𝐷)) ∧
𝑗 ∈ ran
(pmTrsp‘𝐷)) ∧
(𝐷 ∈ Fin →
∃𝑤 ∈ Word 𝐶(𝑆 Σg 𝑢) = (𝑆 Σg 𝑤))) → (𝐷 ∈ Fin → ∃𝑤 ∈ Word 𝐶(𝑆 Σg (𝑢 ++ 〈“𝑖𝑗”〉)) = (𝑆 Σg 𝑤))) |
126 | 125 | ex3 1347 |
. . . . . . 7
⊢ ((𝑢 ∈ Word ran
(pmTrsp‘𝐷) ∧
𝑖 ∈ ran
(pmTrsp‘𝐷) ∧
𝑗 ∈ ran
(pmTrsp‘𝐷)) →
((𝐷 ∈ Fin →
∃𝑤 ∈ Word 𝐶(𝑆 Σg 𝑢) = (𝑆 Σg 𝑤)) → (𝐷 ∈ Fin → ∃𝑤 ∈ Word 𝐶(𝑆 Σg (𝑢 ++ 〈“𝑖𝑗”〉)) = (𝑆 Σg 𝑤)))) |
127 | 26, 30, 34, 38, 45, 126 | wrdt2ind 30800 |
. . . . . 6
⊢ ((𝑣 ∈ Word ran
(pmTrsp‘𝐷) ∧ 2
∥ (♯‘𝑣))
→ (𝐷 ∈ Fin →
∃𝑤 ∈ Word 𝐶(𝑆 Σg 𝑣) = (𝑆 Σg 𝑤))) |
128 | 127 | imp 410 |
. . . . 5
⊢ (((𝑣 ∈ Word ran
(pmTrsp‘𝐷) ∧ 2
∥ (♯‘𝑣))
∧ 𝐷 ∈ Fin) →
∃𝑤 ∈ Word 𝐶(𝑆 Σg 𝑣) = (𝑆 Σg 𝑤)) |
129 | 1, 22, 7, 128 | syl21anc 837 |
. . . 4
⊢ ((((𝐷 ∈ Fin ∧ 𝑄 ∈ 𝐴) ∧ 𝑣 ∈ Word ran (pmTrsp‘𝐷)) ∧ 𝑄 = (𝑆 Σg 𝑣)) → ∃𝑤 ∈ Word 𝐶(𝑆 Σg 𝑣) = (𝑆 Σg 𝑤)) |
130 | 5 | eqeq1d 2740 |
. . . . 5
⊢ ((((𝐷 ∈ Fin ∧ 𝑄 ∈ 𝐴) ∧ 𝑣 ∈ Word ran (pmTrsp‘𝐷)) ∧ 𝑄 = (𝑆 Σg 𝑣)) → (𝑄 = (𝑆 Σg 𝑤) ↔ (𝑆 Σg 𝑣) = (𝑆 Σg 𝑤))) |
131 | 130 | rexbidv 3207 |
. . . 4
⊢ ((((𝐷 ∈ Fin ∧ 𝑄 ∈ 𝐴) ∧ 𝑣 ∈ Word ran (pmTrsp‘𝐷)) ∧ 𝑄 = (𝑆 Σg 𝑣)) → (∃𝑤 ∈ Word 𝐶𝑄 = (𝑆 Σg 𝑤) ↔ ∃𝑤 ∈ Word 𝐶(𝑆 Σg 𝑣) = (𝑆 Σg 𝑤))) |
132 | 129, 131 | mpbird 260 |
. . 3
⊢ ((((𝐷 ∈ Fin ∧ 𝑄 ∈ 𝐴) ∧ 𝑣 ∈ Word ran (pmTrsp‘𝐷)) ∧ 𝑄 = (𝑆 Σg 𝑣)) → ∃𝑤 ∈ Word 𝐶𝑄 = (𝑆 Σg 𝑤)) |
133 | 83 | sseli 3873 |
. . . 4
⊢ (𝑄 ∈ 𝐴 → 𝑄 ∈ (Base‘𝑆)) |
134 | 11, 12, 16 | psgnfitr 18763 |
. . . . 5
⊢ (𝐷 ∈ Fin → (𝑄 ∈ (Base‘𝑆) ↔ ∃𝑣 ∈ Word ran
(pmTrsp‘𝐷)𝑄 = (𝑆 Σg 𝑣))) |
135 | 134 | biimpa 480 |
. . . 4
⊢ ((𝐷 ∈ Fin ∧ 𝑄 ∈ (Base‘𝑆)) → ∃𝑣 ∈ Word ran
(pmTrsp‘𝐷)𝑄 = (𝑆 Σg 𝑣)) |
136 | 133, 135 | sylan2 596 |
. . 3
⊢ ((𝐷 ∈ Fin ∧ 𝑄 ∈ 𝐴) → ∃𝑣 ∈ Word ran (pmTrsp‘𝐷)𝑄 = (𝑆 Σg 𝑣)) |
137 | 132, 136 | r19.29a 3199 |
. 2
⊢ ((𝐷 ∈ Fin ∧ 𝑄 ∈ 𝐴) → ∃𝑤 ∈ Word 𝐶𝑄 = (𝑆 Σg 𝑤)) |
138 | | simpr 488 |
. . . 4
⊢ (((𝐷 ∈ Fin ∧ 𝑤 ∈ Word 𝐶) ∧ 𝑄 = (𝑆 Σg 𝑤)) → 𝑄 = (𝑆 Σg 𝑤)) |
139 | 11 | altgnsg 30993 |
. . . . . . . . 9
⊢ (𝐷 ∈ Fin →
(pmEven‘𝐷) ∈
(NrmSGrp‘𝑆)) |
140 | 9, 139 | eqeltrid 2837 |
. . . . . . . 8
⊢ (𝐷 ∈ Fin → 𝐴 ∈ (NrmSGrp‘𝑆)) |
141 | | nsgsubg 18428 |
. . . . . . . 8
⊢ (𝐴 ∈ (NrmSGrp‘𝑆) → 𝐴 ∈ (SubGrp‘𝑆)) |
142 | | subgsubm 18419 |
. . . . . . . 8
⊢ (𝐴 ∈ (SubGrp‘𝑆) → 𝐴 ∈ (SubMnd‘𝑆)) |
143 | 140, 141,
142 | 3syl 18 |
. . . . . . 7
⊢ (𝐷 ∈ Fin → 𝐴 ∈ (SubMnd‘𝑆)) |
144 | 143 | adantr 484 |
. . . . . 6
⊢ ((𝐷 ∈ Fin ∧ 𝑤 ∈ Word 𝐶) → 𝐴 ∈ (SubMnd‘𝑆)) |
145 | | sswrd 13963 |
. . . . . . . 8
⊢ (𝐶 ⊆ 𝐴 → Word 𝐶 ⊆ Word 𝐴) |
146 | 81, 145 | syl 17 |
. . . . . . 7
⊢ (𝐷 ∈ Fin → Word 𝐶 ⊆ Word 𝐴) |
147 | 146 | sselda 3877 |
. . . . . 6
⊢ ((𝐷 ∈ Fin ∧ 𝑤 ∈ Word 𝐶) → 𝑤 ∈ Word 𝐴) |
148 | | gsumwsubmcl 18117 |
. . . . . 6
⊢ ((𝐴 ∈ (SubMnd‘𝑆) ∧ 𝑤 ∈ Word 𝐴) → (𝑆 Σg 𝑤) ∈ 𝐴) |
149 | 144, 147,
148 | syl2anc 587 |
. . . . 5
⊢ ((𝐷 ∈ Fin ∧ 𝑤 ∈ Word 𝐶) → (𝑆 Σg 𝑤) ∈ 𝐴) |
150 | 149 | adantr 484 |
. . . 4
⊢ (((𝐷 ∈ Fin ∧ 𝑤 ∈ Word 𝐶) ∧ 𝑄 = (𝑆 Σg 𝑤)) → (𝑆 Σg 𝑤) ∈ 𝐴) |
151 | 138, 150 | eqeltrd 2833 |
. . 3
⊢ (((𝐷 ∈ Fin ∧ 𝑤 ∈ Word 𝐶) ∧ 𝑄 = (𝑆 Σg 𝑤)) → 𝑄 ∈ 𝐴) |
152 | 151 | r19.29an 3198 |
. 2
⊢ ((𝐷 ∈ Fin ∧ ∃𝑤 ∈ Word 𝐶𝑄 = (𝑆 Σg 𝑤)) → 𝑄 ∈ 𝐴) |
153 | 137, 152 | impbida 801 |
1
⊢ (𝐷 ∈ Fin → (𝑄 ∈ 𝐴 ↔ ∃𝑤 ∈ Word 𝐶𝑄 = (𝑆 Σg 𝑤))) |