Step | Hyp | Ref
| Expression |
1 | | gsumwspan.b |
. . . . . 6
⊢ 𝐵 = (Base‘𝑀) |
2 | 1 | submacs 18253 |
. . . . 5
⊢ (𝑀 ∈ Mnd →
(SubMnd‘𝑀) ∈
(ACS‘𝐵)) |
3 | 2 | acsmred 17159 |
. . . 4
⊢ (𝑀 ∈ Mnd →
(SubMnd‘𝑀) ∈
(Moore‘𝐵)) |
4 | 3 | adantr 484 |
. . 3
⊢ ((𝑀 ∈ Mnd ∧ 𝐺 ⊆ 𝐵) → (SubMnd‘𝑀) ∈ (Moore‘𝐵)) |
5 | | simpr 488 |
. . . . . . . 8
⊢ (((𝑀 ∈ Mnd ∧ 𝐺 ⊆ 𝐵) ∧ 𝑥 ∈ 𝐺) → 𝑥 ∈ 𝐺) |
6 | 5 | s1cld 14160 |
. . . . . . 7
⊢ (((𝑀 ∈ Mnd ∧ 𝐺 ⊆ 𝐵) ∧ 𝑥 ∈ 𝐺) → 〈“𝑥”〉 ∈ Word 𝐺) |
7 | | ssel2 3895 |
. . . . . . . . . 10
⊢ ((𝐺 ⊆ 𝐵 ∧ 𝑥 ∈ 𝐺) → 𝑥 ∈ 𝐵) |
8 | 7 | adantll 714 |
. . . . . . . . 9
⊢ (((𝑀 ∈ Mnd ∧ 𝐺 ⊆ 𝐵) ∧ 𝑥 ∈ 𝐺) → 𝑥 ∈ 𝐵) |
9 | 1 | gsumws1 18264 |
. . . . . . . . 9
⊢ (𝑥 ∈ 𝐵 → (𝑀 Σg
〈“𝑥”〉) = 𝑥) |
10 | 8, 9 | syl 17 |
. . . . . . . 8
⊢ (((𝑀 ∈ Mnd ∧ 𝐺 ⊆ 𝐵) ∧ 𝑥 ∈ 𝐺) → (𝑀 Σg
〈“𝑥”〉) = 𝑥) |
11 | 10 | eqcomd 2743 |
. . . . . . 7
⊢ (((𝑀 ∈ Mnd ∧ 𝐺 ⊆ 𝐵) ∧ 𝑥 ∈ 𝐺) → 𝑥 = (𝑀 Σg
〈“𝑥”〉)) |
12 | | oveq2 7221 |
. . . . . . . 8
⊢ (𝑤 = 〈“𝑥”〉 → (𝑀 Σg
𝑤) = (𝑀 Σg
〈“𝑥”〉)) |
13 | 12 | rspceeqv 3552 |
. . . . . . 7
⊢
((〈“𝑥”〉 ∈ Word 𝐺 ∧ 𝑥 = (𝑀 Σg
〈“𝑥”〉)) → ∃𝑤 ∈ Word 𝐺𝑥 = (𝑀 Σg 𝑤)) |
14 | 6, 11, 13 | syl2anc 587 |
. . . . . 6
⊢ (((𝑀 ∈ Mnd ∧ 𝐺 ⊆ 𝐵) ∧ 𝑥 ∈ 𝐺) → ∃𝑤 ∈ Word 𝐺𝑥 = (𝑀 Σg 𝑤)) |
15 | | eqid 2737 |
. . . . . . . 8
⊢ (𝑤 ∈ Word 𝐺 ↦ (𝑀 Σg 𝑤)) = (𝑤 ∈ Word 𝐺 ↦ (𝑀 Σg 𝑤)) |
16 | 15 | elrnmpt 5825 |
. . . . . . 7
⊢ (𝑥 ∈ V → (𝑥 ∈ ran (𝑤 ∈ Word 𝐺 ↦ (𝑀 Σg 𝑤)) ↔ ∃𝑤 ∈ Word 𝐺𝑥 = (𝑀 Σg 𝑤))) |
17 | 16 | elv 3414 |
. . . . . 6
⊢ (𝑥 ∈ ran (𝑤 ∈ Word 𝐺 ↦ (𝑀 Σg 𝑤)) ↔ ∃𝑤 ∈ Word 𝐺𝑥 = (𝑀 Σg 𝑤)) |
18 | 14, 17 | sylibr 237 |
. . . . 5
⊢ (((𝑀 ∈ Mnd ∧ 𝐺 ⊆ 𝐵) ∧ 𝑥 ∈ 𝐺) → 𝑥 ∈ ran (𝑤 ∈ Word 𝐺 ↦ (𝑀 Σg 𝑤))) |
19 | 18 | ex 416 |
. . . 4
⊢ ((𝑀 ∈ Mnd ∧ 𝐺 ⊆ 𝐵) → (𝑥 ∈ 𝐺 → 𝑥 ∈ ran (𝑤 ∈ Word 𝐺 ↦ (𝑀 Σg 𝑤)))) |
20 | 19 | ssrdv 3907 |
. . 3
⊢ ((𝑀 ∈ Mnd ∧ 𝐺 ⊆ 𝐵) → 𝐺 ⊆ ran (𝑤 ∈ Word 𝐺 ↦ (𝑀 Σg 𝑤))) |
21 | | gsumwspan.k |
. . . . . . . . . 10
⊢ 𝐾 =
(mrCls‘(SubMnd‘𝑀)) |
22 | 21 | mrccl 17114 |
. . . . . . . . 9
⊢
(((SubMnd‘𝑀)
∈ (Moore‘𝐵)
∧ 𝐺 ⊆ 𝐵) → (𝐾‘𝐺) ∈ (SubMnd‘𝑀)) |
23 | 3, 22 | sylan 583 |
. . . . . . . 8
⊢ ((𝑀 ∈ Mnd ∧ 𝐺 ⊆ 𝐵) → (𝐾‘𝐺) ∈ (SubMnd‘𝑀)) |
24 | 21 | mrcssid 17120 |
. . . . . . . . . . 11
⊢
(((SubMnd‘𝑀)
∈ (Moore‘𝐵)
∧ 𝐺 ⊆ 𝐵) → 𝐺 ⊆ (𝐾‘𝐺)) |
25 | 3, 24 | sylan 583 |
. . . . . . . . . 10
⊢ ((𝑀 ∈ Mnd ∧ 𝐺 ⊆ 𝐵) → 𝐺 ⊆ (𝐾‘𝐺)) |
26 | | sswrd 14077 |
. . . . . . . . . 10
⊢ (𝐺 ⊆ (𝐾‘𝐺) → Word 𝐺 ⊆ Word (𝐾‘𝐺)) |
27 | 25, 26 | syl 17 |
. . . . . . . . 9
⊢ ((𝑀 ∈ Mnd ∧ 𝐺 ⊆ 𝐵) → Word 𝐺 ⊆ Word (𝐾‘𝐺)) |
28 | 27 | sselda 3901 |
. . . . . . . 8
⊢ (((𝑀 ∈ Mnd ∧ 𝐺 ⊆ 𝐵) ∧ 𝑤 ∈ Word 𝐺) → 𝑤 ∈ Word (𝐾‘𝐺)) |
29 | | gsumwsubmcl 18263 |
. . . . . . . 8
⊢ (((𝐾‘𝐺) ∈ (SubMnd‘𝑀) ∧ 𝑤 ∈ Word (𝐾‘𝐺)) → (𝑀 Σg 𝑤) ∈ (𝐾‘𝐺)) |
30 | 23, 28, 29 | syl2an2r 685 |
. . . . . . 7
⊢ (((𝑀 ∈ Mnd ∧ 𝐺 ⊆ 𝐵) ∧ 𝑤 ∈ Word 𝐺) → (𝑀 Σg 𝑤) ∈ (𝐾‘𝐺)) |
31 | 30 | fmpttd 6932 |
. . . . . 6
⊢ ((𝑀 ∈ Mnd ∧ 𝐺 ⊆ 𝐵) → (𝑤 ∈ Word 𝐺 ↦ (𝑀 Σg 𝑤)):Word 𝐺⟶(𝐾‘𝐺)) |
32 | 31 | frnd 6553 |
. . . . 5
⊢ ((𝑀 ∈ Mnd ∧ 𝐺 ⊆ 𝐵) → ran (𝑤 ∈ Word 𝐺 ↦ (𝑀 Σg 𝑤)) ⊆ (𝐾‘𝐺)) |
33 | 3, 21 | mrcssvd 17126 |
. . . . . 6
⊢ (𝑀 ∈ Mnd → (𝐾‘𝐺) ⊆ 𝐵) |
34 | 33 | adantr 484 |
. . . . 5
⊢ ((𝑀 ∈ Mnd ∧ 𝐺 ⊆ 𝐵) → (𝐾‘𝐺) ⊆ 𝐵) |
35 | 32, 34 | sstrd 3911 |
. . . 4
⊢ ((𝑀 ∈ Mnd ∧ 𝐺 ⊆ 𝐵) → ran (𝑤 ∈ Word 𝐺 ↦ (𝑀 Σg 𝑤)) ⊆ 𝐵) |
36 | | wrd0 14094 |
. . . . . 6
⊢ ∅
∈ Word 𝐺 |
37 | | eqid 2737 |
. . . . . . . . 9
⊢
(0g‘𝑀) = (0g‘𝑀) |
38 | 37 | gsum0 18156 |
. . . . . . . 8
⊢ (𝑀 Σg
∅) = (0g‘𝑀) |
39 | 38 | eqcomi 2746 |
. . . . . . 7
⊢
(0g‘𝑀) = (𝑀 Σg
∅) |
40 | 39 | a1i 11 |
. . . . . 6
⊢ ((𝑀 ∈ Mnd ∧ 𝐺 ⊆ 𝐵) → (0g‘𝑀) = (𝑀 Σg
∅)) |
41 | | oveq2 7221 |
. . . . . . 7
⊢ (𝑤 = ∅ → (𝑀 Σg
𝑤) = (𝑀 Σg
∅)) |
42 | 41 | rspceeqv 3552 |
. . . . . 6
⊢ ((∅
∈ Word 𝐺 ∧
(0g‘𝑀) =
(𝑀
Σg ∅)) → ∃𝑤 ∈ Word 𝐺(0g‘𝑀) = (𝑀 Σg 𝑤)) |
43 | 36, 40, 42 | sylancr 590 |
. . . . 5
⊢ ((𝑀 ∈ Mnd ∧ 𝐺 ⊆ 𝐵) → ∃𝑤 ∈ Word 𝐺(0g‘𝑀) = (𝑀 Σg 𝑤)) |
44 | | fvex 6730 |
. . . . . 6
⊢
(0g‘𝑀) ∈ V |
45 | 15 | elrnmpt 5825 |
. . . . . 6
⊢
((0g‘𝑀) ∈ V →
((0g‘𝑀)
∈ ran (𝑤 ∈ Word
𝐺 ↦ (𝑀 Σg
𝑤)) ↔ ∃𝑤 ∈ Word 𝐺(0g‘𝑀) = (𝑀 Σg 𝑤))) |
46 | 44, 45 | ax-mp 5 |
. . . . 5
⊢
((0g‘𝑀) ∈ ran (𝑤 ∈ Word 𝐺 ↦ (𝑀 Σg 𝑤)) ↔ ∃𝑤 ∈ Word 𝐺(0g‘𝑀) = (𝑀 Σg 𝑤)) |
47 | 43, 46 | sylibr 237 |
. . . 4
⊢ ((𝑀 ∈ Mnd ∧ 𝐺 ⊆ 𝐵) → (0g‘𝑀) ∈ ran (𝑤 ∈ Word 𝐺 ↦ (𝑀 Σg 𝑤))) |
48 | | ccatcl 14129 |
. . . . . . . 8
⊢ ((𝑧 ∈ Word 𝐺 ∧ 𝑣 ∈ Word 𝐺) → (𝑧 ++ 𝑣) ∈ Word 𝐺) |
49 | | simpll 767 |
. . . . . . . . . 10
⊢ (((𝑀 ∈ Mnd ∧ 𝐺 ⊆ 𝐵) ∧ (𝑧 ∈ Word 𝐺 ∧ 𝑣 ∈ Word 𝐺)) → 𝑀 ∈ Mnd) |
50 | | sswrd 14077 |
. . . . . . . . . . . 12
⊢ (𝐺 ⊆ 𝐵 → Word 𝐺 ⊆ Word 𝐵) |
51 | 50 | ad2antlr 727 |
. . . . . . . . . . 11
⊢ (((𝑀 ∈ Mnd ∧ 𝐺 ⊆ 𝐵) ∧ (𝑧 ∈ Word 𝐺 ∧ 𝑣 ∈ Word 𝐺)) → Word 𝐺 ⊆ Word 𝐵) |
52 | | simprl 771 |
. . . . . . . . . . 11
⊢ (((𝑀 ∈ Mnd ∧ 𝐺 ⊆ 𝐵) ∧ (𝑧 ∈ Word 𝐺 ∧ 𝑣 ∈ Word 𝐺)) → 𝑧 ∈ Word 𝐺) |
53 | 51, 52 | sseldd 3902 |
. . . . . . . . . 10
⊢ (((𝑀 ∈ Mnd ∧ 𝐺 ⊆ 𝐵) ∧ (𝑧 ∈ Word 𝐺 ∧ 𝑣 ∈ Word 𝐺)) → 𝑧 ∈ Word 𝐵) |
54 | | simprr 773 |
. . . . . . . . . . 11
⊢ (((𝑀 ∈ Mnd ∧ 𝐺 ⊆ 𝐵) ∧ (𝑧 ∈ Word 𝐺 ∧ 𝑣 ∈ Word 𝐺)) → 𝑣 ∈ Word 𝐺) |
55 | 51, 54 | sseldd 3902 |
. . . . . . . . . 10
⊢ (((𝑀 ∈ Mnd ∧ 𝐺 ⊆ 𝐵) ∧ (𝑧 ∈ Word 𝐺 ∧ 𝑣 ∈ Word 𝐺)) → 𝑣 ∈ Word 𝐵) |
56 | | eqid 2737 |
. . . . . . . . . . 11
⊢
(+g‘𝑀) = (+g‘𝑀) |
57 | 1, 56 | gsumccat 18268 |
. . . . . . . . . 10
⊢ ((𝑀 ∈ Mnd ∧ 𝑧 ∈ Word 𝐵 ∧ 𝑣 ∈ Word 𝐵) → (𝑀 Σg (𝑧 ++ 𝑣)) = ((𝑀 Σg 𝑧)(+g‘𝑀)(𝑀 Σg 𝑣))) |
58 | 49, 53, 55, 57 | syl3anc 1373 |
. . . . . . . . 9
⊢ (((𝑀 ∈ Mnd ∧ 𝐺 ⊆ 𝐵) ∧ (𝑧 ∈ Word 𝐺 ∧ 𝑣 ∈ Word 𝐺)) → (𝑀 Σg (𝑧 ++ 𝑣)) = ((𝑀 Σg 𝑧)(+g‘𝑀)(𝑀 Σg 𝑣))) |
59 | 58 | eqcomd 2743 |
. . . . . . . 8
⊢ (((𝑀 ∈ Mnd ∧ 𝐺 ⊆ 𝐵) ∧ (𝑧 ∈ Word 𝐺 ∧ 𝑣 ∈ Word 𝐺)) → ((𝑀 Σg 𝑧)(+g‘𝑀)(𝑀 Σg 𝑣)) = (𝑀 Σg (𝑧 ++ 𝑣))) |
60 | | oveq2 7221 |
. . . . . . . . 9
⊢ (𝑤 = (𝑧 ++ 𝑣) → (𝑀 Σg 𝑤) = (𝑀 Σg (𝑧 ++ 𝑣))) |
61 | 60 | rspceeqv 3552 |
. . . . . . . 8
⊢ (((𝑧 ++ 𝑣) ∈ Word 𝐺 ∧ ((𝑀 Σg 𝑧)(+g‘𝑀)(𝑀 Σg 𝑣)) = (𝑀 Σg (𝑧 ++ 𝑣))) → ∃𝑤 ∈ Word 𝐺((𝑀 Σg 𝑧)(+g‘𝑀)(𝑀 Σg 𝑣)) = (𝑀 Σg 𝑤)) |
62 | 48, 59, 61 | syl2an2 686 |
. . . . . . 7
⊢ (((𝑀 ∈ Mnd ∧ 𝐺 ⊆ 𝐵) ∧ (𝑧 ∈ Word 𝐺 ∧ 𝑣 ∈ Word 𝐺)) → ∃𝑤 ∈ Word 𝐺((𝑀 Σg 𝑧)(+g‘𝑀)(𝑀 Σg 𝑣)) = (𝑀 Σg 𝑤)) |
63 | | ovex 7246 |
. . . . . . . 8
⊢ ((𝑀 Σg
𝑧)(+g‘𝑀)(𝑀 Σg 𝑣)) ∈ V |
64 | 15 | elrnmpt 5825 |
. . . . . . . 8
⊢ (((𝑀 Σg
𝑧)(+g‘𝑀)(𝑀 Σg 𝑣)) ∈ V → (((𝑀 Σg
𝑧)(+g‘𝑀)(𝑀 Σg 𝑣)) ∈ ran (𝑤 ∈ Word 𝐺 ↦ (𝑀 Σg 𝑤)) ↔ ∃𝑤 ∈ Word 𝐺((𝑀 Σg 𝑧)(+g‘𝑀)(𝑀 Σg 𝑣)) = (𝑀 Σg 𝑤))) |
65 | 63, 64 | ax-mp 5 |
. . . . . . 7
⊢ (((𝑀 Σg
𝑧)(+g‘𝑀)(𝑀 Σg 𝑣)) ∈ ran (𝑤 ∈ Word 𝐺 ↦ (𝑀 Σg 𝑤)) ↔ ∃𝑤 ∈ Word 𝐺((𝑀 Σg 𝑧)(+g‘𝑀)(𝑀 Σg 𝑣)) = (𝑀 Σg 𝑤)) |
66 | 62, 65 | sylibr 237 |
. . . . . 6
⊢ (((𝑀 ∈ Mnd ∧ 𝐺 ⊆ 𝐵) ∧ (𝑧 ∈ Word 𝐺 ∧ 𝑣 ∈ Word 𝐺)) → ((𝑀 Σg 𝑧)(+g‘𝑀)(𝑀 Σg 𝑣)) ∈ ran (𝑤 ∈ Word 𝐺 ↦ (𝑀 Σg 𝑤))) |
67 | 66 | ralrimivva 3112 |
. . . . 5
⊢ ((𝑀 ∈ Mnd ∧ 𝐺 ⊆ 𝐵) → ∀𝑧 ∈ Word 𝐺∀𝑣 ∈ Word 𝐺((𝑀 Σg 𝑧)(+g‘𝑀)(𝑀 Σg 𝑣)) ∈ ran (𝑤 ∈ Word 𝐺 ↦ (𝑀 Σg 𝑤))) |
68 | | oveq2 7221 |
. . . . . . . . 9
⊢ (𝑤 = 𝑧 → (𝑀 Σg 𝑤) = (𝑀 Σg 𝑧)) |
69 | 68 | cbvmptv 5158 |
. . . . . . . 8
⊢ (𝑤 ∈ Word 𝐺 ↦ (𝑀 Σg 𝑤)) = (𝑧 ∈ Word 𝐺 ↦ (𝑀 Σg 𝑧)) |
70 | 69 | rneqi 5806 |
. . . . . . 7
⊢ ran
(𝑤 ∈ Word 𝐺 ↦ (𝑀 Σg 𝑤)) = ran (𝑧 ∈ Word 𝐺 ↦ (𝑀 Σg 𝑧)) |
71 | 70 | raleqi 3323 |
. . . . . 6
⊢
(∀𝑥 ∈
ran (𝑤 ∈ Word 𝐺 ↦ (𝑀 Σg 𝑤))∀𝑦 ∈ ran (𝑤 ∈ Word 𝐺 ↦ (𝑀 Σg 𝑤))(𝑥(+g‘𝑀)𝑦) ∈ ran (𝑤 ∈ Word 𝐺 ↦ (𝑀 Σg 𝑤)) ↔ ∀𝑥 ∈ ran (𝑧 ∈ Word 𝐺 ↦ (𝑀 Σg 𝑧))∀𝑦 ∈ ran (𝑤 ∈ Word 𝐺 ↦ (𝑀 Σg 𝑤))(𝑥(+g‘𝑀)𝑦) ∈ ran (𝑤 ∈ Word 𝐺 ↦ (𝑀 Σg 𝑤))) |
72 | | oveq2 7221 |
. . . . . . . . . . 11
⊢ (𝑤 = 𝑣 → (𝑀 Σg 𝑤) = (𝑀 Σg 𝑣)) |
73 | 72 | cbvmptv 5158 |
. . . . . . . . . 10
⊢ (𝑤 ∈ Word 𝐺 ↦ (𝑀 Σg 𝑤)) = (𝑣 ∈ Word 𝐺 ↦ (𝑀 Σg 𝑣)) |
74 | 73 | rneqi 5806 |
. . . . . . . . 9
⊢ ran
(𝑤 ∈ Word 𝐺 ↦ (𝑀 Σg 𝑤)) = ran (𝑣 ∈ Word 𝐺 ↦ (𝑀 Σg 𝑣)) |
75 | 74 | raleqi 3323 |
. . . . . . . 8
⊢
(∀𝑦 ∈
ran (𝑤 ∈ Word 𝐺 ↦ (𝑀 Σg 𝑤))(𝑥(+g‘𝑀)𝑦) ∈ ran (𝑤 ∈ Word 𝐺 ↦ (𝑀 Σg 𝑤)) ↔ ∀𝑦 ∈ ran (𝑣 ∈ Word 𝐺 ↦ (𝑀 Σg 𝑣))(𝑥(+g‘𝑀)𝑦) ∈ ran (𝑤 ∈ Word 𝐺 ↦ (𝑀 Σg 𝑤))) |
76 | | eqid 2737 |
. . . . . . . . . 10
⊢ (𝑣 ∈ Word 𝐺 ↦ (𝑀 Σg 𝑣)) = (𝑣 ∈ Word 𝐺 ↦ (𝑀 Σg 𝑣)) |
77 | | oveq2 7221 |
. . . . . . . . . . 11
⊢ (𝑦 = (𝑀 Σg 𝑣) → (𝑥(+g‘𝑀)𝑦) = (𝑥(+g‘𝑀)(𝑀 Σg 𝑣))) |
78 | 77 | eleq1d 2822 |
. . . . . . . . . 10
⊢ (𝑦 = (𝑀 Σg 𝑣) → ((𝑥(+g‘𝑀)𝑦) ∈ ran (𝑤 ∈ Word 𝐺 ↦ (𝑀 Σg 𝑤)) ↔ (𝑥(+g‘𝑀)(𝑀 Σg 𝑣)) ∈ ran (𝑤 ∈ Word 𝐺 ↦ (𝑀 Σg 𝑤)))) |
79 | 76, 78 | ralrnmptw 6913 |
. . . . . . . . 9
⊢
(∀𝑣 ∈
Word 𝐺(𝑀 Σg 𝑣) ∈ V → (∀𝑦 ∈ ran (𝑣 ∈ Word 𝐺 ↦ (𝑀 Σg 𝑣))(𝑥(+g‘𝑀)𝑦) ∈ ran (𝑤 ∈ Word 𝐺 ↦ (𝑀 Σg 𝑤)) ↔ ∀𝑣 ∈ Word 𝐺(𝑥(+g‘𝑀)(𝑀 Σg 𝑣)) ∈ ran (𝑤 ∈ Word 𝐺 ↦ (𝑀 Σg 𝑤)))) |
80 | | ovexd 7248 |
. . . . . . . . 9
⊢ (𝑣 ∈ Word 𝐺 → (𝑀 Σg 𝑣) ∈ V) |
81 | 79, 80 | mprg 3075 |
. . . . . . . 8
⊢
(∀𝑦 ∈
ran (𝑣 ∈ Word 𝐺 ↦ (𝑀 Σg 𝑣))(𝑥(+g‘𝑀)𝑦) ∈ ran (𝑤 ∈ Word 𝐺 ↦ (𝑀 Σg 𝑤)) ↔ ∀𝑣 ∈ Word 𝐺(𝑥(+g‘𝑀)(𝑀 Σg 𝑣)) ∈ ran (𝑤 ∈ Word 𝐺 ↦ (𝑀 Σg 𝑤))) |
82 | 75, 81 | bitri 278 |
. . . . . . 7
⊢
(∀𝑦 ∈
ran (𝑤 ∈ Word 𝐺 ↦ (𝑀 Σg 𝑤))(𝑥(+g‘𝑀)𝑦) ∈ ran (𝑤 ∈ Word 𝐺 ↦ (𝑀 Σg 𝑤)) ↔ ∀𝑣 ∈ Word 𝐺(𝑥(+g‘𝑀)(𝑀 Σg 𝑣)) ∈ ran (𝑤 ∈ Word 𝐺 ↦ (𝑀 Σg 𝑤))) |
83 | 82 | ralbii 3088 |
. . . . . 6
⊢
(∀𝑥 ∈
ran (𝑧 ∈ Word 𝐺 ↦ (𝑀 Σg 𝑧))∀𝑦 ∈ ran (𝑤 ∈ Word 𝐺 ↦ (𝑀 Σg 𝑤))(𝑥(+g‘𝑀)𝑦) ∈ ran (𝑤 ∈ Word 𝐺 ↦ (𝑀 Σg 𝑤)) ↔ ∀𝑥 ∈ ran (𝑧 ∈ Word 𝐺 ↦ (𝑀 Σg 𝑧))∀𝑣 ∈ Word 𝐺(𝑥(+g‘𝑀)(𝑀 Σg 𝑣)) ∈ ran (𝑤 ∈ Word 𝐺 ↦ (𝑀 Σg 𝑤))) |
84 | | eqid 2737 |
. . . . . . . 8
⊢ (𝑧 ∈ Word 𝐺 ↦ (𝑀 Σg 𝑧)) = (𝑧 ∈ Word 𝐺 ↦ (𝑀 Σg 𝑧)) |
85 | | oveq1 7220 |
. . . . . . . . . 10
⊢ (𝑥 = (𝑀 Σg 𝑧) → (𝑥(+g‘𝑀)(𝑀 Σg 𝑣)) = ((𝑀 Σg 𝑧)(+g‘𝑀)(𝑀 Σg 𝑣))) |
86 | 85 | eleq1d 2822 |
. . . . . . . . 9
⊢ (𝑥 = (𝑀 Σg 𝑧) → ((𝑥(+g‘𝑀)(𝑀 Σg 𝑣)) ∈ ran (𝑤 ∈ Word 𝐺 ↦ (𝑀 Σg 𝑤)) ↔ ((𝑀 Σg 𝑧)(+g‘𝑀)(𝑀 Σg 𝑣)) ∈ ran (𝑤 ∈ Word 𝐺 ↦ (𝑀 Σg 𝑤)))) |
87 | 86 | ralbidv 3118 |
. . . . . . . 8
⊢ (𝑥 = (𝑀 Σg 𝑧) → (∀𝑣 ∈ Word 𝐺(𝑥(+g‘𝑀)(𝑀 Σg 𝑣)) ∈ ran (𝑤 ∈ Word 𝐺 ↦ (𝑀 Σg 𝑤)) ↔ ∀𝑣 ∈ Word 𝐺((𝑀 Σg 𝑧)(+g‘𝑀)(𝑀 Σg 𝑣)) ∈ ran (𝑤 ∈ Word 𝐺 ↦ (𝑀 Σg 𝑤)))) |
88 | 84, 87 | ralrnmptw 6913 |
. . . . . . 7
⊢
(∀𝑧 ∈
Word 𝐺(𝑀 Σg 𝑧) ∈ V → (∀𝑥 ∈ ran (𝑧 ∈ Word 𝐺 ↦ (𝑀 Σg 𝑧))∀𝑣 ∈ Word 𝐺(𝑥(+g‘𝑀)(𝑀 Σg 𝑣)) ∈ ran (𝑤 ∈ Word 𝐺 ↦ (𝑀 Σg 𝑤)) ↔ ∀𝑧 ∈ Word 𝐺∀𝑣 ∈ Word 𝐺((𝑀 Σg 𝑧)(+g‘𝑀)(𝑀 Σg 𝑣)) ∈ ran (𝑤 ∈ Word 𝐺 ↦ (𝑀 Σg 𝑤)))) |
89 | | ovexd 7248 |
. . . . . . 7
⊢ (𝑧 ∈ Word 𝐺 → (𝑀 Σg 𝑧) ∈ V) |
90 | 88, 89 | mprg 3075 |
. . . . . 6
⊢
(∀𝑥 ∈
ran (𝑧 ∈ Word 𝐺 ↦ (𝑀 Σg 𝑧))∀𝑣 ∈ Word 𝐺(𝑥(+g‘𝑀)(𝑀 Σg 𝑣)) ∈ ran (𝑤 ∈ Word 𝐺 ↦ (𝑀 Σg 𝑤)) ↔ ∀𝑧 ∈ Word 𝐺∀𝑣 ∈ Word 𝐺((𝑀 Σg 𝑧)(+g‘𝑀)(𝑀 Σg 𝑣)) ∈ ran (𝑤 ∈ Word 𝐺 ↦ (𝑀 Σg 𝑤))) |
91 | 71, 83, 90 | 3bitri 300 |
. . . . 5
⊢
(∀𝑥 ∈
ran (𝑤 ∈ Word 𝐺 ↦ (𝑀 Σg 𝑤))∀𝑦 ∈ ran (𝑤 ∈ Word 𝐺 ↦ (𝑀 Σg 𝑤))(𝑥(+g‘𝑀)𝑦) ∈ ran (𝑤 ∈ Word 𝐺 ↦ (𝑀 Σg 𝑤)) ↔ ∀𝑧 ∈ Word 𝐺∀𝑣 ∈ Word 𝐺((𝑀 Σg 𝑧)(+g‘𝑀)(𝑀 Σg 𝑣)) ∈ ran (𝑤 ∈ Word 𝐺 ↦ (𝑀 Σg 𝑤))) |
92 | 67, 91 | sylibr 237 |
. . . 4
⊢ ((𝑀 ∈ Mnd ∧ 𝐺 ⊆ 𝐵) → ∀𝑥 ∈ ran (𝑤 ∈ Word 𝐺 ↦ (𝑀 Σg 𝑤))∀𝑦 ∈ ran (𝑤 ∈ Word 𝐺 ↦ (𝑀 Σg 𝑤))(𝑥(+g‘𝑀)𝑦) ∈ ran (𝑤 ∈ Word 𝐺 ↦ (𝑀 Σg 𝑤))) |
93 | 1, 37, 56 | issubm 18230 |
. . . . 5
⊢ (𝑀 ∈ Mnd → (ran (𝑤 ∈ Word 𝐺 ↦ (𝑀 Σg 𝑤)) ∈ (SubMnd‘𝑀) ↔ (ran (𝑤 ∈ Word 𝐺 ↦ (𝑀 Σg 𝑤)) ⊆ 𝐵 ∧ (0g‘𝑀) ∈ ran (𝑤 ∈ Word 𝐺 ↦ (𝑀 Σg 𝑤)) ∧ ∀𝑥 ∈ ran (𝑤 ∈ Word 𝐺 ↦ (𝑀 Σg 𝑤))∀𝑦 ∈ ran (𝑤 ∈ Word 𝐺 ↦ (𝑀 Σg 𝑤))(𝑥(+g‘𝑀)𝑦) ∈ ran (𝑤 ∈ Word 𝐺 ↦ (𝑀 Σg 𝑤))))) |
94 | 93 | adantr 484 |
. . . 4
⊢ ((𝑀 ∈ Mnd ∧ 𝐺 ⊆ 𝐵) → (ran (𝑤 ∈ Word 𝐺 ↦ (𝑀 Σg 𝑤)) ∈ (SubMnd‘𝑀) ↔ (ran (𝑤 ∈ Word 𝐺 ↦ (𝑀 Σg 𝑤)) ⊆ 𝐵 ∧ (0g‘𝑀) ∈ ran (𝑤 ∈ Word 𝐺 ↦ (𝑀 Σg 𝑤)) ∧ ∀𝑥 ∈ ran (𝑤 ∈ Word 𝐺 ↦ (𝑀 Σg 𝑤))∀𝑦 ∈ ran (𝑤 ∈ Word 𝐺 ↦ (𝑀 Σg 𝑤))(𝑥(+g‘𝑀)𝑦) ∈ ran (𝑤 ∈ Word 𝐺 ↦ (𝑀 Σg 𝑤))))) |
95 | 35, 47, 92, 94 | mpbir3and 1344 |
. . 3
⊢ ((𝑀 ∈ Mnd ∧ 𝐺 ⊆ 𝐵) → ran (𝑤 ∈ Word 𝐺 ↦ (𝑀 Σg 𝑤)) ∈ (SubMnd‘𝑀)) |
96 | 21 | mrcsscl 17123 |
. . 3
⊢
(((SubMnd‘𝑀)
∈ (Moore‘𝐵)
∧ 𝐺 ⊆ ran (𝑤 ∈ Word 𝐺 ↦ (𝑀 Σg 𝑤)) ∧ ran (𝑤 ∈ Word 𝐺 ↦ (𝑀 Σg 𝑤)) ∈ (SubMnd‘𝑀)) → (𝐾‘𝐺) ⊆ ran (𝑤 ∈ Word 𝐺 ↦ (𝑀 Σg 𝑤))) |
97 | 4, 20, 95, 96 | syl3anc 1373 |
. 2
⊢ ((𝑀 ∈ Mnd ∧ 𝐺 ⊆ 𝐵) → (𝐾‘𝐺) ⊆ ran (𝑤 ∈ Word 𝐺 ↦ (𝑀 Σg 𝑤))) |
98 | 97, 32 | eqssd 3918 |
1
⊢ ((𝑀 ∈ Mnd ∧ 𝐺 ⊆ 𝐵) → (𝐾‘𝐺) = ran (𝑤 ∈ Word 𝐺 ↦ (𝑀 Σg 𝑤))) |