Step | Hyp | Ref
| Expression |
1 | | frgp0.m |
. . 3
⊢ 𝐺 = (freeGrp‘𝐼) |
2 | | eqid 2610 |
. . 3
⊢
(freeMnd‘(𝐼
× 2𝑜)) = (freeMnd‘(𝐼 ×
2𝑜)) |
3 | | frgp0.r |
. . 3
⊢ ∼ = (
~FG ‘𝐼) |
4 | 1, 2, 3 | frgpval 17994 |
. 2
⊢ (𝐼 ∈ 𝑉 → 𝐺 = ((freeMnd‘(𝐼 × 2𝑜))
/s ∼ )) |
5 | | 2on 7455 |
. . . . 5
⊢
2𝑜 ∈ On |
6 | | xpexg 6858 |
. . . . 5
⊢ ((𝐼 ∈ 𝑉 ∧ 2𝑜 ∈ On)
→ (𝐼 ×
2𝑜) ∈ V) |
7 | 5, 6 | mpan2 703 |
. . . 4
⊢ (𝐼 ∈ 𝑉 → (𝐼 × 2𝑜) ∈
V) |
8 | | eqid 2610 |
. . . . 5
⊢
(Base‘(freeMnd‘(𝐼 × 2𝑜))) =
(Base‘(freeMnd‘(𝐼 ×
2𝑜))) |
9 | 2, 8 | frmdbas 17212 |
. . . 4
⊢ ((𝐼 × 2𝑜)
∈ V → (Base‘(freeMnd‘(𝐼 × 2𝑜))) = Word
(𝐼 ×
2𝑜)) |
10 | 7, 9 | syl 17 |
. . 3
⊢ (𝐼 ∈ 𝑉 → (Base‘(freeMnd‘(𝐼 ×
2𝑜))) = Word (𝐼 ×
2𝑜)) |
11 | 10 | eqcomd 2616 |
. 2
⊢ (𝐼 ∈ 𝑉 → Word (𝐼 × 2𝑜) =
(Base‘(freeMnd‘(𝐼 ×
2𝑜)))) |
12 | | eqidd 2611 |
. 2
⊢ (𝐼 ∈ 𝑉 →
(+g‘(freeMnd‘(𝐼 × 2𝑜))) =
(+g‘(freeMnd‘(𝐼 ×
2𝑜)))) |
13 | | eqid 2610 |
. . . 4
⊢ ( I
‘Word (𝐼 ×
2𝑜)) = ( I ‘Word (𝐼 ×
2𝑜)) |
14 | 13, 3 | efger 17954 |
. . 3
⊢ ∼ Er ( I
‘Word (𝐼 ×
2𝑜)) |
15 | | wrdexg 13170 |
. . . . 5
⊢ ((𝐼 × 2𝑜)
∈ V → Word (𝐼
× 2𝑜) ∈ V) |
16 | | fvi 6165 |
. . . . 5
⊢ (Word
(𝐼 ×
2𝑜) ∈ V → ( I ‘Word (𝐼 × 2𝑜)) = Word
(𝐼 ×
2𝑜)) |
17 | 7, 15, 16 | 3syl 18 |
. . . 4
⊢ (𝐼 ∈ 𝑉 → ( I ‘Word (𝐼 × 2𝑜)) = Word
(𝐼 ×
2𝑜)) |
18 | | ereq2 7637 |
. . . 4
⊢ (( I
‘Word (𝐼 ×
2𝑜)) = Word (𝐼 × 2𝑜) → (
∼
Er ( I ‘Word (𝐼
× 2𝑜)) ↔ ∼ Er Word (𝐼 ×
2𝑜))) |
19 | 17, 18 | syl 17 |
. . 3
⊢ (𝐼 ∈ 𝑉 → ( ∼ Er ( I ‘Word
(𝐼 ×
2𝑜)) ↔ ∼ Er Word (𝐼 ×
2𝑜))) |
20 | 14, 19 | mpbii 222 |
. 2
⊢ (𝐼 ∈ 𝑉 → ∼ Er Word (𝐼 ×
2𝑜)) |
21 | | fvex 6113 |
. . 3
⊢
(freeMnd‘(𝐼
× 2𝑜)) ∈ V |
22 | 21 | a1i 11 |
. 2
⊢ (𝐼 ∈ 𝑉 → (freeMnd‘(𝐼 × 2𝑜)) ∈
V) |
23 | | eqid 2610 |
. . . 4
⊢
(+g‘(freeMnd‘(𝐼 × 2𝑜))) =
(+g‘(freeMnd‘(𝐼 ×
2𝑜))) |
24 | 1, 2, 3, 23 | frgpcpbl 17995 |
. . 3
⊢ ((𝑎 ∼ 𝑏 ∧ 𝑐 ∼ 𝑑) → (𝑎(+g‘(freeMnd‘(𝐼 ×
2𝑜)))𝑐)
∼
(𝑏(+g‘(freeMnd‘(𝐼 ×
2𝑜)))𝑑)) |
25 | 24 | a1i 11 |
. 2
⊢ (𝐼 ∈ 𝑉 → ((𝑎 ∼ 𝑏 ∧ 𝑐 ∼ 𝑑) → (𝑎(+g‘(freeMnd‘(𝐼 ×
2𝑜)))𝑐)
∼
(𝑏(+g‘(freeMnd‘(𝐼 ×
2𝑜)))𝑑))) |
26 | 2 | frmdmnd 17219 |
. . . . . 6
⊢ ((𝐼 × 2𝑜)
∈ V → (freeMnd‘(𝐼 × 2𝑜)) ∈
Mnd) |
27 | 7, 26 | syl 17 |
. . . . 5
⊢ (𝐼 ∈ 𝑉 → (freeMnd‘(𝐼 × 2𝑜)) ∈
Mnd) |
28 | 27 | 3ad2ant1 1075 |
. . . 4
⊢ ((𝐼 ∈ 𝑉 ∧ 𝑥 ∈ Word (𝐼 × 2𝑜) ∧ 𝑦 ∈ Word (𝐼 × 2𝑜)) →
(freeMnd‘(𝐼 ×
2𝑜)) ∈ Mnd) |
29 | | simp2 1055 |
. . . . 5
⊢ ((𝐼 ∈ 𝑉 ∧ 𝑥 ∈ Word (𝐼 × 2𝑜) ∧ 𝑦 ∈ Word (𝐼 × 2𝑜)) →
𝑥 ∈ Word (𝐼 ×
2𝑜)) |
30 | 11 | 3ad2ant1 1075 |
. . . . 5
⊢ ((𝐼 ∈ 𝑉 ∧ 𝑥 ∈ Word (𝐼 × 2𝑜) ∧ 𝑦 ∈ Word (𝐼 × 2𝑜)) → Word
(𝐼 ×
2𝑜) = (Base‘(freeMnd‘(𝐼 ×
2𝑜)))) |
31 | 29, 30 | eleqtrd 2690 |
. . . 4
⊢ ((𝐼 ∈ 𝑉 ∧ 𝑥 ∈ Word (𝐼 × 2𝑜) ∧ 𝑦 ∈ Word (𝐼 × 2𝑜)) →
𝑥 ∈
(Base‘(freeMnd‘(𝐼 ×
2𝑜)))) |
32 | | simp3 1056 |
. . . . 5
⊢ ((𝐼 ∈ 𝑉 ∧ 𝑥 ∈ Word (𝐼 × 2𝑜) ∧ 𝑦 ∈ Word (𝐼 × 2𝑜)) →
𝑦 ∈ Word (𝐼 ×
2𝑜)) |
33 | 32, 30 | eleqtrd 2690 |
. . . 4
⊢ ((𝐼 ∈ 𝑉 ∧ 𝑥 ∈ Word (𝐼 × 2𝑜) ∧ 𝑦 ∈ Word (𝐼 × 2𝑜)) →
𝑦 ∈
(Base‘(freeMnd‘(𝐼 ×
2𝑜)))) |
34 | 8, 23 | mndcl 17124 |
. . . 4
⊢
(((freeMnd‘(𝐼
× 2𝑜)) ∈ Mnd ∧ 𝑥 ∈ (Base‘(freeMnd‘(𝐼 ×
2𝑜))) ∧ 𝑦 ∈ (Base‘(freeMnd‘(𝐼 ×
2𝑜)))) → (𝑥(+g‘(freeMnd‘(𝐼 ×
2𝑜)))𝑦)
∈ (Base‘(freeMnd‘(𝐼 ×
2𝑜)))) |
35 | 28, 31, 33, 34 | syl3anc 1318 |
. . 3
⊢ ((𝐼 ∈ 𝑉 ∧ 𝑥 ∈ Word (𝐼 × 2𝑜) ∧ 𝑦 ∈ Word (𝐼 × 2𝑜)) →
(𝑥(+g‘(freeMnd‘(𝐼 ×
2𝑜)))𝑦)
∈ (Base‘(freeMnd‘(𝐼 ×
2𝑜)))) |
36 | 35, 30 | eleqtrrd 2691 |
. 2
⊢ ((𝐼 ∈ 𝑉 ∧ 𝑥 ∈ Word (𝐼 × 2𝑜) ∧ 𝑦 ∈ Word (𝐼 × 2𝑜)) →
(𝑥(+g‘(freeMnd‘(𝐼 ×
2𝑜)))𝑦)
∈ Word (𝐼 ×
2𝑜)) |
37 | 20 | adantr 480 |
. . . 4
⊢ ((𝐼 ∈ 𝑉 ∧ (𝑥 ∈ Word (𝐼 × 2𝑜) ∧ 𝑦 ∈ Word (𝐼 × 2𝑜) ∧ 𝑧 ∈ Word (𝐼 × 2𝑜))) →
∼
Er Word (𝐼 ×
2𝑜)) |
38 | 27 | adantr 480 |
. . . . . 6
⊢ ((𝐼 ∈ 𝑉 ∧ (𝑥 ∈ Word (𝐼 × 2𝑜) ∧ 𝑦 ∈ Word (𝐼 × 2𝑜) ∧ 𝑧 ∈ Word (𝐼 × 2𝑜))) →
(freeMnd‘(𝐼 ×
2𝑜)) ∈ Mnd) |
39 | 35 | 3adant3r3 1268 |
. . . . . 6
⊢ ((𝐼 ∈ 𝑉 ∧ (𝑥 ∈ Word (𝐼 × 2𝑜) ∧ 𝑦 ∈ Word (𝐼 × 2𝑜) ∧ 𝑧 ∈ Word (𝐼 × 2𝑜))) →
(𝑥(+g‘(freeMnd‘(𝐼 ×
2𝑜)))𝑦)
∈ (Base‘(freeMnd‘(𝐼 ×
2𝑜)))) |
40 | | simpr3 1062 |
. . . . . . 7
⊢ ((𝐼 ∈ 𝑉 ∧ (𝑥 ∈ Word (𝐼 × 2𝑜) ∧ 𝑦 ∈ Word (𝐼 × 2𝑜) ∧ 𝑧 ∈ Word (𝐼 × 2𝑜))) →
𝑧 ∈ Word (𝐼 ×
2𝑜)) |
41 | 11 | adantr 480 |
. . . . . . 7
⊢ ((𝐼 ∈ 𝑉 ∧ (𝑥 ∈ Word (𝐼 × 2𝑜) ∧ 𝑦 ∈ Word (𝐼 × 2𝑜) ∧ 𝑧 ∈ Word (𝐼 × 2𝑜))) →
Word (𝐼 ×
2𝑜) = (Base‘(freeMnd‘(𝐼 ×
2𝑜)))) |
42 | 40, 41 | eleqtrd 2690 |
. . . . . 6
⊢ ((𝐼 ∈ 𝑉 ∧ (𝑥 ∈ Word (𝐼 × 2𝑜) ∧ 𝑦 ∈ Word (𝐼 × 2𝑜) ∧ 𝑧 ∈ Word (𝐼 × 2𝑜))) →
𝑧 ∈
(Base‘(freeMnd‘(𝐼 ×
2𝑜)))) |
43 | 8, 23 | mndcl 17124 |
. . . . . 6
⊢
(((freeMnd‘(𝐼
× 2𝑜)) ∈ Mnd ∧ (𝑥(+g‘(freeMnd‘(𝐼 ×
2𝑜)))𝑦)
∈ (Base‘(freeMnd‘(𝐼 × 2𝑜))) ∧
𝑧 ∈
(Base‘(freeMnd‘(𝐼 × 2𝑜)))) →
((𝑥(+g‘(freeMnd‘(𝐼 ×
2𝑜)))𝑦)(+g‘(freeMnd‘(𝐼 ×
2𝑜)))𝑧)
∈ (Base‘(freeMnd‘(𝐼 ×
2𝑜)))) |
44 | 38, 39, 42, 43 | syl3anc 1318 |
. . . . 5
⊢ ((𝐼 ∈ 𝑉 ∧ (𝑥 ∈ Word (𝐼 × 2𝑜) ∧ 𝑦 ∈ Word (𝐼 × 2𝑜) ∧ 𝑧 ∈ Word (𝐼 × 2𝑜))) →
((𝑥(+g‘(freeMnd‘(𝐼 ×
2𝑜)))𝑦)(+g‘(freeMnd‘(𝐼 ×
2𝑜)))𝑧)
∈ (Base‘(freeMnd‘(𝐼 ×
2𝑜)))) |
45 | 44, 41 | eleqtrrd 2691 |
. . . 4
⊢ ((𝐼 ∈ 𝑉 ∧ (𝑥 ∈ Word (𝐼 × 2𝑜) ∧ 𝑦 ∈ Word (𝐼 × 2𝑜) ∧ 𝑧 ∈ Word (𝐼 × 2𝑜))) →
((𝑥(+g‘(freeMnd‘(𝐼 ×
2𝑜)))𝑦)(+g‘(freeMnd‘(𝐼 ×
2𝑜)))𝑧)
∈ Word (𝐼 ×
2𝑜)) |
46 | 37, 45 | erref 7649 |
. . 3
⊢ ((𝐼 ∈ 𝑉 ∧ (𝑥 ∈ Word (𝐼 × 2𝑜) ∧ 𝑦 ∈ Word (𝐼 × 2𝑜) ∧ 𝑧 ∈ Word (𝐼 × 2𝑜))) →
((𝑥(+g‘(freeMnd‘(𝐼 ×
2𝑜)))𝑦)(+g‘(freeMnd‘(𝐼 ×
2𝑜)))𝑧)
∼
((𝑥(+g‘(freeMnd‘(𝐼 ×
2𝑜)))𝑦)(+g‘(freeMnd‘(𝐼 ×
2𝑜)))𝑧)) |
47 | 31 | 3adant3r3 1268 |
. . . 4
⊢ ((𝐼 ∈ 𝑉 ∧ (𝑥 ∈ Word (𝐼 × 2𝑜) ∧ 𝑦 ∈ Word (𝐼 × 2𝑜) ∧ 𝑧 ∈ Word (𝐼 × 2𝑜))) →
𝑥 ∈
(Base‘(freeMnd‘(𝐼 ×
2𝑜)))) |
48 | 33 | 3adant3r3 1268 |
. . . 4
⊢ ((𝐼 ∈ 𝑉 ∧ (𝑥 ∈ Word (𝐼 × 2𝑜) ∧ 𝑦 ∈ Word (𝐼 × 2𝑜) ∧ 𝑧 ∈ Word (𝐼 × 2𝑜))) →
𝑦 ∈
(Base‘(freeMnd‘(𝐼 ×
2𝑜)))) |
49 | 8, 23 | mndass 17125 |
. . . 4
⊢
(((freeMnd‘(𝐼
× 2𝑜)) ∈ Mnd ∧ (𝑥 ∈ (Base‘(freeMnd‘(𝐼 ×
2𝑜))) ∧ 𝑦 ∈ (Base‘(freeMnd‘(𝐼 ×
2𝑜))) ∧ 𝑧 ∈ (Base‘(freeMnd‘(𝐼 ×
2𝑜))))) → ((𝑥(+g‘(freeMnd‘(𝐼 ×
2𝑜)))𝑦)(+g‘(freeMnd‘(𝐼 ×
2𝑜)))𝑧)
= (𝑥(+g‘(freeMnd‘(𝐼 ×
2𝑜)))(𝑦(+g‘(freeMnd‘(𝐼 ×
2𝑜)))𝑧))) |
50 | 38, 47, 48, 42, 49 | syl13anc 1320 |
. . 3
⊢ ((𝐼 ∈ 𝑉 ∧ (𝑥 ∈ Word (𝐼 × 2𝑜) ∧ 𝑦 ∈ Word (𝐼 × 2𝑜) ∧ 𝑧 ∈ Word (𝐼 × 2𝑜))) →
((𝑥(+g‘(freeMnd‘(𝐼 ×
2𝑜)))𝑦)(+g‘(freeMnd‘(𝐼 ×
2𝑜)))𝑧)
= (𝑥(+g‘(freeMnd‘(𝐼 ×
2𝑜)))(𝑦(+g‘(freeMnd‘(𝐼 ×
2𝑜)))𝑧))) |
51 | 46, 50 | breqtrd 4609 |
. 2
⊢ ((𝐼 ∈ 𝑉 ∧ (𝑥 ∈ Word (𝐼 × 2𝑜) ∧ 𝑦 ∈ Word (𝐼 × 2𝑜) ∧ 𝑧 ∈ Word (𝐼 × 2𝑜))) →
((𝑥(+g‘(freeMnd‘(𝐼 ×
2𝑜)))𝑦)(+g‘(freeMnd‘(𝐼 ×
2𝑜)))𝑧)
∼
(𝑥(+g‘(freeMnd‘(𝐼 ×
2𝑜)))(𝑦(+g‘(freeMnd‘(𝐼 ×
2𝑜)))𝑧))) |
52 | | wrd0 13185 |
. . 3
⊢ ∅
∈ Word (𝐼 ×
2𝑜) |
53 | 52 | a1i 11 |
. 2
⊢ (𝐼 ∈ 𝑉 → ∅ ∈ Word (𝐼 ×
2𝑜)) |
54 | 52, 11 | syl5eleq 2694 |
. . . . . 6
⊢ (𝐼 ∈ 𝑉 → ∅ ∈
(Base‘(freeMnd‘(𝐼 ×
2𝑜)))) |
55 | 54 | adantr 480 |
. . . . 5
⊢ ((𝐼 ∈ 𝑉 ∧ 𝑥 ∈ Word (𝐼 × 2𝑜)) →
∅ ∈ (Base‘(freeMnd‘(𝐼 ×
2𝑜)))) |
56 | 11 | eleq2d 2673 |
. . . . . 6
⊢ (𝐼 ∈ 𝑉 → (𝑥 ∈ Word (𝐼 × 2𝑜) ↔ 𝑥 ∈
(Base‘(freeMnd‘(𝐼 ×
2𝑜))))) |
57 | 56 | biimpa 500 |
. . . . 5
⊢ ((𝐼 ∈ 𝑉 ∧ 𝑥 ∈ Word (𝐼 × 2𝑜)) →
𝑥 ∈
(Base‘(freeMnd‘(𝐼 ×
2𝑜)))) |
58 | 2, 8, 23 | frmdadd 17215 |
. . . . 5
⊢ ((∅
∈ (Base‘(freeMnd‘(𝐼 × 2𝑜))) ∧
𝑥 ∈
(Base‘(freeMnd‘(𝐼 × 2𝑜)))) →
(∅(+g‘(freeMnd‘(𝐼 × 2𝑜)))𝑥) = (∅ ++ 𝑥)) |
59 | 55, 57, 58 | syl2anc 691 |
. . . 4
⊢ ((𝐼 ∈ 𝑉 ∧ 𝑥 ∈ Word (𝐼 × 2𝑜)) →
(∅(+g‘(freeMnd‘(𝐼 × 2𝑜)))𝑥) = (∅ ++ 𝑥)) |
60 | | ccatlid 13222 |
. . . . 5
⊢ (𝑥 ∈ Word (𝐼 × 2𝑜) →
(∅ ++ 𝑥) = 𝑥) |
61 | 60 | adantl 481 |
. . . 4
⊢ ((𝐼 ∈ 𝑉 ∧ 𝑥 ∈ Word (𝐼 × 2𝑜)) →
(∅ ++ 𝑥) = 𝑥) |
62 | 59, 61 | eqtrd 2644 |
. . 3
⊢ ((𝐼 ∈ 𝑉 ∧ 𝑥 ∈ Word (𝐼 × 2𝑜)) →
(∅(+g‘(freeMnd‘(𝐼 × 2𝑜)))𝑥) = 𝑥) |
63 | 20 | adantr 480 |
. . . 4
⊢ ((𝐼 ∈ 𝑉 ∧ 𝑥 ∈ Word (𝐼 × 2𝑜)) →
∼
Er Word (𝐼 ×
2𝑜)) |
64 | | simpr 476 |
. . . 4
⊢ ((𝐼 ∈ 𝑉 ∧ 𝑥 ∈ Word (𝐼 × 2𝑜)) →
𝑥 ∈ Word (𝐼 ×
2𝑜)) |
65 | 63, 64 | erref 7649 |
. . 3
⊢ ((𝐼 ∈ 𝑉 ∧ 𝑥 ∈ Word (𝐼 × 2𝑜)) →
𝑥 ∼ 𝑥) |
66 | 62, 65 | eqbrtrd 4605 |
. 2
⊢ ((𝐼 ∈ 𝑉 ∧ 𝑥 ∈ Word (𝐼 × 2𝑜)) →
(∅(+g‘(freeMnd‘(𝐼 × 2𝑜)))𝑥) ∼ 𝑥) |
67 | | revcl 13361 |
. . . 4
⊢ (𝑥 ∈ Word (𝐼 × 2𝑜) →
(reverse‘𝑥) ∈
Word (𝐼 ×
2𝑜)) |
68 | 67 | adantl 481 |
. . 3
⊢ ((𝐼 ∈ 𝑉 ∧ 𝑥 ∈ Word (𝐼 × 2𝑜)) →
(reverse‘𝑥) ∈
Word (𝐼 ×
2𝑜)) |
69 | | eqid 2610 |
. . . . 5
⊢ (𝑦 ∈ 𝐼, 𝑧 ∈ 2𝑜 ↦
〈𝑦,
(1𝑜 ∖ 𝑧)〉) = (𝑦 ∈ 𝐼, 𝑧 ∈ 2𝑜 ↦
〈𝑦,
(1𝑜 ∖ 𝑧)〉) |
70 | 69 | efgmf 17949 |
. . . 4
⊢ (𝑦 ∈ 𝐼, 𝑧 ∈ 2𝑜 ↦
〈𝑦,
(1𝑜 ∖ 𝑧)〉):(𝐼 ×
2𝑜)⟶(𝐼 ×
2𝑜) |
71 | 70 | a1i 11 |
. . 3
⊢ ((𝐼 ∈ 𝑉 ∧ 𝑥 ∈ Word (𝐼 × 2𝑜)) →
(𝑦 ∈ 𝐼, 𝑧 ∈ 2𝑜 ↦
〈𝑦,
(1𝑜 ∖ 𝑧)〉):(𝐼 ×
2𝑜)⟶(𝐼 ×
2𝑜)) |
72 | | wrdco 13428 |
. . 3
⊢
(((reverse‘𝑥)
∈ Word (𝐼 ×
2𝑜) ∧ (𝑦 ∈ 𝐼, 𝑧 ∈ 2𝑜 ↦
〈𝑦,
(1𝑜 ∖ 𝑧)〉):(𝐼 ×
2𝑜)⟶(𝐼 × 2𝑜)) →
((𝑦 ∈ 𝐼, 𝑧 ∈ 2𝑜 ↦
〈𝑦,
(1𝑜 ∖ 𝑧)〉) ∘ (reverse‘𝑥)) ∈ Word (𝐼 ×
2𝑜)) |
73 | 68, 71, 72 | syl2anc 691 |
. 2
⊢ ((𝐼 ∈ 𝑉 ∧ 𝑥 ∈ Word (𝐼 × 2𝑜)) →
((𝑦 ∈ 𝐼, 𝑧 ∈ 2𝑜 ↦
〈𝑦,
(1𝑜 ∖ 𝑧)〉) ∘ (reverse‘𝑥)) ∈ Word (𝐼 ×
2𝑜)) |
74 | 11 | adantr 480 |
. . . . 5
⊢ ((𝐼 ∈ 𝑉 ∧ 𝑥 ∈ Word (𝐼 × 2𝑜)) → Word
(𝐼 ×
2𝑜) = (Base‘(freeMnd‘(𝐼 ×
2𝑜)))) |
75 | 73, 74 | eleqtrd 2690 |
. . . 4
⊢ ((𝐼 ∈ 𝑉 ∧ 𝑥 ∈ Word (𝐼 × 2𝑜)) →
((𝑦 ∈ 𝐼, 𝑧 ∈ 2𝑜 ↦
〈𝑦,
(1𝑜 ∖ 𝑧)〉) ∘ (reverse‘𝑥)) ∈
(Base‘(freeMnd‘(𝐼 ×
2𝑜)))) |
76 | 2, 8, 23 | frmdadd 17215 |
. . . 4
⊢ ((((𝑦 ∈ 𝐼, 𝑧 ∈ 2𝑜 ↦
〈𝑦,
(1𝑜 ∖ 𝑧)〉) ∘ (reverse‘𝑥)) ∈
(Base‘(freeMnd‘(𝐼 × 2𝑜))) ∧
𝑥 ∈
(Base‘(freeMnd‘(𝐼 × 2𝑜)))) →
(((𝑦 ∈ 𝐼, 𝑧 ∈ 2𝑜 ↦
〈𝑦,
(1𝑜 ∖ 𝑧)〉) ∘ (reverse‘𝑥))(+g‘(freeMnd‘(𝐼 ×
2𝑜)))𝑥)
= (((𝑦 ∈ 𝐼, 𝑧 ∈ 2𝑜 ↦
〈𝑦,
(1𝑜 ∖ 𝑧)〉) ∘ (reverse‘𝑥)) ++ 𝑥)) |
77 | 75, 57, 76 | syl2anc 691 |
. . 3
⊢ ((𝐼 ∈ 𝑉 ∧ 𝑥 ∈ Word (𝐼 × 2𝑜)) →
(((𝑦 ∈ 𝐼, 𝑧 ∈ 2𝑜 ↦
〈𝑦,
(1𝑜 ∖ 𝑧)〉) ∘ (reverse‘𝑥))(+g‘(freeMnd‘(𝐼 ×
2𝑜)))𝑥)
= (((𝑦 ∈ 𝐼, 𝑧 ∈ 2𝑜 ↦
〈𝑦,
(1𝑜 ∖ 𝑧)〉) ∘ (reverse‘𝑥)) ++ 𝑥)) |
78 | 17 | eleq2d 2673 |
. . . . 5
⊢ (𝐼 ∈ 𝑉 → (𝑥 ∈ ( I ‘Word (𝐼 × 2𝑜)) ↔
𝑥 ∈ Word (𝐼 ×
2𝑜))) |
79 | 78 | biimpar 501 |
. . . 4
⊢ ((𝐼 ∈ 𝑉 ∧ 𝑥 ∈ Word (𝐼 × 2𝑜)) →
𝑥 ∈ ( I ‘Word
(𝐼 ×
2𝑜))) |
80 | | eqid 2610 |
. . . . 5
⊢ (𝑣 ∈ ( I ‘Word (𝐼 × 2𝑜))
↦ (𝑛 ∈
(0...(#‘𝑣)), 𝑤 ∈ (𝐼 × 2𝑜) ↦
(𝑣 splice 〈𝑛, 𝑛, 〈“𝑤((𝑦 ∈ 𝐼, 𝑧 ∈ 2𝑜 ↦
〈𝑦,
(1𝑜 ∖ 𝑧)〉)‘𝑤)”〉〉))) = (𝑣 ∈ ( I ‘Word (𝐼 × 2𝑜)) ↦
(𝑛 ∈
(0...(#‘𝑣)), 𝑤 ∈ (𝐼 × 2𝑜) ↦
(𝑣 splice 〈𝑛, 𝑛, 〈“𝑤((𝑦 ∈ 𝐼, 𝑧 ∈ 2𝑜 ↦
〈𝑦,
(1𝑜 ∖ 𝑧)〉)‘𝑤)”〉〉))) |
81 | 13, 3, 69, 80 | efginvrel1 17964 |
. . . 4
⊢ (𝑥 ∈ ( I ‘Word (𝐼 × 2𝑜))
→ (((𝑦 ∈ 𝐼, 𝑧 ∈ 2𝑜 ↦
〈𝑦,
(1𝑜 ∖ 𝑧)〉) ∘ (reverse‘𝑥)) ++ 𝑥) ∼
∅) |
82 | 79, 81 | syl 17 |
. . 3
⊢ ((𝐼 ∈ 𝑉 ∧ 𝑥 ∈ Word (𝐼 × 2𝑜)) →
(((𝑦 ∈ 𝐼, 𝑧 ∈ 2𝑜 ↦
〈𝑦,
(1𝑜 ∖ 𝑧)〉) ∘ (reverse‘𝑥)) ++ 𝑥) ∼
∅) |
83 | 77, 82 | eqbrtrd 4605 |
. 2
⊢ ((𝐼 ∈ 𝑉 ∧ 𝑥 ∈ Word (𝐼 × 2𝑜)) →
(((𝑦 ∈ 𝐼, 𝑧 ∈ 2𝑜 ↦
〈𝑦,
(1𝑜 ∖ 𝑧)〉) ∘ (reverse‘𝑥))(+g‘(freeMnd‘(𝐼 ×
2𝑜)))𝑥)
∼
∅) |
84 | 4, 11, 12, 20, 22, 25, 36, 51, 53, 66, 73, 83 | qusgrp2 17356 |
1
⊢ (𝐼 ∈ 𝑉 → (𝐺 ∈ Grp ∧ [∅] ∼ =
(0g‘𝐺))) |