Step | Hyp | Ref
| Expression |
1 | | gsumwspan.b |
. . . . . 6
⊢ 𝐵 = (Base‘𝑀) |
2 | 1 | submacs 17365 |
. . . . 5
⊢ (𝑀 ∈ Mnd →
(SubMnd‘𝑀) ∈
(ACS‘𝐵)) |
3 | 2 | acsmred 16317 |
. . . 4
⊢ (𝑀 ∈ Mnd →
(SubMnd‘𝑀) ∈
(Moore‘𝐵)) |
4 | 3 | adantr 481 |
. . 3
⊢ ((𝑀 ∈ Mnd ∧ 𝐺 ⊆ 𝐵) → (SubMnd‘𝑀) ∈ (Moore‘𝐵)) |
5 | | simpr 477 |
. . . . . . . 8
⊢ (((𝑀 ∈ Mnd ∧ 𝐺 ⊆ 𝐵) ∧ 𝑥 ∈ 𝐺) → 𝑥 ∈ 𝐺) |
6 | 5 | s1cld 13383 |
. . . . . . 7
⊢ (((𝑀 ∈ Mnd ∧ 𝐺 ⊆ 𝐵) ∧ 𝑥 ∈ 𝐺) → 〈“𝑥”〉 ∈ Word 𝐺) |
7 | | ssel2 3598 |
. . . . . . . . . 10
⊢ ((𝐺 ⊆ 𝐵 ∧ 𝑥 ∈ 𝐺) → 𝑥 ∈ 𝐵) |
8 | 7 | adantll 750 |
. . . . . . . . 9
⊢ (((𝑀 ∈ Mnd ∧ 𝐺 ⊆ 𝐵) ∧ 𝑥 ∈ 𝐺) → 𝑥 ∈ 𝐵) |
9 | 1 | gsumws1 17376 |
. . . . . . . . 9
⊢ (𝑥 ∈ 𝐵 → (𝑀 Σg
〈“𝑥”〉) = 𝑥) |
10 | 8, 9 | syl 17 |
. . . . . . . 8
⊢ (((𝑀 ∈ Mnd ∧ 𝐺 ⊆ 𝐵) ∧ 𝑥 ∈ 𝐺) → (𝑀 Σg
〈“𝑥”〉) = 𝑥) |
11 | 10 | eqcomd 2628 |
. . . . . . 7
⊢ (((𝑀 ∈ Mnd ∧ 𝐺 ⊆ 𝐵) ∧ 𝑥 ∈ 𝐺) → 𝑥 = (𝑀 Σg
〈“𝑥”〉)) |
12 | | oveq2 6658 |
. . . . . . . . 9
⊢ (𝑤 = 〈“𝑥”〉 → (𝑀 Σg
𝑤) = (𝑀 Σg
〈“𝑥”〉)) |
13 | 12 | eqeq2d 2632 |
. . . . . . . 8
⊢ (𝑤 = 〈“𝑥”〉 → (𝑥 = (𝑀 Σg 𝑤) ↔ 𝑥 = (𝑀 Σg
〈“𝑥”〉))) |
14 | 13 | rspcev 3309 |
. . . . . . 7
⊢
((〈“𝑥”〉 ∈ Word 𝐺 ∧ 𝑥 = (𝑀 Σg
〈“𝑥”〉)) → ∃𝑤 ∈ Word 𝐺𝑥 = (𝑀 Σg 𝑤)) |
15 | 6, 11, 14 | syl2anc 693 |
. . . . . 6
⊢ (((𝑀 ∈ Mnd ∧ 𝐺 ⊆ 𝐵) ∧ 𝑥 ∈ 𝐺) → ∃𝑤 ∈ Word 𝐺𝑥 = (𝑀 Σg 𝑤)) |
16 | | vex 3203 |
. . . . . . 7
⊢ 𝑥 ∈ V |
17 | | eqid 2622 |
. . . . . . . 8
⊢ (𝑤 ∈ Word 𝐺 ↦ (𝑀 Σg 𝑤)) = (𝑤 ∈ Word 𝐺 ↦ (𝑀 Σg 𝑤)) |
18 | 17 | elrnmpt 5372 |
. . . . . . 7
⊢ (𝑥 ∈ V → (𝑥 ∈ ran (𝑤 ∈ Word 𝐺 ↦ (𝑀 Σg 𝑤)) ↔ ∃𝑤 ∈ Word 𝐺𝑥 = (𝑀 Σg 𝑤))) |
19 | 16, 18 | ax-mp 5 |
. . . . . 6
⊢ (𝑥 ∈ ran (𝑤 ∈ Word 𝐺 ↦ (𝑀 Σg 𝑤)) ↔ ∃𝑤 ∈ Word 𝐺𝑥 = (𝑀 Σg 𝑤)) |
20 | 15, 19 | sylibr 224 |
. . . . 5
⊢ (((𝑀 ∈ Mnd ∧ 𝐺 ⊆ 𝐵) ∧ 𝑥 ∈ 𝐺) → 𝑥 ∈ ran (𝑤 ∈ Word 𝐺 ↦ (𝑀 Σg 𝑤))) |
21 | 20 | ex 450 |
. . . 4
⊢ ((𝑀 ∈ Mnd ∧ 𝐺 ⊆ 𝐵) → (𝑥 ∈ 𝐺 → 𝑥 ∈ ran (𝑤 ∈ Word 𝐺 ↦ (𝑀 Σg 𝑤)))) |
22 | 21 | ssrdv 3609 |
. . 3
⊢ ((𝑀 ∈ Mnd ∧ 𝐺 ⊆ 𝐵) → 𝐺 ⊆ ran (𝑤 ∈ Word 𝐺 ↦ (𝑀 Σg 𝑤))) |
23 | | gsumwspan.k |
. . . . . . . . . . 11
⊢ 𝐾 =
(mrCls‘(SubMnd‘𝑀)) |
24 | 23 | mrccl 16271 |
. . . . . . . . . 10
⊢
(((SubMnd‘𝑀)
∈ (Moore‘𝐵)
∧ 𝐺 ⊆ 𝐵) → (𝐾‘𝐺) ∈ (SubMnd‘𝑀)) |
25 | 3, 24 | sylan 488 |
. . . . . . . . 9
⊢ ((𝑀 ∈ Mnd ∧ 𝐺 ⊆ 𝐵) → (𝐾‘𝐺) ∈ (SubMnd‘𝑀)) |
26 | 25 | adantr 481 |
. . . . . . . 8
⊢ (((𝑀 ∈ Mnd ∧ 𝐺 ⊆ 𝐵) ∧ 𝑤 ∈ Word 𝐺) → (𝐾‘𝐺) ∈ (SubMnd‘𝑀)) |
27 | 23 | mrcssid 16277 |
. . . . . . . . . . 11
⊢
(((SubMnd‘𝑀)
∈ (Moore‘𝐵)
∧ 𝐺 ⊆ 𝐵) → 𝐺 ⊆ (𝐾‘𝐺)) |
28 | 3, 27 | sylan 488 |
. . . . . . . . . 10
⊢ ((𝑀 ∈ Mnd ∧ 𝐺 ⊆ 𝐵) → 𝐺 ⊆ (𝐾‘𝐺)) |
29 | | sswrd 13313 |
. . . . . . . . . 10
⊢ (𝐺 ⊆ (𝐾‘𝐺) → Word 𝐺 ⊆ Word (𝐾‘𝐺)) |
30 | 28, 29 | syl 17 |
. . . . . . . . 9
⊢ ((𝑀 ∈ Mnd ∧ 𝐺 ⊆ 𝐵) → Word 𝐺 ⊆ Word (𝐾‘𝐺)) |
31 | 30 | sselda 3603 |
. . . . . . . 8
⊢ (((𝑀 ∈ Mnd ∧ 𝐺 ⊆ 𝐵) ∧ 𝑤 ∈ Word 𝐺) → 𝑤 ∈ Word (𝐾‘𝐺)) |
32 | | gsumwsubmcl 17375 |
. . . . . . . 8
⊢ (((𝐾‘𝐺) ∈ (SubMnd‘𝑀) ∧ 𝑤 ∈ Word (𝐾‘𝐺)) → (𝑀 Σg 𝑤) ∈ (𝐾‘𝐺)) |
33 | 26, 31, 32 | syl2anc 693 |
. . . . . . 7
⊢ (((𝑀 ∈ Mnd ∧ 𝐺 ⊆ 𝐵) ∧ 𝑤 ∈ Word 𝐺) → (𝑀 Σg 𝑤) ∈ (𝐾‘𝐺)) |
34 | 33, 17 | fmptd 6385 |
. . . . . 6
⊢ ((𝑀 ∈ Mnd ∧ 𝐺 ⊆ 𝐵) → (𝑤 ∈ Word 𝐺 ↦ (𝑀 Σg 𝑤)):Word 𝐺⟶(𝐾‘𝐺)) |
35 | | frn 6053 |
. . . . . 6
⊢ ((𝑤 ∈ Word 𝐺 ↦ (𝑀 Σg 𝑤)):Word 𝐺⟶(𝐾‘𝐺) → ran (𝑤 ∈ Word 𝐺 ↦ (𝑀 Σg 𝑤)) ⊆ (𝐾‘𝐺)) |
36 | 34, 35 | syl 17 |
. . . . 5
⊢ ((𝑀 ∈ Mnd ∧ 𝐺 ⊆ 𝐵) → ran (𝑤 ∈ Word 𝐺 ↦ (𝑀 Σg 𝑤)) ⊆ (𝐾‘𝐺)) |
37 | 3, 23 | mrcssvd 16283 |
. . . . . 6
⊢ (𝑀 ∈ Mnd → (𝐾‘𝐺) ⊆ 𝐵) |
38 | 37 | adantr 481 |
. . . . 5
⊢ ((𝑀 ∈ Mnd ∧ 𝐺 ⊆ 𝐵) → (𝐾‘𝐺) ⊆ 𝐵) |
39 | 36, 38 | sstrd 3613 |
. . . 4
⊢ ((𝑀 ∈ Mnd ∧ 𝐺 ⊆ 𝐵) → ran (𝑤 ∈ Word 𝐺 ↦ (𝑀 Σg 𝑤)) ⊆ 𝐵) |
40 | | wrd0 13330 |
. . . . . 6
⊢ ∅
∈ Word 𝐺 |
41 | | eqid 2622 |
. . . . . . . . 9
⊢
(0g‘𝑀) = (0g‘𝑀) |
42 | 41 | gsum0 17278 |
. . . . . . . 8
⊢ (𝑀 Σg
∅) = (0g‘𝑀) |
43 | 42 | eqcomi 2631 |
. . . . . . 7
⊢
(0g‘𝑀) = (𝑀 Σg
∅) |
44 | 43 | a1i 11 |
. . . . . 6
⊢ ((𝑀 ∈ Mnd ∧ 𝐺 ⊆ 𝐵) → (0g‘𝑀) = (𝑀 Σg
∅)) |
45 | | oveq2 6658 |
. . . . . . . 8
⊢ (𝑤 = ∅ → (𝑀 Σg
𝑤) = (𝑀 Σg
∅)) |
46 | 45 | eqeq2d 2632 |
. . . . . . 7
⊢ (𝑤 = ∅ →
((0g‘𝑀) =
(𝑀
Σg 𝑤) ↔ (0g‘𝑀) = (𝑀 Σg
∅))) |
47 | 46 | rspcev 3309 |
. . . . . 6
⊢ ((∅
∈ Word 𝐺 ∧
(0g‘𝑀) =
(𝑀
Σg ∅)) → ∃𝑤 ∈ Word 𝐺(0g‘𝑀) = (𝑀 Σg 𝑤)) |
48 | 40, 44, 47 | sylancr 695 |
. . . . 5
⊢ ((𝑀 ∈ Mnd ∧ 𝐺 ⊆ 𝐵) → ∃𝑤 ∈ Word 𝐺(0g‘𝑀) = (𝑀 Σg 𝑤)) |
49 | | fvex 6201 |
. . . . . 6
⊢
(0g‘𝑀) ∈ V |
50 | 17 | elrnmpt 5372 |
. . . . . 6
⊢
((0g‘𝑀) ∈ V →
((0g‘𝑀)
∈ ran (𝑤 ∈ Word
𝐺 ↦ (𝑀 Σg
𝑤)) ↔ ∃𝑤 ∈ Word 𝐺(0g‘𝑀) = (𝑀 Σg 𝑤))) |
51 | 49, 50 | ax-mp 5 |
. . . . 5
⊢
((0g‘𝑀) ∈ ran (𝑤 ∈ Word 𝐺 ↦ (𝑀 Σg 𝑤)) ↔ ∃𝑤 ∈ Word 𝐺(0g‘𝑀) = (𝑀 Σg 𝑤)) |
52 | 48, 51 | sylibr 224 |
. . . 4
⊢ ((𝑀 ∈ Mnd ∧ 𝐺 ⊆ 𝐵) → (0g‘𝑀) ∈ ran (𝑤 ∈ Word 𝐺 ↦ (𝑀 Σg 𝑤))) |
53 | | ccatcl 13359 |
. . . . . . . . 9
⊢ ((𝑧 ∈ Word 𝐺 ∧ 𝑣 ∈ Word 𝐺) → (𝑧 ++ 𝑣) ∈ Word 𝐺) |
54 | 53 | adantl 482 |
. . . . . . . 8
⊢ (((𝑀 ∈ Mnd ∧ 𝐺 ⊆ 𝐵) ∧ (𝑧 ∈ Word 𝐺 ∧ 𝑣 ∈ Word 𝐺)) → (𝑧 ++ 𝑣) ∈ Word 𝐺) |
55 | | simpll 790 |
. . . . . . . . . 10
⊢ (((𝑀 ∈ Mnd ∧ 𝐺 ⊆ 𝐵) ∧ (𝑧 ∈ Word 𝐺 ∧ 𝑣 ∈ Word 𝐺)) → 𝑀 ∈ Mnd) |
56 | | sswrd 13313 |
. . . . . . . . . . . 12
⊢ (𝐺 ⊆ 𝐵 → Word 𝐺 ⊆ Word 𝐵) |
57 | 56 | ad2antlr 763 |
. . . . . . . . . . 11
⊢ (((𝑀 ∈ Mnd ∧ 𝐺 ⊆ 𝐵) ∧ (𝑧 ∈ Word 𝐺 ∧ 𝑣 ∈ Word 𝐺)) → Word 𝐺 ⊆ Word 𝐵) |
58 | | simprl 794 |
. . . . . . . . . . 11
⊢ (((𝑀 ∈ Mnd ∧ 𝐺 ⊆ 𝐵) ∧ (𝑧 ∈ Word 𝐺 ∧ 𝑣 ∈ Word 𝐺)) → 𝑧 ∈ Word 𝐺) |
59 | 57, 58 | sseldd 3604 |
. . . . . . . . . 10
⊢ (((𝑀 ∈ Mnd ∧ 𝐺 ⊆ 𝐵) ∧ (𝑧 ∈ Word 𝐺 ∧ 𝑣 ∈ Word 𝐺)) → 𝑧 ∈ Word 𝐵) |
60 | | simprr 796 |
. . . . . . . . . . 11
⊢ (((𝑀 ∈ Mnd ∧ 𝐺 ⊆ 𝐵) ∧ (𝑧 ∈ Word 𝐺 ∧ 𝑣 ∈ Word 𝐺)) → 𝑣 ∈ Word 𝐺) |
61 | 57, 60 | sseldd 3604 |
. . . . . . . . . 10
⊢ (((𝑀 ∈ Mnd ∧ 𝐺 ⊆ 𝐵) ∧ (𝑧 ∈ Word 𝐺 ∧ 𝑣 ∈ Word 𝐺)) → 𝑣 ∈ Word 𝐵) |
62 | | eqid 2622 |
. . . . . . . . . . 11
⊢
(+g‘𝑀) = (+g‘𝑀) |
63 | 1, 62 | gsumccat 17378 |
. . . . . . . . . 10
⊢ ((𝑀 ∈ Mnd ∧ 𝑧 ∈ Word 𝐵 ∧ 𝑣 ∈ Word 𝐵) → (𝑀 Σg (𝑧 ++ 𝑣)) = ((𝑀 Σg 𝑧)(+g‘𝑀)(𝑀 Σg 𝑣))) |
64 | 55, 59, 61, 63 | syl3anc 1326 |
. . . . . . . . 9
⊢ (((𝑀 ∈ Mnd ∧ 𝐺 ⊆ 𝐵) ∧ (𝑧 ∈ Word 𝐺 ∧ 𝑣 ∈ Word 𝐺)) → (𝑀 Σg (𝑧 ++ 𝑣)) = ((𝑀 Σg 𝑧)(+g‘𝑀)(𝑀 Σg 𝑣))) |
65 | 64 | eqcomd 2628 |
. . . . . . . 8
⊢ (((𝑀 ∈ Mnd ∧ 𝐺 ⊆ 𝐵) ∧ (𝑧 ∈ Word 𝐺 ∧ 𝑣 ∈ Word 𝐺)) → ((𝑀 Σg 𝑧)(+g‘𝑀)(𝑀 Σg 𝑣)) = (𝑀 Σg (𝑧 ++ 𝑣))) |
66 | | oveq2 6658 |
. . . . . . . . . 10
⊢ (𝑤 = (𝑧 ++ 𝑣) → (𝑀 Σg 𝑤) = (𝑀 Σg (𝑧 ++ 𝑣))) |
67 | 66 | eqeq2d 2632 |
. . . . . . . . 9
⊢ (𝑤 = (𝑧 ++ 𝑣) → (((𝑀 Σg 𝑧)(+g‘𝑀)(𝑀 Σg 𝑣)) = (𝑀 Σg 𝑤) ↔ ((𝑀 Σg 𝑧)(+g‘𝑀)(𝑀 Σg 𝑣)) = (𝑀 Σg (𝑧 ++ 𝑣)))) |
68 | 67 | rspcev 3309 |
. . . . . . . 8
⊢ (((𝑧 ++ 𝑣) ∈ Word 𝐺 ∧ ((𝑀 Σg 𝑧)(+g‘𝑀)(𝑀 Σg 𝑣)) = (𝑀 Σg (𝑧 ++ 𝑣))) → ∃𝑤 ∈ Word 𝐺((𝑀 Σg 𝑧)(+g‘𝑀)(𝑀 Σg 𝑣)) = (𝑀 Σg 𝑤)) |
69 | 54, 65, 68 | syl2anc 693 |
. . . . . . 7
⊢ (((𝑀 ∈ Mnd ∧ 𝐺 ⊆ 𝐵) ∧ (𝑧 ∈ Word 𝐺 ∧ 𝑣 ∈ Word 𝐺)) → ∃𝑤 ∈ Word 𝐺((𝑀 Σg 𝑧)(+g‘𝑀)(𝑀 Σg 𝑣)) = (𝑀 Σg 𝑤)) |
70 | | ovex 6678 |
. . . . . . . 8
⊢ ((𝑀 Σg
𝑧)(+g‘𝑀)(𝑀 Σg 𝑣)) ∈ V |
71 | 17 | elrnmpt 5372 |
. . . . . . . 8
⊢ (((𝑀 Σg
𝑧)(+g‘𝑀)(𝑀 Σg 𝑣)) ∈ V → (((𝑀 Σg
𝑧)(+g‘𝑀)(𝑀 Σg 𝑣)) ∈ ran (𝑤 ∈ Word 𝐺 ↦ (𝑀 Σg 𝑤)) ↔ ∃𝑤 ∈ Word 𝐺((𝑀 Σg 𝑧)(+g‘𝑀)(𝑀 Σg 𝑣)) = (𝑀 Σg 𝑤))) |
72 | 70, 71 | ax-mp 5 |
. . . . . . 7
⊢ (((𝑀 Σg
𝑧)(+g‘𝑀)(𝑀 Σg 𝑣)) ∈ ran (𝑤 ∈ Word 𝐺 ↦ (𝑀 Σg 𝑤)) ↔ ∃𝑤 ∈ Word 𝐺((𝑀 Σg 𝑧)(+g‘𝑀)(𝑀 Σg 𝑣)) = (𝑀 Σg 𝑤)) |
73 | 69, 72 | sylibr 224 |
. . . . . 6
⊢ (((𝑀 ∈ Mnd ∧ 𝐺 ⊆ 𝐵) ∧ (𝑧 ∈ Word 𝐺 ∧ 𝑣 ∈ Word 𝐺)) → ((𝑀 Σg 𝑧)(+g‘𝑀)(𝑀 Σg 𝑣)) ∈ ran (𝑤 ∈ Word 𝐺 ↦ (𝑀 Σg 𝑤))) |
74 | 73 | ralrimivva 2971 |
. . . . 5
⊢ ((𝑀 ∈ Mnd ∧ 𝐺 ⊆ 𝐵) → ∀𝑧 ∈ Word 𝐺∀𝑣 ∈ Word 𝐺((𝑀 Σg 𝑧)(+g‘𝑀)(𝑀 Σg 𝑣)) ∈ ran (𝑤 ∈ Word 𝐺 ↦ (𝑀 Σg 𝑤))) |
75 | | oveq2 6658 |
. . . . . . . . 9
⊢ (𝑤 = 𝑧 → (𝑀 Σg 𝑤) = (𝑀 Σg 𝑧)) |
76 | 75 | cbvmptv 4750 |
. . . . . . . 8
⊢ (𝑤 ∈ Word 𝐺 ↦ (𝑀 Σg 𝑤)) = (𝑧 ∈ Word 𝐺 ↦ (𝑀 Σg 𝑧)) |
77 | 76 | rneqi 5352 |
. . . . . . 7
⊢ ran
(𝑤 ∈ Word 𝐺 ↦ (𝑀 Σg 𝑤)) = ran (𝑧 ∈ Word 𝐺 ↦ (𝑀 Σg 𝑧)) |
78 | 77 | raleqi 3142 |
. . . . . 6
⊢
(∀𝑥 ∈
ran (𝑤 ∈ Word 𝐺 ↦ (𝑀 Σg 𝑤))∀𝑦 ∈ ran (𝑤 ∈ Word 𝐺 ↦ (𝑀 Σg 𝑤))(𝑥(+g‘𝑀)𝑦) ∈ ran (𝑤 ∈ Word 𝐺 ↦ (𝑀 Σg 𝑤)) ↔ ∀𝑥 ∈ ran (𝑧 ∈ Word 𝐺 ↦ (𝑀 Σg 𝑧))∀𝑦 ∈ ran (𝑤 ∈ Word 𝐺 ↦ (𝑀 Σg 𝑤))(𝑥(+g‘𝑀)𝑦) ∈ ran (𝑤 ∈ Word 𝐺 ↦ (𝑀 Σg 𝑤))) |
79 | | oveq2 6658 |
. . . . . . . . . . 11
⊢ (𝑤 = 𝑣 → (𝑀 Σg 𝑤) = (𝑀 Σg 𝑣)) |
80 | 79 | cbvmptv 4750 |
. . . . . . . . . 10
⊢ (𝑤 ∈ Word 𝐺 ↦ (𝑀 Σg 𝑤)) = (𝑣 ∈ Word 𝐺 ↦ (𝑀 Σg 𝑣)) |
81 | 80 | rneqi 5352 |
. . . . . . . . 9
⊢ ran
(𝑤 ∈ Word 𝐺 ↦ (𝑀 Σg 𝑤)) = ran (𝑣 ∈ Word 𝐺 ↦ (𝑀 Σg 𝑣)) |
82 | 81 | raleqi 3142 |
. . . . . . . 8
⊢
(∀𝑦 ∈
ran (𝑤 ∈ Word 𝐺 ↦ (𝑀 Σg 𝑤))(𝑥(+g‘𝑀)𝑦) ∈ ran (𝑤 ∈ Word 𝐺 ↦ (𝑀 Σg 𝑤)) ↔ ∀𝑦 ∈ ran (𝑣 ∈ Word 𝐺 ↦ (𝑀 Σg 𝑣))(𝑥(+g‘𝑀)𝑦) ∈ ran (𝑤 ∈ Word 𝐺 ↦ (𝑀 Σg 𝑤))) |
83 | | eqid 2622 |
. . . . . . . . . 10
⊢ (𝑣 ∈ Word 𝐺 ↦ (𝑀 Σg 𝑣)) = (𝑣 ∈ Word 𝐺 ↦ (𝑀 Σg 𝑣)) |
84 | | oveq2 6658 |
. . . . . . . . . . 11
⊢ (𝑦 = (𝑀 Σg 𝑣) → (𝑥(+g‘𝑀)𝑦) = (𝑥(+g‘𝑀)(𝑀 Σg 𝑣))) |
85 | 84 | eleq1d 2686 |
. . . . . . . . . 10
⊢ (𝑦 = (𝑀 Σg 𝑣) → ((𝑥(+g‘𝑀)𝑦) ∈ ran (𝑤 ∈ Word 𝐺 ↦ (𝑀 Σg 𝑤)) ↔ (𝑥(+g‘𝑀)(𝑀 Σg 𝑣)) ∈ ran (𝑤 ∈ Word 𝐺 ↦ (𝑀 Σg 𝑤)))) |
86 | 83, 85 | ralrnmpt 6368 |
. . . . . . . . 9
⊢
(∀𝑣 ∈
Word 𝐺(𝑀 Σg 𝑣) ∈ V → (∀𝑦 ∈ ran (𝑣 ∈ Word 𝐺 ↦ (𝑀 Σg 𝑣))(𝑥(+g‘𝑀)𝑦) ∈ ran (𝑤 ∈ Word 𝐺 ↦ (𝑀 Σg 𝑤)) ↔ ∀𝑣 ∈ Word 𝐺(𝑥(+g‘𝑀)(𝑀 Σg 𝑣)) ∈ ran (𝑤 ∈ Word 𝐺 ↦ (𝑀 Σg 𝑤)))) |
87 | | ovexd 6680 |
. . . . . . . . 9
⊢ (𝑣 ∈ Word 𝐺 → (𝑀 Σg 𝑣) ∈ V) |
88 | 86, 87 | mprg 2926 |
. . . . . . . 8
⊢
(∀𝑦 ∈
ran (𝑣 ∈ Word 𝐺 ↦ (𝑀 Σg 𝑣))(𝑥(+g‘𝑀)𝑦) ∈ ran (𝑤 ∈ Word 𝐺 ↦ (𝑀 Σg 𝑤)) ↔ ∀𝑣 ∈ Word 𝐺(𝑥(+g‘𝑀)(𝑀 Σg 𝑣)) ∈ ran (𝑤 ∈ Word 𝐺 ↦ (𝑀 Σg 𝑤))) |
89 | 82, 88 | bitri 264 |
. . . . . . 7
⊢
(∀𝑦 ∈
ran (𝑤 ∈ Word 𝐺 ↦ (𝑀 Σg 𝑤))(𝑥(+g‘𝑀)𝑦) ∈ ran (𝑤 ∈ Word 𝐺 ↦ (𝑀 Σg 𝑤)) ↔ ∀𝑣 ∈ Word 𝐺(𝑥(+g‘𝑀)(𝑀 Σg 𝑣)) ∈ ran (𝑤 ∈ Word 𝐺 ↦ (𝑀 Σg 𝑤))) |
90 | 89 | ralbii 2980 |
. . . . . 6
⊢
(∀𝑥 ∈
ran (𝑧 ∈ Word 𝐺 ↦ (𝑀 Σg 𝑧))∀𝑦 ∈ ran (𝑤 ∈ Word 𝐺 ↦ (𝑀 Σg 𝑤))(𝑥(+g‘𝑀)𝑦) ∈ ran (𝑤 ∈ Word 𝐺 ↦ (𝑀 Σg 𝑤)) ↔ ∀𝑥 ∈ ran (𝑧 ∈ Word 𝐺 ↦ (𝑀 Σg 𝑧))∀𝑣 ∈ Word 𝐺(𝑥(+g‘𝑀)(𝑀 Σg 𝑣)) ∈ ran (𝑤 ∈ Word 𝐺 ↦ (𝑀 Σg 𝑤))) |
91 | | eqid 2622 |
. . . . . . . 8
⊢ (𝑧 ∈ Word 𝐺 ↦ (𝑀 Σg 𝑧)) = (𝑧 ∈ Word 𝐺 ↦ (𝑀 Σg 𝑧)) |
92 | | oveq1 6657 |
. . . . . . . . . 10
⊢ (𝑥 = (𝑀 Σg 𝑧) → (𝑥(+g‘𝑀)(𝑀 Σg 𝑣)) = ((𝑀 Σg 𝑧)(+g‘𝑀)(𝑀 Σg 𝑣))) |
93 | 92 | eleq1d 2686 |
. . . . . . . . 9
⊢ (𝑥 = (𝑀 Σg 𝑧) → ((𝑥(+g‘𝑀)(𝑀 Σg 𝑣)) ∈ ran (𝑤 ∈ Word 𝐺 ↦ (𝑀 Σg 𝑤)) ↔ ((𝑀 Σg 𝑧)(+g‘𝑀)(𝑀 Σg 𝑣)) ∈ ran (𝑤 ∈ Word 𝐺 ↦ (𝑀 Σg 𝑤)))) |
94 | 93 | ralbidv 2986 |
. . . . . . . 8
⊢ (𝑥 = (𝑀 Σg 𝑧) → (∀𝑣 ∈ Word 𝐺(𝑥(+g‘𝑀)(𝑀 Σg 𝑣)) ∈ ran (𝑤 ∈ Word 𝐺 ↦ (𝑀 Σg 𝑤)) ↔ ∀𝑣 ∈ Word 𝐺((𝑀 Σg 𝑧)(+g‘𝑀)(𝑀 Σg 𝑣)) ∈ ran (𝑤 ∈ Word 𝐺 ↦ (𝑀 Σg 𝑤)))) |
95 | 91, 94 | ralrnmpt 6368 |
. . . . . . 7
⊢
(∀𝑧 ∈
Word 𝐺(𝑀 Σg 𝑧) ∈ V → (∀𝑥 ∈ ran (𝑧 ∈ Word 𝐺 ↦ (𝑀 Σg 𝑧))∀𝑣 ∈ Word 𝐺(𝑥(+g‘𝑀)(𝑀 Σg 𝑣)) ∈ ran (𝑤 ∈ Word 𝐺 ↦ (𝑀 Σg 𝑤)) ↔ ∀𝑧 ∈ Word 𝐺∀𝑣 ∈ Word 𝐺((𝑀 Σg 𝑧)(+g‘𝑀)(𝑀 Σg 𝑣)) ∈ ran (𝑤 ∈ Word 𝐺 ↦ (𝑀 Σg 𝑤)))) |
96 | | ovexd 6680 |
. . . . . . 7
⊢ (𝑧 ∈ Word 𝐺 → (𝑀 Σg 𝑧) ∈ V) |
97 | 95, 96 | mprg 2926 |
. . . . . 6
⊢
(∀𝑥 ∈
ran (𝑧 ∈ Word 𝐺 ↦ (𝑀 Σg 𝑧))∀𝑣 ∈ Word 𝐺(𝑥(+g‘𝑀)(𝑀 Σg 𝑣)) ∈ ran (𝑤 ∈ Word 𝐺 ↦ (𝑀 Σg 𝑤)) ↔ ∀𝑧 ∈ Word 𝐺∀𝑣 ∈ Word 𝐺((𝑀 Σg 𝑧)(+g‘𝑀)(𝑀 Σg 𝑣)) ∈ ran (𝑤 ∈ Word 𝐺 ↦ (𝑀 Σg 𝑤))) |
98 | 78, 90, 97 | 3bitri 286 |
. . . . 5
⊢
(∀𝑥 ∈
ran (𝑤 ∈ Word 𝐺 ↦ (𝑀 Σg 𝑤))∀𝑦 ∈ ran (𝑤 ∈ Word 𝐺 ↦ (𝑀 Σg 𝑤))(𝑥(+g‘𝑀)𝑦) ∈ ran (𝑤 ∈ Word 𝐺 ↦ (𝑀 Σg 𝑤)) ↔ ∀𝑧 ∈ Word 𝐺∀𝑣 ∈ Word 𝐺((𝑀 Σg 𝑧)(+g‘𝑀)(𝑀 Σg 𝑣)) ∈ ran (𝑤 ∈ Word 𝐺 ↦ (𝑀 Σg 𝑤))) |
99 | 74, 98 | sylibr 224 |
. . . 4
⊢ ((𝑀 ∈ Mnd ∧ 𝐺 ⊆ 𝐵) → ∀𝑥 ∈ ran (𝑤 ∈ Word 𝐺 ↦ (𝑀 Σg 𝑤))∀𝑦 ∈ ran (𝑤 ∈ Word 𝐺 ↦ (𝑀 Σg 𝑤))(𝑥(+g‘𝑀)𝑦) ∈ ran (𝑤 ∈ Word 𝐺 ↦ (𝑀 Σg 𝑤))) |
100 | 1, 41, 62 | issubm 17347 |
. . . . 5
⊢ (𝑀 ∈ Mnd → (ran (𝑤 ∈ Word 𝐺 ↦ (𝑀 Σg 𝑤)) ∈ (SubMnd‘𝑀) ↔ (ran (𝑤 ∈ Word 𝐺 ↦ (𝑀 Σg 𝑤)) ⊆ 𝐵 ∧ (0g‘𝑀) ∈ ran (𝑤 ∈ Word 𝐺 ↦ (𝑀 Σg 𝑤)) ∧ ∀𝑥 ∈ ran (𝑤 ∈ Word 𝐺 ↦ (𝑀 Σg 𝑤))∀𝑦 ∈ ran (𝑤 ∈ Word 𝐺 ↦ (𝑀 Σg 𝑤))(𝑥(+g‘𝑀)𝑦) ∈ ran (𝑤 ∈ Word 𝐺 ↦ (𝑀 Σg 𝑤))))) |
101 | 100 | adantr 481 |
. . . 4
⊢ ((𝑀 ∈ Mnd ∧ 𝐺 ⊆ 𝐵) → (ran (𝑤 ∈ Word 𝐺 ↦ (𝑀 Σg 𝑤)) ∈ (SubMnd‘𝑀) ↔ (ran (𝑤 ∈ Word 𝐺 ↦ (𝑀 Σg 𝑤)) ⊆ 𝐵 ∧ (0g‘𝑀) ∈ ran (𝑤 ∈ Word 𝐺 ↦ (𝑀 Σg 𝑤)) ∧ ∀𝑥 ∈ ran (𝑤 ∈ Word 𝐺 ↦ (𝑀 Σg 𝑤))∀𝑦 ∈ ran (𝑤 ∈ Word 𝐺 ↦ (𝑀 Σg 𝑤))(𝑥(+g‘𝑀)𝑦) ∈ ran (𝑤 ∈ Word 𝐺 ↦ (𝑀 Σg 𝑤))))) |
102 | 39, 52, 99, 101 | mpbir3and 1245 |
. . 3
⊢ ((𝑀 ∈ Mnd ∧ 𝐺 ⊆ 𝐵) → ran (𝑤 ∈ Word 𝐺 ↦ (𝑀 Σg 𝑤)) ∈ (SubMnd‘𝑀)) |
103 | 23 | mrcsscl 16280 |
. . 3
⊢
(((SubMnd‘𝑀)
∈ (Moore‘𝐵)
∧ 𝐺 ⊆ ran (𝑤 ∈ Word 𝐺 ↦ (𝑀 Σg 𝑤)) ∧ ran (𝑤 ∈ Word 𝐺 ↦ (𝑀 Σg 𝑤)) ∈ (SubMnd‘𝑀)) → (𝐾‘𝐺) ⊆ ran (𝑤 ∈ Word 𝐺 ↦ (𝑀 Σg 𝑤))) |
104 | 4, 22, 102, 103 | syl3anc 1326 |
. 2
⊢ ((𝑀 ∈ Mnd ∧ 𝐺 ⊆ 𝐵) → (𝐾‘𝐺) ⊆ ran (𝑤 ∈ Word 𝐺 ↦ (𝑀 Σg 𝑤))) |
105 | 104, 36 | eqssd 3620 |
1
⊢ ((𝑀 ∈ Mnd ∧ 𝐺 ⊆ 𝐵) → (𝐾‘𝐺) = ran (𝑤 ∈ Word 𝐺 ↦ (𝑀 Σg 𝑤))) |