Step | Hyp | Ref
| Expression |
1 | | frgp0.m |
. . 3
⊢ 𝐺 = (freeGrp‘𝐼) |
2 | | eqid 2622 |
. . 3
⊢
(freeMnd‘(𝐼
× 2𝑜)) = (freeMnd‘(𝐼 ×
2𝑜)) |
3 | | frgp0.r |
. . 3
⊢ ∼ = (
~FG ‘𝐼) |
4 | 1, 2, 3 | frgpval 18171 |
. 2
⊢ (𝐼 ∈ 𝑉 → 𝐺 = ((freeMnd‘(𝐼 × 2𝑜))
/s ∼ )) |
5 | | 2on 7568 |
. . . . 5
⊢
2𝑜 ∈ On |
6 | | xpexg 6960 |
. . . . 5
⊢ ((𝐼 ∈ 𝑉 ∧ 2𝑜 ∈ On)
→ (𝐼 ×
2𝑜) ∈ V) |
7 | 5, 6 | mpan2 707 |
. . . 4
⊢ (𝐼 ∈ 𝑉 → (𝐼 × 2𝑜) ∈
V) |
8 | | eqid 2622 |
. . . . 5
⊢
(Base‘(freeMnd‘(𝐼 × 2𝑜))) =
(Base‘(freeMnd‘(𝐼 ×
2𝑜))) |
9 | 2, 8 | frmdbas 17389 |
. . . 4
⊢ ((𝐼 × 2𝑜)
∈ V → (Base‘(freeMnd‘(𝐼 × 2𝑜))) = Word
(𝐼 ×
2𝑜)) |
10 | 7, 9 | syl 17 |
. . 3
⊢ (𝐼 ∈ 𝑉 → (Base‘(freeMnd‘(𝐼 ×
2𝑜))) = Word (𝐼 ×
2𝑜)) |
11 | 10 | eqcomd 2628 |
. 2
⊢ (𝐼 ∈ 𝑉 → Word (𝐼 × 2𝑜) =
(Base‘(freeMnd‘(𝐼 ×
2𝑜)))) |
12 | | eqidd 2623 |
. 2
⊢ (𝐼 ∈ 𝑉 →
(+g‘(freeMnd‘(𝐼 × 2𝑜))) =
(+g‘(freeMnd‘(𝐼 ×
2𝑜)))) |
13 | | eqid 2622 |
. . . 4
⊢ ( I
‘Word (𝐼 ×
2𝑜)) = ( I ‘Word (𝐼 ×
2𝑜)) |
14 | 13, 3 | efger 18131 |
. . 3
⊢ ∼ Er ( I
‘Word (𝐼 ×
2𝑜)) |
15 | | wrdexg 13315 |
. . . . 5
⊢ ((𝐼 × 2𝑜)
∈ V → Word (𝐼
× 2𝑜) ∈ V) |
16 | | fvi 6255 |
. . . . 5
⊢ (Word
(𝐼 ×
2𝑜) ∈ V → ( I ‘Word (𝐼 × 2𝑜)) = Word
(𝐼 ×
2𝑜)) |
17 | 7, 15, 16 | 3syl 18 |
. . . 4
⊢ (𝐼 ∈ 𝑉 → ( I ‘Word (𝐼 × 2𝑜)) = Word
(𝐼 ×
2𝑜)) |
18 | | ereq2 7750 |
. . . 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 223 |
. 2
⊢ (𝐼 ∈ 𝑉 → ∼ Er Word (𝐼 ×
2𝑜)) |
21 | | fvexd 6203 |
. 2
⊢ (𝐼 ∈ 𝑉 → (freeMnd‘(𝐼 × 2𝑜)) ∈
V) |
22 | | eqid 2622 |
. . . 4
⊢
(+g‘(freeMnd‘(𝐼 × 2𝑜))) =
(+g‘(freeMnd‘(𝐼 ×
2𝑜))) |
23 | 1, 2, 3, 22 | frgpcpbl 18172 |
. . 3
⊢ ((𝑎 ∼ 𝑏 ∧ 𝑐 ∼ 𝑑) → (𝑎(+g‘(freeMnd‘(𝐼 ×
2𝑜)))𝑐)
∼
(𝑏(+g‘(freeMnd‘(𝐼 ×
2𝑜)))𝑑)) |
24 | 23 | a1i 11 |
. 2
⊢ (𝐼 ∈ 𝑉 → ((𝑎 ∼ 𝑏 ∧ 𝑐 ∼ 𝑑) → (𝑎(+g‘(freeMnd‘(𝐼 ×
2𝑜)))𝑐)
∼
(𝑏(+g‘(freeMnd‘(𝐼 ×
2𝑜)))𝑑))) |
25 | 2 | frmdmnd 17396 |
. . . . . 6
⊢ ((𝐼 × 2𝑜)
∈ V → (freeMnd‘(𝐼 × 2𝑜)) ∈
Mnd) |
26 | 7, 25 | syl 17 |
. . . . 5
⊢ (𝐼 ∈ 𝑉 → (freeMnd‘(𝐼 × 2𝑜)) ∈
Mnd) |
27 | 26 | 3ad2ant1 1082 |
. . . 4
⊢ ((𝐼 ∈ 𝑉 ∧ 𝑥 ∈ Word (𝐼 × 2𝑜) ∧ 𝑦 ∈ Word (𝐼 × 2𝑜)) →
(freeMnd‘(𝐼 ×
2𝑜)) ∈ Mnd) |
28 | | simp2 1062 |
. . . . 5
⊢ ((𝐼 ∈ 𝑉 ∧ 𝑥 ∈ Word (𝐼 × 2𝑜) ∧ 𝑦 ∈ Word (𝐼 × 2𝑜)) →
𝑥 ∈ Word (𝐼 ×
2𝑜)) |
29 | 11 | 3ad2ant1 1082 |
. . . . 5
⊢ ((𝐼 ∈ 𝑉 ∧ 𝑥 ∈ Word (𝐼 × 2𝑜) ∧ 𝑦 ∈ Word (𝐼 × 2𝑜)) → Word
(𝐼 ×
2𝑜) = (Base‘(freeMnd‘(𝐼 ×
2𝑜)))) |
30 | 28, 29 | eleqtrd 2703 |
. . . 4
⊢ ((𝐼 ∈ 𝑉 ∧ 𝑥 ∈ Word (𝐼 × 2𝑜) ∧ 𝑦 ∈ Word (𝐼 × 2𝑜)) →
𝑥 ∈
(Base‘(freeMnd‘(𝐼 ×
2𝑜)))) |
31 | | simp3 1063 |
. . . . 5
⊢ ((𝐼 ∈ 𝑉 ∧ 𝑥 ∈ Word (𝐼 × 2𝑜) ∧ 𝑦 ∈ Word (𝐼 × 2𝑜)) →
𝑦 ∈ Word (𝐼 ×
2𝑜)) |
32 | 31, 29 | eleqtrd 2703 |
. . . 4
⊢ ((𝐼 ∈ 𝑉 ∧ 𝑥 ∈ Word (𝐼 × 2𝑜) ∧ 𝑦 ∈ Word (𝐼 × 2𝑜)) →
𝑦 ∈
(Base‘(freeMnd‘(𝐼 ×
2𝑜)))) |
33 | 8, 22 | mndcl 17301 |
. . . 4
⊢
(((freeMnd‘(𝐼
× 2𝑜)) ∈ Mnd ∧ 𝑥 ∈ (Base‘(freeMnd‘(𝐼 ×
2𝑜))) ∧ 𝑦 ∈ (Base‘(freeMnd‘(𝐼 ×
2𝑜)))) → (𝑥(+g‘(freeMnd‘(𝐼 ×
2𝑜)))𝑦)
∈ (Base‘(freeMnd‘(𝐼 ×
2𝑜)))) |
34 | 27, 30, 32, 33 | syl3anc 1326 |
. . 3
⊢ ((𝐼 ∈ 𝑉 ∧ 𝑥 ∈ Word (𝐼 × 2𝑜) ∧ 𝑦 ∈ Word (𝐼 × 2𝑜)) →
(𝑥(+g‘(freeMnd‘(𝐼 ×
2𝑜)))𝑦)
∈ (Base‘(freeMnd‘(𝐼 ×
2𝑜)))) |
35 | 34, 29 | eleqtrrd 2704 |
. 2
⊢ ((𝐼 ∈ 𝑉 ∧ 𝑥 ∈ Word (𝐼 × 2𝑜) ∧ 𝑦 ∈ Word (𝐼 × 2𝑜)) →
(𝑥(+g‘(freeMnd‘(𝐼 ×
2𝑜)))𝑦)
∈ Word (𝐼 ×
2𝑜)) |
36 | 20 | adantr 481 |
. . . 4
⊢ ((𝐼 ∈ 𝑉 ∧ (𝑥 ∈ Word (𝐼 × 2𝑜) ∧ 𝑦 ∈ Word (𝐼 × 2𝑜) ∧ 𝑧 ∈ Word (𝐼 × 2𝑜))) →
∼
Er Word (𝐼 ×
2𝑜)) |
37 | 26 | adantr 481 |
. . . . . 6
⊢ ((𝐼 ∈ 𝑉 ∧ (𝑥 ∈ Word (𝐼 × 2𝑜) ∧ 𝑦 ∈ Word (𝐼 × 2𝑜) ∧ 𝑧 ∈ Word (𝐼 × 2𝑜))) →
(freeMnd‘(𝐼 ×
2𝑜)) ∈ Mnd) |
38 | 34 | 3adant3r3 1276 |
. . . . . 6
⊢ ((𝐼 ∈ 𝑉 ∧ (𝑥 ∈ Word (𝐼 × 2𝑜) ∧ 𝑦 ∈ Word (𝐼 × 2𝑜) ∧ 𝑧 ∈ Word (𝐼 × 2𝑜))) →
(𝑥(+g‘(freeMnd‘(𝐼 ×
2𝑜)))𝑦)
∈ (Base‘(freeMnd‘(𝐼 ×
2𝑜)))) |
39 | | simpr3 1069 |
. . . . . . 7
⊢ ((𝐼 ∈ 𝑉 ∧ (𝑥 ∈ Word (𝐼 × 2𝑜) ∧ 𝑦 ∈ Word (𝐼 × 2𝑜) ∧ 𝑧 ∈ Word (𝐼 × 2𝑜))) →
𝑧 ∈ Word (𝐼 ×
2𝑜)) |
40 | 11 | adantr 481 |
. . . . . . 7
⊢ ((𝐼 ∈ 𝑉 ∧ (𝑥 ∈ Word (𝐼 × 2𝑜) ∧ 𝑦 ∈ Word (𝐼 × 2𝑜) ∧ 𝑧 ∈ Word (𝐼 × 2𝑜))) →
Word (𝐼 ×
2𝑜) = (Base‘(freeMnd‘(𝐼 ×
2𝑜)))) |
41 | 39, 40 | eleqtrd 2703 |
. . . . . 6
⊢ ((𝐼 ∈ 𝑉 ∧ (𝑥 ∈ Word (𝐼 × 2𝑜) ∧ 𝑦 ∈ Word (𝐼 × 2𝑜) ∧ 𝑧 ∈ Word (𝐼 × 2𝑜))) →
𝑧 ∈
(Base‘(freeMnd‘(𝐼 ×
2𝑜)))) |
42 | 8, 22 | mndcl 17301 |
. . . . . 6
⊢
(((freeMnd‘(𝐼
× 2𝑜)) ∈ Mnd ∧ (𝑥(+g‘(freeMnd‘(𝐼 ×
2𝑜)))𝑦)
∈ (Base‘(freeMnd‘(𝐼 × 2𝑜))) ∧
𝑧 ∈
(Base‘(freeMnd‘(𝐼 × 2𝑜)))) →
((𝑥(+g‘(freeMnd‘(𝐼 ×
2𝑜)))𝑦)(+g‘(freeMnd‘(𝐼 ×
2𝑜)))𝑧)
∈ (Base‘(freeMnd‘(𝐼 ×
2𝑜)))) |
43 | 37, 38, 41, 42 | syl3anc 1326 |
. . . . 5
⊢ ((𝐼 ∈ 𝑉 ∧ (𝑥 ∈ Word (𝐼 × 2𝑜) ∧ 𝑦 ∈ Word (𝐼 × 2𝑜) ∧ 𝑧 ∈ Word (𝐼 × 2𝑜))) →
((𝑥(+g‘(freeMnd‘(𝐼 ×
2𝑜)))𝑦)(+g‘(freeMnd‘(𝐼 ×
2𝑜)))𝑧)
∈ (Base‘(freeMnd‘(𝐼 ×
2𝑜)))) |
44 | 43, 40 | eleqtrrd 2704 |
. . . 4
⊢ ((𝐼 ∈ 𝑉 ∧ (𝑥 ∈ Word (𝐼 × 2𝑜) ∧ 𝑦 ∈ Word (𝐼 × 2𝑜) ∧ 𝑧 ∈ Word (𝐼 × 2𝑜))) →
((𝑥(+g‘(freeMnd‘(𝐼 ×
2𝑜)))𝑦)(+g‘(freeMnd‘(𝐼 ×
2𝑜)))𝑧)
∈ Word (𝐼 ×
2𝑜)) |
45 | 36, 44 | erref 7762 |
. . 3
⊢ ((𝐼 ∈ 𝑉 ∧ (𝑥 ∈ Word (𝐼 × 2𝑜) ∧ 𝑦 ∈ Word (𝐼 × 2𝑜) ∧ 𝑧 ∈ Word (𝐼 × 2𝑜))) →
((𝑥(+g‘(freeMnd‘(𝐼 ×
2𝑜)))𝑦)(+g‘(freeMnd‘(𝐼 ×
2𝑜)))𝑧)
∼
((𝑥(+g‘(freeMnd‘(𝐼 ×
2𝑜)))𝑦)(+g‘(freeMnd‘(𝐼 ×
2𝑜)))𝑧)) |
46 | 30 | 3adant3r3 1276 |
. . . 4
⊢ ((𝐼 ∈ 𝑉 ∧ (𝑥 ∈ Word (𝐼 × 2𝑜) ∧ 𝑦 ∈ Word (𝐼 × 2𝑜) ∧ 𝑧 ∈ Word (𝐼 × 2𝑜))) →
𝑥 ∈
(Base‘(freeMnd‘(𝐼 ×
2𝑜)))) |
47 | 32 | 3adant3r3 1276 |
. . . 4
⊢ ((𝐼 ∈ 𝑉 ∧ (𝑥 ∈ Word (𝐼 × 2𝑜) ∧ 𝑦 ∈ Word (𝐼 × 2𝑜) ∧ 𝑧 ∈ Word (𝐼 × 2𝑜))) →
𝑦 ∈
(Base‘(freeMnd‘(𝐼 ×
2𝑜)))) |
48 | 8, 22 | mndass 17302 |
. . . 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𝑜)))𝑧))) |
49 | 37, 46, 47, 41, 48 | syl13anc 1328 |
. . 3
⊢ ((𝐼 ∈ 𝑉 ∧ (𝑥 ∈ Word (𝐼 × 2𝑜) ∧ 𝑦 ∈ Word (𝐼 × 2𝑜) ∧ 𝑧 ∈ Word (𝐼 × 2𝑜))) →
((𝑥(+g‘(freeMnd‘(𝐼 ×
2𝑜)))𝑦)(+g‘(freeMnd‘(𝐼 ×
2𝑜)))𝑧)
= (𝑥(+g‘(freeMnd‘(𝐼 ×
2𝑜)))(𝑦(+g‘(freeMnd‘(𝐼 ×
2𝑜)))𝑧))) |
50 | 45, 49 | breqtrd 4679 |
. 2
⊢ ((𝐼 ∈ 𝑉 ∧ (𝑥 ∈ Word (𝐼 × 2𝑜) ∧ 𝑦 ∈ Word (𝐼 × 2𝑜) ∧ 𝑧 ∈ Word (𝐼 × 2𝑜))) →
((𝑥(+g‘(freeMnd‘(𝐼 ×
2𝑜)))𝑦)(+g‘(freeMnd‘(𝐼 ×
2𝑜)))𝑧)
∼
(𝑥(+g‘(freeMnd‘(𝐼 ×
2𝑜)))(𝑦(+g‘(freeMnd‘(𝐼 ×
2𝑜)))𝑧))) |
51 | | wrd0 13330 |
. . 3
⊢ ∅
∈ Word (𝐼 ×
2𝑜) |
52 | 51 | a1i 11 |
. 2
⊢ (𝐼 ∈ 𝑉 → ∅ ∈ Word (𝐼 ×
2𝑜)) |
53 | 51, 11 | syl5eleq 2707 |
. . . . . 6
⊢ (𝐼 ∈ 𝑉 → ∅ ∈
(Base‘(freeMnd‘(𝐼 ×
2𝑜)))) |
54 | 53 | adantr 481 |
. . . . 5
⊢ ((𝐼 ∈ 𝑉 ∧ 𝑥 ∈ Word (𝐼 × 2𝑜)) →
∅ ∈ (Base‘(freeMnd‘(𝐼 ×
2𝑜)))) |
55 | 11 | eleq2d 2687 |
. . . . . 6
⊢ (𝐼 ∈ 𝑉 → (𝑥 ∈ Word (𝐼 × 2𝑜) ↔ 𝑥 ∈
(Base‘(freeMnd‘(𝐼 ×
2𝑜))))) |
56 | 55 | biimpa 501 |
. . . . 5
⊢ ((𝐼 ∈ 𝑉 ∧ 𝑥 ∈ Word (𝐼 × 2𝑜)) →
𝑥 ∈
(Base‘(freeMnd‘(𝐼 ×
2𝑜)))) |
57 | 2, 8, 22 | frmdadd 17392 |
. . . . 5
⊢ ((∅
∈ (Base‘(freeMnd‘(𝐼 × 2𝑜))) ∧
𝑥 ∈
(Base‘(freeMnd‘(𝐼 × 2𝑜)))) →
(∅(+g‘(freeMnd‘(𝐼 × 2𝑜)))𝑥) = (∅ ++ 𝑥)) |
58 | 54, 56, 57 | syl2anc 693 |
. . . 4
⊢ ((𝐼 ∈ 𝑉 ∧ 𝑥 ∈ Word (𝐼 × 2𝑜)) →
(∅(+g‘(freeMnd‘(𝐼 × 2𝑜)))𝑥) = (∅ ++ 𝑥)) |
59 | | ccatlid 13369 |
. . . . 5
⊢ (𝑥 ∈ Word (𝐼 × 2𝑜) →
(∅ ++ 𝑥) = 𝑥) |
60 | 59 | adantl 482 |
. . . 4
⊢ ((𝐼 ∈ 𝑉 ∧ 𝑥 ∈ Word (𝐼 × 2𝑜)) →
(∅ ++ 𝑥) = 𝑥) |
61 | 58, 60 | eqtrd 2656 |
. . 3
⊢ ((𝐼 ∈ 𝑉 ∧ 𝑥 ∈ Word (𝐼 × 2𝑜)) →
(∅(+g‘(freeMnd‘(𝐼 × 2𝑜)))𝑥) = 𝑥) |
62 | 20 | adantr 481 |
. . . 4
⊢ ((𝐼 ∈ 𝑉 ∧ 𝑥 ∈ Word (𝐼 × 2𝑜)) →
∼
Er Word (𝐼 ×
2𝑜)) |
63 | | simpr 477 |
. . . 4
⊢ ((𝐼 ∈ 𝑉 ∧ 𝑥 ∈ Word (𝐼 × 2𝑜)) →
𝑥 ∈ Word (𝐼 ×
2𝑜)) |
64 | 62, 63 | erref 7762 |
. . 3
⊢ ((𝐼 ∈ 𝑉 ∧ 𝑥 ∈ Word (𝐼 × 2𝑜)) →
𝑥 ∼ 𝑥) |
65 | 61, 64 | eqbrtrd 4675 |
. 2
⊢ ((𝐼 ∈ 𝑉 ∧ 𝑥 ∈ Word (𝐼 × 2𝑜)) →
(∅(+g‘(freeMnd‘(𝐼 × 2𝑜)))𝑥) ∼ 𝑥) |
66 | | revcl 13510 |
. . . 4
⊢ (𝑥 ∈ Word (𝐼 × 2𝑜) →
(reverse‘𝑥) ∈
Word (𝐼 ×
2𝑜)) |
67 | 66 | adantl 482 |
. . 3
⊢ ((𝐼 ∈ 𝑉 ∧ 𝑥 ∈ Word (𝐼 × 2𝑜)) →
(reverse‘𝑥) ∈
Word (𝐼 ×
2𝑜)) |
68 | | eqid 2622 |
. . . . 5
⊢ (𝑦 ∈ 𝐼, 𝑧 ∈ 2𝑜 ↦
〈𝑦,
(1𝑜 ∖ 𝑧)〉) = (𝑦 ∈ 𝐼, 𝑧 ∈ 2𝑜 ↦
〈𝑦,
(1𝑜 ∖ 𝑧)〉) |
69 | 68 | efgmf 18126 |
. . . 4
⊢ (𝑦 ∈ 𝐼, 𝑧 ∈ 2𝑜 ↦
〈𝑦,
(1𝑜 ∖ 𝑧)〉):(𝐼 ×
2𝑜)⟶(𝐼 ×
2𝑜) |
70 | 69 | a1i 11 |
. . 3
⊢ ((𝐼 ∈ 𝑉 ∧ 𝑥 ∈ Word (𝐼 × 2𝑜)) →
(𝑦 ∈ 𝐼, 𝑧 ∈ 2𝑜 ↦
〈𝑦,
(1𝑜 ∖ 𝑧)〉):(𝐼 ×
2𝑜)⟶(𝐼 ×
2𝑜)) |
71 | | wrdco 13577 |
. . 3
⊢
(((reverse‘𝑥)
∈ Word (𝐼 ×
2𝑜) ∧ (𝑦 ∈ 𝐼, 𝑧 ∈ 2𝑜 ↦
〈𝑦,
(1𝑜 ∖ 𝑧)〉):(𝐼 ×
2𝑜)⟶(𝐼 × 2𝑜)) →
((𝑦 ∈ 𝐼, 𝑧 ∈ 2𝑜 ↦
〈𝑦,
(1𝑜 ∖ 𝑧)〉) ∘ (reverse‘𝑥)) ∈ Word (𝐼 ×
2𝑜)) |
72 | 67, 70, 71 | syl2anc 693 |
. 2
⊢ ((𝐼 ∈ 𝑉 ∧ 𝑥 ∈ Word (𝐼 × 2𝑜)) →
((𝑦 ∈ 𝐼, 𝑧 ∈ 2𝑜 ↦
〈𝑦,
(1𝑜 ∖ 𝑧)〉) ∘ (reverse‘𝑥)) ∈ Word (𝐼 ×
2𝑜)) |
73 | 11 | adantr 481 |
. . . . 5
⊢ ((𝐼 ∈ 𝑉 ∧ 𝑥 ∈ Word (𝐼 × 2𝑜)) → Word
(𝐼 ×
2𝑜) = (Base‘(freeMnd‘(𝐼 ×
2𝑜)))) |
74 | 72, 73 | eleqtrd 2703 |
. . . 4
⊢ ((𝐼 ∈ 𝑉 ∧ 𝑥 ∈ Word (𝐼 × 2𝑜)) →
((𝑦 ∈ 𝐼, 𝑧 ∈ 2𝑜 ↦
〈𝑦,
(1𝑜 ∖ 𝑧)〉) ∘ (reverse‘𝑥)) ∈
(Base‘(freeMnd‘(𝐼 ×
2𝑜)))) |
75 | 2, 8, 22 | frmdadd 17392 |
. . . 4
⊢ ((((𝑦 ∈ 𝐼, 𝑧 ∈ 2𝑜 ↦
〈𝑦,
(1𝑜 ∖ 𝑧)〉) ∘ (reverse‘𝑥)) ∈
(Base‘(freeMnd‘(𝐼 × 2𝑜))) ∧
𝑥 ∈
(Base‘(freeMnd‘(𝐼 × 2𝑜)))) →
(((𝑦 ∈ 𝐼, 𝑧 ∈ 2𝑜 ↦
〈𝑦,
(1𝑜 ∖ 𝑧)〉) ∘ (reverse‘𝑥))(+g‘(freeMnd‘(𝐼 ×
2𝑜)))𝑥)
= (((𝑦 ∈ 𝐼, 𝑧 ∈ 2𝑜 ↦
〈𝑦,
(1𝑜 ∖ 𝑧)〉) ∘ (reverse‘𝑥)) ++ 𝑥)) |
76 | 74, 56, 75 | syl2anc 693 |
. . 3
⊢ ((𝐼 ∈ 𝑉 ∧ 𝑥 ∈ Word (𝐼 × 2𝑜)) →
(((𝑦 ∈ 𝐼, 𝑧 ∈ 2𝑜 ↦
〈𝑦,
(1𝑜 ∖ 𝑧)〉) ∘ (reverse‘𝑥))(+g‘(freeMnd‘(𝐼 ×
2𝑜)))𝑥)
= (((𝑦 ∈ 𝐼, 𝑧 ∈ 2𝑜 ↦
〈𝑦,
(1𝑜 ∖ 𝑧)〉) ∘ (reverse‘𝑥)) ++ 𝑥)) |
77 | 17 | eleq2d 2687 |
. . . . 5
⊢ (𝐼 ∈ 𝑉 → (𝑥 ∈ ( I ‘Word (𝐼 × 2𝑜)) ↔
𝑥 ∈ Word (𝐼 ×
2𝑜))) |
78 | 77 | biimpar 502 |
. . . 4
⊢ ((𝐼 ∈ 𝑉 ∧ 𝑥 ∈ Word (𝐼 × 2𝑜)) →
𝑥 ∈ ( I ‘Word
(𝐼 ×
2𝑜))) |
79 | | eqid 2622 |
. . . . 5
⊢ (𝑣 ∈ ( I ‘Word (𝐼 × 2𝑜))
↦ (𝑛 ∈
(0...(#‘𝑣)), 𝑤 ∈ (𝐼 × 2𝑜) ↦
(𝑣 splice 〈𝑛, 𝑛, 〈“𝑤((𝑦 ∈ 𝐼, 𝑧 ∈ 2𝑜 ↦
〈𝑦,
(1𝑜 ∖ 𝑧)〉)‘𝑤)”〉〉))) = (𝑣 ∈ ( I ‘Word (𝐼 × 2𝑜)) ↦
(𝑛 ∈
(0...(#‘𝑣)), 𝑤 ∈ (𝐼 × 2𝑜) ↦
(𝑣 splice 〈𝑛, 𝑛, 〈“𝑤((𝑦 ∈ 𝐼, 𝑧 ∈ 2𝑜 ↦
〈𝑦,
(1𝑜 ∖ 𝑧)〉)‘𝑤)”〉〉))) |
80 | 13, 3, 68, 79 | efginvrel1 18141 |
. . . 4
⊢ (𝑥 ∈ ( I ‘Word (𝐼 × 2𝑜))
→ (((𝑦 ∈ 𝐼, 𝑧 ∈ 2𝑜 ↦
〈𝑦,
(1𝑜 ∖ 𝑧)〉) ∘ (reverse‘𝑥)) ++ 𝑥) ∼
∅) |
81 | 78, 80 | syl 17 |
. . 3
⊢ ((𝐼 ∈ 𝑉 ∧ 𝑥 ∈ Word (𝐼 × 2𝑜)) →
(((𝑦 ∈ 𝐼, 𝑧 ∈ 2𝑜 ↦
〈𝑦,
(1𝑜 ∖ 𝑧)〉) ∘ (reverse‘𝑥)) ++ 𝑥) ∼
∅) |
82 | 76, 81 | eqbrtrd 4675 |
. 2
⊢ ((𝐼 ∈ 𝑉 ∧ 𝑥 ∈ Word (𝐼 × 2𝑜)) →
(((𝑦 ∈ 𝐼, 𝑧 ∈ 2𝑜 ↦
〈𝑦,
(1𝑜 ∖ 𝑧)〉) ∘ (reverse‘𝑥))(+g‘(freeMnd‘(𝐼 ×
2𝑜)))𝑥)
∼
∅) |
83 | 4, 11, 12, 20, 21, 24, 35, 50, 52, 65, 72, 82 | qusgrp2 17533 |
1
⊢ (𝐼 ∈ 𝑉 → (𝐺 ∈ Grp ∧ [∅] ∼ =
(0g‘𝐺))) |