| Step | Hyp | Ref
| Expression |
| 1 | | gsumwspan.b |
. . . . . 6
⊢ 𝐵 = (Base‘𝑀) |
| 2 | 1 | submacs 18840 |
. . . . 5
⊢ (𝑀 ∈ Mnd →
(SubMnd‘𝑀) ∈
(ACS‘𝐵)) |
| 3 | 2 | acsmred 17699 |
. . . 4
⊢ (𝑀 ∈ Mnd →
(SubMnd‘𝑀) ∈
(Moore‘𝐵)) |
| 4 | 3 | adantr 480 |
. . 3
⊢ ((𝑀 ∈ Mnd ∧ 𝐺 ⊆ 𝐵) → (SubMnd‘𝑀) ∈ (Moore‘𝐵)) |
| 5 | | simpr 484 |
. . . . . . . 8
⊢ (((𝑀 ∈ Mnd ∧ 𝐺 ⊆ 𝐵) ∧ 𝑥 ∈ 𝐺) → 𝑥 ∈ 𝐺) |
| 6 | 5 | s1cld 14641 |
. . . . . . 7
⊢ (((𝑀 ∈ Mnd ∧ 𝐺 ⊆ 𝐵) ∧ 𝑥 ∈ 𝐺) → 〈“𝑥”〉 ∈ Word 𝐺) |
| 7 | | ssel2 3978 |
. . . . . . . . . 10
⊢ ((𝐺 ⊆ 𝐵 ∧ 𝑥 ∈ 𝐺) → 𝑥 ∈ 𝐵) |
| 8 | 7 | adantll 714 |
. . . . . . . . 9
⊢ (((𝑀 ∈ Mnd ∧ 𝐺 ⊆ 𝐵) ∧ 𝑥 ∈ 𝐺) → 𝑥 ∈ 𝐵) |
| 9 | 1 | gsumws1 18851 |
. . . . . . . . 9
⊢ (𝑥 ∈ 𝐵 → (𝑀 Σg
〈“𝑥”〉) = 𝑥) |
| 10 | 8, 9 | syl 17 |
. . . . . . . 8
⊢ (((𝑀 ∈ Mnd ∧ 𝐺 ⊆ 𝐵) ∧ 𝑥 ∈ 𝐺) → (𝑀 Σg
〈“𝑥”〉) = 𝑥) |
| 11 | 10 | eqcomd 2743 |
. . . . . . 7
⊢ (((𝑀 ∈ Mnd ∧ 𝐺 ⊆ 𝐵) ∧ 𝑥 ∈ 𝐺) → 𝑥 = (𝑀 Σg
〈“𝑥”〉)) |
| 12 | | oveq2 7439 |
. . . . . . . 8
⊢ (𝑤 = 〈“𝑥”〉 → (𝑀 Σg
𝑤) = (𝑀 Σg
〈“𝑥”〉)) |
| 13 | 12 | rspceeqv 3645 |
. . . . . . 7
⊢
((〈“𝑥”〉 ∈ Word 𝐺 ∧ 𝑥 = (𝑀 Σg
〈“𝑥”〉)) → ∃𝑤 ∈ Word 𝐺𝑥 = (𝑀 Σg 𝑤)) |
| 14 | 6, 11, 13 | syl2anc 584 |
. . . . . 6
⊢ (((𝑀 ∈ Mnd ∧ 𝐺 ⊆ 𝐵) ∧ 𝑥 ∈ 𝐺) → ∃𝑤 ∈ Word 𝐺𝑥 = (𝑀 Σg 𝑤)) |
| 15 | | eqid 2737 |
. . . . . . . 8
⊢ (𝑤 ∈ Word 𝐺 ↦ (𝑀 Σg 𝑤)) = (𝑤 ∈ Word 𝐺 ↦ (𝑀 Σg 𝑤)) |
| 16 | 15 | elrnmpt 5969 |
. . . . . . 7
⊢ (𝑥 ∈ V → (𝑥 ∈ ran (𝑤 ∈ Word 𝐺 ↦ (𝑀 Σg 𝑤)) ↔ ∃𝑤 ∈ Word 𝐺𝑥 = (𝑀 Σg 𝑤))) |
| 17 | 16 | elv 3485 |
. . . . . 6
⊢ (𝑥 ∈ ran (𝑤 ∈ Word 𝐺 ↦ (𝑀 Σg 𝑤)) ↔ ∃𝑤 ∈ Word 𝐺𝑥 = (𝑀 Σg 𝑤)) |
| 18 | 14, 17 | sylibr 234 |
. . . . 5
⊢ (((𝑀 ∈ Mnd ∧ 𝐺 ⊆ 𝐵) ∧ 𝑥 ∈ 𝐺) → 𝑥 ∈ ran (𝑤 ∈ Word 𝐺 ↦ (𝑀 Σg 𝑤))) |
| 19 | 18 | ex 412 |
. . . 4
⊢ ((𝑀 ∈ Mnd ∧ 𝐺 ⊆ 𝐵) → (𝑥 ∈ 𝐺 → 𝑥 ∈ ran (𝑤 ∈ Word 𝐺 ↦ (𝑀 Σg 𝑤)))) |
| 20 | 19 | ssrdv 3989 |
. . 3
⊢ ((𝑀 ∈ Mnd ∧ 𝐺 ⊆ 𝐵) → 𝐺 ⊆ ran (𝑤 ∈ Word 𝐺 ↦ (𝑀 Σg 𝑤))) |
| 21 | | gsumwspan.k |
. . . . . . . . . 10
⊢ 𝐾 =
(mrCls‘(SubMnd‘𝑀)) |
| 22 | 21 | mrccl 17654 |
. . . . . . . . 9
⊢
(((SubMnd‘𝑀)
∈ (Moore‘𝐵)
∧ 𝐺 ⊆ 𝐵) → (𝐾‘𝐺) ∈ (SubMnd‘𝑀)) |
| 23 | 3, 22 | sylan 580 |
. . . . . . . 8
⊢ ((𝑀 ∈ Mnd ∧ 𝐺 ⊆ 𝐵) → (𝐾‘𝐺) ∈ (SubMnd‘𝑀)) |
| 24 | 21 | mrcssid 17660 |
. . . . . . . . . . 11
⊢
(((SubMnd‘𝑀)
∈ (Moore‘𝐵)
∧ 𝐺 ⊆ 𝐵) → 𝐺 ⊆ (𝐾‘𝐺)) |
| 25 | 3, 24 | sylan 580 |
. . . . . . . . . 10
⊢ ((𝑀 ∈ Mnd ∧ 𝐺 ⊆ 𝐵) → 𝐺 ⊆ (𝐾‘𝐺)) |
| 26 | | sswrd 14560 |
. . . . . . . . . 10
⊢ (𝐺 ⊆ (𝐾‘𝐺) → Word 𝐺 ⊆ Word (𝐾‘𝐺)) |
| 27 | 25, 26 | syl 17 |
. . . . . . . . 9
⊢ ((𝑀 ∈ Mnd ∧ 𝐺 ⊆ 𝐵) → Word 𝐺 ⊆ Word (𝐾‘𝐺)) |
| 28 | 27 | sselda 3983 |
. . . . . . . 8
⊢ (((𝑀 ∈ Mnd ∧ 𝐺 ⊆ 𝐵) ∧ 𝑤 ∈ Word 𝐺) → 𝑤 ∈ Word (𝐾‘𝐺)) |
| 29 | | gsumwsubmcl 18850 |
. . . . . . . 8
⊢ (((𝐾‘𝐺) ∈ (SubMnd‘𝑀) ∧ 𝑤 ∈ Word (𝐾‘𝐺)) → (𝑀 Σg 𝑤) ∈ (𝐾‘𝐺)) |
| 30 | 23, 28, 29 | syl2an2r 685 |
. . . . . . 7
⊢ (((𝑀 ∈ Mnd ∧ 𝐺 ⊆ 𝐵) ∧ 𝑤 ∈ Word 𝐺) → (𝑀 Σg 𝑤) ∈ (𝐾‘𝐺)) |
| 31 | 30 | fmpttd 7135 |
. . . . . 6
⊢ ((𝑀 ∈ Mnd ∧ 𝐺 ⊆ 𝐵) → (𝑤 ∈ Word 𝐺 ↦ (𝑀 Σg 𝑤)):Word 𝐺⟶(𝐾‘𝐺)) |
| 32 | 31 | frnd 6744 |
. . . . 5
⊢ ((𝑀 ∈ Mnd ∧ 𝐺 ⊆ 𝐵) → ran (𝑤 ∈ Word 𝐺 ↦ (𝑀 Σg 𝑤)) ⊆ (𝐾‘𝐺)) |
| 33 | 3, 21 | mrcssvd 17666 |
. . . . . 6
⊢ (𝑀 ∈ Mnd → (𝐾‘𝐺) ⊆ 𝐵) |
| 34 | 33 | adantr 480 |
. . . . 5
⊢ ((𝑀 ∈ Mnd ∧ 𝐺 ⊆ 𝐵) → (𝐾‘𝐺) ⊆ 𝐵) |
| 35 | 32, 34 | sstrd 3994 |
. . . 4
⊢ ((𝑀 ∈ Mnd ∧ 𝐺 ⊆ 𝐵) → ran (𝑤 ∈ Word 𝐺 ↦ (𝑀 Σg 𝑤)) ⊆ 𝐵) |
| 36 | | wrd0 14577 |
. . . . . 6
⊢ ∅
∈ Word 𝐺 |
| 37 | | eqid 2737 |
. . . . . . . . 9
⊢
(0g‘𝑀) = (0g‘𝑀) |
| 38 | 37 | gsum0 18697 |
. . . . . . . 8
⊢ (𝑀 Σg
∅) = (0g‘𝑀) |
| 39 | 38 | eqcomi 2746 |
. . . . . . 7
⊢
(0g‘𝑀) = (𝑀 Σg
∅) |
| 40 | 39 | a1i 11 |
. . . . . 6
⊢ ((𝑀 ∈ Mnd ∧ 𝐺 ⊆ 𝐵) → (0g‘𝑀) = (𝑀 Σg
∅)) |
| 41 | | oveq2 7439 |
. . . . . . 7
⊢ (𝑤 = ∅ → (𝑀 Σg
𝑤) = (𝑀 Σg
∅)) |
| 42 | 41 | rspceeqv 3645 |
. . . . . 6
⊢ ((∅
∈ Word 𝐺 ∧
(0g‘𝑀) =
(𝑀
Σg ∅)) → ∃𝑤 ∈ Word 𝐺(0g‘𝑀) = (𝑀 Σg 𝑤)) |
| 43 | 36, 40, 42 | sylancr 587 |
. . . . 5
⊢ ((𝑀 ∈ Mnd ∧ 𝐺 ⊆ 𝐵) → ∃𝑤 ∈ Word 𝐺(0g‘𝑀) = (𝑀 Σg 𝑤)) |
| 44 | | fvex 6919 |
. . . . . 6
⊢
(0g‘𝑀) ∈ V |
| 45 | 15 | elrnmpt 5969 |
. . . . . 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 234 |
. . . 4
⊢ ((𝑀 ∈ Mnd ∧ 𝐺 ⊆ 𝐵) → (0g‘𝑀) ∈ ran (𝑤 ∈ Word 𝐺 ↦ (𝑀 Σg 𝑤))) |
| 48 | | ccatcl 14612 |
. . . . . . . 8
⊢ ((𝑧 ∈ Word 𝐺 ∧ 𝑣 ∈ Word 𝐺) → (𝑧 ++ 𝑣) ∈ Word 𝐺) |
| 49 | | simpll 767 |
. . . . . . . . . 10
⊢ (((𝑀 ∈ Mnd ∧ 𝐺 ⊆ 𝐵) ∧ (𝑧 ∈ Word 𝐺 ∧ 𝑣 ∈ Word 𝐺)) → 𝑀 ∈ Mnd) |
| 50 | | sswrd 14560 |
. . . . . . . . . . . 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 3984 |
. . . . . . . . . 10
⊢ (((𝑀 ∈ Mnd ∧ 𝐺 ⊆ 𝐵) ∧ (𝑧 ∈ Word 𝐺 ∧ 𝑣 ∈ Word 𝐺)) → 𝑧 ∈ Word 𝐵) |
| 54 | | simprr 773 |
. . . . . . . . . . 11
⊢ (((𝑀 ∈ Mnd ∧ 𝐺 ⊆ 𝐵) ∧ (𝑧 ∈ Word 𝐺 ∧ 𝑣 ∈ Word 𝐺)) → 𝑣 ∈ Word 𝐺) |
| 55 | 51, 54 | sseldd 3984 |
. . . . . . . . . 10
⊢ (((𝑀 ∈ Mnd ∧ 𝐺 ⊆ 𝐵) ∧ (𝑧 ∈ Word 𝐺 ∧ 𝑣 ∈ Word 𝐺)) → 𝑣 ∈ Word 𝐵) |
| 56 | | eqid 2737 |
. . . . . . . . . . 11
⊢
(+g‘𝑀) = (+g‘𝑀) |
| 57 | 1, 56 | gsumccat 18854 |
. . . . . . . . . 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 7439 |
. . . . . . . . 9
⊢ (𝑤 = (𝑧 ++ 𝑣) → (𝑀 Σg 𝑤) = (𝑀 Σg (𝑧 ++ 𝑣))) |
| 61 | 60 | rspceeqv 3645 |
. . . . . . . 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 7464 |
. . . . . . . 8
⊢ ((𝑀 Σg
𝑧)(+g‘𝑀)(𝑀 Σg 𝑣)) ∈ V |
| 64 | 15 | elrnmpt 5969 |
. . . . . . . 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 234 |
. . . . . 6
⊢ (((𝑀 ∈ Mnd ∧ 𝐺 ⊆ 𝐵) ∧ (𝑧 ∈ Word 𝐺 ∧ 𝑣 ∈ Word 𝐺)) → ((𝑀 Σg 𝑧)(+g‘𝑀)(𝑀 Σg 𝑣)) ∈ ran (𝑤 ∈ Word 𝐺 ↦ (𝑀 Σg 𝑤))) |
| 67 | 66 | ralrimivva 3202 |
. . . . 5
⊢ ((𝑀 ∈ Mnd ∧ 𝐺 ⊆ 𝐵) → ∀𝑧 ∈ Word 𝐺∀𝑣 ∈ Word 𝐺((𝑀 Σg 𝑧)(+g‘𝑀)(𝑀 Σg 𝑣)) ∈ ran (𝑤 ∈ Word 𝐺 ↦ (𝑀 Σg 𝑤))) |
| 68 | | oveq2 7439 |
. . . . . . . . 9
⊢ (𝑤 = 𝑧 → (𝑀 Σg 𝑤) = (𝑀 Σg 𝑧)) |
| 69 | 68 | cbvmptv 5255 |
. . . . . . . 8
⊢ (𝑤 ∈ Word 𝐺 ↦ (𝑀 Σg 𝑤)) = (𝑧 ∈ Word 𝐺 ↦ (𝑀 Σg 𝑧)) |
| 70 | 69 | rneqi 5948 |
. . . . . . 7
⊢ ran
(𝑤 ∈ Word 𝐺 ↦ (𝑀 Σg 𝑤)) = ran (𝑧 ∈ Word 𝐺 ↦ (𝑀 Σg 𝑧)) |
| 71 | 70 | raleqi 3324 |
. . . . . 6
⊢
(∀𝑥 ∈
ran (𝑤 ∈ Word 𝐺 ↦ (𝑀 Σg 𝑤))∀𝑦 ∈ ran (𝑤 ∈ Word 𝐺 ↦ (𝑀 Σg 𝑤))(𝑥(+g‘𝑀)𝑦) ∈ ran (𝑤 ∈ Word 𝐺 ↦ (𝑀 Σg 𝑤)) ↔ ∀𝑥 ∈ ran (𝑧 ∈ Word 𝐺 ↦ (𝑀 Σg 𝑧))∀𝑦 ∈ ran (𝑤 ∈ Word 𝐺 ↦ (𝑀 Σg 𝑤))(𝑥(+g‘𝑀)𝑦) ∈ ran (𝑤 ∈ Word 𝐺 ↦ (𝑀 Σg 𝑤))) |
| 72 | | oveq2 7439 |
. . . . . . . . . . 11
⊢ (𝑤 = 𝑣 → (𝑀 Σg 𝑤) = (𝑀 Σg 𝑣)) |
| 73 | 72 | cbvmptv 5255 |
. . . . . . . . . 10
⊢ (𝑤 ∈ Word 𝐺 ↦ (𝑀 Σg 𝑤)) = (𝑣 ∈ Word 𝐺 ↦ (𝑀 Σg 𝑣)) |
| 74 | 73 | rneqi 5948 |
. . . . . . . . 9
⊢ ran
(𝑤 ∈ Word 𝐺 ↦ (𝑀 Σg 𝑤)) = ran (𝑣 ∈ Word 𝐺 ↦ (𝑀 Σg 𝑣)) |
| 75 | 74 | raleqi 3324 |
. . . . . . . 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 7439 |
. . . . . . . . . . 11
⊢ (𝑦 = (𝑀 Σg 𝑣) → (𝑥(+g‘𝑀)𝑦) = (𝑥(+g‘𝑀)(𝑀 Σg 𝑣))) |
| 78 | 77 | eleq1d 2826 |
. . . . . . . . . 10
⊢ (𝑦 = (𝑀 Σg 𝑣) → ((𝑥(+g‘𝑀)𝑦) ∈ ran (𝑤 ∈ Word 𝐺 ↦ (𝑀 Σg 𝑤)) ↔ (𝑥(+g‘𝑀)(𝑀 Σg 𝑣)) ∈ ran (𝑤 ∈ Word 𝐺 ↦ (𝑀 Σg 𝑤)))) |
| 79 | 76, 78 | ralrnmptw 7114 |
. . . . . . . . 9
⊢
(∀𝑣 ∈
Word 𝐺(𝑀 Σg 𝑣) ∈ V → (∀𝑦 ∈ ran (𝑣 ∈ Word 𝐺 ↦ (𝑀 Σg 𝑣))(𝑥(+g‘𝑀)𝑦) ∈ ran (𝑤 ∈ Word 𝐺 ↦ (𝑀 Σg 𝑤)) ↔ ∀𝑣 ∈ Word 𝐺(𝑥(+g‘𝑀)(𝑀 Σg 𝑣)) ∈ ran (𝑤 ∈ Word 𝐺 ↦ (𝑀 Σg 𝑤)))) |
| 80 | | ovexd 7466 |
. . . . . . . . 9
⊢ (𝑣 ∈ Word 𝐺 → (𝑀 Σg 𝑣) ∈ V) |
| 81 | 79, 80 | mprg 3067 |
. . . . . . . 8
⊢
(∀𝑦 ∈
ran (𝑣 ∈ Word 𝐺 ↦ (𝑀 Σg 𝑣))(𝑥(+g‘𝑀)𝑦) ∈ ran (𝑤 ∈ Word 𝐺 ↦ (𝑀 Σg 𝑤)) ↔ ∀𝑣 ∈ Word 𝐺(𝑥(+g‘𝑀)(𝑀 Σg 𝑣)) ∈ ran (𝑤 ∈ Word 𝐺 ↦ (𝑀 Σg 𝑤))) |
| 82 | 75, 81 | bitri 275 |
. . . . . . 7
⊢
(∀𝑦 ∈
ran (𝑤 ∈ Word 𝐺 ↦ (𝑀 Σg 𝑤))(𝑥(+g‘𝑀)𝑦) ∈ ran (𝑤 ∈ Word 𝐺 ↦ (𝑀 Σg 𝑤)) ↔ ∀𝑣 ∈ Word 𝐺(𝑥(+g‘𝑀)(𝑀 Σg 𝑣)) ∈ ran (𝑤 ∈ Word 𝐺 ↦ (𝑀 Σg 𝑤))) |
| 83 | 82 | ralbii 3093 |
. . . . . 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 7438 |
. . . . . . . . . 10
⊢ (𝑥 = (𝑀 Σg 𝑧) → (𝑥(+g‘𝑀)(𝑀 Σg 𝑣)) = ((𝑀 Σg 𝑧)(+g‘𝑀)(𝑀 Σg 𝑣))) |
| 86 | 85 | eleq1d 2826 |
. . . . . . . . 9
⊢ (𝑥 = (𝑀 Σg 𝑧) → ((𝑥(+g‘𝑀)(𝑀 Σg 𝑣)) ∈ ran (𝑤 ∈ Word 𝐺 ↦ (𝑀 Σg 𝑤)) ↔ ((𝑀 Σg 𝑧)(+g‘𝑀)(𝑀 Σg 𝑣)) ∈ ran (𝑤 ∈ Word 𝐺 ↦ (𝑀 Σg 𝑤)))) |
| 87 | 86 | ralbidv 3178 |
. . . . . . . 8
⊢ (𝑥 = (𝑀 Σg 𝑧) → (∀𝑣 ∈ Word 𝐺(𝑥(+g‘𝑀)(𝑀 Σg 𝑣)) ∈ ran (𝑤 ∈ Word 𝐺 ↦ (𝑀 Σg 𝑤)) ↔ ∀𝑣 ∈ Word 𝐺((𝑀 Σg 𝑧)(+g‘𝑀)(𝑀 Σg 𝑣)) ∈ ran (𝑤 ∈ Word 𝐺 ↦ (𝑀 Σg 𝑤)))) |
| 88 | 84, 87 | ralrnmptw 7114 |
. . . . . . 7
⊢
(∀𝑧 ∈
Word 𝐺(𝑀 Σg 𝑧) ∈ V → (∀𝑥 ∈ ran (𝑧 ∈ Word 𝐺 ↦ (𝑀 Σg 𝑧))∀𝑣 ∈ Word 𝐺(𝑥(+g‘𝑀)(𝑀 Σg 𝑣)) ∈ ran (𝑤 ∈ Word 𝐺 ↦ (𝑀 Σg 𝑤)) ↔ ∀𝑧 ∈ Word 𝐺∀𝑣 ∈ Word 𝐺((𝑀 Σg 𝑧)(+g‘𝑀)(𝑀 Σg 𝑣)) ∈ ran (𝑤 ∈ Word 𝐺 ↦ (𝑀 Σg 𝑤)))) |
| 89 | | ovexd 7466 |
. . . . . . 7
⊢ (𝑧 ∈ Word 𝐺 → (𝑀 Σg 𝑧) ∈ V) |
| 90 | 88, 89 | mprg 3067 |
. . . . . 6
⊢
(∀𝑥 ∈
ran (𝑧 ∈ Word 𝐺 ↦ (𝑀 Σg 𝑧))∀𝑣 ∈ Word 𝐺(𝑥(+g‘𝑀)(𝑀 Σg 𝑣)) ∈ ran (𝑤 ∈ Word 𝐺 ↦ (𝑀 Σg 𝑤)) ↔ ∀𝑧 ∈ Word 𝐺∀𝑣 ∈ Word 𝐺((𝑀 Σg 𝑧)(+g‘𝑀)(𝑀 Σg 𝑣)) ∈ ran (𝑤 ∈ Word 𝐺 ↦ (𝑀 Σg 𝑤))) |
| 91 | 71, 83, 90 | 3bitri 297 |
. . . . 5
⊢
(∀𝑥 ∈
ran (𝑤 ∈ Word 𝐺 ↦ (𝑀 Σg 𝑤))∀𝑦 ∈ ran (𝑤 ∈ Word 𝐺 ↦ (𝑀 Σg 𝑤))(𝑥(+g‘𝑀)𝑦) ∈ ran (𝑤 ∈ Word 𝐺 ↦ (𝑀 Σg 𝑤)) ↔ ∀𝑧 ∈ Word 𝐺∀𝑣 ∈ Word 𝐺((𝑀 Σg 𝑧)(+g‘𝑀)(𝑀 Σg 𝑣)) ∈ ran (𝑤 ∈ Word 𝐺 ↦ (𝑀 Σg 𝑤))) |
| 92 | 67, 91 | sylibr 234 |
. . . 4
⊢ ((𝑀 ∈ Mnd ∧ 𝐺 ⊆ 𝐵) → ∀𝑥 ∈ ran (𝑤 ∈ Word 𝐺 ↦ (𝑀 Σg 𝑤))∀𝑦 ∈ ran (𝑤 ∈ Word 𝐺 ↦ (𝑀 Σg 𝑤))(𝑥(+g‘𝑀)𝑦) ∈ ran (𝑤 ∈ Word 𝐺 ↦ (𝑀 Σg 𝑤))) |
| 93 | 1, 37, 56 | issubm 18816 |
. . . . 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 480 |
. . . 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 1343 |
. . 3
⊢ ((𝑀 ∈ Mnd ∧ 𝐺 ⊆ 𝐵) → ran (𝑤 ∈ Word 𝐺 ↦ (𝑀 Σg 𝑤)) ∈ (SubMnd‘𝑀)) |
| 96 | 21 | mrcsscl 17663 |
. . 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 4001 |
1
⊢ ((𝑀 ∈ Mnd ∧ 𝐺 ⊆ 𝐵) → (𝐾‘𝐺) = ran (𝑤 ∈ Word 𝐺 ↦ (𝑀 Σg 𝑤))) |