Step |
Hyp |
Ref |
Expression |
1 |
|
gsumwspan.b |
⊢ 𝐵 = ( Base ‘ 𝑀 ) |
2 |
|
gsumwspan.k |
⊢ 𝐾 = ( mrCls ‘ ( SubMnd ‘ 𝑀 ) ) |
3 |
1
|
submacs |
⊢ ( 𝑀 ∈ Mnd → ( SubMnd ‘ 𝑀 ) ∈ ( ACS ‘ 𝐵 ) ) |
4 |
3
|
acsmred |
⊢ ( 𝑀 ∈ Mnd → ( SubMnd ‘ 𝑀 ) ∈ ( Moore ‘ 𝐵 ) ) |
5 |
4
|
adantr |
⊢ ( ( 𝑀 ∈ Mnd ∧ 𝐺 ⊆ 𝐵 ) → ( SubMnd ‘ 𝑀 ) ∈ ( Moore ‘ 𝐵 ) ) |
6 |
|
simpr |
⊢ ( ( ( 𝑀 ∈ Mnd ∧ 𝐺 ⊆ 𝐵 ) ∧ 𝑥 ∈ 𝐺 ) → 𝑥 ∈ 𝐺 ) |
7 |
6
|
s1cld |
⊢ ( ( ( 𝑀 ∈ Mnd ∧ 𝐺 ⊆ 𝐵 ) ∧ 𝑥 ∈ 𝐺 ) → 〈“ 𝑥 ”〉 ∈ Word 𝐺 ) |
8 |
|
ssel2 |
⊢ ( ( 𝐺 ⊆ 𝐵 ∧ 𝑥 ∈ 𝐺 ) → 𝑥 ∈ 𝐵 ) |
9 |
8
|
adantll |
⊢ ( ( ( 𝑀 ∈ Mnd ∧ 𝐺 ⊆ 𝐵 ) ∧ 𝑥 ∈ 𝐺 ) → 𝑥 ∈ 𝐵 ) |
10 |
1
|
gsumws1 |
⊢ ( 𝑥 ∈ 𝐵 → ( 𝑀 Σg 〈“ 𝑥 ”〉 ) = 𝑥 ) |
11 |
9 10
|
syl |
⊢ ( ( ( 𝑀 ∈ Mnd ∧ 𝐺 ⊆ 𝐵 ) ∧ 𝑥 ∈ 𝐺 ) → ( 𝑀 Σg 〈“ 𝑥 ”〉 ) = 𝑥 ) |
12 |
11
|
eqcomd |
⊢ ( ( ( 𝑀 ∈ Mnd ∧ 𝐺 ⊆ 𝐵 ) ∧ 𝑥 ∈ 𝐺 ) → 𝑥 = ( 𝑀 Σg 〈“ 𝑥 ”〉 ) ) |
13 |
|
oveq2 |
⊢ ( 𝑤 = 〈“ 𝑥 ”〉 → ( 𝑀 Σg 𝑤 ) = ( 𝑀 Σg 〈“ 𝑥 ”〉 ) ) |
14 |
13
|
rspceeqv |
⊢ ( ( 〈“ 𝑥 ”〉 ∈ Word 𝐺 ∧ 𝑥 = ( 𝑀 Σg 〈“ 𝑥 ”〉 ) ) → ∃ 𝑤 ∈ Word 𝐺 𝑥 = ( 𝑀 Σg 𝑤 ) ) |
15 |
7 12 14
|
syl2anc |
⊢ ( ( ( 𝑀 ∈ Mnd ∧ 𝐺 ⊆ 𝐵 ) ∧ 𝑥 ∈ 𝐺 ) → ∃ 𝑤 ∈ Word 𝐺 𝑥 = ( 𝑀 Σg 𝑤 ) ) |
16 |
|
eqid |
⊢ ( 𝑤 ∈ Word 𝐺 ↦ ( 𝑀 Σg 𝑤 ) ) = ( 𝑤 ∈ Word 𝐺 ↦ ( 𝑀 Σg 𝑤 ) ) |
17 |
16
|
elrnmpt |
⊢ ( 𝑥 ∈ V → ( 𝑥 ∈ ran ( 𝑤 ∈ Word 𝐺 ↦ ( 𝑀 Σg 𝑤 ) ) ↔ ∃ 𝑤 ∈ Word 𝐺 𝑥 = ( 𝑀 Σg 𝑤 ) ) ) |
18 |
17
|
elv |
⊢ ( 𝑥 ∈ ran ( 𝑤 ∈ Word 𝐺 ↦ ( 𝑀 Σg 𝑤 ) ) ↔ ∃ 𝑤 ∈ Word 𝐺 𝑥 = ( 𝑀 Σg 𝑤 ) ) |
19 |
15 18
|
sylibr |
⊢ ( ( ( 𝑀 ∈ Mnd ∧ 𝐺 ⊆ 𝐵 ) ∧ 𝑥 ∈ 𝐺 ) → 𝑥 ∈ ran ( 𝑤 ∈ Word 𝐺 ↦ ( 𝑀 Σg 𝑤 ) ) ) |
20 |
19
|
ex |
⊢ ( ( 𝑀 ∈ Mnd ∧ 𝐺 ⊆ 𝐵 ) → ( 𝑥 ∈ 𝐺 → 𝑥 ∈ ran ( 𝑤 ∈ Word 𝐺 ↦ ( 𝑀 Σg 𝑤 ) ) ) ) |
21 |
20
|
ssrdv |
⊢ ( ( 𝑀 ∈ Mnd ∧ 𝐺 ⊆ 𝐵 ) → 𝐺 ⊆ ran ( 𝑤 ∈ Word 𝐺 ↦ ( 𝑀 Σg 𝑤 ) ) ) |
22 |
2
|
mrccl |
⊢ ( ( ( SubMnd ‘ 𝑀 ) ∈ ( Moore ‘ 𝐵 ) ∧ 𝐺 ⊆ 𝐵 ) → ( 𝐾 ‘ 𝐺 ) ∈ ( SubMnd ‘ 𝑀 ) ) |
23 |
4 22
|
sylan |
⊢ ( ( 𝑀 ∈ Mnd ∧ 𝐺 ⊆ 𝐵 ) → ( 𝐾 ‘ 𝐺 ) ∈ ( SubMnd ‘ 𝑀 ) ) |
24 |
2
|
mrcssid |
⊢ ( ( ( SubMnd ‘ 𝑀 ) ∈ ( Moore ‘ 𝐵 ) ∧ 𝐺 ⊆ 𝐵 ) → 𝐺 ⊆ ( 𝐾 ‘ 𝐺 ) ) |
25 |
4 24
|
sylan |
⊢ ( ( 𝑀 ∈ Mnd ∧ 𝐺 ⊆ 𝐵 ) → 𝐺 ⊆ ( 𝐾 ‘ 𝐺 ) ) |
26 |
|
sswrd |
⊢ ( 𝐺 ⊆ ( 𝐾 ‘ 𝐺 ) → Word 𝐺 ⊆ Word ( 𝐾 ‘ 𝐺 ) ) |
27 |
25 26
|
syl |
⊢ ( ( 𝑀 ∈ Mnd ∧ 𝐺 ⊆ 𝐵 ) → Word 𝐺 ⊆ Word ( 𝐾 ‘ 𝐺 ) ) |
28 |
27
|
sselda |
⊢ ( ( ( 𝑀 ∈ Mnd ∧ 𝐺 ⊆ 𝐵 ) ∧ 𝑤 ∈ Word 𝐺 ) → 𝑤 ∈ Word ( 𝐾 ‘ 𝐺 ) ) |
29 |
|
gsumwsubmcl |
⊢ ( ( ( 𝐾 ‘ 𝐺 ) ∈ ( SubMnd ‘ 𝑀 ) ∧ 𝑤 ∈ Word ( 𝐾 ‘ 𝐺 ) ) → ( 𝑀 Σg 𝑤 ) ∈ ( 𝐾 ‘ 𝐺 ) ) |
30 |
23 28 29
|
syl2an2r |
⊢ ( ( ( 𝑀 ∈ Mnd ∧ 𝐺 ⊆ 𝐵 ) ∧ 𝑤 ∈ Word 𝐺 ) → ( 𝑀 Σg 𝑤 ) ∈ ( 𝐾 ‘ 𝐺 ) ) |
31 |
30
|
fmpttd |
⊢ ( ( 𝑀 ∈ Mnd ∧ 𝐺 ⊆ 𝐵 ) → ( 𝑤 ∈ Word 𝐺 ↦ ( 𝑀 Σg 𝑤 ) ) : Word 𝐺 ⟶ ( 𝐾 ‘ 𝐺 ) ) |
32 |
31
|
frnd |
⊢ ( ( 𝑀 ∈ Mnd ∧ 𝐺 ⊆ 𝐵 ) → ran ( 𝑤 ∈ Word 𝐺 ↦ ( 𝑀 Σg 𝑤 ) ) ⊆ ( 𝐾 ‘ 𝐺 ) ) |
33 |
4 2
|
mrcssvd |
⊢ ( 𝑀 ∈ Mnd → ( 𝐾 ‘ 𝐺 ) ⊆ 𝐵 ) |
34 |
33
|
adantr |
⊢ ( ( 𝑀 ∈ Mnd ∧ 𝐺 ⊆ 𝐵 ) → ( 𝐾 ‘ 𝐺 ) ⊆ 𝐵 ) |
35 |
32 34
|
sstrd |
⊢ ( ( 𝑀 ∈ Mnd ∧ 𝐺 ⊆ 𝐵 ) → ran ( 𝑤 ∈ Word 𝐺 ↦ ( 𝑀 Σg 𝑤 ) ) ⊆ 𝐵 ) |
36 |
|
wrd0 |
⊢ ∅ ∈ Word 𝐺 |
37 |
|
eqid |
⊢ ( 0g ‘ 𝑀 ) = ( 0g ‘ 𝑀 ) |
38 |
37
|
gsum0 |
⊢ ( 𝑀 Σg ∅ ) = ( 0g ‘ 𝑀 ) |
39 |
38
|
eqcomi |
⊢ ( 0g ‘ 𝑀 ) = ( 𝑀 Σg ∅ ) |
40 |
39
|
a1i |
⊢ ( ( 𝑀 ∈ Mnd ∧ 𝐺 ⊆ 𝐵 ) → ( 0g ‘ 𝑀 ) = ( 𝑀 Σg ∅ ) ) |
41 |
|
oveq2 |
⊢ ( 𝑤 = ∅ → ( 𝑀 Σg 𝑤 ) = ( 𝑀 Σg ∅ ) ) |
42 |
41
|
rspceeqv |
⊢ ( ( ∅ ∈ Word 𝐺 ∧ ( 0g ‘ 𝑀 ) = ( 𝑀 Σg ∅ ) ) → ∃ 𝑤 ∈ Word 𝐺 ( 0g ‘ 𝑀 ) = ( 𝑀 Σg 𝑤 ) ) |
43 |
36 40 42
|
sylancr |
⊢ ( ( 𝑀 ∈ Mnd ∧ 𝐺 ⊆ 𝐵 ) → ∃ 𝑤 ∈ Word 𝐺 ( 0g ‘ 𝑀 ) = ( 𝑀 Σg 𝑤 ) ) |
44 |
|
fvex |
⊢ ( 0g ‘ 𝑀 ) ∈ V |
45 |
16
|
elrnmpt |
⊢ ( ( 0g ‘ 𝑀 ) ∈ V → ( ( 0g ‘ 𝑀 ) ∈ ran ( 𝑤 ∈ Word 𝐺 ↦ ( 𝑀 Σg 𝑤 ) ) ↔ ∃ 𝑤 ∈ Word 𝐺 ( 0g ‘ 𝑀 ) = ( 𝑀 Σg 𝑤 ) ) ) |
46 |
44 45
|
ax-mp |
⊢ ( ( 0g ‘ 𝑀 ) ∈ ran ( 𝑤 ∈ Word 𝐺 ↦ ( 𝑀 Σg 𝑤 ) ) ↔ ∃ 𝑤 ∈ Word 𝐺 ( 0g ‘ 𝑀 ) = ( 𝑀 Σg 𝑤 ) ) |
47 |
43 46
|
sylibr |
⊢ ( ( 𝑀 ∈ Mnd ∧ 𝐺 ⊆ 𝐵 ) → ( 0g ‘ 𝑀 ) ∈ ran ( 𝑤 ∈ Word 𝐺 ↦ ( 𝑀 Σg 𝑤 ) ) ) |
48 |
|
ccatcl |
⊢ ( ( 𝑧 ∈ Word 𝐺 ∧ 𝑣 ∈ Word 𝐺 ) → ( 𝑧 ++ 𝑣 ) ∈ Word 𝐺 ) |
49 |
|
simpll |
⊢ ( ( ( 𝑀 ∈ Mnd ∧ 𝐺 ⊆ 𝐵 ) ∧ ( 𝑧 ∈ Word 𝐺 ∧ 𝑣 ∈ Word 𝐺 ) ) → 𝑀 ∈ Mnd ) |
50 |
|
sswrd |
⊢ ( 𝐺 ⊆ 𝐵 → Word 𝐺 ⊆ Word 𝐵 ) |
51 |
50
|
ad2antlr |
⊢ ( ( ( 𝑀 ∈ Mnd ∧ 𝐺 ⊆ 𝐵 ) ∧ ( 𝑧 ∈ Word 𝐺 ∧ 𝑣 ∈ Word 𝐺 ) ) → Word 𝐺 ⊆ Word 𝐵 ) |
52 |
|
simprl |
⊢ ( ( ( 𝑀 ∈ Mnd ∧ 𝐺 ⊆ 𝐵 ) ∧ ( 𝑧 ∈ Word 𝐺 ∧ 𝑣 ∈ Word 𝐺 ) ) → 𝑧 ∈ Word 𝐺 ) |
53 |
51 52
|
sseldd |
⊢ ( ( ( 𝑀 ∈ Mnd ∧ 𝐺 ⊆ 𝐵 ) ∧ ( 𝑧 ∈ Word 𝐺 ∧ 𝑣 ∈ Word 𝐺 ) ) → 𝑧 ∈ Word 𝐵 ) |
54 |
|
simprr |
⊢ ( ( ( 𝑀 ∈ Mnd ∧ 𝐺 ⊆ 𝐵 ) ∧ ( 𝑧 ∈ Word 𝐺 ∧ 𝑣 ∈ Word 𝐺 ) ) → 𝑣 ∈ Word 𝐺 ) |
55 |
51 54
|
sseldd |
⊢ ( ( ( 𝑀 ∈ Mnd ∧ 𝐺 ⊆ 𝐵 ) ∧ ( 𝑧 ∈ Word 𝐺 ∧ 𝑣 ∈ Word 𝐺 ) ) → 𝑣 ∈ Word 𝐵 ) |
56 |
|
eqid |
⊢ ( +g ‘ 𝑀 ) = ( +g ‘ 𝑀 ) |
57 |
1 56
|
gsumccat |
⊢ ( ( 𝑀 ∈ Mnd ∧ 𝑧 ∈ Word 𝐵 ∧ 𝑣 ∈ Word 𝐵 ) → ( 𝑀 Σg ( 𝑧 ++ 𝑣 ) ) = ( ( 𝑀 Σg 𝑧 ) ( +g ‘ 𝑀 ) ( 𝑀 Σg 𝑣 ) ) ) |
58 |
49 53 55 57
|
syl3anc |
⊢ ( ( ( 𝑀 ∈ Mnd ∧ 𝐺 ⊆ 𝐵 ) ∧ ( 𝑧 ∈ Word 𝐺 ∧ 𝑣 ∈ Word 𝐺 ) ) → ( 𝑀 Σg ( 𝑧 ++ 𝑣 ) ) = ( ( 𝑀 Σg 𝑧 ) ( +g ‘ 𝑀 ) ( 𝑀 Σg 𝑣 ) ) ) |
59 |
58
|
eqcomd |
⊢ ( ( ( 𝑀 ∈ Mnd ∧ 𝐺 ⊆ 𝐵 ) ∧ ( 𝑧 ∈ Word 𝐺 ∧ 𝑣 ∈ Word 𝐺 ) ) → ( ( 𝑀 Σg 𝑧 ) ( +g ‘ 𝑀 ) ( 𝑀 Σg 𝑣 ) ) = ( 𝑀 Σg ( 𝑧 ++ 𝑣 ) ) ) |
60 |
|
oveq2 |
⊢ ( 𝑤 = ( 𝑧 ++ 𝑣 ) → ( 𝑀 Σg 𝑤 ) = ( 𝑀 Σg ( 𝑧 ++ 𝑣 ) ) ) |
61 |
60
|
rspceeqv |
⊢ ( ( ( 𝑧 ++ 𝑣 ) ∈ Word 𝐺 ∧ ( ( 𝑀 Σg 𝑧 ) ( +g ‘ 𝑀 ) ( 𝑀 Σg 𝑣 ) ) = ( 𝑀 Σg ( 𝑧 ++ 𝑣 ) ) ) → ∃ 𝑤 ∈ Word 𝐺 ( ( 𝑀 Σg 𝑧 ) ( +g ‘ 𝑀 ) ( 𝑀 Σg 𝑣 ) ) = ( 𝑀 Σg 𝑤 ) ) |
62 |
48 59 61
|
syl2an2 |
⊢ ( ( ( 𝑀 ∈ Mnd ∧ 𝐺 ⊆ 𝐵 ) ∧ ( 𝑧 ∈ Word 𝐺 ∧ 𝑣 ∈ Word 𝐺 ) ) → ∃ 𝑤 ∈ Word 𝐺 ( ( 𝑀 Σg 𝑧 ) ( +g ‘ 𝑀 ) ( 𝑀 Σg 𝑣 ) ) = ( 𝑀 Σg 𝑤 ) ) |
63 |
|
ovex |
⊢ ( ( 𝑀 Σg 𝑧 ) ( +g ‘ 𝑀 ) ( 𝑀 Σg 𝑣 ) ) ∈ V |
64 |
16
|
elrnmpt |
⊢ ( ( ( 𝑀 Σg 𝑧 ) ( +g ‘ 𝑀 ) ( 𝑀 Σg 𝑣 ) ) ∈ V → ( ( ( 𝑀 Σg 𝑧 ) ( +g ‘ 𝑀 ) ( 𝑀 Σg 𝑣 ) ) ∈ ran ( 𝑤 ∈ Word 𝐺 ↦ ( 𝑀 Σg 𝑤 ) ) ↔ ∃ 𝑤 ∈ Word 𝐺 ( ( 𝑀 Σg 𝑧 ) ( +g ‘ 𝑀 ) ( 𝑀 Σg 𝑣 ) ) = ( 𝑀 Σg 𝑤 ) ) ) |
65 |
63 64
|
ax-mp |
⊢ ( ( ( 𝑀 Σg 𝑧 ) ( +g ‘ 𝑀 ) ( 𝑀 Σg 𝑣 ) ) ∈ ran ( 𝑤 ∈ Word 𝐺 ↦ ( 𝑀 Σg 𝑤 ) ) ↔ ∃ 𝑤 ∈ Word 𝐺 ( ( 𝑀 Σg 𝑧 ) ( +g ‘ 𝑀 ) ( 𝑀 Σg 𝑣 ) ) = ( 𝑀 Σg 𝑤 ) ) |
66 |
62 65
|
sylibr |
⊢ ( ( ( 𝑀 ∈ Mnd ∧ 𝐺 ⊆ 𝐵 ) ∧ ( 𝑧 ∈ Word 𝐺 ∧ 𝑣 ∈ Word 𝐺 ) ) → ( ( 𝑀 Σg 𝑧 ) ( +g ‘ 𝑀 ) ( 𝑀 Σg 𝑣 ) ) ∈ ran ( 𝑤 ∈ Word 𝐺 ↦ ( 𝑀 Σg 𝑤 ) ) ) |
67 |
66
|
ralrimivva |
⊢ ( ( 𝑀 ∈ Mnd ∧ 𝐺 ⊆ 𝐵 ) → ∀ 𝑧 ∈ Word 𝐺 ∀ 𝑣 ∈ Word 𝐺 ( ( 𝑀 Σg 𝑧 ) ( +g ‘ 𝑀 ) ( 𝑀 Σg 𝑣 ) ) ∈ ran ( 𝑤 ∈ Word 𝐺 ↦ ( 𝑀 Σg 𝑤 ) ) ) |
68 |
|
oveq2 |
⊢ ( 𝑤 = 𝑧 → ( 𝑀 Σg 𝑤 ) = ( 𝑀 Σg 𝑧 ) ) |
69 |
68
|
cbvmptv |
⊢ ( 𝑤 ∈ Word 𝐺 ↦ ( 𝑀 Σg 𝑤 ) ) = ( 𝑧 ∈ Word 𝐺 ↦ ( 𝑀 Σg 𝑧 ) ) |
70 |
69
|
rneqi |
⊢ ran ( 𝑤 ∈ Word 𝐺 ↦ ( 𝑀 Σg 𝑤 ) ) = ran ( 𝑧 ∈ Word 𝐺 ↦ ( 𝑀 Σg 𝑧 ) ) |
71 |
70
|
raleqi |
⊢ ( ∀ 𝑥 ∈ ran ( 𝑤 ∈ Word 𝐺 ↦ ( 𝑀 Σg 𝑤 ) ) ∀ 𝑦 ∈ ran ( 𝑤 ∈ Word 𝐺 ↦ ( 𝑀 Σg 𝑤 ) ) ( 𝑥 ( +g ‘ 𝑀 ) 𝑦 ) ∈ ran ( 𝑤 ∈ Word 𝐺 ↦ ( 𝑀 Σg 𝑤 ) ) ↔ ∀ 𝑥 ∈ ran ( 𝑧 ∈ Word 𝐺 ↦ ( 𝑀 Σg 𝑧 ) ) ∀ 𝑦 ∈ ran ( 𝑤 ∈ Word 𝐺 ↦ ( 𝑀 Σg 𝑤 ) ) ( 𝑥 ( +g ‘ 𝑀 ) 𝑦 ) ∈ ran ( 𝑤 ∈ Word 𝐺 ↦ ( 𝑀 Σg 𝑤 ) ) ) |
72 |
|
oveq2 |
⊢ ( 𝑤 = 𝑣 → ( 𝑀 Σg 𝑤 ) = ( 𝑀 Σg 𝑣 ) ) |
73 |
72
|
cbvmptv |
⊢ ( 𝑤 ∈ Word 𝐺 ↦ ( 𝑀 Σg 𝑤 ) ) = ( 𝑣 ∈ Word 𝐺 ↦ ( 𝑀 Σg 𝑣 ) ) |
74 |
73
|
rneqi |
⊢ ran ( 𝑤 ∈ Word 𝐺 ↦ ( 𝑀 Σg 𝑤 ) ) = ran ( 𝑣 ∈ Word 𝐺 ↦ ( 𝑀 Σg 𝑣 ) ) |
75 |
74
|
raleqi |
⊢ ( ∀ 𝑦 ∈ ran ( 𝑤 ∈ Word 𝐺 ↦ ( 𝑀 Σg 𝑤 ) ) ( 𝑥 ( +g ‘ 𝑀 ) 𝑦 ) ∈ ran ( 𝑤 ∈ Word 𝐺 ↦ ( 𝑀 Σg 𝑤 ) ) ↔ ∀ 𝑦 ∈ ran ( 𝑣 ∈ Word 𝐺 ↦ ( 𝑀 Σg 𝑣 ) ) ( 𝑥 ( +g ‘ 𝑀 ) 𝑦 ) ∈ ran ( 𝑤 ∈ Word 𝐺 ↦ ( 𝑀 Σg 𝑤 ) ) ) |
76 |
|
eqid |
⊢ ( 𝑣 ∈ Word 𝐺 ↦ ( 𝑀 Σg 𝑣 ) ) = ( 𝑣 ∈ Word 𝐺 ↦ ( 𝑀 Σg 𝑣 ) ) |
77 |
|
oveq2 |
⊢ ( 𝑦 = ( 𝑀 Σg 𝑣 ) → ( 𝑥 ( +g ‘ 𝑀 ) 𝑦 ) = ( 𝑥 ( +g ‘ 𝑀 ) ( 𝑀 Σg 𝑣 ) ) ) |
78 |
77
|
eleq1d |
⊢ ( 𝑦 = ( 𝑀 Σg 𝑣 ) → ( ( 𝑥 ( +g ‘ 𝑀 ) 𝑦 ) ∈ ran ( 𝑤 ∈ Word 𝐺 ↦ ( 𝑀 Σg 𝑤 ) ) ↔ ( 𝑥 ( +g ‘ 𝑀 ) ( 𝑀 Σg 𝑣 ) ) ∈ ran ( 𝑤 ∈ Word 𝐺 ↦ ( 𝑀 Σg 𝑤 ) ) ) ) |
79 |
76 78
|
ralrnmptw |
⊢ ( ∀ 𝑣 ∈ Word 𝐺 ( 𝑀 Σg 𝑣 ) ∈ V → ( ∀ 𝑦 ∈ ran ( 𝑣 ∈ Word 𝐺 ↦ ( 𝑀 Σg 𝑣 ) ) ( 𝑥 ( +g ‘ 𝑀 ) 𝑦 ) ∈ ran ( 𝑤 ∈ Word 𝐺 ↦ ( 𝑀 Σg 𝑤 ) ) ↔ ∀ 𝑣 ∈ Word 𝐺 ( 𝑥 ( +g ‘ 𝑀 ) ( 𝑀 Σg 𝑣 ) ) ∈ ran ( 𝑤 ∈ Word 𝐺 ↦ ( 𝑀 Σg 𝑤 ) ) ) ) |
80 |
|
ovexd |
⊢ ( 𝑣 ∈ Word 𝐺 → ( 𝑀 Σg 𝑣 ) ∈ V ) |
81 |
79 80
|
mprg |
⊢ ( ∀ 𝑦 ∈ ran ( 𝑣 ∈ Word 𝐺 ↦ ( 𝑀 Σg 𝑣 ) ) ( 𝑥 ( +g ‘ 𝑀 ) 𝑦 ) ∈ ran ( 𝑤 ∈ Word 𝐺 ↦ ( 𝑀 Σg 𝑤 ) ) ↔ ∀ 𝑣 ∈ Word 𝐺 ( 𝑥 ( +g ‘ 𝑀 ) ( 𝑀 Σg 𝑣 ) ) ∈ ran ( 𝑤 ∈ Word 𝐺 ↦ ( 𝑀 Σg 𝑤 ) ) ) |
82 |
75 81
|
bitri |
⊢ ( ∀ 𝑦 ∈ ran ( 𝑤 ∈ Word 𝐺 ↦ ( 𝑀 Σg 𝑤 ) ) ( 𝑥 ( +g ‘ 𝑀 ) 𝑦 ) ∈ ran ( 𝑤 ∈ Word 𝐺 ↦ ( 𝑀 Σg 𝑤 ) ) ↔ ∀ 𝑣 ∈ Word 𝐺 ( 𝑥 ( +g ‘ 𝑀 ) ( 𝑀 Σg 𝑣 ) ) ∈ ran ( 𝑤 ∈ Word 𝐺 ↦ ( 𝑀 Σg 𝑤 ) ) ) |
83 |
82
|
ralbii |
⊢ ( ∀ 𝑥 ∈ ran ( 𝑧 ∈ Word 𝐺 ↦ ( 𝑀 Σg 𝑧 ) ) ∀ 𝑦 ∈ ran ( 𝑤 ∈ Word 𝐺 ↦ ( 𝑀 Σg 𝑤 ) ) ( 𝑥 ( +g ‘ 𝑀 ) 𝑦 ) ∈ ran ( 𝑤 ∈ Word 𝐺 ↦ ( 𝑀 Σg 𝑤 ) ) ↔ ∀ 𝑥 ∈ ran ( 𝑧 ∈ Word 𝐺 ↦ ( 𝑀 Σg 𝑧 ) ) ∀ 𝑣 ∈ Word 𝐺 ( 𝑥 ( +g ‘ 𝑀 ) ( 𝑀 Σg 𝑣 ) ) ∈ ran ( 𝑤 ∈ Word 𝐺 ↦ ( 𝑀 Σg 𝑤 ) ) ) |
84 |
|
eqid |
⊢ ( 𝑧 ∈ Word 𝐺 ↦ ( 𝑀 Σg 𝑧 ) ) = ( 𝑧 ∈ Word 𝐺 ↦ ( 𝑀 Σg 𝑧 ) ) |
85 |
|
oveq1 |
⊢ ( 𝑥 = ( 𝑀 Σg 𝑧 ) → ( 𝑥 ( +g ‘ 𝑀 ) ( 𝑀 Σg 𝑣 ) ) = ( ( 𝑀 Σg 𝑧 ) ( +g ‘ 𝑀 ) ( 𝑀 Σg 𝑣 ) ) ) |
86 |
85
|
eleq1d |
⊢ ( 𝑥 = ( 𝑀 Σg 𝑧 ) → ( ( 𝑥 ( +g ‘ 𝑀 ) ( 𝑀 Σg 𝑣 ) ) ∈ ran ( 𝑤 ∈ Word 𝐺 ↦ ( 𝑀 Σg 𝑤 ) ) ↔ ( ( 𝑀 Σg 𝑧 ) ( +g ‘ 𝑀 ) ( 𝑀 Σg 𝑣 ) ) ∈ ran ( 𝑤 ∈ Word 𝐺 ↦ ( 𝑀 Σg 𝑤 ) ) ) ) |
87 |
86
|
ralbidv |
⊢ ( 𝑥 = ( 𝑀 Σg 𝑧 ) → ( ∀ 𝑣 ∈ Word 𝐺 ( 𝑥 ( +g ‘ 𝑀 ) ( 𝑀 Σg 𝑣 ) ) ∈ ran ( 𝑤 ∈ Word 𝐺 ↦ ( 𝑀 Σg 𝑤 ) ) ↔ ∀ 𝑣 ∈ Word 𝐺 ( ( 𝑀 Σg 𝑧 ) ( +g ‘ 𝑀 ) ( 𝑀 Σg 𝑣 ) ) ∈ ran ( 𝑤 ∈ Word 𝐺 ↦ ( 𝑀 Σg 𝑤 ) ) ) ) |
88 |
84 87
|
ralrnmptw |
⊢ ( ∀ 𝑧 ∈ Word 𝐺 ( 𝑀 Σg 𝑧 ) ∈ V → ( ∀ 𝑥 ∈ ran ( 𝑧 ∈ Word 𝐺 ↦ ( 𝑀 Σg 𝑧 ) ) ∀ 𝑣 ∈ Word 𝐺 ( 𝑥 ( +g ‘ 𝑀 ) ( 𝑀 Σg 𝑣 ) ) ∈ ran ( 𝑤 ∈ Word 𝐺 ↦ ( 𝑀 Σg 𝑤 ) ) ↔ ∀ 𝑧 ∈ Word 𝐺 ∀ 𝑣 ∈ Word 𝐺 ( ( 𝑀 Σg 𝑧 ) ( +g ‘ 𝑀 ) ( 𝑀 Σg 𝑣 ) ) ∈ ran ( 𝑤 ∈ Word 𝐺 ↦ ( 𝑀 Σg 𝑤 ) ) ) ) |
89 |
|
ovexd |
⊢ ( 𝑧 ∈ Word 𝐺 → ( 𝑀 Σg 𝑧 ) ∈ V ) |
90 |
88 89
|
mprg |
⊢ ( ∀ 𝑥 ∈ ran ( 𝑧 ∈ Word 𝐺 ↦ ( 𝑀 Σg 𝑧 ) ) ∀ 𝑣 ∈ Word 𝐺 ( 𝑥 ( +g ‘ 𝑀 ) ( 𝑀 Σg 𝑣 ) ) ∈ ran ( 𝑤 ∈ Word 𝐺 ↦ ( 𝑀 Σg 𝑤 ) ) ↔ ∀ 𝑧 ∈ Word 𝐺 ∀ 𝑣 ∈ Word 𝐺 ( ( 𝑀 Σg 𝑧 ) ( +g ‘ 𝑀 ) ( 𝑀 Σg 𝑣 ) ) ∈ ran ( 𝑤 ∈ Word 𝐺 ↦ ( 𝑀 Σg 𝑤 ) ) ) |
91 |
71 83 90
|
3bitri |
⊢ ( ∀ 𝑥 ∈ ran ( 𝑤 ∈ Word 𝐺 ↦ ( 𝑀 Σg 𝑤 ) ) ∀ 𝑦 ∈ ran ( 𝑤 ∈ Word 𝐺 ↦ ( 𝑀 Σg 𝑤 ) ) ( 𝑥 ( +g ‘ 𝑀 ) 𝑦 ) ∈ ran ( 𝑤 ∈ Word 𝐺 ↦ ( 𝑀 Σg 𝑤 ) ) ↔ ∀ 𝑧 ∈ Word 𝐺 ∀ 𝑣 ∈ Word 𝐺 ( ( 𝑀 Σg 𝑧 ) ( +g ‘ 𝑀 ) ( 𝑀 Σg 𝑣 ) ) ∈ ran ( 𝑤 ∈ Word 𝐺 ↦ ( 𝑀 Σg 𝑤 ) ) ) |
92 |
67 91
|
sylibr |
⊢ ( ( 𝑀 ∈ Mnd ∧ 𝐺 ⊆ 𝐵 ) → ∀ 𝑥 ∈ ran ( 𝑤 ∈ Word 𝐺 ↦ ( 𝑀 Σg 𝑤 ) ) ∀ 𝑦 ∈ ran ( 𝑤 ∈ Word 𝐺 ↦ ( 𝑀 Σg 𝑤 ) ) ( 𝑥 ( +g ‘ 𝑀 ) 𝑦 ) ∈ ran ( 𝑤 ∈ Word 𝐺 ↦ ( 𝑀 Σg 𝑤 ) ) ) |
93 |
1 37 56
|
issubm |
⊢ ( 𝑀 ∈ 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 |
⊢ ( ( 𝑀 ∈ 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 |
⊢ ( ( 𝑀 ∈ Mnd ∧ 𝐺 ⊆ 𝐵 ) → ran ( 𝑤 ∈ Word 𝐺 ↦ ( 𝑀 Σg 𝑤 ) ) ∈ ( SubMnd ‘ 𝑀 ) ) |
96 |
2
|
mrcsscl |
⊢ ( ( ( SubMnd ‘ 𝑀 ) ∈ ( Moore ‘ 𝐵 ) ∧ 𝐺 ⊆ ran ( 𝑤 ∈ Word 𝐺 ↦ ( 𝑀 Σg 𝑤 ) ) ∧ ran ( 𝑤 ∈ Word 𝐺 ↦ ( 𝑀 Σg 𝑤 ) ) ∈ ( SubMnd ‘ 𝑀 ) ) → ( 𝐾 ‘ 𝐺 ) ⊆ ran ( 𝑤 ∈ Word 𝐺 ↦ ( 𝑀 Σg 𝑤 ) ) ) |
97 |
5 21 95 96
|
syl3anc |
⊢ ( ( 𝑀 ∈ Mnd ∧ 𝐺 ⊆ 𝐵 ) → ( 𝐾 ‘ 𝐺 ) ⊆ ran ( 𝑤 ∈ Word 𝐺 ↦ ( 𝑀 Σg 𝑤 ) ) ) |
98 |
97 32
|
eqssd |
⊢ ( ( 𝑀 ∈ Mnd ∧ 𝐺 ⊆ 𝐵 ) → ( 𝐾 ‘ 𝐺 ) = ran ( 𝑤 ∈ Word 𝐺 ↦ ( 𝑀 Σg 𝑤 ) ) ) |